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-19Online:
2019-10-28Published:
2019-11-25
CLC Number:
Cite this article
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.
share this article
Add to citation manager EndNote|Ris|BibTeX
URL: https://journal.bupt.edu.cn/EN/10.13190/j.jbupt.2019-001
[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 36th 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/. |
[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. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||