Formalization of the Equivalence among Completeness Theorems of Real Number in Coq
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2020-12-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/9/1/38 |
| _version_ | 1797543510379855872 |
|---|---|
| author | Yaoshun Fu Wensheng Yu |
| author_facet | Yaoshun Fu Wensheng Yu |
| author_sort | Yaoshun Fu |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-10T13:46:37Z |
| format | Article |
| id | doaj.art-8e4d74242b8e4d7aa21f6b39c3967e87 |
| institution | Directory Open Access Journal |
| issn | 2227-7390 |
| language | English |
| last_indexed | 2024-03-10T13:46:37Z |
| publishDate | 2020-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj.art-8e4d74242b8e4d7aa21f6b39c3967e872023-11-21T02:36:20ZengMDPI AGMathematics2227-73902020-12-01913810.3390/math9010038Formalization of the Equivalence among Completeness Theorems of Real Number in CoqYaoshun Fu0Wensheng Yu1Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, ChinaBeijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, ChinaThe 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.https://www.mdpi.com/2227-7390/9/1/38real number theorycompleteness theoremsCoqformalizationanalysis |
| spellingShingle | Yaoshun Fu Wensheng Yu Formalization of the Equivalence among Completeness Theorems of Real Number in Coq Mathematics real number theory completeness theorems Coq formalization analysis |
| title | Formalization of the Equivalence among Completeness Theorems of Real Number in Coq |
| title_full | Formalization of the Equivalence among Completeness Theorems of Real Number in Coq |
| title_fullStr | Formalization of the Equivalence among Completeness Theorems of Real Number in Coq |
| title_full_unstemmed | Formalization of the Equivalence among Completeness Theorems of Real Number in Coq |
| title_short | Formalization of the Equivalence among Completeness Theorems of Real Number in Coq |
| title_sort | formalization of the equivalence among completeness theorems of real number in coq |
| topic | real number theory completeness theorems Coq formalization analysis |
| url | https://www.mdpi.com/2227-7390/9/1/38 |
| work_keys_str_mv | AT yaoshunfu formalizationoftheequivalenceamongcompletenesstheoremsofrealnumberincoq AT wenshengyu formalizationoftheequivalenceamongcompletenesstheoremsofrealnumberincoq |