Finite-support forcing iterations

An ordinal-length finite-support iteration is defined recursively from set-indexed data $⟨P_{\alpha },{\dot{Q}}_{\alpha },{\dot{1}}_{\alpha }:\alpha <\delta ⟩$. The order $P_0$ is trivial. At each stage let $R_{\alpha }$ be the set-sized second-name carrier of Two-step forcing iterations for the $P_{\alpha }$-name ${\dot{Q}}_{\alpha }$, and supply a distinguished ${\dot{1}}_{\alpha }\in R_{\alpha }$ such that $1_{P_{\alpha }}⊩{\dot{1}}_{\alpha }$ is a largest condition of the nonempty preorder ${\dot{Q}}_{\alpha }$. Present $P_{\alpha +1}$ as the functions $p$ on $\alpha +1$ such that $p\upharpoonright \alpha \in P_{\alpha }$ and $p(\alpha )\in R_{\alpha }$ is forced by $p\upharpoonright \alpha$ to lie in ${\dot{Q}}_{\alpha }$. The map $p\mapsto (p\upharpoonright \alpha ,p(\alpha ))$ is the stipulated identification with $P_{\alpha }\ast {\dot{Q}}_{\alpha }$, and the all-top function is its largest condition. At a limit $\gamma$, a condition is a coherent function $p$ on $\gamma$ with each $p(\alpha )\in R_{\alpha }$ and $p\upharpoonright \alpha ⊩p(\alpha )\in {\dot{Q}}_{\alpha }$, whose support

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

is finite. The order is coordinatewise in the forcing sense: $p\le q$ iff for every $\alpha <\gamma$, $p\upharpoonright \alpha ⊩p(\alpha )\le q(\alpha )$. The supplied top names fill all coordinates outside the finite support. The limit carrier is a definable subset of the set of functions selecting from the set-indexed carriers $R_{\alpha }$; its all-top condition exists by Replacement, without Choice. From the weaker premise that each iterand merely has a forced largest condition, selecting these names uniformly is an additional operation and is not asserted here in ZF.