The denotation of a pronoun

import Linglib.Semantics.Reference.Pronoun · namespace PersonalPronoun

This file defines the denotation of a personal pronoun. A PersonalPronoun entry denotes a Nominal whose selector is the value of the entry's index under the assignment, and whose intrinsic presupposition is that the resolved referent lies in the entry's φ-domain (PersonalPronoun.phiDom, PersonalPronoun.denote). The φ-domain is the intersection of Person.dom at the context of utterance with Number.dom and Gender.dom at the entry's referential person and number and its gender. The selector does not vary with the world of evaluation (PersonalPronoun.isRigid_denote_selector), so a pronoun refers directly. This is the account Büring surveys: one denotation serves the bound, anaphoric and deictic uses, binding is abstraction over the assignment (Montague.lambdaAbsG), and, as Sauerland proposes, an absent or unmarked feature restricts nothing.

Implementation notes

The φ-domain reads the entry's referential person and number (PersonalPronoun.referentialPerson, PersonalPronoun.referentialNumber), not its agreement features, so a polite pronoun that agrees as third plural presupposes its addressee (PersonalPronoun.phiDom_congr). The speaker and the addressee are the agent and the addressee of the context of utterance (Kaplan.Context), and the female and the inanimate referents are the gender of referents the entity domain comes equipped with (Gendered).

References

Büring 2012, Pronouns formalized
Sauerland 2003, A new semantics for number formalized

Declarations

The φ-domain of a pronoun entry over an entity domain E is the intersection of the person domain of its referential person at the context of utterance, the number domain of its referential number and the gender domain of its gender.

def phiDom L52–58

{E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (c : Kaplan.Context W E P T) :

Set E

e.phiDom c = Person.dom c e.referentialPerson ∩ Number.dom e.referentialNumber ∩ Gender.dom e.gender

Used by mem_phiDom, phiDom_congr, denote, denote_presup

L60–64

L66–68

A pronoun denotes the nominal whose selector is the value g i of its index, always defined under a total assignment, and whose intrinsic presupposition is that the resolved referent g i lies in the φ-domain.

def denote L70–75

{E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (i : ℕ) (c : Kaplan.Context W E P T) :

Nominal (Assignment E) W E

e.denote i c = { presup := fun (g : Assignment E) (x : W) => g i ∈ e.phiDom c, selector := fun (g : Assignment E) (x : W) => some (g i) }

Built from

Used by denote_presup, denote_selector, isRigid_denote_selector

Used in Buring2012

L79–84

L86–88

L90–92

theorem isRigid_denote_selector L94–96

{E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] [Gendered E] (e : PersonalPronoun) (i : ℕ) (c : Kaplan.Context W E P T) (g : Assignment E) :

IsRigid ((e.denote i c).selector g)

Built from