Büring (2012): Pronouns

This file formalizes the semantics of definite pronouns in Büring's handbook survey, as theorems about the project's pronoun denotation applied to the English Fragment's entries. A pronoun is indexed and denotes the value its index has under the assignment; bound, anaphoric and deictic uses share that one denotation, so a binder is an external operator manipulating the assignment rather than a second lexical entry. The φ-features are presuppositions on the resolved referent: she picks out the assignment value only when that value is singular and not gendered masculine, I only when it includes the agent of the context, and each is undefined, neither true nor false, merely infelicitous, otherwise. The unmarked feature values contribute nothing, so a pronoun that carries only unmarked values is defined of any referent at all. That is the survey's underspecification treatment of they, whose gender-neutrality is the absence of a gender feature rather than a feature of its own.

Main results

• selector_eq_assignment: a pronoun denotes the assignment value at its index.
• undefined_of_masculine, undefined_of_not_agent: a feminine entry is undefined of a referent gendered masculine, a first-person entry of one not including the agent.
• defined_of_unmarked_features: an entry with only unmarked values imposes no condition.
• they_defined_where_she_undefined: the two English entries at a male referent.
• bound_reading: binding is an assignment update, with the entry's denotation unchanged.

References

• D. Büring, Pronouns (2012)
• U. Sauerland, A new semantics for number (2003)

theorem Buring2012.selector_eq_assignment {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) : (e.denote n c).selector g PUnit.unit = some (HeimKratzer.interpPronoun n g)

A pronoun denotes the value of its index under the assignment. Its selector is the canonical variable lookup, the same one for the bound, anaphoric and deictic uses.

theorem Buring2012.undefined_of_masculine {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (hfem : e.gender = some Gender.feminine) (h : g n ∈ Gendered.masculine) : (e.denote n c).toTrivalent scope g PUnit.unit = 0

A feminine pronoun is undefined of a referent gendered masculine. The feature does not assert the referent's gender but presupposes it, so the denotation has no value at all when it fails.

theorem Buring2012.she_undefined_of_masculine {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (h : g n ∈ Gendered.masculine) : (English.Pronouns.she.denote n c).toTrivalent scope g PUnit.unit = 0

She is undefined of a referent gendered masculine.

theorem Buring2012.undefined_of_not_agent {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (hp : e.referentialPerson = some Person.first) (h : ¬c.agent ≤ g n) : (e.denote n c).toTrivalent scope g PUnit.unit = 0

A first-person pronoun is undefined of a referent that does not include the agent.

theorem Buring2012.i_undefined_of_not_agent {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (h : ¬c.agent ≤ g n) : (English.Pronouns.i.denote n c).toTrivalent scope g PUnit.unit = 0

I is undefined of a referent that does not include the agent.

theorem Buring2012.defined_of_unmarked_features {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (hp : e.referentialPerson = some Person.third) (hn : e.referentialNumber = some Number.plural) (hg : e.gender = none) : (e.denote n c).toTrivalent scope g PUnit.unit ≠ 0

An entry carrying only unmarked values — third person, plural, no gender — restricts the referent to nothing, so it is defined wherever any pronoun is. Unmarked values are the absence of a feature rather than a feature of their own, which is why the underspecified form can be used to avoid a gender specification.

theorem Buring2012.they_defined_regardless_of_gender {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) : (English.Pronouns.they.denote n c).toTrivalent scope g PUnit.unit ≠ 0

They is defined of a referent of any gender.

theorem Buring2012.they_defined_where_she_undefined {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (scope : E → PUnit.{u_4 + 1} → Prop) (h : g n ∈ Gendered.masculine) : (English.Pronouns.she.denote n c).toTrivalent scope g PUnit.unit = 0 ∧ (English.Pronouns.they.denote n c).toTrivalent scope g PUnit.unit ≠ 0

The two entries come apart exactly at the referents the gender feature excludes, where she has no value and they has one.

theorem Buring2012.bound_reading {E : Type u_1} {P : Type u_2} {T : Type u_3} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (g : Assignment E) (n : ℕ) (c : Reference.Context PUnit.{u_4 + 1} E P T) (b : E) : (e.denote n c).selector (Function.update g n b) PUnit.unit = some b

Binding leaves the pronoun alone. The binding operator updates the assignment at the pronoun's index, and the unchanged denotation then returns the binder. There is no bound-pronoun lexeme.