Document Open Access Logo

Constructive Substitutes for Kőnig’s Lemma

Author Dominique Larchey-Wendling

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.2.pdf
  • Filesize: 0.77 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Kőnig’s lemma
  • FAN theorem
  • constructive mathematics
  • inductive covers
  • inductive bars
  • almost full relations
  • inductive type theory
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We propose weaker but constructively provable variants of the contrapositive of Kőnig’s lemma. We derive those from a generalization of the FAN theorem for inductive bars to inductive covers, for which we give a concise proof. We compare the positive, negative and sequential characterizations of covers and bars in classical and constructive contexts, giving precise accounts of the role played by the axioms of excluded middle and dependent choice. As an application, we discuss some examples where the use of Kőnig’s lemma can be replaced by one of our weaker variants to obtain fully constructive accounts of results or proofs that could otherwise appear as inherently classical.

Cite As Get BibTex

Dominique Larchey-Wendling. Constructive Substitutes for Kőnig’s Lemma. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.2

Author Details

Dominique Larchey-Wendling
  • Université de Lorraine, CNRS, LORIA, F-54000 Nancy, France

Funding

  • Larchey-Wendling, Dominique: partially supported by NARCO (ANR-21-CE48-0011).

Supplementary Materials

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. J. Berger. Brouwer’s fan theorem, 2021. URL: https://doi.org/10.48550/arXiv.2001.00064.
  3. J. Berger and H. Ishihara. Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51(4):360-364, 2005. URL: https://doi.org/10.1002/malq.200410038.
  4. J. Berger and G. Svindland. Brouwer’s fan theorem and convexity. The Journal of Symbolic Logic, 83(4):1363-1375, 2018. URL: https://doi.org/10.1017/jsl.2018.49.
  5. C. Cheung. Brouwer’s Fan Theorem: An Overview. Master’s thesis, Cornell University, 2015. URL: https://api.semanticscholar.org/CorpusID:203584866.
  6. T. Coquand. About Brouwer’s Fan Theorem. Revue internationale de philosophie, 230:483-489, September 2004. URL: http://www.jstor.org/stable/23955601.
  7. T. Coquand, G. Sambin, J. Smith, and S. Valentini. Inductively generated formal topologies. Annals of Pure and Applied Logic, 124(1):71-106, 2003. URL: https://doi.org/10.1016/S0168-0072(03)00052-6.
  8. H. B. Curry. A Theory of Formal Deductibility. Notre Dame mathematical lectures. University of Notre Dame, 1957. Google Scholar
  9. M. Escardo. Infinite sets that admit fast exhaustive search. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 443-452, 2007. URL: https://doi.org/10.1109/LICS.2007.25.
  10. D. Fridlender. An Interpretation of the Fan Theorem in Type Theory. In Types for Proofs and Programs, pages 93-105. Springer Berlin Heidelberg, 1999. URL: https://doi.org/10.1007/3-540-48167-2_7.
  11. H. M. Friedman. Internal finite tree embeddings. In Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic, pages 60-91. Cambridge University Press, 2002. Google Scholar
  12. M. Fujiwara. Kőnig’s lemma, weak Kőnig’s lemma, and the decidable fan theorem. Mathematical Logic Quarterly, 67(2):241-257, 2021. URL: https://doi.org/10.1002/malq.202000020.
  13. J. H. Gallier. What’s so special about Kruskal’s theorem and the ordinal Γ₀? A survey of some results in proof theory. Annals of Pure and Applied Logic, 53(3):199-260, 1991. URL: https://doi.org/10.1016/0168-0072(91)90022-E.
  14. W. Hanf. Nonrecursive Tilings of the Plane. I. The Journal of Symbolic Logic, 39(2):283-285, 1974. URL: https://doi.org/10.2307/2272640.
  15. H. Ishihara. Weak Kőnig’s Lemma Implies Brouwer’s Fan Theorem: A Direct Proof. Notre Dame Journal of Formal Logic, 47(2):249-252, 2006. URL: https://doi.org/10.1305/ndjfl/1153858649.
  16. S. C. Kleene and R. E. Vesley. The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions. North-Holland Publishing Co., 1965. Google Scholar
  17. S. Kripke. The Problem of Entailment (abstract). Journal of Symbolic Logic, 24:324, 1959. Google Scholar
  18. D. Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged), 3(2-3):121-130, 1927. Google Scholar
  19. D. Larchey-Wendling. Constructive substitutes for Kőnig’s lemma (artifact). Software, NARCO (ANR-21-CE48-0011), (visited on 2025-05-25). URL: https://github.com/DmxLarchey/Constructive-Konig
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23151
  20. D. Larchey-Wendling. Constructive Decision via Redundancy-Free Proof-Search. Journal of Automated Reasoning, 64:1197-1219, 2020. URL: https://doi.org/10.1007/s10817-020-09555-y.
  21. D. Larchey-Wendling. Quasi Morphisms for Almost Full Relations. In 30th International Conference on Types for Proofs and Programs, TYPES, 2024. URL: https://easychair.org/publications/preprint/M3Km.
  22. D. Larchey-Wendling. The Coq-Kruskal project, April 2024. URL: https://github.com/DmxLarchey/Coq-Kruskal.
  23. D. Larchey-Wendling. The Friedman-TREE project, November 2024. URL: https://github.com/DmxLarchey/Friedman-TREE.
  24. D. Myers. Nonrecursive Tilings of the Plane. II. The Journal of Symbolic Logic, 39(2):286-294, 1974. URL: https://doi.org/10.2307/2272641.
  25. C. Sacerdoti Coen and S. Valentini. General Recursion and Formal Topology. In PAR-10. Partiality and Recursion in Interactive Theorem Provers, volume 5 of EPiC Series in Computing, pages 72-83. EasyChair, 2012. URL: https://doi.org/10.29007/hl75.
  26. S. G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Logic. Cambridge University Press, 2 edition, 2009. Google Scholar
  27. A. S. Troelstra. Note on the Fan Theorem. The Journal of Symbolic Logic, 39(3):584-596, 1974. URL: https://doi.org/10.2307/2272902.
  28. A. S. Troelstra. Some Models for Intuitionistic Finite Type Arithmetic with Fan Functional. The Journal of Symbolic Logic, 42(2):194-202, 1977. URL: https://doi.org/10.2307/2272120.
  29. W. Veldman. Brouwer’s Real Thesis on Bars. Philosophia Scientiæ, pages 21-42, 2006. URL: https://doi.org/10.4000/philosophiascientiae.404.
  30. W. Veldman. Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s alternative. Arch. Math. Logic, 53:621-693, 2014. URL: https://doi.org/10.1007/s00153-014-0384-9.
  31. D. Vytiniotis, T. Coquand, and D. Wahlstedt. Stop When You Are Almost-Full. In Interactive Theorem Proving, pages 250-265. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-32347-8_17.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact