Modal force and flavor

This file defines the vocabulary of modal typology. A modal force is a quantificational strength, necessity, weak necessity or possibility, ordered by strength; a modal flavor is a source of modality, epistemic, deontic, bouletic or circumstantial ([Kra81b]); and a modal item pairs a form with the force-flavor pairs it can express, the representation of a modal's meaning in [IGST26]. The temporal perspective and orientation of [Con02] locate a modal claim in time.

Main definitions

• Modality.ModalForce, with the strength order possibility < weakNecessity < necessity, the classical dual ModalForce.dual, the concord class ModalForce.IsUniversal, and the classical force ModalForce.classical, which reads weak necessity as necessity.
• Modality.ModalFlavor and the pair type Modality.ForceFlavor.
• Modality.ModalItem, with its domain and variation predicates and its classical reading ModalItem.classical.
• Modality.TemporalPerspective, Modality.TemporalOrientation.

References

• [Kra81b]
• [vFI08]
• [Rub14]
• [AJ22]
• [AJ26]
• [IGST26]
• [Zei07]
• [Nau08]
• [Mat16]
• [Con02]

Modal force

inductive Modality.ModalForce : Type

A modal force is a quantificational strength. Weak necessity, ought and should, lies between necessity and possibility ([vFI08]); whether it quantifies universally over a narrower domain ([vFI08]), compares alternatives ([Rub14]) or predicates of a plurality of worlds ([AJ22]) is open ([AJ26]).

• necessity : ModalForce
• weakNecessity : ModalForce
• possibility : ModalForce

@[instance_reducible]

instance Modality.instDecidableEqModalForce : DecidableEq ModalForce

Equations

• Modality.instDecidableEqModalForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprModalForce.repr : ModalForce → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprModalForce : Repr ModalForce

Equations

• Modality.instReprModalForce = { reprPrec := Modality.instReprModalForce.repr }

@[instance_reducible]

instance Modality.instInhabitedModalForce : Inhabited ModalForce

Equations

• Modality.instInhabitedModalForce = { default := Modality.instInhabitedModalForce.default }

@[instance_reducible]

instance Modality.instFintypeModalForce : Fintype ModalForce

Equations

• Modality.instFintypeModalForce = { elems := { val := ↑Modality.ModalForce.enumList, nodup := Modality.ModalForce.enumList_nodup }, complete := Modality.instFintypeModalForce._proof_1 }

def Modality.ModalForce.rank : ModalForce → ℕ

The strength of a force, possibility the weakest.

Equations

• Modality.ModalForce.possibility.rank = 0
• Modality.ModalForce.weakNecessity.rank = 1
• Modality.ModalForce.necessity.rank = 2

@[instance_reducible]

instance Modality.ModalForce.instLinearOrder : LinearOrder ModalForce

Forces are ordered by strength: a necessity claim entails the weak necessity claim, which entails the possibility claim.

Equations

• Modality.ModalForce.instLinearOrder = LinearOrder.lift' Modality.ModalForce.rank Modality.ModalForce.instLinearOrder._proof_1

@[instance_reducible]

instance Modality.ModalForce.instBoundedOrder : BoundedOrder ModalForce

Equations

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

def Modality.ModalForce.dual : ModalForce → ModalForce

The classical dual exchanges necessity and possibility. Weak necessity has no settled possibility counterpart ([AJ26] §2.4) and is sent to possibility.

Equations

• Modality.ModalForce.necessity.dual = Modality.ModalForce.possibility
• Modality.ModalForce.weakNecessity.dual = Modality.ModalForce.possibility
• Modality.ModalForce.possibility.dual = Modality.ModalForce.necessity

def Modality.ModalForce.IsUniversal (f : ModalForce) : Prop

Necessity and weak necessity quantify universally, the concord class that separates them from possibility ([Zei07]).

Equations

• f.IsUniversal = (f ≠ Modality.ModalForce.possibility)

@[instance_reducible]

instance Modality.ModalForce.instDecidablePredIsUniversal : DecidablePred IsUniversal

Equations

• x✝.instDecidablePredIsUniversal = { decide := !decide (x✝ = Modality.ModalForce.possibility), reflects_decide := ⋯ }

def Modality.ModalForce.classical : ModalForce → ModalForce

The classical force of a force, on the two-point scale of necessity and possibility along which [Nau08] and [Mat16] compare modal systems: weak necessity quantifies universally ([vFI08]) and counts as necessity.

Equations

• Modality.ModalForce.possibility.classical = Modality.ModalForce.possibility
• x✝.classical = Modality.ModalForce.necessity

@[simp]

theorem Modality.ModalForce.dual_classical {f : ModalForce} : f.classical.dual = f.dual

The classical dual is blind to the weak–strong distinction.

theorem Modality.ModalForce.dual_dual {f : ModalForce} : f.dual.dual = f.classical

The double dual of a force is its classical force: dualizing twice closes weak necessity up to necessity.

@[simp]

theorem Modality.ModalForce.classical_eq_necessity_iff {f : ModalForce} : f.classical = necessity ↔ f.IsUniversal

Modal flavor

inductive Modality.ModalFlavor : Type

A modal flavor is the source of a modal claim: an epistemic or a circumstantial modal base, or a circumstantial base ordered by what the law requires or what someone wants ([Kra81b]); teleological modality, ordered by goals, counts as circumstantial.

• epistemic : ModalFlavor
• deontic : ModalFlavor
• bouletic : ModalFlavor
• circumstantial : ModalFlavor

@[instance_reducible]

instance Modality.instDecidableEqModalFlavor : DecidableEq ModalFlavor

Equations

• Modality.instDecidableEqModalFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Modality.instReprModalFlavor : Repr ModalFlavor

Equations

• Modality.instReprModalFlavor = { reprPrec := Modality.instReprModalFlavor.repr }

def Modality.instReprModalFlavor.repr : ModalFlavor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instInhabitedModalFlavor : Inhabited ModalFlavor

Equations

• Modality.instInhabitedModalFlavor = { default := Modality.instInhabitedModalFlavor.default }

@[instance_reducible]

instance Modality.instFintypeModalFlavor : Fintype ModalFlavor

Equations

• Modality.instFintypeModalFlavor = { elems := { val := ↑Modality.ModalFlavor.enumList, nodup := Modality.ModalFlavor.enumList_nodup }, complete := Modality.instFintypeModalFlavor._proof_1 }

@[reducible, inline]

abbrev Modality.ForceFlavor : Type

A force-flavor pair is one point of the modal semantic space of [IGST26], which has two forces and three flavors; weak necessity ([AJ26]) and bouletic flavor ([Kra81b]) extend the space to twelve points.

Equations

• Modality.ForceFlavor = (Modality.ModalForce × Modality.ModalFlavor)

@[reducible, inline]

abbrev Modality.ForceFlavor.force : ForceFlavor → ModalForce

The force of a force-flavor pair.

Equations

• Modality.ForceFlavor.force = Prod.fst

@[reducible, inline]

abbrev Modality.ForceFlavor.flavor : ForceFlavor → ModalFlavor

The flavor of a force-flavor pair.

Equations

• Modality.ForceFlavor.flavor = Prod.snd

Modal items

structure Modality.ModalItem : Type

A modal item is the shared core of an expression carrying modal meaning, which Auxiliary.toModalItem projects onto and which a modal adverb's entry instantiates directly.

• form : String
• meaning : Finset ForceFlavor

  The force-flavor pairs the item can express, in an upward-entailing context.

• register : SocialMeaning.Register

@[instance_reducible]

instance Modality.instDecidableEqModalItem : DecidableEq ModalItem

Equations

• Modality.instDecidableEqModalItem = Modality.instDecidableEqModalItem.decEq

def Modality.instDecidableEqModalItem.decEq (x✝ x✝¹ : ModalItem) : Decidable (x✝ = x✝¹)

Equations

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

def Modality.ModalItem.Epistemic (m : ModalItem) : Prop

A modal item is epistemic when every pair it expresses is.

Equations

• m.Epistemic = ∀ ff ∈ m.meaning, ff.flavor = Modality.ModalFlavor.epistemic

def Modality.ModalItem.Circumstantial (m : ModalItem) : Prop

A modal item is circumstantial, in the broad sense covering the priority flavours, when no pair it expresses is epistemic.

Equations

• m.Circumstantial = ∀ ff ∈ m.meaning, ff.flavor ≠ Modality.ModalFlavor.epistemic

def Modality.ModalItem.forces (m : ModalItem) : Finset ModalForce

The forces a modal item expresses.

Equations

• m.forces = Finset.image Prod.fst m.meaning

def Modality.ModalItem.flavors (m : ModalItem) : Finset ModalFlavor

The flavours a modal item expresses.

Equations

• m.flavors = Finset.image Prod.snd m.meaning

def Modality.ModalItem.forcesOf (m : ModalItem) (fl : ModalFlavor) : Finset ModalForce

The forces a modal item expresses under a flavour.

Equations

• m.forcesOf fl = Finset.image Prod.fst ({x ∈ m.meaning | x.flavor = fl})

def Modality.ModalItem.VariesForce (m : ModalItem) : Prop

A modal item varies in force when it expresses two forces.

Equations

• m.VariesForce = (2 ≤ m.forces.card)

def Modality.ModalItem.VariesFlavor (m : ModalItem) : Prop

A modal item varies in flavour when it expresses two flavours.

Equations

• m.VariesFlavor = (2 ≤ m.flavors.card)

@[instance_reducible]

instance Modality.ModalItem.instDecidablePredEpistemic : DecidablePred Epistemic

Equations

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

@[instance_reducible]

instance Modality.ModalItem.instDecidablePredCircumstantial : DecidablePred Circumstantial

Equations

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

@[instance_reducible]

instance Modality.ModalItem.instDecidablePredVariesForce : DecidablePred VariesForce

Equations

• x✝.instDecidablePredVariesForce = { decide := Nat.ble 2 x✝.forces.card, reflects_decide := ⋯ }

@[instance_reducible]

instance Modality.ModalItem.instDecidablePredVariesFlavor : DecidablePred VariesFlavor

Equations

• x✝.instDecidablePredVariesFlavor = { decide := Nat.ble 2 x✝.flavors.card, reflects_decide := ⋯ }

def Modality.ModalItem.classical (m : ModalItem) : ModalItem

A modal item on the classical force scale, its weak necessity read as necessity.

Equations

• m.classical = { form := m.form, meaning := Finset.image (Prod.map Modality.ModalForce.classical id) m.meaning, register := m.register }

@[simp]

theorem Modality.ModalItem.forces_classical (m : ModalItem) : m.classical.forces = Finset.image ModalForce.classical m.forces

@[simp]

theorem Modality.ModalItem.flavors_classical (m : ModalItem) : m.classical.flavors = m.flavors

Modal-temporal axes

The two temporal axes of modal interpretation ([Con02] §2): the perspective is the time at which the modal base and ordering source are evaluated, the orientation the relation between the perspective time and the prejacent's time. [Con02] uses only the future and past orientations.

inductive Modality.TemporalPerspective : Type

The time at which a modal base and ordering source are evaluated.

• present : TemporalPerspective

  Evaluation at the utterance time.

• past : TemporalPerspective

  Evaluation at a prior time, as under a perfect.

@[instance_reducible]

instance Modality.instDecidableEqTemporalPerspective : DecidableEq TemporalPerspective

Equations

• Modality.instDecidableEqTemporalPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprTemporalPerspective.repr : TemporalPerspective → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprTemporalPerspective : Repr TemporalPerspective

Equations

• Modality.instReprTemporalPerspective = { reprPrec := Modality.instReprTemporalPerspective.repr }

@[instance_reducible]

instance Modality.instInhabitedTemporalPerspective : Inhabited TemporalPerspective

Equations

• Modality.instInhabitedTemporalPerspective = { default := Modality.instInhabitedTemporalPerspective.default }

@[instance_reducible]

instance Modality.instFintypeTemporalPerspective : Fintype TemporalPerspective

Equations

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

inductive Modality.TemporalOrientation : Type

The relation between the perspective time and the prejacent's instantiation time.

• past : TemporalOrientation

  The prejacent is instantiated before the perspective time.

• present : TemporalOrientation

  The prejacent coincides with the perspective time.

• future : TemporalOrientation

  The prejacent is instantiated at or after the perspective time.

@[instance_reducible]

instance Modality.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

• Modality.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprTemporalOrientation.repr : TemporalOrientation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprTemporalOrientation : Repr TemporalOrientation

Equations

• Modality.instReprTemporalOrientation = { reprPrec := Modality.instReprTemporalOrientation.repr }

@[instance_reducible]

instance Modality.instInhabitedTemporalOrientation : Inhabited TemporalOrientation

Equations

• Modality.instInhabitedTemporalOrientation = { default := Modality.instInhabitedTemporalOrientation.default }

@[instance_reducible]

instance Modality.instFintypeTemporalOrientation : Fintype TemporalOrientation

Equations

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