Decidability in Intuitionistic Type Theory is Functionally Decidable
Silvio Valentini · Mathematical logic quarterly · 1996
Abstract In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B(x) prop [x : A], i. e. to require that the predicate (∀x ∈ A) (B(x) ∨ ¬ B(x)) is provable, is equivalent, when working within the framework of Martin‐Löf's Intuitionistic Type Theory, to require that there exists a decision function ψ: A → Boole such that (∀x ∈ A) ((ψ(x) = Boole true) ↔ B(x)). Since we will also show that the proposition x = Boole true [x: Boole] is decidable, we can alternatively say that the main result of this paper is a proof that the decidability of the predicate B(x) prop [x : A] can be effectively reduced by a function ψ A → Boole to the decidability of the predicate ψ(x) = Boole true [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function ψ, together with a proof of its correctness, is effectively constructed as a function of the proof of (∀x ∈ A)(B(x) ∨ ¬ B(x)). Mathematics Subject Classification: 03B15, 03B20.