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

$\forall x \forall y (S (x) = S (y) \to x = y)$
$\forall x \neg x = 0 \to \exists y (S (y) = x)$
$\forall x \neg S (x) = 0$
$\forall x \neg S (S (\dots (x) \dots)) = 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$
$\forall x (\neg x = 0 \to 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 $θ (\overline{x})$ of $Succ (P)$ . We shall apply several reductions to the atomic formulas in $θ (\overline{x})$ to simplify it. Our objectives are particularly to simplify the terms involving $S, P$ in $θ$ and to remove occurences of $P (S (\dots))$ or $S (P (\dots))$ . In the following, $t, s$ range over arbitrary terms of $L (P)$ .

A subformula of the form $t = s$ in $θ (\overline{x})$ can be replaced if required by $s = t$ , resulting in a formula equivalent to $θ (\overline{x})$ over $Succ (P)$ .
A term of the form $P (S (t))$ in $θ (\overline{x})$ can be replaced if required by just $t$ , resulting in a formula equivalent to $θ (\overline{x})$ over $Succ (P)$ . This is because $Succ (P) ⊢ \forall x P (S (x)) = x$ (Exercise!)
Similarly, we may replace $θ (S (P (t)))$ with the equivalent $(t = 0 \land θ (S (0))) \lor (\neg t = 0 \land θ (t))$ .
We may replace a subformula $P (t) = P (s)$ by $(t = 0 \land s = 0) \lor (t = 0 \land s = S (0)) \lor (s = 0 \land t = S (0)) \lor (\neg t = 0 \land \neg s = 0 \land 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 (\dots (S (t)) \dots)) = t$ is always false, equivalent to $\neg 0 = 0$ .
For any term $t$ , the formula $P (P (\dots (P (t)) \dots)) = t$ is equivalent to $t = 0$ .
We may replace a subformula $P (s) = t$ with $(t = 0 \land s = 0) \lor S (t) = s$ .
We may replace a subformula $S (s) = t$ with $\neg t = 0 \land P (t) = s$ .

Now to prove QE. We argue inductively, eliminating quantifiers from successively complex formulas. Consider a formula $\exists y θ (\overline{x}, y)$ . By induction we may assume that $θ (\overline{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 (\dots)$ or $P (\dots)$ . For such $θ (\overline{x}, y)$ we can apply the result on disjunctive normal form (DNF) to find a quantifier free formula of the form $⋁_{i}^{} ⋀_{j}^{} (\neg) α_{i j} (\overline{x}, y)$ equivalent to $θ (\overline{x}, y)$ , where $(\neg) α_{i j} (\overline{x}, y)$ is either an atomic formula occuring in $θ (\overline{x}, y)$ or is the negation of some such formula. We need to eliminate the quantifier $\exists y$ from $\exists y ⋁_{i}^{} ⋀_{j}^{} (\neg) α_{i j} (\overline{x}, y)$ and since the $⋁_{}^{}$ and the $\exists y$ commute here it suffices to show that each $\exists y ⋀_{j}^{} (\neg) α_{i j} (\overline{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 (\overline{x})$ or as $\neg y = t (\overline{x})$ in the $(\neg) α_{i j} (\overline{x}, y)$ . The first case we consider is when one of the statements $(\neg) α_{i j} (\overline{x}, y)$ is $y = t (\overline{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 (\overline{x})$ . Therefore if we replace $y$ by $t (\overline{x})$ throughout $⋀_{j}^{} (\neg) α_{i j} (\overline{x}, y)$ we get an equivalent statement that contains no $y$ and hence there is no need for the $\exists y$ quantifier.

The other case is when every occurence of $y$ is like $\neg y = t (\overline{x})$ . In this case, $\exists y ⋀_{j}^{} (\neg) α_{i j} (\overline{x}, y)$ says that various equalities and inequalities hold amongst the $\overline{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 $\exists y ⋀_{j}^{} (\neg) α_{i j} (\overline{x}, y)$ is equivalent in $Succ (P)$ to the conjunction of all statements $(\neg) α_{i j} (\overline{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 \cup \{\neg σ\}$ is consistent, so has a model. This model has an expansion to a model of $Succ (P)$ hence $Succ (P) \cup \{\neg σ\}$ 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 $θ (\overline{x})$ in $L$ there is a qf formula $ψ (\overline{x})$ in $L (P)$ equivalent to $θ (\overline{x})$ in $Succ (P)$ . Hence by the reductions, there is a qf formula $ϕ (\overline{x})$ in $L$ equivalent to $ψ (\overline{x})$ in $Succ (P)$ . But the equivalence of $θ (\overline{x})$ and $ϕ (\overline{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.