选择公理与Tukey引理等价性的机器证明

孙天宇, 郁文生

北京邮电大学 天地互联与融合北京市重点实验室, 北京 100876

收稿日期:2019-01-19出版日期:2019-10-28发布日期:2019-11-25

作者简介:孙天宇(1993-),男,博士生,E-mail:stycyj@bupt.edu.cn;郁文生(1967-),男,教授,博士生导师.
基金资助:国家自然科学基金项目（61571064，61936008）

A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma

SUN Tian-yu, YU Wen-sheng

Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China

Received:2019-01-19Online:2019-10-28Published:2019-11-25

摘要/Abstract

摘要： 基于计算机证明辅助工具Coq，提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上，给出选择公理与Tukey引理的形式化描述，这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码，并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性和交互性的特点，其证明过程规范、严谨、可靠，在集合论、拓扑学和代数学的形式化构建中具有重要应用.
中图分类号:
TN929.53

引用本文

孙天宇, 郁文生. 选择公理与Tukey引理等价性的机器证明[J]. 北京邮电大学学报, 2019, 42(5): 1-7.
SUN Tian-yu, YU Wen-sheng. A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma[J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2019, 42(5): 1-7.





PDF全文下载地址:

https://journal.bupt.edu.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=3382