[FOM] Algorithmic view of Goedel incompleteness
Martin Davis
martin at eipye.com
Thu May 8 15:07:05 EDT 2003
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?
More information about the FOM
mailing list