From 79f99facf8227619c1f4c750e3fd9a15da7742dc Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 13:42:48 +0200
Subject: [PATCH 1/9] Modal Logic

---
 Cslib.lean                           |   3 +
 Cslib/Foundations/Data/Relation.lean |  16 ++
 Cslib/Logics/Modal/Basic.lean        | 284 +++++++++++++++++++++++++++
 Cslib/Logics/Modal/Cube.lean         | 138 +++++++++++++
 Cslib/Logics/Modal/Denotation.lean   |  51 +++++
 references.bib                       |  10 +
 6 files changed, 502 insertions(+)
 create mode 100644 Cslib/Logics/Modal/Basic.lean
 create mode 100644 Cslib/Logics/Modal/Cube.lean
 create mode 100644 Cslib/Logics/Modal/Denotation.lean

diff --git a/Cslib.lean b/Cslib.lean
index 7db43680b..e5fa4fb51 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -129,4 +129,7 @@ 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.Propositional.Defs
diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 743e2f22d..26ba3dc8a 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -69,6 +69,22 @@ 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 `r` is serial if every element is related to some element. -/
+class Serial (r : α → α → Prop) where
+  serial : ∀ a, ∃ b, r a b
+
+@[scoped grind →]
+lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r := by
+  constructor
+  intro a
+  obtain ⟨h⟩ := h
+  exists a
+  exact h a
+
 /-- 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
 
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
new file mode 100644
index 000000000..3a4ccff4b
--- /dev/null
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -0,0 +1,284 @@
+/-
+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
+
+/-! # 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. -/
+  | neg (φ : Proposition Atom)
+  /-- Conjunction. -/
+  | and (φ₁ φ₂ : Proposition Atom)
+  /-- Possibility. -/
+  | diamond (φ : Proposition Atom)
+
+@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg
+@[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. -/
+@[simp, scoped grind =]
+def Proposition.biImpl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
+
+@[inherit_doc] scoped infix:30 " ↔ " => Proposition.biImpl
+
+/-- 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
+  | .neg φ => ¬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 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} :
+  ⇓(m,w ⊨ φ) = Satisfies m w φ := rfl
+
+/-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
+@[scoped grind =]
+theorem neg_satisfies : ⇓(m,w ⊨ ¬φ) ↔ ¬⇓(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_char {m : Model World Atom} :
+    ⇓(m,w ⊨ φ₁ ∨ φ₂) ↔ ⇓(m,w ⊨ φ₁) ∨ ⇓(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_char {m : Model World Atom} :
+    ⇓(m,w ⊨ φ₁ → φ₂) ↔ (⇓(m,w ⊨ φ₁) → ⇓(m,w ⊨ φ₂)) := by grind [Proposition.impl]
+
+/-- 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_char {m : Model World Atom} :
+    ⇓(m,w ⊨ □φ) ↔ ∀ w', m.r w w' → ⇓(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) :=
+  {φ | ⇓(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₂) :
+    ∃ φ, (⇓(m,w₁ ⊨ φ) ∧ ¬⇓(m,w₂ ⊨ φ)) := by grind [=_ neg_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₁ φ) : ⇓(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 : ⇓(m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind
+
+/-- The dual axiom, valid for all models. -/
+theorem Satisfies.dual : ⇓(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) : ⇓(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},
+      ⇓((Model.mk r v),w ⊨ φ → ⋄φ)) :
+    Std.Refl r where
+  refl := by
+    intro w
+    rcases instAtomNonempty with ⟨a⟩
+    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] : ⇓(m,w ⊨ □φ → φ) ↔ ⇓(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) : ⇓(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},
+      ⇓(Model.mk r v,w ⊨ φ → □⋄φ)) :
+    Std.Symm r where
+  symm := by
+    intro w₁
+    rcases instAtomNonempty with ⟨a⟩
+    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) : ⇓(m,w ⊨ ⋄⋄φ → ⋄φ) := by
+  simp only [impl_char]
+  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},
+      ⇓(Model.mk r v,w ⊨ ⋄⋄φ → ⋄φ)) :
+    IsTrans World r where
+  trans := by
+    intro w₁ w₂ w₃ h₁ h₂
+    rcases instAtomNonempty with ⟨a⟩
+    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) : ⇓(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},
+      ⇓(Model.mk r v,w ⊨ ⋄φ → □⋄φ)) :
+    Relation.RightEuclidean r where
+  rightEuclidean := by
+    intro w₁ w₂ w₃ h₁ h₂
+    rcases instAtomNonempty with ⟨a⟩
+    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) : ⇓(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},
+      ⇓(Model.mk r v,w ⊨ □φ → ⋄φ)) :
+    Relation.Serial r where
+  serial := by
+    intro w₁
+    rcases instAtomNonempty with ⟨a⟩
+    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), ⇓(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..96c047a23
--- /dev/null
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -0,0 +1,138 @@
+/-
+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
+
+theorem d_leq_t : (D World Atom ≤ T World Atom) := by
+  intro φ; grind [Relation.refl_serial]
+
+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..ec860c16c
--- /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}
+  | .neg φ => (φ.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 ↔ ⇓(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/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},

From c738be6f50800afc45741cf72b381e7b67657dda Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 18:01:22 +0200
Subject: [PATCH 2/9] Update Cslib/Foundations/Data/Relation.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Foundations/Data/Relation.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 26ba3dc8a..de2019224 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -73,9 +73,9 @@ def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s)
 class RightEuclidean (r : α → α → Prop) where
   rightEuclidean : r a b → r a c → r b c
 
-/-- A relation `r` is serial if every element is related to some element. -/
+/-- A relation `r` is serial if every element is `Reducible`. -/
 class Serial (r : α → α → Prop) where
-  serial : ∀ a, ∃ b, r a b
+  serial a : Reducible r a
 
 @[scoped grind →]
 lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r := by

From a143c5b2a504adf6e6fcbd7889af0b3949708cc1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 18:01:49 +0200
Subject: [PATCH 3/9] Update Cslib/Foundations/Data/Relation.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 Cslib/Foundations/Data/Relation.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index de2019224..1b818a90d 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -77,13 +77,8 @@ class RightEuclidean (r : α → α → Prop) where
 class Serial (r : α → α → Prop) where
   serial a : Reducible r a
 
-@[scoped grind →]
-lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r := by
-  constructor
-  intro a
-  obtain ⟨h⟩ := h
-  exists a
-  exact h a
+instance [Std.Refl r] : Relation.Serial r where
+  serial a := ⟨a, Std.Refl.refl a⟩
 
 /-- 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

From a8adb15b40376a25ef9c85475e8b8d3b6a12bff8 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 18:09:37 +0200
Subject: [PATCH 4/9] reducible fix

---
 Cslib/Foundations/Data/Relation.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 1b818a90d..946dc650b 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -73,13 +73,6 @@ def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s)
 class RightEuclidean (r : α → α → Prop) where
   rightEuclidean : r a b → r a c → r b c
 
-/-- A relation `r` is serial if every element is `Reducible`. -/
-class Serial (r : α → α → Prop) where
-  serial a : Reducible r a
-
-instance [Std.Refl r] : Relation.Serial r where
-  serial a := ⟨a, Std.Refl.refl a⟩
-
 /-- 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
 
@@ -159,6 +152,13 @@ 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
+
+instance [Std.Refl r] : Relation.Serial r where
+  serial a := ⟨a, Std.Refl.refl a⟩
+
 /-- An element is normal if it is not reducible. -/
 abbrev Normal (r : α → α → Prop) (x : α) : Prop := ¬ Reducible r x
 

From ebc723ca1c2494c9c19a941cc4f725906bb20998 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 18:26:33 +0200
Subject: [PATCH 5/9] Classical.arbitrary

---
 Cslib/Logics/Modal/Basic.lean | 11 ++++++-----
 Cslib/Logics/Modal/Cube.lean  |  2 +-
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 3a4ccff4b..4bf1fbd35 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -11,6 +11,7 @@ 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
 
@@ -179,7 +180,7 @@ theorem Satisfies.t_refl
     Std.Refl r where
   refl := by
     intro w
-    rcases instAtomNonempty with ⟨a⟩
+    have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w
     let h' := h (v := v) (w := w) (φ := .atom a)
     grind
@@ -202,7 +203,7 @@ theorem Satisfies.b_symm
     Std.Symm r where
   symm := by
     intro w₁
-    rcases instAtomNonempty with ⟨a⟩
+    have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
     let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
     grind
@@ -225,7 +226,7 @@ theorem Satisfies.four_trans
     IsTrans World r where
   trans := by
     intro w₁ w₂ w₃ h₁ h₂
-    rcases instAtomNonempty with ⟨a⟩
+    have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := .atom a)
     grind
@@ -244,7 +245,7 @@ theorem Satisfies.five_rightEuclidean
     Relation.RightEuclidean r where
   rightEuclidean := by
     intro w₁ w₂ w₃ h₁ h₂
-    rcases instAtomNonempty with ⟨a⟩
+    have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := .atom a)
     grind
@@ -265,7 +266,7 @@ theorem Satisfies.d_serial
     Relation.Serial r where
   serial := by
     intro w₁
-    rcases instAtomNonempty with ⟨a⟩
+    have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₁
     let h' := h (v := v) (w := w₁) (φ := .atom a)
     grind
diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 96c047a23..235af846e 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -108,7 +108,7 @@ theorem k_leq_five : (K World Atom ≤ Five World Atom) := by
   intro φ; grind
 
 theorem d_leq_t : (D World Atom ≤ T World Atom) := by
-  intro φ; grind [Relation.refl_serial]
+  intro φ; grind [Relation.instSerialOfRefl]
 
 theorem k_leq_t : (K World Atom ≤ T World Atom) := by
   calc

From 0475e2fab9dbf1b47d1071eb3558a31cb16b7b42 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 18:33:45 +0200
Subject: [PATCH 6/9] fix refl_serial

---
 Cslib/Foundations/Data/Relation.lean | 7 +++++--
 Cslib/Logics/Modal/Cube.lean         | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 946dc650b..256540b9e 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -156,8 +156,11 @@ abbrev Reducible (r : α → α → Prop) (x : α) : Prop := ∃ y, r x y
 class Serial (r : α → α → Prop) where
   serial a : Reducible r a
 
-instance [Std.Refl r] : Relation.Serial r where
-  serial a := ⟨a, Std.Refl.refl 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/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 235af846e..96c047a23 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -108,7 +108,7 @@ theorem k_leq_five : (K World Atom ≤ Five World Atom) := by
   intro φ; grind
 
 theorem d_leq_t : (D World Atom ≤ T World Atom) := by
-  intro φ; grind [Relation.instSerialOfRefl]
+  intro φ; grind [Relation.refl_serial]
 
 theorem k_leq_t : (K World Atom ≤ T World Atom) := by
   calc

From b80b8ef87fb7c49fac4360ec23a8b08270378fed Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 29 Apr 2026 20:22:58 +0200
Subject: [PATCH 7/9] Modal notation

---
 Cslib/Logics/Modal/Basic.lean      | 52 +++++++++++++++---------------
 Cslib/Logics/Modal/Denotation.lean |  2 +-
 2 files changed, 27 insertions(+), 27 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 4bf1fbd35..c7dde115b 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -62,10 +62,9 @@ def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ
 @[inherit_doc] scoped infix:30 " → " => Proposition.impl
 
 /-- Bi-implication. -/
-@[simp, scoped grind =]
-def Proposition.biImpl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
+def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
 
-@[inherit_doc] scoped infix:30 " ↔ " => Proposition.biImpl
+@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff
 
 /-- Necessity. -/
 def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬⋄¬φ
@@ -92,7 +91,7 @@ structure Judgement World Atom where
   /-- The proposition satisfied by the world `w`. -/
   φ : Proposition Atom
 
-@[inherit_doc] scoped notation m "," w " ⊨ " φ => Judgement.mk m w φ
+@[inherit_doc] scoped notation "Modal[" m "," w " ⊨ " φ "]" => Judgement.mk m w φ
 
 /-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/
 @[simp, scoped grind =]
@@ -104,11 +103,11 @@ open scoped InferenceSystem Proposition
 
 @[scoped grind =]
 theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} :
-  ⇓(m,w ⊨ φ) = Satisfies m w φ := rfl
+  ⇓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 neg_satisfies : ⇓(m,w ⊨ ¬φ) ↔ ¬⇓(m,w ⊨ φ) := by
+theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
   induction φ generalizing w <;> grind
 
 /-- Characterisation of the `∨` connective.
@@ -117,7 +116,7 @@ Disjunction is defined in terms of the more primitive connectives given in `Prop
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.or_char {m : Model World Atom} :
-    ⇓(m,w ⊨ φ₁ ∨ φ₂) ↔ ⇓(m,w ⊨ φ₁) ∨ ⇓(m,w ⊨ φ₂) := by grind [Proposition.or]
+    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or]
 
 /-- Characterisation of the `→` connective.
 
@@ -126,7 +125,7 @@ This result proves that the definition is correct.
 -/
 @[scoped grind =]
 theorem Satisfies.impl_char {m : Model World Atom} :
-    ⇓(m,w ⊨ φ₁ → φ₂) ↔ (⇓(m,w ⊨ φ₁) → ⇓(m,w ⊨ φ₂)) := by grind [Proposition.impl]
+    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl]
 
 /-- Characterisation of the `□` modality.
 
@@ -134,11 +133,11 @@ Necessity is defined in terms of the more primitive connectives given in `Propos
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.box_char {m : Model World Atom} :
-    ⇓(m,w ⊨ □φ) ↔ ∀ w', m.r w w' → ⇓(m,w' ⊨ φ) := by grind [Proposition.box]
+    ⇓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) :=
-  {φ | ⇓(m,w ⊨ φ)}
+  {φ | ⇓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) :=
@@ -150,33 +149,33 @@ 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₂) :
-    ∃ φ, (⇓(m,w₁ ⊨ φ) ∧ ¬⇓(m,w₂ ⊨ φ)) := by grind [=_ neg_satisfies]
+    ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ neg_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₁ φ) : ⇓(m,w₂ ⊨ φ) := by
+    (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 : ⇓(m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind
+theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
 
 /-- The dual axiom, valid for all models. -/
-theorem Satisfies.dual : ⇓(m,w ⊨ ⋄φ ↔ ¬□¬φ) := by
+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) : ⇓(m,w ⊨ φ → ⋄φ) := by grind [instRefl.refl w]
+    (φ : 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},
-      ⇓((Model.mk r v),w ⊨ φ → ⋄φ)) :
+      ⇓Modal[⟨r, v⟩,w ⊨ φ → ⋄φ]) :
     Std.Refl r where
   refl := by
     intro w
@@ -186,12 +185,13 @@ theorem Satisfies.t_refl
     grind
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ⋄φ`. -/
-theorem Satisfies.t_box_diamond [instRefl : Std.Refl m.r] : ⇓(m,w ⊨ □φ → φ) ↔ ⇓(m,w ⊨ φ → ⋄φ) := by
+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) : ⇓(m,w ⊨ φ → □⋄φ) := by
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → □⋄φ] := by
   grind [instSymm.symm w]
 
 /-- Any model that admits the axiom B is symmetric. -/
@@ -199,7 +199,7 @@ theorem Satisfies.b_symm
     {r : World → World → Prop}
     [instAtomNonempty : Nonempty Atom]
     (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
-      ⇓(Model.mk r v,w ⊨ φ → □⋄φ)) :
+      ⇓Modal[⟨r, v⟩,w ⊨ φ → □⋄φ]) :
     Std.Symm r where
   symm := by
     intro w₁
@@ -210,7 +210,7 @@ theorem Satisfies.b_symm
 
 /-- The 4 axiom, valid for all transitive models. -/
 theorem Satisfies.four {m : Model World Atom} [instTrans : IsTrans World m.r] {w : World}
-    (φ : Proposition Atom) : ⇓(m,w ⊨ ⋄⋄φ → ⋄φ) := by
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ⋄⋄φ → ⋄φ] := by
   simp only [impl_char]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
@@ -222,7 +222,7 @@ theorem Satisfies.four_trans
     {r : World → World → Prop}
     [instAtomNonempty : Nonempty Atom]
     (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
-      ⇓(Model.mk r v,w ⊨ ⋄⋄φ → ⋄φ)) :
+      ⇓Modal[⟨r, v⟩,w ⊨ ⋄⋄φ → ⋄φ]) :
     IsTrans World r where
   trans := by
     intro w₁ w₂ w₃ h₁ h₂
@@ -234,14 +234,14 @@ theorem Satisfies.four_trans
 /-- The 5 axiom, valid for all Euclidean models. -/
 theorem Satisfies.five {m : Model World Atom} [instRightEuclidean : Relation.RightEuclidean m.r]
     {w : World}
-    (φ : Proposition Atom) : ⇓(m,w ⊨ ⋄φ → □⋄φ) := by grind [Relation.RightEuclidean]
+    (φ : 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},
-      ⇓(Model.mk r v,w ⊨ ⋄φ → □⋄φ)) :
+      ⇓Modal[⟨r, v⟩,w ⊨ ⋄φ → □⋄φ]) :
     Relation.RightEuclidean r where
   rightEuclidean := by
     intro w₁ w₂ w₃ h₁ h₂
@@ -253,7 +253,7 @@ theorem Satisfies.five_rightEuclidean
 /-- The D axiom, valid for all serial models. -/
 theorem Satisfies.d {m : Model World Atom} [instSerial : Relation.Serial m.r]
     {w : World}
-    (φ : Proposition Atom) : ⇓(m,w ⊨ □φ → ⋄φ) := by
+    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ □φ → ⋄φ] := by
   have : ∃ w', m.r w w' := instSerial.serial w
   grind
 
@@ -262,7 +262,7 @@ theorem Satisfies.d_serial
     {r : World → World → Prop}
     [instAtomNonempty : Nonempty Atom]
     (h : ∀ {v : World → Atom → Prop} {w : World} {φ : Proposition Atom},
-      ⇓(Model.mk r v,w ⊨ □φ → ⋄φ)) :
+      ⇓Modal[⟨r, v⟩,w ⊨ □φ → ⋄φ]) :
     Relation.Serial r where
   serial := by
     intro w₁
@@ -275,7 +275,7 @@ theorem Satisfies.d_serial
 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), ⇓(m,w ⊨ φ)
+  ∀ (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 =]
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index ec860c16c..63e88000e 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -32,7 +32,7 @@ def Proposition.denotation (m : Model World Atom) :
 /-- Characterisation theorem for the denotational semantics. -/
 @[scoped grind =]
 theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} :
-    w ∈ φ.denotation m ↔ ⇓(m,w ⊨ φ) := by
+    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

From 7d222223e72c0f5a939dbfc0fc8d0eec6127a588 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Thu, 30 Apr 2026 08:35:52 +0200
Subject: [PATCH 8/9] review fixes

---
 Cslib/Logics/Modal/Cube.lean | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 96c047a23..19798d53d 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -45,7 +45,7 @@ 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))
+def K45 World Atom := (K World Atom) ⊔ (Four World Atom) ⊔ (Five World Atom)
 
 /-- The modal logic D. -/
 @[simp, scoped grind =]
@@ -53,35 +53,35 @@ 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))
+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))
+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)))
+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))
+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))
+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))
+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))
+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)))
+def S5 World Atom := (K World Atom) ⊔ (T World Atom) ⊔ (Four World Atom) ⊔ (Five World Atom)
 
 section Order
 
@@ -107,8 +107,9 @@ theorem k_leq_four : (K World Atom ≤ Four World Atom) := by
 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 [Relation.refl_serial]
+  intro φ; grind
 
 theorem k_leq_t : (K World Atom ≤ T World Atom) := by
   calc

From 8627585dbfa076ced1948acd21efde00b939257c Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 1 May 2026 14:47:19 +0200
Subject: [PATCH 9/9] rename _char theorems

---
 Cslib/Logics/Modal/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index c7dde115b..3d43259a5 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -115,7 +115,7 @@ theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
 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_char {m : Model World Atom} :
+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.
@@ -124,7 +124,7 @@ Implication is defined in terms of the more primitive connectives given in `Prop
 This result proves that the definition is correct.
 -/
 @[scoped grind =]
-theorem Satisfies.impl_char {m : Model World Atom} :
+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 `□` modality.
@@ -132,7 +132,7 @@ theorem Satisfies.impl_char {m : Model World Atom} :
 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_char {m : Model World Atom} :
+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. -/
@@ -211,7 +211,7 @@ theorem Satisfies.b_symm
 /-- 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_char]
+  simp only [impl_iff_impl]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
   exists w''