refactor(Core/Logic): move ConvBackground and Lumping out of Intensional into Semantics

Linglib.lean

@@ -66,9 +66,9 @@ import Linglib.Core.Logic.Intensional.Algebra
 import Linglib.Core.Logic.Intensional.CategoryType
 import Linglib.Core.Logic.Intensional.RestrictedModality
 import Linglib.Core.Logic.Intensional.Premise
-import Linglib.Core.Logic.Intensional.ConversationalBackground
+import Linglib.Semantics.Modality.Kratzer.ConversationalBackground
 import Linglib.Core.Logic.Intensional.Situations
-import Linglib.Core.Logic.Intensional.Lumping
+import Linglib.Semantics.Conditionals.Counterfactual.Lumping
 import Linglib.Core.Logic.BeliefRevision
 import Linglib.Core.Order.Tree
 import Linglib.Core.Order.Command

Linglib/Core/Logic/Intensional/Lumping.lean → Linglib/Semantics/Conditionals/Counterfactual/Lumping.lean

@@ -16,7 +16,7 @@ counterfactuals that arise when independent true propositions are added
 freely (the Paula-paints-a-still-life and zebra-escapes examples in
 @cite{kratzer-2012}, §5.4.1).
 
-This module sits on top of `Core.Logic.Intensional.Situations`, which
+This module sits on top of `Core/Logic/Intensional/Situations.lean`, which
 provides the `SituationFrame` carrier — a `Frame` whose `Index` carries
 a partial order representing parthood. Propositions are `Set F.Index`;
 the order grounds both lumping and persistence (= mathlib's `Monotone`,
@@ -48,9 +48,10 @@ formal definitions in §5.4.4 — is out of scope here.
   shows how to recover Kratzer's worlds-only reading.
 -/
 
-namespace Core.Logic.Intensional.Lumping
+namespace Semantics.Conditionals.Counterfactual
 
 open Set
+open Core.Logic.Intensional
 
 /-! ## Lumping (@cite{kratzer-2012} §5.3.3, p. 118)
 
@@ -242,4 +243,4 @@ theorem Lumps.discrete_iff (p q : Set G.Index) (w : G.Index) :
 
 end DiscreteCorollary
 
-end Core.Logic.Intensional.Lumping
+end Semantics.Conditionals.Counterfactual

Linglib/Semantics/Conditionals/PremiseSemantic.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.Logic.Intensional.Lumping
+import Linglib.Semantics.Conditionals.Counterfactual.Lumping
 
 /-!
 # Kratzer 2012 Premise-Semantic Counterfactuals
@@ -76,7 +76,7 @@ three, the lumping CF does NOT use `SimilarityOrdering` /
 namespace Semantics.Conditionals.PremiseSemantic
 
 open Core.Logic.Intensional
-open Core.Logic.Intensional.Lumping (Lumps IsConsistent IsCompatible Follows)
+open Semantics.Conditionals.Counterfactual (Lumps IsConsistent IsCompatible Follows)
 
 variable {F : SituationFrame}
 

Linglib/Core/Logic/Intensional/ConversationalBackground.lean → Linglib/Semantics/Modality/Kratzer/ConversationalBackground.lean

@@ -10,14 +10,11 @@ A conversational background maps worlds to sets of propositions. Two roles:
 - **Modal base** (`ModalBase`) determines accessibility — `R_f(w, w') ≡ w' ∈ ⋂f(w)`.
 - **Ordering source** (`OrderingSource`) ranks accessible worlds by how many
   ordering propositions they satisfy.
-
-Despite being introduced by Kratzer for natural-language modality, these are
-generic IL primitives — no Kratzer-specific commitments live here. The
-Kratzer-flavored modality theory in `Semantics/Modality/Kratzer/`
-re-exports these so that consumers can keep using either namespace.
 -/
 
-namespace Core.Logic.Intensional
+open Core.Logic.Intensional.Premise (propIntersection)
+
+namespace Semantics.Modality.Kratzer
 
 variable {W : Type*}
 
@@ -45,11 +42,11 @@ def isRealistic (f : ConvBackground W) : Prop :=
     `⋂f(w) = {w}`. The strongest form: only the actual world is accessible.
     UNVERIFIED page reference. -/
 def isTotallyRealistic (f : ConvBackground W) : Prop :=
-  ∀ w : W, Premise.propIntersection (f w) = {w}
+  ∀ w : W, propIntersection (f w) = {w}
 
 /-- The **empty** conversational background: `f(w) = ∅` for all w.
     `⋂f(w) = W` (vacuous intersection), so the empty background is itself
     trivially realistic. UNVERIFIED page reference. -/
 def emptyBackground : ConvBackground W := λ _ => []
 
-end Core.Logic.Intensional
+end Semantics.Modality.Kratzer

Linglib/Semantics/Modality/Kratzer/Ordering.lean

@@ -12,24 +12,22 @@ All types are polymorphic over the world type `W`. Propositions are
 - Kratzer, A. (1981). The Notional Category of Modality. de Gruyter. pp. 38-74.
 -/
 
-import Linglib.Core.Logic.Intensional.ConversationalBackground
+import Linglib.Semantics.Modality.Kratzer.ConversationalBackground
 import Linglib.Core.Order.Normality
 import Mathlib.Order.Basic
 import Mathlib.Data.Set.Basic
 
 namespace Semantics.Modality.Kratzer
 
-/-! The conversational-background primitives live in
-`Core.Logic.Intensional`; re-export them under `Semantics.Modality.Kratzer`
-so the historical `Kratzer.foo` call style continues to work. -/
+/-! The premise primitives live in `Core.Logic.Intensional.Premise`; re-export
+them under `Semantics.Modality.Kratzer` so the historical `Kratzer.foo` call
+style continues to work. The conversational-background primitives
+(`ConvBackground`, `ModalBase`, …) are defined directly in this namespace by
+`ConversationalBackground.lean`. -/
 
 export Core.Logic.Intensional.Premise
   (propExtension propIntersection followsFrom isConsistent isCompatibleWith)
 
-export Core.Logic.Intensional
-  (ConvBackground ModalBase OrderingSource isRealistic isTotallyRealistic
-   emptyBackground)
-
 variable {W : Type*}
 
 /--

Linglib/Studies/CiardelliZhangChampollion2018Lumping.lean

@@ -85,7 +85,7 @@ The empty Base Set keeps the proofs direct.
 namespace CiardelliZhangChampollion2018Lumping
 
 open Core.Logic.Intensional
-open Core.Logic.Intensional.Lumping (Lumps IsConsistent IsCompatible Follows)
+open Semantics.Conditionals.Counterfactual (Lumps IsConsistent IsCompatible Follows)
 open Semantics.Conditionals.PremiseSemantic
   (CrucialSet IsCrucialSet wouldCF)
 

Linglib/Studies/Kratzer2012Lumping.lean

@@ -138,7 +138,7 @@ still-life painting variant from §5.2.
 namespace Kratzer2012Lumping
 
 open Core.Logic.Intensional
-open Core.Logic.Intensional.Lumping (Lumps IsConsistent IsCompatible Follows)
+open Semantics.Conditionals.Counterfactual (Lumps IsConsistent IsCompatible Follows)
 open Semantics.Conditionals.PremiseSemantic
 
 /-! ## The minimal Paula scenario -/