[FOM] Algorithmic view of Goedel incompleteness

[Martin Davis]

I believe that some light on the ongoing discussion of Goedel's finding a 
"true" but unprovable sentence of number theory can be shed by taking 
advantage of the most basic results of recursive function theory, aka 
computability theory or recursion theory (in particular the existence of 
creative sets), and the work on Hilbert's 10th Problem, aka MRDP  (my 
preference :-) ) or Matiyasevich's Theorem). Two points:
1. None of this is even remotely new
2. This is meant to apply only to the 1st incompleteness theorem, not to 
the unprovability of consistency.

First, without reference to any particular formal system, let us consider 
what the minimum requirements would be for someone's claim that some 
certain string of symbols may be viewed as a "proof" of some assertion. For 
our purpose we can restrict ourselves to proofs of propositions that state 
that some polynomial equation p=0 with integer coefficients has NO solution 
in natural numbers. Note that verifying that some particular numbers do 
satisfy the equation is a matter of simple elementary-school arithmetic. So 
saying that some assertion of this kind is TRUE says no more than that 
there are no numbers for which this can be done.

Presumably the deviser of a proof would wish to show it to others in order 
to convince them that it really is a proof of what is being maintained. We 
may interpret this to mean that there must be an agreed upon algorithm to 
determine whether for a given pair <E,p>, the string E is indeed a proof 
that the equation p=0 has no solutions. (Of course formal systems like PA 
and ZFC do satisfy this condition.) Such a proof system is SOUND if the 
equations p=0 for which corresponding proofs exist indeed have no solutions

If we accept this and agree with the Church-Turing thesis, then we can 
prove that following version of Goedel incompleteness:

There exists (and can be displayed) a particular polynomial
                             p(a,x_1, ...,x_n)
such that for any particular sound proof system there will be a 
corresponding number a_0 such that the equation
                             p(a_0,x_1, ...,x_n) = 0
has no solutions in natural numbers but that assertion is not provable with 
respect to the given proof system. In fact the value of the number a_0 can 
be computed from a precise specification of the algorithm defining the 
proof system.

What would Herr W say about that?