How logic was formulated by Russel's type theory.

Logic.agda

{-# OPTIONS --prop #-}
module Logic where

id : ∀ {ℓ} {A : Set ℓ} -> A -> A
id x = x

data 𝕋 : Set where
    𝒩𝒶𝓉 : 𝕋
    𝒫𝓇ℴ𝓅 : 𝕋
    _⟶_ : 𝕋 -> 𝕋 -> 𝕋
infixr 10 _⟶_

data Ctx : Set where
    ⋆ : Ctx
    _∷_ : Ctx -> 𝕋 -> Ctx
infixl 7 _∷_

infix 5 _∋_
data _∋_ : Ctx -> 𝕋 -> Set where
    𝕫 : ∀ {Γ T} -> Γ ∷ T ∋ T
    𝕤_ : ∀ {Γ S T} -> Γ ∋ T -> Γ ∷ S ∋ T
infixr 20 𝕤_

data Constant : 𝕋 -> Set where
    -- No constants yet.

infix 5 _⊢_
infixl 15 _∙_
infix 14 _==_ _!=_
infixl 6 ƛ_⇒_ ε_⇒_
data _⊢_ : Ctx -> 𝕋 -> Set where
    𝕧 : ∀ {Γ T} -> Γ ∋ T -> Γ ⊢ T  -- TODO a tactic for that
    𝕔 : ∀ {Γ T} -> Constant T -> Γ ⊢ T
    _∙_ : ∀ {Γ S T} -> Γ ⊢ S ⟶ T -> Γ ⊢ S -> Γ ⊢ T
    ƛ_⇒_ : ∀ {Γ T} S -> Γ ∷ S ⊢ T -> Γ ⊢ S ⟶ T
    _==_ : ∀ {Γ T} -> Γ ⊢ T -> Γ ⊢ T -> Γ ⊢ 𝒫𝓇ℴ𝓅
    ε_⇒_ : ∀ {Γ} S -> Γ ∷ S ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ S

ℜ𝔢𝔫 : Ctx -> Ctx -> Set
ℜ𝔢𝔫 Γ Δ = ∀ {T} -> Γ ∋ T -> Δ ∋ T

𝔖𝔲𝔟 : Ctx -> Ctx -> Set
𝔖𝔲𝔟 Γ Δ = ∀ {T} -> Γ ∋ T -> Δ ⊢ T

𝔉𝔫𝔱 : Ctx -> Ctx -> Set
𝔉𝔫𝔱 Γ Δ = ∀ {T} -> Γ ⊢ T -> Δ ⊢ T

private
    wr : ∀ {Γ Δ T} -> ℜ𝔢𝔫 Γ Δ -> ℜ𝔢𝔫 (Γ ∷ T) (Δ ∷ T)
    wr ρ 𝕫 = 𝕫
    wr ρ (𝕤 i) = 𝕤 ρ i

    infixr 14 r⟦_⟧_
    r⟦_⟧_ : ∀ {Γ Δ} -> ℜ𝔢𝔫 Γ Δ -> 𝔉𝔫𝔱 Γ Δ
    r⟦ ρ ⟧ 𝕧 x = 𝕧 (ρ x)
    r⟦ ρ ⟧ 𝕔 x = 𝕔 x
    r⟦ ρ ⟧ s ∙ t = (r⟦ ρ ⟧ s) ∙ (r⟦ ρ ⟧ t)
    r⟦ ρ ⟧ (ƛ S ⇒ s) = ƛ S ⇒ r⟦ (wr ρ) ⟧ s
    r⟦ ρ ⟧ (s == t) = (r⟦ ρ ⟧ s) == (r⟦ ρ ⟧ t)
    r⟦ ρ ⟧ (ε _ ⇒ s) = ε _ ⇒ r⟦ (wr ρ) ⟧ s

    ws : ∀ {Γ Δ T} -> 𝔖𝔲𝔟 Γ Δ -> 𝔖𝔲𝔟 (Γ ∷ T) (Δ ∷ T)
    ws σ 𝕫 = 𝕧 𝕫
    ws σ (𝕤 i) = r⟦ 𝕤_ ⟧ σ i

infixr 20 ⟦_⟧_
⟦_⟧_ : ∀ {Γ Δ} -> 𝔖𝔲𝔟 Γ Δ -> 𝔉𝔫𝔱 Γ Δ
⟦ σ ⟧ 𝕧 x = σ x
⟦ σ ⟧ 𝕔 c = 𝕔 c
⟦ σ ⟧ (t ∙ s) = ⟦ σ ⟧ t ∙ ⟦ σ ⟧ s
⟦ σ ⟧ (ƛ S ⇒ t) = ƛ S ⇒ ⟦ ws σ ⟧ t
⟦ σ ⟧ (t == s) = ⟦ σ ⟧ t == ⟦ σ ⟧ s
⟦ σ ⟧ (ε _ ⇒ t) = ε _ ⇒ ⟦ ws σ ⟧ t

infixr 20 𝕫/_
𝕫/_ : ∀ {Γ S} -> Γ ⊢ S -> 𝔖𝔲𝔟 (Γ ∷ S) Γ
(𝕫/ t) 𝕫 = t
(𝕫/ t) (𝕤 x) = 𝕧 x

infixr 20 ↑_
↑_ : ∀ {Γ T} -> 𝔉𝔫𝔱 Γ (Γ ∷ T)
↑_ = r⟦ 𝕤_ ⟧_

private variable
    Γ Δ : Ctx
    S T : 𝕋

-- Now some defined connectives
ID : Γ ⊢ 𝒫𝓇ℴ𝓅 ⟶ 𝒫𝓇ℴ𝓅
ID = ƛ 𝒫𝓇ℴ𝓅 ⇒ 𝕧 𝕫

True : Γ ⊢ 𝒫𝓇ℴ𝓅
True = ID == ID

KT : Γ ⊢ 𝒫𝓇ℴ𝓅 ⟶ 𝒫𝓇ℴ𝓅
KT = ƛ 𝒫𝓇ℴ𝓅 ⇒ True

False : Γ ⊢ 𝒫𝓇ℴ𝓅
False = ID == KT

infixr 20 ¬_
¬_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
¬ p = p == False

_!=_ : Γ ⊢ T -> Γ ⊢ T -> Γ ⊢ 𝒫𝓇ℴ𝓅
a != b = ¬ (a == b)

infixl 12 _∨_
infixl 13 _∧_
infixr 12 _=>_ _<=>_
_∧_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
p ∧ q = (ƛ _              ⇒ 𝕧 𝕫 ∙ True ∙ True)
     == (ƛ _ ⟶ _ ⟶ 𝒫𝓇ℴ𝓅 ⇒ 𝕧 𝕫 ∙ ↑ p  ∙ ↑ q)

_∨_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
p ∨ q = ¬ (¬ p ∧ ¬ q)

_=>_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
p => q = ¬ (p ∧ ¬ q)

_<=>_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
_<=>_ = _==_

Forall : ∀ T -> Γ ∷ T ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
Forall T p = (ƛ T ⇒ p) == (ƛ T ⇒ True)

Exists : ∀ T -> Γ ∷ T ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ 𝒫𝓇ℴ𝓅
Exists T p = ¬ (Forall T (¬ p))

syntax Forall T p = ∀[ T ] p
syntax Exists T p = ∃[ T ] p
infixr 6 Forall Exists

⊥ : Γ ⊢ T
⊥ = ε _ ⇒ 𝕧 𝕫 != 𝕧 𝕫

if_then_else_ : Γ ⊢ 𝒫𝓇ℴ𝓅 -> Γ ⊢ T -> Γ ⊢ T -> Γ ⊢ T
if p then a else b = ε _ ⇒
    ↑   p => 𝕧 𝕫 == ↑ a ∧
    ↑ ¬ p => 𝕧 𝕫 == ↑ a

infix 4 _≫_
data _≫_ : ∀ Γ -> Γ ⊢ 𝒫𝓇ℴ𝓅 -> Prop where
    Eq : ∀ {a b} -> Γ ≫ a == b
        -> (C : Γ ⊢ S -> Δ ⊢ 𝒫𝓇ℴ𝓅) -> Δ ≫ C a -> Δ ≫ C b
    Beta : {a : Γ ∷ S ⊢ T} {b : Γ ⊢ S}
        -> Γ ≫ (ƛ S ⇒ a) ∙ b == ⟦ 𝕫/ b ⟧ a
    Eta : Γ ≫ ∀[ S ⟶ T ] ∀[ S ⟶ T ]
            𝕧 𝕫 == 𝕧 (𝕤 𝕫) <=>
                (∀[ S ] 𝕧 (𝕤 𝕫) ∙ 𝕧 𝕫 == 𝕧 (𝕤 𝕤 𝕫) ∙ 𝕧 𝕫)
    LEM : Γ ≫ ∀[ 𝒫𝓇ℴ𝓅 ⟶ 𝒫𝓇ℴ𝓅 ]
            (𝕧 𝕫 ∙ True ∧ 𝕧 𝕫 ∙ False) <=> (∀[ 𝒫𝓇ℴ𝓅 ] 𝕧 (𝕤 𝕫) ∙ 𝕧 𝕫)
    PropExt : Γ ≫ ∀[ 𝒫𝓇ℴ𝓅 ] 𝕧 𝕫 <=> 𝕧 𝕫 == True
    Choice : ∀ {a}
        -> Γ ≫ (∃[ S ] a) => ⟦ 𝕫/ (ε _ ⇒ a) ⟧ a
    Undefined : ∀ {a}
        -> Γ ≫ ¬ (∃[ S ] a) => (ε _ ⇒ a) == ⊥

-- Next up, some theorems
Transitivity : ∀ {a b c : Γ ⊢ S}  -- Transitivity turns out to be easier to prove!
    -> Γ ≫ a == b -> Γ ≫ b == c -> Γ ≫ a == c
Transitivity ab bc = Eq bc _ ab

infixl 10 _⋯_
_⋯_ = Transitivity

Reflexivity : ∀ (a : Γ ⊢ S) -> Γ ≫ a == a
Reflexivity _ = lemma (Beta {a = 𝕧 𝕫})
    where
        lemma : ∀ {a b : Γ ⊢ S} -> Γ ≫ a == b -> Γ ≫ b == b
        lemma ab = Eq ab _ ab

Symmetry : ∀ {a b : Γ ⊢ S}
    -> Γ ≫ a == b -> Γ ≫ b == a
Symmetry {a = a} ab = Eq ab
    (\ x -> x == a) (Reflexivity a)

Congruence : ∀ {a b : Γ ⊢ S}
    -> Γ ≫ a == b
    -> (f : Γ ⊢ S -> Δ ⊢ T)
    -> Δ ≫ f a == f b
Congruence eq f = Eq eq (\ x -> _ == f x) (Reflexivity _)

≫True : Γ ≫ True
≫True = Reflexivity ID

Rewrite : ∀ {p : Γ ⊢ 𝒫𝓇ℴ𝓅}
    -> Γ ≫ p == True -> Γ ≫ p
Rewrite eq = Eq (Symmetry eq) id ≫True

∀Elim : ∀ {p : Γ ∷ S ⊢ 𝒫𝓇ℴ𝓅} {a : Γ ⊢ S}
    -> Γ ≫ ∀[ S ] p -> Γ ≫ ⟦ 𝕫/ a ⟧ p
∀Elim {Γ = Γ} {S = S} {p = p} {a = a} pa = Rewrite (
    --    ⟦ 𝕫/ a ⟧ p
          Symmetry Beta
    -- == (ƛ S ⇒ p) ∙ a
        ⋯ lemma
    -- == (ƛ S ⇒ True) ∙ a
        ⋯ Beta
    -- == True
    )
    where
        lemma : Γ ≫ (ƛ S ⇒ p) ∙ a == (ƛ S ⇒ True) ∙ a
        lemma = Congruence pa (_∙ a)

==True : ∀ {p : Γ ⊢ 𝒫𝓇ℴ𝓅}
    -> Γ ≫ p -> Γ ≫ p == True
==True pp = Eq (∀Elim PropExt) id pp

⟨_,_⟩ : ∀ {p q : Γ ⊢ 𝒫𝓇ℴ𝓅}
    -> Γ ≫ p -> Γ ≫ q -> Γ ≫ p ∧ q
⟨_,_⟩ {q = q} pp qq = Eq (Symmetry (
          Congruence (==True pp) (\p -> 𝕧 𝕫 ∙ ↑ p  ∙ ↑ q)
        ⋯ Congruence (==True qq) (\q -> 𝕧 𝕫 ∙ True ∙ ↑ q)
    )) (\u -> (ƛ _ ⇒ 𝕧 𝕫 ∙ True ∙ True) ==
             (ƛ _ ⇒ u))
    (Reflexivity (ƛ 𝒫𝓇ℴ𝓅 ⟶ 𝒫𝓇ℴ𝓅 ⟶ 𝒫𝓇ℴ𝓅 ⇒ 𝕧 𝕫 ∙ True ∙ True))

-- From here on we encounter coherence problems
{-
π₁ : ∀ {p q : Γ ⊢ 𝒫𝓇ℴ𝓅}
    -> Γ ≫ p ∧ q -> Γ ≫ p
π₁ {p = p} {q = q} pq = Rewrite (
    --    p
          Symmetry (Beta {a = ↑ p} {b = q})
    -- == (λq.p) q
        ⋯ Congruence (Symmetry Beta) (_∙ q)
    -- == (λp.λq.p) p q
        ⋯ Symmetry Beta
    -- == (λf.f p q) (λp.λq.p)
        ⋯ Congruence pq (_∙ (ƛ 𝒫𝓇ℴ𝓅 ⇒ ƛ 𝒫𝓇ℴ𝓅 ⇒ 𝕧 (𝕤 𝕫)))
    -- == (λf.f T T) (λp.λq.p)
        ⋯ Beta
    -- == (λp.λq.p) T T
        ⋯ Congruence Beta (_∙ True)
    -- == (λq.p) T
        ⋯ Beta
    -- == True
    )
-- -}