选择公理及其等价定理的形式化
计算机科学中的逻辑
2019-06-11 v1 形式语言与自动机理论
摘要
在本文中，我们描述了 Morse-Kelley 集合论中选取公理及其若干著名等价定理的形式化。这些定理包括 Tukey 引理、Hausdorff 极大原理、极大原理、Zermelo 公设、Zorn 引理和良序定理。我们依次由选择公理证明上述定理，最后由 Zermelo 公设和良序定理证明选择公理，从而完成它们之间的等价性的循环证明。证明使用 Coq 证明辅助工具在形式化了的 Morse-Kelley 集合论中进行了形式化检验。整个形式化证明过程表明，基于 Coq 的数学定理机器证明具有高度的可靠性和严谨性。本文的形式化工作足以满足大多数应用，特别是在集合论、拓扑学和代数中。
引用
@article{arxiv.1906.03930,
title = {Formalization of the Axiom of Choice and its Equivalent Theorems},
author = {Tianyu Sun and Wensheng Yu},
journal= {arXiv preprint arXiv:1906.03930},
year = {2019}
}
备注
26 pages, 2 figures, 2 tables, journal