classical logic

classic.agda

module classic where

open import Level
open import Relation.Nullary
open import Data.Empty
open import Data.Sum
open import Data.Product

-- peirce : ∀ {a b} (P : Set a) (Q : Set b) → Set (a ⊔ b)
-- peirce P Q = ((P → Q) → P) → P

-- classic : ∀ {a} (P : Set a) → Set a
-- classic P = (¬ (¬ P)) → P

-- excluded-middle : ∀ {a} (P : Set a) → Set a
-- excluded-middle P = P ⊎ ¬ P

-- de-morgan-not-and-not : ∀ {a b} (P : Set a) (Q : Set b) → Set (a ⊔ b)
-- de-morgan-not-and-not P Q = ¬ (¬ P × ¬ Q) → P ⊎ Q

-- implies-to-or : ∀ {a b} (P : Set a) (Q : Set b) → Set (a ⊔ b)
-- implies-to-or P Q = (P → Q) → (¬ P ⊎ Q)

peirce : (P : Set) (Q : Set) → Set
peirce P Q = ((P → Q) → P) → P

classic : (P : Set) → Set
classic P = (¬ (¬ P)) → P

excluded-middle : (P : Set) → Set
excluded-middle P = P ⊎ ¬ P

de-morgan-not-and-not : (P : Set) (Q : Set) → Set
de-morgan-not-and-not P Q = ¬ (¬ P × ¬ Q) → P ⊎ Q

implies-to-or : (P : Set) (Q : Set) → Set
implies-to-or P Q = (P → Q) → (¬ P ⊎ Q)

--

peirce→classic :
  ((P : Set) (Q : Set) → peirce P Q)
  → (P : Set) → classic P
peirce→classic p P ¬¬P = p ((¬ P → P) → P) P (λ _ → p P ⊥) (λ x → ⊥-elim (¬¬P x))

classic→excluded-middle :
  ((P : Set) → classic P)
  → (P : Set) → excluded-middle P
classic→excluded-middle cl P = cl (P ⊎ ((x : P) → ⊥)) (λ x → x (inj₁ (cl P (λ z → x (inj₂ z)))))

excluded-middle→de-morgan-not-and-not :
  ((P : Set) → excluded-middle P)
  → (P : Set) (Q : Set) → de-morgan-not-and-not P Q
excluded-middle→de-morgan-not-and-not em P Q pq with em P | em Q
... | inj₁ x | _      = inj₁ x
... | inj₂ _ | inj₁ x = inj₂ x
... | inj₂ x | inj₂ y with pq (x , y)
... | ()

de-morgan-not-and-not→implies-to-or :
  ((P : Set) (Q : Set) → de-morgan-not-and-not P Q)
  → (P : Set) (Q : Set) → implies-to-or P Q
de-morgan-not-and-not→implies-to-or dm P Q pq = dm ((x : P) → ⊥) Q (λ x → proj₁ x (λ y → (proj₂ x) (pq y)))

implies-to-or→peirce :
  ((P : Set) (Q : Set) → implies-to-or P Q)
  → (P : Set) (Q : Set) → peirce P Q
implies-to-or→peirce it P Q pqp with it (((P → Q) → P) → P) (((P → Q) → P) → P) (λ z → z)
implies-to-or→peirce it P Q pqp | inj₁ x with it Q Q (λ z → z)
implies-to-or→peirce it P Q pqp | inj₁ x | inj₁ y with it P P (λ z → z)
implies-to-or→peirce it P Q pqp | inj₁ x₁ | inj₁ y | inj₁ x with x₁ (λ x₂ → x₂ (λ x₃ → ⊥-elim (x x₃)))
... | ()
implies-to-or→peirce it P Q pqp | inj₁ x | inj₁ y₁ | inj₂ y = y
implies-to-or→peirce it P Q pqp | inj₁ x | inj₂ y = pqp (λ x → y)
implies-to-or→peirce it P Q pqp | inj₂ y = y pqp

--

classic→peirce :
  ((P : Set) → classic P)
  → (P : Set) (Q : Set) → peirce P Q
classic→peirce cl P Q =
  cl (((P → Q) → P) → P)
     (λ x → x (λ y → y (λ z → cl Q (λ _ → x (λ w → z)))))

implies-to-or→classic :
  ((P : Set) (Q : Set) → implies-to-or P Q)
  → (P : Set) → classic P
implies-to-or→classic it P nnp with it P P (λ z → z)
... | inj₂ x = x
... | inj₁ x with nnp x
... | ()

--

double-negation-elimination :
  (P : Set) → ¬ ¬ ¬ P → ¬ P
double-negation-elimination P = λ nnnp p → nnnp (λ np → np p)