Enhancing Grothendieck's universes and Grothendieck's axiom: Feferman's universe

Question

A Grothendieck's universe is such a set $U$ so that

• $\forall x \in U, x \subseteq U$,

• $\forall x,y \in U, \{x,y\} \in U$,

• $\forall x \in U, \mathcal{P}(x) \in U$,

• given a family $(X_i)_{i \in I}$ such that $I \in U$ and any $X_i \in U$ we have $\bigcup_{i \in I} X_i$,

• $\mathbb{N} \in U$.

We can "do set theory" inside a single Grothendieck's universe. However, the existence of a single universe wasn't enough for Grothendieck, he introduced the axiom of universes:

Let $X$ be a set. Then there is a universe $U$ such that $X \in U$.

In particular, this guarantees that given a universe $U$, there is always a universe $V$ so that $U \in V$, hence we can enlarge a given universe.

Now, I'm personally interested in not the universe itself but it's enhancement based on a model-theoretic concept of "elementary substructure". Here Michael Shulman introduces a theory which he calls $ZMC/S$ (which is based on S.Feferman's theory $ZFC/S$) which takes $ZFC$ and adds a constant symbol $S$ which is a set which is both a universe and an which satsfies the following reflection principle:

Let $\phi(x_1,...,x_n)$ be a formula in the language of set theory. Then

$$\forall x_1...\forall x_n, (\phi(x_1,...,x_n) \Longleftrightarrow \phi^S(x_1,...,x_n)),$$

where $\phi^S(x_1,...,x_n)$ denoted the formula obtained from $\phi(x_1,...,x_n)$ by restricting all quantifiers to the set $S$.

Assume this is the approach we wish to take for the foundations of category theory (I do not wish to discuss whether it is useful with respect to ordinary universes). Is a single such set $S$ enough for all purposes of category theory or do we instead need a proper class of similar universes, such as introduced there? Note that both Michael Shulman in his notes and Joel David Hamkins in his aforementioned answer claim that these theories are both equiconsistent with the assumption that "$Ord$ is Mahlo", which would imply that that they are equiconsistent with each other. However, consistency is not what interests me right now, what I want to understand is there there a matter of enlarging a universe when working with a single Feferman-Shulman universe $S$ as it is when working with a single Gorthendieck universe?

Answer 1

I haven't thought deeply about this question, but shooting from the hip my reaction is that one might sometimes need two or three such universes, or maybe even countably many, but proper-class many seems unlikely to be needed.

The point of Feferman's ZFC/S (and its slight modification ZMC/S) for category theory is that when we want to prove general category-theoretic theorems and then apply them to an arbitrary structure $K$, we no longer have to choose a universe containing $K$ to define the categories to which we apply our theorems. Instead, we prove our theorems about "the" reflective universe $S$, so that a priori they only make statements about "small" structures, and then apply the reflection property of $S$ to deduce that the same statements we proved about small structures using category theory are true about "large" structures as well.

Thus, if we proceed in this way, it seems to me that the only situation in which we might need more than one $S$-like universe is if while doing the abstract category theory we need more than one universe at the same time. This might happen: for instance, we might want to talk about a 2-category of categories which contains as an object a category of sets. I've wanted to do that myself. Or a 3-category of 2-categories containing such a 2-category; I think maybe once I wanted to do that too. Maybe nowadays it would be an $(\infty,1)$-category containing as an object an $(\infty,1)$-category of $(\infty,1)$-categories, etc. etc. While I certainly can't rule out that we might want proper-class-much such nesting, right now I'm not thinking of any situation in which we would need to go beyond finitely or at most countably many such categories.

(But, this is the sort of statement that tends to get proven wrong as soon as it is made. All readers are invited to take it as a challenge: find an argument in abstract category theory that uses proper-class-many universes at the same time.)