Plurality Licensing for Anaphors

@cite{rakosi-2019}

The split between morphosyntactic and semantic plurality licensing of anaphors. @cite{rakosi-2019} demonstrates that Hungarian reciprocals (egymás) tolerate morphosyntactically singular antecedents (quantified NPs, singular coordinate DPs, collective nouns) while reflexives (maga/maguk) require morphosyntactic plurality (plural noun head + plural verb agreement + plural anaphor form).

The distinction is derivable from the formal semantics:

• Reflexive binding (=) operates via φ-feature agreement. The anaphor must match the morphosyntactic features of its antecedent and the verb. Agreement is a syntactic mechanism → morphosyntactic plurality required.
• Reciprocity (R) requires per-state distinctness, presupposing multiple individuals in the denotation. This is a semantic requirement: the antecedent must denote a plurality, but need not bear plural morphology.

Anchoring

Substrate originating with @cite{rakosi-2019}; consumed by Studies/Rakosi2019.lean (the paper formalisation) and Fragments/Hungarian/Reciprocals.lean (the per-language data file). Two consumers cross the linglib substrate-promotion threshold; sits in Reference/ rather than directly in either consumer to preserve the Fragments → Substrate dependency arrow (Fragments may not import Studies).

This file does not depend on H&D 2020 or DH 2024 — only on the PPCDRT substrate that defines bindingCond, reciprocityCond, groupIdentityCond.

inductive Semantics.Reference.PluralityLicensing.PluralityRequirement : Type

What kind of plurality an anaphor requires from its antecedent.

@cite{rakosi-2019}: Hungarian reciprocals tolerate morphosyntactically singular antecedents while reflexives do not. The distinction is derivable from the formal semantics:

• Reflexive binding (=) operates via φ-feature agreement → requires morphosyntactic plurality.
• Reciprocity (R) requires per-state distinctness in the denotation → semantic plurality suffices.

• morphosyntactic : PluralityRequirement

  Requires plural morphology on the antecedent + plural verb agreement

  • plural anaphor form. Characteristic of reflexive anaphors.
• semantic : PluralityRequirement

  Requires only that the antecedent denote multiple individuals. Syntactic number features are irrelevant. Characteristic of reciprocal anaphors.

@[implicit_reducible]

instance Semantics.Reference.PluralityLicensing.instDecidableEqPluralityRequirement : DecidableEq PluralityRequirement

Equations

• Semantics.Reference.PluralityLicensing.instDecidableEqPluralityRequirement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Reference.PluralityLicensing.instReprPluralityRequirement.repr : PluralityRequirement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Reference.PluralityLicensing.instReprPluralityRequirement : Repr PluralityRequirement

Equations

• Semantics.Reference.PluralityLicensing.instReprPluralityRequirement = { reprPrec := Semantics.Reference.PluralityLicensing.instReprPluralityRequirement.repr }

def Semantics.Reference.PluralityLicensing.anaphorPluralityReq (isReciprocal : Bool) : PluralityRequirement

The plurality requirement for each anaphor type, derived from the underlying anaphoric relation:

• Reflexives use binding (=) → φ-agreement → morphosyntactic.
• Reciprocals use reciprocity (R) → semantic distinctness → semantic.

Equations

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

def Semantics.Reference.PluralityLicensing.satisfiesPluralityReq (req : PluralityRequirement) (syntacticPl semanticPl : Bool) : Bool

Whether an antecedent satisfies the plurality requirement.

Equations

• Semantics.Reference.PluralityLicensing.satisfiesPluralityReq Semantics.Reference.PluralityLicensing.PluralityRequirement.morphosyntactic syntacticPl semanticPl = syntacticPl
• Semantics.Reference.PluralityLicensing.satisfiesPluralityReq Semantics.Reference.PluralityLicensing.PluralityRequirement.semantic syntacticPl semanticPl = semanticPl

theorem Semantics.Reference.PluralityLicensing.recip_licensed_by_semantic_plurality (semanticPl : Bool) (h : semanticPl = true) : satisfiesPluralityReq (anaphorPluralityReq true) false semanticPl = true

Reciprocals are licensed by semantic plurality alone.

theorem Semantics.Reference.PluralityLicensing.refl_needs_morphosyntactic_plurality : satisfiesPluralityReq (anaphorPluralityReq false) false true = false

Reflexives require morphosyntactic plurality: semantic plurality alone is insufficient.

theorem Semantics.Reference.PluralityLicensing.morphosyntactic_pl_licenses_both : satisfiesPluralityReq (anaphorPluralityReq false) true true = true ∧ satisfiesPluralityReq (anaphorPluralityReq true) true true = true

When an antecedent IS morphosyntactically plural, both anaphor types are licensed (morphosyntactic plurality implies semantic).

theorem Semantics.Reference.PluralityLicensing.reciprocity_implies_multiple_individuals {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (hdef : ∃ (s : Core.PartialAssign E), s ∈ S ∧ (s uAnaph).isSome = true ∧ (s uAnt).isSome = true) (h : Theories.Semantics.Dynamic.PPCDRT.reciprocityCond uAnaph uAnt S Δ) : ∃ (a : E), ∃ (b : E), a ≠ b

Reciprocity in PPCDRT — restricted to states where both drefs are defined — forces at least two distinct individuals in the value range. The distinctness clause of reciprocityCond says that whenever s uAnaph = some d_a and s uAnt = some d_b, d_a ≠ d_b; so any jointly-defined witness produces a pair of distinct values.

Partiality means we can't derive the existence of some jointly-defined state from S.IsNonempty alone — the anaphor and antecedent could each be defined on disjoint subsets of S (or nowhere), leaving the distinctness clause vacuously true. The strengthened hypothesis hdef : ∃ s ∈ S, (s uAnaph).isSome ∧ (s uAnt).isSome is the natural one for the linguistic case (a discourse referent introduced by a reciprocal forces its antecedent to be jointly defined at some state — paper eq 41 makes this explicit through the ∂(∪u = ∪𝒜(u)) presupposition combined with the existential extension [u]).

This is the formal-semantic justification for .semantic plurality licensing of reciprocals: when the meaning is non-vacuously satisfied, the denotation is forced to contain plurality, regardless of whether the antecedent bears plural morphology.

theorem Semantics.Reference.PluralityLicensing.binding_compatible_with_singleton {E : Type u} (e : E) (uAnaph uAnt : ℕ) : Theories.Semantics.Dynamic.PPCDRT.bindingCond uAnaph uAnt (Core.PluralAssign.singleton ((Core.PartialAssign.empty.update uAnaph e).update uAnt e)) ∅

Binding (bindingCond) is compatible with a singleton state where both drefs are mapped to the same value — there is no distinctness requirement, so the antecedent can be a single individual. This is why reflexive binding does NOT impose a semantic plurality requirement.