Created
December 28, 2021 06:36
-
-
Save Trebor-Huang/f797ed57e28389511031d942072c5118 to your computer and use it in GitHub Desktop.
How logic was formulated by Russel's type theory.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 | |
) | |
-- -} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment