In set theory and category theory one easily runs into the problem of size. For example Russell's paradox tells us that it is impossible to have consistent set theory allowing a set of all sets. Similarly a category with ALL limits/colimits is a poset, so a consistent theory allowing interesting categories should rather talk about having small limits/colimits.
The "formal" way around this problem is to add the axiom of universes to our favorite set theory, which allows us to restrict to certain small sets, which basically form a model of set theory within set theory. I do not doubt that this is useful or that it solves these problems! However it does not address the following issue:
When introducing material set theories (say ZFC) we usually define it as a first order theory satisfying some axioms. Likewise when introducing structural set theories (say ETCS) we define it speaking of a category of objects (called sets), which satisfies some axioms. In either way the surrounding metatheory (in which we define the notion of first order theory / category) makes use of notions such as collection, equal, distinct, exists, for all, finite, infinite etc. So in some sense our definitions make use of themselves, which makes me feel very uncomfortable, as it somewhat invalidates all formalism.
The only way around this problem I see is to state another axiom, that every model of our set theory is an internal model of another (larger) model ie. something like
- Every model of ZFC is a universe in a model of ZFC
- Every category satisfying ETCS is an internal category (ie. small category) in a category satisfying ETCS.
I could not find a treatment of this problem (maybe because I am unfamiliar with the literature), or someone mentioning my axiom. Why is this?
PS: Again, on the practical side it doesn't really matter, whether universes "go inside" or "go outside". Yet I think philosophically it does make a difference…
Best Answer
Let me address the set theoretic part of your question.
First of all, the term "universe" is a bit loaded. It can mean either (1) just a mathematical universe, understood as a universe of sets, i.e. a model of set theory; or (2) a Grothendieck universe, specifically, especially in the context of category theory, which is a model of second-order set theory, which means that it is isomorphic with $V_\kappa$ for an inaccessible cardinal $\kappa$, if you're unfamiliar with these notions, the key point to take forward is that this is a very special model of set theory which agrees with its metatheory on things like power sets, etc.
So right off the bat, we get that in the specific interpretation as a Grothendieck universe, it cannot be that every model of set theory is a universe in a larger model of set theory. But let's focus on the first meaning, simply "a model" (which raises the obvious question: why not just refer to it as a model?)
Nevertheless, these things are indeed studied, mostly in philosophy of set theory. You can read about the multiverse axioms, specifically in Hamkins' approach to the multiverse. Hamkins also has work on set theoretic potentialism, which you might want to read about.
Overall, if there is a proper class of inaccessible cardinals, you immediately get an ever growing hierarchy of universes that are even Grothendieck universes as well. This can be made stronger (e.g. require that "$\mathrm{Ord}$ is Mahlo") or weaker (e.g. require that simply every set is a transitive model of $\sf ZFC$", or even that there is a proper class of cardinals $\alpha$, such that $V_\alpha$ is a model of $\sf ZFC$; both of which are weaker than even a single inaccessible cardinal as far as consistency strength goes).
If my understanding of Grothendieck universes is correct, we actually do use them as you suggest. To make something "small", you must first envelope it by a larger universe. And since both universes agree on things like power sets, we get exactly what you're asking for.
One last thing worth pointing out, though, is that we can easily formalise all of the theories you mentioned, and more, in something like Peano arithmetic, or even Primitive Recursive Arithmetic, where there is no innate notion of "collection", rather this is meaning we assign—as people, as the readers and executors of mathematics—to the objects of set theory.