Cumulative Predication

Formalizes Beck & Sauerland's cumulative operator **, which derives cumulative truth conditions from transitive predicates applied to pluralities.

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.

Beck & Sauerland's ** is an operator that 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.

Connection to Distributivity

DIST (in Distributivity.lean) universally distributes a one-place predicate over atoms of a plurality:

DIST(P)(x) = ∀a ≤ x. P(a)

** symmetrically distributes a two-place predicate over atoms of both argument pluralities:

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

@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.

def Semantics.Lexical.Plural.Cumulativity.cumulativeOp {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) : Bool

The cumulative operator ** (Beck & Sauerland 2000).

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.Lexical.Plural.Cumulativity.cumulativeOp R x y = (decide (∀ a ∈ x, ∃ b ∈ y, R a b = true) && decide (∀ b ∈ y, ∃ a ∈ x, R a b = true))

def Semantics.Lexical.Plural.Cumulativity.leftCoverage {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) : Bool

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

Equations

• Semantics.Lexical.Plural.Cumulativity.leftCoverage R x y = decide (∀ a ∈ x, ∃ b ∈ y, R a b = true)

def Semantics.Lexical.Plural.Cumulativity.rightCoverage {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) : Bool

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

Equations

• Semantics.Lexical.Plural.Cumulativity.rightCoverage R x y = decide (∀ b ∈ y, ∃ a ∈ x, R a b = true)

theorem Semantics.Lexical.Plural.Cumulativity.cumulativeOp_eq_coverages {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) : cumulativeOp R x y = (leftCoverage R x y && rightCoverage R x y)

** is the conjunction of left and right coverage.

theorem Semantics.Lexical.Plural.Cumulativity.cumulativeOp_left_universal {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) (h : cumulativeOp R x y = true) (a : A) (ha : a ∈ x) : ∃ b ∈ y, R a b = true

** 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.Lexical.Plural.Cumulativity.cumulativeOp_right_universal {A B : Type} (R : A → B → Bool) (x : Finset A) (y : Finset B) (h : cumulativeOp R x y = true) (b : B) (hb : b ∈ y) : ∃ a ∈ x, R a b = true

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

inductive Semantics.Lexical.Plural.Cumulativity.Elephant : Type

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

instance Semantics.Lexical.Plural.Cumulativity.instDecidableEqElephant : DecidableEq Elephant

Equations

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

def Semantics.Lexical.Plural.Cumulativity.instBEqElephant.beq : Elephant → Elephant → Bool

Equations

• Semantics.Lexical.Plural.Cumulativity.instBEqElephant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Plural.Cumulativity.instBEqElephant : BEq Elephant

Equations

• Semantics.Lexical.Plural.Cumulativity.instBEqElephant = { beq := Semantics.Lexical.Plural.Cumulativity.instBEqElephant.beq }

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

Equations

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

instance Semantics.Lexical.Plural.Cumulativity.instReprElephant : Repr Elephant

Equations

• Semantics.Lexical.Plural.Cumulativity.instReprElephant = { reprPrec := Semantics.Lexical.Plural.Cumulativity.instReprElephant.repr }

inductive Semantics.Lexical.Plural.Cumulativity.Continent : Type

• africa : Continent
• asia : Continent

instance Semantics.Lexical.Plural.Cumulativity.instDecidableEqContinent : DecidableEq Continent

Equations

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

instance Semantics.Lexical.Plural.Cumulativity.instBEqContinent : BEq Continent

Equations

• Semantics.Lexical.Plural.Cumulativity.instBEqContinent = { beq := Semantics.Lexical.Plural.Cumulativity.instBEqContinent.beq }

def Semantics.Lexical.Plural.Cumulativity.instBEqContinent.beq : Continent → Continent → Bool

Equations

• Semantics.Lexical.Plural.Cumulativity.instBEqContinent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Plural.Cumulativity.instReprContinent : Repr Continent

Equations

• Semantics.Lexical.Plural.Cumulativity.instReprContinent = { reprPrec := Semantics.Lexical.Plural.Cumulativity.instReprContinent.repr }

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

Equations

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

instance Semantics.Lexical.Plural.Cumulativity.instFintypeElephant : Fintype Elephant

Equations

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

instance Semantics.Lexical.Plural.Cumulativity.instFintypeContinent : Fintype Continent

Equations

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

def Semantics.Lexical.Plural.Cumulativity.livesIn : Elephant → Continent → Bool

Equations

• Semantics.Lexical.Plural.Cumulativity.livesIn Semantics.Lexical.Plural.Cumulativity.Elephant.dumbo Semantics.Lexical.Plural.Cumulativity.Continent.africa = true
• Semantics.Lexical.Plural.Cumulativity.livesIn Semantics.Lexical.Plural.Cumulativity.Elephant.babar Semantics.Lexical.Plural.Cumulativity.Continent.africa = true
• Semantics.Lexical.Plural.Cumulativity.livesIn Semantics.Lexical.Plural.Cumulativity.Elephant.tantor Semantics.Lexical.Plural.Cumulativity.Continent.asia = true
• Semantics.Lexical.Plural.Cumulativity.livesIn x✝¹ x✝ = false

def Semantics.Lexical.Plural.Cumulativity.allElephants : Finset Elephant

Equations

• Semantics.Lexical.Plural.Cumulativity.allElephants = Finset.univ

def Semantics.Lexical.Plural.Cumulativity.africaAndAsia : Finset Continent

Equations

• Semantics.Lexical.Plural.Cumulativity.africaAndAsia = Finset.univ