FOM: My wrap on universes

[Colin McLarty]

        Joe Shipman asked whether Grothendeick universes were ever used to
prove a theorem of ordinary mathematics. Privately he confirmed that he was
not asking whether they were formally indispensible to any such theorem, but
whether they occur in the published proof. I answered that they do occur, in
famous results, though it is known they are formally eliminable. The experts
agree with this.

        I say that a proof "uses universes" if it not only quantifies over
universe-sized sets, but also defines those sets by properties that quantify
over universe sized sets. Every textbook on cohomological number theory does
this. Hartshorne ALGEBRAIC GEOMETRY does extensively. Wiles's paper
justifies a key step by reference to a proof that uses universes in this
sense. Papers in MODULAR FORMS AND FERMAT'S LAST THEOREM routinely do this.
They could avoid it. But the authors want people to understand the argument.

        And I pose an analogy between Grothendieck's and Friedman's
attitudes towards "essential use" of a principle:

        Friedman has combinatorial theorems formally provable in ZFC plus
some consistency assumptions on cardinals. Friedman regards those proofs as
essential uses of the cardinals themselves since the consistency statements
have no genuine mathematical meaning.

        Grothendieck and his heirs have theorems of number theory formally
provable in ZFC. Grothendieck regards those proofs as essential uses of
universes since the proofs which eliminate universes have no genuine
mathematical meaning.

        The real questions of how to formalize universes, and how to
interpret their use in the literature, have been obscured by sweepingly
false claims such as "The use of universes in FLT - or any serious number
theory has never, even remotely, been any kind of issue". Can anyone name a
single textbook on cohomological number theory that does not use universes,
in the sense defined above?