Reciprocal scope: anaphoric relations, locus, and readings

On the relational analysis of reciprocals (Sternefeld, Beck, Dotlačil, Haug and Dalrymple) each other is a pronoun bearing an anaphoric relation to its antecedent; on the quantificational analysis (Heim, Lasnik and May) it contains a distributive quantifier. The narrow/wide scope ambiguity of a reciprocal in a complement clause is then, relationally, the ambiguity Williams found in any plural anaphor between group identity with the matrix subject (the we-reading) and binding by it (the I-reading).

The relations are conditions on plural information states in Semantics/Dynamic/PPCDRT/Anaphora.lean. This file holds their labels and the two-parameter classification of readings of Haug and Dalrymple §3.3: the locus of the reciprocal, high or low, crossed with the antecedent relation. Three of the four cells are attested; a bound local antecedent denotes an individual and so does not make available the plurality a low reciprocal needs.

Main definitions

• Reciprocal.AnaphoricRelation — binding, group identity, reciprocity.
• Reciprocal.Locus, Reciprocal.Scope — the locus of the reciprocal, ordered by scope, and the two scope readings.
• Reciprocal.ScopeReading — locus × antecedent relation × reciprocal relation, with the three attested cells and Reciprocal.Scope.reading.

References

• [D. T. T. Haug and M. Dalrymple, Reciprocity: Anaphora, scope, and quantification (2020)][haug-dalrymple-2020]
• [M. Dalrymple and D. T. T. Haug, Constraints on reciprocal scope (2024)][dalrymple-haug-2024]
• [I. Heim, H. Lasnik and R. May, Reciprocity and plurality (1991)][heim-lasnik-may-1991]
• [E. Williams, Reciprocal scope (1991)][williams-1991]
• [J. Higginbotham, On semantics (1985)][higginbotham-1985]
• [W. Sternefeld, Reciprocity and cumulative predication (1998)][sternefeld-1998]
• [S. Beck, Reciprocals are definites (2001)][beck-2001]
• [J. Dotlačil, Reciprocals distribute over information states (2013)][dotlacil-2013]

inductive Reciprocal.AnaphoricRelation : Type

The three anaphoric relations Dalrymple and Haug label their arrows with (the arrow is Higginbotham's, the binding/group-identity ambiguity Williams's): properties of a resolution rather than of the pronoun, since the same they can be bound or group-identical.

• binding : AnaphoricRelation

  The pronoun is a bound variable of its antecedent and denotes an individual.

• groupIdentity : AnaphoricRelation

  The pronoun denotes the same plurality as its antecedent.

• reciprocity : AnaphoricRelation

  The same plurality across situations and distinct individuals in each.

@[instance_reducible]

instance Reciprocal.instDecidableEqAnaphoricRelation : DecidableEq AnaphoricRelation

Equations

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

def Reciprocal.instReprAnaphoricRelation.repr : AnaphoricRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reciprocal.instReprAnaphoricRelation : Repr AnaphoricRelation

Equations

• Reciprocal.instReprAnaphoricRelation = { reprPrec := Reciprocal.instReprAnaphoricRelation.repr }

inductive Reciprocal.Locus : Type

The locus of the reciprocal in the matrix update, ordered by scope.

• low : Locus

  In situ in the complement clause.

• high : Locus

  Lifted to the matrix clause.

@[instance_reducible]

instance Reciprocal.instDecidableEqLocus : DecidableEq Locus

Equations

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

@[instance_reducible]

instance Reciprocal.instReprLocus : Repr Locus

Equations

• Reciprocal.instReprLocus = { reprPrec := Reciprocal.instReprLocus.repr }

def Reciprocal.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

• Reciprocal.instReprLocus.repr Reciprocal.Locus.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Locus.low")).group prec✝
• Reciprocal.instReprLocus.repr Reciprocal.Locus.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Locus.high")).group prec✝

@[instance_reducible]

instance Reciprocal.instFintypeLocus : Fintype Locus

Equations

• Reciprocal.instFintypeLocus = { elems := { val := ↑Reciprocal.Locus.enumList, nodup := Reciprocal.Locus.enumList_nodup }, complete := Reciprocal.instFintypeLocus._proof_1 }

def Reciprocal.Locus.toNat : Locus → ℕ

The height of a locus.

Equations

• Reciprocal.Locus.low.toNat = 0
• Reciprocal.Locus.high.toNat = 1

@[instance_reducible]

instance Reciprocal.instLinearOrderLocus : LinearOrder Locus

Equations

• Reciprocal.instLinearOrderLocus = LinearOrder.lift' Reciprocal.Locus.toNat Reciprocal.instLinearOrderLocus._proof_1

@[simp]

theorem Reciprocal.Locus.lt_iff (a b : Locus) : a < b ↔ a = low ∧ b = high

inductive Reciprocal.Scope : Type

The scope readings of a reciprocal in a complement clause.

• narrow : Scope

  The we-reading: "Tracy and Chris each thought 'We saw each other'".

• wide : Scope

  The I-reading: "Tracy thought 'I saw Chris' and Chris thought 'I saw Tracy'".

@[instance_reducible]

instance Reciprocal.instDecidableEqScope : DecidableEq Scope

Equations

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

@[instance_reducible]

instance Reciprocal.instReprScope : Repr Scope

Equations

• Reciprocal.instReprScope = { reprPrec := Reciprocal.instReprScope.repr }

def Reciprocal.instReprScope.repr : Scope → ℕ → Std.Format

Equations

• Reciprocal.instReprScope.repr Reciprocal.Scope.narrow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Scope.narrow")).group prec✝
• Reciprocal.instReprScope.repr Reciprocal.Scope.wide prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reciprocal.Scope.wide")).group prec✝

@[instance_reducible]

instance Reciprocal.instFintypeScope : Fintype Scope

Equations

• Reciprocal.instFintypeScope = { elems := { val := ↑Reciprocal.Scope.enumList, nodup := Reciprocal.Scope.enumList_nodup }, complete := Reciprocal.instFintypeScope._proof_1 }

structure Reciprocal.ScopeReading : Type

A reading in the two-parameter classification.

• locus : Locus

  The locus of the reciprocal.

• antecedentRel : AnaphoricRelation

  The relation between the matrix subject and the reciprocal's local antecedent.

• reciprocalRel : AnaphoricRelation

  The relation between the local antecedent and the reciprocal.

@[instance_reducible]

instance Reciprocal.instDecidableEqScopeReading : DecidableEq ScopeReading

Equations

• Reciprocal.instDecidableEqScopeReading = Reciprocal.instDecidableEqScopeReading.decEq

def Reciprocal.instDecidableEqScopeReading.decEq (x✝ x✝¹ : ScopeReading) : Decidable (x✝ = x✝¹)

Equations

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

def Reciprocal.instReprScopeReading.repr : ScopeReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reciprocal.instReprScopeReading : Repr ScopeReading

Equations

• Reciprocal.instReprScopeReading = { reprPrec := Reciprocal.instReprScopeReading.repr }

def Reciprocal.ScopeReading.narrow : ScopeReading

Narrow scope: low locus, group-identical antecedent, reciprocity in situ.

Equations

• Reciprocal.ScopeReading.narrow = { locus := Reciprocal.Locus.low, antecedentRel := Reciprocal.AnaphoricRelation.groupIdentity, reciprocalRel := Reciprocal.AnaphoricRelation.reciprocity }

@[simp]

theorem Reciprocal.ScopeReading.narrow_antecedentRel : narrow.antecedentRel = AnaphoricRelation.groupIdentity

@[simp]

theorem Reciprocal.ScopeReading.narrow_reciprocalRel : narrow.reciprocalRel = AnaphoricRelation.reciprocity

@[simp]

theorem Reciprocal.ScopeReading.narrow_locus : narrow.locus = Locus.low

def Reciprocal.ScopeReading.wide : ScopeReading

Wide scope: high locus, bound antecedent, reciprocity in the matrix clause.

Equations

• Reciprocal.ScopeReading.wide = { locus := Reciprocal.Locus.high, antecedentRel := Reciprocal.AnaphoricRelation.binding, reciprocalRel := Reciprocal.AnaphoricRelation.reciprocity }

@[simp]

theorem Reciprocal.ScopeReading.wide_locus : wide.locus = Locus.high

@[simp]

theorem Reciprocal.ScopeReading.wide_reciprocalRel : wide.reciprocalRel = AnaphoricRelation.reciprocity

@[simp]

theorem Reciprocal.ScopeReading.wide_antecedentRel : wide.antecedentRel = AnaphoricRelation.binding

def Reciprocal.ScopeReading.crossed : ScopeReading

The crossed reading: high locus, group-identical antecedent and reciprocal, with reciprocity contributed by the distinctness presupposition alone.

Equations

• Reciprocal.ScopeReading.crossed = { locus := Reciprocal.Locus.high, antecedentRel := Reciprocal.AnaphoricRelation.groupIdentity, reciprocalRel := Reciprocal.AnaphoricRelation.groupIdentity }

@[simp]

theorem Reciprocal.ScopeReading.crossed_reciprocalRel : crossed.reciprocalRel = AnaphoricRelation.groupIdentity

@[simp]

theorem Reciprocal.ScopeReading.crossed_locus : crossed.locus = Locus.high

@[simp]

theorem Reciprocal.ScopeReading.crossed_antecedentRel : crossed.antecedentRel = AnaphoricRelation.groupIdentity

def Reciprocal.ScopeReading.attested : List ScopeReading

The three attested cells; the fourth, a low reciprocal with a bound antecedent, is empty.

Equations

• Reciprocal.ScopeReading.attested = [Reciprocal.ScopeReading.narrow, Reciprocal.ScopeReading.wide, Reciprocal.ScopeReading.crossed]

def Reciprocal.Scope.reading : Scope → ScopeReading

The cell of each scope reading.

Equations

• Reciprocal.Scope.narrow.reading = Reciprocal.ScopeReading.narrow
• Reciprocal.Scope.wide.reading = Reciprocal.ScopeReading.wide

@[simp]

theorem Reciprocal.Scope.reading_narrow : narrow.reading = ScopeReading.narrow

@[simp]

theorem Reciprocal.Scope.reading_wide : wide.reading = ScopeReading.wide