Set-length Easton-support forcing iterations

A set-length Easton-support iteration of length $\delta$ follows the successor rule of an ordinary forcing iteration and replaces the finite support of Finite-support forcing iterations at limit stages by Easton support. Precisely, it is the transfinite recursion (Transfinite recursion) over an ordinal $\delta$ of set-indexed data $⟨P_{\alpha },{\dot{Q}}_{\alpha },{\dot{1}}_{\alpha }:\alpha <\delta ⟩$. For each $\alpha$, let $R_{\alpha }$ be the set-sized second-name carrier specified in Finite-support forcing iterations, and require a supplied ${\dot{1}}_{\alpha }\in R_{\alpha }$ with $1_{P_{\alpha }}⊩{\dot{1}}_{\alpha }$ a largest condition of the nonempty preorder ${\dot{Q}}_{\alpha }$. The recursion satisfies:

• $P_0$ is the trivial order, and $P_{\alpha +1}=P_{\alpha }\ast {\dot{Q}}_{\alpha }$ is the two-step iteration of Finite-support forcing iterations, with the same carrier and the same coordinatewise order;
• at a limit $\gamma \le \delta$, a condition is a coherent function $p$ on $\gamma$ with $p\upharpoonright \alpha \in P_{\alpha }$, $p(\alpha )\in R_{\alpha }$, and $p\upharpoonright \alpha ⊩p(\alpha )\in {\dot{Q}}_{\alpha }$ for every $\alpha <\gamma$, whose non-top support $\{\alpha <\gamma :p\upharpoonright \alpha ⊮p(\alpha )={\dot{1}}_{\alpha }\}$ meets $[0,{\gamma }^{\mathrm{\prime }})$ in fewer than ${\gamma }^{\mathrm{\prime }}$ elements for every infinite regular ${\gamma }^{\mathrm{\prime }}\le \gamma$ (Cofinality $\mathrm{cf}(\alpha )$, and regular and singular cardinals).

The order is coordinatewise in the forcing sense, as in the finite-support iteration. At $\gamma =\delta$ the resulting order has a largest condition, the all-top function supplied by the distinguished top names. Each initial segment $P_{\alpha }$, including the final $P_{\delta }$, is a set: at a limit it is a definable subset of the set of functions with values in the supplied carriers $R_{\alpha }$. The top names are part of the data, so no uniform selection of names is inferred from mere existence of forced largest conditions.

This is a different presentation from the ground-model Easton product The Easton-support product of higher Cohen forcings: the iteration's $P_{\gamma }$-levels are built by recursion inside the ground model and need not be isomorphic to any $P(F)$, and no such equivalence is asserted here. The product presentation carries the cardinal-preservation and continuum computations of this page; the iteration is recorded because the Easton support condition (15.9) of the source is stated for products of fibres and because a set-length iteration is the natural setting in which the same support bound is imposed at limit stages.