= Solution
Inside $M$, the finite-function order has the <countable chain condition for finite-function forcing>. In an uncountable family of binary conditions there are uncountably many distinct finite domains, since each domain supports only finitely many conditions. These domains would have an uncountable <Delta-system> subfamily by the <Delta-system lemma>. There are only finitely many assignments to the common finite root, so thin further to an uncountable family agreeing there. Any two such conditions have a union that is again a function and is a common stronger extension. Thus no uncountable <antichain in a forcing order> exists.
Here is the relevant preservation argument, rather than an appeal to the condition alone. Fix $p\in G$ forcing that a <forcing name> $\dot h$ is a function $\omega\to\alpha_1$. For each $n$, choose inside $M$ a maximal <antichain in a forcing order> below $p$ deciding $\dot h(n)$. By the <countable chain condition for forcing>, this antichain is countable in $M$, so the possible values form a countable $B_n\subseteq\alpha_1$. The union $B=\bigcup_nB_n$ is countable in $M$, hence bounded below its regular $\omega_1=\alpha_1$. The interpreted $h$ has range contained in $B$, by maximality and the <dense-below generic meeting lemma>. It therefore cannot be a surjection onto $\alpha_1$.
If $\alpha_1$ were not a <cardinal number> in $M[G]$, it would be equinumerous with a smaller ordinal, which was countable already in $M$; composing with that ground-model enumeration would give a surjection $\omega\to\alpha_1$. This is impossible. Therefore
$$
\boxed{M[G]\models\text{“}\alpha_1\text{ is a cardinal”}}.
$$
This is the <possible-values lemma for chain-condition forcing> specialized to $\omega_1$. Countability and regularity in this proof are computed inside $M$, not inferred from the external countability of $M$.
Back to article page
