The theory of a successor function

This web page provides another example of the method of Elimination of Quantifiers (QE), this time applied to the theory of ( , S , 0 ) where S ( x ) = x +1 . 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 ( , S , P , 0 ) where P ( x ) = max ( 0 , x - 1 ) , which for technical reasons is a little more straightforward to work with.

Definition.

Let L be the first order language with unary function sysmbol S and a constant 0 . Let L ( P ) be the language L with a further unary function P . Let Succ be the L -theory with axioms

  • x y ( S ( x ) = S ( y ) x = y )
  • x ¬ x = 0 y ( S ( y ) = x )
  • x ¬ S ( x ) = 0
  • x ¬ S ( S ( ( x ) ) ) = x , where there are k usages of the function symbol S , for each k > 0

and let Succ ( P ) be the L ( P ) -theory with the above axioms together with

  • P ( 0 ) = 0
  • x ( ¬ x = 0 S ( P ( x ) ) = x )

Exercise.

Both Succ and Succ ( P ) are λ -categorical for each uncountable λ . They are therefore both complete (for their language).

It follows from the Exercise and the models in that Succ = ( , S , 0 ) and Succ ( P ) = ( , S , P , 0 ) where S ( x ) = x +1 and P ( x ) = max ( x - 1 , 0 ) .

Theorem.

Succ has Quantifier Elimination.

The proof is in several stages. We shall first show Succ ( P ) has QE and derive the theorem from this.

Consider a quantifier-free formula θ ( x _ ) of Succ ( P ) . We shall apply several reductions to the atomic formulas in θ ( x _ ) to simplify it. Our objectives are particularly to simplify the terms involving S , P in θ and to remove occurences of P ( S ( ) ) or S ( P ( ) ) . In the following, t , s range over arbitrary terms of L ( P ) .

Now to prove QE. We argue inductively, eliminating quantifiers from successively complex formulas. Consider a formula y θ ( x _ , y ) . By induction we may assume that θ ( x _ , y ) is already quantifier free. By applying the above reductions (especially the last two) we may assume that y does not occur as an argument to a function symbol S ( ) or P ( ) . For such θ ( x _ , y ) we can apply the result on disjunctive normal form (DNF) to find a quantifier free formula of the form i j ( ¬ ) α i j ( x _ , y ) equivalent to θ ( x _ , y ) , where ( ¬ ) α i j ( x _ , y ) is either an atomic formula occuring in θ ( x _ , y ) or is the negation of some such formula. We need to eliminate the quantifier y from y i j ( ¬ ) α i j ( x _ , y ) and since the and the y commute here it suffices to show that each y j ( ¬ ) α i j ( x _ , y ) is equivalent to something that is quantifier free.

There are two cases. By the reductions already applied, the variable y occurs as either y = t ( x _ ) or as ¬ y = t ( x _ ) in the ( ¬ ) α i j ( x _ , y ) . The first case we consider is when one of the statements ( ¬ ) α i j ( x _ , y ) is y = t ( x _ ) , without the not sign. In this case, we have no choice as to what element y must be: it must be the element given by the term t ( x _ ) . Therefore if we replace y by t ( x _ ) throughout j ( ¬ ) α i j ( x _ , y ) we get an equivalent statement that contains no y and hence there is no need for the y quantifier.

The other case is when every occurence of y is like ¬ y = t ( x _ ) . In this case, y j ( ¬ ) α i j ( x _ , y ) says that various equalities and inequalities hold amongst the x _ and also that there is some y not equal to finitely many terms in x . But the latter is always true since models of Succ ( P ) are always infinite. So y j ( ¬ ) α i j ( x _ , y ) is equivalent in Succ ( P ) to the conjunction of all statements ( ¬ ) α i j ( x _ , y ) that do not mention y , and again we have eliminated the quantifier.

This (together with an induction on formulas) proves QE for Succ ( P ) . 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 Succ from QE for Succ ( P ) .

To do this, note that Succ ( P ) is essentially the same theory as Succ in the sense that for every model M of Succ there is one and only one way of expanding it to a model ( M , P ) Succ ( P ) . Put more formally, this is the following result.

Theorem.

Succ ( P ) is a conservative extension of Succ : for all sentences σ of L , if Succ ( P ) σ then Succ σ .

Proof.

If not, suppose Succ ¬ σ is consistent, so has a model. This model has an expansion to a model of Succ ( P ) hence Succ ( P ) ¬ σ is consistent.

Furthermore, note that the reductions described above actually allow the function symbol P to be eliminated entirely.

Thus we have proved that for every formula θ ( x _ ) in L there is a qf formula ψ ( x _ ) in L ( P ) equivalent to θ ( x _ ) in Succ ( P ) . Hence by the reductions, there is a qf formula ϕ ( x _ ) in L equivalent to ψ ( x _ ) in Succ ( P ) . But the equivalence of θ ( x _ ) and ϕ ( x _ ) is a statement of L provable in Succ ( P ) , hence this equivalence is provable in Succ , giving QE for Succ .

For related theories, the reader may consider the theories ( , S ) , ( , P ) 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 ( , < , S , P , 0 ) and prove that this theory has elimination of quantifiers. Show that S , P , 0 are all definable in ( , < ) but that ( , < ) does not have QE.