Proper iteration master-condition lemma

We prove the displayed extension property by transfinite induction on $\alpha$. At $\alpha =\gamma$ take $q=q_0$: the hypothesis already says $q_0$ forces $\dot{p}\in {\dot{G}}_{\gamma }$. Assume as induction hypothesis that the property holds at every smaller iteration length.

We record the name-selection argument used below. Suppose $u$ forces that there is a set $x$ satisfying a fixed formula $\phi (x)$. By the existential forcing clause, the conditions below $u$ that force $\phi (\dot{x})$ for some name $\dot{x}$ are dense below $u$. Use A1 to choose a maximal antichain $A$ of such conditions and, for each $a\in A$, one witness name ${\dot{x}}_a$. The usual mixed name $\dot{x}={\bigcup }_{a\in A}({\dot{x}}_a\upharpoonright a)$ agrees with ${\dot{x}}_a$ below $a$. Thus the conditions forcing $\phi (\dot{x})$ are dense below $u$, and the forcing definition gives $u⊩\phi (\dot{x})$. This derives the needed maximum principle from the forcing clauses and AC rather than attributing it to F4.

Let $\alpha =\beta +1$. Apply the induction hypothesis at $\beta$ to obtain an $(M,P_{\beta })$-generic $q_{\beta }$ extending $q_0$ and forcing $\dot{p}\upharpoonright \beta \in {\dot{G}}_{\beta }$. In a $P_{\beta }$-extension containing $q_{\beta }$, the last coordinate $p(\beta )$ belongs to $M[G_{\beta }]\cap Q_{\beta }$. Since $Q_{\beta }$ is proper there, choose an $(M[G_{\beta }],Q_{\beta })$-master $q_{\beta }^{\ast }$ below it, and apply step 1.2 to choose a name for this condition. By F3, $(q_{\beta },{\dot{q}}_{\beta }^{\ast })$ forces $\dot{p}$ into the two-step generic. It is $(M,P_{\beta +1})$-generic: for any ordinal-valued $P_{\beta +1}$-name in $M$, the quotient master forces its value into $M[G_{\beta }]$, and the first-stage master then forces that ground ordinal into $M$; F2 applies. This gives the successor case.

Now let $\alpha$ be limit. The case $\gamma =\alpha$ was settled at step 1.1, so assume $\gamma <\alpha$ and put $\rho =\sup (M\cap \alpha )$. Choose an increasing sequence $⟨{\gamma }_n:n<\omega ⟩$ from $M\cap (\alpha +1)$ with ${\gamma }_0=\gamma$ and supremum $\rho$, and enumerate the dense subsets of $P_{\alpha }$ in $M$ as $⟨D_n:n<\omega ⟩$. Recursively construct $(M,P_{{\gamma }_n})$-generic $q_n$ and $P_{{\gamma }_n}$-names ${\dot{p}}_n$, beginning with the given pair, so that $q_{n+1}\upharpoonright {\gamma }_n=q_n$ and $q_n$ forces: $p_n\in P_{\alpha }\cap M$; $p_n\le p_{n-1}$ and $p_n\in D_{n-1}$ for $n>0$; and $p_n\upharpoonright {\gamma }_n\in G_{{\gamma }_n}$. For the recursive step, work in a $P_{{\gamma }_n}$-generic extension containing $q_n$ and resolve $p_n\in P_{\alpha }\cap M$. In the ground model define $E=\{u\in P_{{\gamma }_n}:u\perp p_n\upharpoonright {\gamma }_n\text{ or }(\mathrm{\exists }r\le p_n)[r\in D_n\mathrm{\&}u\le r\upharpoonright {\gamma }_n]\}\mathrm{.}$ The set $E$ belongs to $M$ and is dense: below a condition compatible with $p_n\upharpoonright {\gamma }_n$, first take a common extension, paste it to the tail of $p_n$, and then strengthen the resulting $P_{\alpha }$-condition into $D_n$. Since $q_n$ is an $(M,P_{{\gamma }_n})$-master, the generic meets $E\cap M$. Its member cannot take the incompatible alternative because $p_n\upharpoonright {\gamma }_n$ is in the same generic. Elementarity therefore supplies $p_{n+1}\in D_n\cap M$ below $p_n$ whose restriction lies in the generic. Apply step 1.2 to name that choice, then apply the induction hypothesis at ${\gamma }_{n+1}<\alpha$ to obtain $q_{n+1}$.

Define $q$ on $\rho$ by $q={\bigcup }_n{q}_n$ and fill every coordinate in $[\rho ,\alpha )$ with its supplied top name. This is a condition: the equalities $q_{n+1}\upharpoonright {\gamma }_n=q_n$ make the union a coherent function, and F6 makes its support, a subset of ${\bigcup }_n\mathrm{supp}(q_n)$, countable. This is the only fusion operation; no coordinatewise lower bound in an arbitrary proper iterand is used. To check what $q$ forces, take any $P_{\alpha }$-generic $G$ containing it and resolve the names $p_n$. For $k\ge n$, the construction and truth lemma give $p_n\upharpoonright {\gamma }_k\in G_{{\gamma }_k}$. Also $p_n\in M$, so the countable set $\mathrm{supp}(p_n)$ belongs to $M$ and is a subset of $M\cap \alpha \subseteq \rho$; hence $p_n\upharpoonright \rho =p_n$. The inverse-limit generic is determined on a condition by these cofinal projections, so $p_n\in G_{\rho }\subseteq G_{\alpha }$. Thus $q$ forces $p_n\in G_{\alpha }$ for every $n$, in particular $p_0=p$.

Step 3.1 shows that $q$ forces $p_{n+1}\in D_n\cap M\cap G_{\alpha }$ for every $n$, so every $D_n\cap M$ is predense below $q$; F2 makes $q$ $(M,P_{\alpha })$-generic. Its restriction to ${\gamma }_0$ is $q_0$, and step 3.1 gives $q⊩\dot{p}\in {\dot{G}}_{\alpha }$. The base, successor, and limit cases exhaust the induction, so the lemma holds for every $\alpha$. AC is used exactly in A1, including the countable-support union through F6.