FOM: computer proofs
Vladimir Sazonov
sazonov at logic.botik.ru
Wed Dec 2 18:26:27 EST 1998
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
More information about the FOM
mailing list