Classical.agda

module Classical where

open import Data.Empty
  using (⊥-elim)
open import Data.Product
  using (_×_; _,_)
open import Data.Sum
  using (_⊎_; inj₁; inj₂; [_,_])
open import Function
  using (id; _∘_)
open import Relation.Nullary
  using (¬_)
open import Level
  using (_⊔_; lower)

-- Reductio ad absurdum
-- (double negation elimination).
RAA : ∀ p → Set _
RAA p = {P : Set p} → ¬ ¬ P → P

-- Tertium non datur
-- (the law of excluded middle).
TND : ∀ p → Set _
TND p = {P : Set p} → P ⊎ ¬ P

-- Peirce's law.
Peirce : ∀ p q → Set _
Peirce p q = {P : Set p} {Q : Set q} → ((P → Q) → P) → P


-- Logical equivalence.
_↔_ : ∀ {p q} → Set p → Set q → Set (p ⊔ q)
P ↔ Q = (P → Q) × (Q → P)


raa↔peirce : ∀ p q → RAA p ↔ Peirce p q
raa↔peirce p q = ⇒ , ⇐
  where
  ⇒ : RAA p → Peirce p q
  ⇒ raa pqp = raa λ np → np (pqp (⊥-elim ∘ np))

  ⇐ : Peirce p q → RAA p
  ⇐ peirce nnp = peirce (⊥-elim ∘ nnp ∘ _∘_ lower)

raa↔tnd : ∀ p → RAA p ↔ TND p
raa↔tnd p = ⇒ , ⇐
  where
  ⇒ : RAA p → TND p
  ⇒ raa = raa λ ¬p∨np → ¬p∨np (inj₂ (¬p∨np ∘ inj₁))

  ⇐ : TND p → RAA p
  ⇐ tnd nnp = [ id , ⊥-elim ∘ nnp ] tnd

peirce↔tnd : ∀ p q → Peirce p q ↔ TND p
peirce↔tnd p q = ⇒ , ⇐
  where
  ⇒ : Peirce p q → TND p
  ⇒ peirce = peirce λ ¬tnd → inj₂ (lower ∘ ¬tnd ∘ inj₁)

  ⇐ : TND p → Peirce p q
  ⇐ tnd pqp = [ id , pqp ∘ _∘_ ⊥-elim ] tnd