On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles

Authors Hugo Herbelin , Jad Koleilat



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.26.pdf
  • Filesize: 0.72 MB
  • 15 pages

Document Identifiers

Author Details

Hugo Herbelin
  • Université de Paris Cité, Inria, CNRS, IRIF, France
Jad Koleilat
  • Université Paris Cité, France

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

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)
    0
    PDF Downloads

References

  1. 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. Google Scholar
  2. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. 36th Annual Symposium on Logic in Computer Science, 2021. Google Scholar
  3. 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. Google Scholar
  4. Horst Herrlich. Axiom of Choice. Lecture Notes in Mathematics. Springer, 2006. Google Scholar
  5. Thomas J. Jech. The Axiom of Choice. Dover Books on Mathematics Series. Courier corporation, 1973. Google Scholar
  6. Herman Rubin and Jean E. Rubin. Equivalents of the Axiom of Choice. North-Holland Publishing Company, 1970. Google Scholar