diff --git a/Foundation.lean b/Foundation.lean
index a16e6823..44c69ea1 100644
--- a/Foundation.lean
+++ b/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
diff --git a/Foundation/Modal/Axioms.lean b/Foundation/Modal/Axioms.lean
index df55a987..3efe02aa 100644
--- a/Foundation/Modal/Axioms.lean
+++ b/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
diff --git a/Foundation/Modal/Hilbert/Equiv/S5_KT4B.lean b/Foundation/Modal/Hilbert/Equiv/S5_KT4B.lean
index ba73d86c..82c05b4a 100644
--- a/Foundation/Modal/Hilbert/Equiv/S5_KT4B.lean
+++ b/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
 
diff --git a/Foundation/Modal/Hilbert/Geach.lean b/Foundation/Modal/Hilbert/Geach.lean
index c99bc2f1..966869a5 100644
--- a/Foundation/Modal/Hilbert/Geach.lean
+++ b/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
diff --git a/Foundation/Modal/Hilbert/Systems.lean b/Foundation/Modal/Hilbert/Systems.lean
index bcaf5eef..4a6540ef 100644
--- a/Foundation/Modal/Hilbert/Systems.lean
+++ b/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,79 +32,93 @@ 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;
 
@@ -110,7 +126,7 @@ instance : System.Grz (Hilbert.Grz α) where
   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
 
 
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K45_KB4.lean b/Foundation/Modal/Hilbert/WeakerThan/K45_KB4.lean
new file mode 100644
index 00000000..a65cdbf1
--- /dev/null
+++ b/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
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K4_K45.lean b/Foundation/Modal/Hilbert/WeakerThan/K4_K45.lean
new file mode 100644
index 00000000..2d87caaf
--- /dev/null
+++ b/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
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K4_KD4.lean b/Foundation/Modal/Hilbert/WeakerThan/K4_KD4.lean
new file mode 100644
index 00000000..b8b551a8
--- /dev/null
+++ b/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
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K4_S4.lean b/Foundation/Modal/Hilbert/WeakerThan/K4_S4.lean
index 7412739c..f0a382ba 100644
--- a/Foundation/Modal/Hilbert/WeakerThan/K4_S4.lean
+++ b/Foundation/Modal/Hilbert/WeakerThan/K4_S4.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal.Hilbert
 
@@ -16,12 +16,14 @@ theorem K4_strictlyWeakerThan_S4 : (Hilbert.K4 ℕ) <ₛ (Hilbert.S4 ℕ) := by
     push_neg;
     use (□(atom 0) ➝ (atom 0));
     constructor;
-    . exact Deduction.maxm! (by simp)
+    . exact Deduction.maxm! $ by simp;
     . apply K4.Kripke.sound.not_provable_of_countermodel;
-      simp [ValidOnModel, ValidOnFrame, Satisfies];
+      suffices ∃ F : Frame, Transitive F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
       use ⟨Fin 3, λ _ y => y = 1⟩;
       constructor;
-      . intro _ _ _; simp_all;
+      . simp [Transitive];
       . use (λ w _ => w = 1), 0;
         simp [Semantics.Realize, Satisfies];
 
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K5_K45.lean b/Foundation/Modal/Hilbert/WeakerThan/K5_K45.lean
new file mode 100644
index 00000000..e65a8843
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/K5_K45.lean
@@ -0,0 +1,54 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma K5_weakerThan_K45 : (Hilbert.K5 α) ≤ₛ (Hilbert.K45 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem K5_strictlyWeakerThan_K45 : (Hilbert.K5 ℕ) <ₛ (Hilbert.K45 ℕ) := by
+  constructor;
+  . exact K5_weakerThan_K45;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ □□(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply K5.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Euclidean F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      let F : Frame := ⟨
+          Fin 3,
+          λ x y =>
+            match x, y with
+            | 0, 1 => True
+            | 1, 1 => True
+            | 1, 2 => True
+            | 2, 1 => True
+            | 2, 2 => True
+            | _, _ => False
+        ⟩;
+      use F;
+      constructor;
+      . unfold Euclidean; aesop;
+      . use (λ w _ => w = 1), 0;
+        suffices (∀ (y : F.World), (0 : F.World) ≺ y → y = 1) ∧ ∃ x, (0 : F.World) ≺ x ∧ ∃ z, x ≺ z ∧ ¬z = 1 by simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . intro y R0y;
+          match y with
+          | 0 => simpa;
+          | 1 => tauto;
+          | 2 => simpa;
+        . use 1;
+          constructor;
+          . tauto;
+          . use 2;
+            constructor;
+            . tauto;
+            . trivial;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/K5_KD5.lean b/Foundation/Modal/Hilbert/WeakerThan/K5_KD5.lean
new file mode 100644
index 00000000..880b68d0
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/K5_KD5.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 K5_weakerThan_KD5 : (Hilbert.K5 α) ≤ₛ (Hilbert.KD5 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem K5_strictlyWeakerThan_KD5 : (Hilbert.K5 ℕ) <ₛ (Hilbert.KD5 ℕ) := by
+  constructor;
+  . exact K5_weakerThan_KD5;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ ◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply K5.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Euclidean 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 [Euclidean];
+      . use (λ w _ => w = 0), 0;
+        simp [Semantics.Realize, Satisfies];
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KB5_S5.lean b/Foundation/Modal/Hilbert/WeakerThan/KB5_S5.lean
new file mode 100644
index 00000000..4197d887
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KB5_S5.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 KB5_weakerThan_S5 : (Hilbert.KB5 ℕ) ≤ₛ (Hilbert.S5 ℕ) := by
+  apply Kripke.weakerThan_of_subset_FrameClass SymmetricEuclideanFrameClass ReflexiveEuclideanFrameClass;
+  rintro F ⟨h_refl, h_eucl⟩;
+  refine ⟨symm_of_refl_eucl h_refl h_eucl, h_eucl⟩;
+
+theorem KB5_strictlyWeakerThan_S5 : (Hilbert.KB5 ℕ) <ₛ (Hilbert.S5 ℕ) := by
+  constructor;
+  . exact KB5_weakerThan_S5;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ (atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply KB5.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame,  Symmetric F.Rel ∧ Euclidean F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      use ⟨Fin 1, λ x y => False⟩;
+      refine ⟨?_, ?_, ?_⟩;
+      . simp [Symmetric];
+      . simp [Euclidean];
+      . use (λ w _ => False), 0;
+        simp [Satisfies, Semantics.Realize];
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KB_KDB.lean b/Foundation/Modal/Hilbert/WeakerThan/KB_KDB.lean
new file mode 100644
index 00000000..ae5b915e
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KB_KDB.lean
@@ -0,0 +1,30 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma KB_weakerThan_KDB : (Hilbert.KB α) ≤ₛ (Hilbert.KDB α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem KB_strictlyWeakerThan_KDB : (Hilbert.KB ℕ) <ₛ (Hilbert.KDB ℕ) := by
+  constructor;
+  . exact KB_weakerThan_KDB;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ ◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KB.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Symmetric F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _)  by
+        simpa [ValidOnModel, ValidOnFrame, Satisfies];
+      let F : Frame := ⟨Fin 1, λ x y => False⟩;
+      use F;
+      constructor;
+      . simp [Symmetric];
+      . use (λ w _ => w = 0), 0;
+        simp [Semantics.Realize, Satisfies];
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KD45_S5.lean b/Foundation/Modal/Hilbert/WeakerThan/KD45_S5.lean
new file mode 100644
index 00000000..4a8a4e15
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KD45_S5.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 KD45_weakerThan_S5 : (Hilbert.KD45 ℕ) ≤ₛ (Hilbert.S5 ℕ) :=  by
+  apply Kripke.weakerThan_of_subset_FrameClass SerialTransitiveEuclideanFrameClass ReflexiveEuclideanFrameClass;
+  rintro F ⟨F_refl, F_eucl⟩;
+  refine ⟨serial_of_refl F_refl, trans_of_refl_eucl F_refl F_eucl, F_eucl⟩;
+
+theorem KD45_strictlyWeakerThan_S5 : (Hilbert.KD45 ℕ) <ₛ (Hilbert.S5 ℕ) := by
+  constructor;
+  . exact KD45_weakerThan_S5;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ (atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply KD45.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Serial F.Rel ∧ Transitive F.Rel ∧ Euclidean 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 => y = 1⟩;
+      use F;
+      refine ⟨?_, ?_, ?_, ?_⟩;
+      . simp [Serial];
+      . simp [Transitive];
+      . simp [Euclidean];
+      . use (λ w _ => w = 1), 0;
+        simp [Semantics.Realize, Satisfies];
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KD4_KD45.lean b/Foundation/Modal/Hilbert/WeakerThan/KD4_KD45.lean
new file mode 100644
index 00000000..b67c9ce2
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KD4_KD45.lean
@@ -0,0 +1,37 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma KD4_weakerThan_KD45 : (Hilbert.KD4 α) ≤ₛ (Hilbert.KD45 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem KD4_strictlyWeakerThan_KD45 : (Hilbert.KD4 ℕ) <ₛ (Hilbert.KD45 ℕ) := by
+  constructor;
+  . exact KD4_weakerThan_KD45;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (◇(atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply KD4.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Serial F.Rel ∧ 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 ∨ x < y⟩;
+      use F;
+      refine ⟨?_, ?_, ?_⟩;
+      . simp [Serial];
+      . simp [Transitive];
+        omega;
+      . use (λ w _ => w = 0), 0;
+        suffices (0 : F.World) ≺ 0 ∧ ∃ x : F.World, (0 : F.World) ≺ x ∧ ¬x ≺ 0 by
+          simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . tauto;
+        . use 1; omega;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KD5_KD45.lean b/Foundation/Modal/Hilbert/WeakerThan/KD5_KD45.lean
new file mode 100644
index 00000000..783d217e
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KD5_KD45.lean
@@ -0,0 +1,60 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma KD5_weakerThan_KD45 : (Hilbert.KD5 α) ≤ₛ (Hilbert.KD45 α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem KD5_strictlyWeakerThan_KD45 : (Hilbert.KD5 ℕ) <ₛ (Hilbert.KD45 ℕ) := by
+  constructor;
+  . exact KD5_weakerThan_KD45;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ □□(atom 0));
+    constructor;
+    . exact Deduction.maxm! $ by simp;
+    . apply KD5.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Serial F.Rel ∧ Euclidean F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Kripke.Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      let F : Frame := ⟨
+        Fin 3,
+        λ x y =>
+          match x, y with
+          | 0, 1 => True
+          | 1, 2 => True
+          | 1, 1 => True
+          | 2, 1 => True
+          | 2, 2 => True
+          | _, _ => False
+      ⟩;
+      use F;
+      refine ⟨?_, ?_, ?_⟩;
+      . intro x;
+        match x with
+        | 0 => use 1; tauto;
+        | 1 => use 2; tauto;
+        | 2 => use 1; tauto;
+      . unfold Euclidean; aesop;
+      . use (λ w _ => w = 1), 0;
+        suffices (∀ (y : F.World), (0 : F.World) ≺ y → y = 1) ∧ ∃ x, (0 : F.World) ≺ x ∧ ∃ y, x ≺ y ∧ y ≠ 1 by
+          simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . intro y;
+          match y with
+          | 0 => tauto;
+          | 1 => tauto;
+          | 2 => tauto;
+        . use 1;
+          constructor;
+          . tauto;
+          . use 2;
+            constructor;
+            . tauto;
+            . simp;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KDB_KTB.lean b/Foundation/Modal/Hilbert/WeakerThan/KDB_KTB.lean
new file mode 100644
index 00000000..9b0e6a1e
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KDB_KTB.lean
@@ -0,0 +1,39 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma KDB_weakerThan_KTB : (Hilbert.KDB ℕ) ≤ₛ (Hilbert.KTB ℕ) := by
+  apply Kripke.weakerThan_of_subset_FrameClass SerialSymmetricFrameClass ReflexiveSymmetricFrameClass;
+  rintro F ⟨F_refl, F_symm⟩;
+  refine ⟨serial_of_refl F_refl, F_symm⟩;
+
+theorem KDB_strictlyWeakerThan_KTB : (Hilbert.KDB ℕ) <ₛ (Hilbert.KTB ℕ) := by
+  constructor;
+  . exact KDB_weakerThan_KTB;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ (atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KDB.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Serial F.Rel ∧ Symmetric F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _)  by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      use ⟨Fin 2, λ x y => x ≠ y⟩;
+      refine ⟨?_, ?_, ?_⟩;
+      . intro x;
+        match x with
+        | 0 => use 1; simp;
+        | 1 => use 0; simp;
+      . unfold Symmetric;
+        tauto;
+      . use (λ x _ => x = 1), 0;
+        simp [Semantics.Realize, Satisfies];
+        omega;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KD_KDB.lean b/Foundation/Modal/Hilbert/WeakerThan/KD_KDB.lean
new file mode 100644
index 00000000..517d2bdd
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KD_KDB.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 KD_weakerThan_KDB : (Hilbert.KD α) ≤ₛ (Hilbert.KDB α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem KD_strictlyWeakerThan_KDB : (Hilbert.KD ℕ) <ₛ (Hilbert.KDB ℕ) := by
+  constructor;
+  . exact KD_weakerThan_KDB;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use ((atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KD.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Serial F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _)  by
+        simpa [ValidOnModel, ValidOnFrame, Satisfies];
+      let F : Frame := ⟨Fin 2, λ x y => x ≤ y⟩;
+      use F;
+      constructor;
+      . intro x;
+        match x with
+        | 0 => use 1; omega;
+        | 1 => use 1;
+      . use (λ w _ => w = 0), 0;
+        suffices ∃ x, (0 : F.World) ≺ x ∧ ¬x ≺ 0 by
+          simpa [Semantics.Realize, Satisfies];
+        use 1;
+        omega;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KD_KT.lean b/Foundation/Modal/Hilbert/WeakerThan/KD_KT.lean
index 78212fae..72ae95bd 100644
--- a/Foundation/Modal/Hilbert/WeakerThan/KD_KT.lean
+++ b/Foundation/Modal/Hilbert/WeakerThan/KD_KT.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal.Hilbert
 
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KTB_S5.lean b/Foundation/Modal/Hilbert/WeakerThan/KTB_S5.lean
new file mode 100644
index 00000000..3b29b254
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KTB_S5.lean
@@ -0,0 +1,48 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula
+open Formula.Kripke
+
+lemma KTB_weakerThan_S5 : (Hilbert.KTB ℕ) ≤ₛ (Hilbert.S5 ℕ) := by
+  apply Kripke.weakerThan_of_subset_FrameClass ReflexiveSymmetricFrameClass ReflexiveEuclideanFrameClass;
+  rintro F ⟨F_refl, F_eucl⟩;
+  refine ⟨F_refl, symm_of_refl_eucl F_refl F_eucl⟩;
+
+theorem KTB_strictlyWeakerThan_S5 : (Hilbert.KTB ℕ) <ₛ (Hilbert.S5 ℕ) := by
+  constructor;
+  . exact KTB_weakerThan_S5;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (◇(atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KTB.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Reflexive F.Rel ∧ Symmetric F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _) by
+        simp [ValidOnModel, ValidOnFrame, Satisfies];
+        tauto;
+      let F : Frame := ⟨
+        Fin 3,
+        λ x y =>
+          match x, y with
+          | 1, 2 => False
+          | 2, 1 => False
+          | _, _ => True
+      ⟩;
+      use F;
+      refine ⟨?_, ?_, ?_⟩;
+      . simp [Reflexive];
+      . unfold Symmetric;
+        aesop;
+      . use (λ w _ => w = 1), 0;
+        suffices (0 : F.World) ≺ 1 ∧ ∃ x, (0 : F.World) ≺ x ∧ ¬x ≺ 1 by
+          simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . tauto;
+        . use 2;
+          tauto;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KT_KTB.lean b/Foundation/Modal/Hilbert/WeakerThan/KT_KTB.lean
new file mode 100644
index 00000000..5d62c736
--- /dev/null
+++ b/Foundation/Modal/Hilbert/WeakerThan/KT_KTB.lean
@@ -0,0 +1,30 @@
+import Foundation.Modal.Kripke.Geach.Systems
+
+namespace LO.Modal.Hilbert
+
+open System
+open Modal.Kripke
+open Formula (atom)
+open Formula.Kripke
+
+lemma KT_weakerThan_KTB : (Hilbert.KT α) ≤ₛ (Hilbert.KTB α) := normal_weakerThan_of_subset $ by intro; aesop;
+
+theorem KT_strictlyWeakerThan_KTB : (Hilbert.KT ℕ) <ₛ (Hilbert.KTB ℕ) := by
+  constructor;
+  . exact KT_weakerThan_KTB;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use ((atom 0) ➝ □◇(atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KT.Kripke.sound.not_provable_of_countermodel;
+      simp [ValidOnModel, ValidOnFrame, Satisfies];
+      use ⟨Fin 2, λ x y => x ≤ y⟩;
+      constructor;
+      . simp [Reflexive];
+      . use (λ x _ => x = 0), 0;
+        simp [Semantics.Realize, Satisfies];
+        use 1;
+        omega;
+
+end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/KT_S4.lean b/Foundation/Modal/Hilbert/WeakerThan/KT_S4.lean
index 200b0a8a..f1ff128e 100644
--- a/Foundation/Modal/Hilbert/WeakerThan/KT_S4.lean
+++ b/Foundation/Modal/Hilbert/WeakerThan/KT_S4.lean
@@ -1,11 +1,58 @@
-import Foundation.Modal.Hilbert.Systems
-import Foundation.Modal.System.Grz
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal.Hilbert
 
 open System
-open Formula (atom)
+open Modal.Kripke
+open Formula
+open Formula.Kripke
 
 lemma KT_weakerThan_S4 : (Hilbert.KT α) ≤ₛ (Hilbert.S4 α) := normal_weakerThan_of_subset $ by intro; aesop;
 
+theorem KT_strictlyWeakerThan_S4 : (Hilbert.KT ℕ) <ₛ (Hilbert.S4 ℕ) := by
+  constructor;
+  . exact KT_weakerThan_S4;
+  . apply weakerThan_iff.not.mpr;
+    push_neg;
+    use (□(atom 0) ➝ □□(atom 0));
+    constructor;
+    . exact Deduction.maxm! (by simp);
+    . apply KT.Kripke.sound.not_provable_of_countermodel;
+      suffices ∃ F : Frame, Reflexive F.Rel ∧ ∃ V : Valuation F, ∃ w : F.World, ¬(Satisfies ⟨F, V⟩ w _)  by
+        simpa [ValidOnModel, ValidOnFrame, Satisfies];
+      let F : Frame := ⟨
+        Fin 3,
+        λ x y =>
+          match x, y with
+          | 0, 0 => True
+          | 0, 1 => True
+          | 1, 1 => True
+          | 1, 2 => True
+          | 2, 2 => True
+          | _, _ => False
+      ⟩;
+      use F;
+      constructor;
+      . intro x;
+        match x with
+        | 0 => tauto;
+        | 1 => tauto;
+        | 2 => tauto;
+      . use (λ w _ => w = 0 ∨ w = 1), 0;
+        suffices (∀ (y : F.World), (0 : F.World) ≺ y → y = 0 ∨ y = 1) ∧ ∃ x, (0 : F.World) ≺ x ∧ ∃ y, x ≺ y ∧ y ≠ 0 ∧ y ≠ 1 by
+          simpa [Semantics.Realize, Satisfies];
+        constructor;
+        . intro y hy;
+          match y with
+          | 0 => tauto;
+          | 1 => tauto;
+          | 2 => tauto;
+        . use 1;
+          constructor;
+          . tauto;
+          . use 2;
+            constructor;
+            . tauto;
+            . simp;
+
 end LO.Modal.Hilbert
diff --git a/Foundation/Modal/Hilbert/WeakerThan/S4_S5.lean b/Foundation/Modal/Hilbert/WeakerThan/S4_S5.lean
index f562cf08..74b1466b 100644
--- a/Foundation/Modal/Hilbert/WeakerThan/S4_S5.lean
+++ b/Foundation/Modal/Hilbert/WeakerThan/S4_S5.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal.Hilbert
 
diff --git a/Foundation/Modal/Kripke/Dot3.lean b/Foundation/Modal/Kripke/Dot3.lean
index 5985ad39..4379b777 100644
--- a/Foundation/Modal/Kripke/Dot3.lean
+++ b/Foundation/Modal/Kripke/Dot3.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO.Modal
 
diff --git a/Foundation/Modal/Kripke/Filteration.lean b/Foundation/Modal/Kripke/Filteration.lean
index ef2742ed..b19fe5dd 100644
--- a/Foundation/Modal/Kripke/Filteration.lean
+++ b/Foundation/Modal/Kripke/Filteration.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 import Foundation.Modal.Kripke.Closure
 
 universe u v
diff --git a/Foundation/Modal/Kripke/Geach.lean b/Foundation/Modal/Kripke/Geach/Basic.lean
similarity index 69%
rename from Foundation/Modal/Kripke/Geach.lean
rename to Foundation/Modal/Kripke/Geach/Basic.lean
index a41514d8..66116337 100644
--- a/Foundation/Modal/Kripke/Geach.lean
+++ b/Foundation/Modal/Kripke/Geach/Basic.lean
@@ -59,63 +59,117 @@ abbrev FrameClass.IsGeach (C : FrameClass) (ts : List GeachConfluent.Taple) := C
 
 section
 
+/-- Frame class of `Hilbert.KT` -/
 abbrev ReflexiveFrameClass : FrameClass := { F | Reflexive F.Rel }
-
 lemma ReflexiveFrameClass.is_geach : ReflexiveFrameClass.IsGeach [⟨0, 0, 1, 0⟩] := by
   simp only [FrameClass.IsGeach, ReflexiveFrameClass, GeachConfluent.reflexive_def,
     MultiGeachConfluentFrameClass.def_one, GeachConfluentFrameClass];
 
-
+/-- Frame class of `Hilbert.KD` -/
 abbrev SerialFrameClass : FrameClass := { F | Serial F.Rel }
-
 lemma SerialFrameClass.is_geach : SerialFrameClass.IsGeach [⟨0, 0, 1, 1⟩] := by
   simp only [FrameClass.IsGeach, SerialFrameClass, GeachConfluent.serial_def,
     MultiGeachConfluentFrameClass.def_one, GeachConfluentFrameClass];
 
+/-- Frame class of `Hilbert.KB` -/
+abbrev SymmetricFrameClass : FrameClass := { F | Symmetric F.Rel }
+lemma SymmetricFrameClass.is_geach : SymmetricFrameClass.IsGeach [⟨0, 1, 0, 1⟩] := by
+  simp only [FrameClass.IsGeach, SymmetricFrameClass, GeachConfluent.symmetric_def,
+    MultiGeachConfluentFrameClass.def_one, GeachConfluentFrameClass];
 
+/-- Frame class of `Hilbert.K4` -/
 abbrev TransitiveFrameClass : FrameClass := { F | Transitive F.Rel }
-
 lemma TransitiveFrameClass.is_geach : TransitiveFrameClass.IsGeach ([⟨0, 2, 1, 0⟩]) := by
   simp only [FrameClass.IsGeach, TransitiveFrameClass, GeachConfluent.transitive_def,
     MultiGeachConfluentFrameClass.def_one, GeachConfluentFrameClass];
 
+/-- Frame class of `Hilbert.K5` -/
+abbrev EuclideanFrameClass : FrameClass := { F | Euclidean F.Rel }
+lemma EuclideanFrameClass.is_geach : EuclideanFrameClass.IsGeach ([⟨1, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, EuclideanFrameClass, GeachConfluent.euclidean_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
+/-- Frame class of `Hilbert.S5` -/
 abbrev ReflexiveEuclideanFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Euclidean F.Rel }
-
 lemma ReflexiveEuclideanFrameClass.is_geach : ReflexiveEuclideanFrameClass.IsGeach ([⟨0, 0, 1, 0⟩, ⟨1, 1, 0, 1⟩]) := by
   simp only [FrameClass.IsGeach, ReflexiveEuclideanFrameClass, GeachConfluent.reflexive_def,
     GeachConfluent.euclidean_def, MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
-
+/-- Frame class of `Hilbert.KTB` -/
 abbrev ReflexiveSymmetricFrameClass : FrameClass := { F | Reflexive F ∧ Symmetric F }
-
 lemma ReflexiveSymmetricFrameClass.is_geach : ReflexiveSymmetricFrameClass.IsGeach ([⟨0, 0, 1, 0⟩, ⟨0, 1, 0, 1⟩]) := by
   simp only [FrameClass.IsGeach, ReflexiveSymmetricFrameClass, GeachConfluent.reflexive_def,
     GeachConfluent.symmetric_def, MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
-
+/-- Frame class of `Hilbert.S4` -/
 abbrev ReflexiveTransitiveFrameClass : FrameClass := { F | Reflexive F ∧ Transitive F }
-
 lemma ReflexiveTransitiveFrameClass.is_geach : ReflexiveTransitiveFrameClass.IsGeach ([⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩]) := by
   simp only [FrameClass.IsGeach, ReflexiveTransitiveFrameClass, GeachConfluent.reflexive_def,
     GeachConfluent.transitive_def, MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
-
+/-- Frame class of `Hilbert.S4Dot2` -/
 abbrev ReflexiveTransitiveConfluentFrameClass : FrameClass := { F | Reflexive F ∧ Transitive F ∧ Confluent F }
-
 lemma ReflexiveTransitiveConfluentFrameClass.is_geach : ReflexiveTransitiveConfluentFrameClass.IsGeach ([⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 1, 1⟩]) := by
   simp only [FrameClass.IsGeach, ReflexiveTransitiveConfluentFrameClass,
     GeachConfluent.reflexive_def, GeachConfluent.transitive_def, GeachConfluent.confluent_def,
     MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
-
+/-- Frame class of `Hilbert.KT4B` -/
 abbrev ReflexiveTransitiveSymmetricFrameClass : FrameClass := { F | Reflexive F ∧ Transitive F ∧ Symmetric F }
-
 lemma ReflexiveTransitiveSymmetricFrameClass.is_geach : ReflexiveTransitiveSymmetricFrameClass.IsGeach ([⟨0, 0, 1, 0⟩, ⟨0, 2, 1, 0⟩, ⟨0, 1, 0, 1⟩]) := by
   simp only [FrameClass.IsGeach, ReflexiveTransitiveSymmetricFrameClass,
     GeachConfluent.reflexive_def, GeachConfluent.transitive_def, GeachConfluent.symmetric_def,
     MultiGeachConfluentFrameClass, MultiGeachConfluent];
 
+/-- Frame class of `Hilbert.KD45` -/
+abbrev SerialTransitiveEuclideanFrameClass : FrameClass := { F | Serial F ∧ Transitive F ∧ Euclidean F }
+lemma SerialTransitiveEuclideanFrameClass.is_geach : SerialTransitiveEuclideanFrameClass.IsGeach ([⟨0, 0, 1, 1⟩, ⟨0, 2, 1, 0⟩, ⟨1, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, SerialTransitiveEuclideanFrameClass,
+    GeachConfluent.serial_def, GeachConfluent.transitive_def, GeachConfluent.euclidean_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
+/-- Frame class of `Hilbert.K45` -/
+abbrev TransitiveEuclideanFrameClass : FrameClass := { F | Transitive F ∧ Euclidean F }
+lemma TransitiveEuclideanFrameClass.is_geach : TransitiveEuclideanFrameClass.IsGeach ([⟨0, 2, 1, 0⟩, ⟨1, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, TransitiveEuclideanFrameClass,
+    GeachConfluent.transitive_def, GeachConfluent.euclidean_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
+/-- Frame class of `Hilbert.KB4` -/
+abbrev SymmetricTransitiveFrameClass : FrameClass := { F | Symmetric F ∧ Transitive F }
+lemma SymmetricTransitiveFrameClass.is_geach : SymmetricTransitiveFrameClass.IsGeach ([⟨0, 1, 0, 1⟩, ⟨0, 2, 1, 0⟩]) := by
+  simp only [FrameClass.IsGeach, SymmetricTransitiveFrameClass,
+    GeachConfluent.symmetric_def, GeachConfluent.transitive_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
+/-- Frame class of `Hilbert.KB5` -/
+abbrev SymmetricEuclideanFrameClass : FrameClass := { F | Symmetric F ∧ Euclidean F }
+lemma SymmetricEuclideanFrameClass.is_geach : SymmetricEuclideanFrameClass.IsGeach ([⟨0, 1, 0, 1⟩, ⟨1, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, SymmetricEuclideanFrameClass,
+    GeachConfluent.symmetric_def, GeachConfluent.euclidean_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
+/-- Frame class of `Hilbert.KDB` -/
+abbrev SerialSymmetricFrameClass : FrameClass := { F | Serial F ∧ Symmetric F }
+lemma SerialSymmetricFrameClass.is_geach : SerialSymmetricFrameClass.IsGeach ([⟨0, 0, 1, 1⟩, ⟨0, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, SerialSymmetricFrameClass,
+    GeachConfluent.serial_def, GeachConfluent.symmetric_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
+/-- Frame class of `Hilbert.KD4` -/
+abbrev SerialTransitiveFrameClass : FrameClass := { F | Serial F ∧ Transitive F }
+lemma SerialTransitiveFrameClass.is_geach : SerialTransitiveFrameClass.IsGeach ([⟨0, 0, 1, 1⟩, ⟨0, 2, 1, 0⟩]) := by
+  simp only [FrameClass.IsGeach, SerialTransitiveFrameClass,
+    GeachConfluent.serial_def, GeachConfluent.transitive_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent]
+
+/-- Frame class of `Hilbert.KD5` -/
+abbrev SerialEuclideanFrameClass : FrameClass := { F | Serial F ∧ Euclidean F }
+lemma SerialEuclideanFrameClass.is_geach : SerialEuclideanFrameClass.IsGeach ([⟨0, 0, 1, 1⟩, ⟨1, 1, 0, 1⟩]) := by
+  simp only [FrameClass.IsGeach, SerialEuclideanFrameClass,
+    GeachConfluent.serial_def, GeachConfluent.euclidean_def,
+    MultiGeachConfluentFrameClass, MultiGeachConfluent];
+
 end
 
 
@@ -201,83 +255,6 @@ namespace Hilbert
 
 open Modal.Kripke
 
-
-section soundness
-
-open Hilbert.Kripke
-
-instance KD.Kripke.sound : Sound (Hilbert.KD ℕ) (SerialFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [SerialFrameClass.is_geach]; apply GeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach, Axioms.MultiGeach.def_one])
-
-instance KD.consistent : System.Consistent (Hilbert.KD ℕ) := instConsistent_of_nonempty_frameclass (C := SerialFrameClass) $ by
-  rw [SerialFrameClass.is_geach];
-  simp;
-
-
-instance KT.Kripke.sound : Sound (Hilbert.KT ℕ) (ReflexiveFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [ReflexiveFrameClass.is_geach]; apply GeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach, Axioms.MultiGeach.def_one])
-
-instance KT.consistent : System.Consistent (Hilbert.KT ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveFrameClass) $ by
-  rw [ReflexiveFrameClass.is_geach];
-  simp;
-
-
-instance KTB.Kripke.sound : Sound (Hilbert.KTB ℕ) (ReflexiveSymmetricFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [ReflexiveSymmetricFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach])
-
-instance KTB.consistent : System.Consistent (Hilbert.KTB ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveSymmetricFrameClass) $ by
-  rw [ReflexiveSymmetricFrameClass.is_geach];
-  simp;
-
-
-instance K4.Kripke.sound : Sound (Hilbert.K4 ℕ) (TransitiveFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [TransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach])
-
-instance K4.consistent : System.Consistent (Hilbert.K4 ℕ) := instConsistent_of_nonempty_frameclass (C := TransitiveFrameClass) $ by
-  rw [TransitiveFrameClass.is_geach];
-  simp;
-
-
-instance S4.Kripke.sound : Sound (Hilbert.S4 ℕ) (ReflexiveTransitiveFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [ReflexiveTransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach])
-
-instance S4.consistent : System.Consistent (Hilbert.S4 ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveTransitiveFrameClass) $ by
-  rw [ReflexiveTransitiveFrameClass.is_geach];
-  simp;
-
-
-instance S5.Kripke.sound : Sound (Hilbert.S5 ℕ) (ReflexiveEuclideanFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [ReflexiveEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach])
-
-instance S5.consistent : System.Consistent (Hilbert.S5 ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveEuclideanFrameClass) $ by
-  rw [ReflexiveEuclideanFrameClass.is_geach];
-  simp;
-
-
-instance KT4B.Kripke.sound : Sound (Hilbert.KT4B ℕ) (ReflexiveTransitiveSymmetricFrameClass) :=
-  instSound_of_frameClass_definedBy
-  (by rw [ReflexiveTransitiveSymmetricFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
-  (by simp [is_geach, Hilbert.Geach])
-
-instance KT4B.consistent : System.Consistent (Hilbert.KT4B ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveTransitiveSymmetricFrameClass) $ by
-  rw [ReflexiveTransitiveSymmetricFrameClass.is_geach];
-  simp;
-
-end soundness
-
-
 namespace Kripke
 
 open System
@@ -358,45 +335,15 @@ lemma is_symmetric_of_subset_B (h : 𝗕 ⊆ Ax) : Symmetric (canonicalFrame (Hi
   apply is_geachConfluent_of_subset_Geach;
   exact h;
 
+lemma is_confluent_of_subset_dot2 (h : .𝟮 ⊆ Ax) : Confluent (canonicalFrame (Hilbert.ExtK Ax)).Rel := by
+  rw [GeachConfluent.confluent_def, Axioms.Dot2.is_geach] at *
+  apply is_geachConfluent_of_subset_Geach;
+  exact h;
+
 end canonicalFrame
 
 end Kripke
 
-
-section completeness
-
-instance KT.Kripke.complete : Complete (Hilbert.KT ℕ) ReflexiveFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [ReflexiveFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp [Axioms.T.is_geach];
-
-instance KTB.Kripke.complete : Complete (Hilbert.KTB ℕ) ReflexiveSymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [ReflexiveSymmetricFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp [Axioms.MultiGeach.def_two, Axioms.T.is_geach, Axioms.B.is_geach];
-
-instance K4.Kripke.complete : Complete (Hilbert.K4 ℕ) TransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [TransitiveFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp;
-
-instance S4.Kripke.complete : Complete (Hilbert.S4 ℕ) ReflexiveTransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [ReflexiveTransitiveFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp [Axioms.T.is_geach, Axioms.Four.is_geach, Axioms.MultiGeach.def_two];
-
-instance KT4B.Kripke.complete : Complete (Hilbert.KT4B ℕ) ReflexiveTransitiveSymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [ReflexiveTransitiveSymmetricFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp [Axioms.T.is_geach, Axioms.Four.is_geach, Axioms.B.is_geach, Axioms.MultiGeach.def_three];
-
-instance S5.Kripke.complete : Complete (Hilbert.S5 ℕ) ReflexiveEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
-  rw [ReflexiveEuclideanFrameClass.is_geach];
-  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
-  simp [Axioms.T.is_geach, Axioms.Five.is_geach, Axioms.MultiGeach.def_two];
-
-end completeness
-
 end Hilbert
 
 end LO.Modal
diff --git a/Foundation/Modal/Kripke/Geach/Systems.lean b/Foundation/Modal/Kripke/Geach/Systems.lean
new file mode 100644
index 00000000..b61cb385
--- /dev/null
+++ b/Foundation/Modal/Kripke/Geach/Systems.lean
@@ -0,0 +1,313 @@
+import Foundation.Modal.Kripke.Geach.Basic
+
+namespace LO.Modal
+
+namespace Hilbert
+
+open Modal.Kripke
+open Kripke
+open Hilbert.Kripke
+
+namespace KD
+
+instance Kripke.sound : Sound (Hilbert.KD ℕ) (SerialFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SerialFrameClass.is_geach]; apply GeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach, Axioms.MultiGeach.def_one])
+
+instance consistent : System.Consistent (Hilbert.KD ℕ) := instConsistent_of_nonempty_frameclass (C := SerialFrameClass) $ by
+  rw [SerialFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+end KD
+
+
+namespace KT
+
+instance Kripke.sound : Sound (Hilbert.KT ℕ) (ReflexiveFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [ReflexiveFrameClass.is_geach]; apply GeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach, Axioms.MultiGeach.def_one])
+
+instance consistent : System.Consistent (Hilbert.KT ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveFrameClass) $ by
+  rw [ReflexiveFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KT ℕ) ReflexiveFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [ReflexiveFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KT
+
+
+namespace KB
+
+instance Kripke.sound : Sound (Hilbert.KB ℕ) (SymmetricFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SymmetricFrameClass.is_geach]; apply GeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach, Axioms.MultiGeach.def_one])
+
+instance consistent : System.Consistent (Hilbert.KB ℕ) := instConsistent_of_nonempty_frameclass (C := SymmetricFrameClass) $ by
+  rw [SymmetricFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KB ℕ) SymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SymmetricFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KB
+
+
+namespace KTB
+
+instance Kripke.sound : Sound (Hilbert.KTB ℕ) (ReflexiveSymmetricFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [ReflexiveSymmetricFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KTB ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveSymmetricFrameClass) $ by
+  rw [ReflexiveSymmetricFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KTB ℕ) ReflexiveSymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [ReflexiveSymmetricFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KTB
+
+
+namespace K4
+
+instance Kripke.sound : Sound (Hilbert.K4 ℕ) (TransitiveFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [TransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.K4 ℕ) := instConsistent_of_nonempty_frameclass (C := TransitiveFrameClass) $ by
+  rw [TransitiveFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.K4 ℕ) TransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [TransitiveFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end K4
+
+
+namespace K5
+
+instance Kripke.sound : Sound (Hilbert.K5 ℕ) (EuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [EuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.K5 ℕ) := instConsistent_of_nonempty_frameclass (C := EuclideanFrameClass) $ by
+  rw [EuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.K5 ℕ) EuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [EuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end K5
+
+
+namespace S4
+
+instance Kripke.sound : Sound (Hilbert.S4 ℕ) (ReflexiveTransitiveFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [ReflexiveTransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.S4 ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveTransitiveFrameClass) $ by
+  rw [ReflexiveTransitiveFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.S4 ℕ) ReflexiveTransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [ReflexiveTransitiveFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end S4
+
+
+
+namespace S5
+
+instance Kripke.sound : Sound (Hilbert.S5 ℕ) (ReflexiveEuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [ReflexiveEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.S5 ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveEuclideanFrameClass) $ by
+  rw [ReflexiveEuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.S5 ℕ) ReflexiveEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [ReflexiveEuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end S5
+
+
+namespace KT4B
+
+instance Kripke.sound : Sound (Hilbert.KT4B ℕ) (ReflexiveTransitiveSymmetricFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [ReflexiveTransitiveSymmetricFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KT4B ℕ) := instConsistent_of_nonempty_frameclass (C := ReflexiveTransitiveSymmetricFrameClass) $ by
+  rw [ReflexiveTransitiveSymmetricFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KT4B ℕ) ReflexiveTransitiveSymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [ReflexiveTransitiveSymmetricFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KT4B
+
+
+namespace KD45
+
+instance Kripke.sound : Sound (Hilbert.KD45 ℕ) (SerialTransitiveEuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SerialTransitiveEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KD45 ℕ) := instConsistent_of_nonempty_frameclass (C := SerialTransitiveEuclideanFrameClass) $ by
+  rw [SerialTransitiveEuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KD45 ℕ) SerialTransitiveEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SerialTransitiveEuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KD45
+
+
+namespace K45
+
+instance Kripke.sound : Sound (Hilbert.K45 ℕ) (TransitiveEuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [TransitiveEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.K45 ℕ) := instConsistent_of_nonempty_frameclass (C := TransitiveEuclideanFrameClass) $ by
+  rw [TransitiveEuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.K45 ℕ) TransitiveEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [TransitiveEuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end K45
+
+
+namespace KB4
+
+instance Kripke.sound : Sound (Hilbert.KB4 ℕ) (SymmetricTransitiveFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SymmetricTransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KB4 ℕ) := instConsistent_of_nonempty_frameclass (C := SymmetricTransitiveFrameClass) $ by
+  rw [SymmetricTransitiveFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KB4 ℕ) SymmetricTransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SymmetricTransitiveFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KB4
+
+
+namespace KB5
+
+instance Kripke.sound : Sound (Hilbert.KB5 ℕ) (SymmetricEuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SymmetricEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KB5 ℕ) := instConsistent_of_nonempty_frameclass (C := SymmetricEuclideanFrameClass) $ by
+  rw [SymmetricEuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KB5 ℕ) SymmetricEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SymmetricEuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KB5
+
+
+namespace KDB
+
+instance Kripke.sound : Sound (Hilbert.KDB ℕ) (SerialSymmetricFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SerialSymmetricFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KDB ℕ) := instConsistent_of_nonempty_frameclass (C := SerialSymmetricFrameClass) $ by
+  rw [SerialSymmetricFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KDB ℕ) SerialSymmetricFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SerialSymmetricFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KDB
+
+
+namespace KD4
+
+instance Kripke.sound : Sound (Hilbert.KD4 ℕ) (SerialTransitiveFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SerialTransitiveFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KD4 ℕ) := instConsistent_of_nonempty_frameclass (C := SerialTransitiveFrameClass) $ by
+  rw [SerialTransitiveFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KD4 ℕ) SerialTransitiveFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SerialTransitiveFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KD4
+
+
+namespace KD5
+
+instance Kripke.sound : Sound (Hilbert.KD5 ℕ) (SerialEuclideanFrameClass) :=
+  instSound_of_frameClass_definedBy
+  (by rw [SerialEuclideanFrameClass.is_geach]; apply MultiGeachConfluentFrameClass.isDefinedBy)
+  (by simp [is_geach, Hilbert.Geach])
+
+instance consistent : System.Consistent (Hilbert.KD5 ℕ) := instConsistent_of_nonempty_frameclass (C := SerialEuclideanFrameClass) $ by
+  rw [SerialEuclideanFrameClass.is_geach];
+  exact MultiGeachConfluentFrameClass.nonempty;
+
+instance Kripke.complete : Complete (Hilbert.KD5 ℕ) SerialEuclideanFrameClass := Kripke.instCompleteOfCanonical $ by
+  rw [SerialEuclideanFrameClass.is_geach];
+  apply Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach;
+  simp;
+
+end KD5
+
+
+end Hilbert
+
+end LO.Modal
diff --git a/Foundation/Modal/Kripke/Grz/Definability.lean b/Foundation/Modal/Kripke/Grz/Definability.lean
index 6b9bd732..bf953b0b 100644
--- a/Foundation/Modal/Kripke/Grz/Definability.lean
+++ b/Foundation/Modal/Kripke/Grz/Definability.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 
 namespace LO
 
diff --git a/Foundation/Modal/Kripke/Kripke.lean b/Foundation/Modal/Kripke/Kripke.lean
index 500dc661..e5edbdd2 100644
--- a/Foundation/Modal/Kripke/Kripke.lean
+++ b/Foundation/Modal/Kripke/Kripke.lean
@@ -6,7 +6,7 @@ import Foundation.Modal.Kripke.Filteration
 
 import Foundation.Modal.Kripke.ComplexityLimited
 
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 import Foundation.Modal.Kripke.Ver
 import Foundation.Modal.Kripke.Dot3
 import Foundation.Modal.Kripke.S5
diff --git a/Foundation/Modal/Kripke/S5.lean b/Foundation/Modal/Kripke/S5.lean
index 61046e00..aaaec91b 100644
--- a/Foundation/Modal/Kripke/S5.lean
+++ b/Foundation/Modal/Kripke/S5.lean
@@ -1,4 +1,4 @@
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 import Foundation.Modal.Kripke.Preservation
 
 namespace LO.Modal
diff --git a/Foundation/Modal/ModalCompanion/GMT.lean b/Foundation/Modal/ModalCompanion/GMT.lean
index b0a8d67b..edc86fd5 100644
--- a/Foundation/Modal/ModalCompanion/GMT.lean
+++ b/Foundation/Modal/ModalCompanion/GMT.lean
@@ -1,5 +1,5 @@
 import Foundation.IntProp.Kripke.Completeness
-import Foundation.Modal.Kripke.Geach
+import Foundation.Modal.Kripke.Geach.Systems
 import Foundation.Modal.ModalCompanion.Basic
 
 namespace LO.Modal
diff --git a/Foundation/Modal/System/Basic.lean b/Foundation/Modal/System/Basic.lean
index f5dc8f24..baf51267 100644
--- a/Foundation/Modal/System/Basic.lean
+++ b/Foundation/Modal/System/Basic.lean
@@ -378,6 +378,20 @@ protected class KT extends System.K 𝓢, HasAxiomT 𝓢
 
 protected class KTc extends System.K 𝓢, HasAxiomTc 𝓢
 
+protected class KTB extends System.K 𝓢, HasAxiomT 𝓢, HasAxiomB 𝓢
+
+protected class KD45 extends System.K 𝓢, HasAxiomD 𝓢, HasAxiomFour 𝓢, HasAxiomFive 𝓢
+
+protected class KB4 extends System.K 𝓢, HasAxiomB 𝓢, HasAxiomFour 𝓢
+
+protected class KDB extends System.K 𝓢, HasAxiomD 𝓢, HasAxiomB 𝓢
+
+protected class KD4 extends System.K 𝓢, HasAxiomD 𝓢, HasAxiomFour 𝓢
+
+protected class KD5 extends System.K 𝓢, HasAxiomD 𝓢, HasAxiomFive 𝓢
+
+protected class K45 extends System.K 𝓢, HasAxiomFour 𝓢, HasAxiomFive 𝓢
+
 protected class Triv extends System.K 𝓢, HasAxiomT 𝓢, HasAxiomTc 𝓢
 instance [System.Triv 𝓢] : System.KT 𝓢 where
 instance [System.Triv 𝓢] : System.KTc 𝓢 where