Documentation

Linglib.Studies.Sternefeld1998

Sternefeld (1998): Reciprocity and Cumulative Predication #

[Ste98]

Natural Language Semantics 6(3): 303–337. doi:10.1023/A:1008352502939.

[Ste98] extends [Lan78]'s reciprocity-as-cumulativity insight into a fully compositional theory. Distinct readings of plural and reciprocal sentences arise from different placements of the pluralization operators (* and **) at Logical Form. The reciprocal NP itself denotes "the others", with the non-identity statement injected into the LF as semantic glue.

Headline analysis (paper §3, eq 26b) #

Sternefeld's WR analysis: ⟨A, A⟩ ∈ **λxy[R(x, y) ∧ x ≠ y]. The distinctness condition x ≠ y is inside the **'s relation argument — NOT a separate asserted clause as some readings of the literature suggest.

In bivalent semantics this is structurally identical to [Bec01]'s eq 120 (**(λxλy.[R(x,y) ∧ @(x ≠ y)])(A,A)). The two analyses agree on the bivalent predicate — Plurality.Reciprocal.WeakReciprocity — and diverge only on:

  1. Status of distinctness: Sternefeld asserts; Beck presupposes (@). Visible only in trivalent semantics (truth-value gap when R holds with x = y).
  2. Status of SR: [Ste98] §3.5 argues SR is expressible in his framework but defends in §3.6 (the Geach-Kaplan sentence) that SR is "probably a special case of WR" plus only-focus on the non-identity statement. [Bec01] takes SR as a basic reading.
  3. ** operator shape: [Ste98] eq 5 uses [Kri89]'s closure form (smallest relation closed under ⟨a,b⟩+⟨c,d⟩ → ⟨a∪c, b∪d⟩); [BS00] use bidirectional coverage ((∀a∈x. ∃b∈y. R(a,b)) ∧ (∀b∈y. ∃a∈x. R(a,b))). Equivalent on Quine-innovation domains where individuals are identified with singletons.

What is formalized #

Paper §TopicLean encoding
§2 eq 5** operator ([Kri89] closure form)sternefeldStarStar (inductive)
§2.4 eq 12WD analysis (Scha 1981 cumulative)(deferred)
§3 eq 26bWR analysis (distinctness inside relation)sternefeldWR
§3 eq 25bLangendoen-style WR (existence-witnessed)langendoenWR
§3.5 eq 48bSR expressed as iterated * distributionsternefeldSR_iff_stronglyReciprocal

The ** closure-form ↔ bidirectional-coverage equivalence is proved in the easy direction (sternefeldStarStar_implies_cumulative). The reverse direction is a substantial inductive argument that would properly belong in Semantics/Plurality/Cumulativity.lean as substrate justification for treating the two ** formulations as interchangeable; not in this study file.

Out of scope #

Connection to [Bec01] and [HD20] #

[Bec01] cites Sternefeld 1998 as the immediate predecessor and at one point characterises Sternefeld's analysis as bare-**(R)(A,A) (i.e., without distinctness in the relation). Reading Sternefeld 1998 directly: bare **(R)(A,A) does NOT appear in his analysis; his actual eq 26b has distinctness inside the relation. The Beck-vs-Sternefeld difference is therefore presupposition-vs-assertion of the distinctness clause, not structural placement.

[HD20] consumes the same ** machinery via the PPCDRT bridge groupIdentityCond_iff_cumulative_eq. The three-paper convergence on **-cumulation as the heart of reciprocity is the linglib interconnection-density payoff: Sternefeld's WR ↔ Beck's eq 120 ↔ H&D's group identity all factor through Plurality.Cumulativity.Cumulative.

inductive Sternefeld1998.sternefeldStarStar {α : Type u_1} [DecidableEq α] (R : ααProp) :
Finset αFinset αProp

Sternefeld eq 5 / [Kri89]: the smallest relation Q over Finset α × Finset α such that R ⊆ Q (lifted to singletons) and Q is closed under ⟨a,b⟩ + ⟨c,d⟩ → ⟨a∪c, b∪d⟩.

On Quine-innovation domains, this is equivalent to [BS00]'s bidirectional-coverage Cumulative — see sternefeldStarStar_implies_cumulative for the easy direction. The reverse direction holds on nonempty pluralities but the inductive proof is non-trivial; substrate-deferred.

Instances For
    theorem Sternefeld1998.sternefeldStarStar_implies_cumulative {α : Type u_1} [DecidableEq α] (R : ααProp) (x y : Finset α) (h : sternefeldStarStar R x y) :

    Sternefeld closure form ** entails [BS00] bidirectional coverage (the easy direction of the equivalence sternefeldStarStar R x y ↔ Cumulative R x y).

    Proof: induction on the closure derivation. Base case ⟨{a},{b}⟩ from R a b: both quantifiers reduce to the witness pair. Union case: bidirectional coverage of ⟨a∪c, b∪d⟩ follows from coverage of ⟨a,b⟩ and ⟨c,d⟩ by case-splitting on the union membership.

    def Sternefeld1998.sternefeldWR {α : Type u_1} (A : Finset α) (R : ααProp) :

    Sternefeld 1998 eq 26b: WR truth conditions are ⟨A, A⟩ ∈ **λxy[R(x, y) ∧ x ≠ y]. The distinctness clause is INSIDE the **'s relation argument, NOT a separate asserted clause.

    Encoding choice: we use [BS00]'s bidirectional coverage Cumulative for ** (see sternefeldStarStar_implies_cumulative for the connection to Sternefeld's closure-form **).

    In bivalent semantics this is structurally identical to Plurality.Reciprocal.WeakReciprocity (and to Beck eq 120). The two analyses diverge only on the trivalent assertion-vs- presupposition status of x ≠ y (Sternefeld asserts; [Bec01] eq 120 presupposes via @).

    Equations
    Instances For
      @[implicit_reducible]
      instance Sternefeld1998.sternefeldWR.instDecidable {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) [(a b : α) → Decidable (R a b)] :
      Decidable (sternefeldWR A R)
      Equations
      theorem Sternefeld1998.sternefeldWR_iff_WeakReciprocity {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) :

      Sternefeld 1998 ↔ Beck 2001 (bivalent collapse): in bivalent encoding, the two reciprocity analyses produce identical predicates. The cumulation-with-distinctness shape is the common ground of both papers; they only diverge at the trivalent (presupposition projection) layer. Substrate form Plurality.Reciprocal.WeakReciprocity.

      def Sternefeld1998.langendoenWR {α : Type u_1} (A : Finset α) (R : ααProp) :

      [Lan78] WR (paper eq 25b): for each x ∈ A, there are y, z ∈ A with x ≠ y, x ≠ z, xRy, zRx. This is the existence-witnessed form Sternefeld attributes to Langendoen.

      Sternefeld notes (paper p. 316) that this form does not entail his eq 26b for non-D-based relations; in particular, in the "problematic situation" f(R) = {⟨⟨a,b⟩, c⟩, ⟨c, a⟩, ⟨c, b⟩}, eq 25b cannot apply but eq 26b is still true. For D-based relations on Quine-innovation domains, the two coincide and both reduce to Plurality.Reciprocal.WeakReciprocity.

      Equations
      Instances For
        @[implicit_reducible]
        instance Sternefeld1998.langendoenWR.instDecidable {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) [(a b : α) → Decidable (R a b)] :
        Decidable (langendoenWR A R)
        Equations
        theorem Sternefeld1998.langendoenWR_implies_WeakReciprocity {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) (h : langendoenWR A R) :

        For symmetric, distinctness-bearing R, [Lan78] WR entails Plurality.Reciprocal.WeakReciprocity: the existence- witnesses on each side are the y and z of the Langendoen formula.

        theorem Sternefeld1998.sternefeldSR_iff_StrongReciprocity {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) :
        (∀ xA, yA, y xR x y) Semantics.Plurality.Reciprocal.StrongReciprocity R A

        Sternefeld §3.5 eq 48b (SR via iterated distribution): A ∈ *λx[{y: y ∈ A ∧ y ≠ x} ∈ *λy.R(x, y)]. The outer * distributes over A; the inner * quantifies universally over {y ∈ A : y ≠ x}. Assuming R is D-based (applies only to atoms), this unfolds to ∀x ∈ A. ∀y ∈ A. y ≠ x → R(x,y) — exactly Plurality.Reciprocal.StrongReciprocity.

        Sternefeld's point (paper §3.5–3.6): SR is expressible in his framework but is not a basic reading; it falls out of more general WR + focus mechanisms (the Geach-Kaplan analysis, paper §3.6). This contrasts with [Bec01], who takes SR as a basic reading.

        theorem Sternefeld1998.sternefeldWR_implies_cumulative_R {α : Type u_1} [DecidableEq α] (A : Finset α) (R : ααProp) (hWR : sternefeldWR A R) :

        Sternefeld 1998 ↔ [Bec01][HD20] (bivalent): chain sternefeldWR → Cumulative via the substrate WeakReciprocity bridge — the meeting point of all three analyses at the cumulation substrate.

        The three-paper convergence makes Plurality.Cumulativity.Cumulative the substrate consumed by all three Studies files; the implementation choice (BS form vs Krifka closure form) is invisible from the consumer side modulo the easy-direction equivalence sternefeldStarStar_implies_cumulative.