The denotation of a determiner

The determiner records of Syntax/Category/Determiner/Basic.lean denote Nominals, in parallel with the pronouns of Semantics/Reference/Pronoun.lean:

	pronoun	determiner
lexical record	PersonalPronoun	Article, DemonstrativeDeterminer
selector	interpPronoun (g ↦ g i)	⟦k⟧ for a Description k
intrinsic presupposition	φ-domain (phiDom)	vicinity of the anchors (χ.image)

The selector is the description's denotation, so a determiner and its description pick the same individual by construction. A demonstrative's deictic content projects as its intrinsic presupposition, so deixis filters the referent but never selects it (DemonstrativeDeterminer.denote_selector_eq_anaphoric). Following Harbour's spatial head χ, the presupposition is that the referent lies in the vicinity of a referent whose participants form one of the demonstrative's participant sets: the χ-image of the preimage of those sets under Reference.Context.participants. For the first person's sets that preimage is the first person's φ-domain, and for the other persons' sets it is their φ-domain less the more prominent ones'.

Main declarations

• Description.toNominal: a description's Nominal, with vacuous intrinsic presupposition.
• DemonstrativeDeterminer.denote: the demonstrative's Nominal.
• Article.toDescriptions, Article.denotations: an article's possible descriptions, one per admissible strength, and their Nominals; a syncretic article (English the) denotes both the weak and the strong description.
• PossessiveDeterminer.denote: the possessive determiner's Nominal, the unique satisfier of the possessee restrictor that stands in the possession relation to the possessor.

Implementation notes

Context is the entity assignment Assignment E and the world coordinate is the resource situation W, as for PersonalPronoun.denote. A demonstrative also reads the context of utterance, whose agent and addressee fix the participants of a referent, and a vicinity relation χ : SetRel E E. Harbour leaves the anchoring referent free; the presupposition closes it existentially, his reading of English here as the vicinity of any group containing the speaker. A demonstrative without a deictic contrast covers every participant set and so presupposes only that its referent lies in some vicinity: its deictic centre is the whole discourse space, as Terenghi puts it. Harbour's (16) and Moroney's (147)–(148) put the deictic condition inside the restriction, where it can select among the restrictor's satisfiers; here it is a presupposition on the indexed referent of the strong-article description, and the two coincide whenever the index supplies a referent that meets the condition. Distance, visibility and elevation, which cross-cut the person cells, are not modeled. Quantifier, a generalized quantifier rather than an individual denotation, has no Nominal.

References

• [Sch09b]
• [CB15]
• [Mor21]
• [Har16a]
• [Ter23]

Descriptions as nominal denotations

noncomputable def Reference.Description.toNominal {E W : Type} (k : Description E W) : Nominal (Assignment E) W E

A description denotes the Nominal whose selector is its denotation and whose intrinsic presupposition is vacuous, a definite's only presupposition being that the selector is defined.

Equations

• k.toNominal = { presup := fun (x : Assignment E) (x_1 : W) => True, selector := Semantics.Denotes.denote k }

@[simp]

theorem Reference.Description.toNominal_selector {E W : Type} (k : Description E W) : k.toNominal.selector = Semantics.Denotes.denote k

@[simp]

theorem Reference.Description.toNominal_presup {E W : Type} (k : Description E W) (g : Assignment E) (s : W) : k.toNominal.presup g s = True

The demonstrative determiner's denotation

noncomputable def DemonstrativeDeterminer.denote {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) (dem : DemonstrativeDeterminer) : Reference.Nominal (Assignment E) W E

A demonstrative determiner denotes the Nominal whose selector is the demonstrative description at discourse index d and whose intrinsic presupposition is that the indexed referent g d lies in the vicinity of a referent whose participants form one of its participant sets.

Equations

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

@[instance_reducible]

noncomputable instance Reference.instDenotesDemonstrativeDeterminerForallForallForallForallForallPartialOrderForallRestrictorForallNatForallContextForallSetRelNominalAssignment : Semantics.Denotes DemonstrativeDeterminer ((E W P T : Type) → [PartialOrder E] → Restrictor E W → ℕ → Context W E P T → SetRel E E → Nominal (Assignment E) W E)

A demonstrative determiner denotes on every model, the restrictor, the index, the context of utterance and the vicinity relation being the Reader arguments of its domain.

Equations

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

@[simp]

theorem DemonstrativeDeterminer.denote_presup {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) (dem : DemonstrativeDeterminer) (g : Assignment E) (s : W) : (denote R d c χ dem).presup g s ↔ ∃ (x : E), c.participants x ∈ dem.deixis ∧ (x, g d) ∈ χ

A demonstrative determiner presupposes that its referent lies in the vicinity of a referent whose participants form one of its participant sets.

theorem DemonstrativeDeterminer.denote_presup_mono {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) {dem₁ dem₂ : DemonstrativeDeterminer} (h : dem₁.deixis ⊆ dem₂.deixis) {g : Assignment E} {s : W} (hp : (denote R d c χ dem₁).presup g s) : (denote R d c χ dem₂).presup g s

A demonstrative with fewer participant sets presupposes more.

theorem DemonstrativeDeterminer.denote_presup_or_iff_of_compl {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) {dem₁ dem₂ : DemonstrativeDeterminer} (h : dem₂.deixis = dem₁.deixisᶜ) (g : Assignment E) (s : W) : (denote R d c χ dem₁).presup g s ∨ (denote R d c χ dem₂).presup g s ↔ ∃ (x : E), (x, g d) ∈ χ

Two demonstratives with complementary participant sets together cover the vicinity of every referent.

theorem DemonstrativeDeterminer.denote_selector_eq_anaphoric {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) (dem : DemonstrativeDeterminer) : (denote R d c χ dem).selector = (Reference.Description.anaphoric R d).toNominal.selector

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

theorem DemonstrativeDeterminer.denote_selector_congr {E W : Type} (R : Reference.Restrictor E W) (d : ℕ) {P T : Type} [PartialOrder E] (c : Reference.Context W E P T) (χ : SetRel E E) (dem₁ dem₂ : DemonstrativeDeterminer) : (denote R d c χ dem₁).selector = (denote R d c χ dem₂).selector

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

The article's descriptions and denotations

def Article.toDescriptions {E W : Type} (a : Article) (R : Reference.Restrictor E W) (idx : ℕ) : Set (Reference.Description E W)

The descriptions an article can denote are the images of its admissible [Sch09b] strengths under Description.ofStrength. A syncretic article such as English the denotes both the weak and the strong description.

Equations

• a.toDescriptions R idx = (fun (x : Reference.Description.Strength) => Reference.Description.ofStrength x R idx) '' ↑a.strengths

theorem Article.realizes_of_mem_toDescriptions {E W : Type} (R : Reference.Restrictor E W) (a : Article) (idx : ℕ) (k : Reference.Description E W) (hk : k ∈ a.toDescriptions R idx) : Determiner.Inventory.Realizes [Determiner.Entry.article a] k.kind

An article realizes the kind of each of its own descriptions, so the denotation pipeline through Description.ofStrength and the inventory pipeline through Determiner.Inventory.Realizes coincide.

def Article.denotations {E W : Type} (a : Article) (R : Reference.Restrictor E W) (idx : ℕ) : Set (Reference.Nominal (Assignment E) W E)

The Nominals an article can denote are those of its descriptions.

Equations

• a.denotations R idx = Reference.Description.toNominal '' a.toDescriptions R idx

@[instance_reducible]

noncomputable instance Reference.instDenotesArticleForallForallForallRestrictorForallNatSetNominalAssignment : Semantics.Denotes Article ((E W : Type) → Restrictor E W → ℕ → Set (Nominal (Assignment E) W E))

An article denotes the set of its readings on every model, the restrictor and the index being the Reader arguments of its domain.

Equations

• Reference.instDenotesArticleForallForallForallRestrictorForallNatSetNominalAssignment = { denote := fun (a : Article) (x x_1 : Type) => a.denotations }

theorem Article.denotations_realized {E W : Type} (R : Reference.Restrictor E W) (a : Article) (idx : ℕ) (nd : Reference.Nominal (Assignment E) W E) (h : nd ∈ a.denotations R idx) : ∃ (k : Reference.Description E W), Determiner.Inventory.Realizes [Determiner.Entry.article a] k.kind ∧ nd = k.toNominal

Every denotation of an article arises from a description whose kind the article realizes.

The possessive determiner's denotation

noncomputable def PossessiveDeterminer.denote {E W : Type} (R : Reference.Restrictor E W) (possessor : Assignment E → W → E) (rel : Assignment E → W → E → E → Prop) (_p : PossessiveDeterminer) : Reference.Nominal (Assignment E) W E

A possessive determiner denotes the Nominal of the definite description selecting the unique satisfier of the possessee restrictor R that stands in rel to the possessor, the Description.possessive selector (iota 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 Possession.PossNP — (individual a) of PossNP reduces here when the possessor is an entity.

Equations

• PossessiveDeterminer.denote R possessor rel _p = (Reference.Description.possessive R possessor rel).toNominal

@[instance_reducible]

noncomputable instance Reference.instDenotesPossessiveDeterminerForallForallForallRestrictorForallForallAssignmentForallForallForallForallForallForallPropNominal : Semantics.Denotes PossessiveDeterminer ((E W : Type) → Restrictor E W → (Assignment E → W → E) → (Assignment E → W → E → E → Prop) → Nominal (Assignment E) W E)

A possessive determiner denotes on every model, the restrictor, the possessor and the possession relation being the Reader arguments of its domain.

Equations

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

@[simp]

theorem PossessiveDeterminer.denote_selector {E W : Type} (R : Reference.Restrictor E W) (possessor : Assignment E → W → E) (rel : Assignment E → W → E → E → Prop) (p : PossessiveDeterminer) : (denote R possessor rel p).selector = Semantics.Denotes.denote (Reference.Description.possessive R possessor rel)

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

theorem PossessiveDeterminer.denote_realized {E W : Type} (R : Reference.Restrictor E W) (possessor : Assignment E → W → E) (rel : Assignment E → W → E → E → Prop) (p : PossessiveDeterminer) : Determiner.Inventory.Realizes [Determiner.Entry.possessive p] (Reference.Description.possessive R possessor rel).kind

A possessive determiner realizes the kind of its own denotation — the denotational pipeline and the inventory pipeline agree, parallel to Article.denotations_realized.