Documentation

Linglib.Core.Definiteness

Definiteness: Types and Classifications #

@cite{donnellan-1966} @cite{hawkins-1978} @cite{heim-1982} @cite{patel-grosz-grosz-2017} @cite{schwarz-2009} @cite{schwarz-2013}

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:

Theories/Semantics.Montague/Determiner/Definite.lean (denotations: ⟦the⟧)
Phenomena/Anaphora/PronounTypology.lean (cross-linguistic article data)
Phenomena/Anaphora/Bridging.lean (bridging presupposition types)

inductive Core.Definiteness.DefPresupType :

The two presupposition types underlying definite descriptions.

@cite{schwarz-2009}: 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

Instances For

instance Core.Definiteness.instDecidableEqDefPresupType :

DecidableEq DefPresupType

Equations

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

instance Core.Definiteness.instBEqDefPresupType :

BEq DefPresupType

Equations

Core.Definiteness.instBEqDefPresupType = { beq := Core.Definiteness.instBEqDefPresupType.beq }

def Core.Definiteness.instBEqDefPresupType.beq :

DefPresupType → DefPresupType → Bool

Equations

Core.Definiteness.instBEqDefPresupType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instReprDefPresupType :

Repr DefPresupType

Equations

Core.Definiteness.instReprDefPresupType = { reprPrec := Core.Definiteness.instReprDefPresupType.repr }

def Core.Definiteness.instReprDefPresupType.repr :

DefPresupType → Nat → Std.Format

Equations

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

Instances For

def Core.Definiteness.demonstrativePresupType :

Demonstratives (this/that) project D_deix — the familiarity/strong-article layer. @cite{schwarz-2013} §5.5 and @cite{patel-grosz-grosz-2017}.

Equations

Core.Definiteness.demonstrativePresupType = Core.Definiteness.DefPresupType.familiarity

Instances For

inductive Core.Definiteness.ArticleType :

@cite{schwarz-2009}: article type in the D-domain.

Schwarz argues for two structurally distinct definite articles:

Weak: situational uniqueness
Strong: anaphoric familiarity

@cite{patel-grosz-grosz-2017} build on this: ArticleType predicts D-layer count and whether DEM pronouns exist.

none_ : ArticleType
weakOnly : ArticleType
weakAndStrong : ArticleType

Instances For

instance Core.Definiteness.instDecidableEqArticleType :

DecidableEq ArticleType

Equations

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

def Core.Definiteness.instBEqArticleType.beq :

ArticleType → ArticleType → Bool

Equations

Core.Definiteness.instBEqArticleType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instBEqArticleType :

BEq ArticleType

Equations

Core.Definiteness.instBEqArticleType = { beq := Core.Definiteness.instBEqArticleType.beq }

instance Core.Definiteness.instReprArticleType :

Repr ArticleType

Equations

Core.Definiteness.instReprArticleType = { reprPrec := Core.Definiteness.instReprArticleType.repr }

def Core.Definiteness.instReprArticleType.repr :

ArticleType → Nat → Std.Format

Equations

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

Instances For

def Core.Definiteness.articleTypeToAvailablePresup :

ArticleType → List DefPresupType

Which presupposition types a language's article system makes available.

Equations

Instances For

theorem Core.Definiteness.two_layers_two_presup_types :

(articleTypeToAvailablePresup ArticleType.weakAndStrong).length = 2

Languages with two article forms have both presupposition types available. This is PG&G's structural claim translated to semantics: 2 D-layers = 2 presupposition types.

theorem Core.Definiteness.one_layer_one_presup_type :

(articleTypeToAvailablePresup ArticleType.weakOnly).length = 1

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

inductive Core.Definiteness.DefiniteUseType :

@cite{hawkins-1978}'s four use types for definite descriptions. @cite{schwarz-2013} shows these map systematically onto weak vs strong articles.

anaphoric : DefiniteUseType
immediateSituation : DefiniteUseType
largerSituation : DefiniteUseType
bridging : DefiniteUseType

Instances For

instance Core.Definiteness.instDecidableEqDefiniteUseType :

DecidableEq DefiniteUseType

Equations

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

instance Core.Definiteness.instBEqDefiniteUseType :

BEq DefiniteUseType

Equations

Core.Definiteness.instBEqDefiniteUseType = { beq := Core.Definiteness.instBEqDefiniteUseType.beq }

def Core.Definiteness.instBEqDefiniteUseType.beq :

DefiniteUseType → DefiniteUseType → Bool

Equations

Core.Definiteness.instBEqDefiniteUseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instReprDefiniteUseType :

Repr DefiniteUseType

Equations

Core.Definiteness.instReprDefiniteUseType = { reprPrec := Core.Definiteness.instReprDefiniteUseType.repr }

def Core.Definiteness.instReprDefiniteUseType.repr :

DefiniteUseType → Nat → Std.Format

Equations

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

Instances For

def Core.Definiteness.useTypeToPresupType :

DefiniteUseType → DefPresupType

Map definite use type to presupposition type (@cite{schwarz-2013} §3.1).

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

Equations

Instances For

inductive Core.Definiteness.BridgingSubtype :

Bridging subtypes (@cite{schwarz-2013} §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

Instances For

instance Core.Definiteness.instDecidableEqBridgingSubtype :

DecidableEq BridgingSubtype

Equations

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

def Core.Definiteness.instBEqBridgingSubtype.beq :

BridgingSubtype → BridgingSubtype → Bool

Equations

Core.Definiteness.instBEqBridgingSubtype.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instBEqBridgingSubtype :

BEq BridgingSubtype

Equations

Core.Definiteness.instBEqBridgingSubtype = { beq := Core.Definiteness.instBEqBridgingSubtype.beq }

instance Core.Definiteness.instReprBridgingSubtype :

Repr BridgingSubtype

Equations

Core.Definiteness.instReprBridgingSubtype = { reprPrec := Core.Definiteness.instReprBridgingSubtype.repr }

def Core.Definiteness.instReprBridgingSubtype.repr :

BridgingSubtype → Nat → Std.Format

Equations

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

Instances For

def Core.Definiteness.bridgingPresupType :

BridgingSubtype → DefPresupType

Map bridging subtype to presupposition type (@cite{schwarz-2013} §3.2).

Equations

Instances For

inductive Core.Definiteness.WeakArticleStrategy :

How a language expresses the weak/strong article contrast.

@cite{schwarz-2013} 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

Instances For

instance Core.Definiteness.instDecidableEqWeakArticleStrategy :

DecidableEq WeakArticleStrategy

Equations

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

instance Core.Definiteness.instBEqWeakArticleStrategy :

BEq WeakArticleStrategy

Equations

Core.Definiteness.instBEqWeakArticleStrategy = { beq := Core.Definiteness.instBEqWeakArticleStrategy.beq }

def Core.Definiteness.instBEqWeakArticleStrategy.beq :

WeakArticleStrategy → WeakArticleStrategy → Bool

Equations

Core.Definiteness.instBEqWeakArticleStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instReprWeakArticleStrategy :

Repr WeakArticleStrategy

Equations

Core.Definiteness.instReprWeakArticleStrategy = { reprPrec := Core.Definiteness.instReprWeakArticleStrategy.repr }

def Core.Definiteness.instReprWeakArticleStrategy.repr :

WeakArticleStrategy → Nat → Std.Format

Equations

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

Instances For

inductive Core.Definiteness.Definiteness :

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.

@cite{heim-1982}: indefinites are novel, definites are familiar. This is the dynamic semantics version of the ∃/ι contrast.

indefinite : Definiteness
definite : Definiteness

Instances For

instance Core.Definiteness.instDecidableEqDefiniteness :

DecidableEq Definiteness

Equations

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

def Core.Definiteness.instBEqDefiniteness.beq :

Definiteness → Definiteness → Bool

Equations

Core.Definiteness.instBEqDefiniteness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Definiteness.instBEqDefiniteness :

BEq Definiteness

Equations

Core.Definiteness.instBEqDefiniteness = { beq := Core.Definiteness.instBEqDefiniteness.beq }

def Core.Definiteness.instReprDefiniteness.repr :

Definiteness → Nat → Std.Format

Equations

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

Instances For

instance Core.Definiteness.instReprDefiniteness :

Repr Definiteness

Equations

Core.Definiteness.instReprDefiniteness = { reprPrec := Core.Definiteness.instReprDefiniteness.repr }

theorem Core.Definiteness.definite_indefinite_exhaustive (d : Definiteness) :

d = Definiteness.indefinite ∨ d = Definiteness.definite

Definiteness is a binary contrast.