Lumping

@cite{kratzer-1989}, @cite{kratzer-2012}

Kratzer's situation-semantic notion of lumping: a proposition p lumps a proposition q in a world w when truth of p at every part of w forces truth of q there. Lumping is the technical glue Kratzer uses to repair the premise-semantic account of counterfactuals — when an antecedent is added to a Base Set, every proposition lumped by the antecedent in the evaluation world comes along, blocking the spurious 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 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, aliased as Persistent in Situations.lean).

Scope

This file covers @cite{kratzer-2012} §5.3.3 (p. 118): the worlds-only logical relations (validity, consistency, compatibility, logical consequence, logical equivalence) and the official lumping definition that closes the section. The counterfactual machinery of §5.4 — base sets, the truth conditions for would/might-counterfactuals, and the formal definitions in §5.4.4 — is out of scope here.

Architectural notes

• Lumping is order-theoretic. Lumps is parametric in any [Preorder S]; only the worlds-restricted relations are bundled through SituationFrame. Mirrors how Persistent is generalized in Situations.lean.
• Logical relations follow Kratzer's set notation literally. Each definition unfolds to the same set-theoretic formula on p. 118 (F.Worlds ⊆ p, F.Worlds ∩ ⋂₀ A ⊆ q, etc.), so the mathlib Set and sInter APIs apply unchanged.
• Worlds vs. arbitrary situations. Kratzer's official definition restricts Lumps p q w to w ∈ W. We define the relation for any situation; combine with IsWorld w (from Situations.lean) for the standard restriction. The Lumps.follows_singleton bridge below shows how to recover Kratzer's worlds-only reading.

Lumping (@cite{kratzer-2012} §5.3.3, p. 118)

The official text of @cite{kratzer-2012}, p. 118:

For all propositions p, q ∈ P(S) and all w ∈ W: p lumps q in w iff (i) w ∈ p. (ii) For all s ∈ S, if s ≤ w and s ∈ p, then s ∈ q.

The same definition appears informally on p. 114, where footnote 4 credits condition (ii) to Yablo's "local implication".

structure Core.Logic.Intensional.Lumping.Lumps {S : Type u_1} [Preorder S] (p q : Set S) (w : S) : Prop

Lumps: p lumps q at w iff (i) p is true at w, and (ii) every part of w at which p is true is also a part at which q is true.

Generalized from @cite{kratzer-2012}'s situation-frame setting to any preordered carrier S; the parthood preorder is the only piece of structure the definition uses.

• holds : w ∈ p

  p is true at w (@cite{kratzer-2012}, p. 118, condition (i)).

• localImpl ⦃s : S⦄ : s ≤ w → s ∈ p → s ∈ q

  Every part of w at which p is true also has q true (@cite{kratzer-2012}, p. 118, condition (ii); = Yablo's "local implication", noted in footnote 4 of @cite{kratzer-2012}, p. 114).

theorem Core.Logic.Intensional.Lumping.Lumps.holds_target {S : Type u_1} [Preorder S] {p q : Set S} {w : S} (h : Lumps p q w) : w ∈ q

Setting s = w in the local-implication conjunct: q is true at w whenever p lumps q there.

theorem Core.Logic.Intensional.Lumping.Lumps.refl_of_holds {S : Type u_1} [Preorder S] {p : Set S} {w : S} (hp : w ∈ p) : Lumps p p w

A true proposition lumps itself (reflexivity, conditional on truth).

theorem Core.Logic.Intensional.Lumping.Lumps.trans {S : Type u_1} [Preorder S] {p q r : Set S} {w : S} (hpq : Lumps p q w) (hqr : Lumps q r w) : Lumps p r w

Lumping composes.

theorem Core.Logic.Intensional.Lumping.Lumps.inter {S : Type u_1} [Preorder S] {p q r : Set S} {w : S} (hq : Lumps p q w) (hr : Lumps p r w) : Lumps p (q ∩ r) w

If p lumps both q and r at w, it lumps their intersection.

theorem Core.Logic.Intensional.Lumping.Lumps.mono_left {S : Type u_1} [Preorder S] {p q : Set S} {w : S} {p' : Set S} (hp' : p' ⊆ p) (hp'w : w ∈ p') (h : Lumps p q w) : Lumps p' q w

Strengthening the lumping proposition: a pointwise stronger p' (true at w) inherits everything p lumps.

theorem Core.Logic.Intensional.Lumping.Lumps.mono_right {S : Type u_1} [Preorder S] {p q : Set S} {w : S} {q' : Set S} (hq' : q ⊆ q') (h : Lumps p q w) : Lumps p q' w

Weakening the lumped proposition: pointwise entailment lifts.

theorem Core.Logic.Intensional.Lumping.Lumps.of_local_universal {S : Type u_1} [Preorder S] {p q : Set S} {w : S} (hp : w ∈ p) (hq : ∀ ⦃s : S⦄, s ≤ w → s ∈ q) : Lumps p q w

A proposition true at every part of w is lumped by every proposition true at w. (Strictly weaker hypothesis than "true everywhere": only the parts of w matter.)

Logical relations (@cite{kratzer-2012} §5.3.3, p. 118)

These quantify only over F.Worlds (maximal situations) and so remain "classical" — equivalent to their possible-worlds counterparts on the worlds part of F.Index. We follow Kratzer's set-theoretic notation verbatim.

def Core.Logic.Intensional.Lumping.IsValid {F : SituationFrame} (p : Set F.Index) : Prop

Validity (@cite{kratzer-2012}, p. 118): every world satisfies p. Kratzer writes this as p ∩ W = W; equivalently F.Worlds ⊆ p.

Equations

• Core.Logic.Intensional.Lumping.IsValid p = (F.Worlds ⊆ p)

def Core.Logic.Intensional.Lumping.Follows {F : SituationFrame} (A : Set (Set F.Index)) (q : Set F.Index) : Prop

Logical consequence (@cite{kratzer-2012}, p. 118): every world that satisfies all of A also satisfies q. Kratzer's text: "for all w ∈ W: if w ∈ ⋂A, then w ∈ q."

Equations

• Core.Logic.Intensional.Lumping.Follows A q = (F.Worlds ∩ ⋂₀ A ⊆ q)

def Core.Logic.Intensional.Lumping.IsConsistent {F : SituationFrame} (A : Set (Set F.Index)) : Prop

Consistency (@cite{kratzer-2012}, p. 118): some world satisfies every member of A.

Equations

• Core.Logic.Intensional.Lumping.IsConsistent A = (F.Worlds ∩ ⋂₀ A).Nonempty

def Core.Logic.Intensional.Lumping.IsCompatible {F : SituationFrame} (p : Set F.Index) (A : Set (Set F.Index)) : Prop

Compatibility (@cite{kratzer-2012}, p. 118): p is compatible with A iff A ∪ {p} is consistent.

Equations

• Core.Logic.Intensional.Lumping.IsCompatible p A = Core.Logic.Intensional.Lumping.IsConsistent (insert p A)

def Core.Logic.Intensional.Lumping.LogEquiv {F : SituationFrame} (p q : Set F.Index) : Prop

Logical equivalence (@cite{kratzer-2012}, p. 118): p and q agree on the worlds part. Kratzer writes p ∩ W = q ∩ W.

Renamed from Kratzer's "logical equivalence" to LogEquiv to avoid collision with mathlib's Equiv (type equivalences).

Equations

• Core.Logic.Intensional.Lumping.LogEquiv p q = (p ∩ F.Worlds = q ∩ F.Worlds)

Characterizations

theorem Core.Logic.Intensional.Lumping.Follows.of_mem {F : SituationFrame} {A : Set (Set F.Index)} {p : Set F.Index} (hp : p ∈ A) : Follows A p

A premise in a set is a logical consequence of the set.

theorem Core.Logic.Intensional.Lumping.isValid_iff_follows_empty {F : SituationFrame} {p : Set F.Index} : IsValid p ↔ Follows ∅ p

Validity is logical consequence from no premises.

theorem Core.Logic.Intensional.Lumping.isConsistent_iff_not_follows_empty_set {F : SituationFrame} {A : Set (Set F.Index)} : IsConsistent A ↔ ¬Follows A ∅

Consistency of A is the negation of "false follows from A".

@[simp]

theorem Core.Logic.Intensional.Lumping.isCompatible_iff_isConsistent_insert {F : SituationFrame} {p : Set F.Index} {A : Set (Set F.Index)} : IsCompatible p A ↔ IsConsistent (insert p A)

Compatibility unfolds to consistency of the augmented set (definitional; this lemma exists for simp-style rewriting).

Bridge: lumping and logical consequence

If p lumps q at every world satisfying p, then q follows logically from p. This is the cleanest connection between the order-theoretic core (Lumps) and the worlds-restricted relations (Follows).

theorem Core.Logic.Intensional.Lumping.Lumps.follows_singleton {F : SituationFrame} {p q : Set F.Index} (h : ∀ w ∈ F.Worlds, w ∈ p → Lumps p q w) : Follows {p} q

Worlds-restricted lumping entails logical consequence from the singleton premise set. The hypothesis is Kratzer 2012's standard "for all w ∈ W" pattern: at every world where p holds, p lumps q there, so q holds at that world.

Possible-worlds reduction

In a discrete situation frame (a Frame promoted via Frame.toDiscreteSituationFrame), parthood reduces to equality. The local-implication conjunct then collapses, and lumping at any index w becomes joint truth at w — a degenerate notion. This is the formal sense in which possible-worlds semantics flattens the distinctions Kratzer's lumping is designed to capture.

@[implicit_reducible]

def Core.Logic.Intensional.Lumping.instPartialOrderIndex (G : Frame) : PartialOrder G.Index

Bring the discrete partial order on G.Index into scope so the corollary below can quote Lumps without explicit @-application.

Equations

• Core.Logic.Intensional.Lumping.instPartialOrderIndex G = Core.Logic.Intensional.discreteOrder G.Index

theorem Core.Logic.Intensional.Lumping.Lumps.discrete_iff (G : Frame) (p q : Set G.Index) (w : G.Index) : Lumps p q w ↔ w ∈ p ∧ w ∈ q

Lumping in a discrete frame collapses to joint truth at the index.