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

On 13 Jun 2006 07:15:37 -0700, "recordmymind" <recordmymind@xxxxxxxxx>
wrote:

David C. Ullrich wrote:
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?

recordmymind: Yes, that is a question I also asked when I read that
particular page I mentioned.

??? You need to get the definitions of the terms straight first...

Note that I'm just guessing here. When we say that a theory
admits elimination of quantifiers surely that means that any
formula is equivalent to a quantifier-free formula. So surely
if a theory implies that two formulas are equivalent then
that means that one formula "can replace" the other. (???)
What else could it mean?

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.

recordmymind: well, perhaps you could check out the book reference and
verify it for yourself. Look forward to your response after you have
read those two pages I mentioned. Thanks.

The two formulas you cite here are not equivalent. But with
a tiny change to one of them they become equivalent. Perhaps
you could look again, and see whether you actually typed
them both correctly.

I thank some kind soul in advance.


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

David C. Ullrich


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

David C. Ullrich
.

Relevant Pages
Loading