8
$\begingroup$

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".)

$\endgroup$
8
  • $\begingroup$ What are you quantifying over? $\endgroup$
    – Chris Eagle
    Mar 25, 2013 at 0:01
  • $\begingroup$ @ChrisEagle Good point. I edited the question to clarify that I quantify over propositional-variables, and that the intended language doesn't even contain objects and equality. $\endgroup$
    – Thomas Klimpel
    Mar 25, 2013 at 0:08
  • $\begingroup$ In my opinion the best way to understand quantified propositional logic is to realize that this is exactly the true first-sentences (sometimes it is only the prenex ones) in a particular first-order structure, which is the two-elements Boolean algebra. $\endgroup$
    – boumol
    Mar 25, 2013 at 9:51
  • $\begingroup$ Sorry for the misprint "first-sentences". In my last comment I meant "first-order sentences". $\endgroup$
    – boumol
    Mar 25, 2013 at 12:18
  • $\begingroup$ @boumol Regarding the misprint, sometimes comments can still be edited, and if it's too late for this, I sometimes post a new comment with fixed typos, and then delete the original comment. $\endgroup$
    – Thomas Klimpel
    Mar 26, 2013 at 18:08

1 Answer 1

Reset to default
6
$\begingroup$

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.

$\endgroup$
6
  • 1
    $\begingroup$ The proposed interpretation must be augmented by the two sentences $(\exists x)[P x]$ and $(\exists x) [\lnot P x]$. I guess this should be enough to make it work. I wasn't aware of this when I asked the question. I agree that having quantified propositional variables would only complicate most presentations of first-order logic without adding any benefit. But still, trying to add it to first-order logic might be an interesting excercise, because it requires certain extensions (or modifications) of the model relation and the deduction system. It probably also leads to some meta-theorems. $\endgroup$
    – Thomas Klimpel
    Mar 25, 2013 at 17:52
  • $\begingroup$ @Mummert: I believe it is more convenient to think the truth value of $(\exists Q)(\forall R)[R \lor Q]$ as the truth value the first-order sentence $(\exists q)(\forall r)[ (r \lor q) = 1]$ in the two-elements Boolean algebra. It is not necessary to consider any extra predicate. $\endgroup$
    – boumol
    Mar 25, 2013 at 18:04
  • $\begingroup$ @boumol: in that case, instead of adding an extra predicate, you are adding extra function symbols such as $\lor$ to the signature. After all the $\lor$ in your formula is not the "or" of first-order logic that connects formulas; it is a function symbol from the signature of boolean algebras. So, yes, you can avoid adding the extra predicate symbol by adding function symbols instead. $\endgroup$
    – Carl Mummert
    Mar 25, 2013 at 18:28
  • $\begingroup$ I would rather say you can avoid the extra predicate by considering the adequate signature for Boolean algebras (for sure you have functional symbols for join, meet, negation, etc.). From the set perspective the $\lor$ is an extra functional symbol, but from the perspective of a Boolean algebra this function (the join) is already given. $\endgroup$
    – boumol
    Mar 25, 2013 at 18:30
  • $\begingroup$ I misread your formula at first, but I think we agree. $\endgroup$
    – Carl Mummert
    Mar 25, 2013 at 18:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .