集合论机械化：基数算术与选择公理
计算机科学中的逻辑
2016-08-31 v1
摘要
使用证明助手 Isabelle 对 Zermelo-Frenkel (ZF) 集合论中相当深度的结果进行了机械化。这些结果涉及基数算术和选择公理（AC）。关于基数乘法的一个关键结果是 K*K = K，其中 K 为任意无限基数。证明该结果需要发展序、序同构、序型、序数算术、基数等理论；这涵盖了 Kunen 所著《集合论》（Set Theory）第一章的大部分内容。此外，我们证明了良序定理的 7 种表述的等价性以及选择公理的 20 种表述的等价性；这涵盖了 Rubin 和 Rubin 所著《选择公理的等价物》（Equivalents of the Axiom of Choice）的前两章，并涉及高度技术性的材料。证明中使用的定义在风格上很大程度上忠实于原始数学。
引用
@article{arxiv.cs/9612104,
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.},
author = {Lawrence C. Paulson and Krzysztof Grabczewski},
journal= {arXiv preprint arXiv:cs/9612104},
year = {2016}
}