Does forcing with a proper class of conditions require Global Choice? When Jech, in his Set Theory, deals with forcing with a class of forcing conditions (with the aim of proving Easton's theorem), he starts with the assumption that there is a well-ordering of the ground model, i.e. the ground model satisfies the Axiom of Global Choice.
Having examined and, to a degree, understood the development in this section, I can't figure out where he actually uses this assumption. The only place I can see where this might be relevant is in the discussion on the existence of a generic set and even here it seems Global Choice isn't needed in every possible solution. For example, if you justify forcing via a reflection theorem argument or a countable ground model, I don't believe you need Global Choice.
On the other hand, you can take the Boolean-valued semantics approach and define the canonical name for the generic set as $\dot{G}(\check{p})=p$ for a forcing condition $p$ (assume here that the forcing notion is a proper class Boolean algebra). So far we're fine,
$\dot{G}$ is a class in the Boolean-valued model, everything is rosy. Conceivably, if we
were to define a class $\check{M}$, representing the ground model in the Boolean-valued model, via $$\|x\in\check{M}\|=\bigvee_{y\in M}\|x=\check{y}\|$$ the Boolean-valued model would see itself as the generic extension of $\check{M}[\dot{G}]$, since this holds when forcing with a set of conditions. Of course, there is a problem in defining $\check{M}$ this way, since we can't generally take sups of a proper class of (different) Boolean values.
I expect this approach should be salvageable, using Global Choice. In particular, I think we should be able to take the offending sup along the given well-ordering of $M$ and somehow "stagger" it, so it becomes well defined. 
I'm not at all sure if this is legitimate or if it even leads anywhere, so I would appreciate comments and an explanation of what is really going on. Additionally, can anyone suggest another reference for class forcing? I generally enjoy Jech's book, but I found this section to be somewhat opaque and hard to understand.
 A: For class forcing I'd suggest to start with Sy Friedman's work which can be found here.
In particular, his chapter from the Handbook of Set Theory (available on the above site) can be used as a good start.
The problem with class forcing is that classes are not "real" objects in the universe of set theory. They are formulas interpreted in the model as definable collections. This means that arguments which you can get "for free" from sets are now very expensive in the sense that you need to verify things. Global choice makes things easier because it keeps all classes in the same size and allows us to choose from everything at once.
A: There exists $L$-definable class forcings $P_0$ and $P_1$  such that whenever $G_0$ and $G_1$ are $P_0$-generic, $P_1$-generic over $L$, respectively. 
(a) $ZFC$ holds in $\langle L[G_0],G_0\rangle$ and in $\langle L[G_1],G_1\rangle$.
(b) ZFC fails in $\langle L[G_0,G_1],G_0,G_1\rangle$.
Thus, we cannot preserve ZFC and have generics for all ZFC preserving $L$-definable class forcings. So the existence of the generic is not a trivial matter. 
A: Global choice can be skipped since we can argue within some CTM, $M$, and noticing that the rest of the construction can be carried only assuming that $M$ is a model of $\mathsf{ZFC+GCH}$ and that there exists a generic filter; notice that $M^B$ is not a Boolean-Valued model, and thus we don't need choice to prove the truth lemma; we don't have to show $M^B$ is a full Boolean-valued model, and we define $p\Vdash\exists x\psi(x,\ldots)$ iff $\forall q\leq p\exists r\leq q\exists a\in M^B(p\Vdash \varphi(a,\ldots)),$ and it is easy to prove the truth lemma using only the genericity of the given $G$. 
However, if you use the canonical name argument approach, you do need global choice to hold in the ground model, as you need to turn $M^B$ into a 2-valued model inside $M$, to accomplish this you construct a non-principal ultrafilter of the Boolean algebra class $B$; as done here. 
To prove the existence of $U$ inside $M$ you use global choice as follows: as $B=\bigcup_\lambda B_\lambda$, where $\lambda$ goes through all regular cardinals. By transifinite induction, choose a non-principal ultrafilter $U_\omega$ of $B_\omega$. For $\lambda>\omega$ regular, choose  a non-principal ultrafilter $U_\lambda$ of $B_\lambda$ extending all of the $U_\kappa$ for regular $\kappa<\lambda$, then put $U=\bigcup_\lambda U_\lambda$.
