Plausibility orderings and preferential consequence

[KLM90] [Hal03]

A plausibility ordering is a Preorder on worlds together with a smoothness (stopperedness) property: every satisfiable proposition has a minimal element below any witness. The most-plausible φ-worlds are mathlib's Minimal (= Normality.optimal). This replaces the former PlausibilityOrder extends NormalityOrder hand-rolled structure.

Main definitions

• Smooth p — [KLM90]'s stopperedness for a Preorder.
• PlausibilityOrder W — a Preorder W bundled with Smooth.
• PreferentialConsequence W — System P for φ |~ ψ.
• PlausibilityOrder.toPreferential — soundness for System P.

Preferential consequence (System P)

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; [Hal03] shows soundness and completeness for preferential models.

• default : Set W → Set W → Prop

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

• refl (φ : Set W) : self.default φ φ

  Reflexivity: φ |~ φ

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

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

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

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

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

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

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

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

• cautiousMono (φ ψ χ : Set 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 (φ ∧ ψ) |~ χ. Strictly stronger than System P; [Hal03] ties it to ranked models.

Equations

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

Plausibility orderings

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

Smoothness ([KLM90] stopperedness): every satisfiable φ has a minimal element below any witness. Automatic for finite W; for infinite W it is the well-foundedness condition ruling out infinite descending chains.

Equations

• Core.Order.Smooth p = ∀ (φ : Set W) (w : W), φ w → ∃ (v : W), φ v ∧ v ≤ w ∧ ∀ (u : W), φ u → u ≤ v → v ≤ u

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

A plausibility ordering: a Preorder with the smoothness property. toPreorder.le w v means w is at least as plausible as v.

• toPreorder : Preorder W

  The underlying plausibility preorder.

• smooth : Smooth self.toPreorder

  Smoothness / stopperedness.

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

The most plausible φ-worlds: those with no strictly more plausible φ-world. The same as Normality.optimal toPreorder φ.

Equations

• po.minimal φ w = (φ w ∧ ∀ (v : W), φ v → v ≤ w → 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 ψ. [Hal03]: System P is sound and complete for this semantics.

Equations

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