A Machine Proof of the Filter-Method Construction for Real Numbers

Guowei Dou and Wensheng Yu ()
Additional contact information
Guowei Dou: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China
Wensheng Yu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China

Mathematics, 2025, vol. 13, issue 17, 1-30

Abstract: This paper presents a machine verification of a real number theory where real numbers are constructed using concepts related to filters. The theory encompasses a special filter, namely the non-principal arithmetical ultrafilter whose existence can be proven with the Continuum Hypothesis, to establish several non-standard number sets: * N , * Z and * Q . The set of real numbers, R , is subsequently obtained by the equivalence classification of a specific subset of * Q . The entire theory is thoroughly formalized, with each detail verified to ensure rigor and precision. The verification is implemented using the Coq proof assistant and is grounded in the Morse–Kelley axiomatic set theory. This work contributes a new selection of foundational material for the formalization of mathematical theories.

Keywords: formal verification; Coq; real numbers; non-standard numbers; Morse–Kelley axiomatic set theory; non-principal arithmetical ultrafilter; Continuum Hypothesis (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2025
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/13/17/2707/pdf (application/pdf)
https://www.mdpi.com/2227-7390/13/17/2707/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:13:y:2025:i:17:p:2707-:d:1730543

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().