Plausibility Orderings and Preferential Consequence

@cite{kraus-magidor-1990} @cite{halpern-2003}

Plausibility orderings and preferential consequence relations are the general mathematical structures underlying default reasoning. This file extracts them from the AGM-specific machinery in BeliefRevision.lean, placing them in Core/Order/ alongside NormalityOrder.

Key definitions

• PlausibilityOrder W: NormalityOrder + smoothness (every satisfiable proposition has minimal elements)
• PreferentialConsequence W: System P axioms for φ |~ ψ
• rationalMonotonicity: the stronger property satisfied by ranked models
• PlausibilityOrder.toPreferential: the sound construction

Architecture

Core/Order/Normality.lean      — NormalityOrder (preorder on worlds)
    ↓ extends
Core/Order/Plausibility.lean   — PlausibilityOrder + System P
    ↑ uses                         ↑ uses
Core/Logic/RankingFunction.lean    Core/Logic/BeliefRevision.lean (AGM)
Core/Logic/SystemZ.lean

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

A preferential consequence relation: φ |~ ψ reads "normally, if φ then ψ".

System P axiomatizes the minimal properties of default reasoning. @cite{halpern-2003} shows that System P is sound and complete for preferential models — structures where worlds are ordered by plausibility, and φ |~ ψ iff ψ holds at all most-plausible φ-worlds.

• default : Prop' W → Prop' W → Prop

  The default consequence relation: default φ ψ means φ |~ ψ

• refl (φ : Prop' W) : self.default φ φ

  Reflexivity: φ |~ φ

• leftEquiv (φ ψ χ : Prop' W) : (∀ (w : W), φ w ↔ ψ w) → (self.default φ χ ↔ self.default ψ χ)

  Left Logical Equivalence: if φ ↔ ψ then (φ | χ ↔ ψ | χ)

• rightWeaken (φ ψ χ : Prop' W) : self.default φ ψ → (∀ (w : W), ψ w → χ w) → self.default φ χ

  Right Weakening: if φ | ψ and ψ → χ, then φ | χ

• and_ (φ ψ χ : Prop' W) : self.default φ ψ → self.default φ χ → self.default φ fun (w : W) => ψ w ∧ χ w

  And: if φ | ψ and φ | χ, then φ |~ (ψ ∧ χ)

• or_ (φ ψ χ : Prop' W) : self.default φ χ → self.default ψ χ → self.default (fun (w : W) => φ w ∨ ψ w) χ

  Or: if φ | χ and ψ | χ, then (φ ∨ ψ) |~ χ

• cautiousMono (φ ψ χ : Prop' W) : self.default φ ψ → self.default φ χ → self.default (fun (w : W) => φ w ∧ ψ w) χ

  Cautious Monotonicity: if φ | ψ and φ | χ, then (φ ∧ ψ) |~ χ

def Core.Order.rationalMonotonicity {W : Type u_1} (pc : PreferentialConsequence W) : Prop

Rational Monotonicity: if φ | χ and ¬(φ | ¬ψ), then (φ ∧ ψ) |~ χ.

This is strictly stronger than System P. @cite{halpern-2003} shows it corresponds to ranked (well-ordered) plausibility models, not merely preferential ones.

Equations

• Core.Order.rationalMonotonicity pc = ∀ (φ ψ χ : Prop' W), pc.default φ χ → (¬pc.default φ fun (w : W) => ¬ψ w) → pc.default (fun (w : W) => φ w ∧ ψ w) χ

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

A plausibility ordering on worlds: w₁ ≤ w₂ means w₁ is at least as plausible as w₂. The minimal elements of a proposition A are the most plausible A-worlds.

Extends NormalityOrder with the smoothness condition (also called "limit assumption"): every satisfiable proposition has minimal elements. This is automatic for finite W; for infinite W it rules out infinite descending chains. @cite{kraus-magidor-1990} call this "stopperedness".

• 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
• smooth (φ : Prop' W) (w : W) : φ w → ∃ (v : W), φ v ∧ self.le v w ∧ ∀ (u : W), φ u → self.le u v → self.le v u

  Smoothness: every satisfiable φ has a minimal element

def Core.Order.PlausibilityOrder.minimal {W : Type u_1} (po : PlausibilityOrder W) (φ : Prop' W) : Prop' W

The most plausible worlds satisfying φ: those with no strictly more plausible φ-world.

This is the same as NormalityOrder.optimal applied to the set {w | φ w}, but stated with Prop' for the System P interface.

Equations

• po.minimal φ w = (φ w ∧ ∀ (v : W), φ v → po.le v w → po.le w v)

def Core.Order.PlausibilityOrder.toPreferential {W : Type u_1} (po : PlausibilityOrder W) : PreferentialConsequence W

A plausibility ordering induces a preferential consequence relation: φ |~ ψ iff all minimal φ-worlds satisfy ψ.

@cite{halpern-2003}, Theorem 8.1.1: System P is sound and complete for this semantics.

Equations

• po.toPreferential = { default := fun (φ ψ : Prop' W) => ∀ (w : W), po.minimal φ w → ψ w, refl := ⋯, leftEquiv := ⋯, rightWeaken := ⋯, and_ := ⋯, or_ := ⋯, cautiousMono := ⋯ }