Heim, Lasnik & May (1991): Reciprocity and Plurality

[HLM91]

Linguistic Inquiry 22(1): 63–101.

The quantificational analysis of reciprocals: each other is not a simplex anaphor but decomposes at LF into a distributor (each, moved to the antecedent NP) and a reciprocator (e other), each inheriting its semantics from its non-reciprocal use. The LF of "the men saw each other" is [[the men]₁ each₂] saw [e₂ other]₃ — a four-part structure group antecedent – distributor – reciprocator – predicate (their (9)). This is the quantificational arm of the comparison drawn in Semantics/Reference/Reciprocals.lean, and the decomposed counterpart of Link's holistic Algebra.DJR operator.

Two puzzles drive the paper (both from [Hig85] and [Hig80]): the grain problem — "John and Mary told each other that they should leave" is three-ways ambiguous (I/you/we readings) though binding theory allows only one indexing — and the scope puzzle — embedded reciprocals allow broad and narrow construals. Both resolve through the double indexing of plural NPs (range + distribution indices, their (26)–(29)): the pronoun construals bound by the quantificational each/other indices are singular bound variables (I/you readings), those coindexed with the referential range index are coreference anaphora (we readings), and scope covaries with anaphora type because distributors are undefined on atoms and cannot iterate.

Main declarations

• other (16), reciprocator (18), distributor (19)/(28) — the compositional pieces; the distributor is the Finset-level, world-free form of Plurality.distMaximal and Algebra.D.
• eachOtherLF + eachOtherLF_iff_strongReciprocity — the keystone: the each∘other composition derives StrongReciprocity (their (21)), plugging the LF analysis into the DKMPK entailment lattice.
• eachOtherLF_singleton — distribution over a singleton is vacuous: the semantic shadow of the definedness restriction that derives the plural-antecedent requirement (*Mary saw each other).
• eachOtherLF_asymmetric_contradictory — (68) "they are taller than each other" is contradictory on any genuine plurality.
• PronounConstrual, GrainReading, AnaphoraType — the grain solution (29)/(49): four construals, four readings, I/you = bound variable vs we = coreference.
• EachAttachment, scopeWellFormed — the scope solution (67): narrow ⇔ coreference and broad ⇔ bound variable, derived from the sum-host requirement on distributors and Principle A on the trace of each.

Todo

• §4.2 long-distance reciprocals (Specified Subject Condition evasion via broad scope) and the each … the other variant constructions.
• Weaker-than-universal force: HLM restrict attention to two-membered groups (their fn. on (18)); connecting the composition to the weaker DKMPK schemes for larger groups is rival territory ([DKK+98]).

The compositional pieces (§2.2)

HLM's model is ⟨D, A, Π⟩: a domain with mereological structure, atoms A, and proper-part-of Π; ·Π is the proper-atomic-part relation. Pluralities are encoded here as Finset A (sums of atoms) with ·Π as membership, matching the (R, X) signature of Semantics.Plurality.Reciprocal.

def HeimLasnikMay1991.other {A : Type u_1} (contrast : A) (range : Finset A) (z : A) : Prop

(16): other as a 3-place relation — referent z is an atomic part of the range y distinct from the contrast x. In reciprocals both implicit arguments are supplied by the derived antecedent phrase: the contrast is bound by each, the range is coreferential with the antecedent.

Equations

• HeimLasnikMay1991.other contrast range z = (z ∈ range ∧ z ≠ contrast)

def HeimLasnikMay1991.reciprocator {A : Type u_1} (range : Finset A) (ζ : A → A → Prop) (x : A) : Prop

(18): the reciprocator [e other] with universal force — x stands in ζ to every other atomic part of the range. (HLM adopt universal force while restricting attention to two-membered groups, where universal and existential force coincide.)

Equations

• HeimLasnikMay1991.reciprocator range ζ x = ∀ (z : A), HeimLasnikMay1991.other x range z → ζ x z

def HeimLasnikMay1991.distributor {A : Type u_1} (np : Finset A) (φ : A → Prop) : Prop

(19)/(28): the distributor — each or the covert D — universally quantifies over the atomic parts of its host NP. The world-free Finset form of Plurality.distMaximal (English floated each) and of Algebra.D (Link's D operator).

Equations

• HeimLasnikMay1991.distributor np φ = ∀ x ∈ np, φ x

def HeimLasnikMay1991.eachOtherLF {A : Type u_1} (np : Finset A) (R : A → A → Prop) : Prop

The LF of "np V each other" after each-movement (their (8)/(20)): the distributor scopes over the reciprocated predicate, with the reciprocator's range and contrast both anaphoric to the derived antecedent.

Equations

• HeimLasnikMay1991.eachOtherLF np R = HeimLasnikMay1991.distributor np (HeimLasnikMay1991.reciprocator np R)

The keystone (their (21))

theorem HeimLasnikMay1991.eachOtherLF_iff_strongReciprocity {A : Type u_1} [DecidableEq A] (np : Finset A) (R : A → A → Prop) : eachOtherLF np R ↔ Semantics.Plurality.Reciprocal.StrongReciprocity R np

The compositional each∘other analysis derives Strong Reciprocity: HLM's truth conditions "coincide with those of the standard semantic analyses". Through the entailment lattice of Semantics.Plurality.Reciprocal, the weaker schemes follow (strong_imp_weak, …).

theorem HeimLasnikMay1991.eachOtherLF_singleton {A : Type u_1} [DecidableEq A] (a : A) (R : A → A → Prop) : eachOtherLF {a} R

Distribution over a singleton yields a vacuously true reciprocal — no reciprocal content at all. HLM derive the plural-antecedent requirement (*Mary saw each other) more strongly: ·Π is defined only on sum counterdomains, so distributors cannot apply to singular NPs; this vacuity is the semantic shadow of that definedness restriction.

theorem HeimLasnikMay1991.eachOtherLF_asymmetric_contradictory {A : Type u_1} [DecidableEq A] {np : Finset A} {R : A → A → Prop} (hasym : ∀ (x y : A), R x y → ¬R y x) (hcard : 2 ≤ np.card) : ¬eachOtherLF np R

(68) "They are taller than each other" is contradictory: the each∘other composition over an asymmetric relation fails on every genuine plurality. Under embedding, only broad scope of each rescues it ((69)/(70)); with an explicit matrix distributor, re-attachment would stack distributors ((71)/(72)), so only the contradictory narrow reading survives.

The grain problem (§3)

Plural NPs bear a range index and, optionally, a distribution index ((26)–(28)); in a reciprocal LF the reciprocator contributes a third index. An embedded plural pronoun anaphoric to the antecedent therefore has exactly four construals ((29)/(49)) — the theory is exactly as fine-grained as the attested ambiguity of "John and Mary told each other that they should leave".

inductive HeimLasnikMay1991.PronounConstrual : Type

The four construals of an embedded plural pronoun in a reciprocal sentence ((49a–d)).

• range : PronounConstrual

  coindexed with the antecedent's referential range index

• rangeDistributed : PronounConstrual

  range-coindexed, with its own covert distributor D

• distributor : PronounConstrual

  bound by the distribution index contributed by each

• reciprocator : PronounConstrual

  bound by the reciprocator's index

@[implicit_reducible]

instance HeimLasnikMay1991.instDecidableEqPronounConstrual : DecidableEq PronounConstrual

Equations

• HeimLasnikMay1991.instDecidableEqPronounConstrual x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeimLasnikMay1991.instReprPronounConstrual : Repr PronounConstrual

Equations

• HeimLasnikMay1991.instReprPronounConstrual = { reprPrec := HeimLasnikMay1991.instReprPronounConstrual.repr }

def HeimLasnikMay1991.instReprPronounConstrual.repr : PronounConstrual → ℕ → Std.Format

Equations

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

inductive HeimLasnikMay1991.GrainReading : Type

The readings of "John and Mary told each other that they should leave" ((43): I = "each told the other: I should leave", you = "…: you should leave", we together/separately).

• I : GrainReading
• you : GrainReading
• weTogether : GrainReading
• weSeparately : GrainReading

@[implicit_reducible]

instance HeimLasnikMay1991.instDecidableEqGrainReading : DecidableEq GrainReading

Equations

• HeimLasnikMay1991.instDecidableEqGrainReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeimLasnikMay1991.instReprGrainReading : Repr GrainReading

Equations

• HeimLasnikMay1991.instReprGrainReading = { reprPrec := HeimLasnikMay1991.instReprGrainReading.repr }

def HeimLasnikMay1991.instReprGrainReading.repr : GrainReading → ℕ → Std.Format

Equations

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

def HeimLasnikMay1991.PronounConstrual.reading : PronounConstrual → GrainReading

(49a–d): each construal yields exactly one reading.

Equations

• HeimLasnikMay1991.PronounConstrual.distributor.reading = HeimLasnikMay1991.GrainReading.I
• HeimLasnikMay1991.PronounConstrual.reciprocator.reading = HeimLasnikMay1991.GrainReading.you
• HeimLasnikMay1991.PronounConstrual.range.reading = HeimLasnikMay1991.GrainReading.weTogether
• HeimLasnikMay1991.PronounConstrual.rangeDistributed.reading = HeimLasnikMay1991.GrainReading.weSeparately

inductive HeimLasnikMay1991.AnaphoraType : Type

Bound-variable vs coreference anaphora — the type distinction the grain solution encodes structurally (§3.1, against [Hig85]'s linking alternative, where I/we would be one vague reading).

• boundVariable : AnaphoraType
• coreference : AnaphoraType

@[implicit_reducible]

instance HeimLasnikMay1991.instDecidableEqAnaphoraType : DecidableEq AnaphoraType

Equations

• HeimLasnikMay1991.instDecidableEqAnaphoraType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeimLasnikMay1991.instReprAnaphoraType : Repr AnaphoraType

Equations

• HeimLasnikMay1991.instReprAnaphoraType = { reprPrec := HeimLasnikMay1991.instReprAnaphoraType.repr }

def HeimLasnikMay1991.instReprAnaphoraType.repr : AnaphoraType → ℕ → Std.Format

Equations

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

def HeimLasnikMay1991.PronounConstrual.anaphoraType : PronounConstrual → AnaphoraType

Construals bound by the quantificational each/other indices are singular bound variables; range-coindexed construals are coreference with the referential sum. Hence I/you = bound variable, we = coreference.

Equations

• HeimLasnikMay1991.PronounConstrual.distributor.anaphoraType = HeimLasnikMay1991.AnaphoraType.boundVariable
• HeimLasnikMay1991.PronounConstrual.reciprocator.anaphoraType = HeimLasnikMay1991.AnaphoraType.boundVariable
• HeimLasnikMay1991.PronounConstrual.range.anaphoraType = HeimLasnikMay1991.AnaphoraType.coreference
• HeimLasnikMay1991.PronounConstrual.rangeDistributed.anaphoraType = HeimLasnikMay1991.AnaphoraType.coreference

def HeimLasnikMay1991.PronounConstrual.denotesAtom (c : PronounConstrual) : Bool

A bound-variable construal ranges over atoms; a coreferential one denotes the antecedent's sum (§2.4).

Equations

• c.denotesAtom = (c.anaphoraType == HeimLasnikMay1991.AnaphoraType.boundVariable)

def HeimLasnikMay1991.PronounConstrual.hostsDistributor : PronounConstrual → Bool

Whether the construal places the pronoun under a distributor of its own ((49d)).

Equations

• HeimLasnikMay1991.PronounConstrual.rangeDistributed.hostsDistributor = true
• x✝.hostsDistributor = false

def HeimLasnikMay1991.PronounConstrual.availableInPreposedAdjunct (c : PronounConstrual) : Bool

Preposed adjuncts block bound-variable anaphora ((61): a quantifier cannot bind into a preposed adjunct), so "After they had left the room, the candidates criticized each other" (60) keeps only the we construals, while the postposed (57) is fully ambiguous.

Equations

• c.availableInPreposedAdjunct = (c.anaphoraType == HeimLasnikMay1991.AnaphoraType.coreference)

theorem HeimLasnikMay1991.preposed_adjunct_blocks_bound_variables (c : PronounConstrual) : c.availableInPreposedAdjunct = false ↔ c.reading = GrainReading.I ∨ c.reading = GrainReading.you

The preposed-adjunct diagnostic isolates exactly the bound-variable construals: what (60) loses relative to (57) is the I and you readings.

The scope puzzle (§4)

"John and Mary think they like each other" (64) has a narrow reading (they think: we like each other) and a broad one (each thinks: I like the other). HLM resolve it as the attachment site of each ((67)): to the embedded pronoun (narrow) or to the matrix subject (broad). The correlation with anaphora type is derived: distributors need sum-denoting hosts and cannot iterate, and the trace of each must be bound by the index its host acquires (Principle A).

inductive HeimLasnikMay1991.EachAttachment : Type

Where each attaches at LF ((67a)/(67b)).

• embedded : EachAttachment

  [they₁ each₂] like [e₂ other] — narrow scope

• matrix : EachAttachment

  [[John and Mary]₁ each₂] think they₂ like [e₂ other] — broad

@[implicit_reducible]

instance HeimLasnikMay1991.instDecidableEqEachAttachment : DecidableEq EachAttachment

Equations

• HeimLasnikMay1991.instDecidableEqEachAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeimLasnikMay1991.instReprEachAttachment : Repr EachAttachment

Equations

• HeimLasnikMay1991.instReprEachAttachment = { reprPrec := HeimLasnikMay1991.instReprEachAttachment.repr }

def HeimLasnikMay1991.instReprEachAttachment.repr : EachAttachment → ℕ → Std.Format

Equations

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

def HeimLasnikMay1991.scopeWellFormed : EachAttachment → PronounConstrual → Prop

Wellformedness of an attachment–construal pair, from two independent constraints: an each attached to the embedded pronoun needs a sum-denoting host that is not already distributed ((72): distributors do not iterate), and under matrix attachment the pronoun must carry the distribution index so that the trace of each is A-bound (Principle A, their (74)).

Equations

• HeimLasnikMay1991.scopeWellFormed HeimLasnikMay1991.EachAttachment.embedded x✝ = (x✝.denotesAtom = false ∧ x✝.hostsDistributor = false)
• HeimLasnikMay1991.scopeWellFormed HeimLasnikMay1991.EachAttachment.matrix x✝ = (x✝ = HeimLasnikMay1991.PronounConstrual.distributor)

theorem HeimLasnikMay1991.narrow_forces_coreference (c : PronounConstrual) (h : scopeWellFormed EachAttachment.embedded c) : c.anaphoraType = AnaphoraType.coreference

Narrow scope forces a coreferential pronoun ((67a)).

theorem HeimLasnikMay1991.broad_forces_bound_variable (c : PronounConstrual) (h : scopeWellFormed EachAttachment.matrix c) : c.anaphoraType = AnaphoraType.boundVariable

Broad scope forces a bound-variable pronoun ((67b)): scope and anaphora type covary, the paper's answer to Williams's nonscope alternative (§4.1).

theorem HeimLasnikMay1991.embedded_unique_construal (c : PronounConstrual) : scopeWellFormed EachAttachment.embedded c ↔ c = PronounConstrual.range

Under embedded attachment exactly one construal survives: plain range coreference — (67a)'s indexing is forced.