Worked solution: Shelah's proof that the Whitehead problem is independent of ZFC (1974)

Assume Martin's Axiom together with $2^{\aleph_0} > \aleph_1$. Using an almost-disjoint family $\{ a_\xi : \xi < \aleph_1 \}$ of infinite subsets of $\omega$ (pairwise intersections finite), one builds a specific abelian group $W$ of cardinality $\aleph_1$, generated by symbols tied to each $a_\xi$ together with a countable free part, glued so that $W$ is $\aleph_1$-free but its filtration cannot be arranged into the well-behaved, club-supported form Pontryagin's criterion demands — so $W$ is provably not free.

Showing $\mathrm{Ext}^1(W, \mathbb{Z}) = 0$ nonetheless requires solving $\aleph_1$-many compatible local lifting problems (one at each stage of the filtration) simultaneously; Shelah showed this reduces to finding a filter meeting $\aleph_1$-many dense subsets of a naturally associated ccc poset, which is exactly what $\mathrm{MA}_{\aleph_1}$ (available since $2^{\aleph_0} > \aleph_1$) guarantees. So under $\mathrm{MA} + \neg\mathrm{CH}$, $W$ is a genuine non-free Whitehead group of cardinality $\aleph_1$.

Since $\mathrm{MA} + \neg\mathrm{CH}$ is itself consistent relative to $\mathrm{ZFC}$ (by Solovay–Tennenbaum's iterated forcing, described in the companion proof of Suslin's problem), this shows $\mathrm{Con}(\mathrm{ZFC}) \implies \mathrm{Con}(\mathrm{ZFC} + \neg\mathrm{Free}(\mathrm{Wh}))$, where $\neg\mathrm{Free}(\mathrm{Wh})$ abbreviates "some Whitehead group is not free" — the second half of the independence result.