Abstract
The formalization of mathematical theorems is an important direction in the field of formal verification. Formalizing mathematical theorems ensures their accuracy and rigor in practical applications. Non-principal arithmetical ultrafilter (NPAUF) was proposed in [27]. It can be directly applied to the extension of number systems such as real numbers and non-standard real numbers. So far, though the existence of NPAUF has not been proven only with general set theories, it can be proven with the help of some additional consistent set-theoretic assumptions, such as the Continuum Hypothesis (CH). This paper presents the formal verification of the existence of NPAUF, implemented with the Coq proof assistant and grounded in the Morse-Kelley (MK) axiomatic set theory augmented with CH. The formal descriptions for the concepts related to filter, arithmetical ultrafilter (AUF), NPAUF, and CH are all provided. This work serves as the first step of our long-term objective – to formalize the non-standard analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
Note that \(\omega \) has many meanings in set theory. It can represent the set of all natural numbers, meanwhile it is both the first infinite ordinal number and the first infinite cardinal number. [18].
- 4.
All definitions are defined with the command “
”.
- 5.
R is an ordinal but not an ordinal number.
References
Avigad, J., Harrison, J.: Formally verified mathematics. Commun. ACM 57(4), 66–75 (2014). https://doi.org/10.1145/2591012
Barras, B.: Sets in Coq, Coq in Sets. J. Formalized Reason. 3(1), 29–48 (2010). https://doi.org/10.6092/issn.1972-5787/1695
Bartoszynski, T., Shelah, S.: There may be no hausdolff ultrafilters (2003). https://doi.org/10.48550/arXiv.math/0311064
Bell, J.L.: Set Theory: Boolean-Valued Models and Independence Proofs (Oxford Logic Guides 47), 3rd edn. Clarendon Press, Oxford (2005)
Bernays, P., Fraenkel, A.A.: Axiomatic Set Theory. North Holland Publishing Company, Amsterdam (1958)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Interactive Constructions. Springer, Berlin (2004). https://doi.org/10.1007/978-3-662-07964-5
Cohen, P.J.: Set Theory and the Continuum Hypothesis. W.A.Benjamin Inc., New York (1966)
Comfort, W.W., Negrepontis, S.: The Theory of Ultrafilters. Springer, Berlin (1974). https://doi.org/10.1007/978-3-642-65780-1
The Coq Development Team. The Coq Proof Assistant Reference Manual (Version 8.19.0) (2024). https://coq.inria.fr/doc/V8.19.0/refman/. Accessed 8 July 2024
Dou, G., Yu, W.: Formalization of the filter extension principle (FEP) in coq. In: Zhang, L., Yu, W., Wang, Q., Laili, Y., Liu, Y. (eds.) Intelligent Networked Things. CINT 2024. CCIS, vol. 2138, pp. 95-106. Springer, Singapore (2024). https://doi.org/10.1007/978-981-97-3951-6_10
Gödel, K.: Consistency-proof for the generalized continuum-hypothesis. Proc. Natl. Acad. Sci. 25(4), 220–224 (1939). https://doi.org/10.1073/pnas.25.4.220
Gödel, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis With the Axioms of Set Theory. Princeton University Press, Princeton (1940)
Gonthier, G.: Formal proof - the Four Color Theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008). https://www.ams.org/notices/200811/tx081101382p.pdf
Gonthier, G., et al.: A machine-checked proof of the Odd Order Theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. ITP 2013. LNCS, vol. 7998, pp. 163-179. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_14. https://www.cs.unibo.it/~asperti/PAPERS/odd_order.pdf
Hewitt, E.: Rings of real-valued continuous functions. I. Trans. Am. Math. Soc. 64(1), 45-99 (1948). https://sci-hub.st/10.1090/s0002-9947-1948-0026239-9
Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq Proof Assistant: A Tutorial (Version 8.5). Technical Report 178, INRIA (2016). https://coq.inria.fr/tutorial/
Jin, R.L.: Nonstandard analysis and its applications. Scientia Sinica Mathematica 46(4), 371–408 (2016). https://doi.org/10.1360/N012015-00266. (in Chinese)
Kelley, J.L.: General Topology. Springer, New York (1955). https://doi.org/10.1007/978-1-4757-4032-5
Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman and Hall, London (1997)
Monk, J.D.: Introduction to Set Theory. McGraw-Hill, New York (1969)
Pierce, B.C., de Amorim, A.A., Casinghino, C., et al.: Software Foundation. http://softwarefoundations.cis.upenn.edu/. Accessed 8 July 2024
Robinson, A.: Non-standard Analysis, revised edn. North Holland Publishing Company, Amsterdam (1974)
Rubin, J.E.: Set Theory for the Mathematician. Holden Day, San Francisco (1967)
Sun, T., Yu, W.: A formal system of axiomatic set theory in Coq. IEEE Access 8, 21510–21523 (2020). https://doi.org/10.1109/ACCESS.2020.2969486
Thomas, J.J.: The Axiom of Choice. North-Holland Publishing Company, Amsterdam (1973)
Wan, X., Xu, K., Cao, Q.: Coq formalization of ZFC set theory for teaching scenarios. Int. J. Softw. Inf. 13(3), 323–357 (2023). https://www.ijsi.org/ijsi/article/pdf/303
Wang, F.: On a special kind of points in stone-\(\check{c}\)ech compactification \(\beta \omega \). J. China Univ. Sci. Tech. 28(5), 567–570 (1998)
Wang, F.: A result on arithmetical ultrafilters. J. China Univ. Sci. Tech. 30(5), 517–522 (2000)
Wang, F.: Arithmetical Ultrafilters: End-Extenstions of \(\textbf{N} \) in \(\beta {\textbf{N} }\). University of Science and Technology of China Press, Hefei (2016). (in Chinese)
Wang, F.: Mathematical Foundations, revised edn. Higher Education Press, Beijing (2018). (in Chinese)
Wang, H.: On Zermelo’s and Von Neumann’s axioms for set theory. Proc. Natl. Acad. Sci. U.S.A. 35(3), 150–155 (1949). https://doi.org/10.1073/pnas.35.3.150
Werner, B.: Sets in types, types in sets. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530–546. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014566
Herbelin, H., Palmskog, K., et al.: An encoding of Zermelo-Fraenkel Set Theory in Coq (1996). https://github.com/coq-contribs/zfc
Wiedijk, F.: Formal proof - getting started. Not. Am. Math. Soc. 55(11), 1408–1414 (2008). https://www.ams.org/notices/200811/tx081101408p.pdf
Yu, W., Sun, T., Fu, Y.: A Machine Proof System for Axiomatic Set Theory. Science Press, Beijing (2020). (in Chinese)
Zhang, Q.P.: Set-Theory: Coq encoding of ZFC and formalization of the textbook elements of set theory. https://github.com/choukh/Set-Theory
Acknowledgments
Our work is funded by National Natural Science Foundation (NNSF) of China under Grant 61936008.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
A Partial Definitions and Notations of MK
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Dou, G., Chen, S., Yu, W., Zhang, R. (2024). The Continuum Hypothesis Implies the Existence of Non-principal Arithmetical Ultrafilters – A Coq Formal Verification. In: Ogata, K., Mery, D., Sun, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2024. Lecture Notes in Computer Science, vol 15394. Springer, Singapore. https://doi.org/10.1007/978-981-96-0617-7_15
Download citation
DOI: https://doi.org/10.1007/978-981-96-0617-7_15
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-96-0616-0
Online ISBN: 978-981-96-0617-7
eBook Packages: Computer ScienceComputer Science (R0)