[FOM] Proving FLT in PA

[joeshipman@aol.com]

Tim , one place you've seen it raised is on the FOM, by me, in 
March/April 1999.

Friedman, in this post,

http://www.cs.nyu.edu/pipermail/fom/1999-April/002974.html

reports that, according to an expert source, the use of Grothendieck 
Universes (that is, infinitely many inaccessible cardinals) is not 
necessary in Wiles's proof of FLT and all the top number theorists know 
how to eliminate the assumption.

However, there are many other theorems of number theory and algenraic 
geometry proved that use the full machinery Grothendieck and others 
developed, and nobody ever gave a satisfactory answer to my repeated 
query "WHERE is the metatheorem that allows us to tell when the 
'Universes' assumption can be eliminated?"

I think this ought to be considered scandalous.

The 1993 newsgroup discussions you link to seem to be more worried 
about eliminating AC from Wiles's proof than about eliminating the 
Universes assumption, but that's just silly, because in this case there 
IS a metatheorem, due to Godel, that any arithmetical statement 
provable from ZFC (or even from ZFC + V=L) is provable in ZF.

Obviously, one can't simply say "statements of a certain form which are 
provable with Grothendieck Universes are theorems of ZFC", because 
Con(ZFC) is of a very simple logical form and follows almost trivially 
 from the Universes assumption. What I would expect to see is a 
metatheorem of the form "pi^0_1 statements proved using etale 
cohomological facts X Y and Z applied to sets of type A B and C are 
theorems of ZFC". That is, even if X Y and Z need a strong assumption 
in order to be proven in their full generality, the assumptions can be 
eliminated for applications of a certain type.

-- Joe Shipman


Chow:

>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.