Definiteness: Types and Classifications

[Don66] [Haw78] [Hei82] [PGG17] [Sch09b] [Sch13]

Framework-agnostic vocabulary for definiteness phenomena. These types classify definite descriptions, article systems, and presupposition types without committing to any particular semantic theory.

The organizing principle is DefPresupType (.uniqueness |.familiarity) — every other type in this module is a dimension that maps into this binary distinction: article morphology, pragmatic use type, bridging relation, etc.

Used by:

• Semantics.Montague/Determiner/Definite.lean (denotations: ⟦the⟧)
• Studies/Schwarz2009.lean (weak/strong articles, donkey anaphora)
• Studies/Moroney2021.lean (bridging subtypes)

inductive Features.Definiteness.DefPresupType : Type

The two presupposition types underlying definite descriptions.

[Sch09b]: these correspond to two morphologically distinct articles in languages like German, Fering, Lakhota, and Akan. Every classification in this module ultimately maps into this binary type.

• uniqueness : DefPresupType
• familiarity : DefPresupType

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqDefPresupType : DecidableEq DefPresupType

Equations

• Features.Definiteness.instDecidableEqDefPresupType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Definiteness.instReprDefPresupType : Repr DefPresupType

Equations

• Features.Definiteness.instReprDefPresupType = { reprPrec := Features.Definiteness.instReprDefPresupType.repr }

def Features.Definiteness.instReprDefPresupType.repr : DefPresupType → Nat → Std.Format

Equations

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

def Features.Definiteness.demonstrativePresupType : DefPresupType

Demonstratives (this/that) project D_deix — the familiarity/strong-article layer. [Sch13] §5.5 and [PGG17].

Equations

• Features.Definiteness.demonstrativePresupType = Features.Definiteness.DefPresupType.familiarity

inductive Features.Definiteness.ArticleType : Type

[Sch09b]: article type in the D-domain.

Schwarz argues for two structurally distinct definite articles:

• Weak: situational uniqueness
• Strong: anaphoric familiarity

[PGG17] build on this: ArticleType predicts D-layer count and whether DEM pronouns exist.

• none_ : ArticleType
• weakOnly : ArticleType
• weakAndStrong : ArticleType

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqArticleType : DecidableEq ArticleType

Equations

• Features.Definiteness.instDecidableEqArticleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Definiteness.instReprArticleType.repr : ArticleType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Definiteness.instReprArticleType : Repr ArticleType

Equations

• Features.Definiteness.instReprArticleType = { reprPrec := Features.Definiteness.instReprArticleType.repr }

def Features.Definiteness.articleTypeToDistinguishedPresup : ArticleType → List DefPresupType

Which presupposition types are morphologically distinguished by a language's article system. This tracks overt marking, not semantic availability: a language with no articles (.none_) morphologically distinguishes zero presupposition types, but may still express both uniqueness and familiarity via covert type-shifting (e.g., Shan bare nouns; [Mor21]). Semantic availability of presupposition types is determined by the blocking principle and type-shift hierarchy ([Day04]), not by article inventory alone.

Equations

• One or more equations did not get rendered due to their size.
• Features.Definiteness.articleTypeToDistinguishedPresup Features.Definiteness.ArticleType.none_ = []
• Features.Definiteness.articleTypeToDistinguishedPresup Features.Definiteness.ArticleType.weakOnly = [Features.Definiteness.DefPresupType.uniqueness]

theorem Features.Definiteness.two_forms_two_distinguished : (articleTypeToDistinguishedPresup ArticleType.weakAndStrong).length = 2

Languages with two article forms morphologically distinguish both presupposition types. This is [PGG17]'s structural claim: 2 D-layers = 2 morphologically distinct presupposition signals.

theorem Features.Definiteness.one_form_one_distinguished : (articleTypeToDistinguishedPresup ArticleType.weakOnly).length = 1

Languages with one article form morphologically distinguish one presupposition type (modulo ambiguity).

inductive Features.Definiteness.DefiniteUseType : Type

[Haw78]'s four use types for definite descriptions. [Sch13] shows these map systematically onto weak vs strong articles.

• anaphoric : DefiniteUseType
• immediateSituation : DefiniteUseType
• largerSituation : DefiniteUseType
• bridging : DefiniteUseType
• donkey : DefiniteUseType

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqDefiniteUseType : DecidableEq DefiniteUseType

Equations

• Features.Definiteness.instDecidableEqDefiniteUseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Definiteness.instReprDefiniteUseType : Repr DefiniteUseType

Equations

• Features.Definiteness.instReprDefiniteUseType = { reprPrec := Features.Definiteness.instReprDefiniteUseType.repr }

def Features.Definiteness.instReprDefiniteUseType.repr : DefiniteUseType → Nat → Std.Format

Equations

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

def Features.Definiteness.useTypeToPresupType : DefiniteUseType → DefPresupType

Map definite use type to presupposition type ([Sch13] §3.1).

Anaphoric uses require the strong article (familiarity); situational uses require the weak article (uniqueness).

Equations

• Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.anaphoric = Features.Definiteness.DefPresupType.familiarity
• Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.immediateSituation = Features.Definiteness.DefPresupType.uniqueness
• Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.largerSituation = Features.Definiteness.DefPresupType.uniqueness
• Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.bridging = Features.Definiteness.DefPresupType.uniqueness
• Features.Definiteness.useTypeToPresupType Features.Definiteness.DefiniteUseType.donkey = Features.Definiteness.DefPresupType.familiarity

inductive Features.Definiteness.BridgingSubtype : Type

Bridging subtypes ([Sch13] §3.2). German and Fering show that bridging splits across the two article forms:

• Part-whole bridging → weak article (situational uniqueness)
• Relational bridging → strong article (anaphoric link)

Schwarz's "producer bridging" (e.g., "the play... the author") is the prototypical case of relational bridging.

• partWhole : BridgingSubtype
• relational : BridgingSubtype

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqBridgingSubtype : DecidableEq BridgingSubtype

Equations

• Features.Definiteness.instDecidableEqBridgingSubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Definiteness.instReprBridgingSubtype.repr : BridgingSubtype → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Definiteness.instReprBridgingSubtype : Repr BridgingSubtype

Equations

• Features.Definiteness.instReprBridgingSubtype = { reprPrec := Features.Definiteness.instReprBridgingSubtype.repr }

def Features.Definiteness.bridgingPresupType : BridgingSubtype → DefPresupType

Map bridging subtype to presupposition type ([Sch13] §3.2).

Equations

• Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.partWhole = Features.Definiteness.DefPresupType.uniqueness
• Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.relational = Features.Definiteness.DefPresupType.familiarity

inductive Features.Definiteness.WeakArticleStrategy : Type

How a language expresses the weak/strong article contrast.

[Sch13] surveys languages along two dimensions:

• How many overt article forms? (0, 1, or 2)
• What expresses weak-article definites? (bare nominal, overt article, etc.)

• bareNominal : WeakArticleStrategy
• overtArticle : WeakArticleStrategy
• sameAsStrong : WeakArticleStrategy

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqWeakArticleStrategy : DecidableEq WeakArticleStrategy

Equations

• Features.Definiteness.instDecidableEqWeakArticleStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Definiteness.instReprWeakArticleStrategy.repr : WeakArticleStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Definiteness.instReprWeakArticleStrategy : Repr WeakArticleStrategy

Equations

• Features.Definiteness.instReprWeakArticleStrategy = { reprPrec := Features.Definiteness.instReprWeakArticleStrategy.repr }

inductive Features.Definiteness.Definiteness : Type

The fundamental semantic contrast between indefinite and definite:

• Indefinite (some/a): existential quantification, no presupposition on prior discourse. Introduces a NEW discourse referent.
• Definite (the): presupposes existence (+ uniqueness or familiarity). Retrieves an EXISTING referent.

[Hei82]: indefinites are novel, definites are familiar. This is the dynamic semantics version of the ∃/ι contrast.

• indefinite : Definiteness
• definite : Definiteness

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqDefiniteness : DecidableEq Definiteness

Equations

• Features.Definiteness.instDecidableEqDefiniteness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Definiteness.instReprDefiniteness : Repr Definiteness

Equations

• Features.Definiteness.instReprDefiniteness = { reprPrec := Features.Definiteness.instReprDefiniteness.repr }

def Features.Definiteness.instReprDefiniteness.repr : Definiteness → Nat → Std.Format

Equations

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

theorem Features.Definiteness.definite_indefinite_exhaustive (d : Definiteness) : d = Definiteness.indefinite ∨ d = Definiteness.definite

Definiteness is a binary contrast.

inductive Features.Definiteness.DefMarkingStrategy : Type

Cross-linguistic strategy for marking definiteness, following [Jen18]'s typology extended by [Mor21] with the .unmarked category.

The original [Jen18] typology had four cells (2×2: both-marked × same/different + one-marked × unique/anaphoric), but "one-marked, unique" was unattested. [Mor21] adds a fifth: neither type is obligatorily marked, yet both are expressible via bare nouns. This captures Shan, Serbian, and Kannada.

This is strictly finer than ArticleType: .generallyMarked and .markedAnaphoric both map to ArticleType.weakOnly, so ArticleType collapses a real distinction.

• generallyMarked : DefMarkingStrategy

  Both unique and anaphoric definiteness are marked with the same form. Languages: English (the), Cantonese.

• bipartite : DefMarkingStrategy

  Unique and anaphoric definiteness are marked with different forms. Languages: German (weak/strong articles), Lakhota.

• markedAnaphoric : DefMarkingStrategy

  Only anaphoric definiteness is obligatorily marked (via demonstrative). Unique definiteness is expressed with bare nouns. Languages: Mandarin, Akan, Wu.

• unmarked : DefMarkingStrategy

  Neither type is obligatorily marked. Bare nouns can express both unique and anaphoric definiteness. Demonstrative-noun phrases are optional in anaphoric contexts. Languages: Shan, Serbian, Kannada. NEW in [Mor21].

@[implicit_reducible]

instance Features.Definiteness.instDecidableEqDefMarkingStrategy : DecidableEq DefMarkingStrategy

Equations

• Features.Definiteness.instDecidableEqDefMarkingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Definiteness.instReprDefMarkingStrategy.repr : DefMarkingStrategy → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Definiteness.instReprDefMarkingStrategy : Repr DefMarkingStrategy

Equations

• Features.Definiteness.instReprDefMarkingStrategy = { reprPrec := Features.Definiteness.instReprDefMarkingStrategy.repr }

def Features.Definiteness.strategyToArticleType : DefMarkingStrategy → ArticleType

Map marking strategy to ArticleType. Lossy: .generallyMarked and .markedAnaphoric both map to .weakOnly.

Per-language strategy values are not stipulated here — they are derived from each language's declared determiner set via Determiner.markingStrategy. This function records only the cross-typology coarsening relation (Moroney's 4-cell strategy → Schwarz's 3-cell ArticleType).

Equations

• Features.Definiteness.strategyToArticleType Features.Definiteness.DefMarkingStrategy.generallyMarked = Features.Definiteness.ArticleType.weakOnly
• Features.Definiteness.strategyToArticleType Features.Definiteness.DefMarkingStrategy.bipartite = Features.Definiteness.ArticleType.weakAndStrong
• Features.Definiteness.strategyToArticleType Features.Definiteness.DefMarkingStrategy.markedAnaphoric = Features.Definiteness.ArticleType.weakOnly
• Features.Definiteness.strategyToArticleType Features.Definiteness.DefMarkingStrategy.unmarked = Features.Definiteness.ArticleType.none_

theorem Features.Definiteness.strategy_finer_than_articleType : strategyToArticleType DefMarkingStrategy.generallyMarked = strategyToArticleType DefMarkingStrategy.markedAnaphoric ∧ DefMarkingStrategy.generallyMarked ≠ DefMarkingStrategy.markedAnaphoric

The marking strategy typology is finer than ArticleType: .generallyMarked and .markedAnaphoric both map to .weakOnly, so ArticleType cannot distinguish them.