[FOM] Proving FLT in PA

Timothy Y. Chow tchow at alum.mit.edu
Tue Feb 21 19:00:09 EST 2006

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 


Tim Chow

More information about the FOM mailing list