Formalization of the equivalence among completeness theorems of real number in Coq

5Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

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.

Cite

CITATION STYLE

APA

Fu, Y., & Yu, W. (2021). Formalization of the equivalence among completeness theorems of real number in Coq. Mathematics, 9(1), 1–21. https://doi.org/10.3390/math9010038

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free