Is Quantified Boolean Formula (QBF) the same as First-order logic (FOL)?
$\begingroup$
$\endgroup$
1
-
$\begingroup$ This question should probably be moved to Theoretical Computer Science stack, since it involves theoretical aspects of comparing two formal systems and theory of computability. Especially, since it is fundamentally related to topics discussed in TCS stack and includes low-traffic tags, as noted here. Can you act upon this? $\endgroup$– ivchaCommented Oct 3, 2016 at 6:03
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
Firstly, a quantified Boolean formula is a formula in quantified propositional logic (which consists of Boolean variables and quantifiers). A true quantified Boolean formula is a formula that can be made true (formulas have no free variables so they can be either true or false). Note that this term is also used for the true quantified Boolean formulas (TQBF) language which contains all true Boolean qualified formulas. Therefore, you probably had a comparison of the respective logics in mind, namely quantified propositional logic and first-order logic.
To make a connection of quantified propositional logic and first-order logic, let us consider predicate logic (that is more general, and includes first-order logic). When comparing propositional logic and predicate logic, a basic difference is that the latter includes a richer ontology: objects, functions and predicates on objects. (This allows more flexible and compact representation of knowledge, as expressing a binary predicate on a set of n terms might lead to n*n terms in propositional logic.) Having this in mind, effectively, first-order logic and quantified propositional logic add quantification to propositional and predicate logic, respectively.
Consequently, from the perspective of the comparison of the formal systems represented by these two logics, one might consider their expressiveness. While quantified propositional logic is restricted to Boolean variables (that might hold either true or false), first-order logic does not have such restrictions. It can model different sets of objects (terms), together with predicates and functions on them (it is most widely used to express properties in wide range of mathematical theories). Therefore, strictly speaking, first-order logic is more expressive.
One important distinction between these logics is in terms of decidability. Namely, to check whether a formula in quantified propositional logic is true is decidable (the language TQBF is decidable; more specifically, it is PSPACE-complete). Unlike quantified propositional logic, first-order logic is undecidable if the language has at least one predicate of arity at least 2 (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. (This can be shown by encoding the statement "the Turing machine T halts on empty input", which is known to be undecidable, in first-order logic.)
Note that formulas in quantified propositional logic can be straightforwardly interpreted in first-order logic. (This is explained in more details in this answer.)
