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

• A subformula of the form $t = s$ in $θ ( x _ )$ can be replaced if required by $s = t$, resulting in a formula equivalent to $θ ( x _ )$ over $Succ ( P )$.
• A term of the form $P ( S ( t ) )$ in $θ ( x _ )$ can be replaced if required by just $t$, resulting in a formula equivalent to $θ ( x _ )$ over $Succ ( P )$. This is because $Succ ( P ) ⊢ ∀ x P ( S ( x ) ) = x$ (Exercise!)
• Similarly, we may replace $θ ( S ( P ( t ) ) )$ with the equivalent $( t = 0 ∧ θ ( S ( 0 ) ) ) ∨ ( ¬ t = 0 ∧ θ ( t ) )$.
• We may replace a subformula $P ( t ) = P ( s )$ by $( t = 0 ∧ s = 0 ) ∨ ( t = 0 ∧ s = S ( 0 ) ) ∨ ( s = 0 ∧ t = S ( 0 ) ) ∨ ( ¬ t = 0 ∧ ¬ s = 0 ∧ t = s )$.
• We may replace a subformula $S ( s ) = S ( t )$ with $s = t$.
• We may replace a subformula $S ( s ) = P ( t )$ with $S ( S ( s ) = t$.
• For any term $t$, the formula $S ( S ( … ( S ( t ) ) … ) ) = t$ is always false, equivalent to $¬ 0 = 0$.
• For any term $t$, the formula $P ( P ( … ( P ( t ) ) … ) ) = t$ is equivalent to $t = 0$.
• We may replace a subformula $P ( s ) = t$ with $( t = 0 ∧ s = 0 ) ∨ S ( t ) = s$.
• We may replace a subformula $S ( s ) = t$ with $¬ t = 0 ∧ P ( t ) = s$.

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.