PPCDRT — Cumulativity Bridge

[Lan78] [HD20]

[Lan78] first observed that reciprocity is a species of cumulativity: in the women pointed at each other, every woman points at some other woman and every woman is pointed at by some other woman. [HD20] §1 reaffirms this. The link is structural: the PPCDRT condition groupIdentityCond u_anaph u_ant — equality of the value-sets ∪u_anaph(S) and ∪u_ant(S) across the plural state — collapses to Cumulative (· = ·) on the Finsets of values.

The Plurality/Cumulativity.lean substrate is Prop-valued over Finset × Finset, while PPCDRT is Prop-valued over PluralAssign. The bridge theorem, under finiteness assumptions on the value-sets, establishes the structural identity that the original Reference/Reciprocals.lean docstring asserted as prose.

The cumulative operator on equality

theorem PPCDRT.cumulative_eq_iff_finset_eq {E : Type u_1} (x y : Finset E) : Semantics.Plurality.Cumulativity.Cumulative (fun (a b : E) => a = b) x y ↔ x = y

The cumulative operator ** of [Kri89]/Beck-Sauerland on the equality relation reduces to Finset equality.

This is the structural identity behind the Langendoen reciprocity-as- cumulativity claim: bidirectional value-coverage IS the equality of value sets.

⊆ direction: if Cumulative (· = ·) x y, then for every a ∈ x there is b ∈ y with a = b, so a ∈ y; and symmetrically. ⊇ direction: if x = y, every element witnesses itself.

Bridge: groupIdentityCond ↔ Cumulative

theorem PPCDRT.groupIdentityCond_iff_cumulative_eq {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) (xa xb : Finset E) (hxa : ∀ (d : E), d ∈ xa ↔ d ∈ S.sumDref uAnaph) (hxb : ∀ (d : E), d ∈ xb ↔ d ∈ S.sumDref uAnt) : groupIdentityCond uAnaph uAnt S ∅ ↔ Semantics.Plurality.Cumulativity.Cumulative (fun (a b : E) => a = b) xa xb

Bridge: when the value-sets of the two drefs across the plural state are given as Finsets matching sumDref, group identity holds iff those Finsets are equal — iff Cumulative (· = ·) holds.

The hypothesis is stated as Set membership on sumDref because Set E → Finset E requires Set.Finite, which is downstream of the consumer's choice of value domain. Concrete H&D examples instantiate this with [Fintype] toy domains where the value-sets are automatically finite.

This theorem is the formal realisation of [Lan78]'s reciprocity-as-cumulativity claim within PPCDRT.