[FOM] Recursion Theory and Goedel's theorems

[Arnon Avron]

On Tue, Jul 24, 2007 at 10:42:20AM -0700, H. Enderton wrote:

> Maybe it's not clear that this undecidable sentence is Pi^0_1.  
> But  I still advance the claim that the heart of the 
> first incompleteness  theorem lies in recursion theory.

I am not sure. First, the fact that the undecidable sentence 
is Pi^0_1 is very important - these are the sentences
which are mechanically refutable in case they are false.
More important: Goedel's proof includes a procedure which
given an r.e. true theory, provides a true sentence 
(which we know to be true if we know that the theory is true!) 
which is undecidable in that theory. For me this is a 
positive part of the first incompleteness  theorem which 
is no less important than the negative part. Does recursion 
theory provide such a procedure too?

Arnon Avron.