structure Semantics.Modality.Kratzer.EpistemicFlavor (W : Type u_2) : Type u_2

Epistemic modality: what is known/believed.

• Modal base: evidence/knowledge
• Ordering source: empty (or stereotypical for "probably")

• evidence : ModalBase W
• ordering : OrderingSource W

structure Semantics.Modality.Kratzer.DeonticFlavor (W : Type u_2) : Type u_2

Deontic modality: what is required/permitted by norms.

• Modal base: circumstances
• Ordering source: laws/norms

• circumstances : ModalBase W
• norms : OrderingSource W

structure Semantics.Modality.Kratzer.BouleticFlavor (W : Type u_2) : Type u_2

Bouletic modality: what is wanted/desired.

• Modal base: circumstances
• Ordering source: desires

• circumstances : ModalBase W
• desires : OrderingSource W

structure Semantics.Modality.Kratzer.TeleologicalFlavor (W : Type u_2) : Type u_2

Teleological modality: what leads to goals.

• Modal base: circumstances
• Ordering source: goals

• circumstances : ModalBase W
• goals : OrderingSource W

Flavor Tags

Each flavor structure maps to the theory-neutral ModalFlavor enum from Intensional, bridging Kratzer's parameterized semantics to the typological meaning space (Imel, Guo, & [IGST26]).

def Semantics.Modality.Kratzer.EpistemicFlavor.flavorTag : ModalFlavor

Epistemic modality maps to the epistemic flavor tag.

Equations

• Semantics.Modality.Kratzer.EpistemicFlavor.flavorTag = Semantics.Modality.ModalFlavor.epistemic

def Semantics.Modality.Kratzer.DeonticFlavor.flavorTag : ModalFlavor

Deontic modality maps to the deontic flavor tag.

Equations

• Semantics.Modality.Kratzer.DeonticFlavor.flavorTag = Semantics.Modality.ModalFlavor.deontic

def Semantics.Modality.Kratzer.BouleticFlavor.flavorTag : ModalFlavor

Bouletic modality maps to the bouletic flavor tag (desire-based ordering).

Equations

• Semantics.Modality.Kratzer.BouleticFlavor.flavorTag = Semantics.Modality.ModalFlavor.bouletic

def Semantics.Modality.Kratzer.TeleologicalFlavor.flavorTag : ModalFlavor

Teleological modality maps to the circumstantial flavor tag (teleological is subsumed under circumstantial in the 2×3 space).

Equations

• Semantics.Modality.Kratzer.TeleologicalFlavor.flavorTag = Semantics.Modality.ModalFlavor.circumstantial

Background Classification (Kratzer 2012)

Each flavor structure maps to a BackgroundClass from [Kra12]'s three-way classification, which refines the traditional epistemic/circumstantial binary based on the projection mode of the conversational background ([Mat16] Table 18.3).

def Semantics.Modality.Kratzer.EpistemicFlavor.toBackgroundClass {W : Type u_1} : EpistemicFlavor W → BackgroundClass

Epistemic modality: factual-evidential by default.

Equations

• x✝.toBackgroundClass = Semantics.Modality.BackgroundClass.factualEvidential

def Semantics.Modality.Kratzer.DeonticFlavor.toBackgroundClass {W : Type u_1} : DeonticFlavor W → BackgroundClass

Equations

• x✝.toBackgroundClass = Semantics.Modality.BackgroundClass.factualCircumstantial

def Semantics.Modality.Kratzer.BouleticFlavor.toBackgroundClass {W : Type u_1} : BouleticFlavor W → BackgroundClass

Equations

• x✝.toBackgroundClass = Semantics.Modality.BackgroundClass.factualCircumstantial

def Semantics.Modality.Kratzer.TeleologicalFlavor.toBackgroundClass {W : Type u_1} : TeleologicalFlavor W → BackgroundClass

Equations

• x✝.toBackgroundClass = Semantics.Modality.BackgroundClass.factualCircumstantial

theorem Semantics.Modality.Kratzer.deontic_factual {W : Type u_1} (f : DeonticFlavor W) : f.toBackgroundClass.projectionMode = ProjectionMode.factual

theorem Semantics.Modality.Kratzer.bouletic_factual {W : Type u_1} (f : BouleticFlavor W) : f.toBackgroundClass.projectionMode = ProjectionMode.factual

theorem Semantics.Modality.Kratzer.teleological_factual {W : Type u_1} (f : TeleologicalFlavor W) : f.toBackgroundClass.projectionMode = ProjectionMode.factual

theorem Semantics.Modality.Kratzer.epistemic_default_factual {W : Type u_1} (f : EpistemicFlavor W) : f.toBackgroundClass.projectionMode = ProjectionMode.factual

Kratzer Parameters

structure Semantics.Modality.Kratzer.KratzerParams (W : Type u_2) : Type u_2

• base : ModalBase W
• ordering : OrderingSource W

def Semantics.Modality.Kratzer.EpistemicFlavor.toKratzerParams {W : Type u_1} (f : EpistemicFlavor W) : KratzerParams W

Equations

• f.toKratzerParams = { base := f.evidence, ordering := f.ordering }

def Semantics.Modality.Kratzer.DeonticFlavor.toKratzerParams {W : Type u_1} (f : DeonticFlavor W) : KratzerParams W

Equations

• f.toKratzerParams = { base := f.circumstances, ordering := f.norms }

def Semantics.Modality.Kratzer.BouleticFlavor.toKratzerParams {W : Type u_1} (f : BouleticFlavor W) : KratzerParams W

Equations

• f.toKratzerParams = { base := f.circumstances, ordering := f.desires }

def Semantics.Modality.Kratzer.TeleologicalFlavor.toKratzerParams {W : Type u_1} (f : TeleologicalFlavor W) : KratzerParams W

Equations

• f.toKratzerParams = { base := f.circumstances, ordering := f.goals }

Standard parameter configurations

def Semantics.Modality.Kratzer.emptyModalBase {W : Type u_1} : ModalBase W

Equations

• Semantics.Modality.Kratzer.emptyModalBase = Semantics.Modality.Kratzer.emptyBackground

def Semantics.Modality.Kratzer.emptyOrderingSource {W : Type u_1} : OrderingSource W

Equations

• Semantics.Modality.Kratzer.emptyOrderingSource = Semantics.Modality.Kratzer.emptyBackground

def Semantics.Modality.Kratzer.minimalParams {W : Type u_1} : KratzerParams W

Equations

• Semantics.Modality.Kratzer.minimalParams = { base := Semantics.Modality.Kratzer.emptyModalBase, ordering := Semantics.Modality.Kratzer.emptyOrderingSource }

def Semantics.Modality.Kratzer.epistemicParams {W : Type u_1} (evidence : ModalBase W) : KratzerParams W

Equations

• Semantics.Modality.Kratzer.epistemicParams evidence = { base := evidence, ordering := Semantics.Modality.Kratzer.emptyBackground }

def Semantics.Modality.Kratzer.deonticParams {W : Type u_1} (circumstances : ModalBase W) (norms : OrderingSource W) : KratzerParams W

Equations

• Semantics.Modality.Kratzer.deonticParams circumstances norms = { base := circumstances, ordering := norms }

Duality (polymorphic)

Modal duality holds directly from necessity/possibility (Prop-based). See Operators.duality for the proof.

def Semantics.Modality.Kratzer.KratzerParams.necessity {W : Type u_1} (params : KratzerParams W) (p : W → Prop) (w : W) : Prop

Evaluate a KratzerParams as necessity (∀ over best worlds).

Equations

• params.necessity p w = Semantics.Modality.Kratzer.necessity params.base params.ordering p w

def Semantics.Modality.Kratzer.KratzerParams.possibility {W : Type u_1} (params : KratzerParams W) (p : W → Prop) (w : W) : Prop

Evaluate a KratzerParams as possibility (∃ over best worlds).

Equations

• params.possibility p w = Semantics.Modality.Kratzer.possibility params.base params.ordering p w

theorem Semantics.Modality.Kratzer.KratzerParams.duality {W : Type u_1} (params : KratzerParams W) (p : W → Prop) (w : W) : params.necessity p w ↔ ¬params.possibility (fun (w' : W) => ¬p w') w

Duality: □p ↔ ¬◇¬p for any KratzerParams.