# Why not add boolean constants to first order logic in model theory?

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.

• 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. Feb 2, 2023 at 7:09
• It's just one of the minimization hobbies of logicians Feb 5, 2023 at 3:13

## 1 Answer

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$$.

• 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$ Feb 5, 2023 at 14:52
• @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. Feb 5, 2023 at 15:52