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

[H. Enderton]

 Martin Davis wrote:   >> 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.

>And then Arnon Avron objected:
>The trouble with this proof is that it misses ...  the actual
>construction of a *true* sentence which the system fails to prove,
>and a *proof* that it is true.

I think the proof Martin Davis describes works better than you
are giving it credit for.  We show that the set of arithmetic
truths is not r.e. by showing that recursive sets are arithmetical,
whence K and its complement (for example) are many-one reducible
to the theory of true arithmetic.

Then for any recursive set of true axioms ("true" to avoid
Torkel's point), that fact that K is creative does indeed yield the
construction of a specific true but unprovable sentence.  Moreover,
examination of that sentence shows that it says "I am unprovable"!
So maybe there are not so many different proofs after all.
(Supporting details are on page 257-258 of the the second edition
of my logic book.)

--Herb Enderton