Definiteness

This file gives the frame-free vocabulary of definiteness. A nominal is definite or indefinite, as Heim distinguishes them, and on the continuum of definiteness, or specificity, that Comrie, Aissen and Haspelmath share, a definite ranks above a specific indefinite above a non-specific one; Farkas and Brasoveanu separate the kinds of specificity, scopal, epistemic and partitive. A definite article has one of two strengths, uniqueness and familiarity, after Schwarz, and the article typologies are built on them. The strength a use of a definite calls for, after Hawkins and Schwarz, and the strength of a bridging relation are recorded as data here; which cell a language's determiner inventory falls in is derived in Syntax/Category/Determiner/Basic.lean, and the descriptions themselves denote in Semantics/Reference/Description.lean.

Main definitions

• Reference.Definiteness: definite or indefinite, as a two-element bounded linear order.
• Reference.DefinitenessDegree: the continuum of definiteness, with its cut DefinitenessDegree.definiteness.
• Reference.Description.Strength, Reference.Description.Kind: the strength of a definite article and the kind of a description, with Strength.toKind and Kind.strength.
• Reference.DefiniteUse, Reference.Bridging: the uses of a definite and the bridging relations, each with the strength it calls for.
• Reference.ArticleType, Reference.MarkingStrategy: the three-cell and four-cell article typologies of Schwarz and of Jenks with Moroney's unmarked cell, and the coarsening MarkingStrategy.articleType.

References

• [Ais03]
• [Com89]
• [FB20a]
• [Has21c]
• [Sch09b]
• [Sch13]
• [Haw78]
• [Hei82a]
• [Jen18]
• [Mor21]
• [PGG17]

inductive Reference.Definiteness : Type

A nominal is definite or indefinite. A definite retrieves a unique or familiar referent, an indefinite introduces a new one ([Hei82a]).

• indefinite : Definiteness
• definite : Definiteness

@[instance_reducible]

instance Reference.instDecidableEqDefiniteness : DecidableEq Definiteness

Equations

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

def Reference.instReprDefiniteness.repr : Definiteness → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprDefiniteness : Repr Definiteness

Equations

• Reference.instReprDefiniteness = { reprPrec := Reference.instReprDefiniteness.repr }

@[instance_reducible]

instance Reference.instFintypeDefiniteness : Fintype Definiteness

Equations

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

def Reference.Definiteness.rank : Definiteness → ℕ

The rank on the definiteness scale, higher for definite.

Equations

• Reference.Definiteness.indefinite.rank = 0
• Reference.Definiteness.definite.rank = 1

@[instance_reducible]

instance Reference.Definiteness.instLinearOrder : LinearOrder Definiteness

The order indefinite < definite is the definiteness scale of differential argument marking in its binary form ([Ais03]).

Equations

• Reference.Definiteness.instLinearOrder = LinearOrder.lift' Reference.Definiteness.rank Reference.Definiteness.instLinearOrder._proof_1

@[instance_reducible]

instance Reference.Definiteness.instBoundedOrder : BoundedOrder Definiteness

⊥ = indefinite, ⊤ = definite.

Equations

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

instance Reference.Definiteness.instIsSimpleOrder : IsSimpleOrder Definiteness

inductive Reference.DefinitenessDegree : Type

The degree of definiteness of a nominal ranks a definite above a specific indefinite above a non-specific indefinite. A specific indefinite is one of whichever kind of specificity a language's marking tracks.

• nonSpecific : DefinitenessDegree
• specific : DefinitenessDegree
• definite : DefinitenessDegree

@[instance_reducible]

instance Reference.instDecidableEqDefinitenessDegree : DecidableEq DefinitenessDegree

Equations

• Reference.instDecidableEqDefinitenessDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reference.instReprDefinitenessDegree.repr : DefinitenessDegree → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprDefinitenessDegree : Repr DefinitenessDegree

Equations

• Reference.instReprDefinitenessDegree = { reprPrec := Reference.instReprDefinitenessDegree.repr }

@[instance_reducible]

instance Reference.instFintypeDefinitenessDegree : Fintype DefinitenessDegree

Equations

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

def Reference.DefinitenessDegree.rank : DefinitenessDegree → ℕ

The rank on the continuum, 0 for a non-specific indefinite up to 2 for a definite.

Equations

• Reference.DefinitenessDegree.nonSpecific.rank = 0
• Reference.DefinitenessDegree.specific.rank = 1
• Reference.DefinitenessDegree.definite.rank = 2

@[instance_reducible]

instance Reference.DefinitenessDegree.instLinearOrder : LinearOrder DefinitenessDegree

Equations

• Reference.DefinitenessDegree.instLinearOrder = LinearOrder.lift' Reference.DefinitenessDegree.rank Reference.DefinitenessDegree.instLinearOrder._proof_1

def Reference.DefinitenessDegree.definiteness (d : DefinitenessDegree) : Definiteness

A degree is definite at the top of the continuum and indefinite below it.

Equations

• d.definiteness = if Reference.DefinitenessDegree.definite ≤ d then Reference.Definiteness.definite else Reference.Definiteness.indefinite

theorem Reference.DefinitenessDegree.definiteness_monotone : Monotone definiteness

inductive Reference.Description.Strength : Type

The strength of a definite article ([Sch09b]): the weak article presupposes uniqueness, the strong article familiarity.

• uniqueness : Strength
• familiarity : Strength

@[instance_reducible]

instance Reference.Description.instDecidableEqStrength : DecidableEq Strength

Equations

• Reference.Description.instDecidableEqStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Reference.Description.instReprStrength : Repr Strength

Equations

• Reference.Description.instReprStrength = { reprPrec := Reference.Description.instReprStrength.repr }

def Reference.Description.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

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

inductive Reference.Description.Kind : Type

The kind of a nominal description is a constructor of Description with its payload erased, or the indefinite, which denotes no partial individual but which an inventory may realize.

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

@[instance_reducible]

instance Reference.Description.instDecidableEqKind : DecidableEq Kind

Equations

• Reference.Description.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reference.Description.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.Description.instReprKind : Repr Kind

Equations

• Reference.Description.instReprKind = { reprPrec := Reference.Description.instReprKind.repr }

def Reference.Description.Strength.toKind : Strength → Kind

The weak article realizes the unique description and the strong article the anaphoric one.

Equations

• Reference.Description.Strength.uniqueness.toKind = Reference.Description.Kind.unique
• Reference.Description.Strength.familiarity.toKind = Reference.Description.Kind.anaphoric

def Reference.Description.Kind.strength : Kind → Option Strength

The strength a kind of description presupposes, where it is definite.

Equations

• Reference.Description.Kind.bare.strength = none
• Reference.Description.Kind.indefinite.strength = none
• Reference.Description.Kind.unique.strength = some Reference.Description.Strength.uniqueness
• Reference.Description.Kind.possessive.strength = some Reference.Description.Strength.uniqueness
• Reference.Description.Kind.anaphoric.strength = some Reference.Description.Strength.familiarity
• Reference.Description.Kind.demonstrative.strength = some Reference.Description.Strength.familiarity

@[simp]

theorem Reference.Description.Strength.strength_toKind (p : Strength) : p.toKind.strength = some p

inductive Reference.DefiniteUse : Type

[Haw78]'s uses of a definite description, with the donkey use of [Sch09b].

• anaphoric : DefiniteUse
• immediateSituation : DefiniteUse
• largerSituation : DefiniteUse
• bridging : DefiniteUse
• donkey : DefiniteUse

@[instance_reducible]

instance Reference.instDecidableEqDefiniteUse : DecidableEq DefiniteUse

Equations

• Reference.instDecidableEqDefiniteUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reference.instReprDefiniteUse.repr : DefiniteUse → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprDefiniteUse : Repr DefiniteUse

Equations

• Reference.instReprDefiniteUse = { reprPrec := Reference.instReprDefiniteUse.repr }

def Reference.DefiniteUse.strength : DefiniteUse → Description.Strength

The article strength a use calls for ([Sch13]): the anaphoric and donkey uses the strong article, the situational uses the weak one, bridging the weak one by default.

Equations

• Reference.DefiniteUse.anaphoric.strength = Reference.Description.Strength.familiarity
• Reference.DefiniteUse.donkey.strength = Reference.Description.Strength.familiarity
• Reference.DefiniteUse.immediateSituation.strength = Reference.Description.Strength.uniqueness
• Reference.DefiniteUse.largerSituation.strength = Reference.Description.Strength.uniqueness
• Reference.DefiniteUse.bridging.strength = Reference.Description.Strength.uniqueness

inductive Reference.Bridging : Type

The bridging relations ([Sch13]): part–whole bridging, the fridge and its crisper, and relational bridging, the play and its author.

• partWhole : Bridging
• relational : Bridging

@[instance_reducible]

instance Reference.instDecidableEqBridging : DecidableEq Bridging

Equations

• Reference.instDecidableEqBridging x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reference.instReprBridging.repr : Bridging → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprBridging : Repr Bridging

Equations

• Reference.instReprBridging = { reprPrec := Reference.instReprBridging.repr }

def Reference.Bridging.strength : Bridging → Description.Strength

The article strength a bridging relation calls for ([Sch13]): part–whole bridging the weak article, relational bridging the strong one.

Equations

• Reference.Bridging.partWhole.strength = Reference.Description.Strength.uniqueness
• Reference.Bridging.relational.strength = Reference.Description.Strength.familiarity

inductive Reference.ArticleType : Type

The article systems of [Sch09b] and [PGG17]: no article, a weak article only, or weak and strong articles.

• articleless : ArticleType
• weakOnly : ArticleType
• weakAndStrong : ArticleType

@[instance_reducible]

instance Reference.instDecidableEqArticleType : DecidableEq ArticleType

Equations

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

@[instance_reducible]

instance Reference.instReprArticleType : Repr ArticleType

Equations

• Reference.instReprArticleType = { reprPrec := Reference.instReprArticleType.repr }

def Reference.instReprArticleType.repr : ArticleType → ℕ → Std.Format

Equations

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

inductive Reference.MarkingStrategy : Type

The definiteness-marking strategies of [Jen18], with [Mor21]'s unmarked cell: one form marks both strengths, two forms mark them apart, only the anaphoric strength is obligatorily marked, or neither is. A language's cell is derived from its determiner inventory by Determiner.Inventory.markingStrategy.

• generallyMarked : MarkingStrategy
• bipartite : MarkingStrategy
• markedAnaphoric : MarkingStrategy
• unmarked : MarkingStrategy

@[instance_reducible]

instance Reference.instDecidableEqMarkingStrategy : DecidableEq MarkingStrategy

Equations

• Reference.instDecidableEqMarkingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Reference.instReprMarkingStrategy.repr : MarkingStrategy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Reference.instReprMarkingStrategy : Repr MarkingStrategy

Equations

• Reference.instReprMarkingStrategy = { reprPrec := Reference.instReprMarkingStrategy.repr }

def Reference.MarkingStrategy.articleType : MarkingStrategy → ArticleType

The article system of a marking strategy, which collapses the generally-marked and marked-anaphoric cells to a single weak article.

Equations

• Reference.MarkingStrategy.generallyMarked.articleType = Reference.ArticleType.weakOnly
• Reference.MarkingStrategy.markedAnaphoric.articleType = Reference.ArticleType.weakOnly
• Reference.MarkingStrategy.bipartite.articleType = Reference.ArticleType.weakAndStrong
• Reference.MarkingStrategy.unmarked.articleType = Reference.ArticleType.articleless