Document Open Access Logo

Not Choosing Is Still a Choice: Constructive mathematics without any choice

Authors Martin Baillon , Yannick Forster , Dominik Kirst , Assia Mahboubi , Pierre-Marie Pédrot

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.5.pdf
  • Filesize: 1.08 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • Axiom of Choice
  • Constructive Mathematics
  • Type Theory

Metrics

Abstract

The axiom of choice (AC) states that every total relation contains a function. It enjoys a pivotal role in both classical and constructive dialects of mathematics. In the former, it is seen as a useful closure property invoked especially in set-theoretic contexts, in the latter it is seen either as a tautology, following from a constructive reading of totality proofs, or as a taboo, as by an extensional reading of totality proofs it enforces full classical logic. It has therefore been debated how much of AC should be accepted in constructive foundations and authors like Richman argued for 
"Constructive mathematics without choice" 
where even countable choice, not immediately jeopardising constructive reasoning, is avoided.
With this paper, we propose a continuation of Richman’s programme of more radical extent and systematically study constructive foundations absent of countable, unique, or quantifier-free choice principles as well as the spurious fragments of (the actual) AC in form of extensionality principles: 
"Constructive mathematics without any choice" 
We argue that such a minimalistic setting is advantageous, for instance for studies in constructive reverse mathematics and synthetic computability theory. Apart from these programmatic considerations and a careful encyclopedia of choice principles, we revisit and refine several results from the literature: We show that already the partition principle (a consequence of AC of unknown strength) implies the excluded middle, that already logically decidable (inductive) equality of propositions implies proof irrelevance, and that function inversion principles such as the Cantor-Bernstein theorem not only rely on the excluded middle but also on unique choice. To the best of our knowledge, the latter is the first reverse mathematics result regarding the full axiom of unique choice, enabled by our minimal setting. Implementing such a minimalistic foundation, the proofs of all our results have been mechanised with the Rocq prover.

Cite As Get BibTex

Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, and Pierre-Marie Pédrot. Not Choosing Is Still a Choice: Constructive mathematics without any choice. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.5

Author Details

Martin Baillon
  • Inria, Paris, France
Yannick Forster
  • Inria, Paris, France
Dominik Kirst
  • Inria, Paris, France
Assia Mahboubi
  • Inria, Rennes, France
Pierre-Marie Pédrot
  • Inria, Rennes, France

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreements No. 101001995 and 101167526). Dominik Kirst received funding from the European Union’s Horizon research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101152583.

Acknowledgements

We want to thank Timothée Huneau and Sam van Gool for discussions about the partition principle which sparked this work, Hugo Herbelin for discussions and his work on the ChoiceFacts file of Rocq’s standard library, Nicolas Tabareau for discussions about the relation between accessibility proofs and quantifier-free choice, Milly Maietti for pointers to the literature of minimalist foundations, Martin Escardó for discussions of the Cantor-Bernstein theorem, as well as Meven Lennon-Bertrand, Thierry Coquand, Tom de Jong, and Andrej Bauer for discussions on Coquand’s theorem. We received helpful feedback on this work from participants of Dagstuhl Seminar 26121: Proof Systems in Actual Practice: Reasoning and Computation.

Supplementary Materials

References

  1. Andreas Abel and Thierry Coquand. Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Log. Methods Comput. Sci., 16(2), 2020. URL: https://doi.org/10.23638/LMCS-16(2:14)2020.
  2. Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach. An arithmetical hierarchy of the law of excluded middle and related principles. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 192-201. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319613.
  3. Franco Barbanera and Stefano Berardi. Proof-irrelevance out of excluded-middle and choice in the calculus of constructions. Journal of Functional Programming, 6(3):519-525, 1996. URL: https://doi.org/10.1017/S0956796800001829.
  4. Josef Berger, Hajime Ishihara, and Peter Schuster. The weak koenig lemma, brouwer’s fan theorem, de morgan’s law, and dependent choice. Reports Math. Log., 47:63-86, 2012. URL: https://rml.tcs.uj.edu.pl/rml-47/3-Schuster.pdf.
  5. Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the quintic formalized in dependent type theory. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference), June 29 - July 1, 2021, volume 193 of LIPIcs, pages 8:1-8:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.8.
  6. Errett Bishop. Foundations of Constructive Analysis. Mcgraw-Hill, New York, NY, USA, 1967. Google Scholar
  7. Luitzen Egbertus Jan Brouwer. De onbetrouwbaarheid der logische principes. Tijdschrift voor Wijsbegeerte, 2:152-158, 1908. (In Dutch). Google Scholar
  8. Ulrik Buchholtz, Tom De Jong, and Egbert Rijke. Epimorphisms and acyclic types in univalent foundations. The Journal of Symbolic Logic, pages 1-36, February 2025. URL: https://doi.org/10.1017/jsl.2024.76.
  9. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli. Separating Markov’s Principles. In LICS, pages 28:1-28:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662104.
  10. Paul J. Cohen. The independence of the axiom of choice, 1963. Google Scholar
  11. Thierry Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, 1989. URL: https://hal.inria.fr/inria-00075471.
  12. Thierry Coquand and Gérard P Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  13. Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176, August 1975. URL: https://doi.org/10.2307/2039868.
  14. Martín Hötzel Escardó. The Cantor–Schröder–Bernstein theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3):363-366, 2021. URL: https://doi.org/10.1007/s40062-021-00284-6.
  15. Solomon Feferman. Constructive theories of functions and classes. In Maurice Boffa, Dirk van Dalen, and Kenneth Mcaloon, editors, Logic Colloquium '78, volume 97 of Studies in Logic and the Foundations of Mathematics, pages 159-224. Elsevier, 1979. URL: https://doi.org/10.1016/S0049-237X(08)71625-2.
  16. Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter. Definitional Proof Irrelevance Made Accessible. to be published at LICS 2026, 2026. URL: https://hal.science/hal-05474391.
  17. Yannick Forster. Church’s thesis and related axioms in Coq’s type theory. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 21:1-21:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
  18. Yannick Forster and Felix Jahn. Constructive and synthetic reducibility degrees: Post’s problem for many-one and truth-table reducibility in Coq. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, Warsaw, Poland, February 13-16, 2023, volume 252 of LIPIcs, pages 21:1-21:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.21.
  19. Yannick Forster, Felix Jahn, and Gert Smolka. A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl). In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’23, pages 159-166. ACM, January 2023. URL: https://doi.org/10.1145/3573105.3575690.
  20. Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, Naples, Italy, February 19-23, 2024, volume 288 of LIPIcs, pages 29:1-29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.29.
  21. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’19, pages 38-51. ACM, January 2019. URL: https://doi.org/10.1145/3293880.3294091.
  22. Yannick Forster and Gert Smolka. Call-by-Value Lambda Calculus as a Model of Computation in Coq. Journal of Automated Reasoning, 63(2):393-413, October 2018. URL: https://doi.org/10.1007/s10817-018-9484-2.
  23. Makoto Fujiwara. Δ⁰₁ variants of the law of excluded middle and related principles. Archive for Mathematical Logic, 61(7–8):1113-1127, April 2022. URL: https://doi.org/10.1007/s00153-022-00827-5.
  24. Makoto Fujiwara and Ulrich Kohlenbach. Interrelation between weak fragments of double negation shift and related principles. The Journal of Symbolic Logic, 83(3):991-1012, September 2018. URL: https://doi.org/10.1017/jsl.2017.63.
  25. Gaëtan Gilbert. A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle). PhD thesis, Mines ParisTech, France, 2019. URL: https://tel.archives-ouvertes.fr/tel-03236271.
  26. Jean-Yves Girard. Une extension de l'interprétation de gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63-92. North-Holland, 1972. Google Scholar
  27. Kurt Gödel. The consistency of the axiom of choice and of the generalized Continuum-Hypothesis. Proceedings of the National Academy of Sciences, 24(12):556-557, 1938. URL: https://doi.org/10.1073/pnas.24.12.556.
  28. N. Goodman and J. Myhill. Choice implies excluded middle. Mathematical Logic Quarterly, 24(25–30):461-461, January 1978. URL: https://doi.org/10.1002/malq.19780242514.
  29. Robert Harper and John C. Mitchell. Parametricity and variants of girard’s J operator. Inf. Process. Lett., 70(1):1-5, 1999. URL: https://doi.org/10.1016/S0020-0190(99)00036-8.
  30. Michael Hedberg. A coherence theorem for Martin-Löf’s type theory. Journal of Functional Programming, 8(4):413-436, 1998. URL: https://doi.org/10.1017/S0956796898003153.
  31. Arend Heyting. Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preußischen Akademie der Wissenschaften. Physikalisch-mathematische Klasse, pages 42-56, 1930. Google Scholar
  32. Masasi Higasikawa. Partition principles and infinite sums of cardinal numbers. Notre Dame Journal of Formal Logic, 36(3):425-434, 1995. URL: https://doi.org/10.1305/NDJFL/1040149358.
  33. Martin Hofmann. Extensional Constructs in Intensional Type Theory. Springer London, 1997. URL: https://doi.org/10.1007/978-1-4471-0963-1.
  34. Paul Howard and Jean Rubin. Consequences of the Axiom of Choice. American Mathematical Society, June 1998. URL: https://doi.org/10.1090/surv/059.
  35. Antonius J. C. Hurkens. A simplification of Girard’s paradox, pages 266-278. Springer Berlin Heidelberg, 1995. URL: https://doi.org/10.1007/bfb0014058.
  36. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientae, (CS 6):43-59, 2006. URL: https://doi.org/10.4000/philosophiascientiae.406.
  37. Dominik Kirst. Mechanised Metamathematics: An Investigation of First-Order Logic and Set Theory in Constructive Type Theory. PhD thesis, Saarland University, 2022. URL: https://doi.org/10.22028/D291-39150.
  38. 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. IEEE, June 2025. URL: https://doi.org/10.1109/lics65433.2025.00073.
  39. Stephen Cole Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41, January 1943. URL: https://doi.org/10.2307/1990131.
  40. Stephen Cole Kleene and Richard Eugene Vesley. The foundations of intuitionistic mathematics: especially in relation to recursive functions, 1965. Google Scholar
  41. Dominique Larchey-Wendling. Typing Total Recursive Functions in Coq, pages 371-388. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_24.
  42. Francis William Lawvere. Diagonal arguments and cartesian closed categories. In Lecture Notes in Mathematics, pages 134-145. Springer, 1969. URL: https://doi.org/10.1007/bfb0080769.
  43. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  44. Maria Emilia Maietti. About Effective Quotients in Constructive Type Theory, pages 166-178. Springer Berlin Heidelberg, 1999. URL: https://doi.org/10.1007/3-540-48167-2_12.
  45. Maria Emilia Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, September 2009. URL: https://doi.org/10.1016/j.apal.2009.01.006.
  46. Maria Emilia Maietti and Giovanni Sambin. Toward a minimalistic foundation for constructive mathematics. In Laura Crosilla and Peter M. Schuster, editors, From sets and types to topology and analysis - Towards practicable foundations for constructive mathematics, volume 48 of Oxford logic guides. Oxford University Press, 2005. Google Scholar
  47. Per Martin-Löf. Notes on Constructive Analysis. Almqvist & Wiksell, Stockholm, 1968. Google Scholar
  48. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in proof theory. Bibliopolis, 1984. Google Scholar
  49. Per Martin-Löf. 100 years of Zermelo’s axiom of choice: what was the problem with it? The Computer Journal, 49(3):345-350, December 2005. URL: https://doi.org/10.1093/comjnl/bxh162.
  50. Joan Rand Moschovakis. Disjunction, existence and λ-eliminability in formalized intuitionistic analysis. PhD thesis, University of Wisconsin-Madison, Madison, WI, USA, 1965. Google Scholar
  51. Andrzej Mostowski. On definable sets of positive integers. Fundamenta Mathematicae, 34:81-112, 1947. URL: https://doi.org/10.4064/fm-34-1-81-112.
  52. John Myhill. Constructive set theory. Journal of Symbolic Logic, 40(3):347-382, September 1975. URL: https://doi.org/10.2307/2272159.
  53. Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  54. Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, and Éric Tanter. All your base are belong to us: Sort polymorphism for proof assistants. Proc. ACM Program. Lang., 9(POPL):2253-2281, 2025. URL: https://doi.org/10.1145/3704912.
  55. Cécilia Pradic and Chad E. Brown. Cantor-Bernstein implies Excluded Middle. CoRR, abs/1904.09193, 2019. URL: https://arxiv.org/abs/1904.09193.
  56. Cécilia Pradic. The myhill isomorphism theorem does not generalize much, 2025. URL: https://doi.org/10.48550/arXiv.2507.05028.
  57. Loïc Pujet and Nicolas Tabareau. Observational equality: now for good. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498693.
  58. Loïc Pujet and Nicolas Tabareau. Impredicative Observational Equality. Proc. ACM Program. Lang., 7(POPL):2171-2196, 2023. URL: https://doi.org/10.1145/3571739.
  59. Fred Richman. Constructive Mathematics without Choice. In Peter Schuster, Ulrich Berger, and Horst Osswald, editors, Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum, pages 199-205. Springer Netherlands, Dordrecht, 2001. URL: https://doi.org/10.1007/978-94-015-9757-9_17.
  60. The Rocq Development Team. The Rocq Prover, September 2025. URL: https://doi.org/10.5281/zenodo.17473943.
  61. Anne Sjerp Troelstra. Aspects of constructive mathematics. In Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 973-1052. North-Holland, Amsterdam, 1978. Google Scholar
  62. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. I. Studies in Logic and the Foundations of Mathematics, 26, 1988. Google Scholar
  63. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  64. Garyfallia Vafeiadou. A comparison of minimal systems for constructive analysis, 2018. URL: https://arxiv.org/abs/1808.00383.
  65. Mark van Atten. The Creating Subject, the Brouwer–Kripke Schema, and infinite proofs. Indagationes Mathematicae, 29(6):1565-1636, December 2018. URL: https://doi.org/10.1016/j.indag.2018.06.005.
  66. Wim Veldman. Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s alternative. Archive for Mathematical Logic, 53(5–6):621-693, June 2014. URL: https://doi.org/10.1007/s00153-014-0384-9.
  67. Louis Warren, Hannes Diener, and Maarten McKubre-Jordens. The drinker paradox and its dual. CoRR, abs/1805.06216, 2018. URL: https://arxiv.org/abs/1805.06216.
  68. Benjamin Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, Volume 4, Issue 3, September 2008. URL: https://doi.org/10.2168/lmcs-4(3:13)2008.
  69. Ernst Zermelo. Beweis, dass jede Menge wohlgeordnet werden kann. Mathematische Annalen, 59(4):514-516, 1904. URL: https://doi.org/10.1007/bf01445300.
  70. Ernst Zermelo. Untersuchungen über die grundlagen der mengenlehre. i. Mathematische Annalen, 65(2):261-281, 1908. URL: https://doi.org/10.1007/bf01449999.
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