Wetzel：与连续统假设相关的不可判定问题的形式化
计算机科学中的逻辑
2022-10-14 v2
摘要
1964年，Paul Erdős 发表了一篇论文，解决了他在一本问题集中看到的一个关于函数空间的问题。Erdős 证明了答案为“是”当且仅当连续统假设为假：一个看似简单的问题竟被证明在 ZFC 公理下是不可判定的。这些证明在 Isabelle/HOL 中的形式化展示了复分析与集合论的结合使用，特别是 Isabelle/HOL 的 ZFC 库如何将集合论与高阶逻辑相集成。
引用
@article{arxiv.2205.03159,
title = {Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis},
author = {Lawrence C Paulson},
journal= {arXiv preprint arXiv:2205.03159},
year = {2022}
}
备注
Accepted to Conference on Intelligent Computer Mathematics (CICM 2022)