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