力迫的 ctm 方法的形式验证

我们讨论了对如下构造的计算机验证证明中的一些要点：给定 $\mathit{ZFC}$ 的可数传递集模型 $M$，构造满足 $\mathit{ZFC}+\neg\mathit{CH}$ 与 $\mathit{ZFC}+\mathit{CH}$ 的泛型扩张。此外，令 $\mathcal{R}$ 为替换公理的实例之集合。我们分离出一个 21 元子集 $\Omega\subseteq\mathcal{R}$ 并定义 $\mathcal{F}:\mathcal{R}\to\mathcal{R}$，使得对每个 $\Phi\subseteq\mathcal{R}$ 与 $M$-泛型 $G$，由 $M\models \mathit{ZC} \cup \mathcal{F}\text{``}\Phi \cup \Omega$ 可推出 $M[G]\models \mathit{ZC} \cup \Phi \cup \{ \neg \mathit{CH} \}$，其中 $\mathit{ZC}$ 为带选择公理的 Zermelo 集合论。为此，我们在证明辅助工具 Isabelle 中工作，以 L. Paulson 等人开发的 Isabelle/ZF 库为基础。