refactor(Core/Logic/Modal): relocate Kripke foundation, boxR→box

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

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

Linglib/Core/Logic/Intensional/Defs.lean → 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,33 +144,33 @@ 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
 
 -- ────────────────────────────────────────────────────────────────
 -- §5 Duality
 -- ────────────────────────────────────────────────────────────────
 
 /-- `□_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

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 -/
 

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]

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

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