论文标题
Wetzel：与连续假设相关的不可确定问题的形式化
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
论文作者
论文摘要
1964年，保罗·埃德（Paul Erd）发表了一篇论文，解决了有关他在问题书中看到的功能空间的问题。埃尔德（Erd）证明，当且仅当连续性假设是错误的情况下，答案是肯定的：一个看上去无辜的问题在ZFC的公理中是不可确定的。这些证明在Isabelle/Hol中的形式化证明了复杂分析和设定理论的联合使用，尤其是ZFC的Isabelle/HOL库如何将设置的理论与高阶逻辑整合在一起。
In 1964, Paul Erdős published a paper settling a question about function spaces that he had seen in a problem book. Erdős proved that the answer was yes if and only if the continuum hypothesis was false: an innocent-looking question turned out to be undecidable in the axioms of ZFC. The formalisation of these proofs in Isabelle/HOL demonstrate the combined use of complex analysis and set theory, and in particular how the Isabelle/HOL library for ZFC integrates set theory with higher-order logic.
