Cohen forcing two-level continuum plateau (source code)

= Cohen forcing two-level continuum plateau
{c}
{title2=$2^{\aleph_0}=2^{\aleph_1}=\aleph_3$}

Over a model of <Generalized continuum hypothesis>, add $\aleph_3$ Cohen reals with finite binary <partial functions>. The <Delta-system lemma> proves the <countable chain condition for forcing>. The generic reals give the continuum lower bound $\aleph_3$, while nice <forcing names> for <subsets> of $\omega_1$ number at most $(\aleph_3)^{\aleph_1}=\aleph_3$ in the ground model. <Cardinal> preservation then gives $2^{\aleph_0}=2^{\aleph_1}=\aleph_3$.