Satisfaction Ordering

A SatisfactionOrdering α Criterion bundles a Preorder α with the data that constructs it: a satisfies : α → Criterion → Bool relation and a criteria : List Criterion. The induced ≤ is subset inclusion of satisfied criteria.

Used by Kratzer modal semantics (worlds by ordering source) and Phillips-Brown desire semantics (propositions by desires).

Design

The structure extends Preorder α, so all of mathlib's order vocabulary (≤, <, IsMax, Maximal, etc.) is available on α once o.toPreorder is opened as an instance (e.g. letI := o.toPreorder). The smart constructor ofCriteria builds the canonical satisfaction-based preorder from a satisfies relation and a criteria list. A decLE field carries decidability of ≤, automatic for the ofCriteria construction.

atLeastAsGood, equivalent, strictlyBetter are kept as @[reducible] aliases for o.le, AntisymmRel, and o.lt so call sites can use domain-friendly names.

structure Core.Order.SatisfactionOrdering (α : Type u_1) (Criterion : Type u_2) extends Preorder α : Type (max u_1 u_2)

Satisfaction-based preorder on α by subset inclusion of satisfied criteria. Extends Preorder α so downstream code gets ≤, <, and mathlib's order vocabulary; retains satisfies/criteria so the construction data is recoverable. decLE carries decidability of ≤.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• satisfies : α → Criterion → Bool
• criteria : List Criterion
• decLE (a a' : α) : Decidable (a ≤ a')

@[implicit_reducible]

instance Core.Order.SatisfactionOrdering.instDecidableLe {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a a' : α) : Decidable (a ≤ a')

Equations

• o.instDecidableLe a a' = o.decLE a a'

def Core.Order.SatisfactionOrdering.satisfiedBy {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a : α) : List Criterion

The list of criteria from o.criteria that a satisfies.

Equations

• o.satisfiedBy a = List.filter (o.satisfies a) o.criteria

def Core.Order.SatisfactionOrdering.ofCriteria {α : Type u_1} {Criterion : Type u_2} (satisfies : α → Criterion → Bool) (criteria : List Criterion) : SatisfactionOrdering α Criterion

Canonical constructor: build a SatisfactionOrdering from a satisfaction relation and a criteria list. The induced ≤ is "every criterion a' satisfies, a also satisfies".

Equations

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

Domain-friendly aliases

These let study files use names that match the source literature ("at least as good as", "strictly better", "equivalent") while staying definitionally equal to the underlying preorder.

@[reducible]

def Core.Order.SatisfactionOrdering.atLeastAsGood {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a a' : α) : Prop

Readability alias for a ≤ a' under o.

Equations

• o.atLeastAsGood a a' = (a ≤ a')

@[reducible]

def Core.Order.SatisfactionOrdering.strictlyBetter {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a a' : α) : Prop

Readability alias for a < a' under o.

Equations

• o.strictlyBetter a a' = (a ≤ a' ∧ ¬a' ≤ a)

@[reducible]

def Core.Order.SatisfactionOrdering.equivalent {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a a' : α) : Prop

a and a' satisfy the same criteria.

Equations

• o.equivalent a a' = (a ≤ a' ∧ a' ≤ a)

Reflexivity, transitivity, symmetry

Direct wrappers over the underlying Preorder methods, exposed under the domain-friendly names.

theorem Core.Order.SatisfactionOrdering.atLeastAsGood_refl {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a : α) : o.atLeastAsGood a a

theorem Core.Order.SatisfactionOrdering.atLeastAsGood_trans {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) {a b c : α} (hab : o.atLeastAsGood a b) (hbc : o.atLeastAsGood b c) : o.atLeastAsGood a c

theorem Core.Order.SatisfactionOrdering.equivalent_refl {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a : α) : o.equivalent a a

theorem Core.Order.SatisfactionOrdering.equivalent_symm {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) {a a' : α} (h : o.equivalent a a') : o.equivalent a' a

theorem Core.Order.SatisfactionOrdering.equivalent_trans {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) {a b c : α} (hab : o.equivalent a b) (hbc : o.equivalent b c) : o.equivalent a c

NormalityOrder projection

def Core.Order.SatisfactionOrdering.toNormalityOrder {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) : NormalityOrder α

The induced NormalityOrder: connects satisfaction-based orderings (Kratzer modal semantics, Phillips-Brown desire) to the default reasoning infrastructure (optimal, refine, respects, CR1–CR4).

Equations

• o.toNormalityOrder = { le := LE.le, le_refl := ⋯, le_trans := ⋯ }

Maxima and undominated elements

def Core.Order.SatisfactionOrdering.best {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (candidates : List α) : List α

Best elements: those at-least-as-good as every candidate. (Greatest elements; when the order is partial, see undominated for maximal elements.)

Equations

• o.best candidates = List.filter (fun (a : α) => decide (∀ (a' : α), a' ∈ candidates → a ≤ a')) candidates

def Core.Order.SatisfactionOrdering.undominated {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (candidates : List α) : List α

Undominated elements: those not strictly dominated by any candidate. The Pareto frontier — equivalent to best when the ordering is total, but more general for partial orders where incomparable elements can both be undominated without either dominating all others.

Equations

• o.undominated candidates = List.filter (fun (a : α) => decide ¬∃ (a' : α), a' ∈ candidates ∧ o.strictlyBetter a' a) candidates

@[simp]

theorem Core.Order.SatisfactionOrdering.mem_best_iff {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (candidates : List α) (a : α) : a ∈ o.best candidates ↔ a ∈ candidates ∧ ∀ (a' : α), a' ∈ candidates → a ≤ a'

Membership characterization for best.

@[simp]

theorem Core.Order.SatisfactionOrdering.mem_undominated_iff {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (candidates : List α) (a : α) : a ∈ o.undominated candidates ↔ a ∈ candidates ∧ ¬∃ (a' : α), a' ∈ candidates ∧ o.strictlyBetter a' a

Membership characterization for undominated.

theorem Core.Order.SatisfactionOrdering.best_sub_undominated {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (candidates : List α) {a : α} (h : a ∈ o.best candidates) : a ∈ o.undominated candidates

Every best element is undominated.

Empty-criteria boundary

When constructed via ofCriteria with an empty criteria list, the induced preorder is total: every pair is ≤.

theorem Core.Order.SatisfactionOrdering.ofCriteria_empty_le {α : Type u_1} {Criterion : Type u_2} (satisfies : α → Criterion → Bool) (a a' : α) : a ≤ a'

theorem Core.Order.SatisfactionOrdering.ofCriteria_empty_equivalent {α : Type u_1} {Criterion : Type u_2} (satisfies : α → Criterion → Bool) (a a' : α) : (ofCriteria satisfies []).equivalent a a'

theorem Core.Order.SatisfactionOrdering.ofCriteria_empty_undominated {α : Type u_1} {Criterion : Type u_2} (satisfies : α → Criterion → Bool) (candidates : List α) : (ofCriteria satisfies []).undominated candidates = candidates

theorem Core.Order.SatisfactionOrdering.ofCriteria_empty_best {α : Type u_1} {Criterion : Type u_2} (satisfies : α → Criterion → Bool) (candidates : List α) : (ofCriteria satisfies []).best candidates = candidates