Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg
TL;DR
This work develops a unified, constructive framework for generalized decidability using Brouwer trees, introducing $\alpha$-decidability to interpolate between decidability and semidecidability via the Brouwer ordinal system in HoTT. It proves closure properties for conjunctions and, in restricted forms, for disjunctions; analyzes semidecidable families through a characteristic ordinal $\Psi(P)$ to derive results about countable meets and joins, and quantifier alternations, with key outcomes like $\forall n. P_n$ being $\omega^2$-decidable and $\exists n. P_n$ being $\omega\cdot 3$-decidable (under certain assumptions). The results are formalized in Cubical Agda, and the work connects to countable choice and Sierpiński-semidecidability, highlighting both the power and limits of this ordinal-based hierarchy. The framework provides a precise, constructive lens for analyzing decidability beyond classical boundaries and lays groundwork for further exploration of upwards-closure, implications between decidability levels, and potential variations of the ordinal model.
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 $α$-decidable, for a Brouwer 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 $\forall i\in \mathbb 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.