add(Modal/Neighborhood): Add EMCT4

Foundation.lean

@@ -144,6 +144,7 @@ import Foundation.Modal.Neighborhood.Logic.E5
 import Foundation.Modal.Neighborhood.Logic.EMC4
 import Foundation.Modal.Neighborhood.Logic.EMCN
 import Foundation.Modal.Neighborhood.Logic.EMCN4
+import Foundation.Modal.Neighborhood.Logic.EMCT4
 import Foundation.Modal.Neighborhood.Logic.EMNT4
 import Foundation.Modal.Neighborhood.Logic.EMT4
 import Foundation.Modal.Neighborhood.Logic.EN4

Foundation/Modal/Hilbert/WithRE/Basic.lean

@@ -222,6 +222,23 @@ instance : EMCN.axioms.HasN where
 protected abbrev EMCN : Logic ℕ := Hilbert.WithRE EMCN.axioms
 instance : Entailment.EMCN Modal.EMCN where
 
+protected abbrev EMCT4.axioms : Axiom ℕ := {
+  Axioms.M (.atom 0) (.atom 1),
+  Axioms.C (.atom 0) (.atom 1),
+  Axioms.T (.atom 0),
+  Axioms.Four (.atom 0)
+}
+namespace EMCT4
+instance : EMCT4.axioms.HasM where p := 0; q := 1
+instance : EMCT4.axioms.HasC where p := 0; q := 1
+instance : EMCT4.axioms.HasT where p := 0;
+instance : EMCT4.axioms.HasFour where p := 0;
+end EMCT4
+protected abbrev EMCT4 : Logic ℕ := Hilbert.WithRE EMCT4.axioms
+instance : Entailment.EMC Modal.EMCT4 where
+instance : Entailment.E4 Modal.EMCT4 where
+instance : Entailment.ET Modal.EMCT4 where
+
 protected abbrev EK.axioms : Axiom ℕ := {Axioms.K (.atom 0) (.atom 1)}
 instance : EK.axioms.HasK where p := 0; q := 1;
 protected abbrev EK : Logic ℕ := Hilbert.WithRE EK.axioms

Foundation/Modal/Neighborhood/Logic/EMC4.lean

@@ -54,4 +54,25 @@ instance : Complete Modal.EMC4 FrameClass.finite_EMC4 := ⟨by
 
 end EMC4
 
+instance : Modal.EMC4 ⪱ Modal.EMCT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.T (.atom 0);
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMC4);
+      apply not_validOnFrameClass_of_exists_frame;
+      use ⟨Fin 1, λ _ => Set.univ⟩;
+      constructor;
+      . exact {
+          mono := by simp,
+          regular := by simp [Frame.box],
+          trans := by simp [Frame.box]
+        }
+      . apply not_imp_not.mpr isReflexive_of_valid_axiomT;
+        by_contra! hC;
+        simpa [Frame.box] using @hC.refl ∅;
+
 end LO.Modal

Foundation/Modal/Neighborhood/Logic/EMCT4.lean

@@ -0,0 +1,56 @@
+import Foundation.Modal.Neighborhood.Hilbert
+import Foundation.Modal.Neighborhood.Logic.EMC4
+import Foundation.Modal.Neighborhood.Logic.EMT4
+
+namespace LO.Modal
+
+open Neighborhood
+open Hilbert.Neighborhood
+open Formula.Neighborhood
+
+namespace Neighborhood
+
+protected class Frame.IsEMCT4 (F : Frame) extends F.IsMonotonic, F.IsRegular, F.IsReflexive, F.IsTransitive where
+protected abbrev FrameClass.EMCT4 : FrameClass := { F | F.IsEMCT4 }
+
+instance : Frame.simple_blackhole.IsEMCT4 where
+
+instance : Frame.simple_whitehole.IsEMCT4 where
+  refl := by simp_all [Frame.simple_whitehole, Frame.box];
+  trans := by simp_all [Frame.simple_whitehole, Frame.box];
+
+end Neighborhood
+
+
+namespace EMCT4
+
+instance : Sound Modal.EMCT4 FrameClass.EMCT4 := instSound_of_validates_axioms $ by
+  constructor;
+  rintro _ (rfl | rfl | rfl | rfl) F ⟨_, _⟩ <;> simp;
+
+instance : Entailment.Consistent Modal.EMCT4 := consistent_of_sound_frameclass FrameClass.EMCT4 $ by
+  use Frame.simple_blackhole;
+  constructor;
+
+instance : Complete Modal.EMCT4 FrameClass.EMCT4 := (supplementedMinimalCanonicity _).completeness $ by
+  apply Set.mem_setOf_eq.mpr;
+  constructor;
+
+end EMCT4
+
+instance : Modal.EMCT4 ⪱ Modal.EMCNT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.N;
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMCT4);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
+      constructor;
+      . tauto;
+      . simp;
+
+end LO.Modal

Foundation/Modal/Neighborhood/Logic/EMN.lean

@@ -40,6 +40,22 @@ instance : Complete Modal.EMN FrameClass.EMN := (supplementedMinimalCanonicity M
 
 end EMN
 
+instance : Modal.EMN ⪱ Modal.EMCN := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use (Axioms.C (.atom 0) (.atom 1));
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMN);
+      apply not_validOnFrameClass_of_exists_frame;
+      use counterframe_axiomC₁;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr;
+        infer_instance;
+      . simp;
+
 instance : Modal.EMN ⪱ Modal.EMCN := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;

Foundation/Modal/Neighborhood/Logic/EMT4.lean

@@ -16,6 +16,56 @@ protected abbrev FrameClass.EMT4 : FrameClass := { F | F.IsEMT4 }
 protected class Frame.IsFiniteEMT4 (F : Frame) extends F.IsEMT4, F.IsFinite
 protected abbrev FrameClass.finite_EMT4 : FrameClass := { F | F.IsFiniteEMT4 }
 
+abbrev counterframe_axiomC₂ : Frame := {
+  World := Fin 2,
+  𝒩 := λ w =>
+    match w with
+    | 0 => {{0}, {1}, {0, 1}}
+    | 1 => {{1}, {0, 1}}
+}
+
+instance : counterframe_axiomC₂.IsEMT4 where
+  mono := by sorry;
+  refl := by sorry;
+  trans := by sorry;
+
+@[simp]
+lemma counterframe_axiomC₂.not_validate_axiomC : ¬counterframe_axiomC₂ ⊧ Axioms.C (.atom 0) (.atom 1) := by
+  apply ValidOnFrame.not_of_exists_valuation_world;
+  use (λ a =>
+    match a with
+    | 0 => {0}
+    | 1 => {1}
+    | _ => ∅
+  ), 0;
+  simp [Satisfies];
+  tauto_set;
+
+/- actual EM4, not EMT4
+instance : counterframe_axiomC₁.IsEMT4 where
+  refl := by sorry;
+  trans := by
+    intro X w;
+    match w with
+    | 0 =>
+      rintro (rfl | rfl | rfl);
+      . left;
+        ext a;
+        match a with | 0 => simp | 1 => simp; tauto_set;
+      . right; right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+      . simp [Frame.box]
+        right; right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+    | 1 =>
+      rintro (rfl | rfl) <;>
+      . right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+-/
+
 end Neighborhood
 
 
@@ -54,4 +104,35 @@ instance : Complete Modal.EMT4 FrameClass.finite_EMT4 := ⟨by
 
 end EMT4
 
+instance : Modal.EMT ⪱ Modal.EMT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use (Axioms.Four (.atom 0));
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMT);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.trivial_nontransitive;
+      constructor;
+      . constructor;
+      . simp;
+
+instance : Modal.EMT4 ⪱ Modal.EMCT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.C (.atom 0) (.atom 1);
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMT4);
+      apply not_validOnFrameClass_of_exists_frame;
+      use counterframe_axiomC₂;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr;
+        infer_instance;
+      . simp;
+
 end LO.Modal

Zoo/modal.typ

@@ -71,6 +71,7 @@
       "LO.Modal.EMC4": $Logic("EMC4")$,
       "LO.Modal.EMCN": $Logic("EMCN")$,
       "LO.Modal.EMCNT": $Logic("EMCNT")$,
+      "LO.Modal.EMCT4": $Logic("EMCT4")$,
       "LO.Modal.EMCNT4": $Logic("EMCNT4")$,
       "LO.Modal.EMCT4": $Logic("EMCT4")$,
       "LO.Modal.EMN": $Logic("EMN")$,