What is a "class model" exactly?

Question

In the literature about set theory, one encounters the words "set-model" and "class-model" which I have difficulties to understand. Here is my viewpoint :

1. One starts with a metalangage which is strong enough to talk about sets. We call these naive sets. Examples of naive sets are sets of variable for first order theories, base sets for models of first order theories, etc. There is no notion of "class" in this metalangage, just a naive set theory.
2. ZF being a first order theory among others, I can consider a model $(M,\in)$ of this theory. $M$ is therefore a naive set of my metalangage.
3. Naive elements of $M$ are called "formal sets" and naive subset of $M$ are called "classes". After that, one can also define the notion of "definable class", etc.

In this presentation there is no notion of "class model". Now of course I could create a model inside another model. Let's say $N \subset M$. Then $N$ is a "class model" with respect to $M$ but that doesn't change the fact that $N$ is a naive set with respect to the metalangage. So this notion of "class model" at best makes sense if we already work inside another model. However, in the literature I have seen class models popping from nowhere, not built inside a previous model. How can that happen ? Thanks for any clarification on this subject. All these considerations about set theories built inside set metatheories can be particularly messy.

Answer 1

If we work in a metatheory like ZFC with only sets, then classes become part of the meta-meta-theory. A class is just a formula $\varphi(x)$ which we intuitively interpret as $\{x:\varphi(x)\}.$ If we use class notation, we might call the class $C$, and then to assert $x\in C$ for some set $x$ is just an abbreviation for asserting $\varphi(x).$

(Classes can also have parameters, but let's keep it simple.)

Class models are classes satisfying certain axioms. For a class $C$ to satisfy a sentence $\psi$ means that the relativization $\psi^C$ holds.

(The relativization is obtained by recursively replacing all quantifiers by quantifers over $C,$ e.g. $(\forall x\chi(x))^C$ means $\forall x( x\in C\to \chi^C(x))$.)

The simplest example of a class model is the class of all sets, $V,$ whose corresponding formula is just $x = x$ (or anything else that's always satisfied). Trivially, for any sentence $\psi,$ $\psi^V$ is logically equivalent to $\psi,$ so since each ZFC axiom holds, $V$ is a class model of ZFC.

---

We can also work in a metatheory like NBG where classes are first-class, and we have an actual thing $V$ called the class of all sets. One might worry that you run into trouble here: NBG famously can't prove the consistency of ZFC (unless it is inconsistent), and yet if we have a formal object that satisfies ZFC, shouldn't we be able to do just that?

Fortunately for math, and unfortunately for NBG, we can't do this, because while we can talk formally about $V$ in the theory, we can't formally express the notion of $V$ satisfying a sentence or set of sentences. Like in ZFC, class satisfaction in NBG happens via relativization in the meta-meta theory and $V$ is only a model of ZFC in that weaker sense.

If we use the class theory MK instead (which is NBG with a stronger class comprehension scheme), then we can express class satisfaction formally, and sure enough, MK proves the consistency of ZFC.

---

If we're working in a truly naive informal metatheory, then one must simply stretch one's naive informal notions to include one of proper classes as well. It will miraculously happen that the rules that naively apply to naive informal classes and naive informal sets are in agreement with these formal theories.

Answer 2

Let me add a bit to spaceisdarkgreen's answer. The key difficulty that class models introduce is with respect to their theories.

Given a structure $\mathcal{M}$, the theory $Th(\mathcal{M})=\{\varphi:\mathcal{M}\models\varphi\}$ is defined in a $\Sigma^1_1(\mathcal{M})$ way: "$\mathcal{M}\models\varphi$" is taken to mean "There is a [family of Skolem functions/appropriate subtree of the syntax tree of $\varphi$/some other similar object]," and this witnessing object is more-or-less a function defined on all of $\mathcal{M}$. If we blindly try to apply the same definition to a class-sized structure, no such functions exist at all, so for instance $$V\models \forall x(x=x)$$ would technically be false if interpreted this way.

Now it is true that for each $n$ we can come up with a truth predicate for $n$-quantifier formulas which works for class-sized structures. So for instance we can perfectly well talk about the $\Sigma_n$ theory of $V$ inside $V$ itself, for a fixed $n$. But this is the fundamental limitation that shifting from set-sized to class-sized structures introduces: their theories are no longer appropriately definable.

(This basic point occurs in various guises; I've written a couple posts treating it, e.g. here or the last paragraph of here.)