Satisfaction Ordering

Satisfaction-based orderings: ordering elements by how many criteria they satisfy. Used by Kratzer modal semantics (worlds by propositions) and Phillips-Brown desire semantics (propositions by desires).

The induced ordering is a NormalityOrder — connecting Kratzer's ordering source semantics to the default reasoning infrastructure in Core/Order/.

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

Satisfaction-based ordering on type α by subset inclusion of satisfied criteria.

• satisfies : α → Criterion → Bool
• criteria : List Criterion

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

Equations

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

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

Weak ordering: a ≥ a' iff a satisfies everything a' satisfies.

Equations

• o.atLeastAsGood a a' = (o.satisfiedBy a').all (o.satisfies a)

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

Strict ordering: a > a' iff a ≥ a' but not a' ≥ a.

Equations

• o.strictlyBetter a a' = (o.atLeastAsGood a a' && !o.atLeastAsGood a' a)

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

Equivalence: a and a' satisfy the same criteria.

Equations

• o.equivalent a a' = (o.atLeastAsGood a a' && o.atLeastAsGood a' a)

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

Best elements: those at least as good as all others.

Equations

• o.best candidates = List.filter (fun (a : α) => candidates.all fun (a' : α) => o.atLeastAsGood a a') candidates

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

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

theorem Core.SatisfactionOrdering.SatisfactionOrdering.empty_criteria_all_equivalent {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (h : o.criteria = []) (a a' : α) : o.equivalent a a' = true

theorem Core.SatisfactionOrdering.SatisfactionOrdering.empty_criteria_all_best {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (h : o.criteria = []) (candidates : List α) : o.best candidates = candidates

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

Prop-valued ordering: a ≥ a' iff atLeastAsGood a a' = true.

Equations

• o.le a a' = (o.atLeastAsGood a a' = true)

def Core.SatisfactionOrdering.SatisfactionOrdering.toNormalityOrder {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) : Order.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 := o.le, le_refl := ⋯, le_trans := ⋯ }

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

Equations

• o.equiv a a' = (o.le a a' ∧ o.le a' a)

theorem Core.SatisfactionOrdering.SatisfactionOrdering.equiv_refl {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a : α) : o.equiv a a

theorem Core.SatisfactionOrdering.SatisfactionOrdering.equiv_symm {α : Type u_1} {Criterion : Type u_2} (o : SatisfactionOrdering α Criterion) (a a' : α) (h : o.equiv a a') : o.equiv a' a

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