[FOM] Proving FLT in ZF (was in PA)
Colin McLarty
colin.mclarty at case.edu
Mon Feb 27 13:51:36 EST 2006
Harvey Friedman wrote, quite rightly, on the use of universes in
proving FLT:
> So I gather from this that as it stands, the
> current proof of FLT is not conducted even within
> ZFC, but instead within some fairly modest
> extension of ZFC. Furthermore, that, in your opinion,
> this state of affairs is unlikely to change in the
> near future because of a lack of incentive
> for the relevant people to do the necessary work.
Only I would add that they feel the work is routine. I do not think
it is any intransigeant disregard for formalization.
I am pretty sure this is the best prospect for a principled proof in
ZF that stays close to Grothendick's strategy: The arguments of the
SGA (which are cited by Wiles) do use universes in universes. But
with one exception they do not use replacement in any universe. The
arguments within any universe are really just Z arguments, Zermelo set
theory (maybe with choice, I have not worried about that). That needs
to be checked more thoroughly but I am not just flying blind on it.
So for all but this one theorem you could weaken the definition
of "universe" to any transitive set that models Z. ZF already gives
proper-class many of these. (They are just V at each limit cardinal,
aren't they?)
The one proof that uses replacement is the one saying that the
category of sheaves of modules over any Grothendieck topos has enough
injectives. In many concrete cases there are easy work arounds for
this. In general I believe (though I have not gone back to check
this) you can use any site for a topos to bound the length of the
replacement needed for this theorem over that topos. The bounds based
on Grothendieck's original argument (in the paper called Tohoku) are
much bigger cardinals than mathematicians usually think about, but
they all provably exist in ZF.
So I believe the whole thing can be done in nearly Grothendieck's way,
for any one set of Grothendieck topologies, using "weak universes" in
the sense of sets that model Z and have sufficient, but cardinally
bounded, replacement.
Okay, I have some parts of that written up and should go ahead with
the rest. But that means I have to check through all of the SGA--
though really the issues will all be in SGA 4 and Tohoku. And even
myself, while I do not hope to advance algebraic geometry on this
level, keep getting pulled away by other interesting issues in the SGA.
There are numerous places in the SGA that cry out for re-organization
and simplification, and even where Grothendieck in the texts calls for
this. And such reorganization can suddenly open up into a huge
project.
In the long run these methods will get a lot of both routine
expository improvement and radical conceptual improvement by hard new
theorems. If only I could predict which issues need which kind of
work!
best, Colin
More information about the FOM
mailing list