[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
> Tim Chow
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM