Definiteness classifications

Framework-agnostic vocabulary for definiteness phenomena: types classifying definite descriptions, article systems, and presupposition types without committing to a particular semantic theory.

The organizing principle is DefPresupType — [Sch09b]'s binary between uniqueness and familiarity presuppositions. Every other type here is a dimension that maps into that distinction: description kinds (DescriptionKind), article inventories (ArticleType, [PGG17]), [Haw78]'s definite use types (DefiniteUseType, refined by [Sch13]), bridging subtypes (BridgingSubtype), and marking typology (DefMarkingStrategy, [Jen18] extended by [Mor21]). The [Hei82] novelty/familiarity contrast appears as the binary Definiteness. The denotational layer lives in Semantics/Definiteness/Basic.lean and Semantics/Definiteness/Description.lean.

The core binary distinction

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqDefPresupType : DecidableEq DefPresupType

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprDefPresupType : Repr DefPresupType

Equations

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

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

Equations

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

def Semantics.Definiteness.demonstrativePresupType : DefPresupType

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

Equations

• Semantics.Definiteness.demonstrativePresupType = Semantics.Definiteness.DefPresupType.familiarity

Description kinds

inductive Semantics.Definiteness.DescriptionKind : Type

The kinds of nominal description an inventory can realize — the Frame-free skeleton of Semantics.Definiteness.Description (one case per constructor, payload erased). Inventory questions (realization, marking typology) depend only on this kind, so they are stated over it rather than over the entity/index-parameterized Description.

• bare : DescriptionKind
• indefinite : DescriptionKind
• unique : DescriptionKind
• anaphoric : DescriptionKind
• demonstrative : DescriptionKind
• possessive : DescriptionKind

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqDescriptionKind : DecidableEq DescriptionKind

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprDescriptionKind : Repr DescriptionKind

Equations

• Semantics.Definiteness.instReprDescriptionKind = { reprPrec := Semantics.Definiteness.instReprDescriptionKind.repr }

def Semantics.Definiteness.instReprDescriptionKind.repr : DescriptionKind → Nat → Std.Format

Equations

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

def Semantics.Definiteness.DefPresupType.toKind : DefPresupType → DescriptionKind

The description kind realizing a [Sch09b] article strength: the weak article (uniqueness) realizes unique, the strong article (familiarity) realizes anaphoric. The Frame-free counterpart of Semantics.Definiteness.Description.ofPresupType.

Equations

• Semantics.Definiteness.DefPresupType.uniqueness.toKind = Semantics.Definiteness.DescriptionKind.unique
• Semantics.Definiteness.DefPresupType.familiarity.toKind = Semantics.Definiteness.DescriptionKind.anaphoric

def Semantics.Definiteness.DescriptionKind.IsDefinite : DescriptionKind → Prop

The kind is a definite description (in the broad sense — uniqueness, familiarity, demonstrative, or possessive).

Equations

• Semantics.Definiteness.DescriptionKind.bare.IsDefinite = False
• Semantics.Definiteness.DescriptionKind.indefinite.IsDefinite = False
• Semantics.Definiteness.DescriptionKind.unique.IsDefinite = True
• Semantics.Definiteness.DescriptionKind.anaphoric.IsDefinite = True
• Semantics.Definiteness.DescriptionKind.demonstrative.IsDefinite = True
• Semantics.Definiteness.DescriptionKind.possessive.IsDefinite = True

@[instance_reducible]

instance Semantics.Definiteness.DescriptionKind.instDecidablePredIsDefinite : DecidablePred IsDefinite

Equations

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

def Semantics.Definiteness.DescriptionKind.IsAnaphoric : DescriptionKind → Prop

The kind requires a discourse antecedent: anaphoric and demonstrative do; unique, possessive, bare, and indefinite do not.

Equations

• Semantics.Definiteness.DescriptionKind.anaphoric.IsAnaphoric = True
• Semantics.Definiteness.DescriptionKind.demonstrative.IsAnaphoric = True
• x✝.IsAnaphoric = False

@[instance_reducible]

instance Semantics.Definiteness.DescriptionKind.instDecidablePredIsAnaphoric : DecidablePred IsAnaphoric

Equations

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

def Semantics.Definiteness.DescriptionKind.UsesSituationPronoun : DescriptionKind → Prop

The kind binds a structural situation pronoun: Coppock–Beaver uniqueness and demonstratives do (resource situation for maximality and the deictic check); the other kinds do not.

Equations

• Semantics.Definiteness.DescriptionKind.unique.UsesSituationPronoun = True
• Semantics.Definiteness.DescriptionKind.demonstrative.UsesSituationPronoun = True
• x✝.UsesSituationPronoun = False

@[instance_reducible]

instance Semantics.Definiteness.DescriptionKind.instDecidablePredUsesSituationPronoun : DecidablePred UsesSituationPronoun

Equations

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

def Semantics.Definiteness.DescriptionKind.presupType : DescriptionKind → Option DefPresupType

The [Sch09b]–[Sch13] presupposition type a kind expresses, where applicable. Bare and indefinite return none because they are not (in themselves) definites.

Equations

• Semantics.Definiteness.DescriptionKind.bare.presupType = none
• Semantics.Definiteness.DescriptionKind.indefinite.presupType = none
• Semantics.Definiteness.DescriptionKind.unique.presupType = some Semantics.Definiteness.DefPresupType.uniqueness
• Semantics.Definiteness.DescriptionKind.possessive.presupType = some Semantics.Definiteness.DefPresupType.uniqueness
• Semantics.Definiteness.DescriptionKind.anaphoric.presupType = some Semantics.Definiteness.DefPresupType.familiarity
• Semantics.Definiteness.DescriptionKind.demonstrative.presupType = some Semantics.Definiteness.DefPresupType.familiarity

theorem Semantics.Definiteness.DescriptionKind.isDefinite_iff_presupType_isSome (k : DescriptionKind) : k.IsDefinite ↔ k.presupType.isSome = true

Definites are exactly the kinds with a presupposition type.

theorem Semantics.Definiteness.DescriptionKind.IsAnaphoric.presupType_familiarity {k : DescriptionKind} (h : k.IsAnaphoric) : k.presupType = some DefPresupType.familiarity

Anaphoric kinds all carry the familiarity presupposition type.

theorem Semantics.Definiteness.DescriptionKind.presupType_toKind (p : DefPresupType) : p.toKind.presupType = some p

toKind recovers its strength through presupType: the round-trip of DefPresupType.toKind.

Article types

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqArticleType : DecidableEq ArticleType

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprArticleType : Repr ArticleType

Equations

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

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

Equations

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

def Semantics.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.
• Semantics.Definiteness.articleTypeToDistinguishedPresup Semantics.Definiteness.ArticleType.none_ = []
• Semantics.Definiteness.articleTypeToDistinguishedPresup Semantics.Definiteness.ArticleType.weakOnly = [Semantics.Definiteness.DefPresupType.uniqueness]

theorem Semantics.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 Semantics.Definiteness.one_form_one_distinguished : (articleTypeToDistinguishedPresup ArticleType.weakOnly).length = 1

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

Definite use types

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqDefiniteUseType : DecidableEq DefiniteUseType

Equations

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

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

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprDefiniteUseType : Repr DefiniteUseType

Equations

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

def Semantics.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

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

Bridging subtypes

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqBridgingSubtype : DecidableEq BridgingSubtype

Equations

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

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

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprBridgingSubtype : Repr BridgingSubtype

Equations

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

def Semantics.Definiteness.bridgingPresupType : BridgingSubtype → DefPresupType

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

Equations

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

Weak article strategies

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqWeakArticleStrategy : DecidableEq WeakArticleStrategy

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprWeakArticleStrategy : Repr WeakArticleStrategy

Equations

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

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

Equations

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

The indefinite–definite contrast

inductive Semantics.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

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqDefiniteness : DecidableEq Definiteness

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprDefiniteness : Repr Definiteness

Equations

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

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

Equations

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

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

Definiteness is a binary contrast.

Definiteness marking typology

inductive Semantics.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].

@[instance_reducible]

instance Semantics.Definiteness.instDecidableEqDefMarkingStrategy : DecidableEq DefMarkingStrategy

Equations

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

@[instance_reducible]

instance Semantics.Definiteness.instReprDefMarkingStrategy : Repr DefMarkingStrategy

Equations

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

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

Equations

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

def Semantics.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.Inventory.markingStrategy. This function records only the cross-typology coarsening relation (Moroney's 4-cell strategy → Schwarz's 3-cell ArticleType).

Equations

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

theorem Semantics.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.