Reciprocal Semantics: Anaphoric Relations and Scope

@cite{dalrymple-haug-2024} @cite{dalrymple-et-al-1998}

Two competing analyses of reciprocal expressions like each other:

1. Quantificational (@cite{heim-lasnik-may-1991}): the reciprocal is (or contains) a quantifier that can raise to the matrix clause, yielding a wide-scope (I-)reading. The local antecedent is bound by the raised quantifier part.

2. Relational (@cite{dalrymple-haug-2024}, @cite{sternenfeld-1998}, @cite{beck-2001}, @cite{dotlacil-2013}, @cite{haug-dalrymple-2020}): the reciprocal is a pronoun bearing an anaphoric relation to its antecedent. The narrow/wide scope ambiguity reduces to the choice of anaphoric relation: group identity (∪) for narrow scope vs. binding (=) for wide scope.

Three Anaphoric Relations

Following @cite{higginbotham-1985} and @cite{williams-1991}, anaphoric dependencies between a pronoun and its antecedent come in three types:

• Binding (=): the pronoun is a bound variable; the antecedent denotes an individual. Requires c-command.
• Group identity (∪): the pronoun denotes the same plurality as its antecedent. No c-command required.
• Reciprocity (R): cumulative identity across situations (the group picked out is the same) but distinctness within each situation (each pair involves different individuals). This is the core contribution of the reciprocal.

Key Prediction

The two analyses diverge on whether properties of the local antecedent (the embedded-clause pronoun coreferent with the matrix subject) can constrain reciprocal scope. The relational analysis predicts they can, because the local antecedent participates directly in the anaphoric relation. The quantificational analysis predicts they cannot for cases involving distributive operators (§5) and logophoric antecedents (§6), because the quantifier part of the reciprocal scopes independently of the local antecedent.

inductive Semantics.Reference.Reciprocals.AnaphoricRelation : Type

The three types of anaphoric relation between a pronoun and its antecedent. These are properties of the resolution, not the expression: the same pronoun (e.g., they) can participate in binding or group identity depending on context.

• binding : AnaphoricRelation

  Bound variable: pronoun gets its value from a c-commanding binder. The antecedent denotes an individual.

• groupIdentity : AnaphoricRelation

  Group identity: pronoun denotes the same plurality as its antecedent. Cumulative identity across all contexts.

• reciprocity : AnaphoricRelation

  Reciprocity: cumulative identity across situations (same group) but per-situation distinctness (different individuals in each pair). This is the semantic core of reciprocal each other.

instance Semantics.Reference.Reciprocals.instDecidableEqAnaphoricRelation : DecidableEq AnaphoricRelation

Equations

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

def Semantics.Reference.Reciprocals.instBEqAnaphoricRelation.beq : AnaphoricRelation → AnaphoricRelation → Bool

Equations

• Semantics.Reference.Reciprocals.instBEqAnaphoricRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Reference.Reciprocals.instBEqAnaphoricRelation : BEq AnaphoricRelation

Equations

• Semantics.Reference.Reciprocals.instBEqAnaphoricRelation = { beq := Semantics.Reference.Reciprocals.instBEqAnaphoricRelation.beq }

def Semantics.Reference.Reciprocals.instReprAnaphoricRelation.repr : AnaphoricRelation → ℕ → Std.Format

Equations

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

instance Semantics.Reference.Reciprocals.instReprAnaphoricRelation : Repr AnaphoricRelation

Equations

• Semantics.Reference.Reciprocals.instReprAnaphoricRelation = { reprPrec := Semantics.Reference.Reciprocals.instReprAnaphoricRelation.repr }

inductive Semantics.Reference.Reciprocals.RecipScope : Type

Scope reading of a reciprocal in a complex sentence.

• narrow (we-reading): "Tracy and Chris each thought 'We saw each other.'" The reciprocal is interpreted inside the embedded clause.
• wide (I-reading): "Tracy thought 'I saw Chris' and Chris thought 'I saw Tracy.'" The reciprocal's semantic contribution is in the matrix clause.

• narrow : RecipScope
• wide : RecipScope

instance Semantics.Reference.Reciprocals.instDecidableEqRecipScope : DecidableEq RecipScope

Equations

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

def Semantics.Reference.Reciprocals.instBEqRecipScope.beq : RecipScope → RecipScope → Bool

Equations

• Semantics.Reference.Reciprocals.instBEqRecipScope.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Reference.Reciprocals.instBEqRecipScope : BEq RecipScope

Equations

• Semantics.Reference.Reciprocals.instBEqRecipScope = { beq := Semantics.Reference.Reciprocals.instBEqRecipScope.beq }

def Semantics.Reference.Reciprocals.instReprRecipScope.repr : RecipScope → ℕ → Std.Format

Equations

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

instance Semantics.Reference.Reciprocals.instReprRecipScope : Repr RecipScope

Equations

• Semantics.Reference.Reciprocals.instReprRecipScope = { reprPrec := Semantics.Reference.Reciprocals.instReprRecipScope.repr }

inductive Semantics.Reference.Reciprocals.RecipAnalysis : Type

The two families of reciprocal analysis.

• quantificational : RecipAnalysis

  Reciprocal is/contains a quantifier that can QR to the matrix clause. @cite{heim-lasnik-may-1991}, @cite{sigurdsson-et-al-2022}, @cite{atlamaz-ozturk-2023}, @cite{paparounas-salzmann-2023}.

• relational : RecipAnalysis

  Reciprocal is a pronoun bearing an anaphoric relation on its antecedent. Scope ambiguity reduces to binding (=) vs. group identity (∪). @cite{sternenfeld-1998}, @cite{beck-2001}, @cite{dotlacil-2013}, @cite{haug-dalrymple-2020}.

instance Semantics.Reference.Reciprocals.instDecidableEqRecipAnalysis : DecidableEq RecipAnalysis

Equations

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

instance Semantics.Reference.Reciprocals.instBEqRecipAnalysis : BEq RecipAnalysis

Equations

• Semantics.Reference.Reciprocals.instBEqRecipAnalysis = { beq := Semantics.Reference.Reciprocals.instBEqRecipAnalysis.beq }

def Semantics.Reference.Reciprocals.instBEqRecipAnalysis.beq : RecipAnalysis → RecipAnalysis → Bool

Equations

• Semantics.Reference.Reciprocals.instBEqRecipAnalysis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Reference.Reciprocals.instReprRecipAnalysis : Repr RecipAnalysis

Equations

• Semantics.Reference.Reciprocals.instReprRecipAnalysis = { reprPrec := Semantics.Reference.Reciprocals.instReprRecipAnalysis.repr }

def Semantics.Reference.Reciprocals.instReprRecipAnalysis.repr : RecipAnalysis → ℕ → Std.Format

Equations

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

structure Semantics.Reference.Reciprocals.AntecedentProperties : Type

Properties of the local antecedent of the reciprocal (the embedded-clause pronoun coreferent with the matrix subject) that affect scopal possibilities.

• isBound : Bool

  Whether the local antecedent is syntactically bound (=) by the matrix subject. If true, the antecedent denotes an individual, forcing wide scope. If false (group identity ∪), narrow scope.

• hasCollectiveConjunct : Bool

  Whether the embedded predicate is conjoined with a necessarily collective predicate. Collective predicates require a plurality argument, which wide scope (individual denotation) cannot provide.

• isExhaustiveControl : Bool

  Whether the construction involves exhaustive control (PRO has same reference as controller) vs. partial control (PRO can denote a superset).

• controllerIsCollective : Bool

  Whether the controller is interpreted collectively.

• forcesGroupIdentity : Bool

  Whether the pronoun type forces group identity (∪) with the matrix subject, excluding the binding (=) option. Japanese zibun-tati (plural reflexive) resists bound readings, forcing group identity and thus narrow scope only (@cite{dalrymple-haug-2024} §2, @cite{nishigauchi-1992}).

• isLogophoric : Bool

  Whether the antecedent is a logophoric pronoun. Logophoric pronouns are interpreted inside the report context, and the reciprocal cannot "drag" them out to the matrix clause.

• hasDistributiveOperator : Bool

  Whether a distributive operator (each, each of them) is present in the matrix clause. On the quantificational analysis, this should block wide scope (can't distribute over an already-distributed NP). On the relational analysis, distributors are orthogonal to reciprocal scope: each other is a pronoun, not a quantifier, so there is no double-distribution problem. @cite{dalrymple-haug-2024} §5.

instance Semantics.Reference.Reciprocals.instReprAntecedentProperties : Repr AntecedentProperties

Equations

• Semantics.Reference.Reciprocals.instReprAntecedentProperties = { reprPrec := Semantics.Reference.Reciprocals.instReprAntecedentProperties.repr }

def Semantics.Reference.Reciprocals.instReprAntecedentProperties.repr : AntecedentProperties → ℕ → Std.Format

Equations

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

def Semantics.Reference.Reciprocals.relationalPrediction (props : AntecedentProperties) : List RecipScope

Scope readings predicted by the relational analysis.

The relational analysis predicts scope from the anaphoric relation between the local antecedent and the matrix subject:

• Group identity (∪) → narrow scope
• Binding (=) → wide scope

Key constraints:

1. Logophoric antecedent → only narrow scope (logophor confined to report context)
2. Collective conjunct → only narrow scope (wide gives individual, can't satisfy collectivity)
3. Forces group identity → only narrow scope (pronoun type excludes binding; e.g., Japanese zibun-tati)
4. Exhaustive control + non-collective → wide only
5. Exhaustive control + collective → narrow only
6. Bound antecedent → only wide scope (binding forces individual)
7. Distributive operator → BOTH readings (no constraint; each other is a pronoun, not a quantified NP, so distribution is orthogonal)

Equations

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

def Semantics.Reference.Reciprocals.quantificationalPrediction (props : AntecedentProperties) : List RecipScope

Scope readings predicted by the quantificational analysis.

The quantificational analysis derives scope from QR of the quantifier part of the reciprocal. It makes the same predictions as the relational analysis for §§2–4, but diverges on:

• Distributive operators (§5): predicts only narrow scope when a distributor is present, because a distributive operator cannot apply to an already-distributed NP (each in the quantificational analysis of each other). @cite{heim-lasnik-may-1991} claim (18b) "*They each examined each other" is ungrammatical — but corpus evidence refutes this. The relational analysis correctly allows both readings.

• Logophoric antecedents (§6): predicts both readings should be available (the quantifier scopes independently of logophoricity). The relational analysis correctly restricts to narrow only.

Equations

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

def Semantics.Reference.Reciprocals.narrowScopeRelations : AnaphoricRelation × AnaphoricRelation

On the relational analysis, narrow scope reciprocity decomposes into group identity (∪) between the local antecedent and the matrix subject, plus in-situ reciprocity (R) between the local antecedent and the reciprocal pronoun.

Equations

• Semantics.Reference.Reciprocals.narrowScopeRelations = (Semantics.Reference.Reciprocals.AnaphoricRelation.groupIdentity, Semantics.Reference.Reciprocals.AnaphoricRelation.reciprocity)

def Semantics.Reference.Reciprocals.wideScopeRelations : AnaphoricRelation × AnaphoricRelation

Wide scope reciprocity decomposes into binding (=) of the local antecedent by the matrix subject, plus reciprocity (R) in the matrix clause between the matrix subject and the reciprocal.

Equations

• Semantics.Reference.Reciprocals.wideScopeRelations = (Semantics.Reference.Reciprocals.AnaphoricRelation.binding, Semantics.Reference.Reciprocals.AnaphoricRelation.reciprocity)

theorem Semantics.Reference.Reciprocals.both_readings_binary : narrowScopeRelations.1 ≠ narrowScopeRelations.2 ∧ wideScopeRelations.1 ≠ wideScopeRelations.2

Both scope readings require exactly two anaphoric relations: one between matrix subject and local antecedent, one involving the reciprocal.

theorem Semantics.Reference.Reciprocals.readings_differ_on_antecedent_relation : narrowScopeRelations.1 ≠ wideScopeRelations.1

The two readings differ in whether the local antecedent is bound or group-identical with the matrix subject.

theorem Semantics.Reference.Reciprocals.both_use_reciprocity : narrowScopeRelations.2 = AnaphoricRelation.reciprocity ∧ wideScopeRelations.2 = AnaphoricRelation.reciprocity

Both readings share the reciprocity relation.

def Semantics.Reference.Reciprocals.bindingSem {S : Type u_1} {E : Type u_2} (u_ant u_pro : S → E) : Prop

Binding (=): the pronoun's value is identical to the antecedent's in every situation. @cite{haug-dalrymple-2020} §2.2.

Equations

• Semantics.Reference.Reciprocals.bindingSem u_ant u_pro = ∀ (s : S), u_pro s = u_ant s

def Semantics.Reference.Reciprocals.groupIdentitySem {S : Type u_1} {E : Type u_2} (u_ant u_pro : S → E) : Prop

Group identity (∪): the set of values taken by the pronoun across all situations equals the set taken by the antecedent. @cite{haug-dalrymple-2020} §2.3: ∪u₂ → ∪u₁.

Structurally parallel to cumulativeOp in Theories.Semantics.Lexical.Plural.Cumulativity: both express bidirectional existential coverage over a domain.

Equations

• Semantics.Reference.Reciprocals.groupIdentitySem u_ant u_pro = ((∀ (s : S), ∃ (s' : S), u_pro s = u_ant s') ∧ ∀ (s : S), ∃ (s' : S), u_ant s = u_pro s')

def Semantics.Reference.Reciprocals.reciprocitySem {S : Type u_1} {E : Type u_2} (u_ant u_pro : S → E) : Prop

Reciprocity (R): cumulative identity plus per-situation distinctness. @cite{haug-dalrymple-2020} §2.4.

Equations

• Semantics.Reference.Reciprocals.reciprocitySem u_ant u_pro = (Semantics.Reference.Reciprocals.groupIdentitySem u_ant u_pro ∧ ∀ (s : S), u_ant s ≠ u_pro s)

def Semantics.Reference.Reciprocals.underspecifiedSem {S : Type u_1} {E : Type u_2} (u_ant u_pro : S → E) : Prop

The underspecified reflexive/reciprocal meaning (German sich, Czech se, Cheyenne REFL/RECIP affix). Group identity without distinctness. Permits reflexive, reciprocal, and mixed readings (@cite{haug-dalrymple-2020} §4.2, @cite{murray-2008}).

Equations

• Semantics.Reference.Reciprocals.underspecifiedSem u_ant u_pro = Semantics.Reference.Reciprocals.groupIdentitySem u_ant u_pro

theorem Semantics.Reference.Reciprocals.binding_implies_groupIdentity {S : Type u_1} {E : Type u_2} {u_ant u_pro : S → E} (h : bindingSem u_ant u_pro) : groupIdentitySem u_ant u_pro

Binding implies group identity: pointwise equality entails range equality.

theorem Semantics.Reference.Reciprocals.reciprocity_excludes_binding {S : Type u_1} {E : Type u_2} {u_ant u_pro : S → E} (s : S) (h : reciprocitySem u_ant u_pro) : ¬bindingSem u_ant u_pro

Reciprocity excludes binding: per-situation distinctness contradicts pointwise identity.

theorem Semantics.Reference.Reciprocals.reciprocity_strengthens_underspecified {S : Type u_1} {E : Type u_2} {u_ant u_pro : S → E} : reciprocitySem u_ant u_pro → underspecifiedSem u_ant u_pro

The full reciprocal meaning strengthens the underspecified form by adding distinctness.

def Semantics.Reference.Reciprocals.AnaphoricRelation.denotes (r : AnaphoricRelation) {S : Type u_1} {E : Type u_2} (u_ant u_pro : S → E) : Prop

Maps each AnaphoricRelation constructor to its formal semantics over discourse referent functions S → E.

This connects the enum-level scope decomposition (narrowScopeRelations, wideScopeRelations) to the Prop-valued definitions (bindingSem, groupIdentitySem, reciprocitySem).

Equations

• Semantics.Reference.Reciprocals.AnaphoricRelation.binding.denotes u_ant u_pro = Semantics.Reference.Reciprocals.bindingSem u_ant u_pro
• Semantics.Reference.Reciprocals.AnaphoricRelation.groupIdentity.denotes u_ant u_pro = Semantics.Reference.Reciprocals.groupIdentitySem u_ant u_pro
• Semantics.Reference.Reciprocals.AnaphoricRelation.reciprocity.denotes u_ant u_pro = Semantics.Reference.Reciprocals.reciprocitySem u_ant u_pro