Reflection principle vs universes

Question

In category-theoretic discussions, there is often the temptation to look at the category of all abelian groups, or of all categories, etc., which quickly leads to the usual set-theoretic problems. These are often avoided by using Grothendieck universes. In set-theoretic language, one fixes some strongly inaccessible cardinal $\kappa$ -- this means that $\kappa$ is some uncountable cardinal such that for all $\lambda<\kappa$, also $2^\lambda<\kappa$, and for any set of $<\kappa$ many sets $S_i$ of size $<\kappa$, also their union is of size $<\kappa$. This implies that the stage $V_\kappa\subset V$ of "sets of size $<\kappa$" is itself a model of ZFC -- by applying any of the operations on sets, like taking powersets or unions, you can never leave $V_\kappa$. These sets are then termed "small", and then the category of small abelian groups is definitely well-defined.

Historically, this approach was first used by Grothendieck; a more recent foundational text is Lurie's work on $\infty$-categories. However, their use has always created somewhat of a backlash, with some people unwilling to let axioms beyond ZFC slip into established literature. For example, I think at some point there was a long discussion whether Fermat's Last Theorem has been proved in ZFC, now settled by McLarty. More recently, I've seen similar arguments come up for theorems whose proofs refer to Lurie's work. (Personally, I do not have strong feelings about this and understand the arguments either way.)

On the other hand, it has also always been the case that a closer inspection revealed that any use of universes was in fact unnecessary. For example, the Stacks Project does not use universes. Instead, (see Tag 000H say) it effectively weakens the hypothesis that $\kappa$ is strongly inaccessible, to something like a strong limit cardinal of uncountable cofinality, i.e.: for all $\lambda<\kappa$, one has $2^\lambda<\kappa$, and whenever you have a countable collection of sets $S_i$ of size $<\kappa$, also the union of the $S_i$ has size $<\kappa$. ZFC easily proves the existence of such $\kappa$, and almost every argument one might envision doing in the category of abelian groups actually also works in the category of $\kappa$-small abelian groups for such $\kappa$. If one does more complicated arguments, one can accordingly strengthen the initial hypothesis on $\kappa$. I've had occasion to play this game myself, see Section 4 of www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf for the result. From this experience, I am pretty sure that one can similarly rewrite Lurie's "Higher Topos Theory", or any other similar category-theoretic work, in a way to remove all strongly inaccessible cardinals, replacing them by carefully chosen $\kappa$ with properties such as the ones above.

In fact, there seems to be a theorem of ZFC, the reflection principle (discussed briefly in Tag 000F of the Stacks project, for example), that seems to guarantee that this is always possible. Namely, for any given finite set of formulas of set theory, there is some sufficiently large $\kappa$ such that, roughly speaking, these formulas hold in $V_\kappa$ if and only if they hold in $V$. This seems to say that for any given finite set of formulas, one can find some $\kappa$ such that $V_\kappa$ behaves like a universe with respect to these formulas, but please correct me in my very naive understanding of the reflection principle! (A related fact is that ZFC proves the consistency of any given finite fragment of the axioms of ZFC.)

On the other hand, any given mathematical text only contains finitely many formulas (unless it states a "theorem schema", which does not usually happen I believe). The question is thus, phrased slightly provocatively:

Does the reflection principle imply that it must be possible to rewrite Higher Topos Theory in a way that avoids the use of universes?

Edit (28.01.2021): Thanks a lot for all the very helpful answers! I think I have a much clearer picture of the situation now, but I am still not exactly sure what the answer to the question is.

From what I understand, (roughly) the best meta-theorem in this direction is the following (specialized to HTT). Recall that HTT fixes two strongly inaccessible cardinals $\kappa_0$ and $\kappa_1$, thus making room for small (in $V_{\kappa_0}$), large (in $V_{\kappa_1}$), and very large (in $V$) objects. One can then try to read HTT in the following axiom system (this is essentially the one of Feferman's article "Set-theoretic foundations of category theory", and has also been proposed in the answer of Rodrigo Freire below).

(i) The usual ZFC axioms

(ii) Two other symbols $\kappa_0$ and $\kappa_1$, with the axioms that they are cardinals, that the cofinality of $\kappa_0$ is uncountable, and that the cofinality of $\kappa_1$ is larger than $\kappa_0$.

(iii) An axiom schema, saying that for every formula $\phi$ of set theory, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ and $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.

Then the reflection principle can be used to show (see Rodrigo Freire's answer below for a sketch of the proof):

Theorem. This axiom system is conservative over ZFC. In other words, any theorem in this formal system that does not refer to $\kappa_0$ and $\kappa_1$ is also a theorem of ZFC.

This is precisely the conclusion I'd like to have.

Note that $V_{\kappa_0}$ and $V_{\kappa_1}$ are models of ZFC, but (critically!) this cannot be proved inside the formal system, as ZFC is not finitely axiomatizable, and only each individual axiom of ZFC is posited by (iii).

One nice thing about this axiom system is that it explicitly allows the occasional arguments of the form "we proved this theorem for small categories, but then we can also apply it to large categories".

A more precise question is then:

Do the arguments of HTT work in this formal system?

Mike Shulman in Section 11 of https://arxiv.org/abs/0810.1279 gives a very clear exposition of what the potential trouble here is. Namely, if you have a set $I\in V_{\kappa_0}$ and sets $S_i\in V_{\kappa_0}$ for $i\in I$, you are not allowed to conclude that the union of the $S_i$ is in $V_{\kappa_0}$. This conclusion is only guaranteed if the function $i\mapsto S_i$ is also defined in $V_{\kappa_0}$ (or if $I$ is countable, by the extra assumption of uncountable cofinality). In practice, this means that when one wants to assert that something is "small" (i.e. in $V_{\kappa_0}$), this judgment pertains not only to objects, but also to morphisms etc. It is not clear to me now how much of a problem this actually is, I would have to think more about it; I might actually imagine that it is quite easy to read HTT to meet this formal system. Shulman does say that, with this caveat, the adjoint functor theorem can be proved, and as Lurie says in his answers, the arguments in HTT are of similar set-theoretic complexity. However, I'd still be interested in a judgment whether the answer to the question is "Yes, as written" or rather "Probably yes, but you have to put some effort in" or in fact "Not really". (I sincerely hope that the experts will be able to agree on roughly where the answer falls on this spectrum.)

A final remark: One may find the "uncountability" assumption above a bit arbitrary; why not allow some slightly larger unions? One way to take care of this is to add a symbol $\kappa_{-1}$ with the same properties, and ask instead that the cofinality of $\kappa_0$ is larger than $\kappa_{-1}$. Similarly, one might want to replace the bound $\mathrm{cf} \kappa_1>\kappa_0$ by a slightly stronger bound like $\mathrm{cf} \kappa_1>2^{\kappa_0}$ say. Again, if it simplifies things, one could then just squeeze another $\kappa_{1/2}$ in between, so that $\mathrm{cf} \kappa_{1/2}>\kappa_0$ and $\mathrm{cf} \kappa_1>\kappa_{1/2}$. This way one does not have to worry whether any of the "standard" objects that appear in some proofs stay of countable size, or whether one can still take colimits in $V_{\kappa_1}$ when index sets are not exactly of size bounded by $\kappa_0$ but have been manipulated a little.

PS: I'm only now finding all the relevant previous MO questions and answers. Some very relevant ones are Joel Hamkins' answers here and here.

Answer 1

Reflecting on Gabe's comment on my original answer, I now think what I wrote is misleading because it conflates two separate (but related) assertions:

1. The existence of strongly inaccessible cardinals is not really needed in category theory.

2. The full strength of ZFC is not really needed in category theory.

I agree with both of these statements, but think that the best way to convince someone of 1) would not be to combine 2) with a reflection principle: that is, one shouldn't try to replace the use of a strongly inaccessible cardinal $\kappa$ by one for which $V_{\kappa}$ models a large part of ZFC.

As I see it, the "problem" which universes solve is to justify the combination of two types of reasoning:

A) It is sometimes useful to prove theorems about small categories $\mathcal{C}$ by embedding them into "big" categories (for example, using the Yoneda embedding) which have nice additional features: for example, the existence of limits and colimits.

B) Big categories are also categories, so any theorem which applies to categories in general should also apply to big categories.

If you were worried only about B), then a reflection principle could be relevant. Choosing a cardinal $\kappa$ such that $V_{\kappa}$ satisfies a big chunk of ZFC, you can redefine "small category" to mean "category belonging to $V_{\kappa}$" and "big category" to mean "category not necessarily belonging to $V_{\kappa}$", and you can feel confident that all the basic theorems you might want are valid in both cases.

But if you're also worried about A), then this isn't necessarily helpful. Say you start with a category $\mathcal{C}$ belonging to $V_{\kappa}$, and you want some version of the Yoneda embedding. A natural guess would be to embed into the category of functors from $\mathcal{C}^{\mathrm{op}}$ to the category of sets of size $<\tau$ (or some equivalent model of it), for some cardinal $\tau$. A first guess is that you should take $\tau = \kappa$, but I think this only makes sense $\kappa$ is strongly inaccessible (otherwise some Hom sets will be too big). In any case guarantee that this construction has good properties, you're going to want to demand different properties of the cardinal $\tau$. For example, if you want the this category of presheaves to have lots of colimits, then you're going to want $\tau$ to have large cofinality. And if you start thinking about what kinds of additional assumptions you might need to make, you're back where you started: thinking about what kind of cardinality estimates guarantee that "presheaves of sets of size $< \tau$" are a good approximation to the category of all presheaves of sets. So the reflection principle doesn't really help you to avoid those issues.

(Edit: I realized after writing that the text below is mostly reiterating Peter's original post. But I'll leave it here in case anyone finds it useful.)

If you want a rigorous formalization in something like ZFC, probably the best thing to do is to do away with big categories altogether. So then B) is a non-issue. To deal with A), let me remark that many of the "big" categories that one would like to talk about arise in a particular way: one starts with a small category $\mathcal{C}$ which has certain kinds of colimits already, and formally enlarges $\mathcal{C}$ to make a bigger category $\mathcal{C}^{+}$ which has arbitrary colimits (without changing the ones that you started with). Categories which arise this way are called locally presentable, and there's a simple formula for $\mathcal{C}^{+}$: it's the category of functors $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ which preserve the limits that you started with (that is, the colimits which you started with in $\mathcal{C}$).

Now, if you want to mimic this in the world of small categories, you could instead pick some cardinal $\kappa$ and instead contemplate functors $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\kappa$} \}$, which is equivalent to a small category $\mathcal{C}^{+}_{\kappa}$. The question you meet is whether this is a good enough replacement for the big category $\mathcal{C}^{+}$ above. For example, does it have lots of limits and colimits? It's unreasonable to ask for it to have all colimits, but you could instead ask the following:

Q) Does the category $\mathcal{C}^{+}_{\kappa}$ have colimits indexed by diagrams of size $< \kappa$?

The answer to Q) is "no in general, but yes if $\kappa$ is nicely chosen". For example, if you have some infinite cardinal $\lambda$ bounding the size of $\mathcal{C}$ and the number of colimit diagrams that you start with, then I believe you can guarantee (i) by taking $\kappa = (2^{\lambda})^{+}$ (and the category $\mathcal{C}^{+}_{\kappa}$ can be characterized by the expected universal property). Moreover, to prove this you don't need any form of replacement.

Now you could also ask the following:

Q') Does the category $\mathcal{C}^{+}_{\kappa}$ have limits indexed by diagrams of size $< \kappa$?

Here the answer will usually be "no" unless $\kappa$ is strongly inaccessible. But if you're only interested in limits of a particular type (for example, if you're studying Grothendieck topoi, you might be especially interested in finite limits), then the answer will again "yes for $\kappa$ well chosen". And this is something you can prove using very little of ZFC.

Now my claim is that, based on my experience, the above discussion is representative of the kind of questions that you'll run into trying to navigate the distinction between "small" and "large" categories (certainly it's representative of the way these things come up in my book, which the original question asked about). In practice, you never need to talk about the entirety of a big category like $\mathcal{C}^{+}$; it's enough to build a large enough piece of it (like $\mathcal{C}^{+}_{\kappa}$) having the features that you want to see, which you can arrange by choosing $\kappa$ carefully.

I find it conceptually clearer to ignore the issue of how things are formalized in ZFC and to phrase things in terms of the "big" category $\mathcal{C}^{+}$, referring back to its "small" approximations $\mathcal{C}^{+}_{\kappa}$ only as auxiliaries in a proof (which will inevitably still turn up somewhere!). The invocation of "universes" is just a way to write like this while still paying lip service to the axiomatic framework of ZFC, and is definitely inessential.

Answer 2

I'm going to go out on a limb and suggest that the book HTT never uses anything stronger than replacement for $\Sigma_{15}$-formulas of set theory. (Here $15$ is a randomly chosen large number, and HTT is randomly chosen math book that is not specifically about set theory.)

Answer 3

I'd like to mention something that I think hasn't been pointed out yet. The original question began with

In set-theoretic language, one fixes some strongly inaccessible cardinal $\kappa$... This implies that the stage $𝑉_\kappa\subset 𝑉$ of "sets of size $<\kappa$" is itself a model of ZFC.

However, the statement that $V_\kappa$ is a model of ZFC is significantly weaker than saying that $\kappa$ is inaccessible. In fact, if $\kappa$ is inaccessible, then $\{ \lambda\mid V_\lambda$ is a model of ZFC $\}$ is stationary in $\kappa$. Hence, the smallest inaccessible (if there is one) is much bigger than the smallest $\kappa$ such that $V_\kappa$ models ZFC.

Insofar as the reflection principle is useful (which, as some other answers have pointed out, one may at least question), it is only directly helpful for arguments in which the relevant property of a Grothendieck universe is that it is a model of ZFC. However, at least when formulated naively, there are plenty of places where category theory uses more than this. Specifically, we use the fact that a Grothendieck universe satisfies second-order replacement, meaning that any function $f:A\to V_\kappa$, where $A \in V_\kappa$, has an image. Saying that $V_\kappa$ models ZFC only implies that it satisfies first-order replacement, which only allows us to conclude that such an $f$ has an image if $f$ is definable from $V_\kappa$ by a logical formula.

I believe that second-order replacement is ubiquitous in universe-based category theory as usually formulated. For instance, if ${\rm Set}_\kappa$ denotes the category of sets in $V_\kappa$, then to prove that ${\rm Set}_\kappa$ is "complete and cocomplete" in the naive sense that it admits a limit and colimit for any functor whose domain is small, we need second-order replacement to collect the images of such a functor into a single set.

Now, there are ways to reformulate category theory to avoid this. McLarty's paper does it in some set-theoretic ways. A categorically consistent approach is to replace naive "large categories" (meaning categories whose sets of objects and morphisms may not belong to $V_\kappa$) with large ${\rm Set}_\kappa$-indexed categories. But this is a much more substantial sort of reformulation to perform by hand.

Answer 4

OK, I spent much of today trying to figure this out by actually looking in some detail at HTT. It's been quite a ride; I have definitely changed my perspective multiple times in the process. Currently, it seems to me that the answer is that HTT, as written, can be read in this formal system. (So this is like in the joke where after hours someone says "Yes, it is obvious." There are definitely points where the correct interpretation has to be chosen, but as in any mathematical text, that is already the case anyways.) So with this answer, I want to advance an argument that HTT can be read in this formal system, trying to explain a little how to interpret certain things in case ambiguity can arise, and why I think reading it this way everything should work. But it is fairly likely that I overlooked something important, so please correct me!

As Tim Campion notes, most of the early stuff works without problems -- in fact, it doesn't even mention universes. As long as it doesn't, everything works in $V_{\kappa_0}$, in $V_{\kappa_1}$, and in $V$, and the given axiom schema even guarantees that any constructions made will be compatible.

One has to pay closer attention when one reaches Chapters 5 and 6. Let me try to present some definitions and propositions from these chapters from three different points of view.

1. The classical ZFC point of view, or (equiconsistently) the one of von Neumann--Bernays--Gödel (NBG) theory, which allows classes in addition to sets, so we can talk about the (class-sized) category of all sets $\mathrm{Set}$.

2. The point of view of HTT, which is ZFC + Grothendieck universes.

3. The point of view of Feferman's set theory, in the form stated in the question. (Actually, I am no longer sure whether I really need these cofinality bounds. But it's nice to know that they can be assumed.)

Note that the question asked presumes that one is really interested in the first point of view, and in the others only insofar as they are conveniences to prove something about the first setting. This aligns with the contents of Chapter 5 and 6: the whole theory of presentable categories fits nicely into the first setting, also philosophically.

OK, so recall that a presentable category -- let me just stick with categories instead of $\infty$-categories, the difference is inessential for our concerns -- is a (class-sized) category $C$ that admits all small colimits, and such that for some regular cardinal $\kappa$, there is some small category $C_0$ and an equivalence $C\cong \mathrm{Ind}_{\kappa}(C_0)$,

i.e. $C$ is obtained by freely adjoining $\kappa$-filtered colimits to $C_0$. (In particular, $C_0$ is necessarily equivalent to the full subcategory of $\kappa$-compact objects of $C$.) In particular, presentable categories are determined by a small amount of data. Also, the idea is that $C$ is really the category of all objects (sets, groups, whatever). This point of view is really most clearly articulated in 1), while in 2) and 3) the notion of presentability suddenly depends again on the universe, and suddenly they are again only containing small sets/groups/...; let me then accordingly call them small-presentable. Note that this notion makes sense in both 2) and 3), and it depends only on $V_{\kappa_0}$. A small-presentable category is then in particular small-definable, so lives in $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, where this inclusion is an equality in 2) (but not in 3)).

In 2), one would usually define a small-presentable category as a special kind of large category, which is the approach of HTT. But here I'm actually alreading getting a bit confused: There seem to be two notions of functors $F: C\to D$: The ones definable in $V_{\kappa_0}$, equivalently $F\in V_{\kappa_0+1}$ (namely, $V_{\kappa_0+1}$ are exactly the classes of $V_{\kappa_0}$), or all functors in $V_{\kappa_1}$. It does not seem obvious to me that any functor $F: C\to D$ in $V_{\kappa_1}$ lies in $V_{\kappa_0+1}$, as $C$ and $D$ themselves only live in $V_{\kappa_0+1}$. The difference between these two notions disappears when one restricts to accessible functors, all of which are definable. Note that 1) says it's really the first notion we should care about! (Before writing this post, I was not aware of the difference.)

In 3), the proper way to proceed is to use the perspective dictated by 1), which is that of "$V_{\kappa_0}$-definable categories", so they live in $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. One can again consider these as $\kappa_1$-small categories. At first I thought that there would be a substantial difference here between the approaches of 2) and 3), but actually it seems that in both cases one arrives at two different notions of functors, which are reconciled once one restricts to accessible functors.

One of the main theorems is the adjoint functor theorem: If $F: C\to D$ is a functor of presentable categories that preserves all small colimits, then it admits a right adjoint. What does this theorem actually mean?

In 1), it means that there is a functor $G: D\to C$ -- which in particular means that it must be definable by formulas, as this is what functors between class-sized categories are -- together with (definable!) unit and counit transformations satisfying the usual conditions.

In 2), one is simply regarding $C$ and $D$ as being small when considered in $V_{\kappa_1}$ and then asserts the existence of the right adjoint there. Without further information, this actually does not seem to give what we wanted in 1), as a priori $G$ (and the unit and counit transformations) all lie in the larger universe. But this information can be obtained by remembering that $G$ is actually accessible (a part of the adjoint functor theorem I omitted to state above, but should be included), and so everything is determined on a set.

In 3), one would again like to get to the result of 1), but can try to do this as in 2) by first proving the existence of such data in $V_{\kappa_1}$ and then proving accessibility, thus yielding that everything lies in $\mathrm{Def}(V_{\kappa_0})$.

Let us see how this plays out in a couple of early places in Chapter 5 where universes are used.

Definition 5.1.6.2: Let $C$ be a category which admits all small colimits. An object $X\in C$ is completely compact if the functor $j_X: C\to \widehat{\mathrm{Set}}$ copresented by $X$ preserves small colimits.

Here $\widehat{\mathrm{Set}}$ is the (very large) category of sets in $V_{\kappa_1}$. Let us interpret what this definition means in the above systems.

1. Here $C$ is any (possibly class-sized) category. Note that, especially in HTT, "locally small" is not a standard hypothesis, so this allows even morphisms between two objects to be proper sets. For this reason, the functor really has to go to $\widehat{\mathrm{Set}}$, and this is something we cannot talk about in this setting. So one would have to reformulate the condition to meet this objection; this should not be hard, but may be a bit nasty.

2. I think it is implied in the definition that $C$ is any category that lies in $V_{\kappa_1}$. This is strictly capturing the setup of 1) in that if $C$ is small-definable as coming from 1), then any small colimit diagram in $C$ is automatically small-definable.

3. Here we have two choices: Either the one from 1) or the one from 2), and they give different notions. In case of conflict the perspective from 1) is the correct one, so $C$ is small-definable, and one asks for commutation with colimits of small-definable diagrams. But while in 1) we had trouble formulating the condition, the universes at hand in 3) mean that the condition can now be formulated: we can ask that it takes small-definable colimits in $C$ to colimits in $\widehat{\mathrm{Set}}$. Here $\widehat{\mathrm{Set}}$ are the sets in $V_{\kappa_1}$.

So in this case, the upshot is that one has to be a bit careful in 3) about the interpretation, but guided by 1) one can give the right definition; and then the system actually helps.

Proposition 5.2.6.2: Let $C$ and $D$ be categories. Then the categories $\mathrm{Fun}^L(C,D)$ of left adjoint functors from $C$ to $D$, and $\mathrm{Fun}^R(D,C)$ of right adjoint functors from $D$ to $C$ are (canonically) equivalent to one another.

1. In this perspective, this proposition only really makes sense when $C$ and $D$ are small, as otherwise $\mathrm{Fun}(C,D)$ is too large. (One wants to consider such functor categories when $C$ and $D$ are presentable (or accessible), but only when restricting to accessible functors. So that's a discussion that would appear later in Chapter 5.) Then the statement is clear enough, and the proof given applies.

2. In this perspective, I think it's the same as in 1), except that one can also formulate the same result in a different universe.

3. Same here.

Note however that as it stands, in 1) this proposition can not (yet) be applied in case $C$ and $D$ are presentable. In 2) and 3), (small-)presentable ones are special large categories, to which the result applies. Note however that the functor categories and their equivalence are all living in a larger universe, and we get no information of them lying in either $V_{\kappa_0+1}$ or $\mathrm{Def}(V_{\kappa_0})$.

The next proposition considers the presheaf category $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, and the proof is a typical argument involving passage to a larger universe to resolve homotopy-coherence issues.

Proposition 5.2.6.3: Let $f: C\to C'$ be a functor between small categories and let $G: \mathcal P(C')\to \mathcal P(C)$ be the induced functor of presheaf categories induced by composition with $f$. Then $G$ is right adjoint to $\mathcal P(f)$.

Here $\mathcal P(f)$ is defined to be the unique small colimit-preserving extension of $f$ (under the Yoneda embedding).

1. Here, we have two class-sized categories and functors between them, all definable (as must be). The proposition would ask us to find (definable!) unit and counit transformations, making some diagrams commute. This seems not too hard. But in $\infty$-categories, it is famously hard to define functors by hand, so this is not actually how Lurie proceeds!

2. Here $\mathcal P(C)$ and $\mathcal P(C')$ are special large categories. Lurie in fact applies the large Yoneda embedding in the proof. So this is really producing the unit and counit adjunctions only in some larger universe. As discussed above, I think this proof does not actually give what we wanted in 1)!

3. We can argue as Lurie does to produce the data in some larger "universe". (Edit: Actually, as Tim Campion points out, one has to make a minimal detour in order to justify what's written. See comments to his answer.)

So when reading this proposition, in either system 2) or 3), one should make a mental marker that so far the statement proved is weaker than one might naively hope for. But this is corrected later, by observing that everything is determined by a small amount of data.

Upshot: While at first I thought there would be a substantial difference between 2) and 3), I actually think there is (almost) none. One difference is that $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ is a proper inclusion, but in practice the way to guarantee containment in $V_{\kappa_0+1}$ seems to be to prove definability in $V_{\kappa_0}$ (for example, by proving that certain functors are accessible).

OK, now tell me why this doesn't work! :-)

Answer 5

If I understand correctly, you're after a statement of the form :

"If something was proved in HTT using universes, it can be proved without them by restricting to some $V_\kappa$ for $\kappa$ large enough"

The rigourous answer to that, if we don't have more information about HTT, is that there can be no such statement if ZFC is consistent.

Indeed, it is possible that the existence of universes are inconsistent (in fact it's not possible to prove that it is consistent), and in that situation, anything can be proved using universes, and so such a statement would imply that anything can be proved, i.e. ZFC is inconsistent.

I'm being a bit sloppy about what's provable in what etc. but the main idea is there

Of course, we do know things about HTT, and if we read it carefully we can analyze where it uses universes, and see that they can in fact be replaced with transitive models of ZC+ replacement up to $\Sigma_{15}$-formulas, as Jacob points out. In that case, since there provably exist such nicely behaved models (of the form $V_\kappa$, for $\kappa$ well-chosen), this is not a problem; and HTT can be rewritten without universes - but this can not be proved without knowledge of what's in HTT.

The "moral" of this is that, in most mainstream category theoretic questions, universes are a time-saving device, and not an actual part of the mathematics.

Answer 6

Answering this question depends strongly on exactly what you want from Higher Topos Theory, because expressing high logical strength is a different goal from expressing an aptly unified logical framework for algebraic geometry and number theory.  Unified strong foundations for general categorical mathematics are one fine goal, and seem to be the goal of many contributors here.  For that goal everything said in comments and answers to this question is relevant. But apt work in geometry and number theory does not call for vast logical strength.

While HTT is more intertwined with universes than SGA, neither HTT nor SGA makes real use of the (very strong) axiom scheme of replacement. Thus they can use "universes" radically weaker than Grothendieck's. As a typical and germane example, Grothendieck he made just one appeal to the axiom scheme of replacement.  That is in his quite crucial proof that every AB5 category with a generating set has enough injectives.   And this use of replacement turns out to be eliminable.  It worked, but Grothendieck actually did not need it to get his result.

To expand on Grothendieck's use of replacement: Reinhold Baer in the 1940s used transfinite induction (which requires the axiom scheme of replacement) to prove modules (over any given ring) have enough injectives.  He was consciously exploring new proof techniques and got a good result.  Grothendieck's Tohoku cast that proof in a form showing every AB5 category with a small set of generators has enough injectives--and a few years later Grothendieck found this was exactly the theorem he needed for topos cohomology.   Baer and Grothendieck both had practical goals, not tied to foundation concerns, but both wanted to get foundations right too.  And they did.  But it turns out they could have gotten those same theorems, correctly, without replacement, by nearly the same proofs, by specifying large enough function sets to begin with (using power set, but not replacement).  There are results that genuinely require the replacement axiom scheme.  But those results rarely occur outside of foundational research.

A lot of people coming from very different angles (some logicians, some disliking logic) since the 1960s have remarked that in the context of algebraic geometry and number theory, the high logical strength  of Grothendieck's universe axiom, is an actually unused by-product of Grothendieck's desire for a unified framework for cohomology.  That can now be made quite precise:  The entire Grothendieck apparatus including not just derived functor cohomology of toposes but the 2-category of toposes, and derived categories, can be formalized in almost exactly the same way as it was formalized by Grothendieck, but at logical strength far below Zermelo-Fraenkel or even Zermelo set theory.    The same is true for HTT.  You can get it without inaccessible universes or reflection as long as you do not need the vast (and rarely used) strength of replacement.  The proof has not actually been given for HTT.  It has been for Grothendieck's uses of universes. It seems clear the same will work for HTT.

The logical strength needed has been expressed indifferent ways:  Simple Type Theory (with arithmetic), Finite Order Arithmetic, the Elementary Theory of the Category of Sets, Bounded Quantifier Zermelo set theory.  Roughly put, you posit a set of natural numbers, and you posit that every set has a power set, but you do not posit unbounded iteration of power sets.  A fairly naive theory of universes can be given conservative over any one of these (the way Godel-Bernays set theory is conservative over ZFC) and adequate to all the large structure apparatus of the Grothendieck school.  

Answer 7

Any theorem $T$ of $\mathsf{ZFC}$ follows from a finite subset of the axioms of $\mathsf{ZFC}$ or, to keep things simple, from $\mathsf{ZFC}$ where the axiom scheme of replacement is restricted to $\Sigma_n$ predicates¹, call this $\mathsf{ZFC}_n$. Now $\mathsf{ZFC}$, and more precisely $\mathsf{ZFC}_{n+1}$, proves the existence of arbitrarily large cardinals $\kappa$, strong limits of uncountable cofinality, such that $V_\kappa$ is a model of $\mathsf{ZFC}_n$, and, in particular, of the theorem $T$, and such that, moreover, that the truth value of any $\Sigma_n$ statement, with parameters in $V_\kappa$ is the same in $V_\kappa$ as in the (true) universe. We can call these $V_\kappa$ “limited universes” in that they are closed under most set-theoretic operation, like taking powersets, except that replacement needs to be either countable (included for convenience) or restricted to a $\Sigma_n$ predicate; and in particular, they are closed under whatever existence statements $T$ makes.

So the idea would be to apply the above to the conjunction $T$ of all the theorems which you consider to be part of Higher Topos Theory (and whatever other theories are used as prerequisisites) and find the appropriate $n$. (I actually suspect that $n=1$ should be sufficient: I would be very surprised to find an instance of replacement in ordinary mathematics which does not follow from $\Sigma_1$-replacement.) Then $\mathsf{ZFC}_n$ would prove $T$ (all the theorems of the theory) and $\mathsf{ZFC}_{n+1}$ would prove the existence of an endless supply of limited universes in which to use the theory.

Of course, to avoid an infinite loop, you cannot consider that theorem (the one asserting the existence of an endless supply of $V_\kappa$) to be part of the theory, or you need to move to a larger $n$.

To explain what might seem like a logical contradiction, here, it must be clarified that the statement that the existence of many models of $\mathsf{ZFC}_n$ can be proved in $\mathsf{ZFC}$ for every $n$, but not uniformly so (the proof gets longer and longer as $n$ grows), so $n$ must be a concrete natural number, the universally quantified (over $n$) statement is not provable in $\mathsf{ZFC}$. But this is not a problem so long as your theory is fixed and is formulated in $\mathsf{ZFC}$ (which demands that it does not, itself, contain such metatheorems as “for any concrete $n$ we can prove the following in $\mathsf{ZFC}$”). So it is up to you to ascertain that this is the case for HTT (and, if you're courageous enough, find the appropriate $n$).

(Just to give a sense of how the kinds of cardinals involved, the cardinals $\kappa$ such that $V_\kappa$ is a model of $\mathsf{ZFC}_1$ are the fixed points of the $\gamma \mapsto \beth_\gamma$ function. I don't think there's any hope for a reasonable description of the $\kappa$ such that $V_\kappa$ is a model of $\mathsf{ZFC}_n$ for any concrete $n\geq 2$. See also this question.)

1. Meaning predicates with at most $n$ alternating sets of unbounded quantifiers, starting with existential quantifiers, followed by formula with bounded quantifiers (meaning of the form $\forall x\in y$ or $\exists x\in y$).

Answer 8

A question that came up in the comments was about the motivation for asking the question. Let me try to address this here.

Foremost, it is about learning! As I mentioned in the original question, I had myself toyed around with some "stupid" cardinal bounds, and only later learned about the reflection principle, so I wanted to understand what it can do (and what it cannot do), and whether I can somehow automatically relegate any further complicated versions of such estimates into this machine. So it's the usual thing where you are just stumbling around in a dark room, and would very much like the room to be illuminated! So, thanks to you all for the illuminating answers!

Another reason is that recently I got a bit frustrated with the solution of Grothendieck universes to the problem at hand. Let me explain.

I very much want to talk about the category of all sets, or all groups, etc., and want to prove theorems about it. And, at least in the von Neumann-Bernays-Gödel (NBG) version of ZFC theory that allows classes, this is a perfectly valid notion. So I find it ontologically very pleasing to work in this setting, and would very much like the adjoint functor theorem to be a theorem about (presentable) categories in that sense.

Now presentable categories are determined by a small amount of data, so one could always work with this small amount of data and keep careful track of relative sizes. In fact, many proofs in HTT explicitly do keep track of such relative sizes, but there are still a few spots where it is nice to first take a "broader view" and look at these large categories as if they were small.

Indeed, the adjoint functor theorem is about functors between large categories, and it quickly becomes nasty to talk about this from within NBG/ZFC. Note that the statement of the adjoint functor theorem makes perfect sense -- it just asks that all the data of the adjunction is definable. But it's a bit nasty to try to speak of these things from "within". So it would definitely be nice to have some kind of meta-theory using which to argue about these large categories, and pretend that they are small. The subtle question of "definability from within" may be a priori lost in this meta-theory, but I regard this question of "definability from within" as central, because after all what I wanted was a theorem about all sets, so I'm fine with having to pay a little bit of attention to it -- and, to take the punchline away, it turns out that this is precisely the difference between working with Grothendieck universes and working with Feferman's "universes".

So this is the thing that Grothendieck universes are for: They always give you a larger universe for any universe you are currently working in. I find the existence of Grothendieck universes completely intuitive, and in fact positing their existence seems completely on par with positing an infinite set in the first place: You are just allowing to collect everything you already have into a bigger entity of its own.

But now suddenly what I used to think of as all sets are called the small sets, and there are also many larger sets. So even if I prove an adjoint functor theorem in this setting, it's not anymore a theorem about functors between categories of all sets/groups/..., but only one of functors between small sets/groups/.... So if you think about it, even in ZFC + Grothendieck universes, you will never prove that theorem you actually wanted, about the category of all sets. (Actually, until very recently, I assumed that the adjoint functor theorem (for $\infty$-categories) is a statement of ZFC that has been proved under "ZFC + Universes", but that's not quite right: The statement that has been proved can even only be formulated in ZFC + Universes.)

What has been proved is that it is consistent that the adjoint functor theorem holds. Namely, assuming consistency of ZFC + Universes, you now produced a model of ZFC -- that of small sets in your model of ZFC + Universes -- in which the theorem is true. So you could now work in the theory "ZFC + the adjoint functor theorem", in which the adjoint functor theorem can be applied to the category of all sets/groups/..., but that definitely feels like a cheat to me. You did not even prove that "ZFC + Universes + the adjoint functor theorem" is consistent! (You would get that if you start with the consistency of slightly more than ZFC + Universes, asking for $\kappa$ such that $V_\kappa$ satisfies ZFC + Universes. Again, that seems like a completely fair assumption to me -- just keep going.) But now you might get to see the danger that you inadvertently climb up the consistency ladder as you implicitly start to invoke more and more theorems proved for small sets also for all sets.

It would be much nicer if you would know that, in ZFC + Grothendieck universes, everything you proved about small sets is also a theorem about the whole ambient category of all sets. This is not automatic, but you can add this as an axiom schema. Mike Shulman in Section 12 of Set theory for category theory (arXiv:0810.1279) discusses this idea (that he denotes ZMC): I find it ontologically quite pleasing, it also seems to have a very simple axiomatization (even simpler than ZFC!), but

a) this additional axiom schema is not completely self-evident to me: Why should everything that is true in small sets also hold for all sets? (Especially if we had some trouble proving the desired result in the first place. Also, note that it definitely does not hold for any notion of small sets: Rather, the axiom schema guarantees that there is some notion of small sets for which this sort of reflection holds. Now this appears a bit dubious to me as in the first place I never wanted small sets, so now I'm positing them, and also ask that they still reflect the whole behaviour of all sets. Probably fine, but not self-evident to me.)

b) the consistency strength of this axiom schema is considerably higher: It is the same as the consistency of a Mahlo cardinal. This is still low-ish as large cardinals go, but it's much much higher than mere Grothendieck universes (which are really low at the bottom of the hierarchy).

Regarding a), the fact that we could prove the consistency of the adjoint functor theorem from the consistency of Grothendieck universes points in the right direction, but this does not in itself guarantee that the two together are consistent. I can imagine that I might convince myself that the axiom schema is reasonable, but I certainly think it needs much more justification than mere Grothendieck universes. (Side question: How large are the large cardinals one can justify using the idea of "allowing to collect together everything we already had"? I'm not sure if this is a completely well-defined question... but to me, a measurable cardinal is definitely not of that sort (but I'm happy to stand corrected), as it seems to posit the emergence of new combinatorial features.)

Another reason I recently got a bit unhappy with Grothendieck universes is that while in some sense we would like to use them to be able to ignore set-theoretic subtleties, in some ways they come back to bite you, as now you have to specify in which universe certain things live. Sometimes, you might then even have to specify several different universes for different types of objects (think of sheaves on profinite sets), and I find that it quickly gets quite ugly. I would much rather have all objects live together in one universe.

So, while thinking about sheaves on profinite sets, I came to find the solution with only one universe much more asthetically and ontologically pleasing, and this solution (condensed sets) can be formalized in ZFC without trouble.

OK, so I claim that Grothendieck universes did not really solve the problem they set out to solve, as

a) they still do not allow you to prove theorems about the category of all sets/groups/... (except as a consistency result, or under stronger large cardinal axioms)

b) working with them, you still have to worry about size issues -- your category of all sets now comes stratified into sets of all sorts of different sizes (i.e. in different universes).

Moreover, they also increase consistency strength.

Now, after this wonderful discussion here, I think Feferman's proposal is actually much better. However, as also Mike Shulman commented, I regard Feferman's axioms not as describing any ontologically correct world, but I regard the "universes" of Feferman's theory merely as conveniences, in order to talk about large categories as if they were small. In other words, Feferman's theory exactly gives you a meta-theory in which to argue about such large categories from the "outside". But it's a theory I would only ever use to give a proof of a theorem of ZFC. Comparing to Grothendieck universes, Feferman's theory

a) does allow you to prove theorems about the category of all sets/groups/..., because it explicitly includes an axiom schema that all theorems about small sets are also theorems about all sets.

b) Of course, within a proof of a theorem of ZFC that invokes some nontrivial size issues, it's very welcome that the theory enables you to talk about various sizes. Moreover, it does so in a way where you can still apply all axioms of ZFC to each of the "universes", and also is taking care "behind the scenes" of how to rewrite everything in terms of (potentially extremely subtle) cardinal bounds in ZFC itself. So it's like a high-level programming language for arguments involving difficult cardinal estimates in ZFC.

In addition, it does not increase consistency strength, and in fact any statements of ZFC proved in this language are theorems of ZFC. (As I recalled above, we could also have a) + b) with Grothendieck universes, but would then run up to the consistency of a Mahlo cardinal.)

So, the upshot is that I think Feferman's universes do a much better job at solving the problem of providing a meta-theory to "talk about large categories as if they were small" than Grothendieck universes do.

Let me add some final reasons for asking the question. I think higher-categorical techniques such as the ones laid out in HTT are of very central importance, not just in algebraic topology where they originated, but in all of mathematics. I can certainly attest to that as regards number theory and algebraic geometry. So their centrality is also an important reason to analyze their consistency strength.

Reading HTT is a very nontrivial matter -- it is long and complicated. Some number theory colleagues have however told that one of the primary reasons they could not read HTT is that it uses universes. Namely, they are so used to ZFC (and to checking with extreme care!) that they will automatically try to eliminate any use of universes in an argument. Now in SGA, at least if you were only interested in applications to etale cohomology of reasonable schemes, this was something you could by hand -- for example, just add some countability assumptions to make things small. However, in HTT I do not see any way that someone will be able to put cardinal bounds in as you read along -- the arguments are way too complex for this.

So now I hope I can tell them that they can check that everything works in ZFC, and they can still read HTT (essentially) as written, if they read it in Feferman's set theory. If they check carefully (which they will), they may still need to fill in a little lemma here and some small extra argument there -- but they would have to do so anyways, in any book of ~1000 pages, and I might imagine that less than half of these side remarks have to do with replacing Grothendieck universes by Feferman's "universes". Should anybody actually undertake that project, of course they deserve full credit if they succeed in this important work!

Let me end with a very brief note on what seems to be the key salient point in the translation to Feferman's theory. I came to appreciate the point that Tim Campion raised in his answer, and I now see that this was also mentioned in Jacob Lurie's second answer. Roughly, it is the following. If $C$ is a presentable category, then there is some small category $C_0$ such that $C=\mathrm{Ind}_\kappa(C_0)$

for some regular cardinal $\kappa$, adjoining freely all small $\kappa$-filtered colimits. This makes $C$ naturally a union of $C_\tau$'s, where $C_\tau$ only collects the $\tau$-small $\kappa$-filtered colimits. Here $\tau$ is a regular cardinal such that $\tau\gg \kappa$. This increasing structure of $C$ as a union of $C_\tau$'s is central in the theory of presentable categories, but the levels are really enumerated by (certain) regular cardinals $\tau$. If you increase your universe, then you also get a larger version $C'$ of $C$ itself, and in Grothendieck universes $C$ is now one of the nice layers $C'_\tau$ of $C$, where $\tau$ is the cutoff cardinal of the previous universe. But in Feferman's universes, this $\tau$ is not regular. This might make some arguments more subtle, but I would expect that one can usually solve this issue by simply embedding $C$ into some $C'_\tau$ with $\tau$ some regular cardinal larger than the cutoff cardinal of the smaller universe.

Answer 9

I would consider a conservative extension of ZFC obtained from ZFC by the adition of a constant $\alpha$ and the following axioms:

1. $\alpha$ is an ordinal ($Ord(\alpha)$).

2. The sentence $\phi\leftrightarrow\phi^{V_\alpha}$, for each sentence in the original language $\phi$ (axiom scheme).

$V_{\alpha}$ behaves as $V$ (for all sentences in the language of set theory). If two (or more) universes are needed, one can add another constant $\beta$ with the corresponding axioms, and the axiom $\alpha<\beta$.

The proof that the resulting theory is conservative over ZFC is easy.

Assume that $\phi$ is provable from the new axioms (axioms using $\alpha$), in which $\phi$ is in the original language. Since any proof is finite, there are finitely many sentences $\phi_1$, ..., $\phi_n$ such that

$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$

is provable without any new axioms. Therefore, one can think of $\alpha$ as a free variable and the above sentence is provable in ZFC (theorem on constants). Since $\alpha$ does not occur in $\phi$, the following implication is provable in ZFC ($\exists$-introduction):

$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$

Now, the reflection principle for ZFC says that the antecedent is a ZFC-theorem. From modus ponens, ZFC proves $\phi$.

So you can work with the new axioms and $V_{\alpha}$ behaves as a universe, and everything that is proved that does not mention $\alpha$ can be proved already in ZFC.

Answer 10

In response to the edit which nails things down to a formal system involving cardinals $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:

I'm going to go out on a perhaps more ill-advised limb and predict that in order to fit Chapters 1-4 into this formal system, no real cardinal arithmetic will be necessary. Rather, for this part of the book, all you'll have to do is go through and add to various theorem statements hypotheses of the form "$X$ is $\kappa_{-1}$-small". After all, this part of the book really only deals with small objects, with the exception of a few particular large objects like the the category of small simplicial sets, the category of small simplicial categories, etc., and things like slice categories thereof. Various model structures are constructed, but I believe in each case one can get by with using the special case of the small object argument for generating cofibrations / acyclic cofibrations between finitely-presentable objects, so that no transfinite induction is needed. On the face of it, straightening / unstraightening have the look of constructions which might be using set theory in serious ways. But I'm going to go ahead and predict that they present no problems to the proposed formal system.

Chapter 5 becomes more annoying. I believe that one will have to make some careful choices about the core theorems of presentable ($\infty$)-categories. What makes presentable categories tick is that they package the adjoint functor theorem very cleanly, but as you say, the ordinary adjoint functor theorem comes with caveats in this setting. I might go so far as to say that the whole point of thinking about presentable categories in the first place is completely undone in this setting. You won't be able to prove basic things like "presentable categories are precisely the accessible localizations of presheaf categories". I predict that whatever choices are made about formulating weak versions of the core theorems of presentable categories in this setting, there will be some application or potential application which suffers.

Chapters 5 and 6 also contain some theorems about particular very large categories such as the $\infty$-category of presentable $\infty$-categories and the $\infty$-category of $\infty$-topoi [1]. The system seems to be such that this won't really be an issue per se, except that the issues encountered in basic presentability theory will now be compounded. You won't be able to prove that $Pr^L$ is dual to $Pr^R$. You won't be able to prove Giraud's theorem (well, the definitions are going to be in flux anyway, so I should clarify: you won't be able to prove that left exact accessible localizations of presheaf categories are the same as locally small categories satisfying a a list of completeness, generation, and exactness conditions). So any theorem about $\infty$-topoi whose proof proceeds by starting with the presheaf case and then localizing will have to be completely re-thought.

Maybe I'm off-base here, but I believe that significant extra work and genuinely new mathematical ideas would be required for Chapters 5 and 6, and the the result would be a theory which is substantially harder to use.

By contrast, I think if you're willing to restrict attention to large categories which are definable from small parameters, then although you'll be missing the beautiful ability to say "we proved this for small categories but now we can apply it to large ones", you'll end up with a much more useable theory of presentability, without leaving ZFC.

[1] Actually, in usual foundations these categories are (up to equivalence) only large and not very large (more precisely, they are have $\kappa_0$-many objects and $\kappa_0$-sized homs), but a modicum of work is required to show this. Will that still be the case in this formal system? I'm not sure.

---

EDIT: A long comment in response to Peter Scholze's answer.

• One thing I just realized is that if $\kappa_0$ is not a $\beth$-fixed-point, then not every set in $V_{\kappa_0}$ has cardinality $<\kappa_0$, so that the notions of "smallness" are multiplied. Happily, I think your formal system proves that $V_{\kappa_0}$ has $\Sigma_1$-replacement, which implies that it's a $\beth$-fixed-point. Crisis averted!

• Perhaps this approach of systematically using definability hypotheses within a "universe setting" will be workable -- combining the "best of both worlds". One nice thing is that even though you're explicitly using metamathematical hypotheses, it would appear that you'll still be able to state and prove these theorems as single theorems rather than schema.

• I'm a bit confused about Proposition 5.2.6.3 (the last one you discuss, and a baby version of the adjoint functor theorem). I presume that the presheaf category $P(C)$ will be defined to comprise those functors $C^{op} \to Spaces$ which lie in $Def(V_{\kappa_0})$. When we pass to a larger universe, the transition is usually pretty seamless, because we expect $P(C)$ to have all colimits indexed by $\kappa_0$-small categories -- a perfectly natural property to work with in $V_{\kappa_1}$. Indeed, the first step of Lurie's proof of 5.2.6.3 is to show that a left adjoint exists using the fact that $P(C)$ has all small colimits [2]. However, in the present setting we can never assume that $\kappa_0$ is regular, and therefore we can never assume that $P(C)$ has all small colimits. The best we can say is that $V_{\kappa_0}$ thinks $P(C)$ has all small colimits. As long as we're working in $V_{\kappa_0}$, this property is "just as good" as actually having all small colimits. But when we move up to $V_{\kappa_1}$, suddenly we have to think of it for what it is -- a metamathematical property. Perhaps later I will sit down and try to see whether Lurie's proof of 5.2.6.3 can be made to work in this setting, but I think prima facie it's unclear.

[2] Only after verifying existence abstractly in this way does he show that the left adjoint must be the functor indicated. Of course, this maneuver is actually an additional complication which comes with the $\infty$-categorical setting -- in ordinary categories the formulas for the two functors can be directly verified to be adjoint, but in $\infty$-categories the formula for the left adjoint is not obviously functorial.