[FOM] Proving FLT in PA

[Colin McLarty]

Joe Shipman wrote

> What I would expect to see is a metatheorem of the form "pi^0_1 
> statements proved using etale cohomological facts X Y and Z 
> applied to 
> sets of type A B and C are theorems of ZFC". That is, even 
> if X Y and Z need a strong assumption in order to be proven in
> their full generality, 
> the assumptions can be eliminated for applications of a certain type.

and Timothy Y. Chow

> To put your expectation in context, let me say that one might also 
> expect to see (1) a translation of SGA into English; (2) a more
> readable exposition of the material of SGA4, that is at the same
> level of generality and doesn't refer the reader to SGA4 for proofs. 
> Neither of these exists either.

The technical situation is probably much simpler than Joe expects in 
two ways.  Probably the metatheorem will have nothing to do with 
details of etale cohomology but will apply to all Grothendieck 
topologies.  And it will probably not use notions like $pi_0^1$ since 
it is a reduction to ZF and not to some fragment of second order 
rithmetic.   

But the practical situation is as bad as Timothy says and worse.  Or, 
we could say it is "better" depending on how you like open problems. 
Etale cohomology relies heavily on SGA 1, and the published version of 
that already says it should all be re-written 
in terms of SGA 4.  It has not been yet.  The re-write would not be a 
routine job for some MA thesis but as Timothy notes it is likely not to 
get anyone much credit either.  SGA 3 should also be re-written using 
SGA 4, not to mention the volumes that actually prove the duality and 
related theorems, SGA 5--7. 

These things are basically typewritten seminar reports and the people 
who understand them well are off doing new things in the same 
direction, not writing improved versions.  

Someday someone (or some people) will find essentially new insights to 
simplify the proof on finite simple groups.  This may or may not come 
from deliberate efforts to clarify the existing proofs.  Who knows?  
The same is true for etale cohomology and all topos cohomologies. 

best, Colin