[FOM] Non-constructive but predictive proofs
Martin Davis
martin at eipye.com
Sun Sep 16 14:35:45 EDT 2007
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
More information about the FOM
mailing list