The omega_2 bookkeeping iteration for MA

Assume ground-model GCH. At each stage choose, as part of the recursion, a coherent dense coded suborder $D_{\alpha }\subseteq P_{\alpha }$ of size at most ${\mathrm{\aleph }}_2$ using Size bound for finite-support ccc iterations. Fix a well-order of $H({\mathrm{\aleph }}_3)$ and a bookkeeping map on ${\omega }_2$ that repeats every relevant canonical nice code over an earlier $D_{\alpha }$ cofinally often. The ${\omega }_2$ MA iteration is the finite-support iteration $⟨P_{\alpha },{\dot{Q}}_{\alpha },{\dot{1}}_{\alpha }:\alpha <{\omega }_2⟩$ in which bookkeeping selects a coded candidate name for an order on a subset of ${\mathrm{\aleph }}_1$. Choose a maximal antichain deciding whether that candidate is a ccc order of the required size. On each positive branch, use its top-adjoined version as in Martin's Axiom reduces to small ccc orders; on each negative branch, use the one-point order. Mix those branch names into the single name ${\dot{Q}}_{\alpha }$, including a branchwise name ${\dot{t}}_{\alpha }$ for its largest condition. Thus $P_{\alpha }$ forces that the iterand is nonempty, ccc, and has ${\dot{t}}_{\alpha }$ as a largest condition. A candidate already forced ccc is used, with its adjoined top, on every branch. Cohen forcing, with a top adjoined, is selected at cofinally many stages.

The local mixed top name ${\dot{t}}_{\alpha }$ need not lie in the prescribed set-sized carrier $R_{\alpha }$. Apply the AC/maximal-antichain mixing clause of Two-step forcing iterations at $1_{P_{\alpha }}$ to choose ${\dot{1}}_{\alpha }\in R_{\alpha }$ forced equal to ${\dot{t}}_{\alpha }$. Recursively choose these representatives as part of the set-indexed stage data, so the all-top condition and literal top padding required by Finite-support forcing iterations are defined at every stage.

The bookkeeping enumerates canonical codes, not arbitrary raw $P_{\alpha }$-names. Given a name which a condition forces to be a ccc order of size at most ${\mathrm{\aleph }}_1$, first use ambient AC to name an isomorphic presentation on a subset of ${\mathrm{\aleph }}_1$. Encode its domain and order relation as a subset of the fixed ground set ${\mathrm{\aleph }}_1\times {\mathrm{\aleph }}_1$. Below a coded $D_{\alpha }$-condition, apply Nice-name reduction and the ccc counting bound using countable deciding antichains from the dense ccc suborder $D_{\alpha }$; this gives an equivalent nice code over $D_{\alpha }$. By GCH there are at most $({\mathrm{\aleph }}_2^{{\mathrm{\aleph }}_0}{)}^{{\mathrm{\aleph }}_1}={\mathrm{\aleph }}_2$ such codes at each stage. The coherent coding and schedule revisit each earlier canonical code later, while the raw presentation may have unboundedly many forced-equal names. AC chooses the master well-order, deciding antichains, carrier representatives, and scheduling map. The branch mixture makes “${\dot{Q}}_{\alpha }$ is ccc” forced by $P_{\alpha }$ rather than merely decided by some conditions; it never discards a positive branch merely because the top condition did not decide it.