Various sizes of models of NBG inside NBG (what does a class-sized model give us?)

Question

Following this question and that one illustrating how induction in NBG can be tricky, I realized I'm also confused about the notion of “model” of NBG. The goal of this confusion is to hopefully lift this confusion (for me and, perhaps, for other people).

A model of NBG inside NBG is a collection $V$ of (internal) “sets”, a collection $W$ of (internal) “classes” and a collection $E$ of belonging relations, with $V \subseteq W$ and $E \subseteq V\times W$, which satisfies the axioms of NBG. Depending on how “collection” is interpreted in this definition, this seems to give three different possible concepts:

• a “small model” of NBG, or (set,set)-sized model, is one in which $V$, $W$ and $E$ are all sets (in the sense of the “external” NBG, of course),

• a “medium model” of NBG, or (set,class)-sized model, is one in which $V$ is a set but $W$ and $E$ are classes,

• a “large model” of NBG, or (class,class)-sized model, is one in which $V$, $W$ and $E$ are all classes,

Actually, a medium model is the same as a small model because Extensionality for classes tells us we can identify $W$ with a subset of $\mathscr{P}(V)$, so if $V$ is a set then so is $W$. So we can forget about medium models.

Now small models are the ones Gödel's completeness theorem tells us something about: it is a theorem of ZFC that there exists a model of NBG iff NBG is consistent, and since theorems of ZFC are the same as theorems of NBG that talk only about sets, it is a theorem of NBG that there is a small model of NBG iff NBG is consistent (and this is also equivalent to the existence of a small model of ZFC and to the consistency of ZFC).

If we look at models of ZFC inside NBG (which have just $V$ and $E$), the existence of a small (i.e., set-sized) model is tantamount to an arithmetic statement, as pointed out in the previous paragraph; on the other hand the existence of a large (i.e., class-sized) model should be obvious: just take the class of all sets. Except I'm not sure we can even express in NBG the fact that a class is a model of ZFC because ZFC has infinitely many axioms (and as I learned in the questions mentioned at the start we can't even perform mathematical induction on classes), so I'm treading on thin ice here.

But for models of NBG, which has finitely many axioms, this difficulty should not arise, so it appears the notion of “large model” of NBG inside NBG is well-defined, and I don't see an obvious way to get one, nor an argument why it should imply the consistency of NBG. Hence:

Question: What does the existence of a “large model” of NBG, as a statement of NBG, tell us? Is it equivalent to an arithmetical statement? Is it equivalent to a statement purely about sets?

More general plea: Please help me clear up the confusion which is probably obvious in this question!

Answer 1

In NBG, the existence of a large model of NBG implies (and therefore is equivalent to) the consistency of NBG.

Since NBG is finitely axiomatized, all its axioms have quantifier rank bounded by a constant $k$. Thus, the cut-elimination theorem (which is provable in $I\Delta_0+\mathrm{SUPEXP}$, and a fortiori in NBG) ensures that if NBG is inconsistent, then there is a proof of inconsistency in NBG in which all formulas have quantifier rank at most $k$ (or $k+1$ or so, depending on the exact details of the proof system). But if $M=(V,W,E)$ is a large model of NBG, you can easily define (as a class) a satisfaction predicate for $M$ for formulas of fixed quantifier rank. Then you can prove by induction on the length of a proof that all formulas in a proof from NBG using only formulas of rank at most $k$ are true, and in particular, no such proof can be a proof of inconsistency.