pith. sign in

arxiv: 2602.10844 · v2 · pith:CRS7O6MVnew · submitted 2026-02-11 · 💻 cs.LO · math.LO

Generalized Decidability via Brouwer Trees

Tom de Jong , Nicolai Kraus , Aref Mohammadzadeh , Fredrik Nordvall Forsberg This is my paper

Pith reviewed 2026-05-16 03:05 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords decidabilityBrouwer treeshomotopy type theoryconstructive mathematicssemidecidabilityordinal hierarchycountable quantifiersCubical Agda
0
0 comments X

The pith

Using Brouwer trees, countable meets of semidecidable properties are ω²-decidable in homotopy type theory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a framework for graded decidability in constructive mathematics by defining what it means for a proposition to be α-decidable for a Brouwer ordinal α. This generalizes the usual notions of decidability and semidecidability. It proves closure under conjunction for all α and gives specific bounds for disjunction and quantifiers. In particular, the universal quantification over all natural numbers of semidecidable properties turns out to be decidable at level ω². All results are formalized in Cubical Agda.

Core claim

The central discovery is a hierarchy of decidability levels indexed by Brouwer ordinals where α-decidability means a property can be decided using a Brouwer tree of height α. The key result is that if each P(i) for i in natural numbers is semidecidable, then the conjunction over all i of P(i) is ω²-decidable. Analogous results are shown for disjunctions and higher quantifiers.

What carries the argument

α-decidability defined using Brouwer trees, which provide a way to measure the height or complexity of the decision process in a constructive setting.

If this is right

  • If each P(i) is semidecidable then ∀i. P(i) is ω²-decidable.
  • α-decidable propositions are closed under binary conjunction for any Brouwer ordinal α.
  • Similar closure results hold for countable joins under appropriate ordinal bounds.
  • The framework interacts with countable choice in specific ways.
  • These properties can be iterated for higher quantifiers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This grading might allow distinguishing different levels of almost decidable properties in program verification.
  • Connections could be explored to other ordinal analyses in proof theory or computability theory.
  • Examples in type theory could be checked to see if the ω² bound is tight for some common properties.

Load-bearing premise

The definition of α-decidability via Brouwer trees forms a meaningful hierarchy that refines the classical decidable versus semidecidable distinction in a useful way.

What would settle it

Finding a family of semidecidable properties whose universal quantification cannot be decided by any Brouwer tree of height less than or equal to ω², or showing that the closure under conjunction fails for some α.

read the original 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 ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is $\alpha$-decidable, for a Brouwer ordinal $\alpha$, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that $\alpha$-decidable propositions are closed under binary conjunction, and discuss for which $\alpha$ they are closed under binary disjunction. We prove that if each $P(i)$ is semidecidable, then the countable meet $\forall i\in \mathbb N. P(i)$ is $\omega^2$-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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces a framework in homotopy type theory for α-decidability of propositions, parameterized by Brouwer ordinals. It shows that this notion generalizes decidability (at finite ordinals) and semidecidability (at ω), proves closure under binary conjunction (and discusses disjunction), and establishes that the countable meet of semidecidable predicates is ω²-decidable, with analogous results for countable joins and iterated quantifiers. All results are formalized in Cubical Agda.

Significance. If the results hold, the work supplies a precise, ordinal-indexed hierarchy of decidability levels inside constructive mathematics. The machine-checked Cubical Agda development supplies strong evidence for the central claims and the inductive constructions on Brouwer trees.

minor comments (2)
  1. [Abstract] The abstract states that 'similar results' hold for countable joins and iterated quantifiers; a single sentence in the introduction listing the exact ordinals obtained for each case would improve immediate readability.
  2. [Section 2] In the definition of α-decidability via Brouwer trees, the base case for the successor ordinal is clear, but an explicit remark on how the limit case is handled constructively would help readers unfamiliar with the ordinal arithmetic in HoTT.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and the recommendation to accept. The provided summary accurately reflects the framework for α-decidability parameterized by Brouwer ordinals, the generalizations of decidability and semidecidability, the closure properties, the results on countable meets and joins, and the Cubical Agda formalization.

Circularity Check

0 steps flagged

No significant circularity; results machine-verified in Cubical Agda

full rationale

The paper defines α-decidability using Brouwer ordinals in homotopy type theory and proves closure properties plus results on countable meets/joins/quantifiers. All claims are supported by a complete Cubical Agda formalization, which constitutes independent machine-checked evidence rather than self-referential fitting or load-bearing self-citation. No step reduces a prediction or theorem to its own inputs by construction; the framework specializes correctly to decidability at finite ordinals and semidecidability at ω without circular renaming or ansatz smuggling. This is a standard self-contained constructive development.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the background of homotopy type theory and the constructive definition of Brouwer ordinals; no free parameters are fitted and no new entities are postulated.

axioms (2)
  • standard math Homotopy type theory
    The entire development takes place inside HoTT, including univalence and higher inductive types.
  • domain assumption Brouwer ordinals defined as trees
    Brouwer ordinals are used to index the decidability levels; their standard constructive definition is assumed.

pith-pipeline@v0.9.0 · 5484 in / 1327 out tokens · 172291 ms · 2026-05-16T03:05:59.825423+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    Notes on constructive set theory

    Peter Aczel and Michael Rathjen. Notes on constructive set theory. Book draft, available at: https://www1.maths.leeds.ac.uk/~rathjen/book.pdf, 2010

    work page 2010

  2. [2]

    Quotient inductive-inductive types

    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 , page 293–310. Springer, 2018. doi:10.1007/ 978-3-...

    work page 2018

  3. [3]

    First steps in synthetic computability theory

    Andrej Bauer. First steps in synthetic computability theory. In Mart´ ın Escard´ o, 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. doi:10.1016/j.entcs.2005.11.049

    work page doi:10.1016/j.entcs.2005.11.049 2006

  4. [4]

    Toward the interpretation of non-constructive reasoning as non-monotonic learning

    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. doi:10.1016/ j.ic.2008.10.003

    work page 2009

  5. [5]

    Modelling general recursion in type theory

    Ana Bove and Venanzio Capretta. Modelling general recursion in type theory. Mathematical Structures in Computer Science , 15(4):671–708, 2005. doi:10.1017/s0960129505004822

    work page doi:10.1017/s0960129505004822 2005

  6. [6]

    Varieties of Constructive Mathematics , volume 97 of London Mathematical Society Lecture Note Series

    Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics , volume 97 of London Mathematical Society Lecture Note Series . Cambridge University Press, 1987. doi:10.1017/CBO9780511565663

    work page doi:10.1017/cbo9780511565663 1987

  7. [7]

    Notation systems for infinitary derivations

    Wilfried Buchholz. Notation systems for infinitary derivations. Archive for Mathematical Logic, 30:227–296, 1991. doi:10.1007/BF01621472

    work page doi:10.1007/bf01621472 1991

  8. [8]

    Quotienting the delay monad by weak bisimilarity

    James Chapman, Tarmo Uustalu, and Niccol` o Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science , 29(1):67–92, 2019. doi: 10.1017/S0960129517000184

    work page doi:10.1017/s0960129517000184 2019

  9. [9]

    The constructive second number class

    Alonzo Church. The constructive second number class. Bulletin of the American Mathematical Society, 44(4):224–232, 1938. doi:10.1090/s0002-9904-1938-06720-1

    work page doi:10.1090/s0002-9904-1938-06720-1 1938

  10. [10]

    Ordinals in type theory

    Thierry Coquand, Peter Hancock, and Anton Setzer. Ordinals in type theory. Invited talk at Computer Science Logic (CSL), 1997. http://www.cse.chalmers.se/~coquand/ordinal.ps

    work page 1997

  11. [11]

    Semidecidability: Constructive taboos, choice principles and closure prop- erties, 2022

    Tom de Jong. Semidecidability: Constructive taboos, choice principles and closure prop- erties, 2022. Agda development. URL: https://martinescardo.github.io/TypeTopology/ NotionsOfDecidability.SemiDecidable.html

    work page 2022

  12. [12]

    Synthetic topology of data types and classical spaces

    Mart´ ın Escard´ o. Synthetic topology of data types and classical spaces. In Jos´ ee 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. doi:10.1016/j.entcs.2004.09.017

    work page doi:10.1016/j.entcs.2004.09.017 2004

  13. [13]

    Quasidecidable propositions

    Martin Escardo. Quasidecidable propositions. Agda code with comments, 2020. URL: https: //cs.bham.ac.uk/~mhe/TypeTopology/NotionsOfDecidability.QuasiDecidable.html

    work page 2020

  14. [14]

    Partial elements and recursion via dominances in univalent type theory

    Mart´ ın H Escard´ o 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¨ ur Inform...

    work page doi:10.4230/lipics.csl.2017.21 2017

  15. [15]

    Ordinals in univalent type theory in Agda notation

    Mart´ ın H¨ otzel Escard´ o et al. Ordinals in univalent type theory in Agda notation. Agda de- velopment, HTML rendering available at: https://www.cs.bham.ac.uk/~mhe/TypeTopology/ Ordinals.index.html, Since 2018. URL: https://github.com/martinescardo/TypeTopology

    work page 2018

  16. [16]

    The HoTT Library: A Formalizatio n of Homotopy Type Theory in Coq

    Ga¨ etan Gilbert. Formalising real numbers in homotopy type theory. InProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , pages 112–124, 2017. doi:10.1145/3018610.3018614

    work page doi:10.1145/3018610.3018614 2017

  17. [17]

    Limiting recursion

    E Mark Gold. Limiting recursion. The Journal of Symbolic Logic , 30(1):28–48, 1965. doi: 10.2307/2270580

    work page doi:10.2307/2270580 1965

  18. [18]

    Robin J. Grayson. Constructive well-orderings. Mathematical Logic Quarterly, 28(33–38):495– 504, 1982. doi:10.1002/malq.19820283304

    work page doi:10.1002/malq.19820283304 1982

  19. [19]

    Intuitionistic set theory

    Robin John Grayson. Intuitionistic set theory . PhD thesis, University of Oxford, 1978. doi: 10.5287/ORA-AZGXAYAOR. GENERALIZED DECIDABILITY VIA BROUWER TREES 23

    work page doi:10.5287/ora-azgxayaor 1978

  20. [20]

    Infinite time turing machines

    Joel David Hamkins and Andy Lewis. Infinite time turing machines. The Journal of Symbolic Logic, 65(2):567–604, 2000. doi:10.2307/2586556

    work page doi:10.2307/2586556 2000

  21. [21]

    Towards limit computable mathematics

    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. doi:10.1007/3-540-45842-5_9

    work page doi:10.1007/3-540-45842-5_9 2000

  22. [22]

    Separating fragments of WLEM, LPO, and MP

    Matt Hendtlass and Robert Lubarsky. Separating fragments of WLEM, LPO, and MP. The Journal of Symbolic Logic , 81(4):1315–1343, 2016. doi:10.1017/jsl.2016.38

    work page doi:10.1017/jsl.2016.38 2016

  23. [23]

    Stephen C. Kleene. On notations for ordinal numbers. The Journal of Symbolic Logic, 3(4):150– 155, 1938. doi:10.2307/2267778

    work page doi:10.2307/2267778 1938

  24. [24]

    Generalizations of hedberg’s theorem

    Nicolai Kraus, Martin Escard´ o, 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. doi:10.1007/978-3-642-38946-7_14

    work page doi:10.1007/978-3-642-38946-7_14 2013

  25. [25]

    Connecting constructive notions of ordinals in homotopy type theory

    Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting constructive notions of ordinals in homotopy type theory. In 46th International Symposium on Mathematical Foun- dations of Computer Science (MFCS 2021) , Leibniz International Proceedings in Informatics (LIPIcs), Vol. 202, pages 70:1–70:16, 2021. doi:10.4230/LIPIcs.MFCS.2021.70

    work page doi:10.4230/lipics.mfcs.2021.70 2021

  26. [26]

    Decidability and semidecidability via ordinals

    Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Decidability and semidecidability via ordinals. In TYPES 2022 , Nantes, France, 2022. Available at https://nicolaikraus. github.io/docs/decidabilityViaOrdinals.pdf

    work page 2022

  27. [27]

    Type-theoretic approaches to ordinals

    Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Type-theoretic approaches to ordinals. Theoretical Computer Science, 957:113843, 2023. arXiv:2208.03844, doi:10.1016/ j.tcs.2023.113843

    work page arXiv 2023

  28. [28]

    bounded gaps between primes

    D. H. J Polymath. The “bounded gaps between primes” Polymath project. Newsletter of the European Mathematical Society, 94:13–23, 2014

    work page 2014

  29. [29]

    William C. Powell. Extending G¨ odel’s negative interpretation to ZF.The Journal of Symbolic Logic, 40(2):221–229, 1975. doi:10.1017/jsl.2017.84

    work page doi:10.1017/jsl.2017.84 1975

  30. [30]

    Continuity and Effectiveness in Topoi

    Giuseppe Rosolini. Continuity and Effectiveness in Topoi . Phd thesis, University of Oxford, 1986

    work page 1986

  31. [31]

    Springer-Verlag, 1977

    Kurt Sch¨ utte.Proof Theory, volume 225 of Grundlehren der mathematischen Wissenschaften . Springer-Verlag, 1977. doi:10.1007/978-3-642-66473-1

    work page doi:10.1007/978-3-642-66473-1 1977

  32. [32]

    Choice, collection and covering in cubical sets

    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

    work page 2019

  33. [33]

    Counterexamples in cubical sets

    Andrew W Swan. Counterexamples in cubical sets. Talk at Mathematical Logic and Con- structivity: The Scope and Limits of Neutral Constructivism , Stockholm, Sweden, 2019. URL: https://logic.math.su.se/mloc-2019/slides/Swan-mloc-2019-slides.pdf

    work page 2019

  34. [34]

    North-Holland, second edition, 1987

    Gaisi Takeuti.Proof Theory, volume 81 ofStudies in Logic and the Foundations of Mathematics. North-Holland, second edition, 1987. Reprinted by Dover Publications in 2013

    work page 1987

  35. [35]

    Homotopy Type Theory: Univalent Foundations of Mathematics

    The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/ book/

    work page 2013

  36. [36]

    PhD thesis, Tallinn University of Technology, 2017

    Niccol` o Veltri.A type-theoretical study of nontermination . PhD thesis, Tallinn University of Technology, 2017

    work page 2017

  37. [37]

    Bounded gaps between primes

    Yitang Zhang. Bounded gaps between primes. Annals of Mathematics , 179:1121–1174, 2014. doi:10.4007/annals.2014.179.3.7. School of Computer Science, University of Nottingham, UK Email address: {tom.dejong, nicolai.kraus, aref.mohammadzadeh }@nottingham.ac.uk URL: https://tdejong.com https://nicolaikraus.github.io https://arefmohammadzadeh.com Department o...

    work page doi:10.4007/annals.2014.179.3.7 2014