Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912094752866304 |
|---|---|
| author | Incatasciato, Guillermo L. Terraf, Pedro Sánchez |
| author_facet | Incatasciato, Guillermo L. Terraf, Pedro Sánchez |
| contents | We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results through the use of Chain Bounding are amongst the simplest ones that we are aware of. As a by-product, we show that for every poset $P$ and function $f$ from the powerset of $P$ into $P$, there exists a maximal well-ordered chain whose family of initial segments is appropriately closed under $f$.
We also provide an introduction to the process of "computer formalization" of mathematical proofs by using *proofs assistants*. As an illustration, we verify our main results with the Lean proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_11638 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization Incatasciato, Guillermo L. Terraf, Pedro Sánchez Logic History and Overview 06A06, 03E25, 68V20, 03-01 F.4.1; I.2.3 We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results through the use of Chain Bounding are amongst the simplest ones that we are aware of. As a by-product, we show that for every poset $P$ and function $f$ from the powerset of $P$ into $P$, there exists a maximal well-ordered chain whose family of initial segments is appropriately closed under $f$. We also provide an introduction to the process of "computer formalization" of mathematical proofs by using *proofs assistants*. As an illustration, we verify our main results with the Lean proof assistant. |
| title | Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization |
| topic | Logic History and Overview 06A06, 03E25, 68V20, 03-01 F.4.1; I.2.3 |
| url | https://arxiv.org/abs/2404.11638 |