Darwiche & Pearl (1997): On the Logic of Iterated Belief Revision #
@cite{darwiche-pearl-1997}
AGM belief revision constrains how a single revision should update an agent's beliefs, but says nothing about how the agent's disposition to revise should change. @cite{darwiche-pearl-1997} show that AGM- compatible revision operators can behave pathologically under iteration, and propose four additional postulates C1–C4 that rule out these pathologies.
Representation Theorem (Theorem 13) #
C1–C4 are equivalent to conditions CR1–CR4 on the faithful assignment (total pre-order) that represents an epistemic state:
- CR1: The ordering among μ-worlds is preserved.
- CR2: The ordering among ¬μ-worlds is preserved.
- CR3: If a μ-world was strictly below a ¬μ-world, it stays so.
- CR4: If a μ-world was ≤ a ¬μ-world, it stays so.
Counterexamples (Tables A.1–A.4) #
For each CR_i, there exists an AGM-compatible revision operator that violates CR_i while satisfying the other three. This shows the four conditions are logically independent — none is derivable from the rest.
Bridge to Ranking Functions #
Core.Logic.Ranking.ranking_satisfies_C1..C4 proves that Spohn's
A,α-conditionalization satisfies all four postulates. The counterexamples
here use non-ranking revision operators — arbitrary total pre-order
transformations that respect AGM success but violate the D&P constraints.
Linguistic Connection #
Ranking functions → PlausibilityOrder → NormalityOrder → Kratzer's
ordering sources for modals/conditionals. The D&P postulates constrain
how modal bases evolve under discourse update — without them, an
agent's conditional beliefs can shift arbitrarily between utterances.
Dynamic semantics (DRT/DPL context update) is iterated revision:
each sentence revises the common ground, and C1–C4 ensure that
the ordering of live possibilities evolves rationally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Convert a ranking function to its induced normality ordering.
le w v ↔ κ(w) ≤ κ(v). Defined directly (not via toPlausibilityOrder)
so that le reduces for native_decide.
Equations
- One or more equations did not get rendered due to their size.
Instances For
rankToOrder agrees with the canonical path through PlausibilityOrder.
AGM success: all rank-0 worlds in the posterior satisfy μ.
Equations
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.agmSuccess post μ = ∀ (w : Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4), post.rank w = 0 → μ w = true
Instances For
Prior: w1=0, w2=1, w3=2, w4=3. Revise by μ = {w2,w3,w4}. Posterior: w1=1, w2=0, w3=2, w4=1. Within μ, the ordering of w3 vs w4 flips (2<3 → 2>1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prior: w1=0, w2=1, w3=1, w4=2. Revise by μ = {w3,w4}. Posterior: w1=2, w2=1, w3=0, w4=1. Within ¬μ = {w1,w2}, the ordering flips (0<1 → 2>1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A2 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w3 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A2 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w4 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A2 x✝ = false
Instances For
Prior: w1=0, w2=1, w3=2, w4=3. Revise by μ = {w1,w2}. Posterior: w1=0, w2=2, w3=2, w4=3. w2 ∈ μ, w3 ∈ ¬μ: prior 1 < 2 (strict), posterior 2 ≤ 2 (not strict).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A3 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w1 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A3 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w2 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A3 x✝ = false
Instances For
Prior: w1=0, w2=1, w3=1, w4=2. Revise by μ = {w1,w2}. Posterior: w1=0, w2=2, w3=1, w4=3. w2 ∈ μ, w3 ∈ ¬μ: prior 1 ≤ 1, but posterior 2 > 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A4 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w1 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A4 Phenomena.DefaultReasoning.Studies.DarwichePearl1997.W4.w2 = true
- Phenomena.DefaultReasoning.Studies.DarwichePearl1997.mu_A4 x✝ = false
Instances For
The four conditions are logically independent: for each CR_i, there exists an AGM-compatible revision that violates CR_i alone.
This is the content of @cite{darwiche-pearl-1997}, Appendix A.
@cite{darwiche-pearl-1997}, Theorem 17: Spohn's ranking conditioning
satisfies C1–C4 (equivalently CR1–CR4). The proofs are in
Core.Logic.Ranking:
- `ranking_satisfies_C1` — C1 holds for `conditionα` with any α, β
- `ranking_satisfies_C2` — C2 holds for `conditionα` with any α, β
- `ranking_satisfies_C3` — C3 holds for canonical `revise`
- `ranking_satisfies_C4` — C4 holds for canonical `revise`
Together with the counterexamples above, this shows that ranking
conditioning is the *tightest* well-behaved revision operator:
it satisfies all four independence conditions that AGM alone
leaves unconstrained.
The chain to linguistics:
```
RankingFunction.revise
→ satisfies C1–C4 (this file's counterexamples show AGM alone doesn't)
→ PlausibilityOrder (via toPlausibilityOrder)
→ NormalityOrder (via toNormalityOrder)
→ Kratzer ordering sources (via fromProps)
→ modal/conditional semantics
```