The axiom of choice, interpreted with constructive & classical existentials.

AxiomOfChoice.agda

-- The axiom of choice is equivalent to the following schema:
--
--     (∀(a ∈ A) ∃(b ∈ B) P(a,b))
--     implies
--     ∃(f ∈ A → B) ∀(a ∈ A) P(a, f(a))
--
-- Here I give two interpretations of this statement into Agda's constructive
-- type theory:
--
-- 1. Interpreting ∃ "constructively" as Σ. Values of Σ come with a witness
--    indicating _which_ value satisfies P; consequently, this interpretation is
--    provable in Agda.
--
-- 2. Interpreting ∃ "classically" as ¬∀¬. You cannot constructively extract a
--    witness from ¬∀¬. Consequently I believe this interpretation unprovable.
--
-- Normally we think of classical logic as having "more" theorems (eg. the law
-- of the excluded middle, the equivalence of various notions of infinity) than
-- constructive logic, but "fewer" meta-theorems (eg. that if A ∨ B is provable,
-- then either A is provable or B is provable).
--
-- I see the axiom of choice as "internalising" the meta-theorem that from a
-- proof of a ∀∃-statement we can extract a function. This neatly explains why
-- the axiom of choice seems "obviously true" in a constructive setting
-- (interpretation #1), but in a classical setting it feels "non-constructive"
-- (interpretation #2).

module AxiomOfChoice where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
open import Relation.Nullary using (¬_)
open import Function using (_∘_; const)

-- Alternate syntax for ∀.
infix 2 Π
syntax Π A (λ x → B) = Π[ x ∈ A ] B  -- forall
Π : (A : Set) → (A → Set) → Set
Π A P = ∀(x : A) → P x

-- The weak, "classical" existential, as ¬∀¬. Also equivalent to ¬¬Σ (see bottom
-- of file).
infix 2 Σ?
syntax Σ? A (λ x → B) = ∃[ x ∈ A ] B -- weak, classical existential
Σ? : (A : Set) → (A → Set) → Set
Σ? A P = ¬ (Π[ a ∈ A ] ¬ P a)

-- 1. Interpreting ZFC ∃ as strong Σ.
AC-Σ : Set1
AC-Σ = ∀{A B} {P : A → B → Set}
     → Π[ a ∈ A ] Σ[ b ∈ B ] P a b
     → Σ[ f ∈ (A → B) ] Π[ a ∈ A ] P a (f a)

-- 2. Interpreting ZFC ∃ as weak Σ?.
AC-∃ : Set1
AC-∃ = ∀{A B} {P : A → B → Set}
     → Π[ a ∈ A ] ∃[ b ∈ B ] P a b
     → ∃[ f ∈ (A → B) ] Π[ a ∈ A ] P a (f a)

-- AC-Σ is easy to prove; but I believe AC-∃ to be unprovable.
choice : AC-Σ
choice f = proj₁ ∘ f , proj₂ ∘ f


-- A side-note: ¬∀¬ is constructively equivalent to ¬¬Σ.
Σ?→¬¬Σ : ∀{A}{P : A → Set} → ∃[ a ∈ A ] P a → ¬ ¬(Σ[ a ∈ A ] P a)
Σ?→¬¬Σ ¬∀¬ ¬Σ = ¬∀¬ λ a Pa → ¬Σ (a , Pa)

¬¬Σ→Σ? : ∀{A}{P : A → Set} → ¬ ¬(Σ[ a ∈ A ] P a) → ∃[ a ∈ A ] P a
¬¬Σ→Σ? ¬¬Σ ∀¬P = ¬¬Σ λ { (a , P) → ∀¬P a P }