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 (For All x is an element of A)(B(x) V-B(x)) is provable, is equivalent, when working within the framework of Martin-Lof's Intuitionistic Type Theory, to require that there exists a decision function rho : A --> Boole such that (For All x is an element of A) ((rho(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 rho is an element of A --> Boole to the decidability of the predicate rho(x) = (Boole) true [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function rho, together with a proof of its correctness, is effectively constructed as a function of the proof of (For All s is an element of A)(B(x)V - B(x)).

Decidability in Intuitionistic Type Theory is functionally decidable

VALENTINI, SILVIO
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 (For All x is an element of A)(B(x) V-B(x)) is provable, is equivalent, when working within the framework of Martin-Lof's Intuitionistic Type Theory, to require that there exists a decision function rho : A --> Boole such that (For All x is an element of A) ((rho(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 rho is an element of A --> Boole to the decidability of the predicate rho(x) = (Boole) true [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function rho, together with a proof of its correctness, is effectively constructed as a function of the proof of (For All s is an element of A)(B(x)V - B(x)).
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/136994
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 5
  • OpenAlex ND
social impact