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.

-
The forcing is done internally even if you use the CTM argument, it will not be countable internally, and you want to make the choice within the model. –  Asaf Karagila Feb 4 '12 at 10:17
@AsafKaragila Surely, the CTM argument is done externally. You can't argue inside the model that there are only countably many dense sets. On the other hand, I seem to unconsciously believe that the proof that there is a generic set for countably many dense sets should work for any cardinal. Silly inner voice. –  Miha Habič Feb 4 '12 at 11:01
True, it is done externally. However depending on the forcing you could argue it only have so-many dense sets. As for the generalizations, I asked my advisor once and he thought about it and said it's not immediate and you'd have to require more on the forcing itself and on the cardinal. –  Asaf Karagila Feb 4 '12 at 11:04
@AsafKaragila I had a thought. Since the CTM argument doesn't seem to work as is, would it be possible to cheat a bit and temporarily move the discussion to a countable model of NBG? There we can reproduce the argument verbatim and get our generic class. Since ZFC and NBG are equiconsistent, this should be adequate for relative consistency proofs. I'm beginning to suspect Easton had the right idea, originally working in NBG. Doing these things in ZFC looks really tedious. –  Miha Habič Feb 4 '12 at 18:55
It is indeed cheating, the fact NBG is a conservative extension of ZFC means only that proofs which only contain statements about sets (and maybe definable classes) can be done in ZFC; but class forcing is a whole other thing. Equiconsistency is of no help either, ZF is equiconsistent with ZFC but this doesn't mean you can just go about using the axiom of choice if you did not assume it at first, nor it will help you prove things in pure ZF. –  Asaf Karagila Feb 4 '12 at 19:04

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.

-
Could you elaborate how Global Choice actually helps here? In particular, as I gather from Friedman's papers and other places, the problem seems to be identifying the ground model in an extension. –  Miha Habič Feb 5 '12 at 18:36
@Miha: No, I cannot really tell you because I am unfamiliar with the intimate details of class forcing. Whenever I bring this up I mostly get the reaction "Oh this is very complicated... you should check out Sy Friedman's work. He's done some cool things but they are very hard to understand to the most part." You asked for a reference and I gave you one. The little intuition I have is that classes are not actual objects in ZFC therefore require a much more careful handling. –  Asaf Karagila Feb 5 '12 at 22:10

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.

-
You could at least say that you copied this from Friedman's Fine structure and class forcing (Preface, Fact 1)... –  Asaf Karagila Feb 5 '12 at 22:06

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$.

-
You know, in just one year you seem to have studied a lot of set theory. Nice work! –  Asaf Karagila Dec 10 '13 at 0:36
@AsafKaragila, How not to do it, it's so much fun! :-) –  Camilo Arosemena Dec 10 '13 at 0:38