Lainaus Pat Hayes <phayes@xxxxxxx>: (01)
> Choose your formal arithmetic, and I'll give you
> the proof (which will be very trivial). But look:
> what you say is obviously wrong, because a formal
> proof does not use any "ability". It (the proof)
> is a syntactically defined entity satisfying
> certain formal constraints, and merely by
> existing it establishes that its conclusion is a
> theorem. Ability does not enter into this
> discussion. (02)
Just choose the one that you like the best, and
we'll analyze the proof. (03)
> >This is copied from Wikipedia:
> >
> > Gödel specifically used this scheme at two levels: first,
> > to encode sequences of symbols representing formulas, and
> > second, to encode sequences of formulas representing proofs.
> > This allowed him to show a correspondence between
> > statements about natural numbers and statements about the
> > provability of theorems about natural numbers, the key
> > observation of the proof.
>
> And this does not mention self-reference anywhere, right?
> (04)
Yes, it strongly seems that it does. (05)
> >
> >If the key idea is not self-reference, then what is it?
> >
> >Suppose that I'm totally wrong. This does not change the fact
> >that proving 1+1=2 requires understanding the difference of
> >I and II. It does not change anything if Gödel took a longer
> >road and included conventions used by modern mathematicians.
> >It is still the same old story: self-reference.
>
> Honestly, you have no idea what you are talking
> about. (06)
Being arrogant does not help solving issues. It won't
kill you to try to be polite, even if you disagree. (07)
> I see where you are coming from (that in
> order to understand a the formal proof one needs
> the same cognitive or intuitive abilities as one
> needs to simply understand that the conclusion is
> true.So the formal proof does not itself add
> anything to our pre-mathematical intuition. Do I
> have that more or less right?) (08)
That too, but also that understanding 1+1=2 is a
prerequisite for any reasoning in general. (09)
but this is NOT
> what the Goedel theorem is about: its conclusion
> is that certain things that are, in a sense,
> clearly true cannot be proved *at all*, even from
> the obvious premises; and it establishes this by
> showing that one can always construct a sentence
> which has the logical structure similar to the
> liar paradox: this sentence is unprovable. If
> this were provable, the whole system would be
> inconsistent: so (assuming that the system is
> consistent) it cannot be: but then what it says
> is correct, so it is in fact true. True, but
> unprovable. The really clever part of the proof
> was to show that one can do this is any axiomatic
> system for arithmetic, so arithmetic is itself
> undecideable. This last part was done using
> Goedel numbering, which is what the above quote
> from Wikipedia is all about. (010)
And what you described above was only a round-route
of saying that to prove that 1+1=2 requires
self-reference. It is the _same_ as that it cannot
be proved at all. If a proof of X requires self-
reference, then it is not a proof at all. We
can give axioms with which 1+1=2 can be proved,
but these axioms require understanding that 1+1=2. (011)
> >Why do you? After you have proved it, do you
> >feel more certain about 1+1=2?
>
> I don't. You miss the point altogether. The
> purpose of the formalization is not to provide
> better evidence for obvious truths. It is to
> support highly non-obvious reasoning with some
> confidence that it will be correct. (012)
Sometimes I feel that what should be studied
is not how to make proofs, but to study what
is it that needs to be proven in the first place. (013)
Proof analysis and a coherent system is one thing.
The intelligibility of the system is something else.
Both criteria are important, but sometimes the
applicability of a system does not even matter to a
mathematician. It is enough that some system is in
some way 'interesting'. (014)
Avril (015)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (016)
|