Cross-Linguistic Modal Typology

Empirical modal inventories from 27 languages (17 families) mapped to the 3×3 force-flavor meaning space, following Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}.

Mapping conventions (raw typological data → 3×3 grid)

• Force: weak → .possibility, strong → .necessity, weak necessity → .weakNecessity
• Flavor: epistemic → .epistemic, deontic → .deontic, circumstantial → .circumstantial, teleological → .circumstantial
• Bouletic, reportative, ability, intentional flavors are outside the 2×3 space and are dropped from the mapping.
• Only positive-polarity, can_express = 1 entries are included.

Data source

@cite{steinert-threlkeld-imel-guo-2023}. A database for modal semantic typology. https://clmbr.shane.st/modal-typology/

Abbreviations for the nine meaning points

def Phenomena.Modality.Studies.ImelGuoST2026.tlingit : Semantics.Modality.Typology.ModalInventory

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.tlingit_all_iff : tlingit.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.tlingit_size : tlingit.size = 5

theorem Phenomena.Modality.Studies.ImelGuoST2026.tlingit_has_synonymy : tlingit.hasSynonymy = true

def Phenomena.Modality.Studies.ImelGuoST2026.javanese : Semantics.Modality.Typology.ModalInventory

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.javanese_all_iff : javanese.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.javanese_size : javanese.size = 7

def Phenomena.Modality.Studies.ImelGuoST2026.gitksan : Semantics.Modality.Typology.ModalInventory

Gitksan has variable-force modals: ima('a) and gat express both weak and strong epistemic force. These satisfy SAV (varying on force only, single flavor) and IFF (since {poss, nec} × {epistemic} is a Cartesian product).

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.gitksan = { language := "Gitksan", family := "Tsimshian", source := "Matthewson (2013)", expressions := Fragments.Gitksan.Modals.allExpressions }

theorem Phenomena.Modality.Studies.ImelGuoST2026.gitksan_all_iff : gitksan.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.gitksan_size : gitksan.size = 5

theorem Phenomena.Modality.Studies.ImelGuoST2026.gitksan_ima_sav : Semantics.Modality.Typology.satisfiesSAV [Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.ne✝] = true

Gitksan's variable-force epistemic modals satisfy both SAV and IFF: {poss, nec} × {epistemic} varies on force only (single flavor).

theorem Phenomena.Modality.Studies.ImelGuoST2026.gitksan_ima_is_iff : Semantics.Modality.Typology.satisfiesIFF [Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.ne✝] = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.prepei_not_sav : Semantics.Modality.Typology.satisfiesSAV [Phenomena.Modality.Studies.ImelGuoST2026.ne✝, Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝, Phenomena.Modality.Studies.ImelGuoST2026.nc✝] = false

Greek's Prepei violates SAV: it varies on both force and flavor axes.

def Phenomena.Modality.Studies.ImelGuoST2026.korean : Semantics.Modality.Typology.ModalInventory

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.korean = { language := "Korean", family := "Koreanic", source := "Uegaki et al. (2025)", expressions := Fragments.Korean.Modals.allExpressions }

theorem Phenomena.Modality.Studies.ImelGuoST2026.korean_all_iff : korean.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.korean_size : korean.size = 10

def Phenomena.Modality.Studies.ImelGuoST2026.greek : Semantics.Modality.Typology.ModalInventory

Greek has non-IFF modals: Prepei and Mporei express non-rectangular subsets of the meaning space. Prepei covers {(nec,e),(poss,e),(nec,d),(nec,c)} which is NOT a Cartesian product (missing (poss,d) and (poss,c)).

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.greek_not_all_iff : greek.allIFF = false

theorem Phenomena.Modality.Studies.ImelGuoST2026.greek_size : greek.size = 3

theorem Phenomena.Modality.Studies.ImelGuoST2026.greek_iff_count : greek.iffCount = 1

theorem Phenomena.Modality.Studies.ImelGuoST2026.greek_prepei_not_iff : Semantics.Modality.Typology.satisfiesIFF [Phenomena.Modality.Studies.ImelGuoST2026.ne✝, Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝, Phenomena.Modality.Studies.ImelGuoST2026.nc✝] = false

Prepei is NOT IFF: it expresses both forces and all three flavors, but does not express (possibility, deontic) or (possibility, circumstantial).

def Phenomena.Modality.Studies.ImelGuoST2026.mandarin : Semantics.Modality.Typology.ModalInventory

Mandarin has many modals, extensive synonymy, but all satisfy IFF. The paper notes Mandarin has three modals all encoding strong ∧ epistemic.

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.mandarin_all_iff : mandarin.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.mandarin_size : mandarin.size = 12

theorem Phenomena.Modality.Studies.ImelGuoST2026.mandarin_has_synonymy : mandarin.hasSynonymy = true

def Phenomena.Modality.Studies.ImelGuoST2026.dutch : Semantics.Modality.Typology.ModalInventory

Dutch has one non-IFF modal: zou/zouden...kunnen expresses {(nec,e),(poss,e),(poss,c)} which is not Cartesian-closed (missing (nec,c)).

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.dutch = { language := "Dutch", family := "Indo-European", source := "Uegaki et al. (2025)", expressions := Fragments.Dutch.Modals.allExpressions }

theorem Phenomena.Modality.Studies.ImelGuoST2026.dutch_not_all_iff : dutch.allIFF = false

theorem Phenomena.Modality.Studies.ImelGuoST2026.dutch_size : dutch.size = 10

theorem Phenomena.Modality.Studies.ImelGuoST2026.dutch_iff_count : dutch.iffCount = 9

def Phenomena.Modality.Studies.ImelGuoST2026.hungarian : Semantics.Modality.Typology.ModalInventory

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.hungarian = { language := "Hungarian", family := "Uralic", source := "Uegaki et al. (2025)", expressions := Fragments.Hungarian.Modals.allExpressions }

theorem Phenomena.Modality.Studies.ImelGuoST2026.hungarian_all_iff : hungarian.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.hungarian_size : hungarian.size = 8

def Phenomena.Modality.Studies.ImelGuoST2026.english : Semantics.Modality.Typology.ModalInventory

English modal inventory, derived from the Fragment (single source of truth). Uses ModalInventory.fromAuxEntries to extract modals from AuxEntry data.

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.english_all_iff : english.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.english_size : english.size = 9

def Phenomena.Modality.Studies.ImelGuoST2026.washo : Semantics.Modality.Typology.ModalInventory

Washo is a key counterexample to the SAV universal: -eʔ expresses both possibility and necessity with both epistemic and deontic flavors, varying on both axes simultaneously. Its meaning is the full Cartesian product {□,◇} × {e,d}, so it satisfies IFF. @cite{steinert-threlkeld-imel-guo-2023} §4.1.

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.washo = { language := "Washo", family := "isolate", source := "Bochnak (2015a,b)", expressions := Fragments.Washo.Modals.allExpressions }

theorem Phenomena.Modality.Studies.ImelGuoST2026.washo_all_iff : washo.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.washo_size : washo.size = 1

theorem Phenomena.Modality.Studies.ImelGuoST2026.washo_eq_iff : Semantics.Modality.Typology.satisfiesIFF [Phenomena.Modality.Studies.ImelGuoST2026.ne✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝, Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.pd✝] = true

-eʔ satisfies IFF despite varying on both axes.

theorem Phenomena.Modality.Studies.ImelGuoST2026.washo_eq_not_sav : Semantics.Modality.Typology.satisfiesSAV [Phenomena.Modality.Studies.ImelGuoST2026.ne✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝, Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.pd✝] = false

-eʔ does NOT satisfy SAV: it varies on both force and flavor.

def Phenomena.Modality.Studies.ImelGuoST2026.koryak : Semantics.Modality.Typology.ModalInventory

Koryak ivək is the other SAV counterexample: it expresses both necessity and possibility with doxastic and assertive flavors (both mapped to epistemic in the 3×3 space). @cite{steinert-threlkeld-imel-guo-2023} §3, §4.1.

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.koryak_all_iff : koryak.allIFF = true

theorem Phenomena.Modality.Studies.ImelGuoST2026.koryak_size : koryak.size = 1

theorem Phenomena.Modality.Studies.ImelGuoST2026.mighst_not_iff : Semantics.Modality.Typology.satisfiesIFF [Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝] = false

The hypothetical modal mighst (epistemic possibility + deontic necessity) is ruled out by IFF: its meaning {(◇,e),(□,d)} is not Cartesian-closed (missing (◇,d) and (□,e)). @cite{steinert-threlkeld-imel-guo-2023} §4.1.

theorem Phenomena.Modality.Studies.ImelGuoST2026.mighst_not_sav : Semantics.Modality.Typology.satisfiesSAV [Phenomena.Modality.Studies.ImelGuoST2026.pe✝, Phenomena.Modality.Studies.ImelGuoST2026.nd✝] = false

mighst also fails SAV (as expected, since SAV → IFF).

def Phenomena.Modality.Studies.ImelGuoST2026.allInventories : List Semantics.Modality.Typology.ModalInventory

All twelve inventories.

Equations

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

theorem Phenomena.Modality.Studies.ImelGuoST2026.ten_of_twelve_perfect_iff : (List.filter (fun (x : Semantics.Modality.Typology.ModalInventory) => x.allIFF) allInventories).length = 10

Ten of twelve encoded languages have perfect IFF degree (1.0).

theorem Phenomena.Modality.Studies.ImelGuoST2026.all_have_some_iff : (allInventories.all fun (inv : Semantics.Modality.Typology.ModalInventory) => decide (inv.iffCount > 0)) = true

All twelve languages have IFF degree > 0 (the minimum is Greek at 1/3).

theorem Phenomena.Modality.Studies.ImelGuoST2026.sav_counterexamples_satisfy_iff : washo.allIFF = true ∧ koryak.allIFF = true

The two SAV counterexamples (Washo, Koryak) both satisfy IFF: this is the core empirical claim of @cite{steinert-threlkeld-imel-guo-2023}.

Efficient Communication (Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026})

Key computational results (verified over 32,301 generated + 27 natural languages):

1. Every Pareto-optimal modal system consists only of IFF modals.
2. IFF degree correlates positively with simplicity, informativeness, and Pareto-optimality.
3. Attested modal systems are more Pareto-optimal than the vast majority of hypothetically possible systems (mean optimality: 0.937 vs 0.776).

def Phenomena.Modality.Studies.ImelGuoST2026.naturalMeanOptimality : Float

Mean Pareto-optimality of natural languages (Table 6).

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.naturalMeanOptimality = 0.937

def Phenomena.Modality.Studies.ImelGuoST2026.populationMeanOptimality : Float

Mean Pareto-optimality of the generated population (Table 6).

Equations

• Phenomena.Modality.Studies.ImelGuoST2026.populationMeanOptimality = 0.776

theorem Phenomena.Modality.Studies.ImelGuoST2026.natural_more_optimal : naturalMeanOptimality > populationMeanOptimality