Finite-support bookkeeping kills all named Suslin trees

By [F1] every iterand is forced ccc, so [F2] makes $P_{{\omega }_2}$ ccc. Hence [F4] preserves ${\omega }_1^M$ and ${\omega }_2^M$, while [F6] gives ${\mathrm{cf}}^M({\omega }_2)={\omega }_2$. Every intermediate and final extension satisfies ZFC by [F14].

Suppose toward a contradiction that $T\in M[G]$ is Suslin. Every level $T_{\alpha }$ is nonempty: height ${\omega }_1$ supplies a node above $\alpha$, whose predecessor well-order contains a node of height $\alpha$. By AC choose $t_{\alpha }\in T_{\alpha }$ and an injection $e_{\alpha }:T_{\alpha }\to \omega$ for every $\alpha <{\omega }_1$. Then $\alpha \mapsto t_{\alpha }$ injects ${\omega }_1$ into $T$, while $t\mapsto (\mathrm{ht}(t),e_{\mathrm{ht}(t)}(t))$ injects $T$ into ${\omega }_1\times \omega$. By [F7] and [F8], fix a bijection $b:{\omega }_1\to T$. Transport the tree order to a relation $R$ on ${\omega }_1$. Fixing a bijection $\pi :{\omega }_1\times {\omega }_1\to {\omega }_1$ from [F7], the set $C=\{\pi (\xi ,\eta ):\xi R\eta \}\subseteq {\omega }_1$ codes the isomorphic tree $T^{\ast }=({\omega }_1,R)$.

The code $C$ has size at most ${\mathrm{\aleph }}_1<\mathrm{cf}({\omega }_2)$ by steps 1.1-1.2. Since its members are ground ordinals, [F3] gives $\alpha <{\omega }_2$ with $C,T^{\ast }\in M[G_{\alpha }]$. The tree $T^{\ast }$ is already Suslin there. Its tree laws, height and absence of a cofinal branch follow downward from the final model because its carrier, relation and ordinals are unchanged. If the earlier model had an uncountable level or antichain $A$, AC there would give an injection ${\omega }_1\to A$; in the final model the corresponding level or antichain is countable by the assumed Suslinity, so composition would make ${\omega }_1$ countable, contrary to step 1.1. Thus levels were countable and no uncountable antichain existed at stage $\alpha$. The same argument applies at every later intermediate stage as long as the final model is assumed to see $T^{\ast }$ as Suslin.

In $M[G_{\alpha }]$ form the finite-specialization order $P(T^{\ast })$. It is ccc by [F11]. Its conditions are finite functions from ${\omega }_1$ to $\omega$; increasing enumeration of a finite graph codes it by a finite sequence from ${\omega }_1\times \omega$, and the union over finite lengths has size at most ${\mathrm{\aleph }}_1$ by repeated absorption in [F7]. Take a ground $P_{\alpha }$-name for this order. The truth lemma in [F15] supplies a condition on the actual generic branch forcing that it is ccc of size at most ${\mathrm{\aleph }}_1$; the canonical-code clause of [F1] turns it into a scheduled nice code. Because every code is revisited cofinally, choose a scheduled stage $\beta >\alpha$. Step 2.1 ensures that on the maximal-antichain branch met by $G_{\beta }$, the evaluated coordinate iterand is an isomorphic top-adjoined presentation of $P(T^{\ast })$, not the one-point negative branch.

By [F9], $G_{\beta +1}$ factors over $M[G_{\beta }]$ through a generic for that evaluated coordinate iterand. The isomorphism from its positive presentation to a top-adjoined $P(T^{\ast })$ is onto, and the inclusion of $P(T^{\ast })$ below the new top is a dense order embedding: the new top has every old condition below it. Therefore [F10] identifies its generic extension with a $P(T^{\ast })$-generic extension. Since $T^{\ast }$ is Suslin in $M[G_{\beta }]$ by step 2.1, [F11] supplies there a total function $f:T^{\ast }\to \omega$ separating every comparable distinct pair. This function and those pointwise inequalities persist to $M[G]$.

In the final model each fiber $A_n=f^{-1}(\{n\})$ is an antichain of the assumed Suslin tree $T^{\ast }$, hence is countable by [F5]. Their countable union is all of the carrier ${\omega }_1$, so [F12] would make ${\omega }_1$ countable, contradicting step 1.1. This includes the fiber $n=0$ and does not presume that any fiber is nonempty. Thus the alleged final Suslin tree cannot exist.

The tree $T$ was arbitrary, so $M[G]$ has no Suslin tree; [F13] yields SH under the strong line convention. The argument applies to every supplied $M$-generic. If generics through all conditions are externally available, [F15] converts that universal generic-extension conclusion into $1_{P_{{\omega }_2}}{⊩}_M\mathrm{S}\mathrm{H}$. Without that extra availability, the internal forcing predicate still exists but this semantic equivalence is not asserted.