Winter (2018): Symmetric Predicates and Reciprocal Alternations

[Win18]

Semantics & Pragmatics 11(1): 1–52.

Reciprocal alternations pair a unary-collective predicate P (Sue and Dan dated) with a binary predicate R (Sue dated Dan). Winter's Reciprocity-Symmetry Generalization (RSG, def. 18): the alternation is plain — P(x+y) ⇔ R(x,y) ∧ R(y,x) (def. 7) — iff R is truth-conditionally symmetric. The RSG is not a logical necessity (an artificial ★Xhug refutes it, fn. 12); Winter derives it lexically: symmetric predicates take the collective meaning as basic and obtain the binary form as its symmetric image R := λx λy. P(x+y) (def. 22). This reverses the derivation direction of [Dim08] and [Sil12], which map binary meanings to reciprocal ones (fn. 14) — a genuine divergence from Studies/Siloni2012.lean, where lexical reciprocal verbs are derived from transitive alternates by bundling.

Non-symmetric reciprocals (hug, fight, collide) satisfy no plain equivalence; §3.3 charts their logical patterns (Pr₁–Pr₅, Table 3), of which only the weak disjunctive Pr₅ — P(x+y) ⇒ R(x,y) ∨ R(y,x) — is shared by all reciprocal alternations. Their full semantics is preferential (typicality-based, §3.5, supported by experimental judgment data on Dutch contact and communication verbs), beyond the event-free logical core formalized here.

Sums of two distinct atoms are encoded as pair Finsets {x, y}, matching the (R, X) signature of Semantics.Plurality.Reciprocal.

Main declarations

• PlainReciprocity (def. 7), TCSymmetric, symmetricImage (def. 22)
• symmetricImage_tcSymmetric, plainReciprocity_symmetricImage — the symmetric image is symmetric and plain: principle P1, which derives the RSG for collective-basic predicates
• plainReciprocity_iff_pr1_pr2 — plain reciprocity decomposes exactly into Pr₁ ∧ Pr₂
• exists_plainReciprocity_not_tcSymmetric — plainR alone does not force symmetry (fn. 12's ★Xhug): the RSG is a lexicon fact, not logic
• AlternationProfile + table3 — Table 3's per-verb Pr-patterns, with the Pr₅ universal and the Pr₄ ⇒ Pr₁ consistency check

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

Def. (7), plain reciprocity: for distinct atoms, the collective holds of the pair-sum iff the binary holds in both directions ("A and B dated" ⇔ "A dated B and B dated A").

Equations

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

def Winter2018.TCSymmetric {A : Type u_1} (R : A → A → Prop) : Prop

Truth-conditional symmetry of a binary predicate (§2.2; Strawson effects like sister's gender presupposition are factored out).

Equations

• Winter2018.TCSymmetric R = ∀ (x y : A), R x y ↔ R y x

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

Def. (22), the symmetric image of a collective predicate: R x y iff P holds of the pair-sum (similar to from collective similar).

Equations

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

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

The symmetric image is truth-conditionally symmetric — by commutativity of sum formation (Winter's point (i) on def. 7).

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

Principle P1: the symmetric image stands in plain reciprocity with its source collective. With symmetricImage_tcSymmetric this derives the RSG for predicates whose binary form is the symmetric image of a basic collective meaning.

theorem Winter2018.exists_plainReciprocity_not_tcSymmetric : ∃ (R : Bool → Bool → Prop) (P : Finset Bool → Prop), PlainReciprocity P R ∧ ¬TCSymmetric R

The RSG is not logically forced: a plain alternation with a non-symmetric binary predicate exists (fn. 12's ★Xhug — a one-way hug paired with the everywhere-false collective is vacuously plain). The RSG is thus a generalization about natural-language lexicons, not a consequence of the notion of reciprocity.

The Pr-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₁): bidirectional R yields the collective. Fails for hug (separate unidirectional hugs do not make a mutual hug).

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 R — in both directions, by sum commutativity (Pr2.both). Holds for be in love and Hebrew makir; experimental judgments refute it for hug-type verbs.

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-directional R already yields the collective (break up, divorce).

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 R in at least one direction — the weak disjunctive pattern shared by ALL reciprocal alternations, plain and non-plain alike.

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 {x, y} = {y, x}.

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 logically stronger than Pr₁ (§3.3).

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 logically 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

Plain reciprocity entails the weak universal Pr₅.

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 decomposes exactly into Pr₁ together with Pr₂.

Table 3: logical patterns per verb

structure Winter2018.AlternationProfile : Type

A row of Winter's Table 3: which Pr-patterns a non-plain reciprocal alternation exhibits (none where the paper leaves the cell undetermined). Pr₃ — bidirectional R plus simultaneity yields the collective — is event-level and recorded as data only.

• predicate : String
• pr1 : Option Bool
• pr2 : Option Bool
• pr3 : Bool
• pr4 : Bool
• pr5 : Bool

@[implicit_reducible]

instance Winter2018.instDecidableEqAlternationProfile : DecidableEq AlternationProfile

Equations

• Winter2018.instDecidableEqAlternationProfile = Winter2018.instDecidableEqAlternationProfile.decEq

def Winter2018.instDecidableEqAlternationProfile.decEq (x✝ x✝¹ : AlternationProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Winter2018.instReprAlternationProfile : Repr AlternationProfile

Equations

• Winter2018.instReprAlternationProfile = { reprPrec := Winter2018.instReprAlternationProfile.repr }

def Winter2018.instReprAlternationProfile.repr : AlternationProfile → ℕ → Std.Format

Equations

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

def Winter2018.hug : AlternationProfile

Equations

• Winter2018.hug = { predicate := "hug", pr1 := some false, pr2 := some false, pr3 := true, pr4 := false, pr5 := true }

def Winter2018.kiss : AlternationProfile

Equations

• Winter2018.kiss = { predicate := "kiss", pr1 := some false, pr2 := none, pr3 := true, pr4 := false, pr5 := true }

def Winter2018.fight : AlternationProfile

Equations

• Winter2018.fight = { predicate := "fight", pr1 := some false, pr2 := some false, pr3 := true, pr4 := false, pr5 := true }

def Winter2018.breakUp : AlternationProfile

Equations

• Winter2018.breakUp = { predicate := "break up", pr1 := some true, pr2 := some false, pr3 := true, pr4 := true, pr5 := true }

def Winter2018.divorce : AlternationProfile

Equations

• Winter2018.divorce = { predicate := "divorce", pr1 := some true, pr2 := some false, pr3 := true, pr4 := true, pr5 := true }

def Winter2018.collide : AlternationProfile

Equations

• Winter2018.collide = { predicate := "collide", pr1 := none, pr2 := some false, pr3 := true, pr4 := false, pr5 := true }

def Winter2018.inLove : AlternationProfile

Equations

• Winter2018.inLove = { predicate := "be/fall in love", pr1 := some false, pr2 := some true, pr3 := false, pr4 := false, pr5 := true }

def Winter2018.talk : AlternationProfile

Equations

• Winter2018.talk = { predicate := "talk", pr1 := some false, pr2 := some false, pr3 := false, pr4 := false, pr5 := true }

def Winter2018.makir : AlternationProfile

Equations

• Winter2018.makir = { predicate := "makir (Hebrew 'know')", pr1 := some false, pr2 := some true, pr3 := false, pr4 := false, pr5 := true }

def Winter2018.table3 : List AlternationProfile

Equations

• Winter2018.table3 = [Winter2018.hug, Winter2018.kiss, Winter2018.fight, Winter2018.breakUp, Winter2018.divorce, Winter2018.collide, Winter2018.inLove, Winter2018.talk, Winter2018.makir]

theorem Winter2018.table3_pr5 : (table3.all fun (x : AlternationProfile) => x.pr5) = true

§3.3's universal: every alternation in Table 3 satisfies the weak disjunctive Pr₅.

theorem Winter2018.table3_pr4_consistent : (table3.all fun (r : AlternationProfile) => !r.pr4 || r.pr1 == some true) = true

Data-logic consistency: rows claiming Pr₄ also claim Pr₁, as Pr4.pr1 requires (break up, divorce).