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@[10.100.0.14]> |
At 9:04 PM +0200 1/31/08, Avril Styrman wrote:
Pat, > > This is the idea 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.
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.
observation of the proof. And this does not mention self-reference anywhere, right?
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.
No, of course not. Why do you? After you have proved it, do you 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.
Pat
-- ---------------------------------------------------------------------
IHMC 40 South Alcaniz St. Pensacola FL 32502 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> |
---|---|---|
|
Previous by Date: | Re: [ontolog-forum] Axiomatic ontology, Pat Hayes |
---|---|
Next by Date: | Re: [ontolog-forum] Axiomatic ontology, Ed Barkmeyer |
Previous by Thread: | Re: [ontolog-forum] Axiomatic ontology, Avril Styrman |
Next by Thread: | Re: [ontolog-forum] Axiomatic ontology, Avril Styrman |
Indexes: | [Date] [Thread] [Top] [All Lists] |