Decidability in Intuitionistic Type Theory is Functionally Decidable

✍ Scribed by Silvio Valentini

• Publisher: John Wiley and Sons
• Year: 1996
• Tongue: English
• Weight: 255 KB
• Volume: 42
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19960420125

✦ Synopsis

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.