Martin Escardo 2011.

\begin{code}

module DecidableAndDetachable where

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

\end{code}

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

\begin{code}

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))

\end{code}

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:

\begin{code}

truth-value : {A : Prp} →

 decidable A → ∃ \(b : ₂) → (b ≡ ₀ → A) ∧ (b ≡ ₁ → ¬ A)

truth-value = which-of

\end{code} 

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:

\begin{code}

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))
 where
  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)

\end{code}

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.

 \begin{code}

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

\end{code}

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