diff --git a/Cslib.lean b/Cslib.lean
index 070e6dc0f..5c87186d8 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -136,6 +136,7 @@ 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
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
 public import Cslib.MachineLearning.PACLearning.Defs
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index a62792367..aa9582014 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -41,13 +41,13 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Atomic proposition. -/
   | atom (p : Atom)
   /-- Negation. -/
-  | neg (φ : Proposition Atom)
+  | not (φ : Proposition Atom)
   /-- Conjunction. -/
   | and (φ₁ φ₂ : Proposition Atom)
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
-@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg
+@[inherit_doc] scoped prefix:40 "¬" => Proposition.not
 @[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
 @[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond
 
@@ -76,7 +76,7 @@ the proposition `φ`. -/
 @[scoped grind]
 def Satisfies (m : Model World Atom) (w : World) : Proposition Atom → Prop
   | .atom p => m.v w p
-  | .neg φ => ¬Satisfies m w φ
+  | .not φ => ¬Satisfies m w φ
   | .and φ₁ φ₂ => Satisfies m w φ₁ ∧ Satisfies m w φ₂
   | .diamond φ => ∃ w', m.r w w' ∧ Satisfies m w' φ
 
@@ -107,7 +107,7 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom
 
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
-theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
+theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
   induction φ generalizing w <;> grind
 
 /-- Characterisation of the `∨` connective.
@@ -127,6 +127,16 @@ This result proves that the definition is correct.
 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`.
@@ -152,7 +162,7 @@ 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 [=_ neg_satisfies]
+    ∃ φ, (⇓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. -/
@@ -167,10 +177,8 @@ theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → 
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The dual axiom, valid for all models. -/
 theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
-  constructor
-  · grind
-  · grind only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def,
-    = neg_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
+  grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl,
+    = derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 63e88000e..b74e8f3f1 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -25,7 +25,7 @@ open scoped Proposition InferenceSystem
 def Proposition.denotation (m : Model World Atom) :
     Proposition Atom → Set World
   | .atom p => {w | m.v w p}
-  | .neg φ => (φ.denotation m)ᶜ
+  | .not φ => (φ.denotation m)ᶜ
   | .and φ₁ φ₂ => φ₁.denotation m ∩ φ₂.denotation m
   | .diamond φ => {w | ∃ w', m.r w w' ∧ w' ∈ φ.denotation m}
 
@@ -38,7 +38,7 @@ theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom}
 /-- 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) :
+theorem not_denotation {m : Model World Atom} (φ : Proposition Atom) :
     w ∉ (¬φ).denotation m ↔ w ∈ φ.denotation m := by
   grind [_=_ satisfies_mem_denotation]
 
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
new file mode 100644
index 000000000..88a4b0110
--- /dev/null
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -0,0 +1,149 @@
+/-
+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
+
+@[scoped grind =]
+theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
+    (φ₁ ≡[S] φ₂) ↔
+    (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
+  simp [Proposition.equiv_def, Satisfies.iff_iff_iff]
+
+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
+  eqvFillValid {φ₁ φ₂ : 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