[FOM] Harvey Friedman's proof of Goedel's 2nd and MRDP
Martin Davis
martin at eipye.com
Mon Dec 18 11:19:59 EST 2006
Regarding Harvey's neat proof of Goedel's 2nd incompleteness theorem
http://www.cs.nyu.edu/pipermail/fom/2006-December/011194.html
I believe that using MRDP would simplify the formal details greatly.
Reminder:
MRDP: For every r.e. set S, there is a polynomial p(t,x1,...,xk) with
integer coefficients such that
S = {t | (Ex1,...,xk)(p(t,x1,...,xk) =0)}
A corollary is the Universal Diophantine Equation theorem:
There is a polynomial p(n,t,x1,...,xk) such that if we write:
S_n = t | (Ex1,...,xk)(p(n,t,x1,...,xk) =0)}
every r.e. set is S_i for some i.
Suggestion: In Harvey's proof, avoid the issue of formalizing the
theory of Turing machines in PA by using the universal equation
instead. The equation can be written directly as a quantifier-free
formula of PA with no coding.
Harvey mentions the need remaining for a formal proof predicate. MRDP
can help here as well. Only need to prove that the theorems of PA are r.e.
From a pedagogic point of view, if one wants to do this but avoid
the modicum of number theory needed to prove MRDP, a compromise is
available: Work with PA+ which is PA augmented by the defining
recursion equations for the exponential function: x^0 =S0; x^Sy =
(x^y)*x. Then, instead of MRDP one can get by with RDP (every r.e.set
is exponential Diophantine). Neat proofs involving almost no number
theory of RDP are available: using register machines
(Jones-Matiyasevich), using Turing machines (Matiyasevich).
Martin
Martin Davis
Visiting Scholar UC Berkeley
Professor Emeritus, NYU
martin at eipye.com
(Add 1 and get 0)
http://www.eipye.com
More information about the FOM
mailing list