Finite-Support Iterations and Martin's Axiom

From $K$ put $G=\{p:\mathrm{\exists }\dot{q}\in R(p,\dot{q})\in K\}$ and $H=\{{\dot{q}}_G:\mathrm{\exists }p\in G(p,\dot{q})\in K\}$. Preimages of ground dense subsets of $P$ are dense in the iteration, so $G$ is generic. If ${\dot{D}}_G$ is dense in ${\dot{Q}}_G$, the forcing theorem produces below each pair a name for a second-coordinate extension in $\dot{D}$; [F1] replaces that local name by a forced-equal name in the set carrier $R$. The resulting pairs are dense, and meeting them proves $H$ generic over $M[G]$.

Conversely, for generics $G,H$ take the filter generated by pairs $(p,\dot{q})$ in the restricted iteration with $p\in G$ and ${\dot{q}}_G\in H$. Every quotient condition has a name occurring in $\dot{Q}$, or a locally forced-equal representative in $R$ by [F1], so the same dense-set translation meets every ground dense subset of $P\ast \dot{Q}$. Recursive evaluation of names first by $G$ and then by $H$ proves $M[K]=M[G][H]$.

Suppose $A=\{(p_{\alpha },{\dot{q}}_{\alpha }):\alpha <{\omega }_1^M\}$ were an antichain and put $\dot{I}=\{(\check{\alpha },p_{\alpha }):\alpha <{\omega }_1^M\}$. We prove syntactically that $1_P$ forces the map $\alpha \mapsto {\dot{q}}_{\alpha }$ from $\dot{I}$ into $\dot{Q}$ to have pairwise incompatible, hence distinct, values. Otherwise some $s$ forces distinct $\alpha ,\beta \in \dot{I}$ and a common $\dot{Q}$-extension of their values. The forcing membership clause lets us strengthen below $p_{\alpha }$ and $p_{\beta }$; the existential clause of [F2] then supplies a further condition $t$ and a name $\dot{r}$ with $t⊩\dot{r}{\le }_{\dot{Q}}{\dot{q}}_{\alpha },{\dot{q}}_{\beta }$. By [F1], replace $\dot{r}$ below $t$ by a forced-equal $\rho \in R$. Then $(t,\rho )$ belongs to the restricted iteration and extends both members of $A$, a contradiction. Thus $1_P⊩\dot{I}$ injects into a $\dot{Q}$-antichain. Since $1_P⊩\dot{Q}$ is ccc, $1_P⊩\dot{I}$ is countable.

Induct on $\beta$. Top-padding preserves order. Given $p\in P_{\beta }$ and $r\le p\upharpoonright \alpha$, amalgamate $r$ with the tail of $p$: at each tail coordinate use the name selected by $p$, strengthening it only when the earlier amalgam requires a deciding extension. Successors use the two-step order; at limits the union has support contained in the union of two finite supports. Thus $p\upharpoonright \alpha$ is a reduction of $p$.

A reduction proves completeness: every maximal antichain of $P_{\alpha }$ remains predense after top-padding, and two padded conditions are compatible in $P_{\beta }$ exactly when they were compatible in $P_{\alpha }$. This assertion is restricted to padded conditions; two arbitrary long conditions may have compatible restrictions and incompatible tails.

The inverse image of any dense subset of $P_{\alpha }$ is predense in $P_{\beta }$, so a $P_{\beta }$-generic restricts to a $P_{\alpha }$-generic. Padded stages form the increasing chain. At a successor, F2 identifies the quotient over the restricted generic with $({\dot{Q}}_{\alpha }{)}_{G_{\alpha }}$.

First normalize any $p\in P_{\beta }$ without changing its forcing condition up to equivalence. At every $\xi \mathrm{\notin }\mathrm{supp}(p)$ replace $p(\xi )$ by the distinguished literal top name ${\dot{1}}_{\xi }$; retain $p(\xi )$ on its finite support. Induction on $\xi \le \beta$ shows that the original and normalized prefixes force each other below themselves. At an off-support coordinate the original prefix forces $p(\xi )={\dot{1}}_{\xi }$ by the definition of support, and forcing-equivalent prefixes preserve that assertion; at a support coordinate the names coincide. Consequently the normalized function is a valid condition with the same support and is equivalent to $p$ in both order directions. If its support lies below $\alpha <\beta$, it is literally the top-padding of its $P_{\alpha }$ restriction. Replacing members of an antichain by equivalent normalized conditions preserves incompatibility. This normalization uses the supplied top names of the finite-support definition, not a property claimed by F2.

Induct on $\beta$. The trivial initial stage is ccc and F1 gives every successor step. If $\mathrm{cf}(\beta )=\omega$, write $\beta ={\sup }_n{\beta }_n$. Normalize an alleged ${\omega }_1$-antichain by step 1.1. Every finite support is contained in some ${\beta }_n$, so one $n$ captures uncountably many normalized members. They are literal top-paddings of $P_{{\beta }_n}$-conditions. Induction makes two compatible in $P_{{\beta }_n}$, and F2 carries that compatibility to their paddings in $P_{\beta }$, contradicting the antichain.

At a limit of uncountable cofinality, normalize an alleged ${\omega }_1$-antichain by step 1.1. If one finite support occurs uncountably often, choose $\alpha <\beta$ above it; the corresponding normalized conditions are literal paddings from $P_{\alpha }$, contradicting induction and F2. Otherwise thin to uncountably many distinct supports and apply F3 to obtain a delta system with finite root $r$. Choose $\alpha <\beta$ above $r$. By induction two restrictions to $\alpha$ are compatible. Their support petals above $\alpha$ are disjoint. Let $s\in P_{\alpha }$ extend both restrictions and form the function whose prefix is $s$, whose coordinates above $\alpha$ on the two disjoint petals are those of the respective normalized conditions, and whose other coordinates are literal top names. At a tail coordinate belonging to one petal, the new prefix extends that condition's original prefix, so its forced iterand membership and order comparison persist by monotonicity; at coordinates of $s$, validity is already checked in $P_{\alpha }$. Hence this finite-support function is a valid condition extending both normalized conditions. The disjoint-tail amalgamation is proved from the iteration order; F2 is used only for the literal padded prefix. This contradicts the antichain, and equivalence transfers the contradiction to the original conditions. AC is used for thinning.

Work in the given extension $V[G]$. By F2 choose a ground cardinal $\nu <\mathrm{cf}(\delta )$ equal to $\mathrm{\mid }A\mathrm{\mid }$ there, and choose in $V[G]$ a surjection $f:\nu \twoheadrightarrow A$. The truth lemma gives a ground $P_{\delta }$-name $\dot{f}$ and $p\in G$ forcing that $\dot{f}:\check{\nu }\to \mathrm{Ord}$ and is onto a name $\dot{A}$ for $A$. Thus the antichains below are indexed by the ground ordinal $\nu$, not by the extension set $A$. For every $\xi <\nu$, choose in the ground model a maximal antichain below $p$ deciding $\dot{f}(\check{\xi })$ as some check ordinal. Each antichain is countable by ccc. There are fewer than $\mathrm{cf}(\delta )$ antichains, and every condition has finite support, so the union $S$ of all their supports, together with $\mathrm{supp}(p)$, has size below $\mathrm{cf}(\delta )$. AC supplies the simultaneous antichains and code.

By regularity of $\mathrm{cf}(\delta )$, $S$ is bounded by some $\alpha <\delta$. Normalize $p$ and every member $a$ of every chosen antichain: replace each coordinate outside its finite support by the distinguished literal top name. At such a coordinate the original prefix forces equality to top, so induction on coordinates makes the normalized condition forcing-equivalent to the original in both order directions and preserves every decision. The normalized support is still contained in $\alpha$; hence these conditions, unlike the raw ones, are literal top-paddings of their $P_{\alpha }$ restrictions. Replace each antichain by its normalized image, removing duplicates if needed. Equivalence preserves antichain maximality below normalized $p$ and the ordinal labels.

Each normalized antichain is predense below normalized $p\mathrm{\mid }\alpha$ in $P_{\alpha }$: a $P_{\alpha }$-extension of that prefix has a top-padding below normalized $p$; maximality supplies a compatible normalized antichain member, and F3 reflects compatibility between these padded conditions. For each $\xi <\nu$, label the resulting $P_{\alpha }$-antichain by the ground ordinal it forces for $\dot{f}(\check{\xi })$. These labelled antichains define an explicit $P_{\alpha }$-name ${\dot{f}}_{\alpha }$; this construction does not restrict the original $P_{\delta }$-name $\dot{f}$. Since normalized $p$ is equivalent to $p\in G$, it belongs to $G$, and $G_{\alpha }$ meets each predense antichain below its prefix. The corresponding padded antichain member lies in $G$ and forces the same value of $\dot{f}(\check{\xi })$, so ${\dot{f}}_{\alpha ,G_{\alpha }}=f_G$. Thus its range $A$ lies in $V[G_{\alpha }]$. F2 ensures that “fewer than $\mathrm{cf}(\delta )$” has not changed.

A structure or indexed family coded by a small set of ground ordinals is recovered by fixed decoding operations from that set, so it belongs to the same intermediate model. The coding qualification is essential: no assertion is made for arbitrary unbounded collections lacking such a code.

Inductively build a coded order $P_{\alpha }^{\ast }$ of size at most $\mu$ with a dense embedding into $P_{\alpha }$, coherent under restriction. At a successor, the forcing hypothesis and AC give a $P_{\alpha }$-name ${\dot{e}}_{\alpha }$ forced to be a surjection from $\check{\mu }$ onto ${\dot{Q}}_{\alpha }$ (allow repetitions). The local names ${\dot{e}}_{\alpha }(\check{\xi })$ need not belong to the prescribed second-name carrier $R_{\alpha }$. For every $\xi <\mu$, use the AC/maximal-antichain mixing clause of the two-step convention underlying F1 to choose ${\rho }_{\alpha \xi }\in R_{\alpha }$ with $1_{P_{\alpha }}⊩{\rho }_{\alpha \xi }={\dot{e}}_{\alpha }(\check{\xi })$. AC selects these representatives simultaneously; retain only these at most $\mu$ carrier names as coded second coordinates. Given a raw $(p,\dot{q})$, first strengthen its prefix to a coded condition and then choose a stronger coded prefix forcing $\dot{q}={\rho }_{\alpha \xi }$ for some ground $\xi <\mu$, using the forced surjectivity and density of ordinal decisions. The pair with second coordinate ${\rho }_{\alpha \xi }$ is then a legal restricted-iteration condition below the raw pair. The coded successor has at most $\mu \cdot \mu =\mu$ conditions by F3. No arbitrary value name is silently used as an $R_{\alpha }$-coordinate.

At a limit, every raw condition is forcing-equivalent to the one obtained by replacing each off-support coordinate by its distinguished literal top name: the original prefix forces equality to top there, and induction on coordinates preserves the iteration order in both directions. Its remaining support is finite. Strengthen those finitely many coordinates successively to the coded carrier representatives from step 1.1, and pad every other coordinate with the distinguished top names. A finite support is chosen from an ordinal of size at most $\mu$, and each coordinate from one of at most $\mu$ earlier codes; F3 bounds the set of finite coded tuples by $\mu$.

Successor evaluation and the limit union maps are dense embeddings, so the coded iteration is forcing-equivalent stage by stage and coherent under restriction. AC is used to choose the forced enumerations and dense-embedding representatives. Raw presentations may contain arbitrarily many forced-equal names, which is why only a dense presentation, not their literal size, is bounded.

Enumerate the dense family as $D_0,D_1,\dots$ (repetitions allowed, and for an empty family choose any $p_0$). Choose recursively $p_{n+1}\le p_n$ in $D_n$. The upward closure $G=\{q:\mathrm{\exists }n{p}_n\le q\}$ is directed and upward closed, and it meets each $D_n$. No chain condition was used. AC provides the enumeration and choices.

Under CH, $2^{{\mathrm{\aleph }}_0}={\mathrm{\aleph }}_1$. The only infinite cardinal strictly below the continuum is ${\mathrm{\aleph }}_0$, so the MA scheme of F1 is exactly the instance proved in step 1.1.

Adjoin a largest condition if necessary. Starting with it, recursively form increasing sets $Q_n\subseteq P$ of size at most $\kappa$. To obtain $Q_{n+1}$, include all of $Q_n$; for every $q\in Q_n$ and every original dense $D$ choose one $d(q,D)\le q$ in $D$; and for every pair $q,r\in Q_n$ compatible in $P$, choose one common extension $s(q,r)\le q,r$. Put all these witnesses together with $Q_n$ into $Q_{n+1}$. AC supplies the simultaneous choices, and cardinal absorption preserves the size bound. Let $Q={\bigcup }_n{Q}_n$.

Every $D\cap Q$ is dense in $Q$ by the first closure requirement. Compatibility between members of $Q$ is reflected in $Q$ by the second: once both occur at some $Q_n$, their chosen common extension lies in $Q_{n+1}$. Hence every antichain of $Q$ is an antichain of the ccc order $P$, so $Q$ is ccc. A filter on $Q$ meeting the intersections generates an upward-closed directed filter in $P$ meeting every original $D$. Therefore the small-order restriction implies full $\mathrm{M}\mathrm{A}(\kappa )$; the converse is immediate.

Since $\mathrm{\mid }Q\mathrm{\mid }\le \kappa$, choose an injection $Q\hookrightarrow \kappa$ and transport the order to its image. The unused points of $\kappa$ are not forcing conditions; no duplicate largest elements are needed. This gives the fixed-domain coding used in bookkeeping without changing filters or ccc.

F1 makes $P_{{\omega }_2}$ ccc, and F2 preserves ${\omega }_1,{\omega }_2$. F3 and GCH give at most ${\mathrm{\aleph }}_2^{{\mathrm{\aleph }}_0}={\mathrm{\aleph }}_2$ real names. At every selected Cohen stage, the coordinate-domain dense sets make the union a total real, and for each real in the preceding intermediate model the dense set requiring disagreement at a fresh coordinate makes the new real different from it. Hence Cohen reals added at distinct selected stages are distinct. There are cofinally, thus ${\mathrm{\aleph }}_2$, many such stages, giving the reverse inequality. Therefore the final continuum is ${\mathrm{\aleph }}_2$.

In the final extension fix $\kappa <{\mathrm{\aleph }}_2$, a ccc order $Q$, and at most $\kappa$ dense subsets. By F5 replace $Q$ by a coded dense order of size at most $\kappa$, and code it and the family by a set of ground ordinals of size at most ${\mathrm{\aleph }}_1$. F4 places that code in some intermediate $V[G_{\alpha }]$.

The earlier model sees $Q$ as ccc: otherwise it contains an ${\omega }_1$-antichain, and the ccc tail preserves both that set and its incompatibility, contradicting final ccc. Bookkeeping therefore selects the name at a later stage $\beta$. Its coordinate generic is a filter on $Q$ meeting every dense set already coded at stage $\alpha$, hence the original family. Since $\kappa <{\mathrm{\aleph }}_2$ was arbitrary, MA holds.

step 1.1 gives $2^{{\mathrm{\aleph }}_0}={\mathrm{\aleph }}_2>{\mathrm{\aleph }}_1$, so CH fails. AC is used in coding, bookkeeping, cardinal arithmetic, and the preservation/name arguments.

Fix the actual ZFC axiom and MA instances in $\mathrm{\Delta }$. Expand the finite-support iteration proof F3 for those formulas. Its ccc induction, size and bounded-stage capture calculations, bookkeeping argument, and Cohen-coordinate argument use only finitely many ZFC schema instances and the GCH cardinal arithmetic needed at the relevant cardinals. Collect these in a finite source support. The iteration and its forcing relation are set definitions in that support; AC is used in the ccc, cardinal and bookkeeping choices.

Apply F1 to the fixed GCH part of that support. Add its finitely many $L$-relativized certificates and the source instances required to construct the $L$ model. Enlarge the resulting finite $\mathrm{\Gamma }$ to cover the forcing theorem and the finite target formulas. F2 gives a countable transitive source model of $\mathrm{\Gamma }$; its constructible inner model has the particular source GCH instances, and the generic iteration over that model satisfies each member of $\mathrm{\Delta }$ by F3. These are ZFC-formalizable fixed-fragment steps, so ZFC proves the existence of the resulting set model of $\mathrm{\Delta }$.

The argument chooses a finite proof separately for the actual $\mathrm{\Delta }$. A semantic schedule for all MA instances does not by itself verify a numerical proof constructor or its PA checker invariant.

A contradiction proof in $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{M}\mathrm{A}+\mathrm{\neg }\mathrm{C}\mathrm{H}$ uses some finite set $\mathrm{\Delta }$ of target axioms, including finitely many MA instances. Apply F1 to that particular $\mathrm{\Delta }$. ZFC proves that a model of $\mathrm{\Delta }$ exists, while the alleged contradiction proof and finite-model soundness give a ZFC proof that no such model exists. Thus a target inconsistency would imply a ZFC inconsistency.

Contraposition yields the displayed external relative-consistency implication. No assertion about PA verification of the fragment-selection map is needed.

Fix an explicit bijection $e:2^{<\omega }\to \omega$. For each branch $x\in 2^{\omega }$, put $A_x=\{e(x\upharpoonright n):n\in \omega \}$. This set is infinite because distinct lengths give distinct nodes.

If $x\mathrm{\ne }y$, let $m$ be their first differing coordinate. Then $x\upharpoonright n\mathrm{\ne }y\upharpoonright n$ for every $n>m$, so $A_x\cap A_y$ is contained in the finite set of codes of their common initial segments. Also $A_x=A_y$ would force equality of every initial segment, so $x\mapsto A_x$ is injective. The family therefore has size $\mathrm{\mid }{2}^{\omega }\mathrm{\mid }=2^{{\mathrm{\aleph }}_0}$. The construction makes no arbitrary choice after $e$ is fixed.

Fix $X\subseteq \kappa$. Let $P_X$ consist of pairs $(s,F)$ with $s$ a finite partial map $\omega \to 2$ and $F\subseteq \kappa \setminus X$ finite. Put $(t,H)\le (s,F)$ iff $s\subseteq t$, $F\subseteq H$, and $t^{-1}(1)\cap (\mathrm{dom}(t)\setminus \mathrm{dom}(s))\text{is disjoint from}{\bigcup }_{\alpha \in F}{A}_{\alpha }\mathrm{.}$ This is transitive: an extension never puts a new $1$ on any set already protected by the weaker condition. Conditions with the same stem $s$ are compatible, since $(s,F\cup H)$ extends both. There are only countably many finite stems, so $P_X$ is $\sigma$-centered and hence ccc.

For $\alpha \mathrm{\notin }X$, let $E_{\alpha }=\{(s,F):\alpha \in F\};$ this is dense because adjoining $\alpha$ to $F$ changes no stem. For $\alpha \in X$ and $n<\omega$, let $D_{\alpha ,n}=\{(s,F):(\mathrm{\exists }m>n)[m\in A_{\alpha }\cap \mathrm{dom}(s)\text{ and }s(m)=1]\}\mathrm{.}$ Given $(s,F)$, the set $A_{\alpha }\cap {\bigcup }_{\beta \in F}{A}_{\beta }$ is finite by almost disjointness. Since $A_{\alpha }$ is infinite, choose $m>n$ outside that finite set and $\mathrm{dom}(s)$; setting $s(m)=1$ gives an extension in $D_{\alpha ,n}$. Thus all these sets are dense. Their number is at most $\kappa \cdot {\mathrm{\aleph }}_0=\kappa$, so MA supplies a filter $G$ meeting them. Let $r_X=\{m:(\mathrm{\exists }(s,F)\in G)s(m)=1\}\mathrm{.}$ Directedness makes the stems in $G$ consistent. If $\alpha \in X$, meeting every $D_{\alpha ,n}$ makes $r_X\cap A_{\alpha }$ infinite. If $\alpha \mathrm{\notin }X$, choose $(s,F)\in G\cap E_{\alpha }$. For any $(t,H)\in G$, take $(u,K)\in G$ below both. Since $(u,K)\le (s,F)$ and $\alpha \in F$, no new $1$ of $u$ beyond $s$ lies in $A_{\alpha }$; hence $t^{-1}(1)\cap A_{\alpha }\subseteq s^{-1}(1)$. Consequently $r_X\cap A_{\alpha }\subseteq s^{-1}(1)$ is finite. Therefore $X=\{\alpha :\mathrm{\mid }{r}_X\cap A_{\alpha }\mathrm{\mid }={\mathrm{\aleph }}_0\}$.

Choosing the least real in a fixed well-order among the codes for each $X$ gives an injection $\mathcal{P}(\kappa )\hookrightarrow \mathcal{P}(\omega )$; AC is used here. Monotonicity gives $\mathfrak{c}\le 2^{\kappa }$, hence equality. If $\mathrm{cf}(\mathfrak{c})=\lambda <\mathfrak{c}$, then $\mathfrak{c}\le {\mathfrak{c}}^{\lambda }=(2^{\lambda }{)}^{\lambda }=2^{\lambda }=\mathfrak{c}$, while König gives ${\mathfrak{c}}^{\lambda }>\mathfrak{c}$, contradiction. Therefore $\mathfrak{c}$ is regular.

By AC choose increasing closed nowhere-dense covers $M_{\alpha }\subseteq {\bigcup }_n{F}_{\alpha n}$. Fix a countable base $(B_j)$ of rational intervals. A condition is $(m,F,w)$, where $m<\omega$, $F\subseteq \kappa$ is finite, and $w(n,j)$ for $n,j<m$ is a nonempty rational interval with closure inside $B_j$. A condition $(m^{\mathrm{\prime }},F^{\mathrm{\prime }},w^{\mathrm{\prime }})$ extends $(m,F,w)$ when $m^{\mathrm{\prime }}\ge m$, $F^{\mathrm{\prime }}\supseteq F$, it preserves old $w$, and every newly assigned cell $(n,j)\in [0,m^{\mathrm{\prime }}{)}^2\setminus [0,m{)}^2$ has closure disjoint from $F_{\alpha n}$ for all $\alpha \in F$, the old side set. This includes the new columns of old rows. The relation is transitive: cells added at the first extension avoid the original side set, and cells added later avoid the larger intermediate side set. Finite unions of closed nowhere-dense sets leave the required subintervals in every $B_j$.

Conditions with the same $m,w$ are compatible: take the union of their finite side sets without adding a new row. There are only countably many finite rational arrays $w$, so the order is ccc. For each $\alpha$, the set requiring $\alpha \in F$ is dense. For every $r$, the set requiring $m>r$ is dense by filling the finitely many new cells inside the complements prescribed in step 1.1. These are only $\kappa +{\mathrm{\aleph }}_0<\mathfrak{c}$ requirements, so MA supplies a filter $G$.

Coherence of the filter defines $I_{nj}=w(n,j)$ for every $n,j$. Put $V_n={\bigcup }_j{I}_{nj}$ and $W_r={\bigcup }_{n\ge r}{V}_n$. Each $V_n$, hence each $W_r$, is open dense because $I_{nj}\subseteq B_j$ exists for every basic interval. Fix $\alpha$ and a filter condition that first has $\alpha$ in its side set at length $m$. For every $n\ge m$ and every $j$, the cell $(n,j)$ is assigned only in an extension of that condition and its closure avoids $F_{\alpha n}$ by step 1.1, even if it is a new column of an earlier row. Thus $V_n\cap F_{\alpha n}=\mathrm{\varnothing }$. If $x\in M_{\alpha }$, choose $k$ with $x\in F_{\alpha k}$; since the cover is increasing, $x\mathrm{\notin }{V}_n$ for all $n\ge \max (m,k)$. Thus $x\mathrm{\notin }{W}_{\max (m,k)}$ and $x\mathrm{\notin }{\bigcap }_r{W}_r$. Therefore the union of the $M_{\alpha }$ is covered by the meagre set ${\bigcup }_r(\mathbb{R}\setminus W_r)$. Singletons are nowhere dense, proving the final clause. The simultaneous cover choice is the exact AC use; the defective published sigma-ideal proposition is not used.

Let $P_{\epsilon }$ be the set of open subsets $U$ of $\mathbb{R}$ with $m(U)<\epsilon$, ordered by reverse inclusion: $U\le V$ means $U\supseteq V$, so a larger open set is a stronger condition in the convention of [F3]. For every $\alpha$, the subcollection $D_{\alpha }=\{U:N_{\alpha }\subseteq U\}$ is dense: given $U$, choose by F1 an open cover $O$ of the null set $N_{\alpha }\setminus U$ with $m(O)<\epsilon -m(U)$; then $U\cup O\le U$ lies in $D_{\alpha }$.

The order is ccc. Enumerate the rational open intervals whose closures lie in a condition $U$; their union is $U$. The increasing finite unions $W_j\subseteq U$ therefore have union $U$, so F2 supplies some finite rational-interval union $W=W_j$ with $m(U\setminus W)<(\epsilon -m(U))\mathrm{/}2$. If two conditions $U,V$ share this $W$, then, labelling so that $m(U)\le m(V)$, $m(U\cup V)\le m(W)+m(U\setminus W)+m(V\setminus W)<m(U)+\frac{\epsilon -m(U)}{2}+\frac{\epsilon -m(U)}{2}=\epsilon ,$ so $U\cup V$ is a condition below both in the declared reverse-inclusion order. Only countably many sets $W$ occur, so no antichain of conditions is uncountable.

MA gives a filter meeting all $D_{\alpha }$. Its union $U$ covers every $N_{\alpha }$. Directedness toward stronger conditions in the reverse-inclusion order makes every finite subunion of filter members a subset of one stronger member, so it has measure below $\epsilon$. The rational base gives a countable cofinal subfamily for the union, so continuity from below yields $m(U)\le \epsilon$. Repeating for $\epsilon =2^{-n}$ proves the total union has outer measure zero, and completeness gives nullity.

A singleton has measure zero. Applying the first clause to the family of singletons indexed by any set of reals of size below $\mathfrak{c}$ gives the second. AC was used to enumerate/cardinalize the family and choose all covers and approximations.

To prove the Knaster consequence, let $\{p_{\alpha }:\alpha <{\omega }_1\}$ lie in a ccc order. Some $p_{\ast }$ has the property that every extension of $p_{\ast }$ is compatible with uncountably many $p_{\alpha }$. Otherwise, for each $\alpha$ choose $q_{\alpha }\le p_{\alpha }$ compatible with only countably many of the $p_{\beta }$, and choose a bound $b_{\alpha }<{\omega }_1$ above all their indices. Recursively select ${\alpha }_{\xi }$ above every earlier $b_{{\alpha }_{\eta }}$. Then for $\eta <\xi$, $q_{{\alpha }_{\eta }}$ is incompatible with $p_{{\alpha }_{\xi }}$ and hence with $q_{{\alpha }_{\xi }}$, producing an uncountable antichain, contrary to ccc. Below $p_{\ast }$, each $D_{\xi }=\{q:\mathrm{\exists }\alpha \ge \xi ,q\le p_{\alpha }\}$ is dense open. Let an MA filter meet all $D_{\xi }$. For each $\xi$, select $q_{\xi }$ in the filter and ${\alpha }_{\xi }\ge \xi$ with $q_{\xi }\le p_{{\alpha }_{\xi }}$. The indices ${\alpha }_{\xi }$ are unbounded, hence yield uncountably many distinct $p_{{\alpha }_{\xi }}$; any two are compatible because directedness gives a common extension of their corresponding $q_{\xi }$. Thus the order is Knaster.

Given uncountably many nonempty rectangles $U_{\alpha }\times V_{\alpha }$ in $X\times Y$, order the nonempty open subsets of $X$ by reverse inclusion. step 1.1 thins the $U_{\alpha }$ to an uncountable pairwise-intersecting family. Since $Y$ is ccc, two corresponding $V_{\alpha },V_{\beta }$ intersect; the two rectangles then intersect. Thus binary, and by induction every finite, product is ccc.

In an arbitrary product, refine an alleged uncountable disjoint family to basic opens with finite supports. If one support occurs uncountably often, those opens project to an uncountable family in its finite ccc product; two projections intersect, and the corresponding basic opens intersect. Otherwise thin to ${\omega }_1$ opens with pairwise distinct finite supports, as required by F3, and apply F3 to obtain a delta system with finite root $r$. Their root projections form an uncountable family in the finite product over $r$, which is ccc by step 2.1, so two root projections intersect. Outside $r$ their supports are disjoint; choose points in their finitely many constrained coordinates and use an AC-chosen base point in every remaining nonempty factor to obtain a point in both basic opens, contradiction. AC supplies that base point as well as the refinements and thinning. If a factor is empty, the whole product is empty and hence ccc.