Determiner

The determiner (D head) as a lexical object, following the standard determiner taxonomy: Article, DemonstrativeDeterminer, Quantifier, and Possessive each extends the base Determiner. The base carries only what is universal to all determiners — a surface form; each specialization adds its own structure.

A language's determiner inventory is a Determiner.Inventory (a heterogeneous list of the four kinds) declared in its Fragment as {Lang}.Determiners.inventory — there is no per-language wrapper record. The [Mor21] definiteness-marking typology (DefMarkingStrategy) is derived from the inventory by Inventory.markingStrategy, not stipulated: a language's Moroney cell is a theorem about its declared determiners, checked by decide.

Because Article records its exponent, a classifier-phrase definite and a dedicated-article definite are both Articles differing only there, so a classifier language declares a definite and an indefinite Article symmetrically — the contested "is [Clf-N] a definite marker" question is localized to a single declaration.

Main declarations

• Determiner — the base D-head record (just form).
• Article, DemonstrativeDeterminer, Quantifier, Possessive — the four specializations.
• Determiner.Entry — a determiner occurrence in a language's inventory.
• Determiner.Inventory — a language's declared determiner inventory; the carrier of the inventory operations.
• Determiner.Inventory.markingStrategy — derives the [Mor21] 4-cell typology from a declared inventory.
• Determiner.Inventory.Realizes — morphological realization: the declared inventory carries a form for a given DescriptionKind.

Implementation notes

An Article's admissible [Sch09b] strengths are Article.presupTypes (Frame-free, read off uses); its denotation is Article.toDescriptions (Semantics/Definiteness/DeterminerDenotation.lean, Frame-aware) — the set of Descriptions those strengths admit via Description.ofPresupType, so a syncretic article like English the denotes both the weak and the strong description. (Semantics/Quantification), and the Possessive possession relation remain deferred; Quantifier/Possessive are declared but not fleshed out beyond form. This file stays the Frame-free lexical/typological layer.

inductive Determiner.Exponent : Type

How an article is morphosyntactically realized. Analysis-neutral: the distinction between a dedicated article morpheme and a classifier/numeral/ demonstrative construction is recorded here, not used to decide whether the form "counts" as marking definiteness — that is the uses field's job.

• dedicatedMorpheme : Exponent

  A dedicated article morpheme (English the/a, German der/ein).

• classifierPhrase : Exponent

  A bare classifier phrase (Cantonese [Clf-N] definite).

• numeralClassifier : Exponent

  A numeral-classifier phrase (Cantonese [jat-Clf-N] indefinite).

• demonstrativeForm : Exponent

  A demonstrative form doing definite duty (Mandarin na anaphoric).

• bareNoun : Exponent

  A bare noun whose reading is fixed by covert type-shift.

@[implicit_reducible]

instance Determiner.instDecidableEqExponent : DecidableEq Exponent

Equations

• Determiner.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Determiner.instReprExponent : Repr Exponent

Equations

• Determiner.instReprExponent = { reprPrec := Determiner.instReprExponent.repr }

def Determiner.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

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

structure Determiner : Type

The base determiner (D head): only what is universal to every determiner — a surface form. Specializations (Article, DemonstrativeDeterminer, Quantifier, Possessive) extends this.

• form : String

  Surface form (a representative morpheme or construction label).

def instDecidableEqDeterminer.decEq (x✝ x✝¹ : Determiner) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDeterminer.decEq { form := a } { form := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqDeterminer : DecidableEq Determiner

Equations

• instDecidableEqDeterminer = instDecidableEqDeterminer.decEq

def instReprDeterminer.repr : Determiner → ℕ → Std.Format

Equations

• instReprDeterminer.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "form" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.form)).group) " }"

@[implicit_reducible]

instance instReprDeterminer : Repr Determiner

Equations

• instReprDeterminer = { reprPrec := instReprDeterminer.repr }

structure Articleextends Determiner : Type

An article: the definite/indefinite determiner. uses is the definite use-types it obligatorily expones (empty for indefinites).

• form : String
• definiteness : Features.Definiteness.Definiteness

  Definite or indefinite.

• exponent : Determiner.Exponent

  How the article is realized.

• uses : List Features.Definiteness.DefiniteUseType

  The definite use-types this article obligatorily expones.

def instDecidableEqArticle.decEq (x✝ x✝¹ : Article) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqArticle : DecidableEq Article

Equations

• instDecidableEqArticle = instDecidableEqArticle.decEq

@[implicit_reducible]

instance instReprArticle : Repr Article

Equations

• instReprArticle = { reprPrec := instReprArticle.repr }

def instReprArticle.repr : Article → ℕ → Std.Format

Equations

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

structure DemonstrativeDeterminerextends Determiner : Type

A demonstrative determiner (this/that book). definiteUses is nonempty iff the demonstrative is the obligatory exponent of some definite use (Mandarin anaphoric); for a plain demonstrative that merely can be used deictically it is empty. The determiner carrier of the word-class-neutral Demonstrative deixis capability, sharing it with DemonstrativePronoun.

• form : String
• deictic : Features.Deixis.Feature

  Deictic feature (proximal/medial/distal/unspecified).

• definiteUses : List Features.Definiteness.DefiniteUseType

  Definite use-types this demonstrative obligatorily expones.

@[implicit_reducible]

instance instDecidableEqDemonstrativeDeterminer : DecidableEq DemonstrativeDeterminer

Equations

• instDecidableEqDemonstrativeDeterminer = instDecidableEqDemonstrativeDeterminer.decEq

def instDecidableEqDemonstrativeDeterminer.decEq (x✝ x✝¹ : DemonstrativeDeterminer) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instReprDemonstrativeDeterminer : Repr DemonstrativeDeterminer

Equations

• instReprDemonstrativeDeterminer = { reprPrec := instReprDemonstrativeDeterminer.repr }

def instReprDemonstrativeDeterminer.repr : DemonstrativeDeterminer → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instDemonstrativeDemonstrativeDeterminer : Demonstrative DemonstrativeDeterminer

The demonstrative determiner exposes its deictic field as the Demonstrative capability, shared word-class-neutrally with DemonstrativePronoun.

Equations

• instDemonstrativeDemonstrativeDeterminer = { deixis := DemonstrativeDeterminer.deictic }

structure Quantifierextends Determiner : Type

A quantificational determiner (every/some/most/no), marked like a Pronoun: a decidable lexical record carrying only what the meaning leaves open — the morphosyntactic idiosyncrasies on which synonymous determiners diverge. Its denotation is a generalized quantifier (Semantics/Quantification) supplied externally (the entry carries no GQ, exactly as Pronoun carries no referent); everything the meaning fixes — force, class, monotonicity, strength, conservativity — is a theorem about that denotation, not a field.

• form : String
• numberRestriction : Option Number

  Selectional number: the grammatical number the determiner combines with (every → singular, all/most → plural; none = number-neutral). Not fixed by the GQ — every and all can share a denotation yet differ here.

• selectsMass : Bool

  Selects mass NPs? (much/all do; every/both don't.) Likewise not fixed by the GQ.

def instDecidableEqQuantifier.decEq (x✝ x✝¹ : Quantifier) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqQuantifier : DecidableEq Quantifier

Equations

• instDecidableEqQuantifier = instDecidableEqQuantifier.decEq

def instReprQuantifier.repr : Quantifier → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprQuantifier : Repr Quantifier

Equations

• instReprQuantifier = { reprPrec := instReprQuantifier.repr }

structure Possessiveextends Determiner : Type

A possessive determiner (my/your/the boy's). Its denotation is definiteness via a possession relation; deferred.

• form : String

@[implicit_reducible]

instance instDecidableEqPossessive : DecidableEq Possessive

Equations

• instDecidableEqPossessive = instDecidableEqPossessive.decEq

def instDecidableEqPossessive.decEq (x✝ x✝¹ : Possessive) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPossessive.decEq { toDeterminer := a } { toDeterminer := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprPossessive : Repr Possessive

Equations

• instReprPossessive = { reprPrec := instReprPossessive.repr }

def instReprPossessive.repr : Possessive → ℕ → Std.Format

Equations

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

inductive Determiner.Entry : Type

A determiner occurrence in a language's inventory: one of the four kinds, carrying its typed payload.

• article (a : Article) : Entry
• demonstrative (d : DemonstrativeDeterminer) : Entry
• quantifier (q : Quantifier) : Entry
• possessive (p : Possessive) : Entry

def Determiner.instDecidableEqEntry.decEq (x✝ x✝¹ : Entry) : Decidable (x✝ = x✝¹)

Equations

• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.article b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative a) (Determiner.Entry.demonstrative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier a) (Determiner.Entry.quantifier b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive a) (Determiner.Entry.possessive b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Determiner.instDecidableEqEntry : DecidableEq Entry

Equations

• Determiner.instDecidableEqEntry = Determiner.instDecidableEqEntry.decEq

def Determiner.instReprEntry.repr : Entry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Determiner.instReprEntry : Repr Entry

Equations

• Determiner.instReprEntry = { reprPrec := Determiner.instReprEntry.repr }

def Determiner.Entry.definiteUses : Entry → List Features.Definiteness.DefiniteUseType

The definite use-types a determiner occurrence obligatorily expones. Only definite articles and (obligatory) demonstratives contribute; indefinite articles, quantifiers, and possessives expone none.

Equations

• (Determiner.Entry.article a).definiteUses = a.uses
• (Determiner.Entry.demonstrative a).definiteUses = a.definiteUses
• (Determiner.Entry.quantifier a).definiteUses = []
• (Determiner.Entry.possessive a).definiteUses = []

def Determiner.Inventory : Type

A language's declared determiner inventory — the per-language object a Fragment declares ({Lang}.Determiners.inventory) and the carrier of the inventory operations (markingStrategy, Realizes, …), which hang off it via dot notation. A def (not abbrev) so the operations resolve through the Inventory head constant.

Equations

• Determiner.Inventory = List Determiner.Entry

@[implicit_reducible]

instance Determiner.instMembershipEntryInventory : Membership Entry Inventory

Equations

• Determiner.instMembershipEntryInventory = { mem := Determiner.instMembershipEntryInventory._aux_1 }

@[implicit_reducible]

instance Determiner.instDecidableEqInventory : DecidableEq Inventory

Equations

• Determiner.instDecidableEqInventory = Determiner.instDecidableEqInventory._aux_1

@[implicit_reducible]

instance Determiner.instDecidableExistsEntryAndMemInventoryOfDecidablePred (ds : Inventory) (p : Entry → Prop) [DecidablePred p] : Decidable (∃ e ∈ ds, p e)

Equations

• Determiner.instDecidableExistsEntryAndMemInventoryOfDecidablePred ds p = List.decidableBEx p ds

Deriving the Moroney typology from a declared determiner set

def Determiner.Inventory.MarksPresup (ds : Inventory) (p : Features.Definiteness.DefPresupType) : Prop

The declared inventory obligatorily marks presupposition type p — some determiner expones a definite use whose presupposition is p.

Equations

• ds.MarksPresup p = ∃ e ∈ ds, ∃ u ∈ e.definiteUses, Features.Definiteness.useTypeToPresupType u = p

@[implicit_reducible]

instance Determiner.Inventory.instDecidableMarksPresup (ds : Inventory) (p : Features.Definiteness.DefPresupType) : Decidable (ds.MarksPresup p)

Equations

• ds.instDecidableMarksPresup p = id inferInstance

def Determiner.Inventory.IsSyncretic (ds : Inventory) : Prop

Some single determiner is the exponent of both presupposition types (English the). Distinguishes .generallyMarked (one form covers both) from .bipartite (German weak vs strong).

Equations

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

@[implicit_reducible]

instance Determiner.Inventory.instDecidableIsSyncretic (ds : Inventory) : Decidable ds.IsSyncretic

Equations

• ds.instDecidableIsSyncretic = id inferInstance

def Determiner.Inventory.markingStrategy (ds : Inventory) : Features.Definiteness.DefMarkingStrategy

Derive the [Mor21] four-cell definiteness-marking typology from a declared determiner inventory. Stored nowhere — a language's cell is a theorem about its Determiner.Inventory. Reproduces the decision table of the former boolean article inventory:

• uniqueness marked, familiarity marked, by one form → .generallyMarked
• uniqueness marked, familiarity marked, by distinct forms → .bipartite
• uniqueness marked, familiarity unmarked → .generallyMarked
• uniqueness unmarked, familiarity marked (e.g. via demonstrative) → .markedAnaphoric
• neither marked → .unmarked

Equations

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

def Determiner.Inventory.articleType (ds : Inventory) : Features.Definiteness.ArticleType

Derived Schwarz/Patel-Grosz–Grosz 3-cell ArticleType classification. Lossy: .generallyMarked and .markedAnaphoric both collapse to .weakOnly, as strategyToArticleType documents.

Equations

• ds.articleType = Features.Definiteness.strategyToArticleType ds.markingStrategy

Kind predicates over an inventory (for realization)

def Determiner.Entry.IsIndefiniteArticle : Entry → Prop

The occurrence is an indefinite article.

Equations

• (Determiner.Entry.article a).IsIndefiniteArticle = (a.definiteness = Features.Definiteness.Definiteness.indefinite)
• x✝.IsIndefiniteArticle = False

@[implicit_reducible]

instance Determiner.instDecidablePredEntryIsIndefiniteArticle : DecidablePred Entry.IsIndefiniteArticle

Equations

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

def Determiner.Entry.IsDemonstrative : Entry → Prop

The occurrence is a demonstrative.

Equations

• (Determiner.Entry.demonstrative d).IsDemonstrative = True
• x✝.IsDemonstrative = False

@[implicit_reducible]

instance Determiner.instDecidablePredEntryIsDemonstrative : DecidablePred Entry.IsDemonstrative

Equations

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

def Determiner.Entry.IsPossessive : Entry → Prop

The occurrence is a possessive.

Equations

• (Determiner.Entry.possessive p).IsPossessive = True
• x✝.IsPossessive = False

@[implicit_reducible]

instance Determiner.instDecidablePredEntryIsPossessive : DecidablePred Entry.IsPossessive

Equations

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

Realization: which description kinds the inventory has forms for

def Determiner.Inventory.Realizes (ds : Inventory) : Features.Definiteness.DescriptionKind → Prop

Morphological realization: the declared determiner inventory contains a form for the given kind of nominal description. Bare nominals need no determiner, so .bare is vacuously realized; unique and anaphoric definites need a determiner exponing the corresponding presupposition type (MarksPresup); indefinite/demonstrative/possessive need a determiner of that kind.

This is inventory data, not syntactic licensing — no structural relation between a licensor and licensee is modeled — and not expressibility or felicity: a kind can be expressed without a determiner realizing it (Shan anaphoric definites surface as bare nouns, [Mor21]), and which realized form a context selects (type-shift blocking, Index!, Maximize Presupposition) is downstream pragmatics ([Jen18], Studies/Jenks2018.lean).

Equations

• ds.Realizes Features.Definiteness.DescriptionKind.bare = True
• ds.Realizes Features.Definiteness.DescriptionKind.indefinite = ∃ e ∈ ds, e.IsIndefiniteArticle
• ds.Realizes Features.Definiteness.DescriptionKind.unique = ds.MarksPresup Features.Definiteness.DefPresupType.uniqueness
• ds.Realizes Features.Definiteness.DescriptionKind.anaphoric = ds.MarksPresup Features.Definiteness.DefPresupType.familiarity
• ds.Realizes Features.Definiteness.DescriptionKind.demonstrative = ∃ e ∈ ds, e.IsDemonstrative
• ds.Realizes Features.Definiteness.DescriptionKind.possessive = ∃ e ∈ ds, e.IsPossessive

@[implicit_reducible]

instance Determiner.Inventory.instDecidablePredDescriptionKindRealizes (ds : Inventory) : DecidablePred ds.Realizes

Equations

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

theorem Determiner.Inventory.realizes_toKind (ds : Inventory) (p : Features.Definiteness.DefPresupType) : ds.Realizes p.toKind ↔ ds.MarksPresup p

Realizing an article strength's kind is exactly marking that strength: the description-kind pipeline (DefPresupType.toKind) and the inventory pipeline (MarksPresup) coincide by construction.

Cell coverage: the derivation reproduces all four Moroney cells

Admissible article strengths

The [Sch09b] presupposition types an article can express — its admissible readings, read off uses. A syncretic article (English the) admits both; a weak- or strong-only article admits one. The image of these under Description.ofPresupType is the article's set of possible denotations (Article.toDescriptions, in DeterminerDenotation.lean).

def Article.presupTypes (a : Article) : List Features.Definiteness.DefPresupType

The [Sch09b] strengths an article admits, read off its uses (as a list — DefPresupType is binary, so its content is the membership-closure).

Equations

• a.presupTypes = List.map Features.Definiteness.useTypeToPresupType a.uses

theorem Article.mem_presupTypes_iff_marksPresup (a : Article) (p : Features.Definiteness.DefPresupType) : p ∈ a.presupTypes ↔ Determiner.Inventory.MarksPresup [Determiner.Entry.article a] p

An article admits strength p iff a one-article inventory containing it marks p — the single-article case of Determiner.Inventory.MarksPresup.