[FOM] Proving FLT in ZF (was in PA)

[Colin McLarty]

Harvey Friedman wrote, quite rightly, on the use of universes in 
proving FLT:

> So I gather from this that as it stands, the 
> current proof of FLT is not conducted even within
> ZFC, but instead within some fairly modest
> extension of ZFC. Furthermore, that, in your opinion,
> this state of affairs is unlikely to change in the
> near future because of a lack of incentive 
> for the relevant people to do the necessary work.

Only I would add that they feel the work is routine.  I do not think 
it is any intransigeant disregard for formalization. 

I am pretty sure this is the best prospect for a principled proof in 
ZF that stays close to Grothendick's strategy:  The arguments of the 
SGA (which are cited by Wiles) do use universes in universes.  But 
with one exception they do not use replacement in any universe.  The 
arguments within any universe are really just Z arguments, Zermelo set 
theory (maybe with choice, I have not worried about that).  That needs 
to be checked more thoroughly but I am not just flying blind on it.

So for all but this one theorem you could weaken the definition 
of "universe" to any transitive set that models Z.  ZF already gives 
proper-class many of these.  (They are just V at each limit cardinal, 
aren't they?)   

The one proof that uses replacement is the one saying that the 
category of sheaves of modules over any Grothendieck topos has enough 
injectives.  In many concrete cases there are easy work arounds for 
this.  In general I believe (though I have not gone back to check 
this) you can use any site for a topos to bound the length of the 
replacement needed for this theorem over that topos.  The bounds based 
on Grothendieck's original argument (in the paper called Tohoku) are 
much bigger cardinals than mathematicians usually think about, but 
they all provably exist in ZF. 

So I believe the whole thing can be done in nearly Grothendieck's way, 
for any one set of Grothendieck topologies, using "weak universes" in 
the sense of sets that model Z and have sufficient, but cardinally 
bounded, replacement.
 
Okay, I have some parts of that written up and should go ahead with 
the rest. But that means I have to check through all of the SGA--
though really the issues will all be in SGA 4 and Tohoku.  And even 
myself, while I do not hope to advance algebraic geometry on this 
level, keep getting pulled away by other interesting issues in the SGA.

There are numerous places in the SGA that cry out for re-organization 
and simplification, and even where Grothendieck in the texts calls for 
this.  And such reorganization can suddenly open up into a huge 
project.

In the long run these methods will get a lot of both routine 
expository improvement and radical conceptual improvement by hard new 
theorems.  If only I could predict which issues need which kind of 
work!

best, Colin