From 7ff06d3d074e3655ca72c4ec15123de848af5da5 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Fri, 2 Jun 2023 14:37:08 +0200 Subject: [PATCH] Tried to add First order logic and First order Kripke. Some misconceptions ... --- FirstOrderKripke.agda | 91 ++++++++++++++++++++++++++++++++++++++ FirstOrderLogic.agda | 100 +++++++++++++++++++++++++++++++++++++----- 2 files changed, 180 insertions(+), 11 deletions(-) create mode 100644 FirstOrderKripke.agda diff --git a/FirstOrderKripke.agda b/FirstOrderKripke.agda new file mode 100644 index 0000000..0311b14 --- /dev/null +++ b/FirstOrderKripke.agda @@ -0,0 +1,91 @@ +{-# OPTIONS --prop --no-termination-check #-} + +open import Agda.Builtin.Nat +open import Agda.Builtin.Bool + +module FirstOrderKripke (PV : Set) (TV : Set) (TV= : TV → TV → Bool) (Fu : Nat → Set) (R : Nat → Set) where + + open import ListUtil + open import PropUtil + open import FirstOrderLogic TV TV= Fu R + + private + variable + n : Nat + t : Term + x : TV + y : TV + F : Form + G : Form + Γ : Con + Γ' : Con + Η : Con + Η' : Con + + record Kripke : Set₁ where + field + Worlds : Set₀ + _≤_ : Worlds → Worlds → Prop + refl≤ : {w : Worlds} → w ≤ w + tran≤ : {a b c : Worlds} → a ≤ b → b ≤ c → a ≤ c + _⊩_[_] : Worlds → R n → Args n → Prop + mon⊩ : {a b : Worlds} → a ≤ b → {r : R n} {A : Args n} → a ⊩ r [ A ] → b ⊩ r [ A ] + + private + variable + w : Worlds + w' : Worlds + w₁ : Worlds + w₂ : Worlds + w₃ : Worlds + + {- Extending ⊩ to Formulas and Contexts -} + -- It is in fact + _⊩ᶠ_ : Worlds → Form → Prop + w ⊩ᶠ (Rel {n = n} r A) = {B : Args n} → A ⊂sub B → w ⊩ r [ B ] + w ⊩ᶠ (fp ⇒ fq) = {w' : Worlds} → w ≤ w' → w' ⊩ᶠ fp → w' ⊩ᶠ fq + w ⊩ᶠ (fp ∧∧ fq) = w ⊩ᶠ fp ∧ w ⊩ᶠ fq + w ⊩ᶠ ⊤⊤ = ⊤ + w ⊩ᶠ (∀∀ x F) = (t : Term) → w ⊩ᶠ ([ t / x ] F) + + _⊩ᶜ_ : Worlds → Con → Prop + w ⊩ᶜ [] = ⊤ + w ⊩ᶜ (p ∷ c) = (w ⊩ᶠ p) ∧ (w ⊩ᶜ c) + + -- The extensions are monotonous + mon⊩ᶠ : w ≤ w' → w ⊩ᶠ F → w' ⊩ᶠ F + mon⊩ᶠ {F = Rel r A} ww' wF s = mon⊩ ww' (wF s) + mon⊩ᶠ {F = F ⇒ G} ww' wF w'w'' w''F = wF (tran≤ ww' w'w'') w''F + mon⊩ᶠ {F = F ∧∧ G} ww' ⟨ wF , wG ⟩ = ⟨ mon⊩ᶠ {F = F} ww' wF , mon⊩ᶠ {F = G} ww' wG ⟩ + mon⊩ᶠ {F = ⊤⊤} ww' wF = tt + mon⊩ᶠ {F = ∀∀ x F} ww' wF t = mon⊩ᶠ {F = [ t / x ] F} ww' (wF t) + + mon⊩ᶜ : w ≤ w' → w ⊩ᶜ Γ → w' ⊩ᶜ Γ + mon⊩ᶜ {Γ = []} ww' wΓ = wΓ + mon⊩ᶜ {Γ = F ∷ Γ} ww' wΓ = ⟨ mon⊩ᶠ {F = F} ww' (proj₁ wΓ) , mon⊩ᶜ ww' (proj₂ wΓ) ⟩ + + {- General operator matching the shape of ⊢ -} + _⊫_ : Con → Form → Prop + Γ ⊫ F = {w : Worlds} → w ⊩ᶜ Γ → w ⊩ᶠ F + + {- Soundness -} + th' : w ⊩ᶠ F → w ⊩ᶠ [ t / x ] F + th' {F = Rel r A} h {B} s = h {B} (tran⊂sub (next zero) s) + th' {F = F ⇒ F₁} h o hF = {!h o ?!} + th' {F = F ∧∧ F₁} h = {!!} + th' {F = ⊤⊤} h = {!!} + th' {F = ∀∀ x F} h = {!!} + th : Γ ⊫ F → Γ ⊫ [ t / x ] F + th {[]} h _ = {!!} + th {x ∷ Γ} h = {!!} + ⟦_⟧ : Γ ⊢ F → Γ ⊫ F + ⟦ zero zero∈ ⟧ wΓ = proj₁ wΓ + ⟦ zero (next∈ h) ⟧ wΓ = ⟦ zero h ⟧ (proj₂ wΓ) + ⟦ lam p ⟧ = λ wΓ w≤ w'A → ⟦ p ⟧ ⟨ w'A , mon⊩ᶜ w≤ wΓ ⟩ + ⟦ app p p₁ ⟧ wΓ = ⟦ p ⟧ wΓ refl≤ (⟦ p₁ ⟧ wΓ) + ⟦ andi p₁ p₂ ⟧ wΓ = ⟨ (⟦ p₁ ⟧ wΓ) , (⟦ p₂ ⟧ wΓ) ⟩ + ⟦ ande₁ p ⟧ wΓ = proj₁ $ ⟦ p ⟧ wΓ + ⟦ ande₂ p ⟧ wΓ = proj₂ $ ⟦ p ⟧ wΓ + ⟦ true ⟧ wΓ = tt + ⟦ ∀-i i p ⟧ wΓ t = {!⟦ p ⟧!} + ⟦ ∀-e {t = t} p ⟧ wΓ = ⟦ p ⟧ wΓ t diff --git a/FirstOrderLogic.agda b/FirstOrderLogic.agda index 72f9519..fdab25f 100644 --- a/FirstOrderLogic.agda +++ b/FirstOrderLogic.agda @@ -1,30 +1,108 @@ {-# OPTIONS --prop #-} open import Agda.Builtin.Nat +open import Agda.Builtin.Bool +open import Agda.Primitive using (Level) -module FirstOrderLogic (TV : Set) (F : Nat → Set) (R : Nat → Set) where +module FirstOrderLogic (TV : Set) (TV= : TV → TV → Bool) (F : Nat → Set) (R : Nat → Set) where open import PropUtil open import ListUtil mutual - data FArgs : Nat → Set where - zero : FArgs 0 - next : {n : Nat} → FArgs n → Term → FArgs (suc n) + data Args : Nat → Set where + zero : Args 0 + next : {n : Nat} → Args n → Term → Args (suc n) data Term : Set where Var : TV → Term - Fun : {n : Nat} → F n → FArgs n → Term + Fun : {n : Nat} → F n → Args n → Term - data RArgs : Nat → Set where - zero : RArgs 0 - next : {n : Nat} → RArgs n → Term → RArgs (suc n) - + private + variable + n : Nat + + if : {ℓ : Level} → {T : Set ℓ} → Bool → T → T → T + if true a b = a + if false a b = b + + mutual + [_/_]ᵗ : Term → TV → Term → Term + [_/_]ᵃ : Term → TV → Args n → Args n + [ t / x ]ᵗ (Var x') = if (TV= x x') t (Var x') + [ t / x ]ᵗ (Fun f A) = Fun f ([ t / x ]ᵃ A) + [ t / x ]ᵃ zero = zero + [ t / x ]ᵃ (next A t₁) = next ([ t / x ]ᵃ A) ([ t / x ]ᵗ t₁) + + -- A ⊂sub B if B can be obtained with finite substitution from A + data _⊂sub_ : Args n → Args n → Prop where + zero : {A : Args n} → A ⊂sub A + next : {A B : Args n} → {t : Term} → {x : TV} → A ⊂sub B → A ⊂sub ([ t / x ]ᵃ B) + + tran⊂sub : {A B C : Args n} → A ⊂sub B → B ⊂sub C → A ⊂sub C + tran⊂sub zero h₂ = h₂ + tran⊂sub h₁ zero = h₁ + tran⊂sub h₁ (next h₂) = next (tran⊂sub h₁ h₂) + data Form : Set where - Rel : {n : Nat} → R n → (RArgs n) → Form + Rel : {n : Nat} → R n → (Args n) → Form _⇒_ : Form → Form → Form _∧∧_ : Form → Form → Form - _∀∀_ : TV → Form → Form + ⊤⊤ : Form + ∀∀ : TV → Form → Form infixr 10 _∧∧_ infixr 8 _⇒_ + + Con = List Form + private + variable + A : Form + A' : Form + B : Form + B' : Form + C : Form + Γ : Con + Γ' : Con + Γ'' : Con + Δ : Con + Δ' : Con + x : TV + t : Term + + [_/_] : Term → TV → Form → Form + [ t / x ] (Rel r tz) = Rel r ([ t / x ]ᵃ tz) + [ t / x ] (A ⇒ A₁) = ([ t / x ] A) ⇒ ([ t / x ] A₁) + [ t / x ] (A ∧∧ A₁) = ([ t / x ] A) ∧∧ ([ t / x ] A₁) + [ t / x ] ⊤⊤ = ⊤⊤ + [ t / x ] (∀∀ x₁ A) = if (TV= x x₁) A ([ t / x ] A) + + mutual + _∉FVᵗ_ : TV → Term → Prop + _∉FVᵃ_ : TV → Args n → Prop + x ∉FVᵗ Var x₁ = if (TV= x x₁) ⊥ ⊤ + x ∉FVᵗ Fun f A = x ∉FVᵃ A + x ∉FVᵃ zero = ⊤ + x ∉FVᵃ next A t = (x ∉FVᵃ A) ∧ (x ∉FVᵗ t) + _∉FVᶠ_ : TV → Form → Prop + x ∉FVᶠ Rel R A = x ∉FVᵃ A + x ∉FVᶠ (A ⇒ A₁) = x ∉FVᶠ A ∧ x ∉FVᶠ A₁ + x ∉FVᶠ (A ∧∧ A₁) = x ∉FVᶠ A ∧ x ∉FVᶠ A₁ + x ∉FVᶠ ⊤⊤ = ⊤ + x ∉FVᶠ ∀∀ x₁ A = if (TV= x x₁) ⊤ (x ∉FVᶠ A) + _∉FVᶜ_ : TV → Con → Prop + x ∉FVᶜ [] = ⊤ + x ∉FVᶜ (A ∷ Γ) = x ∉FVᶠ A ∧ x ∉FVᶜ Γ + + data _⊢_ : Con → Form → Prop where + zero : A ∈ Γ → Γ ⊢ A + lam : (A ∷ Γ) ⊢ B → Γ ⊢ (A ⇒ B) + app : Γ ⊢ (A ⇒ B) → Γ ⊢ A → Γ ⊢ B + andi : Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧∧ B + ande₁ : Γ ⊢ A ∧∧ B → Γ ⊢ A + ande₂ : Γ ⊢ A ∧∧ B → Γ ⊢ B + true : Γ ⊢ ⊤⊤ + ∀-i : x ∉FVᶜ Γ → Γ ⊢ A → Γ ⊢ ∀∀ x A + ∀-e : Γ ⊢ ∀∀ x A → Γ ⊢ [ t / x ] A + + infix 5 _⊢_