feat(Modal/Kripke): Kripke Completeness of Logics with McKinsey Axioms (#212)

Author: SnO2WMaN

Foundation/Logic/HilbertStyle/Basic.lean

@@ -327,6 +327,7 @@ def Conj_intro (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢ φ) : 𝓢
   match Γ with
   |     [] => verum
   | ψ :: Γ => K_intro (b ψ (by simp)) (Conj_intro Γ (fun ψ hq ↦ b ψ (by simp [hq])))
+lemma Conj!_intro {Γ : List F} (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢! φ) : 𝓢 ⊢! Γ.conj := ⟨Conj_intro Γ λ φ hφ => (b φ hφ).some⟩
 
 def right_Conj_intro (φ : F) (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢ φ ➝ ψ) : 𝓢 ⊢ φ ➝ Γ.conj :=
   match Γ with

Foundation/Logic/HilbertStyle/Supplemental.lean

@@ -148,6 +148,9 @@ lemma K!_assoc : 𝓢 ⊢! (φ ⋏ ψ) ⋏ χ ⭤ φ ⋏ (ψ ⋏ χ) := by
     . exact K!_intro hp hq;
     . exact hr;
 
+omit [DecidableEq F] in lemma K!_assoc_mp (h : 𝓢 ⊢! (φ ⋏ ψ) ⋏ χ) : 𝓢 ⊢! φ ⋏ (ψ ⋏ χ) := C_of_E_mp! K!_assoc ⨀ h
+omit [DecidableEq F] in lemma K!_assoc_mpr (h : 𝓢 ⊢! φ ⋏ (ψ ⋏ χ)) : 𝓢 ⊢! (φ ⋏ ψ) ⋏ χ := C_of_E_mpr! K!_assoc ⨀ h
+
 def K_replace_left (hc : 𝓢 ⊢ φ ⋏ ψ) (h : 𝓢 ⊢ φ ➝ χ) : 𝓢 ⊢ χ ⋏ ψ := K_intro (h ⨀ K_left hc) (K_right hc)
 omit [DecidableEq F] in lemma K!_replace_left (hc : 𝓢 ⊢! φ ⋏ ψ) (h : 𝓢 ⊢! φ ➝ χ) : 𝓢 ⊢! χ ⋏ ψ := ⟨K_replace_left hc.some h.some⟩
 

Foundation/Modal/Entailment/Basic.lean

@@ -461,6 +461,21 @@ instance (Γ : Context F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ Context.of axiomZ
 end
 
 
+class HasAxiomM (𝓢 : S) where
+  M (φ : F) : 𝓢 ⊢ Axioms.M φ
+
+section
+
+variable [HasAxiomM 𝓢]
+
+def axiomM : 𝓢 ⊢ □◇φ ➝ ◇□φ := HasAxiomM.M _
+@[simp] lemma axiomM! : 𝓢 ⊢! □◇φ ➝ ◇□φ := ⟨axiomM⟩
+
+variable [Entailment.Minimal 𝓢]
+instance (Γ : FiniteContext F 𝓢) : HasAxiomM Γ := ⟨fun _ ↦ FiniteContext.of axiomM⟩
+instance (Γ : Context F 𝓢) : HasAxiomM Γ := ⟨fun _ ↦ Context.of axiomM⟩
+
+end
 
 section
 
@@ -530,9 +545,12 @@ instance [Entailment.Modal.Triv 𝓢] : Entailment.Modal.KTc 𝓢 where
 
 protected class Ver extends Entailment.Modal.K 𝓢, HasAxiomVer 𝓢
 
+protected class KM extends Entailment.Modal.K 𝓢, HasAxiomM 𝓢
+
 protected class K4 extends Entailment.Modal.K 𝓢, HasAxiomFour 𝓢
-protected class K4Point2 extends Entailment.Modal.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakPoint2 𝓢
-protected class K4Point3 extends Entailment.Modal.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakPoint3 𝓢
+protected class K4Point1 extends Entailment.Modal.K4 𝓢, HasAxiomM 𝓢
+protected class K4Point2 extends Entailment.Modal.K4 𝓢, HasAxiomWeakPoint2 𝓢
+protected class K4Point3 extends Entailment.Modal.K4 𝓢, HasAxiomWeakPoint3 𝓢
 protected class KD4Point3Z extends Entailment.Modal.K 𝓢, HasAxiomD 𝓢, HasAxiomFour 𝓢, HasAxiomWeakPoint3 𝓢, HasAxiomZ 𝓢
 
 protected class K5 extends Entailment.Modal.K 𝓢, HasAxiomFive 𝓢
@@ -541,6 +559,8 @@ protected class S4 extends Entailment.Modal.K 𝓢, HasAxiomT 𝓢, HasAxiomFour
 instance [Entailment.Modal.S4 𝓢] : Entailment.Modal.K4 𝓢 where
 instance [Entailment.Modal.S4 𝓢] : Entailment.Modal.KT 𝓢 where
 
+protected class S4Point1 extends Entailment.Modal.S4 𝓢, HasAxiomM 𝓢
+
 protected class S4Point2 extends Entailment.Modal.S4 𝓢, HasAxiomPoint2 𝓢
 
 protected class S4Point3 extends Entailment.Modal.S4 𝓢, HasAxiomPoint3 𝓢

Foundation/Modal/Entailment/K.lean

@@ -161,6 +161,8 @@ def diaK' (h : 𝓢 ⊢ φ ➝ ψ) : 𝓢 ⊢ ◇φ ➝ ◇ψ := by
   assumption;
 lemma diaK'! (h : 𝓢 ⊢! φ ➝ ψ) : 𝓢 ⊢! ◇φ ➝ ◇ψ := ⟨diaK' h.some⟩
 
+lemma diaK''! (h₁ : 𝓢 ⊢! φ ➝ ψ) (h₂ : 𝓢 ⊢! ◇φ) : 𝓢 ⊢! ◇ψ := (diaK'! h₁) ⨀ h₂
+
 lemma CMultidiaMultidia_of_C (h : 𝓢 ⊢! φ ➝ ψ) : 𝓢 ⊢! ◇^[n]φ ➝ ◇^[n]ψ := by
   induction n with
   | zero => simpa;
@@ -221,6 +223,15 @@ def boxDuality_mpr : 𝓢 ⊢ ∼(◇(∼φ)) ➝ □φ := K_right boxDuality
 def boxDuality_mpr' (h : 𝓢 ⊢ ∼(◇(∼φ))) : 𝓢 ⊢ □φ := boxDuality_mpr ⨀ h
 lemma boxDuality_mpr'! (h : 𝓢 ⊢! ∼(◇(∼φ))) : 𝓢 ⊢! □φ := ⟨boxDuality_mpr' h.some⟩
 
+@[simp]
+lemma CNDiaBoxN! : 𝓢 ⊢! □(∼φ) ➝ ∼◇φ := by
+  apply C!_trans boxDuality_mp!;
+  apply contra!;
+  apply diaK'!;
+  simp;
+
+lemma NDia_of_BoxN! (h : 𝓢 ⊢! □(∼φ)) : 𝓢 ⊢! ∼◇φ := CNDiaBoxN! ⨀ h
+
 lemma multibox_duality'! : 𝓢 ⊢! □^[n]φ ↔ 𝓢 ⊢! ∼(◇^[n](∼φ)) := by
   constructor;
   . intro h; exact (K!_left multibox_duality!) ⨀ h;

Foundation/Modal/Entailment/K4.lean

@@ -7,6 +7,16 @@ open FiniteContext
 variable {S F : Type*} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S]
 variable {𝓢 : S} [Entailment.Modal.K4 𝓢]
 
+@[simp]
+lemma diaFour! : 𝓢 ⊢! ◇◇φ ➝ ◇φ := by
+  apply C!_replace diaDuality_mp! diaDuality_mpr!;
+  apply contra!;
+  suffices 𝓢 ⊢! □□(∼φ) ➝ □(∼◇φ) by apply C!_trans axiomFour! this;
+  apply axiomK'!;
+  apply nec!;
+  simp;
+lemma diaFour'! (h : 𝓢 ⊢! ◇◇φ) : 𝓢 ⊢! ◇φ := diaFour! ⨀ h
+
 def imply_BoxBoxdot_Box: 𝓢 ⊢  □⊡φ ➝ □φ := by
   exact C_trans distribute_box_and and₁
 @[simp] lemma imply_boxboxdot_box : 𝓢 ⊢! □⊡φ ➝ □φ := ⟨imply_BoxBoxdot_Box⟩

Foundation/Modal/Hilbert/WellKnown.lean

@@ -228,6 +228,19 @@ instance [hZ : H.HasZ] : Entailment.HasAxiomZ H where
     . use (λ b => if hZ.p = b then φ else (.atom b));
       simp;
 
+class HasM (H : Hilbert α) where
+  p : α
+  mem_M : Axioms.M (.atom p) ∈ H.axioms := by tauto;
+
+instance [hM : H.HasM] : Entailment.HasAxiomM H where
+  M φ := by
+    apply maxm;
+    use Axioms.M (.atom hM.p);
+    constructor;
+    . exact hM.mem_M;
+    . use (λ b => if hM.p = b then φ else (.atom b));
+      simp;
+
 end
 
 protected abbrev KT : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0)}⟩
@@ -261,12 +274,31 @@ instance : (Hilbert.KTB).HasT where p := 0
 instance : (Hilbert.KTB).HasB where p := 0
 instance : Entailment.Modal.KTB (Hilbert.KTB) where
 
+protected abbrev KM : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.M (.atom 0)}⟩
+instance : (Hilbert.KM).HasK where p := 0; q := 1;
+instance : (Hilbert.KM).HasM where p := 0
+instance : Entailment.Modal.KM (Hilbert.KM) where
+
+instance K_weakerThan_KM : Hilbert.K ⪯ Hilbert.KM := weakerThan_of_dominate_axioms $ by simp;
 
 protected abbrev K4 : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.Four (.atom 0)}⟩
 instance : (Hilbert.K4).HasK where p := 0; q := 1;
 instance : (Hilbert.K4).HasFour where p := 0
 instance : Entailment.Modal.K4 (Hilbert.K4) where
 
+protected abbrev K4Point1 : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.Four (.atom 0), Axioms.M (.atom 0)}⟩
+instance : (Hilbert.K4Point1).HasK where p := 0; q := 1;
+instance : (Hilbert.K4Point1).HasFour where p := 0
+instance : (Hilbert.K4Point1).HasM where p := 0
+instance : Entailment.Modal.K4Point1 (Hilbert.K4Point1) where
+
+instance K_weakerThan_K4Point1 : Hilbert.K ⪯ Hilbert.K4Point1 := weakerThan_of_dominate_axioms $ by simp;
+
+noncomputable instance {H : Hilbert _} [Hilbert.K4Point1 ⪯ H] : Entailment.Modal.K4Point1 H where
+  K _ _ := Entailment.WeakerThan.pbl (𝓢 := Hilbert.K4Point1) (by simp) |>.some
+  Four _ := Entailment.WeakerThan.pbl (𝓢 := Hilbert.K4Point1) (by simp) |>.some
+  M _ := Entailment.WeakerThan.pbl (𝓢 := Hilbert.K4Point1) (by simp) |>.some
+
 protected abbrev K4Point2 : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.Four (.atom 0), Axioms.WeakPoint2 (.atom 0) (.atom 1)}⟩
 instance : (Hilbert.K4Point2).HasK where p := 0; q := 1;
 instance : (Hilbert.K4Point2).HasFour where p := 0
@@ -335,7 +367,16 @@ instance : (Hilbert.S4).HasT where p := 0
 instance : (Hilbert.S4).HasFour where p := 0
 instance : Entailment.Modal.S4 (Hilbert.S4) where
 
-lemma K4_weakerThan_S4 : Hilbert.K4 ⪯ Hilbert.S4 := weakerThan_of_dominate_axioms $ by simp;
+instance K4_weakerThan_S4 : Hilbert.K4 ⪯ Hilbert.S4 := weakerThan_of_dominate_axioms $ by simp;
+
+protected abbrev S4Point1 : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0), Axioms.Four (.atom 0), Axioms.M (.atom 0)}⟩
+instance : (Hilbert.S4Point1).HasK where p := 0; q := 1;
+instance : (Hilbert.S4Point1).HasT where p := 0
+instance : (Hilbert.S4Point1).HasFour where p := 0
+instance : (Hilbert.S4Point1).HasM where p := 0
+instance : Entailment.Modal.S4Point1 (Hilbert.S4Point1) where
+
+instance K4Point1_weakerThan_S4Point1 : Hilbert.K4Point1 ⪯ Hilbert.S4Point1 := weakerThan_of_dominate_axioms $ by simp;
 
 protected abbrev S4Point2 : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0), Axioms.Four (.atom 0), Axioms.Point2 (.atom 0)}⟩
 instance : (Hilbert.S4Point2).HasK where p := 0; q := 1;
@@ -421,7 +462,6 @@ instance : (Hilbert.KTc).HasK where p := 0; q := 1;
 instance : (Hilbert.KTc).HasTc where p := 0
 instance : Entailment.Modal.KTc (Hilbert.KTc) where
 
-
 protected abbrev KD4Point3Z : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.D (.atom 0), Axioms.Four (.atom 0), Axioms.WeakPoint3 (.atom 0) (.atom 1), Axioms.Z (.atom 0)}⟩
 instance : (Hilbert.KD4Point3Z).HasK where p := 0; q := 1;
 instance : (Hilbert.KD4Point3Z).HasD where p := 0

Foundation/Modal/Kripke/AxiomGeach.lean

@@ -222,7 +222,7 @@ instance [Entailment.HasAxiomGeach g 𝓢] : IsGeachean g _ (canonicalFrame 𝓢
     exact hu.2 hφ;
 ⟩
 
-instance [Entailment.HasAxiomFour 𝓢] : IsTrans _ (canonicalFrame 𝓢).Rel := inferInstance
+instance isTrans [Entailment.HasAxiomFour 𝓢] : IsTrans _ (canonicalFrame 𝓢).Rel := inferInstance
 instance [Entailment.HasAxiomT 𝓢] : IsRefl _ (canonicalFrame 𝓢).Rel := inferInstance
 instance [Entailment.HasAxiomFive 𝓢] : IsEuclidean _ (canonicalFrame 𝓢).Rel := inferInstance
 instance [Entailment.HasAxiomD 𝓢] : IsSerial _ (canonicalFrame 𝓢).Rel := inferInstance