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?
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.