Re: H. Enderton's proof that theory of natural numbers with successor admits elimination of quantifiers

On 12 Jun 2006 11:11:14 -0700, "recordmymind" <recordmymind@xxxxxxxxx>
wrote:

I'm looking for someone who is familiar with the second edition of
Enderton's A Mathematical Introduction to Logic. I'm having
difficulties understanding one of Enderton's proofs and would be
extremely grateful if someone here could help me with my difficulties.

In page 191, Theorem 31 G states that the theory of the natural numbers
with successor admits elimination of quantifier.

First question, on page 192, I do not understand why 0=0 can replace
the entire formula in Case 1. Is it because in Case 1,

A_s |= (0 = 0 <---> Exists x (alpha_0 /\ ... /\ alpha_q) )

where each alpha_i is a formula of this form: ~ (S^m x = S^n u )?

If p and q are two formulas, exactly what does it mean to say
that "p can replace q" here?

Second question, why is it that in Case 2, alpha_0 is replaceable by t
not equal to 0 /\ .../\ t not equal to S^(m-1) 0? Note: alpha_0 is S^m
x = t

Is that _exactly_ what alpha_0 is? I tend to doubt it.

I thank some kind soul in advance.


************************

David C. Ullrich
.