From 64b11ff2d45f91585e57bc41f90fd212b8683d91 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Mon, 17 Feb 2025 04:48:46 +0900 Subject: [PATCH] =?UTF-8?q?Add=20KB4=20=E2=8A=82=20KTc?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Foundation/Modal/Logic/Sublogic.lean | 31 +++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/Foundation/Modal/Logic/Sublogic.lean b/Foundation/Modal/Logic/Sublogic.lean index 332c71ad..9886378d 100644 --- 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