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)) : Core.SatisfactionOrdering.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.kratzerNormality (A : List (BProp Attitudes.Intensional.World)) : Core.Order.NormalityOrder Attitudes.Intensional.World

Kratzer's ordering as a NormalityOrder.

Connects Kratzer's ordering source to the default reasoning infrastructure, enabling optimal, refine, respects, and CR1–CR4 for modal semantics.

Equations

• Semantics.Modality.Kratzer.kratzerNormality A = (Semantics.Modality.Kratzer.worldOrdering A).toNormalityOrder

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

Backwards-compatible alias.

Equations

• Semantics.Modality.Kratzer.kratzerPreorder A = { le := (Semantics.Modality.Kratzer.kratzerNormality A).le, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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.