[FOM] Proving FLT in PA

[Timothy Y. Chow]

Harvey Friedman wrote:
> I was wondering if you could give some sort of indication of some of the 
> difficulties involved, and work needed, to show that FLT is provable in 
> PA or even in EFA?

Here's one issue I've seen raised.  The fundamental facts of etale 
cohomology are developed in SGA, specifically SGA4, and Grothendieck 
universes are (apparently---I've never studied SGA4) freely assumed 
whenever necessary.

The experts seem to feel that for a "concrete application" like FLT, it 
would be routine to eliminate any use of Grothendieck universes.  In 
particular, there's probably no interesting math involved in the 
elimination process.  However, unless someone actually goes to the trouble 
of doing the necessary bookkeeping, there remains a question mark.  
Unfortunately, because of the highly technical nature of the subject, 
doing the bookkeeping would seem to require an inordinate amount of 
effort.

References:
http://groups.google.com/group/sci.math/msg/af38a0ad1d7e878b
http://groups.google.com/group/sci.math/msg/c7a5c4fd185e06ef

Tim Chow