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?
 A: 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:


*

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

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

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

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

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