[FOM] Weaker foundations for FLT

[Colin McLarty]

We now have thoughts about proving FLT in ZF, 3rd order PA, and EFA.

Harvey well points to some particulars of my strategy for Grothendieck 
techniques in gneral into ZF.  Taking those into account I think I can 
replace universes by V(lambda) where lambda are suitable ordinals (all 
provably existing in ZF), and "suitable" means that V(lambda) supports 
a certain amount of second order replacement, which is adapted to work 
for a given site (or set of sites).  I will look at it.

The question of ZFC helps me to focus something I keep trying to say 
more clearly: Grothendieck's use of universes is not to gain vast 
generality or to MAXIMIZE in Pen Maddy's sense or to have large 
cardinals.  It is just a quick and dirty way to get enough elbow 
room.  So relativizing to constructible sets is fine.  It loses 
nothing that we want.  So we cannot need the Axiom of Choice.  We can 
just do it all in constructibles.  I have not looked into how often 
choice is even ostensibly used in SGA style proofs.  It certainly is 
in some.

Solovay wrote:

>     As the cited book shows the Wiles-Taylor proof is a truly
>enormous beast. The work naturally seems to be carried out in third 
order
>number theory, and to compress it into PA seems a heroic if not 
impossible
>task.

Okay, with this nuance:  Look at Washington's article on Galois 
cohomology in the book.  It introduces group cohomology as a derived 
functor cohomology, which on the face of it uses a universe.  But the 
point of the article is to say that we really only need the 0- 1- and 
2- dimensional cohomology groups of some structures coming from 
arithmetic. These have explicit constructions in some low-order PA 
(indeed the constructions were known to Emmy Noether in the 1930's 
before group cohomology existed).  I will take Solovay's word that it 
is 3rd order, I have not looked into it.

This is a strategy of ``work-arounds.''  Wherever Wiles uses a theorem 
from Galois cohomology we need to find a work-around getting the 
specific information he needs without the general theory.  This can 
surely be done, but of course the result will be specific to FLT.  
Other theorems would need other work-arounds.

I suspect this is the main reason that algebraic geometers have not 
worked harder on our problem--they know that easy work-arounds exist 
and will be uninteresting in themselves.   

As to a proof in EFA, I am no expert but I think it would take real 
new insights if it exists at all.  Maybe really good insights.  I 
think I agree with Solovay here?  I do not at all doubt the theorem is 
provable in EFA.  I just have no idea.  But the current proof will 
probably not compress that far without being fundamentally reconceived.

There has lately been progress on the algebraic geometry side, which I 
just noticed.  Angelo Vistoli has substantially re-written SGA 1 in 
the terms of SGA 4, as Grothendieck said someone should do when he 
first published SGA 1.  This is in an AMS book FUNDAMENTAL ALGEBRAIC 
GEOMETRY published last Fall and just arrived in my university library 
this week.  Others in the book rewrite theorems from the rest of 
Grothendieck's algebraic geometry.

This does not go directly to the logical question but is part of an 
overall clarification that will help clarify the logic in the long 
run.