[FOM] Non-constructive but predictive proofs

[Martin Davis]

In a previous post, I wrote that I couldn't think offhand of a 
good  example of a non-constructive predicative proof. (Harvey 
Friedman supplied such in a subsequent post.)

I had forgotten that a proof of just this character had played an 
important role in my early career: A Diophantine relation on the 
natural numbers is one expressible in the form
                  (Et1 t2 ... tk)[p(x1,x2, ...,xn,t1,...,tk) = 0]
where p is a polynomial with integer coefficients. Working on my 
dissertation (in 1949), I proved that there is a Diophantine relation 
whose negation is not Diophantine. The proof was simple but quite 
non-constructive: the class of Diophantine relations is closed under 
existential quantification. Were it also closed under negation, it 
would also be closed under universal quantification and hence, 
include all arithmetically definable relations. But, since all 
Diophantine relations are r.e., this is obviously impossible.

It was this result that gave me the courage to conjecture, 20 years 
before it was proved, that all r.e. relations are Diophantine, what 
Yuri Matiyasevich has called Davis's daring hypothesis.

Martin


                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com