Logic – Why Quantified Propositional Logic is Not First-Order Logic

logicpredicate-logic

If propositional logic is extended by quantifiers ($\forall$ and $\exists$) without adding functions and relations (or even objects and equality, i.e. we quantify over propositional-variables), the result could be called quantified propositional logic. This system is more expressive than propositional logic (the true quantified Boolean formulas are a PSPACE-complete language), but less expressive than first-order logic. Because first-order logic is sometimes considered as "the true logic", I find it interesting that it doesn't include this subsystem. (Second-order logic on the other hand includes it as a subsystem.)

Note: Even so this question is similar to another question about omitting parts of first order logic, the motivation behind this question is different. It arose by considerations about the relation between constants and variables (and why there are "only" countably many different variables), and that there should be a similar relation between propositions and propositional-variables. (A related question would be "how many different variables/propositional-variables are required for deducing all consequences from a given set of axioms".)

Best Answer

This system of quantified propositional logic is straightforward to interpret into first-order logic. We make a theory $T$ that has a single, unary relation symbol, say $P$, and no other symbols in the signature, not even equality. Then, to quantify over "propositional variables", we quantify over elements in first order logic as usual. For each element $x$ in a model of $T$, $Px$ is either true or false, so the elements of the model can be treated as if they were propositional variables.

Thus the quantified propositional sentence $(\exists Q)(\forall R)[R \lor Q]$ is interpreted into $T$ as $(\exists q)(\forall r)[Pr \lor Pq]$. In this way, every sentence of quantified propositional logic is interpreted as a sentence of $T$, and vice-versa.

If we wanted to add constant symbols to $T$, that would be equivalent to adding constant (i.e. non-variable) propositional variables to quantified propositional logic.

I would suggest that the main reason that we don't bother having quantified propositional variables in the "usual" framework for first-order logic is that they are not useful for formalizing the typical mathematical theories (group theory, linear orders, set theory, arithmetic, etc.), and a central goal in most presentations of first-order logic is to be able to formalize these theories. The same holds for $\lambda$ terms to define functions. There is no reason that they could not be included in first-order theories, and in fact they sometimes are, but most presentations have no use for them.

Related Question