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

On 14 Jun 2006 09:54:52 -0700, "recordmymind" <recordmymind@xxxxxxxxx>
wrote:

Dear David,

Thank you for taking the trouble to reply. I'm sorry for what is a
quick and careless reply from me.

Regarding the definition of "replace", there is no definition of it in
the book. I checked the index to be sure. What follows will make clear
whether I have any understanding at all of the subject matter (I'm not
sure myself!). I gather that " alpha can replace beta" means that in a
model A, any function s from the variables in the language to the
domain of model A would satisfy this formula: alpha <--> beta, i.e.
make alpha <--> beta true in A. In other words, either both alpha and
beta are true in A or they are both false.

Regarding:

S^m x = t being replaceable by t not equal to 0 /\ .../\ t not equal to
S^(m-1) 0

I swear I checked it again and I stared at what I typed with what was
printed on the book. The reason Enderton gives for the longer formula
being able to replace the shorter one is "the solution for x must be
non-negative".

Nonetheless, I still allow for the possibility that either my eyes have
deceived me or I have typed wrongly. If you could give me your email, I
will scan the relevant pages and email them to you within 2 days' time.

Before you do that, look again. Is it really S^m x = t, or is it
"Ex S^m x = t"? I ask because the second one _is_ equivalent to
"t not equal to 0 /\ .../\ t not equal to S^(m-1) 0".

(Also it's not clear what your version might have to do
with quantifier elimination, since there are
no quantifiers on either side. Also the comment about
"the solution" is a little hard to follow unless there's
an "Ex" there.)

Come to think of it, I bet there's also a condition that
says something like "if x does not occur in t" that
you haven't told us about, right? (Here I'm assuming
that t is supposed to be a term...)

If you do end up scanning something don't email it to me.
(i) It probably wouldn't survive my large-file filter anyway
(ii) A better idea is to post the scan on a web site and
then post a link to it here - then anyone who's curious
can see it.

I appreciate your kindness and patience in wanting to help me see my
way through the proof. Thanks.


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


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

David C. Ullrich
.

Relevant Pages
Quantcast