diff --git a/Foundation.lean b/Foundation.lean
index a60bcf8d7..f39db4f72 100644
--- a/Foundation.lean
+++ b/Foundation.lean
@@ -258,6 +258,7 @@ public import Foundation.Modal.Hilbert.Axiom
 public import Foundation.Modal.Hilbert.GL_K4Loeb_K4Henkin_K4Hen
 public import Foundation.Modal.Hilbert.NNFormula
 public import Foundation.Modal.Hilbert.Normal.Basic
+public import Foundation.Modal.Hilbert.Normal2.Basic
 public import Foundation.Modal.Hilbert.WithHenkin.Basic
 public import Foundation.Modal.Hilbert.WithLoeb.Basic
 public import Foundation.Modal.Hilbert.WithRE.Basic
@@ -343,6 +344,13 @@ public import Foundation.Modal.Kripke.Root
 public import Foundation.Modal.Kripke.Terminated
 public import Foundation.Modal.Kripke.Tree
 public import Foundation.Modal.Kripke.Undefinability
+public import Foundation.Modal.Kripke2.Axiom.Geach
+public import Foundation.Modal.Kripke2.Basic
+public import Foundation.Modal.Kripke2.Completeness
+public import Foundation.Modal.Kripke2.Hilbert
+public import Foundation.Modal.Kripke2.Logic.K
+public import Foundation.Modal.Kripke2.Logic.K4
+public import Foundation.Modal.Kripke2.Logic.KT
 public import Foundation.Modal.Logic.Basic
 public import Foundation.Modal.Logic.D.Basic
 public import Foundation.Modal.Logic.GL.Independency
diff --git a/Foundation/Modal/Hilbert/Normal2/Basic.lean b/Foundation/Modal/Hilbert/Normal2/Basic.lean
new file mode 100644
index 000000000..8e88fd66f
--- /dev/null
+++ b/Foundation/Modal/Hilbert/Normal2/Basic.lean
@@ -0,0 +1,308 @@
+module
+
+public import Foundation.Modal.Entailment.GL
+public import Foundation.Modal.Entailment.Grz
+public import Foundation.Modal.Entailment.K4Hen
+public import Foundation.Modal.Entailment.K4Henkin
+public import Foundation.Modal.Entailment.S5Grz
+public import Foundation.Modal.Hilbert.Axiom
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Propositional.Entailment.Cl.Łukasiewicz
+
+@[expose] public section
+
+namespace LO.Modal
+
+open LO.Entailment LO.Modal.Entailment
+
+inductive Hilbert.Normal2 {α} (Ax : Set (Formula α)) : Logic α
+| axm {φ}       : φ ∈ Ax → Normal2 Ax φ
+| mdp {φ ψ}     : Normal2 Ax (φ ➝ ψ) → Normal2 Ax φ → Normal2 Ax ψ
+| nec {φ}       : Normal2 Ax φ → Normal2 Ax (□φ)
+| implyK φ ψ    : Normal2 Ax $ Axioms.ImplyK φ ψ
+| implyS φ ψ χ  : Normal2 Ax $ Axioms.ImplyS φ ψ χ
+| ec φ ψ        : Normal2 Ax $ Axioms.ElimContra φ ψ
+
+namespace Hilbert.Normal2
+
+variable {Ax Ax₁ Ax₂ : Axiom α}
+
+instance : Entailment.Łukasiewicz (Hilbert.Normal2 Ax) where
+  implyK {_ _} := by constructor; apply Hilbert.Normal2.implyK;
+  implyS {_ _ _} := by constructor; apply Hilbert.Normal2.implyS;
+  elimContra {_ _} := by constructor; apply Hilbert.Normal2.ec;
+  mdp h₁ h₂ := by
+    constructor;
+    apply Hilbert.Normal2.mdp;
+    . exact h₁.1;
+    . exact h₂.1;
+
+instance : Entailment.Necessitation (Hilbert.Normal2 Ax) where
+  nec h := by constructor; apply Hilbert.Normal2.nec; exact h.1;
+
+lemma axm' {φ} : φ ∈ Ax → Hilbert.Normal2 Ax ⊢ φ := fun h ↦ ⟨⟨axm h⟩⟩
+
+protected lemma rec!
+  {motive   : (φ : Formula α) → (Normal2 Ax ⊢ φ) → Sort}
+  (axm      : ∀ {φ : Formula α}, (h : φ ∈ Ax) → motive φ (axm' h))
+  (mdp      : ∀ {φ ψ : Formula α}, {hφψ : (Normal2 Ax) ⊢ φ ➝ ψ} → {hφ : (Normal2 Ax) ⊢ φ} → motive (φ ➝ ψ) hφψ → motive φ hφ → motive ψ (hφψ ⨀ hφ))
+  (nec      : ∀ {φ}, {hφψ : (Normal2 Ax) ⊢ φ} → motive (φ) hφψ → motive (□φ) (nec! hφψ))
+  (implyK   : ∀ {φ ψ}, motive (Axioms.ImplyK φ ψ) $ by simp)
+  (implyS   : ∀ {φ ψ χ}, motive (Axioms.ImplyS φ ψ χ) $ by simp)
+  (ec       : ∀ {φ ψ}, motive (Axioms.ElimContra φ ψ) $ by simp)
+  : ∀ {φ}, (d : Normal2 Ax ⊢ φ) → motive φ d := by
+  rintro φ d;
+  replace d := Logic.iff_provable.mp d;
+  induction d with
+  | axm h => apply axm h;
+  | mdp hφψ hφ ihφψ ihφ =>
+    apply mdp;
+    . exact ihφψ (Logic.iff_provable.mpr hφψ);
+    . exact ihφ (Logic.iff_provable.mpr hφ);
+  | nec hφ ihφ => apply nec; exact ihφ (Logic.iff_provable.mpr hφ);
+  | implyK φ ψ => apply implyK;
+  | implyS φ ψ χ => apply implyS;
+  | ec φ ψ => apply ec;
+
+open Axiom
+
+
+section
+
+inductive buildAxioms.Symbol
+  | B
+  | C4
+  | CD
+  | D
+  | Dum
+  | Five
+  | Four
+  | Grz
+  | H
+  | Hen
+  | K
+  | L
+  | McK
+  | Mk
+  | P
+  | Point2
+  | Point3
+  | Point4
+  | T
+  | Tc
+  | Ver
+  | WeakPoint2
+  | WeakPoint3
+  | Z
+deriving DecidableEq
+
+def buildAxioms (α : Type*) (l : List buildAxioms.Symbol)
+  : Set (Formula α) :=
+    (if l.contains .B          then { Axioms.B φ            | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .C4         then { Axioms.C4 φ           | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .CD         then { Axioms.CD φ           | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .D          then { Axioms.D φ            | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Dum        then { Axioms.Dum φ          | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Five       then { Axioms.Five φ         | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Four       then { Axioms.Four φ         | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Grz        then { Axioms.Grz φ          | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .H          then { Axioms.H φ            | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Hen        then { Axioms.Hen φ          | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .K          then { Axioms.K φ ψ          | (φ : Formula α) (ψ : Formula α) } else ∅) ∪
+    (if l.contains .L          then { Axioms.L φ            | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .McK        then { Axioms.McK φ          | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Mk         then { Axioms.Mk φ ψ         | (φ : Formula α) (ψ : Formula α) } else ∅) ∪
+    (if l.contains .P          then { Axioms.P }                                                else ∅) ∪
+    (if l.contains .Point2     then { Axioms.Point2 φ       | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Point3     then { Axioms.Point3 φ ψ     | (φ : Formula α) (ψ : Formula α) } else ∅) ∪
+    (if l.contains .T          then { Axioms.T φ            | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Tc         then { Axioms.Tc φ           | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .Ver        then { Axioms.Ver φ          | (φ : Formula α) }                 else ∅) ∪
+    (if l.contains .WeakPoint2 then { Axioms.WeakPoint2 φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪
+    (if l.contains .WeakPoint3 then { Axioms.WeakPoint3 φ ψ | (φ : Formula α) (ψ : Formula α) } else ∅) ∪
+    (if l.contains .Z          then { Axioms.Z φ            | (φ : Formula α) }                 else ∅)
+
+variable {l : List buildAxioms.Symbol} {φ ψ χ : Formula α}
+
+protected lemma buildAxioms.mem_axiomK (h : .K ∈ l := by decide) : Axioms.K φ ψ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomD (h : .D ∈ l := by decide) : Axioms.D φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomT (h : .T ∈ l := by decide) : Axioms.T φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomB (h : .B ∈ l := by decide) : Axioms.B φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomFour (h : .Four ∈ l := by decide) : Axioms.Four φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomFive (h : .Five ∈ l := by decide) : Axioms.Five φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomPoint2 (h : .Point2 ∈ l := by decide) : Axioms.Point2 φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomPoint3 (h : .Point3 ∈ l := by decide) : Axioms.Point3 φ ψ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomGrz (h : .Grz ∈ l := by decide) : Axioms.Grz φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+protected lemma buildAxioms.mem_axiomL (h : .L ∈ l := by decide) : Axioms.L φ ∈ buildAxioms α l := by
+  simp only [buildAxioms, Set.mem_union, Set.mem_ite_empty_right, Set.mem_setOf_eq];
+  grind;
+
+attribute [simp, grind <=]
+  buildAxioms.mem_axiomK
+  buildAxioms.mem_axiomD
+  buildAxioms.mem_axiomT
+  buildAxioms.mem_axiomB
+  buildAxioms.mem_axiomFour
+  buildAxioms.mem_axiomFive
+  buildAxioms.mem_axiomPoint2
+  buildAxioms.mem_axiomPoint3
+  buildAxioms.mem_axiomGrz
+  buildAxioms.mem_axiomL
+
+end
+
+end Hilbert.Normal2
+
+
+section
+
+
+open Lean in
+macro "defineModalLogic" name:ident "[" xs:ident,* "]" : command => do
+  let xs ← xs.getElems.mapM $ λ stx => pure (Lean.mkIdentFrom stx stx.getId)
+
+  let logicName := mkIdent (name.getId.appendAfter "'")
+
+  let instHasAxiomK ←
+    if xs.contains (mkIdent `K)
+    then `(command| instance {α} : Entailment.HasAxiomK ($logicName α) where K φ ψ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomD ←
+    if xs.contains (mkIdent `D)
+    then `(command| instance {α} : Entailment.HasAxiomD ($logicName α) where D φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomT ←
+    if xs.contains (mkIdent `T)
+    then `(command| instance {α} : Entailment.HasAxiomT ($logicName α) where T φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomB ←
+    if xs.contains (mkIdent `B)
+    then `(command| instance {α} : Entailment.HasAxiomB ($logicName α) where B φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomFour ←
+    if xs.contains (mkIdent `Four)
+    then `(command| instance {α} : Entailment.HasAxiomFour ($logicName α) where Four φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomFive ←
+    if xs.contains (mkIdent `Five)
+    then `(command| instance {α} : Entailment.HasAxiomFive ($logicName α) where Five φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomPoint2 ←
+    if xs.contains (mkIdent `Point2)
+    then `(command| instance {α} : Entailment.HasAxiomPoint2 ($logicName α) where Point2 φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomPoint3 ←
+    if xs.contains (mkIdent `Point3)
+    then `(command| instance {α} : Entailment.HasAxiomPoint3 ($logicName α) where Point3 φ ψ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomGrz ←
+    if xs.contains (mkIdent `Grz)
+    then `(command| instance {α} : Entailment.HasAxiomGrz ($logicName α) where Grz φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+  let instHasAxiomL ←
+    if xs.contains (mkIdent `L)
+    then `(command| instance {α} : Entailment.HasAxiomL ($logicName α) where L φ := by constructor; apply Hilbert.Normal2.axm; simp)
+    else `(section end)
+
+  `(
+    abbrev $logicName (α : Type*) := Hilbert.Normal2 $ Hilbert.Normal2.buildAxioms α [$[$xs],*]
+
+    namespace $logicName
+
+    $instHasAxiomK
+    $instHasAxiomT
+    $instHasAxiomD
+    $instHasAxiomPoint2
+    $instHasAxiomPoint3
+    $instHasAxiomGrz
+    $instHasAxiomL
+    $instHasAxiomB
+    $instHasAxiomFour
+    $instHasAxiomFive
+
+    end $logicName
+  )
+
+open Hilbert.Normal2.buildAxioms.Symbol
+
+defineModalLogic Dum         [K, T, Four, Dum]
+defineModalLogic DumPoint2   [K, T, Four, Dum, Point2]
+defineModalLogic DumPoint3   [K, T, Four, Dum, Point3]
+defineModalLogic GL          [K, L]
+defineModalLogic GLPoint2    [K, L, WeakPoint2]
+defineModalLogic GLPoint3    [K, L, WeakPoint3]
+defineModalLogic Grz         [K, Grz]
+defineModalLogic GrzPoint2   [K, Grz, Point2]
+defineModalLogic GrzPoint3   [K, Grz, Point3]
+defineModalLogic K           [K]
+defineModalLogic K4          [K, Four]
+defineModalLogic K45         [K, Four, Five]
+defineModalLogic K4Hen       [K, Four, Hen]
+defineModalLogic K4McK       [K, Four, McK]
+defineModalLogic K4Point2    [K, Four, WeakPoint2]
+defineModalLogic K4Point3    [K, Four, WeakPoint3]
+defineModalLogic K5          [K, Five]
+defineModalLogic KB          [K, B]
+defineModalLogic KB4         [K, B, Four]
+defineModalLogic KB5         [K, B, Five]
+defineModalLogic KD          [K, D]
+defineModalLogic KD4         [K, D, Four]
+defineModalLogic KD45        [K, D, Four, Five]
+defineModalLogic KD4Point3Z  [K, D, Four, Point3, Z]
+defineModalLogic KD5         [K, D, Five]
+defineModalLogic KDB         [K, D, B]
+defineModalLogic KHen        [K, Hen]
+defineModalLogic KT          [K, T]
+defineModalLogic KT4B        [K, T, Four, B]
+defineModalLogic KTB         [K, T, B]
+defineModalLogic KTc         [K, Tc]
+defineModalLogic KTMk        [K, T, Mk]
+defineModalLogic N           []
+defineModalLogic NP          [P]
+defineModalLogic S4          [K, T, Four]
+defineModalLogic S4H         [K, T, Four, H]
+defineModalLogic S4McK       [K, T, Four, McK]
+defineModalLogic S4Point2    [K, T, Four, Point2]
+defineModalLogic S4Point2McK [K, T, Four, Point2, McK]
+defineModalLogic S4Point3    [K, T, Four, Point3]
+defineModalLogic S4Point3McK [K, T, Four, Point3, McK]
+defineModalLogic S4Point4    [K, T, Four, Point4]
+defineModalLogic S4Point4McK [K, T, Four, Point4, McK]
+defineModalLogic S5          [K, T, Five]
+defineModalLogic S5Grz       [K, T, Five, Grz]
+defineModalLogic Triv        [K, T, Tc]
+defineModalLogic Ver         [K, Ver]
+
+end
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Axiom/Geach.lean b/Foundation/Modal/Kripke2/Axiom/Geach.lean
new file mode 100644
index 000000000..79f9c1e81
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Axiom/Geach.lean
@@ -0,0 +1,177 @@
+module
+
+public import Foundation.Modal.Kripke2.Completeness
+public import Foundation.Vorspiel.Rel.Coreflexive
+
+@[expose] public section
+
+namespace Rel
+
+variable {R : Rel α α} {x y z : α}
+
+protected structure IsGeachConvergent.Taple where
+  i : ℕ
+  j : ℕ
+  m : ℕ
+  n : ℕ
+
+class IsGeachConvergent (R : Rel α α) (i j m n : ℕ) : Prop where
+  gconv : ∀ ⦃x y z : α⦄, R.Iterate i x y → R.Iterate j x z → ∃ u, R.Iterate m y u ∧ R.Iterate n z u
+
+instance [R.IsGeachConvergent 0 0 1 0] : Std.Refl R := by
+  constructor;
+  simpa using IsGeachConvergent.gconv (i := 0) (j := 0) (m := 1) (n := 0);
+
+instance [Std.Refl R] : R.IsGeachConvergent 0 0 1 0 := by
+  constructor;
+  rintro x y z Rxy Rxz;
+  simp_all [Std.Refl.refl];
+
+
+instance [R.IsGeachConvergent 0 0 1 1] : IsSerial R := by
+  constructor;
+  have := IsGeachConvergent.gconv (R := R) (i := 0) (j := 0) (m := 1) (n := 1);
+  simp only [Iterate.iff_zero, Iterate.iff_succ, exists_eq_right, forall_apply_eq_imp_iff, forall_eq', and_self] at this;
+  apply this;
+
+instance [IsSerial R] : R.IsGeachConvergent 0 0 1 1 := by
+  constructor;
+  rintro x y z Rxy rfl;
+  simp_all only [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ, exists_eq_right, and_self];
+  apply _root_.IsSerial.serial
+
+
+instance [R.IsGeachConvergent 0 2 1 0] : IsTrans _ R := by
+  constructor;
+  rintro x y z Rxy Ryz;
+  have := IsGeachConvergent.gconv (R := R) (i := 0) (j := 2) (m := 1) (n := 0) (x := x) (y := x) (z := z) rfl;
+  simp only [Iterate.iff_succ, Iterate.iff_zero, exists_eq_right, exists_eq_right', forall_exists_index, and_imp] at this;
+  apply this y Rxy Ryz;
+instance [IsTrans _ R] : R.IsGeachConvergent 0 2 1 0 := by
+  constructor;
+  rintro x _ z rfl ⟨y, Rxy, Ryz⟩;
+  use z;
+  have := IsTrans.trans _ _ z Rxy (by simpa using Ryz);
+  tauto;
+
+
+end Rel
+
+
+
+namespace LO.Modal
+
+namespace KripkeModel
+
+variable {κ α} [Nonempty κ] {φ ψ χ : Formula α} {K : Rel κ κ}
+
+lemma models_axiomGeach_of_isGeachConvergent
+  (i j m n : ℕ) [K.IsGeachConvergent i j m n]
+  : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ ((◇^[i](□^[m]φ)) ➝ (□^[j](◇^[n]φ))) := by
+  intro V x him;
+  apply KripkeModel.forces_boxItr.mpr;
+  intro y Rxy;
+  apply forces_diaItr.mpr;
+  obtain ⟨z, Rxz, hm⟩ := forces_diaItr.mp him;
+  obtain ⟨u, Rzu, hnu⟩ := Rel.IsGeachConvergent.gconv (i := i) (j := j) (m := m) (n := n) Rxz Rxy;
+  use u;
+  constructor;
+  . assumption;
+  . exact (KripkeModel.forces_boxItr.mp hm) _ Rzu;
+
+lemma models_axiomT_of_reflexive [Std.Refl K] : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.T φ) := models_axiomGeach_of_isGeachConvergent 0 0 1 0
+lemma models_axiomD_of_serial [IsSerial K] : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.D φ) := models_axiomGeach_of_isGeachConvergent 0 0 1 1
+lemma models_axiomFour_of_transitive [IsTrans _ K] : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.Four φ) := models_axiomGeach_of_isGeachConvergent 0 2 1 0
+attribute [grind .]
+  models_axiomT_of_reflexive
+  models_axiomD_of_serial
+  models_axiomFour_of_transitive
+
+
+variable {a : α}
+
+lemma isGeachConvergent_of_models_axiomGeach
+  (i j m n : ℕ) (h : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ ((◇^[i](□^[m](.atom a))) ➝ (□^[j](◇^[n](.atom a)))))
+  : K.IsGeachConvergent i j m n := by
+  constructor;
+  rintro x y z Rxy Rxz;
+  let M : KripkeModel κ α := ⟨K, (λ _ v => K.Iterate m y v)⟩;
+  have : M.Forces x (□^[j](◇^[n](.atom a))) := h M.val x $ forces_diaItr.mpr ⟨y, ⟨Rxy, forces_boxItr.mpr (by tauto)⟩⟩;
+  replace : M.Forces z (◇^[n](.atom a)) := forces_boxItr.mp this z Rxz;
+  obtain ⟨u, Rzu, Ryu⟩ := forces_diaItr.mp this;
+  use u;
+  constructor;
+  . exact Ryu;
+  . assumption;
+
+lemma reflexive_of_models_axiomT (h : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.T (.atom a))) : Std.Refl K := by
+  suffices K.IsGeachConvergent 0 0 1 0 by infer_instance;
+  exact isGeachConvergent_of_models_axiomGeach _ _ _ _ h;
+
+lemma serial_of_models_axiomD (h : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.D (.atom a))) : IsSerial K := by
+  suffices K.IsGeachConvergent 0 0 1 1 by infer_instance;
+  exact isGeachConvergent_of_models_axiomGeach _ _ _ _ h;
+
+lemma transitive_of_models_axiomFour (h : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ (Axioms.Four (.atom a))) : IsTrans _ K := by
+  suffices K.IsGeachConvergent 0 2 1 0 by infer_instance;
+  apply isGeachConvergent_of_models_axiomGeach _ _ _ _ h;
+
+end KripkeModel
+
+
+namespace canonicalKripkeModel
+
+open Entailment
+open MaximalConsistentTableau
+open canonicalKripkeModel
+
+variable {α} [DecidableEq α] [Encodable α]
+         {S} [Entailment S (Formula α)]
+         {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢]
+
+instance instGeachConvergent (i j m n : ℕ) [Entailment.HasAxiomGeach ⟨i, j, m, n⟩ 𝓢]
+  : (canonicalKripkeModel 𝓢).frame.IsGeachConvergent i j m n := by
+  constructor;
+  rintro x y z Rxy Rxz;
+  have ⟨u, hu⟩ := MaximalConsistentTableau.lindenbaum (𝓢 := 𝓢) (t₀ := ⟨□⁻¹^[m]'y.1.1, ◇⁻¹^[n]'z.1.2⟩) $ by
+    rintro Γ Δ hΓ hΔ;
+    by_contra! hC;
+    have hγ : □^[m](Γ.conj) ∈ y.1.1 := y.mdp_mem₁_provable collect_boxItr_fconj! $ iff_mem₁_fconj.mpr $ by
+      intro χ hχ;
+      obtain ⟨ξ, hξ, rfl⟩ := Finset.LO.exists_of_mem_boxItr hχ;
+      apply hΓ;
+      assumption;
+    have hδ : ◇^[n](Δ.disj) ∈ z.1.2 := mdp_mem₂_provable distribute_diaItr_fdisj! $ iff_mem₂_fdisj.mpr $ by
+      intro χ hχ;
+      obtain ⟨ξ, hξ, rfl⟩ := Finset.LO.exists_of_mem_diaItr hχ;
+      apply hΔ;
+      assumption;
+    generalize Γ.conj = γ at hγ hC;
+    generalize Δ.disj = δ at hδ hC;
+    have : 𝓢 ⊢ □^[m]γ ➝ □^[m]δ := imply_boxItr_distribute'! hC;
+    have : □^[m]δ ∈ y.1.1 := mdp_mem₁_provable this hγ;
+    have : ◇^[i](□^[m]δ) ∈ x.1.1 := iff_relItr_diaItr_subset₁.mp Rxy this;
+    have : □^[j](◇^[n]δ) ∈ x.1.1 := mdp_mem₁_provable (axiomGeach! (g := ⟨i, j, m, n⟩)) this;
+    have : ◇^[n]δ ∈ z.1.1 := iff_relItr_boxItr_subset₁.mp Rxz this;
+    have : ◇^[n]δ ∉ z.1.2 := iff_not_mem₂_mem₁.mpr this;
+    contradiction;
+  use u;
+  constructor;
+  . apply iff_relItr_boxItr_subset₁.mpr;
+    apply hu.1;
+  . apply iff_relItr_diaItr_subset₂.mpr;
+    apply hu.2;
+
+instance instReflexive [Entailment.HasAxiomT 𝓢] : Std.Refl (canonicalKripkeModel 𝓢).frame := by
+  suffices (canonicalKripkeModel 𝓢).frame.IsGeachConvergent 0 0 1 0 by infer_instance;
+  infer_instance;
+
+instance instTransitive [Entailment.HasAxiomFour 𝓢] : IsTrans _ (canonicalKripkeModel 𝓢).frame := by
+  suffices (canonicalKripkeModel 𝓢).frame.IsGeachConvergent 0 2 1 0 by infer_instance;
+  infer_instance;
+
+end canonicalKripkeModel
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Basic.lean b/Foundation/Modal/Kripke2/Basic.lean
new file mode 100644
index 000000000..4d1874568
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Basic.lean
@@ -0,0 +1,222 @@
+module
+
+public import Foundation.Modal.Logic.Basic
+public import Foundation.Vorspiel.Rel.Basic
+public import Foundation.Logic.ForcingRelation
+
+@[expose] public section
+
+variable {κ α : Type*} [Nonempty κ]
+
+namespace LO.Modal
+
+open Entailment
+
+structure KripkeModel (κ : Type*) [Nonempty κ] (α : Type*) where
+  frame : Rel κ κ
+  val : α → κ → Prop
+
+namespace KripkeModel
+
+abbrev world (_ : KripkeModel κ α) := κ
+
+variable {M : KripkeModel κ α} {x y z : M.world} {a : α} {φ ψ χ : Formula α} {n m : ℕ}
+
+
+abbrev rel : Rel M.world M.world := M.frame
+infix:45 " ≺ " => rel
+
+abbrev relInv (x y : M.world) := M.frame y x
+infix:45 " ≻ " => relInv
+
+abbrev relItr (n : ℕ) : Rel M.world M.world := M.frame.Iterate n
+notation x:45 " ≺^[" n:0 "] " y:46 => relItr n x y
+
+-- instance : CoeSort (KripkeModel κ α) (Type*) := ⟨λ M => M.world⟩
+instance : CoeFun (KripkeModel κ α) (λ _ => α → κ → Prop) := ⟨fun M => M.val⟩
+
+abbrev replaceVal (M : KripkeModel κ α) (V : α → M.world → Prop) : KripkeModel κ α where
+  frame := M.frame
+  val := V
+
+@[simp]
+lemma replaceVal_comp {V₁ V₂ : α → M.world → Prop}
+  : (M.replaceVal V₁ |>.replaceVal V₂) = M.replaceVal V₂ := by tauto;
+
+section Forces
+
+@[grind]
+def Forces (M : KripkeModel κ α) (x : M.world) : Formula α → Prop
+  | .atom a  => M a x
+  | ⊥  => False
+  | φ ➝ ψ => (M.Forces x φ) ➝ (M.Forces x ψ)
+  | □φ   => ∀ y, x ≺ y → (M.Forces y φ)
+
+instance : ForcingRelation M.world (Formula α) where
+  Forces := Forces M
+
+@[grind =] lemma forces_atom : x ⊩ (.atom a) ↔ M a x := by tauto
+@[simp, grind .] lemma forces_falsum : x ⊮ ⊥ := by tauto;
+@[simp, grind .] lemma forces_verum : x ⊩ ⊤ := by tauto;
+@[grind =] lemma forces_imp : x ⊩ (φ ➝ ψ) ↔ (x ⊩ φ) ➝ (x ⊩ ψ) := by tauto;
+@[grind =] lemma forces_neg : x ⊩ ∼φ ↔ x ⊮ φ := by tauto;
+@[grind =] lemma forces_and : x ⊩ (φ ⋏ ψ) ↔ (x ⊩ φ) ∧ (x ⊩ ψ) := by grind;
+@[grind =] lemma forces_or : x ⊩ (φ ⋎ ψ) ↔ (x ⊩ φ) ∨ (x ⊩ ψ) := by grind;
+@[grind =] lemma forces_iff : x ⊩ (φ ⭤ ψ) ↔ ((x ⊩ φ) ↔ (x ⊩ ψ)) := by grind [LogicalConnective.iff];
+@[grind =] lemma forces_box : x ⊩ □φ ↔ ∀ y, x ≺ y → (y ⊩ φ) := by tauto;
+
+@[grind =] lemma iff_forces_dn : x ⊩ ∼∼φ ↔ x ⊩ φ := by simp [forces_neg, forces_neg.not];
+
+@[grind =]
+lemma forces_dia : x ⊩ ◇φ ↔ ∃ y, x ≺ y ∧ (y ⊩ φ) := calc
+  _ ↔ x ⊩ ∼□(∼φ) := by rw [DiaByBox.dia_by_box]
+  _ ↔ x ⊮ □(∼φ)  := by grind;
+  _ ↔ ¬x ⊩ □(∼φ) := by grind;
+  _ ↔ ¬(∀ y, x ≺ y → y ⊩ ∼φ) := by grind;
+  _ ↔ ∃ y, x ≺ y ∧ y ⊮ ∼φ := by grind;
+  _ ↔ ∃ y, x ≺ y ∧ y ⊩ (∼∼φ) := by simp [forces_neg];
+  _ ↔ _ := by simp [iff_forces_dn];
+
+instance : ForcingRelation.BasicSemantics M.world where
+  verum {_} := forces_verum
+  falsum {_} := forces_falsum
+  and {_ _ _} := forces_and
+  or {_ _ _} := forces_or
+
+
+@[grind =]
+lemma forces_boxItr : x ⊩ □^[n]φ ↔ ∀ y, x ≺^[n] y → y ⊩ φ := by
+  induction n generalizing x <;> grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+@[grind =]
+lemma forces_diaItr : x ⊩ ◇^[n]φ ↔ ∃ y, x ≺^[n] y ∧ (y ⊩ φ) := by
+  induction n generalizing x <;> grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+
+@[grind =]
+lemma forces_lconj {l : List _} : x ⊩ l.conj ↔ ∀ φ ∈ l, x ⊩ φ := by
+  induction l <;>
+  grind [List.conj_cons, List.conj_nil];
+
+@[grind =]
+lemma forces_lconj₂ {l : List _} : x ⊩ ⋀l ↔ ∀ φ ∈ l, x ⊩ φ := by
+  induction l using List.induction_with_singleton <;>
+  grind [List.conj₂_nil, List.conj₂_cons_nonempty, List.conj₂_singleton]
+
+@[grind =]
+lemma forces_lconj' {l : List β} {ι : β → Formula α} : x ⊩ l.conj' ι ↔ ∀ i ∈ l, x ⊩ (ι i) := by
+  grind [List.conj'];
+
+@[grind =]
+lemma forces_fconj {s : Finset _} : x ⊩ s.conj ↔ ∀ φ ∈ s, x ⊩ φ := by
+  apply Iff.trans forces_lconj₂;
+  simp;
+
+@[grind =]
+lemma forces_fconj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.conj' ι ↔ ∀ i ∈ s, x ⊩ (ι i) := by
+  apply Iff.trans forces_lconj';
+  simp;
+
+
+@[grind =]
+lemma forces_ldisj {l : List _} : x ⊩ l.disj ↔ ∃ φ ∈ l, x ⊩ φ := by
+  induction l <;>
+  grind [List.disj_cons, List.disj_nil];
+
+@[grind =]
+lemma forces_ldisj₂ {l : List _} : x ⊩ ⋁l ↔ ∃ φ ∈ l, x ⊩ φ := by
+  induction l using List.induction_with_singleton <;>
+  grind [List.disj₂_nil, List.disj₂_cons_nonempty, List.disj₂_singleton]
+
+@[grind =]
+lemma forces_ldisj' {l : List β} {ι : β → Formula α} : x ⊩ l.disj' ι ↔ ∃ i ∈ l, x ⊩ (ι i) := by
+  grind [List.disj']
+
+@[grind =]
+lemma forces_fdisj {s : Finset _} : x ⊩ s.disj ↔ ∃ φ ∈ s, x ⊩ φ := by
+  apply Iff.trans forces_ldisj₂;
+  simp;
+
+@[grind =]
+lemma forces_fdisj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.disj' ι ↔ ∃ i ∈ s, x ⊩ (ι i) := by
+  apply Iff.trans forces_ldisj';
+  simp;
+
+
+/-
+lemma iff_forces_diaItr_dual : (x ⊩ ◇^[n]φ) ↔ (x ⊩ ∼□^[n](∼φ)) := calc
+  _ ↔ ∃ y, x ≺^[n] y ∧ (y ⊩ φ) := forces_diaItr
+  _ ↔ ¬(∀ y, x ≺^[n] y → ¬y ⊩ φ) := by push_neg; rfl;
+  _ ↔ _ := by sorry;
+-/
+
+lemma iff_dia_dual : (x ⊩ ◇φ) ↔ (x ⊩ ∼□(∼φ)) := by
+  grind [Rel.Iterate.iff_zero, Rel.Iterate.iff_succ];
+
+
+abbrev replaceSubstVal (M : KripkeModel κ α) (s : Substitution α) : KripkeModel κ α
+  := M.replaceVal (λ a x => x ⊩ (s a))
+
+lemma iff_forces_replaceSubstVal (s : Substitution α) :
+  (M.replaceSubstVal s).Forces x φ ↔ x ⊩ (φ⟦s⟧) := by
+  induction φ generalizing x <;> . dsimp [Forces]; grind;
+
+end Forces
+
+
+section Models
+
+variable {M : KripkeModel κ α} {φ ψ χ : Formula α}
+
+def Validates (M : KripkeModel κ α) (φ) := M.world ∀⊩ φ
+
+instance : Semantics (KripkeModel κ α) (Formula α) where
+  Models := Validates
+
+
+@[simp, grind .]
+lemma validates_verum : M ⊧ ⊤ := ForcingRelation.AllForces.verum
+
+@[simp, grind .]
+lemma validates_falsum : M ⊭ ⊥ := by
+  have : Inhabited M.world := Inhabited.mk $ Nonempty.some inferInstance;
+  apply ForcingRelation.AllForces.falsum
+
+@[grind =]
+lemma validates_and : M ⊧ (φ ⋏ ψ) ↔ M ⊧ φ ∧ M ⊧ ψ := ForcingRelation.AllForces.and
+
+@[grind =]
+lemma iff_notValidates_exists_world_notForces : M ⊭ φ ↔ ∃ x : M.world, x ⊮ φ := by
+  simp [Semantics.Models, Semantics.NotModels, Validates];
+alias ⟨exists_world_notForces_of_notValidates, notValidates_of_exists_world_notForces⟩ := iff_notValidates_exists_world_notForces
+
+@[grind <=]
+lemma validates_mdp (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ := fun x ↦ hpq x (hp x)
+
+@[grind <=]
+lemma validates_nec (hp : M ⊧ φ) : M ⊧ □φ := fun _ y _ ↦ hp y
+
+@[grind <=]
+lemma validates_multinec (hp : M ⊧ φ) : M ⊧ □^[n]φ := by induction n <;> grind;
+
+lemma validates_implyK : M ⊧ (Axioms.ImplyK φ ψ) := by intro x; grind;
+lemma validates_implyS : M ⊧ (Axioms.ImplyS φ ψ χ) := by intro x; grind;
+lemma validates_elimContra : M ⊧ (Axioms.ElimContra φ ψ) := by intro x; grind;
+lemma validates_axiomK : M ⊧ (Axioms.K φ ψ) := by tauto;
+
+attribute [simp, grind .]
+  validates_implyK
+  validates_implyS
+  validates_elimContra
+  validates_axiomK
+
+end Models
+
+
+def logic (M : KripkeModel κ α) : Logic α := { φ | M ⊧ φ }
+
+end KripkeModel
+
+
+
+end LO.Modal
diff --git a/Foundation/Modal/Kripke2/Completeness.lean b/Foundation/Modal/Kripke2/Completeness.lean
new file mode 100644
index 000000000..c7245e375
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Completeness.lean
@@ -0,0 +1,200 @@
+module
+
+public import Foundation.Modal.Tableau
+public import Foundation.Modal.Kripke2.Basic
+
+@[expose] public section
+
+namespace LO.Modal
+
+open Entailment
+open Formula
+open MaximalConsistentTableau
+open KripkeModel
+
+variable [DecidableEq α] [Encodable α]
+variable {S} [Entailment S (Formula α)]
+variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢]
+variable {φ ψ : Formula α}
+
+@[grind]
+def canonicalKripkeModel (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.K 𝓢] : KripkeModel (MaximalConsistentTableau 𝓢) α where
+  frame t₁ t₂ := □⁻¹'t₁.1.1 ⊆ t₂.1.1
+  val a t := (atom a) ∈ t.1.1
+
+attribute [grind .]
+  MaximalConsistentTableau.not_mem₁_falsum
+  MaximalConsistentTableau.mem₂_falsum
+attribute [grind =] MaximalConsistentTableau.iff_mem₁_imp
+attribute [grind =] MaximalConsistentTableau.iff_not_mem₁_mem₂
+attribute [grind =]
+  MaximalConsistentTableau.iff_mem₁_box
+  MaximalConsistentTableau.iff_mem₂_box
+
+namespace canonicalKripkeModel
+
+variable {t : (canonicalKripkeModel 𝓢).world}
+
+lemma truthlemma : (φ ∈ t.1.1 ↔ t ⊩ φ) ∧ (φ ∈ t.1.2 ↔ t ⊮ φ) := by
+  induction φ generalizing t with
+  | hatom | hfalsum | himp => grind;
+  | hbox φ ihφ =>
+    constructor;
+    . constructor;
+      . intro h t' Rtt';
+        apply ihφ.1.1;
+        grind;
+      . intro h;
+        apply iff_mem₁_box.mpr;
+        intro t' Rtt';
+        apply ihφ.1.2;
+        exact h t' Rtt';
+    . constructor;
+      . intro h;
+        apply forces_box.not.mpr;
+        push_neg;
+        obtain ⟨t', Rtt', ht'⟩ := iff_mem₂_box.mp h;
+        use t';
+        grind;
+      . intro h;
+        apply iff_mem₂_box.mpr;
+        replace h := forces_box.not.mp h;
+        grind;
+
+@[grind =] lemma truthlemma₁ : φ ∈ t.1.1 ↔ t ⊩ φ := truthlemma.1
+@[grind =] lemma truthlemma₂ : φ ∈ t.1.2 ↔ t ⊮ φ := truthlemma.2
+
+@[grind =]
+lemma iff_valid_provable : (canonicalKripkeModel 𝓢) ⊧ φ ↔ 𝓢 ⊢ φ := by
+  constructor;
+  . contrapose!;
+    intro h;
+    have : Tableau.Consistent 𝓢 (∅, {φ}) := by
+      apply Tableau.iff_consistent_empty_singleton₂.mpr;
+      exact h;
+    obtain ⟨t, ht⟩ := lindenbaum this;
+    apply notValidates_of_exists_world_notForces;
+    use t;
+    apply truthlemma₂.mp;
+    apply ht.2;
+    tauto_set;
+  . intro h t;
+    exact truthlemma₁.mp $ MaximalConsistentTableau.iff_provable_mem₁.mp h t;
+
+
+variable {x y : (canonicalKripkeModel 𝓢).world} {n : ℕ}
+
+lemma iff_rel_forces_box : x ≺ y ↔ ∀ {φ}, x ⊩ □φ → y ⊩ φ := by grind;
+lemma iff_relItr_forces_boxItr : x ≺^[n] y ↔ ∀ {φ}, x ⊩ □^[n]φ → y ⊩ φ := by
+  constructor;
+  . grind;
+  . induction n generalizing x y with
+    | zero =>
+      suffices (∀ {φ : Formula _}, x ⊩ φ → y ⊩ φ) → x = y by simpa;
+      intro h;
+      apply intro_equality;
+      . grind;
+      . intro φ hφ;
+        rw [truthlemma₂] at hφ ⊢;
+        apply h (φ := ∼φ) (by grind);
+    | succ n ih =>
+      intro h;
+      obtain ⟨t, ht⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := ⟨{ φ | x ⊩ □φ }, □^[n]'{ φ | y ⊮ φ }⟩) $ by
+        intro Γ Δ hΓ hΔ;
+        by_contra! hC;
+        have : 𝓢 ⊢ □Γ.conj ➝ □Δ.disj := imply_box_distribute'! hC;
+        have : □Δ.disj ∈ x.1.1 := mdp_mem₁_provable this $ by
+          apply truthlemma₁.mpr;
+          intro y Rxy;
+          apply forces_fconj.mpr;
+          intro φ hφ;
+          apply hΓ hφ y Rxy;
+        have : x ⊩ □Δ.disj := truthlemma₁.mp this;
+        have : x ⊩ □^[(n + 1)](□⁻¹^[n]'Δ).disj := by
+          suffices x ⊩ □□^[n](□⁻¹^[n]'Δ).disj by simpa;
+          intro y Rxy;
+          apply forces_boxItr.mpr;
+          intro z Ryz;
+          apply forces_fdisj.mpr;
+          obtain ⟨ψ, hψ₁, hψ₂⟩ := forces_fdisj.mp $ this y Rxy;
+          obtain ⟨ξ, hξ, rfl⟩ := hΔ hψ₁;
+          use ξ;
+          constructor;
+          . simpa [Finset.LO.preboxItr];
+          . exact forces_boxItr.mp hψ₂ _ Ryz;
+        have : y ⊩ (□⁻¹^[n]'Δ).disj := h this;
+        obtain ⟨ψ, hψ₁, hψ₂⟩ := forces_fdisj.mp $ this;
+        have : y ⊮ ψ := Set.LO.mem_of_mem_boxItr $ @hΔ (□^[n]ψ) $ by
+          show □^[n]ψ ∈ ↑Δ;
+          grind;
+        contradiction;
+      use t;
+      constructor;
+      . intro φ hφ;
+        apply ht.1;
+        exact truthlemma₁.mp hφ;
+      . apply ih;
+        intro φ hφ;
+        have := Set.compl_subset_compl.mpr ht.2 $ iff_not_mem₂_mem₁.mpr $ truthlemma₁.mpr hφ;
+        grind;
+
+lemma iff_relItr_boxItr_subset₁ : x ≺^[n] y ↔ ((□⁻¹^[n]'x.1.1) ⊆ y.1.1) := ⟨
+  fun h _ hφ => truthlemma₁.mpr $ iff_relItr_forces_boxItr.mp h $ truthlemma₁.mp hφ,
+  fun h => iff_relItr_forces_boxItr.mpr fun hφ => truthlemma₁.mp (h $ truthlemma₁.mpr hφ)
+⟩
+lemma iff_rel_box_subset₁ : x ≺ y ↔ □⁻¹'x.1.1 ⊆ y.1.1 := by
+  simpa using iff_relItr_boxItr_subset₁ (n := 1);
+
+
+lemma iff_relItr_boxItr_subset₂ : x ≺^[n] y ↔ (y.1.2 ⊆ (□⁻¹^[n]'x.1.2)) := by
+  apply Iff.trans iff_relItr_boxItr_subset₁;
+  grind;
+lemma iff_rel_box_subset₂ : x ≺ y ↔ (y.1.2 ⊆ (□⁻¹'x.1.2)) := by
+  simpa using iff_relItr_boxItr_subset₂ (n := 1);
+
+lemma iff_relItr_forces_diaItr : x ≺^[n] y ↔ ∀ {φ}, y ⊩ φ → x ⊩ (◇^[n]φ) := by
+  constructor;
+  . intro Rxy φ hφ;
+    apply forces_diaItr.mpr;
+    use y;
+  . intro h;
+    apply iff_relItr_forces_boxItr.mpr;
+    intro φ;
+    contrapose!;
+    intro hφ;
+    obtain ⟨z, Rxz, hz⟩ := forces_diaItr.mp $ h (φ := ∼φ) (by grind);
+    grind;
+lemma iff_rel_forces_dia : x ≺ y ↔ ∀ {φ}, y ⊩ φ → x ⊩ (◇φ) := by
+  simpa using iff_relItr_forces_diaItr (n := 1);
+
+
+lemma iff_relItr_diaItr_subset₁ : x ≺^[n] y ↔ (y.1.1 ⊆ (◇⁻¹^[n]'x.1.1)) := ⟨
+  fun h _ hφ => truthlemma₁.mpr $ iff_relItr_forces_diaItr.mp h $ truthlemma₁.mp hφ,
+  fun h => iff_relItr_forces_diaItr.mpr fun hφ => truthlemma₁.mp $ h $ truthlemma₁.mpr hφ
+⟩
+lemma iff_rel_dia_subset₁ : x ≺ y ↔ (y.1.1 ⊆ (◇'⁻¹x.1.1)) := by
+  simpa using iff_relItr_diaItr_subset₁ (n := 1);
+
+
+lemma iff_relItr_diaItr_subset₂ : x ≺^[n] y ↔ ((◇⁻¹^[n]'x.1.2) ⊆ y.1.2) := by
+  constructor;
+  . intro Rxy φ;
+    contrapose;
+    intro hφ;
+    apply iff_not_mem₂_mem₁.mpr;
+    apply iff_relItr_diaItr_subset₁.mp Rxy;
+    exact iff_not_mem₂_mem₁.mp hφ;
+  . intro H;
+    apply iff_relItr_diaItr_subset₁.mpr;
+    intro φ;
+    contrapose;
+    intro hφ;
+    exact iff_not_mem₁_mem₂.mpr $ @H φ (iff_not_mem₁_mem₂.mp hφ);
+lemma iff_rel_dia_subset₂ : x ≺ y ↔ ((◇'⁻¹x.1.2) ⊆ y.1.2) := by
+  simpa using iff_relItr_diaItr_subset₂ (n := 1);
+
+end canonicalKripkeModel
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Hilbert.lean b/Foundation/Modal/Kripke2/Hilbert.lean
new file mode 100644
index 000000000..51b191e0c
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Hilbert.lean
@@ -0,0 +1,69 @@
+module
+
+public import Foundation.Modal.Hilbert.Normal2.Basic
+public import Foundation.Modal.Kripke2.Basic
+
+@[expose] public section
+
+namespace LO.Modal
+
+/-
+namespace KripkeModel
+
+abbrev validOnFrame (M : KripkeModel α) (φ : Formula α) :=  ∀ V, (M.replaceVal V) ⊧ φ
+infix:45 " ⊧ᶠ " => validOnFrame
+
+end KripkeModel
+-/
+
+
+namespace Hilbert.Normal2
+
+open Formula
+
+variable {κ α} [Nonempty κ] {Ax : Axiom α} {φ : Formula α}
+
+lemma valid_of_provable (K) (hK : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧* Ax)
+  : Hilbert.Normal2 Ax ⊢ φ → (∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ) := by
+  intro hφ;
+  induction hφ using Hilbert.Normal2.rec! with
+  | axm hφ =>
+    intro V x;
+    apply hK V |>.models_set hφ;
+  | implyK | implyS | ec => grind;
+  | mdp ih₁ ih₂ => intro V; exact KripkeModel.validates_mdp (ih₁ V) (ih₂ V);
+  | nec ih => intro V; exact KripkeModel.validates_nec (ih V);
+
+lemma valid_of_provable2' (K) (hK : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧* Ax)
+  : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧* (Hilbert.Normal2 Ax) := by
+  intro V;
+  constructor;
+  intro φ hφ;
+  apply valid_of_provable (K := K) hK $ Logic.iff_provable.mpr hφ;
+
+lemma consistent_of_valid_model' (K) (hK : ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧* Ax)
+  : Entailment.Consistent (Hilbert.Normal2 Ax) := by
+  apply Entailment.Consistent.of_unprovable (φ := ⊥);
+  by_contra! h;
+  apply KripkeModel.validates_falsum (M := ⟨K, λ _ _ => True⟩);
+  apply valid_of_provable K hK h;
+
+/-
+#check Semantics.Meaningful
+
+lemma consistent_of_valid_model'
+  (P : ∀ {κ : Type v}, [Nonempty κ] → Rel κ κ → Prop)
+  {κ : Type v} [Nonempty κ] (K : Rel κ κ) (hP : P K)
+  (S : ∀ φ, (Hilbert.Normal2 Ax) ⊢ φ → (∀ {κ : Type v}, [Nonempty κ] → ∀ K, P K → ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ))
+  : Entailment.Consistent (Hilbert.Normal2 Ax) := by
+  apply Entailment.Consistent.of_unprovable (φ := ⊥);
+  by_contra! h;
+  have := @S ⊥ h κ _ K hP (λ _ _ => True);
+  sorry;
+-/
+
+end Hilbert.Normal2
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Logic/K.lean b/Foundation/Modal/Kripke2/Logic/K.lean
new file mode 100644
index 000000000..8072a8b39
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Logic/K.lean
@@ -0,0 +1,50 @@
+module
+
+public import Foundation.Modal.Kripke2.Hilbert
+public import Foundation.Modal.Kripke2.Completeness
+
+@[expose] public section
+
+namespace LO.Modal
+
+variable {α : Type u} {φ : Formula α}
+
+namespace K
+
+theorem forall_frame_validates_of_provable (h : Modal.K' α ⊢ φ)
+  : ∀ {κ}, [Nonempty κ] → ∀ F, ∀ V, (⟨F, V⟩ : KripkeModel κ α) ⊧ φ := by
+  intro κ _ K;
+  apply Hilbert.Normal2.valid_of_provable K ?_ h;
+  rintro V;
+  constructor;
+  intro _ h;
+  rcases (by simpa [Hilbert.Normal2.buildAxioms] using h) with ⟨_, _, rfl⟩; grind;
+
+theorem forall_model_validates_of_provable (h : Modal.K' α ⊢ φ)
+  : ∀ {κ}, [Nonempty κ] → ∀ M : KripkeModel κ α, M ⊧ φ
+  := fun M ↦ forall_frame_validates_of_provable h M.frame M.val
+
+instance : Entailment.Consistent (Modal.K' α) := by
+  apply Entailment.Consistent.of_unprovable (φ := ⊥);
+  by_contra! hC;
+  apply KripkeModel.validates_falsum $
+    forall_frame_validates_of_provable hC (λ (_ : Fin 1) _ => True) (λ _ _ => True);
+
+instance : Entailment.K (Modal.K' α) where
+
+variable [DecidableEq α] [Encodable α]
+
+theorem provable_of_forall_model_validates : (∀ {κ : Type u}, [Nonempty κ] → ∀ M : KripkeModel κ α, M ⊧ φ) → Modal.K' _ ⊢ φ
+  := fun h ↦ canonicalKripkeModel.iff_valid_provable.mp $ h _
+
+theorem iff_provable_valid_all_kripkeModel : Modal.K' α ⊢ φ ↔ (∀ κ : Type u, [Nonempty κ] → ∀ M : KripkeModel κ α, M ⊧ φ) := by
+  constructor;
+  . exact forall_model_validates_of_provable;
+  . exact provable_of_forall_model_validates;
+
+end K
+
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Logic/K4.lean b/Foundation/Modal/Kripke2/Logic/K4.lean
new file mode 100644
index 000000000..57eeaeed1
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Logic/K4.lean
@@ -0,0 +1,62 @@
+module
+
+public import Foundation.Modal.Kripke2.Logic.K
+public import Foundation.Modal.Kripke2.Axiom.Geach
+
+@[expose] public section
+
+namespace LO.Modal
+
+variable {α : Type u} {κ : Type*} [Nonempty κ] {φ : Formula α}
+
+namespace K4'
+
+instance : Entailment.K4 (Modal.K4' α) where
+
+theorem forall_transitive_frame_validates_of_provable (h : Modal.K4' α ⊢ φ)
+  : ∀ {κ : Type*}, [Nonempty κ] → ∀ K, [IsTrans _ K] → ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ := by
+  intro κ _ F _;
+  apply Hilbert.Normal2.valid_of_provable F ?_ h;
+  rintro V;
+  constructor;
+  intro _ hφ;
+  rcases (by simpa [Hilbert.Normal2.buildAxioms] using hφ) with (⟨_, rfl⟩ | (⟨_, _, rfl⟩)) <;> grind;
+
+lemma forall_transitive_frame_validates_of_provable' (h : Modal.K4' α ⊢ φ)
+  : ∀ {κ : Type*}, [Nonempty κ] → ∀ K, (Transitive K) → ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ
+  := by
+  rintro _ _ F F_trans;
+  have : IsTrans _ F := by constructor; tauto;
+  exact forall_transitive_frame_validates_of_provable h F;
+
+theorem forall_transitive_model_validates_of_provable (h : Modal.K4' α ⊢ φ)
+  : ∀ {κ}, [Nonempty κ] → ∀ M : KripkeModel κ α, [IsTrans _ M.rel] → M ⊧ φ
+  := fun M ↦ forall_transitive_frame_validates_of_provable h M.frame M.val
+
+
+instance : Entailment.Consistent (Modal.K4' α) := by
+  apply Entailment.Consistent.of_unprovable (φ := ⊥);
+  by_contra! hC;
+  apply KripkeModel.validates_falsum $
+    forall_transitive_frame_validates_of_provable' hC (λ (_ : Fin 1) _ => True) (by tauto) (λ _ _ => True);
+
+variable [DecidableEq α] [Encodable α]
+
+theorem provable_of_forall_transitive_model_validate
+  (h : ∀ {κ : Type u}, [Nonempty κ] → ∀ M : KripkeModel κ α, [IsTrans _ M.rel] → M ⊧ φ)
+  : Modal.K4' α ⊢ φ
+  := canonicalKripkeModel.iff_valid_provable.mp $ h _
+
+theorem iff_provable_provable_forall_transitive_model_validate
+  : Modal.K4' α ⊢ φ ↔ (∀ {κ : Type u}, [Nonempty κ] → ∀ M : KripkeModel κ α, [IsTrans _ M.rel] → M ⊧ φ)
+  := by
+  constructor;
+  . apply forall_transitive_model_validates_of_provable;
+  . apply provable_of_forall_transitive_model_validate;
+
+end K4'
+
+
+end LO.Modal
+
+end
diff --git a/Foundation/Modal/Kripke2/Logic/KT.lean b/Foundation/Modal/Kripke2/Logic/KT.lean
new file mode 100644
index 000000000..7d34bbdbd
--- /dev/null
+++ b/Foundation/Modal/Kripke2/Logic/KT.lean
@@ -0,0 +1,62 @@
+module
+
+public import Foundation.Modal.Kripke2.Logic.K
+public import Foundation.Modal.Kripke2.Axiom.Geach
+
+@[expose] public section
+
+namespace LO.Modal
+
+variable {α : Type u} {φ : Formula α}
+
+namespace KT'
+
+instance : Entailment.KT (Modal.KT' α) where
+
+theorem forall_reflexive_frame_validates_of_provable (h : Modal.KT' α ⊢ φ)
+  : ∀ {κ : Type*}, [Nonempty κ] → ∀ K, [Std.Refl K] → ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ := by
+  intro κ _ F _;
+  apply Hilbert.Normal2.valid_of_provable F ?_ h;
+  rintro V;
+  constructor;
+  intro _ hφ;
+  rcases (by simpa [Hilbert.Normal2.buildAxioms] using hφ) with ((⟨_, _, rfl⟩ | ⟨_, rfl⟩)) <;> grind;
+
+lemma forall_reflexive_frame_validates_of_provable' (h : Modal.KT' α ⊢ φ)
+  : ∀ {κ : Type*}, [Nonempty κ] → ∀ K, (Reflexive K) → ∀ V, (⟨K, V⟩ : KripkeModel κ α) ⊧ φ
+  := by
+  rintro _ _ F F_reflexive;
+  have : Std.Refl F := by constructor; tauto;
+  exact forall_reflexive_frame_validates_of_provable h F;
+
+theorem forall_reflexive_model_validates_of_provable (h : Modal.KT' α ⊢ φ)
+  : ∀ {κ}, [Nonempty κ] → ∀ M : KripkeModel κ α, [Std.Refl M.rel] → M ⊧ φ
+  := fun M ↦ forall_reflexive_frame_validates_of_provable h M.frame M.val
+
+
+instance : Entailment.Consistent (Modal.KT' α) := by
+  apply Entailment.Consistent.of_unprovable (φ := ⊥);
+  by_contra! hC;
+  apply KripkeModel.validates_falsum $
+    forall_reflexive_frame_validates_of_provable' hC (λ (_ : Fin 1) _ => True) (by tauto) (λ _ _ => True);
+
+variable [DecidableEq α] [Encodable α]
+
+theorem provable_of_forall_reflexive_model_validate
+  (h : ∀ {κ : Type u}, [Nonempty κ] → ∀ M : KripkeModel κ α, [Std.Refl M.rel] → M ⊧ φ)
+  : Modal.KT' α ⊢ φ
+  := canonicalKripkeModel.iff_valid_provable.mp $ h _
+
+theorem iff_provable_provable_forall_reflexive_model_validate
+  : Modal.KT' α ⊢ φ ↔ (∀ {κ : Type u}, [Nonempty κ] → ∀ M : KripkeModel κ α, [Std.Refl M.rel] → M ⊧ φ)
+  := by
+  constructor;
+  . apply forall_reflexive_model_validates_of_provable;
+  . apply provable_of_forall_reflexive_model_validate;
+
+end KT'
+
+
+end LO.Modal
+
+end