[FOM] Harvey Friedman's proof of Goedel's 2nd and MRDP

[Martin Davis]

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