Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

Yaoshun Fu and Wensheng Yu
Additional contact information
Yaoshun Fu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China
Wensheng Yu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China

Mathematics, 2020, vol. 9, issue 1, 1-21

Abstract: The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.

Keywords: real number theory; completeness theorems; Coq; formalization; analysis (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2020
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/1/38/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/1/38/ (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:9:y:2020:i:1:p:38-:d:468491

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 ().