The denotation of a pronoun

Gives the PersonalPronoun lexical record a meaning, as a NominalDenot: the selector is the project-canonical variable denotation interpPronoun (g ↦ g i), so the pronoun-as-object and the bare assignment-indexed variable are the same individual by construction — not via a bridge theorem. The intrinsic presupposition is the φ-feature presupposition read off the entry's person/number/gender via the [Sau03]-style cells in Semantics.Presupposition.PhiFeatures.

This follows [Bur12]'s survey: the assignment lookup (his (14)), the feature presuppositions (his (49)/(50)), and the absence-of-features treatment of unmarked values. The same interpPronoun selector serves bound, anaphoric, and deictic uses (his §2.1.1); binding is the external β-operator (Semantics.Reference.Binding).

Main definitions

• PersonalPronoun.phiPresup — the conjoined φ-feature presupposition of an entry (absent or featurally-uncovered values contribute PartialProp.top).
• PersonalPronoun.denote — the pronoun's NominalDenot (static case).

Implementation notes

Number values beyond singular/plural (dual, trial, …) and the non-sex-based surface genders contribute the vacuous cell here; the principled route is the Number.fromUD/Gender.Features.fromGender bridges plus ContainmentPairLike.toPair, deferred until a study needs them.

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

The conjoined φ-feature presupposition of a pronoun entry, over an entity domain E. The model supplies the entity-level predicates the cells need (speaker/addressee for person, isFemale/isInanimate for gender; number atomicity comes from the PartialOrder). A feature that is absent — or present but outside the cells' coverage — contributes PartialProp.top.

Equations

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

def PersonalPronoun.denote {E : Type} [PartialOrder E] (e : PersonalPronoun) (i : ℕ) (speaker addressee : E) (isFemale isInanimate : E → Prop) : Semantics.Reference.NominalDenot (Core.Assignment E) PUnit.{u_1 + 1} E

A pronoun's denotation as a NominalDenot: the selector is the canonical variable denotation interpPronoun i (always defined under a total assignment), and the intrinsic presupposition is the φ-feature presupposition imposed on the resolved referent g i. The static case; world is trivial.

Equations

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

Fusion seam with the dynamic lookup interface

theorem interpPronoun_eq_iLookup {E W : Type} (i : ℕ) (g : Core.Assignment E) (w : PUnit.{1}) : Intensional.Variables.interpPronoun i g = Semantics.Dynamic.Context.HasFiberedLookup.iLookup g i w

The pronoun's canonical variable selector interpPronoun i is exactly the M = Id extensional-baseline instance of the dynamic-anaphora lookup interface HasFiberedLookup.iLookup (Semantics.Dynamic.Effects.HasFiberedLookup, instAssignmentHasFiberedLookup). So static reference and dynamic (Set/PMF) anaphora already agree at the static fiber — modulo the Option partiality layer Entry.denote adds. This discharges the first step of the functor- parametric NominalDenot consolidation (Nominal.lean's Todo): the remaining, higher-blast-radius stage makes selector itself functor-valued and be iLookup.

Featural definedness tests

Pronouns are definite descriptions ([Elb05], [PGG17])

A referential pronoun is a (null-NP) definite description over its φ-feature restrictor — a Description. [PGG17]'s proposal is that the personal/demonstrative split is the [Sch09b] weak/strong-article split: PER (er) the weak article (Description.ofPresupType .uniqueness = .unique), "DEM" (der) the strong article (…ofPresupType .familiarity = .anaphoric, the weak description plus an anaphoric index). PG&G's "DEM = PER + index" is the weak/strong refinement Semantics.Definiteness.interpret_anaphoric_eq_unique_of_existsUnique; the strength round-trips through expectedPresupType. The extra layer is that index, not spatial deixis (footnote 1) — der is a strong personal pronoun, not a separate type; genuine deictic demonstratives are Description.demonstrative.

Caveat on denote below: the project's canonical PersonalPronoun.denote realizes the [Bur12] assignment lookup g i — the indexed/anaphoric referent, i.e. the strong arm — so the bridge proves denote = ofPresupType .familiarity. PG&G's weak PER (ofPresupType .uniqueness, the uniqueness iota over the φ-restrictor) is a distinct denotation denote does not compute; the two arms agree exactly when g i is the unique satisfier.

theorem PersonalPronoun.denote_selector_eq_ofPresupType {E W : Type} [PartialOrder E] (e : PersonalPronoun) (i : ℕ) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (speaker addressee : E) (isFemale isInanimate : E → Prop) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (w : PUnit.{u_1 + 1}) (h : R g gs (g i)) : (e.denote i speaker addressee isFemale isInanimate).selector g w = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.ofPresupType Features.Definiteness.DefPresupType.familiarity R i) g gs

A pronoun's [Bur12] variable-lookup referent equals its definite description whenever the restrictor holds of the indexed referent: the strong-article (Description.ofPresupType .familiarity) reading, since the anaphoric index is the indexed entity. The weak reading coincides too when that entity is the unique satisfier (Semantics.Definiteness.interpret_anaphoric_eq_unique_of_existsUnique).