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.

翻译：在构造性数学的框架下，我们提出并研究了一种关于性质可判定性的理论框架，该框架允许比简单的"可判定、半可判定或不可判定"更精细的区分。我们以同伦类型论为工作基础，利用布劳威尔序数来刻画性质的可判定性层级。在此框架中，我们定义了命题关于布劳威尔序数α的"α-可判定性"概念，并证明其推广了传统可判定性与半可判定性。进一步推广已有结论，我们证明α-可判定命题在二元合取下封闭，并讨论了在哪些α取值下其对二元析取保持封闭性。我们证明了：若每个P(i)均为半可判定，则可数合取∀i∈N.P(i)是ω²-可判定的，并给出了可数析取及叠用量词情形的类似结论。我们还探讨了该框架与可数选择公理的关系。所有结果均在立方Agda中进行了形式化验证。