Iterated belief revision

This file defines revision operators on epistemic states and the postulates of Darwiche and Pearl for iterated belief revision, and proves their representation by total preorders on worlds.

Darwiche and Pearl revise epistemic states rather than belief sets. A state carries the worlds its belief set admits together with a disposition to revise, and a revision operator sends a state and a proposition, a set of worlds, to a new state. The postulates of Alchourrón, Gärdenfors and Makinson, in the form Katsuno and Mendelzon gave them, transfer to states with syntax-irrelevance weakened. An operator satisfies them iff a faithful assignment of total preorders to states represents it, which means that the belief worlds of a state are its least worlds and that revision by μ selects the least μ-worlds (Theorem 2). A state accepts β given α when revising it by α yields a state that believes β. These conditional beliefs form a rational consequence relation in the sense of Lehmann and Magidor, and the preorder of the state encodes them. This is the translation between belief revision and nonmonotonic inference that Gärdenfors and Makinson describe, under which superexpansion corresponds to Or, subexpansion to rational monotonicity, and consistency to consistency preservation. The iterated-revision postulates C1–C4 say which conditional beliefs a revision preserves. Each of them, and Boutilier's postulate CB, is equivalent to a condition on how the preorder of a state relates to the preorder of its revision (Theorems 3 and 4). The conditions are agreement on the μ-worlds, agreement on the non-μ-worlds, preservation of strict and of weak rankings of a μ-world over a non-μ-world, and agreement outside the revised belief set. Spohn's conditionalisation of rankings, which makes the evidence one degree more plausible than it was implausible, is represented by the rankings' own orderings and meets every postulate (Theorem 5). On a normalised ranking it is conditionalisation on the evidence at the firmness one above the rank of its negation.

Implementation notes

• Rankings are bare functions W → ℕ, as the paper relaxes normalisation so that revision by an unsatisfiable proposition yields an unsatisfiable belief set; rank of a proposition is the infimum of its worlds' ranks.
• A faithful assignment sends each state to a preorder given as a term, with totality a field of Faithful. The revised belief worlds are then Preorder.minimals of the evidence, and the conditional beliefs of a state are Nonmonotonic.Entails of its preorder (Faithful.accepts_iff).
• The postulate of syntax-irrelevance holds by construction: propositions are sets of worlds and revision is a function of the state.
• The consistency postulate and the representation of C3 and C4 need least elements to exist, which a finite set of worlds, the paper's propositional setting, guarantees.

References

• A. Darwiche and J. Pearl, On the Logic of Iterated Belief Revision (1997)
• C. E. Alchourrón, P. Gärdenfors and D. Makinson, On the Logic of Theory Change: Partial Meet Contraction and Revision Functions (1985)
• H. Katsuno and A. O. Mendelzon, Propositional Knowledge Base Revision and Minimal Change (1991)
• D. Lehmann and M. Magidor, What Does a Conditional Knowledge Base Entail? (1992)
• P. Gärdenfors and D. Makinson, Nonmonotonic Inference Based on Expectations (1994)
• W. Spohn, Ordinal Conditional Functions: A Dynamic Theory of Epistemic States (1988)

structure BeliefRevision.Revision (S : Type u_3) (W : Type u_4) : Type (max u_3 u_4)

A revision operator on epistemic states over the worlds W assigns each state the worlds its belief set admits and revises a state by a proposition.

• bel : S → Set W

  The worlds admitted by the state's belief set.

• revise : S → Set W → S

  Revision of a state by a proposition.

def BeliefRevision.AgreesOn {W : Type u_2} (p q : Preorder W) (d : Set W) : Prop

Two preorders agree on d.

Equations

• BeliefRevision.AgreesOn p q d = ∀ w ∈ d, ∀ v ∈ d, w ≤ v ↔ w ≤ v

def BeliefRevision.PreservesLt {W : Type u_2} (p q : Preorder W) (μ : Set W) : Prop

A μ-world strictly below a non-μ-world in p stays strictly below in q.

Equations

• BeliefRevision.PreservesLt p q μ = ∀ w ∈ μ, ∀ v ∉ μ, w < v → w < v

def BeliefRevision.PreservesLe {W : Type u_2} (p q : Preorder W) (μ : Set W) : Prop

A μ-world weakly below a non-μ-world in p stays weakly below in q.

Equations

• BeliefRevision.PreservesLe p q μ = ∀ w ∈ μ, ∀ v ∉ μ, w ≤ v → w ≤ v

@[instance_reducible]

instance BeliefRevision.instDecidableAgreesOn {W : Type u_2} [Fintype W] {p q : Preorder W} [DecidableRel LE.le] [DecidableRel LE.le] {d : Set W} [DecidablePred fun (x : W) => x ∈ d] : Decidable (AgreesOn p q d)

Equations

• BeliefRevision.instDecidableAgreesOn = id inferInstance

@[instance_reducible]

instance BeliefRevision.instDecidablePreservesLt {W : Type u_2} [Fintype W] {p q : Preorder W} [DecidableRel LT.lt] [DecidableRel LT.lt] {d : Set W} [DecidablePred fun (x : W) => x ∈ d] : Decidable (PreservesLt p q d)

Equations

• BeliefRevision.instDecidablePreservesLt = id inferInstance

@[instance_reducible]

instance BeliefRevision.instDecidablePreservesLe {W : Type u_2} [Fintype W] {p q : Preorder W} [DecidableRel LE.le] [DecidableRel LE.le] {d : Set W} [DecidablePred fun (x : W) => x ∈ d] : Decidable (PreservesLe p q d)

Equations

• BeliefRevision.instDecidablePreservesLe = id inferInstance

theorem BeliefRevision.AgreesOn.minimals_eq {W : Type u_2} {p q : Preorder W} {d α : Set W} (h : AgreesOn p q d) (hα : α ⊆ d) : p.minimals α = q.minimals α

structure BeliefRevision.Revision.IsAGM {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

A revision operator satisfies the AGM postulates on epistemic states when it has success, expansion when the evidence is consistent with the beliefs, consistency, superexpansion and subexpansion.

• success (Ψ : S) (μ : Set W) : r.bel (r.revise Ψ μ) ⊆ μ
• expansion (Ψ : S) (μ : Set W) : (r.bel Ψ ∩ μ).Nonempty → r.bel (r.revise Ψ μ) = r.bel Ψ ∩ μ
• consistency (Ψ : S) (μ : Set W) : μ.Nonempty → (r.bel (r.revise Ψ μ)).Nonempty
• superexpansion (Ψ : S) (μ φ : Set W) : r.bel (r.revise Ψ μ) ∩ φ ⊆ r.bel (r.revise Ψ (μ ∩ φ))
• subexpansion (Ψ : S) (μ φ : Set W) : (r.bel (r.revise Ψ μ) ∩ φ).Nonempty → r.bel (r.revise Ψ (μ ∩ φ)) ⊆ r.bel (r.revise Ψ μ) ∩ φ

structure BeliefRevision.Revision.Faithful {S : Type u_1} {W : Type u_2} (r : Revision S W) (ord : S → Preorder W) : Prop

An assignment of total preorders to states is faithful and represents r when the belief worlds of a state are equally plausible and strictly more plausible than the others, and revision selects the least worlds of the evidence.

• total (Ψ : S) : Std.Total LE.le
• equiv_of_mem (Ψ : S) (w v : W) : w ∈ r.bel Ψ → v ∈ r.bel Ψ → AntisymmRel LE.le w v
• lt_of_mem (Ψ : S) (w v : W) : w ∈ r.bel Ψ → v ∉ r.bel Ψ → w < v
• bel_revise (Ψ : S) (μ : Set W) : r.bel (r.revise Ψ μ) = (ord Ψ).minimals μ

def BeliefRevision.Revision.C1 {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

Postulate (C1) says that evidence entailed by later evidence is redundant.

Equations

• r.C1 = ∀ (Ψ : S) (μ α : Set W), α ⊆ μ → r.bel (r.revise (r.revise Ψ μ) α) = r.bel (r.revise Ψ α)

def BeliefRevision.Revision.C2 {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

Postulate (C2) says that evidence contradicted by later evidence is overridden.

Equations

• r.C2 = ∀ (Ψ : S) (μ α : Set W), α ⊆ μᶜ → r.bel (r.revise (r.revise Ψ μ) α) = r.bel (r.revise Ψ α)

def BeliefRevision.Revision.C3 {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

Postulate (C3) says that evidence implied by later evidence given the state is retained.

Equations

• r.C3 = ∀ (Ψ : S) (μ α : Set W), r.bel (r.revise Ψ α) ⊆ μ → r.bel (r.revise (r.revise Ψ μ) α) ⊆ μ

def BeliefRevision.Revision.C4 {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

Postulate (C4) says that evidence not contradicted by later evidence stays uncontradicted.

Equations

• r.C4 = ∀ (Ψ : S) (μ α : Set W), ¬r.bel (r.revise Ψ α) ⊆ μᶜ → ¬r.bel (r.revise (r.revise Ψ μ) α) ⊆ μᶜ

def BeliefRevision.Revision.CB {S : Type u_1} {W : Type u_2} (r : Revision S W) : Prop

Boutilier's postulate (CB) says that evidence contradicted by later evidence is forgotten.

Equations

• r.CB = ∀ (Ψ : S) (μ α : Set W), r.bel (r.revise Ψ μ) ⊆ αᶜ → r.bel (r.revise (r.revise Ψ μ) α) = r.bel (r.revise Ψ α)

theorem BeliefRevision.Revision.IsAGM.revise_inter {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) {Ψ : S} {μ φ : Set W} (hne : (r.bel (r.revise Ψ μ) ∩ φ).Nonempty) : r.bel (r.revise Ψ (μ ∩ φ)) = r.bel (r.revise Ψ μ) ∩ φ

Revising by a conjunction is conditioning the revision by the first conjunct on the second, when that leaves something.

def BeliefRevision.Revision.Accepts {S : Type u_1} {W : Type u_2} (r : Revision S W) (Ψ : S) (α β : Set W) : Prop

The state Ψ accepts β given α, and β ∣ α is a conditional belief of Ψ, when the belief set of the revision of Ψ by α entails β.

Equations

• r.Accepts Ψ α β = (r.bel (r.revise Ψ α) ⊆ β)

theorem BeliefRevision.Revision.c1_iff_accepts {S : Type u_1} {W : Type u_2} (r : Revision S W) : r.C1 ↔ ∀ (Ψ : S) (μ α β : Set W), α ⊆ μ → (r.Accepts (r.revise Ψ μ) α β ↔ r.Accepts Ψ α β)

Postulate (C1) holds iff accommodating μ perturbs no conditional belief whose premise entails μ.

theorem BeliefRevision.Revision.c2_iff_accepts {S : Type u_1} {W : Type u_2} (r : Revision S W) : r.C2 ↔ ∀ (Ψ : S) (μ α β : Set W), α ⊆ μᶜ → (r.Accepts (r.revise Ψ μ) α β ↔ r.Accepts Ψ α β)

Postulate (C2) holds iff accommodating μ perturbs no conditional belief whose premise contradicts μ.

theorem BeliefRevision.Revision.c3_iff_accepts {S : Type u_1} {W : Type u_2} (r : Revision S W) : r.C3 ↔ ∀ (Ψ : S) (μ α : Set W), r.Accepts Ψ α μ → r.Accepts (r.revise Ψ μ) α μ

Postulate (C3) holds iff the conditional belief μ ∣ α is never given up on accommodating μ.

theorem BeliefRevision.Revision.c4_iff_accepts {S : Type u_1} {W : Type u_2} (r : Revision S W) : r.C4 ↔ ∀ (Ψ : S) (μ α : Set W), ¬r.Accepts Ψ α μᶜ → ¬r.Accepts (r.revise Ψ μ) α μᶜ

Postulate (C4) holds iff the conditional belief μᶜ ∣ α is never acquired on accommodating μ.

theorem BeliefRevision.Revision.IsAGM.isRational_accepts {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) (Ψ : S) : Nonmonotonic.IsRational (r.Accepts Ψ)

The conditional beliefs of a state of an AGM operator form a rational consequence relation. Superexpansion gives Or, and subexpansion gives cautious and rational monotonicity.

theorem BeliefRevision.Revision.IsAGM.accepts_empty_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) {Ψ : S} {α : Set W} : r.Accepts Ψ α ∅ ↔ α = ∅

A state of an AGM operator accepts the contradiction only given the contradiction (consistency preservation).

The representation theorem

theorem BeliefRevision.Revision.Faithful.mem_bel_revise {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) {Ψ : S} {μ : Set W} {w : W} : w ∈ r.bel (r.revise Ψ μ) ↔ w ∈ μ ∧ ∀ y ∈ μ, w ≤ y

Under a faithful assignment the revised belief worlds are the least worlds of the evidence.

theorem BeliefRevision.Revision.Faithful.le_of_mem {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) {Ψ : S} {w v : W} (hw : w ∈ r.bel Ψ) (hv : v ∉ r.bel Ψ) : w ≤ v

theorem BeliefRevision.Revision.Faithful.not_le_of_mem {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) {Ψ : S} {w v : W} (hw : w ∈ r.bel Ψ) (hv : v ∉ r.bel Ψ) : ¬v ≤ w

theorem BeliefRevision.Revision.Faithful.mem_bel_revise_pair {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) {Ψ : S} {w v : W} : w ∈ r.bel (r.revise Ψ {w, v}) ↔ w ≤ v

Under a faithful assignment w survives revision by the pair {w, v} exactly when it is at least as plausible as v.

theorem BeliefRevision.Revision.Faithful.isAGM {S : Type u_1} {W : Type u_2} {r : Revision S W} [Finite W] {ord : S → Preorder W} (h : r.Faithful ord) : r.IsAGM

A faithfully represented operator satisfies the postulates.

@[reducible]

def BeliefRevision.Revision.IsAGM.ord {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) (Ψ : S) : Preorder W

In the ordering an AGM operator induces on a state, w is at least as plausible as v when w is believed or survives revision by the pair.

Equations

• h.ord Ψ = Preorder.ofLE (fun (w v : W) => w ∈ r.bel Ψ ∨ w ∈ r.bel (r.revise Ψ {w, v})) ⋯ ⋯

theorem BeliefRevision.Revision.IsAGM.ord_total {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) (Ψ : S) : Std.Total LE.le

The induced ordering is total.

theorem BeliefRevision.Revision.IsAGM.faithful {S : Type u_1} {W : Type u_2} {r : Revision S W} (h : r.IsAGM) : r.Faithful h.ord

The induced ordering is a faithful assignment representing the operator.

theorem BeliefRevision.Revision.Faithful.accepts_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) {Ψ : S} {α β : Set W} : r.Accepts Ψ α β ↔ Nonmonotonic.Entails (ord Ψ) α β

The preorder of a state encodes its conditional beliefs, since β is accepted given α exactly when the least α-worlds are β-worlds.

theorem BeliefRevision.Revision.isAGM_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} [Finite W] : r.IsAGM ↔ ∃ (ord : S → Preorder W), r.Faithful ord

An operator satisfies the postulates iff a faithful assignment represents it (Theorem 2).

The iterated-revision postulates

theorem BeliefRevision.Revision.Faithful.agreesAfter_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) (D : S → Set W → Set W) : (∀ (Ψ : S) (μ α : Set W), α ⊆ D Ψ μ → r.bel (r.revise (r.revise Ψ μ) α) = r.bel (r.revise Ψ α)) ↔ ∀ (Ψ : S) (μ : Set W), AgreesOn (ord Ψ) (ord (r.revise Ψ μ)) (D Ψ μ)

Revising by μ before α ⊆ D Ψ μ leaves the beliefs of revising by α alone iff the preorders of a state and of its revision agree on D Ψ μ.

theorem BeliefRevision.Revision.Faithful.c1_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) : r.C1 ↔ ∀ (Ψ : S) (μ : Set W), AgreesOn (ord Ψ) (ord (r.revise Ψ μ)) μ

Postulate (C1) holds iff the preorders of a state and of its revision by μ agree on the μ-worlds, which is condition (CR1) of Theorem 4.

theorem BeliefRevision.Revision.Faithful.c2_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) : r.C2 ↔ ∀ (Ψ : S) (μ : Set W), AgreesOn (ord Ψ) (ord (r.revise Ψ μ)) μᶜ

Postulate (C2) holds iff the preorders of a state and of its revision by μ agree on the non-μ-worlds, which is condition (CR2) of Theorem 4.

theorem BeliefRevision.Revision.Faithful.cb_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} {ord : S → Preorder W} (h : r.Faithful ord) : r.CB ↔ ∀ (Ψ : S) (μ : Set W), AgreesOn (ord Ψ) (ord (r.revise Ψ μ)) (r.bel (r.revise Ψ μ))ᶜ

Postulate (CB) holds iff the preorders of a state and of its revision agree outside the revised belief set, which is condition (CBR) of Theorem 3.

theorem BeliefRevision.Revision.Faithful.c3_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} [Finite W] {ord : S → Preorder W} (h : r.Faithful ord) : r.C3 ↔ ∀ (Ψ : S) (μ : Set W), PreservesLt (ord Ψ) (ord (r.revise Ψ μ)) μ

Postulate (C3) holds iff revision by μ preserves each strict ranking of a μ-world below a non-μ-world, which is condition (CR3) of Theorem 4.

theorem BeliefRevision.Revision.Faithful.c4_iff {S : Type u_1} {W : Type u_2} {r : Revision S W} [Finite W] {ord : S → Preorder W} (h : r.Faithful ord) : r.C4 ↔ ∀ (Ψ : S) (μ : Set W), PreservesLe (ord Ψ) (ord (r.revise Ψ μ)) μ

Postulate (C4) holds iff revision by μ preserves each weak ranking of a μ-world below a non-μ-world, which is condition (CR4) of Theorem 4.

Spohn's revision of rankings

noncomputable def BeliefRevision.rank {W : Type u_2} (κ : W → ℕ) (μ : Set W) : ℕ

The rank of a proposition is the least rank of its worlds, and 0 for the empty proposition.

Equations

• BeliefRevision.rank κ μ = sInf (κ '' μ)

theorem BeliefRevision.rank_le {W : Type u_2} (κ : W → ℕ) (μ : Set W) {w : W} (hw : w ∈ μ) : rank κ μ ≤ κ w

theorem BeliefRevision.exists_rank_eq {W : Type u_2} (κ : W → ℕ) (μ : Set W) (hμ : μ.Nonempty) : ∃ w ∈ μ, κ w = rank κ μ

theorem BeliefRevision.rank_eq_of {W : Type u_2} (κ : W → ℕ) (μ : Set W) {n : ℕ} (h₁ : ∃ w ∈ μ, κ w = n) (h₂ : ∀ w ∈ μ, n ≤ κ w) : rank κ μ = n

noncomputable def BeliefRevision.spohn {W : Type u_2} (κ : W → ℕ) (μ : Set W) : W → ℕ

Spohn's revision shifts the μ-worlds down so that the best reach rank 0 and the others up by one, which makes the evidence one degree more plausible than it was implausible.

Equations

• BeliefRevision.spohn κ μ w = if w ∈ μ then κ w - BeliefRevision.rank κ μ else κ w + 1

noncomputable def BeliefRevision.spohnRevision (W : Type u_3) : Revision (W → ℕ) W

Spohn's revision is an operator on rankings whose belief sets are the rank-0 worlds.

Equations

• BeliefRevision.spohnRevision W = { bel := fun (κ : W → ℕ) => {w : W | κ w = 0}, revise := BeliefRevision.spohn }

theorem BeliefRevision.faithful_lift {W : Type u_2} {f : (W → ℕ) → Set W → W → ℕ} (hμ : ∀ (κ : W → ℕ) (μ : Set W), ∀ w ∈ μ, f κ μ w = κ w - rank κ μ) (hν : ∀ (κ : W → ℕ) (μ : Set W), ∀ w ∉ μ, 0 < f κ μ w) : { bel := fun (κ : W → ℕ) => {w : W | κ w = 0}, revise := f }.Faithful fun (κ : W → ℕ) => Preorder.lift κ

A revision of rankings that conditions the μ-worlds on μ and leaves the rest disbelieved is represented by the rankings' own orderings.

theorem BeliefRevision.agreesOn_lift {W : Type u_2} (κ : W → ℕ) (μ : Set W) {f : (W → ℕ) → Set W → W → ℕ} (hμ : ∀ (κ : W → ℕ) (μ : Set W), ∀ w ∈ μ, f κ μ w = κ w - rank κ μ) : AgreesOn (Preorder.lift κ) (Preorder.lift (f κ μ)) μ

Conditioning the μ-worlds on μ preserves their ordering.

theorem BeliefRevision.spohn_of_mem {W : Type u_2} (κ : W → ℕ) (μ : Set W) {w : W} (hw : w ∈ μ) : spohn κ μ w = κ w - rank κ μ

theorem BeliefRevision.spohn_of_notMem {W : Type u_2} (κ : W → ℕ) (μ : Set W) {w : W} (hw : w ∉ μ) : spohn κ μ w = κ w + 1

theorem BeliefRevision.spohnRevision_faithful {W : Type u_2} : (spohnRevision W).Faithful fun (κ : W → ℕ) => Preorder.lift κ

The rankings' orderings faithfully represent Spohn's revision (Lemma 2).

theorem BeliefRevision.spohn_agreesOn {W : Type u_2} (κ : W → ℕ) (μ : Set W) : AgreesOn (Preorder.lift κ) (Preorder.lift (spohn κ μ)) μ

Spohn's revision satisfies condition (CR1), the first part of Lemma 3.

theorem BeliefRevision.spohn_agreesOn_compl {W : Type u_2} (κ : W → ℕ) (μ : Set W) : AgreesOn (Preorder.lift κ) (Preorder.lift (spohn κ μ)) μᶜ

Spohn's revision satisfies condition (CR2), the second part of Lemma 3.

theorem BeliefRevision.spohn_preservesLt {W : Type u_2} (κ : W → ℕ) (μ : Set W) : PreservesLt (Preorder.lift κ) (Preorder.lift (spohn κ μ)) μ

Spohn's revision satisfies condition (CR3), the third part of Lemma 3.

theorem BeliefRevision.spohn_preservesLe {W : Type u_2} (κ : W → ℕ) (μ : Set W) : PreservesLe (Preorder.lift κ) (Preorder.lift (spohn κ μ)) μ

Spohn's revision satisfies condition (CR4), the fourth part of Lemma 3.

theorem BeliefRevision.spohnRevision_isAGM {W : Type u_2} [Finite W] : (spohnRevision W).IsAGM

Spohn's revision satisfies the AGM postulates (Theorem 5).

theorem BeliefRevision.spohnRevision_c1 {W : Type u_2} : (spohnRevision W).C1

Spohn's revision satisfies (C1) (Theorem 5).

theorem BeliefRevision.spohnRevision_c2 {W : Type u_2} : (spohnRevision W).C2

Spohn's revision satisfies (C2) (Theorem 5).

theorem BeliefRevision.spohnRevision_c3 {W : Type u_2} [Finite W] : (spohnRevision W).C3

Spohn's revision satisfies (C3) (Theorem 5).

theorem BeliefRevision.spohnRevision_c4 {W : Type u_2} [Finite W] : (spohnRevision W).C4

Spohn's revision satisfies (C4) (Theorem 5).

theorem BeliefRevision.spohn_eq_conditionα {W : Type u_2} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) : spohn (⇑κ) A = ⇑(κ.conditionα A hA ((κ.rank Aᶜ).toNat + 1))

On a ranking function, Spohn's revision by A is conditionalization on A at the firmness κ(Aᶜ) + 1.

theorem RankingFunction.accepts_spohnRevision_iff {W : Type u_2} (κ : RankingFunction W) {A B : Set W} : (BeliefRevision.spohnRevision W).Accepts (⇑κ) A B ↔ κ.Entails A B

The conditional beliefs of a ranking function under Spohn's revision are the consequences of its ranked model.