From: ENAYAT@american.edu Newsgroups: sci.math.research Subject: Re: [Q] Is proof of Fermat's Last Theorem within Peano Arithmetic? Date: Sat, 06 Jun 98 16:39:41 EDT In article <3576B90A.771C@win.tue.nl> Tom Verhoeff writes: > >Is the (current) proof of Fermat's Last Theorem (FLT) by Wiles et al., >and subsequently simplified by others (?), a proof (that can, >in principle, be reduced to a proof) from the axioms of Peano Arithmetic >(PA) for natural numbers? > Your question is on many people's minds, and the answer seems to be unknown. Many suspect that the current proof cannot be carried out in PA, but the definitive answer is yet to emerge. On a recent visit of Wiles to our campus last month I asked him the same question, and he simply said that he does not know whether PA can prove FLT, and I suspect the question struck him (as it seems to strike many non-logicians) as one which is of limited interest. Although most mathematicians know of the so-called Peano's axioms, they know of it as what logicians refer to as a "second order theory", i.e., one which is couched in a formal language allowing not only quantification over elements of the domain of discourse, but also subsets of the domain of discourse. On the other hand, what logicians commonly refer to as Peano Arithmetic, is the "first order projection" of the second order theory, i.e., one in which the second order axiom of induction is replaced by the so-called induction scheme, which consists of a set of first order axioms asserting that any first order definable subset which includes 0 and is closed under successor is equal to the whole set of natural numbers. The logicians move to the first order theory is motivated by the fact that first order logic is "complete", in the sense that there is a set of axioms and rules of inference for which the concepts "provable" and "true in all models" coincide, but as a consequence of Godel's incompleteness theorem, no such proof system exists for full-second order logic. There is a first order theory, confusingly referred to as "second order number theory", which "should" be able to accomodate the existing proof of FLT. There is a brief discussion of this theory in H. Enderton's classic text " A Mathematical Introduction to Logic", at the very last section of the text entitled "Models of Analysis" (In this usage, Analysis = Second Order Number Theory"). Of course second order number theory is subject to Godelian incompleteness. The definitive text on the subject is "Subsystems of Second Order Arithmetic", by Stephen Simpson of Pennsylvania State University, which is scheduled to be appear in 1998 (by Springer-Verlag). Ali Enayat Dept. of Math. and Stats. American University Washington, D.C. 20016-8050 e-mail: enayat@american.edu