Darwiche and Pearl (1997): On the Logic of Iterated Belief Revision

This file formalizes the examples and appendix tables of Darwiche and Pearl's paper on iterated belief revision.

The AGM postulates constrain a single revision of a belief set and leave the agent's conditional beliefs, its disposition to revise, almost unconstrained, so an AGM-compatible operator may drop a conditional belief because the observation that would have triggered it arrived (an animal seen to fly is no longer believed to fly should it be a bird) or acquire one (a lady believed smart and rich is no longer believed rich once evidence against her smartness is overturned). The paper moves revision to epistemic states, weakens the postulate of syntax-irrelevance accordingly, since two states with the same beliefs may revise differently (two jurors who both believe A guilty but rank B and C differently), and adds four postulates: revising by a weaker proposition before a stronger one is redundant (C1), by a contradicted one is overridden (C2), evidence implied by later evidence is retained (C3), and evidence not contradicted by later evidence stays uncontradicted (C4). Each is equivalent to a condition on the faithful total preorders that represent the operator, Spohn's conditionalisation satisfies them all, and Boutilier's stronger postulate, minimising every change of conditional belief, forgets a colour observation once the animal's species is corrected. Four partial operators in the appendix show that the AGM postulates entail none of C1–C4, and an operator that moves the disbelieved worlds of rank two or more down rather than up satisfies C1 but neither C3 nor C4.

The framework and its theorems are in Logic/BeliefRevision/Iterated.lean; here the paper's examples and appendix tables are checked against them.

Implementation notes

• The worlds of an appendix table are the valuations of its two propositions, so a proposition is a set of pairs of Booleans, first and second naming the two.
• A table gives only the preorders before and after one revision; its compatibility with the postulates is that the revised belief worlds are the least evidence-worlds of the prior.

References

• A. Darwiche and J. Pearl, On the logic of iterated belief revision (1997)
• C. Boutilier, Iterated revision and minimal change of conditional beliefs (1996)
• M. Goldszmidt and J. Pearl, Qualitative probabilities for default reasoning, belief revision, and causal modeling (1996)

Epistemic states against belief sets

inductive DarwichePearl1997.Suspect : Type

The suspects of the murder trial of Example 3, which the paper takes from Goldszmidt and Pearl.

• a : Suspect
• b : Suspect
• c : Suspect

@[instance_reducible]

instance DarwichePearl1997.instDecidableEqSuspect : DecidableEq Suspect

Equations

• DarwichePearl1997.instDecidableEqSuspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DarwichePearl1997.instFintypeSuspect : Fintype Suspect

Equations

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

def DarwichePearl1997.juror₁ : Suspect → ℕ

The first juror holds A guilty, B a remote possibility and C innocent.

Equations

• DarwichePearl1997.juror₁ DarwichePearl1997.Suspect.a = 0
• DarwichePearl1997.juror₁ DarwichePearl1997.Suspect.b = 1
• DarwichePearl1997.juror₁ DarwichePearl1997.Suspect.c = 2

def DarwichePearl1997.juror₂ : Suspect → ℕ

The second juror holds A guilty, C a remote possibility and B innocent.

Equations

• DarwichePearl1997.juror₂ DarwichePearl1997.Suspect.a = 0
• DarwichePearl1997.juror₂ DarwichePearl1997.Suspect.c = 1
• DarwichePearl1997.juror₂ DarwichePearl1997.Suspect.b = 2

theorem DarwichePearl1997.jurors_bel : (BeliefRevision.spohnRevision Suspect).bel juror₁ = (BeliefRevision.spohnRevision Suspect).bel juror₂

The jurors share a belief set.

theorem DarwichePearl1997.jurors_revise : Suspect.b ∈ (BeliefRevision.spohnRevision Suspect).bel ((BeliefRevision.spohnRevision Suspect).revise juror₁ {w : Suspect | w ≠ Suspect.a}) ∧ Suspect.b ∉ (BeliefRevision.spohnRevision Suspect).bel ((BeliefRevision.spohnRevision Suspect).revise juror₂ {w : Suspect | w ≠ Suspect.a})

Told that A is innocent, the jurors part, the first blaming B and the second not, so revision cannot be a function of the belief set.

The appendix tables

@[reducible, inline]

abbrev DarwichePearl1997.World : Type

A world of a language with two propositions gives the truth values of its propositions.

Equations

• DarwichePearl1997.World = (Bool × Bool)

@[reducible, inline]

abbrev DarwichePearl1997.first : Set World

The first proposition.

Equations

• DarwichePearl1997.first = {w : DarwichePearl1997.World | w.1 = true}

@[reducible, inline]

abbrev DarwichePearl1997.second : Set World

The second proposition.

Equations

• DarwichePearl1997.second = {w : DarwichePearl1997.World | w.2 = true}

def DarwichePearl1997.table₁ : World → ℕ

Table 1, before revising by ¬(adder_ok ∧ multiplier_ok).

Equations

• DarwichePearl1997.table₁ (true, true) = 0
• DarwichePearl1997.table₁ (true, false) = 1
• DarwichePearl1997.table₁ (false, true) = 2
• DarwichePearl1997.table₁ (false, false) = 3

def DarwichePearl1997.table₁' : World → ℕ

Table 1, after.

Equations

• DarwichePearl1997.table₁' (true, true) = 1
• DarwichePearl1997.table₁' (true, false) = 0
• DarwichePearl1997.table₁' (false, true) = 2
• DarwichePearl1997.table₁' (false, false) = 1

theorem DarwichePearl1997.example₆ : (∀ (w : World), w ∈ (Preorder.lift table₁').minimals Set.univ ↔ w ∈ (Preorder.lift table₁).minimals {w : World | ¬(w ∈ first ∧ w ∈ second)}) ∧ (∀ (w : World), w ∈ (Preorder.lift table₁).minimals {w : World | w ∉ first} ↔ w = (false, true)) ∧ (∀ (w : World), w ∈ (Preorder.lift table₁').minimals {w : World | w ∉ first} ↔ w = (false, false)) ∧ ¬BeliefRevision.AgreesOn (Preorder.lift table₁) (Preorder.lift table₁') {w : World | ¬(w ∈ first ∧ w ∈ second)}

In Example 6, with adder_ok first and multiplier_ok second, the revision is compatible with the postulates, its belief worlds being the least μ-worlds of the prior. Revising by ¬adder_ok yields ¬adder_ok ∧ multiplier_ok from the prior but ¬adder_ok ∧ ¬multiplier_ok after μ, against (C1), and the two orderings disagree on μ, against (CR1).

def DarwichePearl1997.table₂ : World → ℕ

Table 2, before revising by ¬smart.

Equations

• DarwichePearl1997.table₂ (true, true) = 0
• DarwichePearl1997.table₂ (true, false) = 1
• DarwichePearl1997.table₂ (false, true) = 1
• DarwichePearl1997.table₂ (false, false) = 2

def DarwichePearl1997.table₂' : World → ℕ

Table 2, after.

Equations

• DarwichePearl1997.table₂' (true, true) = 2
• DarwichePearl1997.table₂' (true, false) = 1
• DarwichePearl1997.table₂' (false, true) = 0
• DarwichePearl1997.table₂' (false, false) = 1

theorem DarwichePearl1997.example₇ : (∀ (w : World), w ∈ (Preorder.lift table₂').minimals Set.univ ↔ w ∈ (Preorder.lift table₂).minimals {w : World | w ∉ first}) ∧ (∀ (w : World), w ∈ (Preorder.lift table₂).minimals first ↔ w = (true, true)) ∧ (∀ (w : World), w ∈ (Preorder.lift table₂').minimals first ↔ w = (true, false)) ∧ ¬BeliefRevision.AgreesOn (Preorder.lift table₂) (Preorder.lift table₂') first

In Example 7, with smart first and rich second, revising by smart yields smart ∧ rich from the prior but smart ∧ ¬rich after ¬smart, against (C2), and the orderings disagree on the smart-worlds, against (CR2).

def DarwichePearl1997.table₃ : World → ℕ

Table 3, before revising by flies.

Equations

• DarwichePearl1997.table₃ (true, true) = 2
• DarwichePearl1997.table₃ (true, false) = 3
• DarwichePearl1997.table₃ (false, true) = 1
• DarwichePearl1997.table₃ (false, false) = 0

def DarwichePearl1997.table₃' : World → ℕ

Table 3, after.

Equations

• DarwichePearl1997.table₃' (true, true) = 1
• DarwichePearl1997.table₃' (true, false) = 1
• DarwichePearl1997.table₃' (false, true) = 0
• DarwichePearl1997.table₃' (false, false) = 1

theorem DarwichePearl1997.example₈ : (∀ (w : World), w ∈ (Preorder.lift table₃').minimals Set.univ ↔ w ∈ (Preorder.lift table₃).minimals second) ∧ (∀ (w : World), w ∈ (Preorder.lift table₃).minimals first ↔ w = (true, true)) ∧ (∀ (w : World), w ∈ (Preorder.lift table₃').minimals first ↔ w ∈ first) ∧ ¬BeliefRevision.PreservesLt (Preorder.lift table₃) (Preorder.lift table₃') second

In Example 8, with bird first and flies second, revising by bird yields bird ∧ flies from the prior, which entails flies, but only bird after flies, against (C3), and a flies-world strictly below a ¬flies-world no longer is, against (CR3).

def DarwichePearl1997.table₄ : World → ℕ

Table 4, before revising by nice_day.

Equations

• DarwichePearl1997.table₄ (true, true) = 1
• DarwichePearl1997.table₄ (true, false) = 1
• DarwichePearl1997.table₄ (false, true) = 0
• DarwichePearl1997.table₄ (false, false) = 0

def DarwichePearl1997.table₄' : World → ℕ

Table 4, after.

Equations

• DarwichePearl1997.table₄' (true, true) = 2
• DarwichePearl1997.table₄' (true, false) = 1
• DarwichePearl1997.table₄' (false, true) = 0
• DarwichePearl1997.table₄' (false, false) = 1

theorem DarwichePearl1997.example₉ : (∀ (w : World), w ∈ (Preorder.lift table₄').minimals Set.univ ↔ w ∈ (Preorder.lift table₄).minimals second) ∧ (∀ (w : World), w ∈ (Preorder.lift table₄).minimals first ↔ w ∈ first) ∧ (∀ (w : World), w ∈ (Preorder.lift table₄').minimals first ↔ w = (true, false)) ∧ ¬BeliefRevision.PreservesLe (Preorder.lift table₄) (Preorder.lift table₄') second

In Example 9, with shining_sun first and nice_day second, revising by shining_sun yields shining_sun from the prior, leaving nice_day open, but shining_sun ∧ ¬nice_day after nice_day, against (C4), and a nice_day-world weakly below a ¬nice_day-world no longer is, against (CR4).

Boutilier's postulate forgets

theorem DarwichePearl1997.cb_forgets {S : Type u_1} {W : Type u_2} {r : BeliefRevision.Revision S W} (h : r.IsAGM) (hCB : r.CB) {Ψ : S} {bird red : Set W} (hΨ : r.bel Ψ = bird) (hne : (bird ∩ red).Nonempty) (hΨ' : r.bel (r.revise Ψ birdᶜ) = birdᶜ) : r.bel (r.revise (r.revise Ψ red) birdᶜ) = birdᶜ

In Example 10, under (CB), once a bird is seen to be red and then found not to be a bird, all that is believed is that it is not a bird, provided revising the original state by ¬bird left the colour open.

An operator satisfying (C1) but neither (C3) nor (C4)

noncomputable def DarwichePearl1997.diamond {W : Type u_1} (κ : W → ℕ) (μ : Set W) : W → ℕ

The operator of Theorem 6 is Spohn's, except that a disbelieved world of rank two or more moves down a degree instead of up.

Equations

• DarwichePearl1997.diamond κ μ w = if w ∈ μ then κ w - BeliefRevision.rank κ μ else if κ w < 2 then κ w + 1 else κ w - 1

noncomputable def DarwichePearl1997.diamondRevision (W : Type u_1) : BeliefRevision.Revision (W → ℕ) W

diamond as a revision operator on rankings.

Equations

• DarwichePearl1997.diamondRevision W = { bel := fun (κ : W → ℕ) => {w : W | κ w = 0}, revise := DarwichePearl1997.diamond }

theorem DarwichePearl1997.diamond_of_mem {W : Type u_1} {κ : W → ℕ} {μ : Set W} {w : W} (hw : w ∈ μ) : diamond κ μ w = κ w - BeliefRevision.rank κ μ

theorem DarwichePearl1997.diamond_of_notMem {W : Type u_1} {κ : W → ℕ} {μ : Set W} {w : W} (hw : w ∉ μ) : diamond κ μ w = if κ w < 2 then κ w + 1 else κ w - 1

theorem DarwichePearl1997.diamondRevision_faithful (W : Type u_1) : (diamondRevision W).Faithful fun (κ : W → ℕ) => Preorder.lift κ

The rankings' orderings represent diamond, so it satisfies the postulates (Theorem 6).

theorem DarwichePearl1997.diamondRevision_isAGM (W : Type u_1) [Finite W] : (diamondRevision W).IsAGM

theorem DarwichePearl1997.diamondRevision_c1 (W : Type u_1) : (diamondRevision W).C1

diamond satisfies (C1) (Theorem 6).

def DarwichePearl1997.table₅ : Fin 4 → ℕ

The prior of Table 5.

Equations

• DarwichePearl1997.table₅ 0 = 0
• DarwichePearl1997.table₅ 1 = 3
• DarwichePearl1997.table₅ 2 = 4
• DarwichePearl1997.table₅ 3 = 0

def DarwichePearl1997.table₅' : Fin 4 → ℕ

Table 5 after diamond by μ.

Equations

• DarwichePearl1997.table₅' 0 = 0
• DarwichePearl1997.table₅' 1 = 3
• DarwichePearl1997.table₅' 2 = 3
• DarwichePearl1997.table₅' 3 = 1

@[reducible, inline]

abbrev DarwichePearl1997.μ₅ : Set (Fin 4)

The evidence μ of Tables 5 and 6.

Equations

• DarwichePearl1997.μ₅ = {w : Fin 4 | w = 0 ∨ w = 1}

@[reducible, inline]

abbrev DarwichePearl1997.α₅ : Set (Fin 4)

The evidence α of Tables 5 and 6.

Equations

• DarwichePearl1997.α₅ = {w : Fin 4 | w = 1 ∨ w = 2}

theorem DarwichePearl1997.diamond_table₅ : diamond table₅ μ₅ = table₅'

theorem DarwichePearl1997.not_diamondRevision_c3 : ¬(diamondRevision (Fin 4)).C3

diamond violates (C3), by Table 5 (Theorem 6).

def DarwichePearl1997.table₆ : Fin 4 → ℕ

The prior of Table 6.

Equations

• DarwichePearl1997.table₆ 0 = 0
• DarwichePearl1997.table₆ 1 = 3
• DarwichePearl1997.table₆ 2 = 3
• DarwichePearl1997.table₆ 3 = 0

def DarwichePearl1997.table₆' : Fin 4 → ℕ

Table 6 after diamond by μ.

Equations

• DarwichePearl1997.table₆' 0 = 0
• DarwichePearl1997.table₆' 1 = 3
• DarwichePearl1997.table₆' 2 = 2
• DarwichePearl1997.table₆' 3 = 1

theorem DarwichePearl1997.diamond_table₆ : diamond table₆ μ₅ = table₆'

theorem DarwichePearl1997.not_diamondRevision_c4 : ¬(diamondRevision (Fin 4)).C4

diamond violates (C4), by Table 6 (Theorem 6).