Belief Revision and Preferential Reasoning

@cite{halpern-2003} @cite{alchouron-gardenfors-makinson-1985} @cite{kraus-magidor-1990}

@cite{halpern-2003} connects three frameworks — default reasoning @cite{kratzer-1981} @cite{kratzer-2012} (System P), AGM belief revision, and conditional plausibility measures — showing they are algebraically equivalent. This file formalizes:

1. AGM revision postulates (K1–K5): the rational constraints on how a belief set should change when new evidence arrives.
2. Bridge to Kratzer: Kratzer's ordering source induces a PlausibilityOrder, connecting modal semantics to belief revision.
3. Bridge to probability: regular conditional plausibility measures induce AGM revision operators.

PreferentialConsequence (System P) and PlausibilityOrder are in Core/Order/Plausibility.lean.

The Connection

Kratzer ordering source (Theories/Semantics/Modality/Kratzer.lean)
    ↓
PlausibilityOrder (Core/Order/Plausibility.lean)
    ↓
Conditional plausibility (EpistemicScale/Conditional.lean)
    ↓
AGM revision operator (this file: K*1–K*5)

@[reducible, inline]

abbrev Core.Logic.BeliefRevision.BeliefSet (W : Type u_1) : Type u_1

A belief set: a deductively closed set of propositions. Represented as a predicate on propositions (K is a theory).

Equations

• Core.Logic.BeliefRevision.BeliefSet W = Set (Prop' W)

structure Core.Logic.BeliefRevision.AGMRevision (W : Type u_1) : Type u_1

An AGM revision operator with fixed prior beliefs.

The prior belief set K is determined by the measure (the probability-1 propositions), not freely chosen. This matches @cite{halpern-2003}'s representation theorem, where the AGM postulates hold for the specific K induced by the conditional plausibility measure.

K3 (inclusion) is stated in logical-consequence form: Kφ ⊆ Cn(K ∪ {φ}), meaning every revised belief is entailed by the prior beliefs together with φ. This is the standard semantic formulation that avoids requiring explicit deductive closure infrastructure.

• beliefs : BeliefSet W

  The prior belief set, determined by the measure

• revise : Prop' W → BeliefSet W

  The revision operation: φ ↦ K * φ

• success (φ : Prop' W) : (∃ (w : W), φ w) → φ ∈ self.revise φ

  K*2 (success): φ ∈ K * φ (when φ is satisfiable)

• inclusion (φ ψ : Prop' W) : ψ ∈ self.revise φ → ∀ (w : W), (∀ χ ∈ self.beliefs, χ w) → φ w → ψ w

  K*3 (inclusion): K * φ ⊆ Cn(K ∪ {φ}). Every revised belief follows from the prior beliefs plus φ. Stated semantically: if w satisfies all prior beliefs and φ, then w satisfies every ψ ∈ K * φ.

• vacuity (φ ψ : Prop' W) : (fun (w : W) => ¬φ w) ∉ self.beliefs → (∀ (w : W), (∀ χ ∈ self.beliefs, χ w) → φ w → ψ w) → ψ ∈ self.revise φ

  K4 (vacuity): if ¬φ ∉ K, then Cn(K ∪ {φ}) ⊆ K * φ. If φ is consistent with the prior beliefs, everything entailed by beliefs + φ is in the revised set. Together with K3, this gives K * φ = Cn(K ∪ {φ}) when φ is consistent with K.

• consistency (φ : Prop' W) : (∃ (w : W), φ w) → ∃ (w : W), ∀ ψ ∈ self.revise φ, ψ w

  K*5 (consistency): K * φ is consistent when φ is satisfiable

def Core.Logic.BeliefRevision.kratzerPlausibility {W : Type u_1} [Fintype W] [DecidableEq W] (orderingSource : List (BProp W)) : Order.PlausibilityOrder W

Equations

• Core.Logic.BeliefRevision.kratzerPlausibility orderingSource = { toNormalityOrder := Core.Order.NormalityOrder.fromProps orderingSource, smooth := ⋯ }

def Core.Logic.BeliefRevision.kratzerDefault {W : Type u_1} [Fintype W] [DecidableEq W] (orderingSource : List (BProp W)) : Order.PreferentialConsequence W

The preferential consequence relation induced by Kratzer's ordering source: φ |~ ψ iff all most-plausible φ-worlds (given the ordering source) satisfy ψ. This is the formal content of Kratzer's claim that "modal base + ordering source = conditional".

Equations

• Core.Logic.BeliefRevision.kratzerDefault orderingSource = (Core.Logic.BeliefRevision.kratzerPlausibility orderingSource).toPreferential

structure Core.Logic.BeliefRevision.Core.Scale.RegularCondMeasure (W : Type u_1) extends Core.Scale.CondMeasure W : Type u_1

A regular conditional measure: every satisfiable proposition is normal (P(φ|φ) ≠ 0 when φ ≠ ∅), and every satisfiable set has positive unconditional measure. The latter ("full support") ensures consistency of revised beliefs in finite W.

For the ratio construction FinAddMeasure.toCondMeasure, regularity is equivalent to: every singleton has positive measure.

@cite{halpern-2003}'s regularity condition.

• mu : Set W → ℚ
• nonneg (A : Set W) : 0 ≤ self.mu A
• additive (A B : Set W) : (∀ x ∈ A, x ∉ B) → self.mu (A ∪ B) = self.mu A + self.mu B
• total : self.mu Set.univ = 1
• condMu : Set W → Set W → ℚ
• cond_nonneg (A B : Set W) : 0 ≤ self.condMu A B
• cond_norm (B : Set W) : self.condMu B B ≠ 0 → self.condMu B B = 1
• cond_additive (A₁ A₂ B : Set W) : (∀ x ∈ A₁, x ∉ A₂) → self.condMu (A₁ ∪ A₂) B = self.condMu A₁ B + self.condMu A₂ B
• cond_chain (A B C : Set W) : self.condMu (A ∩ B) C = self.condMu A (B ∩ C) * self.condMu B C
• cond_univ (A : Set W) : self.condMu A Set.univ = self.mu A
• regular (φ : Set W) : (∃ (w : W), w ∈ φ) → self.condMu φ φ ≠ 0
• muPositive (φ : Set W) : (∃ (w : W), w ∈ φ) → 0 < self.mu φ

noncomputable def Core.Logic.BeliefRevision.Core.Scale.RegularCondMeasure.toAGM {W : Type u_1} [Fintype W] [DecidableEq W] (m : RegularCondMeasure W) : AGMRevision W

Theorem: every regular conditional plausibility measure induces an AGM revision operator on finite W.

Construction:

• K (beliefs) = {ψ | μ(ψ) = 1} — the probability-1 propositions
• K * φ = {ψ | P(ψ | φ) = P(⊤ | φ)} — the conditional probability-1 propositions

The AGM postulates K2–K5 are verified:

• K*2 (success): P(φ|φ) = P(⊤|φ) by regularity + cond_norm
• K*3 (inclusion): P(ψ|φ) = 1 → μ(φ \ ψ) = 0 → (ψ ∪ φᶜ) ∈ K → ψ follows from beliefs + φ
• K*4 (vacuity): if ¬φ ∉ K (i.e., μ(φ) > 0), then beliefs + φ entailing ψ implies P(ψ|φ) = 1 (by finite decomposition: every φ \ ψ world has measure 0, so μ(φ \ ψ) = 0)
• K5 (consistency): finite W has a positive-measure φ-world satisfying all beliefs, which satisfies all of Kφ by K*3

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Core.Logic.BeliefRevision.rankingToAGM {W : Type u_1} [Fintype W] [DecidableEq W] (κ : Ranking.RankingFunction W) : AGMRevision W

A ranking function induces an AGM revision operator.

@cite{goldszmidt-pearl-1996} §6: ranking conditioning satisfies the AGM postulates K2–K5. K = beliefSet κ (propositions true at all rank-0 worlds), K*φ = beliefSet of κ revised by φ.

When φ is a tautology (¬φ unsatisfiable), revision is trivial and Kφ = K. The unsatisfiable case never arises since K2 and K*5 require ∃ w, φ w.

Equations

• Core.Logic.BeliefRevision.rankingToAGM κ = { beliefs := κ.beliefSet, revise := Core.Logic.BeliefRevision.rankingReviseSet✝ κ, success := ⋯, inclusion := ⋯, vacuity := ⋯, consistency := ⋯ }