FOM: Does PA prove FLT?

[Matthew Frank]

On Tue, 30 Apr 2002, wiman lucas raymond wrote:

> Wiles's proof of Fermat's last theorem has been pretty much accepted by
> the experts in his field.  His proof, however, uses very powerful
> techniques in arithmetic algebraic geometry.  Is is possible to
> translate his proof into a strictly Peano arithmetic version, or is
> this still an open question?

I'm surprised no one has responded to this.  Here's my impression of the
state of things:

The current proof of Fermat's last theorem appears to be predicative.  For
predicative systems like Feferman's (higher-order) or ACA_0 (second-order)
there are procedures for translating proofs of arithmetic statements into
proofs in Peano Arithmetic.

So the real question is the predicativity of the proof.  Knowledgeable
mathematicians say that the proof does not rely crucially on discontinuous
functions (this according to something I heard from Harvey Friedman, who
interviewed some such mathematicians on this question).  Since the
mathematics of continuous functions is predicative, this is good evidence
for the predicativity of the proof.  On the other hand, the proof is still
so long and hard to understand that it is hard to be confident of these
claims.

Harvey Friedman has made the conjecture that Fermat's last theorem is
provable not just in Peano arithmetic but in the weaker system of
exponential function arithmetic (whose provably total functions are
bounded by towers of exponentials).

A good comparison for all this is the complex-analytic proof of the Prime
Number Theorem, and Takeuti's demonstration (in Two Applications of Logic
to Mathematics) of how to reduce it to Peano arithmetic.  If and when the
algebraic geometry proving Fermat's Last Theorem becomes as well exposited
and well known as the complex analysis proving the Prime Number Theorem,
we presumably will be similarly confident that the proof of Fermat's Last
Theorem can be rendered in Peano arithmetic.  However, the wait promises
to be long for that algebraic geometry to become so well known.

--Matt