Possessive pronouns: where the possessive and pronoun APIs meet

A possessive pronoun (his book, mine) is the possessive Kleisli arrow (Possessive.applyTo / theOf) applied to a possessor that is a pronoun denotation. Because both APIs trade in NominalDenot and possessive-of is bind, they compose with no glue:

• the selector picks the possessee (the unique R-possessee of the pronoun's referent), while
• the intrinsic presupposition is the pronoun's φ-features on the possessor (g i) — not on the possessee.

That presup-on-possessor / selector-on-possessee split — what distinguishes a possessive pronoun from a plain pronoun — is exactly Possessive.applyTo_presup, i.e. derived, not stipulated.

Main statements

• possessivePronoun_presup — his N's presupposition is the possessor pronoun's φ-presupposition (on g i).
• possessivePronoun_selector — his N's selector is the unique R-possessee of the pronoun's referent.

theorem Possessive.possessivePronoun_presup {E : Type} [PartialOrder E] (p : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) (R : E → E → Prop) (g : Core.Assignment E) (w : PUnit.{1}) : (applyTo (p.denote i speaker addressee isFemale isInanimate) R).presup g w = (p.phiPresup speaker addressee isFemale isInanimate).presup (g i)

his N's intrinsic presupposition is the possessor pronoun's φ-feature presupposition, imposed on the possessor g i — the φ-features ride along the possessive by applyTo_presup.

theorem Possessive.possessivePronoun_selector {E : Type} [PartialOrder E] (p : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) (R : E → E → Prop) (g : Core.Assignment E) (w : PUnit.{1}) : (applyTo (p.denote i speaker addressee isFemale isInanimate) R).selector g w = Semantics.Definiteness.russellIota fun (y : E) => R (Intensional.Variables.interpPronoun i g) y

his N's selector picks the unique R-possessee of the pronoun's referent — the possessee, not the possessor.