The Gateway to Computer Science Excellence
First time here? Checkout the FAQ!
+1 vote
Is satisfiability in FOL  undecidable or semidecidable?

asked in Theory of Computation by (121 points)
edited by | 32 views

1 Answer

+2 votes

Not Decidable. Not even Semidecidable.

As Wikipedia states :

The question whether a sentence in propositional logic is satisfiable is a decidable problem. In general, the question whether sentences in first-order logic are satisfiable is not decidable. 

Satisfiability in first-order logic is undecidable and indeed it isn't even a semidecidable property of formulae in first order logic (FOL).

I don't yet know the formal proof But In case you are interested in Proof then Refer here :

Satisfiability in Propositional Logic :

Satisfiability(SAT) is Standard NP-Complete Problem, Hence It is Decidable. Since, Every NP problem is Decidable. Actually, SAT is the first problem that was proven to be NP-Complete. Since, It is Decidable, It is Semi-decidable as well, Because Every Decidable problem is Semi-decidable.

More about SAT problem can be studied in Complexity Classes, which unfortunately is not in GATE syllabus. But worth learning for Knowledge' sake.(Or After GATE you can learn about it)

The Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to True. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is False for all possible variable assignments and the formula is unsatisfiable

answered by Boss (13.2k points)
edited by
For first order logic, what difference happens?
Oh Sorry..My bad. I answered for Propositional logic formulas.

Satisfiability in First Order logic is Not decidable.

Quick search syntax
tags tag:apple
author user:martin
title title:apple
content content:apple
exclude -tag:apple
force match +apple
views views:100
score score:10
answers answers:2
is accepted isaccepted:true
is closed isclosed:true

36,157 questions
43,608 answers
42,860 users