FOM: Nice idea works

[Colin McLarty]

        Yes, you can formalize Grothendieck's program inside of ZFC, yet
pretty much verbatim, by altering his definition of universes to simply say
they are sets V(i) for i a limit ordinal greater than w. I find no trace of
anyone doing this before though it would hardly be surprising if someone
did. I will say a bit about how it works but first look at Kanovei's
pertinent question: If it works then why was it not done long ago?

        The forwards from Feferman are clear that he has two interests, and
I think these are typical of people thinking about universes: Find the
weakest formal system that can accomodate the number theoretic proofs, and
explore very strong systems that yield some of the "symmetry" that category
theorists want. This second interest is reflected (no pun intended) in
Feferman's obsrvation that his method: 

>is one way to show
>that the distinction between small and large categories or between
>categories in one universe and those in another universe, is not an
>essential distinction, though something like it seems to be needed for the
>current set-theoretical foundations of category theory.

The foundation I describe achieves neither of these goals. It does preserve
Grothendieck's methods within ZFC.

So, in ZFC, define a "universe" to be any set V(i) for i a limit ordinal
greater than w. Thus each universe interprets Zermelo set theory with choice
(and more as Kanovei pointed out). Require all "groups" and "rings" and
"fields" and "topological spaces" and "schemes" etc to be members of V(w+w).
Notice we may freely invoke the axiom of replacement to study analysis, or
whatever. If you like, you could call these "small groups" et cetera. but we
will not need any others so there is no use for the name. These are the
objects of what Shipman calls "ordinary mathematics".

Do not bound the rank of categories or functors. Call a category "small" if
it is a member of V(w+w), and more generally "i-small" if it is a member of
V(i). Here is the only faintly subtle point: usually a "sheaf" on a small
category takes sets in V(w+w) as values; but to be explicit whenever we
speak of a sheaf on a category we must say which universe it takes values in.

That's it. All the large categories mentioned in a book like MODULAR FORMS
AND FERMAT'S LAST THEOREM are members of V(w+w+w). Some even bigger
constructions are used, but they are available here. Grothendieck's general
category theory does not use replacement so it can all be interpreted inside
of any universe, or pair of successive universe if it involves a large
construction such s forming the topos of sheaves on a given category.