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∈ℕ. P(i)是ω²-可判定的，并对可数并和迭代量词给出了类似结果。我们还讨论了与可数选择公理的关系。我们的所有结果均在Cubical Agda中形式化验证。