Cumulative predication

This file relates the two forms of the cumulative operator ** on relations between individuals. In the coverage form of [BS00], **R holds of two pluralities when every member of the first is R-related to some member of the second and conversely: this is the relation lifting Set.LiftRel R of Linglib/Core/Data/Set/Functor.lean, and over a singleton it is distribution (Set.liftRel_singleton_right), the number effect of [Joh23]. In the closure form of [Kri86] and [Ste98], **R is the smallest relation containing R and closed under componentwise sum, which is Link's * on the product semilattice. The two agree on nonempty finite sets of individuals.

Definitions

• Plurality.Cumulativity.Cumulation R x y: the closure form, on any pair of join-semilattices.

Main results

• Plurality.Cumulativity.cumulation_iff_of_cum: a cumulative relation is its own cumulation.
• Plurality.Cumulativity.cumulation_map_singleton: on finite sets, the closure form of a relation between individuals is the coverage form, Set.LiftRel, of a nonempty pair.

References

• M. Krifka, Nominalreferenz und Zeitkonstitution (1986)
• W. Sternefeld, Reciprocity and cumulative predication (1998)
• S. Beck and U. Sauerland, Cumulation is needed: A reply to Winter (2000) (2000)
• G. Link, The logical analysis of plurals and mass terms (1983)
• W. Johnston, Pair-list answers to questions with plural definites (2023)

Closure form

Krifka's **R is Link's * applied to R as a predicate on the product semilattice: the smallest relation containing R and closed under componentwise sum.

def Plurality.Cumulativity.Cumulation {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (R : α → β → Prop) (x : α) (y : β) : Prop

The cumulation **R of a relation ([Kri86]; [Ste98]): the closure of R under componentwise sum, Mereology.AlgClosure on the product semilattice.

Equations

• Plurality.Cumulativity.Cumulation R x y = Mereology.AlgClosure (Function.uncurry R) (x, y)

theorem Plurality.Cumulativity.Cumulation.of_rel {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {R : α → β → Prop} {x : α} {y : β} (h : R x y) : Cumulation R x y

theorem Plurality.Cumulativity.Cumulation.sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {R : α → β → Prop} {x x' : α} {y y' : β} (h : Cumulation R x y) (h' : Cumulation R x' y') : Cumulation R (x ⊔ x') (y ⊔ y')

theorem Plurality.Cumulativity.Cumulation.mono {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {R S : α → β → Prop} {x : α} {y : β} (hRS : ∀ (x : α) (y : β), R x y → S x y) (h : Cumulation R x y) : Cumulation S x y

theorem Plurality.Cumulativity.cumulation_iff_of_cum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {R : α → β → Prop} {x : α} {y : β} (hR : Mereology.CUM (Function.uncurry R)) : Cumulation R x y ↔ R x y

A cumulative relation is its own cumulation.

Sets of individuals

theorem Plurality.Cumulativity.cumulation_map_singleton {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (R : A → B → Prop) (x : Finset A) (y : Finset B) : Cumulation (Relation.Map R (fun (x : A) => {x}) fun (x : B) => {x}) x y ↔ x.Nonempty ∧ Set.LiftRel R ↑x ↑y

On finite sets, ** of a relation between individuals, taken as singletons, is bidirectional coverage of a nonempty pair: the closure form of [Kri86] and the coverage form of [BS00] agree away from the empty pair.