Solution (source code)

= Solution

Use <standard notation for forcing>: $q\leq p$ means that $q$ is stronger than $p$. A <closed forcing> order is $\lambda$-closed when every decreasing sequence $\langle p_\xi:\xi<\delta\rangle$ with $\delta<\lambda$ has a common lower bound:
$$
\boxed{\forall\delta<\lambda\ \forall\text{ decreasing }(p_\xi)_{\xi<\delta}\ \exists q\ \forall\xi<\delta\ (q\leq p_\xi).}
$$
The <chain condition for forcing> is
$$
\boxed{\text{every antichain in }\mathbb P\text{ has cardinality strictly below }\lambda.}
$$
An <antichain in a forcing order> consists of pairwise <incompatible forcing conditions>; incompatibility means having no common stronger extension. In particular, the $\aleph_1$-chain condition is the <countable chain condition for forcing>. These properties and their sequences or antichains are computed inside the ground model $M$.