[FOM] Re: Proof "from the book" of the incompleteness theorem

[Marcin Mostowski]

Arnon Avron is wrong in repeating the argument describing Tarski's proof -
as 
mentioned by Martin Davis - as nonconstructive in the sense that it does
not 
give an example of an independent sentence. As I remember the argument is 
taken from one of the books by Penrose. 2 years ago I was discussing some 
claims by Penrose at my seminar. Somebody has observed (probably not me but
one of my students) that the argument is wrong. It suffices to look at one
of the simplest proofs of the Tarski Theorem (TT) based on the Diagonal
Lemma (DL).

TT: There is no arithmetical P(x) such that for all arithmetical sentences
F, 
N |= (F <=> P("F")), where N is the standard model of arithmetic and "F" is
the Goedel number of F.

Proof: Assume that such P(x) exists. Then by DL we have a sentence G such 
that N |= (G <=> ~P("G")). On the other hand by the assumption we have N |=
(G <=> P("G")), what by the truth conditions gives the contradiction. QED.

To obtain the 1st Goedel Theorem (GT1) we need also the following:

Lemma. The set of each axiomatizable theory is \Sigma_1 in arithmetical 
hierarchy. Therefore the set of Goedel numbers of its theorems is definable
in the standard model N.

GT1: For each axiomatizable arithmetical theory T true of natural numbers
(N 
|= T) there is G logically undecidable in T.

Proof: Let T satisfies the assumptions. By the lemma we have an arithetical
formula P(x) such that

for all arithetical F, T |- F iff N |= P("F").

Now we essentially repeat the proof of TT,

By DL we have G such that: N |= (G <=> ~P("G")).
It means that: N |= G iff not T |- G.

If T |- G then N |= P("G") and N |= ~G, what is impossible because N |=T.

If T |- ~G then not T |- G and N |= G, what is impossible because N |=T.
QED.

The constructivity of the proof follows from the constructivity of DL,
which 
effectively gives G for P(x).


All of this can be found (maybe in slightly different formulations) in the 
papers by Tarski. The only possible exception is the observation about 
constructivity. However it seems to be obvious.

Let me observe additionally that the sentence G constructed in the proof of
GT1 is the same as that in the classical proof given by Goedel.

Another observation. Goedel has taken weaker assumptions that T is
consistent for the first part and omega consistent for the second part
instead of "truth of natural numbers". However in the Tarski version we can
replace the assumption "axiomatizable" by "arithmetically definable". 

Still another observation. The reasoning discussed is short and smart 
similarly as the classical proof of DL. Nevertheless all the technical 
details are put here into the lemma, which is obvious for specislists but
not 
for larger mathematical public. This is not usual for the majority of the 
proofs from the book.



Arnon Avron napisa³(a):

> > 
> > How about:
> > 
> > The set of arithmetic theorems of any formal system  is recursively 
> > enumerable, while the set of arithmetic truths is not. So any sound formal 
> > system must fail to prove some arithmetic truth.
> > 
> > Martin
> 
> This is indeed the first proof (out of 3) that Smullyan presents
> in his book on the incompleteness theorems. The trouble with this 
> proof is that it misses one of the most important aspects of Godel's
> proof: the actual construction of a *true* sentence which the system
> fails to prove, and a *proof* that it is true. The most interesting 
> debates concerning the implications of Godel's theorem are connected
> with this aspect (in particular: the debate about Lucas-Penrose argument).
> 
> Arnon Avron
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom



_____________________

Marcin Mostowski
Department of Logic
Institute of Philosophy
Warsaw University