[FOM] query about proving Fermat's last theorem in first-order PA

[Colin McLarty]

To Rupert McCallum: I am not sure what you mean by predicative, but as one
step in the proof which I would like someone to work through fully, let me
name the opening pages of
Ken Ribet's "On modular representations of Gal(Q-bar/Q} arising from
modular forms."  This is definitely not predicatively expressed.  Whether
it can be made predicative is a whole different question.

On the general question, let me quote something Angus said at Warwick
University (
https://urldefense.proofpoint.com/v2/url?u=https-3A__warwick.ac.uk_fac_sci_maths_research_events_2013-2D2014_nonsymp_fermat_&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=Vhd3XYsaXddzWjY4Fpbgj8QkYKlmpGGflvpI3eyIY34&s=tDUViIA3lRLFj8ERr08h3HODhyh9IiOEDUCMPTg8e4w&e= 
):

Peano arithmetic, although frequently described by logicians as far too
> weak for mathematics, is far too strong for mathematics.


I entirely agree with Angus, and for example with Harvey Friedman, that all
the concrete math we do (including FLT) can be done in PA.  In fact I think
Harvey may be right that FLT can be done in the finitely axiomatized
fragment Exponential Function Arithmetic.  But belief is not proof.  Angus
has been skeptical of the claim about EFA.  Here obviously there is no way
to decide except looking for proofs.

Like Timothy Chow I recommend that anyone interested in first order proofs
of FLT read Angus's appendix to his chapter 1 of "Kurt Gödel and the
Foundations of Mathematics: Horizons of Truth."   I will stress what Angus
says on page 8.  There are

a number of distinct regions of the proof, almost all hitherto unvisited by
> proof
> theorists..... Some but certainly not all this territory is known to some
> model theorists


Specifically on modular forms (Angus, page 16]

inspection shows no hint of higher-order maneuvers or associated
> obstruction to finite approximation. At the same time, I concede that
> spelling out the finite approximations would be a lengthy enterprise, and
> here it would be useful to have some metatheorems to apply.


This is where I begin to diverge form Angus's view.  He seems to insist,
and Timothy Chow seems to agree, that getting through those results would
just be a huge amount of routine work.  On the other hand I insist

A) We cannot really be sure how much work it would be.

and

B) We can be sure that if people try, they will find better concepts and
approaches to organize and simplify the tasks.  How far this will go
depends on how much insight can be found.  Maybe a lot.  Maybe not. There
are no guarantees how well it will work.

Angus on pages 19 and 23 quotes Georg Kreisel suggesting mathematical
benefits that might come from knowing a first order proof.

On the other hand, I will say the proof theory of FLT has always been
synecdoche for the proof theory of modern number theory.  It is (so far)
not about the 3-5 trick, or R=S strategy.  We are nowhere near that level
of detail yet.   Currently, it is about basic class field theory,
modularity, and cohomology.  These are all topics logicians could
understand much better than we now do -- proof theorists or model
theorists.

Colin

On Thu, Sep 5, 2019 at 11:39 AM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

> Rupert McCallum wrote:
>
> > Colin McLarty states in "What does it take to prove Fermat's Last
> > Theorem?" that when one thoroughly understands Wiles' proof of FLT it is
> > clear that in principle the argument can be made to go through in
> > nth-order Peano arithmetic for large finite n, but adapting the argument
> > so that it clearly goes through in first-order PA is far from trivial
> > (he describes how Angus Macintyre has proposed a program for doing
> > this). He also describes how some parts of the argument use
> > cohomological results whose standard proofs make use of a proper class
> > of inaccessible cardinals, but special cases tailored to the specific
> > applications needed can easily enough be seen to go through in Zermelo
> > set theory.
> >
> > I was wondering if anyone could point me to a specific part
> > of the proof such that it's definitely not clear how this part of the
> > argument is predicatively justifiable? I am currently trying to
> > understand the proof and would like to identify a point where it's
> > clearly using impredicative reasoning.
>
> It's not clear to me whether you've read through Macintyre's sketch.  If
> not, then I would recommend that you do so.  It's the appendix to Chapter
> 1 of "Kurt Gödel and the Foundations of Mathematics: Horizons of Truth."
> I make a few comments about Macintyre's sketch here:
>
>
> https://urldefense.proofpoint.com/v2/url?u=https-3A__mathoverflow.net_a_293081&d=DwIDbA&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=svWq_d4OsRZBeQlEa6cVItOU4l2L3dOl0dUIFEJpPg8&s=0NHVQ8oxAPQyDM-YZKOZdkk4BQ0MZdMbXivsA-FNG04&e=
>
> I'm not sure exactly what your definition of "predicative" is, and I'm
> also not sure what you mean by "clear."  As I try to explain in the above
> MathOverflow post, this particular research project is much more like an
> engineering project than a traditional mathematics research project.  In a
> traditional mathematics research project, the stumbling blocks typically
> are of the form, "I have no clue what to do next"; but once the light bulb
> goes on and you figure out what to do, actually doing it doesn't take that
> much time.  In an engineering project, it's typically the other way
> around.  You pretty much know what you need to do, but carrying it out
> takes a huge amount of grunt work.  In the process of doing the grunt
> work, you may run into unexpected obstacles, but they're rarely of the
> type that cause you to stop dead in your tracks because you can't figure
> out what to do.  Rather, you find that you have to do things slightly
> differently from how you thought you would at first.
>
> I don't think that there's any specific part of the proof of FLT where
> it's "definitely not clear" what to do in the sense that there is a known
> obstacle that people are stumped by.  It's true that there might be some
> point in the proof where one has to use slightly stronger axioms than one
> might naively expect, but there may be no way of detecting where these
> points are other than by slogging laboriously through the details.
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190905/496fb850/attachment-0001.html>