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

@[implicit_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 ⋯

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

Equations

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

@[implicit_reducible]

instance Semantics.Plurality.Reciprocal.instReprReciprocalScheme : Repr ReciprocalScheme

Equations

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

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

@[implicit_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)

@[implicit_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

@[implicit_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)

@[implicit_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.