[Top] [All Lists]

Re: [ontolog-forum] Axiomatic ontology

To: Avril Styrman <Avril.Styrman@xxxxxxxxxxx>
Cc: ontolog-forum@xxxxxxxxxxxxxxxx
From: Pat Hayes <phayes@xxxxxxx>
Date: Thu, 31 Jan 2008 13:59:35 -0600
Message-id: <p0623090ac3c7d5d222b0@[]>
At 9:04 PM +0200 1/31/08, Avril Styrman wrote:

> >  This is the idea
> >of Gödel numbering: the things that are to be proved have to
> >be used in their own proof.
> Apparently you know very little about formal arithmetic or Goedel's
> theorem.
> a. 1+1=2 is provable in any formal arithmetic.

So, prove it Pat! Prove it here. After that I'll prove that you
used the very ability to distinguish between I and II.

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.

> b. "the things that are to be proved have to be
> used in their own proof"  is not the idea of
> Goedel numbering

What else is the idea in the end, than to prove that
proving X requires self-reference?

Um.. do you want me to explain the Goedel proof? There are many intuitive accounts already written,and I don't have the energy to write out yet another one.

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?

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. 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?) 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.

If you 'prove' something that is as obvious as can be like
1+1=2, you only prove that you yourself feel more comfortable
after having used some conventions. Tell me, do you need to
prove that 1+1=2?

No, of course not.
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.

IHMC               (850)434 8903 or (650)494 3973   home
40 South Alcaniz St.       (850)202 4416   office
Pensacola                 (850)202 4440   fax
FL 32502                     (850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes

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    (01)

<Prev in Thread] Current Thread [Next in Thread>