论文标题
CTM强迫方法的正式验证
The formal verification of the ctm approach to forcing
论文作者
论文摘要
我们讨论了我们的计算机验证的构造证明的一些亮点，鉴于可计数的$ \ mathit $ \ mathit {zfc} $的可计数套件，可满足$ \ Mathit {Zfc}+\ neg \ neg \ neg \ Mathit {Ch} $ {ch} $ and $ \ \ \ \ \ \ \ sfc}+Mathit {Ch}+Mathit {Ch}的通用扩展。此外，令$ \ Mathcal {r} $为替换公理的实例集。我们隔离了一个21元素子集$ω\ subseteq \ mathcal {r} $，并定义了$ \ nathcal {f}：\ Mathcal {r} \ to \ Mathcal {r} $ \ Mathit {zc} \ cup \ Mathcal {f} \ text {`}φ\cupΩ$暗示$ m [g] \ MATCOLD \ MATHIT \ MATHIT {ZC} \cupφ\ cup \ cup \ cup \ \ cup {\ neg \ neg \ neg \ neg \ mathit {ch} {ch} {ch} {ch} \ is zer zers $ sepers $ sepers osevers osevers osevers。 为了实现这一目标，我们在L. Paulson等人的Isabelle/ZF图书馆的发展助理Isabelle工作。
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $Ω\subseteq\mathcal{R}$ and defined $\mathcal{F}:\mathcal{R}\to\mathcal{R}$ such that for every $Φ\subseteq\mathcal{R}$ and $M$-generic $G$, $M\models \mathit{ZC} \cup \mathcal{F}\text{``}Φ\cup Ω$ implies $M[G]\models \mathit{ZC} \cup Φ\cup \{ \neg \mathit{CH} \}$, where $\mathit{ZC}$ is Zermelo set theory with Choice. To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others.
