Reciprocal Semantics: Anaphoric Relations and Scope

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

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{sternefeld-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.

The formal semantics of these relations is defined over plural information states in Theories/Semantics/Dynamic/PPCDRT/Anaphora.lean. This file holds the enum-level classification — the abstract relation labels, the scope readings, the antecedent property bundle, and the prediction functions used by the Dalrymple–Haug 2024 cross-construction survey.

Two-parameter scope classification

@cite{haug-dalrymple-2020} §3.3 (p. 24) makes the reciprocal-scope classification two-dimensional: the locus of the reciprocal in the matrix DRS (high or low) crossed with the type of anaphoric relation between the matrix subject and the embedded local antecedent (binding or group identity). Three of the four cells are attested; the (low, bound) cell is empty (paper p. 24: "the bound reading of the reciprocal's antecedent cannot cooccur with a low locus for the reciprocal, because it does not make available the plurality that the reciprocal needs").

The RecipReading structure exposes locus alongside the two anaphoric relations so that consumers can witness the three cells distinctly.

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; the quantificational analysis predicts they cannot for cases involving distributive operators (§5) and logophoric antecedents (§6) — see @cite{dalrymple-haug-2024} for the empirical contrast.

inductive Semantics.Reference.Reciprocals.AnaphoricRelation : Type

The three types of anaphoric relation between a pronoun and its antecedent. 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).

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instDecidableEqAnaphoricRelation : DecidableEq AnaphoricRelation

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprAnaphoricRelation : Repr AnaphoricRelation

Equations

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

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

Equations

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

inductive Semantics.Reference.Reciprocals.RecipLocus : Type

Locus of the reciprocal in the matrix DRS. @cite{haug-dalrymple-2020} §3.3 (p. 24): the reciprocal is either interpreted in-situ inside the embedded clause (low locus) or lifted to the matrix DRS (high locus). The locus is one of the two parameters in the §3.3 classification of reciprocal readings.

• high : RecipLocus

  High locus: reciprocal lifted to matrix DRS. Required for wide scope and for the crossed reading.

• low : RecipLocus

  Low locus: reciprocal interpreted in-situ inside the embedded clause. Required for narrow scope.

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instDecidableEqRecipLocus : DecidableEq RecipLocus

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprRecipLocus : Repr RecipLocus

Equations

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

def Semantics.Reference.Reciprocals.instReprRecipLocus.repr : RecipLocus → ℕ → Std.Format

Equations

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

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instDecidableEqRecipScope : DecidableEq RecipScope

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprRecipScope : Repr RecipScope

Equations

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

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

Equations

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

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}.

• relational : RecipAnalysis

  Reciprocal is a pronoun bearing an anaphoric relation on its antecedent. @cite{sternefeld-1998}, @cite{beck-2001}, @cite{dotlacil-2013}, @cite{haug-dalrymple-2020}.

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instDecidableEqRecipAnalysis : DecidableEq RecipAnalysis

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprRecipAnalysis : Repr RecipAnalysis

Equations

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

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. @cite{dalrymple-haug-2024}.

• isBound : Bool

  Whether the local antecedent is syntactically bound (=) by the matrix subject.

• hasCollectiveConjunct : Bool

  Whether the embedded predicate is conjoined with a necessarily collective predicate.

• isExhaustiveControl : Bool

  Whether the construction involves exhaustive control vs. partial control.

• controllerIsCollective : Bool

  Whether the controller is interpreted collectively.

• forcesGroupIdentity : Bool

  Whether the pronoun type forces group identity (∪), excluding the binding (=) option. Japanese zibun-tati (plural reflexive), @cite{nishigauchi-1992}.

• isLogophoric : Bool

  Whether the antecedent is a logophoric pronoun.

• hasDistributiveOperator : Bool

  Whether a distributive operator (each, each of them) is present in the matrix clause.

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

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprAntecedentProperties : Repr AntecedentProperties

Equations

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

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

Scope readings predicted by the relational analysis.

Distributive operators are orthogonal on the relational analysis: each other is a pronoun, not a quantified NP, so distribution is orthogonal — both readings remain available. Logophoric antecedents restrict to narrow only.

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.

Diverges from relationalPrediction on:

• Distributive operators: predicts narrow only (incorrect; both attested).
• Logophoric antecedents: predicts both (incorrect; only narrow attested).

Equations

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

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

A synthetic Strongest Meaning Hypothesis at the scope-ambiguity layer (@cite{dalrymple-et-al-1998}'s SMH idea, applied to the choice between narrow and wide scope): when both readings are available, pick the logically stronger one. Narrow scope is stronger than wide in the sense that the narrow-scope reciprocity reading is more restrictive on doxastic alternatives.

Caveat. This is NOT what @cite{haug-dalrymple-2020} §6.1 actually argues against. The paper's §6.1 contrast (eq 132–133) is about SMH applied to reciprocal-reading STRENGTH (Strong vs Weak Reciprocity) under downward-entailing contexts — a different dimension from scope. Properly formalising the §6.1 argument would require a Strong/Weak Reciprocity gradation in the substrate, which PPCDRT does not currently expose. The SMH_diverges_from_relational theorem below is synthetic divergence at the scope layer — a Lean fact, not a paper-faithful refutation.

Equations

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

theorem Semantics.Reference.Reciprocals.SMH_diverges_from_relational : ∃ (props : AntecedentProperties), strongestMeaningPrediction props ≠ relationalPrediction props

Synthetic SMH-vs-relational divergence at the scope layer. On the default property bundle, the relational analysis leaves both readings available; the synthetic SMH commits to narrow only. See the caveat on strongestMeaningPrediction — this is not the paper's §6.1 argument, which is about Strong/Weak Reciprocity not formalised here.

structure Semantics.Reference.Reciprocals.RecipReading : Type

A reciprocal reading per the @cite{haug-dalrymple-2020} two-parameter classification: locus of the reciprocal × type of antecedent relation × type of reciprocal-to-antecedent relation. The three valid cells are exhibited by narrowScopeReading, wideScopeReading, crossedReading; the fourth cell (low locus + bound antecedent) is empirically empty per paper p. 24.

• locus : RecipLocus

  Locus of the reciprocal in the matrix DRS.

• antecedentRel : AnaphoricRelation

  Anaphoric relation between the matrix subject and the embedded local antecedent.

• reciprocalRel : AnaphoricRelation

  Anaphoric relation between the embedded local antecedent and the reciprocal pronoun itself.

def Semantics.Reference.Reciprocals.instDecidableEqRecipReading.decEq (x✝ x✝¹ : RecipReading) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instDecidableEqRecipReading : DecidableEq RecipReading

Equations

• Semantics.Reference.Reciprocals.instDecidableEqRecipReading = Semantics.Reference.Reciprocals.instDecidableEqRecipReading.decEq

@[implicit_reducible]

instance Semantics.Reference.Reciprocals.instReprRecipReading : Repr RecipReading

Equations

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

def Semantics.Reference.Reciprocals.instReprRecipReading.repr : RecipReading → ℕ → Std.Format

Equations

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

def Semantics.Reference.Reciprocals.narrowScopeReading : RecipReading

Narrow-scope reading (we-reading): low locus, group-identity antecedent, in-situ reciprocity. @cite{haug-dalrymple-2020} eq 52.

Equations

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

def Semantics.Reference.Reciprocals.wideScopeReading : RecipReading

Wide-scope reading (I-reading): high locus, bound antecedent, matrix-clause reciprocity. @cite{haug-dalrymple-2020} eq 54.

Equations

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

def Semantics.Reference.Reciprocals.crossedReading : RecipReading

Crossed reading (paper §3.3, eq 56): high locus, group-identity antecedent, group-identity reciprocal slot — reciprocity is contributed by the DRS distinctness presupposition ∂(u₃ ≠ u₂), not by an anaphoric reciprocity relation.

Equations

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

def Semantics.Reference.Reciprocals.recipReadings : List RecipReading

The three attested cells. The empirically-empty fourth cell ({low, bound, _}) is not listed.

Equations

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

theorem Semantics.Reference.Reciprocals.readings_pairwise_distinct : narrowScopeReading ≠ wideScopeReading ∧ crossedReading ≠ narrowScopeReading ∧ crossedReading ≠ wideScopeReading

The three readings are pairwise distinct as RecipReading records. Sanity check that the four-cell classification produces three different cells (not three name-aliases for the same cell).