Cumulative Predication

@cite{krifka-1989} @cite{sternefeld-1998} @cite{beck-sauerland-2000}

Formalises the cumulative operator **. The operator's lineage:

• @cite{krifka-1989}: original closure-form definition (smallest relation closed under ⟨a,b⟩+⟨c,d⟩ → ⟨a∪c, b∪d⟩).
• @cite{sternefeld-1998}: extension to the n-ary case (paper §3.1 defines *** for three-place relations) — formalised in Phenomena/Anaphora/Studies/Sternefeld1998.lean (just the binary closure form so far).
• @cite{beck-sauerland-2000}: the bidirectional-coverage reformulation (∀a∈x. ∃b∈y. R(a,b)) ∧ (∀b∈y. ∃a∈x. R(a,b)) that this file uses.

The two formulations are equivalent on Quine-innovation domains; the forward direction closure → coverage is proven in Studies/Sternefeld1998.lean::sternefeldStarStar_implies_cumulative.

Distinction from CUM Reference

Link's CUM (Mereology.CUM) is a property of denotations: a predicate P has cumulative reference iff P(x) ∧ P(y) → P(x ⊔ y). That is a closure condition on extensions.

The ** operator here takes a two-place predicate and returns a new predicate with cumulative truth conditions. The output of ** applied to a non-cumulative predicate is itself cumulative.

Consumers

• @cite{guerrini-2026} §4 uses ** for cumulative kind predication: "Elephants live in Africa and Asia" is true iff every elephant lives in at least one of Africa/Asia, and each of Africa/Asia has at least one elephant living in it.
• @cite{haug-dalrymple-2020} consumes ** indirectly via the bridge theorem groupIdentityCond_iff_cumulative_eq in Theories/Semantics/Dynamic/PPCDRT/Cumulativity.lean: H&D's group identity condition is ** applied to equality on the sum-dref value-sets — formalising @cite{langendoen-1978}'s reciprocity-as- cumulativity claim within PPCDRT.
• @cite{beck-2001} §4.3 derives Weak Reciprocity from **(λxλy.[R(x,y) ∧ @(x ≠ y)])(A,A) (paper eq 120) — ** applied to the verb relation strengthened by presupposed distinctness. See Phenomena/Anaphora/Studies/Beck2001.lean.
• @cite{sternefeld-1998} §3 derives Weak Reciprocity from ⟨A, A⟩ ∈ **λxy[R(x,y) ∧ x ≠ y] (paper eq 26b) — same shape as Beck eq 120 but with asserted distinctness. In bivalent encoding the two predicates coincide. See Phenomena/Anaphora/Studies/Sternefeld1998.lean (which also defines @cite{krifka-1989}'s closure form ** and proves the forward direction of its equivalence to the bidirectional-coverage form here).

def Semantics.Plurality.Cumulativity.Cumulative {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) : Prop

The cumulative operator ** in @cite{beck-sauerland-2000}'s bidirectional-coverage form.

Given a two-place predicate R and two pluralities x : Finset A, y : Finset B:

**(R)(x, y) = [∀a ∈ x. ∃b ∈ y. R(a, b)] ∧ [∀b ∈ y. ∃a ∈ x. R(a, b)]

Both argument pluralities must be "covered": every atom in x is R-related to some atom in y, and vice versa.

Heterogeneous: A and B may be different types (e.g., Elephant × Continent).

Equations

• Semantics.Plurality.Cumulativity.Cumulative R x y = ((∀ a ∈ x, ∃ b ∈ y, R a b) ∧ ∀ b ∈ y, ∃ a ∈ x, R a b)

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.Cumulative.instDecidable {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (R : A → B → Prop) [(a : A) → (b : B) → Decidable (R a b)] (x : Finset A) (y : Finset B) : Decidable (Cumulative R x y)

Equations

• Semantics.Plurality.Cumulativity.Cumulative.instDecidable R x y = id inferInstance

def Semantics.Plurality.Cumulativity.LeftCoverage {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) : Prop

Left coverage: every atom in x is R-related to some atom in y.

Equations

• Semantics.Plurality.Cumulativity.LeftCoverage R x y = ∀ a ∈ x, ∃ b ∈ y, R a b

def Semantics.Plurality.Cumulativity.RightCoverage {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) : Prop

Right coverage: every atom in y is R-related to some atom in x.

Equations

• Semantics.Plurality.Cumulativity.RightCoverage R x y = ∀ b ∈ y, ∃ a ∈ x, R a b

theorem Semantics.Plurality.Cumulativity.cumulative_iff_coverages {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) : Cumulative R x y ↔ LeftCoverage R x y ∧ RightCoverage R x y

** is the conjunction of left and right coverage.

theorem Semantics.Plurality.Cumulativity.cumulative_left_universal {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) (h : Cumulative R x y) (a : A) (ha : a ∈ x) : ∃ b ∈ y, R a b

** entails DIST on the left argument: if **(R)(x, y) then every atom in x is R-related to something in y (left universality).

theorem Semantics.Plurality.Cumulativity.cumulative_right_universal {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : Finset B) (h : Cumulative R x y) (b : B) (hb : b ∈ y) : ∃ a ∈ x, R a b

** entails DIST on the right argument: if **(R)(x, y) then every atom in y is R-related to something in x (right universality).

theorem Semantics.Plurality.Cumulativity.singleton_right_left_coverage {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : B) : LeftCoverage R x {y} ↔ ∀ a ∈ x, R a y

Left coverage with singleton right argument reduces to universal quantification.

When the right plurality has exactly one element y, left coverage becomes: ∀a ∈ x. R(a, y).

This is one half of @cite{johnston-2023}'s "number effect": with a singular object DP, the cumulative reading collapses to universal distribution, eliminating the pairing uncertainty that motivates over-informative elaboration.

theorem Semantics.Plurality.Cumulativity.singleton_right_cumulative {A : Type u_1} {B : Type u_2} (R : A → B → Prop) (x : Finset A) (y : B) (hne : x.Nonempty) : Cumulative R x {y} ↔ ∀ a ∈ x, R a y

Full ** with singleton right argument and nonempty left argument.

When |Y| = 1 and X is nonempty, **(R)(X, {y}) = ∀a ∈ X. R(a, y). Right coverage is trivially satisfied by any witness from X.

inductive Semantics.Plurality.Cumulativity.Elephant : Type

• dumbo : Elephant
• babar : Elephant
• tantor : Elephant

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instDecidableEqElephant : DecidableEq Elephant

Equations

• Semantics.Plurality.Cumulativity.instDecidableEqElephant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instReprElephant : Repr Elephant

Equations

• Semantics.Plurality.Cumulativity.instReprElephant = { reprPrec := Semantics.Plurality.Cumulativity.instReprElephant.repr }

def Semantics.Plurality.Cumulativity.instReprElephant.repr : Elephant → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Semantics.Plurality.Cumulativity.Continent : Type

• africa : Continent
• asia : Continent

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instDecidableEqContinent : DecidableEq Continent

Equations

• Semantics.Plurality.Cumulativity.instDecidableEqContinent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instReprContinent : Repr Continent

Equations

• Semantics.Plurality.Cumulativity.instReprContinent = { reprPrec := Semantics.Plurality.Cumulativity.instReprContinent.repr }

def Semantics.Plurality.Cumulativity.instReprContinent.repr : Continent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instFintypeElephant : Fintype Elephant

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instFintypeContinent : Fintype Continent

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Plurality.Cumulativity.livesIn : Elephant → Continent → Prop

Equations

• Semantics.Plurality.Cumulativity.livesIn Semantics.Plurality.Cumulativity.Elephant.dumbo Semantics.Plurality.Cumulativity.Continent.africa = True
• Semantics.Plurality.Cumulativity.livesIn Semantics.Plurality.Cumulativity.Elephant.babar Semantics.Plurality.Cumulativity.Continent.africa = True
• Semantics.Plurality.Cumulativity.livesIn Semantics.Plurality.Cumulativity.Elephant.tantor Semantics.Plurality.Cumulativity.Continent.asia = True
• Semantics.Plurality.Cumulativity.livesIn x✝¹ x✝ = False

@[implicit_reducible]

instance Semantics.Plurality.Cumulativity.instDecidableRelElephantContinentLivesIn : DecidableRel livesIn

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Plurality.Cumulativity.allElephants : Finset Elephant

Equations

• Semantics.Plurality.Cumulativity.allElephants = Finset.univ

def Semantics.Plurality.Cumulativity.africaAndAsia : Finset Continent

Equations

• Semantics.Plurality.Cumulativity.africaAndAsia = Finset.univ