= Solution
\b[Closure preserves the ground-model cardinal $\lambda$.] We use the stronger fact that <closed forcing adds no short ordinal sequences>. Fix an ordinal $\mu<\lambda$ in $M$ and a <forcing name> $\dot h$ that a condition $p$ forces to be an ordinal-valued function with domain $\mu$.
Inside $M$, recursively strengthen $p$ to decide each value $\dot h(\xi)$, for $\xi<\mu$. At a limit stage take a lower bound of the previously chosen descending sequence; its length is below $\lambda$, so $\lambda$-closure supplies one. After all $\mu$ values have been decided, closure supplies a common lower bound $q$. The decided values form a function $h\in M$ by the <Axiom schema of replacement>, and
$$
q\Vdash\dot h=\check h.
$$
The recursion is carried out within $M$ using the definable <forcing theorem> and a ground-model choice of deciding extensions, so every sequence to which closure is applied belongs to $M$. Repeating the construction below any stronger condition shows that such full-decision conditions are <dense below a forcing condition> $p$. The <dense-below generic meeting lemma> ensures that a <generic filter> containing $p$ meets them. Thus the interpreted function is in $M$.
If $\lambda$ ceased to be a <cardinal number> in $M[G]$, there would be a surjection $\mu\to\lambda$ for some ordinal $\mu<\lambda$. The <forcing theorem> gives a name and a condition in $G$ forcing this. The argument above makes its interpretation a ground-model function, but $M$ regards $\lambda$ as a <cardinal number> and admits no such surjection. Therefore
$$
\boxed{M[G]\models\text{“}\lambda\text{ is a cardinal”}}.
$$
No regularity of $\lambda$ is required; every recursion used has length strictly below $\lambda$. Finite cardinals are preserved automatically. This is <cardinal preservation by closed forcing>.
Back to article page
