# Axiomatic framework used for Class Forcing

In Class Forcing, one inevitably has to discuss proper classes as concrete mathematical objects.

For example, in defining pretameness in Chapter 8 definition 2.2 of the Handbook, we speak of a sequence of classes, which we later enumerate over. I'm trying to understand in what axiomatic framework could we be working in.

In ZFC we can't speak about classes this way. In NBG we can talk about classes, but we can't quantify over them. Specifically, if a class is a member of another class, then it must be a set, so we can't talk about an infinite sequence of them. But our sequence is made of proper classes. If we go up to MK, then our theory isn't a conservative extension of ZFC anymore, and we can't really be sure our conclusions about sets are valid in ZFC.

Alternatively, we could try and justify our discussion by working within $V_\kappa$, for some $\kappa$ inaccessible cardinal. Then all our annoying classes become sets. But this presupposes the existence of such a cardinal, which I don't think the theory of class forcing really hinges on.

In what axiomatic framework are we working in when discussing class forcing?

• Just a minor remark, if you're more comfortable with $V_\kappa$ for an inaccessible cardinal than with Kelley–Morse, then you're doing it backwards. Since $V_{\kappa+1}$ would be a model of Kelley–Morse, this means that the assumption is stronger from a foundational point of view. Dec 10 '17 at 20:01

First of all, you can quantify over classes in NBG. It wouldn't be much of a class-enabled set theory otherwise. What you can't do, however, is use Comprehension with class quantifiers.

Note that just like in ZFC, if you can uniformly index your classes, then what you have is a class $\{\langle i,v\rangle\mid i\in I, \varphi(v,i)\}$ where $\varphi$ is a uniform definition (e.g. a ground model can be defined uniformly with the parameters varying). In that case, the $i$th class is obtained by simply taking $\{x\mid\varphi(v,i)\}$. It is certainly an object of the theory, and the Comprehension is well within the power of NBG (and even ZFC, if you consider classes as formal objects).

So you can certainly use NBG to formalize class forcing. Whenever you are quantifying over classes, if necessary this can be turned into a schema-theorem. Namely, a theorem where there is a meta-theoretic universal quantifier, but the theory (in this case NBG) proves every single instance. This situation is similar to the proof that $L$ is a model of ZFC, which is itself a schema-theorem.

In any case, there has been a lot of recent work on the topic. You can start by looking at the following papers:

1. The Ground Axiom, Jonas Reitz's PhD thesis which includes an appendix with the framework for class forcing.

2. Class forcing, the forcing theorem and Boolean completions, by Peter Holy, Regula Krapf, Philipp Lücke, Ana Njegomir, Philipp Schlicht.

3. Characterizations of pretameness and the Ord-cc, by Peter Holy, Regula Krapf, Philipp Schlicht.

4. Sufficient conditions for the forcing theorem, and turning proper classes into sets, by Peter Holy, Regula Krapf, Philipp Schlicht.

5. The exact strength of the class forcing theorem, by Victoria Gitman, Joel David Hamkins, Peter Holy, Philipp Schlicht, Kameryn Williams.

• מה הקשר בין מחט לתחת? :) Dec 9 '17 at 20:23
• @AlonNavon: Given a class $I$, you can define an $I$-indexed family of classes to just be a subclass $S$ of $I\times V$, where the class corresponding to $i\in I$ is $\{x:(i,x)\in S\}$. Dec 9 '17 at 20:32
• @Alon: One way out is to have a "template theorem". It's a theorem that whenever you plug into it a class which has such and such properties (e.g. an inner model), then you can prove something. Then the quantification over a collection of inner models is in the meta-theory. But you still get the results, for the most part. Dec 9 '17 at 20:37
• @Alon: It's not a real term. It means that the quantification is in the meta-theorem. Kinda like how we can prove that for every axiom of ZFC, it holds in L. The general proof is the same, but ultimately it's a template-theorem: ZFC proves every instance, but not uniformly. Dec 9 '17 at 20:43
• @Alon: Is that better? Dec 10 '17 at 20:00