Dalrymple, Kanazawa, Kim, Mchombo and Peters (1998): Reciprocal Expressions and the Concept of Reciprocity

The reciprocal has one meaning that varies with context. It ranges over six quantifiers, the settings of two parameters (Reciprocal.Recip), which are genuinely polyadic: an iteration of two type ⟨1,1⟩ quantifiers whose inner one is permutation invariant cannot tell a cycle of six from two cycles of three, so it is not Intermediate Reciprocity (intermediateReciprocity_not_iterateOthers). By the Strongest Meaning Hypothesis a reciprocal sentence is felicitous in a context when, among its interpretations consistent with the non-linguistic information, one entails all the others, and the sentence then expresses that one. Since the quantifiers are ordered by entailment as the product of the parameters, the hypothesis selects the strongest setting consistent with the context (isLeast_of_isGreatest), Strong Reciprocity whenever that is consistent (isLeast_strong). For gave each other measles, asymmetry, acyclicity and catching measles once leave Intermediate Alternative Reciprocity (measles_isLeast). The paper's two admitted failures follow as well. With two members and an asymmetric relation the hypothesis makes the sentence felicitous whether the paper marks it acceptable or not (smh_mispredicts_taller). For the staring pirates it predicts Intermediate Reciprocity (pirates_isLeast), which a single-valued relation satisfies only without eye contact, while the sentence allows eye contact (pirates_eyeContact).

Implementation notes

A situation is an extension of the scope relation over a fixed antecedent set, so an interpretation is the set of relations satisfying a quantifier, the non-linguistic information is a set of relations, and entailment is inclusion. Each context is stated by the properties of the relation the paper appeals to. The quantified antecedents of §7 are not formalized.

References

• [DKK+98]

The six quantifiers (§5)

theorem DalrympleEtAl1998.recip_alternative_iff {A : Type u_1} {R : A → A → Prop} {X : Finset A} [Std.Symm R] (c : Reciprocal.Coverage) : Reciprocal.Recip (c, Reciprocal.Direction.alternative) R X ↔ Reciprocal.Recip (c, Reciprocal.Direction.plain) R X

For a symmetric scope relation the direction parameter makes no difference, so the six quantifiers reduce to three (§5.4).

Intermediate Reciprocity is not an iteration (footnote 8)

On a symmetric relation, the reading obtained by iterating two type ⟨1,1⟩ quantifiers, Q₁ members of the antecedent bearing R to Q₂ of the other members, cannot be Intermediate Reciprocity once Q₂ is permutation invariant. A cycle of six individuals and two cycles of three give every individual two neighbours, so the iteration cannot tell them apart, while only the cycle of six is connected.

def DalrympleEtAl1998.iterateOthers {A : Type u_1} (Q₁ Q₂ : Quantifier.GQ A) (P : A → Prop) (R : A → A → Prop) : Prop

The iteration (i) of footnote 8, in which Q₁ members of P bear R to Q₂ of the other members of P.

Equations

• DalrympleEtAl1998.iterateOthers Q₁ Q₂ P R = Q₁ P fun (x : A) => Q₂ (fun (y : A) => P y ∧ x ≠ y) (R x)

theorem DalrympleEtAl1998.intermediate_of_succ {n : ℕ} [NeZero n] (hn : 2 ≤ n) {R : Fin n → Fin n → Prop} (hR : ∀ (x : Fin n), R x (x + 1)) : Reciprocal.IntermediateReciprocity R Finset.univ

A relation containing the successor step joins any two elements of Fin n.

def DalrympleEtAl1998.hexagon (x y : Fin 6) : Prop

Six individuals in a cycle, each beside two neighbours, the model (ii).

Equations

• DalrympleEtAl1998.hexagon x y = (y = x + 1 ∨ x = y + 1)

def DalrympleEtAl1998.twoTriangles (x y : Fin 6) : Prop

Six individuals in two cycles of three, the model (iii).

Equations

• DalrympleEtAl1998.twoTriangles x y = (x ≠ y ∧ ↑x / 3 = ↑y / 3)

@[instance_reducible]

instance DalrympleEtAl1998.instDecidableRelFinOfNatNatHexagon : DecidableRel hexagon

Equations

• DalrympleEtAl1998.instDecidableRelFinOfNatNatHexagon x✝¹ x✝ = { decide := decide (x✝ = x✝¹ + 1) || decide (x✝¹ = x✝ + 1), reflects_decide := ⋯ }

@[instance_reducible]

instance DalrympleEtAl1998.instDecidableRelFinOfNatNatTwoTriangles : DecidableRel twoTriangles

Equations

• DalrympleEtAl1998.instDecidableRelFinOfNatNatTwoTriangles x✝¹ x✝ = { decide := decide (x✝¹ ≠ x✝) && decide (↑x✝¹ / 3 = ↑x✝ / 3), reflects_decide := ⋯ }

theorem DalrympleEtAl1998.intermediate_hexagon : Reciprocal.IntermediateReciprocity hexagon Finset.univ

theorem DalrympleEtAl1998.not_intermediate_twoTriangles : ¬Reciprocal.IntermediateReciprocity twoTriangles Finset.univ

theorem DalrympleEtAl1998.iterateOthers_hexagon_iff (Q₁ Q₂ : Quantifier.GQ (Fin 6)) (hQ₂ : Q₂.QuantityInvariant) : iterateOthers Q₁ Q₂ (fun (x : Fin 6) => True) hexagon ↔ iterateOthers Q₁ Q₂ (fun (x : Fin 6) => True) twoTriangles

With a permutation-invariant inner quantifier the iteration has the same value on both models, since a bijection fixing each individual carries its neighbours in the cycle of six to its neighbours in its cycle of three.

theorem DalrympleEtAl1998.intermediateReciprocity_not_iterateOthers (Q₁ Q₂ : Quantifier.GQ (Fin 6)) (hQ₂ : Q₂.QuantityInvariant) : ¬∀ (R : Fin 6 → Fin 6 → Prop), Std.Symm R → (iterateOthers Q₁ Q₂ (fun (x : Fin 6) => True) R ↔ Reciprocal.IntermediateReciprocity R Finset.univ)

No iteration with a permutation-invariant inner quantifier is Intermediate Reciprocity on every symmetric relation (footnote 8). The paper assumes both quantifiers permutation invariant; the outer one needs no assumption.

The Strongest Meaning Hypothesis (§6.2)

def DalrympleEtAl1998.interpretation {A : Type u_1} (X : Finset A) (q : Reciprocal.Coverage × Reciprocal.Direction) : Set (A → A → Prop)

The interpretation of the Xs R each other with the reciprocal read at setting q is the set of extensions of the scope relation that make the sentence true.

Equations

• DalrympleEtAl1998.interpretation X q = {R : A → A → Prop | Reciprocal.Recip q R X}

def DalrympleEtAl1998.candidates {A : Type u_1} (X : Finset A) (I : Set (A → A → Prop)) : Set (Set (A → A → Prop))

The interpretations consistent with the non-linguistic information I. By the Strongest Meaning Hypothesis the sentence is felicitous in I when this set has a least element, and it then expresses that one.

Equations

• DalrympleEtAl1998.candidates X I = {p : Set (A → A → Prop) | ∃ (q : Reciprocal.Coverage × Reciprocal.Direction), DalrympleEtAl1998.interpretation X q = p ∧ (p ∩ I).Nonempty}

theorem DalrympleEtAl1998.interpretation_antitone {A : Type u_1} {X : Finset A} : Antitone (interpretation X)

theorem DalrympleEtAl1998.nonempty_inter_of_le {A : Type u_1} {X : Finset A} {I : Set (A → A → Prop)} {q q' : Reciprocal.Coverage × Reciprocal.Direction} (hq : q ≤ q') (h : (interpretation X q' ∩ I).Nonempty) : (interpretation X q ∩ I).Nonempty

theorem DalrympleEtAl1998.isLeast_of_isGreatest {A : Type u_1} {X : Finset A} {I : Set (A → A → Prop)} {q : Reciprocal.Coverage × Reciprocal.Direction} (h : IsGreatest {q : Reciprocal.Coverage × Reciprocal.Direction | (interpretation X q ∩ I).Nonempty} q) : IsLeast (candidates X I) (interpretation X q)

The hypothesis expresses the interpretation at the strongest setting consistent with the context.

theorem DalrympleEtAl1998.isLeast_strong {A : Type u_1} {X : Finset A} {I : Set (A → A → Prop)} (h : ∃ R ∈ I, Reciprocal.StrongReciprocity R X) : IsLeast (candidates X I) (interpretation X (Reciprocal.Coverage.ful, Reciprocal.Direction.plain))

Whenever Strong Reciprocity is consistent with the context, the sentence expresses it, as the legislators' sentence (95) does.

Measles (§6.1)

theorem DalrympleEtAl1998.exists_transGen_of_oneWayWeak {A : Type u_1} {R : A → A → Prop} {X : Finset A} (h : Reciprocal.OneWayWeakReciprocity R X) : ∃ (x : A), Relation.TransGen R x x

One-way Weak Reciprocity over finitely many members needs a cycle. If each third grader gave another one measles, some of them passed it around in a circle (99).

def DalrympleEtAl1998.measles {A : Type u_1} : Set (A → A → Prop)

In the non-linguistic information for gave each other measles, a person catches measles from at most one person, and measles is not passed around in a circle.

Equations

• DalrympleEtAl1998.measles = {R : A → A → Prop | (∀ (x x' y : A), R x y → R x' y → x = x') ∧ ∀ (x : A), ¬Relation.TransGen R x x}

theorem DalrympleEtAl1998.not_oneWayWeak_of_measles {A : Type u_1} {R : A → A → Prop} {X : Finset A} (hR : R ∈ measles) : ¬Reciprocal.OneWayWeakReciprocity R X

theorem DalrympleEtAl1998.not_strongAlternative_of_measles {A : Type u_1} {R : A → A → Prop} {X : Finset A} (hR : R ∈ measles) (hX : 3 ≤ X.card) : ¬Reciprocal.Recip (Reciprocal.Coverage.ful, Reciprocal.Direction.alternative) R X

With three or more students, Strong Alternative Reciprocity is false of measles, since the last to catch it would have caught it from each of the others.

theorem DalrympleEtAl1998.exists_intermediateAlternative_measles {A : Type u_1} {X : Finset A} (hX : X.Nontrivial) {s : A} (hs : s ∈ X) : ∃ R ∈ measles, Reciprocal.Recip (Reciprocal.Coverage.lin, Reciprocal.Direction.alternative) R X

One student giving measles to all the others is a measles situation in which Intermediate Alternative Reciprocity holds.

theorem DalrympleEtAl1998.measles_isLeast {A : Type u_1} {X : Finset A} (hX : 3 ≤ X.card) : IsLeast (candidates X measles) (interpretation X (Reciprocal.Coverage.lin, Reciprocal.Direction.alternative))

With three or more students, gave each other measles expresses Intermediate Alternative Reciprocity (98), since every stronger quantifier is inconsistent with the measles facts.

Two members and an asymmetric relation (§6.3)

def DalrympleEtAl1998.asymmetric {A : Type u_1} : Set (A → A → Prop)

The non-linguistic information that the relation is asymmetric, as on top of and taller than are.

Equations

• DalrympleEtAl1998.asymmetric = {R : A → A → Prop | ∀ (x y : A), R x y → ¬R y x}

theorem DalrympleEtAl1998.interpretation_pair_alternative {A : Type u_1} [DecidableEq A] {a b : A} (hab : a ≠ b) : interpretation {a, b} (Reciprocal.Coverage.tot, Reciprocal.Direction.alternative) = interpretation {a, b} (Reciprocal.Coverage.ful, Reciprocal.Direction.alternative)

On two members the three alternative quantifiers agree, each saying that one member bears the relation to the other.

theorem DalrympleEtAl1998.pair_isLeast {A : Type u_1} [DecidableEq A] {a b : A} (hab : a ≠ b) : IsLeast (candidates {a, b} asymmetric) (interpretation {a, b} (Reciprocal.Coverage.tot, Reciprocal.Direction.alternative))

With two members and an asymmetric relation, the sentence expresses that one member bears the relation to the other, Inclusive Alternative Ordering, as for the bunk beds of (108).

theorem DalrympleEtAl1998.smh_mispredicts_taller {A : Type u_1} [DecidableEq A] {a b : A} (hab : a ≠ b) : (∃ (p : Set (A → A → Prop)), IsLeast (candidates {a, b} asymmetric) p) ∧ Examples.ex108.judgment = Judgment.acceptable ∧ Examples.ex109.judgment = Judgment.unacceptable

The hypothesis cannot tell (108) from (109). With two members and an asymmetric relation it makes both felicitous, but the paper marks (109) infelicitous.

The staring pirates (§6.3)

def DalrympleEtAl1998.singleValued {A : Type u_1} : Set (A → A → Prop)

In the non-linguistic information for staring at each other, each stares at only one other.

Equations

• DalrympleEtAl1998.singleValued = {R : A → A → Prop | ∀ (x y y' : A), R x y → R x y' → y = y'}

theorem DalrympleEtAl1998.card_le_three_of_singleValued {A : Type u_1} {R : A → A → Prop} {X : Finset A} (hR : R ∈ singleValued) (h : Reciprocal.Recip (Reciprocal.Coverage.ful, Reciprocal.Direction.alternative) R X) : X.card ≤ 3

A single-valued relation is strongly alternative-reciprocal on at most three members, since each pair of members needs an arrow of its own.

theorem DalrympleEtAl1998.not_mutual_of_intermediate {A : Type u_1} {R : A → A → Prop} {X : Finset A} (hR : R ∈ singleValued) (h : Reciprocal.IntermediateReciprocity R X) (hX : 3 ≤ X.card) {a b : A} (ha : a ∈ X) (hab : R a b) (hba : R b a) : False

With a single-valued relation, Intermediate Reciprocity over three or more members leaves no two members bearing the relation to each other. A pirate who stares back at one staring at him leaves some pirate out of the loop.

def DalrympleEtAl1998.stareRound (x y : Fin 4) : Prop

Four pirates, each staring at the next around a circle.

Equations

• DalrympleEtAl1998.stareRound x y = (y = x + 1)

def DalrympleEtAl1998.stareBack (x y : Fin 4) : Prop

Four pirates in two pairs, each staring at the other of the pair.

Equations

• DalrympleEtAl1998.stareBack x y = (x ≠ y ∧ ↑x / 2 = ↑y / 2)

@[instance_reducible]

instance DalrympleEtAl1998.instDecidableRelFinOfNatNatStareBack : DecidableRel stareBack

Equations

• DalrympleEtAl1998.instDecidableRelFinOfNatNatStareBack x✝¹ x✝ = { decide := decide (x✝¹ ≠ x✝) && decide (↑x✝¹ / 2 = ↑x✝ / 2), reflects_decide := ⋯ }

theorem DalrympleEtAl1998.stareRound_intermediate : Reciprocal.IntermediateReciprocity stareRound Finset.univ

theorem DalrympleEtAl1998.pirates_isLeast : IsLeast (candidates Finset.univ singleValued) (interpretation Finset.univ (Reciprocal.Coverage.lin, Reciprocal.Direction.plain))

With four pirates, the fewest for which the paper's argument excludes both quantifiers built on FUL, staring at each other expresses Intermediate Reciprocity (110).

theorem DalrympleEtAl1998.pirates_eyeContact : stareBack ∈ singleValued ∧ Reciprocal.OneWayWeakReciprocity stareBack Finset.univ ∧ stareBack ∉ interpretation Finset.univ (Reciprocal.Coverage.lin, Reciprocal.Direction.plain)

The predicted meaning is too strong. When the four pirates stare at each other in two pairs, every pirate is in eye contact and One-way Weak Reciprocity holds, the meaning the paper gives (110), but Intermediate Reciprocity fails.