No subject

[Jeff Remmel]

I agree with John Baldwin about the foundational aspects of Matijesvic' theorem.
Certainly one way to look at Matijasevic' results is that it is a coding 
result, i.e. one can code any arbitrary r.e. set as the solution set 
of a diophantine equation.  It is a spectacular coding result but it 
is no different than the coding results which establish many other 
undecidability results such as the word problem on groups, etc. The 
foundational import is due to the work of Godel, Church, Post, Turing, 
Kleene, etc who estabilished a formal definition of computable function 
which seems to capture the intuitive notion of computable function.
If at some point, someone was able to come up with an acceptable 
computable procedure which is outside of current definition of 
computable function, then of course, Hilbert's 10-th problem would 
have to be revisted.  This is true of all undecidability results, 
many counterexamples in recursive mathematics, etc.  I think that 
the reason that Matijasevic' result is important is that it showed 
that undecidability results appear naturally in mathematics. This 
is very much what Harvey is trying to do with his results which 
show that results which require large cardinals can occur in 
setting that most mathematicians would consider as natural.

I forgot now who first brought up the idea of generally 
acceptable proof methods, but there is still considerable 
controversy about what is an acceptable proof as is witnessed by 
the controversy about computer aided proofs that has occured recently in 
the Notices.  There are some mathematicians who are very uncomfortable 
with proofs that rely on verification of computations or case 
analysis which are done by the computer.  However such proofs 
are clearly going to become much more common as the sybolic 
computation packages such as Maple, Mathematica, etc 
are becoming a research tool used by an increasing number of 
mathematicians in a variety of fields.  Then there is 
the idea of proof which can be verified by checking a small 
number of random bits which has emerged from the work on 
interactive proof checkers in computer science.  Do we 
want to accept proofs which have a greater 1 - 1\10^20 chance 
of being true?.  Is that some how different than the proof 
for the classification of finite groups which because of its 
length and complication is extremely difficult to understand 
and check?  


Jeff Remmel