Document Open Access Logo

Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem

Authors Titouan Leclercq , Étienne Miquey

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.63.pdf
  • Filesize: 0.89 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • Constructive Mathematics
  • Reverse mathematics
  • Fan Theorem
  • Oracles
  • Realizability
  • Evidenced frames

Metrics

Abstract

Friedman-Simpson’s original program of reverse mathematics, as is also the case for most of standard mathematics, has been developed in classical subsystems of second-order arithmetic. As such, (classical) reverse mathematics presents various limitations from a constructive point of view, since for instance it is unable to distinguish between a statement and its contrapositive (e.g. dependent choice and the bar induction principles). The case of (Weak) Kőnig’s Lemma (WKL) and Fan Theorem (FT) is particularly interesting in that regard: while WKL is well-known to imply FT, and if constructivists like Brouwer rejected the former while admitting the latter, the converse implication has not been much studied for years. It is only recently that a growing enthusiasm for constructive reverse mathematics pushed towards a finer-grained analysis of the connection between such principles.
In addition to intuitionistic reverse mathematics, the realizability approach to logical principles adds a computational meaning to purely logical statements. We follow this path to investigate the computational meaning of Brouwer’s Fan Theorem: building on recent work by Lubarsky and Rathjen, we first construct a realizability interpretation of higher-order logic validating FT while refuting WKL. This interpretation relies on a λ-calculus extended with oracles while preserving a notion of continuity for realizers.
We then push this approach a step further to show the robustness of this realizability interpretation by identifying, in the abstract and general setting of evidenced frames, sufficient computational conditions entailing FT.

Cite As Get BibTex

Titouan Leclercq and Étienne Miquey. Oracles Just for Fan: A Robust Computational Interpretation of the Fan Theorem. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 63:1-63:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.63

Author Details

Titouan Leclercq
  • Aix Marseille Université, CNRS, I2M, Marseille, France
Étienne Miquey
  • Aix Marseille Université, CNRS, I2M, Marseille, France

Funding

This work was supported by the ANR-23-CE48-0016 CHoICE project.

References

  1. Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), Birmingham, France, July 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.9.
  2. Andrej Bauer. Instance reducibility and Weihrauch degrees. Logical Methods in Computer Science, Volume 18, Issue 3, August 2022. URL: https://doi.org/10.46298/lmcs-18(3:20)2022.
  3. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. JSL, 1998. URL: https://doi.org/10.2307/2586854.
  4. Josef Berger. A decomposition of brouwer’s fan theorem. J. Log. Anal., 1, 2009. URL: https://doi.org/10.4115/JLA.2009.1.6.
  5. Valentin Blot. A direct computational interpretation of second-order arithmetic via update recursion. In LICS '22, 2022. URL: https://doi.org/10.1145/3531130.3532458.
  6. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles . In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, Los Alamitos, CA, USA, July 2021. IEEE Computer Society. URL: https://doi.org/10.1109/LICS52264.2021.9470523.
  7. L.E.J. Brouwer. Begruündung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten 2. Tl., Theorie der Punktmenge. Müller, Amsterdam, 1919. Google Scholar
  8. Liron Cohen, Sofia A. Faro, and Ross Tate. The effects of effects on constructivism. MFPS, 347, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.006.
  9. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno Da Rocha Paiva, and Vincent Rahli. Separating markov’s principles. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662104.
  10. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. From Partial to Monadic: Combinatory Algebra with Effects. In Proceedings of FSCD 2025, volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.14.
  11. Liron Cohen, Ariel Grunfeld, Dominik Kirst, and Étienne Miquey. Syntactic effectful realizability in higher-order logic. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 16-30. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00009.
  12. Liron Cohen, Étienne Miquey, and Ross Tate. Evidenced frames: A unifying framework broadening realizability models. In LICS'21, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470514.
  13. Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.15.
  14. Martín Escardó. Continuity of Gödel’s System T definable functionals via effectful forcing. Electronic Notes in Theoretical Computer Science, 298:119-141, 2013. Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  15. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput., 31(1):112-151, 2021. URL: https://doi.org/10.1093/logcom/exaa073.
  16. Makoto Fujiwara. An Extension of the Equivalence Between Brouwer’s Fan Theorem and Weak König’s Lemma with a Uniqueness Hypothesis. In Ulrich Berger, Johanna N. Y. Franklin, Florin Manea, and Arno Pauly, editors, Revolutions and Revelations in Computability, volume 13359, pages 115-124. Springer International Publishing, Cham, 2022. URL: https://doi.org/10.1007/978-3-031-08740-0_10.
  17. Makoto Fujiwara and Takako Nemoto. Choice principles characterizing the difference between König’s lemma and weak König’s lemma in constructive reverse mathematics. Computability, 14(1):30-37, February 2025. URL: https://doi.org/10.3233/COM-230478.
  18. Samuel Gardelle and Étienne Miquey. Do CPS translations also translate realizers? In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 134-151, Praz-sur-Arly, France, January 2023. URL: https://hal.inria.fr/hal-03910311.
  19. Guillaume Geoffroy. Classical realizability as a classifier for nondeterminism. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 462-471. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209140.
  20. Nicolas D. Goodman. Relativized realizability in intuitionistic arithmetic of all finite types. Journal of Symbolic Logic, 43(1):23-44, 1978. URL: https://doi.org/10.2307/2271946.
  21. Timothy Griffin. A formulae-as-type notion of control. In POPL '90, New York, NY, USA, 1990. ACM. URL: https://doi.org/10.1145/96709.96714.
  22. Hugo Herbelin. On the degeneracy of sigma-types in presence of computational classical logic. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, pages 209-220, 2005. URL: https://doi.org/10.1007/11417170_16.
  23. Hugo Herbelin. A constructive proof of dependent choice, compatible with classical logic. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, 2012. URL: https://doi.org/10.1109/LICS.2012.47.
  24. Hugo Herbelin and Danko Illik. An analysis of the constructive content of henkins’s proof of Gödel’s completeness theorem. The Journal of Symbolic Logic, pages 1-43, 2025. URL: https://doi.org/10.1017/jsl.2025.10137.
  25. Marc Hermes and Dominik Kirst. An analysis of tennenbaum’s theorem in constructive type theory. Logical Methods in Computer Science, Volume 20, Issue 1, March 2024. URL: https://doi.org/10.46298/lmcs-20(1:19)2024.
  26. Hajime Ishihara. Continuity properties in constructive mathematics. Journal of Symbolic Logic, 57(2):557-565, 1992. URL: https://doi.org/10.2307/2275292.
  27. Hajime Ishihara. Reverse mathematics in bishop’s constructive mathematics. Philosophia Scientiæ, 6:43-59, 2006. URL: https://doi.org/10.4000/philosophiascientiae.406.
  28. B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.
  29. Dominik Kirst and Haoyi Zeng. The blurred drinker paradox: Constructive reverse mathematics of the downward löwenheim-skolem theorem. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 926-940, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00073.
  30. S. C. Kleene. Recursive functions and intuitionistic mathematics. Journal of Symbolic Logic, 18(2):181-182, 1953. URL: https://doi.org/10.2307/2268961.
  31. Stephen Cole Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53:41-73, 1943. URL: https://doi.org/10.2307/2267986.
  32. Stephen Cole Kleene and Richard Eugene Vesley. The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions. North-Holland Pub. Co., Amsterdam, 1965. Google Scholar
  33. Jean-Louis Krivine. A call-by-name lambda-calculus machine. In Higher Order and Symbolic Computation, 2004. URL: https://doi.org/10.1007/s10990-007-9018-9.
  34. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. URL: https://doi.org/10.1073/pnas.50.5.869.
  35. Robert S. Lubarsky and Michael Rathjen. Realizability models separating various fan theorems. In Paola Bonizzoni, Vasco Brattka, and Benedikt Löwe, editors, The Nature of Computation. Logic, Algorithms, Applications, pages 306-315, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39053-1_35.
  36. Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2), 2011. URL: https://doi.org/10.2168/LMCS-7(2:2)2011.
  37. Alexandre Miquel. Implicative algebras: a new foundation for realizability and forcing. Mathematical Structures in Computer Science, 30(5), 2020. URL: https://doi.org/10.1017/S0960129520000079.
  38. Étienne Miquey. A sequent calculus with dependent types for classical arithmetic. In LICS 2018. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209199.
  39. Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in mathematical logic. Springer, 2 edition, 1999. URL: https://doi.org/10.1017/CBO9780511581007.
  40. A.S. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1988. URL: https://doi.org/10.1016/S0049-237X(09)70529-4.
  41. Mark van Atten and Dirk van Dalen. Arguments for the continuity principle. Bulletin of Symbolic Logic, 8(3):329-347, 2002. URL: https://doi.org/10.2178/bsl/1182353892.
  42. Jaap van Oosten. Partial Combinatory Algebras of Functions. Notre Dame Journal of Formal Logic, 52(4):431-448, 2011. URL: https://doi.org/10.1215/00294527-1499381.
  43. Wim Veldman. On some of brouwer’s axioms. The Bulletin of Symbolic Logic, 31(1):pp. 1-52, 2025. URL: https://doi.org/10.1017/bsl.2024.52.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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