This web page provides another example of the method of Elimination of Quantifiers (QE), this time applied to the theory of where . The QE will be done more-or-less explicitly here: other web pages will introduce general model theoretic results that simplify such arguments.
We start looking at where , which for technical reasons is a little more straightforward to work with.
Definition.
Let be the first order language with unary function sysmbol and a constant . Let be the language with a further unary function . Let be the -theory with axioms
and let be the -theory with the above axioms together with
Exercise.
Both and are -categorical for each uncountable . They are therefore both complete (for their language).
It follows from the Exercise and the models in that and where and .
Theorem.
has Quantifier Elimination.
The proof is in several stages. We shall first show has QE and derive the theorem from this.
Consider a quantifier-free formula of
. We shall apply several reductions to the
atomic formulas in to simplify
it.
Our objectives are particularly to simplify the terms
involving in and to remove occurences
of or . In the
following, range over arbitrary terms of .
Now to prove QE. We argue inductively, eliminating quantifiers from successively complex formulas. Consider a formula . By induction we may assume that is already quantifier free. By applying the above reductions (especially the last two) we may assume that does not occur as an argument to a function symbol or . For such we can apply the result on disjunctive normal form (DNF) to find a quantifier free formula of the form equivalent to , where is either an atomic formula occuring in or is the negation of some such formula. We need to eliminate the quantifier from and since the and the commute here it suffices to show that each is equivalent to something that is quantifier free.
There are two cases. By the reductions already applied, the variable occurs as either or as in the . The first case we consider is when one of the statements is , without the not sign. In this case, we have no choice as to what element must be: it must be the element given by the term . Therefore if we replace by throughout we get an equivalent statement that contains no and hence there is no need for the quantifier.
The other case is when every occurence of is like . In this case, says that various equalities and inequalities hold amongst the and also that there is some not equal to finitely many terms in . But the latter is always true since models of are always infinite. So is equivalent in to the conjunction of all statements that do not mention , and again we have eliminated the quantifier.
This (together with an induction on formulas) proves QE for . QE results are, however, often sensitive to the particular language being used. In general, a QE result for a definable extension of a theory to a larger language does not imply QE for the original theory. But in the case here, we can deduce QE for from QE for .
To do this, note that is essentially the same theory as in the sense that for every model of there is one and only one way of expanding it to a model . Put more formally, this is the following result.
Theorem.
is a conservative extension of : for all sentences of , if then .
Proof.
If not, suppose is consistent, so has a model. This model has an expansion to a model of hence is consistent.
Furthermore, note that the reductions described above actually allow the function symbol to be eliminated entirely.
Thus we have proved that for every formula in there is a qf formula in equivalent to in . Hence by the reductions, there is a qf formula in equivalent to in . But the equivalence of and is a statement of provable in , hence this equivalence is provable in , giving QE for .
For related theories, the reader may consider the theories , and . None of these have elimination of quantifiers, though certain definable extensions of each of these do have QE. (I leave this as an exercise.)
Exercise.
Give an axiomatization for and prove that this theory has elimination of quantifiers. Show that are all definable in but that does not have QE.