“Theorem. Absurdity of absurdity of absurdity is equivalent to absurdity.”

Brouwer.agda

module Brouwer where


-- From Brouwer’s Cambridge lectures on intuitionism (1946-1951):
--
-- “Theorem. Absurdity of absurdity of absurdity is equivalent to absurdity.
--
-- Proof. Firstly, since implication of the assertion y by the assertion x implies
-- implication of absurdity of x by absurdity of y, the implication of absurdity of
-- absurdity by truth (which is an established fact) implies the implication of
-- absurdity of truth, that is to say, of absurdity, by absurdity of absurdity of
-- absurdity. Secondly, since truth of an assertion implies absurdity of its
-- absurdity, in particular truth of absurdity implies absurdity of absurdity of
-- absurdity.”
--
-- (Hat tip to Martín Hötzel Escardó.)


-- Poetic? Maybe. Opaque? Definitely.
--
-- Have I been convinced? Here’s my reinterpretation:

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

record _∧_ (A B : Set) : Set where
  constructor _,_
  field
    π₁ : A
    π₂ : B

_↔_ : Set → Set → Set
A ↔ B = (A → B) ∧ (B → A)

Theorem : (¬ ¬ ⊥) ↔ ⊥
Theorem = (λ f → f (λ x → x)) , (λ x y → x)


-- Attempting to follow the original prose more closely is problematic, because
-- even though it may seem that “…of absurdity of truth, that is to say, of
-- absurdity…” is a fine thing to say, it turns out that (⊤ → ⊥) is not quite
-- the same thing as ⊥.

⊤ : Set
⊤ = ⊥ → ⊥

elim⊥ : ∀ {X : Set} → ⊥ → X
elim⊥ ()

_↯_ : ∀ {X Y : Set} → X → ¬ X → Y
p ↯ ¬p = elim⊥ (¬p p)

firstly : (⊤ → ¬ ⊥) → ¬ ¬ ⊥ → ¬ ⊤
firstly = since
  where
    since : ∀ {X Y : Set} → (X → Y) → ¬ Y → ¬ X
    since x→y ¬y = λ x → x→y x ↯ ¬y

secondly : ⊥ → ¬ ¬ ⊥
secondly = since
  where
    since : ∀ {X : Set} → X → ¬ ¬ X
    since x = λ ¬x → x ↯ ¬x

Theorem′ : (¬ ¬ ⊥) ↔ ⊥
Theorem′ = {!firstly fact!} , secondly
  where
    fact : ⊤ → ¬ ⊥
    fact t = t


-- Allowing for this slight indiscretion allows us to recover the theorem.

firstly′ : (⊤ → ¬ ⊥) → ¬ ¬ ⊥ → ⊥
firstly′ t→¬f ¬¬f = t→¬f true ↯ ¬¬f
  where
    true : ⊤
    true f = f

Theorem″ : (¬ ¬ ⊥) ↔ ⊥
Theorem″ = firstly′ fact , secondly
  where
    fact : ⊤ → ¬ ⊥
    fact t = t

-- EDIT: Turns out I’ve just misinterpreted the proposition in question.
-- The actual theorem follows:

Theorem‴ : ∀ {X : Set} → (¬ ¬ ¬ X) ↔ (¬ X)
Theorem‴ = fst snd , snd
  where
    fst : ∀ {X Y : Set} → (X → Y) → ¬ Y → ¬ X
    fst x→y ¬y = λ x → x→y x ↯ ¬y

    snd : ∀ {X : Set} → X → ¬ ¬ X
    snd x = λ ¬x → x ↯ ¬x