Downgrading from ZFC with universes to ZFC

If you want a universe-like theory that is conservative over ZFC, that is, which proves no additional facts about sets that ZFC cannot prove alone, then the thing to do is to work in the following theory, which is also described in the answers to this MO question.

The theory consists of ZFC plus the assertion that there is a hierarchy of universe-like sets, namely, $V_\theta$ for all $\theta\in C$, a closed unbounded proper class of cardinals, and furthermore that truth in these $V_\theta$ cohere with each other and with the full set-theoretic universe $V$, so that they form an elementary chain. Specifically, the theory has ZFC, the assertion that $C$, a new class predicate, is a closed unbounded proper class of cardinals, and the scheme asserting that $V_\theta$ is an elementary substructure of $V$ for every $\theta\in C$, namely, the scheme expressing of each formula $\varphi$ in the language of set theory that

• $\forall x\ \forall\theta\in C\text{ above the rank of }x \ (\varphi(x)\iff V_\theta\models\varphi[x])$.

It follows from this theory that the models $V_\theta$ for $\theta\in C$ form an elementary chain, all agreeing with each other and with the full set-theoretic background universe on what is true as you ascend to higher models. It follows that every $\theta$ in $C$ will be a strong limit cardinal, a beth fixed point and so on, and so these cardinal exhibit very strong closure properties. In particular, I could have written $H_\theta$ instead of $V_\theta$---these are essentially the $\theta$-small universes, the collection of sets of hereditary size less than $\theta$. The only difference between these $V_\theta$ and an actual Grothendieck universe is that in this theory, you may not assume that $\theta$ is regular. But otherwise, they function just like universes in many ways, and indeed, every $V_\theta$ for $\theta\in C$ is a model of ZFC. Because of the coherence in the theories, these weak universes can be more useful than Grothendieck universes for certain purposes. For example, any statement true about an object in the full background universe will also be true about that object in every weak universe $V_\theta$ for $\theta\in C$ in which it resides. Thus, it one takes care, one can use the $V_\theta$ much like Grothendieck universes, and this was the point of my linked answer above (as well as Andreas's).

Meanwhile, the theory is conservative over ZFC, since in fact every model of ZFC can be elementary embedded into (a reduct of) a model of this theory. This can be proved by a simple compactness argument, using the reflection theory. If $M\models ZFC$, then add constants for every element of $M$, add the full elementary diagram of $M$, add a new predicate symbol for $C$ and all the axioms of the new theory. Every finite subtheory of this theory is consistent, by the reflection theorem, and so we get a model of the new theory, which elementary embeds $M$ since it satisfies the elementary diagram of $M$.

(Although it seems counterintuitive at first to some set-theorists, this theory does not prove Con(ZFC), if ZFC is consistent, even though it asserts in a sense that $V_\theta$ is elementary in $V$ for all $\theta\in C$ and hence that $V_\theta$ is a model of ZFC. The explanation is that the theory only makes the assertion that $V_\theta$ is elementary in $V$ as a scheme, and not as a single assertion (which is not expressible anyway by Tarski's theorem), and thus the theory does not actually prove that $V_\theta\models ZFC$ for $\theta\in C$, even though they do model ZFC, since the theory only proves every finite instance of this, rather than the universal assertion that every axiom of ZFC is satisfied in every $V_\theta$.)