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 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.

Steinert-Threlkeld, Imel, & @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 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 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 : 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 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.

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

instance Semantics.Modality.Typology.instReprModalExpression : Repr ModalExpression

Equations

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

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

Equations

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

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.

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 : Type

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

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

def Semantics.Modality.Typology.canonicalAssignment (epist : Kratzer.EpistemicFlavor) (deont : Kratzer.DeonticFlavor) (teleo : Kratzer.TeleologicalFlavor) : FlavorAssignment

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 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.