Article-and-demonstrative typology — substrate types and WALS data

@cite{wals-2013} (Chs 37, 38, 41, 42, 43) @cite{bhat-2013} @cite{diessel-2013} @cite{dryer-haspelmath-2013} @cite{greenberg-1978} @cite{himmelmann-1997}

Type-level enums + per-language profile struct for definiteness marking, indefinite articles, and demonstrative systems across @cite{wals-2013} chapters 37, 38, 41, 42, 43, plus WALS distribution data, the principal cross-linguistic generalizations, and the demonstrative→article→affix grammaticalization cline.

Schema

• DefiniteArticleType (Ch 37): how (or whether) definiteness is marked
• IndefiniteArticleType (Ch 38): indefinite article strategy
• DemDistanceSystem (Ch 41): number of distance contrasts
• DemOrientationType: distance- vs person-oriented (for 3-way systems)
• DemFormRelation (Ch 42): pronominal vs adnominal demonstrative form
• PronounDemRelation (Ch 43): 3rd-pronoun ↔ demonstrative relationship
• ArticleDemProfile: per-language bundle (all five chapters)
• GrammaticalizationStage: stages of definiteness grammaticalization

Per-language data lives in Fragments/{Lang}/Reference.lean.

inductive Typology.DefiniteArticleType : Type

Definite article type (WALS Ch 37, @cite{dryer-haspelmath-2013}). Categories ordered along the grammaticalization cline: demonstrative → definite word → definite affix.

• definiteWord : DefiniteArticleType

  Definite word distinct from demonstratives (e.g., English the).

• definiteAffix : DefiniteArticleType

  Definite affix on the noun (e.g., Danish -en, Arabic al-).

• demonstrativeUsed : DefiniteArticleType

  No dedicated definite article; a demonstrative is used for definiteness (e.g., Ojibwa, Swahili).

• noDefButIndef : DefiniteArticleType

  No definite article, but language has an indefinite article.

• noArticle : DefiniteArticleType

  Neither definite nor indefinite article.

@[implicit_reducible]

instance Typology.instDecidableEqDefiniteArticleType : DecidableEq DefiniteArticleType

Equations

• Typology.instDecidableEqDefiniteArticleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.instReprDefiniteArticleType.repr : DefiniteArticleType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprDefiniteArticleType : Repr DefiniteArticleType

Equations

• Typology.instReprDefiniteArticleType = { reprPrec := Typology.instReprDefiniteArticleType.repr }

inductive Typology.IndefiniteArticleType : Type

Indefinite article type (WALS Ch 38, @cite{dryer-haspelmath-2013}). Languages either have a dedicated indefinite word, use the numeral 'one' as an indefinite (the most common grammaticalization path), have an indefinite affix, or lack indefinite articles entirely.

• indefiniteWord : IndefiniteArticleType

  Indefinite word distinct from the numeral 'one' (e.g., English a).

• numeralOne : IndefiniteArticleType

  Numeral 'one' used as indefinite article (e.g., German ein).

• indefiniteAffix : IndefiniteArticleType

  Indefinite affix on noun.

• noIndefButDef : IndefiniteArticleType

  No indefinite article, but language has a definite article.

• noArticle : IndefiniteArticleType

  Neither indefinite nor definite article.

@[implicit_reducible]

instance Typology.instDecidableEqIndefiniteArticleType : DecidableEq IndefiniteArticleType

Equations

• Typology.instDecidableEqIndefiniteArticleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprIndefiniteArticleType : Repr IndefiniteArticleType

Equations

• Typology.instReprIndefiniteArticleType = { reprPrec := Typology.instReprIndefiniteArticleType.repr }

def Typology.instReprIndefiniteArticleType.repr : IndefiniteArticleType → Nat → Std.Format

Equations

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

inductive Typology.DemDistanceSystem : Type

Number of distance contrasts in adnominal demonstratives (WALS Ch 41, @cite{diessel-2013}). Two-way systems are by far the most common (54.3%), followed by three-way (37.6%).

• noContrast : DemDistanceSystem

  No distance contrast (e.g., Modern German dieser).

• twoWay : DemDistanceSystem

  Two-way contrast: proximal vs distal (e.g., English this/that).

• threeWay : DemDistanceSystem

  Three-way contrast (e.g., Japanese ko/so/a, Latin hic/iste/ille).

• fourWay : DemDistanceSystem

  Four-way contrast (e.g., Hausa).

• fiveOrMore : DemDistanceSystem

  Five or more distance contrasts.

@[implicit_reducible]

instance Typology.instDecidableEqDemDistanceSystem : DecidableEq DemDistanceSystem

Equations

• Typology.instDecidableEqDemDistanceSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprDemDistanceSystem : Repr DemDistanceSystem

Equations

• Typology.instReprDemDistanceSystem = { reprPrec := Typology.instReprDemDistanceSystem.repr }

def Typology.instReprDemDistanceSystem.repr : DemDistanceSystem → Nat → Std.Format

Equations

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

inductive Typology.DemOrientationType : Type

Whether a three-way demonstrative system is distance- or person-oriented. @cite{diessel-2013}: about 2/3 of three-way systems are distance-oriented, 1/3 person-oriented (e.g., Japanese is the canonical person-oriented system).

• distanceOriented : DemOrientationType

  All terms encode distance from speaker (proximal/medial/distal).

• personOriented : DemOrientationType

  One term encodes proximity to the hearer (near-speaker / near-hearer / distal).

• notApplicable : DemOrientationType

  Not applicable (system is not three-way).

@[implicit_reducible]

instance Typology.instDecidableEqDemOrientationType : DecidableEq DemOrientationType

Equations

• Typology.instDecidableEqDemOrientationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprDemOrientationType : Repr DemOrientationType

Equations

• Typology.instReprDemOrientationType = { reprPrec := Typology.instReprDemOrientationType.repr }

def Typology.instReprDemOrientationType.repr : DemOrientationType → Nat → Std.Format

Equations

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

inductive Typology.DemFormRelation : Type

Relationship between pronominal and adnominal demonstratives (WALS Ch 42, @cite{diessel-2013}). English uses the same forms; French uses different stems (ce/cette vs celui/celle); Turkish uses the same stems but different inflectional features.

• sameForms : DemFormRelation

  Same forms for pronominal and adnominal use (e.g., English).

• differentStems : DemFormRelation

  Different stems (e.g., French ce/celui).

• differentInflection : DemFormRelation

  Same stems but different inflectional features (e.g., Turkish).

@[implicit_reducible]

instance Typology.instDecidableEqDemFormRelation : DecidableEq DemFormRelation

Equations

• Typology.instDecidableEqDemFormRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprDemFormRelation : Repr DemFormRelation

Equations

• Typology.instReprDemFormRelation = { reprPrec := Typology.instReprDemFormRelation.repr }

def Typology.instReprDemFormRelation.repr : DemFormRelation → Nat → Std.Format

Equations

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

inductive Typology.PronounDemRelation : Type

Relationship between third-person pronouns and demonstratives (WALS Ch 43, @cite{bhat-2013}). In "two-person languages", 3rd-person pronouns are demonstrative-derived; in "three-person languages", 3rd-person pronouns form an independent person paradigm.

• unrelated : PronounDemRelation

  3rd-person pronouns unrelated to demonstratives (e.g., Ainu, Polish).

• relatedAll : PronounDemRelation

  Related to all demonstratives (e.g., Basque).

• relatedRemote : PronounDemRelation

  Related specifically to remote/distal demonstratives (e.g., Eastern Armenian: 3sg na = distal na).

• relatedNonRemote : PronounDemRelation

  Related specifically to non-remote (proximal/medial) demonstratives (e.g., Brahui).

• relatedGender : PronounDemRelation

  Related via shared gender/noun-class markers (e.g., Venda).

• relatedNonhuman : PronounDemRelation

  Demonstratives used as 3rd-person pronouns for nonhuman reference only (e.g., Jaqaru).

@[implicit_reducible]

instance Typology.instDecidableEqPronounDemRelation : DecidableEq PronounDemRelation

Equations

• Typology.instDecidableEqPronounDemRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprPronounDemRelation : Repr PronounDemRelation

Equations

• Typology.instReprPronounDemRelation = { reprPrec := Typology.instReprPronounDemRelation.repr }

def Typology.instReprPronounDemRelation.repr : PronounDemRelation → Nat → Std.Format

Equations

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

def Typology.PronounDemRelation.isRelated : PronounDemRelation → Bool

Whether 3rd-person pronouns show ANY relationship to demonstratives (Bhat's "two-person" vs "three-person" distinction).

Equations

• Typology.PronounDemRelation.unrelated.isRelated = false
• x✝.isRelated = true

structure Typology.ArticleDemProfile : Type

A language's article-and-demonstrative profile across @cite{wals-2013} Chs 37, 38, 41, 42, 43. WALS samples vary by chapter, so each field is optional.

• language : String
• family : String
• iso : String

  ISO 639-3 code.

• defArticle : Option DefiniteArticleType

  Ch 37: definite article type.

• indefArticle : Option IndefiniteArticleType

  Ch 38: indefinite article type.

• demDistance : Option DemDistanceSystem

  Ch 41: distance contrasts in demonstratives.

• demOrientation : Option DemOrientationType

  Ch 41 subtype: distance- vs person-oriented (for three-way systems).

• demFormType : Option DemFormRelation

  Ch 42: pronominal vs adnominal demonstrative form.

• pronDemRelation : Option PronounDemRelation

  Ch 43: 3rd-person pronoun ~ demonstrative relationship.

def Typology.instReprArticleDemProfile.repr : ArticleDemProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprArticleDemProfile : Repr ArticleDemProfile

Equations

• Typology.instReprArticleDemProfile = { reprPrec := Typology.instReprArticleDemProfile.repr }

def Typology.ArticleDemProfile.hasDefinite (p : ArticleDemProfile) : Bool

Does this language have any form of definite marking (word, affix, or demonstrative used as definite)?

Equations

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

def Typology.ArticleDemProfile.hasIndefinite (p : ArticleDemProfile) : Bool

Does this language have any indefinite article (word, numeral 'one', or affix)?

Equations

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

def Typology.fromWALS37A : Data.WALS.F37A.DefiniteArticleType → DefiniteArticleType

Convert WALS 37A definite-article values into the substrate enum.

Equations

• Typology.fromWALS37A Data.WALS.F37A.DefiniteArticleType.definiteWordDistinctFromDemonstrative = Typology.DefiniteArticleType.definiteWord
• Typology.fromWALS37A Data.WALS.F37A.DefiniteArticleType.demonstrativeWordUsedAsDefiniteArticle = Typology.DefiniteArticleType.demonstrativeUsed
• Typology.fromWALS37A Data.WALS.F37A.DefiniteArticleType.definiteAffix = Typology.DefiniteArticleType.definiteAffix
• Typology.fromWALS37A Data.WALS.F37A.DefiniteArticleType.noDefiniteButIndefiniteArticle = Typology.DefiniteArticleType.noDefButIndef
• Typology.fromWALS37A Data.WALS.F37A.DefiniteArticleType.noDefiniteOrIndefiniteArticle = Typology.DefiniteArticleType.noArticle

def Typology.fromWALS38A : Data.WALS.F38A.IndefiniteArticleType → IndefiniteArticleType

Convert WALS 38A indefinite-article values into the substrate enum.

Equations

• Typology.fromWALS38A Data.WALS.F38A.IndefiniteArticleType.indefiniteWordDistinctFromOne = Typology.IndefiniteArticleType.indefiniteWord
• Typology.fromWALS38A Data.WALS.F38A.IndefiniteArticleType.indefiniteWordSameAsOne = Typology.IndefiniteArticleType.numeralOne
• Typology.fromWALS38A Data.WALS.F38A.IndefiniteArticleType.indefiniteAffix = Typology.IndefiniteArticleType.indefiniteAffix
• Typology.fromWALS38A Data.WALS.F38A.IndefiniteArticleType.noIndefiniteButDefiniteArticle = Typology.IndefiniteArticleType.noIndefButDef
• Typology.fromWALS38A Data.WALS.F38A.IndefiniteArticleType.noDefiniteOrIndefiniteArticle = Typology.IndefiniteArticleType.noArticle

def Typology.fromWALS41A : Data.WALS.F41A.DistanceContrastsInDemonstratives → DemDistanceSystem

Convert WALS 41A distance-contrast values into the substrate enum.

Equations

• Typology.fromWALS41A Data.WALS.F41A.DistanceContrastsInDemonstratives.noDistanceContrast = Typology.DemDistanceSystem.noContrast
• Typology.fromWALS41A Data.WALS.F41A.DistanceContrastsInDemonstratives.twoWayContrast = Typology.DemDistanceSystem.twoWay
• Typology.fromWALS41A Data.WALS.F41A.DistanceContrastsInDemonstratives.threeWayContrast = Typology.DemDistanceSystem.threeWay
• Typology.fromWALS41A Data.WALS.F41A.DistanceContrastsInDemonstratives.fourWayContrast = Typology.DemDistanceSystem.fourWay
• Typology.fromWALS41A Data.WALS.F41A.DistanceContrastsInDemonstratives.fiveWayContrast = Typology.DemDistanceSystem.fiveOrMore

def Typology.fromWALS42A : Data.WALS.F42A.PronominalAndAdnominalDemonstratives → DemFormRelation

Convert WALS 42A pronominal/adnominal-form values into the substrate enum.

Equations

• Typology.fromWALS42A Data.WALS.F42A.PronominalAndAdnominalDemonstratives.identical = Typology.DemFormRelation.sameForms
• Typology.fromWALS42A Data.WALS.F42A.PronominalAndAdnominalDemonstratives.differentStem = Typology.DemFormRelation.differentStems
• Typology.fromWALS42A Data.WALS.F42A.PronominalAndAdnominalDemonstratives.differentInflection = Typology.DemFormRelation.differentInflection

def Typology.fromWALS43A : Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives → PronounDemRelation

Convert WALS 43A 3rd-person-pronoun values into the substrate enum.

Equations

• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.unrelated = Typology.PronounDemRelation.unrelated
• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.relatedForAllDemonstratives = Typology.PronounDemRelation.relatedAll
• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.relatedToRemoteDemonstratives = Typology.PronounDemRelation.relatedRemote
• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.relatedToNonRemoteDemonstratives = Typology.PronounDemRelation.relatedNonRemote
• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.relatedByGenderMarkers = Typology.PronounDemRelation.relatedGender
• Typology.fromWALS43A Data.WALS.F43A.ThirdPersonPronounsAndDemonstratives.relatedForNonHumanReference = Typology.PronounDemRelation.relatedNonhuman

structure Typology.DefiniteArticleCounts : Type

WALS Ch 37: definite article distribution (@cite{dryer-haspelmath-2013}, n = 566).

• definiteWord : Nat
• demonstrativeUsed : Nat
• definiteAffix : Nat
• noDefButIndef : Nat
• noArticle : Nat

def Typology.instReprDefiniteArticleCounts.repr : DefiniteArticleCounts → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprDefiniteArticleCounts : Repr DefiniteArticleCounts

Equations

• Typology.instReprDefiniteArticleCounts = { reprPrec := Typology.instReprDefiniteArticleCounts.repr }

def Typology.DefiniteArticleCounts.total (c : DefiniteArticleCounts) : Nat

Equations

• c.total = c.definiteWord + c.demonstrativeUsed + c.definiteAffix + c.noDefButIndef + c.noArticle

def Typology.walsDefiniteArticle : DefiniteArticleCounts

WALS Ch 37 counts (566 languages).

Equations

• Typology.walsDefiniteArticle = { definiteWord := 197, demonstrativeUsed := 56, definiteAffix := 84, noDefButIndef := 41, noArticle := 188 }

structure Typology.IndefiniteArticleCounts : Type

WALS Ch 38: indefinite article distribution (@cite{dryer-haspelmath-2013}, n = 473).

• indefiniteWord : Nat
• numeralOne : Nat
• indefiniteAffix : Nat
• noIndefButDef : Nat
• noArticle : Nat

@[implicit_reducible]

instance Typology.instReprIndefiniteArticleCounts : Repr IndefiniteArticleCounts

Equations

• Typology.instReprIndefiniteArticleCounts = { reprPrec := Typology.instReprIndefiniteArticleCounts.repr }

def Typology.instReprIndefiniteArticleCounts.repr : IndefiniteArticleCounts → Nat → Std.Format

Equations

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

def Typology.IndefiniteArticleCounts.total (c : IndefiniteArticleCounts) : Nat

Equations

• c.total = c.indefiniteWord + c.numeralOne + c.indefiniteAffix + c.noIndefButDef + c.noArticle

def Typology.walsIndefiniteArticle : IndefiniteArticleCounts

WALS Ch 38 counts (473 languages).

Equations

• Typology.walsIndefiniteArticle = { indefiniteWord := 91, numeralOne := 90, indefiniteAffix := 23, noIndefButDef := 81, noArticle := 188 }

structure Typology.DemDistanceCounts : Type

WALS Ch 41: demonstrative distance contrasts (@cite{diessel-2013}, n = 234).

• noContrast : Nat
• twoWay : Nat
• threeWay : Nat
• fourWay : Nat
• fiveOrMore : Nat

@[implicit_reducible]

instance Typology.instReprDemDistanceCounts : Repr DemDistanceCounts

Equations

• Typology.instReprDemDistanceCounts = { reprPrec := Typology.instReprDemDistanceCounts.repr }

def Typology.instReprDemDistanceCounts.repr : DemDistanceCounts → Nat → Std.Format

Equations

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

def Typology.DemDistanceCounts.total (c : DemDistanceCounts) : Nat

Equations

• c.total = c.noContrast + c.twoWay + c.threeWay + c.fourWay + c.fiveOrMore

def Typology.walsDemDistance : DemDistanceCounts

WALS Ch 41 counts (234 languages).

Equations

• Typology.walsDemDistance = { noContrast := 7, twoWay := 127, threeWay := 88, fourWay := 8, fiveOrMore := 4 }

structure Typology.DemFormCounts : Type

WALS Ch 42: pronominal/adnominal demonstrative form (@cite{diessel-2013}, n = 201).

• sameForms : Nat
• differentStems : Nat
• differentInflection : Nat

@[implicit_reducible]

instance Typology.instReprDemFormCounts : Repr DemFormCounts

Equations

• Typology.instReprDemFormCounts = { reprPrec := Typology.instReprDemFormCounts.repr }

def Typology.instReprDemFormCounts.repr : DemFormCounts → Nat → Std.Format

Equations

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

def Typology.DemFormCounts.total (c : DemFormCounts) : Nat

Equations

• c.total = c.sameForms + c.differentStems + c.differentInflection

def Typology.walsDemForm : DemFormCounts

WALS Ch 42 counts (201 languages).

Equations

• Typology.walsDemForm = { sameForms := 143, differentStems := 37, differentInflection := 21 }

structure Typology.PronounDemCounts : Type

WALS Ch 43: 3rd-person pronoun ~ demonstrative relationship (@cite{bhat-2013}, n = 225).

• unrelated : Nat
• relatedAll : Nat
• relatedRemote : Nat
• relatedNonRemote : Nat
• relatedGender : Nat
• relatedNonhuman : Nat

def Typology.instReprPronounDemCounts.repr : PronounDemCounts → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPronounDemCounts : Repr PronounDemCounts

Equations

• Typology.instReprPronounDemCounts = { reprPrec := Typology.instReprPronounDemCounts.repr }

def Typology.PronounDemCounts.total (c : PronounDemCounts) : Nat

Equations

• c.total = c.unrelated + c.relatedAll + c.relatedRemote + c.relatedNonRemote + c.relatedGender + c.relatedNonhuman

def Typology.PronounDemCounts.totalRelated (c : PronounDemCounts) : Nat

Total count of languages where 3rd-person pronouns show any relationship to demonstratives.

Equations

• c.totalRelated = c.relatedAll + c.relatedRemote + c.relatedNonRemote + c.relatedGender + c.relatedNonhuman

def Typology.walsPronounDem : PronounDemCounts

WALS Ch 43 counts (225 languages).

Equations

• Typology.walsPronounDem = { unrelated := 100, relatedAll := 52, relatedRemote := 18, relatedNonRemote := 14, relatedGender := 24, relatedNonhuman := 17 }

theorem Typology.twoWay_most_common : walsDemDistance.twoWay > walsDemDistance.threeWay ∧ walsDemDistance.twoWay > walsDemDistance.fourWay ∧ walsDemDistance.twoWay > walsDemDistance.fiveOrMore ∧ walsDemDistance.twoWay > walsDemDistance.noContrast

Two-way demonstrative systems (proximal/distal) are the most common type: 127 of 234 languages (54.3%). @cite{diessel-2013}: "the vast majority of the world's languages employ two or three distance-marked demonstratives".

theorem Typology.twoAndThreeWay_dominate : walsDemDistance.twoWay + walsDemDistance.threeWay > 9 * (walsDemDistance.noContrast + walsDemDistance.fourWay + walsDemDistance.fiveOrMore)

Two-way and three-way systems together account for over 90% of languages; one-way, four-way, and five-or-more systems together are under 10%.

theorem Typology.defArticle_more_robust_than_indef : walsIndefiniteArticle.noIndefButDef > walsDefiniteArticle.noDefButIndef

Languages with definite articles tend to also have indefinite articles. The asymmetry: 81 languages have a definite but no indefinite article, vs. 41 languages with indefinite but no definite article. Definiteness marking is the typologically prior category.

theorem Typology.majority_have_some_definite_marking : walsDefiniteArticle.definiteWord + walsDefiniteArticle.demonstrativeUsed + walsDefiniteArticle.definiteAffix > walsDefiniteArticle.noDefButIndef + walsDefiniteArticle.noArticle

Languages with some form of definite marking (word, affix, or demonstrative) outnumber those without. 337 of 566 languages (59.5%) have definite marking.

theorem Typology.majority_pronoun_dem_related : walsPronounDem.totalRelated > walsPronounDem.unrelated

In a majority of languages (125 of 225 = 55.6%), 3rd-person pronouns show some relationship to demonstratives. Supports the diachronic pathway demonstrative → 3rd-person pronoun (@cite{bhat-2013}).

theorem Typology.relatedAll_most_common_subtype : walsPronounDem.relatedAll > walsPronounDem.relatedRemote ∧ walsPronounDem.relatedAll > walsPronounDem.relatedNonRemote ∧ walsPronounDem.relatedAll > walsPronounDem.relatedGender ∧ walsPronounDem.relatedAll > walsPronounDem.relatedNonhuman

The most common subtype of pronoun-demonstrative relationship is "related to all demonstratives" (52 languages), where any demonstrative can serve as a 3rd-person pronoun.

theorem Typology.sameForm_demonstratives_majority : walsDemForm.sameForms > walsDemForm.differentStems + walsDemForm.differentInflection

In most languages (143 of 201 = 71.1%), pronominal and adnominal demonstratives have the same forms (@cite{diessel-2013}). Differential marking via different stems (37) or different inflection (21) is the minority.

inductive Typology.GrammaticalizationStage : Type

The grammaticalization hierarchy for definiteness marking (@cite{greenberg-1978}, @cite{himmelmann-1997}):

Stage 0 — No definiteness marking (bare nouns; e.g., Mandarin, Russian) Stage 1 — Demonstrative used for definiteness (e.g., Swahili, Ojibwa) Stage 2 — Definite word distinct from demonstrative (e.g., English) Stage 3 — Definite affix (e.g., Danish, Arabic)

Each stage represents further grammaticalization: phonological reduction, semantic bleaching (loss of deictic content), and increased obligatoriness.

• noMarking : GrammaticalizationStage
• demonstrative : GrammaticalizationStage
• definiteWord : GrammaticalizationStage
• definiteAffix : GrammaticalizationStage

@[implicit_reducible]

instance Typology.instDecidableEqGrammaticalizationStage : DecidableEq GrammaticalizationStage

Equations

• Typology.instDecidableEqGrammaticalizationStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprGrammaticalizationStage : Repr GrammaticalizationStage

Equations

• Typology.instReprGrammaticalizationStage = { reprPrec := Typology.instReprGrammaticalizationStage.repr }

def Typology.instReprGrammaticalizationStage.repr : GrammaticalizationStage → Nat → Std.Format

Equations

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

def Typology.DefiniteArticleType.stage : DefiniteArticleType → GrammaticalizationStage

Map a DefiniteArticleType to its grammaticalization stage.

Equations

• Typology.DefiniteArticleType.noArticle.stage = Typology.GrammaticalizationStage.noMarking
• Typology.DefiniteArticleType.noDefButIndef.stage = Typology.GrammaticalizationStage.noMarking
• Typology.DefiniteArticleType.demonstrativeUsed.stage = Typology.GrammaticalizationStage.demonstrative
• Typology.DefiniteArticleType.definiteWord.stage = Typology.GrammaticalizationStage.definiteWord
• Typology.DefiniteArticleType.definiteAffix.stage = Typology.GrammaticalizationStage.definiteAffix

def Typology.GrammaticalizationStage.ord : GrammaticalizationStage → Nat

Numeric rank for the grammaticalization stage (higher = more grammaticalized).

Equations

• Typology.GrammaticalizationStage.noMarking.ord = 0
• Typology.GrammaticalizationStage.demonstrative.ord = 1
• Typology.GrammaticalizationStage.definiteWord.ord = 2
• Typology.GrammaticalizationStage.definiteAffix.ord = 3

theorem Typology.grammaticalization_cline_attested : walsDefiniteArticle.demonstrativeUsed > 0 ∧ walsDefiniteArticle.definiteWord > 0 ∧ walsDefiniteArticle.definiteAffix > 0 ∧ walsDefiniteArticle.demonstrativeUsed < walsDefiniteArticle.definiteWord ∧ walsDefiniteArticle.demonstrativeUsed < walsDefiniteArticle.definiteAffix

All three intermediate stages of the grammaticalization cline are well attested cross-linguistically: 56 languages use demonstratives as definite markers (Stage 1), 197 have distinct definite words (Stage 2), and 84 have definite affixes (Stage 3). The transitional Stage 1 is smaller than both later stages.