Countable-support forcing iterations

Fix an ordinal $\delta$ and set-indexed data $⟨P_{\alpha },{\dot{Q}}_{\alpha },{\dot{1}}_{\alpha }:\alpha <\delta ⟩$. As in Finite-support forcing iterations, $P_0$ is trivial, $P_{\alpha +1}$ is identified with the two-step iteration $P_{\alpha }\ast {\dot{Q}}_{\alpha }$, and ${\dot{1}}_{\alpha }$ is a supplied name forced to be the largest condition of the nonempty preorder ${\dot{Q}}_{\alpha }$. More precisely, for each $\alpha <\delta$ let $R_{\alpha }$ be the set-sized second-name carrier used for that two-step iteration and require ${\dot{1}}_{\alpha }\in R_{\alpha }$. At a limit $\gamma \le \delta$, a condition $p\in P_{\gamma }$ is a coherent function on $\gamma$ with $p(\alpha )\in R_{\alpha }$ such that

$p\upharpoonright \alpha {⊩}_{P_{\alpha }}p(\alpha )\in {\dot{Q}}_{\alpha }$

for every $\alpha <\gamma$, and its nontrivial support

$\mathrm{supp}(p)=\{\alpha <\gamma :p\upharpoonright \alpha ⊮p(\alpha )={\dot{1}}_{\alpha }\}$

is at most countable. Coordinates outside the support are filled by the specified top names. The order is stronger-is-smaller:

$p\le q⟺(\mathrm{\forall }\alpha <\gamma )p\upharpoonright \alpha ⊩p(\alpha ){\le }_{{\dot{Q}}_{\alpha }}q(\alpha )\mathrm{.}$

This recursive system is a countable-support iteration, and the limit order is its countable-support inverse limit. It differs from the direct finite-support limit precisely by allowing countably many nontrivial coordinates.

For $\eta \le \gamma$, the restriction map is $p\mapsto p\upharpoonright \eta$. In a $P_{\eta }$-generic extension, the quotient is

$P_{\gamma }\mathrm{/}{G}_{\eta }=\{p\in P_{\gamma }:p\upharpoonright \eta \in G_{\eta }\},$

with the inherited order; equivalently one may use the canonical $P_{\eta }$-name for the tails $p\upharpoonright [\eta ,\gamma )$. Thus a name for a quotient condition always comes with the requirement that its initial restriction belongs to the generic filter.

The definition itself makes no choice. Later limit arguments may take the union of a sequence of coherent initial segments, meaning $q_{n+1}\upharpoonright {\eta }_n=q_n$ for increasing ${\eta }_n$; this is not an assertion that arbitrary coordinatewise descending sequences in proper iterands have lower bounds. Showing that the resulting union has countable support uses the applicable countable-union principle and is kept as an explicit proof obligation there.