Winter (2018): Symmetric Predicates and the Semantics of Reciprocal Alternations

This file formalizes [Win18]'s account of reciprocal alternations, which pair a unary collective predicate with a binary one. An alternation is plain when the collective holds of a sum of two entities exactly if the binary predicate holds between them in both directions (7) (PlainReciprocity), and the Reciprocity-Symmetry Generalization says that an alternation is plain if and only if the binary predicate is truth-conditionally symmetric (18) (RSG). The generalization is not a matter of logic, since a one-way binary predicate paired with an empty collective is vacuously plain (exists_plainReciprocity_not_symm); it follows from taking the collective meaning as basic and the binary predicate as its symmetric image (22), which is symmetric and plain by the commutativity of sum formation (rsg_symmetricImage). Non-symmetric predicates like hug show weaker patterns (Pr1, Pr2, Pr4), of which only the disjunctive entailment from the collective to one direction of the binary predicate is shared by all alternations (Pr5); plain reciprocity is exactly the conjunction of the first two (plainReciprocity_iff_pr1_pr2). The event-based rule of [Dim08] (42), which derives the collective from two specifying sub-events, leaves the two unidirectional hugs of (38) without a common event (exists_dimitriadis_not_pr1). The paper's own account of the non-plain cases is preferential: the typicality of an event as a collective one grows with the number of directed pairs the binary predicate relates in it (58) (typ), so that more directed relations only raise it (typ_mono), a positive threshold yields the disjunctive entailment (Pr5_of_preferential), and the threshold of two yields plain reciprocity on a pair (two_le_typ_pair_iff).

Implementation notes

Sums of two distinct entities are pair finsets, and the typicality of (58) is the count of directed pairs rather than a value proportional to it. Table 3's per-verb patterns are judgments about lexical items and are recorded in the paper's examples rather than as a table; the counting of events and the comparison with [Sil12]'s derivation of reciprocals from transitives are not formalized.

References

• [Win18]
• [Dim08]
• [Sil12]

Plain reciprocity and symmetry

def Winter2018.PlainReciprocity {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

Plain reciprocity (7): for distinct entities, the collective holds of their sum exactly if the binary predicate holds between them in both directions.

Equations

• Winter2018.PlainReciprocity P R = ∀ (x y : A), x ≠ y → (P {x, y} ↔ R x y ∧ R y x)

def Winter2018.RSG {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

The Reciprocity-Symmetry Generalization (18) for one alternation: it is plain exactly if its binary predicate is truth-conditionally symmetric.

Equations

• Winter2018.RSG P R = (Winter2018.PlainReciprocity P R ↔ Std.Symm R)

def Winter2018.symmetricImage {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) : A → A → Prop

The symmetric image of a collective predicate (22): the binary predicate holding of two entities when the collective holds of their sum.

Equations

• Winter2018.symmetricImage P x y = P {x, y}

theorem Winter2018.symmetricImage_symm {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) : Std.Symm (symmetricImage P)

The symmetric image is symmetric, by the commutativity of sum formation.

theorem Winter2018.plainReciprocity_symmetricImage {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) : PlainReciprocity P (symmetricImage P)

The symmetric image is in plain reciprocity with its collective.

theorem Winter2018.rsg_symmetricImage {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) : RSG P (symmetricImage P)

A collective predicate with its symmetric image satisfies the generalization: this is how the paper derives it for plain reciprocals.

theorem Winter2018.exists_plainReciprocity_not_symm : ∃ (R : Bool → Bool → Prop) (P : Finset Bool → Prop), PlainReciprocity P R ∧ ¬Std.Symm R

The generalization is not logically forced: a one-way binary predicate paired with the empty collective is vacuously plain.

The patterns of non-plain alternations (§3.3)

def Winter2018.Pr1 {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

(Pr₁): the binary predicate in both directions yields the collective.

Equations

• Winter2018.Pr1 P R = ∀ (x y : A), x ≠ y → R x y → R y x → P {x, y}

def Winter2018.Pr2 {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

(Pr₂): the collective yields the binary predicate.

Equations

• Winter2018.Pr2 P R = ∀ (x y : A), x ≠ y → P {x, y} → R x y

def Winter2018.Pr4 {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

(Pr₄): one direction of the binary predicate yields the collective, as with break up (46).

Equations

• Winter2018.Pr4 P R = ∀ (x y : A), x ≠ y → R x y → P {x, y}

def Winter2018.Pr5 {A : Type u_1} [DecidableEq A] (P : Finset A → Prop) (R : A → A → Prop) : Prop

(Pr₅): the collective yields the binary predicate in at least one direction, the pattern every reciprocal alternation shares.

Equations

• Winter2018.Pr5 P R = ∀ (x y : A), x ≠ y → P {x, y} → R x y ∨ R y x

theorem Winter2018.Pr2.both {A : Type u_1} [DecidableEq A] {P : Finset A → Prop} {R : A → A → Prop} (h : Pr2 P R) {x y : A} (hxy : x ≠ y) (hP : P {x, y}) : R x y ∧ R y x

(Pr₂) delivers both directions, since the sum is commutative.

theorem Winter2018.Pr4.pr1 {A : Type u_1} [DecidableEq A] {P : Finset A → Prop} {R : A → A → Prop} (h : Pr4 P R) : Pr1 P R

(Pr₄) is stronger than (Pr₁).

theorem Winter2018.Pr2.pr5 {A : Type u_1} [DecidableEq A] {P : Finset A → Prop} {R : A → A → Prop} (h : Pr2 P R) : Pr5 P R

(Pr₂) is stronger than (Pr₅).

theorem Winter2018.PlainReciprocity.pr5 {A : Type u_1} [DecidableEq A] {P : Finset A → Prop} {R : A → A → Prop} (h : PlainReciprocity P R) : Pr5 P R

theorem Winter2018.plainReciprocity_iff_pr1_pr2 {A : Type u_1} [DecidableEq A] {P : Finset A → Prop} {R : A → A → Prop} : PlainReciprocity P R ↔ Pr1 P R ∧ Pr2 P R

Plain reciprocity is (Pr₁) together with (Pr₂).

Events: Dimitriadis's rule and preferential reciprocity

def Winter2018.Dimitriadis {A : Type u_1} [DecidableEq A] {E : Type u_2} (spec : E → E → Prop) (R : E → A → A → Prop) (P : E → Finset A → Prop) : Prop

[Dim08]'s rule (42): a collective event of two entities is one specified by a sub-event of the binary predicate in each direction.

Equations

• Winter2018.Dimitriadis spec R P = ∀ (e : E) (x y : A), x ≠ y → (P e {x, y} ↔ ∃ (e₁ : E) (e₂ : E), spec e₁ e ∧ spec e₂ e ∧ R e₁ x y ∧ R e₂ y x)

theorem Winter2018.exists_dimitriadis_not_pr1 : ∃ (spec : Bool → Bool → Prop) (R : Bool → Bool → Bool → Prop) (P : Bool → Finset Bool → Prop), Dimitriadis spec R P ∧ (∃ (e₁ : Bool) (e₂ : Bool), R e₁ true false ∧ R e₂ false true) ∧ ∀ (e : Bool), ¬P e {true, false}

The rule does not make (38) entail (37): with a domain of events not closed under a common specified event, the two unidirectional hugs belong to no collective hug.

def Winter2018.typ {A : Type u_1} [DecidableEq A] {E : Type u_2} (R : E → A → A → Prop) [(e : E) → DecidableRel (R e)] (e : E) (s : Finset A) : ℕ

The typicality of an event as a collective event of a group (58): the number of ordered pairs of distinct members the binary predicate relates in it.

Equations

• Winter2018.typ R e s = {p ∈ s ×ˢ s | p.1 ≠ p.2 ∧ R e p.1 p.2}.card

theorem Winter2018.typ_mono {A : Type u_1} [DecidableEq A] {E : Type u_2} (R : E → A → A → Prop) [(e : E) → DecidableRel (R e)] {R' : E → A → A → Prop} [(e : E) → DecidableRel (R' e)] {e : E} (h : ∀ (x y : A), R e x y → R' e x y) (s : Finset A) : typ R e s ≤ typ R' e s

(57): an event with more directed relations is at least as typical.

theorem Winter2018.typ_pair {A : Type u_1} [DecidableEq A] {E : Type u_2} (R : E → A → A → Prop) [(e : E) → DecidableRel (R e)] {x y : A} (hxy : x ≠ y) (e : E) : typ R e {x, y} = (if R e x y then 1 else 0) + if R e y x then 1 else 0

On a pair the typicality counts the two directions.

theorem Winter2018.Pr5_of_preferential {A : Type u_1} [DecidableEq A] {E : Type u_2} (R : E → A → A → Prop) [(e : E) → DecidableRel (R e)] {θ : ℕ} (hθ : 0 < θ) (e : E) : Pr5 (fun (s : Finset A) => θ ≤ typ R e s) (R e)

A preferential reciprocal with a positive threshold satisfies (Pr₅): the collective needs some directed relation.

theorem Winter2018.two_le_typ_pair_iff {A : Type u_1} [DecidableEq A] {E : Type u_2} (R : E → A → A → Prop) [(e : E) → DecidableRel (R e)] {x y : A} (hxy : x ≠ y) (e : E) : 2 ≤ typ R e {x, y} ↔ R e x y ∧ R e y x

The threshold of two is plain reciprocity on a pair: both directions are required.