Class forcing: Pelletier vs Friedman

[Apologies in advance for a fluffy question]

I'm reading this old paper by Pelletier, where he gives a Boolean-valued model version of class forcing, assuming that the Boolean algebra in question can be written as an $Ord$-indexed increasing union of CBAs $B_\alpha$. The model is given by induction, as usual, with a twist:

• $^RV^B_0 = \emptyset$
• $^RV^B_{\alpha+1} = \lbrace u \in B_{\alpha+1}^{dom(u)} |\ dom(u) \subseteq {}^RV^B_\alpha\rbrace$
• $^RV^B_\lambda = \bigcup_{\alpha \lt \lambda} {}^RV^B_\alpha$ for $\lambda$ limit.
• $^RV^B = \bigcup_{\alpha \in Ord} {}^RV^B_\alpha$

So in a sense, our hierarchy is restricted as to what can appear at the $\alpha$th stage. Given a certain condition on $B$ called ARP (I can supply details if desired), he shows that $^RV$ is a model of ZFC-Powerset. Another condition on $B$ gives us Powerset, and all this works in the usual Easton situation (ARP seems to be related to Easton support, but I may be wrong).

On the other hand, Friedman (although I'm reading his book), given a proper class $P$ of conditions defines names and interpretations as per usual for an ordinary forcing with no restrictions to get $M[G]$ (here $M$ satisfies a relativised $V=L$). He then shows that with a pretameness condition on P - that every set-indexed collection of dense (definable-with-parameters) classes in $P$, at the cost of passing to a $q\leq p$, there are subsets of each class whose down-closure is dense below $q$ - we have that $M[G]$ is a model of ZF(C)-Powerset. Then with an additional tameness condition on $P$, which refers to the cumulative hierarchy of the base model $M$, he shows $M[G]$ is a model of ZF(C).

What I want to know is how these two approaches can get away with introducing the stratification in the two different parts of constructing the new, class-forced model. Pelletier uses ARP to show that $|| - ||$ is well-defined (so not having to quantify over classes) using his stratification of $B$, then the other condition to show that powerclasses are sets. Friedman uses pretameness to show $\Vdash$ is definable and then proves the relevant axioms hold, then uses tameness, and its condition using $V_\alpha^M$ to get powersets.

Perhaps it is just the different approaches of BVM and forcing using conditions, but I'm trying to take a third approach, and seeing where the stratification restriction is used seems to be crucial for what I need.

EDIT: Then again, Jech just says to form the BVM $V^{B_\alpha}$ for each $\alpha$ and then take the union of them all, so this stratifies in yet another way.

Since you are interested in comparing various approaches to class forcing, I would recommend that you also take a look at the dissertation of Jonas Reitz, which has an extended, detailed appendix presenting class forcing for both ZFC and GBC models. Reitz follows a line similar to the Pelletier approach, defining the extension in the case that the class partial order $\mathbb{P}$ is a tower of complete set-sized subposets, using these subposets to stratify the final model in way that is fundamentally similar to what you describe.

Ultimately, the main focus for Reitz is on the class forcing notions $\mathbb{P}$ that are what he calls progressively closed, meaning that for every cardinal $\delta$, the forcing has a complete subposet---in particular, a set---whose quotient is forced to be $\lt\delta$-closed (see the details in his dissertation). This kind of forcing is particularly nice, in that every set that is added by the full class forcing is also added by some set-sized complete subposet, and the hypothesis allows one to handle various arguments much more easily than otherwise. Furthermore, many of the most natural class forcing notions that arise in set theory are in fact progressively closed, such as the canonical forcing of the GCH, the forcing of V=HOD by coding sets into the GCH pattern, the universal Laver preparation, Easton forcing to control the GCH pattern and many others.

The important fact about progressively closed class forcing is that, as Reitz proves, the corresponding forcing extensions by them will always satisfy ZFC and even GBC.

One must make some kind of extra assumption like that, even in the Pelletier approach, where $\mathbb{P}$ is a tower of complete subposets, since otherwise one may not have ZFC in the extension. To see this, consider the case of adding ORD many Cohen reals, which stratifies very nicely in just the way you describe in your question (although it is not progressively closed), but which does not have ZFC in the extension, since even power set will fail at $\omega$---the set of reals in the resulting model will form a proper class!

The Friedman approach is aimed at a more general situation, where he is specifically interested in class forcing that is not progressively closed, and which admits no stratification of the sort for which you are looking. For example, a motivating instance for him, I believe, is the case of Jensen's "coding the universe" forcing, which is definitely not progressively closed, and has the property that it adds sets that are not generic for any set-sized poset in the ground model. Because of this more general setting, he has to pay attention to when the forcing relation will be definable with respect to the class forcing notion, and when the partial order will ensure the power set axiom, and these are the issues at which the tameness concepts are aimed.

The main difficulty with attempting to use a purely Boolean-valued model approach with class forcing is that one generally doesn't actually have a complete Boolean algebra in this context. The reason is that one usually conceives of a forcing notion first and most naturally as a partial order $\mathbb{P}$, rather than as a Boolean algebra. When this is a set, it is a simple matter to take the Boolean completion $\mathbb{B}$, for example as the regular open algebra, and so working with $\mathbb{P}$ or $\mathbb{B}$ makes little difference. But when the forcing partial order $\mathbb{P}$ is a proper class, then it may not be possible to find a completion of $\mathbb{P}$ in any suitable sense. Generally, objects in the completion correspond to antichains in the partial order, and the collection of all (class-sized) antichains may not itself be a class; they are too big themselves and there are too many of them.

For this reason, one is tempted to extend the universe upward, adding extra layers on top, so that one can make sense of the forcing in a set-theoretic context, but the difficulty is that one cannot always expect to extend the universe upward in that way while retaining a nice theory.

Ultimately, the goal is only to make class forcing work. Pelletier's stratification and Friedman's pretameness are what worked for them. Their solutions are well motivated but it is nonetheless a means-to-an-end scenario. So, what does it take to make class forcing work? There are lots of necessary ingredients but two stand out as key ingredients. A good approach is to cook these two key ingredients first and then season to taste.

The first key ingredient is that names should be sets or, more generally, coded by sets. One of the reasons for this is that to make sense of the forcing relation you need to quantify over names and this is not possible in ZFC with proper classes and even in NBG, where proper classes actually exist, you cannot use class quantifiers in instances of comprehension; MK can get away with a lot more but it still has issues gathering a bunch of classes together in order to manipulate them in various ways. So, the ideal situation is that names are sets but there is a little room for tweaking if you are very careful about it.

The second key ingredient is the maximality principle: if $p \Vdash \exists x\phi(x)$ then there should be a name $\dot{a}$ such that $p \Vdash \phi(\dot{a})$. This is usually accomplished by patching names together. Indeed, if $p \Vdash \exists x\phi(x)$ then there certainly ought to be densely many extensions $q$ of $p$ such that $q \Vdash \phi(\dot{a}_q)$ for some name $\dot{a}_q$. The usual trick is to get a maximal antichain $q_i$, $i \in I$, of extensions of $p$ together with matching names $\dot{a}_i$ with $q_i \Vdash \phi(\dot{a}_i)$ and patch these names together into a name $\dot{a}$ such that $q_i \Vdash \dot{a} = \dot{a}_i$ for each $i \in I$. (Compare with the definition of sheaf in category theory.) In order to make this work, it is best that $I$ is a set and that the axiom of choice holds in the ground model. Again there is a bit of flexibility here. For example, Friedman is able to get by with a slightly weaker version of the maximality principle.

The remaining ingredients often fall into place by themselves (provided your target forcing isn't trying to do something unreasonable) so once you have these two key ingredients most of the work is already done.

I think the last paragraph of Joel Hamkins's answer provides a useful way to think about these sorts of forcing. Imagine that you have an inaccessible $\kappa$ (or, perhaps better, a $\kappa$ such that $V_\kappa$ is an elementary submodel of the universe) and that you're forcing with a poset $\mathbb P\subseteq V_\kappa$. You get a forcing extension of the universe (since $\mathbb P$ is a mere set in this picture), but your objective is to get a ZFC model by restricting this model to ranks $<\kappa$. Several issues arise. You need to decide what "restricting to ranks $<\kappa$" means. It could mean taking $V_\kappa$ in the forcing extension. It could mean taking those elements of the forcing extension that have names (in the ground model) of ranks $<\kappa$. I've seen both versions, and I don't think they're equivalent.

If you want to use Boolean-valued models, then the complete Boolean algebra $\mathbb B$ associated to $\mathbb P$ is one level higher in the cumulative hierarchy than $\mathbb P$, so you need to reconsider anything involving ranks of names.

These issues are "formal" in the sense that they concern how you want to set up the machinery. But there are also some substantive issues that you must face no matter how you set up the machinery. For example, as Joel mentioned, you'd better make sure you haven't added $\kappa$ new reals, as they would ruin ZFC restricted to ranks $<\kappa$. (Whether they ruin the power set axiom or the replacement scheme seems to depend on how you choose to "restrict to ranks $<\kappa$".)