structure Semantics.Modality.Kratzer.EpistemicFlavor : Type

Epistemic modality: what is known/believed.

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

• evidence : ModalBase
• ordering : OrderingSource

structure Semantics.Modality.Kratzer.DeonticFlavor : Type

Deontic modality: what is required/permitted by norms.

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

• circumstances : ModalBase
• norms : OrderingSource

structure Semantics.Modality.Kratzer.BouleticFlavor : Type

Bouletic modality: what is wanted/desired.

• Modal base: circumstances
• Ordering source: desires

• circumstances : ModalBase
• desires : OrderingSource

structure Semantics.Modality.Kratzer.TeleologicalFlavor : Type

Teleological modality: what leads to goals.

• Modal base: circumstances
• Ordering source: goals

• circumstances : ModalBase
• goals : OrderingSource

Flavor Tags

Each flavor structure maps to the theory-neutral ModalFlavor enum from Core.ModalLogic, bridging Kratzer's parameterized semantics to the typological meaning space (Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}).

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

Epistemic modality maps to the epistemic flavor tag.

Equations

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

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

Deontic modality maps to the deontic flavor tag.

Equations

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

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

Bouletic modality maps to the deontic flavor tag (both norm-based).

Equations

• Semantics.Modality.Kratzer.BouleticFlavor.flavorTag = Core.Modality.ModalFlavor.deontic

def Semantics.Modality.Kratzer.TeleologicalFlavor.flavorTag : Core.Modality.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 = Core.Modality.ModalFlavor.circumstantial

structure Semantics.Modality.Kratzer.KratzerParams : Type

• base : ModalBase
• ordering : OrderingSource

def Semantics.Modality.Kratzer.EpistemicFlavor.toKratzerParams (f : EpistemicFlavor) : KratzerParams

Extract KratzerParams from an epistemic flavor structure.

Equations

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

def Semantics.Modality.Kratzer.DeonticFlavor.toKratzerParams (f : DeonticFlavor) : KratzerParams

Extract KratzerParams from a deontic flavor structure.

Equations

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

def Semantics.Modality.Kratzer.BouleticFlavor.toKratzerParams (f : BouleticFlavor) : KratzerParams

Extract KratzerParams from a bouletic flavor structure.

Equations

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

def Semantics.Modality.Kratzer.TeleologicalFlavor.toKratzerParams (f : TeleologicalFlavor) : KratzerParams

Extract KratzerParams from a teleological flavor structure.

Equations

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

def Semantics.Modality.Kratzer.KratzerTheory (params : KratzerParams) : ModalTheory

Equations

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

def Semantics.Modality.Kratzer.emptyModalBase : ModalBase

Equations

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

def Semantics.Modality.Kratzer.emptyOrderingSource : OrderingSource

Equations

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

def Semantics.Modality.Kratzer.minimalParams : KratzerParams

Equations

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

def Semantics.Modality.Kratzer.epistemicParams (evidence : ModalBase) : KratzerParams

Equations

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

def Semantics.Modality.Kratzer.deonticParams (circumstances : ModalBase) (norms : OrderingSource) : KratzerParams

Equations

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

def Semantics.Modality.Kratzer.KratzerMinimal : ModalTheory

Equations

• Semantics.Modality.Kratzer.KratzerMinimal = Semantics.Modality.Kratzer.KratzerTheory Semantics.Modality.Kratzer.minimalParams

theorem Semantics.Modality.Kratzer.kratzer_duality (params : KratzerParams) (p : Proposition) (w : Attitudes.Intensional.World) : (KratzerTheory params).dualityHolds p w = true

theorem Semantics.Modality.Kratzer.kratzer_isNormal (params : KratzerParams) : (KratzerTheory params).isNormal

theorem Semantics.Modality.Kratzer.kratzerMinimal_isNormal : KratzerMinimal.isNormal