Imel, Guo and Steinert-Threlkeld (2026): An Efficient Communication Analysis of Modal Typology

This file formalizes the efficient-communication model of [IGST26]. A modal meaning is a subset of the six-point space space, weak and strong force by epistemic, deontic and circumstantial flavor, and a language is a multiset of meanings. The complexity of a meaning, Equation (1), is the least number of atoms of a formula of a Boolean Language of Thought denoting it, computed here from the denotations of formulas with a given number of atoms (Formula.dens, complexity). The informativeness of a language, Equations (2) and (3), is the expected utility of literal communication under a communicative need distribution (a MeasureTheory.Measure on the space): the speaker picks uniformly among the modals expressing the intended point (speak), the listener guesses uniformly among the points of the modal heard (ProbabilityTheory.uniformOn) and earns half credit for each axis guessed right (listen, informativeness). Languages are compared by Pareto dominance on complexity and communicative cost (Dominates), and naturalness is the fraction of a vocabulary satisfying the Independence of Force and Flavor universal of [STIG23], the substrate's Modality.ForceFlavorIndependent.

The paper's three results, that every Pareto-optimal system consists of IFF modals, that naturalness correlates with optimality, and that the attested inventories are more optimal than the sampled ones, are computational and are not formalized. What is proved are the properties of the measures the results rest on. Table 2's complexities are recomputed over the experiment's space, a modal for each point conveys every point exactly (the informativeness is the need of the space) where a single all-purpose modal earns five twelfths of it, a product meaning's listener utility depends only on its two axis sizes, and a language with synonyms is dominated by, and so never Pareto-optimal against, the same language without them.

Implementation notes

• Table 2 illustrates complexity over a four-flavor space with a teleological flavor the library folds into circumstantial. Over the experiment's six-point space may is denoted by w ∧ ¬c and has complexity two, not the table's three, so the table's language has total complexity seven rather than eight.
• may and St'át'imcets k'a are read off the paper's examples (2) and (3), whose rows record a force and a flavor each.
• The paper's two counterexamples to the Single Axis of Variability universal, Washo -eʔ and Koryak ivək, are not in its sample of 27 languages. ivək's doxastic and assertive flavors ([MA19]) lie outside the six-point space.
• The probabilistic layer is measure-theoretic: the need distribution is a measure, the listener is ProbabilityTheory.uniformOn and the speaker a sum of Dirac measures over the multiset of applicable modals, so synonyms keep their multiplicity, and the statements are ℝ≥0∞-valued; cost is a truncated subtraction, zero if a non-probability need drove the informativeness above one.

References

• [IGST26]
• [STIG23]
• [Nau08]
• [RMD08]
• [Boc15b]
• [MA19]

def ImelGuoSteinertThrelkeld2026.forces : Finset Modality.ModalForce

The forces of the experiment's space, weak and strong.

Equations

• ImelGuoSteinertThrelkeld2026.forces = {Modality.ModalForce.possibility, Modality.ModalForce.necessity}

def ImelGuoSteinertThrelkeld2026.flavors : Finset Modality.ModalFlavor

The flavors of the experiment's space.

Equations

• ImelGuoSteinertThrelkeld2026.flavors = {Modality.ModalFlavor.epistemic, Modality.ModalFlavor.deontic, Modality.ModalFlavor.circumstantial}

def ImelGuoSteinertThrelkeld2026.space : Finset Modality.ForceFlavor

The meaning space P, six force-flavor pairs.

Equations

• ImelGuoSteinertThrelkeld2026.space = ImelGuoSteinertThrelkeld2026.forces ×ˢ ImelGuoSteinertThrelkeld2026.flavors

@[reducible, inline]

abbrev ImelGuoSteinertThrelkeld2026.Meaning : Type

A modal meaning, the force-flavor pairs a modal can express.

Equations

• ImelGuoSteinertThrelkeld2026.Meaning = Finset Modality.ForceFlavor

The paper's examples

def ImelGuoSteinertThrelkeld2026.Examples.forceFlavor (e : Datum) : Option Modality.ForceFlavor

The force-flavor pair a row's annotation records.

Equations

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

def ImelGuoSteinertThrelkeld2026.may : Meaning

English may, the pairs of examples (2a) and (2b).

Equations

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

def ImelGuoSteinertThrelkeld2026.ka : Meaning

St'át'imcets k'a, the pairs of examples (3a) and (3b), after [RMD08].

Equations

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

theorem ImelGuoSteinertThrelkeld2026.may_eq : may = {(Modality.ModalForce.possibility, Modality.ModalFlavor.epistemic), (Modality.ModalForce.possibility, Modality.ModalFlavor.deontic)}

theorem ImelGuoSteinertThrelkeld2026.ka_eq : ka = {(Modality.ModalForce.necessity, Modality.ModalFlavor.epistemic), (Modality.ModalForce.possibility, Modality.ModalFlavor.epistemic)}

theorem ImelGuoSteinertThrelkeld2026.singleAxis_may_ka : Modality.SingleAxis may ∧ Modality.SingleAxis ka

Table 1: may varies in flavor and k'a in force, each on a single axis.

The Language of Thought and complexity

inductive ImelGuoSteinertThrelkeld2026.Atom : Type

The atoms of the Language of Thought, one per force and one per flavor of the space.

• weak : Atom
• strong : Atom
• epistemic : Atom
• deontic : Atom
• circumstantial : Atom

@[instance_reducible]

instance ImelGuoSteinertThrelkeld2026.instDecidableEqAtom : DecidableEq Atom

Equations

• ImelGuoSteinertThrelkeld2026.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ImelGuoSteinertThrelkeld2026.instFintypeAtom : Fintype Atom

Equations

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

def ImelGuoSteinertThrelkeld2026.Atom.den : Atom → Meaning

The points at which an atom holds, a row or a column of the space.

Equations

• ImelGuoSteinertThrelkeld2026.Atom.weak.den = {Modality.ModalForce.possibility} ×ˢ ImelGuoSteinertThrelkeld2026.flavors
• ImelGuoSteinertThrelkeld2026.Atom.strong.den = {Modality.ModalForce.necessity} ×ˢ ImelGuoSteinertThrelkeld2026.flavors
• ImelGuoSteinertThrelkeld2026.Atom.epistemic.den = ImelGuoSteinertThrelkeld2026.forces ×ˢ {Modality.ModalFlavor.epistemic}
• ImelGuoSteinertThrelkeld2026.Atom.deontic.den = ImelGuoSteinertThrelkeld2026.forces ×ˢ {Modality.ModalFlavor.deontic}
• ImelGuoSteinertThrelkeld2026.Atom.circumstantial.den = ImelGuoSteinertThrelkeld2026.forces ×ˢ {Modality.ModalFlavor.circumstantial}

def ImelGuoSteinertThrelkeld2026.Atom.ofForce : Modality.ModalForce → Atom

The atom for a force of the space.

Equations

• ImelGuoSteinertThrelkeld2026.Atom.ofForce Modality.ModalForce.possibility = ImelGuoSteinertThrelkeld2026.Atom.weak
• ImelGuoSteinertThrelkeld2026.Atom.ofForce x✝ = ImelGuoSteinertThrelkeld2026.Atom.strong

def ImelGuoSteinertThrelkeld2026.Atom.ofFlavor : Modality.ModalFlavor → Atom

The atom for a flavor of the space.

Equations

• ImelGuoSteinertThrelkeld2026.Atom.ofFlavor Modality.ModalFlavor.epistemic = ImelGuoSteinertThrelkeld2026.Atom.epistemic
• ImelGuoSteinertThrelkeld2026.Atom.ofFlavor Modality.ModalFlavor.deontic = ImelGuoSteinertThrelkeld2026.Atom.deontic
• ImelGuoSteinertThrelkeld2026.Atom.ofFlavor x✝ = ImelGuoSteinertThrelkeld2026.Atom.circumstantial

inductive ImelGuoSteinertThrelkeld2026.Formula : Type

Formulas of the Boolean Language of Thought.

• atom (a : Atom) : Formula
• not (φ : Formula) : Formula
• and (φ ψ : Formula) : Formula
• or (φ ψ : Formula) : Formula

def ImelGuoSteinertThrelkeld2026.Formula.atoms : Formula → ℕ

The number of atom occurrences, the length in literals of the complexity measure.

Equations

• (ImelGuoSteinertThrelkeld2026.Formula.atom a).atoms = 1
• φ.not.atoms = φ.atoms
• (φ.and ψ).atoms = φ.atoms + ψ.atoms
• (φ.or ψ).atoms = φ.atoms + ψ.atoms

def ImelGuoSteinertThrelkeld2026.Formula.den : Formula → Meaning

The points of the space at which a formula holds.

Equations

• (ImelGuoSteinertThrelkeld2026.Formula.atom a).den = a.den
• φ.not.den = ImelGuoSteinertThrelkeld2026.space \ φ.den
• (φ.and ψ).den = φ.den ∩ ψ.den
• (φ.or ψ).den = φ.den ∪ ψ.den

theorem ImelGuoSteinertThrelkeld2026.Formula.one_le_atoms (φ : Formula) : 1 ≤ φ.atoms

theorem ImelGuoSteinertThrelkeld2026.Formula.den_subset (φ : Formula) : φ.den ⊆ space

def ImelGuoSteinertThrelkeld2026.Formula.point (p : Modality.ForceFlavor) : Formula

The conjunction of a force atom and a flavor atom denoting one point of the space.

Equations

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

theorem ImelGuoSteinertThrelkeld2026.Formula.den_point {p : Modality.ForceFlavor} (hp : p ∈ space) : (point p).den = {p}

theorem ImelGuoSteinertThrelkeld2026.Formula.exists_den (m : Meaning) (hm : m ⊆ space) : ∃ (φ : Formula), φ.den = m

Every meaning within the space is denoted, by the disjunction of its points.

Denotations by number of atoms

dens n is the set of denotations of formulas with exactly n atoms: the literals for one atom, and for more the meets and joins of denotations of formulas whose atoms add up to n. The recursion is fuelled so that it computes.

def ImelGuoSteinertThrelkeld2026.Formula.literals : Finset Meaning

The denotations of literals, an atom's points or their complement in the space.

Equations

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

def ImelGuoSteinertThrelkeld2026.Formula.combine (A B : Finset Meaning) : Finset Meaning

The meets and joins of a member of each set.

Equations

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

theorem ImelGuoSteinertThrelkeld2026.Formula.inter_mem_combine {A B : Finset Meaning} {a b : Meaning} (ha : a ∈ A) (hb : b ∈ B) : a ∩ b ∈ combine A B

theorem ImelGuoSteinertThrelkeld2026.Formula.union_mem_combine {A B : Finset Meaning} {a b : Meaning} (ha : a ∈ A) (hb : b ∈ B) : a ∪ b ∈ combine A B

theorem ImelGuoSteinertThrelkeld2026.Formula.mem_combine {A B : Finset Meaning} {m : Meaning} : m ∈ combine A B ↔ ∃ a ∈ A, ∃ b ∈ B, m = a ∩ b ∨ m = a ∪ b

def ImelGuoSteinertThrelkeld2026.Formula.densAux : ℕ → ℕ → Finset Meaning

densAux fuel n is dens n once n ≤ fuel.

Equations

• One or more equations did not get rendered due to their size.
• ImelGuoSteinertThrelkeld2026.Formula.densAux 0 x✝ = ∅

def ImelGuoSteinertThrelkeld2026.Formula.dens (n : ℕ) : Finset Meaning

The denotations of formulas with exactly n atoms.

Equations

• ImelGuoSteinertThrelkeld2026.Formula.dens n = ImelGuoSteinertThrelkeld2026.Formula.densAux n n

theorem ImelGuoSteinertThrelkeld2026.Formula.densAux_succ (f n : ℕ) : densAux (f + 1) n = if n = 1 then literals else (Finset.range (n - 1)).biUnion fun (i : ℕ) => combine (densAux f (i + 1)) (densAux f (n - 1 - i))

theorem ImelGuoSteinertThrelkeld2026.Formula.densAux_eq {n f g : ℕ} : n ≤ f → n ≤ g → densAux f n = densAux g n

theorem ImelGuoSteinertThrelkeld2026.Formula.dens_one : dens 1 = literals

theorem ImelGuoSteinertThrelkeld2026.Formula.dens_eq_biUnion {n : ℕ} (hn : 2 ≤ n) : dens n = (Finset.range (n - 1)).biUnion fun (i : ℕ) => combine (dens (i + 1)) (dens (n - 1 - i))

theorem ImelGuoSteinertThrelkeld2026.Formula.combine_dens_subset {a b : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) : combine (dens a) (dens b) ⊆ dens (a + b)

theorem ImelGuoSteinertThrelkeld2026.Formula.den_mem_dens (φ : Formula) : φ.den ∈ dens φ.atoms ∧ space \ φ.den ∈ dens φ.atoms

A formula's denotation, and its complement in the space, lie in the denotations of its number of atoms.

theorem ImelGuoSteinertThrelkeld2026.Formula.exists_den_of_mem_dens {n : ℕ} {m : Meaning} : m ∈ dens n → ∃ (φ : Formula), φ.atoms = n ∧ φ.den = m

Every denotation with n atoms is the denotation of a formula with n atoms.

theorem ImelGuoSteinertThrelkeld2026.Formula.exists_mem_dens {m : Meaning} (hm : m ⊆ space) : ∃ (n : ℕ), m ∈ dens n

def ImelGuoSteinertThrelkeld2026.complexity (m : Meaning) : ℕ

Equation (1) for one modal, the least number of atoms of a formula denoting it.

Equations

• ImelGuoSteinertThrelkeld2026.complexity m = if h : m ⊆ ImelGuoSteinertThrelkeld2026.space then Nat.find ⋯ else 0

theorem ImelGuoSteinertThrelkeld2026.complexity_eq_iff {m : Meaning} (hm : m ⊆ space) {n : ℕ} : complexity m = n ↔ m ∈ Formula.dens n ∧ ∀ k < n, m ∉ Formula.dens k

theorem ImelGuoSteinertThrelkeld2026.le_complexity_iff {m : Meaning} (hm : m ⊆ space) {n : ℕ} : n ≤ complexity m ↔ ∀ k < n, m ∉ Formula.dens k

theorem ImelGuoSteinertThrelkeld2026.complexity_le {m : Meaning} (φ : Formula) (h : φ.den = m) : complexity m ≤ φ.atoms

theorem ImelGuoSteinertThrelkeld2026.exists_den_atoms {m : Meaning} (hm : m ⊆ space) : ∃ (φ : Formula), φ.atoms = complexity m ∧ φ.den = m

theorem ImelGuoSteinertThrelkeld2026.one_le_complexity {m : Meaning} (hm : m ⊆ space) : 1 ≤ complexity m

def ImelGuoSteinertThrelkeld2026.mought : Meaning

The hypothetical mought of Table 2, weak epistemic or strong deontic.

Equations

• ImelGuoSteinertThrelkeld2026.mought = {(Modality.ModalForce.possibility, Modality.ModalFlavor.epistemic), (Modality.ModalForce.necessity, Modality.ModalFlavor.deontic)}

def ImelGuoSteinertThrelkeld2026.notcirc : Meaning

The hypothetical notcirc of Table 2, everything but circumstantial.

Equations

• ImelGuoSteinertThrelkeld2026.notcirc = ImelGuoSteinertThrelkeld2026.forces ×ˢ {Modality.ModalFlavor.epistemic, Modality.ModalFlavor.deontic}

theorem ImelGuoSteinertThrelkeld2026.complexity_may : complexity may = 2

Over the six-point space may is w ∧ ¬c, two atoms, where Table 2's four-flavor space needs three.

theorem ImelGuoSteinertThrelkeld2026.complexity_mought : complexity mought = 4

mought needs four atoms, (w ∧ e) ∨ (s ∧ d).

theorem ImelGuoSteinertThrelkeld2026.complexity_notcirc : complexity notcirc = 1

notcirc is the single literal ¬c.

def ImelGuoSteinertThrelkeld2026.totalComplexity (L : Multiset Meaning) : ℕ

Complexity of a language, the sum over its modals, Equation (1).

Equations

• ImelGuoSteinertThrelkeld2026.totalComplexity L = (Multiset.map ImelGuoSteinertThrelkeld2026.complexity L).sum

theorem ImelGuoSteinertThrelkeld2026.totalComplexity_table2 : totalComplexity {may, mought, notcirc} = 7

Table 2's language costs seven atoms over the experiment's space, one fewer than the paper's eight over its illustration space.

theorem ImelGuoSteinertThrelkeld2026.totalComplexity_replicate (k : ℕ) (m : Meaning) : totalComplexity (Multiset.replicate k m) = k * complexity m

Informativeness

@[instance_reducible]

instance ImelGuoSteinertThrelkeld2026.instMeasurableSpaceModalForce_studies : MeasurableSpace Modality.ModalForce

Equations

• ImelGuoSteinertThrelkeld2026.instMeasurableSpaceModalForce_studies = ⊤

instance ImelGuoSteinertThrelkeld2026.instMeasurableSingletonClassModalForce_studies : MeasurableSingletonClass Modality.ModalForce

@[instance_reducible]

instance ImelGuoSteinertThrelkeld2026.instMeasurableSpaceModalFlavor_studies : MeasurableSpace Modality.ModalFlavor

Equations

• ImelGuoSteinertThrelkeld2026.instMeasurableSpaceModalFlavor_studies = ⊤

instance ImelGuoSteinertThrelkeld2026.instMeasurableSingletonClassModalFlavor_studies : MeasurableSingletonClass Modality.ModalFlavor

@[instance_reducible]

instance ImelGuoSteinertThrelkeld2026.instMeasurableSpaceMeaning : MeasurableSpace Meaning

Equations

• ImelGuoSteinertThrelkeld2026.instMeasurableSpaceMeaning = ⊤

instance ImelGuoSteinertThrelkeld2026.instMeasurableSingletonClassMeaning : MeasurableSingletonClass Meaning

noncomputable def ImelGuoSteinertThrelkeld2026.utility (p q : Modality.ForceFlavor) : ENNReal

Equation (3), half credit for each axis of the intended point guessed right.

Equations

• ImelGuoSteinertThrelkeld2026.utility p q = (if p.force = q.force then 1 / 2 else 0) + if p.flavor = q.flavor then 1 / 2 else 0

noncomputable def ImelGuoSteinertThrelkeld2026.listen (m : Meaning) (p : Modality.ForceFlavor) : ENNReal

The expected utility when the speaker intends p and a literal listener guesses uniformly among the points a modal expresses.

Equations

• ImelGuoSteinertThrelkeld2026.listen m p = ∫⁻ (q : Modality.ForceFlavor), ImelGuoSteinertThrelkeld2026.utility p q ∂ProbabilityTheory.uniformOn ↑m

theorem ImelGuoSteinertThrelkeld2026.listen_eq_measure (m : Meaning) (p : Modality.ForceFlavor) : listen m p = ((ProbabilityTheory.uniformOn ↑m) {q : Modality.ForceFlavor | p.force = q.force} + (ProbabilityTheory.uniformOn ↑m) {q : Modality.ForceFlavor | p.flavor = q.flavor}) / 2

The expected utility is the mean of the probabilities that the listener's guess matches each axis of the intended point.

theorem ImelGuoSteinertThrelkeld2026.listen_eq (m : Meaning) (p : Modality.ForceFlavor) : listen m p = (↑{q ∈ m | p.force = q.force}.card / ↑(Finset.card m) + ↑{q ∈ m | p.flavor = q.flavor}.card / ↑(Finset.card m)) / 2

The axis-match probabilities counted on the modal's finset.

theorem ImelGuoSteinertThrelkeld2026.listen_singleton (p : Modality.ForceFlavor) : listen {p} p = 1

theorem ImelGuoSteinertThrelkeld2026.listen_product {F : Finset Modality.ModalForce} {Φ : Finset Modality.ModalFlavor} {p : Modality.ForceFlavor} (hF : p.force ∈ F) (hΦ : p.flavor ∈ Φ) : listen (F ×ˢ Φ) p = (1 / ↑F.card + 1 / ↑Φ.card) / 2

A listener hearing a product modal earns half the reciprocal of each axis size, so the utility of an IFF modal depends only on how many forces and how many flavors it leaves open.

theorem ImelGuoSteinertThrelkeld2026.listen_may_mought : listen may (Modality.ModalForce.possibility, Modality.ModalFlavor.epistemic) = 3 / 4 ∧ listen mought (Modality.ModalForce.possibility, Modality.ModalFlavor.epistemic) = 1 / 2

Table 2's may and mought have two points each; the IFF one is the more informative, sharing an axis with any guess.

def ImelGuoSteinertThrelkeld2026.speakers (L : Multiset Meaning) (p : Modality.ForceFlavor) : Multiset Meaning

The modals of a language a literal speaker chooses among to express p.

Equations

• ImelGuoSteinertThrelkeld2026.speakers L p = Multiset.filter (fun (x : ImelGuoSteinertThrelkeld2026.Meaning) => p ∈ x) L

noncomputable def ImelGuoSteinertThrelkeld2026.speak (L : Multiset Meaning) (p : Modality.ForceFlavor) : MeasureTheory.Measure Meaning

The literal speaker's choice among the modals of L expressing p, uniform over the multiset so that synonyms keep their multiplicity.

Equations

• ImelGuoSteinertThrelkeld2026.speak L p = (↑(ImelGuoSteinertThrelkeld2026.speakers L p).card)⁻¹ • (Multiset.map MeasureTheory.Measure.dirac (ImelGuoSteinertThrelkeld2026.speakers L p)).sum

noncomputable def ImelGuoSteinertThrelkeld2026.informativeness (need : MeasureTheory.Measure Modality.ForceFlavor) (L : Multiset Meaning) : ENNReal

Equation (2), the expected utility of literal communication under a communicative need distribution.

Equations

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

noncomputable def ImelGuoSteinertThrelkeld2026.cost (need : MeasureTheory.Measure Modality.ForceFlavor) (L : Multiset Meaning) : ENNReal

Communicative cost, the inverse of informativeness.

Equations

• ImelGuoSteinertThrelkeld2026.cost need L = 1 - ImelGuoSteinertThrelkeld2026.informativeness need L

noncomputable def ImelGuoSteinertThrelkeld2026.needTable5 : MeasureTheory.Measure Modality.ForceFlavor

Table 5, the communicative need distribution estimated from the corpus.

Equations

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

instance ImelGuoSteinertThrelkeld2026.instIsProbabilityMeasureForceFlavorNeedTable5 : MeasureTheory.IsProbabilityMeasure needTable5

The corpus need distribution sums to one.

theorem ImelGuoSteinertThrelkeld2026.speak_of_speakers_eq_zero {L : Multiset Meaning} {p : Modality.ForceFlavor} (h : speakers L p = 0) : speak L p = 0

def ImelGuoSteinertThrelkeld2026.singletons : Multiset Meaning

A language with a modal for each point of the space.

Equations

• ImelGuoSteinertThrelkeld2026.singletons = Multiset.map (fun (x : Modality.ForceFlavor) => {x}) ImelGuoSteinertThrelkeld2026.space.val

def ImelGuoSteinertThrelkeld2026.whole : Multiset Meaning

The language of one modal expressing every point.

Equations

• ImelGuoSteinertThrelkeld2026.whole = {ImelGuoSteinertThrelkeld2026.space}

theorem ImelGuoSteinertThrelkeld2026.speakers_singletons {p : Modality.ForceFlavor} (hp : p ∈ space) : speakers singletons p = {{p}}

theorem ImelGuoSteinertThrelkeld2026.speakers_singletons_of_notMem {p : Modality.ForceFlavor} (hp : p ∉ space) : speakers singletons p = 0

theorem ImelGuoSteinertThrelkeld2026.speak_singletons {p : Modality.ForceFlavor} (hp : p ∈ space) : speak singletons p = MeasureTheory.Measure.dirac {p}

theorem ImelGuoSteinertThrelkeld2026.informativeness_singletons (need : MeasureTheory.Measure Modality.ForceFlavor) : informativeness need singletons = need ↑space

A modal for each point is maximally informative: every point of the space is conveyed exactly, so the informativeness is the need of the space, whatever the need.

theorem ImelGuoSteinertThrelkeld2026.speakers_whole {p : Modality.ForceFlavor} (hp : p ∈ space) : speakers whole p = {space}

theorem ImelGuoSteinertThrelkeld2026.speakers_whole_of_notMem {p : Modality.ForceFlavor} (hp : p ∉ space) : speakers whole p = 0

theorem ImelGuoSteinertThrelkeld2026.informativeness_whole (need : MeasureTheory.Measure Modality.ForceFlavor) : informativeness need whole = 5 / 12 * need ↑space

One all-purpose modal conveys five twelfths of a point on average, half of a half plus a third, whatever the need.

Synonymy and dominance

def ImelGuoSteinertThrelkeld2026.Dominates (need : MeasureTheory.Measure Modality.ForceFlavor) (L L' : Multiset Meaning) : Prop

L dominates L' on the trade-off: no worse on either measure, better on one.

Equations

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

def ImelGuoSteinertThrelkeld2026.ParetoOptimal (need : MeasureTheory.Measure Modality.ForceFlavor) (pool : Set (Multiset Meaning)) (L : Multiset Meaning) : Prop

Pareto optimality within a pool of languages.

Equations

• ImelGuoSteinertThrelkeld2026.ParetoOptimal need pool L = (L ∈ pool ∧ ∀ L' ∈ pool, ¬ImelGuoSteinertThrelkeld2026.Dominates need L' L)

theorem ImelGuoSteinertThrelkeld2026.speakers_replicate (k : ℕ) (m : Meaning) (p : Modality.ForceFlavor) : speakers (Multiset.replicate k m) p = if p ∈ m then Multiset.replicate k m else 0

theorem ImelGuoSteinertThrelkeld2026.speak_replicate {k : ℕ} (hk : k ≠ 0) (m : Meaning) (p : Modality.ForceFlavor) : speak (Multiset.replicate k m) p = speak {m} p

The speaker of a language of copies of one modal is the speaker of the modal alone.

theorem ImelGuoSteinertThrelkeld2026.informativeness_replicate (need : MeasureTheory.Measure Modality.ForceFlavor) {k : ℕ} (hk : k ≠ 0) (m : Meaning) : informativeness need (Multiset.replicate k m) = informativeness need {m}

Copies of one modal are as informative as the modal alone.

theorem ImelGuoSteinertThrelkeld2026.dominates_replicate (need : MeasureTheory.Measure Modality.ForceFlavor) {m : Meaning} (hm : m ⊆ space) {k : ℕ} (hk : 2 ≤ k) : Dominates need {m} (Multiset.replicate k m)

Synonymy hurts the trade-off: copies of a modal cost the same and add complexity.

theorem ImelGuoSteinertThrelkeld2026.not_paretoOptimal_replicate (need : MeasureTheory.Measure Modality.ForceFlavor) {pool : Set (Multiset Meaning)} {m : Meaning} (hm : m ⊆ space) (hpool : {m} ∈ pool) {k : ℕ} (hk : 2 ≤ k) : ¬ParetoOptimal need pool (Multiset.replicate k m)

A language of copies of one modal is not Pareto-optimal in any pool containing the modal alone.

The universals and naturalness

noncomputable def ImelGuoSteinertThrelkeld2026.naturalness (L : List Modality.ModalItem) : ENNReal

Naturalness, the fraction of an inventory satisfying the IFF universal.

Equations

• ImelGuoSteinertThrelkeld2026.naturalness L = ↑(List.countP (fun (x : Modality.ModalItem) => decide (Modality.ForceFlavorIndependent x.meaning)) L) / ↑L.length

theorem ImelGuoSteinertThrelkeld2026.washo_not_singleAxis_forceFlavorIndependent : ¬Modality.SingleAxis Washo.modalEq.meaning ∧ Modality.ForceFlavorIndependent Washo.modalEq.meaning

Washo -eʔ varies on both axes, against the Single Axis of Variability universal of [Nau08], and satisfies IFF, its meaning being every force-flavor pair.

theorem ImelGuoSteinertThrelkeld2026.ivek_not_singleAxis : ¬Modality.SingleAxis MocnikAbramovitz2019.attested

Koryak ivək varies on both axes too, in force and between the doxastic and assertive flavors of [MA19], even without the existential 'say' they could not confirm.

theorem ImelGuoSteinertThrelkeld2026.not_forceFlavorIndependent_diagonal : ¬Modality.ForceFlavorIndependent {(Modality.ModalForce.necessity, Modality.ModalFlavor.epistemic), (Modality.ModalForce.possibility, Modality.ModalFlavor.circumstantial)}

The meaning the universal rules out, epistemic necessity with circumstantial possibility.

theorem ImelGuoSteinertThrelkeld2026.naturalness_greek : naturalness Greek.StandardModern.modals = 1 / 3

Naturalness is graded: Modern Greek, one of the sampled languages, has one IFF modal in three.