Worked solution: Independence of Suslin's Hypothesis from ZFC (Jensen, Solovay–Tennenbaum, 1971)

Step 8 of 8: Coda: iterated forcing becomes a general-purpose method

In plain words

Solovay and Tennenbaum's finite-support technique only works smoothly when every step of the iteration is ccc. When set theorists later wanted to iterate a broader class of forcings, called "proper" forcings (needed for many other independence results), the finite-support recipe stopped working reliably.

Saharon Shelah, building directly on the Solovay–Tennenbaum blueprint, invented countable-support iteration in the late 1970s and 1980s to handle this broader class, and used it to prove the Proper Forcing Axiom ( $\mathrm{PFA}$ ) — a much stronger cousin of Martin's Axiom — is consistent and, among many other consequences, also implies $\mathrm{SH}$ .

\mathrm{PFA} \implies \mathrm{SH} \quad \text{(Shelah's proper forcing, countable-support iteration)}

Detailed analysis

The Proper Forcing Axiom ( $\mathrm{PFA}$ ) strengthens $\mathrm{MA}$ by allowing the poset $\mathbb{P}$ to range over all proper forcings (a class including ccc forcings but much larger, defined by a preservation property for stationary sets rather than by the ccc condition itself), while still guaranteeing filters meeting $\aleph_1$ -many dense sets. Shelah's countable-support iteration is the technology that makes forcing with $\aleph_2$ -many proper forcings in sequence possible while still preserving $\aleph_1$ , generalizing the role finite-support ccc iteration played for Solovay and Tennenbaum.

$\mathrm{PFA}$ implies $\mathrm{SH}$ (since it implies $\mathrm{MA} + \neg\mathrm{CH}$ , in fact it forces $2^{\aleph_0} = \aleph_2$ outright), giving yet another route to the consistency of $\mathrm{SH}$ , alongside a vast array of other combinatorial consequences that make $\mathrm{PFA}$ one of the most powerful and widely used extra axioms in modern set theory.

Suslin's problem's independence, and the iterated forcing machinery invented to prove it, seeded an entire research program: similar techniques (and similarly "ordinary"-looking independent statements) soon appeared outside set theory itself, most famously in abstract algebra with the Whitehead problem in abelian group theory, which the companion proof preset in this library covers.

Terms in this step

Proper Forcing Axiom (PFA): A strengthening of Martin's Axiom to the much broader class of "proper" forcings; it has an especially rich set of combinatorial consequences and is one of the most studied extra axioms of set theory beyond $\mathrm{ZFC}$ .