Partial Plural CDRT

Haug and Dalrymple's Partial Plural Compositional DRT joins the plural information states of Plural CDRT (Brasoveanu, Dotlačil) with the partial assignments of Partial CDRT (Haug), in which an anaphoric condition is a presupposition rather than a resolution the grammar makes. This file defines the conditions of a PPDRS on the states of PCDRT, reading a dref's values and dependencies through PCDRT.value and PCDRT.dep.

A condition takes the output state and the set Δ of drefs the DRS distributes over. Three anaphoric relations are distinguished, after Higginbotham and Williams:

• binding (u_anaph = u_ant), pointwise equality of the two drefs, which needs c-command;
• group identity (∪u_anaph → ∪u_ant), the anaphor's values summed over each state's class under distribution equal to the antecedent's values over the whole state, so that the antecedent escapes the distribution;
• reciprocity, group identity with distinctness in every state, the contribution of each other; without the distinctness it is the underspecified meaning of German sich or the Cheyenne reflexive/reciprocal affix (Murray, Cable).

Main definitions

• PPCDRT.PPDRSCond: a condition on a plural state under a distribution context.
• PPCDRT.eqClass: the class of a state under distribution.
• PPCDRT.bindingCond, PPCDRT.groupIdentityCond, PPCDRT.reciprocityCond, PPCDRT.underspecifiedCond: the anaphoric relations.
• PPCDRT.extend, PPCDRT.introPartial: partial dref introduction on assignments and on plural states.

Main results

• PPCDRT.groupIdentityCond_empty: without distribution, group identity is equality of the two drefs' values.
• PPCDRT.reciprocityCond_empty_iff: without distribution, reciprocity is a dependency with equal domain and codomain and no reflexive pair.
• PPCDRT.binding_implies_groupIdentity, PPCDRT.reciprocity_excludes_binding: binding and reciprocity against group identity.
• PPCDRT.nontrivial_value_of_reciprocityCond: a reciprocal's antecedent denotes a plurality.
• PPCDRT.mem_extend_iff_covBy: introducing a dref is a covering step of the extension order.
• PPCDRT.introPartial_subset_intro: partial introduction refines Plural CDRT's.

References

• D. T. T. Haug and M. Dalrymple, Reciprocity: Anaphora, scope, and quantification (2020)
• D. T. T. Haug, Partial dynamic semantics for anaphora: Compositionality without syntactic coindexation (2014)
• A. Brasoveanu, Structured nominal and modal reference (2007)
• J. Dotlačil, Reciprocals distribute over information states (2013)
• J. Higginbotham, On semantics (1985)
• E. Williams, Reciprocal scope (1991)
• S. E. Murray, Reflexivity and reciprocity with(out) underspecification (2008)
• S. Cable, Reflexives, reciprocals and contrast (2014)

@[reducible, inline]

abbrev PPCDRT.PPDRSCond (E : Type u_2) : Type u_2

A PPDRS condition ([HD20] (27)): a property of the output plural state and of the set Δ of drefs the DRS distributes over ((25)).

Equations

• PPCDRT.PPDRSCond E = (PluralAssign ℕ E → Set ℕ → Prop)

Distribution

def PPCDRT.eqClass {E : Type u_1} (S : PluralAssign ℕ E) (Δ : Set ℕ) (s : PartialAssign ℕ E) : PluralAssign ℕ E

The class of s under distribution over Δ ([HD20] (26)): the states of S agreeing with s on every dref in Δ.

Equations

• PPCDRT.eqClass S Δ s = {t : PartialAssign ℕ E | t ∈ S ∧ ∀ u ∈ Δ, t u = s u}

@[simp]

theorem PPCDRT.eqClass_empty {E : Type u_1} (S : PluralAssign ℕ E) (s : PartialAssign ℕ E) : eqClass S ∅ s = S

theorem PPCDRT.mem_eqClass {E : Type u_1} (S : PluralAssign ℕ E) (Δ : Set ℕ) {s t : PartialAssign ℕ E} : t ∈ eqClass S Δ s ↔ t ∈ S ∧ ∀ u ∈ Δ, t u = s u

theorem PPCDRT.self_mem_eqClass {E : Type u_1} (S : PluralAssign ℕ E) (Δ : Set ℕ) {s : PartialAssign ℕ E} (hs : s ∈ S) : s ∈ eqClass S Δ s

Anaphoric relations

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

Binding (u_anaph = u_ant, [HD20] (30)): the two drefs hold the same value in every state, both defined and equal or both undefined. This is stronger than the coreference presupposition of (29), which constrains only the states where both are defined.

Equations

• PPCDRT.bindingCond uAnaph uAnt S x✝ = ∀ s ∈ S, s uAnaph = s uAnt

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

Group identity (∪u_anaph → ∪u_ant, [HD20] (29), (38)): in every state, the anaphor's values over the state's class under distribution are the antecedent's values over the whole state.

Equations

• PPCDRT.groupIdentityCond uAnaph uAnt S Δ = ∀ s ∈ S, PCDRT.value uAnaph (PPCDRT.eqClass S Δ s) = PCDRT.value uAnt S

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

Reciprocity (∪u_anaph → ∪u_ant, ∂(u_anaph ≠ u_ant), [HD20] (41)): group identity, with the two drefs distinct in every state where both are defined.

Equations

• PPCDRT.reciprocityCond uAnaph uAnt S Δ = (PPCDRT.groupIdentityCond uAnaph uAnt S Δ ∧ ∀ s ∈ S, ∀ (a b : E), s uAnaph = ↑a → s uAnt = ↑b → a ≠ b)

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

The underspecified reflexive/reciprocal ([HD20] (79b)): group identity without distinctness, admitting reflexive, reciprocal and mixed construals ([Mur08], [Cab14]).

Equations

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

theorem PPCDRT.groupIdentityCond_empty {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) : groupIdentityCond uAnaph uAnt S ∅ ↔ PCDRT.value uAnaph S = PCDRT.value uAnt S

Without distribution, group identity is equality of the two drefs' values, the cumulative identity ∪u_anaph = ∪u_ant of [HD20] (39).

theorem PPCDRT.binding_implies_groupIdentity {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) (h : bindingCond uAnaph uAnt S ∅) : groupIdentityCond uAnaph uAnt S ∅

Binding implies group identity without distribution. Under distribution the two come apart ([HD20] (24) against (31)).

theorem PPCDRT.reciprocity_excludes_binding {E : Type u_1} (uAnaph uAnt : ℕ) (S : PluralAssign ℕ E) (Δ : Set ℕ) (hdef : ∃ s ∈ S, ∃ (d : E), s uAnaph = ↑d) (h : reciprocityCond uAnaph uAnt S Δ) : ¬bindingCond uAnaph uAnt S Δ

Reciprocity excludes binding once some state defines the anaphor: distinctness there contradicts pointwise equality. Without such a state both drefs may be undefined throughout, and binding and reciprocity hold together vacuously.

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

theorem PPCDRT.reciprocityCond_empty_iff {E : Type u_1} {uAnaph uAnt : ℕ} {S : PluralAssign ℕ E} (hdef : ∀ s ∈ S, s uAnaph ≠ ⊥ ↔ s uAnt ≠ ⊥) : reciprocityCond uAnaph uAnt S ∅ ↔ (PCDRT.dep uAnt uAnaph S).dom = (PCDRT.dep uAnt uAnaph S).cod ∧ (PCDRT.dep uAnt uAnaph S).IsIrrefl

Without distribution, and where the two drefs are defined in the same states, reciprocity is a property of the dependency between antecedent and anaphor: its domain and codomain coincide, and it is irreflexive. This is [HD20]'s gloss of (39), cumulative identity across states combined with distinctness within each.

theorem PPCDRT.nontrivial_value_of_reciprocityCond {E : Type u_1} {uAnaph uAnt : ℕ} {S : PluralAssign ℕ E} {Δ : Set ℕ} (h : reciprocityCond uAnaph uAnt S Δ) {s : PartialAssign ℕ E} (hs : s ∈ S) {a b : E} (ha : s uAnaph = ↑a) (hb : s uAnt = ↑b) : (PCDRT.value uAnt S).Nontrivial

A reciprocal's antecedent denotes a plurality: at a state defining both drefs, the anaphor's value lies among the antecedent's by group identity and differs from the antecedent's value there. This holds under any distribution.

Partial dref introduction

def PPCDRT.extend {Var : Type u_2} {D : Type u_3} (u : Var) : DynamicSemantics.Update (PartialAssign Var D)

Partial dref introduction i[u]o ([HD20] (20)): i leaves u unvalued, o values it, and the two agree on every other dref.

Equations

• PPCDRT.extend u = {p : PartialAssign Var D × PartialAssign Var D | p.1 u = ⊥ ∧ p.2 u ≠ ⊥ ∧ ∀ (v : Var), v ≠ u → p.1 v = p.2 v}

theorem PPCDRT.mem_extend {Var : Type u_2} {D : Type u_3} {u : Var} {i o : PartialAssign Var D} : (i, o) ∈ extend u ↔ i u = ⊥ ∧ o u ≠ ⊥ ∧ ∀ (v : Var), v ≠ u → i v = o v

theorem PPCDRT.mem_extend_iff_covBy {Var : Type u_2} {D : Type u_3} {u : Var} {i o : PartialAssign Var D} : (i, o) ∈ extend u ↔ i ⋖ o ∧ i u ≠ o u

Introducing u is a covering step of the extension order, the one that values u.

theorem PPCDRT.extend_subset_randomAssign {Var : Type u_2} {D : Type u_3} {u : Var} [DecidableEq Var] : extend u ⊆ DynamicSemantics.Update.randomAssign u

Partial introduction is a random assignment that genuinely values u.

def PPCDRT.introPartial {Var : Type u_2} {D : Type u_3} (u : Var) : DynamicSemantics.Update (PluralAssign Var D)

Partial dref introduction on plural states ([HD20] (6), after [Dot13]): every input row has an extension at u among the output rows, every output row extends some input row, and the output state is nonempty. It refines Plural CDRT's PCDRT.intro (introPartial_subset_intro) in two ways: every output row values u, where a random assignment may leave it ★, and the output is nonempty.

Equations

• PPCDRT.introPartial u = {p : PluralAssign Var D × PluralAssign Var D | Set.Nonempty p.2 ∧ p ∈ (PPCDRT.extend u).cumul}

theorem PPCDRT.introPartial_subset_intro {Var : Type u_2} {D : Type u_3} {u : Var} [DecidableEq Var] : introPartial u ⊆ PCDRT.intro u