Modal Semantic Universals

Formalizes the Independence of Force and Flavor (IFF) universal and the Single Axis of Variability (SAV) universal from cross-linguistic modal typology.

Key Definitions

• satisfiesIFF: A modal meaning ⟦m⟧ satisfies IFF iff ⟦m⟧ = fo(m) × fl(m)
• satisfiesSAV: A modal meaning satisfies SAV iff it varies on at most one axis
• iffDegree: Fraction of modals in a language satisfying IFF

Key Theorems

• sav_implies_iff: SAV is strictly stronger than IFF
• cartesianProduct_satisfies_iff: Kratzer's independent parameterization → IFF

Modal Meaning Projections

def Semantics.Modality.Typology.forces (m : List Core.Modality.ForceFlavor) : List Core.Modality.ModalForce

The set of forces expressed by a modal meaning.

Equations

• Semantics.Modality.Typology.forces m = (List.map (fun (x : Core.Modality.ForceFlavor) => x.force) m).eraseDups

def Semantics.Modality.Typology.flavors (m : List Core.Modality.ForceFlavor) : List Core.Modality.ModalFlavor

The set of flavors expressed by a modal meaning.

Equations

• Semantics.Modality.Typology.flavors m = (List.map (fun (x : Core.Modality.ForceFlavor) => x.flavor) m).eraseDups

Semantic Universals

def Semantics.Modality.Typology.satisfiesIFF (m : List Core.Modality.ForceFlavor) : Bool

Independence of Force and Flavor (IFF).

A modal meaning satisfies IFF iff for any two pairs (fo₁, fl₁) and (fo₂, fl₂) in the meaning, the pair (fo₁, fl₂) is also in the meaning. Equivalently: ⟦m⟧ = fo(m) × fl(m) (Cartesian closure).

Alternative formulation: a modal m satisfies IFF just in case ⟦m⟧ = fo(m) × fl(m), where × is the Cartesian product.

@cite{steinert-threlkeld-imel-guo-2023}.

Equations

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

def Semantics.Modality.Typology.satisfiesSAV (m : List Core.Modality.ForceFlavor) : Bool

Single Axis of Variability (SAV).

A modal meaning satisfies SAV iff it exhibits variation along at most one axis of the force-flavor space: either all pairs share the same force, or all pairs share the same flavor.

[Alternative formulation: |fo(m)| = 1 or |fl(m)| = 1.]

@cite{nauze-2008}.

Equations

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

Relationship Between Universals

theorem Semantics.Modality.Typology.sav_implies_iff (m : List Core.Modality.ForceFlavor) (h : satisfiesSAV m = true) : satisfiesIFF m = true

SAV is strictly stronger than IFF: every SAV meaning is IFF.

Proof sketch: If all forces are equal to fo₀ (SAV left disjunct), then for any (fo₁, fl₁) ∈ m and (_, fl₂) ∈ m, fo₁ = fo₀ and the pair (fo₂, fl₂) with flavor fl₂ already has force fo₀ = fo₁, so (fo₁, fl₂) ∈ m. Symmetric for the right disjunct.

theorem Semantics.Modality.Typology.iff_not_implies_sav : ∃ (m : List Core.Modality.ForceFlavor), satisfiesIFF m = true ∧ satisfiesSAV m = false

IFF does NOT imply SAV: a meaning can vary on both axes while satisfying IFF. E.g., {(nec,e),(nec,d),(poss,e),(poss,d)} is IFF but not SAV.

Cartesian Products in the Force-Flavor Space

@[reducible, inline]

abbrev Semantics.Modality.Typology.cartesianProduct (fos : List Core.Modality.ModalForce) (fls : List Core.Modality.ModalFlavor) : List Core.Modality.ForceFlavor

Local abbreviation for the Core infrastructure, for readability.

Equations

• Semantics.Modality.Typology.cartesianProduct = Core.Modality.ForceFlavor.cartesianProduct

theorem Semantics.Modality.Typology.mem_cartesianProduct (ff : Core.Modality.ForceFlavor) (fos : List Core.Modality.ModalForce) (fls : List Core.Modality.ModalFlavor) : ff ∈ cartesianProduct fos fls ↔ ff.force ∈ fos ∧ ff.flavor ∈ fls

Membership in a Cartesian product: ⟨fo, fl⟩ ∈ fos × fls iff fo ∈ fos ∧ fl ∈ fls.

theorem Semantics.Modality.Typology.cartesianProduct_satisfies_iff (fos : List Core.Modality.ModalForce) (fls : List Core.Modality.ModalFlavor) : satisfiesIFF (cartesianProduct fos fls) = true

Any Cartesian product of forces and flavors satisfies IFF.

This is the formal content of @cite{kratzer-1981}'s insight that force (quantificational) and flavor (contextual) are independent parameters in the semantics of modals.

theorem Semantics.Modality.Typology.cartesianProduct_singleton_force_satisfies_sav (fo : Core.Modality.ModalForce) (fls : List Core.Modality.ModalFlavor) : satisfiesSAV (cartesianProduct [fo] fls) = true

A Cartesian product with a singleton force axis satisfies SAV. Covers fixed-force Kratzer modals (e.g., English "must", "can").

theorem Semantics.Modality.Typology.cartesianProduct_singleton_flavor_satisfies_sav (fos : List Core.Modality.ModalForce) (fl : Core.Modality.ModalFlavor) : satisfiesSAV (cartesianProduct fos [fl]) = true

A Cartesian product with a singleton flavor axis satisfies SAV. Covers variable-force Kratzer modals (e.g., Gitksan ima'a).

theorem Semantics.Modality.Typology.singleton_satisfies_iff (ff : Core.Modality.ForceFlavor) : satisfiesIFF [ff] = true

Singleton meanings trivially satisfy IFF.

theorem Semantics.Modality.Typology.empty_satisfies_iff : satisfiesIFF [] = true

Empty meanings trivially satisfy IFF.

Convexity Characterization

IFF is equivalent to convexity in the grid betweenness relation on the force-flavor space (@cite{steinert-threlkeld-imel-guo-2023} §4.2).

Betweenness on a 2D grid: (fo_b, fl_b) lies between (fo_a, fl_a) and (fo_c, fl_c) iff one can reach (fo_b, fl_b) by first changing force, then flavor (or vice versa) on the path from a to c.

Following @cite{chemla-buccola-dautriche-2019}: a set S is convex iff for any a, c ∈ S, every point between a and c is also in S.

def Semantics.Modality.Typology.isBetween (b a c : Core.Modality.ForceFlavor) : Bool

Grid betweenness: b lies between a and c iff each coordinate of b matches one of the corresponding coordinates of a or c.

Equations

• Semantics.Modality.Typology.isBetween b a c = ((b.force == a.force || b.force == c.force) && (b.flavor == a.flavor || b.flavor == c.flavor))

def Semantics.Modality.Typology.isConvex (S : List Core.Modality.ForceFlavor) : Bool

A set of force-flavor pairs is convex iff it is closed under grid betweenness: for any two members, all points between them are members.

Equations

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

theorem Semantics.Modality.Typology.iff_eq_convex (m : List Core.Modality.ForceFlavor) : satisfiesIFF m = isConvex m

def Semantics.Modality.Typology.satisfiesPathConnected (m : List Core.Modality.ForceFlavor) : Bool

Path-connectedness — a weaker alternative to IFF/convexity.

A set S is path-connected iff for any two members, some point between them is also in S. Equivalently: replace the "and" in IFF with "or" — if (fo₁, fl₁) and (fo₂, fl₂) ∈ S, then (fo₁, fl₂) or (fo₂, fl₁) ∈ S.

Strictly weaker than IFF. @cite{steinert-threlkeld-imel-guo-2023} §4.2, footnote 17.

Equations

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

theorem Semantics.Modality.Typology.iff_implies_pathConnected (m : List Core.Modality.ForceFlavor) (h : satisfiesIFF m = true) : satisfiesPathConnected m = true

IFF implies path-connectedness: if all between-points are present, certainly some are.

theorem Semantics.Modality.Typology.pathConnected_not_implies_iff : ∃ (m : List Core.Modality.ForceFlavor), satisfiesPathConnected m = true ∧ satisfiesIFF m = false

Path-connectedness does NOT imply IFF. Table 1(b) in @cite{steinert-threlkeld-imel-guo-2023}: {(◇,e),(◇,d),(◇,c),(□,d),(□,c)} is path-connected but not IFF (missing (□,e)).

Force Pattern (derived from meaning)

ForcePattern captures the observable force structure of a modal meaning: how many distinct forces appear, and whether there is a single flavor. This is derivable from the List ForceFlavor without theoretical stipulation. The per-fragment ForceAnalysis (which distinguishes variableForce from strengthened) adds an explanatory layer on top.

ForceAnalysis.isConsistentWith verifies that the stipulated analysis is compatible with the observed pattern.

inductive Semantics.Modality.Typology.ForcePattern : Type

The observable force structure of a modal meaning.

• empty : ForcePattern

  Meaning is empty.

• singleForce (f : Core.Modality.ModalForce) : ForcePattern

  Single force value (possibly across multiple flavors).

• multiForce : ForcePattern

  Multiple distinct force values.

@[implicit_reducible]

instance Semantics.Modality.Typology.instDecidableEqForcePattern : DecidableEq ForcePattern

Equations

• Semantics.Modality.Typology.instDecidableEqForcePattern = Semantics.Modality.Typology.instDecidableEqForcePattern.decEq

def Semantics.Modality.Typology.instDecidableEqForcePattern.decEq (x✝ x✝¹ : ForcePattern) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq Semantics.Modality.Typology.ForcePattern.empty Semantics.Modality.Typology.ForcePattern.empty = isTrue ⋯
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq Semantics.Modality.Typology.ForcePattern.empty (Semantics.Modality.Typology.ForcePattern.singleForce f) = isFalse ⋯
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq (Semantics.Modality.Typology.ForcePattern.singleForce f) Semantics.Modality.Typology.ForcePattern.empty = isFalse ⋯
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq (Semantics.Modality.Typology.ForcePattern.singleForce f) Semantics.Modality.Typology.ForcePattern.multiForce = isFalse ⋯
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq Semantics.Modality.Typology.ForcePattern.multiForce (Semantics.Modality.Typology.ForcePattern.singleForce f) = isFalse ⋯
• Semantics.Modality.Typology.instDecidableEqForcePattern.decEq Semantics.Modality.Typology.ForcePattern.multiForce Semantics.Modality.Typology.ForcePattern.multiForce = isTrue ⋯

@[implicit_reducible]

instance Semantics.Modality.Typology.instReprForcePattern : Repr ForcePattern

Equations

• Semantics.Modality.Typology.instReprForcePattern = { reprPrec := Semantics.Modality.Typology.instReprForcePattern.repr }

def Semantics.Modality.Typology.instReprForcePattern.repr : ForcePattern → ℕ → Std.Format

Equations

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

def Semantics.Modality.Typology.inferForcePattern (m : List Core.Modality.ForceFlavor) : ForcePattern

Derive the force pattern from a modal meaning.

Equations

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

def Semantics.Modality.Typology.ForceAnalysis.isConsistentWith : Core.Modality.ForceAnalysis → ForcePattern → Bool

A ForceAnalysis is consistent with the observed ForcePattern when:

• fixed fo requires singleForce fo (only one force attested)
• variableForce requires multiForce (both forces attested)
• strengthened fo requires singleForce fo (base semantics has one force; strengthened readings are pragmatic and not encoded in the meaning)

Equations

• Semantics.Modality.Typology.ForceAnalysis.isConsistentWith (Core.Modality.ForceAnalysis.fixed fo) (Semantics.Modality.Typology.ForcePattern.singleForce fo') = (fo == fo')
• Semantics.Modality.Typology.ForceAnalysis.isConsistentWith Core.Modality.ForceAnalysis.variableForce Semantics.Modality.Typology.ForcePattern.multiForce = true
• Semantics.Modality.Typology.ForceAnalysis.isConsistentWith (Core.Modality.ForceAnalysis.strengthened fo) (Semantics.Modality.Typology.ForcePattern.singleForce fo') = (fo == fo')
• Semantics.Modality.Typology.ForceAnalysis.isConsistentWith x✝ Semantics.Modality.Typology.ForcePattern.empty = true
• Semantics.Modality.Typology.ForceAnalysis.isConsistentWith x✝¹ x✝ = false

Language-Level Measures

structure Semantics.Modality.Typology.ModalExpression : Type

A modal expression datum: a form paired with its meaning in the 3×3 space.

• form : String
• meaning : List Core.Modality.ForceFlavor

def Semantics.Modality.Typology.instReprModalExpression.repr : ModalExpression → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Typology.instReprModalExpression : Repr ModalExpression

Equations

• Semantics.Modality.Typology.instReprModalExpression = { reprPrec := Semantics.Modality.Typology.instReprModalExpression.repr }

@[implicit_reducible]

instance Semantics.Modality.Typology.instBEqModalExpression : BEq ModalExpression

Equations

• Semantics.Modality.Typology.instBEqModalExpression = { beq := Semantics.Modality.Typology.instBEqModalExpression.beq }

def Semantics.Modality.Typology.instBEqModalExpression.beq : ModalExpression → ModalExpression → Bool

Equations

• Semantics.Modality.Typology.instBEqModalExpression.beq { form := a, meaning := a_1 } { form := b, meaning := b_1 } = (a == b && a_1 == b_1)
• Semantics.Modality.Typology.instBEqModalExpression.beq x✝¹ x✝ = false

def Semantics.Modality.Typology.ModalExpression.toModalItem (e : ModalExpression) : Core.Modality.ModalItem

Project to the shared modal item core. Register defaults to neutral since typological surveys don't annotate register.

Equations

• e.toModalItem = { form := e.form, meaning := e.meaning }

structure Semantics.Modality.Typology.ModalInventory : Type

A language's modal inventory.

• language : String
• family : String
• source : String
• expressions : List ModalExpression

def Semantics.Modality.Typology.instReprModalInventory.repr : ModalInventory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Typology.instReprModalInventory : Repr ModalInventory

Equations

• Semantics.Modality.Typology.instReprModalInventory = { reprPrec := Semantics.Modality.Typology.instReprModalInventory.repr }

def Semantics.Modality.Typology.ModalInventory.allIFF (inv : ModalInventory) : Bool

Whether all modals in a language satisfy IFF.

Equations

• inv.allIFF = inv.expressions.all fun (e : Semantics.Modality.Typology.ModalExpression) => Semantics.Modality.Typology.satisfiesIFF e.meaning

def Semantics.Modality.Typology.ModalInventory.iffCount (inv : ModalInventory) : ℕ

Number of IFF-satisfying modals in a language.

Equations

• inv.iffCount = (List.filter (fun (e : Semantics.Modality.Typology.ModalExpression) => Semantics.Modality.Typology.satisfiesIFF e.meaning) inv.expressions).length

def Semantics.Modality.Typology.ModalInventory.size (inv : ModalInventory) : ℕ

Total number of modals in a language.

Equations

• inv.size = inv.expressions.length

def Semantics.Modality.Typology.ModalInventory.iffDegreeNum (inv : ModalInventory) : ℕ × ℕ

IFF degree: fraction of modals satisfying IFF (as a rational). This is the paper's "naturalness" measure.

Equations

• inv.iffDegreeNum = (inv.iffCount, inv.size)

def Semantics.Modality.Typology.ModalInventory.hasSynonymy (inv : ModalInventory) : Bool

Whether a language has any synonymous modals (same meaning, different form).

Equations

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

Fragment Integration

def Semantics.Modality.Typology.ModalInventory.fromAuxEntries {α : Type} (language family source : String) (entries : List α) (form : α → String) (meaning : α → List Core.Modality.ForceFlavor) : ModalInventory

Construct a modal inventory from fragment auxiliary entries. Filters to entries with non-empty modal meanings.

Equations

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

Kratzer-Typology Bridge

Connects Kratzer's parameterized modal semantics (conversational backgrounds, ordering sources) to the typological force-flavor space. A Kratzerian modal with fixed force and contextually variable flavors produces a meaning cartesianProduct [force] flavors, which satisfies both IFF and SAV. Variable-force modals (e.g., Gitksan ima'a) produce cartesianProduct forces [flavor], also satisfying both.

structure Semantics.Modality.Typology.FlavorAssignment (W : Type u_2) [DecidableEq W] [Fintype W] : Type u_2

A flavor assignment maps each typological ModalFlavor to a Kratzer parameterization (modal base + ordering source).

• assign : Core.Modality.ModalFlavor → Kratzer.KratzerParams W

def Semantics.Modality.Typology.canonicalAssignment {W : Type u_1} [DecidableEq W] [Fintype W] (epist : Kratzer.EpistemicFlavor W) (deont : Kratzer.DeonticFlavor W) (boul : Kratzer.BouleticFlavor W) (teleo : Kratzer.TeleologicalFlavor W) : FlavorAssignment W

Canonical assignment from the standard Kratzer flavor structures.

Equations

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

Bridge: ModalItem.decomposition ↔ satisfiesIFF

ModalItem.decomposition (Core/ModalLogic.lean) and satisfiesIFF (this file) compute the same property through different algorithms:

• decomposition projects forces/flavors, builds the Cartesian product, checks containment
• satisfiesIFF checks the closure property directly on the meaning list

Both reduce to: ∀ fo ∈ forces(m), ∀ fl ∈ flavors(m), ⟨fo, fl⟩ ∈ m.

theorem Semantics.Modality.Typology.decomposition_eq_satisfiesIFF (m : Core.Modality.ModalItem) : (m.decomposition == Core.Modality.ModalDecomposition.decomposable) = satisfiesIFF m.meaning

ModalItem.decomposition agrees with satisfiesIFF: a modal is decomposable iff its meaning satisfies IFF.

Both sides reduce to checking that m.meaning is closed under force-flavor recombination:

• Forward: if the Cartesian product of projected forces/flavors is contained in m.meaning, then for any two pairs (fo₁, fl₁) and (fo₂, fl₂) in m.meaning, (fo₁, fl₂) is in the product (since fo₁ ∈ forces and fl₂ ∈ flavors), hence in m.meaning.
• Backward: if IFF holds, take any (fo, fl) in the Cartesian product. Then fo ∈ forces means ∃ (fo, fl₁) ∈ m.meaning, and fl ∈ flavors means ∃ (fo₂, fl) ∈ m.meaning. By IFF closure, (fo, fl) ∈ m.meaning.

Corollaries: Decomposability via the Bridge

The equivalence decomposition_eq_satisfiesIFF transfers results freely between the Core structural classifier (ModalItem.decomposition) and the typological universal (satisfiesIFF). The following corollaries make this transfer explicit.

theorem Semantics.Modality.Typology.cartesianProduct_decomposable (form : String) (fos : List Core.Modality.ModalForce) (fls : List Core.Modality.ModalFlavor) : ({ form := form, meaning := cartesianProduct fos fls }.decomposition == Core.Modality.ModalDecomposition.decomposable) = true

Any Kratzer modal — whose meaning is a Cartesian product of forces and flavors — is decomposable. Follows from @cite{kratzer-1981}'s independent parameterization: cartesianProduct_satisfies_iff + bridge.

theorem Semantics.Modality.Typology.sav_implies_decomposable (m : Core.Modality.ModalItem) (h : satisfiesSAV m.meaning = true) : (m.decomposition == Core.Modality.ModalDecomposition.decomposable) = true

SAV modals are decomposable: if a modal varies on at most one axis, it is decomposable. Follows from sav_implies_iff + bridge.

theorem Semantics.Modality.Typology.singleton_decomposable (form : String) (ff : Core.Modality.ForceFlavor) : ({ form := form, meaning := [ff] }.decomposition == Core.Modality.ModalDecomposition.decomposable) = true

Singleton meanings are decomposable, derived from the IFF universal rather than finite case analysis.

theorem Semantics.Modality.Typology.empty_decomposable (form : String) : ({ form := form, meaning := [] }.decomposition == Core.Modality.ModalDecomposition.decomposable) = true

Empty meanings are decomposable.

theorem Semantics.Modality.Typology.unitary_iff_not_iff (m : Core.Modality.ModalItem) : m.isUnitary = !satisfiesIFF m.meaning

A modal is unitary iff its meaning fails IFF. The contrapositive of decomposition_eq_satisfiesIFF.

theorem Semantics.Modality.Typology.allIFF_eq_all_decomposable (inv : ModalInventory) : inv.allIFF = inv.expressions.all fun (e : ModalExpression) => e.toModalItem.decomposition == Core.Modality.ModalDecomposition.decomposable

ModalInventory.allIFF is equivalent to checking that every expression is decomposable. Connects the typological survey predicate to the Kratzer-theoretic structural classifier.