# Showing that the theory $R_s$ admits quantifier elimination

In Enderton's logic page $192$, in his proof that the theory $R_s$ (natural numbers with successor and constant symbol $0$) admits quantifier elimination, he uses the fact that it suffices to show that formulas of the form $\exists x\bigwedge_{1\leq i\leq n}A_i$ admits quantifier elimination.

In some case in the proof that $x$ occurs in every $A_i$ and that there is at least of an equation $A_i$ of the form $S^m=t$ that is an atomic formula (not a negation of an atomic formula). and he says that this particular $A_i$ is equivalent to the quantifier-free formula $\phi: t\ne 0\wedge ...\wedge t\ne S^{m-1}0$. This seems ok at first, but for me:$\phi\nvDash A_i$, I know that $\phi\vDash A_i[s]$ for some variable assignment $s$ but this doesn't mean that this is the case for all variable assignments $s$.

Any clarifications for this?

In other words:

The question is: why $∃x(Sm(x)=t)$is equivalent to $A:= t≠0∧t≠S(0)∧…∧t≠S^{m−1}(0)$?

One of the things I'm thinking of is that it seems that both are sentences (considering$\exists x A_i$ after distributing the existential quantifier over all $A_i$'s instead of just $A_i$) and hence since both $\exists xA_i,\phi$ are satisfiable by one variable assignment then they are satisfiable for all variable assignment, Is that the point? or am I missing something?

• I can't follow your second paragraph - can you be a little more clear? – Noah Schweber Feb 15 '15 at 2:00
• The theory of natural numbers with successor doesn't admit quantifier elimination (you need $0$ in the language). In the second paragraph you use $0$, so I assume it is in the language. Is the question why $\exists x\,(S^m(x)=t)$ is equivalent to $A:=\ t\neq 0\wedge t\neq S(0)\wedge\ldots\wedge t\neq S^{m-1}(0)$? If so, if $\exists x\,(S^m(x)=t)$ holds in some valuation $v$ and $a$ witnesses existential quantifier, then $t[v]=a+m$, hence $t[v]\geq m$ and $A[v]$ holds. If $\exists x\,(S^m(x)=t)$ doesn't hold in some valuation $v$, it is only possible if $t[v]<m$, hence $A[v]$ doesn't hold. – SMM Feb 15 '15 at 9:46
• @SMM, yup $0$ is in the language but I wasn't precise. Could you please convert your comment into an answer so I will be able to close the question since I understand now the point and it should be closed? – Fawzy Hegab Feb 16 '15 at 20:20
• @user28111, I've edited the question and after all, the answer of SMM gives what I needed , I'm sorry for not being clear, I will make sure it's clear next time. – Fawzy Hegab Feb 16 '15 at 20:23
• @MathsLover Ok, I copied the comment as an answer. – SMM Feb 16 '15 at 20:58

The theory of natural numbers with successor doesn't admit quantifier elimination (you need $0$ in the language). In the second paragraph you use $0$, so I assume it is in the language. Is the question why $\exists x(S^m(x)=t)$ is equivalent to $A:= t\neq 0\wedge t\neq S(0)\wedge\ldots\wedge t\neq S^{m−1}(0)$? If so, if $\exists x(S^m(x)=t)$ holds in some valuation $v$ and $a$ witnesses existential quantifier, then $t[v]=a+m$, hence $t[v]\geq m$ and $A[v]$ holds. If $\exists x(S^m(x)=t)$ doesn't hold in some valuation $v$, it is only possible if $t[v]<m$, hence $A[v]$ doesn't hold.