Cumulative Predication

[Kri89] [Ste98] [BS00]

Formalises the cumulative operator ** in the bidirectional-coverage form. The operator originates with [Kri89] §3 (the SUM property D.29 for binary relations); [Ste98] §3.1 generalises to an n-ary closure operation (***); the bidirectional-coverage reformulation (∀a∈x. ∃b∈y. R(a,b)) ∧ (∀b∈y. ∃a∈x. R(a,b)) used here is from [BS00]. The two formulations are equivalent on Quine-innovation domains; Studies/Sternefeld1998.lean::sternefeldStarStar_implies_cumulative proves the forward direction.

Main declarations

• Cumulative R x y — bidirectional-coverage cumulative predication.
• LeftCoverage, RightCoverage — the two conjuncts; their conjunction IS Cumulative (cumulative_iff_coverages).
• cumulative_left_universal, cumulative_right_universal — per-argument distributive consequences.
• singleton_right_cumulative — ** on a singleton right argument collapses to universal distribution.

Implementation notes

Link's CUM (Mereology.CUM) is a property of denotations: P(x) ∧ P(y) → P(x ⊔ y). 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.

Todo

• n-ary *** (Sternefeld 1998 §3.1) currently lives in Studies/Sternefeld1998.lean; promote when ≥ 2 consumers.
• Schein (1993) Plurals and Events (bib entry pending) — the event-quantification alternative to the **-relational treatment of cumulativity — is not yet formalised.

Bidirectional-coverage **

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 [BS00]'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) [DecidableRel R] (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 [Joh23]'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.