Generalized decidability via Brouwer trees

Tools

de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik; Faggian, Claudia and Katoen, Joost-Pieter, eds. (2026) Generalized decidability via Brouwer trees. In: Forty-First Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics . Schloss Dagstuhl – Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, PRT. (In Press)

[thumbnail of de-Jong-etal-LICS-2026-Generalized-decidability-via-Brouwer-trees] Text. Filename: de-Jong-etal-LICS-2026-Generalized-decidability-via-Brouwer-trees.pdf
Accepted Author Manuscript
Restricted to Repository staff only until 1 January 2099.
Download (771kB) | Request a copy

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 ∈ N.P(i) is ω 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.

ORCID iDs

de Jong, Tom, Kraus, Nicolai, Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288; Faggian, Claudia and Katoen, Joost-Pieter
CORE (COnnecting REpositories)