Martin Escardo 2011. \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} module DecidableAndDetachable where open import SpartanMLTT open import Two \end{code} We look at decidable propositions and subsets (using the terminogy "detachable" for the latter"). \begin{code} decidable : U → U decidable A = A + ¬ A ¬¬-elim : {A : U} → decidable A → ¬¬ A → A ¬¬-elim (inl a) f = a ¬¬-elim (inr g) f = ∅-elim(f g) negation-preserves-decidability : {A : U} → decidable A → decidable(¬ A) negation-preserves-decidability (inl a) = inr (λ f → f a) negation-preserves-decidability (inr g) = inl g which-of : {A B : U} → A + B → Σ \(b : 𝟚) → (b ≡ ₀ → A) × (b ≡ ₁ → B) which-of (inl a) = ₀ , ((λ r → a) , (λ ())) which-of (inr b) = ₁ , ((λ ()) , (λ 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 : U} → 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 : U} → {A B : X → U} → ((x : X) → A x + B x) → Σ \(p : X → 𝟚) → (x : X) → (p x ≡ ₀ → A x) × (p x ≡ ₁ → B x) indicator {X} {A} {B} h = (λ x → pr₁(lemma₁ x)) , (λ x → pr₂(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 : U} → (A : X → U) → U detachable A = ∀ x → decidable(A x) characteristic-function : {X : U} → {A : X → U} → detachable A → Σ \(p : X → 𝟚) → (x : X) → (p x ≡ ₀ → A x) × (p x ≡ ₁ → ¬(A x)) characteristic-function = indicator co-characteristic-function : {X : U} {A : X → U} → 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).