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

doi:10.13190/j.jbupt.2019-001

北京邮电大学学报 ›› 2019, Vol. 42 ›› Issue (5): 1-7.doi: 10.13190/j.jbupt.2019-001

• 论文 • 下一篇

选择公理与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-19 Online:2019-10-28 Published:2019-11-25

摘要/Abstract

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

关键词: 机器证明, 形式化数学, 选择公理, Tukey引理

Abstract: On the basis of the computer proof assistant Coq, a formal proof of the equivalence between the axiom of choice and Tukey's lemma is presented. The formal description of axiom of choice and Tukey lemma was given based on the "axiomatic set theory" formal system, which was the first formalization of Tukey's lemma. A complete proof code of the equivalence between the axiom of choice and Tukey's lemma was completed. All the proofs were formally checked in Coq. The formal proof demonstrated that the Coq-based mechanized proof of mathematics theorem had the characteristics of readability and interactivity. The proof process was standardized, rigorous and reliable. This formal work has important applications in many fields of formal mathematics, especially in set theory, topology and algebra.

Key words: mechanized proof, formal mathematics, axiom of choice, Tukey's lemma

中图分类号:

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.

参考文献

[1] Jech T. The axiom of choice[M]. Amsterdam:North Holland Publishing Company, 1973:1-56.
[2] Bernays P, Fraenkel A A. Axiomatic set theory[M]. Amsterdam:North Holland Publishing Company, 1958:1-73.
[3] Bertot Y, Castéran P. Interactive theorem proving and program development, Coq'art:the calculus of inductive constructions[M]. Heidelberg:Springer, 2004:1-11.
[4] Gonthier G. Formal proof-the four color theorem[J]. Notices of the American Mathematical Society, 2008, 55(11):1382-1393.
[5] Gonthier G, Asperti A, Avigad J, et al. Machine-checked proof of the odd order theorem[C]//ITP 2013. Heidelberg:Springer, 2013:163-179.
[6] Wiedijk F. Formal proof-getting started[J]. Notices of the American Mathematical Society, 2008, 55(11):1408-1414.
[7] Wang Hao. On Zermelo's and Von Neumann's axioms for set theory[J]. Proc Natl Acad Sci USA, 1949, 35(3):150-155.
[8] Kelley J L. General topology[M]. New York:Springer-Verlag, 1955:250-281.
[9] Sun Tianyu. Axiomatic set theory[EB/OL]. (2018-10-20)[2018-12-10]. https://github.com/styzystyzy/Axiomatic_Set_Theory/.
[10] Werner B. Sets in types, types in sets[C]//Proceedings of TACS' 97. Heidelberg:Springer, 1997:530-546.
[11] Barras B. Sets in Coq, Coq in sets[J]. Journal of Formalized Reasoning, 2010, 3(1):29-48.
[12] Kirst D, Smolka G. Categoricity results for second-order ZF in dependent type theory[C]//ITP 2017. Heidelberg:Springer, 2017:304-318.
[13] Paulson L C. The relative consistency of the axiom of choice mechanized using Isabelle/ZF[J]. LMS Journal of Computation and Mathematics, 2003(6):98-248.
[14] Sun Tianyu, Yu Wensheng. Machine proving system for mathematical theorems based on Coq-machine proving of Hausdorff maximal principle and Zermelo postulate[C]//Proceedings of the 36^th Chinese Control Conference. New York:IEEE, 2017:9871-9878.
[15] 熊金城. 点集拓扑讲义[M]. 北京:高等教育出版社, 2011:36-40.
[16] Sun Tianyu. Tukey's lemma and AC[EB/OL]. (2018-11-30)[2018-12-10]. https://github.com/BKLSIC/Tukey_AC/.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	章晨宇温向明陈亚文. 蜂窝移动网络低成本高精度授时[J]. 北京邮电大学学报, 2023, 46(1): 103-108.
[2]	郭令奇褚智贤廖建新王敬宇陆璐. 意图驱动的自智网络资源按需服务[J]. 北京邮电大学学报, 2022, 45(6): 85-91.
[3]	初星河, 路兆铭, 王鲁晗, 武穆清, 温向明. 多径信号辅助的网联车辆无线协作定位[J]. 北京邮电大学学报, 2021, 44(2): 116-123.
[4]	张天魁, 王筱斐, 杨立伟, 杨鼎成. 移动网络SFC部署与计算资源分配联合算法[J]. 北京邮电大学学报, 2021, 44(1): 7-13.
[5]	吕廷杰, 宋罗娜, 滕颖蕾, 丰业媛. 面向生态可持续的下一代通信网络架构与评价体系[J]. 北京邮电大学学报, 2020, 43(6): 18-26,35.
[6]	何建华, 赵辉, 徐晓斌, 闫蕾, 王尚广. 基于改进双层LT码的天基物联网数据收集方法[J]. 北京邮电大学学报, 2020, 43(6): 118-125.
[7]	马璐, 刘铭, 李超, 路兆铭, 马欢. 面向6G边缘网络的云边协同计算任务调度算法[J]. 北京邮电大学学报, 2020, 43(6): 66-73.
[8]	管婉青, 张海君, 路兆铭. 基于DRL的6G多租户网络切片智能资源分配算法[J]. 北京邮电大学学报, 2020, 43(6): 132-139.
[9]	罗轶, 王雨婷, 施荣华, 严梦纯, 曾豪. 能量采集衬底式认知协作中继网络安全中断概率分析[J]. 北京邮电大学学报, 2020, 43(3): 105-111,124.
[10]	李君瑶, 常永宇, 曾天一. 大规模3D MIMO中基于信道相关的LOS/NLOS识别算法[J]. 北京邮电大学学报, 2020, 43(1): 1-7.
[11]	蒋芳, 张南飞, 胡艳军, 王翊. 基于BP神经网络的CSI无源目标分类方法[J]. 北京邮电大学学报, 2020, 43(1): 40-45.
[12]	任佳智, 田辉, 聂高峰. 基于本地内容流行度预测的主动缓存策略[J]. 北京邮电大学学报, 2020, 43(1): 80-91.
[13]	徐九韵, 孙忠顺, 张如如. 基于链路预测的手机节能方法[J]. 北京邮电大学学报, 2020, 43(1): 8-13,27.
[14]	李晓辉, 杜洋帆, 石潇竹, 杨胥. 基于信道模糊关联识别的NLOS测距误差补偿算法[J]. 北京邮电大学学报, 2020, 43(1): 21-27.
[15]	李鹏, 王德勇, 师文喜, 姜志国. 大数据环境下基于深度学习的行人再识别[J]. 北京邮电大学学报, 2019, 42(6): 29-34.