Pith. sign in

REVIEW 2 major objections 4 minor 37 references

Generalized Decidability via Brouwer Trees

T0 review · 2 major / 4 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper introduces α-decidability via Brouwer ordinals and argues that every countable meet of semidecidable propositions — including the Twin Prime Conjecture — is ω²-decidable.

desk verdict The reader's central counterexample misses the mark, but the proof of Theorem 7.12 has a real gap; the main framework deserves a serious referee. read the letter →

arxiv 2602.10844 v3 pith:CRS7O6MV submitted 2026-02-11 cs.LO math.LO

Tom de Jong , Nicolai Kraus , Aref Mohammadzadeh , Fredrik Nordvall Forsberg This is my paper · ORCID
classification cs.LOmath.LO MSC 03F5503F50
keywords constructivemathematicshomotopytypetheoryBrouwerordinalsordinaldecidabilitysemidecidabilitycountablemeetsTwinPrimeConjectureCubicalAgda
topics The Twin Prime Conjecture
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper proposes a graded notion of decidability that goes beyond the binary decidable/semidecidable distinction, using Brouwer ordinals as the grading. A proposition is α-decidable when it is equivalent to some ordinal being at least α; with the right ordinal construction, ordinary decidability and semidecidability reappear as special cases. The central claim is that for any family P : N → Prop of semidecidable propositions, the countable meet ∀n.Pn is ω²-decidable, making conjectures like the Twin Prime Conjecture instances of this result. The paper also establishes closure properties for conjunctions, restricted disjunctions, countable joins, and a quantifier-alternation case, and analyzes the role of countable choice. A sympathetic reader would care because this offers a way to measure and compare the constructive difficulty of problems that are not semidecidable.

What carries the argument

The central object is the type Brw of Brouwer ordinals, a quotient inductive-inductive type with constructors zero, succ, and limit of strictly increasing sequences, together with a bisimilarity path constructor. Its order relation ≤ has the key property that finiteness is decidable and inequalities like limit f ≥ ω+1 are semidecidable. The paper also uses the characteristic ordinal Ψ(P) of a semidecidable family, built from normalized binary witnesses as Ψ(P) = limit(λn.Ψn(P)+n), where Ψn(P) measures the first n entries. Additional tools are the rounding functions ⇑ and ⇓, which allow restricting attention to limit ordinals, and the weak-constancy argument that lets functions out of truncat

What would settle it

Take the family P with P0 := ⊤ and Pi := ⊥ for all i>0. Compute its characteristic ordinal: Ψ(P) is at least ω² (because the first entry already contributes ω·2), while the shifted family λi.P_{i+1} has characteristic ordinal exactly ω. This directly refutes Lemma 7.7, the load-bearing step used to prove that ∀i.Pi is ω²-decidable.

Watch

Extended reading notes

Core claim

On the paper's own terms: a proposition P is α-decidable if there exists a Brouwer ordinal y such that P ↔ y ≥ α. Using the type Brw of Brouwer trees, whose limit constructor accepts only strictly increasing sequences, the paper shows that 1-decidability coincides with ordinary decidability and (ω+1)-decidability with semidecidability. The main theorem (Theorem 7.5) states that for a family P : N → Prop of semidecidable propositions, the countable meet ∀n.Pn is ω²-decidable. The proof constructs a characteristic ordinal Ψ(P) for such a family and establishes the equivalence ∀i.Pi ↔ Ψ(P) ≥ ω², relying on Lemma 7.7, which says that dropping a finite prefix does not push the characteristic ordi

Load-bearing premise

The proof of Theorem 7.5 relies on Lemma 7.7's claim that removing a finite prefix of a semidecidable family cannot reduce its characteristic ordinal below ω²; this claim is false for the family with P0 true and all later entries false, so the central equivalence is unsupported.

Editorial extensions

If this is right

  • The Twin Prime Conjecture becomes an instance of ω²-decidability: no single semidecision procedure need exist, but a search of length ω² would find a counterexample if one exists.
  • The negation of any semidecidable proposition is ω²-decidable, giving a general statement about the decidability of universal statements over the natural numbers.
  • Countable joins of semidecidable families are (ω·3)-decidable, and become semidecidable only under countable choice.
  • Assuming countable choice, every (ω·k)-decidable proposition is semidecidable, and every ω²-decidable proposition is equivalent to a countable meet of semidecidable propositions.
  • A search for a counterexample to the Twin Prime Conjecture is (ω²+ω)-decidable if the conjecture fails.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the main theorem survives scrutiny, the framework suggests a general recipe: any family of propositions with a uniform witness type yields an ordinal measuring how much nested search is needed, potentially connecting to infinite-time or limit-computable models.
  • The dependence on Lemma 7.7 means that a counterexample family such as P0 = true and Pi = false for i>0 would invalidate the equivalence ∀i.Pi ↔ Ψ(P) ≥ ω², even though the rest of the α-decidability hierarchy could remain intact.
  • The distinction between semidecidability and Sierpiński-semidecidability under countable choice hints that a choice-free variant of Brouwer trees could yield a cleaner theory of countable joins, a direction the paper leaves open.
  • Since all results are formalized in Cubical Agda, the formalization itself provides a concrete check: if the counterexample to Lemma 7.7 type-checks in the same framework, then the proof of Theorem 7.5 has a gap.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper introduces a synthetic hierarchy of decidability for propositions in homotopy type theory, parameterized by Brouwer ordinals (Brw). A proposition P is α-decidable if there is an ordinal x with P ↔ x ≥ α. The authors show that this notion generalizes ordinary decidability and semidecidability, prove closure properties for binary conjunctions and for restricted disjunctions, and construct a characteristic ordinal Ψ(P) for a countable family of semidecidable propositions. This is used to prove that the countable meet ∀n. Pn is ω²-decidable, that the countable join is (ω·3)-decidable, and that a quantifier-alternation instance is (ω²+ω)-decidable. Later sections connect the hierarchy to countable choice and Sierpiński-semidecidability. All results are claimed to be formalized in Cubical Agda.

Significance. If the central construction is correct, the paper offers a genuine refinement of the decidable/semidecidable dichotomy in a constructive setting, with an interesting connection between Brouwer ordinals and search depth. The claimed machine-checked formalization is a substantial asset, and the central theorem—countable meets of semidecidable families at level ω²—is nontrivial and suggestive. I checked the review's proposed counterexample to Lemma 7.7: it does not land, since a family with exactly P0 true and all later Pi false has Ψ(P)=ω·3<ω², so the hypothesis of Lemma 7.7 is not met. However, the proof of Theorem 7.12 applies equivalence (7) outside its domain of validity; this is a genuine gap, though it appears repairable by normalizing each row first. The paper's contribution remains significant if the repair is made.

major comments (2)
  1. [§7.5, proof of Theorem 7.12] The proof applies equivalence (7) to the family λn. P(n,m). But (7) was proved in §7.3 only for downwards-closed families (after Lemma 7.4(1)); λn. P(n,m) is not downwards-closed under the hypothesis P(n,m)→P(n,m+1), which is monotonicity in m, not n. The equivalence is false for arbitrary rows: take P(n,m) := 'n is even'. Each row is semidecidable, satisfies P(n,m)→P(n,m+1), and has Ψ(λn. P(n,m)) = ω² ≥ ω², yet ∀n. P(n,m) is false. The theorem can be repaired by first applying Lemma 7.4(1) to each row, letting Q_m(n) := ∀j≤n. P(j,m), proving Q_m(n)→Q_{m+1}(n), and then applying (7) to the Q_m; but as written the proof is unsupported.
  2. [§7.3, proof of Lemma 7.7] The step following (6) says 'Using Lemma 2.1(6) and cancellation of addition with ω' to derive Ψ_n(λi. P_{i+1}) ≥ ω·m. Right-cancellation of ω is not valid for Brw in general (e.g. (ω+1)+ω = ω+ω with ω+1 not ≤ ω), so the inference needs a proof. In the specific form α+ω+n ≥ ω·m+ω it is true, but only because n is finite; this should be stated explicitly. As written, the key step of this lemma, which is load-bearing for Theorem 7.5, is too compressed for a referee to verify.
minor comments (4)
  1. [Definition 3.3] The definition of s↑ should clarify the behavior after the first 1 has been found: the 'else' branch applies at later indices, so the sequence does not reset to ω. Otherwise the clause could be misread.
  2. [Lemma 7.4(1)] The displayed equivalence '∀k.Pk ↔ ∀k.Qk' should be parenthesized; as printed it is easy to misread as a pointwise equivalence.
  3. [Theorem 7.5, proof] The '→' direction is not literally immediate from Lemma 7.8: one must use that the assumption is ∀i.Pi and take the limit over all n. This should be said for clarity.
  4. [§7.5, proof of Theorem 7.12] If the theorem is repaired by normalizing rows, the phrase 'by the construction of (7)' should cite the normalized family Q_m explicitly, and the proof should not claim (7) for arbitrary rows.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the framework and characteristic ordinals are constructed and proved, not fitted; self-citations carry independent machine-checked support.

full rationale

None of the load-bearing steps reduces to its own input by construction. Definition 3.1 defines α-decidability as ∃y.(P ↔ α≤y), and Proposition 3.2 proves, rather than assumes, that this coincides with ordinary decidability and semidecidability. The characteristic ordinal Ψ(P) in Definition 7.3 is built from semidecidability witnesses through Ψn and a weak-constancy argument; the crucial equivalence (7) in Theorem 7.5 is derived via Lemmas 7.6–7.8, not inserted into the definition of Ψ. The paper's reliance on the Brouwer-tree framework of Kraus, Nordvall Forsberg, and Xu is a self-citation, but it is not an unverified circular chain: the framework is independently published and the present paper's results are formalized in Cubical Agda, so the cited infrastructure is machine-checked external evidence. The most apparent issue in the text is the proof sketch of Theorem 7.12, which appears to apply equivalence (7) to families λn.P(n,m) without assuming downward closure; that is a potential correctness gap or missing normalization step, not a definitional equivalence or fitted prediction, and therefore does not constitute circularity. No parameter fitting, definitional self-reference, or author-imported uniqueness theorem forces the conclusions.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The ledger is light on free parameters because the framework defines new concepts rather than fitting data. The main assumptions are the standard HoTT background, the prior construction of Brouwer trees, and the synthetic definition of semidecidability. No new entities are postulated.

assumptions (4)
  • standard math HoTT with univalence, function extensionality, propositional truncation
    Stated in the Setting paragraph of Section 1; used throughout.
  • domain assumption The type Brw of Brouwer trees and its relation ≤ exist with the properties in Lemma 2.1, as constructed in [27]
    Introduced in Section 2 from prior work; all later results rely on its characterization lemmas.
  • domain assumption Semidecidability is captured by binary sequences N→2
    Standard synthetic computability definition adopted in Section 1 and used in Proposition 3.2.
  • domain assumption In Section 8.2, the Sierpiński type S as the free ω-cpo on the unit type exists
    Used only for the alternative Sierpiński-semidecidability discussion; not part of the central flawed theorem.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generalized Decidability via Brouwer Trees." pith.science (2026). https://pith.science/paper/CRS7O6MV

@misc{pith2026260210844,
  author       = {Pith},
  title        = {Pith review of: Generalized Decidability via Brouwer Trees},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CRS7O6MV}},
  note         = {Machine review of arXiv:2602.10844}
}
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.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 1 linked inside Pith

  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

    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-...

    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

    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

    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

    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

    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

    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

    doi:10.1017/s0960129517000184 2019

Show all 37 references
  1. [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

    1938 doi

  2. [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

    1997

  3. [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

    2022

  4. [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...

    2004 doi

  5. [13]

    Quasidecidable propositions

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

    2020

  6. [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 Info...

    2017 doi

  7. [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

    2018

  8. [16]

    Formalising real numbers in homotopy type theory

    Ga¨ etan 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. doi:10.1145/3018610.3018614

    2017

  9. [17]

    Limiting recursion

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

    1965 doi

  10. [18]

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

    1982 doi

  11. [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

    1978 doi

  12. [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

    2000 doi

  13. [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, ...

    doi

  14. [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

    2016 doi

  15. [23]

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

    1938 doi

  16. [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...

    2013 doi

  17. [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 (LI...

    2021 doi

  18. [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

    2022

  19. [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

    2023 arXiv

  20. [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

    2014

  21. [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

    1975 doi

  22. [30]

    Continuity and Effectiveness in Topoi

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

    1986

  23. [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

    1977 doi

  24. [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

    2019

  25. [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

    2019

  26. [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

    1987

  27. [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/

    2013

  28. [36]

    PhD thesis, Tallinn University of Technology, 2017

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

    2017

  29. [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://tdejo...

    2014 doi

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.