Sternefeld (1998): Reciprocity and cumulative predication

This file formalizes [Ste98]'s derivation of the readings of plural and reciprocal sentences from the placement of Link's * and Krifka's ** at Logical Form, on [Sch96c]'s set-based ontology: pluralities are finite sets of individuals, an individual is its singleton, and sum is union. Weak distributivity is **R and weak reciprocity is ** of the relation with non-identity conjoined into it, so the reciprocal carries no quantifier of its own; strong distributivity and strong reciprocity are iterated *. We prove that for a relation between individuals each form is the corresponding formula of [Lan78], that Langendoen's weak reciprocity always entails the cumulation form, and that the converse fails in Langendoen's model where two individuals relate to a third only jointly.

Implementation notes

• A relation between individuals enters the set-based ontology as its image under singleton formation, Relation.Map R ({·}) ({·}); this is the paper's D-based case (§2.3), and Langendoen's formulae are the substrate schemes Reciprocal.WeakReciprocity and Reciprocal.StrongReciprocity of R itself.
• Denotations are nonempty, so the weak equivalences carry the nonemptiness hypothesis that * and ** build in and Langendoen's formulae leave vacuous. Strong reciprocity requires two or more members, as iterated * does.
• The n-ary *** (§3.1), dependent plurals (§3.2–3.3), LF movement (§3.4), the Geach–Kaplan sentence (§3.6) and the cover pragmatics of §4 are not formalized.

References

• [Ste98]
• [Lan78]
• [Kri86]
• [Lin83]
• [Sch96c]

Relations between individuals

@[simp]

theorem Sternefeld1998.map_singleton_singleton {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (a : α) (b : β) : Relation.Map R (fun (x : α) => {x}) (fun (x : β) => {x}) {a} {b} ↔ R a b

theorem Sternefeld1998.algClosure_map_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] (R : α → β → Prop) (a : α) (B : Finset β) : Mereology.AlgClosure (Relation.Map R (fun (x : α) => {x}) (fun (x : β) => {x}) {a}) B ↔ B.Nonempty ∧ ∀ b ∈ B, R a b

* of a relation between individuals, in its second argument, holds of the nonempty pluralities all of whose members are related to the first.

Weak distributivity and weak reciprocity

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

Weak distributivity (2b) is ⟨A, B⟩ ∈ **R (26a) between nonempty pluralities.

def Sternefeld1998.WR {α : Type u_1} [DecidableEq α] (R : Finset α → Finset α → Prop) (A : Finset α) : Prop

Weak reciprocity (6), (26b): the reciprocal NP denotes the others, and non-identity is conjoined into the relation before cumulation.

Equations

• Sternefeld1998.WR R A = Plurality.Cumulativity.Cumulation (fun (x y : Finset α) => R x y ∧ x ≠ y) A A

theorem Sternefeld1998.wr_of_weakReciprocity {α : Type u_1} [DecidableEq α] {R : Finset α → Finset α → Prop} {A : Finset α} (hA : A.Nonempty) (h : Reciprocal.WeakReciprocity (fun (a b : α) => R {a} {b}) A) : WR R A

Langendoen's weak reciprocity (25b) between individuals entails (26b), for any relation over pluralities.

theorem Sternefeld1998.wr_map_iff {α : Type u_1} [DecidableEq α] (R : α → α → Prop) {A : Finset α} (hA : A.Nonempty) : WR (Relation.Map R (fun (x : α) => {x}) fun (x : α) => {x}) A ↔ Reciprocal.WeakReciprocity R A

For a relation between individuals, (26b) is Langendoen's (25b).

Langendoen's model

A = {a, b, c} and R = {⟨{a, b}, c⟩, ⟨c, a⟩, ⟨c, b⟩} (§3): the As relate to each other, but no individual relates to c on its own, so (25b) fails while (26b) holds.

def Sternefeld1998.langendoenModel (x y : Finset (Fin 3)) : Prop

Langendoen's relation: a and b relate to c jointly, and c relates to each.

Equations

• Sternefeld1998.langendoenModel x y = (x = {0, 1} ∧ y = {2} ∨ x = {2} ∧ y = {0} ∨ x = {2} ∧ y = {1})

@[instance_reducible]

instance Sternefeld1998.instDecidableRelFinsetFinOfNatNatLangendoenModel : DecidableRel langendoenModel

Equations

• Sternefeld1998.instDecidableRelFinsetFinOfNatNatLangendoenModel x✝¹ x✝ = id inferInstance

theorem Sternefeld1998.langendoenModel_ne_map (R : Fin 3 → Fin 3 → Prop) : langendoenModel ≠ Relation.Map R (fun (x : Fin 3) => {x}) fun (x : Fin 3) => {x}

Langendoen's relation is not a relation between individuals.

theorem Sternefeld1998.wr_langendoenModel : WR langendoenModel Finset.univ

(26b) holds in Langendoen's model.

theorem Sternefeld1998.not_weakReciprocity_langendoenModel : ¬Reciprocal.WeakReciprocity (fun (a b : Fin 3) => langendoenModel {a} {b}) Finset.univ

(25b) fails in Langendoen's model.

Strong distributivity and strong reciprocity by iterated *

def Sternefeld1998.SD {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (R : α → β → Prop) (A : Finset α) (B : Finset β) : Prop

Strong distributivity by iterated * (7): A ∈ *{x : B ∈ *{y : R(x, y)}}.

Equations

• Sternefeld1998.SD R A B = Mereology.AlgClosure (fun (x : Finset α) => Mereology.AlgClosure (Relation.Map R (fun (x : α) => {x}) (fun (x : β) => {x}) x) B) A

def Sternefeld1998.SR {α : Type u_1} [DecidableEq α] (R : α → α → Prop) (A : Finset α) : Prop

Strong reciprocity by iterated * (48b): A ∈ *λx[{y : y ∈ A ∧ y ≠ x} ∈ *λy.R(x, y)], the reciprocal interpreted in situ as one NP.

Equations

• Sternefeld1998.SR R A = Mereology.AlgClosure (fun (x : Finset α) => Mereology.AlgClosure (Relation.Map R (fun (x : α) => {x}) (fun (x : α) => {x}) x) ({b ∈ A | {b} ≠ x})) A

theorem Sternefeld1998.sd_iff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (R : α → β → Prop) {A : Finset α} {B : Finset β} (hA : A.Nonempty) (hB : B.Nonempty) : SD R A B ↔ ∀ a ∈ A, ∀ b ∈ B, R a b

(7) is Langendoen's strong distributivity (2a) between nonempty pluralities.

theorem Sternefeld1998.sr_iff {α : Type u_1} [DecidableEq α] (R : α → α → Prop) {A : Finset α} : SR R A ↔ Reciprocal.StrongReciprocity R A

(48b) is strong reciprocity, Langendoen's (3a) on a plurality of two or more.