The denotation of a pronoun

A PersonalPronoun entry denotes as a Nominal whose selector is the variable denotation interpPronoun, the value of the entry's index under the assignment, and whose intrinsic presupposition is the φ-feature presupposition read off the entry's person, number and gender through the cells of Presupposition.PhiFeatures (PersonalPronoun.phiPresup, PersonalPronoun.denote). The selector does not vary with the world of evaluation (PersonalPronoun.isRigid_denote_selector): a pronoun refers directly. This is the survey of [Bur12]: one denotation serves the bound, anaphoric and deictic uses, binding being an operator on the assignment (Composition/Binding.lean), and an absent or unmarked feature contributes the trivial presupposition, the treatment of [sauerland-2003].

Implementation notes

Number values beyond singular and plural and the non-sex-based genders contribute the trivial cell; the bridges Number.fromUD and Gender.Features.fromGender are the principled route, deferred until a study needs them.

References

• [Bur12]
• [sauerland-2003]

def PersonalPronoun.phiPresup {E : Type u_1} [PartialOrder E] (e : PersonalPronoun) (speaker addressee : E) (isFemale isInanimate : E → Prop) : Presupposition.PartialProp E

The conjoined φ-feature presupposition of a pronoun entry over an entity domain E: the model supplies the speaker and addressee for person and the gender predicates; number atomicity comes from the parthood order. An absent or uncovered feature contributes PartialProp.top.

Equations

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

def PersonalPronoun.denote {E W : Type} [PartialOrder E] (e : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) : Reference.Nominal (Assignment E) W E

A pronoun's denotation: the selector is the variable denotation interpPronoun i, always defined under a total assignment, and the intrinsic presupposition is the φ-feature presupposition of the resolved referent g i.

Equations

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

@[simp]

theorem PersonalPronoun.denote_selector {E W : Type} [PartialOrder E] (e : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) (g : Assignment E) (w : W) : (e.denote i speaker addressee isFemale isInanimate).selector g w = some (g i)

theorem PersonalPronoun.isRigid_denote_selector {E W : Type} [PartialOrder E] (e : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) (g : Assignment E) : Reference.IsRigid ((e.denote i speaker addressee isFemale isInanimate).selector g)

A pronoun's referent does not vary with the world: the selector is rigid.