中央研究院 資訊科學研究所

Decidability and semidecidability are at the heart of computer science. In the context of constructive mathematics and type theory, we can say that a proposition is decidable if P ∨ ¬ P is provable, and semidecidable if there exists a binary sequence that is 1 somewhere if and only if P holds. Intuitively, a property is decidable if an answer is discoverable in finitely many steps, whereas a property is semidecidable if an answer is discoverable in countably many steps. This formulation suggests a hierarchy beyond just decidable, semidecidable and undecidable. For example, if every P(i) is semidecidable, then ∀i∈ℕ.P(i) may not be semidecidable, but intuitively, its answer is discoverable in ω² steps: each P(i) requires at most ω steps, and there are ω instances.

We suggest and study a framework in which the above and other statements can be made precise and proved. Working in homotopy type theory, we use ordinals in the form of Brouwer trees 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 conjunctions and discuss for which α they are closed under binary disjunction. We prove the result about countable meets alluded to in the first paragraph, similar results for countable joins and iterated quantifiers, and discuss the relationship with countable choice.