Add KB4 ⊂ KTc (#210)

FormalizedFormalLogic · Feb 16, 2025 · 94d1821 · 94d1821
1 parent 25f7d64
commit 94d1821
Showing 1 changed file with 30 additions and 1 deletion.
diff --git a/Foundation/Modal/Logic/Sublogic.lean b/Foundation/Modal/Logic/Sublogic.lean
@@ -788,7 +788,7 @@ instance : ProperSublogic Logic.KTc Logic.Triv := ⟨by
 instance : ProperSublogic Logic.KTc Logic.Ver := ⟨by
   constructor;
   . rw [KTc.eq_CoreflexiveKripkeFrameClass_Logic, Ver.eq_IsolatedFrameClass_Logic];
-    rintro φ hφ F F_corefl;
+    rintro φ hφ F F_iso;
     apply hφ;
     simp_all [Coreflexive, Isolated];
   . suffices ∃ φ, Hilbert.Ver ⊢! φ ∧ ¬CoreflexiveFrameClass ⊧ φ by
@@ -805,4 +805,33 @@ instance : ProperSublogic Logic.KTc Logic.Ver := ⟨by
         use 0;
 ⟩
 
+instance : ProperSublogic Logic.KB4 Logic.KTc := ⟨by
+  constructor;
+  . rw [KB4.eq_ReflexiveTransitiveKripkeFrameClass_Logic, KTc.eq_CoreflexiveKripkeFrameClass_Logic];
+    rintro φ hφ F F_corefl;
+    apply hφ;
+    refine ⟨?_, ?_⟩;
+    . intro x y Rxy;
+      rw [F_corefl Rxy] at *;
+      assumption;
+    . intro x y z Rxy Ryz;
+      rw [F_corefl Rxy, F_corefl Ryz] at *;
+      assumption;
+  . suffices ∃ φ, Hilbert.KTc ⊢! φ ∧ ¬SymmetricTransitiveFrameClass ⊧ φ by
+      simpa [KB4.eq_ReflexiveTransitiveKripkeFrameClass_Logic];
+    use (Axioms.Tc (.atom 0));
+    constructor;
+    . exact axiomTc!;
+    . apply Formula.Kripke.ValidOnFrameClass.not_of_exists_model_world;
+      let M : Model := ⟨⟨Fin 2, λ x y => True⟩, λ w _ => w = 0⟩;
+      use M, 0;
+      constructor;
+      . simp [Symmetric, Transitive, M];
+      . suffices ∃ x, (x : M.World) ≠ 0 by
+          simp [M, Semantics.Realize, Satisfies];
+          tauto;
+        use 1;
+        aesop;
+⟩
+
 end LO.Modal.Logic