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