Martin Escardo 2011.


{-# OPTIONS --without-K #-}

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

co-characteristic-function : {X : Set}  {A : X  Prp} 

 detachable A
     \(p : X  )  ∀(x : X)  (p x    ¬(A x))  (p x    A x)

co-characteristic-function d = indicator x  ∨-commutative(d x))


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