add(Modal/Kripke): Makinson's Logic KTMk without Finite Modal Property (#354)

Author: SnO2WMaN

Foundation/Modal/Axioms.lean

@@ -1,5 +1,7 @@
 import Foundation.Modal.LogicSymbol
 
+-- TODO: move to `LO.Axioms.Modal`
+
 namespace LO.Axioms
 
 variable {F : Type*} [BasicModalLogicalConnective F]
@@ -82,3 +84,13 @@ protected abbrev H := □(□φ ⭤ φ) ➝ □φ
 protected abbrev Z := □(□φ ➝ φ) ➝ (◇□φ ➝ □φ)
 
 end LO.Axioms
+
+
+namespace LO.Axioms.Modal
+
+variable {F : Type*} [BasicModalLogicalConnective F]
+variable (φ ψ χ : F)
+
+protected abbrev Mk := □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ)
+
+end LO.Axioms.Modal

Foundation/Modal/Entailment/Basic.lean

@@ -505,6 +505,34 @@ end
 
 namespace Modal
 
+
+section HasAxiom
+
+variable {S F : Type*} [BasicModalLogicalConnective F] [Entailment F S]
+variable {𝓢 : S} {φ ψ : F}
+
+protected class HasAxiomMk [LogicalConnective F] [Box F](𝓢 : S) where
+  Mk (φ ψ : F) : 𝓢 ⊢ Axioms.Modal.Mk φ ψ
+
+section
+
+variable [Modal.HasAxiomMk 𝓢]
+
+def axiomMk : 𝓢 ⊢ □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ) := Modal.HasAxiomMk.Mk _ _
+@[simp] lemma axiomMk! : 𝓢 ⊢! □φ ⋏ ψ ➝ ◇(□□φ ⋏ ◇ψ) := ⟨axiomMk⟩
+
+variable [Entailment.Minimal 𝓢]
+
+instance (Γ : FiniteContext F 𝓢) : Modal.HasAxiomMk Γ := ⟨fun _ _ ↦ FiniteContext.of axiomMk⟩
+instance (Γ : Context F 𝓢) : Modal.HasAxiomMk Γ := ⟨fun _ _ ↦ Context.of axiomMk⟩
+
+end
+
+end HasAxiom
+
+
+section
+
 variable (𝓢 : S)
 
 protected class K extends Entailment.Cl 𝓢, Necessitation 𝓢, HasAxiomK 𝓢, HasDiaDuality 𝓢
@@ -575,6 +603,10 @@ protected class GLPoint3 extends Entailment.Modal.GL 𝓢, HasAxiomWeakPoint3 
 
 protected class Grz extends Entailment.Modal.K 𝓢, HasAxiomGrz 𝓢
 
+protected class KTMk (𝓢 : S) extends Entailment.Modal.KT 𝓢, Entailment.Modal.HasAxiomMk 𝓢
+
+end
+
 end Modal
 
 

Foundation/Modal/Entailment/KT.lean

@@ -6,7 +6,7 @@ namespace LO.Entailment
 
 open FiniteContext
 
-variable {S F : Type*} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S]
+variable {S F : Type*} [DecidableEq F] [BasicModalLogicalConnective F] [Entailment F S]
 variable {𝓢 : S}
 
 namespace KT
@@ -39,4 +39,19 @@ instance : Entailment.Modal.KD 𝓢 where
 end KT'
 
 
+section
+
+variable [Entailment.Modal.KT 𝓢]
+
+omit [DecidableEq F] in
+@[simp] lemma reduce_box_in_CAnt! : 𝓢 ⊢! □^[(i + n)]φ ➝ □^[i]φ := by
+  induction n with
+  | zero => simp;
+  | succ n ih =>
+    simp only [show (i + (n + 1)) = (i + n) + 1 by omega, Box.multibox_succ];
+    apply C!_trans ?_ ih;
+    apply axiomT!;
+
+end
+
 end LO.Entailment

Foundation/Modal/Hilbert/WellKnown.lean

@@ -241,6 +241,21 @@ instance [hM : H.HasM] : Entailment.HasAxiomM H where
     . use (λ b => if hM.p = b then φ else (.atom b));
       simp;
 
+class HasMk (H : Hilbert α) where
+  p : α
+  q : α
+  ne_pq : p ≠ q := by trivial;
+  mem_Mk : Axioms.Modal.Mk (.atom p) (.atom q) ∈ H.axioms := by tauto;
+
+instance [H.HasMk] : Entailment.Modal.HasAxiomMk H where
+  Mk φ ψ := by
+    apply maxm;
+    use Axioms.Modal.Mk (.atom $ HasMk.p H) (.atom $ HasMk.q H);
+    constructor;
+    . exact HasMk.mem_Mk;
+    . use (λ b => if b = (HasMk.q H) then ψ else if b = (HasMk.p H) then φ else (.atom b));
+      simp [HasMk.ne_pq];
+
 end
 
 protected abbrev KT : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0)}⟩
@@ -470,6 +485,12 @@ instance : (Hilbert.KD4Point3Z).HasWeakPoint3 where p := 0; q := 1;
 instance : (Hilbert.KD4Point3Z).HasZ where p := 0
 instance : Entailment.Modal.KD4Point3Z (Hilbert.KD4Point3Z) where
 
+protected abbrev KTMk : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0), Axioms.Modal.Mk (.atom 0) (.atom 1)}⟩
+instance : (Hilbert.KTMk).HasK where p := 0; q := 1;
+instance : (Hilbert.KTMk).HasT where p := 0
+instance : (Hilbert.KTMk).HasMk where p := 0; q := 1
+instance : Entailment.Modal.KTMk (Hilbert.KTMk) where
+
 protected abbrev N : Hilbert ℕ := ⟨{}⟩
 
 end Hilbert

Foundation/Modal/Kripke/AxiomMk.lean

@@ -0,0 +1,120 @@
+import Foundation.Modal.Kripke.Completeness
+
+
+
+section
+
+variable {α : Type u} (rel : α → α → Prop)
+
+def MakinsonCondition := ∀ x, ∃ y, rel x y ∧ rel y x ∧ (∀ z, Rel.iterate rel 2 y z → rel x z)
+
+class SatisfiesMakinsonCondition (α) (rel : α → α → Prop) : Prop where
+  mkCondition : MakinsonCondition rel
+
+end
+
+
+
+
+namespace LO.Modal
+
+open Formula.Kripke
+
+namespace Kripke
+
+section definability
+
+variable {F : Kripke.Frame}
+
+lemma validate_axiomMk_of_makinsonCondition (h : MakinsonCondition F.Rel) : F ⊧ (Axioms.Modal.Mk (.atom 0) (.atom 1)) := by
+  intro V x hx;
+  replace ⟨hx₁, hx₂⟩ := Satisfies.and_def.mp hx;
+  obtain ⟨y, Rxy, Ryx, hz⟩ := @h x;
+  apply Satisfies.dia_def.mpr;
+  use y;
+  constructor;
+  . assumption;
+  . apply Satisfies.and_def.mpr;
+    constructor;
+    . suffices Satisfies ⟨F, V⟩ y (□^[2](.atom 0)) by simpa using this;
+      apply Satisfies.multibox_def.mpr
+      intro z Ryz;
+      apply hx₁;
+      apply hz;
+      exact Ryz;
+    . apply Satisfies.dia_def.mpr;
+      use x;
+
+lemma validate_axiomMk_of_satisfiesMakinsonCondition [SatisfiesMakinsonCondition _ F.Rel] : F ⊧ (Axioms.Modal.Mk (.atom 0) (.atom 1)) :=
+  validate_axiomMk_of_makinsonCondition SatisfiesMakinsonCondition.mkCondition
+
+instance : SatisfiesMakinsonCondition _ whitepoint := ⟨by
+  intro x;
+  use x;
+  tauto;
+⟩
+
+end definability
+
+section canonicality
+
+variable {S} [Entailment (Formula ℕ) S]
+variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Modal.K 𝓢]
+
+open Formula.Kripke
+open Entailment
+     Entailment.FiniteContext
+open Entailment.Modal
+open canonicalModel
+open MaximalConsistentTableau
+
+namespace Canonical
+
+open Classical in
+instance [Entailment.HasAxiomT 𝓢] [Entailment.Modal.HasAxiomMk 𝓢] : SatisfiesMakinsonCondition _ (canonicalFrame 𝓢).Rel := ⟨by
+  sorry;
+  /-
+  rintro x;
+  obtain ⟨y, hy⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := ⟨x.1.1.prebox, x.1.2.box ∪ x.1.2.dia⟩) $ by
+    rintro Γ Δ hΓ hΔ;
+    by_contra! hC;
+    let Δ₁ := { φ ∈ Δ | φ ∈ x.1.2.box };
+    let Δ₂ := { φ ∈ Δ | φ ∈ x.1.2.dia };
+    have eΔ : Δ = Δ₁ ∪ Δ₂ := by
+      ext φ;
+      simp only [Set.mem_image, Function.iterate_one, Finset.mem_union, Finset.mem_filter, Δ₁, Δ₂];
+      constructor;
+      . rintro h;
+        rcases hΔ h with h₁ | h₂ <;> tauto;
+      . tauto;
+    rw [eΔ] at hC;
+    have : 𝓢 ⊢! Γ.conj ➝ Δ₁.disj ⋎ Δ₂.disj := C!_trans hC CFdisjUnionAFdisj;
+    have : 𝓢 ⊢! □Γ.prebox.conj ➝ Δ₁.disj ⋎ Δ₂.disj := C!_trans (by
+      apply right_Fconj!_intro;
+      intro φ hφ;
+      have := hΓ hφ;
+      simp at this;
+      sorry
+    ) this;
+    sorry;
+  use y;
+  refine ⟨?_, ?_, ?_⟩;
+  . exact hy.1;
+  . apply def_rel_box_mem₂.mpr;
+    intro φ hφ;
+    exact @hy.2 (□φ) (by left; simpa);
+  . rintro z Ryz;
+    apply def_rel_dia_mem₂.mpr;
+    intro φ hφ;
+    apply def_multirel_multidia_mem₂.mp Ryz;
+    exact @hy.2 (◇◇φ) (by simpa);
+  -/
+⟩
+
+end Canonical
+
+end canonicality
+
+end Kripke
+
+end LO.Modal

Foundation/Modal/Kripke/Basic.lean

@@ -147,6 +147,8 @@ lemma multibox_dn : x ⊧ □^[n](∼∼φ) ↔ x ⊧ □^[n]φ := by
     . intro h y Rxy;
       exact ih.mpr $ (h y Rxy);
 
+lemma box_dn : x ⊧ □(∼∼φ) ↔ x ⊧ □φ := multibox_dn (n := 1)
+
 lemma multidia_dn : x ⊧ ◇^[n](∼∼φ) ↔ x ⊧ ◇^[n]φ := by
   induction n generalizing x with
   | zero => simp;
@@ -168,6 +170,8 @@ lemma multidia_dn : x ⊧ ◇^[n](∼∼φ) ↔ x ⊧ ◇^[n]φ := by
       . exact Rxy;
       . exact ih.mpr h;
 
+lemma dia_dn : x ⊧ ◇(∼∼φ) ↔ x ⊧ ◇φ := multidia_dn (n := 1)
+
 lemma multibox_def : x ⊧ □^[n]φ ↔ ∀ {y}, x ≺^[n] y → y ⊧ φ := by
   induction n generalizing x with
   | zero => simp;

Foundation/Modal/Kripke/Completeness.lean

@@ -145,7 +145,7 @@ open Formula.Kripke.Satisfies
 
 variable {x y : (canonicalModel 𝓢).World}
 
-lemma def_rel_box_mem₁ : x ≺ y ↔ ∀ {φ}, □φ ∈ x.1.1 → φ ∈ y.1.1 := by simp [Frame.Rel']; aesop;
+lemma def_rel_box_mem₁ : x ≺ y ↔ x.1.1.prebox ⊆ y.1.1 := by simp [Frame.Rel'];
 
 lemma def_rel_box_satisfies : x ≺ y ↔ ∀ {φ}, x ⊧ □φ → y ⊧ φ := by
   constructor;
@@ -205,11 +205,32 @@ lemma def_multirel_multibox_satisfies : x ≺^[n] y ↔ (∀ {φ}, x ⊧ □^[n]
         intro φ hφ;
         simpa using (Set.compl_subset_compl.mpr ht.2) $ iff_not_mem₂_mem₁.mpr $ truthlemma₁.mpr hφ
 
-lemma def_multirel_multibox_mem₁ : x ≺^[n] y ↔ (∀ {φ}, □^[n]φ ∈ x.1.1 → φ ∈ y.1.1) := ⟨
+lemma def_multirel_multibox_mem₁ : x ≺^[n] y ↔ (x.1.1.premultibox n ⊆ y.1.1) := ⟨
   fun h _ hφ => truthlemma₁.mpr $ def_multirel_multibox_satisfies.mp h $ truthlemma₁.mp hφ,
   fun h => def_multirel_multibox_satisfies.mpr fun hφ => truthlemma₁.mp (h $ truthlemma₁.mpr hφ)
 ⟩
 
+lemma def_multirel_multibox_mem₂ : x ≺^[n] y ↔ (y.1.2 ⊆ x.1.2.premultibox n) := by
+  apply Iff.trans def_multirel_multibox_mem₁;
+  constructor;
+  . intro h φ;
+    contrapose!;
+    intro hφ;
+    apply iff_not_mem₂_mem₁.mpr;
+    apply h;
+    apply iff_not_mem₂_mem₁.mp;
+    assumption;
+  . intro h φ;
+    contrapose!;
+    intro hφ;
+    apply iff_not_mem₁_mem₂.mpr;
+    apply h;
+    apply iff_not_mem₁_mem₂.mp;
+    assumption;
+
+lemma def_rel_box_mem₂ : x ≺ y ↔ (y.1.2 ⊆ x.1.2.prebox) := by
+  simpa using def_multirel_multibox_mem₂ (n := 1);
+
 lemma def_multirel_multidia_satisfies : x ≺^[n] y ↔ (∀ {φ}, y ⊧ φ → x ⊧ ◇^[n]φ) := by
   constructor;
   . intro h φ hφ;
@@ -228,15 +249,15 @@ lemma def_multirel_multidia_satisfies : x ≺^[n] y ↔ (∀ {φ}, y ⊧ φ →
     intro _ _;
     apply negneg_def.mpr;
 
-lemma def_multirel_multidia_mem₁ : x ≺^[n] y ↔ (∀ {φ}, φ ∈ y.1.1 → ◇^[n]φ ∈ x.1.1) := ⟨
+lemma def_multirel_multidia_mem₁ : x ≺^[n] y ↔ (y.1.1 ⊆ x.1.1.premultidia n) := ⟨
   fun h _ hφ => truthlemma₁.mpr $ def_multirel_multidia_satisfies.mp h (truthlemma₁.mp hφ),
   fun h => def_multirel_multidia_satisfies.mpr fun hφ => truthlemma₁.mp $ h (truthlemma₁.mpr hφ)
 ⟩
 
-lemma def_rel_dia_mem₁ : x ≺ y ↔ (∀ {φ}, φ ∈ y.1.1 → ◇φ ∈ x.1.1) := by
+lemma def_rel_dia_mem₁ : x ≺ y ↔ (y.1.1 ⊆ x.1.1.predia) := by
   simpa using def_multirel_multidia_mem₁ (n := 1);
 
-lemma def_multirel_multidia_mem₂ : x ≺^[n] y ↔ (∀ {φ}, ◇^[n]φ ∈ x.1.2 → φ ∈ y.1.2) := by
+lemma def_multirel_multidia_mem₂ : x ≺^[n] y ↔ (x.1.2.premultidia n ⊆ y.1.2) := by
   constructor;
   . intro Rxy φ;
     contrapose;
@@ -251,7 +272,7 @@ lemma def_multirel_multidia_mem₂ : x ≺^[n] y ↔ (∀ {φ}, ◇^[n]φ ∈ x.
     intro hφ;
     exact iff_not_mem₁_mem₂.mpr $ @H φ (iff_not_mem₁_mem₂.mp hφ);
 
-lemma def_rel_dia_mem₂ : x ≺ y ↔ (∀ {φ}, ◇φ ∈ x.1.2 → φ ∈ y.1.2) := by
+lemma def_rel_dia_mem₂ : x ≺ y ↔ (x.1.2.predia ⊆ y.1.2) := by
   simpa using def_multirel_multidia_mem₂ (n := 1);
 
 end canonicalModel