Nominal Descriptions: Unified Sum Type

[CB15] [PGG17] [Han21] [Mor21] [Sch09b] [Sch13] [Sha80] [Kri15b]

A single sum type Description E W covering the principal flavors of nominal description that the syntax–semantics interface needs to distinguish:

• bare noun (number-neutral; covert type-shifts decide the reading)
• indefinite (∃; introduces a new discourse referent)
• unique (Coppock–Beaver weak/uniqueness; Sharvy/Križ maximal)
• anaphoric (Schwarz strong-article familiarity; Hanink-indexed; PG&G's German der)
• demonstrative (genuinely deictic this/that: a deictic feature, distinct from the strong article)
• possessive (definite via a possession relation)

The whole type is parameterized by entity and index types E/W, so all restrictors, situation pronouns, and possessor expressions are typed via the unified Denot E W machinery rather than ad-hoc E → Bool predicates.

Design notes

• Restrictors are DenotGS E W .et. Both entity assignments and situation assignments are first-class. This is the [Han21] position: a noun's resource situation is a bound variable in the structure, not a free contextual parameter.

• unique carries a situation-pronoun index. Weak-article ([CB15] uniqueness) definites are evaluated at a structurally-bound situation, the situationIdx-th situation pronoun retrievable via interpSitPronoun situationIdx gs.

• anaphoric carries a discourse index. [Sch09b] strong-article and [Han21] anaphoric definites point to a discourse referent, the discourseIdx-th entity slot. This is the entity assignment's role.

• demonstrative is a separate constructor for genuinely deictic demonstratives (this/that; [Mor21] Shan nâj/nân): it carries both a discourse/pointing index and a deictic feature (Features.Deixis.Feature), checked at a situation pronoun. This is distinct from the [Sch09b] strong article (anaphoric): [PGG17] analyze German der as the strong article (anaphoric), not as a deictic demonstrative — their footnote 1 doubts der is truly demonstrative at all.

• possessive carries possessor + relation expressions rather than conflating them with the restrictor. The relation has type e ⇒ e ⇒ t, and the possessor is an e-type expression that may itself be derived from a Description higher in the structure.

• Reuses Features.Deixis.Feature for the deictic content, so Shan/English/Latin/German fragments share the same enum.

• No semantic interpretation here. This file only declares the type and its Frame-free kind projection (classification predicates live on Semantics.Definiteness.DescriptionKind). The interpretation function lives in Semantics/Definiteness/Interpret.lean.

inductive Semantics.Definiteness.Description (E W : Type) : Type

Principal flavors of nominal description — the definiteness/reference axis (bare/indefinite vs the definite subtypes), orthogonal to Features.BindingClass (binding distribution) and to a pronoun's lexical kind. The type parameters E/W supply the entity domain and index set so all subexpressions live in the same Denot E W universe.

• bare {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) : Description E W

  Bare noun (no overt determiner). The actual reading — kind, indefinite, unique, or anaphoric — is selected by the language's covert type-shift hierarchy ([Chi98], [Day04]).

• indefinite {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) : Description E W

  Overt-article indefinite (∃): a marked indefinite (English a). Introduces a new discourse referent and presupposes nothing about prior discourse ([Hei82]/Kamp novelty). Article-less languages express indefinite readings through bare (the type-shift hierarchy selects ∃), not this constructor.

• unique {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (situationIdx : ℕ) : Description E W

  Coppock–Beaver weak/uniqueness definite (Sharvy/Križ maximal). The restrictor is evaluated at the resource situation pointed to by the situationIdx-th situation pronoun (Hanink 2021 binding).

• anaphoric {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (discourseIdx : ℕ) : Description E W

  Schwarz strong-article / Hanink-indexed anaphoric definite. The discourseIdx-th entity-assignment slot is the antecedent.

• demonstrative {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (deictic : Features.Deixis.Feature) (situationIdx discourseIdx : ℕ) : Description E W

  Demonstrative (genuinely deictic this/that). Carries a deictic feature ([Mor21] Shan nâj/nân) and a discourse/pointing index; the restrictor is checked at the resource situation situationIdx. Distinct from the [Sch09b] strong article anaphoric (PG&G's German der).

• possessive {E W : Type} (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (relation : Intensional.Variables.DenotGS E W Intensional.Ty.eet) : Description E W

  Definite description via a possession relation: ⟦the N of x⟧ where the restrictor and relation jointly pin down a unique satisfier related to possessor.

def Semantics.Definiteness.Description.kind {E W : Type} : Description E W → DescriptionKind

The Frame-free kind of a description: its constructor with payload erased (Semantics.Definiteness.DescriptionKind). Inventory questions (Determiner.Inventory.Realizes, marking typology) depend only on this.

Equations

• (Semantics.Definiteness.Description.bare restrictor).kind = Semantics.Definiteness.DescriptionKind.bare
• (Semantics.Definiteness.Description.indefinite restrictor).kind = Semantics.Definiteness.DescriptionKind.indefinite
• (Semantics.Definiteness.Description.unique restrictor situationIdx).kind = Semantics.Definiteness.DescriptionKind.unique
• (Semantics.Definiteness.Description.anaphoric restrictor discourseIdx).kind = Semantics.Definiteness.DescriptionKind.anaphoric
• (Semantics.Definiteness.Description.demonstrative restrictor deictic situationIdx discourseIdx).kind = Semantics.Definiteness.DescriptionKind.demonstrative
• (Semantics.Definiteness.Description.possessive restrictor possessor relation).kind = Semantics.Definiteness.DescriptionKind.possessive

def Semantics.Definiteness.Description.ofPresupType {E W : Type} (p : DefPresupType) (restrictor : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) : Description E W

The definite description for a [Sch09b] presupposition type: the weak article (uniqueness) is unique, the strong article (familiarity) is anaphoric. Any item carrying a DefPresupType — a determiner, a definite, or (per [PGG17]) a personal/demonstrative pronoun — denotes by ofPresupType and recovers its strength through the Frame-free kind (kind_ofPresupType + DescriptionKind.presupType_toKind).

idx is the strong article's anaphoric/discourse index; for the weak article it fills the situation-pronoun slot, which interpret discards (interpret_unique_index_irrelevant).

Equations

• Semantics.Definiteness.Description.ofPresupType Semantics.Definiteness.DefPresupType.uniqueness restrictor idx = Semantics.Definiteness.Description.unique restrictor idx
• Semantics.Definiteness.Description.ofPresupType Semantics.Definiteness.DefPresupType.familiarity restrictor idx = Semantics.Definiteness.Description.anaphoric restrictor idx

theorem Semantics.Definiteness.Description.kind_ofPresupType {E W : Type} (p : DefPresupType) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) : (ofPresupType p R idx).kind = p.toKind

ofPresupType constructs the description whose kind is the strength's kind (DefPresupType.toKind) — the Frame-aware and Frame-free realization maps agree.