Spohn (1988): Ranking Functions for Graded Belief Revision

@cite{spohn-1988}

This study demonstrates ordinal conditional functions (OCFs) as a model of belief revision with graded evidence strength. The firmness parameter α from @cite{spohn-1988} Definition 6 distinguishes weak evidence (low α, e.g. hearsay) from strong evidence (high α, e.g. direct observation).

Key demonstrations

1. Evidence strength: Different α values produce different post-revision rankings — strong evidence pushes counter-evidence worlds further into disbelief than weak evidence does.

2. Commutativity (Theorem 4): When two pieces of evidence satisfy the conditions of Theorem 4, the order of processing doesn't matter — verified for a concrete 4-world instance.

3. Connection to NormalityOrder: Ranking functions induce connected (total) plausibility orderings, refining any Kratzer-style ordering source with explicit disbelief grades.

Scenario

Four weather worlds with a prior ranking. Two pieces of evidence ("sunny" and "warm") are processed with varying firmness. Hand-computed conditioned rankings are verified against the A,α-conditionalization algorithm.

inductive Spohn1988.Weather : Type

Four weather scenarios.

• sunny_warm : Weather
• sunny_cold : Weather
• rainy_warm : Weather
• rainy_cold : Weather

@[implicit_reducible]

instance Spohn1988.instDecidableEqWeather : DecidableEq Weather

Equations

• Spohn1988.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Spohn1988.instReprWeather.repr : Weather → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Spohn1988.instReprWeather : Repr Weather

Equations

• Spohn1988.instReprWeather = { reprPrec := Spohn1988.instReprWeather.repr }

@[implicit_reducible]

instance Spohn1988.instFintypeWeather : Fintype Weather

Equations

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

def Spohn1988.prior : Core.Logic.Ranking.RankingFunction Weather

Prior ranking: sunny+warm is most normal (rank 0). Both rainy+warm and sunny+cold are mildly surprising (rank 1 each). Rainy+cold is most surprising (rank 2).

This prior satisfies Theorem 4's conditions for "sunny" × "warm": κ(sunny ∩ warm) = 0 and κ(rainy ∩ warm) = 0.

Equations

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

def Spohn1988.isSunny : Weather → Bool

Equations

• Spohn1988.isSunny w = (w == Spohn1988.Weather.sunny_warm || w == Spohn1988.Weather.sunny_cold)

def Spohn1988.isWarm : Weather → Bool

Equations

• Spohn1988.isWarm w = (w == Spohn1988.Weather.sunny_warm || w == Spohn1988.Weather.rainy_warm)

Conditioning on "sunny" with different firmness values α.

Prior ranks: sunny_warm=0, sunny_cold=1, rainy_warm=0, rainy_cold=2
κ(sunny) = min(0,1) = 0, κ(¬sunny) = min(0,2) = 0

A-part of sunny-worlds:  sunny_warm → 0-0=0, sunny_cold → 1-0=1
A-part of ¬sunny-worlds: rainy_warm → 0-0=0, rainy_cold → 2-0=2

conditionα with α:
  sunny_warm → 0, sunny_cold → 1,
  rainy_warm → α+0, rainy_cold → α+2

def Spohn1988.afterSunnyWeak : Core.Logic.Ranking.RankingFunction Weather

After weak evidence for "sunny" (hearsay, α = 1). Rainy worlds only slightly more disbelieved than before.

Equations

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

def Spohn1988.afterSunnyStrong : Core.Logic.Ranking.RankingFunction Weather

After strong evidence for "sunny" (direct observation, α = 3). Rainy worlds pushed far into disbelief.

Equations

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

theorem Spohn1988.strong_more_disbelief_rainy_warm : afterSunnyStrong.rank Weather.rainy_warm > afterSunnyWeak.rank Weather.rainy_warm

Strong evidence makes counter-evidence worlds more disbelieved.

theorem Spohn1988.strong_more_disbelief_rainy_cold : afterSunnyStrong.rank Weather.rainy_cold > afterSunnyWeak.rank Weather.rainy_cold

theorem Spohn1988.weak_preserves_belief : afterSunnyWeak.rank Weather.sunny_warm = 0

Both weak and strong evidence preserve the sunny belief (sunny_warm stays at rank 0).

theorem Spohn1988.strong_preserves_belief : afterSunnyStrong.rank Weather.sunny_warm = 0

theorem Spohn1988.weak_uncertain : afterSunnyWeak.rank Weather.rainy_warm = afterSunnyWeak.rank Weather.sunny_cold

With weak evidence, rainy_warm is equally plausible as sunny_cold (both rank 1) — the agent isn't confident.

theorem Spohn1988.strong_separates : afterSunnyStrong.rank Weather.rainy_warm > afterSunnyStrong.rank Weather.sunny_cold

With strong evidence, all rainy worlds are strictly less plausible than any sunny world.

Process "sunny" (α=2) then "warm" (β=1), and vice versa. Theorem 4 predicts identical results when κ(sunny∩warm)=0 and κ(¬sunny∩warm)=0 — both satisfied by our prior.

def Spohn1988.afterSunny2_thenWarm1 : Core.Logic.Ranking.RankingFunction Weather

After "sunny" (α=2) then "warm" (β=1).

Equations

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

def Spohn1988.afterWarm1_thenSunny2 : Core.Logic.Ranking.RankingFunction Weather

After "warm" (β=1) then "sunny" (α=2).

Equations

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

theorem Spohn1988.commutativity_ranks : afterSunny2_thenWarm1.rank = afterWarm1_thenSunny2.rank

Commutativity: processing order doesn't matter. Both sequences yield identical rankings on all worlds.

theorem Spohn1988.commutativity_verified : (afterSunny2_thenWarm1.rank Weather.sunny_warm, afterSunny2_thenWarm1.rank Weather.sunny_cold, afterSunny2_thenWarm1.rank Weather.rainy_warm, afterSunny2_thenWarm1.rank Weather.rainy_cold) = (0, 1, 2, 4)

Detailed verification: hand computation.

Step 1: prior → conditionα "sunny" α=2 κ(sunny) = 0; aPart sunny: sw→0, sc→1 κ(¬sunny) = 0; aPart ¬sunny: rw→0, rc→2 Result: sw=0, sc=1, rw=2+0=2, rc=2+2=4

Step 2: result → conditionα "warm" β=1 κ(warm) = min(0,2) = 0; aPart warm: sw→0, rw→2 κ(¬warm) = min(1,4) = 1; aPart ¬warm: sc→0, rc→3 Result: sw=0, rw=2, sc=1+0=1, rc=1+3=4

Reverse: prior → conditionα "warm" β=1 → conditionα "sunny" α=2

Step 1: prior → conditionα "warm" β=1 κ(warm) = min(0,0) = 0; aPart warm: sw→0, rw→0 κ(¬warm) = min(1,2) = 1; aPart ¬warm: sc→0, rc→1 Result: sw=0, rw=0, sc=1+0=1, rc=1+1=2

Step 2: result → conditionα "sunny" α=2 κ(sunny) = min(0,1) = 0; aPart sunny: sw→0, sc→1 κ(¬sunny) = min(0,2) = 0; aPart ¬sunny: rw→0, rc→2 Result: sw=0, sc=1, rw=2+0=2, rc=2+2=4

theorem Spohn1988.prior_connected : prior.toPlausibilityOrder.connected

The prior ranking induces a connected (total) plausibility ordering, refining any Kratzer-style ordering source with explicit disbelief grades. This is the structural connection between ranking functions and the 95+ files downstream of NormalityOrder.

theorem Spohn1988.prior_believes_sunny_warm : prior.rank Weather.sunny_warm = 0

The prior's belief set: sunny_warm is believed (rank 0). rainy_warm is also believed (rank 0 in this prior).

theorem Spohn1988.prior_believes_rainy_warm : prior.rank Weather.rainy_warm = 0

theorem Spohn1988.prior_disbelieves_sunny_cold : prior.rank Weather.sunny_cold ≠ 0

theorem Spohn1988.prior_disbelieves_rainy_cold : prior.rank Weather.rainy_cold ≠ 0

theorem Spohn1988.weak_evidence_revises : afterSunnyWeak.rank Weather.rainy_warm ≠ 0

After conditioning on "sunny" (even weakly), the belief set changes: rainy_warm is no longer rank 0.

@cite{spohn-1988} §7 observes that ranking functions are the ordinal analogue of probability measures. The structural parallel:

| Probability (ℚ, ·, Σ)     | Ranking (ℕ, min, +)          |
|---------------------------|------------------------------|
| P(A) = Σ_{w∈A} P(w)      | κ(A) = min_{w∈A} κ(w)       |
| P(A|B) = P(A∩B)/P(B)     | κ(w|A) = κ(w) - κ(A)        |
| P(A∩B) = P(A)·P(B) (ind) | κ(A∩B) = κ(A) + κ(B) (ind)  |

The exact homomorphism requires nonstandard probability (§7 uses
infinitesimal i with P(A) ~ i^{κ(A)}). For finite distributions,
the **ordering** is preserved: worlds with higher probability have
lower rank. We verify this concretely.

See `RSA.RankingBridge` for the formal
connection: `rankToPrior κ w = exp(-κ(w))` gives the exponential
prior, and `softmax_concentrates_unique` proves that softmax
with ranking scores concentrates on rank-0 worlds as α → ∞. 

def Spohn1988.priorWeight : Weather → ℕ

Probability weights compatible with the prior ranking. w(x) = 2^(max_rank - κ(x)), so higher rank → lower weight. These are proportional to probabilities P(x) = w(x)/Σw.

Equations

• Spohn1988.priorWeight Spohn1988.Weather.sunny_warm = 4
• Spohn1988.priorWeight Spohn1988.Weather.sunny_cold = 2
• Spohn1988.priorWeight Spohn1988.Weather.rainy_warm = 4
• Spohn1988.priorWeight Spohn1988.Weather.rainy_cold = 1

theorem Spohn1988.weight_rank_compatible (w v : Weather) : priorWeight w ≥ priorWeight v ↔ prior.rank w ≤ prior.rank v

Order compatibility: weight ordering reflects rank ordering on all pairs of worlds.

theorem Spohn1988.prior_dichotomy_sunny : prior.rank Weather.sunny_warm = 0 ∧ isSunny Weather.sunny_warm = true

Theorem 2(a) verified: for "sunny", either κ(sunny) = 0 or κ(¬sunny) = 0. In this prior, κ(sunny) = 0.

theorem Spohn1988.sunny_warm_independent : prior.rank Weather.sunny_warm = min (prior.rank Weather.sunny_warm) (prior.rank Weather.sunny_cold) + min (prior.rank Weather.sunny_warm) (prior.rank Weather.rainy_warm)

Independence under ranking: sunny and warm are independent. κ(sunny ∩ warm) = κ(sunny_warm) = 0 = κ(sunny) + κ(warm) = 0 + 0.