Can ZFC → NBG be iterated?

Question

von Neumann-Bernays-Gödel set theory (NBG) is a conservative extension of ZFC which contains "classes" (such as the class of all sets) as basic objects. "Conservative" means that anything provable in NBG about sets can also be proven in ZFC. The essential properties which make this true (as opposed to, say, Morse-Kelley set theory, which is not conservative) are that classes cannot be elements of other classes (in particular, powerclasses and function classes do not exist), and class comprehension is "predicative", i.e. quantified variables can range only over sets.

My question is, can the operation "ZFC → NBG" be iterated? Can we add to NBG new basic objects called (say) "2-classes" (such as the 2-class of all classes), which can contain classes as elements (but not other 2-classes), and where 2-class comprehension can use quantified variables that range over classes, but not over 2-classes? (Well, obviously, we can, but the real question is whether it would be conservative over NBG, hence also over ZFC.)

Background: I am wondering about this as a foundation for category theory. Most "large" categories which arise in mathematics, outside of category theory itself, can be defined in NBG (or even in ZFC, sort of, using the usual trick of representing proper classes by the first-order formulas defining them). But in category theory, we sometimes want to study things like "the category of large categories" or "the functor category between two large categories," which cannot be defined in NBG or ZFC. The usual solution is to assume a Grothendieck universe (or inaccessible cardinal), but this seems somewhat extravagant, since most of these new beasts only live "one more level up" from the classes in NBG. So I wonder whether we can get away with a further conservative extension of this sort.

Answer 1

There is a cheap way of doing this, which may not be the optimal approach when a subtle task (such as the foundational question you have in mind) is the goal. But, then again, this may suffice.

Working in an appropriately strong theory, to simplify, the standard way to check that NBG is conservative over ZFC is to see that any model $M$ of ZFC can be extended to a model $N$ of NBG in such a way that the "sets" of $N$ give us back $M$. Again to simplify, assume the model $M$ is transitive. The model $N$ we associate to it is Gödel's $\mathop{\rm Def}(M)$, the collection of subsets of $M$ that are first order definable in $M$ from parameters (The proper classes are the elements of $\mathop{\rm Def}(M)\setminus M$.)

This suggests the simple solution of defining the models of "iterated-NBG" as the result of iterating Gödel's operation. So, given a transitive model $M$ of ZFC, the $\alpha$-th iterate would simply be what we usually denote $L_\alpha(M)$.

I am restricting to transitive models here, but there is a natural first order theory associated to each stage of the iteration just described (at least, for "many" $\alpha$), and I guess one could try to axiomatize it decently if enough pressure is applied.

There are some subtleties in play here. One is that most likely we want to stop the iteration way before we run into serious technicalities ($\alpha$ would have to be a recursive ordinal, for one thing, but I suspect we wouldn't want to venture much beyond the $\omega$-th iteration). Another is that the objects we obtain with this procedure would have wildly varying properties depending on specific properties of $M$.

For example, if $M$ is the least transitive model of set theory, then we "quickly" add a bijection between $M$ and $\omega$. In general, if $M$ is least with some (first order in the set theoretic universe) property, then we "quickly" add a bijection between $M$ and the size of the parameters required to describe this property (this is an old fine-structural observation. "Quickly" can be made pedantically precise, but let me leave it as is).

So you may want to work not with ZFC proper but with a slightly stronger theory (something like ZFC + "there is a transitive model of ZFC" + "there is a transitive model of "ZFC+there is a transitive model of ZFC"" + ...) if you want some stability on the theory of the transitive models produced this way. (Of course, this is an issue of specific models, not of the "iterated-NBG" theory per se).

---

I should add that I do not know of any serious work in the setting I've suggested, with two exceptions. One, in his book on Class Forcing, Sy Friedman briefly mentions a version of "Hyperclass forcing" appropriate to solve some questions that appear in a natural fashion once we show, for example, that no class forcing over $L$ can add $0^\sharp$. The second is by Reinhardt in the context of large cardinals and elementary embeddings, and is described by Maddy in her article "Believing the axioms. II". As far as I remember, neither work goes beyond hyperclasses, i.e., classes of classes.