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

doi:10.13190/j.jbupt.2019-001

JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM ›› 2019, Vol. 42 ›› Issue (5): 1-7.doi: 10.13190/j.jbupt.2019-001

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

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

CLC Number:

TN929.53

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.

References

[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/.

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments

[1]	ZHANG Chenyu, WEN Xiangming, CHEN Yawen. High-Precision and Low-Cost Timing Method of Mobile Cellular Network [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(1): 103-108.
[2]	. Intent-driven Demand-aware Resource Service in Autonomous Networks [J]. Journal of Beijing University of Posts and Telecommunications, 2022, 45(6): 85-91.
[3]	CHU Xing-he, LU Zhao-ming, WANG Lu-han, WU Mu-qing, WEN Xiang-ming. Multi-Path Assisted Cooperative Radio-Based Localization for Connected Vehicles [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(2): 116-123.
[4]	ZHANG Tian-kui, WANG Xiao-fei, YANG Li-wei, YANG Ding-cheng. A SFC Deployment and Computation Resource Allocation Joint Algorithm in Mobile Networks [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(1): 7-13.
[5]	Lü Ting-jie, SONG Luo-na, TENG Ying-lei, FENG Ye-yuan. The Architecture Design and Evaluation Method for Eco-Sustainabability Oriented Next Generation Communication Networks [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(6): 18-26,35.
[6]	HE Jian-hua, ZHAO Hui, XU Xiao-bin, YAN Lei, WANG Shang-guang. Data Collection Method of Space-Based Internet of Things Based on Improved Double Level Distributed LT Code [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(6): 118-125.
[7]	MA Lu, LIU Ming, LI Chao, LU Zhao-ming, MA Huan. A Cloud-Edge Collaborative Computing Task Scheduling Algorithm for 6G Edge Networks [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(6): 66-73.
[8]	GUAN Wan-qing, ZHANG Hai-jun, LU Zhao-ming. Intelligent Resource Allocation Algorithm for 6G Multi-Tenant Network Slicing Based on Deep Reinforcement Learning [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(6): 132-139.
[9]	LUO Yi, WANG Yu-ting, SHI Rong-hua, YAN Meng-chun, ZENG Hao. Secrecy Outage Probability Analysis of Underlay Cognitive Cooperative Relay Network with Energy Harvesting [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(3): 105-111,124.
[10]	LI Jun-yao, CHANG Yong-yu, ZENG Tian-yi. Channel Correlation Based LOS/NLOS Identification for 3D Massive MIMO Systems [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(1): 1-7.
[11]	JIANG Fang, ZHANG Nan-fei, HU Yan-jun, WANG Yi. BP Neural Network Based CSI Device-Free Target Classification Method [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(1): 40-45.
[12]	REN Jia-zhi, TIAN Hui, NIE Gao-feng. Proactive Caching Scheme with Local Content Popularity Prediction [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(1): 80-91.
[13]	XU Jiu-yun, SUN Zhong-shun, ZHANG Ru-ru. Mobile Phone Energy Saving Based on Link Prediction [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(1): 8-13,27.
[14]	LI Xiao-hui, DU Yang-fan, SHI Xiao-zhu, YANG Xu. NLOS Ranging Error Compensation Algorithm Based on Fuzzy Association Channel Identification [J]. Journal of Beijing University of Posts and Telecommunications, 2020, 43(1): 21-27.
[15]	LI Peng, WANG De-yong, SHI Wen-xi, JIANG Zhi-guo. Research on Person Re-Identification Based on Deep Learning under Big Data Environment [J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2019, 42(6): 29-34.