The denotation of a determiner

[Sch09b] [PGG17] [CB15] [Mor21]

Gives the determiner lexical records (Syntax/Determiner/Basic.lean) meanings, as NominalDenots — the determiner half of the API whose pronoun half is Semantics/Reference/PronounDenotation.lean. The wiring is parallel:

	pronoun	determiner
lexical record	PersonalPronoun	Article, DemonstrativeDeterminer
selector	interpPronoun (g ↦ g i)	Semantics.Definiteness.interpret
intrinsic presupposition	φ-features (phiPresup)	deixis (deixisPresup)

The selector is the canonical Description interpretation — determiner-as-object and the interpreted description pick the same individual by construction, not via a bridge theorem. The intrinsic presupposition is where a demonstrative's deictic feature projects: deixis filters the referent but never selects it (denote_selector_eq_anaphoric, the API-level form of interpret_demonstrative_eq_anaphoric).

Main declarations

• Description.denote — a description's NominalDenot (vacuous intrinsic presupposition; a definite's only presupposition is definedness).
• DemonstrativeDeterminer.deixisPresup — the deictic presupposition over an entity domain, with model-supplied proximity predicates (parallel to PersonalPronoun.phiPresup's speaker/addressee).
• DemonstrativeDeterminer.denote — the demonstrative's NominalDenot (previously deferred in the lexical file's implementation notes).
• Article.denotations — an article's possible NominalDenots, the image of Article.toDescriptions under Description.denote; a syncretic article (English the) denotes both the weak and the strong description.
• Possessive.denote — the possessive determiner's NominalDenot (previously deferred): a definite description selecting the unique satisfier of the possessee restrictor that stands in the possession relation to the possessor; the GQ-form possessive (PossW, narrowing-aware) lives in Semantics/Possessive/GQ.lean.
• interpret_possessive_eq_viaModifier, Possessive.denote_isSome_iff_iotaPresupposition, Possessive.toCarrier — the determiner denotation is the Possessive carrier API: same restrictor (Barker's viaModifier), same definedness presupposition, same referent.

Implementation notes

Context is the bi-assignment Assignment E × SitAssignment W and the world coordinate is trivial (PUnit), matching the static case of PersonalPronoun.denote. Quantifier (a generalized quantifier, not an individual denotation — it has no NominalDenot) remains deferred.

Descriptions as nominal denotations

noncomputable def Semantics.Definiteness.Description.denote {E W : Type} (k : Description E W) : Reference.NominalDenot (Core.Assignment E × Intensional.Variables.SitAssignment W) PUnit.{u_1 + 1} E

A description's denotation as a NominalDenot: the selector is the canonical interpretation function interpret, and the intrinsic presupposition is vacuous — a definite's only presupposition is that the selector is defined. The static case; world is trivial.

Equations

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

@[simp]

theorem Semantics.Definiteness.Description.denote_selector {E W : Type} (k : Description E W) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (w : PUnit.{u_1 + 1}) : k.denote.selector (g, gs) w = interpret k g gs

The by-construction identity: a description's selector is interpret.

The demonstrative determiner's denotation

def DemonstrativeDeterminer.deixisPresup {E : Type} (dem : DemonstrativeDeterminer) (proximal medial distal : E → Prop) : E → Prop

The deictic presupposition of a demonstrative determiner, over an entity domain. The model supplies the proximity predicates the deixis cells need (parallel to the speaker/addressee/isFemale parameters of PersonalPronoun.phiPresup); an unspecified feature contributes the trivial presupposition.

Equations

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

noncomputable def DemonstrativeDeterminer.denote {E W : Type} (dem : DemonstrativeDeterminer) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) (proximal medial distal : E → Prop) : Semantics.Reference.NominalDenot (Core.Assignment E × Intensional.Variables.SitAssignment W) PUnit.{u_1 + 1} E

A demonstrative determiner's denotation as a NominalDenot (the DemonstrativeDeterminer.denote deferred by the lexical file): the selector is the canonical interpretation of the demonstrative description at discourse index d, and the intrinsic presupposition is the deictic presupposition imposed on the indexed referent g d — parallel to PersonalPronoun.denote, with deixis in place of φ-features.

Equations

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

theorem Semantics.Definiteness.DemonstrativeDeterminer.denote_selector_eq_anaphoric {E W : Type} (dem : DemonstrativeDeterminer) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) (proximal medial distal : E → Prop) : (dem.denote R sIdx d proximal medial distal).selector = (Description.anaphoric R d).denote.selector

Deixis filters, it does not select: a demonstrative determiner's selector is exactly the bare anaphoric description's selector. The API-level form of interpret_demonstrative_eq_anaphoric — the deictic content lives entirely in the presup component.

theorem Semantics.Definiteness.DemonstrativeDeterminer.denote_selector_congr {E W : Type} (dem₁ dem₂ : DemonstrativeDeterminer) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) (proximal medial distal : E → Prop) : (dem₁.denote R sIdx d proximal medial distal).selector = (dem₂.denote R sIdx d proximal medial distal).selector

Two demonstrative determiners differing only in deictic feature share a selector — this and that pick the same referent and differ only in what they presuppose about it.

The article's denotations

noncomputable def Article.denotations {E W : Type} (a : Article) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) : List (Semantics.Reference.NominalDenot (Core.Assignment E × Intensional.Variables.SitAssignment W) PUnit.{u_1 + 1} E)

An article's possible denotations: the NominalDenots of its admissible descriptions (Article.toDescriptions). A syncretic article (English the) denotes both the weak and the strong description; a German weak or strong article denotes exactly one.

Equations

• a.denotations R idx = List.map Semantics.Definiteness.Description.denote (a.toDescriptions R idx)

theorem Semantics.Definiteness.Article.denotations_licensed {E W : Type} (a : Article) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) (nd : Reference.NominalDenot (Core.Assignment E × Intensional.Variables.SitAssignment W) PUnit.{u_1 + 1} E) (h : nd ∈ a.denotations R idx) : ∃ (k : Description E W), Determiner.licenses [Determiner.Entry.article a] k ∧ nd = k.denote

Every denotation of an article arises from a description the article licenses — the denotational pipeline and the licensing pipeline agree.

The possessive determiner's denotation

noncomputable def Possessive.denote {E W : Type} (_p : Possessive) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) : Semantics.Reference.NominalDenot (Core.Assignment E × Intensional.Variables.SitAssignment W) PUnit.{u_1 + 1} E

A possessive determiner's denotation as a NominalDenot (the Possessive.denote deferred by the lexical file): the definite description selecting the unique satisfier of the possessee restrictor R that stands in rel to the possessor — i.e. the Description.possessive selector (russellIota of R ∧ rel possessor ·). The intrinsic presupposition is vacuous; the definite's only presupposition is definedness, exposed as the selector returning some.

The narrowing-aware GQ form for quantificational possessors ("every student's cat") is Possessive.PossW — (individual a) of PossW reduces here when the possessor is an entity.

Equations

• _p.denote R possessor rel = (Semantics.Definiteness.Description.possessive R possessor rel).denote

@[simp]

theorem Semantics.Definiteness.Possessive.denote_selector {E W : Type} (p : Possessive) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (w : PUnit.{u_1 + 1}) : (p.denote R possessor rel).selector (g, gs) w = interpret (Description.possessive R possessor rel) g gs

A possessive determiner's selector is the possessive description's selector — the determiner picks the unique possessee related to the possessor by construction.

theorem Semantics.Definiteness.Possessive.denote_licensed {E W : Type} (p : Possessive) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) : Determiner.licenses [Determiner.Entry.possessive p] (Description.possessive R possessor rel)

A possessive determiner licenses its own denotation — the denotational pipeline and the licensing pipeline agree, parallel to Article.denotations_licensed.

Unification with the possessive carrier API

The possessive determiner's denotation (Description.possessive/russellIota) and the Possessive carrier API are not two analyses — they are the same construction. The determiner's restrictor is Barker's Possessive.viaModifier (π of the noun predicate and the possession relation); its definedness presupposition is the carrier's Russellian iota-presupposition; and at a context where the presupposition holds, the determiner assembles into a Possessive.Definite carrier whose existsUnique_possessee selects the very referent the determiner does.

theorem Semantics.Definiteness.interpret_possessive_eq_viaModifier {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.possessive R possessor rel) g gs = russellIota fun (x : Intensional.Denot E W Intensional.Ty.e) => Possessive.viaModifier (possessor g gs) (fun (y : Intensional.Denot E W Intensional.Ty.e) (x : PUnit.{u_1 + 1}) => R g gs y) (fun (a b : Intensional.Denot E W Intensional.Ty.e) (x : PUnit.{u_1 + 1}) => rel g gs a b) x PUnit.unit

The possessive determiner's restrictor is Barker's Possessive.viaModifier (π of the noun predicate R and the possession relation rel): the Definiteness and Possessive encodings select through the same construction, by construction.

theorem Semantics.Definiteness.Possessive.denote_isSome_iff_iotaPresupposition {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (p : Possessive) : ((p.denote R possessor rel).selector (g, gs) PUnit.unit).isSome = true ↔ ArgumentStructure.Relational.iotaPresupposition (fun (x : Intensional.Denot E W Intensional.Ty.e) (x_1 : PUnit.{u_2 + 1}) => R g gs x ∧ rel g gs (possessor g gs) x) PUnit.unit

The possessive determiner's definedness presupposition is the carrier API's Russellian iota-presupposition (HasIotaWitness's condition).

def Semantics.Definiteness.Possessive.toCarrier {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (h : ArgumentStructure.Relational.iotaPresupposition (fun (x : Intensional.Denot E W Intensional.Ty.e) (x_1 : PUnit.{u_1 + 1}) => R g gs x ∧ rel g gs (possessor g gs) x) PUnit.unit) : Possessive.Definite E PUnit.{u_2 + 1}

At a context where its presupposition holds, the possessive determiner assembles into a Possessive.Definite carrier (over the trivial situation) whose possessee predicate is the determiner's restrictor.

Equations

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

theorem Semantics.Definiteness.Possessive.toCarrier_existsUnique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (h : ArgumentStructure.Relational.iotaPresupposition (fun (x : Intensional.Denot E W Intensional.Ty.e) (x_1 : PUnit.{u_1 + 1}) => R g gs x ∧ rel g gs (possessor g gs) x) PUnit.unit) : ∃! y : E, HasPossesseePredicate.possesseePredicate (toCarrier R possessor rel g gs h) y PUnit.unit

The carrier's unique possessee (existsUnique_possessee, inherited from HasIotaWitness) is the referent the determiner selects — the two encodings agree by construction.