4
$\begingroup$

I'm working through Marker's (Model Theory: An Introduction) presentation of quantifier elimination. Things get a bit awkward with the use of formulas like $x_1 = x_1$ to represent truth, and $x_1 \neq x_1$ to represent falsehood. Is there any reason not to just introduce propositional constants representing truth and falsehood as part of the boolean logic of a language in model theory?

That is, to allow $T$ and $F$ as first order logical formulas where $T$ is interpreted as always true and $F$ is interpreted as always false.

Does anything break? Does this make any proofs more complicated? It seems like adding these makes the presentation of quantifier elimination easier: if one starts with a formula with no free variables and one quantifier and then eliminates that quantifier one should be left with either $T$ or $F$, and a good quantifier elimination algorithm should naturally handle this sort of special case.

$\endgroup$
2
  • 1
    $\begingroup$ I'm not a specialist, but I find that representing truth by $x_1=x_1$ (for example), makes it more evident for when we want to explicitly prove the equivalence between the original and the quantifier-free formula, especially the right-to-left implication. I don't think there would be an issue with what you are saying though, but again, I am no expert. $\endgroup$
    – davinci_07
    Feb 2, 2023 at 7:09
  • $\begingroup$ It's just one of the minimization hobbies of logicians $\endgroup$
    – Trebor
    Feb 5, 2023 at 3:13

1 Answer 1

3
$\begingroup$

You're exactly right: nothing breaks if we include "true" and "false" as formulas (usually denoted $\top$ and $\bot$), and I think a number of things are simpler with this convention. My notes on model theory here develop all the basics, including quantifier elimination, in a setting where first-order logic includes $\top$ and $\bot$.

$\endgroup$
2
  • $\begingroup$ I would stress you MUST include some logic constant if you want QE in, e.g., $\mathbb Q,<$. Otherwise there would be no qf equivalent of $\forall x\ x=x$ $\endgroup$ Feb 5, 2023 at 14:52
  • $\begingroup$ @PrimoPetri I agree with you! But if you look carefully at a lot of sources (e.g. Marker or Chang & Keisler), they allow things like saying $\forall x\, x = x$ is equivalent to the quantifier-free formula $y = y$. I think the correct definition of quantifier elimination should say that every formula is equivalent to a quantifier-free formula in the same variable context (with the same variables appearing free), and for this, yes, you need to include a logical constant for theories like DLO that don't have constant symbols. $\endgroup$ Feb 5, 2023 at 15:52

You must log in to answer this question.

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