1
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ I can't follow your second paragraph - can you be a little more clear? $\endgroup$ – Noah Schweber Feb 15 '15 at 2:00
  • 2
    $\begingroup$ 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. $\endgroup$ – SMM Feb 15 '15 at 9:46
  • $\begingroup$ @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? $\endgroup$ – Fawzy Hegab Feb 16 '15 at 20:20
  • $\begingroup$ @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. $\endgroup$ – Fawzy Hegab Feb 16 '15 at 20:23
  • $\begingroup$ @MathsLover Ok, I copied the comment as an answer. $\endgroup$ – SMM Feb 16 '15 at 20:58
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.