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

[Arnon Avron]

> 
> 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.
> 
> Martin

This is indeed the first proof (out of 3) that Smullyan presents
in his book on the incompleteness theorems. The trouble with this 
proof is that it misses one of the most important aspects of Godel's
proof: the actual construction of a *true* sentence which the system
fails to prove, and a *proof* that it is true. The most interesting 
debates concerning the implications of Godel's theorem are connected
with this aspect (in particular: the debate about Lucas-Penrose argument).

Arnon Avron