FOM: computer proofs

[Vladimir Sazonov]

Stephen Cook wrote:

> This brings up an interesting question:   Is there a formal version of
> Wiles' proof in ZFC which has feasible length?  More problematical
> is the same question for PA.

First, it would be very strange if Wiles' proof of FLT (implicitly?)
uses 
some new principle outside ZFC or even some known large cardinal axiom
or 
the like. 

[I do not think that Stephen Cook has such opinion, but I say this for 
completeness. Analogous question: to resolve or understand something 
essential on another problem "P=NP?", which seems should be more 
interesting for fomers, do we need some strong set-theoretic principles, 
even Choice Axiom? do we need full strength of ZF or PA or PRA? is not 
bounded induction axiom enough? is not more reasonable to concentrate 
attention even on much weaker feasible arithmetic which postulate that 
some "concrete" large number is infeasible?]

Second, it seems that it should be a routine to convert Wiles' proof 
which was written *by hands* into a formal feasible proof in ZFC with 
using some abbreviation mechanism. 

It is unreasonable to consider the *ordinary* mathematics with 
abbreviations forbidden. But it is interesting to know which kind of 
abbreviations extending some system of first-order logic (say, natural 
deduction) is enough to derive feasibly all the contemporary 
mathematical theorems from ZFC. In principle it could be possible that 
for new interesting proofs from ZFC axioms we should invent some new 
kinds of abbreviations to present these proofs formally and feasibly. 
Is there a "complete" system of abbreviations which will be practically 
enough? Probably Randy Pollack can comment this? Recall the following 
citation from his last message to fom: 

> the business of completely formal mathematics (or "explicit
> mathematics") is largely finding formal systems that we believe and
> that support proofs of feasible length

Finally, can we rigorously *prove* in any reasonable sense that such 
and such kinds of abbreviations are "complete", i.e. "enough", or 
there should be some analogue of G"odel's incompleteness phenomenon? 


Vladimir Sazonov