[FOM] Proving FLT in PA

[Robert M. Solovay]

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
>