Document Open Access Logo

Generalized Decidability via Brouwer Trees

Authors Tom de Jong , Nicolai Kraus , Aref Mohammadzadeh , Fredrik Nordvall Forsberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.59.pdf
  • Filesize: 0.92 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Decidability in constructive mathematics
  • homotopy type theory
  • ordinals
  • Brouwer trees
  • countable choice

Metrics

Abstract

In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer tree ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for an ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀ i ∈ ℕ. P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.

Cite As Get BibTex

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg. Generalized Decidability via Brouwer Trees. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 59:1-59:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.59

Author Details

Tom de Jong
  • School of Computer Science, University of Nottingham, UK
Nicolai Kraus
  • School of Computer Science, University of Nottingham, UK
Aref Mohammadzadeh
  • School of Computer Science, University of Nottingham, UK
Fredrik Nordvall Forsberg
  • Computer & Information Sciences, University of Strathclyde, Glasgow, UK

Funding

  • de Jong, Tom: Royal Society [URF\R1\191055, URF\R\241007].
  • Kraus, Nicolai: Royal Society [URF\R1\191055, URF\R\241007], Engineering and Physical Sciences Research Council [EP/Z000602/1].
  • Nordvall Forsberg, Fredrik: Engineering and Physical Sciences Research Council [EP/Y000455/2].

Acknowledgements

We are grateful to Chuangjie Xu for early discussions on the topic of α-decidability.

Supplementary Materials

References

  1. Peter Aczel and Michael Rathjen. Notes on constructive set theory. Book draft, available at: https://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010.
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2018), volume 10803 of Lecture Notes in Computer Science, pages 293-310. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
  3. Andrej Bauer. First steps in synthetic computability theory. In Martín Escardó, Achim Jung, and Michael Mislove, editors, Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), volume 155 of Electronic Notes in Theoretical Computer Science, pages 5-31. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  4. Stefano Berardi and Ugo de’Liguoro. Toward the interpretation of non-constructive reasoning as non-monotonic learning. Information and Computation, 207(1):63-81, 2009. URL: https://doi.org/10.1016/j.ic.2008.10.003.
  5. Ana Bove and Venanzio Capretta. Modelling general recursion in type theory. Mathematical Structures in Computer Science, 15(4):671-708, 2005. URL: https://doi.org/10.1017/s0960129505004822.
  6. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, volume 97 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1987. URL: https://doi.org/10.1017/CBO9780511565663.
  7. Wilfried Buchholz. Notation systems for infinitary derivations. Archive for Mathematical Logic, 30:227-296, 1991. URL: https://doi.org/10.1007/BF01621472.
  8. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science, 29(1):67-92, 2019. URL: https://doi.org/10.1017/S0960129517000184.
  9. Alonzo Church. The constructive second number class. Bulletin of the American Mathematical Society, 44(4):224-232, 1938. URL: https://doi.org/10.1090/s0002-9904-1938-06720-1.
  10. Thierry Coquand, Peter Hancock, and Anton Setzer. Ordinals in type theory. Invited talk at Computer Science Logic (CSL), 1997. URL: http://www.cse.chalmers.se/~coquand/ordinal.ps.
  11. Tom de Jong. Semidecidability: Constructive taboos, choice principles and closure properties, 2022. Agda development. URL: https://martinescardo.github.io/TypeTopology/NotionsOfDecidability.SemiDecidable.html.
  12. Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, and Chuangjie Xu. Constructive Notions of Ordinals in Homotopy Type Theory. Software, swhId: https://archive.softwareheritage.org/swh:1:snp:af7a3d40f000eeb74aa0f06222f84f76e2046841 (visited on 2026-06-29). URL: https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott.git, URL: https://doi.org/10.4230/artifacts.26786.
  13. Martín Escardó. Synthetic topology of data types and classical spaces. In Josée Desharnais and Prakash Panangaden, editors, Proceedings of the Workshop on Domain Theoretic Methods for Probabilistic Processes, volume 87 of Electronic Notes in Theoretical Computer Science, pages 21-156. Elsevier, 2004. URL: https://doi.org/10.1016/j.entcs.2004.09.017.
  14. Martin Escardo. Quasidecidable propositions. Agda code with comments, 2020. URL: https://cs.bham.ac.uk/~mhe/TypeTopology/NotionsOfDecidability.QuasiDecidable.html.
  15. Martín H. Escardó. Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. The Journal of Symbolic Logic, 78(3):764-784, 2013. URL: https://doi.org/10.2178/jsl.7803040.
  16. Martín H Escardó and Cory M Knapp. Partial elements and recursion via dominances in univalent type theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.21.
  17. Martín Hötzel Escardó et al. Ordinals in univalent type theory in Agda notation. Agda development, HTML rendering available at: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.index.html, Since 2018. URL: https://github.com/martinescardo/TypeTopology.
  18. Gaëtan Gilbert. Formalising real numbers in homotopy type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 112-124, 2017. URL: https://doi.org/10.1145/3018610.3018614.
  19. E Mark Gold. Limiting recursion. The Journal of Symbolic Logic, 30(1):28-48, 1965. URL: https://doi.org/10.2307/2270580.
  20. Robin J. Grayson. Constructive well‐orderings. Mathematical Logic Quarterly, 28(33-38):495-504, 1982. URL: https://doi.org/10.1002/malq.19820283304.
  21. Robin John Grayson. Intuitionistic set theory. PhD thesis, University of Oxford, 1978. URL: https://doi.org/10.5287/ORA-AZGXAYAOR.
  22. Joel David Hamkins and Andy Lewis. Infinite time turing machines. The Journal of Symbolic Logic, 65(2):567-604, 2000. URL: https://doi.org/10.2307/2586556.
  23. Susumu Hayashi and Masahiro Nakata. Towards limit computable mathematics. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs (TYPES 2000), volume 2277 of Lecture Notes in Computer Science, pages 125-144. Springer-Verlag, 2000. URL: https://doi.org/10.1007/3-540-45842-5_9.
  24. Matt Hendtlass and Robert Lubarsky. Separating fragments of WLEM, LPO, and MP. The Journal of Symbolic Logic, 81(4):1315-1343, 2016. URL: https://doi.org/10.1017/jsl.2016.38.
  25. Stephen C. Kleene. On notations for ordinal numbers. The Journal of Symbolic Logic, 3(4):150-155, 1938. URL: https://doi.org/10.2307/2267778.
  26. Nicolai Kraus, Martin Escardó, Thierry Coquand, and Thorsten Altenkirch. Generalizations of Hedberg’s theorem. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications (TLCA 2013), volume 7941 of Lecture Notes in Computer Science, pages 173-188. Springer, Berlin, Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_14.
  27. Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting constructive notions of ordinals in homotopy type theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 202, pages 70:1-70:16, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.70.
  28. Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Decidability and semidecidability via ordinals. In TYPES 2022, Nantes, France, 2022. Available at URL: https://nicolaikraus.github.io/docs/decidabilityViaOrdinals.pdf.
  29. Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Type-theoretic approaches to ordinals. Theoretical Computer Science, 957:113843, 2023. URL: https://doi.org/10.1016/j.tcs.2023.113843.
  30. D. H. J Polymath. The "bounded gaps between primes" Polymath project. Newsletter of the European Mathematical Society, 94:13-23, 2014. Google Scholar
  31. William C. Powell. Extending Gödel’s negative interpretation to ZF. The Journal of Symbolic Logic, 40(2):221-229, 1975. URL: https://doi.org/10.1017/jsl.2017.84.
  32. Giuseppe Rosolini. Continuity and Effectiveness in Topoi. Phd thesis, University of Oxford, 1986. Google Scholar
  33. Kurt Schütte. Proof Theory, volume 225 of Grundlehren der mathematischen Wissenschaften. Springer-Verlag, 1977. URL: https://doi.org/10.1007/978-3-642-66473-1.
  34. Andrew W Swan. Choice, collection and covering in cubical sets. Talk at Homotopy Type Theory Electronic Seminar Talks (HoTTEST), online, 2019. URL: https://www.math.uwo.ca/faculty/kapulkin/seminars/hottestfiles/Swan-2019-11-06-HoTTEST.pdf.
  35. Andrew W Swan. Counterexamples in cubical sets. Talk at Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism, Stockholm, Sweden, 2019. URL: https://logic.math.su.se/mloc-2019/slides/Swan-mloc-2019-slides.pdf.
  36. Gaisi Takeuti. Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1987. Reprinted by Dover Publications in 2013. Google Scholar
  37. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
  38. Niccolò Veltri. A type-theoretical study of nontermination. PhD thesis, Tallinn University of Technology, 2017. Google Scholar
  39. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming, 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  40. Yitang Zhang. Bounded gaps between primes. Annals of Mathematics, 179:1121-1174, 2014. URL: https://doi.org/10.4007/annals.2014.179.3.7.
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