Martin Escardo 2011.


module DecidableAndDetachable where

open import SetsAndFunctions
open import CurryHoward
open import Two
open import Equality


We look at decidable propositions and subsets (using the terminogy
"detachable" for the latter").


decidable : Prp  Prp
decidable A = A  ¬ A 

¬¬-elim : {A : Prp}  

 decidable A  ¬¬ A  A

¬¬-elim (in₀ a) f = a
¬¬-elim (in₁ g) f = ⊥-elim(f g)

negation-preserves-decidability : {A : Prp}  

 decidable A  decidable(¬ A)

negation-preserves-decidability (in₀ a) = in₁  f  f a)
negation-preserves-decidability (in₁ g) = in₀ g

which-of : {A B : Prp}  
 A  B   \(b : )  (b    A)  (b    B)

which-of (in₀ a) = ∃-intro  (∧-intro  r  a)  ()))
which-of (in₁ b) = ∃-intro  (∧-intro  ())  r  b))


Notice that in Agda the term λ () is a proof of an implication that
holds vacuously, by virtue of the premise being false.  In the above
example, the first occurrence is a proof of ₀ ≡ ₁ → B, and the second
one is a proof of ₁ ≡ ₀ → A. The following is a special case we are
interested in:


truth-value : {A : Prp}  
 decidable A   \(b : )  (b    A)  (b    ¬ A)

truth-value = which-of


Notice that this b is unique (Agda exercise) and that the converse
also holds. In classical mathematics it is posited that all
propositions have binary truth values, irrespective of whether they
have BHK-style witnesses. And this is precisely the role of the
principle of excluded middle in classical mathematics.  The following
requires choice, which holds in BHK-style constructive mathematics:


indicator : {X : Set}  {A B : X  Prp}  
 (∀(x : X)  A x  B x)
    \(p : X  )  ∀(x : X)  (p x    A x)  (p x    B x)

indicator {X} {A} {B} h = 
 ∃-intro  x  ∃-witness(lemma₁ x))  x  ∃-elim(lemma₁ x))
  lemma₀ : ∀(x : X)  (A x  B x)   \b  (b    A x)  (b    B x)
  lemma₀ x = which-of {A x} {B x}

  lemma₁ : ∀(x : X)   \b  (b    A x)  (b    B x)
  lemma₁ = λ x  lemma₀ x (h x)


We again have a particular case of interest.  Detachable subsets,
defined below, are often known as decidable subsets. Agda doesn't
allow overloading of terminology, and hence we gladly accept the
slighly non-universal terminology.


detachable : {X : Set}  (A : X  Prp)  Prp
detachable {X} A =  x  decidable(A x)

characteristic-function : {X : Set}  {A : X  Prp}  
 detachable A 
     \(p : X  )  ∀(x : X)  (p x    A x)  (p x    ¬(A x))

characteristic-function = indicator

Notice that p is unique (Agda exercise - you will need extensionality).