[FOM] Proving FLT in PA

[John Baldwin]

Can anyone provide some examples of the kinds of results in Algebraic 
geometry which do use Grothendieck universes?

This post is prompted by the following remarks concerns the use of 
axioms beyond ZF for the proof of 
Fermat's last theorem.

The existence of a Grothendieck universe is equivalent to the existence of
a strongly inaccessible cardinal.


On Tue, 21 Feb 2006 joeshipman at aol.com wrote:

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

John T. Baldwin
Director, Office of Mathematics Education
Department of Mathematics, Statistics, 
and Computer Science  M/C 249
jbaldwin at uic.edu
312-413-2149
Room 327 Science and Engineering Offices (SEO)
851 S. Morgan
Chicago, IL 60607

Assistant to the director
Jan Nekola: 312-413-3750