A Grothendieck universe is known in set theory as the set Vκ for a (strongly) inaccessible cardinal κ. They are exactly the same thing. Thus, the existence of a Grothendieck universe is exactly equivalent to the existence of one inaccessible cardinal. These cardinals and the corresponding universes have been studied in set theory for over a century.
The Grothendieck Universe axiom (AU) is the assertion that every set is an element of a universe in this sense. Thus, it is equivalent to the assertion that the inaccessible cardinals are unbounded in the cardinals. In other words, that there is a proper class of inaccessible cardinals. This is the axiom you sought, which is exactly equivalent to AU. In this sense, the axiom AU is a statement in set theory, having nothing necessarily to do with category theory.
The large cardinal axioms are fruitfully measured in strength not just by direct implication, but also by their consistency strength. One large cardinal property LC1 is stronger than another LC2 in consistency strength if the consistency of ZFC with an LC1 large cardinal implies the consistency of ZFC with an LC2 large cardinal.
Measured in this way, the AU axiom has a stronger consistency strength than the existence of any finite or accessible number of inaccessible cardinals, and so one might think it rather strong. But actually, it is much weaker than the existence of a single Mahlo cardinal, the traditional next-step-up in the large cardinal hierarchy. The reason is that if κ is Mahlo, then κ is a limit of inaccessible cardinals, and so Vκ will satisfy ZFC plus the AU axiom. The difference between AU and Mahloness has to do with the thickness of the class of inaccessible cardinals. For example, strictly stronger than AU and weaker than a Mahlo cardinal is the assertion that the inaccessible cardinals form a stationary proper class, an assertion known as the Levy Scheme (which is provably equivconsistent with some other interesting axioms of set theory, such as the boldface Maximality Principle, which I have studied a lot). Even Mahlo cardinals are regarded as rather low in the large cardinal hierarchy, far below the weakly compact cardinals, Ramsey cardinals, measurable cardinals, strong cardinals and supercompact cardinals. In particular, if δ is any of these large cardinals, then δ is a limit of Mahlo cardinals, and certainly a limit of strongly inaccessible cardinals. So in particular, Vδ will be a model of the AU axiom.
Rather few of the large cardinal axioms imnply AU directly, since most of them remain true if one were to cut off the universe at a given inaccessible cardinal, a process that kills AU. Nevertheless, implicit beteween levels of the large caridnal hiearchy are the axioms of the same form as AU, which assert an unbounded class of the given cardinal. For example, one might want to have unboundedly many Mahlo cardinals, or unboundedly many measurable cardinals, and so on. And the consistency strength of these axioms is still below the consistency strength of a single supercompact cardinal. The hierarchy is extremely fine and intensely studied. For example, the assertion that there are unboundedly many strong cardinals is equiconsistent with the impossiblity to affect projective truth by forcing. The existence of a proper class of Woodin cardinals is particularly robust set-theoretically, and all of these axioms are far stronger than AU.
There are natural weakenings of AU that still allow for almost all if not all of what category theorists do with these universes. Namely, with the universes, it would seem to suffice for almost all category-theoretic purposes, if a given universe U were merely a model of ZFC, rather than Vκ for an inaccessible cardinal κ. The difference is that U is merely a model of the Power set axiom, rather than actually being closed under the true power sets (and similarly using Replacement in place of regularity). The weakening of AU I have in mind is the axiom that asserts that every set is an element of a transitive model of ZFC. This assertion is strictly weaker in consistency strength thatn even a single inaccessible cardinal. One can get much lower, if one weakens the concept of universe to just a fragment of ZFC. Then one could arrive at a version of AU that was actually provable in ZFC, but which could be used for most all of the applications in cateogory theory to my knowledge. In this sense, ZFC itself is a kind of large cardinal axiom relative to the weaker fragments of ZFC.
Typically, generic absoluteness is a consequence of a stronger property, that in many cases is really the goal one is after. To explain this stronger property, let me begin by reviewing two important absoluteness results.
1) The first is Mostowski's Absoluteness. Suppose $\phi$ is $\Sigma^1_1(a)$, where $a\in\omega^\omega$. This means that $\phi(x)$ for $x\in\omega^\omega$, asserts
$∃y\in\omega^\omega\forall n\in \omega R(x\upharpoonright n, y\upharpoonright n,a\upharpoonright n)$,
where $R$ is a predicate recursive in $a$. These statements are very absolute: Suppose that $M$ is a well-founded model of a decent fragment of ZF, and that $a,x\in M$. Then $\phi(x)$ holds iff $M\models \phi(x)$.
In particular, whether or not $\phi(x)$ holds cannot be changed by forcing, or by passing to an inner or outer model. Note that $M$ could be countable. In fact, only needs to be an $\omega$-model; well-foundedness is not necessary.
This is how the result is usually stated. What is going on is the following:
Suppose that $T$ is a tree (in the descriptive set theoretic sense) and that $T\in M$. Then $T$ is ill-founded iff $M\models T$ is ill-founded.
In particular, $T$ could be the tree associated to $\phi$. This is the tree of all $(s,t)$ such that $s,t$ are finite sequences of the same length $l$, and $\forall n\le l$ $ R(s\upharpoonright l,t\upharpoonright n,a\upharpoonright n)$. So $T$ is the tree of attempts to verify $\phi$: $\phi(x)$ holds iff (there is a $y$ such that for all $n$, $(x\upharpoonright n,y\upharpoonright n)\in T$) iff the tree $T_x$ is ill-founded. Recall that $T_x$ consists of all $t$ such that, if $l$ is the length of $t$, then $(x\upharpoonright n,t\upharpoonright n)\in T$ for all $n\le l$.
The point is that $T$ is a very simple object. As soon as $T,x$ are present, $T_x$ can be built, and the result of the construction of $T_x$ is the same whether it is performed in $V$ or in $M$. Since well-foundedness is absolute, whether or not $T_x$ is ill-founded is the same whether we check this in $M$ or in $V$. Of course, $T_x$ is ill-founded iff $\phi(x)$ holds.
The moral is that the truth of $\Sigma^1_1$ statements is certified by trees. And I think that this is saying that in a strong sense, $\Sigma^1_1$ statements are very tractable. All we need to check their validity is a very easy to build tree and, once we have it, the tree is our certificate of truth or falsehood, this cannot be altered.
Recall that proofs in first-order logic can be described by means of certain finite trees. If something is provable, the tree is a very robust certificate. This is a natural weakening of that idea.
Of course one could argue that, if a $\Sigma^1_1$ statement is not provable, then in fact it may be very hard to establish its truth value, so tractability is not clear. Sure. But, independently of whether or not one can prove something or other, the certificate establishing this truth value is present from the beginning. One does not need to worry that this truth value may change by changing the model one is investigating.
2) The second, and best known, absoluteness result, is Shoenfield's absoluteness. Suppose $\phi$ is $\Sigma^1_2(a)$. This means that $\phi(x)$ holds iff
$\exists y\forall z\exists n$ $R(y\upharpoonright n,z\upharpoonright n,x\upharpoonright n,a\upharpoonright n)$,
where $R$ is recursive in $a$. Let $M$ be any transitive model of a decent fragment of ZFC, and suppose that $\omega_1\subset M$ and $a,x\in M$. Then $\phi(x)$ holds iff $M\models\phi(x)$.
This is again a very strong absoluteness statement. Again, if one manages to show the consistency of $\phi(x)$ by, for example, passing to an inner model or a forcing extension, then in fact one has proved its truth.
Again, one could say that if $\phi$ is not provable, then it is in fact not very tractable at all. But the point is that to investigate $\phi$, one can use any tools whatsoever. One only needs to worry about its consistency, for example, and one can make use of any combinatorial statements that one could add to the universe by forcing.
Just as in the previous case, $\Sigma^1_2$ statements can be certified by trees. The tree associated to $\phi$ is more complicated than in the previous case, and it is now a tree of $\omega\times\omega_1$. (Jech's and Kanamori's books explain carefully its construction.) Again, the tree is very absolute: As soon as we have $a$ and all the countable ordinals at our disposal, the tree can be constructed. (One comparing two models $M\subset V$, we mean all the countable ordinals of $V$, even if $M$'s version of $\omega_1$ is smaller.)
3) Generic absoluteness of a statement $\phi$ is typically a consequence of the existence of absolutely complemented trees associated to $\phi$. In fact, all generic absoluteness results I'm aware of are established by proving that there are such trees ("conditional" generic absoluteness results, such as only for proper forcings, or only in the presence of additional axioms, are somewhat different). This is a direct generalization of the situations above.
To define the key concept, recall that if $A$ is a tree of $\omega\times X$, then the projection $p[A]$ of $A$ is the set of all $x\in\omega^\omega$ such that $\exists f\in X^\omega\forall n\in\omega\,(x\upharpoonright n,f\upharpoonright n)\in A$.
Two (proper class) trees $A$ and $B$ on $\omega\times ORD$ are absolutely complemented iff:
- $p[A]\cap p[B]=\emptyset$ and $p[A]\cup p[B]=\omega^\omega$.
- Item 1 holds in all generic extensions.
A statement $\phi$ admits such a pair iff, in addition,
- In any forcing extension, $\phi(x)$ iff $x\in p[A]$.
The idea is that this is a precise, formal, definable approximation to the intuitive statement one would actually like, namely, that there are such trees describing $\phi$ that have this ``complementary'' behavior in all outer models. First-order logic limits ourselves to considering forcing extensions.
Let me point out that $\Sigma^1_1$ and $\Sigma^1_2$ statements admit absolutely complemented pairs, so the existence of such a pair is a natural (far reaching) generalization of the two cases above.
Once we accept large cardinals, we can show that much larger classes than $\Sigma^1_2$ admit absolutely complemented trees. For example, any projective statement does. Once again, the point is that as soon as we have the large cardinals and real parameters in our universe, we have the trees, and the trees certify in unambiguous forcing-unchangeable terms, whether the statements hold at any given real. It is in this sense that we consider these statements more tractable.
Here is a rough sketch of an example I particularly like, due to Martin-Solovay (for measurables) and Woodin (in its optimal form). For details, see my paper with Ralf Schindler, ``projective well-orderings of the reals,'' Arch. Math. Logic (2006) 45:783–793:
$V$ is closed under sharps iff $V$ is $\Sigma^1_3$-absolute. $(*)$
The right hand side means that for any $\Sigma^1_3$ statement $\phi$ (so now we have three alternations of quantifiers) and any two step forcing ${\mathbb P}∗\dot{\mathbb Q}$, for any $G$, ${\mathbb P}$-generic over $V$, any $H$, ${\mathbb Q}$-generic over $V[G]$, and for any real $x$ in $V[G]$, we have
$$ V[G]\models\phi(x)\Longleftrightarrow V[G][H]\models\phi(x). $$
The left hand side of $(*)$ is a weakening of "there is a proper class of measurable cardinals", which is how the statement is usually presented.
The proof of the implication from left to right in $(*)$ goes by building a tree of attempts to find a witness to the negation of a $\Sigma^1_2$ statement. The goal is that if such a witness can be added by forcing, then in fact we can find one in the ground model. If there is a forcing adding a witness, there is a countable transitive model where this is the case. Essentially, the tree gives the construction of such a model, bit by bit, and if we have a branch, then we have such a model.
So: If there is a witness added in a forcing extension, the tree will have there a branch. So it is illfounded. By absoluteness of well-foundedness, the tree has a branch in $V$. The sharps are used to ``stretch'' the model so that we can use Shoenfield absoluteness, and conclude that there must be a witness in $V$.
4) Projective absoluteness, a consequence of large cardinals, is established by showing the existence of absolutely complemented trees for any projective statement. The theory of universally Baire sets originates with this concept, and the closely related notion of homogeneously Suslin trees. All of this is also connected to determinacy. Once again, to drive the point home: Generic absoluteness is not the goal. The goal is the existence of the pair of trees. Once we have them, we have a strong certificate of truth or falsehood of a statement. I do not know if one is to accept the search for such trees as a more tractable problem than the original statement whose pair of trees we are now searching for. But it certainly says that consistency of the statement, using large cardinals or any combinatorial tools whatsoever, is enough to have a proof of the statement. This seems much more hopeful and generous an approach than if only proofs in the usual sense are allowed. The existence of these trees for projective statements is what I meant in a comment by ``large cardinals settle second order arithmetic.'' Put yet another way: If you show, for example, that a projective statement is not 'decidable' (in the presence of large cardinals), meaning that it is consistent and so is its negation, then you have either actually showed that certain large cardinals are inconsistent, or you have found a way of changing the truth of arithmetic statements, and both of these options are much more significant events than the proof of whatever the projective statement you were interested in was. More likely than not, the truth value of the statement will be uncovered at some point, and you know there is no ambiguity as of what it would be, since the witnessing trees are already present in the universe.
(In spite of its length, I am not completely happy with this answer, but I would need to get much more technical to expand on the many interesting points that your question raises. Hopefully there is some food for thought here. For nice references to some of the issues I mention here, Woodin's article in the Notices is a good place to start, and Steel's paper on the derived model theorem has much of the details.)
Best Answer
In a recent result with Shay Moran, Pavel Hrubes, Amir Shpilka and Amir Yehudayoff, we show that the answer to a basic question in statistical machine learning is determined by the value of the continuum, and is therefore independent of the ZFC set theory. The paper will be available on Arxiv within a few weeks. Here is a link to that paper: https://arxiv.org/abs/1711.05195