diff --git a/Linglib/Core/Logic/Aristotelian/Square.lean b/Linglib/Core/Logic/Aristotelian/Square.lean
index f43478e71..7bd7dd1fa 100644
--- a/Linglib/Core/Logic/Aristotelian/Square.lean
+++ b/Linglib/Core/Logic/Aristotelian/Square.lean
@@ -58,23 +58,4 @@ theorem SquareRelations.toContraryAE {α : Type*} [BooleanAlgebra α] {sq : Squa
     (rel : SquareRelations sq) (hne : sq.A ⊔ sq.E ≠ ⊤) : IsContrary sq.A sq.E :=
   ⟨rel.contraryAE, fun hc => hne (codisjoint_iff.mp hc)⟩
 
-/-! ### The box-derived square -/
-
-/-- The square of propositions from a box-like operator `box`: `A = box p`,
-`E = box pᶜ`, `I = (box pᶜ)ᶜ`, `O = (box p)ᶜ`. -/
-def Square.fromBox {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) :
-    Square α where
-  A := box p
-  E := box pᶜ
-  I := (box pᶜ)ᶜ
-  O := (box p)ᶜ
-
-theorem fromBox_contradAO {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) :
-    (Square.fromBox box p).A = (Square.fromBox box p).Oᶜ := by
-  simp [Square.fromBox]
-
-theorem fromBox_contradEI {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) :
-    (Square.fromBox box p).E = (Square.fromBox box p).Iᶜ := by
-  simp [Square.fromBox]
-
 end Aristotelian
diff --git a/Linglib/Core/Logic/Intensional/RestrictedModality.lean b/Linglib/Core/Logic/Intensional/RestrictedModality.lean
index 3e146f7a9..207c5f97c 100644
--- a/Linglib/Core/Logic/Intensional/RestrictedModality.lean
+++ b/Linglib/Core/Logic/Intensional/RestrictedModality.lean
@@ -1,6 +1,7 @@
 import Linglib.Core.Logic.Intensional.Defs
 import Linglib.Core.Logic.Intensional.Quantification
 import Linglib.Core.Logic.Intensional.Algebra
+import Linglib.Core.Logic.Aristotelian.Square
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Order.Lattice
@@ -108,6 +109,61 @@ theorem boxR_not_moore (R : AccessRel W) [hS : IsSerial R] [IsTrans W R]
   obtain ⟨v, hv⟩ := hS.serial w
   exact (h v hv).2 (hbbp v hv)
 
+/-! ### Modal square of opposition
+
+@cite{carnielli-pizzi-2008}. The `□`/`◇` pair forms an Aristotelian square
+(`A = □p`, `E = □¬p`, `I = ◇p`, `O = ¬□p`). Under seriality — the modal D axiom
+(`boxR_D`) — it satisfies all six relations of the square of opposition, so every
+serial modality (epistemic, deontic, temporal, doxastic) inherits the square. -/
+
+/-- Under seriality, `□p` and `□¬p` are incompatible: no world satisfies both. -/
+theorem boxR_disjoint_compl (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) :
+    Disjoint (boxR R p) (boxR R pᶜ) := by
+  rw [Pi.disjoint_iff]
+  intro w
+  rw [disjoint_iff_inf_le]
+  rintro ⟨hp, hnp⟩
+  obtain ⟨v, hwv⟩ := hS.serial w
+  exact hnp v hwv (hp v hwv)
+
+/-- Box–diamond duality as an equation of predicates: `◇p = ¬□¬p`. -/
+theorem diamondR_eq_compl_boxR_compl (R : AccessRel W) (p : W → Prop) :
+    diamondR R p = (boxR R pᶜ)ᶜ := by
+  funext w
+  apply propext
+  constructor
+  · rintro ⟨v, hv, hpv⟩ hbox
+    exact hbox v hv hpv
+  · intro h
+    by_contra hne
+    exact h (fun v hv hpv => hne ⟨v, hv, hpv⟩)
+
+/-- The **modal square of opposition** over an accessibility relation `R`
+(@cite{carnielli-pizzi-2008}): `A = □p`, `E = □¬p`, `I = ◇p`, `O = ¬□p`. -/
+def modalSquare (R : AccessRel W) (p : W → Prop) : Aristotelian.Square (W → Prop) where
+  A := boxR R p
+  E := boxR R pᶜ
+  I := diamondR R p
+  O := (boxR R p)ᶜ
+
+/-- The modal square satisfies all six Aristotelian relations whenever `R` is
+**serial**. `subalternAI` is exactly the D axiom (`boxR_D` : `□p → ◇p`); the two
+contradiction diagonals combine `isCompl_compl` with box–diamond duality; and
+contrariety/subcontrariety reduce to `boxR_disjoint_compl`. -/
+theorem modalSquare_relations (R : AccessRel W) [IsSerial R] (p : W → Prop) :
+    Aristotelian.SquareRelations (modalSquare R p) where
+  subalternAI := by rw [Pi.le_def]; exact fun w => boxR_D R p w
+  subalternEO := le_compl_iff_disjoint_right.mpr (boxR_disjoint_compl R p).symm
+  contradAO := isCompl_compl
+  contradEI := by
+    show IsCompl (boxR R pᶜ) (diamondR R p)
+    rw [diamondR_eq_compl_boxR_compl]; exact isCompl_compl
+  contraryAE := boxR_disjoint_compl R p
+  subcontrIO := by
+    show Codisjoint (diamondR R p) ((boxR R p)ᶜ)
+    rw [diamondR_eq_compl_boxR_compl, codisjoint_iff, ← compl_inf,
+        disjoint_iff.mp (boxR_disjoint_compl R p).symm, compl_bot]
+
 -- ════════════════════════════════════════════════════════════════════════
 -- § 2. Monotonicity
 -- ════════════════════════════════════════════════════════════════════════
diff --git a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
index fbb359ccb..08591cb6b 100644
--- a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
+++ b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
@@ -1,5 +1,6 @@
 import Mathlib.Data.Finset.Basic
 import Linglib.Semantics.Entailment.AsymStronger
+import Linglib.Core.Logic.Intensional.Defs
 
 /-!
 # Sauerland's Epistemic Implicature Framework
@@ -44,6 +45,8 @@ categorical side.
 
 namespace Implicature.EpistemicBlocking
 
+open Core.Logic.Intensional (AccessRel boxR diamondR IsSerial)
+
 /-- An epistemic state represents what the speaker knows.
 We model this as a finite set of worlds the speaker considers possible. -/
 structure EpistemicState (W : Type*) where
@@ -69,9 +72,30 @@ instance {W : Type*} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ]
     Decidable (possible e φ) :=
   inferInstanceAs (Decidable (∃ w ∈ e.possible, φ w))
 
-/-- Standard epistemic duality: ¬K¬φ ↔ Pφ. One of five sibling `theorem duality`s
-    (see `Semantics/Modality/Kratzer/Operators.lean::duality` for the
-    unification opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/
+/-! ### `K`/`P` as restricted modality
+
+`knows`/`possible` are `boxR`/`diamondR` over the (world-independent) epistemic
+accessibility `accessFrom e`, which is serial because `e.possible` is nonempty.
+The epistemic square of opposition is then `Core.Logic.Intensional.modalSquare
+(accessFrom e)` with `modalSquare_relations` discharged by this `IsSerial` instance
+— no bespoke square construction. -/
+
+/-- Epistemic accessibility: from any world, the speaker's live possibilities. -/
+def accessFrom {W : Type*} (e : EpistemicState W) : AccessRel W := fun _ w' => w' ∈ e.possible
+
+instance {W : Type*} (e : EpistemicState W) : IsSerial (accessFrom e) := ⟨fun _ => e.nonempty⟩
+
+/-- `K` is `□` over epistemic accessibility. -/
+theorem knows_eq_boxR {W : Type*} (e : EpistemicState W) (φ : W → Prop) (w : W) :
+    knows e φ = boxR (accessFrom e) φ w := rfl
+
+/-- `P` is `◇` over epistemic accessibility. -/
+theorem possible_eq_diamondR {W : Type*} (e : EpistemicState W) (φ : W → Prop) (w : W) :
+    possible e φ = diamondR (accessFrom e) φ w := rfl
+
+/-- Standard epistemic duality: ¬K¬φ ↔ Pφ. One of five sibling `theorem duality`s —
+    the box–diamond duality underlying the modal square of opposition
+    (`Core.Logic.Intensional.modalSquare_relations`). -/
 theorem duality {W : Type*} (e : EpistemicState W) (φ : W → Prop) :
     ¬ knows e (fun w => ¬ φ w) ↔ possible e φ := by
   simp only [knows, possible, not_forall, not_not, exists_prop]
diff --git a/Linglib/Semantics/Modality/BiasedPQ.lean b/Linglib/Semantics/Modality/BiasedPQ.lean
index 9b7375897..d2525fe7b 100644
--- a/Linglib/Semantics/Modality/BiasedPQ.lean
+++ b/Linglib/Semantics/Modality/BiasedPQ.lean
@@ -327,9 +327,9 @@ def evidentialNecessity (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop
 def evidentialPossibility (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop :=
   possibility f.contextBase f.stereotypical p w
 
-/-- □_ev satisfies modal duality. One of five sibling `theorem duality`s
-    (see `Modality/Kratzer/Operators.lean::duality` for the unification
-    opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/
+/-- □_ev satisfies modal duality. One of five sibling `theorem duality`s — the
+    box–diamond duality underlying the modal square of opposition
+    (`Core.Logic.Intensional.modalSquare_relations`). -/
 theorem evidentialBias_duality (f : EvidentialBiasFlavor W) (p : Set W) (w : W) :
     evidentialNecessity f p w ↔ ¬ evidentialPossibility f (fun w' => ¬ p w') w := by
   unfold evidentialNecessity evidentialPossibility
diff --git a/Linglib/Semantics/Modality/EventRelativity.lean b/Linglib/Semantics/Modality/EventRelativity.lean
index d244d85aa..53e09ae5b 100644
--- a/Linglib/Semantics/Modality/EventRelativity.lean
+++ b/Linglib/Semantics/Modality/EventRelativity.lean
@@ -138,9 +138,9 @@ instance {Event W : Type*} (f : AnchoringFn Event W) (e : Event)
     Decidable (necessity f e allW p w) :=
   inferInstanceAs (Decidable (∀ _ ∈ _, _))
 
-/-- Duality: □_{f(e)} p ↔ ¬◇_{f(e)} ¬p. One of five sibling `theorem duality`s
-    (see `Semantics/Modality/Kratzer/Operators.lean::duality` for the
-    unification opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/
+/-- Duality: □_{f(e)} p ↔ ¬◇_{f(e)} ¬p. One of five sibling `theorem duality`s —
+    the box–diamond duality underlying the modal square of opposition
+    (`Core.Logic.Intensional.modalSquare_relations`). -/
 theorem duality {Event W : Type*} (f : AnchoringFn Event W) (e : Event)
     (allW : List W) (p : W → Prop) [DecidablePred p] (w : W) :
     necessity f e allW p w ↔ ¬ possibility f e allW (λ w' => ¬ p w') w := by
diff --git a/Linglib/Semantics/Modality/Kratzer/Operators.lean b/Linglib/Semantics/Modality/Kratzer/Operators.lean
index 61a173a09..0a9006994 100644
--- a/Linglib/Semantics/Modality/Kratzer/Operators.lean
+++ b/Linglib/Semantics/Modality/Kratzer/Operators.lean
@@ -144,7 +144,9 @@ theorem empty_base_universal_access (w : W) :
 
 /-! ### Modal axioms (from `RestrictedModality`) -/
 
-/-- **Modal duality**: `□p ↔ ¬◇¬p`. -/
+/-- **Modal duality**: `□p ↔ ¬◇¬p`. Since `necessity = boxR (kratzerBestR f g)`,
+    this is the box–diamond duality of the modal square of opposition
+    (`Core.Logic.Intensional.modalSquare_relations`). -/
 theorem duality (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) :
     necessity f g p w ↔ ¬ possibility f g (fun w' => ¬ p w') w := by
   rw [necessity, possibility, boxR_neg_diamondR]
diff --git a/Linglib/Semantics/Modality/Temporal.lean b/Linglib/Semantics/Modality/Temporal.lean
index baf3a0515..6e107776a 100644
--- a/Linglib/Semantics/Modality/Temporal.lean
+++ b/Linglib/Semantics/Modality/Temporal.lean
@@ -96,9 +96,9 @@ theorem temporal_eq_static {Time : Type*}
     necessity f g p w :=
   Iff.rfl
 
-/-- Temporal duality: □ₜp ↔ ¬◇ₜ¬p. One of five sibling `theorem duality`s
-    (see `Modality/Kratzer/Operators.lean::duality` for the unification
-    opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/
+/-- Temporal duality: □ₜp ↔ ¬◇ₜ¬p. One of five sibling `theorem duality`s — the
+    box–diamond duality underlying the modal square of opposition
+    (`Core.Logic.Intensional.modalSquare_relations`). -/
 theorem temporal_duality {Time : Type*}
     (f : TemporalModalBase W Time) (g : TemporalOrderingSource W Time)
     (t : Time) (p : W → Prop) (w : W) :
diff --git a/blog/references.bib b/blog/references.bib
index bf43b50ca..adffb7c6e 100644
--- a/blog/references.bib
+++ b/blog/references.bib
@@ -34,6 +34,20 @@ @inproceedings{spinoso-di-piano-etal-2025
   role      = {formalized},
   sources   = {Phenomena/Nonliteral/Irony/Studies/SpinosoDiPiano2025.lean}
 }
+@book{carnielli-pizzi-2008,
+  author    = {Carnielli, Walter and Pizzi, Claudio},
+  year      = {2008},
+  title     = {Modalities and Multimodalities},
+  publisher = {Springer},
+  series    = {Logic, Epistemology, and the Unity of Science},
+  volume    = {12},
+  doi       = {10.1007/978-1-4020-8590-1},
+  isbn      = {9781402085901},
+  subfield  = {semantics/modality},
+  role      = {cited},
+  sources   = {Core/Logic/Intensional/RestrictedModality.lean}
+}
+
 @book{cover-thomas-2006,
   author    = {Cover, Thomas M. and Thomas, Joy A.},
   year      = {2006},