Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
This paper presents a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant.It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki s...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2010-01-01
|
| Series: | Journal of Formalized Reasoning |
| Online Access: | http://jfr.cib.unibo.it/article/view/1899/1396 |
| _version_ | 1818508116720877568 |
|---|---|
| author | José Grimm |
| author_facet | José Grimm |
| author_sort | José Grimm |
| collection | DOAJ |
| description | This paper presents a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant.It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert's epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo's theorem is also given. The code (including almost all exercises) is available on the Web, underhttp://www-sop.inria.fr/apics/gaia. |
| first_indexed | 2024-12-10T22:27:20Z |
| format | Article |
| id | doaj.art-9781992487bc45a59bb881474fa11f14 |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-12-10T22:27:20Z |
| publishDate | 2010-01-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-9781992487bc45a59bb881474fa11f142022-12-22T01:31:09ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872010-01-013179126Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of SetsJosé GrimmThis paper presents a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant.It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert's epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo's theorem is also given. The code (including almost all exercises) is available on the Web, underhttp://www-sop.inria.fr/apics/gaia.http://jfr.cib.unibo.it/article/view/1899/1396 |
| spellingShingle | José Grimm Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets Journal of Formalized Reasoning |
| title | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets |
| title_full | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets |
| title_fullStr | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets |
| title_full_unstemmed | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets |
| title_short | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets |
| title_sort | implementation of bourbaki s elements of mathematics in coq part one theory of sets |
| url | http://jfr.cib.unibo.it/article/view/1899/1396 |
| work_keys_str_mv | AT josegrimm implementationofbourbakiselementsofmathematicsincoqpartonetheoryofsets |