The criteria-derived preorder

Preorder.ofCriteria sat criteria orders a carrier by inclusion of satisfied criteria: a ≤ b iff every criterion in criteria that b satisfies, a satisfies too. This is [Kra81]'s ordering-source construction at full generality — the pullback of ⊇ along the satisfied-set map (ofCriteria_le_iff_subset; Core.Order.PullbackPreorder is the bundled, decidability-carrying form of the same pattern).

One construction, several instantiations across the library:

• Semantics.Modality.Kratzer.kratzerPreorder / atLeastAsGoodAs — worlds ordered by an ordering source.
• Core.Order.NormalityOrder.fromProps — the same order repackaged as a NormalityOrder for the default-reasoning infrastructure.
• Semantics.Attitudes.Desire.worldAtLeastAsGood — worlds ordered by desires (via atLeastAsGoodAs).
• Core.Order.SatisfactionOrdering.ofCriteria — the bundled Bool-valued/List-criteria specialization with decidable ≤ (SatisfactionOrdering.le_iff_ofCriteria).

@[reducible]

def Preorder.ofCriteria {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) : Preorder α

The criteria-derived preorder: a ≤ b iff every criterion in criteria that b satisfies, a satisfies too — [Kra81]'s ordering-source construction {c ∈ A : sat b c} ⊆ {c ∈ A : sat a c} at full generality.

Equations

• Preorder.ofCriteria sat criteria = { le := fun (a b : α) => ∀ (c : C), c ∈ criteria → sat b c → sat a c, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Preorder.ofCriteria_le_iff {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : a ≤ b ↔ ∀ (c : C), c ∈ criteria → sat b c → sat a c

Unfolding lemma for the criteria-derived order. Not @[simp] — unfolding is opt-in.

theorem Preorder.ofCriteria_le_iff_subset {α : Type u_1} {C : Type u_2} (sat : α → C → Prop) (criteria : Set C) (a b : α) : a ≤ b ↔ {c : C | c ∈ criteria ∧ sat b c} ⊆ {c : C | c ∈ criteria ∧ sat a c}

The criteria-derived order is the pullback of ⊇ along the satisfied-set map a ↦ {c ∈ criteria | sat a c} — the Core.Order.PullbackPreorder pattern with target (Set C)ᵒᵈ.

theorem Preorder.ofCriteria_le_of_subset {α : Type u_1} {C : Type u_2} {sat : α → C → Prop} {criteria criteria' : Set C} (hsub : criteria ⊆ criteria') {a b : α} (h : a ≤ b) : a ≤ b

Fewer criteria, coarser order: dominance over a criteria set transfers to any subset. The general form of "adding a proposition to the ordering source refines it".