[FOM] 18 Word Proof of the Godel, Rosser and Smullyan Incompleteness Theorems

[Martin Davis]

On July 16, 2010 Harvey Friedman wrote:

>Goedel's proof of 1 for PA requires less - that no sentence and its
>negation are provable.
>
>Goedel's proof of 2 for PA requires less - that every provable Sigma01
>sentence is true.

These assertions are true in spirit but as a matter of historical 
fact, they are false. When Goedel wrote his famous 1931 paper, one of 
his concerns was to demonstrate clearly that the undecidability 
phenomenon was not limited to comparatively weak systems like PA. He 
chose to present his proof in the context of his system P, 
essentially the simple theory of types together with the Peano axioms 
for the lowest type. Moreover he emphasized that the results would 
hold if a primitive recursive omega-consistent set of additional 
axioms were added, as well as for systems like ZF. He said nothing about PA.

However, he did supply the basic technique for obtaining arithmetic 
equivalents of primitive recursive relations, namely the Chinese 
Remainder Theorem. The missing step in obtaining his results for PA 
was to show that the Chinese Remainder Theorem is provable in PA, and 
Goedel surely knew how to carry out this exercise.
The details were later carried out in the Hilbert-Bernays classic.

Martin Davis