World Preorder Induced by Maximal Preferences

[CL16] [Kra81] [Por18]

The world-side preorder w ≤ v iff w satisfies every maximal preference that v satisfies. The Kratzer-style derivation of a world ordering from an ordering source, applied to maxElts. Used by [CL16] (88): g_epA(w) = max[EP(Ad, w)].

The bridge to a List-valued Semantics.Modality.Kratzer.OrderingSource requires either a finiteness witness or a non-constructive enumeration; that bridge lives downstream.

def Core.Order.PreferenceStructure.maxInducedLe {W : Type u} (P : PreferenceStructure W) : W → W → Prop

The world-level preorder induced by maximal preferences: maxInducedLe w v iff w verifies every maximal preference that v verifies.

Equations

• P.maxInducedLe w v = ∀ p ∈ P.maxElts, v ∈ p → w ∈ p

theorem Core.Order.PreferenceStructure.maxInducedLe_refl {W : Type u} (P : PreferenceStructure W) (w : W) : P.maxInducedLe w w

theorem Core.Order.PreferenceStructure.maxInducedLe_trans {W : Type u} (P : PreferenceStructure W) {w v u : W} (hwv : P.maxInducedLe w v) (hvu : P.maxInducedLe v u) : P.maxInducedLe w u