FOM: Number theory and elementary arithmetic

[Jeremy Avigad]

A few weeks ago Harvey Friedman brought to my attention a posting by Matt
Frank (reproduced below) and prompted me to finish revising a draft of a
paper that is relevant to the posting. I have done so; it is called
"Number theory and elementary arithmetic," and it is posted on my web
page, http://www.andrew.cmu.edu/~avigad, under "surveys".

In this paper, I discuss Friedman's conjecture that FLT is derivable in
elementary arithmetic. Of course, there is little clear sense that one can
ascribe to notions like the "likelihood" that such a conjecture is true;
instead, I focus on explaining what can be done in elementary arithmetic
and conservative extensions, and how.

The short story is that Matt is absolutely right: one can carry out a
surprising amount of analysis in restricted fragments of arithmetic, but
we are a long way from having a sense as to whether one can
handle the kind of machinery that went into the proof of FLT.

In the paper I also try to clarify some general issues related to
Friedman's conjecture. One issue (that has, I think, befuddled past FOM
exchanges) has to do with varying senses of the word "need".

One sense of the word "need" is nicely captured by formal notions of
derivability. For example, if FLT is derivable in elementary arithmetic,
one might say that this shows that the proof of Fermat's last theorem does
not "need" infinitary notions.

But there is also vaguer (albeit no less interesting) sense of the word
"need". One might argue that even if FLT is derivable in elementary
arithmetic, such an elementary proof may really encode analytic or
infinitary notions, which are in fact "needed" to make the proof
understandable. It seems to me that neither formal logic nor the
philosophy of mathematics currently has a clear methodology for making
sense of this latter notion of necessity, or even the claim that analytic
or infinitary methods can be *useful* in proofs of number theoretic
statements. We can point to notions like length of proof; but while the
length of formal derivations certainly has something to do with it, it is
a fairly crude measure, and unlikely to provide much real insight.

Jeremy Avigad


Here is Matt Frank's posting (from May 10):

> 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