Cross-Linguistic Typology of Modality and Evidentiality (WALS Chapters 74--78)

@cite{aikhenvald-2004} @cite{de-haan-2013} @cite{vanbogaert-2013} @cite{deandradedehaanValenzuela-2013}

Cross-linguistic data on modality and evidentiality from the World Atlas of Language Structures, covering five parameters:

• Ch 74: Situational Possibility: How situational (root, dynamic) possibility ('can', 'be able to') is expressed --- verbal constructions, affixes on verbs, or other markers. Verbal constructions (modal verbs) are the dominant strategy (158/234 = 68%).

• Ch 75: Epistemic Possibility: How epistemic possibility ('may', 'might', 'perhaps') is expressed. Unlike situational possibility, affixes on verbs (84/240 = 35%) and other strategies (91/240 = 38%) together outweigh verbal constructions (65/240 = 27%).

• Ch 76: Overlap between Situational and Epistemic Modal Marking: Whether the same morpheme(s) express both situational and epistemic modality. Most languages show no overlap (105/207 = 51%), meaning they use distinct forms for root vs epistemic possibility. Some overlap for either possibility or necessity (66/207 = 32%), and fewer overlap for both (36/207 = 17%).

Cross-linguistic data on grammatical evidentiality, covering two parameters:

• Ch 77: Semantic Distinctions of Evidentiality: How many and which evidential distinctions a language grammaticalizes. Evidentials encode the speaker's source of information for a proposition --- whether they witnessed it directly, inferred it from indirect evidence, or received it via report. Languages range from no grammatical evidentials at all (English, Mandarin) to systems with three or more obligatory distinctions (Tuyuca, Quechua). The majority of the world's languages (181/418 = 43%) lack grammatical evidentials entirely.

• Ch 78: Coding of Evidentiality: How evidentiality is morphologically expressed. Six strategies: no grammatical evidentials, verbal affix or clitic (the dominant pattern among languages with evidentials, 131/418), part of the tense system, separate particle, modal morpheme, or mixed. Both chapters cover the same 418-language sample.

Key findings

@cite{de-haan-2013} observes that evidentiality is areally concentrated: it is pervasive in the Americas (especially the Andes and Amazonia), common across Central and Inner Asia (Tibetan, Turkic), and well-attested in the Balkans and Caucasus. In other parts of the world --- most of Africa, most of Western Europe, most of East Asia --- grammatical evidentials are absent. When present, evidentials are overwhelmingly verbal affixes; particles and clitics are comparatively rare. Systems with three or more evidential choices always include direct evidence as a grammaticalized category.

inductive Phenomena.Modality.Typology.EvidentialSystem : Type

WALS Ch 77: How many evidential distinctions a language grammaticalizes.

Four values on a scale of increasing complexity: (1) No grammatical evidentials: evidential source is conveyed lexically or pragmatically, never by obligatory morphology. (2) Indirect evidential only: the language has a single evidential marker indicating indirect (reported, inferred, or both) information source, but no dedicated marker for direct evidence. (3) Two-choice system (direct vs indirect): the language distinguishes direct evidence (visual/sensory witness) from indirect evidence (reportative, inferential, or both). (4) Three-or-more-choice system: the language distinguishes at least direct, reportative, and inferential evidence as separate categories. May include further distinctions (visual vs nonvisual, firsthand vs secondhand report, assumption vs inference from results).

• noGrammatical : EvidentialSystem

  No grammatical evidentials. Evidential source may be conveyed by lexical adverbs ("apparently", "reportedly") or pragmatic inference, but is never obligatorily encoded in verbal morphology. (e.g., English, French, Mandarin, German)

• indirectOnly : EvidentialSystem

  Indirect evidential only. A single marker indicates that the speaker's information comes from a non-direct source (inference, report, or both), with no dedicated direct-evidence marker. (e.g., Georgian, Tajik, West Greenlandic)

• directAndIndirect : EvidentialSystem

  Two-choice system: direct vs indirect evidence. The language obligatorily distinguishes firsthand sensory witness from all other information sources. (e.g., Turkish, Bulgarian, Tibetan, Abkhaz)

• threeOrMore : EvidentialSystem

  Three or more evidential choices. The language distinguishes at least direct, reportative, and inferential as separate grammatical categories. May include further splits. (e.g., Quechua, Tuyuca, Kashaya, Aymara)

instance Phenomena.Modality.Typology.instDecidableEqEvidentialSystem : DecidableEq EvidentialSystem

Equations

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

instance Phenomena.Modality.Typology.instBEqEvidentialSystem : BEq EvidentialSystem

Equations

• Phenomena.Modality.Typology.instBEqEvidentialSystem = { beq := Phenomena.Modality.Typology.instBEqEvidentialSystem.beq }

def Phenomena.Modality.Typology.instBEqEvidentialSystem.beq : EvidentialSystem → EvidentialSystem → Bool

Equations

• Phenomena.Modality.Typology.instBEqEvidentialSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Modality.Typology.instReprEvidentialSystem.repr : EvidentialSystem → Nat → Std.Format

Equations

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

instance Phenomena.Modality.Typology.instReprEvidentialSystem : Repr EvidentialSystem

Equations

• Phenomena.Modality.Typology.instReprEvidentialSystem = { reprPrec := Phenomena.Modality.Typology.instReprEvidentialSystem.repr }

def Phenomena.Modality.Typology.EvidentialSystem.hasEvidentials : EvidentialSystem → Bool

Whether a language has any grammatical evidential marking.

Equations

• Phenomena.Modality.Typology.EvidentialSystem.noGrammatical.hasEvidentials = false
• Phenomena.Modality.Typology.EvidentialSystem.indirectOnly.hasEvidentials = true
• Phenomena.Modality.Typology.EvidentialSystem.directAndIndirect.hasEvidentials = true
• Phenomena.Modality.Typology.EvidentialSystem.threeOrMore.hasEvidentials = true

def Phenomena.Modality.Typology.EvidentialSystem.hasDirect : EvidentialSystem → Bool

Whether a language grammaticalizes a direct evidence category.

Equations

• Phenomena.Modality.Typology.EvidentialSystem.directAndIndirect.hasDirect = true
• Phenomena.Modality.Typology.EvidentialSystem.threeOrMore.hasDirect = true
• Phenomena.Modality.Typology.EvidentialSystem.noGrammatical.hasDirect = false
• Phenomena.Modality.Typology.EvidentialSystem.indirectOnly.hasDirect = false

def Phenomena.Modality.Typology.EvidentialSystem.numChoices : EvidentialSystem → Nat

Number of evidential choices in the system (0, 1, 2, or 3+).

Equations

• Phenomena.Modality.Typology.EvidentialSystem.noGrammatical.numChoices = 0
• Phenomena.Modality.Typology.EvidentialSystem.indirectOnly.numChoices = 1
• Phenomena.Modality.Typology.EvidentialSystem.directAndIndirect.numChoices = 2
• Phenomena.Modality.Typology.EvidentialSystem.threeOrMore.numChoices = 3

inductive Phenomena.Modality.Typology.EvidentialCoding : Type

WALS Ch 78: How evidentiality is morphologically expressed.

Only applicable to languages that HAVE grammatical evidentials. Four coding strategies: (1) Verbal affix: evidential is a bound morpheme on the verb. (2) Clitic: evidential is a clitic (phrasal affix, not bound to verb). (3) Modal particle: evidential is a free-standing particle. (4) Part of the TAM system: evidential distinctions are fused with tense-aspect-mood marking and cannot be separated.

• verbalAffix : EvidentialCoding

  Evidential is a verbal affix or clitic (bound morpheme). The dominant strategy worldwide (131/418 languages in WALS Ch 78). (e.g., Quechua ‑mi, ‑si, ‑chá; Turkish ‑mIş; Tuyuca verbal suffixes)

• clitic : EvidentialCoding

  Evidential is a clitic (phrasal-level bound morpheme, not specific to the verb). WALS Ch 78 groups this with verbal affixes. (e.g., Tsafiki =ti, Kham =re)

• particle : EvidentialCoding

  Evidential is a free separate particle. (65/418 in WALS Ch 78). (e.g., Lhasa Tibetan 'dug, Kalmyk gej)

• partOfTAM : EvidentialCoding

  Evidential distinctions are fused into the tense-aspect-mood paradigm and cannot be isolated as a separate morpheme. (e.g., Bulgarian, Georgian, Abkhaz, some Turkic languages)

• notApplicable : EvidentialCoding

  Not applicable: language has no grammatical evidentials (Ch 77 value 1). Used for cross-chapter profile consistency.

instance Phenomena.Modality.Typology.instDecidableEqEvidentialCoding : DecidableEq EvidentialCoding

Equations

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

instance Phenomena.Modality.Typology.instBEqEvidentialCoding : BEq EvidentialCoding

Equations

• Phenomena.Modality.Typology.instBEqEvidentialCoding = { beq := Phenomena.Modality.Typology.instBEqEvidentialCoding.beq }

def Phenomena.Modality.Typology.instBEqEvidentialCoding.beq : EvidentialCoding → EvidentialCoding → Bool

Equations

• Phenomena.Modality.Typology.instBEqEvidentialCoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Modality.Typology.instReprEvidentialCoding.repr : EvidentialCoding → Nat → Std.Format

Equations

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

instance Phenomena.Modality.Typology.instReprEvidentialCoding : Repr EvidentialCoding

Equations

• Phenomena.Modality.Typology.instReprEvidentialCoding = { reprPrec := Phenomena.Modality.Typology.instReprEvidentialCoding.repr }

def Phenomena.Modality.Typology.EvidentialCoding.isBound : EvidentialCoding → Bool

Whether the coding strategy involves a bound morpheme (affix or clitic).

Equations

• Phenomena.Modality.Typology.EvidentialCoding.verbalAffix.isBound = true
• Phenomena.Modality.Typology.EvidentialCoding.clitic.isBound = true
• Phenomena.Modality.Typology.EvidentialCoding.particle.isBound = false
• Phenomena.Modality.Typology.EvidentialCoding.partOfTAM.isBound = false
• Phenomena.Modality.Typology.EvidentialCoding.notApplicable.isBound = false

structure Phenomena.Modality.Typology.WALSCount : Type

A single row in a WALS frequency table: a category label and its count.

• label : String
• count : Nat

def Phenomena.Modality.Typology.instReprWALSCount.repr : WALSCount → Nat → Std.Format

Equations

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

instance Phenomena.Modality.Typology.instReprWALSCount : Repr WALSCount

Equations

• Phenomena.Modality.Typology.instReprWALSCount = { reprPrec := Phenomena.Modality.Typology.instReprWALSCount.repr }

instance Phenomena.Modality.Typology.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Phenomena.Modality.Typology.instDecidableEqWALSCount = Phenomena.Modality.Typology.instDecidableEqWALSCount.decEq

def Phenomena.Modality.Typology.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Modality.Typology.instBEqWALSCount : BEq WALSCount

Equations

• Phenomena.Modality.Typology.instBEqWALSCount = { beq := Phenomena.Modality.Typology.instBEqWALSCount.beq }

def Phenomena.Modality.Typology.instBEqWALSCount.beq : WALSCount → WALSCount → Bool

Equations

• Phenomena.Modality.Typology.instBEqWALSCount.beq { label := a, count := a_1 } { label := b, count := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Modality.Typology.instBEqWALSCount.beq x✝¹ x✝ = false

def Phenomena.Modality.Typology.WALSCount.totalOf (cs : List WALSCount) : Nat

Sum of counts in a WALS table.

Equations

• Phenomena.Modality.Typology.WALSCount.totalOf cs = List.foldl (fun (acc : Nat) (c : Phenomena.Modality.Typology.WALSCount) => acc + c.count) 0 cs

def Phenomena.Modality.Typology.ch77Counts : List WALSCount

Chapter 77 distribution: semantic distinctions of evidentiality (N = 418).

Equations

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

def Phenomena.Modality.Typology.ch78Counts : List WALSCount

Chapter 78 distribution: coding of evidentiality (N = 418). Both chapters 77 and 78 cover the same 418-language sample.

Equations

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

theorem Phenomena.Modality.Typology.ch77_total : WALSCount.totalOf ch77Counts = 418

Ch 77 total: 418 languages.

theorem Phenomena.Modality.Typology.ch78_total : WALSCount.totalOf ch78Counts = 418

Ch 78 total: 418 languages.

theorem Phenomena.Modality.Typology.ch77_ch78_same_total : WALSCount.totalOf ch77Counts = WALSCount.totalOf ch78Counts

Ch 77 and Ch 78 cover the same 418-language sample.

theorem Phenomena.Modality.Typology.ch74_total : Phenomena.Modality.Typology.ch74✝.length = 234

theorem Phenomena.Modality.Typology.ch75_total : Phenomena.Modality.Typology.ch75✝.length = 240

theorem Phenomena.Modality.Typology.ch76_total : Phenomena.Modality.Typology.ch76✝.length = 207

theorem Phenomena.Modality.Typology.ch77_wals_total : Phenomena.Modality.Typology.ch77✝.length = 418

theorem Phenomena.Modality.Typology.ch78_wals_total : Phenomena.Modality.Typology.ch78✝.length = 418

theorem Phenomena.Modality.Typology.ch77_ch78_same_sample : Phenomena.Modality.Typology.ch77✝.length = Phenomena.Modality.Typology.ch78✝.length

Ch 77 and Ch 78 use the same sample in WALS v2020.4.

theorem Phenomena.Modality.Typology.ch74_verbal_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value == Core.WALS.F74A.SituationalPossibility.verbalConstructions) Phenomena.Modality.Typology.ch74✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value == Core.WALS.F74A.SituationalPossibility.affixesOnVerbs) Phenomena.Modality.Typology.ch74✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value == Core.WALS.F74A.SituationalPossibility.verbalConstructions) Phenomena.Modality.Typology.ch74✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value == Core.WALS.F74A.SituationalPossibility.otherKindsOfMarkers) Phenomena.Modality.Typology.ch74✝³).length

Ch 74: Verbal constructions are the dominant strategy for situational possibility (158/234 = 68%).

theorem Phenomena.Modality.Typology.ch75_more_even_distribution : have verbal := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value == Core.WALS.F75A.EpistemicPossibility.verbalConstructions) Phenomena.Modality.Typology.ch75✝).length; have affixes := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value == Core.WALS.F75A.EpistemicPossibility.affixesOnVerbs) Phenomena.Modality.Typology.ch75✝¹).length; have other := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value == Core.WALS.F75A.EpistemicPossibility.other) Phenomena.Modality.Typology.ch75✝²).length; verbal * 5 < Phenomena.Modality.Typology.ch75✝³.length * 2 ∧ affixes * 5 < Phenomena.Modality.Typology.ch75✝⁴.length * 2 ∧ other * 5 < Phenomena.Modality.Typology.ch75✝⁵.length * 2

Ch 75: The three coding strategies for epistemic possibility are more evenly distributed than for situational possibility.

theorem Phenomena.Modality.Typology.ch76_no_overlap_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value == Core.WALS.F76A.ModalOverlap.noOverlap) Phenomena.Modality.Typology.ch76✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value == Core.WALS.F76A.ModalOverlap.overlapForEitherPossibilityOrNecessity) Phenomena.Modality.Typology.ch76✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value == Core.WALS.F76A.ModalOverlap.noOverlap) Phenomena.Modality.Typology.ch76✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value == Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity) Phenomena.Modality.Typology.ch76✝³).length

Ch 76: Most languages show no overlap between situational and epistemic modal marking (105/207 = 51%).

theorem Phenomena.Modality.Typology.ch77_wals_no_evidentials_largest : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch77✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.indirectOnly) Phenomena.Modality.Typology.ch77✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch77✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.directAndIndirect) Phenomena.Modality.Typology.ch77✝³).length

Ch 77 (WALS): Languages without grammatical evidentials form the largest single category.

theorem Phenomena.Modality.Typology.ch78_wals_affix_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem) Phenomena.Modality.Typology.ch78✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝⁵).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝⁶).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.mixed) Phenomena.Modality.Typology.ch78✝⁷).length

Ch 78 (WALS): Verbal affix/clitic is the most common coding strategy among languages with evidentials.

structure Phenomena.Modality.Typology.EvidentialityProfile : Type

A language's evidentiality profile across WALS Chapters 77--78.

• language : String

  Language name

• iso : String

  ISO 639-3 code

• family : String

  Language family

• system : EvidentialSystem

  WALS Ch 77: evidential system type

• coding : EvidentialCoding

  WALS Ch 78: coding strategy

• markers : List String

  Evidential marker forms (if applicable)

• notes : String

  Notes on the evidential system

def Phenomena.Modality.Typology.instReprEvidentialityProfile.repr : EvidentialityProfile → Nat → Std.Format

Equations

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

instance Phenomena.Modality.Typology.instReprEvidentialityProfile : Repr EvidentialityProfile

Equations

• Phenomena.Modality.Typology.instReprEvidentialityProfile = { reprPrec := Phenomena.Modality.Typology.instReprEvidentialityProfile.repr }

def Phenomena.Modality.Typology.instDecidableEqEvidentialityProfile.decEq (x✝ x✝¹ : EvidentialityProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Modality.Typology.instDecidableEqEvidentialityProfile : DecidableEq EvidentialityProfile

Equations

• Phenomena.Modality.Typology.instDecidableEqEvidentialityProfile = Phenomena.Modality.Typology.instDecidableEqEvidentialityProfile.decEq

instance Phenomena.Modality.Typology.instBEqEvidentialityProfile : BEq EvidentialityProfile

Equations

• Phenomena.Modality.Typology.instBEqEvidentialityProfile = { beq := Phenomena.Modality.Typology.instBEqEvidentialityProfile.beq }

def Phenomena.Modality.Typology.instBEqEvidentialityProfile.beq : EvidentialityProfile → EvidentialityProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.Typology.instBEqEvidentialityProfile.beq x✝¹ x✝ = false

def Phenomena.Modality.Typology.english : EvidentialityProfile

English (Indo-European, Germanic). No grammatical evidentials. Evidential source is conveyed lexically by adverbs like "apparently", "reportedly", "evidently", or by hedging expressions like "I hear that...", "it seems that...". None of these are obligatory or part of the verbal paradigm.

Equations

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

def Phenomena.Modality.Typology.french : EvidentialityProfile

French (Indo-European, Romance). No grammatical evidentials. The conditional tense can convey reportative meaning in journalistic French ("le president serait malade" — 'the president is reportedly sick'), but this is not a dedicated evidential marker; it is a secondary use of the conditional.

Equations

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

def Phenomena.Modality.Typology.german : EvidentialityProfile

German (Indo-European, Germanic). No grammatical evidentials. The modal verbs "sollen" (reportative) and "wollen" (self-report) have evidential-like uses but are full modal verbs, not grammaticalized evidential markers.

Equations

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

def Phenomena.Modality.Typology.mandarin : EvidentialityProfile

Mandarin Chinese (Sino-Tibetan). No grammatical evidentials. Evidential source is conveyed by lexical items such as "tinshuo" (听说, 'I hear that'), "juede" (觉得, 'I feel that'), or sentence-final particles like "ba" (吧) for tentativeness.

Equations

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

def Phenomena.Modality.Typology.japanese : EvidentialityProfile

Japanese (Japonic). No grammatical evidentials in the strict sense. The hearsay particle "soo da" (そうだ) and inferential "rashii" (らしい) have evidential-like functions but are analyzed as modal rather than evidential morphology by @cite{de-haan-2013}. WALS classifies Japanese as lacking grammatical evidentials.

Equations

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

def Phenomena.Modality.Typology.korean : EvidentialityProfile

Korean (Koreanic). No grammatical evidentials. Korean has evidential-like constructions (e.g., "-deo-" retrospective, "-da-" reported speech) but these are not classified as grammaticalized evidentials in WALS.

Equations

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

def Phenomena.Modality.Typology.turkish : EvidentialityProfile

Turkish (Turkic). Two-choice evidential system: direct vs indirect. The past tense paradigm contrasts direct-evidence past (-DI, witnessed) with indirect-evidence past (-mIş, inferred or reported). The -mIş suffix is the best-known example of an indirect evidential in a major language. The distinction is obligatory in past-tense contexts. Coded as part of the TAM system (evidentiality is fused with past tense).

Equations

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

def Phenomena.Modality.Typology.bulgarian : EvidentialityProfile

Bulgarian (Indo-European, Slavic). Two-choice evidential system: direct (witnessed) vs indirect (reported, nonwitnessed). Bulgarian is the best-known European language with grammatical evidentials. The distinction is marked by a contrast between the aorist (direct/witnessed) and a separate evidential paradigm (indirect/nonwitnessed). Fused with the TAM system.

Equations

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

def Phenomena.Modality.Typology.tibetan : EvidentialityProfile

Tibetan (Sino-Tibetan, Tibeto-Burman). Two-choice evidential system: direct (egophoric/sensory) vs indirect. Lhasa Tibetan uses the copula/auxiliary contrast: "red" and "yod" for personal knowledge/direct evidence, "yin" and "'dug" for indirect/new information. The evidential markers are particles/auxiliaries.

Equations

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

def Phenomena.Modality.Typology.georgian : EvidentialityProfile

Georgian (Kartvelian). Indirect evidential only. Georgian has an evidential perfect (the "I screeve") that marks the proposition as based on inference or report, but has no dedicated direct-evidence marker. The evidential distinction is fused with the TAM system (part of the verbal screeve paradigm).

Equations

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

def Phenomena.Modality.Typology.quechua : EvidentialityProfile

Quechua (Cuzco) (Quechuan). Three-or-more-choice system: direct (‑mi, ‑n), reportative (‑si, ‑s), and conjectural (‑chá). The three enclitics are obligatory on finite clauses and encode the speaker's information source. Quechua is one of the canonical examples of a three-way evidential system. Coded as verbal affixes (enclitics on the verb or predicate).

Equations

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

def Phenomena.Modality.Typology.aymara : EvidentialityProfile

Aymara (Aymaran). Three-or-more-choice system: direct/personal knowledge, reportative, and non-personal knowledge (inferential). Like Quechua, Aymara has obligatory evidential suffixes marking information source. Coded as verbal affixes.

Equations

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

def Phenomena.Modality.Typology.tuyuca : EvidentialityProfile

Tuyuca (Tucanoan). Three-or-more-choice system with one of the richest evidential inventories known: five evidential categories --- visual, nonvisual sensory, apparent (inferential), secondhand (reported), and assumed. All five are obligatorily encoded as verbal suffixes. @cite{barnes-1984} is the classic description. Coded as verbal affixes.

Equations

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

def Phenomena.Modality.Typology.kashaya : EvidentialityProfile

Kashaya (Pomoan). Three-or-more-choice system: performative/factual (direct), visual, auditory, inferential, and reportative. Coded as verbal suffixes. Kashaya is notable for distinguishing visual from auditory direct evidence. @cite{oswalt-1986} is the primary source.

Equations

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

def Phenomena.Modality.Typology.tariana : EvidentialityProfile

Tariana (Arawakan). Three-or-more-choice system with five evidential categories: visual, nonvisual, inferred, assumed, and reported. Like Tuyuca, Tariana has a five-way system. It is spoken in the multilingual Vaupés area of Brazil where elaborate evidential systems are an areal feature. Verbal affixes.

Equations

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

def Phenomena.Modality.Typology.westGreenlandic : EvidentialityProfile

West Greenlandic (Eskimo-Aleut). Indirect evidential only. West Greenlandic has an inferential mood (expressed by verbal suffixes) but no grammaticalized direct-evidence marker. The speaker uses the inferential when the proposition is based on reasoning from observable effects.

Equations

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

def Phenomena.Modality.Typology.abkhaz : EvidentialityProfile

Abkhaz (Northwest Caucasian). Two-choice system: direct (witnessed) vs indirect (nonwitnessed/reported). The evidential distinction is part of the complex verbal morphology and is fused with tense-aspect marking.

Equations

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

def Phenomena.Modality.Typology.finnish : EvidentialityProfile

Finnish (Uralic). No grammatical evidentiality system. Finnish has modal verbs (voida 'can', täytyä 'must', saattaa 'may') but evidential meanings are expressed lexically, not as part of obligatory verbal morphology.

Equations

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

def Phenomena.Modality.Typology.allLanguages : List EvidentialityProfile

All language profiles in the sample.

Equations

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

def Phenomena.Modality.Typology.EvidentialityProfile.hasEvidentials (p : EvidentialityProfile) : Bool

Does a language have grammatical evidentials?

Equations

• p.hasEvidentials = p.system.hasEvidentials

def Phenomena.Modality.Typology.EvidentialityProfile.hasDirect (p : EvidentialityProfile) : Bool

Does a language have a direct evidence category?

Equations

• p.hasDirect = p.system.hasDirect

def Phenomena.Modality.Typology.countBySystem (langs : List EvidentialityProfile) (s : EvidentialSystem) : Nat

Count of languages in the sample with a given system type.

Equations

• Phenomena.Modality.Typology.countBySystem langs s = (List.filter (fun (x : Phenomena.Modality.Typology.EvidentialityProfile) => x.system == s) langs).length

def Phenomena.Modality.Typology.countByCoding (langs : List EvidentialityProfile) (c : EvidentialCoding) : Nat

Count of languages in the sample with a given coding type.

Equations

• Phenomena.Modality.Typology.countByCoding langs c = (List.filter (fun (x : Phenomena.Modality.Typology.EvidentialityProfile) => x.coding == c) langs).length

theorem Phenomena.Modality.Typology.sample_size : allLanguages.length = 18

Number of languages in our sample.

theorem Phenomena.Modality.Typology.english_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "eng") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.german_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "ger") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.french_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "fre") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.japanese_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "jpn") = some Core.WALS.F74A.SituationalPossibility.affixesOnVerbs

theorem Phenomena.Modality.Typology.mandarin_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "mnd") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.korean_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "kor") = some Core.WALS.F74A.SituationalPossibility.otherKindsOfMarkers

theorem Phenomena.Modality.Typology.turkish_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "tur") = some Core.WALS.F74A.SituationalPossibility.affixesOnVerbs

theorem Phenomena.Modality.Typology.finnish_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "fin") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.georgian_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "geo") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.abkhaz_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "abk") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.aymara_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "aym") = some Core.WALS.F74A.SituationalPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.westGreenlandic_ch74 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F74A.SituationalPossibility) => x.value) (Core.WALS.F74A.lookup "grw") = some Core.WALS.F74A.SituationalPossibility.affixesOnVerbs

theorem Phenomena.Modality.Typology.english_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "eng") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.german_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "ger") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.french_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "fre") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.japanese_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "jpn") = some Core.WALS.F75A.EpistemicPossibility.other

theorem Phenomena.Modality.Typology.mandarin_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "mnd") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.korean_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "kor") = some Core.WALS.F75A.EpistemicPossibility.other

theorem Phenomena.Modality.Typology.turkish_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "tur") = some Core.WALS.F75A.EpistemicPossibility.affixesOnVerbs

theorem Phenomena.Modality.Typology.finnish_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "fin") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.georgian_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "geo") = some Core.WALS.F75A.EpistemicPossibility.other

theorem Phenomena.Modality.Typology.abkhaz_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "abk") = some Core.WALS.F75A.EpistemicPossibility.verbalConstructions

theorem Phenomena.Modality.Typology.aymara_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "aym") = some Core.WALS.F75A.EpistemicPossibility.other

theorem Phenomena.Modality.Typology.westGreenlandic_ch75 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F75A.EpistemicPossibility) => x.value) (Core.WALS.F75A.lookup "grw") = some Core.WALS.F75A.EpistemicPossibility.affixesOnVerbs

theorem Phenomena.Modality.Typology.english_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "eng") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.german_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "ger") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.french_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "fre") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.japanese_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "jpn") = some Core.WALS.F76A.ModalOverlap.overlapForEitherPossibilityOrNecessity

theorem Phenomena.Modality.Typology.mandarin_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "mnd") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.korean_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "kor") = some Core.WALS.F76A.ModalOverlap.overlapForEitherPossibilityOrNecessity

theorem Phenomena.Modality.Typology.turkish_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "tur") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.finnish_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "fin") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.georgian_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "geo") = some Core.WALS.F76A.ModalOverlap.overlapForEitherPossibilityOrNecessity

theorem Phenomena.Modality.Typology.abkhaz_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "abk") = some Core.WALS.F76A.ModalOverlap.overlapForEitherPossibilityOrNecessity

theorem Phenomena.Modality.Typology.aymara_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "aym") = some Core.WALS.F76A.ModalOverlap.noOverlap

theorem Phenomena.Modality.Typology.westGreenlandic_ch76 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F76A.ModalOverlap) => x.value) (Core.WALS.F76A.lookup "grw") = some Core.WALS.F76A.ModalOverlap.overlapForBothPossibilityAndNecessity

theorem Phenomena.Modality.Typology.english_ch77 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => Phenomena.Modality.Typology.fromWALS77A✝ x.value) (Core.WALS.F77A.lookup "eng") = some english.system

theorem Phenomena.Modality.Typology.mandarin_ch77 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => Phenomena.Modality.Typology.fromWALS77A✝ x.value) (Core.WALS.F77A.lookup "mnd") = some mandarin.system

theorem Phenomena.Modality.Typology.turkish_ch77 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => Phenomena.Modality.Typology.fromWALS77A✝ x.value) (Core.WALS.F77A.lookup "tur") = some turkish.system

theorem Phenomena.Modality.Typology.bulgarian_ch77 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => Phenomena.Modality.Typology.fromWALS77A✝ x.value) (Core.WALS.F77A.lookup "bul") = some bulgarian.system

theorem Phenomena.Modality.Typology.westGreenlandic_ch77 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => Phenomena.Modality.Typology.fromWALS77A✝ x.value) (Core.WALS.F77A.lookup "grw") = some westGreenlandic.system

theorem Phenomena.Modality.Typology.english_ch78 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => Phenomena.Modality.Typology.fromWALS78A✝ x.value) (Core.WALS.F78A.lookup "eng") = some english.coding

theorem Phenomena.Modality.Typology.mandarin_ch78 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => Phenomena.Modality.Typology.fromWALS78A✝ x.value) (Core.WALS.F78A.lookup "mnd") = some mandarin.coding

theorem Phenomena.Modality.Typology.turkish_ch78 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => Phenomena.Modality.Typology.fromWALS78A✝ x.value) (Core.WALS.F78A.lookup "tur") = some turkish.coding

theorem Phenomena.Modality.Typology.bulgarian_ch78 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => Phenomena.Modality.Typology.fromWALS78A✝ x.value) (Core.WALS.F78A.lookup "bul") = some bulgarian.coding

theorem Phenomena.Modality.Typology.tuyuca_ch78_raw : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value) (Core.WALS.F78A.lookup "tuy") = some Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem

theorem Phenomena.Modality.Typology.tariana_ch78_raw : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value) (Core.WALS.F78A.lookup "tar") = some Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem

theorem Phenomena.Modality.Typology.kashaya_ch78_raw : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value) (Core.WALS.F78A.lookup "ksh") = some Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic

theorem Phenomena.Modality.Typology.westGreenlandic_ch78_raw : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value) (Core.WALS.F78A.lookup "grw") = some Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic

theorem Phenomena.Modality.Typology.no_evidentials_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch77✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.indirectOnly) Phenomena.Modality.Typology.ch77✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch77✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.directAndIndirect) Phenomena.Modality.Typology.ch77✝³).length

Ch 77: The plurality of languages (181/418 = 43%) lack grammatical evidentials entirely. This is the single largest category.

theorem Phenomena.Modality.Typology.no_evidentials_not_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch77✝).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.indirectOnly) Phenomena.Modality.Typology.ch77✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.directAndIndirect) Phenomena.Modality.Typology.ch77✝²).length

Ch 77: Languages without grammatical evidentials do NOT outnumber all languages with evidentials combined (181 vs 166 + 71 = 237).

theorem Phenomena.Modality.Typology.sample_no_evidentials_count : countBySystem allLanguages EvidentialSystem.noGrammatical = 7

In our sample, over a third of languages lack grammatical evidentials (7 out of 18). The sample deliberately overrepresents languages with evidentials for typological diversity.

theorem Phenomena.Modality.Typology.verbal_affix_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem) Phenomena.Modality.Typology.ch78✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝⁵).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝⁶).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.mixed) Phenomena.Modality.Typology.ch78✝⁷).length

Ch 78: Verbal affix or clitic (131/418) is the most common way to encode evidentiality among languages that have it.

theorem Phenomena.Modality.Typology.verbal_affix_majority_of_evidential_langs : have withEvid := List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value != Core.WALS.F78A.EvidentialityCoding.noGrammaticalEvidentials) Phenomena.Modality.Typology.ch78✝; (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝¹).length * 2 > withEvid.length

Ch 78: Among languages WITH evidentials, verbal affixes account for more than half of all coding strategies (131 out of 237).

theorem Phenomena.Modality.Typology.modal_morpheme_rarest : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.mixed) Phenomena.Modality.Typology.ch78✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝²).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem) Phenomena.Modality.Typology.ch78✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝⁴).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝⁵).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝⁶).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.verbalAffixOrClitic) Phenomena.Modality.Typology.ch78✝⁷).length

Ch 78: Modal morpheme is the rarest evidential coding strategy (7/418).

theorem Phenomena.Modality.Typology.indirect_only_more_common_than_two_choice : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.indirectOnly) Phenomena.Modality.Typology.ch77✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.directAndIndirect) Phenomena.Modality.Typology.ch77✝¹).length

Ch 77: Among languages with evidentials, indirect-only systems (166) are more common than direct-and-indirect systems (71).

theorem Phenomena.Modality.Typology.indirect_only_most_common_with_evidentials : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.indirectOnly) Phenomena.Modality.Typology.ch77✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F77A.EvidentialityDistinctions) => x.value == Core.WALS.F77A.EvidentialityDistinctions.directAndIndirect) Phenomena.Modality.Typology.ch77✝¹).length

Ch 77: Indirect-only systems are the most common type among languages that HAVE evidentials.

theorem Phenomena.Modality.Typology.three_or_more_always_has_direct : have threeOrMore := List.filter (fun (x : EvidentialityProfile) => x.system == EvidentialSystem.threeOrMore) allLanguages; (threeOrMore.all fun (x : EvidentialityProfile) => x.hasDirect) = true

Languages with three or more evidential choices always include a direct evidence category. This follows from the definition: three-choice systems distinguish direct, reportative, and inferential. No language is known to have three evidential categories without including direct evidence.

In our sample, every three-or-more language has a direct category.

theorem Phenomena.Modality.Typology.direct_implies_at_least_two_choices : have withDirect := List.filter (fun (x : EvidentialityProfile) => x.hasDirect) allLanguages; (withDirect.all fun (p : EvidentialityProfile) => p.system == EvidentialSystem.directAndIndirect || p.system == EvidentialSystem.threeOrMore) = true

The converse does not hold: two-choice systems also have direct evidence. In fact, in our sample, every language with direct evidence has either a two-choice or three-or-more system.

theorem Phenomena.Modality.Typology.tam_fusion_in_sample : turkish.coding = EvidentialCoding.partOfTAM ∧ bulgarian.coding = EvidentialCoding.partOfTAM ∧ georgian.coding = EvidentialCoding.partOfTAM ∧ abkhaz.coding = EvidentialCoding.partOfTAM

Evidentiality fused with the TAM system is characteristic of the Balkans and Caucasus. In our sample, Turkish, Bulgarian, Georgian, and Abkhaz all use TAM-fused evidentials.

theorem Phenomena.Modality.Typology.separate_particle_second_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.partOfTheTenseSystem) Phenomena.Modality.Typology.ch78✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.modalMorpheme) Phenomena.Modality.Typology.ch78✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.separateParticle) Phenomena.Modality.Typology.ch78✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F78A.EvidentialityCoding) => x.value == Core.WALS.F78A.EvidentialityCoding.mixed) Phenomena.Modality.Typology.ch78✝⁵).length

Separate particle is the second most common coding strategy after verbal affix or clitic (65/418 vs 131/418).

theorem Phenomena.Modality.Typology.andean_evidential_cluster : quechua.system = EvidentialSystem.threeOrMore ∧ aymara.system = EvidentialSystem.threeOrMore ∧ quechua.coding = EvidentialCoding.verbalAffix ∧ aymara.coding = EvidentialCoding.verbalAffix

Quechua and Aymara, the two major Andean language families, both have three-or-more-choice evidential systems coded as verbal affixes. This is a well-known areal feature of the Andes.

theorem Phenomena.Modality.Typology.amazonian_rich_systems : tuyuca.system = EvidentialSystem.threeOrMore ∧ tariana.system = EvidentialSystem.threeOrMore ∧ tuyuca.coding = EvidentialCoding.verbalAffix ∧ tariana.coding = EvidentialCoding.verbalAffix

The Vaupés-Amazonian area has some of the richest evidential systems. Both Tuyuca and Tariana (from different families but in contact in the Vaupés) have three-or-more evidential categories with five distinctions. This suggests areal diffusion of complex evidential systems.

theorem Phenomena.Modality.Typology.indirect_only_least_common_among_evidentials : 38 < 71

Ch 77: Indirect-only systems (38 languages) are the least common type among languages WITH evidentials (vs 71 two-choice and 28 three-choice). These are languages that only mark non-direct evidence, leaving direct evidence unmarked.

theorem Phenomena.Modality.Typology.sample_indirect_only_count : countBySystem allLanguages EvidentialSystem.indirectOnly = 2

In our sample, exactly 2 languages have indirect-only systems.

theorem Phenomena.Modality.Typology.complex_systems_use_affixes : have complex := List.filter (fun (x : EvidentialityProfile) => x.system == EvidentialSystem.threeOrMore) allLanguages; (complex.all fun (x : EvidentialityProfile) => x.coding == EvidentialCoding.verbalAffix) = true

In our sample, all languages with three-or-more evidential choices use verbal affixes as their coding strategy. This is consistent with the cross-linguistic generalization that complex evidential systems tend to use morphologically integrated (affixal) coding.

def Phenomena.Modality.Typology.westernEuropean : List EvidentialityProfile

In our sample, the three Western European languages (English, French, German) all lack grammatical evidentials. This is consistent with the broader pattern: grammatical evidentials are essentially absent from Western Europe (the Balkan Sprachbund is the notable exception).

Equations

• Phenomena.Modality.Typology.westernEuropean = [Phenomena.Modality.Typology.english, Phenomena.Modality.Typology.french, Phenomena.Modality.Typology.german]

theorem Phenomena.Modality.Typology.western_european_no_evidentials : (westernEuropean.all fun (x : EvidentialityProfile) => x.system == EvidentialSystem.noGrammatical) = true

theorem Phenomena.Modality.Typology.no_evidentials_implies_na_coding : have noEvid := List.filter (fun (x : EvidentialityProfile) => x.system == EvidentialSystem.noGrammatical) allLanguages; (noEvid.all fun (x : EvidentialityProfile) => x.coding == EvidentialCoding.notApplicable) = true

In our sample, every language without grammatical evidentials (Ch 77) has a notApplicable coding (Ch 78).

theorem Phenomena.Modality.Typology.evidentials_implies_real_coding : have withEvid := List.filter (fun (x : EvidentialityProfile) => x.hasEvidentials) allLanguages; (withEvid.all fun (x : EvidentialityProfile) => x.coding != EvidentialCoding.notApplicable) = true

In our sample, every language WITH grammatical evidentials has a real (non-notApplicable) coding strategy.

theorem Phenomena.Modality.Typology.system_coding_consistency : (allLanguages.all fun (p : EvidentialityProfile) => (p.system == EvidentialSystem.noGrammatical) == (p.coding == EvidentialCoding.notApplicable)) = true

The system and coding fields are consistent: the set of languages with notApplicable coding is exactly the set with noGrammatical system.

theorem Phenomena.Modality.Typology.sample_system_counts : countBySystem allLanguages EvidentialSystem.noGrammatical = 7 ∧ countBySystem allLanguages EvidentialSystem.indirectOnly = 2 ∧ countBySystem allLanguages EvidentialSystem.directAndIndirect = 4 ∧ countBySystem allLanguages EvidentialSystem.threeOrMore = 5

System type distribution in our sample.

theorem Phenomena.Modality.Typology.sample_coding_counts : countByCoding allLanguages EvidentialCoding.verbalAffix = 6 ∧ countByCoding allLanguages EvidentialCoding.clitic = 0 ∧ countByCoding allLanguages EvidentialCoding.particle = 1 ∧ countByCoding allLanguages EvidentialCoding.partOfTAM = 4 ∧ countByCoding allLanguages EvidentialCoding.notApplicable = 7

Coding strategy distribution in our sample (excluding notApplicable).

theorem Phenomena.Modality.Typology.sample_has_evidentials_count : (List.filter (fun (x : EvidentialityProfile) => x.hasEvidentials) allLanguages).length = 11

Languages with evidentials in our sample.

theorem Phenomena.Modality.Typology.sample_has_direct_count : (List.filter (fun (x : EvidentialityProfile) => x.hasDirect) allLanguages).length = 9

Languages with direct evidence marking in our sample.

theorem Phenomena.Modality.Typology.evidential_complexity_hierarchy : EvidentialSystem.threeOrMore.numChoices > EvidentialSystem.directAndIndirect.numChoices ∧ EvidentialSystem.directAndIndirect.numChoices > EvidentialSystem.indirectOnly.numChoices ∧ EvidentialSystem.indirectOnly.numChoices > EvidentialSystem.noGrammatical.numChoices

The evidential complexity hierarchy: more evidential categories imply at least as many categories as simpler systems. In our sample:

threeOrMore.numChoices > directAndIndirect.numChoices > indirectOnly.numChoices > noGrammatical.numChoices

theorem Phenomena.Modality.Typology.three_or_more_implies_direct_in_sample : (allLanguages.all fun (p : EvidentialityProfile) => decide ((p.system == EvidentialSystem.threeOrMore) = true → p.hasDirect = true)) = true

In our sample, every language with a three-or-more system also has a direct evidence category (entailed by the type definition, but worth verifying against the data).

theorem Phenomena.Modality.Typology.two_choice_implies_direct_in_sample : have twoChoice := List.filter (fun (x : EvidentialityProfile) => x.system == EvidentialSystem.directAndIndirect) allLanguages; (twoChoice.all fun (x : EvidentialityProfile) => x.hasDirect) = true

In our sample, every language with a two-choice system also has a direct evidence category (the two choices are direct vs indirect).

def Phenomena.Modality.Typology.eastAsian : List EvidentialityProfile

East Asian languages in our sample (Mandarin, Japanese, Korean) all lack grammatical evidentials. This is consistent with the broader pattern that East Asia is an evidential-free zone.

Equations

• Phenomena.Modality.Typology.eastAsian = [Phenomena.Modality.Typology.mandarin, Phenomena.Modality.Typology.japanese, Phenomena.Modality.Typology.korean]

theorem Phenomena.Modality.Typology.east_asian_no_evidentials : (eastAsian.all fun (x : EvidentialityProfile) => x.system == EvidentialSystem.noGrammatical) = true

def Phenomena.Modality.Typology.americas : List EvidentialityProfile

Americas languages in our sample (Quechua, Aymara, Tuyuca, Kashaya, Tariana) all have three-or-more evidential categories. The Americas have the highest density of complex evidential systems worldwide.

Equations

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

theorem Phenomena.Modality.Typology.americas_all_complex_evidentials : (americas.all fun (x : EvidentialityProfile) => x.system == EvidentialSystem.threeOrMore) = true

theorem Phenomena.Modality.Typology.americas_all_verbal_affix : (americas.all fun (x : EvidentialityProfile) => x.coding == EvidentialCoding.verbalAffix) = true

All Americas languages in our sample use verbal affixes.

Deontic necessity is not universally split into strong and weak

Narrog (2010, 2012; cited in @cite{rubinstein-2014} Table 1) surveys 200 genealogically diverse languages for grammaticalized deontic necessity. The sample reveals that weak deontic necessity is rarer than strong: only 62 of 200 languages (31%) grammaticalize it. See Rubinstein2014.lean for the full typological data and implications for the comparative analysis of weak necessity.

Data imported from Core.Modality.DeonticNecessity.

theorem Phenomena.Modality.Typology.weak_deontic_rarity : Core.Modality.DeonticNecessity.countOf Core.Modality.DeonticNecessity.DeonticNecessityType.weak = 62

Only 62 of 200 languages grammaticalize weak deontic necessity (31%).

theorem Phenomena.Modality.Typology.strong_deontic_count : Core.Modality.DeonticNecessity.countOf Core.Modality.DeonticNecessity.DeonticNecessityType.strong = 60

Strong deontic necessity (60 languages) is slightly less common than weak (62), showing that the strong/weak split itself is not universal.