fix: address review findings for PR #636

- Restore LogicalEquivalence typeclass instantiation (HasContext,
  IsEquiv, Congruence, HasHContext, LogicalEquivalence) following
  the HML pattern, adapted for Lukasiewicz primitives
- Add Proposition.Equiv parametric on model class S with notation
- Fix copyright: restore Fabrizio Montesi as co-author on
  LogicalEquivalence.lean
- Fix "fork's" artifact in docstring
- Fix "satifies" typo in Basic.lean
- Simplify redundant have in t_box_diamond proof

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: benbrastmckie

Cslib/Logics/Modal/Basic.lean

@@ -187,7 +187,7 @@ theorem Satisfies.diamond_iff_exists {m : Model World Atom} :
 theorem Satisfies.and_iff_and {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := Satisfies.and_iff
 
-/-- The theory of a world in a model is the set of all propositions that it satifies. -/
+/-- The theory of a world in a model is the set of all propositions that it satisfies. -/
 abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
   {φ | ⇓Modal[m,w ⊨ φ]}
 
@@ -266,8 +266,7 @@ theorem Satisfies.t_box_diamond [Std.Refl m.r] :
     rw [diamond_iff]
     exact ⟨w, hrefl, hφ⟩
   · intro h hbox
-    have hφ := hbox w hrefl
-    exact hφ
+    exact hbox w hrefl
 
 /-- The B axiom, valid for all symmetric models. -/
 theorem Satisfies.b {m : Model World Atom} [instSymm : Std.Symm m.r] {w : World}

Cslib/Logics/Modal/LogicalEquivalence.lean

@@ -1,12 +1,13 @@
 /-
-Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Copyright (c) 2026 Fabrizio Montesi, Benjamin Brast-McKie. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Benjamin Brast-McKie
+Authors: Fabrizio Montesi, Benjamin Brast-McKie
 -/
 
 module
 
 public import Cslib.Logics.Modal.Basic
+public import Cslib.Foundations.Logic.LogicalEquivalence
 
 /-! # Logical Equivalence for Modal Propositions
 
@@ -16,11 +17,10 @@ models and worlds) is a congruence with respect to contexts.
 
 ## Main Definitions
 
-* `Proposition.Context` -- a one-hole context matching the fork's `Proposition` constructors
+* `Proposition.Context` -- a one-hole context matching the `Proposition` constructors
 * `Proposition.Context.fill` -- substitute a proposition into the hole
-* `LogicallyEquivalent` -- two propositions are logically equivalent when they are satisfied by
-  exactly the same model-world pairs
-* `LogicallyEquivalent.congruence` -- logical equivalence is preserved under all contexts
+* `Proposition.Equiv` -- two propositions are logically equivalent relative to a class of models
+* `LogicalEquivalence` -- typeclass instance connecting equivalence, congruence, and validity
 
 ## Design Notes
 
@@ -33,6 +33,27 @@ sub-proposition positions (left and right), and `box` has one. The ground constr
 
 namespace Cslib.Logic.Modal
 
+open scoped InferenceSystem Proposition
+
+/-- Logical equivalence for modal propositions, parametric on a class of models `S`.
+Two propositions are equivalent when they are satisfied by the same model-world pairs in `S`. -/
+def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Prop :=
+  ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]
+
+scoped notation φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂
+
+@[simp]
+theorem Proposition.equiv_def {S : Set (Model World Atom)}
+    {φ₁ φ₂ : Proposition Atom} :
+    (φ₁ ≡[S] φ₂) ↔ ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] :=
+  Iff.rfl
+
+theorem Proposition.equiv_iff {S : Set (Model World Atom)}
+    {φ₁ φ₂ : Proposition Atom}
+    (h : φ₁ ≡[S] φ₂) {m : Model World Atom} (hm : m ∈ S) {w : World} :
+    ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] :=
+  h m hm w
+
 /-- A one-hole context for `Proposition`. Each constructor corresponds to a recursive position
 in `Proposition`: `impL` is the left argument of `imp`, `impR` is the right argument, and `box`
 is the argument of `box`. The `hole` constructor marks the position to be filled. -/
@@ -47,37 +68,73 @@ inductive Proposition.Context (Atom : Type u) : Type u where
   | box (c : Context Atom)
 
 /-- Fill the hole in a context with a proposition. -/
+@[scoped grind =]
 def Proposition.Context.fill : Proposition.Context Atom → Proposition Atom → Proposition Atom
   | .hole, φ => φ
   | .impL c ψ, φ => .imp (c.fill φ) ψ
   | .impR ψ c, φ => .imp ψ (c.fill φ)
   | .box c, φ => .box (c.fill φ)
 
-/-- Two propositions are logically equivalent when they agree on satisfaction across all models
-and worlds. -/
-def LogicallyEquivalent.{v} {Atom : Type u} (φ ψ : Proposition Atom) : Prop :=
-  ∀ (World : Type v) (m : Model World Atom) (w : World), Satisfies m w φ ↔ Satisfies m w ψ
-
-/-- Logical equivalence is a congruence: if `φ` and `ψ` are logically equivalent, then
-`c.fill φ` and `c.fill ψ` are logically equivalent for any context `c`. -/
-theorem LogicallyEquivalent.congruence.{v} {Atom : Type u} {φ ψ : Proposition Atom}
-    (c : Proposition.Context Atom) (h : LogicallyEquivalent.{v} φ ψ) :
-    LogicallyEquivalent.{v} (c.fill φ) (c.fill ψ) := by
-  intro World m
-  induction c with
-  | hole => exact h World m
-  | impL c _ ih =>
-    intro w
-    simp only [Proposition.Context.fill, Satisfies]
-    exact ⟨fun hf ha => hf ((ih w).mpr ha), fun hf ha => hf ((ih w).mp ha)⟩
-  | impR _ c ih =>
-    intro w
-    simp only [Proposition.Context.fill, Satisfies]
-    exact ⟨fun hf ha => (ih w).mp (hf ha), fun hf ha => (ih w).mpr (hf ha)⟩
-  | box c ih =>
-    intro w
-    simp only [Proposition.Context.fill, Satisfies]
-    exact ⟨fun hf w' hr => (ih w').mp (hf w' hr),
-           fun hf w' hr => (ih w').mpr (hf w' hr)⟩
+instance : HasContext (Proposition Atom) :=
+  ⟨Proposition.Context Atom, Proposition.Context.fill⟩
+
+@[simp]
+theorem Proposition.Context.fill_def (c : Proposition.Context Atom) (φ : Proposition Atom) :
+    (c : HasContext.Context (Proposition Atom))<[φ] = c.fill φ := rfl
+
+instance : IsEquiv (Proposition Atom)
+    (Proposition.Equiv (World := World) (S : Set (Model World Atom))) where
+  refl _ _ _ _ := Iff.rfl
+  symm _ _ hab m hm w := (hab m hm w).symm
+  trans _ _ _ hab hbc m hm w := (hab m hm w).trans (hbc m hm w)
+
+instance : Congruence (Proposition Atom)
+    (Proposition.Equiv (World := World) (S : Set (Model World Atom))) where
+  elim := by
+    intro ctx a b hab
+    change Proposition.Equiv S (ctx.fill a) (ctx.fill b)
+    intro m hm
+    induction ctx with
+    | hole => exact hab m hm
+    | impL c _ ih =>
+      intro w
+      simp only [Proposition.Context.fill, derivation_def, Satisfies]
+      exact ⟨fun hf ha => hf ((ih w).mpr ha), fun hf ha => hf ((ih w).mp ha)⟩
+    | impR _ c ih =>
+      intro w
+      simp only [Proposition.Context.fill, derivation_def, Satisfies]
+      exact ⟨fun hf ha => (ih w).mp (hf ha), fun hf ha => (ih w).mpr (hf ha)⟩
+    | box c ih =>
+      intro w
+      simp only [Proposition.Context.fill, derivation_def, Satisfies]
+      exact ⟨fun hf w' hr => (ih w').mp (hf w' hr),
+             fun hf w' hr => (ih w').mpr (hf w' hr)⟩
+
+/-- Judgemental contexts for satisfaction. -/
+structure Satisfies.Context (World : Type*) (Atom : Type*) where
+  /-- The class of models. -/
+  S : Set (Model World Atom)
+  /-- The model. -/
+  m : Model World Atom
+  /-- Evidence that the model belongs to the class. -/
+  hm : m ∈ S
+  /-- The world satisfying the proposition. -/
+  w : World
+
+/-- Fills a judgemental context with a proposition to obtain a judgement. -/
+def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) :
+    Judgement World Atom :=
+  ⟨c.m, c.w, φ⟩
+
+instance : HasHContext (Judgement World Atom) (Proposition Atom) :=
+  ⟨Satisfies.Context World Atom, Satisfies.Context.fill⟩
+
+instance : LogicalEquivalence
+    (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where
+  eqv := Proposition.Equiv Set.univ
+  eqvFillValid heqv c h := by
+    change Satisfies c.m c.w _
+    have h' : Satisfies c.m c.w _ := h
+    exact (heqv c.m (Set.mem_univ _) c.w).mp h'
 
 end Cslib.Logic.Modal