Martin Escardo 2011. \begin{code} {-# OPTIONS --without-K #-} 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 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)) \end{code} Notice that p is unique (Agda exercise - you will need extensionality).