[FOM] 344:Goedel's Second Revisited 2

[Jeremy Avigad]

Harvey Friedman wrote:

> There is a weak form of Goedel's Second - namely that any theory T 
> subject to weak conditions does not prove its own 1-consistency.

> Who is this proof due to? I have known it for some time. Also Saul 
> Kripke has known this for quite some time. But who else?

There is an exposition of this on my home page, under "Teaching":

   http://www.andrew.cmu.edu/user/avigad/Teaching/halting.pdf

I came up with this independently, but I am not surprised others have 
noticed the argument too.

Harvey went on to write:

 > However, I do not quite see how to give a proof of the usual Goedel's
 > Second without use of self referential sentences. I think that the
 > claim has been made that this can be done. What is the best effort
 > along these lines?

My notes give another proof of Goedel's second which doesn't use self 
reference explicitly, but, rather, shows how the self reference can be 
made implicit in a diagonalization argument. On his web page, Haim 
Gaifman has expository notes, "The easy way to Gödel's proof," which 
takes a different approach to the same end. (I wrote my notes after 
seeing an earlier version of his.)

Jeremy