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

Hi David,

Sorry for the trouble. Appreciate your kindness and patience so far,
afterall you helped me understand something I was stuck at for quite a
while. :-)

If I'm hearing you correctly, what are you saying is that the context
(which I would have gotten had I read the entire proof carefully) would
have made it clear that I was not supposed to see alpha_0 in isolation
from the quantifier Ex.

What I had done was to take what Enderton wrote on pg 192 _literally_
that alpha_0 can be replaced by t not equal to 0 /\ .../\ t not equal
to S^(m-1) 0. Reading that particular sentence literally seemed to be
my problem.

But now, this is how I actually understand Case 2 of Enderton's proof.

Given Ex (alpha_0 /\ ... /\ alpha_q) where each alpha_i has the form of
an equation or negation of equation of following form S^m x = S^m u and
u is zero or variable not equal to x, what I have to do is to break up
Ex (alpha_0 /\ ... /\ alpha_q) into Ex (alpha_0) /\ ... /\ Ex
(alpha_q) and consider each Ex alpha_i. If in one of the Ex alpha_i,
alpha_i is not negated, then I replace that particular alpha_i by t not
equal to 0 /\ .../\ t not equal to S^(m-1) 0. For the remaining
Ex(alpha_j), say Ex (S^k x = u), we just remove the the variable x as
follows: Replace Ex (S^k x = u) by Ex(S^(k+m)x = S^m u and then replace
Ex(S^(k+m)x = S^m u by Ex(S^k t = S^m u). And then I can remove Ex. Is
this correct? I have a feeling that you think I don't have to split up
the Ex (alpha_0 /\ ... /\ alpha_q) into Ex (alpha_0) /\ ... /\ Ex
(alpha_q).

Another question. Is this alternative proof for Case 2 acceptable.Given
Ex (alpha_0 /\ ... /\ alpha_q) with the same conditions as last para,
we break up this formula into Ex (alpha_0) /\ ... /\ Ex (alpha_q) and
isolate all the alpha_i that are not negated, eliminate the quantifiers
along the lines described above. We are now left with all the negated
Ex (alpha_j) if any, which is just Case 1.

David C. Ullrich wrote:
On 15 Jun 2006 07:37:37 -0700, "recordmymind" <recordmymind@xxxxxxxxx>
wrote:

Hi David,

Anyway, I took some pictures of the pages in question and the links are
here

pg 191: http://www.flickr.com/photos/48537658@N00/167696412/

pg 192: http://www.flickr.com/photos/48537658@N00/167698616/

I hope the links work.

Aargh. Next time the thing to do is to get an actual web site
that you can simply edit, and add the images to it with IMG
tags. Or simply upload the files to the server and post a
link to the file iteself. I can't find a way to save the
image when you put it on this flickr thing (and I need to
save the image so I can view it at about three times the
size it appears there).

Ok, printscreen/paste/save worked. Back to the math:

The next time someone asks to look again you should look again,
much more carefully! The next time someone asks whether there's
an "Ex" that you're not telling us about you should look carefully
for Ex's, and say _yes_ if one is there!

Enderton does _not_ say that S^m x = t can be replaced in this
theory by t not equal to 0 /\ .../\ t not equal to S^(m-1) 0.

To understand a typical proof you need to read the whole thing.
At the start he says something about what sort of formula he's
going to replace with a quantidier-free formula. The formula P
he's going to replace has the form Ex alpha. Then in the rest
of the proof he doesn't write down P again, he just discusses
the formula alpha. That formula alpha is _inside_ P - it's
P that he's talking about eliminating the quantifiers from.

In particular, the reason that what he says in one case is
right is that if x does not appear in t then Ex S^m x = t
is equivalent to t not equal to 0 /\ .../\ t not equal to S^(m-1) 0.

recordmymind wrote:
Hi David,

Quick reply. I read your post and suddenly things made sense. With some
quick reasoning, I have verified that what you said about the following
is true:

Ex S^m x = t is equivalent to t not equal to 0 /\ .../\ t not equal to
S^(m-1) 0

I think you are absolutely correct regarding the equivalence above.
Also, yes, t is a term where x does not appear.

Anyway, I'll try to scan the relevant pages and link to them, if not by
tomorrow, then by the coming Wed.

I'm quite relieved now because this was a stumbling block for the
longest time and I could not read on further in the book cos I was
stuck at this proof. And this is the second or third time I am trying
after a couple of years cos I still hope to achieve my ultimate goal of
understanding incompleteness.

Thanks a lot, David! Your questions made a big and positive difference
to me! I feel ready and rejuvenated to press on with the book! :-)

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


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

David C. Ullrich

.

Relevant Pages
Loading