noncomputable def Semantics.Modality.Kratzer.satisfiedPropositions {W : Type u_1} (A : List (W → Prop)) (w : W) : List (W → Prop)

The list of propositions from A that world w satisfies.

This is {p ∈ A : w ∈ p} in Kratzer's notation. We use classical decidability to filter the list, so this definition is noncomputable — downstream uses are about lengths/membership, not evaluation.

Equations

• Semantics.Modality.Kratzer.satisfiedPropositions A w = List.filter (fun (p : W → Prop) => decide (p w)) A

def Semantics.Modality.Kratzer.atLeastAsGoodAs {W : Type u_1} (A : List (W → Prop)) (w z : W) : Prop

Kratzer's ordering relation: w ≤_A z

@cite{kratzer-1981}: w ≤_A z iff every ideal proposition p ∈ A that holds at z also holds at w. Intuitively: w is at least as good as z (w.r.t. ideal A) iff every ideal proposition that z satisfies, w also satisfies.

UNVERIFIED page reference (p. 39 quoted in earlier version, not checked against the original).

Equations

• (w ≤[A] z) = ∀ p ∈ A, p z → p w

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

Kratzer's ordering relation: w ≤_A z

@cite{kratzer-1981}: w ≤_A z iff every ideal proposition p ∈ A that holds at z also holds at w. Intuitively: w is at least as good as z (w.r.t. ideal A) iff every ideal proposition that z satisfies, w also satisfies.

UNVERIFIED page reference (p. 39 quoted in earlier version, not checked against the original).

Equations

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

def Semantics.Modality.Kratzer.strictlyBetter {W : Type u_1} (A : List (W → Prop)) (w z : W) : Prop

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

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

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

theorem Semantics.Modality.Kratzer.ordering_reflexive {W : Type u_1} (A : List (W → Prop)) (w : W) : w ≤[A] w

Reflexivity.

theorem Semantics.Modality.Kratzer.ordering_transitive {W : Type u_1} (A : List (W → Prop)) (u v w : W) (huv : u ≤[A] v) (hvw : v ≤[A] w) : u ≤[A] w

Transitivity.

@[reducible]

def Semantics.Modality.Kratzer.kratzerPreorder {W : Type u_1} (A : List (W → Prop)) : Preorder W

Kratzer's world ordering as a Preorder on worlds.

The induced order is ≤[A]. Used by Phillips-Brown desire semantics and other consumers via letI := kratzerPreorder A.

Equations

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

def Semantics.Modality.Kratzer.kratzerNormality {W : Type u_1} (A : List (W → Prop)) : Core.Order.NormalityOrder W

Kratzer's ordering as a NormalityOrder: connects to default reasoning infrastructure (optimal, refine, respects, CR1–CR4).

Equations

• Semantics.Modality.Kratzer.kratzerNormality A = { le := Semantics.Modality.Kratzer.atLeastAsGoodAs A, le_refl := ⋯, le_trans := ⋯ }

def Semantics.Modality.Kratzer.orderingEquiv {W : Type u_1} (A : List (W → Prop)) (w z : W) : Prop

Equivalence under the ordering.

Equations

• Semantics.Modality.Kratzer.orderingEquiv A w z = ((w ≤[A] z) ∧ z ≤[A] w)

theorem Semantics.Modality.Kratzer.orderingEquiv_refl {W : Type u_1} (A : List (W → Prop)) (w : W) : orderingEquiv A w w

theorem Semantics.Modality.Kratzer.orderingEquiv_symm {W : Type u_1} (A : List (W → Prop)) (w z : W) (h : orderingEquiv A w z) : orderingEquiv A z w

theorem Semantics.Modality.Kratzer.orderingEquiv_trans {W : Type u_1} (A : List (W → Prop)) (u v w : W) (huv : orderingEquiv A u v) (hvw : orderingEquiv A v w) : orderingEquiv A u w

theorem Semantics.Modality.Kratzer.empty_ordering_all_equivalent {W : Type u_1} (w z : W) : (w ≤[[]] z) ∧ z ≤[[]] w

Theorem 2: Empty ordering makes all worlds equivalent.

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

Proof: There are no propositions in [] to satisfy, so the universal is vacuous.

theorem Semantics.Modality.Kratzer.empty_ordering_trivial {W : Type u_1} (w z : W) : w ≤ z

theorem Semantics.Modality.Kratzer.empty_ordering_universal_equiv {W : Type u_1} (w z : W) : orderingEquiv [] w z

def Semantics.Modality.Kratzer.accessibleWorlds {W : Type u_1} (f : ModalBase W) (w : W) : Set W

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 = Core.Logic.Intensional.Premise.propIntersection (f w)

def Semantics.Modality.Kratzer.accessibleFrom {W : Type u_1} (f : ModalBase W) (w w' : W) : Prop

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

Equations

• Semantics.Modality.Kratzer.accessibleFrom f w w' = ∀ p ∈ f w, p w'

def Semantics.Modality.Kratzer.bestWorlds {W : Type u_1} (f : ModalBase W) (g : OrderingSource W) (w : W) : Set W

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

• Semantics.Modality.Kratzer.bestWorlds f g w = {w' : W | w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f w ∧ ∀ w'' ∈ Semantics.Modality.Kratzer.accessibleWorlds f w, w' ≤[g w] w''}

theorem Semantics.Modality.Kratzer.empty_ordering_simple {W : Type u_1} (f : ModalBase W) (w : W) : bestWorlds f (fun (x : W) => []) 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 {W : Type u_1} (f : ModalBase W) (w : W) : bestWorlds f emptyBackground w = accessibleWorlds f w

Variant of empty_ordering_simple matching emptyBackground by name.

def Semantics.Modality.Kratzer.bestAmong {W : Type u_1} (worlds : Set W) (ordering : List (W → Prop)) : Set W

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 set. This is needed when the domain has already been restricted (e.g., by promoted priorities in @cite{rubinstein-2014}'s favored worlds).

Equations

• Semantics.Modality.Kratzer.bestAmong worlds ordering = {w' : W | w' ∈ worlds ∧ ∀ w'' ∈ worlds, w' ≤[ordering] w''}

theorem Semantics.Modality.Kratzer.bestAmong_empty {W : Type u_1} (worlds : Set W) : bestAmong worlds [] = worlds

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

theorem Semantics.Modality.Kratzer.bestAmong_sub {W : Type u_1} (worlds : Set W) (ordering : List (W → Prop)) : bestAmong worlds ordering ⊆ worlds

bestAmong is a subset of the input worlds.

theorem Semantics.Modality.Kratzer.bestAmong_superset {W : Type u_1} {sub sup : Set W} {ordering : List (W → Prop)} {w' : W} (hSub : sub ⊆ sup) (hBest : w' ∈ bestAmong sup ordering) (hMem : w' ∈ sub) : w' ∈ bestAmong sub ordering

Best worlds in a superset that belong to a subset are best in the subset.

If w' beats every world in a larger set, it certainly beats every world in any subset. This is the key lemma for showing that star-revision (domain widening) preserves strong necessity.