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