The denotation of a determiner #
[schwarz-2009] [patel-grosz-grosz-2017] [coppock-beaver-2015] [moroney-2021]
Gives the determiner lexical records (Syntax/Category/Determiner/Basic.lean) meanings,
as Nominals — the determiner half of the API whose pronoun half is
Semantics/Reference/Pronoun.lean. The wiring is parallel:
| pronoun | determiner | |
|---|---|---|
| lexical record | PersonalPronoun | Article, DemonstrativeDeterminer |
| selector | interpPronoun (g ↦ g i) | 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'sNominal(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 toPersonalPronoun.phiPresup'sspeaker/addressee).DemonstrativeDeterminer.denote— the demonstrative'sNominal(previously deferred in the lexical file's implementation notes).Article.toDescriptions— an article's possible descriptions, the image of its admissible [schwarz-2009] strengths underDescription.ofPresupType.Article.denotations— an article's possibleNominals, the image ofArticle.toDescriptionsunderDescription.denote; a syncretic article (English the) denotes both the weak and the strong description.Possessive.denote— the possessive determiner'sNominal(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 inSemantics/Possession/Quantifier.lean.interpret_possessive_eq_pi,Possessive.denote_isSome_iff_existsUnique— the determiner denotation is thePossessiondescription: Barker'sπapplied to the possessor as restrictor, definedness as its presupposition.
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 Nominal) remains deferred.
Descriptions as nominal denotations #
A description's denotation as a Nominal: 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.
Instances For
The by-construction identity: a description's selector is interpret.
The demonstrative determiner's denotation #
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.
Instances For
A demonstrative determiner's denotation as a Nominal (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.
Instances For
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.
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 descriptions and denotations #
An article's possible (definite-description) denotations: the image of its
admissible [schwarz-2009] strengths (Article.presupTypes) under
Description.ofPresupType. A syncretic article (English the) denotes both
the weak and the strong description, not a single one.
Equations
- a.toDescriptions R idx = List.map (fun (x : Definiteness.DefPresupType) => Definiteness.Description.ofPresupType x R idx) a.presupTypes
Instances For
An article realizes the kind of each of its own possible descriptions:
the denotation pipeline (ofPresupType) and the inventory pipeline
(Determiner.Inventory.Realizes) coincide through kind_ofPresupType and
realizes_toKind.
An article's possible denotations: the Nominals 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 Definiteness.Description.denote (a.toDescriptions R idx)
Instances For
Every denotation of an article arises from a description whose kind the article realizes — the denotational pipeline and the inventory pipeline agree.
The possessive determiner's denotation #
A possessive determiner's denotation as a Nominal (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 Possession.PossW — (individual a) of
PossW reduces here when the possessor is an entity.
Equations
- _p.denote R possessor rel = (Definiteness.Description.possessive R possessor rel).denote
Instances For
A possessive determiner's selector is the possessive description's selector — the determiner picks the unique possessee related to the possessor by construction.
A possessive determiner realizes the kind of its own denotation — the
denotational pipeline and the inventory pipeline agree, parallel to
Article.denotations_realized.
Unification with the possessive description #
The possessive determiner's denotation (Description.possessive/russellIota) and the
Possession description are not two analyses — they are the same construction. The
determiner's restrictor is Barker's Possession.π of the noun predicate and the possession
relation, applied to the possessor, and its definedness presupposition is the description's
Russellian uniqueness condition.
The possessive determiner's restrictor is Barker's π of the noun predicate R
and the possession relation rel, applied to the possessor: the Definiteness and
Possession encodings select through the same construction, by construction.
The possessive determiner's definedness presupposition is the description's Russellian uniqueness condition.