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?