Reciprocal Predicates

Substrate for the reciprocal-meaning typology. The six interpretation schemes originate in [Lan78] (Strong Reciprocity SR, Intermediate Reciprocity IR, Weak Reciprocity WR), Kański 1987 (bib entry pending; Inclusive Alternative Ordering IAO), Fiengo & Lasnik 1973 (bib entry pending; Partitioned Strong Reciprocity PartSR), and [DKK+98] (the Alternative variants SAR/IAR plus One-way Weak Reciprocity OWR as a methodological waypoint between WR and IAO). DKMPK 1998 organises them along two axes — quantification strength (∀∀ / ∃-chain / ∃∃) and directionality (one-way vs alternative R x y ∨ R y x) — and proposes the Strongest Meaning Hypothesis (SMH): interpretation selects the strongest scheme consistent with context. The substrate here exposes the six schemes, the entailment lattice between the bivalent versions, and a bridge to Cumulativity.Cumulative for WR. SMH itself is left as a Todo.

Main declarations

• ReciprocalScheme — the six-cell typology, named.
• StrongReciprocity — every distinct pair satisfies R.
• PartitionedStrongReciprocity — there is a partition of X such that SR holds within each cell.
• IntermediateReciprocity — every distinct pair is connected by an R-chain.
• WeakReciprocity — every member is R-related to a distinct other in both directions.
• OneWayWeakReciprocity — only the first direction of WR.
• InclusiveAlternativeOrdering — every member participates in R either as subject or as object of a distinct other.
• strong_imp_weak, weak_imp_oneWay, oneWay_imp_inclusiveAlternative, strong_imp_inclusiveAlternative — the entailment lattice ([Bec01] eq 28 right-hand spine).
• weakReciprocity_iff_cumulative_strict — WR factors through Cumulative of the strict-distinct relation (Beck eq 120 / [Ste98] eq 26b, bivalent collapse).

Implementation notes

The standard DKMPK / Langendoen 1978 form of WR requires both ∃y ∈ X. y ≠ x ∧ R x y AND ∃y ∈ X. y ≠ x ∧ R y x for each x ∈ X — i.e., each member must be both an R-subject and an R-object of some distinct other. The single-conjunct version (here: OneWayWeakReciprocity) is empirically too weak; it's named after Sabato & Winter 2005's terminology.

IntermediateReciprocity uses List.IsChain on a list of atoms in X to express "connected by an R-chain"; PartitionedStrongReciprocity uses Finset (Finset α) for the partition witness.

Todo

• Strong/Weak/Intermediate Alternative schemes (R y x ∨ R x y variants): SAR, IAR.
• Strongest Meaning Hypothesis as an interpretation operator selecting among schemes given context.
• Add bib entries: Kański 1987, Fiengo & Lasnik 1973, Sabato & Winter 2005.

inductive Semantics.Plurality.Reciprocal.ReciprocalScheme : Type

The six reciprocal interpretation schemes. SR/IR/WR originate in [Lan78]; IAO in Kański 1987 (bib entry pending); Partitioned SR in Fiengo & Lasnik 1973 (bib entry pending); the Alternative variants (SAR, IAR) in [DKK+98].

• strong : ReciprocalScheme
• partitionedStrong : ReciprocalScheme
• intermediate : ReciprocalScheme
• weak : ReciprocalScheme
• oneWayWeak : ReciprocalScheme
• inclusiveAlternative : ReciprocalScheme

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instDecidableEqReciprocalScheme : DecidableEq ReciprocalScheme

Equations

• Semantics.Plurality.Reciprocal.instDecidableEqReciprocalScheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instReprReciprocalScheme : Repr ReciprocalScheme

Equations

• Semantics.Plurality.Reciprocal.instReprReciprocalScheme = { reprPrec := Semantics.Plurality.Reciprocal.instReprReciprocalScheme.repr }

def Semantics.Plurality.Reciprocal.instReprReciprocalScheme.repr : ReciprocalScheme → ℕ → Std.Format

Equations

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

Strong Reciprocity

def Semantics.Plurality.Reciprocal.StrongReciprocity {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Strong Reciprocity: every distinct pair in X satisfies R. "The students all know each other": every student knows every other student.

Equations

• Semantics.Plurality.Reciprocal.StrongReciprocity R X = ∀ x ∈ X, ∀ y ∈ X, y ≠ x → R x y

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instDecidableStrongReciprocityOfDecidableEqOfDecidableRel {A : Type u_1} [DecidableEq A] (R : A → A → Prop) [DecidableRel R] (X : Finset A) : Decidable (StrongReciprocity R X)

Equations

• Semantics.Plurality.Reciprocal.instDecidableStrongReciprocityOfDecidableEqOfDecidableRel R X = id inferInstance

Partitioned Strong Reciprocity

def Semantics.Plurality.Reciprocal.PartitionedStrongReciprocity {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Partitioned Strong Reciprocity (Fiengo & Lasnik 1973, bib entry pending): there is a partition of X such that SR holds within each cell. "The men are hitting each other" can be true if the men team up in pairs that stand in the hit-relation.

Equations

• Semantics.Plurality.Reciprocal.PartitionedStrongReciprocity R X = ∃ (PART : Finset (Finset A)), (∀ Y ∈ PART, Y ⊆ X) ∧ (∀ a ∈ X, ∃ Y ∈ PART, a ∈ Y) ∧ ∀ Y ∈ PART, ∀ x ∈ Y, ∀ y ∈ Y, y ≠ x → R x y

Intermediate Reciprocity

def Semantics.Plurality.Reciprocal.IntermediateReciprocity {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Intermediate Reciprocity (Langendoen 1978): any two distinct members of X are connected by an R-chain through X. "Five Boston pitchers sat alongside each other": each pitcher has an R-chain to every other pitcher.

Uses List.Chain' over a non-empty list of X-elements whose head is x and whose last element is y.

Equations

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

Weak Reciprocity

def Semantics.Plurality.Reciprocal.WeakReciprocity {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Weak Reciprocity (Langendoen 1978; DKMPK 1998): every member of X is R-related to at least one distinct other member in both directions — as R-subject and as R-object. "The boys are stacked on top of each other": each boy has some other boy on top of him AND is on top of some other boy.

Definitionally identical to Cumulative (R ∧ ≠) X X (see weakReciprocity_iff_cumulative_strict).

Equations

• Semantics.Plurality.Reciprocal.WeakReciprocity R X = ((∀ x ∈ X, ∃ y ∈ X, R x y ∧ x ≠ y) ∧ ∀ y ∈ X, ∃ x ∈ X, R x y ∧ x ≠ y)

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instDecidableWeakReciprocityOfDecidableEqOfDecidableRel {A : Type u_1} [DecidableEq A] (R : A → A → Prop) [DecidableRel R] (X : Finset A) : Decidable (WeakReciprocity R X)

Equations

• Semantics.Plurality.Reciprocal.instDecidableWeakReciprocityOfDecidableEqOfDecidableRel R X = id inferInstance

One-way Weak Reciprocity

def Semantics.Plurality.Reciprocal.OneWayWeakReciprocity {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

One-way Weak Reciprocity (Sabato & Winter 2005 terminology): only the first direction of WR is required. "The pirates are staring at each other" — pirate 6 is not stared at by anybody, but everyone stares at someone.

Equations

• Semantics.Plurality.Reciprocal.OneWayWeakReciprocity R X = ∀ x ∈ X, ∃ y ∈ X, R x y ∧ x ≠ y

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instDecidableOneWayWeakReciprocityOfDecidableEqOfDecidableRel {A : Type u_1} [DecidableEq A] (R : A → A → Prop) [DecidableRel R] (X : Finset A) : Decidable (OneWayWeakReciprocity R X)

Equations

• Semantics.Plurality.Reciprocal.instDecidableOneWayWeakReciprocityOfDecidableEqOfDecidableRel R X = id inferInstance

Inclusive Alternative Ordering

def Semantics.Plurality.Reciprocal.InclusiveAlternativeOrdering {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Inclusive Alternative Ordering (Kański 1987, bib entry pending): each member of X participates in R as either first or second argument of a distinct other. "The plates are stacked on top of each other" — each plate is on top of one or has one on top of itself.

Equations

• Semantics.Plurality.Reciprocal.InclusiveAlternativeOrdering R X = ∀ x ∈ X, ∃ y ∈ X, x ≠ y ∧ (R x y ∨ R y x)

@[instance_reducible]

instance Semantics.Plurality.Reciprocal.instDecidableInclusiveAlternativeOrderingOfDecidableEqOfDecidableRel {A : Type u_1} [DecidableEq A] (R : A → A → Prop) [DecidableRel R] (X : Finset A) : Decidable (InclusiveAlternativeOrdering R X)

Equations

• Semantics.Plurality.Reciprocal.instDecidableInclusiveAlternativeOrderingOfDecidableEqOfDecidableRel R X = id inferInstance

Entailment lattice (Beck 2001 eq 28, right-hand spine)

theorem Semantics.Plurality.Reciprocal.strong_imp_weak {A : Type u_1} [DecidableEq A] (R : A → A → Prop) (X : Finset A) (hcard : 2 ≤ X.card) (hSR : StrongReciprocity R X) : WeakReciprocity R X

Strong Reciprocity entails Weak Reciprocity, on pluralities of cardinality ≥ 2 (so a distinct witness exists).

theorem Semantics.Plurality.Reciprocal.weak_imp_oneWay {A : Type u_1} (R : A → A → Prop) (X : Finset A) (hWR : WeakReciprocity R X) : OneWayWeakReciprocity R X

Weak Reciprocity entails One-way Weak Reciprocity (projection on the first conjunct).

theorem Semantics.Plurality.Reciprocal.oneWay_imp_inclusiveAlternative {A : Type u_1} (R : A → A → Prop) (X : Finset A) (hOWR : OneWayWeakReciprocity R X) : InclusiveAlternativeOrdering R X

One-way Weak Reciprocity entails Inclusive Alternative Ordering.

theorem Semantics.Plurality.Reciprocal.strong_imp_inclusiveAlternative {A : Type u_1} [DecidableEq A] (R : A → A → Prop) (X : Finset A) (hcard : 2 ≤ X.card) (hSR : StrongReciprocity R X) : InclusiveAlternativeOrdering R X

Composition: SR entails IAO via the right-hand spine SR → WR → OWR → IAO.

Cumulativity bridge

theorem Semantics.Plurality.Reciprocal.weakReciprocity_iff_cumulative_strict {A : Type u_1} (R : A → A → Prop) (X : Finset A) : WeakReciprocity R X ↔ Cumulativity.Cumulative (fun (a b : A) => R a b ∧ a ≠ b) X X

Weak Reciprocity factors through Cumulative: Beck-Sauerland's ** applied to the strict-distinct verb relation λ a b. R a b ∧ a ≠ b on (X, X) recovers Weak Reciprocity definitionally. This is the substrate-level form of [Bec01] eq 120 / [Ste98] eq 26b (bivalent collapse). The Beck/Sternefeld trivalent disagreement is invisible here — both reduce to the same proposition under bivalent encoding.

theorem Semantics.Plurality.Reciprocal.weakReciprocity_imp_cumulative {A : Type u_1} (R : A → A → Prop) (X : Finset A) (hWR : WeakReciprocity R X) : Cumulativity.Cumulative R X X

Forward weakening: WR truth conditions entail bare Cumulative R X X (dropping the strict-distinct conjunct). This is strictly weaker than either Beck eq 120 or Sternefeld eq 26b, both of which keep the distinctness clause inside the relation argument.

Configurational typology

The event-configuration typology of [ELGM11] and [MEGL11]: six shapes of mutual relation (strong, pairwise, chain, radial, melee, ring) used in the video-stimulus elicitation studies. Each is rendered as an exact-extension condition on (R, X) — the relation coincides with the named configuration — so symmetry and participant-exhaustiveness are theorems rather than stipulations, and the shapes plug into the entailment lattice above: pairwise strengthens to PartitionedStrongReciprocity, ring yields OneWayWeakReciprocity, chain and radial yield InclusiveAlternativeOrdering, and melee is definitionally the failure of InclusiveAlternativeOrdering (some activity, but not everyone participates). The strong configuration is StrongReciprocity itself.

def Semantics.Plurality.Reciprocal.Consecutive {A : Type u_1} (l : List A) (x y : A) : Prop

y immediately follows x in l.

Equations

• Semantics.Plurality.Reciprocal.Consecutive l x y = ((x, y) ∈ l.zip l.tail)

def Semantics.Plurality.Reciprocal.PairSymmetricOn {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

R is symmetric within X: every realized pair is mutual.

Equations

• Semantics.Plurality.Reciprocal.PairSymmetricOn R X = ∀ x ∈ X, ∀ y ∈ X, R x y → R y x

def Semantics.Plurality.Reciprocal.PairwiseConfig {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Pairwise configuration ([MEGL11]): the participants split into two-member cells, and R holds exactly within cells ("The people at the dinner party were married to one another").

Equations

• Semantics.Plurality.Reciprocal.PairwiseConfig R X = ∃ (P : Finset (Finset A)), (∀ c ∈ P, c.card = 2 ∧ c ⊆ X) ∧ (∀ a ∈ X, ∃ c ∈ P, a ∈ c) ∧ ∀ (x y : A), R x y ↔ ∃ c ∈ P, x ∈ c ∧ y ∈ c ∧ x ≠ y

def Semantics.Plurality.Reciprocal.ChainConfig {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Chain configuration ([MEGL11]): the participants form a line and R holds exactly between adjacent members, directed ("The graduating students followed one another up onto the stage").

Equations

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

def Semantics.Plurality.Reciprocal.RingConfig {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Ring configuration ([MEGL11]): a chain whose last member acts on the first ("The children chased each other round in a ring").

Equations

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

def Semantics.Plurality.Reciprocal.RadialConfig {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Radial configuration ([MEGL11]): one central participant acts (asymmetrically) on each of the others ("The teacher and her pupils intimidated one another").

Equations

• Semantics.Plurality.Reciprocal.RadialConfig R X = ∃ c ∈ X, 2 ≤ X.card ∧ ∀ (x y : A), R x y ↔ x = c ∧ y ∈ X ∧ y ≠ c

def Semantics.Plurality.Reciprocal.MeleeConfig {A : Type u_1} (R : A → A → Prop) (X : Finset A) : Prop

Melee configuration ([MEGL11]): multiple asymmetrical interactions without full saturation ("The drunks in the pub were punching one another") — some activity, but participation fails to be exhaustive, i.e. even InclusiveAlternativeOrdering (the weakest scheme in the lattice above) fails.

Equations

• Semantics.Plurality.Reciprocal.MeleeConfig R X = ((∃ x ∈ X, ∃ y ∈ X, x ≠ y ∧ R x y) ∧ ¬Semantics.Plurality.Reciprocal.InclusiveAlternativeOrdering R X)

Symmetry theorems

theorem Semantics.Plurality.Reciprocal.StrongReciprocity.pairSymmetricOn {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : StrongReciprocity R X) : PairSymmetricOn R X

Strong reciprocity is symmetric on its plurality.

theorem Semantics.Plurality.Reciprocal.PairwiseConfig.pairSymmetricOn {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : PairwiseConfig R X) : PairSymmetricOn R X

The pairwise configuration is symmetric: partners are mutual.

theorem Semantics.Plurality.Reciprocal.ChainConfig.not_pairSymmetricOn {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : ChainConfig R X) : ¬PairSymmetricOn R X

The chain configuration is not symmetric: followers are not followed back ([MEGL11]'s directed line).

theorem Semantics.Plurality.Reciprocal.RingConfig.not_pairSymmetricOn {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : RingConfig R X) : ¬PairSymmetricOn R X

The ring configuration is not symmetric (for genuine rings of three or more): the cycle is directed.

theorem Semantics.Plurality.Reciprocal.RadialConfig.not_pairSymmetricOn {A : Type u_1} [DecidableEq A] {R : A → A → Prop} {X : Finset A} (h : RadialConfig R X) : ¬PairSymmetricOn R X

The radial configuration is not symmetric: the center acts on the periphery, never conversely ([MEGL11]).

Exhaustiveness theorems

Participant-exhaustiveness is InclusiveAlternativeOrdering — the weakest scheme in the lattice. Every configuration except melee entails it (the strong configuration via strong_imp_inclusiveAlternative); melee denies it by definition.

theorem Semantics.Plurality.Reciprocal.PairwiseConfig.inclusiveAlternativeOrdering {A : Type u_1} [DecidableEq A] {R : A → A → Prop} {X : Finset A} (h : PairwiseConfig R X) : InclusiveAlternativeOrdering R X

Everyone at a pairwise event has a partner.

theorem Semantics.Plurality.Reciprocal.ChainConfig.inclusiveAlternativeOrdering {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : ChainConfig R X) : InclusiveAlternativeOrdering R X

Everyone in a chain follows or is followed.

theorem Semantics.Plurality.Reciprocal.RingConfig.oneWayWeak {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : RingConfig R X) : OneWayWeakReciprocity R X

Everyone in a ring chases someone: the ring configuration yields OneWayWeakReciprocity (which a chain does not — its last member acts on nobody).

theorem Semantics.Plurality.Reciprocal.RingConfig.inclusiveAlternativeOrdering {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : RingConfig R X) : InclusiveAlternativeOrdering R X

The ring configuration participates everyone.

theorem Semantics.Plurality.Reciprocal.RadialConfig.inclusiveAlternativeOrdering {A : Type u_1} [DecidableEq A] {R : A → A → Prop} {X : Finset A} (h : RadialConfig R X) : InclusiveAlternativeOrdering R X

Radial events participate everyone: the center acts on each peripheral member.

Lattice connections

theorem Semantics.Plurality.Reciprocal.PairwiseConfig.partitionedStrong {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : PairwiseConfig R X) : PartitionedStrongReciprocity R X

The pairwise configuration realizes Partitioned Strong Reciprocity: the pairing is the partition witness.