feat(Modal): Full Strength Analysis of Modal Cube Part.1 (#171)

* refactor geach

* KT_KTB

* K4, K5, KDB, KTB

* K45_KB4

* KB5_S5

* KTB_S5

* KT_S4

* KB_KDB, KD_KDB

* K4_KD4, K5_KD5

* KD4_KD45, KD5_KD45

* KD45_S5

Foundation.lean

@@ -71,11 +71,25 @@ import Foundation.Modal.Hilbert.WeakerThan.K_KB
 import Foundation.Modal.Hilbert.WeakerThan.K_KD
 import Foundation.Modal.Hilbert.WeakerThan.K4_GL
 import Foundation.Modal.Hilbert.WeakerThan.K4_Grz
+import Foundation.Modal.Hilbert.WeakerThan.K4_K45
+import Foundation.Modal.Hilbert.WeakerThan.K4_KD4
 import Foundation.Modal.Hilbert.WeakerThan.K4_S4
 import Foundation.Modal.Hilbert.WeakerThan.K4_Triv
+import Foundation.Modal.Hilbert.WeakerThan.K45_KB4
+import Foundation.Modal.Hilbert.WeakerThan.K5_K45
+import Foundation.Modal.Hilbert.WeakerThan.K5_KD5
+import Foundation.Modal.Hilbert.WeakerThan.KB_KDB
+import Foundation.Modal.Hilbert.WeakerThan.KB5_S5
+import Foundation.Modal.Hilbert.WeakerThan.KD_KDB
 import Foundation.Modal.Hilbert.WeakerThan.KD_KT
+import Foundation.Modal.Hilbert.WeakerThan.KD4_KD45
+import Foundation.Modal.Hilbert.WeakerThan.KD45_S5
+import Foundation.Modal.Hilbert.WeakerThan.KD5_KD45
+import Foundation.Modal.Hilbert.WeakerThan.KDB_KTB
 import Foundation.Modal.Hilbert.WeakerThan.KT_Grz
+import Foundation.Modal.Hilbert.WeakerThan.KT_KTB
 import Foundation.Modal.Hilbert.WeakerThan.KT_S4
+import Foundation.Modal.Hilbert.WeakerThan.KTB_S5
 import Foundation.Modal.Hilbert.WeakerThan.S4_S5
 
 import Foundation.Modal.Hilbert.Equiv.GL

Foundation/Modal/Axioms.lean

@@ -106,23 +106,23 @@ notation:max "𝗴𝗲(" t ")" => Geach.set t
 
 section
 
-lemma T.is_geach : (𝗧 : Set F) = 𝗴𝗲(⟨0, 0, 1, 0⟩) := rfl
+@[simp] lemma T.is_geach : (𝗧 : Set F) = 𝗴𝗲(⟨0, 0, 1, 0⟩) := rfl
 
-lemma B.is_geach : (𝗕 : Set F) = 𝗴𝗲(⟨0, 1, 0, 1⟩) := rfl
+@[simp] lemma B.is_geach : (𝗕 : Set F) = 𝗴𝗲(⟨0, 1, 0, 1⟩) := rfl
 
-lemma D.is_geach : (𝗗 : Set F) = 𝗴𝗲(⟨0, 0, 1, 1⟩) := rfl
+@[simp] lemma D.is_geach : (𝗗 : Set F) = 𝗴𝗲(⟨0, 0, 1, 1⟩) := rfl
 
-lemma Four.is_geach : (𝟰 : Set F) = 𝗴𝗲(⟨0, 2, 1, 0⟩) := rfl
+@[simp] lemma Four.is_geach : (𝟰 : Set F) = 𝗴𝗲(⟨0, 2, 1, 0⟩) := rfl
 
-lemma Five.is_geach : (𝟱 : Set F) = 𝗴𝗲(⟨1, 1, 0, 1⟩) := rfl
+@[simp] lemma Five.is_geach : (𝟱 : Set F) = 𝗴𝗲(⟨1, 1, 0, 1⟩) := rfl
 
-lemma Dot2.is_geach : (.𝟮 : Set F) = 𝗴𝗲(⟨1, 1, 1, 1⟩) := rfl
+@[simp] lemma Dot2.is_geach : (.𝟮 : Set F) = 𝗴𝗲(⟨1, 1, 1, 1⟩) := rfl
 
-lemma C4.is_geach : (𝗖𝟰 : Set F) = 𝗴𝗲(⟨0, 1, 2, 0⟩) := rfl
+@[simp] lemma C4.is_geach : (𝗖𝟰 : Set F) = 𝗴𝗲(⟨0, 1, 2, 0⟩) := rfl
 
-lemma CD.is_geach : (𝗖𝗗 : Set F) = 𝗴𝗲(⟨1, 1, 0, 0⟩) := rfl
+@[simp] lemma CD.is_geach : (𝗖𝗗 : Set F) = 𝗴𝗲(⟨1, 1, 0, 0⟩) := rfl
 
-lemma Tc.is_geach : (𝗧𝗰 : Set F) = 𝗴𝗲(⟨0, 1, 0, 0⟩) := rfl
+@[simp] lemma Tc.is_geach : (𝗧𝗰 : Set F) = 𝗴𝗲(⟨0, 1, 0, 0⟩) := rfl
 
 end
 
@@ -148,9 +148,8 @@ lemma mem (h : x ∈ l) : (𝗴𝗲(x) : Set F) ⊆ 𝗚𝗲(l) := by
   induction l with
   | nil => contradiction;
   | cons a as ih =>
-    simp_all;
     cases h;
-    . subst_vars; tauto;
+    . tauto;
     . apply Set.subset_union_of_subset_right $ ih (by assumption);
 
 end MultiGeach

Foundation/Modal/Hilbert/Equiv/S5_KT4B.lean

@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal.Hilbert
 

Foundation/Modal/Hilbert/Geach.lean

@@ -19,33 +19,46 @@ lemma ax {H : Hilbert α} (geach : H.IsGeach ts) : H.axioms = (𝗞 ∪ 𝗚𝗲
 end Hilbert.IsGeach
 
 
-instance Hilbert.K.is_geach : (Hilbert.K α).IsGeach [] := by simp;
+namespace Hilbert
 
-instance Hilbert.KD.is_geach : (Hilbert.KD α).IsGeach [⟨0, 0, 1, 1⟩] := by
-  simp [Axioms.D.is_geach];
+instance K.is_geach : (Hilbert.K α).IsGeach [] := by simp;
 
-instance Hilbert.KT.is_geach : (Hilbert.KT α).IsGeach [⟨0, 0, 1, 0⟩] := by
-  simp [Axioms.T.is_geach];
+instance K4.is_geach : (Hilbert.K4 α).IsGeach [⟨0, 2, 1, 0⟩] := by simp;
 
-instance Hilbert.KTB.is_geach : (Hilbert.KTB α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 1⟩] := by
-  simp [Axioms.T.is_geach, Axioms.B.is_geach];
+instance K45.is_geach : (Hilbert.K45 α).IsGeach [⟨0, 2, 1, 0⟩, ⟨1, 1, 0, 1⟩] := by simp;
 
-instance Hilbert.K4.is_geach : (Hilbert.K4 α).IsGeach [⟨0, 2, 1, 0⟩] := by
-  simp [Axioms.Four.is_geach];
+instance K5.is_geach : (Hilbert.K5 α).IsGeach [⟨1, 1, 0, 1⟩] := by simp;
 
-instance Hilbert.S4.is_geach : (Hilbert.S4 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩] := by
-  simp [Axioms.T.is_geach, Axioms.Four.is_geach];
+instance KB4.is_geach : (Hilbert.KB4 α).IsGeach [⟨0, 1, 0, 1⟩, ⟨0, 2, 1, 0⟩] := by simp;
 
-instance Hilbert.S4Dot2.is_geach : (Hilbert.S4Dot2 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 1, 1⟩] := by
-  simp [Axioms.T.is_geach, Axioms.Four.is_geach, Axioms.Dot2.is_geach, Set.union_assoc];
+instance KB5.is_geach : (Hilbert.KB5 α).IsGeach [⟨0, 1, 0, 1⟩, ⟨1, 1, 0, 1⟩] := by simp;
 
-instance Hilbert.S5.is_geach : (Hilbert.S5 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨1, 1, 0, 1⟩] := by
-  simp [Axioms.T.is_geach, Axioms.Five.is_geach];
+instance KD.is_geach : (Hilbert.KD α).IsGeach [⟨0, 0, 1, 1⟩] := by simp;
 
-instance Hilbert.KT4B.is_geach : (Hilbert.KT4B α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨0, 1, 0, 1⟩] := by
-  simp [Axioms.T.is_geach, Axioms.Four.is_geach, Axioms.B.is_geach, Set.union_assoc];
+instance KB.is_geach : (Hilbert.KB α).IsGeach [⟨0, 1, 0, 1⟩] := by simp;
 
-instance Hilbert.Triv.is_geach : (Hilbert.Triv α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 0⟩] := by
-  simp [Axioms.T.is_geach, Axioms.Tc.is_geach];
+instance KD4.is_geach : (Hilbert.KD4 α).IsGeach [⟨0, 0, 1, 1⟩, ⟨0, 2, 1, 0⟩] := by simp;
+
+instance KD45.is_geach : (Hilbert.KD45 α).IsGeach [⟨0, 0, 1, 1⟩,  ⟨0, 2, 1, 0⟩, ⟨1, 1, 0, 1⟩] := by simp [Set.union_assoc];
+
+instance KD5.is_geach : (Hilbert.KD5 α).IsGeach [⟨0, 0, 1, 1⟩, ⟨1, 1, 0, 1⟩] := by simp;
+
+instance KDB.is_geach : (Hilbert.KDB α).IsGeach [⟨0, 0, 1, 1⟩, ⟨0, 1, 0, 1⟩] := by simp;
+
+instance KT.is_geach : (Hilbert.KT α).IsGeach [⟨0, 0, 1, 0⟩] := by simp;
+
+instance KT4B.is_geach : (Hilbert.KT4B α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨0, 1, 0, 1⟩] := by simp [Set.union_assoc];
+
+instance KTB.is_geach : (Hilbert.KTB α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 1⟩] := by simp;
+
+instance S4.is_geach : (Hilbert.S4 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩] := by simp;
+
+instance S4Dot2.is_geach : (Hilbert.S4Dot2 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 1, 1⟩] := by simp [Set.union_assoc];
+
+instance S5.is_geach : (Hilbert.S5 α).IsGeach [⟨0, 0, 1, 0⟩, ⟨1, 1, 0, 1⟩] := by simp;
+
+instance Triv.is_geach : (Hilbert.Triv α).IsGeach [⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 0⟩] := by simp;
+
+end Hilbert
 
 end LO.Modal

Foundation/Modal/Hilbert/Systems.lean

@@ -3,7 +3,9 @@ import Foundation.Modal.System.Basic
 
 namespace LO.Modal.Hilbert
 
-protected abbrev K (α) : Hilbert α := ⟨𝗞, ⟮Nec⟯⟩
+variable (α)
+
+protected abbrev K : Hilbert α := ⟨𝗞, ⟮Nec⟯⟩
 instance : (Hilbert.K α).IsNormal where
 
 
@@ -30,87 +32,101 @@ lemma weakerThan : (Hilbert.K α) ≤ₛ (Hilbert.ExtK Ax) := normal_weakerThan_
 end ExtK
 
 
-protected abbrev KT (α) : Hilbert α := Hilbert.ExtK $ 𝗧
+protected abbrev KT : Hilbert α := Hilbert.ExtK $ 𝗧
 instance : System.KT (Hilbert.KT α) where
   T _ := Deduction.maxm $ by aesop;
 
-protected abbrev KB (α) : Hilbert α := Hilbert.ExtK $ 𝗕
+protected abbrev KB : Hilbert α := Hilbert.ExtK $ 𝗕
 instance : System.KB (Hilbert.KB α) where
   B _ := Deduction.maxm $ by aesop;
 
-protected abbrev KD (α) : Hilbert α := Hilbert.ExtK $ 𝗗
+protected abbrev KD : Hilbert α := Hilbert.ExtK $ 𝗗
 instance : System.KD (Hilbert.KD α) where
   D _ := Deduction.maxm $ by aesop;
 
-protected abbrev KP (α) : Hilbert α := Hilbert.ExtK $ 𝗣
+protected abbrev KP : Hilbert α := Hilbert.ExtK $ 𝗣
 instance : System.KP (Hilbert.KP α) where
   P := Deduction.maxm $ by aesop;
 
-protected abbrev KTB (α) : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗕
+protected abbrev KTB : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗕
 
-protected abbrev K4 (α) : Hilbert α := Hilbert.ExtK $ 𝟰
+protected abbrev K4 : Hilbert α := Hilbert.ExtK $ 𝟰
 instance : System.K4 (Hilbert.K4 α) where
   Four _ := Deduction.maxm $ by aesop;
 
-protected abbrev K5 (α) : Hilbert α := Hilbert.ExtK $ 𝟱
+protected abbrev K5 : Hilbert α := Hilbert.ExtK $ 𝟱
 instance : System.K5 (Hilbert.K5 α) where
   Five _ := Deduction.maxm $ by aesop;
 
+protected abbrev KD45 : Hilbert α := Hilbert.ExtK $ 𝗗 ∪ 𝟰 ∪ 𝟱
+
+protected abbrev K45 : Hilbert α := Hilbert.ExtK $ 𝟰 ∪ 𝟱
+
+protected abbrev KB4 : Hilbert α := Hilbert.ExtK $ 𝗕 ∪ 𝟰
+
+protected abbrev KB5 : Hilbert α := Hilbert.ExtK $ 𝗕 ∪ 𝟱
+
+protected abbrev KDB : Hilbert α := Hilbert.ExtK $ 𝗗 ∪ 𝗕
+
+protected abbrev KD4 : Hilbert α := Hilbert.ExtK $ 𝗗 ∪ 𝟰
+
+protected abbrev KD5 : Hilbert α := Hilbert.ExtK $ 𝗗 ∪ 𝟱
+
 
 protected abbrev ExtS4 {α} (Ax : Theory α) : Hilbert α := Hilbert.ExtK (𝗧 ∪ 𝟰 ∪ Ax)
 
 namespace ExtS4
 
 instance : System.S4 (Hilbert.ExtS4 Ax) where
-  T _ := Deduction.maxm $ by aesop;
-  Four _ := Deduction.maxm $ by aesop;
+  T _ := Deduction.maxm $ by simp
+  Four _ := Deduction.maxm $ by simp;
 
 @[simp] lemma def_ax : (Hilbert.ExtS4 Ax).axioms = (𝗞 ∪ 𝗧 ∪ 𝟰 ∪ Ax) := by aesop;
 
 end ExtS4
 
-protected abbrev S4 (α) : Hilbert α := Hilbert.ExtS4 $ ∅
+protected abbrev S4 : Hilbert α := Hilbert.ExtS4 $ ∅
 
-protected abbrev S4Dot2 (α) : Hilbert α := Hilbert.ExtS4 $ .𝟮
+protected abbrev S4Dot2 : Hilbert α := Hilbert.ExtS4 $ .𝟮
 instance : System.S4Dot2 (Hilbert.S4Dot2 α) where
   Dot2 _ := Deduction.maxm $ by aesop
 
-protected abbrev S4Dot3 (α) : Hilbert α := Hilbert.ExtS4 $ .𝟯
+protected abbrev S4Dot3 : Hilbert α := Hilbert.ExtS4 $ .𝟯
 instance : System.S4Dot3 (Hilbert.S4Dot3 α) where
   Dot3 _ _:= Deduction.maxm $ by aesop;
 
-protected abbrev S4Grz (α) : Hilbert α := Hilbert.ExtS4 $ 𝗚𝗿𝘇
+protected abbrev S4Grz : Hilbert α := Hilbert.ExtS4 $ 𝗚𝗿𝘇
 
-protected abbrev KT4B (α) : Hilbert α := Hilbert.ExtS4 $ 𝗕
+protected abbrev KT4B : Hilbert α := Hilbert.ExtS4 $ 𝗕
 
 
-protected abbrev S5 (α) : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝟱
+protected abbrev S5 : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝟱
 instance : System.S5 (Hilbert.S5 α) where
   T _ := Deduction.maxm $ by aesop;
   Five _ := Deduction.maxm $ by aesop;
 
-protected abbrev Triv (α) : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗧𝗰
+protected abbrev Triv : Hilbert α := Hilbert.ExtK $ 𝗧 ∪ 𝗧𝗰
 instance : System.Triv (Hilbert.Triv α) where
   T _ := Deduction.maxm $ by aesop;
   Tc _ := Deduction.maxm $ by aesop;
 
-protected abbrev Ver (α) : Hilbert α := Hilbert.ExtK $ 𝗩𝗲𝗿
+protected abbrev Ver : Hilbert α := Hilbert.ExtK $ 𝗩𝗲𝗿
 instance : System.Ver (Hilbert.Ver α) where
   Ver _ := Deduction.maxm $ by aesop;
 
-protected abbrev GL (α) : Hilbert α := Hilbert.ExtK $ 𝗟
+protected abbrev GL : Hilbert α := Hilbert.ExtK $ 𝗟
 instance : System.GL (Hilbert.GL α) where
   L _ := Deduction.maxm $ by aesop;
 
-protected abbrev Grz (α) : Hilbert α := Hilbert.ExtK $ 𝗚𝗿𝘇
+protected abbrev Grz : Hilbert α := Hilbert.ExtK $ 𝗚𝗿𝘇
 instance : System.Grz (Hilbert.Grz α) where
   Grz _ := Deduction.maxm $ by aesop;
 
 /--
   Solovey's Provability Logic of True Arithmetic.
   Remark necessitation is *not* permitted.
 -/
-protected abbrev GLS (α) : Hilbert α := ⟨(Hilbert.GL α).theorems ∪ 𝗧, ∅⟩
+protected abbrev GLS : Hilbert α := ⟨(Hilbert.GL α).theorems ∪ 𝗧, ∅⟩
 instance : System.HasAxiomK (Hilbert.GLS α) where
   K _ _ := Deduction.maxm $ Set.mem_of_subset_of_mem (by rfl) $ by simp [Hilbert.theorems, System.theory, System.axiomK!];
 instance : System.HasAxiomL (Hilbert.GLS α) where
@@ -119,7 +135,7 @@ instance : System.HasAxiomT (Hilbert.GLS α) where
   T _ := Deduction.maxm $ by aesop;
 
 /-- Logic of Pure Necessitation -/
-protected abbrev N (α) : Hilbert α := ⟨∅, ⟮Nec⟯⟩
+protected abbrev N : Hilbert α := ⟨∅, ⟮Nec⟯⟩
 instance : (Hilbert.N α).HasNecOnly where
 
 

Foundation/Modal/Hilbert/WeakerThan/K45_KB4.lean

@@ -0,0 +1,34 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma K45_weakerThan_KB4 : (Hilbert.K45 ℕ) ≤ₛ (Hilbert.KB4 ℕ) := by
+  apply Kripke.weakerThan_of_subset_FrameClass TransitiveEuclideanFrameClass SymmetricTransitiveFrameClass;
+  rintro F ⟨h_symm, h_trans⟩;
+  refine ⟨h_trans, (eucl_of_symm_trans h_symm h_trans)⟩;
+
+theorem K45_strictlyWeakerThan_KB4 : (Hilbert.K45 ℕ) <ₛ (Hilbert.KB4 ℕ) := by
+  constructor;
+  . exact K45_weakerThan_KB4;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use ((atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply K45.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame,  Transitive F.Rel ∧ Euclidean F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      use ⟨Fin 2, λ x y => y = 1⟩;
+      refine ⟨?_, ?_, ?_⟩;
+      . simp [Transitive];
+      . simp [Euclidean];
+      . use (λ w _ => w = 0), 0;
+        simp [Satisfies, Semantics.Realize];
+
+end LO.Modal.Hilbert

Foundation/Modal/Hilbert/WeakerThan/K4_K45.lean

@@ -0,0 +1,36 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma K4_weakerThan_K45 : (Hilbert.K4 α) ≤ₛ (Hilbert.K45 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem K4_strictlyWeakerThan_K45 : (Hilbert.K4 ℕ) <ₛ (Hilbert.K45 ℕ) := by
+  constructor;
+  . exact K4_weakerThan_K45;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (◇(atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply K4.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Transitive F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      let F : Frame := ⟨Fin 2, λ x y => x < y⟩;
+      use F;
+      constructor;
+      . simp [Transitive];
+        omega;
+      . use (λ w _ => w = 1), 0;
+        suffices (0 : F.World) ≺ 1 ∧ ∃ x : F.World, (0 : F.World) ≺ x ∧ ¬x ≺ 1 by
+          simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . omega;
+        . use 1; omega;
+
+end LO.Modal.Hilbert

Foundation/Modal/Hilbert/WeakerThan/K4_KD4.lean

@@ -0,0 +1,31 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma K4_weakerThan_KD4 : (Hilbert.K4 α) ≤ₛ (Hilbert.KD4 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem K4_strictlyWeakerThan_KD4 : (Hilbert.K4 ℕ) <ₛ (Hilbert.KD4 ℕ) := by
+  constructor;
+  . exact K4_weakerThan_KD4;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ ◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply K4.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Transitive F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      let F : Frame := ⟨Fin 1, λ x y => False⟩;
+      use F;
+      constructor;
+      . simp [Transitive];
+      . use (λ w _ => w = 0), 0;
+        simp [Semantics.Realize, Satisfies];
+
+end LO.Modal.Hilbert