ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Terminology and Knowledge Engineering

To: Ontolog-forum <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Thu, 26 Jan 2012 13:55:45 +0100
Message-id: <C281C418-BA33-446C-A394-2DE045473B6B@xxxxxxxx>
Am Jan 26, 2012 um 4:42 AM schrieb Pat Hayes:
Chris M has pointed out that I was not quite accurate:
On Jan 25, 2012, at 4:16 PM, Pat Hayes wrote:
....
but the diagonalization Gödel invented for his proof is one which shows a more creative view of math than previously stated by earlier mathematicians.

Nonsense. First, Goedel's proof does not use diagonalization:

Wrong. It does, in one form.

Yes, but you were in fact quite correct regarding Gödel's original proof, which does not use an explicit diagonalization argument. The explicit use of diagonalization is only found in more modern treatments, which prove Gödel's theorem by means of a general lemma usually called (as you know) the Diagonal (or Fixed Point) Lemma.

But the technique was not invented by Goedel.

Quite right, and, as you also pointed out, the real stroke of creative genius — actually, the first but arguably the greatest stroke — in the proof was his invention of arithmetization, the trick of coding syntactic and proof theoretic entities — notably, sentences and proofs — as numbers, thereby making it possible for any theory T containing a small fragment of arithmetic to represent its own syntax and its own proof theory. Gödel's second stroke was realizing that this would enable him to generate a proof-theoretic form of the Liar paradox by coming up with a sentence G in the language of T that "asserts its own unprovability" and, as a consequence, can be neither proved nor refuted in T (assuming T is consistent*). It was only later that logicians came to realize that the sentence G could be usefully seen as an instance of a more general diagonalization construction.

-chris

*Actually, the unrefutability of G in Gödel's original proof requires a stronger condition on T called ω-consistency, viz., the property that T can't simultaneously prove a sentence of the form ∃x~φ(x) as well as all sentences of the form φ(0), φ(1), φ(2), …. J. B. Rosser subsequently found an alternative way of expressing provability that did not require this condition.

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

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