Semantic universals for modal meanings

This file defines the two proposed universals on modal meanings, sets of force-flavor pairs, as predicates on a finite set of pairs, and the weaker property proposed as a fallback. A meaning has independent force and flavor when it is the product of its forces and its flavors ([STIG23]), it varies on a single axis when its pairs all share a force or all share a flavor ([Nau08]), and it is path-connected when any two of its pairs recombine in at least one order. A single-axis meaning is a product, and a product is path-connected.

On a Kratzer semantics ([Kra81b]) a modal's force and its flavor are set by separate parameters, so its meaning is a product and satisfies the universal; a fixed-force modal ranging over flavors, or a variable-force modal of one flavor, varies on a single axis besides.

The forces and flavors are any two types, since [STIG23] leave open what the axes are: a modal's meaning is a Finset ForceFlavor, and an attitude verb's pairs its force with a flavor of its own, doxastic or assertive for Koryak ivək ([MA19]).

Main definitions

• Modality.ForceFlavorIndependent: the meaning is the product of its projections.
• Modality.SingleAxis: at most one force or at most one flavor.
• Modality.PathConnected: closure under recombining two pairs in at least one order.

Main results

• Modality.forceFlavorIndependent_iff: the universal as stated, closure under recombining the force of one pair with the flavor of another.
• Modality.forceFlavorIndependent_iff_pair_product_subset: independence is convexity for the grid betweenness of [CBD19].
• Modality.SingleAxis.forceFlavorIndependent, Modality.ForceFlavorIndependent.pathConnected: the three properties in order of strength.
• Modality.forceFlavorIndependent_product: a product meaning satisfies the universal.
• Modality.ModalItem.singleAxis_meaning_iff: an item varies on a single axis when it does not vary in both force and flavor.

References

• [STIG23]
• [Nau08]
• [Kra81b]
• [CBD19]
• [MA19]

def Modality.ForceFlavorIndependent {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Finset (α × β)) : Prop

A meaning has independent force and flavor when it is the product of its forces and its flavors, so that with (fo₁, fl₁) and (fo₂, fl₂) it expresses (fo₁, fl₂).

Equations

• Modality.ForceFlavorIndependent m = (m = Finset.image Prod.fst m ×ˢ Finset.image Prod.snd m)

def Modality.SingleAxis {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Finset (α × β)) : Prop

A meaning varies on a single axis when its pairs all share a force or all share a flavor.

Equations

• Modality.SingleAxis m = ((Finset.image Prod.fst m).card ≤ 1 ∨ (Finset.image Prod.snd m).card ≤ 1)

def Modality.PathConnected {α : Type u_1} {β : Type u_2} (m : Finset (α × β)) : Prop

A meaning is path-connected when with (fo₁, fl₁) and (fo₂, fl₂) it expresses (fo₁, fl₂) or (fo₂, fl₁), the Ferrers property of a relation.

Equations

• Modality.PathConnected m = ∀ x ∈ m, ∀ y ∈ m, (x.1, y.2) ∈ m ∨ (y.1, x.2) ∈ m

@[instance_reducible]

instance Modality.instDecidableForceFlavorIndependent {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Finset (α × β)) : Decidable (ForceFlavorIndependent m)

Equations

• Modality.instDecidableForceFlavorIndependent m = { decide := decide (m.val = (Finset.image Prod.fst m ×ˢ Finset.image Prod.snd m).val), reflects_decide := ⋯ }

@[instance_reducible]

instance Modality.instDecidableSingleAxis {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Finset (α × β)) : Decidable (SingleAxis m)

Equations

• Modality.instDecidableSingleAxis m = { decide := decide ((Finset.image Prod.fst m).card ≤ 1) || decide ((Finset.image Prod.snd m).card ≤ 1), reflects_decide := ⋯ }

@[instance_reducible]

instance Modality.instDecidablePathConnected {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (m : Finset (α × β)) : Decidable (PathConnected m)

Equations

• Modality.instDecidablePathConnected m = { decide := decide (∀ a ∈ m.val.attach, (fun (x : α × β) (a : x ∈ m) => ∀ y ∈ m, (x.1, y.2) ∈ m ∨ (y.1, x.2) ∈ m) ↑a ⋯), reflects_decide := ⋯ }

theorem Modality.forceFlavorIndependent_iff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} : ForceFlavorIndependent m ↔ ∀ x ∈ m, ∀ y ∈ m, (x.1, y.2) ∈ m

The universal as the paper states it, closure under recombining two pairs into a third.

theorem Modality.ForceFlavorIndependent.of_mk_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} : (∀ x ∈ m, ∀ y ∈ m, (x.1, y.2) ∈ m) → ForceFlavorIndependent m

Alias of the reverse direction of Modality.forceFlavorIndependent_iff.

---

The universal as the paper states it, closure under recombining two pairs into a third.

theorem Modality.ForceFlavorIndependent.mk_mem {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} : ForceFlavorIndependent m → ∀ x ∈ m, ∀ y ∈ m, (x.1, y.2) ∈ m

Alias of the forward direction of Modality.forceFlavorIndependent_iff.

---

The universal as the paper states it, closure under recombining two pairs into a third.

theorem Modality.forceFlavorIndependent_iff_pair_product_subset {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} : ForceFlavorIndependent m ↔ ∀ x ∈ m, ∀ y ∈ m, {x.1, y.1} ×ˢ {x.2, y.2} ⊆ m

A meaning is independent exactly when it contains the rectangle spanned by any two of its pairs, the pairs between them for the grid betweenness on the force-flavor space, so independence is convexity in that sense.

theorem Modality.SingleAxis.forceFlavorIndependent {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} (h : SingleAxis m) : ForceFlavorIndependent m

theorem Modality.ForceFlavorIndependent.pathConnected {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {m : Finset (α × β)} (h : ForceFlavorIndependent m) : PathConnected m

theorem Modality.ForceFlavorIndependent.singleton {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (x : α × β) : ForceFlavorIndependent {x}

theorem Modality.ModalItem.singleAxis_meaning_iff {i : ModalItem} : SingleAxis i.meaning ↔ ¬(i.VariesForce ∧ i.VariesFlavor)

A modal item varies on a single axis exactly when it does not vary in both force and flavor.

Kratzer modals

A modal whose force and flavor are set by separate parameters expresses a product.

theorem Modality.forceFlavorIndependent_product {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (F : Finset α) (Φ : Finset β) : ForceFlavorIndependent (F ×ˢ Φ)

theorem Modality.singleAxis_singleton_product {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (Φ : Finset β) (fo : α) : SingleAxis ({fo} ×ˢ Φ)

A fixed-force modal ranging over flavors varies on a single axis.

theorem Modality.singleAxis_product_singleton {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (F : Finset α) (fl : β) : SingleAxis (F ×ˢ {fl})

A variable-force modal of one flavor varies on a single axis.