[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: FOM <fom@math.psu.edu>*Subject*: Re: FOM: computer proofs*From*: Vladimir Sazonov <sazonov@logic.botik.ru>*Date*: Thu, 03 Dec 1998 02:26:27 +0300*CC*: "Sazonov, Vladimir" <sazonov@logic.botik.ru>*Organization*: Program Systems Institute, RAS*References*: <98Dec2.101739edt.15577-23704@dvp.cs.toronto.edu>*Reply-To*: sazonov@logic.botik.ru*Sender*: owner-fom@math.psu.edu

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

**References**:**Stephen Cook**- FOM: computer proofs

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]