Cross-Linguistic Typology of Articles and Demonstratives (WALS)

@cite{bhat-2013} @cite{greenberg-1978} @cite{himmelmann-1997} @cite{dryer-haspelmath-2013}

Typological data on definiteness marking, indefinite articles, and demonstrative systems across languages, drawn from five chapters of the World Atlas of Language Structures:

• Ch 37 (Dryer): Definite articles -- whether a language has a definite article as a word distinct from demonstratives, an affix, a demonstrative used for definiteness, or no definite marking at all.
• Ch 38 (Dryer): Indefinite articles -- whether a language has an indefinite article distinct from the numeral 'one', uses 'one' as an indefinite article, has an indefinite affix, or lacks indefinite articles entirely.
• Ch 41 (Diessel): Distance contrasts in demonstratives -- the number of distance distinctions encoded in adnominal demonstratives (1 through 5+).
• Ch 42 (Diessel): Pronominal and adnominal demonstratives -- whether the two demonstrative uses have the same form, different stems, or different inflectional features.
• Ch 43 (Bhat): Third-person pronouns and demonstratives -- whether 3rd-person pronouns are identical to, derived, or unrelated to demonstratives.

Key Generalizations

1. Two-way demonstrative distance systems (proximal/distal) are the most common cross-linguistically (54.3%), followed by three-way systems (37.6%).
2. Languages with definite articles tend to also have indefinite articles, but the reverse is not true: 41 languages have only an indefinite article with no definite article.
3. In a majority of languages (125 of 225), third-person pronouns show some relationship to demonstratives -- the diachronic pathway demonstrative -> 3rd-person pronoun is well attested.
4. The grammaticalization cline demonstrative -> definite article -> definite affix is a well-established diachronic pathway.

inductive Phenomena.Reference.Typology.DefiniteArticleType : Type

Definite article type (WALS Ch 37, @cite{dryer-haspelmath-2013}).

Classifies languages by how (or whether) they mark definiteness on nouns. The categories are ordered along a 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.

instance Phenomena.Reference.Typology.instDecidableEqDefiniteArticleType : DecidableEq DefiniteArticleType

Equations

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

instance Phenomena.Reference.Typology.instBEqDefiniteArticleType : BEq DefiniteArticleType

Equations

• Phenomena.Reference.Typology.instBEqDefiniteArticleType = { beq := Phenomena.Reference.Typology.instBEqDefiniteArticleType.beq }

def Phenomena.Reference.Typology.instBEqDefiniteArticleType.beq : DefiniteArticleType → DefiniteArticleType → Bool

Equations

• Phenomena.Reference.Typology.instBEqDefiniteArticleType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

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

instance Phenomena.Reference.Typology.instReprDefiniteArticleType : Repr DefiniteArticleType

Equations

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

inductive Phenomena.Reference.Typology.IndefiniteArticleType : Type

Indefinite article type (WALS Ch 38, @cite{dryer-haspelmath-2013}).

Languages either have a dedicated indefinite word (distinct from 'one'), use the numeral 'one' as an indefinite marker (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.

instance Phenomena.Reference.Typology.instDecidableEqIndefiniteArticleType : DecidableEq IndefiniteArticleType

Equations

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

def Phenomena.Reference.Typology.instBEqIndefiniteArticleType.beq : IndefiniteArticleType → IndefiniteArticleType → Bool

Equations

• Phenomena.Reference.Typology.instBEqIndefiniteArticleType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqIndefiniteArticleType : BEq IndefiniteArticleType

Equations

• Phenomena.Reference.Typology.instBEqIndefiniteArticleType = { beq := Phenomena.Reference.Typology.instBEqIndefiniteArticleType.beq }

instance Phenomena.Reference.Typology.instReprIndefiniteArticleType : Repr IndefiniteArticleType

Equations

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

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

Equations

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

inductive Phenomena.Reference.Typology.DemDistanceSystem : Type

Number of distance contrasts in adnominal demonstratives (WALS Ch 41, @cite{diessel-2013}).

Two-way systems (proximal/distal) are by far the most common (54.3%), followed by three-way systems (37.6%). Systems with four or more distinctions are rare (< 6%).

Three-way systems subdivide into distance-oriented (proximal/medial/distal, about 2/3) and person-oriented (near speaker / near hearer / away from both, about 1/3). Japanese ko/so/a is the canonical person-oriented example.

• noContrast : DemDistanceSystem

  No distance contrast; demonstratives are distance-neutral (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.

instance Phenomena.Reference.Typology.instDecidableEqDemDistanceSystem : DecidableEq DemDistanceSystem

Equations

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

def Phenomena.Reference.Typology.instBEqDemDistanceSystem.beq : DemDistanceSystem → DemDistanceSystem → Bool

Equations

• Phenomena.Reference.Typology.instBEqDemDistanceSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqDemDistanceSystem : BEq DemDistanceSystem

Equations

• Phenomena.Reference.Typology.instBEqDemDistanceSystem = { beq := Phenomena.Reference.Typology.instBEqDemDistanceSystem.beq }

instance Phenomena.Reference.Typology.instReprDemDistanceSystem : Repr DemDistanceSystem

Equations

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

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

Equations

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

inductive Phenomena.Reference.Typology.DemOrientationType : Type

Whether a three-way demonstrative system is distance-oriented or person-oriented.

In a distance-oriented system (e.g. Hunzib), all three terms indicate relative distance from the speaker. In a person-oriented system (e.g. Japanese), one term specifically denotes proximity to the hearer.

@cite{diessel-2013} notes that about 2/3 of three-way systems are distance-oriented and about 1/3 are person-oriented.

• 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).

instance Phenomena.Reference.Typology.instDecidableEqDemOrientationType : DecidableEq DemOrientationType

Equations

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

def Phenomena.Reference.Typology.instBEqDemOrientationType.beq : DemOrientationType → DemOrientationType → Bool

Equations

• Phenomena.Reference.Typology.instBEqDemOrientationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqDemOrientationType : BEq DemOrientationType

Equations

• Phenomena.Reference.Typology.instBEqDemOrientationType = { beq := Phenomena.Reference.Typology.instBEqDemOrientationType.beq }

instance Phenomena.Reference.Typology.instReprDemOrientationType : Repr DemOrientationType

Equations

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

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

Equations

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

inductive Phenomena.Reference.Typology.DemFormRelation : Type

Relationship between pronominal and adnominal demonstratives (WALS Ch 42, @cite{diessel-2013}).

English uses the same forms ("this book" / "I like this"); French uses different stems (adnominal "ce"/"cette" vs pronominal "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, Korean i + defective noun).

• differentInflection : DemFormRelation

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

instance Phenomena.Reference.Typology.instDecidableEqDemFormRelation : DecidableEq DemFormRelation

Equations

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

def Phenomena.Reference.Typology.instBEqDemFormRelation.beq : DemFormRelation → DemFormRelation → Bool

Equations

• Phenomena.Reference.Typology.instBEqDemFormRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqDemFormRelation : BEq DemFormRelation

Equations

• Phenomena.Reference.Typology.instBEqDemFormRelation = { beq := Phenomena.Reference.Typology.instBEqDemFormRelation.beq }

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

Equations

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

instance Phenomena.Reference.Typology.instReprDemFormRelation : Repr DemFormRelation

Equations

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

inductive Phenomena.Reference.Typology.PronounDemRelation : Type

Relationship between third-person pronouns and demonstratives (WALS Ch 43, @cite{bhat-2013}).

In "two-person languages" (Bhat's term), 3rd-person pronouns are related to demonstratives -- the pronoun is either identical to a demonstrative or derived from one. In "three-person languages", 3rd-person pronouns form part of the person paradigm and are unrelated to demonstratives.

The majority of the world's languages (125/225 = 55.6%) show some relationship, supporting the diachronic pathway demonstrative -> 3rd-person pronoun.

• unrelated : PronounDemRelation

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

• relatedAll : PronounDemRelation

  Related to all demonstratives (e.g. Basque, where any demonstrative can serve as 3rd-person pronoun).

• relatedRemote : PronounDemRelation

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

• relatedNonRemote : PronounDemRelation

  Related specifically to non-remote (proximal or medial) demonstratives (e.g. Brahui: 3sg = medial demonstrative).

• relatedGender : PronounDemRelation

  Related via shared gender/noun-class markers (e.g. Venda: both show 21-class distinctions).

• relatedNonhuman : PronounDemRelation

  Demonstratives used as 3rd-person pronouns for nonhuman reference only (e.g. Jaqaru: 3sg "upa" for humans, demonstratives for nonhumans).

instance Phenomena.Reference.Typology.instDecidableEqPronounDemRelation : DecidableEq PronounDemRelation

Equations

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

def Phenomena.Reference.Typology.instBEqPronounDemRelation.beq : PronounDemRelation → PronounDemRelation → Bool

Equations

• Phenomena.Reference.Typology.instBEqPronounDemRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqPronounDemRelation : BEq PronounDemRelation

Equations

• Phenomena.Reference.Typology.instBEqPronounDemRelation = { beq := Phenomena.Reference.Typology.instBEqPronounDemRelation.beq }

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

Equations

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

instance Phenomena.Reference.Typology.instReprPronounDemRelation : Repr PronounDemRelation

Equations

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

def Phenomena.Reference.Typology.PronounDemRelation.isRelated : PronounDemRelation → Bool

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

Equations

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

structure Phenomena.Reference.Typology.ArticleDemProfile : Type

A language's article and demonstrative profile across all five WALS chapters.

Not all chapters have data for every language (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-oriented vs person-oriented (for 3-way systems)

• demFormType : Option DemFormRelation

  Ch 42: Pronominal vs adnominal demonstrative form

• pronDemRelation : Option PronounDemRelation

  Ch 43: 3rd-person pronoun ~ demonstrative relationship

instance Phenomena.Reference.Typology.instReprArticleDemProfile : Repr ArticleDemProfile

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.english : ArticleDemProfile

English (Indo-European, Germanic). Definite article "the" distinct from demonstratives "this"/"that". Indefinite article "a/an" distinct from numeral "one". Two-way demonstrative distance: this (proximal) vs that (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronouns ("he/she/it") unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.french : ArticleDemProfile

French (Indo-European, Romance). Definite article "le/la/les" distinct from demonstratives. Indefinite article "un/une" historically from numeral 'one' but now distinct (WALS codes French as indefinite word distinct from 'one'). Two-way demonstrative distance: ce N-ci (proximal) vs ce N-la (distal), though adnominal "ce" alone is distance-neutral. Different stems for pronominal ("celui/celle") vs adnominal ("ce/cette"). 3rd-person pronouns ("il/elle") unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.german : ArticleDemProfile

German (Indo-European, Germanic). Definite article "der/die/das" distinct from demonstratives. Indefinite article "ein" = numeral 'one' (phonological reduction in speech). Distance-neutral adnominal demonstratives: "dieser" and stressed "der/die/das" are deictically noncontrastive; distance expressed by adding adverbial "hier"/"da". Classified as no-contrast in WALS Ch 41. Different inflectional features: pronominal demonstratives inflect for case while adnominal demonstratives co-occur with inflected nouns. 3rd-person pronouns ("er/sie/es") unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.japanese : ArticleDemProfile

Japanese (Japonic). No definite or indefinite articles. Three-way person-oriented demonstrative system: ko- (near speaker), so- (near hearer), a- (away from both). The canonical person-oriented system. Different stems: adnominal kono/sono/ano vs pronominal kore/sore/are. 3rd-person pronouns ("kare/kanojo") unrelated to demonstratives (borrowed from Classical Chinese / relatively recent innovations).

Equations

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

def Phenomena.Reference.Typology.mandarin : ArticleDemProfile

Mandarin Chinese (Sino-Tibetan). No definite or indefinite articles (bare nouns are ambiguous for definiteness). Two-way demonstrative distance: zhe (proximal) vs na (distal). Same forms for pronominal and adnominal demonstratives (with optional classifier in adnominal use). 3rd-person pronoun "ta" unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.turkish : ArticleDemProfile

Turkish (Turkic). No definite article; indefinite article "bir" = numeral 'one' (different NP position when used as article vs numeral, per @cite{kornfilt-1997}). Two-way demonstrative distance: bu (proximal) vs o (distal), with su as a restricted medial form. WALS codes as two-way. Different inflectional features: pronominal demonstratives inflect for case and number, adnominal demonstratives are uninflected particles. 3rd-person pronoun "o" identical to distal demonstrative.

Equations

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

def Phenomena.Reference.Typology.arabic : ArticleDemProfile

Arabic (Egyptian) (Afro-Asiatic, Semitic). Definite prefix "al-" on nouns (definite affix). No indefinite article (unmarked nouns are indefinite, though tanwin in Standard Arabic marks indefiniteness). Two-way demonstrative distance: hada (proximal) vs daak (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronoun "huwa/hiya" unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.finnish : ArticleDemProfile

Finnish (Uralic). No definite or indefinite articles. Two-way demonstrative distance: tama (proximal) vs tuo/se (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronoun "han" (human) / "se" (nonhuman) -- "se" is identical to the distal demonstrative.

Equations

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

def Phenomena.Reference.Typology.hungarian : ArticleDemProfile

Hungarian (Uralic). Definite article "a/az" distinct from demonstratives. Indefinite article "egy" = numeral 'one'. Two-way demonstrative distance: ez (proximal) vs az (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronoun "o" unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.russian : ArticleDemProfile

Russian (Indo-European, Slavic). No definite or indefinite articles. Two-way demonstrative distance: etot (proximal) vs tot (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronouns ("on/ona/ono") unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.swahili : ArticleDemProfile

Swahili (Niger-Congo, Bantu). Demonstrative used as definite marker (precedes noun for definiteness, follows noun for deictic use; WALS Ch 37 value 2). No indefinite article. Three-way demonstrative distance: h- (proximal) / h-o (medial) / -le (distal). Same forms for pronominal and adnominal demonstratives. 3rd-person pronouns related via shared noun-class agreement prefixes (gender-marker relationship).

Equations

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

def Phenomena.Reference.Typology.tagalog : ArticleDemProfile

Tagalog (Austronesian, Philippine). Definite/indefinite distinction via case markers: "ang" (definite-like topic marker) vs "ng" (indefinite-like). WALS codes as definite word distinct from demonstratives. Two-way demonstrative distance: ito (proximal) vs iyon (distal), with middle term "iyan" sometimes yielding a three-way analysis. WALS codes as three-way. Same forms for pronominal and adnominal demonstratives. 3rd-person pronoun "siya" unrelated to demonstratives.

Equations

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

def Phenomena.Reference.Typology.latin : ArticleDemProfile

Latin (Indo-European, Italic). No definite or indefinite articles (bare nouns are ambiguous). Three-way distance-oriented demonstrative system: hic (proximal), iste (medial), ille (distal). This is the textbook three-way distance-oriented system. Same forms for pronominal and adnominal demonstratives (though with full case/gender/number inflection in both uses). 3rd-person pronoun "is/ea/id" distinct from but historically related to demonstratives (related to all demonstratives via shared inflection patterns).

Equations

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

def Phenomena.Reference.Typology.korean : ArticleDemProfile

Korean (Koreanic). No definite or indefinite articles (topic marker "-un"/"-nun" sometimes conveys definiteness pragmatically). Three-way person-oriented demonstrative system: i (near speaker), ku (near hearer), ce (away from both). Different stems: pronominal demonstratives formed by combining i/ku/ce with a "defective noun" like "il" (thing/fact), giving "i-il", "ku-il", etc. (@cite{sohn-1994}: 295, @cite{diessel-2013}). 3rd-person pronoun "ku" related to medial demonstrative "ku".

Equations

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

def Phenomena.Reference.Typology.danish : ArticleDemProfile

Danish (Indo-European, Germanic). Definite suffix "-en"/"-et" on nouns (definite affix); separate definite article "den/det" used when an adjective is present. Indefinite article "en/et" = numeral 'one'. Two-way demonstrative distance: denne (proximal) vs den (distal). Different inflectional features between pronominal and adnominal uses. 3rd-person pronouns ("han/hun/den/det") -- "den/det" related to demonstratives.

Equations

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

def Phenomena.Reference.Typology.hausa : ArticleDemProfile

Hausa (Afro-Asiatic, Chadic). No definite article; no standard indefinite article (WALS Ch 37 value 5). Four-way person-oriented demonstrative system: nan (near speaker), nan (near hearer, tonal difference), can (away from both), can (far away). Hausa is a key example of a four-or-more-way system. Same forms for pronominal and adnominal demonstratives. 3rd-person pronouns related to demonstratives.

Equations

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

def Phenomena.Reference.Typology.basque : ArticleDemProfile

Basque (language isolate). Definite suffix "-a"/"-ak" (definite affix). No indefinite article (bare nouns are indefinite). Two-way demonstrative distance: hau (proximal) vs hura (distal), with hori (medial) yielding a three-way system. Same forms for pronominal and adnominal demonstratives. 3rd-person pronouns: hau/hori/hura function as both demonstratives and 3rd-person pronouns (@cite{saltarelli-etal-1988}: 213).

Equations

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

def Phenomena.Reference.Typology.allLanguages : List ArticleDemProfile

All 16 language profiles.

Equations

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

theorem Phenomena.Reference.Typology.ch37_total : Phenomena.Reference.Typology.ch37✝.length = 620

theorem Phenomena.Reference.Typology.ch38_total : Phenomena.Reference.Typology.ch38✝.length = 534

theorem Phenomena.Reference.Typology.ch41_total : Phenomena.Reference.Typology.ch41✝.length = 234

theorem Phenomena.Reference.Typology.ch42_total : Phenomena.Reference.Typology.ch42✝.length = 201

theorem Phenomena.Reference.Typology.ch43_total : Phenomena.Reference.Typology.ch43✝.length = 225

structure Phenomena.Reference.Typology.DefiniteArticleCounts : Type

WALS Ch 37: Definite article distribution across 566 languages.

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

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

Equations

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

instance Phenomena.Reference.Typology.instReprDefiniteArticleCounts : Repr DefiniteArticleCounts

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.walsDefiniteArticle : DefiniteArticleCounts

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

Equations

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

structure Phenomena.Reference.Typology.IndefiniteArticleCounts : Type

WALS Ch 38: Indefinite article distribution across 473 languages.

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

instance Phenomena.Reference.Typology.instReprIndefiniteArticleCounts : Repr IndefiniteArticleCounts

Equations

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

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

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.walsIndefiniteArticle : IndefiniteArticleCounts

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

Equations

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

structure Phenomena.Reference.Typology.DemDistanceCounts : Type

WALS Ch 41: Demonstrative distance contrasts across 234 languages.

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

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

Equations

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

instance Phenomena.Reference.Typology.instReprDemDistanceCounts : Repr DemDistanceCounts

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.walsDemDistance : DemDistanceCounts

WALS Ch 41 distribution (@cite{diessel-2013}, n = 234).

Equations

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

structure Phenomena.Reference.Typology.DemFormCounts : Type

WALS Ch 42: Pronominal/adnominal demonstrative form across 201 languages.

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

instance Phenomena.Reference.Typology.instReprDemFormCounts : Repr DemFormCounts

Equations

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

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

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.walsDemForm : DemFormCounts

WALS Ch 42 distribution (@cite{diessel-2013}, n = 201).

Equations

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

structure Phenomena.Reference.Typology.PronounDemCounts : Type

WALS Ch 43: Third-person pronoun ~ demonstrative relationship across 225 languages.

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

instance Phenomena.Reference.Typology.instReprPronounDemCounts : Repr PronounDemCounts

Equations

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

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

Equations

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

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

Equations

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

def Phenomena.Reference.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 Phenomena.Reference.Typology.walsPronounDem : PronounDemCounts

WALS Ch 43 distribution (@cite{bhat-2013}, n = 225).

Equations

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

def Phenomena.Reference.Typology.walsDefArticle_generated : DefiniteArticleCounts

Ch 37 distribution counts derived from WALS generated data (n = 620).

Equations

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

theorem Phenomena.Reference.Typology.walsDefArticle_generated_total : walsDefArticle_generated.total = 620

def Phenomena.Reference.Typology.walsIndefArticle_generated : IndefiniteArticleCounts

Ch 38 distribution counts derived from WALS generated data (n = 534).

Equations

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

theorem Phenomena.Reference.Typology.walsIndefArticle_generated_total : walsIndefArticle_generated.total = 534

def Phenomena.Reference.Typology.walsDemDistance_generated : DemDistanceCounts

Ch 41 distribution counts derived from WALS generated data (n = 234).

Equations

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

theorem Phenomena.Reference.Typology.walsDemDistance_generated_total : walsDemDistance_generated.total = 234

def Phenomena.Reference.Typology.walsDemForm_generated : DemFormCounts

Ch 42 distribution counts derived from WALS generated data (n = 201).

Equations

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

theorem Phenomena.Reference.Typology.walsDemForm_generated_total : walsDemForm_generated.total = 201

def Phenomena.Reference.Typology.walsPronounDem_generated : PronounDemCounts

Ch 43 distribution counts derived from WALS generated data (n = 225).

Equations

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

theorem Phenomena.Reference.Typology.walsPronounDem_generated_total : walsPronounDem_generated.total = 225

theorem Phenomena.Reference.Typology.ch42_generated_matches_handcoded : walsDemForm_generated.sameForms = walsDemForm.sameForms ∧ walsDemForm_generated.differentStems = walsDemForm.differentStems ∧ walsDemForm_generated.differentInflection = walsDemForm.differentInflection

Ch 42 generated counts match hand-coded exactly.

theorem Phenomena.Reference.Typology.ch43_generated_matches_handcoded : walsPronounDem_generated.unrelated = walsPronounDem.unrelated ∧ walsPronounDem_generated.relatedAll = walsPronounDem.relatedAll ∧ walsPronounDem_generated.relatedRemote = walsPronounDem.relatedRemote ∧ walsPronounDem_generated.relatedNonRemote = walsPronounDem.relatedNonRemote ∧ walsPronounDem_generated.relatedGender = walsPronounDem.relatedGender ∧ walsPronounDem_generated.relatedNonhuman = walsPronounDem.relatedNonhuman

Ch 43 generated counts match hand-coded exactly.

theorem Phenomena.Reference.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, accounting for 127 of 234 languages in the WALS sample (54.3%).

@cite{diessel-2013}: "The vast majority of the world's languages employ two or three distance-marked demonstratives: 54.3 per cent of all languages shown on the map have adnominal demonstratives that express a two-way contrast."

theorem Phenomena.Reference.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-way systems together are under 10%.

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

Languages with definite articles tend to also have indefinite articles. The evidence: 81 languages have a definite article but no indefinite article (Ch 38, value 4), compared to 41 languages that have an indefinite article but no definite article (Ch 37, value 4).

This asymmetry suggests that definiteness marking is the typologically "prior" or more basic category: languages are more likely to grammaticalize definiteness without indefiniteness than vice versa.

Note: This is a tendency, not an absolute universal. The 41 exceptions (indefinite without definite) are concentrated in Asia (Turkey to Iran) and New Guinea.

theorem Phenomena.Reference.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 Phenomena.Reference.Typology.majority_pronoun_dem_related : walsPronounDem.totalRelated > walsPronounDem.unrelated

In a majority of languages surveyed (125 of 225 = 55.6%), third-person pronouns show some relationship to demonstratives. This supports the well-documented diachronic pathway: demonstrative -> 3rd-person pronoun.

@cite{bhat-2013} distinguishes "two-person languages" (3rd-person pronouns are demonstrative-derived, so the language really only has 1st/2nd person pronouns plus demonstratives) from "three-person languages" (3rd-person pronouns are independent).

theorem Phenomena.Reference.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 Phenomena.Reference.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}, Ch 42). Languages where adnominal demonstratives have different stems (37) or different inflectional features (21) are the minority.

Languages with same-form demonstratives are especially prevalent in Australia (where no language in the sample differentiates the two uses) and North America (except Pacific Northwest).

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

The grammaticalization cline: demonstrative -> definite article -> definite affix.

This is supported by the WALS data:

• 56 languages use demonstratives as definite markers (mid-cline)
• 84 languages have definite affixes (end of cline)
• 197 languages have definite words distinct from demonstratives (a stage where the article has diverged from the source demonstrative)

The 56 "demonstrative used as definite marker" languages represent the transitional stage where this grammaticalization is actively underway.

See @cite{greenberg-1978}, @cite{himmelmann-1997} for theoretical discussion.

theorem Phenomena.Reference.Typology.demonstratives_fill_article_gap : have totalWithoutDefArticle := walsDefiniteArticle.demonstrativeUsed + walsDefiniteArticle.noDefButIndef + walsDefiniteArticle.noArticle; walsDefiniteArticle.demonstrativeUsed > 0 ∧ totalWithoutDefArticle = 285

Among languages without dedicated definite articles, a substantial proportion (56 out of 285 article-less languages = 19.6%) use demonstratives to mark definiteness. This is the "demonstrative used as definite article" category from Ch 37.

This confirms the typological observation that demonstratives are the natural source for definiteness marking: even languages that lack a grammaticalized definite article often use demonstratives in definite contexts more frequently than expected.

theorem Phenomena.Reference.Typology.japanese_no_articles : japanese.defArticle = some DefiniteArticleType.noArticle ∧ japanese.indefArticle = some IndefiniteArticleType.noArticle

theorem Phenomena.Reference.Typology.mandarin_no_articles : mandarin.defArticle = some DefiniteArticleType.noArticle ∧ mandarin.indefArticle = some IndefiniteArticleType.noArticle

theorem Phenomena.Reference.Typology.russian_no_articles : russian.defArticle = some DefiniteArticleType.noArticle ∧ russian.indefArticle = some IndefiniteArticleType.noArticle

theorem Phenomena.Reference.Typology.latin_no_articles : latin.defArticle = some DefiniteArticleType.noArticle ∧ latin.indefArticle = some IndefiniteArticleType.noArticle

theorem Phenomena.Reference.Typology.korean_no_articles : korean.defArticle = some DefiniteArticleType.noArticle ∧ korean.indefArticle = some IndefiniteArticleType.noArticle

theorem Phenomena.Reference.Typology.english_has_both_articles : english.defArticle = some DefiniteArticleType.definiteWord ∧ english.indefArticle = some IndefiniteArticleType.indefiniteWord

theorem Phenomena.Reference.Typology.french_has_both_articles : french.defArticle = some DefiniteArticleType.definiteWord ∧ french.indefArticle = some IndefiniteArticleType.indefiniteWord

theorem Phenomena.Reference.Typology.arabic_definite_affix : arabic.defArticle = some DefiniteArticleType.definiteAffix

theorem Phenomena.Reference.Typology.danish_definite_affix : danish.defArticle = some DefiniteArticleType.definiteAffix

theorem Phenomena.Reference.Typology.basque_definite_affix : basque.defArticle = some DefiniteArticleType.definiteAffix

theorem Phenomena.Reference.Typology.japanese_person_oriented : japanese.demDistance = some DemDistanceSystem.threeWay ∧ japanese.demOrientation = some DemOrientationType.personOriented

theorem Phenomena.Reference.Typology.korean_person_oriented : korean.demDistance = some DemDistanceSystem.threeWay ∧ korean.demOrientation = some DemOrientationType.personOriented

theorem Phenomena.Reference.Typology.latin_distance_oriented : latin.demDistance = some DemDistanceSystem.threeWay ∧ latin.demOrientation = some DemOrientationType.distanceOriented

theorem Phenomena.Reference.Typology.german_no_dem_distance_contrast : german.demDistance = some DemDistanceSystem.noContrast

theorem Phenomena.Reference.Typology.hausa_four_way : hausa.demDistance = some DemDistanceSystem.fourWay

theorem Phenomena.Reference.Typology.turkish_pronoun_from_distal : turkish.pronDemRelation = some PronounDemRelation.relatedRemote

theorem Phenomena.Reference.Typology.basque_dem_as_pronoun : basque.pronDemRelation = some PronounDemRelation.relatedAll

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

Helper: does a profile have any definite marking?

Equations

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

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

Helper: does a profile have any indefinite article?

Equations

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

theorem Phenomena.Reference.Typology.indef_implies_def_almost : have withIndef := List.filter (fun (x : ArticleDemProfile) => x.hasIndefinite) allLanguages; have withIndefAndDef := List.filter (fun (x : ArticleDemProfile) => x.hasDefinite) withIndef; withIndef.length = 6 ∧ withIndefAndDef.length = 5

In our 16-language sample, all but one language with an indefinite article also has some form of definite marking (article, affix, or demonstrative used). The exception is Turkish, which has the numeral "bir" as an indefinite article but no dedicated definite article (WALS Ch 37, value 4).

This is consistent with the WALS aggregate data, which shows 41 languages with indefinite but no definite articles, concentrated in the Turkey-to-Iran belt and New Guinea.

theorem Phenomena.Reference.Typology.turkish_indef_without_def : turkish.hasIndefinite = true ∧ turkish.hasDefinite = false

Turkish is the one exception: indefinite article but no definite marking.

def Phenomena.Reference.Typology.hasThreeOrMoreDemContrasts (p : ArticleDemProfile) : Bool

In our sample, languages with three-way or larger demonstrative systems tend to lack articles entirely. 5 of the 7 languages with 3+ distance contrasts have no definite or indefinite articles.

Equations

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

theorem Phenomena.Reference.Typology.threeOrMore_count : (List.filter hasThreeOrMoreDemContrasts allLanguages).length = 7

Count of languages in our sample with three-way-or-more demonstratives.

def Phenomena.Reference.Typology.hasPronDemRelated (p : ArticleDemProfile) : Bool

8 of our 16 sample languages show some relationship between 3rd-person pronouns and demonstratives (Turkish, Finnish, Swahili, Latin, Korean, Danish, Hausa, Basque), consistent with Bhat's finding that a majority of languages worldwide (125 of 225) are "two-person languages."

Equations

• Phenomena.Reference.Typology.hasPronDemRelated p = match p.pronDemRelation with | some r => r.isRelated | none => false

theorem Phenomena.Reference.Typology.prondem_related_count : (List.filter hasPronDemRelated allLanguages).length = 8

inductive Phenomena.Reference.Typology.GrammaticalizationStage : Type

The grammaticalization hierarchy for definiteness marking, attested cross-linguistically:

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, French) Stage 3: Definite affix (e.g. Danish, Arabic, Basque)

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

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

instance Phenomena.Reference.Typology.instDecidableEqGrammaticalizationStage : DecidableEq GrammaticalizationStage

Equations

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

def Phenomena.Reference.Typology.instBEqGrammaticalizationStage.beq : GrammaticalizationStage → GrammaticalizationStage → Bool

Equations

• Phenomena.Reference.Typology.instBEqGrammaticalizationStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Typology.instBEqGrammaticalizationStage : BEq GrammaticalizationStage

Equations

• Phenomena.Reference.Typology.instBEqGrammaticalizationStage = { beq := Phenomena.Reference.Typology.instBEqGrammaticalizationStage.beq }

instance Phenomena.Reference.Typology.instReprGrammaticalizationStage : Repr GrammaticalizationStage

Equations

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

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

Equations

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

def Phenomena.Reference.Typology.DefiniteArticleType.stage : DefiniteArticleType → GrammaticalizationStage

Map a DefiniteArticleType to its grammaticalization stage.

Equations

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

def Phenomena.Reference.Typology.GrammaticalizationStage.ord : GrammaticalizationStage → Nat

The stages form a total order (higher = more grammaticalized).

Equations

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

theorem Phenomena.Reference.Typology.all_stages_attested : have stages := List.filterMap (fun (p : ArticleDemProfile) => Option.map DefiniteArticleType.stage p.defArticle) allLanguages; (stages.any fun (x : GrammaticalizationStage) => x == GrammaticalizationStage.noMarking) = true ∧ (stages.any fun (x : GrammaticalizationStage) => x == GrammaticalizationStage.demonstrative) = true ∧ (stages.any fun (x : GrammaticalizationStage) => x == GrammaticalizationStage.definiteWord) = true ∧ (stages.any fun (x : GrammaticalizationStage) => x == GrammaticalizationStage.definiteAffix) = true

All four stages of the grammaticalization cline are attested in our 16-language sample.

theorem Phenomena.Reference.Typology.english_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "eng") = english.defArticle

theorem Phenomena.Reference.Typology.french_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "fre") = french.defArticle

theorem Phenomena.Reference.Typology.german_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "ger") = german.defArticle

theorem Phenomena.Reference.Typology.finnish_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "fin") = finnish.defArticle

theorem Phenomena.Reference.Typology.hungarian_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "hun") = hungarian.defArticle

theorem Phenomena.Reference.Typology.korean_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "kor") = korean.defArticle

theorem Phenomena.Reference.Typology.russian_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "rus") = russian.defArticle

theorem Phenomena.Reference.Typology.turkish_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "tur") = turkish.defArticle

theorem Phenomena.Reference.Typology.arabic_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "aeg") = arabic.defArticle

theorem Phenomena.Reference.Typology.danish_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "dsh") = danish.defArticle

theorem Phenomena.Reference.Typology.swahili_ch37 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F37A.DefiniteArticleType) => Phenomena.Reference.Typology.fromWALS37A✝ x.value) (Core.WALS.F37A.lookup "swa") = swahili.defArticle

theorem Phenomena.Reference.Typology.english_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "eng") = english.indefArticle

theorem Phenomena.Reference.Typology.german_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "ger") = german.indefArticle

theorem Phenomena.Reference.Typology.finnish_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "fin") = finnish.indefArticle

theorem Phenomena.Reference.Typology.korean_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "kor") = korean.indefArticle

theorem Phenomena.Reference.Typology.russian_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "rus") = russian.indefArticle

theorem Phenomena.Reference.Typology.turkish_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "tur") = turkish.indefArticle

theorem Phenomena.Reference.Typology.arabic_ch38 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F38A.IndefiniteArticleType) => Phenomena.Reference.Typology.fromWALS38A✝ x.value) (Core.WALS.F38A.lookup "aeg") = arabic.indefArticle

theorem Phenomena.Reference.Typology.english_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "eng") = english.demDistance

theorem Phenomena.Reference.Typology.german_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "ger") = german.demDistance

theorem Phenomena.Reference.Typology.japanese_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "jpn") = japanese.demDistance

theorem Phenomena.Reference.Typology.mandarin_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "mnd") = mandarin.demDistance

theorem Phenomena.Reference.Typology.turkish_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "tur") = turkish.demDistance

theorem Phenomena.Reference.Typology.arabic_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "aeg") = arabic.demDistance

theorem Phenomena.Reference.Typology.finnish_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "fin") = finnish.demDistance

theorem Phenomena.Reference.Typology.hungarian_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "hun") = hungarian.demDistance

theorem Phenomena.Reference.Typology.russian_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "rus") = russian.demDistance

theorem Phenomena.Reference.Typology.korean_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "kor") = korean.demDistance

theorem Phenomena.Reference.Typology.basque_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "bsq") = basque.demDistance

theorem Phenomena.Reference.Typology.hausa_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "hau") = hausa.demDistance

theorem Phenomena.Reference.Typology.tagalog_ch41 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F41A.DistanceContrastsInDemonstratives) => Phenomena.Reference.Typology.fromWALS41A✝ x.value) (Core.WALS.F41A.lookup "tag") = tagalog.demDistance

theorem Phenomena.Reference.Typology.english_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "eng") = english.demFormType

theorem Phenomena.Reference.Typology.french_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "fre") = french.demFormType

theorem Phenomena.Reference.Typology.mandarin_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "mnd") = mandarin.demFormType

theorem Phenomena.Reference.Typology.turkish_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "tur") = turkish.demFormType

theorem Phenomena.Reference.Typology.arabic_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "aeg") = arabic.demFormType

theorem Phenomena.Reference.Typology.finnish_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "fin") = finnish.demFormType

theorem Phenomena.Reference.Typology.hungarian_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "hun") = hungarian.demFormType

theorem Phenomena.Reference.Typology.russian_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "rus") = russian.demFormType

theorem Phenomena.Reference.Typology.korean_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "kor") = korean.demFormType

theorem Phenomena.Reference.Typology.basque_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "bsq") = basque.demFormType

theorem Phenomena.Reference.Typology.hausa_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "hau") = hausa.demFormType

theorem Phenomena.Reference.Typology.tagalog_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "tag") = tagalog.demFormType

theorem Phenomena.Reference.Typology.swahili_ch42 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F42A.PronominalAndAdnominalDemonstratives) => Phenomena.Reference.Typology.fromWALS42A✝ x.value) (Core.WALS.F42A.lookup "swa") = swahili.demFormType

theorem Phenomena.Reference.Typology.japanese_ch43 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F43A.ThirdPersonPronounsAndDemonstratives) => Phenomena.Reference.Typology.fromWALS43A✝ x.value) (Core.WALS.F43A.lookup "jpn") = japanese.pronDemRelation

theorem Phenomena.Reference.Typology.turkish_ch43 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F43A.ThirdPersonPronounsAndDemonstratives) => Phenomena.Reference.Typology.fromWALS43A✝ x.value) (Core.WALS.F43A.lookup "tur") = turkish.pronDemRelation

theorem Phenomena.Reference.Typology.basque_ch43 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F43A.ThirdPersonPronounsAndDemonstratives) => Phenomena.Reference.Typology.fromWALS43A✝ x.value) (Core.WALS.F43A.lookup "bsq") = basque.pronDemRelation

theorem Phenomena.Reference.Typology.tagalog_ch43 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F43A.ThirdPersonPronounsAndDemonstratives) => Phenomena.Reference.Typology.fromWALS43A✝ x.value) (Core.WALS.F43A.lookup "tag") = tagalog.pronDemRelation