diff --git a/Cslib.lean b/Cslib.lean
index 7db43680b..4ed8c757a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -129,4 +129,8 @@ public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
 public import Cslib.Logics.LinearLogic.CLL.MLL
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
+public import Cslib.Logics.Modal.Basic
+public import Cslib.Logics.Modal.Cube
+public import Cslib.Logics.Modal.Denotation
+public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 743e2f22d..256540b9e 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -69,6 +69,10 @@ theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by
 /-- The relation `r` 'up to' the relation `s`. -/
 def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s)
 
+/-- A relation `r` is (right) Euclidean if `r a b` and `r a c` guarantee `r b c`. -/
+class RightEuclidean (r : α → α → Prop) where
+  rightEuclidean : r a b → r a c → r b c
+
 /-- A relation has the diamond property when all reductions with a common origin are joinable -/
 abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → Join r b c
 
@@ -148,6 +152,16 @@ theorem Confluent_of_unique_end {x : α} (h : ∀ y : α, ReflTransGen r y x) :
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/
 abbrev Reducible (r : α → α → Prop) (x : α) : Prop := ∃ y, r x y
 
+/-- A relation `r` is serial if every element is `Reducible`. -/
+class Serial (r : α → α → Prop) where
+  serial a : Reducible r a
+
+@[scoped grind →]
+lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r where
+  serial a := ⟨a, h.refl a⟩
+
+instance [instRefl : Std.Refl r] : Relation.Serial r := refl_serial r instRefl
+
 /-- An element is normal if it is not reducible. -/
 abbrev Normal (r : α → α → Prop) (x : α) : Prop := ¬ Reducible r x
 
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
new file mode 100644
index 000000000..f0ee38c8e
--- /dev/null
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -0,0 +1,295 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Marianna Girlando
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Mathlib.Data.Set.Basic
+public import Mathlib.Order.Defs.Unbundled
+public import Cslib.Foundations.Data.Relation
+public import Mathlib.Logic.Nonempty
+
+/-! # Modal Logic
+
+Modal logic is a logic for reasoning about relational structures, studying statements about
+necessity (`□φ`) and possibility `⋄φ`.
+
+## References
+
+* [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001]
+* The definitions of theory equivalence and the denotational semantics of worlds are inspired by
+  the development of `Cslib.Logic.HML`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+/-- A model consists of a relation between worlds `r` and a valuation `v`. -/
+structure Model (World : Type*) (Atom : Type*) where
+  /-- World accessibility relation. -/
+  r : World → World → Prop
+  /-- Valuation of atoms at a world. -/
+  v : World → Atom → Prop
+
+/-- Propositions. -/
+inductive Proposition (Atom : Type u) : Type u where
+  /-- Atomic proposition. -/
+  | atom (p : Atom)
+  /-- Negation. -/
+  | not (φ : Proposition Atom)
+  /-- Conjunction. -/
+  | and (φ₁ φ₂ : Proposition Atom)
+  /-- Possibility. -/
+  | diamond (φ : Proposition Atom)
+
+@[inherit_doc] scoped prefix:40 "¬" => Proposition.not
+@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
+@[inherit_doc] scoped prefix:40 "⋄" => Proposition.diamond
+
+/-- Disjunction. -/
+def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂)
+
+@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
+
+/-- Implication. -/
+def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
+
+@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+
+/-- Bi-implication. -/
+def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
+
+@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff
+
+/-- Necessity. -/
+def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬⋄¬φ
+
+@[inherit_doc] scoped prefix:40 "□" => Proposition.box
+
+/-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies
+the proposition `φ`. -/
+@[scoped grind]
+def Satisfies (m : Model World Atom) (w : World) : Proposition Atom → Prop
+  | .atom p => m.v w p
+  | .not φ => ¬Satisfies m w φ
+  | .and φ₁ φ₂ => Satisfies m w φ₁ ∧ Satisfies m w φ₂
+  | .diamond φ => ∃ w', m.r w w' ∧ Satisfies m w' φ
+
+/-- Judgement, representing the conclusions one reaches in modal logic. -/
+structure Judgement World Atom where
+  /-- Constructs a judgement. -/
+  mk ::
+  /-- Model. -/
+  m : Model World Atom
+  /-- The world satisfying the proposition `φ`. -/
+  w : World
+  /-- The proposition satisfied by the world `w`. -/
+  φ : Proposition Atom
+
+@[inherit_doc] scoped notation "Modal[" m "," w " ⊨ " φ "]" => Judgement.mk m w φ
+
+/-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/
+@[simp, scoped grind =]
+def Satisfies.Bundled (j : Judgement World Atom) : Prop := Satisfies j.m j.w j.φ
+
+instance : HasInferenceSystem (Judgement World Atom) := ⟨Satisfies.Bundled⟩
+
+open scoped InferenceSystem Proposition
+
+@[scoped grind =]
+theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} :
+  ⇓Modal[m,w ⊨ φ] = Satisfies m w φ := rfl
+
+/-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
+@[scoped grind =]
+theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
+  induction φ generalizing w <;> grind
+
+/-- Characterisation of the `∨` connective.
+
+Disjunction is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct. -/
+@[scoped grind =]
+theorem Satisfies.or_iff_or {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or]
+
+/-- Characterisation of the `→` connective.
+
+Implication is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct.
+-/
+@[scoped grind =]
+theorem Satisfies.impl_iff_impl {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl]
+
+/-- Characterisation of the `↔` connective.
+
+Bi-implication is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct. -/
+@[scoped grind =]
+theorem Satisfies.iff_iff_iff {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
+  simp only [Proposition.iff]
+  grind [=_ derivation_def]
+
+/-- Characterisation of the `□` modality.
+
+Necessity is defined in terms of the more primitive connectives given in `Proposition`.
+This result proves that the definition is correct. -/
+@[scoped grind =]
+theorem Satisfies.box_iff_forall {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box]
+
+/-- The theory of a world in a model is the set of all propositions that it satifies. -/
+abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
+  {φ | ⇓Modal[m,w ⊨ φ]}
+
+/-- Two worlds are theory-equivalent under a model if they have the same theory. -/
+abbrev TheoryEq (m : Model World Atom) (w₁ w₂ : World) :=
+  theory m w₁ = theory m w₂
+
+/-- Any proposition satisfied by a world is in the theory of that world. -/
+@[scoped grind →]
+theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := by grind
+
+/-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/
+lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) :
+    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ not_satisfies]
+
+/-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as
+well. -/
+theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
+    (hs : Satisfies m w₁ φ) : ⇓Modal[m,w₂ ⊨ φ] := by
+  unfold TheoryEq theory at h
+  rw [Set.ext_iff] at h
+  exact (h φ).mp hs
+
+/-- The K axiom, valid for all models. -/
+theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
+
+/-- The dual axiom, valid for all models. -/
+theorem Satisfies.dual : ⇓Modal[m,w ⊨ ⋄φ ↔ ¬□¬φ] := by
+  constructor <;> grind
+
+/-- The T axiom, valid for all reflexive models. -/
+theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → ⋄φ] := by grind [instRefl.refl w]
+
+/-- Any model that admits the axiom T is reflexive. -/
+theorem Satisfies.t_refl
+    {r : World → World → Prop}
+    [instAtomNonempty : Nonempty Atom]
+    (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
+      ⇓Modal[⟨r, v⟩,w ⊨ φ → ⋄φ]) :
+    Std.Refl r where
+  refl := by
+    intro w
+    have a := Classical.arbitrary Atom
+    let v := fun (w' : World) (a : Atom) => w' = w
+    let h' := h (v := v) (w := w) (φ := .atom a)
+    grind
+
+/-- In any reflexive model, `□φ → φ` is equivalent to `φ → ⋄φ`. -/
+theorem Satisfies.t_box_diamond [instRefl : Std.Refl m.r] :
+    ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ⋄φ] := by
+  grind [instRefl.refl]
+
+/-- The B axiom, valid for all symmetric models. -/
+theorem Satisfies.b {m : Model World Atom} [instSymm : Std.Symm m.r] {w : World}
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → □⋄φ] := by
+  grind [instSymm.symm w]
+
+/-- Any model that admits the axiom B is symmetric. -/
+theorem Satisfies.b_symm
+    {r : World → World → Prop}
+    [instAtomNonempty : Nonempty Atom]
+    (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
+      ⇓Modal[⟨r, v⟩,w ⊨ φ → □⋄φ]) :
+    Std.Symm r where
+  symm := by
+    intro w₁
+    have a := Classical.arbitrary Atom
+    let v₁ := fun (w' : World) (a : Atom) => w' = w₁
+    let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
+    grind
+
+/-- The 4 axiom, valid for all transitive models. -/
+theorem Satisfies.four {m : Model World Atom} [instTrans : IsTrans World m.r] {w : World}
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ⋄⋄φ → ⋄φ] := by
+  simp only [impl_iff_impl]
+  intro h
+  rcases h with ⟨w', h₁, w'', h₂, hs⟩
+  exists w''
+  grind [IsTrans]
+
+/-- Any model that admits 4 is transitive. -/
+theorem Satisfies.four_trans
+    {r : World → World → Prop}
+    [instAtomNonempty : Nonempty Atom]
+    (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
+      ⇓Modal[⟨r, v⟩,w ⊨ ⋄⋄φ → ⋄φ]) :
+    IsTrans World r where
+  trans := by
+    intro w₁ w₂ w₃ h₁ h₂
+    have a := Classical.arbitrary Atom
+    let v := fun (w' : World) (a : Atom) => w' = w₃
+    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    grind
+
+/-- The 5 axiom, valid for all Euclidean models. -/
+theorem Satisfies.five {m : Model World Atom} [instRightEuclidean : Relation.RightEuclidean m.r]
+    {w : World}
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ⋄φ → □⋄φ] := by grind [Relation.RightEuclidean]
+
+/-- Any model that admits 5 is Euclidean. -/
+theorem Satisfies.five_rightEuclidean
+    {r : World → World → Prop}
+    [instAtomNonempty : Nonempty Atom]
+    (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
+      ⇓Modal[⟨r, v⟩,w ⊨ ⋄φ → □⋄φ]) :
+    Relation.RightEuclidean r where
+  rightEuclidean := by
+    intro w₁ w₂ w₃ h₁ h₂
+    have a := Classical.arbitrary Atom
+    let v := fun (w' : World) (a : Atom) => w' = w₃
+    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    grind
+
+/-- The D axiom, valid for all serial models. -/
+theorem Satisfies.d {m : Model World Atom} [instSerial : Relation.Serial m.r]
+    {w : World}
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ □φ → ⋄φ] := by
+  have : ∃ w', m.r w w' := instSerial.serial w
+  grind
+
+/-- Any model that admits D is serial. -/
+theorem Satisfies.d_serial
+    {r : World → World → Prop}
+    [instAtomNonempty : Nonempty Atom]
+    (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
+      ⇓Modal[⟨r, v⟩,w ⊨ □φ → ⋄φ]) :
+    Relation.Serial r where
+  serial := by
+    intro w₁
+    have a := Classical.arbitrary Atom
+    let v := fun (w' : World) (a : Atom) => w' = w₁
+    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    grind
+
+/-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under
+all models in `S` for all worlds. -/
+@[simp, scoped grind =]
+def Proposition.valid (S : Set (Model World Atom)) (φ : Proposition Atom) : Prop :=
+  ∀ (m : Model World Atom), ∀ (_ : m ∈ S), ∀ (w : World), ⇓Modal[m,w ⊨ φ]
+
+/-- The modal logic of a class of models `S` is the set of all propositions valid in `S`. -/
+@[simp, scoped grind =]
+def logic (S : Set (Model World Atom)) : Set (Proposition Atom) :=
+  {φ | φ.valid S}
+
+end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
new file mode 100644
index 000000000..19798d53d
--- /dev/null
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Marianna Girlando
+-/
+
+module
+
+public import Cslib.Logics.Modal.Basic
+
+/-! # Modal Logic Cube
+
+This module formalises the Modal Cube, including all the 15 foundational modal logics and their
+relationships.
+
+## References
+
+* [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001]
+
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+/-- The modal logic K. -/
+@[simp, scoped grind =]
+def K World Atom := logic (Set.univ (α := Model World Atom))
+
+/-- The modal logic T. -/
+@[simp, scoped grind =]
+def T World Atom := logic {m : Model World Atom | Std.Refl m.r}
+
+/-- The modal logic B. -/
+@[simp, scoped grind =]
+def B World Atom := logic {m : Model World Atom | Std.Symm m.r}
+
+/-- The modal logic 4. -/
+@[simp, scoped grind =]
+def Four World Atom := logic {m : Model World Atom | IsTrans World m.r}
+
+/-- The modal logic 5. -/
+@[simp, scoped grind =]
+def Five World Atom := logic {m : Model World Atom | Relation.RightEuclidean m.r}
+
+/-- The modal logic K45. -/
+@[simp, scoped grind =]
+def K45 World Atom := (K World Atom) ⊔ (Four World Atom) ⊔ (Five World Atom)
+
+/-- The modal logic D. -/
+@[simp, scoped grind =]
+def D World Atom := logic {m : Model World Atom | Relation.Serial m.r}
+
+/-- The modal logic D4. -/
+@[simp, scoped grind =]
+def D4 World Atom := (K World Atom) ⊔ (D World Atom) ⊔ (Four World Atom)
+
+/-- The modal logic D5. -/
+@[simp, scoped grind =]
+def D5 World Atom := (K World Atom) ⊔ (D World Atom) ⊔ (Five World Atom)
+
+/-- The modal logic D45. -/
+@[simp, scoped grind =]
+def D45 World Atom := (K World Atom) ⊔ (D World Atom) ⊔ (Four World Atom) ⊔ (Five World Atom)
+
+/-- The modal logic DB. -/
+@[simp, scoped grind =]
+def DB World Atom := (K World Atom) ⊔ (D World Atom) ⊔ (B World Atom)
+
+/-- The modal logic TB. -/
+@[simp, scoped grind =]
+def TB World Atom := (K World Atom) ⊔ (T World Atom) ⊔ (B World Atom)
+
+/-- The modal logic KB5. -/
+@[simp, scoped grind =]
+def KB5 World Atom := (K World Atom) ⊔ (B World Atom) ⊔ (Five World Atom)
+
+/-- The modal logic S4. -/
+@[simp, scoped grind =]
+def S4 World Atom := (K World Atom) ⊔ (T World Atom) ⊔ (Four World Atom)
+
+/-- The modal logic S5. -/
+@[simp, scoped grind =]
+def S5 World Atom := (K World Atom) ⊔ (T World Atom) ⊔ (Four World Atom) ⊔ (Five World Atom)
+
+section Order
+
+/-! ## Ordering of Modal Logics
+
+This section proves the essential inclusions of modal logics.
+
+The other inclusions in the Modal Cube can be derived from the properties of `≤` and `⊔`, as shown
+in `k_leq_t`.
+-/
+
+open scoped Proposition
+
+theorem k_leq_d : (K World Atom ≤ D World Atom) := by
+  intro φ; grind
+
+theorem k_leq_b : (K World Atom ≤ B World Atom) := by
+  intro φ; grind
+
+theorem k_leq_four : (K World Atom ≤ Four World Atom) := by
+  intro φ; grind
+
+theorem k_leq_five : (K World Atom ≤ Five World Atom) := by
+  intro φ; grind
+
+open scoped Relation in
+theorem d_leq_t : (D World Atom ≤ T World Atom) := by
+  intro φ; grind
+
+theorem k_leq_t : (K World Atom ≤ T World Atom) := by
+  calc
+    K World Atom ≤ D World Atom := k_leq_d
+    D World Atom ≤ T World Atom := d_leq_t
+
+end Order
+
+section Validity
+
+/-! ## Validity
+
+This section showcases how to prove the expected validities in the different modal logics.
+-/
+
+/-- The axiom K is valid in the logic K. -/
+theorem K.k_valid : (□(φ₁ → φ₂) → (□φ₁ → □φ₂) : Proposition Atom) ∈ K World Atom := by
+  open scoped Proposition in grind [Satisfies.k]
+
+/-- The axiom T is valid in the logic T. -/
+theorem T.t_valid : (φ → ⋄φ : Proposition Atom) ∈ T World Atom := by
+  intro _ h
+  grind [Satisfies.t (instRefl := (by assumption))]
+
+end Validity
+
+end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
new file mode 100644
index 000000000..93acca7dd
--- /dev/null
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Logics.Modal.Basic
+
+/-! # Denotational semantics for Modal Logic
+
+A denotational semantics for modal logic, inspired by the one for Hennessy-Milner Logic
+(`Cslib.Logic.HML`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+open scoped Proposition InferenceSystem
+
+/-- Denotation of a proposition. -/
+@[simp, scoped grind =]
+def Proposition.denotation (m : Model World Atom) :
+    Proposition Atom → Set World
+  | .atom p => {w | m.v w p}
+  | .not φ => (φ.denotation m)ᶜ
+  | .and φ₁ φ₂ => φ₁.denotation m ∩ φ₂.denotation m
+  | .diamond φ => {w | ∃ w', m.r w w' ∧ w' ∈ φ.denotation m}
+
+/-- Characterisation theorem for the denotational semantics. -/
+@[scoped grind =]
+theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} :
+    w ∈ φ.denotation m ↔ ⇓Modal[m,w ⊨ φ] := by
+  induction φ generalizing w <;> grind
+
+/-- A world is in the denotation of a proposition iff it is not in the denotation of the negation
+of the proposition. -/
+@[scoped grind =]
+theorem neg_denotation {m : Model World Atom} (φ : Proposition Atom) :
+    w ∉ (¬φ).denotation m ↔ w ∈ φ.denotation m := by
+  grind [_=_ satisfies_mem_denotation]
+
+/-- Two worlds are theory-equivalent iff they are denotationally equivalent. -/
+theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} :
+    (TheoryEq m w₁ w₂) ↔
+    (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by
+  apply Iff.intro <;> grind [_=_ satisfies_mem_denotation]
+
+end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
new file mode 100644
index 000000000..621dbb046
--- /dev/null
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Logics.Modal.Basic
+public import Cslib.Foundations.Logic.LogicalEquivalence
+
+/-! # Logical Equivalence in Modal Logic
+
+This module defines logical equivalence for modal propositions.
+The definitions are parametric on the class of models under consideration.
+
+We also instantiate `LogicalEquivalence` for Modal Logic K, i.e., equivalence
+for the class of all models.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+open scoped InferenceSystem Proposition Satisfies
+
+/-- The modal propositions `φ₁` and `φ₂` are equivalent in the class of models `S`. -/
+def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
+    : Prop :=
+  ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]
+
+@[inherit_doc]
+scoped notation φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂
+
+@[inherit_doc]
+scoped notation φ₁ " ≡ " φ₂ => Proposition.Equiv Set.univ φ₁ φ₂
+
+@[scoped grind =]
+theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
+    (φ₁ ≡[S] φ₂) ↔
+    (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) := by rfl
+
+theorem Proposition.equiv_valid (S : Set (Model World Atom))
+    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[S] φ₂) :
+    (φ₁.valid S ↔ φ₂.valid S) := by
+  apply Iff.intro <;> intro h'
+  · simp_all only [valid]
+    intro m hin w
+    specialize h m hin w
+    grind
+  · simp_all only [valid]
+    intro m hin w
+    specialize h m hin w
+    grind
+
+/-- Propositional contexts. -/
+inductive Proposition.Context (Atom : Type u) : Type u where
+  | hole
+  | not (c : Context Atom)
+  | andL (c : Context Atom) (φ : Proposition Atom)
+  | andR (φ : Proposition Atom) (c : Context Atom)
+  | diamond (c : Context Atom)
+
+/-- Replaces a hole in a propositional context with a proposition. -/
+@[scoped grind =]
+def Proposition.Context.fill (c : Context Atom) (φ : Proposition Atom) :=
+  match c with
+  | hole => φ
+  | not c => .not (c.fill φ)
+  | andL c φ' => (c.fill φ).and φ'
+  | andR φ' c => φ'.and (c.fill φ)
+  | diamond c => .diamond (c.fill φ)
+
+instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩
+
+open scoped Proposition Proposition.Context
+
+/-- Logical equivalence is an equivalence relation. -/
+instance (S : Set (Model World Atom)) :
+    IsEquiv (Proposition Atom) (Proposition.Equiv (Atom := Atom) S) where
+  refl := by grind
+  symm := by
+    intro φ₁ φ₂ h m hₘ w
+    specialize h m hₘ w
+    grind
+  trans := by
+    intro φ₁ φ₂ φ₃ h₁ h₂ m hₘ w
+    specialize h₁ m hₘ w
+    specialize h₂ m hₘ w
+    grind
+
+/-- Logical equivalence is a congruence. -/
+instance (S : Set (Model World Atom)) :
+    Congruence (Proposition Atom) (Proposition.Equiv (Atom := Atom) S) where
+  elim :
+      Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill)
+      (Proposition.Equiv S) := by
+    intro ctx φ₁ φ₂ heqv m hₘ w
+    specialize heqv m hₘ
+    induction ctx generalizing w
+    case hole => grind
+    case not c ih | andL c ih | andR c ih =>
+      specialize ih w
+      grind
+    case diamond c ih =>
+      simp only [Satisfies.iff_iff_iff]
+      apply Iff.intro
+      all_goals
+        intro h
+        rcases h with ⟨w', h⟩
+        specialize ih w'
+        grind
+
+/-- Judgemental contexts. -/
+structure Satisfies.Context (World Atom : Type*) where
+  /-- The model to consider. -/
+  m : Model World Atom
+  /-- The world to check propositions against. -/
+  w : World
+
+/-- Fills a judgemental context with a proposition. -/
+def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) :
+    Judgement World Atom where
+  m := c.m
+  w := c.w
+  φ := φ
+
+instance judgementalContext :
+    HasHContext (Judgement World Atom) (Proposition Atom) :=
+  ⟨Satisfies.Context World Atom, Satisfies.Context.fill⟩
+
+/-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
+instance : LogicalEquivalence
+    (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where
+  eqv := Proposition.Equiv Set.univ
+  eqv_fill_valid {φ₁ φ₂ : Proposition Atom} (heqv : φ₁ ≡[Set.univ] φ₂)
+      (c : HasHContext.Context (Judgement World Atom) (Proposition Atom))
+      (h : ⇓c<[φ₁]) : ⇓c<[φ₂] := by
+    simp only [HasHContext.fill, Satisfies.Context.fill] at ⊢ h
+    specialize heqv c.m
+    grind
+
+end Cslib.Logic.Modal
diff --git a/references.bib b/references.bib
index 1f8c0dc51..afa0213e9 100644
--- a/references.bib
+++ b/references.bib
@@ -28,6 +28,16 @@ @book{Baader1998
 address = {USA}
 }
 
+@book{Blackburn2001,
+  place={Cambridge},
+  series={Cambridge Tracts in Theoretical Computer Science},
+  title={Modal Logic},
+  publisher={Cambridge University Press},
+  author={Blackburn, Patrick and Rijke, Maarten de and Venema, Yde},
+  year={2001},
+  collection={Cambridge Tracts in Theoretical Computer Science}
+}
+
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},