Add Modal Logic KD4.3Z

Foundation.lean

@@ -80,6 +80,7 @@ import Foundation.Modal.Kripke.Hilbert.S4Dot3
 import Foundation.Modal.Kripke.Hilbert.S5
 import Foundation.Modal.Kripke.Hilbert.Triv
 import Foundation.Modal.Kripke.Hilbert.Ver
+import Foundation.Modal.Kripke.Hilbert.KD4Point3Z
 
 import Foundation.Modal.Kripke.Hilbert.GL.Unnecessitation
 import Foundation.Modal.Kripke.Hilbert.GL.MDP

Foundation/Modal/Axioms.lean

@@ -109,6 +109,8 @@ protected abbrev H := □(□φ ⭤ φ) ➝ □φ
 abbrev H.set : Set F := { Axioms.H φ | (φ) }
 notation:max "𝗛" => H.set
 
+protected abbrev Z := □(□φ ➝ φ) ➝ (◇□φ ➝ □φ)
+
 end Basic
 
 protected abbrev Geach (t : Geachean.Taple) (φ : F) := ◇^[t.i](□^[t.m]φ) ➝ □^[t.j](◇^[t.n]φ)

Foundation/Modal/Entailment/Basic.lean

@@ -441,6 +441,23 @@ instance (Γ : Context F 𝓢) : HasAxiomH Γ := ⟨fun _ ↦ Context.of axiomH
 end
 
 
+class HasAxiomZ (𝓢 : S) where
+  Z (φ : F) : 𝓢 ⊢ Axioms.Z φ
+
+section
+
+variable [HasAxiomZ 𝓢]
+
+def axiomZ : 𝓢 ⊢ □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := HasAxiomZ.Z _
+@[simp] lemma axiomZ! : 𝓢 ⊢! □(□φ ➝ φ) ➝ (◇□φ ➝ □φ) := ⟨axiomZ⟩
+
+variable [Entailment.Minimal 𝓢]
+
+instance (Γ : FiniteContext F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ FiniteContext.of axiomZ⟩
+instance (Γ : Context F 𝓢) : HasAxiomZ Γ := ⟨fun _ ↦ Context.of axiomZ⟩
+
+end
+
 section
 
 variable [BasicModalLogicalConnective F] [DecidableEq F]
@@ -513,6 +530,8 @@ protected class K4 extends Entailment.K 𝓢, HasAxiomFour 𝓢
 protected class K4Dot2 extends Entailment.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot2 𝓢
 protected class K4Dot3 extends Entailment.K 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot3 𝓢
 
+protected class KD4Point3Z extends Entailment.K 𝓢, HasAxiomD 𝓢, HasAxiomFour 𝓢, HasAxiomWeakDot3 𝓢, HasAxiomZ 𝓢
+
 protected class K5 extends Entailment.K 𝓢, HasAxiomFive 𝓢
 
 protected class S4 extends Entailment.K 𝓢, HasAxiomT 𝓢, HasAxiomFour 𝓢

Foundation/Modal/Hilbert/WellKnown.lean

@@ -214,6 +214,19 @@ instance [hH : H.HasH] : Entailment.HasAxiomH H where
     . use (λ b => if hH.p = b then φ else (.atom b));
       simp;
 
+class HasZ (H : Hilbert α) where
+  p : α
+  mem_Z : Axioms.Z (.atom p) ∈ H.axioms := by tauto;
+
+instance [hZ : H.HasZ] : Entailment.HasAxiomZ H where
+  Z φ := by
+    apply maxm;
+    use Axioms.Z (.atom hZ.p);
+    constructor;
+    . exact hZ.mem_Z;
+    . use (λ b => if hZ.p = b then φ else (.atom b));
+      simp;
+
 end
 
 protected abbrev KT : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0)}⟩
@@ -265,6 +278,14 @@ instance : (Hilbert.K4Dot3).HasFour where p := 0
 instance : (Hilbert.K4Dot3).HasWeakDot3 where p := 0; q := 1;
 instance : Entailment.K4Dot3 (Hilbert.K4Dot3) where
 
+protected abbrev KD4Point3Z : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.D (.atom 0), Axioms.Four (.atom 0), Axioms.WeakDot3 (.atom 0) (.atom 1), Axioms.Z (.atom 0)}⟩
+instance : (Hilbert.KD4Point3Z).HasK where p := 0; q := 1;
+instance : (Hilbert.KD4Point3Z).HasD where p := 0
+instance : (Hilbert.KD4Point3Z).HasFour where p := 0
+instance : (Hilbert.KD4Point3Z).HasWeakDot3 where p := 0; q := 1;
+instance : (Hilbert.KD4Point3Z).HasZ where p := 0
+instance : Entailment.KD4Point3Z (Hilbert.KD4Point3Z) where
+
 protected abbrev KT4B : Hilbert ℕ := ⟨{Axioms.K (.atom 0) (.atom 1), Axioms.T (.atom 0), Axioms.Four (.atom 0), Axioms.B (.atom 0)}⟩
 instance : (Hilbert.KT4B).HasK where p := 0; q := 1;
 instance : (Hilbert.KT4B).HasT where p := 0

Foundation/Modal/Kripke/AxiomGeach.lean

@@ -51,17 +51,20 @@ section
 
 variable {F : Frame}
 
-lemma reflexive_of_validate_AxiomT (h : F ⊧ (Axioms.T (.atom 0))) : Reflexive F.Rel := by
-  have : ValidOnFrame F (Axioms.T (.atom 0)) → Reflexive F.Rel := by
-    simpa [Axioms.Geach, MultiGeachean, ←Geachean.reflexive_def] using
-    MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 0⟩} |>.defines F |>.mpr;
-  exact this h;
-
-lemma transitive_of_validate_AxiomFour (h : F ⊧ (Axioms.Four (.atom 0))) : Transitive F.Rel := by
-  have : ValidOnFrame F (Axioms.Four (.atom 0)) → Transitive F.Rel := by
-    simpa [Axioms.Geach, MultiGeachean, ←Geachean.transitive_def] using
-    MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 2, 1, 0⟩} |>.defines F |>.mpr;
-  exact this h;
+lemma defines_reflexive : Reflexive F.Rel ↔ F ⊧ (Axioms.T (.atom 0)) := by
+  simpa [MultiGeachean, ←Geachean.reflexive_def, Axioms.Geach] using
+    MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 0⟩} |>.defines F
+alias ⟨validate_axiomT_of_reflexive, reflexive_of_validate_axiomT⟩ := defines_reflexive
+
+lemma deines_transitive : Transitive F.Rel ↔ F ⊧ (Axioms.Four (.atom 0)) := by
+  simpa [MultiGeachean, ←Geachean.transitive_def, Axioms.Geach] using
+    MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 2, 1, 0⟩} |>.defines F
+alias ⟨validate_axiomFour_of_transitive, transitive_of_validate_axiomFour⟩ := deines_transitive
+
+lemma defines_serial : Serial F.Rel ↔ F ⊧ (Axioms.D (.atom 0)) := by
+  simpa [MultiGeachean, ←Geachean.serial_def, Axioms.Geach] using
+    MultiGeacheanFrameClass.isDefinedByGeachAxioms {⟨0, 0, 1, 1⟩} |>.defines F
+alias ⟨validate_axiomD_of_serial, serial_of_validate_axiomD⟩ := defines_serial
 
 end
 

Foundation/Modal/Kripke/AxiomGrz.lean

@@ -96,15 +96,15 @@ lemma validate_T_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : F ⊧ (Axiom
   exact Satisfies.and_def.mp (validate_T_Four_of_validate_Grz h V x hx) |>.1;
 
 lemma reflexive_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : Reflexive F := by
-  apply reflexive_of_validate_AxiomT;
+  apply reflexive_of_validate_axiomT;
   simpa using validate_T_of_validate_Grz h;
 
 lemma validate_Four_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : F ⊧ (Axioms.Four (.atom 0))  := by
   intro V x hx;
   exact Satisfies.and_def.mp (validate_T_Four_of_validate_Grz h V x hx) |>.2;
 
 lemma transitive_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : Transitive F := by
-  apply transitive_of_validate_AxiomFour;
+  apply transitive_of_validate_axiomFour;
   simpa using validate_Four_of_validate_Grz h;
 
 lemma WCWF_of_validate_Grz (h : F ⊧ Axioms.Grz (.atom 0)) : WCWF F := by

Foundation/Modal/Kripke/AxiomWeakDot3.lean

@@ -12,7 +12,7 @@ open Formula.Kripke
 
 variable {F : Kripke.Frame}
 
-lemma weakConnected_of_validate_WeakDot3 (hCon : WeakConnected F) : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) := by
+lemma validate_WeakDot3_of_weakConnected (hCon : WeakConnected F) : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) := by
   rintro V x;
   apply Satisfies.or_def.mpr;
   suffices
@@ -30,7 +30,7 @@ lemma weakConnected_of_validate_WeakDot3 (hCon : WeakConnected F) : F ⊧ (Axiom
   . have := hz _ Ryz; contradiction;
   . have := hy _ Rzy; contradiction;
 
-lemma validate_WeakDot3_of_weakConnected : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) → WeakConnected F := by
+lemma weakConnected_of_validate_WeakDot3 : F ⊧ (Axioms.WeakDot3 (.atom 0) (.atom 1)) → WeakConnected F := by
   contrapose;
   intro hCon;
   obtain ⟨x, y, Rxy, z, Rxz, nyz, nRyz, nRzy⟩ := by simpa [WeakConnected] using hCon;
@@ -64,8 +64,8 @@ instance : WeakConnectedFrameClass.IsNonempty := by
 instance WeakConnectedFrameClass.DefinedByWeakDot3 : WeakConnectedFrameClass.DefinedBy {Axioms.WeakDot3 (.atom 0) (.atom 1)} := ⟨by
   intro F;
   constructor;
-  . simpa using weakConnected_of_validate_WeakDot3;
   . simpa using validate_WeakDot3_of_weakConnected;
+  . simpa using weakConnected_of_validate_WeakDot3;
 ⟩
 
 end definability

Foundation/Modal/Kripke/Hilbert/KD4Point3Z.lean

@@ -0,0 +1,84 @@
+import Foundation.Modal.Kripke.Completeness
+import Foundation.Modal.Hilbert.WellKnown
+import Foundation.Modal.Kripke.AxiomWeakDot3
+import Foundation.Modal.Kripke.AxiomGeach
+import Mathlib.Order.Interval.Finset.Nat
+
+namespace LO.Modal
+
+namespace Kripke
+
+
+section definability
+
+open Formula (atom)
+open Formula.Kripke
+
+variable {F : Kripke.Frame}
+
+def natLtFrame : Kripke.Frame where
+  World := ℕ
+  Rel x y := x < y
+
+namespace natLtFrame
+
+protected lemma serial : Serial natLtFrame.Rel := by
+  rintro x;
+  unfold natLtFrame at *;
+  use x + 1;
+  omega;
+
+protected lemma transitive : Transitive natLtFrame.Rel := by simp [Transitive, natLtFrame]; omega;
+
+protected lemma wellConnected : WeakConnected natLtFrame.Rel := by
+  rintro x y z ⟨Rxy, Rxz, hyz⟩;
+  unfold natLtFrame at x y z;
+  rcases lt_trichotomy y z with (Ryz | rfl | Rzy) <;> tauto;
+
+end natLtFrame
+
+lemma natLtFrame_validates_axiomZ : natLtFrame ⊧ (Axioms.Z (.atom 0)) := by
+  rintro V x;
+  intro h₁ h₂ y Rxy;
+  obtain ⟨z, Rxz, h₃⟩ := Satisfies.dia_def.mp h₂;
+  unfold natLtFrame at x y z;
+  rcases lt_trichotomy y z with (Ryz | rfl | Rzy);
+  . apply h₁ _ Rxy;
+    suffices ∀ i ∈ Finset.Ioo y z, Satisfies ⟨natLtFrame, V⟩ i (.atom 0) by
+      intro u Ryu;
+      simp only [natLtFrame, Frame.Rel'] at u Ryu;
+      rcases (lt_trichotomy u z) with (Ruz | rfl | Rzu);
+      . apply this; simp_all [Finset.mem_Ioo];
+      . exact h₁ _ Rxz $ h₃;
+      . apply h₃ _ Rzu;
+    /-
+      Now consider z - 1.
+      We know z ⊧ 0 and z ⊧ □0, imedeiately proves any u > z, u ⊧ 0, so z - 1 ⊧ □0.
+      By hypothesis, z - 1 ⊧ □0 ➝ 0, so z - 1 ⊧ 0.
+      By similar arguents (by induction), z - 2, z - 3, ... y ⊧ 0.
+    -/
+    sorry;
+  . exact h₁ y Rxy $ h₃;
+  . exact h₃ _ Rzy;
+
+lemma Hilbert.KD4Point3Z.Kripke.sound : Hilbert.KD4Point3Z ⊢! φ → natLtFrame ⊧ φ := by
+  intro hφ;
+  induction hφ using Hilbert.Deduction.rec! with
+  | maxm h =>
+    rcases (by simpa using h) with ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩ | ⟨s, rfl⟩;
+    . tauto;
+    . exact ValidOnFrame.subst $ validate_axiomD_of_serial natLtFrame.serial;
+    . exact ValidOnFrame.subst $ validate_axiomFour_of_transitive natLtFrame.transitive;
+    . exact ValidOnFrame.subst $ validate_WeakDot3_of_weakConnected natLtFrame.wellConnected;
+    . exact ValidOnFrame.subst $ natLtFrame_validates_axiomZ;
+  | mdp ihpq ihp => exact ValidOnFrame.mdp ihpq ihp;
+  | nec ih => exact ValidOnFrame.nec ih;
+  | imply₁ => exact ValidOnFrame.imply₁;
+  | imply₂ => exact ValidOnFrame.imply₂;
+  | ec => exact ValidOnFrame.elimContra;
+
+end definability
+
+end Kripke
+
+end LO.Modal

Foundation/Modal/Logic/WellKnown.lean

@@ -81,6 +81,7 @@ protected abbrev KD4 : Logic := Hilbert.KD4.logic
 lemma KD4.eq_SerialTransitiveKripkeFrameClass_Logic : Logic.KD4 = Kripke.SerialTransitiveFrameClass.logic
   := eq_Hilbert_Logic_KripkeFrameClass_Logic
 
+protected abbrev KD4Point3Z : Logic := Hilbert.KD4Point3Z.logic
 
 protected abbrev KD45 : Logic := Hilbert.KD45.logic
 lemma KD45.eq_SerialTransitiveEuclideanKripkeFrameClass_Logic : Logic.KD45 = Kripke.SerialTransitiveEuclideanFrameClass.logic