FOM: Alternatives to ZFC in actual use

[Colin McLarty]

Joe Shipman wrote:

>Here is my question: was any statement of ordinary mathematics (that is,
>a statement about sets of rank less than omega+omega) ever proved from
>Grothendieck Universes, in which the Universe assumption was really
>used? 

        Short answer: yes, the Weil conjectures, Faltings's work (including
the proof of the Bieberbach conjecture), Wiles's theorem--pretty much
anything that uses derived functor cohomologies.

        Longer answer: proofs like these are not given from the ground up.
For example Deligne published his proof of the last Weil conjecture in a 34
page article (in 1973) which relies heavily on Grothendieck's Seminaire de
Geometrie Algebrique du Bois Marie--where Grothendieck used his universes.
Obviously all the steps can be filled in without universes, just as Harvey's
recent combinatoric theorems can be proved without using subtle cardinals
(only assuming their consistency with ZFC). Three years later Deligne
published a book showing how to actually circumvent toposes in his proof,
and thus avoid SOME appeals to Grothendieck universes. That is Deligne's SGA
4 1/2 (Springer Lecture Notes in Math no.569) and its bibliography gives
references to everything I've mentioned. Has anyone checked how the whole
proof would look in ZFC without universes? I doubt it.

        The more common way to avoid Grothendieck universes in this part of
number theory is to forget rigor. See for example _Introduction to Etale
cohomology_, Gunter Tamme (Springer-Verlag, c1994). A very nice book on its
subject but unconcerned with FOM. It simply ignores the difference between
sets and proper classes and assures the reader (quite correctly in practice)
that this will not lead to any trouble.