Logic.lagda

module Logic where

data _∧_ (P Q : Set) : Set where
  conj : P → Q → P ∧ Q

data _∨_ (P Q : Set) : Set where
  injl : P → P ∨ Q
  injr : Q → P ∨ Q

data ⊤ : Set where tt : ⊤
data ⊥ : Set where

¬_ : Set → Set
¬ P = P → ⊥

absurd : ∀ {A : Set} → ⊥ → A
absurd ()

peirce         : Set₁
classic        : Set₁
excludedMiddle : Set₁
deMorgan       : Set₁
impliesToOr    : Set₁

peirce         = ∀ {P Q : Set} → ((P → Q) → P) → P
classic        = ∀ {P : Set} → ¬ (¬ P) → P
excludedMiddle = ∀ {P : Set} → P ∨ ¬ P
deMorgan       = ∀ {P Q : Set} → ¬ (¬ P ∧ ¬ Q) → P ∨ Q
impliesToOr    = ∀ {P Q : Set} → (P → Q) → (¬ P ∨ Q)

id : ∀ {P : Set} → P → P
id p = p

k : ∀ {X N : Set} → X → N → X
k z _ = z

both : ∀ {P Q R : Set} → P ∨ Q → (P → R) → (Q → R) → R
both (injl x) f g = f x
both (injr x) f g = g x

left : ∀ {P Q : Set} → P ∧ Q → P
left (conj x _) = x

right : ∀ {P Q : Set} → P ∧ Q → Q
right (conj _ x) = x

flip : ∀ {P Q : Set} → P ∨ Q → Q ∨ P
flip (injl x) = injr x
flip (injr x) = injl x

infix 9 _∘_
infix 0 _$_

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

_$_ : ∀ {A : Set} {B : A → Set} → ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

data _↔_ : Set₁ → Set₁ → Set₂ where
  iso : ∀ {P Q : Set₁} → (P → Q) → (Q → P) → P ↔ Q

peirce↔classic : peirce ↔ classic
peirce↔classic = iso ⟶ ⟵
  where
    ⟶ : peirce → classic
    ⟵ : classic → peirce
    ⟶ pc {P} cl     = pc {P} {⊥} $ λ negp → absurd $ cl negp
    ⟵ cl {P} {Q} pc = cl {P} $ λ f → f $ pc (λ p → absurd $ f p)

classic↔demorgan : classic ↔ deMorgan
classic↔demorgan = iso ⟶ ⟵
  where 
    ⟶ : classic → deMorgan
    ⟵ : deMorgan → classic
    ⟶ cl {P} {Q} dm = cl {P ∨ Q} $ λ porq→f → dm $ conj (porq→f ∘ injl) (porq→f ∘ injr)
    ⟵ dm {P} cl     = both (dm {P} {P} (λ twoNegPs → cl (left twoNegPs))) id id

classic↔excludedMiddle : classic ↔ excludedMiddle
classic↔excludedMiddle = iso ⟶ ⟵
  where 
    ⟶ : classic → excludedMiddle
    ⟵ : excludedMiddle → classic
    ⟶ cl {P}    = cl {P ∨ (P → ⊥)} $ λ nnpn → nnpn (injr $ nnpn ∘ injl)
    ⟵ em {P} cl = both (em {P}) id (absurd ∘ cl)

excludedMiddle↔impliesToOr : excludedMiddle ↔ impliesToOr
excludedMiddle↔impliesToOr = iso ⟶ ⟵
  where 
    ⟶ : excludedMiddle → impliesToOr
    ⟵ : impliesToOr → excludedMiddle
    ⟶ em {P} {Q} or2or = both (em {P}) (injr ∘ or2or) injl
    ⟵ or2or {P}        = flip ∘ or2or {P} {P} $ id

---

data ∃ {X : Set} (P : X → Set) : Set where
  ex : ∀ (witness : X) → P witness → ∃ P

dist-nEx : {X : Set} {P : X → Set}
           → (∀ x → P x) → ¬ (∃ (λ x → ¬ (P x)))
dist-nEx {X} {P} fa (ex witness p) = p (fa witness)

nEx-dist : excludedMiddle 
           → ∀ {X : Set} {P : X → Set} 
           → ¬ (∃ (λ x → ¬ (P x))) → (∀ x → P x)
nEx-dist em {X} {P} negex x = 
  both (em {P x}) id $ λ negPx → absurd ∘ negex $ ex x negPx

\end{code}