论文标题
Isabelle/ZF强迫的形式化
Formalization of Forcing in Isabelle/ZF
论文作者
论文摘要
我们在Isabelle/ZF的设定理论框架中进行强迫的理论形式化。在存在ZFC的可数及时模型的假设下，我们构建了适当的通用扩展，并表明后者也满足ZFC。在这样做的过程中，我们重塑了Paulson的ZF构建性库。
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library.
