Haug and Dalrymple (2020): Reciprocity: Anaphora, scope, and quantification

Haug and Dalrymple give a relational analysis of reciprocity in Partial Plural Compositional DRT. The reciprocal contributes group identity with its antecedent and pointwise distinctness ((41), PPCDRT.reciprocityCond); the scope ambiguity of a reciprocal in a complement clause is the ambiguity of any plural anaphor between group identity (PPCDRT.groupIdentityCond) and binding (PPCDRT.bindingCond) with the matrix subject, read through the distribution of §2.3 under which the antecedent escapes the distribution operator. The sample output states of the paper are transcribed as plural information states (ofRows) and the conditions checked on them: the two readings of the lawyers' secretary (24), (31), the narrow and wide readings of the girls' belief (49), (51), (53), (55), the crossed reading (56), the modal (69), the mixed construal of the Cheyenne affix (78), multiple reciprocals (85), (86), the forks (93), the sailors (96), and the wide construal with three girls (136). no_low_reciprocal_under_binding derives the empty cell of §3.3: a bound antecedent leaves no plurality for a reciprocal inside the distribution.

The paper's relation to cumulation is stated in general. Pointwise conditions on plural states give cumulative readings (§2.1, cumulative_iff_exists_relCond), with the truth conditions of Sternefeld's cumulation operator (§4.1, cumulation_iff_exists_relCond). A simple reciprocal sentence is true exactly when its antecedent is weakly reciprocal under the verb (§2.4, weakReciprocity_iff_exists_reciprocalDRS), which is Sternefeld's reading (76) (cumulation_iff_exists_reciprocalDRS). Without distribution, and whatever the verb, the dependency between the antecedent and the reciprocal is weakly reciprocal (weakReciprocity_dep_of_reciprocityCond), of which the forks are an instance (forks_weak).

Quantified antecedents (§5) get the two readings of (99), RefSetReading over a maximal reciprocal subset and MaxSetReading over the participants, and the supervaluation truth value of (109), truthValue, with maxSetReading_of_refSetReading for upward monotone determiners and the street and club scenarios of §5.1–§5.2. Maximize Anaphora (128) is MaximizesAnaphora; it selects the states whose dependency contains every pair the verb allows (maximizesAnaphora_iff), hence Strong Reciprocity when the verb allows every pair (strongReciprocity_dep_iff), the strong reading (126b) over the minimal state (126a) (maximize_strong), and it maximizes multiple reciprocals pairwise (§6.2).

Implementation notes

• Distribution is represented by the set Δ of a PPCDRT.PPDRSCond; the operators δ, T and think of (14), (46) are not defined, and each sample state is checked under the Δ its DRS induces. The max operator of (97) is likewise replaced by the static readings it yields.
• A DRS is true when some output state satisfies its conditions. relCond asks every state to value its discourse referents, which the partial introduction (6), (20) guarantees: the states PPCDRT.introPartial reaches from the empty state {⊥} are exactly those whose rows value the introduced drefs (introPartial_comp_iff), and truth reached from {⊥} agrees with truth at some state (weakReciprocity_iff_exists_introPartial).
• ReciprocalDRS fixes the antecedent's plurality, ∪u' = X, as a definite antecedent does; (125b) has the pointwise restrictor boy(u₁) instead. boysKnow takes X to be the three boys.
• The pairs R_u of (127) are the dependency PCDRT.dep, taken antecedent first so that they line up with the verb's arguments; the order does not affect maximization.
• Worlds are values of the same domain as individuals, at the discourse referent w.
• The antecedence condition for the second reciprocal of (85b) is read with u₂, as the indices of (85a) and the state (85c) give.

TODO

• The distribution and maximization relations δ_u and max^u of (14) and (97), so that the sample states are derived from the DRSs rather than transcribed; introduction, (6) and (20), is PPCDRT.introPartial.
• With the pointwise restrictor ∪u' ⊆ A of (125b) in place of ∪u' = X, Maximize Anaphora selects the states whose dependency is full on a maximal weakly reciprocal subset of A, the shape of the reference sets of §5 (IsRefSet).

References

• D. T. T. Haug and M. Dalrymple, Reciprocity: Anaphora, scope, and quantification (2020)
• D. T. Langendoen, The logic of reciprocity (1978)
• W. Sternefeld, Reciprocity and cumulative predication (1998)
• S. Beck and U. Sauerland, Cumulation is needed: A reply to Winter (2000) (2000)
• J. Dotlačil, Reciprocals distribute over information states (2013)
• S. E. Murray, Reflexivity and reciprocity with(out) underspecification (2008)
• M. Križ, Aspects of homogeneity in the semantics of natural language (2015)
• L. Champollion, D. Bumford and R. Henderson, Donkeys under discussion (2019)

Sample states

inductive HaugDalrymple2020.Ind : Type

The individuals and worlds of the sample states.

• girl1 : Ind
• girl2 : Ind
• tracy : Ind
• chris : Ind
• matty : Ind
• world1 : Ind
• world2 : Ind
• world3 : Ind
• lawyer1 : Ind
• lawyer2 : Ind
• lawyer3 : Ind
• secretary1 : Ind
• secretary2 : Ind
• secretary3 : Ind
• picture1 : Ind
• picture2 : Ind
• picture3 : Ind
• fork1 : Ind
• fork2 : Ind
• fork3 : Ind
• sailor1 : Ind
• sailor2 : Ind
• sailor3 : Ind
• ship1 : Ind
• ship2 : Ind
• ship3 : Ind
• child1 : Ind
• child2 : Ind
• child3 : Ind
• boy1 : Ind
• boy2 : Ind
• boy3 : Ind

@[instance_reducible]

instance HaugDalrymple2020.instDecidableEqInd : DecidableEq Ind

Equations

• HaugDalrymple2020.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HaugDalrymple2020.instFintypeInd : Fintype Ind

Equations

• HaugDalrymple2020.instFintypeInd = { elems := { val := ↑HaugDalrymple2020.Ind.enumList, nodup := HaugDalrymple2020.Ind.enumList_nodup }, complete := HaugDalrymple2020.instFintypeInd._proof_1 }

@[instance_reducible]

instance HaugDalrymple2020.instReprInd : Repr Ind

Equations

• HaugDalrymple2020.instReprInd = { reprPrec := HaugDalrymple2020.instReprInd.repr }

def HaugDalrymple2020.instReprInd.repr : Ind → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev HaugDalrymple2020.u₁ : ℕ

The discourse referent u₁.

Equations

• HaugDalrymple2020.u₁ = 1

@[reducible, inline]

abbrev HaugDalrymple2020.u₂ : ℕ

The discourse referent u₂.

Equations

• HaugDalrymple2020.u₂ = 2

@[reducible, inline]

abbrev HaugDalrymple2020.u₃ : ℕ

The discourse referent u₃.

Equations

• HaugDalrymple2020.u₃ = 3

@[reducible, inline]

abbrev HaugDalrymple2020.u₄ : ℕ

The discourse referent u₄.

Equations

• HaugDalrymple2020.u₄ = 4

@[reducible, inline]

abbrev HaugDalrymple2020.w : ℕ

The world discourse referent w of §3.1.

Equations

• HaugDalrymple2020.w = 5

def HaugDalrymple2020.row {E : Type u_1} (l : List (ℕ × E)) : PartialAssign ℕ E

A row of a sample state, from its defined discourse referents.

Equations

• HaugDalrymple2020.row l u = (List.find? (fun (x : ℕ × E) => x.1 == u) l).elim ⊥ fun (p : ℕ × E) => ↑p.2

theorem HaugDalrymple2020.row_pair_left {E : Type u_1} (u v : ℕ) (a b : E) : row [(u, a), (v, b)] u = ↑a

theorem HaugDalrymple2020.row_pair_right {E : Type u_1} {u v : ℕ} (h : u ≠ v) (a b : E) : row [(u, a), (v, b)] v = ↑b

def HaugDalrymple2020.ofRows (rows : List (PartialAssign ℕ Ind)) : PluralAssign ℕ Ind

The plural information state with the given rows.

Equations

• HaugDalrymple2020.ofRows rows = {g : PartialAssign ℕ HaugDalrymple2020.Ind | g ∈ rows}

theorem HaugDalrymple2020.bindingCond_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {u u' : ℕ} : PPCDRT.bindingCond u u' (ofRows rows) Δ ↔ ∀ s ∈ rows, s u = s u'

theorem HaugDalrymple2020.groupIdentityCond_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {u u' : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) : PPCDRT.groupIdentityCond u u' (ofRows rows) Δ ↔ ∀ s ∈ rows, ∀ (d : Ind), (∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u = ↑d) ↔ ∃ t ∈ rows, t u' = ↑d

theorem HaugDalrymple2020.distinct_ofRows {rows : List (PartialAssign ℕ Ind)} {u u' : ℕ} : (∀ s ∈ ofRows rows, ∀ (a b : Ind), s u = ↑a → s u' = ↑b → a ≠ b) ↔ ∀ s ∈ rows, ∀ (a b : Ind), s u = ↑a → s u' = ↑b → a ≠ b

theorem HaugDalrymple2020.reciprocityCond_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {u u' : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) : PPCDRT.reciprocityCond u u' (ofRows rows) Δ ↔ (∀ s ∈ rows, ∀ (d : Ind), (∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u = ↑d) ↔ ∃ t ∈ rows, t u' = ↑d) ∧ ∀ s ∈ rows, ∀ (a b : Ind), s u = ↑a → s u' = ↑b → a ≠ b

theorem HaugDalrymple2020.mem_dep_ofRows {rows : List (PartialAssign ℕ Ind)} {u u' : ℕ} {a b : Ind} : (a, b) ∈ PCDRT.dep u u' (ofRows rows) ↔ ∃ s ∈ rows, s u = ↑a ∧ s u' = ↑b

theorem HaugDalrymple2020.mem_dep_eqClass_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {u u' : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) {s : PartialAssign ℕ Ind} {a b : Ind} : (a, b) ∈ PCDRT.dep u u' (PPCDRT.eqClass (ofRows rows) Δ s) ↔ ∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u = ↑a ∧ t u' = ↑b

def HaugDalrymple2020.sumRows (rows : List (PartialAssign ℕ Ind)) (Δl : List ℕ) (s : PartialAssign ℕ Ind) (u : ℕ) : Finset Ind

The values of u summed over the Δ-class of s, as a finset.

Equations

• HaugDalrymple2020.sumRows rows Δl s u = {d : HaugDalrymple2020.Ind | ∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u = ↑d}

theorem HaugDalrymple2020.coe_sumRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {u : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) (s : PartialAssign ℕ Ind) : ↑(sumRows rows Δl s u) = PCDRT.value u (PPCDRT.eqClass (ofRows rows) Δ s)

theorem HaugDalrymple2020.mem_ofRows {rows : List (PartialAssign ℕ Ind)} {s : PartialAssign ℕ Ind} : s ∈ ofRows rows ↔ s ∈ rows

theorem HaugDalrymple2020.value_ofRows {rows : List (PartialAssign ℕ Ind)} {u : ℕ} : PCDRT.value u (ofRows rows) = ↑(sumRows rows [] (row []) u)

def HaugDalrymple2020.atomsCond (n u : ℕ) : PPCDRT.PPDRSCond Ind

The collective condition n-atoms(∪u) of (9) under distribution holds when, in every state, the values of u summed over the state's class number n ((27), (28b)).

Equations

• HaugDalrymple2020.atomsCond n u S Δ = ∀ s ∈ S, (PCDRT.value u (PPCDRT.eqClass S Δ s)).ncard = n

theorem HaugDalrymple2020.atomsCond_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {n u : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) : atomsCond n u (ofRows rows) Δ ↔ ∀ s ∈ rows, (sumRows rows Δl s u).card = n

def HaugDalrymple2020.relCond {E : Type u_1} (P : E → E → Prop) (u v : ℕ) : PPCDRT.PPDRSCond E

A lexical relation as a condition ((7), (27)) holds when the state is nonempty and every state gives u and v values that P relates. Distribution does not reach individual discourse referents, so Δ is idle.

Equations

• HaugDalrymple2020.relCond P u v S x✝ = (Set.Nonempty S ∧ ∀ s ∈ S, ∃ (a : E) (b : E), s u = ↑a ∧ s v = ↑b ∧ P a b)

theorem HaugDalrymple2020.relCond_ofRows {P : Ind → Ind → Prop} {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {u v : ℕ} : relCond P u v (ofRows rows) Δ ↔ rows ≠ [] ∧ ∀ s ∈ rows, ∃ (a : Ind) (b : Ind), s u = ↑a ∧ s v = ↑b ∧ P a b

def HaugDalrymple2020.distributedGroupIdentityCond (uAnaph uAnt : ℕ) : PPCDRT.PPDRSCond Ind

Group identity read inside the distribution operator of (14), summing both sides over the class. This is the reading under which (23b) is not representable (§2.3).

Equations

• HaugDalrymple2020.distributedGroupIdentityCond uAnaph uAnt S Δ = ∀ s ∈ S, PCDRT.value uAnaph (PPCDRT.eqClass S Δ s) = PCDRT.value uAnt (PPCDRT.eqClass S Δ s)

theorem HaugDalrymple2020.distributedGroupIdentityCond_ofRows {rows : List (PartialAssign ℕ Ind)} {Δ : Set ℕ} {Δl : List ℕ} {u u' : ℕ} (hΔ : ∀ (v : ℕ), v ∈ Δ ↔ v ∈ Δl) : distributedGroupIdentityCond u u' (ofRows rows) Δ ↔ ∀ s ∈ rows, ∀ (d : Ind), (∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u = ↑d) ↔ ∃ t ∈ rows, (∀ v ∈ Δl, t v = s v) ∧ t u' = ↑d

Anaphora under distribution (§2.3)

def HaugDalrymple2020.lawyersBound : List (PartialAssign ℕ Ind)

The lawyers hired secretaries they each liked, u₃ bound to u₁ (24c).

Equations

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

def HaugDalrymple2020.lawyersGroup : List (PartialAssign ℕ Ind)

The lawyers hired secretaries all of them liked, ∪u₃ → ∪u₁ under δ_{u₁} (31c).

Equations

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

theorem HaugDalrymple2020.lawyers_bound : PPCDRT.bindingCond u₃ u₁ (ofRows lawyersBound) {u₁} ∧ atomsCond 1 u₂ (ofRows lawyersBound) {u₁} ∧ ¬PPCDRT.groupIdentityCond u₃ u₁ (ofRows lawyersBound) {u₁}

Read as (24), (23a) has they bound by the lawyers, one secretary per lawyer under δ_{u₁}, and no group identity under the distribution.

theorem HaugDalrymple2020.lawyers_group : PPCDRT.groupIdentityCond u₃ u₁ (ofRows lawyersGroup) {u₁} ∧ atomsCond 1 u₂ (ofRows lawyersGroup) {u₁} ∧ ¬PPCDRT.bindingCond u₃ u₁ (ofRows lawyersGroup) {u₁} ∧ ¬atomsCond 1 u₂ (ofRows lawyersGroup) ∅ ∧ ¬distributedGroupIdentityCond u₃ u₁ (ofRows lawyersGroup) {u₁}

Read as (31), (23b) has ∪u₃ → ∪u₁ escape δ_{u₁}, with one secretary per lawyer and no binding. The same state fails group identity read inside the distribution operator of (14), which is why (23b) needs the distribution of §2.3.

Cumulative readings and Weak Reciprocity (§1, §2.1, §2.4, §4.1)

def HaugDalrymple2020.ofDep {E : Type u_1} (u v : ℕ) (D : SetRel E E) : PluralAssign ℕ E

The state with a row for each pair of D, valuing u and v as its two components, so that its dependency between u and v is D.

Equations

• HaugDalrymple2020.ofDep u v D = (fun (p : E × E) => HaugDalrymple2020.row [(u, p.1), (v, p.2)]) '' D

theorem HaugDalrymple2020.dep_ofDep {E : Type u_1} {u v : ℕ} (h : u ≠ v) (D : SetRel E E) : PCDRT.dep u v (ofDep u v D) = D

theorem HaugDalrymple2020.relCond_ofDep {E : Type u_1} {P : E → E → Prop} {u v : ℕ} {D : SetRel E E} (h : u ≠ v) (hD : D ⊆ {p : E × E | P p.1 p.2}) (hne : Set.Nonempty D) : relCond P u v (ofDep u v D) ∅

theorem HaugDalrymple2020.dep_of_relCond {E : Type u_1} {P : E → E → Prop} {u v : ℕ} {S : PluralAssign ℕ E} {Δ : Set ℕ} (hS : relCond P u v S Δ) : PCDRT.dep u v S ⊆ {p : E × E | P p.1 p.2} ∧ (PCDRT.dep u v S).dom = PCDRT.value u S ∧ (PCDRT.dep u v S).cod = PCDRT.value v S

Under P(u, v) the dependency between u and v lies in P, with the values of u as its domain and the values of v as its codomain.

theorem HaugDalrymple2020.value_ofDep_left {E : Type u_1} {u v : ℕ} (h : u ≠ v) (D : SetRel E E) : PCDRT.value u (ofDep u v D) = D.dom

theorem HaugDalrymple2020.value_ofDep_right {E : Type u_1} {u v : ℕ} (h : u ≠ v) (D : SetRel E E) : PCDRT.value v (ofDep u v D) = D.cod

theorem HaugDalrymple2020.cumulative_iff_exists_relCond {E : Type u_1} {P : E → E → Prop} {u v : ℕ} (h : u ≠ v) {x y : Set E} : x.Nonempty ∧ Set.LiftRel P x y ↔ ∃ (S : PluralAssign ℕ E), PCDRT.value u S = x ∧ PCDRT.value v S = y ∧ relCond P u v S ∅

By §2.1, (12), cumulative readings are the default. A state satisfying P(u, v) relates the values of u to the values of v cumulatively in the sense of [BS00], and any two pluralities so related are the values of such a state.

theorem HaugDalrymple2020.cumulation_iff_exists_relCond {E : Type u_1} {P : E → E → Prop} {u v : ℕ} [DecidableEq E] (h : u ≠ v) {x y : Finset E} : Plurality.Cumulativity.Cumulation (Relation.Map P (fun (x : E) => {x}) fun (x : E) => {x}) x y ↔ ∃ (S : PluralAssign ℕ E), PCDRT.value u S = ↑x ∧ PCDRT.value v S = ↑y ∧ relCond P u v S ∅

By §4.1, (75), the cumulation operator ** that [Ste98] applies to the predicate and the pointwise conditions of Plural CDRT give the same truth conditions.

def HaugDalrymple2020.ReciprocalDRS {E : Type u_1} (P : E → E → Prop) (X : Set E) (u u' : ℕ) (S : PluralAssign ℕ E) : Prop

In the DRS of a reciprocal sentence whose antecedent denotes X, as in (40b) and (125b), the antecedent u' sums to X, P relates u' to the reciprocal u in every state, and u is reciprocal to u' ((42)).

Equations

• HaugDalrymple2020.ReciprocalDRS P X u u' S = (PCDRT.value u' S = X ∧ HaugDalrymple2020.relCond P u' u S ∅ ∧ PPCDRT.reciprocityCond u u' S ∅)

theorem HaugDalrymple2020.reciprocalDRS_iff {E : Type u_1} {P : E → E → Prop} {u : ℕ} {S : PluralAssign ℕ E} {X : Set E} {u' : ℕ} : ReciprocalDRS P X u u' S ↔ PCDRT.value u' S = X ∧ PCDRT.value u S = X ∧ relCond (fun (a b : E) => P a b ∧ a ≠ b) u' u S ∅

The reciprocal DRS is the pointwise condition of P with non-identity conjoined, with X in both argument positions. Group identity puts X in the second, and the distinctness presupposition contributes the non-identity.

theorem HaugDalrymple2020.weakReciprocity_iff_exists_reciprocalDRS {E : Type u_1} {P : E → E → Prop} {u u' : ℕ} (h : u ≠ u') {X : Finset E} : X.Nonempty ∧ Reciprocal.WeakReciprocity P X ↔ ∃ (S : PluralAssign ℕ E), ReciprocalDRS P (↑X) u u' S

As §2.4 puts it, "This proposal, like Dotlačil's, makes Weak Reciprocity the basic reading." Some state verifies the DRS of the Xs P each other exactly when X is weakly reciprocal under P ([Lan78]). The reciprocal is cumulative predication of P with non-identity conjoined, which is Langendoen's comparison of the women pointed at each other with the women released the prisoners (§1).

theorem HaugDalrymple2020.cumulation_iff_exists_reciprocalDRS {E : Type u_1} {P : E → E → Prop} {u : ℕ} [DecidableEq E] {u' : ℕ} (h : u ≠ u') {X : Finset E} : Plurality.Cumulativity.Cumulation (Relation.Map (fun (a b : E) => P a b ∧ a ≠ b) (fun (x : E) => {x}) fun (x : E) => {x}) X X ↔ ∃ (S : PluralAssign ℕ E), ReciprocalDRS P (↑X) u u' S

By §4.1, (76), [Ste98]'s weak reciprocal, ** of P with non-identity conjoined served the same plurality twice, and the PPCDRT reciprocal (42) agree on simple reciprocal sentences; they differ in architecture, not in these truth conditions.

theorem HaugDalrymple2020.introPartial_comp_iff {E : Type u_1} {u u' : ℕ} {O : PluralAssign ℕ E} (h : u ≠ u') : ({⊥}, O) ∈ SetRel.comp (PPCDRT.introPartial u') (PPCDRT.introPartial u) ↔ Set.Nonempty O ∧ ∀ o ∈ O, ∀ (v : ℕ), o v ≠ ⊥ ↔ v = u' ∨ v = u

Introducing u' and then u at the empty state {⊥}, (6) and (20), reaches exactly the nonempty states whose rows value u' and u and nothing else.

theorem HaugDalrymple2020.weakReciprocity_iff_exists_introPartial {E : Type u_1} {P : E → E → Prop} {u u' : ℕ} (h : u ≠ u') {X : Finset E} : X.Nonempty ∧ Reciprocal.WeakReciprocity P X ↔ ∃ (O : PluralAssign ℕ E), ({⊥}, O) ∈ SetRel.comp (PPCDRT.introPartial u') (PPCDRT.introPartial u) ∧ ReciprocalDRS P (↑X) u u' O

Entered by introducing u' and u at {⊥} ((6), (20)), the DRS of the Xs P each other has an output verifying it exactly when X is weakly reciprocal under P. A verifying state restricted to its u' and u columns is reachable and still verifies the DRS.

theorem HaugDalrymple2020.weakReciprocity_dep_of_reciprocityCond {E : Type u_1} {u : ℕ} {S : PluralAssign ℕ E} {u' : ℕ} {X : Finset E} (hdef : ∀ s ∈ S, s u ≠ ⊥ ↔ s u' ≠ ⊥) (hX : PCDRT.value u' S = ↑X) (h : PPCDRT.reciprocityCond u u' S ∅) : Reciprocal.WeakReciprocity (fun (a b : E) => (a, b) ∈ PCDRT.dep u' u S) X

By §2.4, §4.5, whatever the verb, the dependency between the antecedent and a reciprocal without distribution is weakly reciprocal on the antecedent's plurality. The forks of (92), whose verb takes ∪u₂ collectively, are "a special case of weak reciprocity" in this sense.

Reciprocal scope (§3)

def HaugDalrymple2020.girlsNarrow : List (PartialAssign ℕ Ind)

Each girl thought "we will win", ∪u₂ → ∪u₁ under δ_w (49).

Equations

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

def HaugDalrymple2020.girlsWide : List (PartialAssign ℕ Ind)

Each girl thought "I will win", u₂ → u₁ (51).

Equations

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

theorem HaugDalrymple2020.win_readings : (PPCDRT.groupIdentityCond u₂ u₁ (ofRows girlsNarrow) {u₁, w} ∧ ¬PPCDRT.bindingCond u₂ u₁ (ofRows girlsNarrow) {u₁, w}) ∧ PPCDRT.bindingCond u₂ u₁ (ofRows girlsWide) {u₁, w} ∧ ¬PPCDRT.groupIdentityCond u₂ u₁ (ofRows girlsWide) {u₁, w}

By §3.1, the two readings of (44) come apart under the distribution the attitude verb induces, (49) being group identity without binding and (51) binding without group identity.

def HaugDalrymple2020.sawNarrow : List (PartialAssign ℕ Ind)

Each girl thought "we saw each other", the reciprocal inside the belief (53).

Equations

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

def HaugDalrymple2020.sawWide : List (PartialAssign ℕ Ind)

Each girl thought "I saw her", the reciprocal and its antecedent lifted to the matrix DRS (55).

Equations

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

def HaugDalrymple2020.sawCrossed : List (PartialAssign ℕ Ind)

In the crossed reading of (56), girl1 thought girl2 saw girl1 and girl2 thought girl1 saw girl2.

Equations

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

theorem HaugDalrymple2020.saw_narrow : PPCDRT.groupIdentityCond u₂ u₁ (ofRows sawNarrow) {u₁, w} ∧ PPCDRT.reciprocityCond u₃ u₂ (ofRows sawNarrow) {u₁, w}

By §3.2, (53) satisfies (52), group identity of the pronoun and reciprocity of the reciprocal under the distribution.

theorem HaugDalrymple2020.saw_wide : PPCDRT.bindingCond u₂ u₁ (ofRows sawWide) ∅ ∧ PPCDRT.reciprocityCond u₃ u₂ (ofRows sawWide) ∅

By §3.2, (55) satisfies (54), binding of the pronoun and reciprocity in the matrix.

theorem HaugDalrymple2020.saw_crossed : PPCDRT.groupIdentityCond u₂ u₁ (ofRows sawCrossed) ∅ ∧ PPCDRT.reciprocityCond u₃ u₂ (ofRows sawCrossed) ∅ ∧ ¬PPCDRT.bindingCond u₂ u₁ (ofRows sawCrossed) ∅

By §3.3, the crossed state satisfies (56), group identity of the pronoun with reciprocity in the matrix, but not the binding of (54).

theorem HaugDalrymple2020.no_low_reciprocal_under_binding {E : Type u_1} {S : PluralAssign ℕ E} {Δ : Set ℕ} {v₁ v₂ v₃ : ℕ} (hΔ : v₁ ∈ Δ) (hb : PPCDRT.bindingCond v₂ v₁ S Δ) (hr : PPCDRT.reciprocityCond v₃ v₂ S Δ) {s : PartialAssign ℕ E} (hs : s ∈ S) {d : E} (hd : s v₂ = ↑d) : False

By §3.3, a bound antecedent cannot cooccur with a low reciprocal. If u₂ is bound by u₁, the distribution runs over u₁, and the reciprocal u₃ is reciprocal to u₂ under that distribution, no state can assign u₂ a value, since the value must be covered by u₃ within the class, where distinctness excludes it.

def HaugDalrymple2020.beatModal : List (PartialAssign ℕ Ind)

Example (69) distributed over two accessible worlds, with the reciprocal lifted above ◇.

Equations

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

theorem HaugDalrymple2020.beat_modal : PPCDRT.reciprocityCond u₂ u₁ (ofRows beatModal) ∅ ∧ ∀ s ∈ beatModal, (Ind.tracy, Ind.chris) ∈ PCDRT.dep u₁ u₂ (PPCDRT.eqClass (ofRows beatModal) {w} s) ∧ (Ind.chris, Ind.tracy) ∈ PCDRT.dep u₁ u₂ (PPCDRT.eqClass (ofRows beatModal) {w} s)

By §3.4, with the reciprocal above the modal, every accessible world contains both directions of beat, the contradiction that makes (64) strange.

Underspecification, multiple reciprocals, subgroups, collectives (§4)

def HaugDalrymple2020.scratchMixed : List (PartialAssign ℕ Ind)

The mixed construal of the Cheyenne affix (78c) has one child scratching herself and two scratching each other.

Equations

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

theorem HaugDalrymple2020.scratch_mixed : PPCDRT.underspecifiedCond u₂ u₁ (ofRows scratchMixed) ∅ ∧ ¬PPCDRT.reciprocityCond u₂ u₁ (ofRows scratchMixed) ∅ ∧ ¬PPCDRT.bindingCond u₂ u₁ (ofRows scratchMixed) ∅

By §4.2, the mixed construal satisfies the underspecified meaning (79b) but neither reciprocity nor reflexive binding.

def HaugDalrymple2020.picturesSecond : List (PartialAssign ℕ Ind)

Each girl gave the other a picture of herself, the second reciprocal anteceded by the first (85c).

Equations

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

def HaugDalrymple2020.picturesSubject : List (PartialAssign ℕ Ind)

Each girl gave the other a picture of the other, both reciprocals anteceded by the subject (86c).

Equations

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

theorem HaugDalrymple2020.pictures_readings : (PPCDRT.reciprocityCond u₂ u₁ (ofRows picturesSecond) ∅ ∧ PPCDRT.reciprocityCond u₄ u₂ (ofRows picturesSecond) ∅ ∧ ¬PPCDRT.reciprocityCond u₄ u₁ (ofRows picturesSecond) ∅) ∧ PPCDRT.reciprocityCond u₂ u₁ (ofRows picturesSubject) ∅ ∧ PPCDRT.reciprocityCond u₄ u₁ (ofRows picturesSubject) ∅ ∧ ¬PPCDRT.reciprocityCond u₄ u₂ (ofRows picturesSubject) ∅

By §4.4, the two readings of (84) are the two antecedents of the second reciprocal; each state satisfies its own DRS and fails the other's distinctness condition.

def HaugDalrymple2020.forks : List (PartialAssign ℕ Ind)

The forks propped against each other, each on one other (93).

Equations

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

def HaugDalrymple2020.threeForks : Finset Ind

The three forks.

Equations

• HaugDalrymple2020.threeForks = {HaugDalrymple2020.Ind.fork1, HaugDalrymple2020.Ind.fork2, HaugDalrymple2020.Ind.fork3}

theorem HaugDalrymple2020.forks_weak : PPCDRT.reciprocityCond u₂ u₁ (ofRows forks) ∅ ∧ Reciprocal.WeakReciprocity (fun (a b : Ind) => (a, b) ∈ PCDRT.dep u₁ u₂ (ofRows forks)) threeForks ∧ ¬Reciprocal.StrongReciprocity (fun (a b : Ind) => (a, b) ∈ PCDRT.dep u₁ u₂ (ofRows forks)) threeForks

By §4.5, the forks reading is a special case of weak reciprocity. The minimal state (93) is reciprocal, and its dependency is weakly but not strongly reciprocal on the three forks, since each fork is propped against another, not against every other.

def HaugDalrymple2020.sailors : List (PartialAssign ℕ Ind)

The sailors worked together on each other's ships (96c).

Equations

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

theorem HaugDalrymple2020.sailors_collective : PPCDRT.reciprocityCond u₃ u₁ (ofRows sailors) ∅ ∧ atomsCond 3 u₁ (ofRows sailors) ∅

By §4.6, the collective antecedent ∪u₁ of work.together is the group of all three sailors while the reciprocal holds pointwise; the distinctness does no work.

Quantified antecedents (§5)

def HaugDalrymple2020.IsRefSet {D : Type u_1} (R : D → D → Prop) (A Y : Finset D) : Prop

A reference set (101) is a subset of the restrictor A over which R is strongly reciprocal (fn. 24), of the largest cardinality any such subset has, as the operator of (97) maximizes. Maxima need not be unique (fn. 18).

Equations

• HaugDalrymple2020.IsRefSet R A Y = (Y ∈ A.powerset ∧ Reciprocal.StrongReciprocity R Y ∧ ∀ Z ∈ A.powerset, Reciprocal.StrongReciprocity R Z → Z.card ≤ Y.card)

def HaugDalrymple2020.RefSetReading {D : Type u_1} (Q : Finset D → Finset D → Prop) (R : D → D → Prop) (A : Finset D) : Prop

In the reference-set reading, (101) and (110a), the determiner holds of the restrictor and a reference set.

Equations

• HaugDalrymple2020.RefSetReading Q R A = ∃ Y ∈ A.powerset, HaugDalrymple2020.IsRefSet R A Y ∧ Q A Y

def HaugDalrymple2020.participants {D : Type u_1} [DecidableEq D] (R : D → D → Prop) [DecidableRel R] (A : Finset D) : Finset D

The participants (105) are the members of A bearing R to some other member.

Equations

• HaugDalrymple2020.participants R A = {a ∈ A | ∃ b ∈ A, b ≠ a ∧ R a b}

def HaugDalrymple2020.MaxSetReading {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) : Prop

In the maximal-set reading, (104) and (110b), the reciprocal ranges over the whole restrictor and the determiner holds of the restrictor and the participants.

Equations

• HaugDalrymple2020.MaxSetReading Q R A = Q A (HaugDalrymple2020.participants R A)

inductive HaugDalrymple2020.Range : Type

The two ranges of the reciprocal in (99).

• referenceSet : Range
• maximalSet : Range

@[instance_reducible]

instance HaugDalrymple2020.instDecidableEqRange : DecidableEq Range

Equations

• HaugDalrymple2020.instDecidableEqRange x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HaugDalrymple2020.instFintypeRange : Fintype Range

Equations

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

def HaugDalrymple2020.instReprRange.repr : Range → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HaugDalrymple2020.instReprRange : Repr Range

Equations

• HaugDalrymple2020.instReprRange = { reprPrec := HaugDalrymple2020.instReprRange.repr }

def HaugDalrymple2020.reading {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) : Range → Prop

The reading of a quantified reciprocal sentence at a range.

Equations

• HaugDalrymple2020.reading Q R A HaugDalrymple2020.Range.referenceSet = HaugDalrymple2020.RefSetReading Q R A
• HaugDalrymple2020.reading Q R A HaugDalrymple2020.Range.maximalSet = HaugDalrymple2020.MaxSetReading Q R A

theorem HaugDalrymple2020.refSet_subset_participants {D : Type u_1} [DecidableEq D] (R : D → D → Prop) [DecidableRel R] (A : Finset D) {Y : Finset D} (h : IsRefSet R A Y) : Y ⊆ participants R A

Each member of a reference set participates.

theorem HaugDalrymple2020.maxSetReading_of_refSetReading {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) (hQ : Monotone (Q A)) (h : RefSetReading Q R A) : MaxSetReading Q R A

By §5.2, for a determiner upward monotone in its scope, the reciprocal relation holds over the maximal set if it holds over a reference set, so the reference-set reading determines truth and the maximal-set reading falsity.

@[instance_reducible]

instance HaugDalrymple2020.instDecidablePredRangeReading {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] : DecidablePred (reading Q R A)

Equations

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

def HaugDalrymple2020.truthValue {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] : SignType

A quantified reciprocal sentence is true iff true at both ranges, false iff false at both, and neither otherwise, the supervaluation over the two precisifications (109).

Equations

• HaugDalrymple2020.truthValue Q R A = SignType.supervaluation {HaugDalrymple2020.Range.referenceSet, HaugDalrymple2020.Range.maximalSet} (HaugDalrymple2020.reading Q R A)

theorem HaugDalrymple2020.truthValue_true_iff {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] : truthValue Q R A = 1 ↔ RefSetReading Q R A ∧ MaxSetReading Q R A

theorem HaugDalrymple2020.truthValue_false_iff {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] : truthValue Q R A = -1 ↔ ¬RefSetReading Q R A ∧ ¬MaxSetReading Q R A

theorem HaugDalrymple2020.truthValue_true_iff_of_monotone {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] (hQ : Monotone (Q A)) : truthValue Q R A = 1 ↔ RefSetReading Q R A

theorem HaugDalrymple2020.truthValue_false_iff_of_monotone {D : Type u_1} [DecidableEq D] (Q : Finset D → Finset D → Prop) (R : D → D → Prop) [DecidableRel R] (A : Finset D) [DecidableRel Q] (hQ : Monotone (Q A)) : truthValue Q R A = -1 ↔ ¬MaxSetReading Q R A

@[reducible, inline]

abbrev HaugDalrymple2020.Person : Type

The five inhabitants of the street of (100) and (102).

Equations

• HaugDalrymple2020.Person = Fin 5

def HaugDalrymple2020.most (A B : Finset Person) : Prop

Proportional most holds when the scope has more than half of the restrictor.

Equations

• HaugDalrymple2020.most A B = (A.card < 2 * B.card)

def HaugDalrymple2020.few (A B : Finset Person) : Prop

Proportional few holds when the scope has less than half of the restrictor.

Equations

• HaugDalrymple2020.few A B = (2 * B.card < A.card)

def HaugDalrymple2020.clique (a b : Person) : Prop

The first three inhabitants know each other and the other two know nobody (102).

Equations

• HaugDalrymple2020.clique a b = (a ≠ b ∧ ↑a < 3 ∧ ↑b < 3)

def HaugDalrymple2020.pairs (a b : Person) : Prop

The intermediate scenario of §5.2, in which two pairs know each other and one person knows nobody.

Equations

• HaugDalrymple2020.pairs a b = (a ≠ b ∧ (↑a < 2 ∧ ↑b < 2 ∨ 2 ≤ ↑a ∧ ↑a < 4 ∧ 2 ≤ ↑b ∧ ↑b < 4))

@[instance_reducible]

instance HaugDalrymple2020.instDecidableRelPersonClique : DecidableRel clique

Equations

• HaugDalrymple2020.instDecidableRelPersonClique x✝¹ x✝ = { decide := decide (x✝¹ ≠ x✝) && decide (↑x✝¹ < 3 ∧ ↑x✝ < 3), reflects_decide := ⋯ }

@[instance_reducible]

instance HaugDalrymple2020.instDecidableRelPersonPairs : DecidableRel pairs

Equations

• HaugDalrymple2020.instDecidableRelPersonPairs x✝¹ x✝ = { decide := decide (x✝¹ ≠ x✝) && decide (↑x✝¹ < 2 ∧ ↑x✝ < 2 ∨ 2 ≤ ↑x✝¹ ∧ ↑x✝¹ < 4 ∧ 2 ≤ ↑x✝ ∧ ↑x✝ < 4), reflects_decide := ⋯ }

@[instance_reducible]

instance HaugDalrymple2020.instDecidableRelFinsetPersonMost : DecidableRel most

Equations

• HaugDalrymple2020.instDecidableRelFinsetPersonMost x✝¹ x✝ = { decide := x✝¹.card.succ.ble (2 * x✝.card), reflects_decide := ⋯ }

@[instance_reducible]

instance HaugDalrymple2020.instDecidableRelFinsetPersonFew : DecidableRel few

Equations

• HaugDalrymple2020.instDecidableRelFinsetPersonFew x✝¹ x✝ = { decide := (2 * x✝.card).succ.ble x✝¹.card, reflects_decide := ⋯ }

theorem HaugDalrymple2020.street_scenarios : truthValue most clique Finset.univ = 1 ∧ truthValue few clique Finset.univ = -1 ∧ truthValue most pairs Finset.univ = 0 ∧ truthValue few pairs Finset.univ = 0

By (110) and (111), "most people know each other" is true and "few know each other" false in the clique scenario of (102), and both are neither in the scenario of two pairs, which Kamp and Reyle judged arguably true.

Maximize Anaphora (§6)

def HaugDalrymple2020.MaximizesAnaphora {E : Type u_1} (K : PluralAssign ℕ E → Prop) (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) : Prop

A state maximizes anaphora (128) when, among the states a DRS K admits, its set R_u of pairs (127), the dependency between antecedent and anaphor, is not properly included in another admitted state's.

Equations

• HaugDalrymple2020.MaximizesAnaphora K uAnaph uAnt S = (K S ∧ ∀ (S' : PluralAssign ℕ E), K S' → ¬PCDRT.dep uAnt uAnaph S ⊂ PCDRT.dep uAnt uAnaph S')

theorem HaugDalrymple2020.dep_subset_of_reciprocalDRS {E : Type u_1} {P : E → E → Prop} {u u' : ℕ} {S : PluralAssign ℕ E} {X : Set E} (hS : ReciprocalDRS P X u u' S) : PCDRT.dep u' u S ⊆ {p : E × E | p.1 ∈ X ∧ p.2 ∈ X ∧ P p.1 p.2 ∧ p.1 ≠ p.2}

A reciprocal DRS realizes only pairs of distinct members of X that P relates.

theorem HaugDalrymple2020.maximizesAnaphora_iff {E : Type u_1} {P : E → E → Prop} {u u' : ℕ} {S : PluralAssign ℕ E} (h : u ≠ u') {X : Set E} : MaximizesAnaphora (ReciprocalDRS P X u u') u u' S ↔ ReciprocalDRS P X u u' S ∧ PCDRT.dep u' u S = {p : E × E | p.1 ∈ X ∧ p.2 ∈ X ∧ P p.1 p.2 ∧ p.1 ≠ p.2}

Maximize Anaphora (§6, (128)) selects exactly the states of a reciprocal DRS whose dependency is every pair of distinct members of X that P relates.

theorem HaugDalrymple2020.strongReciprocity_dep_iff {E : Type u_1} {P : E → E → Prop} {u u' : ℕ} {S : PluralAssign ℕ E} (h : u ≠ u') {X : Finset E} (hS : MaximizesAnaphora (ReciprocalDRS P (↑X) u u') u u' S) : Reciprocal.StrongReciprocity (fun (a b : E) => (a, b) ∈ PCDRT.dep u' u S) X ↔ Reciprocal.StrongReciprocity P X

By §6, full maximization yields Strong Reciprocity. Under Maximize Anaphora the dependency makes X strongly reciprocal exactly when P relates any two distinct members of X.

def HaugDalrymple2020.boys : Finset Ind

The three boys of (125).

Equations

• HaugDalrymple2020.boys = {HaugDalrymple2020.Ind.boy1, HaugDalrymple2020.Ind.boy2, HaugDalrymple2020.Ind.boy3}

@[reducible, inline]

abbrev HaugDalrymple2020.boysKnow : PluralAssign ℕ Ind → Prop

For the three boys, (125b) makes u₂ reciprocal to u₁, whose values are the boys, with nothing known against any two of them knowing each other.

Equations

• HaugDalrymple2020.boysKnow = HaugDalrymple2020.ReciprocalDRS (fun (x x_1 : HaugDalrymple2020.Ind) => True) (↑HaugDalrymple2020.boys) HaugDalrymple2020.u₂ HaugDalrymple2020.u₁

def HaugDalrymple2020.boysMinimal : List (PartialAssign ℕ Ind)

A minimal state for (125), (126a).

Equations

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

def HaugDalrymple2020.boysStrong : List (PartialAssign ℕ Ind)

The strong reciprocal reading (126b).

Equations

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

theorem HaugDalrymple2020.maximize_strong : boysKnow (ofRows boysMinimal) ∧ ¬MaximizesAnaphora boysKnow u₂ u₁ (ofRows boysMinimal) ∧ MaximizesAnaphora boysKnow u₂ u₁ (ofRows boysStrong) ∧ Reciprocal.StrongReciprocity (fun (a b : Ind) => (a, b) ∈ PCDRT.dep u₁ u₂ (ofRows boysStrong)) boys

By §6, the minimal state (126a) verifies (125), but Maximize Anaphora rejects it and selects (126b), whose dependency is the strong reciprocal reading.

def HaugDalrymple2020.classmates : List (PartialAssign ℕ Ind)

By §6.2, the classmates gave each other pictures of each other, each maximizing pairwise, so that each gave a picture of herself to each of the others.

Equations

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

def HaugDalrymple2020.trio : Finset Ind

The three classmates.

Equations

• HaugDalrymple2020.trio = {HaugDalrymple2020.Ind.tracy, HaugDalrymple2020.Ind.chris, HaugDalrymple2020.Ind.matty}

theorem HaugDalrymple2020.classmates_pairwise : Reciprocal.StrongReciprocity (fun (a b : Ind) => (a, b) ∈ PCDRT.dep u₁ u₂ (ofRows classmates)) trio ∧ Reciprocal.StrongReciprocity (fun (a b : Ind) => (a, b) ∈ PCDRT.dep u₂ u₄ (ofRows classmates)) trio ∧ ¬∃ s ∈ classmates, s u₁ = ↑Ind.tracy ∧ s u₂ = ↑Ind.chris ∧ s u₄ = ↑Ind.matty

By §6.2, both reciprocal relations of (134) are maximal, strongly reciprocal on the classmates, without any all-triples row, in which a classmate gives a picture of a third classmate.

def HaugDalrymple2020.praisedWide : List (PartialAssign ℕ Ind)

In the wide construal of (135), each of Tracy, Matty and Chris believes that she praised the two others (136).

Equations

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

theorem HaugDalrymple2020.praised_wide : PPCDRT.bindingCond u₂ u₁ (ofRows praisedWide) ∅ ∧ PPCDRT.reciprocityCond u₃ u₂ (ofRows praisedWide) ∅ ∧ ∀ s ∈ praisedWide, ∀ (d : Ind), d ∈ sumRows praisedWide [w] s u₃ ↔ d ∈ trio ∧ ↑d ≠ s u₁

By §6.3, (136) is the wide reading, binding of the pronoun with reciprocity in the matrix, and within each girl's world the reciprocal covers exactly the two others.