The Continuum Hypothesis Implies the Existence of Non-principal Arithmetical Ultrafilters – A Coq Formal Verification

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.