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

[Timothy Y. Chow]

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