PPCDRT — Anaphoric Relations

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

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

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.Cumulative expresses for plural arguments.

§6 of [HD20] builds its Maximize Anaphora principle (eq 128) over the set R_u of anaphor-antecedent value pairs (eq 127), defined 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.

Binding

def PPCDRT.bindingCond {E : Type u_1} (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

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

Group identity

def PPCDRT.groupIdentityCond {E : Type u_1} (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.

Equations

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

Reciprocity

def PPCDRT.reciprocityCond {E : Type u_1} (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 Truth.

Equations

• PPCDRT.reciprocityCond uAnaph uAnt S Δ = (PPCDRT.groupIdentityCond uAnaph uAnt S Δ ∧ ∀ (s : PartialAssign ℕ E), s ∈ S → ∀ (d_a d_b : E), s uAnaph = some d_a → s uAnt = some d_b → d_a ≠ d_b)

Underspecified reflexive/reciprocal

def PPCDRT.underspecifiedCond {E : Type u_1} (uAnaph uAnt : ℕ) : PPDRSCond E

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

Equations

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

Implication lattice

theorem PPCDRT.binding_implies_groupIdentity {E : Type u_1} (uAnaph uAnt : ℕ) (S : 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 PPCDRT.reciprocity_excludes_binding {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) (Δ : Set ℕ) (hdef : ∃ (s : 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 PPCDRT.reciprocity_strengthens_underspecified {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) (Δ : Set ℕ) (h : reciprocityCond uAnaph uAnt S Δ) : underspecifiedCond uAnaph uAnt S Δ

Reciprocity strengthens underspecified: reciprocity = underspecified

• per-state distinctness, so reciprocity implies underspecified.

The relation set R_u

def PPCDRT.R_u {E : Type u_1} (uAnaph uAnt : ℕ) (S : 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

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

theorem PPCDRT.R_u_mono {E : Type u_1} (uAnaph uAnt : ℕ) {S₁ S₂ : PluralAssign ℕ E} (h : ∀ (g : 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.