diff --git a/Cslib.lean b/Cslib.lean
index a4da6b124..149a0a9b1 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -169,6 +169,8 @@ 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.Lean.Basic
+public import Cslib.Logics.Modal.Lean.SMul
 public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index 4901f785d..51e0729a0 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -67,6 +67,9 @@ abbrev SemiConfluent (r : α → α → Prop) :=
 /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/
 abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join (ReflTransGen r) x y
 
+/-- Relation `r` preserves predicate `P`. -/
+def Preserves (r : α → α → Prop) (P : α → Prop) : Prop := ∀ ⦃a b⦄, r a b → P a → P b
+
 /-- 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
 
diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean
index 25c954c2d..51ce37eae 100644
--- a/Cslib/Foundations/Syntax/Congruence.lean
+++ b/Cslib/Foundations/Syntax/Congruence.lean
@@ -24,7 +24,7 @@ class Congruence (r : α → α → Prop)
 
 /-- `a ≡[r] b` means that the `a` and `b` are related by the congruence `r`. -/
 @[nolint unusedArguments]
-def Congruence.r (r : α → α → Prop) [Congruence r] := r
+abbrev Congruence.r (r : α → α → Prop) [Congruence r] := r
 
 @[inherit_doc]
 scoped notation:29 a " ≡[" r "] " b => Congruence.r r a b
@@ -35,7 +35,7 @@ class DefaultCongruence (α : Type*) (r : outParam (α → α → Prop))
 /-- `a ≡ b` means that `a` and `b` are related by the canonical congruence relation for their
 type. -/
 @[nolint unusedArguments]
-def DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
+abbrev DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => DefaultCongruence.r
@@ -45,6 +45,6 @@ instance (α : Type*) (r : α → α → Prop) [DefaultCongruence α r] : Congru
 
 /-- An equivalence relation on `α` preserved by all contexts. -/
 class LawfulCongruence (r : α → α → Prop) [Congruence r] [HasContext α] extends
-  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) (· ≡[r] ·)
+  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
 
 end Cslib
diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index cd5a00f9d..b8770c350 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -444,11 +444,8 @@ theorem bisimilarity_is_congruence
 instance : Congruence (HomBisimilarity (lts (defs := defs))) := ⟨⟩
 
 /-- Bisimilarity is a congruence in CCS. -/
-instance bisimilarityCongruence :
-    LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
-  elim := by
-    dsimp [Congruence.r]
-    grind [Covariant, bisimilarity_is_congruence]
+instance bisimilarityCongruence : LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
+  elim := by grind [Covariant, bisimilarity_is_congruence]
 
 end CCS
 
diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean
index 1bba83dd3..00c8f74e3 100644
--- a/Cslib/Logics/HML/Basic.lean
+++ b/Cslib/Logics/HML/Basic.lean
@@ -259,12 +259,6 @@ theorem mem_denotation_iff_satisfies {φ : Proposition Label} :
 theorem mem_theory_iff_satisfies : φ ∈ theory lts s ↔ ⇓HML[lts,s ⊨ φ] := by
   grind
 
-/- A state satisfies a proposition iff it does not satisfy the negation of the proposition. -/
--- @[simp, scoped grind =]
--- theorem Satisfies.not_not_iff {lts : LTS State Label} :
---   ¬⇓HML[lts,s ⊨ ¬φ] ↔ ⇓HML[lts,s ⊨ φ] := by
---   grind
-
 open scoped Satisfies
 
 /-- A state is in the denotation of a proposition iff it is not in the denotation of the negation
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index b00710b46..f397edb4d 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -6,17 +6,18 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Foundations.Logic.Operators
-public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
 public import Cslib.Foundations.Relation.Euclidean
-public import Mathlib.Logic.Nonempty
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.Operators
+public import Cslib.Foundations.Relation.Defs
+public import Mathlib.Order.BooleanAlgebra.Set
 
 /-! # Modal Logic
 
 Modal logic is a logic for reasoning about relational structures, studying statements about
-necessity (`□φ`) and possibility `◇φ`.
+necessity (`□φ`) and possibility (`◇φ`).
 
 ## References
 
@@ -47,6 +48,9 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
+/-- Utility to coerce atoms into atomic propositions. -/
+instance : Coe Atom (Proposition Atom) := ⟨.atom⟩
+
 instance : HasNot (Proposition Atom) := ⟨.not⟩
 instance : HasAnd (Proposition Atom) := ⟨.and⟩
 instance : HasDiamond (Proposition Atom) := ⟨.diamond⟩
@@ -95,7 +99,6 @@ lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl
 
 /-- 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 φ
@@ -116,17 +119,19 @@ structure Judgement World Atom where
 @[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 =_]
+@[scoped grind =]
 theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} :
   Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl
 
+@[simp, scoped grind =]
+theorem Satisfies.atom_iff {a : Atom} : ⇓Modal[m,w ⊨ a] ↔ m.v w a := by rfl
+
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
 theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
@@ -166,7 +171,7 @@ This result proves that the definition is correct. -/
 theorem Satisfies.iff_iff_iff {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
   simp only [HasIff.iff, Proposition.iff]
-  grind [= derivation_def]
+  grind
 
 /-- Characterisation of the `□` modality.
 
@@ -190,7 +195,7 @@ theorem TheoryEq.ext_iff : TheoryEq m w₁ 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
+theorem satisfies_theory (h : ⇓Modal[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₂) :
@@ -203,27 +208,57 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
   apply TheoryEq.ext_iff.1 at h
   exact (h φ).mp hs
 
+/-- Every accessibility relation induces an inference system tag for proving valid axioms under
+the relation. -/
+inductive Axiom (r : World → World → Prop)
+
+/-- A proposition `φ` is an axiom under the relation `r` (the 'frame') if it holds for all
+valuations and worlds. -/
+instance (r : World → World → Prop) : InferenceSystem (Axiom r) (Proposition Atom) where
+  derivation φ := ∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]
+
+@[scoped grind ⇒]
+theorem Satisfies.axiom_def (r : World → World → Prop) :
+    (∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]) ↔ Axiom r⇓φ := by rfl
+
+/-- If a proposition is an axiom under the relation of a model, it is satisfied by every world. -/
+@[scoped grind .]
+theorem Satisfies.of_axiom (m : Model World Atom) (φ : Proposition Atom) (h : Axiom m.r⇓φ)
+    (w : World) : ⇓Modal[m,w ⊨ φ] := h m.v w
+
 /-- The K axiom, valid for all models. -/
-theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
+theorem Satisfies.k (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    Axiom r⇓(□(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind
 
 /-- The dual axiom, valid for all models. -/
-theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
+theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
+    Axiom r⇓(◇φ ↔ ¬□¬φ) := by
+  intro _ w
   simp only [Satisfies.iff_iff_iff]
   constructor
   · grind
   · grind only [= not_iff_not, = diamond_iff_exists, = box_iff_forall]
 
+/-- Possibility preserves conjunction in all models. -/
+theorem Satisfies.diamond_and (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    Axiom r⇓(◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂)) := by grind
+
+/-- Possibility can be combined with necessity. -/
+theorem Satisfies.diamond_and_box (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    Axiom r⇓((◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂)) := by 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]
+theorem Satisfies.t (r : World → World → Prop) [instRefl : Std.Refl r] (φ : Proposition Atom)
+    : Axiom r⇓(φ → ◇φ) := by
+  grind [instRefl.refl]
 
 /-- Any model that admits the axiom T is reflexive. -/
-theorem Satisfies.t_refl {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → ◇φ]) : Std.Refl r where
+theorem Satisfies.t_refl (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(φ → ◇φ)) : Std.Refl r where
   refl w := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w
-    let h' := h (v := v) (w := w) (φ := .atom a)
+    let h' := h (v := v) (w := w) (φ := a)
     grind
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/
@@ -232,70 +267,106 @@ theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ]
   grind
 
 /-- The B axiom, valid for all symmetric models. -/
-theorem Satisfies.b {m : Model World Atom} [Std.Symm m.r] {w : World} (φ : Proposition Atom) :
-    ⇓Modal[m,w ⊨ φ → □◇φ] := by
-  have := Std.Symm.symm (r := m.r) w
+theorem Satisfies.b (r : World → World → Prop) [Std.Symm r] (φ : Proposition Atom) :
+    Axiom r⇓(φ → □◇φ) := by
+  intro _ w
+  have := Std.Symm.symm (r := r) w
   grind
 
 /-- Any model that admits the axiom B is symmetric. -/
-theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → □◇φ]) : Std.Symm r where
+theorem Satisfies.b_symm (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(φ → □◇φ)) : Std.Symm r where
   symm w₁ := by
     have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
-    let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
+    let h₁ := h (v := v₁) (w := w₁) (φ := a)
     simp [imp_iff_imp] at h₁
     grind
 
 /-- The 4 axiom, valid for all transitive models. -/
-theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World}
-    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by
+theorem Satisfies.four (r : World → World → Prop) [IsTrans World r]
+    (φ : Proposition Atom) : Axiom r⇓(◇◇φ → ◇φ) := by
+  intro _ _
   simp only [imp_iff_imp]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
   exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩
 
 /-- Any model that admits 4 is transitive. -/
-theorem Satisfies.four_trans {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇◇φ → ◇φ]) : IsTrans World r where
+theorem Satisfies.four_trans (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ (φ : Proposition Atom), Axiom r⇓(◇◇φ → ◇φ)) : IsTrans World r where
   trans w₁ w₂ w₃ h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
 /-- The 5 axiom, valid for all Euclidean models. -/
-theorem Satisfies.five {m : Model World Atom} [Relation.RightEuclidean m.r]
-    {w : World}
-    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇φ → □◇φ] := by
-  have := @Relation.RightEuclidean.rightEuclidean (r := m.r)
+theorem Satisfies.five (r : World → World → Prop) [Relation.RightEuclidean r]
+    (φ : Proposition Atom) : Axiom r⇓(◇φ → □◇φ) := by
+  have := @Relation.RightEuclidean.rightEuclidean (r := r)
   grind
 
 /-- Any model that admits 5 is Euclidean. -/
-theorem Satisfies.five_rightEuclidean {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w : World} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇φ → □◇φ]) :
+theorem Satisfies.five_rightEuclidean (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(◇φ → □◇φ)) :
     Relation.RightEuclidean r where
   rightEuclidean {w₁ w₂ w₃} h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
 /-- The D axiom, valid for all serial models. -/
-theorem Satisfies.d {m : Model World Atom} [Relation.Serial m.r] {w} (φ : Proposition Atom) :
-    ⇓Modal[m,w ⊨ □φ → ◇φ] := by
-  have : ∃ w', m.r w w' := Relation.Serial.serial w
+theorem Satisfies.d (r : World → World → Prop) [Relation.Serial r] (φ : Proposition Atom) :
+    Axiom r⇓(□φ → ◇φ) := by
+  intro _ w
+  have : ∃ w', r w w' := Relation.Serial.serial w
   grind
 
 /-- Any model that admits D is serial. -/
-theorem Satisfies.d_serial {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ □φ → ◇φ]) : Relation.Serial r where
+theorem Satisfies.d_serial (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(□φ → ◇φ)) : Relation.Serial r where
   serial w₁ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₁
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
+/-- The L axiom, or Löb's theorem, valid for all transitive and converse well-founded models. -/
+theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
+    (hwf : WellFounded (flip r)) (φ : Proposition Atom) : Axiom r⇓(□(□φ → φ) → □φ) := by
+  intro v w
+  let m := Model.mk r v
+  simp_rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall]
+  intro h
+  refine (hwf.induction (C := fun w' => m.r w w' → ⇓Modal[m,w' ⊨ φ]) · ?_)
+  intro w' ih hww'
+  have hImp : ⇓Modal[m, w' ⊨ □φ → φ] := h _ hww'
+  rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall] at hImp
+  apply hImp
+  intro w'' hw'w''
+  apply ih _ hw'w''
+  exact IsTrans.trans _ _ _ hww' hw'w''
+
+open Relation in
+/-- Axiom .2, valid for all frames with the diamond property. -/
+theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
+    (φ : Proposition Atom) : Axiom r⇓(◇□φ → □◇φ) := by
+  simp_rw [← Satisfies.axiom_def, Satisfies.imp_iff_imp, Satisfies.diamond_iff_exists,
+    Satisfies.box_iff_forall]
+  rintro v w ⟨_, hww₁, _⟩ _ hww₂
+  obtain ⟨w₃, hww₃⟩ := h hww₁ hww₂
+  grind
+
+open Relation in
+/-- Any model that admits axiom .2 has the diamond property. -/
+theorem Satisfies.pointTwo_diamond (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(◇□φ → □◇φ)) : Diamond r := by
+  intro w w₁ w₂ hww₁ hww₂
+  specialize h (Classical.arbitrary Atom) (fun w' _ => r w₁ w') w
+  grind [Join]
+
 /-- 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 =]
@@ -307,4 +378,22 @@ def Proposition.valid (S : Set (Model World Atom)) (φ : Proposition Atom) : Pro
 def logic (S : Set (Model World Atom)) : Set (Proposition Atom) :=
   {φ | φ.valid S}
 
+/-- Modal logic is antitone (wrt the class of models). -/
+theorem logic_antitone : Antitone (logic (World := World) (Atom := Atom)) :=
+  fun _ _ hS₁S₂ _ hφ m hm w => hφ m (hS₁S₂ hm) w
+
+/-- The class of all models generated by a frame (relation). -/
+abbrev modelsOfRelation (r : World → World → Prop) : Set (Model World Atom) :=
+  {m | m.r = r}
+
+/-- A proposition is an axiom of a frame exactly when it belongs to the logic of all models over
+that frame. -/
+theorem axiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
+    Axiom r⇓φ ↔ φ ∈ logic (modelsOfRelation r) := by
+  constructor
+  case mp =>
+    rintro h m rfl w
+    exact h m.v w
+  case mpr => grind [Satisfies.axiom_def]
+
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 765193ac0..8eb2dc385 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Marianna Girlando
 module
 
 public import Cslib.Logics.Modal.Basic
+public import Cslib.Foundations.Relation.Euclidean
 
 /-! # Modal Logic Cube
 
@@ -135,6 +136,10 @@ section Validity
 This section showcases how to prove the expected validities in the different modal logics.
 -/
 
+open InferenceSystem
+
+open scoped Satisfies
+
 /-- 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]
@@ -142,7 +147,7 @@ theorem K.k_valid : (□(φ₁ → φ₂) → (□φ₁ → □φ₂) : Proposit
 /-- 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))]
+  grind [Satisfies.t (instRefl := h)]
 
 end Validity
 
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 4b3415b33..f4982e270 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Logics.Modal.Basic
+public import Cslib.Logics.Modal.LogicalEquivalence
 
 /-! # Denotational semantics for Modal Logic
 
@@ -48,4 +48,21 @@ theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} :
     (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by
   apply Iff.intro <;> grind [_=_ satisfies_mem_denotation]
 
+/-- Logically equivalent propositions under a model have the same denotation. -/
+theorem Proposition.equiv_iff_denotation_eq :
+    (φ₁ ≡[Equiv m] φ₂) ↔ φ₁.denotation m = φ₂.denotation m := by
+  constructor <;> intro h
+  case mp =>
+    ext w
+    grind [h w]
+  case mpr =>
+    intro w
+    rw [Set.ext_iff] at h
+    grind [h w]
+
+/-- `grind`-friendly first part of `Proposition.equiv_iff_denotation_eq`. -/
+@[scoped grind ⇒]
+theorem Proposition.denotation_eq_of_equiv (h : φ₁ ≡[Equiv m] φ₂) :
+    φ₁.denotation m = φ₂.denotation m := equiv_iff_denotation_eq.1 h
+
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
new file mode 100644
index 000000000..9c0e11b06
--- /dev/null
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -0,0 +1,107 @@
+/-
+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.Denotation
+
+/-! # Modal Logic for Lean
+
+This module develops the interplay between modal logic and Lean's propositional language, in order
+to enable the use of modal logic to reason about standard Lean relations using `Prop`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+namespace Model
+
+/-- Given a relation `r` on `α`, constructs the modal model whose worlds are elements of `α`
+and whose atoms are Lean predicates on `α` (`α → Prop`).
+
+Valuation checks that a world satisfies a predicate. For example, under `Model.ofPredicates r`, `□P`
+at `a : α` means that `P a'` holds at every `a'` such that `r a a'`. -/
+abbrev ofPredicates (r : α → α → Prop) : Model α (α → Prop) where
+  r := r
+  v w P := P w
+
+/-- Given a relation `r` on `α` and a container type `β` for `α` (`Membership α β`), constructs the
+modal model whose worlds are elements of `α` and whose atoms are of type `β`.
+
+Valuation is membership. For example, under `Model.ofContainers r`, `□b` at `a : α` means that
+`a' ∈ b` holds for every `a'` such that `r a a'`. -/
+abbrev ofContainers [Membership α β] (r : α → α → Prop) : Model α β where
+  r := r
+  v w p := w ∈ p
+
+/-- Abbreviation for `Model.ofContainers` where the container type is a `Set`. -/
+abbrev ofSets (r : α → α → Prop) : Model α (Set α) := ofContainers r
+
+/-- The set model and predicate model of a relation are definitionally equal. -/
+theorem ofSets_eq_ofPredicates (r : α → α → Prop) :
+    ofSets r = ofPredicates r := rfl
+
+end Model
+
+open Model Relation
+open scoped InferenceSystem Satisfies
+
+/-! ## Models of Lean predicates -/
+
+/-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
+@[scoped grind =]
+theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
+    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := Iff.rfl
+
+/-- Under `Model.ofPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/
+@[scoped grind ⇒]
+theorem Satisfies.ofPredicates_preserves_iff {P : α → Prop} (r : α → α → Prop) :
+    (∀ a, ⇓Modal[ofPredicates r, a ⊨ P → □P]) ↔ Preserves r P := by
+  constructor
+  case mp =>
+    intro h a₁ a₂ hr hPa₁
+    grind [h a₁]
+  case mpr =>
+    grind [Preserves]
+
+/-- Logical equivalence under `Model.ofPredicates r`. -/
+abbrev Proposition.Equiv.OfPredicates (r : α → α → Prop) := Proposition.Equiv (ofPredicates r)
+
+/-- Logical equivalence under `Model.ofContainers r`. -/
+abbrev Proposition.Equiv.OfContainers [Membership α β] (r : α → α → Prop) :=
+  Proposition.Equiv (ofContainers (β := β) r)
+
+/-- Logically equivalent propositions under `Equiv.OfPredicates r` have the same denotation in the
+Lean modal model induced by `ofPredicates r`. -/
+@[scoped grind ⇒]
+theorem Proposition.equivOfPredicates_denotation_eq {r : α → α → Prop}
+    {φ₁ φ₂ : Proposition (α → Prop)} :
+    (φ₁ ≡[Equiv.OfPredicates r] φ₂) ↔
+      φ₁.denotation (ofPredicates r) = φ₂.denotation (ofPredicates r) :=
+  equiv_iff_denotation_eq
+
+/-- Logically equivalent propositions under `Equiv.OfContainers r` have the same denotation in the
+Lean modal model induced by `ofContainers r`. -/
+@[scoped grind ⇒]
+theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r : α → α → Prop}
+    {φ₁ φ₂ : Proposition β} :
+    (φ₁ ≡[Equiv.OfContainers (β := β) r] φ₂) ↔
+      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) :=
+  equiv_iff_denotation_eq
+
+/-- Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in
+the Lean modal model induced by `r`. -/
+theorem Proposition.equivOfPredicates_and {r : α → α → Prop} {P Q : α → Prop} :
+    (fun a => P a ∧ Q a) ≡[Equiv.OfPredicates r] (P ∧ Q) := by grind
+
+/-- Under `Equiv.OfContainers r`, if membership in the infimum of two containers is equivalent to
+membership in both containers, then atomic infimum is logically equivalent to modal conjunction. -/
+theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α → α → Prop) (p q : β)
+    (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
+    (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by grind
+
+end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
new file mode 100644
index 000000000..06b7a9f29
--- /dev/null
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -0,0 +1,106 @@
+/-
+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 Mathlib.GroupTheory.GroupAction.SubMulAction
+public import Cslib.Logics.Modal.Lean.Basic
+
+/-! # Modal Logic for scalar multiplication (SMul)
+
+Any scalar multiplication operation `•` induces an accessibility relation where two elements are
+related if the latter is the result of applying a scalar multiplication to the former.
+
+Properties of the operator translate to properties of the relation, for example a semigroup action
+on a commutative semigroup yields a relation with the `Diamond` property. This bridge allows for
+studying properties of the operation using modal logic.
+-/
+
+@[expose] public section
+
+namespace Relation
+
+/-- The accessibility relation induced by a scalar multiplication operation: `x` is related to `y`
+when there exists `m` such that `m • x = y`. -/
+def ofSMul (M α : Type*) [SMul M α] (x y : α) : Prop := ∃ m : M, m • x = y
+
+/-- The relation induced by a monoid action is reflexive. -/
+instance [Monoid M] [MulAction M α] : Std.Refl (ofSMul M α) where
+  refl x := by
+    use 1
+    simp
+
+/-- The relation induced by a semigroup action is transitive. -/
+instance [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α) where
+  trans := by
+    rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
+    use n * m
+    rw [mul_smul]
+
+/-- The relation induced by a group action is symmetric. -/
+instance [Group G] [MulAction G α] : Std.Symm (ofSMul G α) where
+  symm := by
+    rintro x _ ⟨g, rfl⟩
+    use g⁻¹
+    simp
+
+/-- The relation induced by an action of a nonempty type is serial. -/
+instance [SMul M α] [Nonempty M] : Serial (ofSMul M α) where
+  serial x := ⟨Classical.arbitrary M • x, Classical.arbitrary M, rfl⟩
+
+/-- TODO: upstream this generalisation of Mathlib's `smulCommClass_self`, which applies only to
+monoids `M`. -/
+instance {M α} [CommSemigroup M] [SemigroupAction M α] : SMulCommClass M M α where
+  smul_comm m n a := by rw [←mul_smul, mul_comm, mul_smul]
+
+/-- The relation induced by an action commuting with itself has the diamond property. -/
+@[scoped grind .]
+theorem ofSMul_diamond [SMul M α] [SMulCommClass M M α] : Diamond (ofSMul M α) := by
+  rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
+  use! n • m • x, n, m, smul_comm ..
+
+/-- Preservation by an action-induced relation is exactly closure under the action. -/
+@[scoped grind =]
+theorem ofSMul_preserves_iff [SMul M α] {P : α → Prop} :
+    Preserves (ofSMul M α) P ↔ ∀ m : M, ∀ x, P x → P (m • x) := by
+  constructor
+  case mp =>
+    intro h m x hx
+    exact h ⟨m, rfl⟩ hx
+  case mpr =>
+    rintro h x y ⟨m, rfl⟩ hx
+    exact h m x hx
+
+/-- Membership in a type closed under a scalar action is preserved by the relation induced by the
+action. -/
+@[scoped grind .]
+theorem ofSMul_preserves_mem [SMul M α] [SetLike S α] [SMulMemClass S M α]
+    (s : S) : Preserves (ofSMul M α) (· ∈ s) := by
+  rw [Relation.ofSMul_preserves_iff]
+  apply SMulMemClass.smul_mem
+
+end Relation
+
+namespace Cslib.Logic.Modal.Proposition
+
+/-- Characterisation of the denotation of a `◇p` under `ofSMul`. -/
+theorem ofSMul_diamond_denotation [SMul M α] [Membership α β] (p : β) :
+    (◇p : Proposition β).denotation (Model.ofContainers (Relation.ofSMul M α)) =
+      {x | ∃ m : M, m • x ∈ p} := by
+  ext x
+  change (∃ y, (∃ m : M, m • x = y) ∧ y ∈ p) ↔ ∃ m : M, m • x ∈ p
+  grind
+
+/-- For `SetLike` objects closed under a commutative semigroup action, simultaneous reachability is
+equivalent to separate reachability. -/
+theorem ofSMul_diamond_and_equiv [CommSemigroup M] [SemigroupAction M α] [SetLike S α]
+    [SMulMemClass S M α] (p q : S) :
+    ◇(p ∧ q : Proposition S) ≡[Equiv.OfContainers (Relation.ofSMul M α)] (◇p ∧ ◇q) :=
+  diamond_and_equiv_of_preserves Relation.ofSMul_diamond
+    (Relation.ofSMul_preserves_mem p)
+    (Relation.ofSMul_preserves_mem q)
+
+end Cslib.Logic.Modal.Proposition
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 092ff00e6..afd4cd798 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -24,42 +24,46 @@ 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 ⊨ φ₁ ↔ φ₂]
+/-- The modal propositions `φ₁` and `φ₂` are equivalent in the model `m`. -/
+def Proposition.Equiv (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Prop :=
+  ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]
 
-instance : Congruence (Proposition.Equiv S) := ⟨⟩
+instance : Congruence (Proposition.Equiv m) := ⟨⟩
 
 @[scoped grind =]
-theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
-    φ₁.Equiv S φ₂ ↔ (φ₁ ≡[Equiv S] φ₂) := by rfl
+theorem Proposition.equiv_def (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) :
+    (φ₁.Equiv m φ₂) ↔ φ₁ ≡[Equiv m] φ₂ := by rfl
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_forall_der (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[Equiv S] φ₂) : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
-  intro s
-  specialize h s
-  assumption
-
-theorem Proposition.forall_der_equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[Equiv S] φ₂ := by
-  intro s
-  specialize h s
-  assumption
+theorem Proposition.equiv_iff_forall_der (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
+    : (φ₁ ≡[Equiv m] φ₂) ↔ ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by rfl
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[Equiv S] φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) :
-    ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
+theorem Proposition.equiv_iff_forall_iff {m : Model World Atom} {φ₁ φ₂ : Proposition Atom} :
+    (φ₁ ≡[Equiv m] φ₂) ↔ ∀ (w : World), ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
   grind [=_ Satisfies.iff_iff_iff]
 
+/-- A class of models, defined as a set. -/
+abbrev ModelClass World Atom := Set (Model World Atom)
+
+/-- The modal propositions `φ₁` and `φ₂` are equivalent in the model class `S`. -/
+def Proposition.EquivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) :=
+  ∀ m ∈ S, φ₁ ≡[Equiv m] φ₂
+
+instance : Congruence (Proposition.EquivWithin S) := ⟨⟩
+
+@[scoped grind =]
+theorem Proposition.equivWithin_def (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) :
+    φ₁.EquivWithin S φ₂ ↔ (φ₁ ≡[EquivWithin S] φ₂) := by rfl
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_of_EquivWithin {S : ModelClass World Atom} (h : φ₁ ≡[EquivWithin S] φ₂)
+    (m : Model World Atom) (hm : m ∈ S) : φ₁ ≡[Equiv m] φ₂ := h m hm
+
 /-- Logical equivalence preserves validity. -/
-theorem Proposition.equiv_valid (S : Set (Model World Atom))
-    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[Equiv S] φ₂) :
+theorem Proposition.equivWithin_valid (S : ModelClass World Atom)
+    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[EquivWithin S] φ₂) :
     (φ₁.valid S ↔ φ₂.valid S) := by
-  apply Proposition.equiv_forall_der at h
-  simp only [Satisfies.iff_iff_iff] at h
   grind
 
 /-- Propositional contexts. -/
@@ -89,17 +93,33 @@ lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} :
 open scoped Proposition Proposition.Context
 
 /-- Logical equivalence is an equivalence relation. -/
-instance {World Atom} (S : Set (Model World Atom)) :
-    IsEquiv (Proposition Atom) (Proposition.Equiv S) := by
+instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv m) := by
+  rw [← equivalence_iff_isEquiv]
+  constructor
+  case refl => grind [Proposition.Equiv]
+  case symm =>
+    grind
+  case trans =>
+    grind
+
+/-- Logical equivalence within a class is an equivalence relation. -/
+instance {World Atom} (S : ModelClass World Atom) :
+    IsEquiv (Proposition Atom) (Proposition.EquivWithin S) := by
   rw [← equivalence_iff_isEquiv]
-  grind [Equivalence, Proposition.Equiv]
+  unfold Proposition.EquivWithin
+  constructor
+  case refl =>
+    grind [Proposition.Equiv]
+  case symm =>
+    grind
+  case trans =>
+    grind
 
 /-- Logical equivalence is a congruence. -/
-instance {World Atom} (S : Set (Model World Atom)) :
-    LawfulCongruence (Proposition.Equiv S) where
-  elim ctx φ₁ φ₂ heqv m hₘ w := by
+instance (m : Model World Atom) : LawfulCongruence (Proposition.Equiv m) where
+  elim ctx φ₁ φ₂ heqv w := by
     induction ctx generalizing w
-    case hole => grind [=_ Proposition.Context.fill_def]
+    case hole => apply heqv
     case not c ih | andL c ih | andR c ih =>
       specialize ih w
       grind [=_ Proposition.Context.fill_def]
@@ -111,6 +131,12 @@ instance {World Atom} (S : Set (Model World Atom)) :
         specialize ih w'
         grind [=_ Proposition.Context.fill_def]
 
+/-- Logical equivalence within a class is a congruence. -/
+instance (S : ModelClass World Atom) :
+    LawfulCongruence (Proposition.EquivWithin S) where
+  elim ctx _ _ h m hm :=
+    LawfulCongruence.covariant.elim ctx (h m hm)
+
 /-- Judgemental contexts. -/
 structure Satisfies.Context (World Atom : Type*) where
   /-- The model to consider. -/
@@ -122,8 +148,7 @@ structure Satisfies.Context (World Atom : Type*) where
 def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) :
     Judgement World Atom := Modal[c.m, c.w ⊨ φ]
 
-instance : HasHContext (Judgement World Atom) (Proposition Atom) :=
-  ⟨Satisfies.Context.fill⟩
+instance : HasHContext (Judgement World Atom) (Proposition Atom) := ⟨Satisfies.Context.fill⟩
 
 @[scoped grind =]
 lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
@@ -135,9 +160,40 @@ open scoped Satisfies.Context
 instance : LogicalEquivalence
     (α := Proposition Atom)
     (Judgement := Judgement World Atom) InferenceSystem.Default
-    (Proposition.Equiv (Set.univ (α := Model World Atom))) where
+    (Proposition.EquivWithin (Set.univ (α := Model World Atom))) where
   eqvFillValid heqv c h := by
     specialize heqv c.m
     grind [=_ Satisfies.Context.fill_def]
 
+/-- Correspondence of equivalence and axiom validity. -/
+theorem Proposition.axiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) :
+    (Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := Iff.rfl
+
+open Relation in
+/-- In a transitive diamond model, possibility distributes over conjunction for propositions
+whose satisfaction is preserved along accessibility. -/
+@[scoped grind ⇒]
+theorem Proposition.diamond_and_equiv_of_preserves {m : Model World Atom} [IsTrans World m.r]
+    {φ₁ φ₂ : Proposition Atom} (hd : Diamond m.r) (h₁ : Preserves m.r (⇓Modal[m,· ⊨ φ₁]))
+    (h₂ : Preserves m.r (⇓Modal[m,· ⊨ φ₂])) :
+    ◇(φ₁ ∧ φ₂) ≡[Equiv m] (◇φ₁ ∧ ◇φ₂) := by
+  rw [equiv_iff_forall_iff]
+  intro a
+  constructor
+  case mp => grind
+  case mpr =>
+    rintro ⟨⟨b, hab, hb⟩, ⟨c, hac, hc⟩⟩
+    rcases hd hab hac with ⟨d, hbd, hcd⟩
+    use d, IsTrans.trans _ _ _ hab hbd
+    exact ⟨h₁ hbd hb, h₂ hcd hc⟩
+
+/-- In a reflexive and transitive model, diamond absorbs itself (idempotency). -/
+theorem Proposition.diamond_diamond_equiv {m : Model World Atom} [Std.Refl m.r] [IsTrans World m.r]
+    (φ : Proposition Atom) : ◇◇φ ≡[Equiv m] ◇φ := by
+  rw [equiv_iff_forall_iff]
+  intro w
+  constructor <;> rw [← Satisfies.imp_iff_imp]
+  · grind [Satisfies.four]
+  · grind [Satisfies.t]
+
 end Cslib.Logic.Modal
diff --git a/CslibTests.lean b/CslibTests.lean
index 99f1d31f5..d5103dbcb 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -15,5 +15,6 @@ import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Modal
+import CslibTests.Modal.Ideal
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/Modal.lean b/CslibTests/Modal.lean
index be9f5b880..e9a2bdb61 100644
--- a/CslibTests/Modal.lean
+++ b/CslibTests/Modal.lean
@@ -19,19 +19,19 @@ example : ((◇◇φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈
   intro m h w
   let : IsTrans World m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ D4 World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : IsTrans World m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.four φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.four _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ D5 World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example :
     Proposition.and (□φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈
@@ -40,31 +40,31 @@ example :
   let : Relation.Serial m.r := h.1
   let : IsTrans World m.r := h.2.1
   let : Relation.RightEuclidean m.r := h.2.2
-  exact ⟨Satisfies.d φ, Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ DB World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : Std.Symm m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.b φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.b _ φ _ _⟩
 
 example : ((φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ TB World Atom := by
   intro m h w
   let : Std.Refl m.r := h.1
   let : Std.Symm m.r := h.2
-  exact ⟨Satisfies.t φ, Satisfies.b φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.b _ φ _ _⟩
 
 example : ((φ → □◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ KB5 World Atom := by
   intro m h w
   let : Std.Symm m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.b φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.b _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ S4 World Atom := by
   intro m h w
   let : Std.Refl m.r := h.1
   let : IsTrans World m.r := h.2
-  exact ⟨Satisfies.t φ, Satisfies.four φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.four _ φ _ _⟩
 
 example :
     Proposition.and (φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈
@@ -73,6 +73,6 @@ example :
   let : Std.Refl m.r := h.1
   let : IsTrans World m.r := h.2.1
   let : Relation.RightEuclidean m.r := h.2.2
-  exact ⟨Satisfies.t φ, Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 end Cslib.Logic.Modal
diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
new file mode 100644
index 000000000..f9cb8ee2a
--- /dev/null
+++ b/CslibTests/Modal/Ideal.lean
@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Logics.Modal.Lean.SMul
+import Mathlib.RingTheory.Ideal.Operations
+
+/-! # Example: radicals of ideals with modal logic
+
+We leverage the accessibility relation induced by scalar multiplication to exemplify how laws of
+radicals of ideals can be derived from modal logic laws.
+-/
+
+namespace CslibTests
+
+open Cslib Logic Modal Proposition Model Relation
+
+/-! ## Relational view of radicals of ideals
+
+We interpret positive exponentiation as an action and hence as an accessibility relation.
+Ideals are invariant under this action, while radical membership corresponds to reachability.
+-/
+
+/-- Positive naturals act on a monoid by exponentiation. -/
+@[instance_reducible]
+def posPowAction [Monoid α] : MulAction ℕ+ α where
+  smul n x := x ^ (n : ℕ)
+  one_smul x := pow_one x
+  mul_smul m n x := by
+    simp [HSMul.hSMul, ←pow_mul, mul_comm]
+
+local instance [Monoid α] : MulAction ℕ+ α := posPowAction
+
+/-- Ideals are invariant under positive exponentiation. -/
+theorem Ideal.posPowSMulMemClass [Semiring R] : SMulMemClass (Ideal R) ℕ+ R where
+  smul_mem n _ hx := Ideal.pow_mem_of_mem _ hx n n.prop
+
+local instance [Semiring R] : SMulMemClass (Ideal R) ℕ+ R := Ideal.posPowSMulMemClass
+
+/-- Accessibility by positive natural exponentiation. -/
+abbrev PosPow α [Monoid α] := Relation.ofSMul ℕ+ α
+
+/-- The modal model of ideals under positive-power accessibility. -/
+abbrev idealPowerModel [Semiring R] : Model R (Ideal R) := Model.ofContainers (PosPow R)
+
+/-- Logical equivalence under `idealPowerModel`. -/
+abbrev IdealEquiv [Semiring R] := Proposition.Equiv (idealPowerModel (R := R))
+
+/-- An ideal atom denotes its underlying set in `idealPowerModel`. -/
+example [Semiring R] (I : Ideal R) : (I : Set R) = Proposition.denotation idealPowerModel I := rfl
+
+/-- Characterisation of radicals as modal denotations. This is the key bridge that enables reasoning
+about membership of radicals with modal logic. -/
+@[local grind =]
+theorem Ideal.radical_eq_modal_denotation [CommSemiring R] (I : Ideal R) :
+    (I.radical : Set R) = Proposition.denotation idealPowerModel (◇I) := by
+  rw [Proposition.ofSMul_diamond_denotation]
+  ext x
+  apply Iff.intro
+  · rintro ⟨n, hn⟩
+    refine ⟨⟨n + 1, Nat.succ_pos _⟩, ?_⟩
+    exact I.pow_mem_of_pow_mem hn (Nat.le_succ n)
+  · rintro ⟨n, hn⟩
+    exact ⟨(n : ℕ), hn⟩
+
+/-- In `idealPowerModel`, the radical of an ideal is logically equivalent to possibility. -/
+theorem Ideal.radical_equiv_diamond [CommSemiring R] (I : Ideal R) :
+    (I.radical : Proposition (Ideal R)) ≡[IdealEquiv] ◇I :=
+  Proposition.equiv_iff_denotation_eq.mpr (Ideal.radical_eq_modal_denotation I)
+
+open scoped Satisfies
+
+/-- Radical is idempotent, as a consequence of modal idempotence of `◇`. -/
+theorem Ideal.radical_idem [CommSemiring R] (I : Ideal R) : I.radical.radical = I.radical := by
+  apply SetLike.ext'
+  simp only [Ideal.radical_eq_modal_denotation]
+  apply Proposition.denotation_eq_of_equiv
+  calc
+    (◇(I.radical : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] ◇◇I := by
+      let pc : HasContext.Context (Proposition (Ideal R)) := Context.diamond .hole
+      apply LawfulCongruence.covariant.elim pc (Ideal.radical_equiv_diamond I)
+    _ ≡[IdealEquiv] ◇I := by apply Proposition.diamond_diamond_equiv
+
+/-- In `idealPowerModel`, possibility of membership in an infimum is equivalent to simultaneous
+possibility of membership in both ideals. -/
+theorem Ideal.inf_modelEquiv [Semiring R] (I J : Ideal R) :
+    (◇(I ⊓ J : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] (◇I ∧ ◇J) := by
+  calc
+    (◇(I ⊓ J : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] ◇(I ∧ J) := by
+      let pc : HasContext.Context (Proposition (Ideal R)) := Context.diamond .hole
+      exact LawfulCongruence.covariant.elim pc
+        (Proposition.ofContainers_inf_equiv (PosPow R) I J (by simp))
+    _ ≡[IdealEquiv] (◇I ∧ ◇J) := Proposition.ofSMul_diamond_and_equiv I J
+
+/-- Radicals of ideals distribute over intersection, as a consequence that `◇(I ⊓ J)` is logically
+equivalent to `◇I ∧ ◇J`. -/
+theorem Ideal.radical_inf [CommSemiring R] (I J : Ideal R) :
+    (I ⊓ J).radical = I.radical ⊓ J.radical := by
+  apply SetLike.ext'
+  simp_rw [Submodule.coe_inf, Ideal.radical_eq_modal_denotation,
+    Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]
+  rfl
+
+end CslibTests