The premise primitives live in Intensional.Premise; re-export them under Modality.Kratzer so the historical Kratzer.foo call style continues to work. The conversational-background primitives (ConvBackground, ModalBase, …) are defined directly in this namespace by ConversationalBackground.lean.

noncomputable def 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

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

@[reducible]

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

Kratzer's world ordering as a Preorder on worlds — the criteria-derived preorder (Preorder.ofCriteria) with the ordering source A as criteria set and truth-at-a-world as satisfaction. The induced order is ≤[A]. Used by Phillips-Brown desire semantics and other consumers via letI := kratzerPreorder A.

Equations

• Modality.Kratzer.kratzerPreorder A = Preorder.ofCriteria (fun (w : W) (p : W → Prop) => p w) {p : W → Prop | p ∈ A}

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

Kratzer's ordering relation: w ≤_A z — the le of kratzerPreorder.

[Kra81]: 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) = (w ≤ z)

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

Kratzer's ordering relation: w ≤_A z — the le of kratzerPreorder.

[Kra81]: 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.

theorem Modality.Kratzer.atLeastAsGoodAs_iff {W : Type u_1} (A : List (W → Prop)) (w z : W) : (w ≤[A] z) ↔ ∀ p ∈ A, p z → p w

Unfolding lemma: the ordering in its pointwise form. Definitional.

def 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 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 Modality.Kratzer.ordering_reflexive {W : Type u_1} (A : List (W → Prop)) (w : W) : w ≤[A] w

Reflexivity.

theorem 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.

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

Kratzer's ordering as a normality Preorder — definitionally Normality.fromProps (the same Preorder.ofCriteria order); connects to default-reasoning infrastructure (Normality.optimal, refine, respects, CR1–CR4).

Equations

• Modality.Kratzer.kratzerNormality A = Core.Order.Normality.fromProps A

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

Equivalence under the ordering.

Equations

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

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

theorem 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 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 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 Modality.Kratzer.empty_ordering_trivial {W : Type u_1} (w z : W) : w ≤ z

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

def 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

• Modality.Kratzer.accessibleWorlds f w = Intensional.Premise.propIntersection (f w)

theorem Modality.Kratzer.accessibleWorlds_anti {W : Type u_1} {f f' : ModalBase W} {w : W} (h : f w ⊆ f' w) : accessibleWorlds f' w ⊆ accessibleWorlds f w

Growing the modal base can only shrink the accessible worlds.

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

The best accessible worlds: those no accessible world strictly betters. [Kra81]'s official necessity is the limit-free humanNecessity; it quantifies over exactly this set under the Limit Assumption (humanNecessity_iff_necessity). Her practical-inference tripartition (pp. 66-67) is non-connected by construction — the ordering "is not necessarily connected. Technically, ≤_A is a partial preorder" ([Kra12], her note 12 chapter) — so the stronger dominance form (at least as good as every accessible world) would be empty there; minimality is the faithful reading.

Equations

• Modality.Kratzer.bestWorlds f g w = Core.Order.Normality.optimal (Modality.Kratzer.kratzerNormality (g w)) (Modality.Kratzer.accessibleWorlds f w)

theorem 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 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.

theorem Modality.Kratzer.isRealistic_iff_mem_accessible {W : Type u_1} (f : ModalBase W) : isRealistic f ↔ ∀ (w : W), w ∈ accessibleWorlds f w

A modal base is realistic iff every world is accessible from itself.

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

The best worlds among a given set: members no other member strictly betters. Unlike bestWorlds, which computes the domain from a modal base, bestAmong takes a precomputed world set — the form needed when the domain is already restricted, by promoted priorities in [Rub14]'s favored worlds or by a primary ordering in the lexicographic refinement of [Kra81]'s Conclusion.

Equations

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

theorem 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 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 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: unbettered among more competitors, unbettered among fewer. The key lemma for showing that star-revision (domain widening) preserves strong necessity.