Normality orderings (default reasoning over preorders)

[KLM90] [Vel96] [Rud25a] [Kra81]

A normality ordering is just a Preorder on worlds: p.le w v means w is at least as normal as v. There is no bespoke structure here — the order is mathlib's Preorder, so the entire order API (<, Minimal, order-duals, monotone maps) is available, and the default-reasoning operations are thin definitions over it:

• optimal p d — the most-normal worlds in d — is mathlib's Minimal.
• connected p — totality — is ∀ w v, p.le w v ∨ p.le v w.
• total = ⊤ — the all-equal order — is the top of CompleteLattice (Preorder W).
• refine p φ = p ⊓ crit φ — [Vel96]'s promote-φ update — is meet with the criterion preorder crit φ (w ≤ v ↔ (φ v → φ w)). The whole refinement calculus (commutativity, idempotence, the total order as unit) is therefore the meet-semilattice laws (inf_right_comm, inf_right_idem, inf_top_eq).
• fromProps — [Kra81]'s ordering-source order — is Preorder.ofCriteria.

This replaces the former hand-rolled NormalityOrder structure (a field-for-field reimplementation of Preorder).

Optimality, totality, the total order

def Core.Order.Normality.optimal {W : Type u_1} (p : Preorder W) (d : Set W) : Set W

The optimal (most normal) worlds in a domain d: mathlib's Minimal for the membership predicate, under the preorder p.

Equations

• Core.Order.Normality.optimal p d = {w : W | Minimal (fun (x : W) => x ∈ d) w}

theorem Core.Order.Normality.mem_optimal {W : Type u_1} {p : Preorder W} {d : Set W} {w : W} : w ∈ optimal p d ↔ w ∈ d ∧ ∀ ⦃v : W⦄, v ∈ d → v ≤ w → w ≤ v

theorem Core.Order.Normality.optimal_subset {W : Type u_1} (p : Preorder W) (d : Set W) : optimal p d ⊆ d

def Core.Order.Normality.connected {W : Type u_1} (p : Preorder W) : Prop

A preorder is connected (total) if every two worlds are comparable.

Equations

• Core.Order.Normality.connected p = ∀ (w v : W), w ≤ v ∨ v ≤ w

@[reducible, inline]

abbrev Core.Order.Normality.total {W : Type u_1} : Preorder W

The total normality order: all worlds equally normal — the top of the lattice of preorders.

Equations

• Core.Order.Normality.total = ⊤

theorem Core.Order.Normality.total_connected {W : Type u_1} : connected total

theorem Core.Order.Normality.total_all_optimal {W : Type u_1} (d : Set W) : optimal total d = d

Refinement as meet with a criterion preorder

@[reducible]

def Core.Order.Normality.crit {W : Type u_1} (φ : W → Prop) : Preorder W

The criterion preorder for a property φ: w ≤ v ↔ (φ v → φ w). Defined directly (not via Preorder.ofCriteria {φ}) so that (refine p φ).le reduces definitionally to p.le … ∧ (φ … → φ …).

Equations

• Core.Order.Normality.crit φ = Preorder.ofLE (fun (w v : W) => φ v → φ w) ⋯ ⋯

theorem Core.Order.Normality.crit_le {W : Type u_1} {φ : W → Prop} {w v : W} : w ≤ v ↔ φ v → φ w

@[reducible]

def Core.Order.Normality.refine {W : Type u_1} (p : Preorder W) (φ : W → Prop) : Preorder W

Refinement ([Vel96]): promote φ-worlds. refine p φ is the meet of p with the criterion preorder for φ, so (refine p φ).le w v ↔ p.le w v ∧ (φ v → φ w).

Equations

• Core.Order.Normality.refine p φ = p ⊓ Core.Order.Normality.crit φ

theorem Core.Order.Normality.refine_le {W : Type u_1} {p : Preorder W} {φ : W → Prop} {w v : W} : w ≤ v ↔ w ≤ v ∧ (φ v → φ w)

theorem Core.Order.Normality.refine_le_imp {W : Type u_1} {p : Preorder W} {φ : W → Prop} {w v : W} (h : w ≤ v) : w ≤ v

theorem Core.Order.Normality.refine_separates {W : Type u_1} (p : Preorder W) (φ : W → Prop) {w v : W} (hv : φ v) (hw : ¬φ w) : ¬w ≤ v

After refinement by φ, a non-φ-world cannot be as normal as a φ-world.

Respect and persistence

def Core.Order.Normality.respects {W : Type u_1} (p : Preorder W) (φ : W → Prop) : Prop

An ordering respects φ if it already promotes φ-worlds.

Equations

• Core.Order.Normality.respects p φ = ∀ (w v : W), w ≤ v → φ v → φ w

theorem Core.Order.Normality.refine_respects {W : Type u_1} (p : Preorder W) (φ : W → Prop) : respects (refine p φ) φ

theorem Core.Order.Normality.refine_preserves_respects {W : Type u_1} (p : Preorder W) (φ ψ : W → Prop) (h : respects p φ) : respects (refine p ψ) φ

Persistence: respecting φ survives further refinement.

theorem Core.Order.Normality.respects_refine_iff {W : Type u_1} (p : Preorder W) (φ : W → Prop) (h : respects p φ) {w v : W} : w ≤ v ↔ w ≤ v

theorem Core.Order.Normality.refine_idempotent {W : Type u_1} (p : Preorder W) (φ : W → Prop) : refine (refine p φ) φ = refine p φ

Idempotency: refining by φ twice is refining once (inf_right_idem).

theorem Core.Order.Normality.refine_comm {W : Type u_1} (p : Preorder W) (φ ψ : W → Prop) : refine (refine p φ) ψ = refine (refine p ψ) φ

Commutativity: refinement order is immaterial (inf_right_comm).

theorem Core.Order.Normality.crit_const_top {W : Type u_1} (b : Prop) : (crit fun (x : W) => b) = ⊤

theorem Core.Order.Normality.refine_univ {W : Type u_1} (p : Preorder W) : (refine p fun (x : W) => True) = p

Refining by the universal property is the identity (inf_top_eq).

theorem Core.Order.Normality.refine_empty {W : Type u_1} (p : Preorder W) : (refine p fun (x : W) => False) = p

theorem Core.Order.Normality.refine_of_respects {W : Type u_1} (p : Preorder W) (φ : W → Prop) (h : respects p φ) : refine p φ = p

If an ordering respects φ, refining by φ changes nothing.

theorem Core.Order.Normality.respects_no_domination {W : Type u_1} (p : Preorder W) (φ : W → Prop) (hresp : respects p φ) {w v : W} (hv : φ v) (hw : ¬φ w) : ¬w ≤ v

Connectedness and optimality

theorem Core.Order.Normality.optimal_of_respects_connected {W : Type u_1} (p : Preorder W) (φ : W → Prop) (d : Set W) (hresp : respects p φ) (hconn : connected p) (hex : ∃ w ∈ d, φ w) : optimal p d ⊆ {w : W | w ∈ d ∧ φ w}

theorem Core.Order.Normality.refine_total_optimal {W : Type u_1} (φ : W → Prop) (d : Set W) (hex : ∃ w ∈ d, φ w) : optimal (refine total φ) d = {w : W | w ∈ d ∧ φ w}

Refinement makes φ-worlds optimal: from the total order, refining by φ makes the optimal worlds in d exactly the φ-worlds in d.

theorem Core.Order.Normality.optimal_refine_of_mem {W : Type u_1} (p : Preorder W) (φ : W → Prop) (d : Set W) {w : W} (hopt : w ∈ optimal p d) (hφ : φ w) : w ∈ optimal (refine p φ) d

theorem Core.Order.Normality.optimal_refine_nonempty {W : Type u_1} (p : Preorder W) (φ : W → Prop) (d : Set W) (hex : ∃ w ∈ optimal p d, φ w) : (optimal (refine p φ) d).Nonempty

Construction from propositions ([Kra81])

@[reducible]

def Core.Order.Normality.fromProps {W : Type u_1} (props : List (W → Prop)) : Preorder W

Construct a normality ordering from a list of propositions: w ≤ v iff every proposition satisfied by v is satisfied by w. This is Preorder.ofCriteria with the ordering source as criteria.

Equations

• Core.Order.Normality.fromProps props = Preorder.ofCriteria (fun (w : W) (p : W → Prop) => p w) {p : W → Prop | p ∈ props}

theorem Core.Order.Normality.fromProps_nil {W : Type u_1} {w v : W} : w ≤ v

theorem Core.Order.Normality.fromProps_cons_le {W : Type u_1} (p : W → Prop) (ps : List (W → Prop)) {w v : W} (h : w ≤ v) : w ≤ v

theorem Core.Order.Normality.refine_total_connected {W : Type u_1} (φ : W → Prop) : connected (refine total φ)

Darwiche-Pearl representation conditions

[DP97]: conditions on how a total preorder may change under revision by μ. prior/post are the orderings before/after revision.

@[reducible]

def Core.Order.Normality.satisfies_CR1 {W : Type u_1} (prior post : Preorder W) (μ : W → Bool) : Prop

CR1: the ordering among μ-worlds is preserved.

Equations

• Core.Order.Normality.satisfies_CR1 prior post μ = ∀ (w v : W), μ w = true → μ v = true → (w ≤ v ↔ w ≤ v)

@[reducible]

def Core.Order.Normality.satisfies_CR2 {W : Type u_1} (prior post : Preorder W) (μ : W → Bool) : Prop

CR2: the ordering among ¬μ-worlds is preserved.

Equations

• Core.Order.Normality.satisfies_CR2 prior post μ = ∀ (w v : W), μ w = false → μ v = false → (w ≤ v ↔ w ≤ v)

@[reducible]

def Core.Order.Normality.satisfies_CR3 {W : Type u_1} (prior post : Preorder W) (μ : W → Bool) : Prop

CR3: a μ-world strictly below a ¬μ-world stays strictly below. The strict order is spelled le … ∧ ¬ le … (definitionally <) so the relation is decidable on finite world sets.

Equations

• Core.Order.Normality.satisfies_CR3 prior post μ = ∀ (w v : W), μ w = true → μ v = false → w ≤ v ∧ ¬v ≤ w → w ≤ v ∧ ¬v ≤ w

@[reducible]

def Core.Order.Normality.satisfies_CR4 {W : Type u_1} (prior post : Preorder W) (μ : W → Bool) : Prop

CR4: a μ-world ≤ a ¬μ-world stays ≤.

Equations

• Core.Order.Normality.satisfies_CR4 prior post μ = ∀ (w v : W), μ w = true → μ v = false → w ≤ v → w ≤ v