[FOM] Proving FLT in PA

Robert M. Solovay solovay at Math.Berkeley.EDU
Tue Feb 21 20:40:57 EST 2006

One of the comments in the cited postings is silly. There is no need to 
use AC in the proof of FLT.

Proof (due to Kriesel). Drop to Godel's L where one has choice. FLT is 
arithmetic and so absolute between V and L.

On Tue, 21 Feb 2006, Timothy Y. Chow wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list