PPCDRT — Anaphoric Relations and Maximize Anaphora

[HD20] [Dot13] [Mur08] [Lan78]

The anaphoric-relation conditions on top of the PPCDRT substrate, plus the R_u set construction and the Maximize Anaphora principle.

Three relations distinguished by [Hig85], [Wil91] and formalized in [HD20]:

• Binding (u_anaph = u_ant): pointwise equality of dref values across the plural state. Requires c-command in the syntax. [HD20] eq 30.

• Group identity (∪u_anaph = ∪u_ant): the summed set of values across the plural state is identical. The pronoun denotes the same plurality as its antecedent. No c-command required. [HD20] §2.3.

• Reciprocity (group identity + ∂(u ≠ u')): same plurality, plus per-state distinctness. The semantic core of each other. [HD20] eq 41.

• Underspecified (group identity, no distinctness): German sich, Czech se, Cheyenne REFL/RECIP affix. Permits reflexive, reciprocal, and mixed readings ([Mur08], [Cab14]).

The reciprocity-as-cumulativity link asserted by [Lan78] shows up as a structural theorem in Cumulativity.lean: groupIdentityCond is the bidirectional-coverage shape that Plurality.Cumulativity.cumulativeOp expresses for plural arguments.

§6 of [HD20] adds the Maximize Anaphora principle (eq 128): when interpreting a discourse referent introduced by a reciprocal with antecedent and relation φ, maximize the set R_u of pairs in the relation, subject to consistency with world knowledge. The substrate-level statement is given here; the §6.1/§6.2/§6.3 applications (the SMH contrast, the multi-reciprocal pairwise prediction, the Tracy/Matty/Chris case) live in Studies/HaugDalrymple2020.lean.

def Semantics.Dynamic.PPCDRT.bindingCond {E : Type u} (uAnaph uAnt : ℕ) : PPDRSCond E

Binding (u_anaph = u_ant): pointwise dref equality across the plural state. The two drefs hold the same Option E value at every state — either both defined and equal, or both undefined.

Per [HD20] eq 30: u_anaph = u_ant ≡ ∀ s ∈ S. v(s)(u_anaph) = v(s)(u_ant). The pointwise Option equality matches this — both drefs hold the same value (defined or undefined) at every state. Stronger than the coreference presupposition (the eq-29 → abbreviation), which only requires defined-and-equal where both are defined.

Equations

• Semantics.Dynamic.PPCDRT.bindingCond uAnaph uAnt S _Δ = ∀ (s : Core.PartialAssign E), s ∈ S → s uAnaph = s uAnt

def Semantics.Dynamic.PPCDRT.coverCond {E : Type u} (uAnaph uAnt : ℕ) : PPDRSCond E

One-direction sum-dref coverage: every value uAnaph takes across the plural state is also a value uAnt takes.

Note: this is NOT [HD20] eq 29 (the asymmetric →). Paper eq 29 is λS.λΔ.∀s ∈ S. u_anaph(s,[s]_Δ) = u_ant(s,S) — an equation between two evaluations, not a subset relation. At Δ = ∅ paper eq 29 reduces to pointwise bindingCond, not to coverCond. The closer paper match is the SUM-dref equality of eq 37 (p. 16), but eq 37 is also bidirectional.

coverCond is a derived auxiliary used solely by the bidirectional bridge groupIdentityCond_iff_bidir_coverCond below — it spells out one direction of the value-set equality so consumers can reason about it directly. It is not itself paper-stipulated.

Equations

• Semantics.Dynamic.PPCDRT.coverCond uAnaph uAnt S _Δ = (S.sumDref uAnaph ⊆ S.sumDref uAnt)

def Semantics.Dynamic.PPCDRT.groupIdentityCond {E : Type u} (uAnaph uAnt : ℕ) : PPDRSCond E

Group identity (∪u_anaph = ∪u_ant): the value-sets of the two drefs across the plural state are equal.

[HD20] eq 41 stipulates ∂(∪u = ∪𝒜(u)) for each other — exactly this symmetric equality on sum-drefs. Bidirectional coverCond is an alternative formulation provable via groupIdentityCond_iff_bidir_coverCond below.

Equations

• Semantics.Dynamic.PPCDRT.groupIdentityCond uAnaph uAnt S _Δ = (S.sumDref uAnaph = S.sumDref uAnt)

theorem Semantics.Dynamic.PPCDRT.groupIdentityCond_iff_bidir_coverCond {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) : groupIdentityCond uAnaph uAnt S Δ ↔ coverCond uAnaph uAnt S Δ ∧ coverCond uAnt uAnaph S Δ

Group identity is the bidirectional version of coverCond.

def Semantics.Dynamic.PPCDRT.reciprocityCond {E : Type u} (uAnaph uAnt : ℕ) : PPDRSCond E

Reciprocity (∂(∪u = ∪u') ∧ ∂(u ≠ u')): group identity plus per-state distinctness. The presupposition wrappers are realized semantically when consumers project to Truth3.

Equations

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

def Semantics.Dynamic.PPCDRT.underspecifiedCond {E : Type u} (uAnaph uAnt : ℕ) : PPDRSCond E

Underspecified reflexive/reciprocal: group identity with no distinctness. Permits reflexive, reciprocal, and mixed readings. [Mur08] (Cheyenne), [Cab14] (German sich).

Equations

• Semantics.Dynamic.PPCDRT.underspecifiedCond uAnaph uAnt = Semantics.Dynamic.PPCDRT.groupIdentityCond uAnaph uAnt

theorem Semantics.Dynamic.PPCDRT.binding_implies_groupIdentity {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : bindingCond uAnaph uAnt S Δ) : groupIdentityCond uAnaph uAnt S Δ

Binding implies group identity: pointwise Option equality of dref values yields equality of value-sets. [HD20] fig 1.

theorem Semantics.Dynamic.PPCDRT.reciprocity_excludes_binding {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (hdef : ∃ (s : Core.PartialAssign E), s ∈ S ∧ ∃ (d : E), s uAnaph = some d) (h : reciprocityCond uAnaph uAnt S Δ) : ¬bindingCond uAnaph uAnt S Δ

Reciprocity excludes binding when there is some state where both drefs are defined: per-state distinctness then contradicts pointwise equality. The hdef hypothesis is necessary because PPCDRT allows both drefs to be undefined at a state, in which case binding (Option none = none) and reciprocity (vacuous distinctness) trivially co-exist.

theorem Semantics.Dynamic.PPCDRT.reciprocity_strengthens_underspecified {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : reciprocityCond uAnaph uAnt S Δ) : underspecifiedCond uAnaph uAnt S Δ

Reciprocity strengthens underspecified: reciprocity = underspecified

• per-state distinctness, so reciprocity implies underspecified.

def Semantics.Dynamic.PPCDRT.R_u {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) : Set (E × E)

The set of (anaphor-value, antecedent-value) pairs across the plural state. [HD20] eq 127: R_u = {⟨v(s)(u_anaph), v(s)(u_ant)⟩ : s ∈ S}.

Equations

• Semantics.Dynamic.PPCDRT.R_u uAnaph uAnt S = {p : E × E | ∃ (s : Core.PartialAssign E), s ∈ S ∧ s uAnaph = some p.fst ∧ s uAnt = some p.snd}

theorem Semantics.Dynamic.PPCDRT.R_u_mono {E : Type u} (uAnaph uAnt : ℕ) {S₁ S₂ : Core.PluralAssign E} (h : ∀ (g : Core.PartialAssign E), g ∈ S₁ → g ∈ S₂) : R_u uAnaph uAnt S₁ ⊆ R_u uAnaph uAnt S₂

A bigger plural state yields a (weakly) bigger R_u.

def Semantics.Dynamic.PPCDRT.maximizeAnaphora {E : Type u} (φ : ℕ → ℕ → PPDRSCond E) (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) : Prop

Maximize Anaphora ([HD20] eq 128). In interpreting a DRS containing a discourse referent u introduced by a reciprocal with antecedent u' and relation φ, maximize the set R_u of pairs standing in φ, subject to the constraint that φ holds in the local DRS given world knowledge.

The substrate-level statement: for the chosen plural state S, no proper extension of S (in the lifted-Set sense on R_u) also satisfies φ. Per [HD20] §6, this is a generation principle, not a decidable predicate — concrete examples supply per-instance decide-checks.

Note: the principle replaces the Strongest Meaning Hypothesis of [DKK+98]; §6.1 of [HD20] discusses the empirical contrast (paper eq 132–133).

Equations

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

theorem Semantics.Dynamic.PPCDRT.maximizeAnaphora_implies_relation {E : Type u} (φ : ℕ → ℕ → PPDRSCond E) (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : maximizeAnaphora φ uAnaph uAnt S Δ) : φ uAnaph uAnt S Δ

Maximize Anaphora implies the chosen state satisfies the relation.