diff --git a/Linglib.lean b/Linglib.lean
index bec650168..2088303dd 100644
--- a/Linglib.lean
+++ b/Linglib.lean
@@ -59,11 +59,11 @@ import Linglib.Core.Logic.Intensional.Rigidity
 import Linglib.Core.Logic.Intensional.Frame
 import Linglib.Core.Logic.Intensional.Variables
 import Linglib.Core.Logic.Intensional.Conjunction
-import Linglib.Core.Logic.Intensional.Defs
+import Linglib.Core.Logic.Modal.Defs
 import Linglib.Core.Logic.Intensional.Quantification
 import Linglib.Core.Logic.Intensional.Algebra
 import Linglib.Core.Logic.Intensional.CategoryType
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Core.Logic.Intensional.Premise
 import Linglib.Semantics.Modality.Kratzer.ConversationalBackground
 import Linglib.Core.Logic.Intensional.Situations
@@ -644,7 +644,6 @@ import Linglib.Fragments.English.TemporalDeictic
 import Linglib.Fragments.English.TemporalExpressions
 import Linglib.Fragments.English.Conditionals
 import Linglib.Fragments.English.Phonology
-import Linglib.Fragments.English.TDDeletion
 import Linglib.Fragments.English.Relativization
 import Linglib.Fragments.English.Morph
 import Linglib.Fragments.English.Negation
diff --git a/Linglib/Core/Logic/Modal/BSML/Bridge.lean b/Linglib/Core/Logic/Modal/BSML/Bridge.lean
index 8753a3f5d..4643507b5 100644
--- a/Linglib/Core/Logic/Modal/BSML/Bridge.lean
+++ b/Linglib/Core/Logic/Modal/BSML/Bridge.lean
@@ -1,5 +1,5 @@
 import Linglib.Core.Logic.Modal.BSML.Defs
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 
 /-!
 # BSML–CML Bridge
@@ -217,7 +217,7 @@ theorem neFree_flat (M : BSMLModel W Atom)
 -- §5: BSML–CML Type Bridge
 -- ============================================================================
 
-open Core.Logic.Intensional (diamondR)
+open Core.Logic.Modal (diamond)
 
 /-!
 ### Accessibility Type Bridge
@@ -231,16 +231,16 @@ canonical accessibility-relation type in
 /-- Convert BSML accessibility (`Finset`-valued) to a classical Prop-valued
     accessibility relation. -/
 def BSMLModel.toAccessRel (M : BSMLModel W Atom) :
-    Core.Logic.Intensional.AccessRel W :=
+    Core.Logic.Modal.AccessRel W :=
   fun w v => v ∈ M.access w
 
-/-- `classicalEval` of ◇φ agrees with `diamondR` (Prop-valued possibility),
+/-- `classicalEval` of ◇φ agrees with `diamond` (Prop-valued possibility),
     connecting BSML's classical evaluation to the shared modal logic
     infrastructure from `Core.Logic.Intensional`. -/
-theorem classicalEval_agrees_diamondR_poss
+theorem classicalEval_agrees_diamond_poss
     (M : BSMLModel W Atom) (φ : BSMLFormula Atom) (w : W) :
     classicalEval M (.poss φ) w = true ↔
-    diamondR M.toAccessRel (fun v => classicalEval M φ v = true) w := by
-  simp only [classicalEval, decide_eq_true_eq, diamondR, BSMLModel.toAccessRel]
+    diamond M.toAccessRel (fun v => classicalEval M φ v = true) w := by
+  simp only [classicalEval, decide_eq_true_eq, diamond, BSMLModel.toAccessRel]
 
 end Core.Logic.Modal.BSML
diff --git a/Linglib/Core/Logic/Intensional/RestrictedModality.lean b/Linglib/Core/Logic/Modal/Basic.lean
similarity index 68%
rename from Linglib/Core/Logic/Intensional/RestrictedModality.lean
rename to Linglib/Core/Logic/Modal/Basic.lean
index 207c5f97c..95f75e041 100644
--- a/Linglib/Core/Logic/Intensional/RestrictedModality.lean
+++ b/Linglib/Core/Logic/Modal/Basic.lean
@@ -1,6 +1,4 @@
-import Linglib.Core.Logic.Intensional.Defs
-import Linglib.Core.Logic.Intensional.Quantification
-import Linglib.Core.Logic.Intensional.Algebra
+import Linglib.Core.Logic.Modal.Defs
 import Linglib.Core.Logic.Aristotelian.Square
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Fintype.Basic
@@ -8,21 +6,21 @@ import Mathlib.Order.Lattice
 import Mathlib.Order.BoundedOrder.Basic
 
 /-!
-# Restricted Modality: Modal Axioms, Decidability, Logic Lattice, Gallin Hierarchy
+# Modal logic: axioms, the lattice of normal logics, and the modal square
 
 @cite{dowty-wall-peters-1981} @cite{kratzer-1981} @cite{kripke-1963}
 
 Builds on the polymorphic Kripke foundation in `Defs.lean`. This file adds:
 
 1. **Modal axiom correspondence** (T, D, 4, B, 5): which frame conditions on
-   `R` validate which modal axioms when interpreted via `boxR`/`diamondR`.
+   `R` validate which modal axioms when interpreted via `box`/`diamond`.
    The K axiom holds for any `R`.
 
 2. **Monotonicity, distribution, restriction**: standard properties of
-   normal modal operators. Restriction (`boxR_restrict`) is Kratzer's
+   normal modal operators. Restriction (`box_restrict`) is Kratzer's
    insight that conversational backgrounds *strengthen* necessity.
 
-3. **Decidable instances**: `boxR R p w`, `diamondR R p w` are decidable
+3. **Decidable instances**: `box R p w`, `diamond R p w` are decidable
    over finite worlds with decidable accessibility and propositions.
 
 4. **Logic lattice**: `Axiom`, `Logic`, named logics (K, T, D, S4, S5, KD45),
@@ -35,9 +33,9 @@ Builds on the polymorphic Kripke foundation in `Defs.lean`. This file adds:
    of the polymorphic theory, and that non-Kripke operators (tense,
    progressive) live outside `IsIndicial`.
 
-6. **IL Frame specialization**: with universal accessibility, `boxR`/`diamondR`
-   recover S5 `box`/`diamond` from `Quantification.lean` — the formal
-   bridge that the polymorphic theory contains classical IL as a special case.
+6. **Modal square of opposition** (`modalSquare`, @cite{carnielli-pizzi-2008}):
+   under seriality the `box`/`diamond` corners satisfy all six Aristotelian
+   relations — `subalternAI` is the D axiom, `contradEI` the box–diamond duality.
 
 ## Connection to Kratzer semantics
 
@@ -45,12 +43,12 @@ Kratzer's conversational backgrounds derive accessibility from a modal base:
 `R_f(w, w') ≡ w' ∈ ⋂f(w)`. The ordering source further restricts to "best"
 worlds. In IL terms:
 
-- Simple Kratzer necessity = `boxR R_f` (no ordering source)
-- Full Kratzer necessity = `boxR R_{f,g}` where `R_{f,g}` restricts to best worlds
-- S5 necessity = `boxR (fun _ _ => True)` = `box`
+- Simple Kratzer necessity = `box R_f` (no ordering source)
+- Full Kratzer necessity = `box R_{f,g}` where `R_{f,g}` restricts to best worlds
+- S5 necessity = `box universalR`
 -/
 
-namespace Core.Logic.Intensional
+namespace Core.Logic.Modal
 
 variable {W : Type*}
 
@@ -60,39 +58,39 @@ variable {W : Type*}
 
 /-- **K axiom**: `□_R(p → q) → (□_R p → □_R q)`.
     Holds for any accessibility relation. -/
-theorem boxR_K (R : AccessRel W) (p q : W → Prop) (w : W)
-    (hpq : boxR R (fun v => p v → q v) w)
-    (hp : boxR R p w) : boxR R q w :=
+theorem box_K (R : AccessRel W) (p q : W → Prop) (w : W)
+    (hpq : box R (fun v => p v → q v) w)
+    (hp : box R p w) : box R q w :=
   fun v hwv => hpq v hwv (hp v hwv)
 
 /-- **T axiom**: reflexive `R` gives `□_R p w → p w`.
     What is necessary is actual. -/
-theorem boxR_T (R : AccessRel W) [Std.Refl R] (p : W → Prop) (w : W)
-    (h : boxR R p w) : p w :=
+theorem box_T (R : AccessRel W) [Std.Refl R] (p : W → Prop) (w : W)
+    (h : box R p w) : p w :=
   h w (Std.Refl.refl w)
 
 /-- **D axiom**: serial `R` gives `□_R p w → ◇_R p w`.
     What is necessary is possible. -/
-theorem boxR_D (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) (w : W)
-    (h : boxR R p w) : diamondR R p w :=
+theorem box_D (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) (w : W)
+    (h : box R p w) : diamond R p w :=
   let ⟨v, hwv⟩ := hS.serial w; ⟨v, hwv, h v hwv⟩
 
 /-- **4 axiom**: transitive `R` gives `□_R p → □_R □_R p`.
     Positive introspection. -/
-theorem boxR_four (R : AccessRel W) [IsTrans W R] (p : W → Prop) (w : W)
-    (h : boxR R p w) : boxR R (boxR R p) w :=
+theorem box_four (R : AccessRel W) [IsTrans W R] (p : W → Prop) (w : W)
+    (h : box R p w) : box R (box R p) w :=
   fun v hwv u hvu => h u (IsTrans.trans w v u hwv hvu)
 
 /-- **B axiom**: symmetric `R` gives `p w → □_R ◇_R p w`.
     What is actual is necessarily possible. -/
-theorem boxR_B (R : AccessRel W) [Std.Symm R] (p : W → Prop) (w : W)
-    (h : p w) : boxR R (diamondR R p) w :=
+theorem box_B (R : AccessRel W) [Std.Symm R] (p : W → Prop) (w : W)
+    (h : p w) : box R (diamond R p) w :=
   fun v hwv => ⟨w, Std.Symm.symm w v hwv, h⟩
 
 /-- **5 axiom**: euclidean `R` gives `◇_R p w → □_R ◇_R p w`.
     Positive possibility introspection. -/
-theorem boxR_five (R : AccessRel W) [hE : IsEuclidean R] (p : W → Prop) (w : W)
-    (h : diamondR R p w) : boxR R (diamondR R p) w :=
+theorem box_five (R : AccessRel W) [hE : IsEuclidean R] (p : W → Prop) (w : W)
+    (h : diamond R p w) : box R (diamond R p) w :=
   let ⟨u, hwu, hpu⟩ := h
   fun v hwv => ⟨u, hE.eucl w v u hwv hwu, hpu⟩
 
@@ -100,12 +98,12 @@ theorem boxR_five (R : AccessRel W) [hE : IsEuclidean R] (p : W → Prop) (w : W
     `R` is serial and transitive. The content `p ∧ ¬□_R p` is itself
     satisfiable; what fails is *boxing* it. Specialise to belief
     (@cite{hintikka-1962}), knowledge, or any other KD4 modality. -/
-theorem boxR_not_moore (R : AccessRel W) [hS : IsSerial R] [IsTrans W R]
+theorem box_not_moore (R : AccessRel W) [hS : IsSerial R] [IsTrans W R]
     (p : W → Prop) (w : W) :
-    ¬ boxR R (fun v => p v ∧ ¬ boxR R p v) w := by
+    ¬ box R (fun v => p v ∧ ¬ box R p v) w := by
   intro h
-  have hbp : boxR R p w := fun v hwv => (h v hwv).1
-  have hbbp : boxR R (boxR R p) w := boxR_four R p w hbp
+  have hbp : box R p w := fun v hwv => (h v hwv).1
+  have hbbp : box R (box R p) w := box_four R p w hbp
   obtain ⟨v, hv⟩ := hS.serial w
   exact (h v hv).2 (hbbp v hv)
 
@@ -113,12 +111,12 @@ theorem boxR_not_moore (R : AccessRel W) [hS : IsSerial R] [IsTrans W R]
 
 @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
+(`box_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
+theorem box_disjoint_compl (R : AccessRel W) [hS : IsSerial R] (p : W → Prop) :
+    Disjoint (box R p) (box R pᶜ) := by
   rw [Pi.disjoint_iff]
   intro w
   rw [disjoint_iff_inf_le]
@@ -127,8 +125,8 @@ theorem boxR_disjoint_compl (R : AccessRel W) [hS : IsSerial R] (p : W → Prop)
   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
+theorem diamond_eq_compl_box_compl (R : AccessRel W) (p : W → Prop) :
+    diamond R p = (box R pᶜ)ᶜ := by
   funext w
   apply propext
   constructor
@@ -141,43 +139,43 @@ theorem diamondR_eq_compl_boxR_compl (R : AccessRel W) (p : W → Prop) :
 /-- 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)ᶜ
+  A := box R p
+  E := box R pᶜ
+  I := diamond R p
+  O := (box 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
+**serial**. `subalternAI` is exactly the D axiom (`box_D` : `□p → ◇p`); the two
 contradiction diagonals combine `isCompl_compl` with box–diamond duality; and
-contrariety/subcontrariety reduce to `boxR_disjoint_compl`. -/
+contrariety/subcontrariety reduce to `box_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
+  subalternAI := by rw [Pi.le_def]; exact fun w => box_D R p w
+  subalternEO := le_compl_iff_disjoint_right.mpr (box_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
+    show IsCompl (box R pᶜ) (diamond R p)
+    rw [diamond_eq_compl_box_compl]; exact isCompl_compl
+  contraryAE := box_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]
+    show Codisjoint (diamond R p) ((box R p)ᶜ)
+    rw [diamond_eq_compl_box_compl, codisjoint_iff, ← compl_inf,
+        disjoint_iff.mp (box_disjoint_compl R p).symm, compl_bot]
 
 -- ════════════════════════════════════════════════════════════════════════
 -- § 2. Monotonicity
 -- ════════════════════════════════════════════════════════════════════════
 
-/-- `boxR R` is monotone: if `p ≤ q` pointwise, then `□_R p ≤ □_R q`. -/
-theorem boxR_mono (R : AccessRel W) {p q : W → Prop}
+/-- `box R` is monotone: if `p ≤ q` pointwise, then `□_R p ≤ □_R q`. -/
+theorem box_mono (R : AccessRel W) {p q : W → Prop}
     (h : ∀ v, p v → q v) (w : W)
-    (hb : boxR R p w) : boxR R q w :=
+    (hb : box R p w) : box R q w :=
   fun v hwv => h v (hb v hwv)
 
-/-- `diamondR R` is monotone. -/
-theorem diamondR_mono (R : AccessRel W) {p q : W → Prop}
+/-- `diamond R` is monotone. -/
+theorem diamond_mono (R : AccessRel W) {p q : W → Prop}
     (h : ∀ v, p v → q v) (w : W)
-    (hd : diamondR R p w) : diamondR R q w :=
+    (hd : diamond R p w) : diamond R q w :=
   let ⟨v, hwv, hpv⟩ := hd; ⟨v, hwv, h v hpv⟩
 
 -- ════════════════════════════════════════════════════════════════════════
@@ -185,24 +183,24 @@ theorem diamondR_mono (R : AccessRel W) {p q : W → Prop}
 -- ════════════════════════════════════════════════════════════════════════
 
 /-- `□_R` distributes over `∧`. -/
-theorem boxR_conj (R : AccessRel W) (p q : W → Prop) (w : W) :
-    boxR R (fun v => p v ∧ q v) w =
-    (boxR R p w ∧ boxR R q w) := by
+theorem box_conj (R : AccessRel W) (p q : W → Prop) (w : W) :
+    box R (fun v => p v ∧ q v) w =
+    (box R p w ∧ box R q w) := by
   exact propext ⟨fun h => ⟨fun v hwv => (h v hwv).1, fun v hwv => (h v hwv).2⟩,
                   fun ⟨hp, hq⟩ v hwv => ⟨hp v hwv, hq v hwv⟩⟩
 
 /-- `◇_R` distributes over `∨`. -/
-theorem diamondR_disj (R : AccessRel W) (p q : W → Prop) (w : W) :
-    diamondR R (fun v => p v ∨ q v) w =
-    (diamondR R p w ∨ diamondR R q w) := by
+theorem diamond_disj (R : AccessRel W) (p q : W → Prop) (w : W) :
+    diamond R (fun v => p v ∨ q v) w =
+    (diamond R p w ∨ diamond R q w) := by
   exact propext ⟨
     fun ⟨v, hwv, h⟩ => h.elim (fun hp => .inl ⟨v, hwv, hp⟩) (fun hq => .inr ⟨v, hwv, hq⟩),
     fun h => h.elim (fun ⟨v, hwv, hp⟩ => ⟨v, hwv, .inl hp⟩)
                      (fun ⟨v, hwv, hq⟩ => ⟨v, hwv, .inr hq⟩)⟩
 
 /-- Necessitation: if `p` holds at every world, then `□_R p` holds everywhere. -/
-theorem boxR_necessitation (R : AccessRel W) (p : W → Prop)
-    (h : ∀ v, p v) (w : W) : boxR R p w :=
+theorem box_necessitation (R : AccessRel W) (p : W → Prop)
+    (h : ∀ v, p v) (w : W) : box R p w :=
   fun v _ => h v
 
 -- ════════════════════════════════════════════════════════════════════════
@@ -211,16 +209,16 @@ theorem boxR_necessitation (R : AccessRel W) (p : W → Prop)
 
 /-- Restricting accessibility strengthens necessity:
     if `R₂ ⊆ R₁`, then `□_{R₁} p → □_{R₂} p`. -/
-theorem boxR_restrict {R₁ R₂ : AccessRel W}
+theorem box_restrict {R₁ R₂ : AccessRel W}
     (h : ∀ w v, R₂ w v → R₁ w v) (p : W → Prop) (w : W)
-    (hb : boxR R₁ p w) : boxR R₂ p w :=
+    (hb : box R₁ p w) : box R₂ p w :=
   fun v hwv => hb v (h w v hwv)
 
 /-- Restricting accessibility weakens possibility:
     if `R₂ ⊆ R₁`, then `◇_{R₂} p → ◇_{R₁} p`. -/
-theorem diamondR_restrict {R₁ R₂ : AccessRel W}
+theorem diamond_restrict {R₁ R₂ : AccessRel W}
     (h : ∀ w v, R₂ w v → R₁ w v) (p : W → Prop) (w : W)
-    (hd : diamondR R₂ p w) : diamondR R₁ p w :=
+    (hd : diamond R₂ p w) : diamond R₁ p w :=
   let ⟨v, hwv, hpv⟩ := hd; ⟨v, h w v hwv, hpv⟩
 
 -- ════════════════════════════════════════════════════════════════════════
@@ -228,29 +226,29 @@ theorem diamondR_restrict {R₁ R₂ : AccessRel W}
 -- ════════════════════════════════════════════════════════════════════════
 
 /-- With reflexive + euclidean accessibility (= S5 frame conditions),
-    `boxR` validates all of T, D, 4, B, 5. -/
+    `box` validates all of T, D, 4, B, 5. -/
 theorem S5_frame_all_axioms (R : AccessRel W) [Std.Refl R] [IsEuclidean R] :
-    (∀ p w, boxR R p w → p w) ∧                          -- T
-    (∀ p w, boxR R p w → diamondR R p w) ∧               -- D
-    (∀ p w, boxR R p w → boxR R (boxR R p) w) ∧          -- 4
-    (∀ p w, p w → boxR R (diamondR R p) w) ∧             -- B
-    (∀ p w, diamondR R p w → boxR R (diamondR R p) w) := -- 5
-  ⟨boxR_T R, boxR_D R, boxR_four R, boxR_B R, boxR_five R⟩
+    (∀ p w, box R p w → p w) ∧                          -- T
+    (∀ p w, box R p w → diamond R p w) ∧               -- D
+    (∀ p w, box R p w → box R (box R p) w) ∧          -- 4
+    (∀ p w, p w → box R (diamond R p) w) ∧             -- B
+    (∀ p w, diamond R p w → box R (diamond R p) w) := -- 5
+  ⟨box_T R, box_D R, box_four R, box_B R, box_five R⟩
 
 /-- KD45 frame conditions validate all three KD45 axioms (D, 4, 5). -/
 theorem KD45_frame_all_axioms (R : AccessRel W) [IsKD45Frame R] :
-    (∀ p w, boxR R p w → diamondR R p w) ∧               -- D
-    (∀ p w, boxR R p w → boxR R (boxR R p) w) ∧          -- 4
-    (∀ p w, diamondR R p w → boxR R (diamondR R p) w) := -- 5
-  ⟨boxR_D R, boxR_four R, boxR_five R⟩
+    (∀ p w, box R p w → diamond R p w) ∧               -- D
+    (∀ p w, box R p w → box R (box R p) w) ∧          -- 4
+    (∀ p w, diamond R p w → box R (diamond R p) w) := -- 5
+  ⟨box_D R, box_four R, box_five R⟩
 
-/-- `boxR R p i` is the infimum of `p v` over worlds `v` accessible from `w`. -/
-theorem boxR_eq_forall (R : AccessRel W) (p : W → Prop) (w : W) :
-    boxR R p w = (∀ v, R w v → p v) := rfl
+/-- `box R p i` is the infimum of `p v` over worlds `v` accessible from `w`. -/
+theorem box_eq_forall (R : AccessRel W) (p : W → Prop) (w : W) :
+    box R p w = (∀ v, R w v → p v) := rfl
 
-/-- `diamondR R p w` is the supremum of `p v` over worlds `v` accessible from `w`. -/
-theorem diamondR_eq_exists (R : AccessRel W) (p : W → Prop) (w : W) :
-    diamondR R p w = (∃ v, R w v ∧ p v) := rfl
+/-- `diamond R p w` is the supremum of `p v` over worlds `v` accessible from `w`. -/
+theorem diamond_eq_exists (R : AccessRel W) (p : W → Prop) (w : W) :
+    diamond R p w = (∃ v, R w v ∧ p v) := rfl
 
 -- ════════════════════════════════════════════════════════════════════════
 -- § 6. Gallin's Hierarchy of Propositional Operators
@@ -264,8 +262,8 @@ In IL/ML_p, propositional operators form a three-level hierarchy:
    properties of propositions, varying by world.
 
 2. **Indicial** (= Kripke-type): Operators definable via an accessibility
-   relation `R`. The necessity variant is `∀ v, R w v → p v` (= `boxR`);
-   the possibility variant is `∃ v, R w v ∧ p v` (= `diamondR`).
+   relation `R`. The necessity variant is `∀ v, R w v → p v` (= `box`);
+   the possibility variant is `∃ v, R w v ∧ p v` (= `diamond`).
 
 3. **S5**: The indicial case with `R = universalR` — IL's `box`/`diamond`.
 
@@ -277,10 +275,10 @@ All PropOps  ⊋  Indicial (Kripke)  ⊋  S5 (IL's □)
 theorems are the *architectural anchor* for the design choice that
 restricted modality lives in `Core/Logic/Intensional/`: they prove that
 classical IL S5 is exactly the universal-accessibility special case of
-the polymorphic theory, and that every `boxR R` is a normal modal
+the polymorphic theory, and that every `box R` is a normal modal
 operator (monotone, distribConj). Non-indicial PropOps (e.g., tense,
 present progressive) are the formal extension point for tense /
-non-Kripke modal operators that *cannot* be expressed as `boxR R` for
+non-Kripke modal operators that *cannot* be expressed as `box R` for
 any `R`. Removing this section would erase the formal record of why
 the directory layout is what it is.
 -/
@@ -293,7 +291,7 @@ the directory layout is what it is.
     parametrized by world. This is Gallin's most general level —
     an arbitrary property of propositions varying by index.
 
-    Examples: necessity (`boxR R`), possibility (`diamondR R`),
+    Examples: necessity (`box R`), possibility (`diamond R`),
     past tense (`∃ v, v < w ∧ p v`), present progressive, habituals. -/
 abbrev PropOp (W : Type*) := (W → Prop) → W → Prop
 
@@ -316,7 +314,7 @@ def PropOp.DistribConj {W : Type*} (N : PropOp W) : Prop :=
     operators definable via an accessibility relation.
     `indicialNec R p w ↔ ∀ v, R w v → p v`.
 
-    This is `boxR` viewed as a member of the Gallin hierarchy. -/
+    This is `box` viewed as a member of the Gallin hierarchy. -/
 def indicialNec {W : Type*} (R : AccessRel W) : PropOp W :=
   fun p w => ∀ v, R w v → p v
 
@@ -325,13 +323,13 @@ def indicialNec {W : Type*} (R : AccessRel W) : PropOp W :=
 def indicialPoss {W : Type*} (R : AccessRel W) : PropOp W :=
   fun p w => ∃ v, R w v ∧ p v
 
-/-- `boxR` IS `indicialNec` — definitional equality. -/
-theorem boxR_eq_indicialNec (R : AccessRel W) :
-    boxR R = indicialNec R := rfl
+/-- `box` IS `indicialNec` — definitional equality. -/
+theorem box_eq_indicialNec (R : AccessRel W) :
+    box R = indicialNec R := rfl
 
-/-- `diamondR` IS `indicialPoss` — definitional equality. -/
-theorem diamondR_eq_indicialPoss (R : AccessRel W) :
-    diamondR R = indicialPoss R := rfl
+/-- `diamond` IS `indicialPoss` — definitional equality. -/
+theorem diamond_eq_indicialPoss (R : AccessRel W) :
+    diamond R = indicialPoss R := rfl
 
 /-- A propositional operator is **indicial** if there exists an accessibility
     relation `R` such that `N = indicialNec R`. The non-indicial case is
@@ -339,8 +337,8 @@ theorem diamondR_eq_indicialPoss (R : AccessRel W) :
 def IsIndicial {W : Type*} (N : PropOp W) : Prop :=
   ∃ R : AccessRel W, N = indicialNec R
 
-/-- Every `boxR R` is indicial. -/
-theorem boxR_isIndicial (R : AccessRel W) : IsIndicial (boxR R) :=
+/-- Every `box R` is indicial. -/
+theorem box_isIndicial (R : AccessRel W) : IsIndicial (box R) :=
   ⟨R, rfl⟩
 
 /-- Every indicial operator is monotone (every Kripke operator is a
@@ -403,21 +401,21 @@ theorem indicialNec_emptyR (p : W → Prop) (w : W) :
 
 /-! ### Decidability over finite worlds -/
 
-/-- `boxR R p w` is decidable when worlds enumerate, accessibility is decidable,
+/-- `box R p w` is decidable when worlds enumerate, accessibility is decidable,
     and the proposition is decidable. -/
-instance boxR_decidable {W : Type*} [Fintype W]
+instance box_decidable {W : Type*} [Fintype W]
     (R : AccessRel W) (p : W → Prop) (w : W)
     [∀ v, Decidable (R w v)] [DecidablePred p] :
-    Decidable (boxR R p w) :=
+    Decidable (box R p w) :=
   decidable_of_iff (∀ v ∈ (Finset.univ : Finset W), R w v → p v)
     ⟨fun h v hwv => h v (Finset.mem_univ v) hwv,
      fun h v _ hwv => h v hwv⟩
 
-/-- `diamondR R p w` is decidable under the same conditions as `boxR`. -/
-instance diamondR_decidable {W : Type*} [Fintype W]
+/-- `diamond R p w` is decidable under the same conditions as `box`. -/
+instance diamond_decidable {W : Type*} [Fintype W]
     (R : AccessRel W) (p : W → Prop) (w : W)
     [∀ v, Decidable (R w v)] [DecidablePred p] :
-    Decidable (diamondR R p w) :=
+    Decidable (diamond R p w) :=
   decidable_of_iff (∃ v ∈ (Finset.univ : Finset W), R w v ∧ p v)
     ⟨fun ⟨v, _, hwv, hpv⟩ => ⟨v, hwv, hpv⟩,
      fun ⟨v, hwv, hpv⟩ => ⟨v, Finset.mem_univ v, hwv, hpv⟩⟩
@@ -527,61 +525,4 @@ def frameConditions {W : Type*} (L : Logic) (R : AccessRel W) : Prop :=
 
 end Logic
 
--- ════════════════════════════════════════════════════════════════════════
--- § 9. IL Frame Specialization
--- ════════════════════════════════════════════════════════════════════════
-
-/-! Bridge theorems connecting the polymorphic infrastructure to Montague's IL.
-With universal accessibility, `boxR`/`diamondR` recover S5 `box`/`diamond`
-from `Quantification.lean`. These would all be `rfl` if `box`/`diamond` were
-definitionally `boxR universalR ∘ pick-an-index` — see the Quantification module
-for the layering question. As stated they're one-step `simp` proofs. -/
-
-section FrameSpecialization
-
-variable {F : Frame}
-
-/-- S5 necessity (`box`) is restricted necessity with universal accessibility. -/
-theorem boxR_universal (p : F.Denot .prop) :
-    (fun i => boxR (universalR (W := F.Index)) p i) = (fun _ => box (F := F) p) := by
-  ext i
-  simp only [boxR, universalR, box, forall_true_left]
-
-/-- S5 possibility (`diamond`) is restricted possibility with universal accessibility. -/
-theorem diamondR_universal (p : F.Denot .prop) :
-    (fun i => diamondR (universalR (W := F.Index)) p i) = (fun _ => diamond (F := F) p) := by
-  ext i
-  simp only [diamondR, universalR, diamond, true_and]
-
-/-- S5 box implies any restricted box. -/
-theorem box_implies_boxR (R : AccessRel F.Index) (p : F.Denot .prop)
-    (h : box (F := F) p) (i : F.Index) : boxR R p i :=
-  fun v _ => h v
-
-/-- Any restricted diamond implies S5 diamond. -/
-theorem diamondR_implies_diamond (R : AccessRel F.Index) (p : F.Denot .prop) (i : F.Index)
-    (h : diamondR R p i) : diamond (F := F) p :=
-  let ⟨v, _, hpv⟩ := h; ⟨v, hpv⟩
-
--- ────────────────────────────────────────────────────────────────
--- §9.1 Entailment with Restricted Modality
--- ────────────────────────────────────────────────────────────────
-
-open Algebra (valid entails trueAt)
-
-/-- A valid proposition is R-necessary at every world (for any R). -/
-theorem valid_boxR (R : AccessRel F.Index) (p : F.Denot .prop)
-    (hv : valid (F := F) p) (i : F.Index) : boxR R p i :=
-  fun v _ => hv v
-
-/-- Semantic entailment lifts to restricted modality:
-    if `p ⊨ q` then `□_R p ⊨ □_R q`. -/
-theorem boxR_entailment_lift (R : AccessRel F.Index)
-    (p q : F.Denot .prop)
-    (h : ∀ v, p v → q v)
-    (i : F.Index) (hb : boxR R p i) : boxR R q i :=
-  boxR_mono R h i hb
-
-end FrameSpecialization
-
-end Core.Logic.Intensional
+end Core.Logic.Modal
diff --git a/Linglib/Core/Logic/Intensional/Defs.lean b/Linglib/Core/Logic/Modal/Defs.lean
similarity index 86%
rename from Linglib/Core/Logic/Intensional/Defs.lean
rename to Linglib/Core/Logic/Modal/Defs.lean
index fe976a79a..72b202505 100644
--- a/Linglib/Core/Logic/Intensional/Defs.lean
+++ b/Linglib/Core/Logic/Modal/Defs.lean
@@ -6,19 +6,22 @@ import Mathlib.Order.Defs.Unbundled
 
 @cite{kripke-1963}
 
-The bare foundation for accessibility-restricted modal logic, parameterised
-by `{W : Type*}` — no Frame, no Entity, no type system. This file holds the
-definitions and very simple lemmas that the rest of `Core.Logic.Intensional`
-(including Montague's S5 `box`/`diamond` in `Quantification.lean` and the
-modal-axiom theorems in `RestrictedModality.lean`) builds on.
+The bare foundation for accessibility-restricted modal logic, parameterised by
+`{W : Type*}` — no Frame, no Entity, no type system: accessibility relations,
+frame conditions, and the relational `box`/`diamond`. The modal-axiom theorems
+(`RestrictedModality.lean`) build on it.
+
+Montague's S5 `box`/`diamond` in `Core.Logic.Intensional.Quantification` is the
+universal-accessibility special case (`box universalR`), but it lives in the
+typed IL layer and is developed independently there.
 
 `Defs.lean` is the foundation file in mathlib's sense: just the data and the
-relationships among frame conditions. Modal axiom correspondence theorems
-(K/T/D/4/B/5), monotonicity, distribution, restriction, the Logic lattice,
-and the Gallin hierarchy live in `RestrictedModality.lean`.
+relationships among frame conditions. Modal axiom correspondence (K/T/D/4/B/5),
+monotonicity, distribution, restriction, the Logic lattice, and the `PropOp`
+("Gallin") hierarchy live in `RestrictedModality.lean`.
 -/
 
-namespace Core.Logic.Intensional
+namespace Core.Logic.Modal
 
 -- ────────────────────────────────────────────────────────────────
 -- §1 Accessibility Relations
@@ -141,14 +144,14 @@ instance (priority := 100) {R : AccessRel W} [hS : Std.Symm R] [hT : IsTrans W R
     `⟦□_R φ⟧^w = 1` iff `⟦φ⟧^v = 1` for all `v` with `R(w,v)`.
 
     This is the Kripke generalization of DWP's Rule B.13 (`box`); the
-    `Core.Logic.Intensional.box` operator in `Quantification.lean` is the
+    `Core.Logic.Modal.box` operator in `Quantification.lean` is the
     universal-accessibility special case. -/
-def boxR (R : AccessRel W) (p : W → Prop) (w : W) : Prop :=
+def box (R : AccessRel W) (p : W → Prop) (w : W) : Prop :=
   ∀ v, R w v → p v
 
 /-- Restricted possibility: `◇_R p` at world `w` holds iff `p v` for some
-    `v` accessible from `w`. Dual of `boxR`. -/
-def diamondR (R : AccessRel W) (p : W → Prop) (w : W) : Prop :=
+    `v` accessible from `w`. Dual of `box`. -/
+def diamond (R : AccessRel W) (p : W → Prop) (w : W) : Prop :=
   ∃ v, R w v ∧ p v
 
 -- ────────────────────────────────────────────────────────────────
@@ -156,18 +159,18 @@ def diamondR (R : AccessRel W) (p : W → Prop) (w : W) : Prop :=
 -- ────────────────────────────────────────────────────────────────
 
 /-- `□_R p ↔ ¬◇_R ¬p` — restricted modal duality. -/
-theorem boxR_neg_diamondR (R : AccessRel W) (p : W → Prop) (w : W) :
-    boxR R p w = ¬(diamondR R (fun v => ¬(p v)) w) := by
-  simp only [boxR, diamondR, not_exists, not_and, not_not]
+theorem box_neg_diamond (R : AccessRel W) (p : W → Prop) (w : W) :
+    box R p w = ¬(diamond R (fun v => ¬(p v)) w) := by
+  simp only [box, diamond, not_exists, not_and, not_not]
 
 /-- `◇_R p ↔ ¬□_R ¬p` — dual form. -/
-theorem diamondR_neg_boxR (R : AccessRel W) (p : W → Prop) (w : W) :
-    diamondR R p w = ¬(boxR R (fun v => ¬(p v)) w) := by
-  simp only [diamondR, boxR]
+theorem diamond_neg_box (R : AccessRel W) (p : W → Prop) (w : W) :
+    diamond R p w = ¬(box R (fun v => ¬(p v)) w) := by
+  simp only [diamond, box]
   exact propext ⟨
     fun ⟨v, hwv, hpv⟩ h => h v hwv hpv,
     fun h => Classical.byContradiction fun hne => by
       simp only [not_exists, not_and] at hne
       exact h (fun v hwv => hne v hwv)⟩
 
-end Core.Logic.Intensional
+end Core.Logic.Modal
diff --git a/Linglib/Discourse/Commitment/Frame.lean b/Linglib/Discourse/Commitment/Frame.lean
index c700349ed..822c29db3 100644
--- a/Linglib/Discourse/Commitment/Frame.lean
+++ b/Linglib/Discourse/Commitment/Frame.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Set.Basic
-import Linglib.Core.Logic.Intensional.Defs
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Defs
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Semantics.Modality.EpistemicLogic
 
 /-!
@@ -28,8 +28,8 @@ commitment to belief.
 
 namespace Discourse.Commitment.Frame
 
-open Core.Logic.Intensional (AccessRel AgentAccessRel IsKD45Frame IsK4EuclFrame
-  IsEuclidean boxR diamondR boxR_K boxR_four)
+open Core.Logic.Modal (AccessRel AgentAccessRel IsKD45Frame IsK4EuclFrame
+  IsEuclidean box diamond box_K box_four)
 open Semantics.Modality.EpistemicLogic (knows)
 
 /-- Pair-indexed deontic accessibility: `commitment a b w v` means at
@@ -124,25 +124,25 @@ variable {W : Type*} {A : Type*}
 def Believes (c : CommitmentState W A) (a : A) (π : Set W) (w : W) : Prop :=
   knows c.belief a (fun v => v ∈ π) w
 
-theorem Believes_eq_boxR (c : CommitmentState W A) (a : A) (π : Set W) (w : W) :
-    Believes c a π w ↔ boxR (c.belief a) (fun v => v ∈ π) w := Iff.rfl
+theorem Believes_eq_box (c : CommitmentState W A) (a : A) (π : Set W) (w : W) :
+    Believes c a π w ↔ box (c.belief a) (fun v => v ∈ π) w := Iff.rfl
 
 /-- `a` committed towards `b` to `π` at `w`: every `O_{a,b}`-accessible
     world from `w` lies in `π`. K4 + Eucl. (Stalnaker 1984). -/
 def Committed (c : CommitmentState W A) (a b : A) (π : Set W) (w : W) : Prop :=
-  boxR (c.commitment a b) (fun v => v ∈ π) w
+  box (c.commitment a b) (fun v => v ∈ π) w
 
 /-- Belief satisfies the 4 axiom (positive introspection). -/
 theorem believes_four (c : CommitmentState W A) (a : A) (π : Set W) (w : W)
     (h : Believes c a π w) :
     Believes c a (fun v => Believes c a π v) w :=
-  boxR_four (c.belief a) (fun v => v ∈ π) w h
+  box_four (c.belief a) (fun v => v ∈ π) w h
 
 /-- Commitment satisfies the 4 axiom. -/
 theorem committed_four (c : CommitmentState W A) (a b : A) (π : Set W) (w : W)
     (h : Committed c a b π w) :
     Committed c a b (fun v => Committed c a b π v) w :=
-  boxR_four (c.commitment a b) (fun v => v ∈ π) w h
+  box_four (c.commitment a b) (fun v => v ∈ π) w h
 
 /-! ### Frame conditions linking belief and commitment -/
 
diff --git a/Linglib/Fragments/English/TDDeletion.lean b/Linglib/Fragments/English/TDDeletion.lean
deleted file mode 100644
index de01ea9f9..000000000
--- a/Linglib/Fragments/English/TDDeletion.lean
+++ /dev/null
@@ -1,139 +0,0 @@
-import Linglib.Phonology.OptimalityTheory.Constraints
-
-/-!
-# English t/d-Deletion: Cross-Dialectal Data
-@cite{coetzee-pater-2011}
-
-Cross-dialectal deletion rates for word-final t/d in English consonant
-clusters (e.g. *west* → *wes*), from @cite{coetzee-pater-2011} table (10).
-Per-dialect data sources (footnote 3): AAVE (Fasold 1972), Chicano
-(Santa Ana 1992), Jamaican (Patrick 1992), Trinidad (Kang 1994),
-Tejano (Bayley 1995).
-
-## External context
-
-The key conditioning factor is the **following segment** — what comes after
-the word-final cluster:
-
-- **Pre-vocalic** (*west end*): t/d cues are maximally recoverable
-- **Pre-pausal** (*west*): partial cue availability (release only)
-- **Pre-consonantal** (*west side*): minimal cue availability
-
-The cross-dialectal generalization is that deletion rate follows:
-  pre-C ≥ pre-pause ≥ pre-V
-
-with the inequality being strict in most dialects.
-
-## Dialects
-
-Five dialects from the sociolinguistic literature, each with distinct
-absolute rates but obeying the pre-C ≥ pre-pause ≥ pre-V ordering.
-Chicano English is the sole exception: it has pre-V > pre-pause
-(@cite{coetzee-pater-2011} table 10, p. 410).
--/
-
-namespace Fragments.English.TDDeletion
-
--- ============================================================================
--- § 1: Types
--- ============================================================================
-
-/-- External phonological context following the word-final cluster. -/
-inductive Context where
-  | preV   -- pre-vocalic (*west end*)
-  | pause  -- pre-pausal (*west*)
-  | preC   -- pre-consonantal (*west side*)
-  deriving DecidableEq, Repr, Inhabited
-
-/-- English dialects with t/d-deletion data. -/
-inductive Dialect where
-  | aave      -- African American Vernacular English (Fasold 1972; Washington, DC)
-  | chicano   -- Chicano English (Santa Ana 1992)
-  | jamaican  -- Jamaican English (Patrick 1992)
-  | trinidad  -- Trinidadian English (Kang 1994)
-  | tejano    -- Tejano English (Bayley 1995)
-  deriving DecidableEq, Repr, Inhabited
-
-/-- Observed deletion rate as a percentage (integer).
-    From @cite{coetzee-pater-2011} table (10), p. 410. -/
-def deletionRate : Dialect → Context → Nat
-  | .aave,    .preV => 29 | .aave,    .pause => 73 | .aave,    .preC => 76
-  | .chicano, .preV => 45 | .chicano, .pause => 37 | .chicano, .preC => 62
-  | .jamaican,.preV => 63 | .jamaican,.pause => 71 | .jamaican,.preC => 85
-  | .trinidad,.preV => 21 | .trinidad,.pause => 31 | .trinidad,.preC => 81
-  | .tejano,  .preV => 25 | .tejano,  .pause => 46 | .tejano,  .preC => 62
-
-/-- All dialects. -/
-def allDialects : List Dialect := [.aave, .chicano, .jamaican, .trinidad, .tejano]
-
-/-- All contexts. -/
-def allContexts : List Context := [.preV, .pause, .preC]
-
--- ============================================================================
--- § 2: Cross-Dialectal Generalization
--- ============================================================================
-
-/-- Pre-consonantal deletion ≥ pre-vocalic in every dialect. -/
-theorem preC_ge_preV (d : Dialect) :
-    deletionRate d .preC ≥ deletionRate d .preV := by
-  cases d <;> native_decide
-
-/-- Pre-consonantal deletion ≥ pre-pausal in every dialect except Chicano. -/
-theorem preC_ge_pause_non_chicano (d : Dialect) (h : d ≠ .chicano) :
-    deletionRate d .preC ≥ deletionRate d .pause := by
-  cases d <;> simp_all <;> native_decide
-
-/-- Chicano is exceptional: pre-vocalic > pre-pausal. -/
-theorem chicano_preV_gt_pause :
-    deletionRate .chicano .preV > deletionRate .chicano .pause := by
-  native_decide
-
-/-- In all non-Chicano dialects, pre-pausal ≥ pre-vocalic. -/
-theorem pause_ge_preV_non_chicano (d : Dialect) (h : d ≠ .chicano) :
-    deletionRate d .pause ≥ deletionRate d .preV := by
-  cases d <;> simp_all <;> native_decide
-
--- ============================================================================
--- § 3: Morphological Conditioning Data
--- ============================================================================
-
-/-- Morphological status of the word-final t/d.
-    @cite{coetzee-pater-2011} table (7), p. 407. -/
-inductive MorphStatus where
-  | regularPast   -- *missed* (past tense suffix)
-  | semiWeakPast  -- *kept* (semi-weak past)
-  | monomorpheme  -- *mist* (monomorphemic)
-  deriving DecidableEq, Repr
-
-/-- Dialect labels for table (7) morphological data.
-    Note: table (7) uses different dialects than table (10) — Philadelphia
-    English replaces AAVE; Jamaican and Trinidad have no morph data. -/
-inductive MorphDialect where
-  | philadelphia  -- Philadelphia English (Guy 1991b)
-  | chicano       -- Chicano English (Santa Ana 1992)
-  | tejano        -- Tejano English (Bayley 1995)
-  deriving DecidableEq, Repr
-
-/-- Deletion rate by morphological status and dialect (percentages).
-    From @cite{coetzee-pater-2011} table (7). -/
-def morphDeletionRate : MorphDialect → MorphStatus → Nat
-  | .philadelphia, .regularPast => 17 | .philadelphia, .semiWeakPast => 34
-  | .philadelphia, .monomorpheme => 38
-  | .chicano,      .regularPast => 26 | .chicano,      .semiWeakPast => 41
-  | .chicano,      .monomorpheme => 58
-  | .tejano,       .regularPast => 24 | .tejano,       .semiWeakPast => 34
-  | .tejano,       .monomorpheme => 56
-
-/-- Monomorpheme deletion ≥ regular past in every dialect with data.
-    This is the morphological generalization from §3.1. -/
-theorem mono_ge_regular (d : MorphDialect) :
-    morphDeletionRate d .monomorpheme ≥ morphDeletionRate d .regularPast := by
-  cases d <;> native_decide
-
-/-- Semi-weak past ≥ regular past in every dialect with data.
-    This captures the three-way morphological gradient from §3.1. -/
-theorem semiWeak_ge_regular (d : MorphDialect) :
-    morphDeletionRate d .semiWeakPast ≥ morphDeletionRate d .regularPast := by
-  cases d <;> native_decide
-
-end Fragments.English.TDDeletion
diff --git a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
index 08591cb6b..d95030a25 100644
--- a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
+++ b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Finset.Basic
 import Linglib.Semantics.Entailment.AsymStronger
-import Linglib.Core.Logic.Intensional.Defs
+import Linglib.Core.Logic.Modal.Defs
 
 /-!
 # Sauerland's Epistemic Implicature Framework
@@ -45,7 +45,7 @@ categorical side.
 
 namespace Implicature.EpistemicBlocking
 
-open Core.Logic.Intensional (AccessRel boxR diamondR IsSerial)
+open Core.Logic.Modal (AccessRel box diamond IsSerial)
 
 /-- An epistemic state represents what the speaker knows.
 We model this as a finite set of worlds the speaker considers possible. -/
@@ -74,9 +74,9 @@ instance {W : Type*} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ]
 
 /-! ### `K`/`P` as restricted modality
 
-`knows`/`possible` are `boxR`/`diamondR` over the (world-independent) epistemic
+`knows`/`possible` are `box`/`diamond` 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
+The epistemic square of opposition is then `Core.Logic.Modal.modalSquare
 (accessFrom e)` with `modalSquare_relations` discharged by this `IsSerial` instance
 — no bespoke square construction. -/
 
@@ -86,16 +86,16 @@ def accessFrom {W : Type*} (e : EpistemicState W) : AccessRel W := fun _ w' => w
 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
+theorem knows_eq_box {W : Type*} (e : EpistemicState W) (φ : W → Prop) (w : W) :
+    knows e φ = box (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
+theorem possible_eq_diamond {W : Type*} (e : EpistemicState W) (φ : W → Prop) (w : W) :
+    possible e φ = diamond (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`). -/
+    (`Core.Logic.Modal.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/Attitudes/Doxastic.lean b/Linglib/Semantics/Attitudes/Doxastic.lean
index d4a6be31c..7fdde6091 100644
--- a/Linglib/Semantics/Attitudes/Doxastic.lean
+++ b/Linglib/Semantics/Attitudes/Doxastic.lean
@@ -40,7 +40,7 @@ import Linglib.Discourse.IllocutionaryForce
 import Linglib.Discourse.Intentionality
 import Linglib.Discourse.Commitment.Basic
 import Linglib.Semantics.Presupposition.Basic
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Core.Causal.SEM.Bool
 import Linglib.Core.Causal.SEM.Counterfactual
 import Linglib.Features.Aktionsart
diff --git a/Linglib/Semantics/Modality/BiasedPQ.lean b/Linglib/Semantics/Modality/BiasedPQ.lean
index d2525fe7b..d3bdea259 100644
--- a/Linglib/Semantics/Modality/BiasedPQ.lean
+++ b/Linglib/Semantics/Modality/BiasedPQ.lean
@@ -329,7 +329,7 @@ def evidentialPossibility (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Pro
 
 /-- □_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`). -/
+    (`Core.Logic.Modal.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/EpistemicLogic.lean b/Linglib/Semantics/Modality/EpistemicLogic.lean
index d55308aab..c377c9ed5 100644
--- a/Linglib/Semantics/Modality/EpistemicLogic.lean
+++ b/Linglib/Semantics/Modality/EpistemicLogic.lean
@@ -1,5 +1,5 @@
 import Linglib.Discourse.CommonGround
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Core.Scales.EpistemicScale.Defs
 
 /-!
@@ -37,20 +37,20 @@ on finite worlds goes through `Decidable` instances + `decide`.
 
 namespace Semantics.Modality.EpistemicLogic
 
-open Core.Logic.Intensional
-  (AccessRel AgentAccessRel boxR diamondR IsSerial IsEuclidean IsBeliefRefinementOf
-   boxR_T boxR_D boxR_four boxR_B boxR_five)
+open Core.Logic.Modal
+  (AccessRel AgentAccessRel box diamond IsSerial IsEuclidean IsBeliefRefinementOf
+   box_T box_D box_four box_B box_five)
 
 /-! ## Individual Knowledge
 
 Agent i knows φ at world w iff φ holds at all worlds accessible to i.
-This re-uses `boxR` from `RestrictedModality.lean` with agent-indexed
+This re-uses `box` from `RestrictedModality.lean` with agent-indexed
 accessibility relations. -/
 
 /-- Agent i knows φ at world w: Kᵢ(φ)(w) = □ᵢ φ(w). -/
 def knows {W E : Type*} (Rs : AgentAccessRel W E) (i : E)
     (φ : W → Prop) (w : W) : Prop :=
-  boxR (Rs i) φ w
+  box (Rs i) φ w
 
 /-! ## Everyone Knows
 
@@ -130,7 +130,7 @@ def groupAccessRel {W E : Type*} (Rs : AgentAccessRel W E)
 /-- Distributed knowledge: D_G(φ)(w) = □_{∩R} φ(w). -/
 def distributedKnowledge {W E : Type*} (Rs : AgentAccessRel W E)
     (group : List E) (φ : W → Prop) (w : W) : Prop :=
-  boxR (groupAccessRel Rs group) φ w
+  box (groupAccessRel Rs group) φ w
 
 /-- Individual knowledge implies distributed knowledge: the intersection
     of accessibility relations is a subset of each component, so every
@@ -165,7 +165,7 @@ accessible worlds), knowledge is harder to achieve than belief. -/
     S5 (reflexive + Euclidean). -/
 def believes {W E : Type*} (Rs : AgentAccessRel W E) (i : E)
     (φ : W → Prop) (w : W) : Prop :=
-  boxR (Rs i) φ w
+  box (Rs i) φ w
 
 /-- Everyone in group G believes φ at w. -/
 def everyoneBelieves {W E : Type*} (Rs : AgentAccessRel W E)
@@ -186,7 +186,7 @@ def commonBelief {W E : Type*} (Rs : AgentAccessRel W E)
 /-- Distributed belief: DB_G(φ)(w) = □_{∩R_B} φ(w). -/
 def distributedBelief {W E : Type*} (Rs : AgentAccessRel W E)
     (group : List E) (φ : W → Prop) (w : W) : Prop :=
-  boxR (groupAccessRel Rs group) φ w
+  box (groupAccessRel Rs group) φ w
 
 /-- Knowledge implies belief: Kᵢ(φ) → Bᵢ(φ), given that every
     belief-accessible world is knowledge-accessible. The
@@ -203,8 +203,8 @@ theorem knows_implies_believes {W E : Type*}
 theorem believes_consistent {W E : Type*}
     {Rs : AgentAccessRel W E} (i : E) [IsSerial (Rs i)]
     (φ : W → Prop) (w : W) (h : believes Rs i φ w) :
-    diamondR (Rs i) φ w :=
-  boxR_D (Rs i) φ w h
+    diamond (Rs i) φ w :=
+  box_D (Rs i) φ w h
 
 /-- Positive introspection: Bᵢ(φ) → Bᵢ(Bᵢ(φ)) (the 4 axiom).
     Follows from transitivity of the belief accessibility relation. -/
@@ -212,15 +212,15 @@ theorem believes_positive_introspection {W E : Type*}
     {Rs : AgentAccessRel W E} (i : E) [IsTrans W (Rs i)]
     (φ : W → Prop) (w : W) (h : believes Rs i φ w) :
     believes Rs i (believes Rs i φ) w :=
-  boxR_four (Rs i) φ w h
+  box_four (Rs i) φ w h
 
 /-- Negative introspection: ◇Bφ → □◇Bφ (the 5 axiom).
     Follows from Euclideanness of the belief accessibility relation. -/
 theorem believes_negative_introspection {W E : Type*}
     {Rs : AgentAccessRel W E} (i : E) [IsEuclidean (Rs i)]
-    (φ : W → Prop) (w : W) (h : diamondR (Rs i) φ w) :
-    boxR (Rs i) (diamondR (Rs i) φ) w :=
-  boxR_five (Rs i) φ w h
+    (φ : W → Prop) (w : W) (h : diamond (Rs i) φ w) :
+    box (Rs i) (diamond (Rs i) φ) w :=
+  box_five (Rs i) φ w h
 
 /-- Belief is not veridical: there exist frames where Bᵢ(φ) ∧ ¬φ.
     Unlike knowledge (which requires reflexivity), belief frames are
diff --git a/Linglib/Semantics/Modality/EventRelativity.lean b/Linglib/Semantics/Modality/EventRelativity.lean
index 53e09ae5b..262d6f053 100644
--- a/Linglib/Semantics/Modality/EventRelativity.lean
+++ b/Linglib/Semantics/Modality/EventRelativity.lean
@@ -1,4 +1,4 @@
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Semantics.Modality.ModalTypes
 
 /-!
@@ -140,7 +140,7 @@ instance {Event W : Type*} (f : AnchoringFn Event W) (e : Event)
 
 /-- 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`). -/
+    (`Core.Logic.Modal.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 0a9006994..40ad310c3 100644
--- a/Linglib/Semantics/Modality/Kratzer/Operators.lean
+++ b/Linglib/Semantics/Modality/Kratzer/Operators.lean
@@ -1,7 +1,7 @@
 /-
 @cite{kratzer-1981} Modal Operators — IL Foundation
 
-Kratzer-style necessity and possibility, defined as `boxR`/`diamondR` from
+Kratzer-style necessity and possibility, defined as `box`/`diamond` from
 `Core.Logic.Intensional` over conversational-background-derived accessibility
 relations. Frame conditions on the accessibility relation are derived from
 conversational-background properties; modal-axiom derivations then follow from
@@ -13,7 +13,7 @@ the polymorphic correspondence theorems in `RestrictedModality`.
   and from a modal base together with an ordering source.
 * `simpleNecessity`, `simplePossibility`: `□`/`◇` over `kratzerR`.
 * `necessity`, `possibility`: `□`/`◇` over `kratzerBestR`.
-* `duality`: `□p ↔ ¬◇¬p`, delegating to `boxR_neg_diamondR`.
+* `duality`: `□p ↔ ¬◇¬p`, delegating to `box_neg_diamond`.
 * `K_axiom`, `totally_realistic_gives_T`: instances of generic axioms applied
   to Kratzer-specific accessibility.
 * `restrictedBase`: conditional-as-restrictor on the modal base.
@@ -37,11 +37,11 @@ Sources:
 -/
 
 import Linglib.Semantics.Modality.Kratzer.Ordering
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 
 namespace Semantics.Modality.Kratzer
 
-open Core.Logic.Intensional
+open Core.Logic.Modal
 
 variable {W : Type*}
 
@@ -73,24 +73,24 @@ theorem kratzerBestR_empty (f : ModalBase W) (w w' : W) :
 /-- **Simple f-necessity**: `p` holds at every accessible world.
     `⟦must⟧_f(p)(w) = ∀w' ∈ ⋂f(w). p(w')`. -/
 def simpleNecessity (f : ModalBase W) (p : W → Prop) (w : W) : Prop :=
-  boxR (kratzerR f) p w
+  box (kratzerR f) p w
 
 /-- **Simple f-possibility**: `p` holds at some accessible world.
     `⟦can⟧_f(p)(w) = ∃w' ∈ ⋂f(w). p(w')`. -/
 def simplePossibility (f : ModalBase W) (p : W → Prop) (w : W) : Prop :=
-  diamondR (kratzerR f) p w
+  diamond (kratzerR f) p w
 
 /-- **Necessity with ordering**: `p` holds at every best world.
     `⟦must⟧_{f,g}(p)(w) = ∀w' ∈ Best(f,g,w). p(w')`.
 
     Adopts the Limit-Assumption-collapsed form. -/
 def necessity (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop :=
-  boxR (kratzerBestR f g) p w
+  box (kratzerBestR f g) p w
 
 /-- **Possibility with ordering**: `p` holds at some best world.
     `⟦can⟧_{f,g}(p)(w) = ∃w' ∈ Best(f,g,w). p(w')`. -/
 def possibility (f : ModalBase W) (g : OrderingSource W) (p : W → Prop) (w : W) : Prop :=
-  diamondR (kratzerBestR f g) p w
+  diamond (kratzerBestR f g) p w
 
 /-! ### Characterization lemmas -/
 
@@ -144,19 +144,19 @@ theorem empty_base_universal_access (w : W) :
 
 /-! ### Modal axioms (from `RestrictedModality`) -/
 
-/-- **Modal duality**: `□p ↔ ¬◇¬p`. Since `necessity = boxR (kratzerBestR f g)`,
+/-- **Modal duality**: `□p ↔ ¬◇¬p`. Since `necessity = box (kratzerBestR f g)`,
     this is the box–diamond duality of the modal square of opposition
-    (`Core.Logic.Intensional.modalSquare_relations`). -/
+    (`Core.Logic.Modal.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]
+  rw [necessity, possibility, box_neg_diamond]
 
 /-- **K (Distribution)**: `□(p → q) → □p → □q`. -/
 theorem K_axiom (f : ModalBase W) (g : OrderingSource W) (p q : W → Prop) (w : W)
     (hImpl : necessity f g (fun w' => p w' → q w') w)
     (hP : necessity f g p w) :
     necessity f g q w :=
-  boxR_K (kratzerBestR f g) p q w hImpl hP
+  box_K (kratzerBestR f g) p q w hImpl hP
 
 /-- Totally realistic base: simple T holds for full necessity. -/
 theorem totally_realistic_gives_T (f : ModalBase W) (g : OrderingSource W)
diff --git a/Linglib/Semantics/Modality/Orthologic/Modal.lean b/Linglib/Semantics/Modality/Orthologic/Modal.lean
index 5cf61848b..e7d335eec 100644
--- a/Linglib/Semantics/Modality/Orthologic/Modal.lean
+++ b/Linglib/Semantics/Modality/Orthologic/Modal.lean
@@ -1,5 +1,5 @@
 import Linglib.Semantics.Modality.Orthologic.Frames
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Mathlib.Data.Fintype.Pi
 
 /-!
diff --git a/Linglib/Semantics/Modality/Temporal.lean b/Linglib/Semantics/Modality/Temporal.lean
index 6e107776a..6c412fbb8 100644
--- a/Linglib/Semantics/Modality/Temporal.lean
+++ b/Linglib/Semantics/Modality/Temporal.lean
@@ -98,7 +98,7 @@ theorem temporal_eq_static {Time : Type*}
 
 /-- 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`). -/
+    (`Core.Logic.Modal.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/Linglib/Semantics/Presupposition/BeliefEmbedding.lean b/Linglib/Semantics/Presupposition/BeliefEmbedding.lean
index 1f8ec1e6f..6fb555c67 100644
--- a/Linglib/Semantics/Presupposition/BeliefEmbedding.lean
+++ b/Linglib/Semantics/Presupposition/BeliefEmbedding.lean
@@ -297,7 +297,7 @@ Both represent the same concept (agent-indexed world accessibility). The
 
 section BoolPropBridge
 
-open Core.Logic.Intensional (AgentAccessRel IsBeliefRefinementOf)
+open Core.Logic.Modal (AgentAccessRel IsBeliefRefinementOf)
 
 variable {W E : Type*}
 
diff --git a/Linglib/Semantics/Supervaluation/TCS.lean b/Linglib/Semantics/Supervaluation/TCS.lean
index cfdd417e3..93878e201 100644
--- a/Linglib/Semantics/Supervaluation/TCS.lean
+++ b/Linglib/Semantics/Supervaluation/TCS.lean
@@ -2,7 +2,7 @@ import Linglib.Semantics.Supervaluation.Basic
 import Linglib.Core.Logic.Truth3
 import Linglib.Core.Logic.Consequence
 import Linglib.Core.Logic.ThreeValuedLogic
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Logic.Function.Basic
@@ -48,12 +48,12 @@ relation `~_P`. The strict and tolerant satisfaction operators are
 exactly the modal `□` and `◇` over `~_P`, applied to the classical
 extension of `P`:
 
-- `strict P at a` ≡ `boxR (~_P) I(P) a` (Definition 9)
-- `tolerant P at a` ≡ `diamondR (~_P) I(P) a` (Definition 9)
+- `strict P at a` ≡ `box (~_P) I(P) a` (Definition 9)
+- `tolerant P at a` ≡ `diamond (~_P) I(P) a` (Definition 9)
 
-The s ⊆ c ⊆ t hierarchy is the **T axiom** instantiated at `boxR`
-(`Core.Logic.Intensional.boxR_T`); the t/s duality is the standard
-modal de Morgan `boxR R ¬p ↔ ¬diamondR R p`. T-models satisfy
+The s ⊆ c ⊆ t hierarchy is the **T axiom** instantiated at `box`
+(`Core.Logic.Modal.box_T`); the t/s duality is the standard
+modal de Morgan `box R ¬p ↔ ¬diamond R p`. T-models satisfy
 `frameConditions Logic.KTB` by construction (Definition 4 of
 @cite{cobreros-etal-2012}); see `TModel.satisfies_KTB` for the explicit
 witness. The Brouwersche axiom B / symmetric-frame correspondence is
@@ -128,8 +128,8 @@ is addressed in that Studies file's §8-§9.
 namespace Semantics.Supervaluation.TCS
 
 open Core.Duality (Truth3)
-open Core.Logic.Intensional
-  (AccessRel IsKTBFrame IsSerial boxR diamondR boxR_T Logic)
+open Core.Logic.Modal
+  (AccessRel IsKTBFrame IsSerial box diamond box_T Logic)
 open Core.Logic.ThreeValuedLogic (PropFormula MVModel mvEval lpSat k3Sat
   isLPDesignated isK3Designated lpSat_neg_iff k3Sat_neg_iff
   lpSat_conj k3Sat_conj)
@@ -152,7 +152,7 @@ open Semantics.Supervaluation (SpecSpace superTrue
     look like c, but a need not look like c.
 
     Following the modal-logic tradition, the similarity relation is
-    `Prop`-valued so that it integrates directly with `boxR`/`diamondR`.
+    `Prop`-valued so that it integrates directly with `box`/`diamond`.
     Decidability is added per-model where computation is needed. -/
 structure TModel (D Pred : Type*) where
   /-- Classical interpretation `I : Pred → D → Prop`. -/
@@ -177,7 +177,7 @@ variable {D Pred : Type*}
 
 /-- The similarity relation as an `AccessRel` — the Kripke frame
     associated with each predicate. By construction this frame is
-    reflexive + symmetric, i.e., a **KTB frame** (`Core.Logic.Intensional.Logic.KTB`). -/
+    reflexive + symmetric, i.e., a **KTB frame** (`Core.Logic.Modal.Logic.KTB`). -/
 @[reducible] def simAccess (M : TModel D Pred) (P : Pred) : AccessRel D := M.sim P
 
 /-- Per-`(M, P)` KTB-frame instance: lets typeclass search reach
@@ -230,26 +230,26 @@ variable {D Pred : Type*}
 
 /-- **Strict** atomic satisfaction: `P` holds at every `~_P`-neighbour
     of `a`. Definition 9, atomic clause for `⊨ˢ`. Modal-logic-wise,
-    this is `boxR (M.simAccess P)` over the classical extension. -/
+    this is `box (M.simAccess P)` over the classical extension. -/
 def StrictAt (M : TModel D Pred) (P : Pred) (a : D) : Prop :=
   ∀ d, M.sim P a d → M.interp P d
 
 /-- **Tolerant** atomic satisfaction: `P` holds at some `~_P`-neighbour
     of `a`. Definition 9, atomic clause for `⊨ᵗ`. Modal-logic-wise,
-    this is `diamondR (M.simAccess P)` over the classical extension. -/
+    this is `diamond (M.simAccess P)` over the classical extension. -/
 def TolerantAt (M : TModel D Pred) (P : Pred) (a : D) : Prop :=
   ∃ d, M.sim P a d ∧ M.interp P d
 
-/-- **Strict atom = `boxR` over the similarity frame.** This is
+/-- **Strict atom = `box` over the similarity frame.** This is
     definitionally true; the lemma exists to expose the modal-logic
-    framing and to let downstream proofs invoke `boxR_T`/`boxR_B`
+    framing and to let downstream proofs invoke `box_T`/`box_B`
     directly. -/
-theorem strictAt_eq_boxR (M : TModel D Pred) (P : Pred) (a : D) :
-    StrictAt M P a = boxR (M.simAccess P) (λ d => M.interp P d) a := rfl
+theorem strictAt_eq_box (M : TModel D Pred) (P : Pred) (a : D) :
+    StrictAt M P a = box (M.simAccess P) (λ d => M.interp P d) a := rfl
 
-/-- **Tolerant atom = `diamondR` over the similarity frame.** Definitional. -/
-theorem tolerantAt_eq_diamondR (M : TModel D Pred) (P : Pred) (a : D) :
-    TolerantAt M P a = diamondR (M.simAccess P) (λ d => M.interp P d) a := rfl
+/-- **Tolerant atom = `diamond` over the similarity frame.** Definitional. -/
+theorem tolerantAt_eq_diamond (M : TModel D Pred) (P : Pred) (a : D) :
+    TolerantAt M P a = diamond (M.simAccess P) (λ d => M.interp P d) a := rfl
 
 -- ════════════════════════════════════════════════════
 -- § 4. Lemma 1 atomic (extension hierarchy, p. 357)
@@ -260,7 +260,7 @@ theorem tolerantAt_eq_diamondR (M : TModel D Pred) (P : Pred) (a : D) :
     `~_P`. This is the **T axiom** instantiated. -/
 theorem StrictAt.imp_classical (M : TModel D Pred) (P : Pred) (a : D)
     (hs : StrictAt M P a) : M.interp P a :=
-  boxR_T (M.simAccess P) _ a hs
+  box_T (M.simAccess P) _ a hs
 
 /-- **Classical ⟹ tolerant** at the atomic level: `a` itself
     witnesses the existential by reflexivity of `~_P`. -/
diff --git a/Linglib/Studies/Booth2022.lean b/Linglib/Studies/Booth2022.lean
index adf1977f9..9fb9adc80 100644
--- a/Linglib/Studies/Booth2022.lean
+++ b/Linglib/Studies/Booth2022.lean
@@ -166,7 +166,7 @@ def conj (φ ψ : BilatInqProp W) : BilatInqProp W where
 /-! ### §3 Necessity and possibility (Booth Def 14)
 
 `R : W → Set W` is the relevant-worlds accessibility relation
-(equivalent in expressive power to `Core.Logic.Intensional.AccessRel W
+(equivalent in expressive power to `Core.Logic.Modal.AccessRel W
 = W → W → Prop`; Booth uses the curried `W → Set W` form throughout
 his Def 14, which we mirror). -/
 
diff --git a/Linglib/Studies/CobrerosEtAl2012.lean b/Linglib/Studies/CobrerosEtAl2012.lean
index 3a62e2d67..929d5ef56 100644
--- a/Linglib/Studies/CobrerosEtAl2012.lean
+++ b/Linglib/Studies/CobrerosEtAl2012.lean
@@ -102,7 +102,7 @@ def soritesSimBool : Elt → Elt → Bool
   | _, _ => false
 
 /-- The similarity relation as a `Prop`, for direct integration with
-    the modal-logic substrate's `boxR`/`diamondR`. -/
+    the modal-logic substrate's `box`/`diamond`. -/
 def soritesSim (x y : Elt) : Prop := soritesSimBool x y = true
 
 instance : DecidableRel soritesSim := λ x y =>
diff --git a/Linglib/Studies/CoetzeePater2011.lean b/Linglib/Studies/CoetzeePater2011.lean
index 9ff3499e7..4a093941d 100644
--- a/Linglib/Studies/CoetzeePater2011.lean
+++ b/Linglib/Studies/CoetzeePater2011.lean
@@ -3,7 +3,6 @@ import Linglib.Core.Constraint.System
 import Linglib.Core.Constraint.PartiallyOrderedConstraints
 import Linglib.Core.Constraint.PermSubsetCombinatorics
 import Linglib.Phonology.OptimalityTheory.Constraints
-import Linglib.Fragments.English.TDDeletion
 
 /-!
 # Coetzee & Pater (2011): The Place of Variation in Phonological Theory
@@ -52,7 +51,96 @@ namespace CoetzeePater2011
 open Core.Constraint.OT Core.Constraint.Evaluation
 open Core.Constraint
 open Phonology.Constraints
-open Fragments.English.TDDeletion
+
+/-! ### Empirical data (tables 7 and 10) -/
+
+/-- External phonological context following the word-final cluster.
+    @cite{coetzee-pater-2011} table (10), p. 410. -/
+inductive Context where
+  | preV   -- pre-vocalic (*west end*)
+  | pause  -- pre-pausal (*west*)
+  | preC   -- pre-consonantal (*west side*)
+  deriving DecidableEq, Repr, Inhabited, Fintype
+
+/-- English dialects with t/d-deletion data, per @cite{coetzee-pater-2011}
+    footnote 3: AAVE (Fasold 1972), Chicano (Santa Ana 1992), Jamaican
+    (Patrick 1992), Trinidad (Kang 1994), Tejano (Bayley 1995). -/
+inductive Dialect where
+  | aave
+  | chicano
+  | jamaican
+  | trinidad
+  | tejano
+  deriving DecidableEq, Repr, Inhabited, Fintype
+
+/-- Observed deletion rate as a percentage (integer).
+    From @cite{coetzee-pater-2011} table (10), p. 410. -/
+def deletionRate : Dialect → Context → Nat
+  | .aave,    .preV => 29 | .aave,    .pause => 73 | .aave,    .preC => 76
+  | .chicano, .preV => 45 | .chicano, .pause => 37 | .chicano, .preC => 62
+  | .jamaican,.preV => 63 | .jamaican,.pause => 71 | .jamaican,.preC => 85
+  | .trinidad,.preV => 21 | .trinidad,.pause => 31 | .trinidad,.preC => 81
+  | .tejano,  .preV => 25 | .tejano,  .pause => 46 | .tejano,  .preC => 62
+
+/-- Pre-consonantal deletion ≥ pre-vocalic in every dialect. -/
+theorem preC_ge_preV (d : Dialect) :
+    deletionRate d .preC ≥ deletionRate d .preV := by
+  cases d <;> decide
+
+/-- Pre-consonantal deletion ≥ pre-pausal in every dialect (Chicano included:
+    62 ≥ 37). -/
+theorem preC_ge_pause (d : Dialect) :
+    deletionRate d .preC ≥ deletionRate d .pause := by
+  cases d <;> decide
+
+/-- Chicano is exceptional: pre-vocalic > pre-pausal. -/
+theorem chicano_preV_gt_pause :
+    deletionRate .chicano .preV > deletionRate .chicano .pause := by
+  decide
+
+/-- In all non-Chicano dialects, pre-pausal ≥ pre-vocalic. -/
+theorem pause_ge_preV_non_chicano (d : Dialect) (h : d ≠ .chicano) :
+    deletionRate d .pause ≥ deletionRate d .preV := by
+  cases d <;> simp_all <;> decide
+
+/-! ### Morphological conditioning (table 7) -/
+
+/-- Morphological status of the word-final t/d.
+    @cite{coetzee-pater-2011} table (7), p. 407. -/
+inductive MorphStatus where
+  | regularPast   -- *missed* (past tense suffix)
+  | semiWeakPast  -- *kept* (semi-weak past)
+  | monomorpheme  -- *mist* (monomorphemic)
+  deriving DecidableEq, Repr, Fintype
+
+/-- Dialect labels for table (7) morphological data.
+    Table (7) uses different dialects than table (10) — Philadelphia
+    English replaces AAVE; Jamaican and Trinidad have no morph data. -/
+inductive MorphDialect where
+  | philadelphia  -- Philadelphia English (Guy 1991b)
+  | chicano       -- Chicano English (Santa Ana 1992)
+  | tejano        -- Tejano English (Bayley 1995)
+  deriving DecidableEq, Repr, Fintype
+
+/-- Deletion rate by morphological status and dialect (percentages).
+    From @cite{coetzee-pater-2011} table (7). -/
+def morphDeletionRate : MorphDialect → MorphStatus → Nat
+  | .philadelphia, .regularPast => 17 | .philadelphia, .semiWeakPast => 34
+  | .philadelphia, .monomorpheme => 38
+  | .chicano,      .regularPast => 26 | .chicano,      .semiWeakPast => 41
+  | .chicano,      .monomorpheme => 58
+  | .tejano,       .regularPast => 24 | .tejano,       .semiWeakPast => 34
+  | .tejano,       .monomorpheme => 56
+
+/-- Monomorpheme deletion ≥ regular past in every dialect with data. -/
+theorem mono_ge_regular (d : MorphDialect) :
+    morphDeletionRate d .monomorpheme ≥ morphDeletionRate d .regularPast := by
+  cases d <;> decide
+
+/-- Semi-weak past ≥ regular past in every dialect with data. -/
+theorem semiWeak_ge_regular (d : MorphDialect) :
+    morphDeletionRate d .semiWeakPast ≥ morphDeletionRate d .regularPast := by
+  cases d <;> decide
 
 -- ============================================================================
 -- § 1: Candidate Type
@@ -572,14 +660,6 @@ harmony of `(ctx, ·)`, decoder = `softmaxDecoder 1`. The two-candidate
 softmax is the logistic function, so `predict .delete` is genuine
 conditional probability `P(delete | ctx)`. -/
 
-instance : Fintype TDOutput where
-  elems := {.retain, .delete}
-  complete := fun x => by cases x <;> simp
-
-instance : Fintype Context where
-  elems := {.preV, .pause, .preC}
-  complete := fun x => by cases x <;> simp
-
 /-- The AAVE constraint weights from table (23) ME-HG row. -/
 def aaveWeights : List (WeightedConstraint TDCandidate) :=
   mkWeightedConstraints (1006/10) (994/10) (21/10) (2/10)
diff --git a/Linglib/Studies/Cooper2023/Ch6.lean b/Linglib/Studies/Cooper2023/Ch6.lean
index 762088f12..ef1d0234c 100644
--- a/Linglib/Studies/Cooper2023/Ch6.lean
+++ b/Linglib/Studies/Cooper2023/Ch6.lean
@@ -1432,7 +1432,7 @@ section TtrKratzerBridge
 
 open Semantics.Modality.Kratzer (ModalBase OrderingSource bestWorlds
   necessity possibility)
-open Core.Logic.Intensional (boxR diamondR)
+open Core.Logic.Modal (box diamond)
 
 variable {W : Type}
 
@@ -1453,7 +1453,7 @@ Kratzer-derived topos coincides with Kratzer's `necessity f g p w`. -/
 theorem kratzer_topos_nec_iff (f : ModalBase W) (g : OrderingSource W)
     (w : W) (p : W → Prop) :
     (kratzerToTopos f g w p).inducedNec ↔ necessity f g p w := by
-  unfold Topos.inducedNec necessity boxR
+  unfold Topos.inducedNec necessity box
   refine ⟨fun h v hv => ?_, fun h s => ?_⟩
   · exact (h ⟨v, hv⟩).some.down
   · exact ⟨PLift.up (h s.val s.property)⟩
@@ -1463,7 +1463,7 @@ Kratzer-derived topos coincides with Kratzer's `possibility f g p w`. -/
 theorem kratzer_topos_poss_iff (f : ModalBase W) (g : OrderingSource W)
     (w : W) (p : W → Prop) :
     (kratzerToTopos f g w p).inducedPoss ↔ possibility f g p w := by
-  unfold Topos.inducedPoss possibility diamondR
+  unfold Topos.inducedPoss possibility diamond
   refine ⟨fun ⟨s, h⟩ => ⟨s.val, s.property, h.some.down⟩,
           fun ⟨v, hv, hp⟩ => ⟨⟨v, hv⟩, ⟨PLift.up hp⟩⟩⟩
 
diff --git a/Linglib/Studies/FaginHalpern1994.lean b/Linglib/Studies/FaginHalpern1994.lean
index 01d07ffc7..e2479be1b 100644
--- a/Linglib/Studies/FaginHalpern1994.lean
+++ b/Linglib/Studies/FaginHalpern1994.lean
@@ -55,8 +55,8 @@ set_option autoImplicit false
 
 namespace FaginHalpern1994
 
-open Core.Logic.Intensional
-  (AgentAccessRel AccessRel boxR IsEuclidean)
+open Core.Logic.Modal
+  (AgentAccessRel AccessRel box IsEuclidean)
 open Semantics.Modality.EpistemicLogic (knows everyoneKnows)
 open Semantics.Modality.EpistemicProbability (WorldCredence nestedThreshold)
 
diff --git a/Linglib/Studies/FuscoSgrizzi2026.lean b/Linglib/Studies/FuscoSgrizzi2026.lean
index 6408f69e3..d72abba94 100644
--- a/Linglib/Studies/FuscoSgrizzi2026.lean
+++ b/Linglib/Studies/FuscoSgrizzi2026.lean
@@ -68,7 +68,7 @@ theorem empty_inertia_is_simple (circ : ModalBase W) (prop : W → Prop) (w : W)
     inertialNecessity ⟨circ, emptyBackground⟩ prop w ↔
     simpleNecessity circ prop w := by
   simp only [inertialNecessity, necessity, simpleNecessity,
-             Core.Logic.Intensional.boxR]
+             Core.Logic.Modal.box]
   constructor
   · intro h j hj
     exact h j ((kratzerBestR_empty circ w j).mpr hj)
diff --git a/Linglib/Studies/Heim1992Projection.lean b/Linglib/Studies/Heim1992Projection.lean
index 4dd2ad3a4..64bf99540 100644
--- a/Linglib/Studies/Heim1992Projection.lean
+++ b/Linglib/Studies/Heim1992Projection.lean
@@ -38,7 +38,7 @@ namespace Heim1992
 
 open Semantics.Presupposition (PrProp)
 open CommonGround (ContextSet)
-open Core.Logic.Intensional (IsSerial IsEuclidean IsS5Frame IsKD45Frame
+open Core.Logic.Modal (IsSerial IsEuclidean IsS5Frame IsKD45Frame
   IsBeliefRefinementOf)
 open Semantics.Presupposition.LocalContext (presupFiltered)
 open Semantics.Presupposition.BeliefEmbedding
diff --git a/Linglib/Studies/Hintikka1962.lean b/Linglib/Studies/Hintikka1962.lean
index 71a4587dc..23e83d251 100644
--- a/Linglib/Studies/Hintikka1962.lean
+++ b/Linglib/Studies/Hintikka1962.lean
@@ -9,7 +9,7 @@ import Linglib.Discourse.Commitment.Frame
 worlds where `p` holds while the speaker fails to believe `p`. But its
 would-be-believed form `B_a (p ∧ ¬ B_a p)` is *indefensible* in any KD4
 doxastic model: a 1-line specialisation of
-`Core.Logic.Intensional.boxR_not_moore` to the agent-indexed belief
+`Core.Logic.Modal.box_not_moore` to the agent-indexed belief
 accessibility of `CommitmentState`. The knowledge analogue specialises
 the same substrate lemma to epistemic accessibility.
 -/
@@ -17,7 +17,7 @@ the same substrate lemma to epistemic accessibility.
 namespace Hintikka1962
 
 open Discourse.Commitment.Frame
-open Core.Logic.Intensional (boxR_not_moore AgentAccessRel IsSerial)
+open Core.Logic.Modal (box_not_moore AgentAccessRel IsSerial)
 open Semantics.Modality.EpistemicLogic (knows)
 
 variable {W A : Type*}
@@ -39,7 +39,7 @@ def DoxasticallyIndefensible (c : CommitmentState W A) (a : A) (P : Set W) : Pro
 theorem mooreContent_doxasticallyIndefensible
     (c : CommitmentState W A) (a : A) (p : Set W) :
     DoxasticallyIndefensible c a (mooreContent c a p) :=
-  fun w => boxR_not_moore (c.belief a) (fun v => v ∈ p) w
+  fun w => box_not_moore (c.belief a) (fun v => v ∈ p) w
 
 /-- A two-world KD4 frame: every world treats only `false` as belief-
     accessible. Used as a witness for `true_mem_mooreContent`. -/
@@ -63,13 +63,13 @@ theorem true_mem_mooreContent :
 
 /-- **Epistemic analogue** (Hintikka §4.11): under KD4 knowledge,
     "p but I don't know whether p" is unknowable. Direct corollary of
-    `boxR_not_moore` for `knows`. -/
+    `box_not_moore` for `knows`. -/
 theorem knowledge_unknowable
     {E : Type*} (Rs : AgentAccessRel W E) (i : E)
     [IsSerial (Rs i)] [IsTrans W (Rs i)]
     (p : W → Prop) (w : W) :
     ¬ knows Rs i (fun v => p v ∧ ¬ knows Rs i p v) w :=
-  boxR_not_moore (Rs i) p w
+  box_not_moore (Rs i) p w
 
 /-- **Performatory corollary** (state-theoretic restatement of Hintikka
     §4.10): under sincerity, no commitment state hosts a self-commitment
diff --git a/Linglib/Studies/KeshetAbney2024.lean b/Linglib/Studies/KeshetAbney2024.lean
index f9966255d..68581cc73 100644
--- a/Linglib/Studies/KeshetAbney2024.lean
+++ b/Linglib/Studies/KeshetAbney2024.lean
@@ -48,7 +48,7 @@ namespace KeshetAbney2024
 
 open KeshetAbney2024.PIP
 open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext)
-open Core.Logic.Intensional (AccessRel)
+open Core.Logic.Modal (AccessRel)
 open Phenomena.Anaphora
 
 
diff --git a/Linglib/Studies/KeshetAbney2024/Bridges.lean b/Linglib/Studies/KeshetAbney2024/Bridges.lean
index 3e7c5eedf..280118cd3 100644
--- a/Linglib/Studies/KeshetAbney2024/Bridges.lean
+++ b/Linglib/Studies/KeshetAbney2024/Bridges.lean
@@ -20,7 +20,7 @@ between PIP's formulation and the standard treatments in:
 1. **Presupposition projection** — PIP's F operator ↔ `PrProp.andFilter`
 2. **Generalized quantifiers** — PIP's EVERY/SOME ↔ `GQ`
 3. **Plural semantics** — PIP's SINGLE/PLURAL ↔ Link's Atom/properPlural
-4. **Modal logic** — PIP's must/might ↔ `Core.Logic.Intensional.boxR/diamondR`
+4. **Modal logic** — PIP's must/might ↔ `Core.Logic.Intensional.box/diamond`
 5. **Static↔dynamic agreement** — `PIPExprF.truth` ↔ `PUpdate` filtering
 
 The set-based GQ operations (`setEvery`/`setSome`), three-argument modals
@@ -42,8 +42,8 @@ namespace KeshetAbney2024.PIP.Bridges
 
 open KeshetAbney2024.PIP
 open Semantics.Dynamic.Core (IVar ICDRTAssignment Entity IContext)
-open Core.Logic.Intensional (AccessRel boxR diamondR)
-open Core.Logic.Intensional.Logic (frameConditions)
+open Core.Logic.Modal (AccessRel box diamond)
+open Core.Logic.Modal.Logic (frameConditions)
 
 
 -- ============================================================
@@ -247,7 +247,7 @@ PIP's must allows anaphora because of a **realistic modal base**
 itself (`R w* w*`). This is exactly the T axiom (`□p → p`,
 frame condition: reflexivity).
 
-The `must_truth_agrees_boxR` and `must_realistic_of_refl`
+The `must_truth_agrees_box` and `must_realistic_of_refl`
 theorems in `Connectives.lean` already prove this correspondence.
 This section classifies PIP's modal operators in the lattice of
 normal modal logics from `Core.Logic.Intensional`.
@@ -271,10 +271,10 @@ Stated for the Prop-valued `AccessRel`/`Std.Refl`/`frameConditions` API in
 operators now use directly.
 -/
 theorem reflexive_satisfies_T {W : Type*}
-    (R : Core.Logic.Intensional.AccessRel W) [hRefl : Std.Refl R] :
-    frameConditions Core.Logic.Intensional.Logic.T R := by
-  unfold frameConditions Core.Logic.Intensional.Logic.hasAxiom
-    Core.Logic.Intensional.Logic.T
+    (R : Core.Logic.Modal.AccessRel W) [hRefl : Std.Refl R] :
+    frameConditions Core.Logic.Modal.Logic.T R := by
+  unfold frameConditions Core.Logic.Modal.Logic.hasAxiom
+    Core.Logic.Modal.Logic.T
   refine ⟨fun _ => hRefl, fun h => ?_, fun h => ?_, fun h => ?_, fun h => ?_⟩ <;>
     simp_all [Finset.mem_singleton]
 
@@ -296,10 +296,10 @@ This is structurally identical to @cite{kratzer-1991}'s analysis where:
 - The ordering source (for graded modality) is not used in PIP's
   simple must/might
 
-The formal connection is established via `Core.Logic.Intensional.boxR`:
-`must_truth_agrees_boxR` (in Connectives.lean) proves that PIP's
+The formal connection is established via `Core.Logic.Intensional.box`:
+`must_truth_agrees_box` (in Connectives.lean) proves that PIP's
 `must R allWorlds (atom p)` produces the same truth conditions as
-`boxR R (p g)`.
+`box R (p g)`.
 
 Direct import of `Semantics/Modality/Kratzer/` is not possible
 because Kratzer's implementation is monomorphic over `World4`. The
@@ -309,19 +309,19 @@ than definitional.
 
 /--
 Full Kratzer bridge: PIP's three-argument `mustBase` agrees with
-`boxR` when the modal base comes from an `AccessRel` and the restriction
+`box` when the modal base comes from an `AccessRel` and the restriction
 is tautological.
 
 The composition: `mustBase (accessRelToBase R w) ⊤ {w' | φ.truth w'}` ↔
-`boxR R φ.truth w`. Both express
+`box R φ.truth w`. Both express
 "the body holds at every R-accessible world from w".
 -/
-theorem mustBase_agrees_boxR {W D : Type*}
+theorem mustBase_agrees_box {W D : Type*}
     (R : AccessRel W) (φ : PIPExprF W D) (w : W) :
     mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } ↔
-    boxR R φ.truth w := by
+    box R φ.truth w := by
   simp only [mustBase, accessRelToBase, Set.inter_univ, Set.subset_def,
-    Set.mem_setOf_eq, boxR]
+    Set.mem_setOf_eq, box]
 
 
 -- ============================================================
diff --git a/Linglib/Studies/KeshetAbney2024/Composition.lean b/Linglib/Studies/KeshetAbney2024/Composition.lean
index f0fcb46b5..b5a4f25f5 100644
--- a/Linglib/Studies/KeshetAbney2024/Composition.lean
+++ b/Linglib/Studies/KeshetAbney2024/Composition.lean
@@ -26,7 +26,7 @@ type and connected to it via bridge theorems.
 
 namespace KeshetAbney2024.PIP
 
-open Core.Logic.Intensional (AccessRel boxR diamondR)
+open Core.Logic.Modal (AccessRel box diamond)
 
 
 -- ============================================================
@@ -241,13 +241,13 @@ def accessRelToBase (R : AccessRel W) (w : W) : Set W :=
   { w' | R w w' }
 
 /-- `PIPExprF.must R φ` truth agrees with three-argument `mustBase`.
-    Direct, since `must` truth is `boxR` and `mustBase` is set inclusion. -/
+    Direct, since `must` truth is `box` and `mustBase` is set inclusion. -/
 theorem must_truth_iff_mustBase {D : Type*}
     (R : AccessRel W) (φ : PIPExprF W D) (w : W) :
     (PIPExprF.must R φ).truth w ↔
     mustBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } := by
   simp only [mustBase, accessRelToBase, Set.inter_univ, Set.subset_def, Set.mem_setOf_eq,
-    PIPExprF.truth, boxR]
+    PIPExprF.truth, box]
 
 /-- `PIPExprF.might R φ` truth agrees with three-argument `mightBase`. -/
 theorem might_truth_iff_mightBase {D : Type*}
@@ -255,7 +255,7 @@ theorem might_truth_iff_mightBase {D : Type*}
     (PIPExprF.might R φ).truth w ↔
     mightBase (accessRelToBase R w) Set.univ { w' | φ.truth w' } := by
   simp only [mightBase, accessRelToBase, Set.inter_univ, Set.Nonempty,
-    Set.mem_inter_iff, Set.mem_setOf_eq, PIPExprF.truth, diamondR]
+    Set.mem_inter_iff, Set.mem_setOf_eq, PIPExprF.truth, diamond]
 
 end ThreeArgModals
 
diff --git a/Linglib/Studies/KeshetAbney2024/Connectives.lean b/Linglib/Studies/KeshetAbney2024/Connectives.lean
index 69a5d68e7..8b1763178 100644
--- a/Linglib/Studies/KeshetAbney2024/Connectives.lean
+++ b/Linglib/Studies/KeshetAbney2024/Connectives.lean
@@ -1,5 +1,5 @@
 import Linglib.Studies.KeshetAbney2024.Basic
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Mathlib.Data.Fintype.Basic
 
 /-!
@@ -26,15 +26,15 @@ PIP's modals are generalized quantifiers over worlds (paper Section 2.5):
 
 Our encoding parameterizes by an accessibility relation (`KeshetAbney2024.PIP.AccessRel`,
 equivalent to a Kratzer modal base β) and quantifies over accessible worlds.
-The grounding theorem `must_truth_agrees_boxR` proves that PIP's `must`
-produces the same truth conditions as `Core.Logic.Intensional.boxR`.
+The grounding theorem `must_truth_agrees_box` proves that PIP's `must`
+produces the same truth conditions as `Core.Logic.Intensional.box`.
 
 -/
 
 namespace KeshetAbney2024.PIP
 
 open Semantics.Dynamic.Core
-open Core.Logic.Intensional (AccessRel boxR diamondR boxR_T)
+open Core.Logic.Modal (AccessRel box diamond box_T)
 
 variable {W E : Type*}
 
@@ -278,24 +278,24 @@ end Properties
 
 
 -- ============================================================
--- Grounding: PIP modals ↔ Core.Logic.Intensional.boxR/diamondR
+-- Grounding: PIP modals ↔ Core.Logic.Intensional.box/diamond
 -- ============================================================
 
 /--
-PIP's `must` produces the same truth conditions as `Core.Logic.Intensional.boxR`.
+PIP's `must` produces the same truth conditions as `Core.Logic.Intensional.box`.
 
 Specifically: a pair (g, w₀) survives `must R allWorlds (atom p)` iff
-`boxR R (p g) w₀` — the body predicate holds at all R-accessible worlds.
+`box R (p g) w₀` — the body predicate holds at all R-accessible worlds.
 This connects PIP's discourse-update modals to the standard Kripke semantics
 used throughout `Semantics/Modality/`. Since accessibility is now the
 project-canonical Prop-valued `AccessRel`, the identity is direct — no lift.
 -/
-theorem must_truth_agrees_boxR [Fintype W]
+theorem must_truth_agrees_box [Fintype W]
     (R : AccessRel W) (p : ICDRTAssignment W E → W → Prop)
     (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W)
     (hd : (g, w₀) ∈ d.info) :
     ((g, w₀) ∈ (must R (Finset.univ : Finset W).toList (atom p) d).info) ↔
-    boxR R (p g) w₀ := by
+    box R (p g) w₀ := by
   constructor
   · intro ⟨_, h⟩ v hRv
     have := h v (Finset.mem_toList.mpr (Finset.mem_univ v)) hRv
@@ -308,14 +308,14 @@ theorem must_truth_agrees_boxR [Fintype W]
     exact ⟨modalExpand_adds_accessible d.info R g w₀ w₁ hd hacc, hbox w₁ hacc⟩
 
 /--
-PIP's `might` agrees with `diamondR`.
+PIP's `might` agrees with `diamond`.
 -/
-theorem might_truth_agrees_diamondR [Fintype W]
+theorem might_truth_agrees_diamond [Fintype W]
     (R : AccessRel W) (p : ICDRTAssignment W E → W → Prop)
     (d : Discourse W E) (g : ICDRTAssignment W E) (w₀ : W)
     (hd : (g, w₀) ∈ d.info) :
     ((g, w₀) ∈ (might R (Finset.univ : Finset W).toList (atom p) d).info) ↔
-    diamondR R (p g) w₀ := by
+    diamond R (p g) w₀ := by
   constructor
   · intro ⟨_, w₁, _, hacc, hmem⟩
     unfold atom Discourse.mapInfo at hmem
@@ -331,7 +331,7 @@ holds at (g, w₀), then `p g w₀`.
 
 This derives PIP's key insight — must allows anaphora because a realistic
 modal base guarantees the description holds at the evaluation world — from
-`Core.Logic.Intensional.boxR_T`.
+`Core.Logic.Modal.box_T`.
 -/
 theorem must_realistic_of_refl [Fintype W]
     (R : AccessRel W) [Std.Refl R]
@@ -340,7 +340,7 @@ theorem must_realistic_of_refl [Fintype W]
     (hd : (g, w₀) ∈ d.info)
     (hmust : (g, w₀) ∈ (must R (Finset.univ : Finset W).toList (atom p) d).info) :
     p g w₀ :=
-  boxR_T R (p g) w₀ ((must_truth_agrees_boxR R p d g w₀ hd).mp hmust)
+  box_T R (p g) w₀ ((must_truth_agrees_box R p d g w₀ hd).mp hmust)
 
 /--
 Pointwise realistic base: if `R w₀ w₀` and must holds at w₀,
diff --git a/Linglib/Studies/KeshetAbney2024/Expr.lean b/Linglib/Studies/KeshetAbney2024/Expr.lean
index 48bfaf67b..e43062d1a 100644
--- a/Linglib/Studies/KeshetAbney2024/Expr.lean
+++ b/Linglib/Studies/KeshetAbney2024/Expr.lean
@@ -1,5 +1,5 @@
 import Linglib.Studies.KeshetAbney2024.Basic
-import Linglib.Core.Logic.Intensional.Defs
+import Linglib.Core.Logic.Modal.Defs
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Fintype.Basic
 
@@ -41,7 +41,7 @@ all `X ≡ φ` definitions regardless of their structural position.
 
 namespace KeshetAbney2024.PIP
 
-open Core.Logic.Intensional (AccessRel boxR diamondR)
+open Core.Logic.Modal (AccessRel box diamond)
 
 /-- A finite domain of individuals for PIP quantifier evaluation. -/
 class FiniteDomain (D : Type*) where
@@ -118,8 +118,8 @@ def PIPExprF.truth {W D : Type*} :
   | .exists_ body => λ w => ∃ d, (body d).truth w
   | .forall_ body => λ w => ∀ d, (body d).truth w
   | .labelDef _label φ => φ.truth  -- label defs are tautological wrt truth
-  | .must R φ => boxR R φ.truth
-  | .might R φ => diamondR R φ.truth
+  | .must R φ => box R φ.truth
+  | .might R φ => diamond R φ.truth
 
 
 -- ============================================================
@@ -161,9 +161,9 @@ def PIPExprF.felicitous {W D : Type*} :
   -- F(X≡φ) iff Fφ  [labels don't affect felicity]
   | .labelDef _label φ => φ.felicitous
   -- F(□φ) iff ∀w'.Fφ  [felicity universal over accessible worlds]
-  | .must R φ => boxR R φ.felicitous
+  | .must R φ => box R φ.felicitous
   -- F(◇φ) iff ∀w'.Fφ  [felicity universal, NOT existential]
-  | .might R φ => boxR R φ.felicitous
+  | .might R φ => box R φ.felicitous
 
 
 -- ============================================================
@@ -236,7 +236,7 @@ theorem felicitousF_exists (body : D → PIPExprF W D) (w : W) :
 theorem felicitousF_must (R : AccessRel W) (φ : PIPExprF W D)
     (w : W) :
     (PIPExprF.must R φ).felicitous w =
-    boxR R φ.felicitous w := rfl
+    box R φ.felicitous w := rfl
 
 end Properties
 
diff --git a/Linglib/Studies/KeshetAbney2024/Felicity.lean b/Linglib/Studies/KeshetAbney2024/Felicity.lean
index 825246164..f8ee140c6 100644
--- a/Linglib/Studies/KeshetAbney2024/Felicity.lean
+++ b/Linglib/Studies/KeshetAbney2024/Felicity.lean
@@ -57,7 +57,7 @@ world and assignment consistent with γ.
 
 namespace KeshetAbney2024.PIP.Felicity
 
-open Core.Logic.Intensional (AccessRel boxR diamondR)
+open Core.Logic.Modal (AccessRel box diamond)
 
 variable {W : Type*}
 
@@ -308,7 +308,7 @@ theorem existsF_forallF_felicity_agree (body : D → PIPExprF W D) (w : W) :
     (PIPExprF.forall_ body).felicitous w := rfl
 
 /-- F(□_R φ) iff φ is felicitous at every R-accessible world.
-    Holds by definition (`must` felicity is `boxR`). -/
+    Holds by definition (`must` felicity is `box`). -/
 theorem mustF_felicitous_iff (R : AccessRel W) (φ : PIPExprF W D) (w : W) :
     (PIPExprF.must R φ).felicitous w ↔ ∀ w', R w w' → φ.felicitous w' :=
   Iff.rfl
@@ -371,7 +371,7 @@ theorem mustF_presup_factored
     (PIPExprF.must R (PIPExprF.presup φ ψ)).felicitous w ↔
     (∀ w', R w w' → φ.felicitous w') ∧
     (∀ w', R w w' → ψ w') := by
-  simp only [PIPExprF.felicitous, boxR]
+  simp only [PIPExprF.felicitous, box]
   exact ⟨fun h => ⟨fun w' hw' => (h w' hw').1, fun w' hw' => (h w' hw').2⟩,
          fun ⟨h1, h2⟩ w' hw' => ⟨h1 w' hw', h2 w' hw'⟩⟩
 
@@ -381,7 +381,7 @@ theorem mightF_presup_factored
     (PIPExprF.might R (PIPExprF.presup φ ψ)).felicitous w ↔
     (∀ w', R w w' → φ.felicitous w') ∧
     (∀ w', R w w' → ψ w') := by
-  simp only [PIPExprF.felicitous, boxR]
+  simp only [PIPExprF.felicitous, box]
   exact ⟨fun h => ⟨fun w' hw' => (h w' hw').1, fun w' hw' => (h w' hw').2⟩,
          fun ⟨h1, h2⟩ w' hw' => ⟨h1 w' hw', h2 w' hw'⟩⟩
 
diff --git a/Linglib/Studies/Wang2025.lean b/Linglib/Studies/Wang2025.lean
index 6836b844b..2236073ed 100644
--- a/Linglib/Studies/Wang2025.lean
+++ b/Linglib/Studies/Wang2025.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.Rat.Defs
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Linglib.Discourse.CommonGround
 import Linglib.Semantics.Presupposition.Basic
 import Linglib.Features.Acceptability
@@ -189,7 +189,7 @@ open CommonGround (ContextSet)
 
 /-- Local Bool-valued accessibility used by Wang2025 for `List.all` evaluation
 of the speaker-K operator. The Prop-valued canonical version lives in
-`Core.Logic.Intensional.AccessRel`; lift via
+`Core.Logic.Modal.AccessRel`; lift via
 `fun a b => R a b = true` to bridge. -/
 abbrev BAccessRel (W : Type*) := W → W → Bool
 open Semantics.Presupposition.TriggerTypology (AltStructure Obligatoriness)
@@ -356,7 +356,7 @@ epistemic stance. It scopes relative to exh_mx:
 - exh_mx >> K: available for complex sentences
 
 Uses a local Bool-valued accessibility relation; for the Prop-valued
-canonical Kripke semantics see `Core.Logic.Intensional.boxR`.
+canonical Kripke semantics see `Core.Logic.Intensional.box`.
 -/
 noncomputable def speakerK [Fintype W] (R : BAccessRel W) (φ : (W → Bool)) : (W → Bool) :=
   fun w => ((Finset.univ : Finset W).toList.filter (R w)).all φ
diff --git a/Linglib/Studies/ZwickyPullum1983.lean b/Linglib/Studies/ZwickyPullum1983.lean
index 3297ac517..05df37104 100644
--- a/Linglib/Studies/ZwickyPullum1983.lean
+++ b/Linglib/Studies/ZwickyPullum1983.lean
@@ -1,6 +1,6 @@
 import Linglib.Morphology.MorphRule
 import Linglib.Fragments.English.Auxiliaries
-import Linglib.Core.Logic.Intensional.RestrictedModality
+import Linglib.Core.Logic.Modal.Basic
 import Mathlib.Data.Fin.Basic
 
 -- ============================================================================
@@ -322,14 +322,14 @@ if *-n't* is an affix, it forms a lexical unit with the auxiliary, and
 lexical items can have idiosyncratic scope properties. If *-n't* were
 a clitic (a reduced form of *not*), its scope should always match *not*.
 
-We formalize this using `boxR`/`diamondR` from
+We formalize this using `box`/`diamond` from
 `Core.Logic.Intensional`: a Kripke countermodel exhibits
 an accessibility relation under which the two scope readings diverge. -/
 
 section ScopeBridge
 
 open Semantics.Modality (ModalForce)
-open Core.Logic.Intensional (AccessRel boxR diamondR)
+open Core.Logic.Modal (AccessRel box diamond)
 
 abbrev World := Fin 4
 
@@ -416,11 +416,11 @@ accesses worlds where P differs, ◇P and ◇¬P are both true, so
 theorem neg_over_poss_ne_poss_over_neg :
     ∃ (R : AccessRel World),
     ¬(∀ (p : World → Prop) (w : World),
-      ¬ diamondR R p w ↔ diamondR R (fun w' => ¬ p w') w) := by
+      ¬ diamond R p w ↔ diamond R (fun w' => ¬ p w') w) := by
   refine ⟨kripkeR, ?_⟩
   intro h
   have := h witnessP (0 : World)
-  simp [diamondR, kripkeR, witnessP] at this
+  simp [diamond, kripkeR, witnessP] at this
 
 /-- NOT(MUST(P)) and MUST(NOT(P)) are not equivalent in general.
 
@@ -430,11 +430,11 @@ necessarily false (□¬P = false when P holds at w1). -/
 theorem neg_over_nec_ne_nec_over_neg :
     ∃ (R : AccessRel World),
     ¬(∀ (p : World → Prop) (w : World),
-      ¬ boxR R p w ↔ boxR R (fun w' => ¬ p w') w) := by
+      ¬ box R p w ↔ box R (fun w' => ¬ p w') w) := by
   refine ⟨kripkeR, ?_⟩
   intro h
   have := h witnessP (0 : World)
-  simp [boxR, kripkeR, witnessP] at this
+  simp [box, kripkeR, witnessP] at this
 
 end ScopeBridge