FOM: Another gap in Wiles's proof?

[Joe Shipman]

McLarty says that the material in "Modular Forms and Fermat's Last
Theorem" implicitly depends on Grothendieck Universes.  (Grothendieck's
"Universe Axiom" is equivalent to the existence of a proper class of
inaccessibles.)  I have the book on my desk and can verify that it is
full of references to Grothendieck's work.  Nowhere in the book
(according to my superficial perusal) is there any statement that the
results in the book depend on Universes.  McLarty assures us that this
is because the Universe assumption can always be eliminated.

I say, WHERE IS THE METATHEOREM?

The Universe assumption is not conservative over ZFC for pi^0_1
statements like FLT.  I can apply the metatheorem "If the set-theoretic
statement X proves the pi^0_1 statement Y, then the number-theoretic
statement Con(X) also proves the pi^0_1 statement Y" to show that the
Universe assumption U can be replaced by Con(U), but I can't eliminate
Con(U).  Maybe there's a metatheorem that says if you replace U with the
assumption of a single inaccessible you can still get the same results
specialized to "small" categories, and it may be a simple observation
that you only need small categories for Wiles's proof to go through, but
this still requires going beyond ZFC.  Maybe McLarty means that there is
some consequence of U that is conservative for pi^0_1 sentences that is
all that is actually needed for FLT, but THIS NEEDS TO BE STATED for the
proof to be complete.  For example, the statement of Tate's that McLarty
quotes may require ZFC+U rather than ZFC (Colin, can you please provide
details on how you formalize Tate's statement in ZFC and why it is
unprovable there) but may be conservative over ZFC for pi^0_1 sentences;
this would mean ZFC proves FLT but it NEEDS TO BE STATED.  Maybe the
"acting as if proper classes are sets" is not so dubious after all and
only requires a "classy" extension of ZFC like MK rather than an
inaccessible, but THIS NEEDS TO BE STATED.

If in fact there is no metatheorem, and an ad hoc argument is needed for
each particular theorem to eliminate the Universe assumption, then WILES
NEEDS TO DO THIS AND PUBLISH IT before someone else does it for FLT and
argues that he is the person who filled the final gap and "really proved
it".

If it is not really necessary for Wiles to do this, then Harvey is wrong
about the special role of ZFC.

Barry Mazur, you're probably the best-equipped FOMer to settle this --
please help!

-- Joe Shipman