[FOM] Godel Sentences

[Harvey Friedman]

The well known demonstrable provable equivalence of all Godel sentences of
any reasonable theory within that same theory is perhaps implicit in Godel -
at least for PA - probably explicit in Hilbert Bernays, and surely given a
modern polished treatment in

S. Feferman, Arithmetization of metamathematics in a general setting,
Fundamenta Mathematicae 49, 35-92, 1960.

My use of the word "modern" here shows my advancing age.

The Hilbert Bernays "derivability conditions" were weakened in an important
paper by Robert Jerosolow, I think in the 1970's (perhaps a bit later),
which I don't have at my fingertips.

I think there are at least 20 good references for the whole business.

Here is a not very imaginative presentation. One can be more general and
more slick and much more complete in details.

Let T be any recursively axiomatizable theory containing a small amount of
arithmetic, and let a reasonable Godel numbering of sentences in the
language be given. Also let a reasonable formalization within T of the
notion of "n is the Godel number of a sentence in the language of T that is
not provable in T".

(The Hilbert Bernays derivability conditions are basic adequacy conditions
on the above setup. Jerosolow worked out a substantially more elemental
treatment, with weaker conditions).

For this purpose, a Godel sentence for T is a sentence A in the language of
T such that the following holds. Let n be the Godel number of A. Then T
proves 

A if and only if "n is the Godel number of a sentence that is not provable
in T". 

THEOREM. Let A,B be Godel sentences for T. Then T proves "A iff B". In fact,
T proves "A iff T is consistent".

Harvey Friedman