This web page provides another example of the method of Elimination of Quantifiers (QE), this time applied to the theory of $(\mathbb{N},S,0)$ where $S\left(x\right)=x\mathrm{+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 $(\mathbb{N},S,P,0)$ where $P\left(x\right)=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\left(P\right)$ be the language $L$ with a further unary function $P$. Let $\mathrm{Succ}$ be the $L$-theory with axioms

- $\forall x\u200a\forall y\u200a\left(S\right(x)=S(y)\to x=y)$
- $\forall x\u200a\neg x=0\to \exists y\u200a\left(S\right(y)=x)$
- $\forall x\u200a\neg S\left(x\right)=0$
- $\forall x\u200a\neg S\left(S\right(\dots \left(x\right)\dots \left)\right)=x$, where there are $k$ usages of the function symbol $S$, for each $k>0$

and let $\mathrm{Succ}\left(P\right)$ be the $L\left(P\right)$-theory with the above axioms together with

- $P\left(0\right)=0$
- $\forall x\u200a(\neg x=0\to S\left(P\right(x\left)\right)=x)$

Exercise.

Both $\mathrm{Succ}$ and $\mathrm{Succ}\left(P\right)$ are $\lambda $-categorical for each uncountable $\lambda $. They are therefore both complete (for their language).

It follows from the Exercise and the models in $\mathbb{N}$ that $\mathrm{Succ}=(\mathbb{N},S,0)$ and $\mathrm{Succ}\left(P\right)=(\mathbb{N},S,P,0)$ where $S\left(x\right)=x\mathrm{+1}$ and $P\left(x\right)=max(x-1,0)$.

Theorem.

$\mathrm{Succ}$ has Quantifier Elimination.

The proof is in several stages. We shall first show $\mathrm{Succ}\left(P\right)$ has QE and derive the theorem from this.

Consider a quantifier-free formula $\theta \left(\stackrel{\_}{x}\right)$ of
$\mathrm{Succ}\left(P\right)$. We shall apply several reductions to the
atomic formulas in $\theta \left(\stackrel{\_}{x}\right)$ to simplify

it.
Our objectives are particularly to simplify the terms
involving $S,P$ in $\theta $ and to remove occurences
of $P\left(S\right(\dots \left)\right)$ or $S\left(P\right(\dots \left)\right)$. In the
following, $t,s$ range over arbitrary terms of $L\left(P\right)$.

- A subformula of the form $t=s$ in $\theta \left(\stackrel{\_}{x}\right)$ can be replaced if required by $s=t$, resulting in a formula equivalent to $\theta \left(\stackrel{\_}{x}\right)$ over $\mathrm{Succ}\left(P\right)$.
- A term of the form $P\left(S\right(t\left)\right)$ in $\theta \left(\stackrel{\_}{x}\right)$ can be replaced if required by just $t$, resulting in a formula equivalent to $\theta \left(\stackrel{\_}{x}\right)$ over $\mathrm{Succ}\left(P\right)$. This is because $\mathrm{Succ}\left(P\right)\u22a2\forall x\u200aP\left(S\right(x\left)\right)=x$ (Exercise!)
- Similarly, we may replace $\theta \left(S\right(P\left(t\right)\left)\right)$ with the equivalent $(t=0\wedge \theta (S\left(0\right)\left)\right)\vee (\neg t=0\wedge \theta (t\left)\right)$.
- We may replace a subformula $P\left(t\right)=P\left(s\right)$ by $(t=0\wedge s=0)\vee (t=0\wedge s=S(0\left)\right)\vee (s=0\wedge t=S(0\left)\right)\vee (\neg t=0\wedge \neg s=0\wedge t=s)$.
- We may replace a subformula $S\left(s\right)=S\left(t\right)$ with $s=t$.
- We may replace a subformula $S\left(s\right)=P\left(t\right)$ with $S\left(S\right(s)=t$.
- For any term $t$, the formula $S\left(S\right(\dots \left(S\right(t\left)\right)\dots \left)\right)=t$ is always false, equivalent to $\neg 0=0$.
- For any term $t$, the formula $P\left(P\right(\dots \left(P\right(t\left)\right)\dots \left)\right)=t$ is equivalent to $t=0$.
- We may replace a subformula $P\left(s\right)=t$ with $(t=0\wedge s=0)\vee S\left(t\right)=s$.
- We may replace a subformula $S\left(s\right)=t$ with $\neg t=0\wedge P\left(t\right)=s$.

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

The other case is when every occurence of $y$ is like $\neg y=t\left(\stackrel{\_}{x}\right)$. In this case, $\exists y\u200a\underset{j}{\overset{}{\bigwedge}}(\neg \left){\alpha}_{ij}\right(\stackrel{\_}{x},y)$ says that various equalities and inequalities hold amongst the $\stackrel{\_}{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 $\mathrm{Succ}\left(P\right)$ are always infinite. So $\exists y\u200a\underset{j}{\overset{}{\bigwedge}}(\neg \left){\alpha}_{ij}\right(\stackrel{\_}{x},y)$ is equivalent in $\mathrm{Succ}\left(P\right)$ to the conjunction of all statements $(\neg ){\alpha}_{ij}(\stackrel{\_}{x},y)$ that do not mention $y$, and again we have eliminated the quantifier.

This (together with an induction on formulas) proves QE for $\mathrm{Succ}\left(P\right)$. 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 $\mathrm{Succ}$ from QE for $\mathrm{Succ}\left(P\right)$.

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

Theorem.

$\mathrm{Succ}\left(P\right)$ is a conservative extension of $\mathrm{Succ}$: for all sentences $\sigma $ of $L$, if $\mathrm{Succ}\left(P\right)\u22a2\sigma $ then $\mathrm{Succ}\u22a2\sigma $.

**Proof.**

If not, suppose $\mathrm{Succ}\cup \left\{\neg \sigma \right\}$ is consistent, so has a model. This model has an expansion to a model of $\mathrm{Succ}\left(P\right)$ hence $\mathrm{Succ}\left(P\right)\cup \left\{\neg \sigma \right\}$ 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 $\theta \left(\stackrel{\_}{x}\right)$ in $L$ there is a qf formula $\psi \left(\stackrel{\_}{x}\right)$ in $L\left(P\right)$ equivalent to $\theta \left(\stackrel{\_}{x}\right)$ in $\mathrm{Succ}\left(P\right)$. Hence by the reductions, there is a qf formula $\varphi \left(\stackrel{\_}{x}\right)$ in $L$ equivalent to $\psi \left(\stackrel{\_}{x}\right)$ in $\mathrm{Succ}\left(P\right)$. But the equivalence of $\theta \left(\stackrel{\_}{x}\right)$ and $\varphi \left(\stackrel{\_}{x}\right)$ is a statement of $L$ provable in $\mathrm{Succ}\left(P\right)$, hence this equivalence is provable in $\mathrm{Succ}$, giving QE for $\mathrm{Succ}$.

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