semantics

Foundation/FirstOrder/Basic/Semantics/Semantics.lean

@@ -24,6 +24,8 @@ structure Struc (L : Language) where
 
 abbrev SmallStruc (L : Language.{u}) := Struc.{u, u} L
 
+instance : CoeSort (Struc L) (Type _) := ⟨Struc.Dom⟩
+
 namespace Structure
 
 instance [n : Nonempty M] : Nonempty (Structure L M) := by

Foundation/IntFO/Basic/Deduction.lean

@@ -115,6 +115,7 @@ def allIffAllOfIff {φ ψ} (b : Λ ⊢ free φ ⭤ free ψ) : Λ ⊢ ∀' φ ⭤
   (allImplyAllOfAllImply φ ψ ⨀ gen (System.cast (by simp) (System.andLeft b)))
   (allImplyAllOfAllImply ψ φ ⨀ gen (System.cast (by simp) (System.andRight b)))
 
+set_option diagnostics true in
 set_option profiler true in
 def dneOfNegative : {φ : SyntacticFormulaᵢ L} → φ.IsNegative → Λ ⊢ ∼∼φ ➝ φ
   | ⊥,     _ => System.falsumDNE

Foundation/IntFO/Basic/Kripke.lean

@@ -0,0 +1,163 @@
+import Foundation.Logic.Kripke.Basic
+import Foundation.IntFO.Basic.Deduction
+
+namespace LO.Kripke
+
+open Frame
+
+structure PreOrderFrame extends Frame, IsPreorder World Rel
+
+namespace PreOrderFrame
+
+instance : CoeSort PreOrderFrame (Type u) := ⟨fun F ↦ PreOrderFrame.toFrame F⟩
+
+instance (F : PreOrderFrame) : IsPreorder F (· ≺ ·) := F.toIsPreorder
+
+variable {F : PreOrderFrame}
+
+@[refl, simp] lemma rel_refl (w : F) : w ≺ w := IsRefl.refl w
+
+@[trans] lemma rel_trans {w v z : F} : w ≺ v → v ≺ z → w ≺ z := IsTrans.trans w v z
+
+end PreOrderFrame
+
+end LO.Kripke
+
+namespace LO.FirstOrder
+
+structure KripkeModel (L : Language) where
+  Frame : Kripke.PreOrderFrame
+  Dom : Frame → Struc L
+  wire (w v : Frame) : w ≺ v → Dom w ↪ Dom v
+  wire_refl (w : Frame) : wire w w (IsRefl.refl _) = Function.Embedding.refl _
+  wire_trans (w v z : Frame) (hxy : w ≺ v) (hyz : v ≺ z) :
+    wire v z hyz ∘ wire w v hxy = wire w z (IsTrans.trans w v z hxy hyz)
+  monotone {w v : Frame} {k} (R : L.Rel k) (a : Fin k → Dom w) :
+    (hxy : w ≺ v) → (Dom w).struc.rel R a → (Dom v).struc.rel R fun i ↦ wire w v hxy (a i)
+  wire_func {w v : Frame} {k} (f : L.Func k) (a : Fin k → Dom w) (hwv : w ≺ v) :
+    wire w v hwv ((Dom w).struc.func f a) = (Dom v).struc.func f fun i ↦ wire w v hwv (a i)
+
+instance : CoeSort (KripkeModel L) (Type _) := ⟨fun 𝓚 ↦ 𝓚.Frame⟩
+
+attribute [simp] KripkeModel.wire_refl
+
+namespace KripkeModel
+
+variable {L : Language} {𝓚 : KripkeModel L}
+
+abbrev Domain (w : 𝓚) : Struc L := 𝓚.Dom w
+
+def Val {n} (w : 𝓚) (bv : Fin n → Domain w) (fv : ξ → Domain w) : Semiformulaᵢ L ξ n → Prop
+  | .rel R t => (Domain w).struc.rel R fun i ↦ Semiterm.val (Domain w).struc bv fv (t i)
+  | ⊤        => True
+  | ⊥        => False
+  | φ ⋏ ψ    => Val w bv fv φ ∧ Val w bv fv ψ
+  | φ ⋎ ψ    => Val w bv fv φ ∨ Val w bv fv ψ
+  | φ ➝ ψ    => ∀ v, (hwv : w ≺ v) →
+    Val v (fun x ↦ 𝓚.wire w v hwv (bv x)) (fun x ↦ 𝓚.wire w v hwv (fv x)) φ →
+    Val v (fun x ↦ 𝓚.wire w v hwv (bv x)) (fun x ↦ 𝓚.wire w v hwv (fv x)) ψ
+  | ∀' φ     => ∀ v, (hwv : w ≺ v) →
+    ∀ x : Domain v, Val v (x :> fun x ↦ 𝓚.wire w v hwv (bv x)) (fun x ↦ 𝓚.wire w v hwv (fv x)) φ
+  | ∃' φ     => ∃ x : Domain w, Val w (x :> bv) fv φ
+
+scoped notation:45 w " ⊩[" bv "|" fv "] " φ:46 => Val w bv fv φ
+
+variable (w : 𝓚) (bv : Fin n → Domain w) (fv : ξ → Domain w)
+
+@[simp] lemma val_verum : w ⊩[bv|fv] ⊤ := by trivial
+
+@[simp] lemma val_falsum : ¬w ⊩[bv|fv] ⊥ := by rintro ⟨⟩
+
+variable {w bv fv}
+
+@[simp] lemma val_rel {k} {R : L.Rel k} {t} :
+    w ⊩[bv|fv] .rel R t ↔ (Domain w).struc.rel R fun i ↦ Semiterm.val (Domain w).struc bv fv (t i) := by rfl
+
+@[simp] lemma val_and {φ ψ : Semiformulaᵢ L ξ n} : w ⊩[bv|fv] φ ⋏ ψ ↔ w ⊩[bv|fv] φ ∧ w ⊩[bv|fv] ψ := by rfl
+
+@[simp] lemma val_or {φ ψ : Semiformulaᵢ L ξ n} : w ⊩[bv|fv] φ ⋎ ψ ↔ w ⊩[bv|fv] φ ∨ w ⊩[bv|fv] ψ := by rfl
+
+@[simp] lemma val_imply {φ ψ : Semiformulaᵢ L ξ n} :
+    w ⊩[bv|fv] φ ➝ ψ ↔
+    ∀ v, (hwv : w ≺ v) →
+      v ⊩[fun x ↦ 𝓚.wire w v hwv (bv x)|fun x ↦ 𝓚.wire w v hwv (fv x)] φ →
+      v ⊩[fun x ↦ 𝓚.wire w v hwv (bv x)|fun x ↦ 𝓚.wire w v hwv (fv x)] ψ := by rfl
+
+@[simp] lemma val_all {φ : Semiformulaᵢ L ξ (n + 1)} :
+    w ⊩[bv|fv] ∀' φ ↔
+    ∀ v, (hwv : w ≺ v) →
+      ∀ x : Domain v, v ⊩[x :> fun x ↦ 𝓚.wire w v hwv (bv x)|fun x ↦ 𝓚.wire w v hwv (fv x)] φ := by rfl
+
+@[simp] lemma val_ex {φ : Semiformulaᵢ L ξ (n + 1)} :
+    w ⊩[bv|fv] ∃' φ ↔ ∃ x : Domain w, w ⊩[x :> bv|fv] φ := by rfl
+
+@[simp] lemma val_neg {φ : Semiformulaᵢ L ξ n} :
+    w ⊩[bv|fv] ∼φ ↔
+    ∀ v, (hwv : w ≺ v) → ¬v ⊩[fun x ↦ 𝓚.wire w v hwv (bv x)|fun x ↦ 𝓚.wire w v hwv (fv x)] φ := by rfl
+
+lemma wire_val (t : Semiterm L ξ n) {v : 𝓚} (hwv : w ≺ v) :
+    𝓚.wire w v hwv (t.val (Domain w).struc bv fv) =
+    t.val (Domain v).struc (fun x ↦ 𝓚.wire w v hwv (bv x)) (fun x ↦ 𝓚.wire w v hwv (fv x)) := by
+  induction t <;> simp [Semiterm.val_func, wire_func, *]
+
+@[simp] lemma val_rew {bv : Fin n₂ → Domain w} {fv : ξ₂ → Domain w} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformulaᵢ L ξ₁ n₁} :
+    w ⊩[bv|fv] (ω • φ) ↔
+    w ⊩[fun x ↦ (ω #x).val (Domain w).struc bv fv|fun x ↦ (ω &x).val (Domain w).struc bv fv] φ := by
+  induction φ using Semiformulaᵢ.rec' generalizing n₂ w
+  case hRel k R t =>
+    simp only [Semiformulaᵢ.rew_rel, val_rel]
+    apply iff_of_eq; congr; funext x
+    simp [Semiterm.val_rew ω (t x), Function.comp_def]
+  case hImp φ ψ ihφ ihψ =>
+    simp only [Rewriting.smul_imp, val_imply, Function.comp_apply, wire_val]
+    constructor
+    · intro h v hwv hφ
+      simpa [Function.comp_def] using ihψ.mp <| h v hwv (ihφ.mpr <| by simpa [Function.comp_def, wire_val] using hφ)
+    · intro h v hwv hφ
+      exact ihψ.mpr <| h v hwv <| by simpa [Function.comp_def] using ihφ.mp hφ
+  case hAnd φ ψ ihφ ihψ => simp [ihφ, ihψ]
+  case hOr φ ψ ihφ ihψ => simp [ihφ, ihψ]
+  case hVerum => simp
+  case hFalsum => simp
+  case hAll φ ih =>
+    constructor
+    · simp only [Rewriting.smul_all, val_all, Nat.succ_eq_add_one, wire_val]
+      intro h v hwv x
+      exact cast (by congr; { funext x; cases x using Fin.cases <;> simp }; { simp }) <| ih.mp <| h v hwv x
+    · simp only [val_all, Nat.succ_eq_add_one, wire_val, Rewriting.smul_all]
+      intro h v hwv x
+      apply ih.mpr
+      exact cast (by congr; { funext x; cases x using Fin.cases <;> simp }; { simp }) <| h v hwv x
+  case hEx φ ih =>
+    constructor
+    · simp only [Rewriting.smul_ex, val_ex, Nat.succ_eq_add_one, forall_exists_index]
+      intro x h
+      exact ⟨x, cast (by congr; { funext x; cases x using Fin.cases <;> simp }; { simp }) (ih.mp h)⟩
+    · simp only [val_ex, Nat.succ_eq_add_one, Rewriting.smul_ex, forall_exists_index]
+      intro x h
+      exact ⟨x, ih.mpr <| cast (by congr; { funext x; cases x using Fin.cases <;> simp }; { simp }) h⟩
+
+variable (𝓚)
+
+def Force (φ : Semiformulaᵢ L ξ n) : Prop := ∀ (w : 𝓚) bv fv, w ⊩[bv|fv] φ
+
+scoped infix:45 " ⊩ " => Force
+
+instance : Semantics (SyntacticFormulaᵢ L) (KripkeModel L) := ⟨fun 𝓚 φ ↦ 𝓚.Force φ⟩
+
+variable {𝓚}
+
+variable {Λ : Hilbertᵢ L}
+
+open HilbertProofᵢ Semantics
+
+/-
+theorem sound (H : 𝓚 ⊧* Λ) : Λ ⊢ φ → 𝓚 ⊧ φ
+  | eaxm h => RealizeSet.realize 𝓚 h
+  | @mdp _ _ φ ψ bφψ bφ => fun w bv fv ↦ by simpa using sound H bφψ w bv fv w (by simp) (sound H bφ w _ _)
+  | @gen _ _ φ b        => fun w bv fv v hwv x ↦ by { have := sound H b v ![] }
+-/
+
+end KripkeModel
+
+end LO.FirstOrder

Foundation/IntFO/Translation.lean

@@ -112,13 +112,13 @@ def goedelGentzen {Γ : Sequent L} : ⊢ᵀ Γ → (∼Γ)ᴺ ⊢[𝐌𝐢𝐧¹
     have : ((∼φ)ᴺ ⋏ (∼ψ)ᴺ :: (∼Γ)ᴺ) ⊢[𝐌𝐢𝐧¹] ⊥ :=
       System.FiniteContext.weakening (by simp) this ⨀ (andRight (nthAxm 0)) ⨀ (andLeft (nthAxm 0))
     this
-  | @all _ _ Γ φ d =>
+  | @all _ _ Γ φ d       =>
     have eΓ : (∼Γ⁺)ᴺ = ((∼Γ)ᴺ)⁺ := by
       simp [Sequent.doubleNegation, Rewriting.shifts, Sequent.neg_def, Semiformula.rew_doubleNegation]
     have : ((∼Γ)ᴺ)⁺ ⊢[𝐌𝐢𝐧¹] free (∼(∼φ)ᴺ) :=
       FiniteContext.cast (deduct (goedelGentzen d)) eΓ (by simp [Semiformula.rew_doubleNegation]; rfl)
     deductInv <| dni' <| genOverFiniteContext this
-  | @ex _ _ Γ φ t d =>
+  | @ex _ _ Γ φ t d      =>
     have ih : (∼Γ)ᴺ ⊢[𝐌𝐢𝐧¹] ∼((∼φ)ᴺ/[t]) :=
       System.cast (by simp [Semiformula.rew_doubleNegation]; rfl) <| deduct (goedelGentzen d)
     have : ((∀' (∼φ)ᴺ) :: (∼Γ)ᴺ) ⊢[𝐌𝐢𝐧¹] (∼φ)ᴺ/[t] := specializeOverContext (nthAxm 0) t
@@ -129,7 +129,7 @@ def goedelGentzen {Γ : Sequent L} : ⊢ᵀ Γ → (∼Γ)ᴺ ⊢[𝐌𝐢𝐧¹
     have b₁ : (∼Γ)ᴺ ⊢[𝐌𝐢𝐧¹] ∼∼φᴺ := System.impTrans'' (of <| System.andLeft (negDoubleNegation φ)) (deduct ihp)
     have b₂ : (∼Γ)ᴺ ⊢[𝐌𝐢𝐧¹] ∼φᴺ := deduct ihn
     b₁ ⨀ b₂
-  | @wk _ _ Γ Δ d h => FiniteContext.weakening (by simpa using List.map_subset _ h) (goedelGentzen d)
+  | @wk _ _ Γ Δ d h      => FiniteContext.weakening (by simpa using List.map_subset _ h) (goedelGentzen d)
 
 end Derivation