Cross-Linguistic Modal Typology

Empirical modal inventories from 27 languages (17 families) mapped to the 3×3 force-flavor meaning space, following Imel, Guo, & [IGST26].

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

[STIG23]. A database for modal semantic typology. https://clmbr.shane.st/modal-typology/

Abbreviations for the nine meaning points

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

Equations

• ImelGuoST2026.tlingit = { language := "Tlingit", family := "Athabaskan-Eyak-Tlingit", source := "Cable (2017)", expressions := Tlingit.Modals.allExpressions }

theorem ImelGuoST2026.tlingit_all_iff : tlingit.allIFF = true

theorem ImelGuoST2026.tlingit_size : tlingit.size = 5

theorem ImelGuoST2026.tlingit_has_synonymy : tlingit.hasSynonymy = true

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

Equations

• ImelGuoST2026.javanese = { language := "Javanese", family := "Austronesian", source := "Vander Klok (2013a)", expressions := Javanese.Modals.allExpressions }

theorem ImelGuoST2026.javanese_all_iff : javanese.allIFF = true

theorem ImelGuoST2026.javanese_size : javanese.size = 7

def 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

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

theorem ImelGuoST2026.gitksan_all_iff : gitksan.allIFF = true

theorem ImelGuoST2026.gitksan_size : gitksan.size = 5

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

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

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

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

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

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

Equations

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

theorem ImelGuoST2026.korean_all_iff : korean.allIFF = true

theorem ImelGuoST2026.korean_size : korean.size = 10

def 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

• ImelGuoST2026.greek = { language := "Modern Greek", family := "Indo-European", source := "Uegaki et al. (2025)", expressions := Greek.StandardModern.Modals.allExpressions }

theorem ImelGuoST2026.greek_not_all_iff : greek.allIFF = false

theorem ImelGuoST2026.greek_size : greek.size = 3

theorem ImelGuoST2026.greek_iff_count : greek.iffCount = 1

theorem ImelGuoST2026.greek_prepei_not_iff : Semantics.Modality.Typology.satisfiesIFF [ImelGuoST2026.ne✝, ImelGuoST2026.pe✝, ImelGuoST2026.nd✝, 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 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

• ImelGuoST2026.mandarin = { language := "Mandarin", family := "Sino-Tibetan", source := "Uegaki et al. (2025)", expressions := Mandarin.Modals.allExpressions }

theorem ImelGuoST2026.mandarin_all_iff : mandarin.allIFF = true

theorem ImelGuoST2026.mandarin_size : mandarin.size = 12

theorem ImelGuoST2026.mandarin_has_synonymy : mandarin.hasSynonymy = true

def 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

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

theorem ImelGuoST2026.dutch_not_all_iff : dutch.allIFF = false

theorem ImelGuoST2026.dutch_size : dutch.size = 10

theorem ImelGuoST2026.dutch_iff_count : dutch.iffCount = 9

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

Equations

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

theorem ImelGuoST2026.hungarian_all_iff : hungarian.allIFF = true

theorem ImelGuoST2026.hungarian_size : hungarian.size = 8

def 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 ImelGuoST2026.english_all_iff : english.allIFF = true

theorem ImelGuoST2026.english_size : english.size = 9

def ImelGuoST2026.german : Semantics.Modality.Typology.ModalInventory

German modal inventory, derived from the Fragment (single source of truth). Sollte is counted separately from sollen per morphological individuation ([STIG23] §4.3).

Equations

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

theorem ImelGuoST2026.german_all_iff : german.allIFF = true

All seven German modals satisfy IFF (including sollte as distinct from sollen).

def 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. [STIG23] §4.1.

Equations

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

theorem ImelGuoST2026.washo_all_iff : washo.allIFF = true

theorem ImelGuoST2026.washo_size : washo.size = 1

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

-eʔ satisfies IFF despite varying on both axes.

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

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

def 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). [STIG23] §3, §4.1.

Equations

• ImelGuoST2026.koryak = { language := "Koryak", family := "Chukotko-Kamchatkan", source := "Močnik & Abramovitz (2019)", expressions := Koryak.Modals.allExpressions }

theorem ImelGuoST2026.koryak_all_iff : koryak.allIFF = true

theorem ImelGuoST2026.koryak_size : koryak.size = 1

theorem ImelGuoST2026.mighst_not_iff : Semantics.Modality.Typology.satisfiesIFF [ImelGuoST2026.pe✝, 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)). [STIG23] §4.1.

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

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

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

All twelve inventories.

Equations

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

theorem 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 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 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 [STIG23].

Efficient Communication (Imel, Guo, & [IGST26])

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 ImelGuoST2026.naturalMeanOptimality : Float

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

Equations

• ImelGuoST2026.naturalMeanOptimality = 0.937

def ImelGuoST2026.populationMeanOptimality : Float

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

Equations

• ImelGuoST2026.populationMeanOptimality = 0.776

theorem ImelGuoST2026.natural_more_optimal : naturalMeanOptimality > populationMeanOptimality