LIPIcs.FSCD.2024.26.pdf
- Filesize: 0.72 MB
- 15 pages
Document
On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles
Authors
Hugo Herbelin 
,
-
Part of:
Volume:
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-07-05
File
Document Identifiers
Author Details
Cite AsGet BibTex
Hugo Herbelin and Jad Koleilat. On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.26
https://doi.org/10.4230/LIPIcs.FSCD.2024.26
Abstract
We study the logical structure of Teichmüller-Tukey lemma, a maximality principle equivalent to the axiom of choice and show that it corresponds to the generalisation to arbitrary cardinals of update induction, a well-foundedness principle from constructive mathematics classically equivalent to the axiom of dependent choice.
From there, we state general forms of maximality and well-foundedness principles equivalent to the axiom of choice, including a variant of Zorn’s lemma. A comparison with the general class of choice and bar induction principles given by Brede and the first author is initiated.
Subject Classification
ACM Subject Classification
- Theory of computation → Proof theory
Keywords
- axiom of choice
- Teichmüller-Tukey lemma
- update induction
- constructive reverse mathematics
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Ulrich Berger. A computational interpretation of open induction. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS '04, page 326, USA, 2004. IEEE Computer Society.
-
Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. 36th Annual Symposium on Logic in Computer Science, 2021.
-
Thierry Coquand. Constructive topology and combinatorics. In J. Paul Myers and Michael J. O'Donnell, editors, Constructivity in Computer Science, pages 159-164, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.
-
Horst Herrlich. Axiom of Choice. Lecture Notes in Mathematics. Springer, 2006.
-
Thomas J. Jech. The Axiom of Choice. Dover Books on Mathematics Series. Courier corporation, 1973.
-
Herman Rubin and Jean E. Rubin. Equivalents of the Axiom of Choice. North-Holland Publishing Company, 1970.