Normality Orderings

@cite{kraus-magidor-1990} @cite{veltman-1996} @cite{rudin-2025}

A normality ordering is a preorder on worlds encoding relative normalcy. This structure appears in four places across formal semantics:

1. @cite{kratzer-1981}: ordering sources induce normality orderings for modal semantics (Theories/Semantics/Modality/Kratzer.lean)
2. @cite{kraus-magidor-1990}: plausibility orderings interpret default consequence, System P (Core/Logic/BeliefRevision.lean)
3. @cite{veltman-1996}: expectation patterns are normality orderings that get dynamically refined (Theories/Semantics/Dynamic/UpdateSemantics/)
4. @cite{rudin-2025}: ordering-source updates for epistemic modals (Theories/Semantics/Dynamic/Epistemic/)

This module extracts the common mathematical core. The PlausibilityOrder in BeliefRevision.lean adds a smoothness condition (every satisfiable proposition has minimal elements); for finite types smoothness is automatic, and NormalityOrder captures the shared preorder structure without it.

Key definitions

• NormalityOrder W: preorder on worlds (reflexive, transitive)
• optimal: most normal worlds in a domain
• refine: promote φ-worlds — @cite{veltman-1996}'s key operation
• connected: every two worlds are comparable (totality)
• fromProps: construct from ordering source — @cite{kratzer-1981}'s pattern
• respects / persistence: defaults survive further updates

structure Core.Order.NormalityOrder (W : Type u_1) : Type u_1

A normality ordering: a preorder on worlds. le w v means w is at least as normal as v.

• le : W → W → Prop
• le_refl (w : W) : self.le w w
• le_trans (u v w : W) : self.le u v → self.le v w → self.le u w

theorem Core.Order.NormalityOrder.ext {W : Type u_1} {a b : NormalityOrder W} (h : ∀ (w v : W), a.le w v ↔ b.le w v) : a = b

Extensionality: two normality orderings are equal iff they agree on all pairs. Uses propext and funext.

theorem Core.Order.NormalityOrder.ext_iff {W : Type u_1} {a b : NormalityOrder W} : a = b ↔ ∀ (w v : W), a.le w v ↔ b.le w v

def Core.Order.NormalityOrder.connected {W : Type u_1} (no : NormalityOrder W) : Prop

An ordering is connected (total) if every two worlds are comparable: for all w, v, either w ≤ v or v ≤ w.

Equations

• no.connected = ∀ (w v : W), no.le w v ∨ no.le v w

def Core.Order.NormalityOrder.total {W : Type u_1} : NormalityOrder W

The total ordering: all worlds equally normal. This is the initial state before any defaults have been processed.

Equations

• Core.Order.NormalityOrder.total = { le := fun (x x_1 : W) => True, le_refl := ⋯, le_trans := ⋯ }

@[reducible]

def Core.Order.NormalityOrder.slt {W : Type u_1} (no : NormalityOrder W) (w v : W) : Prop

Strict normality: w is strictly more normal than v.

Equations

• no.slt w v = (no.le w v ∧ ¬no.le v w)

def Core.Order.NormalityOrder.optimal {W : Type u_1} (no : NormalityOrder W) (d : Set W) : Set W

Optimal (most normal) worlds in a domain: those with no strictly more normal world in the domain.

Equivalent to PlausibilityOrder.minimal in BeliefRevision.lean and to @cite{veltman-1996}'s opt_ε(σ).

Equations

• no.optimal d = {w : W | w ∈ d ∧ ∀ (v : W), v ∈ d → no.le v w → no.le w v}

theorem Core.Order.NormalityOrder.optimal_subset {W : Type u_1} (no : NormalityOrder W) (d : Set W) : no.optimal d ⊆ d

Optimal worlds are in the domain.

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

The total ordering is connected.

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

Under the total ordering, every world in the domain is optimal.

def Core.Order.NormalityOrder.refine {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) : NormalityOrder W

Refinement: promote φ-worlds in the normality ordering.

After refine no φ, a non-φ-world can no longer be as normal as a φ-world: w ≤' v iff (w ≤ v) ∧ (φ v → φ w).

This is @cite{veltman-1996}'s key operation. "Normally φ" updates the expectation pattern by intersecting with {⟨w,v⟩ : φ v → φ w}.

Equations

• no.refine φ = { le := fun (w v : W) => no.le w v ∧ (φ v → φ w), le_refl := ⋯, le_trans := ⋯ }

theorem Core.Order.NormalityOrder.refine_le_imp {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) {w v : W} (h : (no.refine φ).le w v) : no.le w v

Refinement strengthens: the refined ordering implies the original.

theorem Core.Order.NormalityOrder.refine_separates {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) {w v : W} (hv : φ v) (hw : ¬φ w) : ¬(no.refine φ).le w v

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

theorem Core.Order.NormalityOrder.refine_promotes {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) {w v : W} (hv : φ v) (hw : ¬φ w) (hle : no.le v w) : (no.refine φ).slt v w

After refinement, if v was ≤ w and v is a φ-world while w is not, then v strictly dominates w.

def Core.Order.NormalityOrder.respects {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) : Prop

An ordering respects φ if it already promotes φ-worlds: whenever w ≤ v and v satisfies φ, then w satisfies φ too.

This captures @cite{veltman-1996}'s notion of "accepting" a default: σ accepts "normally φ" iff σ's pattern already respects φ.

Equations

• no.respects φ = ∀ (w v : W), no.le w v → φ v → φ w

theorem Core.Order.NormalityOrder.refine_respects {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) : (no.refine φ).respects φ

Refinement by φ always produces an ordering that respects φ.

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

Persistence: if an ordering respects φ, further refinement by any ψ still respects φ. Defaults are not undone by later defaults.

@cite{veltman-1996}, Proposition 3.6(iv).

theorem Core.Order.NormalityOrder.respects_refine_iff {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) (h : no.respects φ) {w v : W} : (no.refine φ).le w v ↔ no.le w v

When an ordering respects φ, its restriction to φ-worlds is the same as the full ordering: refinement is idempotent on respected defaults.

theorem Core.Order.NormalityOrder.refine_idempotent {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) : (no.refine φ).refine φ = no.refine φ

Idempotency: refining by φ twice is the same as refining once.

@cite{veltman-1996}, Proposition 3.6(ii): (ε ∘ e) ∘ e = ε ∘ e.

theorem Core.Order.NormalityOrder.refine_comm {W : Type u_1} (no : NormalityOrder W) (φ ψ : W → Prop) : (no.refine φ).refine ψ = (no.refine ψ).refine φ

Commutativity: the order of refinements doesn't matter.

Follows from refinement being intersection with a set of pairs: (ε ∘ e₁) ∘ e₂ = ε ∩ R(e₁) ∩ R(e₂) = (ε ∘ e₂) ∘ e₁.

theorem Core.Order.NormalityOrder.refine_univ {W : Type u_1} (no : NormalityOrder W) : (no.refine fun (x : W) => True) = no

Refining by the universal property is the identity.

theorem Core.Order.NormalityOrder.refine_empty {W : Type u_1} (no : NormalityOrder W) : (no.refine fun (x : W) => False) = no

Refining by the empty property is the identity (vacuously).

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

Respecting ordering equality: if an ordering respects φ, then refining by φ gives back the same ordering.

@cite{veltman-1996}: ε ∘ e = ε when e is already a default in ε.

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

Under a connected ordering that respects φ, all optimal worlds in a domain satisfy φ — provided the domain has at least one φ-world.

This generalizes refine_total_optimal beyond the total ordering. Connectedness is essential: without it, a non-φ-world can be optimal by being incomparable with all φ-worlds.

Note: @cite{veltman-1996} Proposition 3.4(i) states this without the connectedness assumption, but his proof implicitly relies on states being reachable from the total ordering, which ensures connectedness after a single refinement. After multiple refinements by "crossing" properties, connectedness can fail and the result no longer holds for arbitrary respecting orderings.

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

Refinement makes φ-worlds optimal. Starting from the total ordering, refining by φ makes the optimal worlds in any domain d exactly the φ-worlds in d — provided at least one φ-world exists.

This is the mathematical core of Veltman's system: "normally φ" followed by "presumably φ" succeeds, because refinement guarantees φ-worlds become the most normal.

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

An optimal φ-world under no remains optimal under no.refine φ.

If w is optimal in d (no world in d strictly dominates it) and w satisfies φ, then w is still optimal in d after refinement by φ. This is the core lemma for coherence preservation (Proposition 4.7): refinement can't destroy the optimality of worlds that satisfy the refinement property.

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

Refinement preserves nonemptiness of optimal sets when the original optimal set contains φ-worlds.

theorem Core.Order.NormalityOrder.respects_no_domination {W : Type u_1} (no : NormalityOrder W) (φ : W → Prop) (hresp : no.respects φ) {w v : W} (hv : φ v) (hw : ¬φ w) : ¬no.le w v

When the ordering respects φ, no non-φ-world can dominate a φ-world. Combined with optimality, this constrains which worlds can be optimal.

def Core.Order.NormalityOrder.fromProps {W : Type u_1} (props : List (W → Bool)) : NormalityOrder W

Construct a normality ordering from a list of propositions. w ≤ v iff every proposition satisfied by v is also satisfied by w.

This is @cite{kratzer-1981}'s ordering source construction: {p ∈ A : v ∈ p} ⊆ {p ∈ A : w ∈ p}.

Equivalent to atLeastAsGoodAs in Modality/Kratzer.lean (computable) and kratzerPlausibility in BeliefRevision.lean (with smoothness).

Equations

• Core.Order.NormalityOrder.fromProps props = { le := fun (w v : W) => ∀ (p : W → Bool), p ∈ props → p v = true → p w = true, le_refl := ⋯, le_trans := ⋯ }

theorem Core.Order.NormalityOrder.fromProps_nil {W : Type u_1} {w v : W} : (fromProps []).le w v

The empty ordering source gives the total ordering.

theorem Core.Order.NormalityOrder.fromProps_cons_le {W : Type u_1} (p : W → Bool) (ps : List (W → Bool)) {w v : W} (h : (fromProps (p :: ps)).le w v) : (fromProps ps).le w v

Adding a proposition to the ordering source refines it.

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

Refining from the total ordering always gives a connected ordering.

In the total ordering, every pair is related in both directions. After one refinement by φ, the ordering (φ v → φ w) is still connected because material implication between truth values always holds in at least one direction.

This does NOT generalize to arbitrary connected orderings: if only w ≤ v holds (not v ≤ w) and φ(v), ¬φ(w), neither refined direction holds. And after two refinements by "crossing" properties, connectedness can fail entirely.

@cite{darwiche-pearl-1997}, Definition 8. Conditions on how a total pre-order (faithful assignment) may change under revision by μ. These are the representation-theorem equivalents of the iterated revision postulates C1–C4. They constrain how any ordering-based semantics — Kratzer modals, Lewis conditionals, Veltman defaults — should evolve under discourse update.

`prior` and `post` are the orderings before and after revision by μ.
Lower in the ordering = more normal/plausible. 

@[reducible]

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

CR1: The ordering among μ-worlds is preserved.

Equations

• prior.satisfies_CR1 post μ = ∀ (w v : W), μ w = true → μ v = true → (prior.le w v ↔ post.le w v)

@[reducible]

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

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

Equations

• prior.satisfies_CR2 post μ = ∀ (w v : W), μ w = false → μ v = false → (prior.le w v ↔ post.le w v)

@[reducible]

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

CR3: If a μ-world was strictly below a ¬μ-world, it stays strictly below.

Equations

• prior.satisfies_CR3 post μ = ∀ (w v : W), μ w = true → μ v = false → prior.slt w v → post.slt w v

@[reducible]

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

CR4: If a μ-world was ≤ a ¬μ-world, it stays ≤.

Equations

• prior.satisfies_CR4 post μ = ∀ (w v : W), μ w = true → μ v = false → prior.le w v → post.le w v