[FOM] 18 Word Proof of the Godel, Rosser and Smullyan Incompleteness Theorems
eipye at pacbell.net
Fri Jul 16 18:01:07 EDT 2010
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.
More information about the FOM