def Semantics.Modality.Kratzer.propExtension (p : BProp Attitudes.Intensional.World) : List Attitudes.Intensional.World

Convert to list of worlds where proposition holds.

Equations

• Semantics.Modality.Kratzer.propExtension p = List.filter p Semantics.Attitudes.Intensional.allWorlds

def Semantics.Modality.Kratzer.propIntersection (props : List (BProp Attitudes.Intensional.World)) : List Attitudes.Intensional.World

The intersection of a set of propositions: worlds satisfying ALL.

Equations

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

def Semantics.Modality.Kratzer.followsFrom (p : BProp Attitudes.Intensional.World) (A : List (BProp Attitudes.Intensional.World)) : Bool

A proposition p follows from a set A iff ∩A ⊆ p (Kratzer p. 31)

In other words: every world satisfying all of A also satisfies p.

Equations

• Semantics.Modality.Kratzer.followsFrom p A = (Semantics.Modality.Kratzer.propIntersection A).all p

def Semantics.Modality.Kratzer.isConsistent (A : List (BProp Attitudes.Intensional.World)) : Bool

A set of propositions is consistent iff ∩A ≠ ∅ (Kratzer p. 31)

Equations

• Semantics.Modality.Kratzer.isConsistent A = !(Semantics.Modality.Kratzer.propIntersection A).isEmpty

def Semantics.Modality.Kratzer.isCompatibleWith (p : BProp Attitudes.Intensional.World) (A : List (BProp Attitudes.Intensional.World)) : Bool

A proposition p is compatible with A iff A ∪ {p} is consistent (Kratzer p. 31)

Equations

• Semantics.Modality.Kratzer.isCompatibleWith p A = Semantics.Modality.Kratzer.isConsistent (p :: A)

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ConvBackground : Type

A conversational background maps worlds to sets of propositions.

This is Kratzer's key innovation: the modal base and ordering source are both conversational backgrounds, but play different roles.

Equations

• Semantics.Modality.Kratzer.ConvBackground = (Semantics.Attitudes.Intensional.World → List (BProp Semantics.Attitudes.Intensional.World))

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ModalBase : Type

The modal base: determines which worlds are accessible.

Equations

• Semantics.Modality.Kratzer.ModalBase = Semantics.Modality.Kratzer.ConvBackground

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.OrderingSource : Type

The ordering source: determines how accessible worlds are ranked.

Equations

• Semantics.Modality.Kratzer.OrderingSource = Semantics.Modality.Kratzer.ConvBackground

def Semantics.Modality.Kratzer.isRealistic (f : ConvBackground) : Prop

A conversational background is realistic iff for all w: w ∈ ∩f(w).

This means the actual world satisfies all propositions in the modal base. Kratzer (p. 32): "For each world, there is a particular body of facts in w that has a counterpart in each world in ∩f(w)."

Equations

• Semantics.Modality.Kratzer.isRealistic f = ∀ (w : Semantics.Attitudes.Intensional.World), ((f w).all fun (p : BProp Semantics.Attitudes.Intensional.World) => p w) = true

def Semantics.Modality.Kratzer.isTotallyRealistic (f : ConvBackground) : Prop

A conversational background is totally realistic iff for all w: ∩f(w) = {w}.

This is the strongest form: only the actual world is accessible. Kratzer (p. 33): "A totally realistic conversational background is a function f such that for any world w, ∩f(w) = {w}."

Equations

• Semantics.Modality.Kratzer.isTotallyRealistic f = ∀ (w : Semantics.Attitudes.Intensional.World), Semantics.Modality.Kratzer.propIntersection (f w) = [w]

def Semantics.Modality.Kratzer.emptyBackground : ConvBackground

The empty conversational background: f(w) = ∅ for all w.

Kratzer (p. 33): "The empty conversational background is the function f such that for any w ∈ W, f(w) = ∅. Since ∩f(w) = W if f(w) = ∅, empty conversational backgrounds are also realistic."

Equations

• Semantics.Modality.Kratzer.emptyBackground x✝ = []

def Semantics.Modality.Kratzer.satisfiedPropositions (A : List (BProp Attitudes.Intensional.World)) (w : Attitudes.Intensional.World) : List (BProp Attitudes.Intensional.World)

The set of propositions from A that world w satisfies.

This is {p ∈ A : w ∈ p} in Kratzer's notation.

Equations

• Semantics.Modality.Kratzer.satisfiedPropositions A w = List.filter (fun (p : BProp Semantics.Attitudes.Intensional.World) => p w) A

def Semantics.Modality.Kratzer.atLeastAsGoodAs (A : List (BProp Attitudes.Intensional.World)) (w z : Attitudes.Intensional.World) : Bool

Kratzer's ordering relation: w ≤_A z

Definition (p. 39): "For all worlds w and z ∈ W: w ≤_A z iff {p: p ∈ A and z ∈ p} ⊆ {p: p ∈ A and w ∈ p}"

Intuitively: w is at least as good as z (w.r.t. ideal A) iff every ideal proposition that z satisfies, w also satisfies.

Note: This is the CORRECT definition using subset inclusion, NOT counting (which would be incorrect).

Equations

• (w ≤[A] z) = (Semantics.Modality.Kratzer.satisfiedPropositions A z).all fun (p : BProp Semantics.Attitudes.Intensional.World) => p w

def Semantics.Modality.Kratzer.«term_≤[_]_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Modality.Kratzer.strictlyBetter (A : List (BProp Attitudes.Intensional.World)) (w z : Attitudes.Intensional.World) : Bool

Strict ordering: w <_A z iff w ≤_A z but not z ≤_A w.

This means w satisfies strictly more ideal propositions than z.

Equations

• (w <[A] z) = ((w ≤[A] z) && !z ≤[A] w)

def Semantics.Modality.Kratzer.«term_<[_]_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Modality.Kratzer.worldOrdering (A : List (BProp Attitudes.Intensional.World)) : SatisfactionOrdering Attitudes.Intensional.World (BProp Attitudes.Intensional.World)

Kratzer's world ordering as a SatisfactionOrdering.

A world w satisfies proposition p iff p(w) = true. This connects Kratzer semantics to the generic ordering framework.

Equations

• Semantics.Modality.Kratzer.worldOrdering A = { satisfies := fun (w : Semantics.Attitudes.Intensional.World) (p : BProp Semantics.Attitudes.Intensional.World) => p w, criteria := A }

theorem Semantics.Modality.Kratzer.atLeastAsGoodAs_eq_generic (A : List (BProp Attitudes.Intensional.World)) (w z : Attitudes.Intensional.World) : (w ≤[A] z) = (worldOrdering A).atLeastAsGood w z

Kratzer's ordering matches the generic framework.

This theorem establishes that atLeastAsGoodAs is exactly the generic SatisfactionOrdering.atLeastAsGood for worlds.

theorem Semantics.Modality.Kratzer.ordering_reflexive (A : List (BProp Attitudes.Intensional.World)) (w : Attitudes.Intensional.World) : (w ≤[A] w) = true

Reflexivity via generic framework.

theorem Semantics.Modality.Kratzer.ordering_transitive (A : List (BProp Attitudes.Intensional.World)) (u v w : Attitudes.Intensional.World) (huv : (u ≤[A] v) = true) (hvw : (v ≤[A] w) = true) : (u ≤[A] w) = true

Transitivity via generic framework.

def Semantics.Modality.Kratzer.kratzerPreorder (A : List (BProp Attitudes.Intensional.World)) : Preorder Attitudes.Intensional.World

Kratzer's ordering as a mathlib Preorder.

Derived from the generic SatisfactionOrdering.toPreorder.

Equations

• Semantics.Modality.Kratzer.kratzerPreorder A = (Semantics.Modality.Kratzer.worldOrdering A).toPreorder

def Semantics.Modality.Kratzer.orderingEquiv (A : List (BProp Attitudes.Intensional.World)) (w z : Attitudes.Intensional.World) : Prop

Equivalence under the ordering (via generic framework).

Equations

• Semantics.Modality.Kratzer.orderingEquiv A w z = (Semantics.Modality.Kratzer.worldOrdering A).equiv w z

theorem Semantics.Modality.Kratzer.orderingEquiv_refl (A : List (BProp Attitudes.Intensional.World)) (w : Attitudes.Intensional.World) : orderingEquiv A w w

theorem Semantics.Modality.Kratzer.orderingEquiv_symm (A : List (BProp Attitudes.Intensional.World)) (w z : Attitudes.Intensional.World) (h : orderingEquiv A w z) : orderingEquiv A z w

theorem Semantics.Modality.Kratzer.orderingEquiv_trans (A : List (BProp Attitudes.Intensional.World)) (u v w : Attitudes.Intensional.World) (huv : orderingEquiv A u v) (hvw : orderingEquiv A v w) : orderingEquiv A u w

theorem Semantics.Modality.Kratzer.empty_ordering_all_equivalent (w z : Attitudes.Intensional.World) : (w ≤[[]] z) = true ∧ (z ≤[[]] w) = true

Theorem 2: Empty ordering makes all worlds equivalent.

If A = ∅, then for all w, z: w ≤_A z and z ≤_A w.

Proof: The set of propositions in ∅ satisfied by any world is ∅. Vacuously, ∅ ⊆ ∅. ∎

theorem Semantics.Modality.Kratzer.empty_ordering_trivial (w z : Attitudes.Intensional.World) : w ≤ z

theorem Semantics.Modality.Kratzer.empty_ordering_universal_equiv (w z : Attitudes.Intensional.World) : orderingEquiv [] w z

def Semantics.Modality.Kratzer.extension (props : List (BProp Attitudes.Intensional.World)) : List Attitudes.Intensional.World

Kratzer's extension: List-based version for the finite World type.

This is propIntersection renamed for clarity.

Equations

• Semantics.Modality.Kratzer.extension props = Semantics.Modality.Kratzer.propIntersection props

def Semantics.Modality.Kratzer.intension (worlds : List Attitudes.Intensional.World) (props : List (BProp Attitudes.Intensional.World)) : List (BProp Attitudes.Intensional.World)

Kratzer's intension: Filter propositions true at all given worlds.

Equations

• Semantics.Modality.Kratzer.intension worlds props = Core.Proposition.GaloisConnection.intensionL worlds props

theorem Semantics.Modality.Kratzer.extension_eq_core (props : List (BProp Attitudes.Intensional.World)) : extension props = Core.Proposition.GaloisConnection.extensionL Attitudes.Intensional.allWorlds props

theorem Semantics.Modality.Kratzer.extension_antitone (A B : List (BProp Attitudes.Intensional.World)) (w : Attitudes.Intensional.World) (hSub : ∀ p ∈ A, p ∈ B) (hw : w ∈ extension B) : w ∈ extension A

theorem Semantics.Modality.Kratzer.intension_antitone (W V : List Attitudes.Intensional.World) (A : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) (hSub : ∀ w ∈ W, w ∈ V) (hp : p ∈ intension V A) : p ∈ intension W A

def Semantics.Modality.Kratzer.accessibleWorlds (f : ModalBase) (w : Attitudes.Intensional.World) : List Attitudes.Intensional.World

The set of worlds accessible from w given modal base f.

These are exactly the worlds in ∩f(w) - worlds compatible with all facts in f(w).

Equations

• Semantics.Modality.Kratzer.accessibleWorlds f w = Semantics.Modality.Kratzer.propIntersection (f w)

theorem Semantics.Modality.Kratzer.accessible_is_extension (f : ModalBase) (w : Attitudes.Intensional.World) : accessibleWorlds f w = extension (f w)

def Semantics.Modality.Kratzer.accessibleFrom (f : ModalBase) (w w' : Attitudes.Intensional.World) : Bool

Accessibility predicate: w' is accessible from w iff w' ∈ ∩f(w).

Equations

• Semantics.Modality.Kratzer.accessibleFrom f w w' = (f w).all fun (p : BProp Semantics.Attitudes.Intensional.World) => p w'

def Semantics.Modality.Kratzer.bestWorlds (f : ModalBase) (g : OrderingSource) (w : Attitudes.Intensional.World) : List Attitudes.Intensional.World

The best worlds among accessible worlds, according to ordering source g.

These are the accessible worlds that are maximal under ≤{g(w)}: worlds w' such that for all accessible w'', w' ≤{g(w)} w''.

When g(w) = ∅, all accessible worlds are best (by Theorem 2).

Equations

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

theorem Semantics.Modality.Kratzer.empty_ordering_simple (f : ModalBase) (w : Attitudes.Intensional.World) : bestWorlds f (fun (x : Attitudes.Intensional.World) => []) w = accessibleWorlds f w

Theorem 3: Empty ordering source reduces to simple accessibility.

When g(w) = ∅, bestWorlds = accessibleWorlds.

theorem Semantics.Modality.Kratzer.empty_ordering_emptyBackground (f : ModalBase) (w : Attitudes.Intensional.World) : bestWorlds f emptyBackground w = accessibleWorlds f w

Variant of empty_ordering_simple matching emptyBackground by name. Avoids the unfold emptyBackground workaround needed before rw [empty_ordering_simple].

def Semantics.Modality.Kratzer.bestAmong (worlds : List Attitudes.Intensional.World) (ordering : List (BProp Attitudes.Intensional.World)) : List Attitudes.Intensional.World

The best worlds among a given set, ranked by an ordering. Unlike bestWorlds which computes accessible worlds from a modal base, bestAmong takes a precomputed world list. This is needed when the domain has already been restricted (e.g., by promoted priorities in @cite{rubinstein-2014}'s favored worlds).

Equations

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

theorem Semantics.Modality.Kratzer.bestAmong_empty (worlds : List Attitudes.Intensional.World) : bestAmong worlds [] = worlds

With empty ordering, all worlds are best (Kratzer's theorem 2).

theorem Semantics.Modality.Kratzer.bestAmong_sub (worlds : List Attitudes.Intensional.World) (ordering : List (BProp Attitudes.Intensional.World)) (w : Attitudes.Intensional.World) : w ∈ bestAmong worlds ordering → w ∈ worlds

bestAmong is a subset of the input worlds.

def Semantics.Modality.Kratzer.simpleNecessity (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Simple f-necessity (Kratzer p. 32): p is true at ALL accessible worlds.

⟦must⟧_f(p)(w) = ∀w' ∈ ∩f(w). p(w')

Equations

• Semantics.Modality.Kratzer.simpleNecessity f p w = (Semantics.Modality.Kratzer.accessibleWorlds f w).all p

def Semantics.Modality.Kratzer.simplePossibility (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Simple f-possibility (Kratzer p. 32): p is true at SOME accessible world.

⟦can⟧_f(p)(w) = ∃w' ∈ ∩f(w). p(w')

Equations

• Semantics.Modality.Kratzer.simplePossibility f p w = (Semantics.Modality.Kratzer.accessibleWorlds f w).any p

def Semantics.Modality.Kratzer.necessity (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Necessity with ordering (Kratzer p. 40): p is true at ALL best worlds.

⟦must⟧_{f,g}(p)(w) = ∀w' ∈ Best(f,g,w). p(w')

Equations

• Semantics.Modality.Kratzer.necessity f g p w = (Semantics.Modality.Kratzer.bestWorlds f g w).all p

def Semantics.Modality.Kratzer.possibility (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Possibility with ordering: p is true at SOME best world.

⟦can⟧_{f,g}(p)(w) = ∃w' ∈ Best(f,g,w). p(w')

Equations

• Semantics.Modality.Kratzer.possibility f g p w = (Semantics.Modality.Kratzer.bestWorlds f g w).any p

theorem Semantics.Modality.Kratzer.duality (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (necessity f g p w == !possibility f g (fun (w' : Attitudes.Intensional.World) => !p w') w) = true

Theorem: Modal duality holds.

□p ↔ ¬◇¬p

theorem Semantics.Modality.Kratzer.totally_realistic_gives_T (f : ModalBase) (g : OrderingSource) (hTotal : ∀ (w : Attitudes.Intensional.World), accessibleWorlds f w = [w]) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hNec : necessity f g p w = true) : p w = true

Theorem 4: Totally realistic base gives T axiom.

If f is totally realistic (∩f(w) = {w}), then □p → p.

theorem Semantics.Modality.Kratzer.realistic_gives_reflexive_access (f : ModalBase) (hReal : isRealistic f) (w : Attitudes.Intensional.World) : w ∈ accessibleWorlds f w

Theorem 5: Realistic base gives reflexive accessibility.

If f is realistic (w ∈ ∩f(w) for all w), then the evaluation world is always accessible from itself.

theorem Semantics.Modality.Kratzer.empty_base_universal_access (w : Attitudes.Intensional.World) : accessibleWorlds emptyBackground w = Attitudes.Intensional.allWorlds

Theorem 6: Empty modal base gives universal accessibility.

If f(w) = ∅ for all w, then ∩f(w) = W (all worlds accessible).

def Semantics.Modality.Kratzer.isTransitiveAccess (f : ModalBase) : Prop

Equations

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

def Semantics.Modality.Kratzer.isSymmetricAccess (f : ModalBase) : Prop

Equations

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

def Semantics.Modality.Kratzer.isEuclideanAccess (f : ModalBase) : Prop

Equations

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

theorem Semantics.Modality.Kratzer.D_axiom (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSerial : (bestWorlds f g w).length > 0) (hNec : necessity f g p w = true) : possibility f g p w = true

D Axiom (Seriality): □p → ◇p

theorem Semantics.Modality.Kratzer.realistic_is_serial (f : ModalBase) (hReal : isRealistic f) (w : Attitudes.Intensional.World) : (accessibleWorlds f w).length > 0

theorem Semantics.Modality.Kratzer.D_axiom_realistic (f : ModalBase) (hReal : isRealistic f) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hNec : necessity f emptyBackground p w = true) : possibility f emptyBackground p w = true

theorem Semantics.Modality.Kratzer.four_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hTrans : isTransitiveAccess f) (hNec : necessity f emptyBackground p w = true) : necessity f emptyBackground (necessity f emptyBackground p) w = true

4 Axiom (Transitivity): □p → □□p

theorem Semantics.Modality.Kratzer.B_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSym : isSymmetricAccess f) (hP : p w = true) : necessity f emptyBackground (possibility f emptyBackground p) w = true

B Axiom (Symmetry): p → □◇p

theorem Semantics.Modality.Kratzer.five_axiom (f : ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hEuc : isEuclideanAccess f) (hPoss : possibility f emptyBackground p w = true) : necessity f emptyBackground (possibility f emptyBackground p) w = true

5 Axiom (Euclidean): ◇p → □◇p

def Semantics.Modality.Kratzer.isS4Base (f : ModalBase) : Prop

Equations

• Semantics.Modality.Kratzer.isS4Base f = (Semantics.Modality.Kratzer.isRealistic f ∧ Semantics.Modality.Kratzer.isTransitiveAccess f)

def Semantics.Modality.Kratzer.isS5Base (f : ModalBase) : Prop

Equations

• Semantics.Modality.Kratzer.isS5Base f = (Semantics.Modality.Kratzer.isRealistic f ∧ Semantics.Modality.Kratzer.isEuclideanAccess f)

theorem Semantics.Modality.Kratzer.euclidean_reflexive_implies_symmetric (f : ModalBase) (hReal : isRealistic f) (hEuc : isEuclideanAccess f) : isSymmetricAccess f

theorem Semantics.Modality.Kratzer.euclidean_reflexive_implies_transitive (f : ModalBase) (hReal : isRealistic f) (hEuc : isEuclideanAccess f) : isTransitiveAccess f

theorem Semantics.Modality.Kratzer.S5_satisfies_all (f : ModalBase) (hS5 : isS5Base f) : isRealistic f ∧ isSymmetricAccess f ∧ isTransitiveAccess f ∧ isEuclideanAccess f

def Semantics.Modality.Kratzer.atLeastAsGoodPossibility (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

p is at least as good a possibility as q in w with respect to f and g.

Equations

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

def Semantics.Modality.Kratzer.betterPossibility (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Equations

• Semantics.Modality.Kratzer.betterPossibility f g p q w = (Semantics.Modality.Kratzer.atLeastAsGoodPossibility f g p q w && !Semantics.Modality.Kratzer.atLeastAsGoodPossibility f g q p w)

theorem Semantics.Modality.Kratzer.comparative_poss_reflexive (f : ModalBase) (g : OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : atLeastAsGoodPossibility f g p p w = true

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

def Semantics.Modality.Kratzer.implies (p q : BProp Attitudes.Intensional.World) : BProp Attitudes.Intensional.World

Equations

• Semantics.Modality.Kratzer.implies p q w = (!p w || q w)

theorem Semantics.Modality.Kratzer.K_axiom (f : ModalBase) (g : OrderingSource) (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hImpl : necessity f g (implies p q) w = true) (hP : necessity f g p w = true) : necessity f g q w = true

Theorem: K Axiom (Distribution) holds.

□(p → q) → (□p → □q)

def Semantics.Modality.Kratzer.restrictedBase (f : ModalBase) (antecedent : BProp Attitudes.Intensional.World) : ModalBase

Conditionals as modal base restrictors.

"If α, (must) β" = must_f+α β

Equations

• Semantics.Modality.Kratzer.restrictedBase f antecedent w = antecedent :: f w

def Semantics.Modality.Kratzer.materialImplication (p q : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

Equations

• Semantics.Modality.Kratzer.materialImplication p q w = (!p w || q w)

def Semantics.Modality.Kratzer.strictImplication (p q : BProp Attitudes.Intensional.World) : Bool

Equations

• Semantics.Modality.Kratzer.strictImplication p q = Semantics.Attitudes.Intensional.allWorlds.all fun (w : Semantics.Attitudes.Intensional.World) => !p w || q w

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

def Semantics.Modality.Kratzer.concreteEpistemicBase : ModalBase

Equations

• Semantics.Modality.Kratzer.concreteEpistemicBase x✝ = [Semantics.Modality.groundWet]

def Semantics.Modality.Kratzer.concreteEpistemicParams : KratzerParams

Equations

• Semantics.Modality.Kratzer.concreteEpistemicParams = { base := Semantics.Modality.Kratzer.concreteEpistemicBase, ordering := Semantics.Modality.Kratzer.emptyBackground }

def Semantics.Modality.Kratzer.KratzerEpistemic : ModalTheory

Equations

• Semantics.Modality.Kratzer.KratzerEpistemic = Semantics.Modality.Kratzer.KratzerTheory Semantics.Modality.Kratzer.concreteEpistemicParams

def Semantics.Modality.Kratzer.concreteCircumstantialBase : ModalBase

Equations

• Semantics.Modality.Kratzer.concreteCircumstantialBase x✝ = []

def Semantics.Modality.Kratzer.concreteDeonticOrdering : OrderingSource

Equations

• Semantics.Modality.Kratzer.concreteDeonticOrdering x✝ = [Semantics.Modality.johnHome]

def Semantics.Modality.Kratzer.concreteDeonticParams : KratzerParams

Equations

• Semantics.Modality.Kratzer.concreteDeonticParams = { base := Semantics.Modality.Kratzer.concreteCircumstantialBase, ordering := Semantics.Modality.Kratzer.concreteDeonticOrdering }

def Semantics.Modality.Kratzer.KratzerDeontic : ModalTheory

Equations

• Semantics.Modality.Kratzer.KratzerDeontic = Semantics.Modality.Kratzer.KratzerTheory Semantics.Modality.Kratzer.concreteDeonticParams

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