Goldszmidt & Pearl (1996): Qualitative Probabilities for Default Reasoning

[GP96]

This study demonstrates System Z — the constructive derivation of minimal ranking functions from a knowledge base of default rules. Where [Spo88] defines ranking functions as primitive objects, G&P show how to compute the unique minimal admissible ranking κ^z from a set of defaults, using tolerance-based stratification.

Key demonstrations

1. Tolerance stratification: Rules are partitioned by iteratively peeling off tolerated rules (Consistency-Test, Fig. 2). In the 3-rule subset of the Tweety scenario (r₁–r₃ from Example 17), "birds fly" is tolerated first (Z = 0), while "penguins are birds" and "penguins don't fly" are tolerated only after removing the first stratum (Z = 1).

2. κ^z ranking (Definition 12): The minimal admissible ranking assigns each world the lowest possible rank. Worlds verifying all rules get rank 0; worlds falsifying only low-priority rules get low ranks.

3. Specificity: More specific defaults automatically override general ones — penguinNoFly outranks penguinFlies because the penguin-specific rule has higher Z-priority.

Ranking Functions as RSA Limits

As the rationality parameter α → ∞, softmax-based probabilistic inference converges to ranking-based default reasoning ([Spo88], [FG12]). We formalize the substrate of this connection (rankToScore, softmax_concentrates_unique, condProb_tendsto_one) and apply it to the Tweety scenario: RSA with infinite rationality assigns probability 1 to the most normal worlds under κ^z.

Scenario

We formalize rules r₁–r₃ from Example 17 (the paper's full example has 5 rules including r₄: b→w and r₅: f→a, which would require extending TweetyWorld with wings/airborne features). The 3-rule subset is sufficient to demonstrate tolerance stratification, κ^z construction, admissibility, and specificity.

Knowledge Base (rules r₁–r₃ from Example 17)

def GoldszmidtPearl1996.r₁ : SystemZ.DefaultRule TweetyNixon.TweetyWorld

r₁: "Birds fly" (b → f).

Equations

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

def GoldszmidtPearl1996.r₂ : SystemZ.DefaultRule TweetyNixon.TweetyWorld

r₂: "Penguins are birds" (p → b). Strict: no world falsifies it in TweetyWorld since all penguins are birds by construction.

Equations

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

def GoldszmidtPearl1996.r₃ : SystemZ.DefaultRule TweetyNixon.TweetyWorld

r₃: "Penguins don't fly" (p → ¬f).

Equations

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

def GoldszmidtPearl1996.Δ_pb : SystemZ.KnowledgeBase TweetyNixon.TweetyWorld

The penguin-bird knowledge base Δ_pb (rules r₁–r₃).

Equations

• GoldszmidtPearl1996.Δ_pb = [GoldszmidtPearl1996.r₁, GoldszmidtPearl1996.r₂, GoldszmidtPearl1996.r₃]

Tolerance and Z-Ordering (Consistency-Test, Fig. 2)

Stratum 0: r₁ is tolerated by Δ_pb (birdFlies verifies r₁ and all material counterparts). r₂ and r₃ are not tolerated (no world satisfies their antecedent + consequent while also satisfying b → f as a material conditional).

Stratum 1: After removing r₁, both r₂ and r₃ are tolerated (penguinNoFly verifies both and satisfies the remaining material counterparts).

Z-priorities: Z(r₁) = 0, Z(r₂) = 1, Z(r₃) = 1.

theorem GoldszmidtPearl1996.r₁_tolerated_by_Δ : SystemZ.tolerated r₁ Δ_pb

theorem GoldszmidtPearl1996.r₂_not_tolerated_by_Δ : ¬SystemZ.tolerated r₂ Δ_pb

theorem GoldszmidtPearl1996.r₃_not_tolerated_by_Δ : ¬SystemZ.tolerated r₃ Δ_pb

def GoldszmidtPearl1996.Δ₁ : SystemZ.KnowledgeBase TweetyNixon.TweetyWorld

After removing stratum 0 (r₁), both r₂ and r₃ are tolerated.

Equations

• GoldszmidtPearl1996.Δ₁ = [GoldszmidtPearl1996.r₂, GoldszmidtPearl1996.r₃]

theorem GoldszmidtPearl1996.r₂_tolerated_by_Δ₁ : SystemZ.tolerated r₂ Δ₁

theorem GoldszmidtPearl1996.r₃_tolerated_by_Δ₁ : SystemZ.tolerated r₃ Δ₁

Minimal Ranking κ^z (Definition 12)

def GoldszmidtPearl1996.prioritized : List (SystemZ.DefaultRule TweetyNixon.TweetyWorld × ℕ)

Z-prioritized rules: Z(r₁) = 0, Z(r₂) = 1, Z(r₃) = 1.

Equations

• GoldszmidtPearl1996.prioritized = [(GoldszmidtPearl1996.r₁, 0), (GoldszmidtPearl1996.r₂, 1), (GoldszmidtPearl1996.r₃, 1)]

def GoldszmidtPearl1996.κ_z : RankingFunction TweetyNixon.TweetyWorld

The minimal ranking κ^z for the Tweety knowledge base.

κ^z values (Definition 12):

• birdFlies: falsifies nothing → 0
• birdNoFly: falsifies r₁ (Z=0) → max(0)+1 = 1
• penguinFlies: falsifies r₃ (Z=1) → max(1)+1 = 2
• penguinNoFly: falsifies r₁ (Z=0) → max(0)+1 = 1

Equations

• GoldszmidtPearl1996.κ_z = SystemZ.zRanking GoldszmidtPearl1996.prioritized GoldszmidtPearl1996.κ_z._proof_1

theorem GoldszmidtPearl1996.κz_birdFlies : κ_z.rank TweetyNixon.TweetyWorld.birdFlies = 0

theorem GoldszmidtPearl1996.κz_birdNoFly : κ_z.rank TweetyNixon.TweetyWorld.birdNoFly = 1

theorem GoldszmidtPearl1996.κz_penguinFlies : κ_z.rank TweetyNixon.TweetyWorld.penguinFlies = 2

theorem GoldszmidtPearl1996.κz_penguinNoFly : κ_z.rank TweetyNixon.TweetyWorld.penguinNoFly = 1

Admissibility Verification (Definition 2)

theorem GoldszmidtPearl1996.r₁_admissible (w : TweetyNixon.TweetyWorld) : r₁.falsified w → ∃ (v : TweetyNixon.TweetyWorld), r₁.ante v ∧ r₁.cons v ∧ κ_z.rank v < κ_z.rank w

r₁ (b → f) is admissible: every world falsifying it (birdNoFly, penguinNoFly, both rank 1) is outranked by birdFlies (rank 0).

theorem GoldszmidtPearl1996.r₂_admissible (w : TweetyNixon.TweetyWorld) : r₂.falsified w → ∃ (v : TweetyNixon.TweetyWorld), r₂.ante v ∧ r₂.cons v ∧ κ_z.rank v < κ_z.rank w

r₂ (p → b) is vacuously admissible: no world falsifies it.

theorem GoldszmidtPearl1996.r₃_admissible (w : TweetyNixon.TweetyWorld) : r₃.falsified w → ∃ (v : TweetyNixon.TweetyWorld), r₃.ante v ∧ r₃.cons v ∧ κ_z.rank v < κ_z.rank w

r₃ (p → ¬f) is admissible: the only falsifying world is penguinFlies (rank 2), outranked by penguinNoFly (rank 1).

theorem GoldszmidtPearl1996.κz_admissible : SystemZ.admissible κ_z Δ_pb

κ^z is admissible relative to the full knowledge base Δ_pb (Definition 2).

Entailment Queries

z-entailment queries on Δ_pb. These cover two of the five queries in Table 2 (the remaining three — red birds fly, birds airborne, penguins winged — require r₄/r₅ and a richer world type).

theorem GoldszmidtPearl1996.penguin_birds_dont_fly : SystemZ.rankEntails κ_z (fun (w : TweetyNixon.TweetyWorld) => TweetyNixon.isPenguin w ∧ TweetyNixon.isBird w) fun (w : TweetyNixon.TweetyWorld) => ¬TweetyNixon.flies w

"Do penguin-birds fly?" → NO (z-entailment). penguinNoFly (rank 1) outranks penguinFlies (rank 2). The more specific default wins.

theorem GoldszmidtPearl1996.birds_not_typically_penguins : ¬SystemZ.rankEntails κ_z TweetyNixon.isBird TweetyNixon.isPenguin

"Are birds typically penguins?" → NO (z-entailment). birdFlies (rank 0) is a non-penguin bird, outranking all penguin worlds.

theorem GoldszmidtPearl1996.birds_fly : SystemZ.rankEntails κ_z TweetyNixon.isBird TweetyNixon.flies

"Do birds fly?" → YES (z-entailment). birdFlies (rank 0) is the most normal bird world and it flies.

Specificity

theorem GoldszmidtPearl1996.specificity_penguinNoFly_beats_penguinFlies : κ_z.rank TweetyNixon.TweetyWorld.penguinNoFly < κ_z.rank TweetyNixon.TweetyWorld.penguinFlies

The κ^z ranking makes penguinNoFly strictly more plausible than penguinFlies.

theorem GoldszmidtPearl1996.general_default_preserved : κ_z.rank TweetyNixon.TweetyWorld.birdFlies < κ_z.rank TweetyNixon.TweetyWorld.birdNoFly

The κ^z ranking preserves the general default: among non-penguin birds, flying is more normal than not flying.

theorem GoldszmidtPearl1996.κz_connected : Core.Order.Normality.connected κ_z.toPlausibilityOrder.toPreorder

The induced plausibility ordering is connected (total), so Rational Monotonicity holds.

RSA Bridge Substrate: Rankings as Softmax Limits

[Spo88] §7 observes that rankings are ordinal probabilities: κ(w) = n corresponds to P(w) ∝ ε^n for infinitesimal ε. The finite analogue replaces ε^n with exp(-n·α) for large α:

softmax(-κ, α)(w) = exp(-α · κ(w)) / Σ_v exp(-α · κ(v))

As α → ∞, this concentrates on rank-0 (most normal) worlds — exactly the worlds that survive ranking-based default reasoning. This makes System Z's κ^z the "infinite rationality" limit of RSA pragmatic inference ([FG12]). Qualitative default reasoning and quantitative Bayesian pragmatics are not rival frameworks but endpoints of the same rationality continuum.

Ranking Functions as Score Functions

noncomputable def GoldszmidtPearl1996.rankToScore {W : Type u_1} (κ : RankingFunction W) : W → ℝ

Convert a ranking function to softmax scores.

s(w) = -(κ(w) : ℝ). Lower rank → higher score → more plausible.

This is the finite analogue of [Spo88] §7's P(w) ∝ ε^{κ(w)}: here exp(α · s(w)) = exp(-α · κ(w)) plays the role of ε^{κ(w)} with ε = exp(-α).

Equations

• GoldszmidtPearl1996.rankToScore κ w = -↑(κ.rank w)

theorem GoldszmidtPearl1996.rankToScore_lt_iff {W : Type u_1} (κ : RankingFunction W) (w v : W) : rankToScore κ w < rankToScore κ v ↔ κ.rank v < κ.rank w

rankToScore reverses the ordering: higher rank ↔ lower score.

theorem GoldszmidtPearl1996.rankToScore_eq_zero_iff {W : Type u_1} (κ : RankingFunction W) (w : W) : rankToScore κ w = 0 ↔ κ.rank w = 0

Rank-0 worlds achieve the maximum score (0).

theorem GoldszmidtPearl1996.rankToScore_nonpos {W : Type u_1} (κ : RankingFunction W) (w : W) : rankToScore κ w ≤ 0

All scores are non-positive.

theorem GoldszmidtPearl1996.rankToScore_le_of_rank_zero {W : Type u_1} (κ : RankingFunction W) (w₀ v : W) (h : κ.rank w₀ = 0) : rankToScore κ v ≤ rankToScore κ w₀

Rank-0 worlds maximize the score.

Softmax Concentration on Normal Worlds

theorem GoldszmidtPearl1996.softmax_concentrates_unique {W : Type u_1} [Fintype W] [DecidableEq W] [Nonempty W] (κ : RankingFunction W) (w₀ : W) (h_zero : κ.rank w₀ = 0) (h_unique : ∀ (v : W), v ≠ w₀ → 0 < κ.rank v) (w : W) : Filter.Tendsto (fun (α : ℝ) => softmax (α • rankToScore κ) w) Filter.atTop (nhds (if w = w₀ then 1 else 0))

When κ has a unique rank-0 world, softmax(rankToScore κ, α) concentrates on it as α → ∞.

This is the core convergence result: the probabilistic distribution approaches a point mass on the most normal world, recovering the ranking-based notion of normality.

Proof: Apply Softmax.tendsto_softmax_infty_unique_max with scores s = rankToScore κ. The unique rank-0 world maximizes s (since s(w) = -κ(w) and κ(w₀) = 0 < κ(v) for v ≠ w₀).

theorem GoldszmidtPearl1996.entropy_vanishes_unique {W : Type u_1} [Fintype W] [DecidableEq W] [Nonempty W] (κ : RankingFunction W) (w₀ : W) (h_zero : κ.rank w₀ = 0) (h_unique : ∀ (v : W), v ≠ w₀ → 0 < κ.rank v) : Filter.Tendsto (fun (α : ℝ) => Softmax.entropy (softmax (α • rankToScore κ))) Filter.atTop (nhds 0)

Entropy of softmax(rankToScore κ, α) → 0 as α → ∞ (unique rank-0 case). The distribution becomes maximally concentrated.

Ranking Entailment via Minimum Rank

theorem GoldszmidtPearl1996.rankEntails_iff_minRank_lt {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ σ : W → Prop) [DecidablePred φ] [DecidablePred σ] [DecidablePred fun (w : W) => φ w ∧ σ w] (hφσ : ∃ (w : W), φ w ∧ σ w) : SystemZ.rankEntails κ φ σ ↔ ∀ (w : W), φ w → ¬σ w → κ.rankProp (fun (v : W) => φ v ∧ σ v) hφσ < κ.rank w

rankEntails is equivalent to: every φ∧¬σ world has strictly higher rank than some φ∧σ world.

When φ∧σ is non-empty, this is the same as: the minimum rank among φ∧σ worlds is strictly less than the rank of every φ∧¬σ world. When φ∧¬σ is empty, rankEntails holds vacuously.

theorem GoldszmidtPearl1996.minRank_worlds_satisfy {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ σ : W → Prop) [DecidablePred φ] [DecidablePred σ] (h : SystemZ.rankEntails κ φ σ) (hφ : ∃ (w : W), φ w) (w : W) : φ w → κ.rank w = κ.rankProp φ hφ → σ w

Under ranking entailment, all minimum-rank φ-worlds satisfy σ.

This is the key lemma connecting ranking entailment to softmax concentration: as α → ∞, softmax concentrates on minimum-rank worlds. If all minimum-rank φ-worlds satisfy σ, then the limiting conditional probability P(σ|φ) = 1.

Proof: If a minimum-rank φ-world w fails σ, then rankEntails gives a φ∧σ world v with κ(v) < κ(w), contradicting w having the minimum rank among φ-worlds.

The Rationality Continuum

The theorems above establish the formal bridge between RSA and ranking-based default reasoning:

α = 0          α finite           α → ∞
uniform ←——— softmax(s, α) ———→ hardmax
no inference   RSA pragmatics     ranking entailment

At α = 0, the listener has no rationality assumption and the posterior is uniform (Softmax.tendsto_softmax_zero). At finite α, the listener performs soft Bayesian inference (standard RSA). As α → ∞, the posterior concentrates on the most normal worlds (softmax_concentrates_unique), and inference becomes ranking entailment.

This justifies two practices:

1. RSA modelers can use System Z rankings as the "skeleton" of their prior, softened by finite α for gradient predictions.
2. Default reasoning theorists can view their qualitative inferences as the limiting case of probabilistic pragmatics.

noncomputable def GoldszmidtPearl1996.rankToPrior {W : Type u_1} (κ : RankingFunction W) : W → ℝ

The exponential prior induced by a ranking function.

P(w) = exp(-κ(w)). This is the natural prior for connecting ranking functions to Bayesian inference: rank-0 worlds get maximal prior probability, and the prior ordering on worlds matches the ranking ordering.

[Spo88] §7 uses P(w) ∝ ε^{κ(w)} with ε infinitesimal; here we use the concrete parameterization exp(-κ(w)).

Equations

• GoldszmidtPearl1996.rankToPrior κ w = Real.exp (-↑(κ.rank w))

theorem GoldszmidtPearl1996.rankToPrior_pos {W : Type u_1} (κ : RankingFunction W) (w : W) : 0 < rankToPrior κ w

The exponential prior is always positive.

theorem GoldszmidtPearl1996.rankToPrior_nonneg {W : Type u_1} (κ : RankingFunction W) (w : W) : 0 ≤ rankToPrior κ w

The exponential prior is non-negative.

theorem GoldszmidtPearl1996.rankToPrior_max_of_rank_zero {W : Type u_1} (κ : RankingFunction W) (w₀ v : W) (h : κ.rank w₀ = 0) : rankToPrior κ v ≤ rankToPrior κ w₀

Rank-0 worlds maximize the exponential prior.

theorem GoldszmidtPearl1996.rankToPrior_lt_iff {W : Type u_1} (κ : RankingFunction W) (w v : W) : rankToPrior κ w < rankToPrior κ v ↔ κ.rank v < κ.rank w

The exponential prior preserves the rank ordering: lower rank ↔ higher prior.

Rankings as Limiting Priors

An RSA chain with world prior rankToPrior κ and boolean meaning computes L1 posteriors that concentrate on the minimum-rank worlds in the support of the utterance as α → ∞.

Specifically, for an utterance u with boolean denotation ⟦u⟧:

• L1(w|u) ∝ rankToPrior(κ, w) · S1(u|w)
• As α → ∞, S1 concentrates on the most informative true utterance
• The prior rankToPrior(κ, ·) breaks ties among equally informative utterances in favor of lower-rank worlds
• The net effect: L1 concentrates on minimum-rank ⟦u⟧-worlds

This is exactly what rankEntails κ ⟦u⟧ σ characterizes: the most normal worlds satisfying the utterance also satisfy σ.

The conditional limit theorem condProb_tendsto_one below formalizes this precisely: P_α(σ|φ) → 1 as α → ∞ whenever κ ⊨ φ → σ.

theorem GoldszmidtPearl1996.softmax_rankToScore_eq_normalized_prior {W : Type u_1} [Fintype W] [Nonempty W] (κ : RankingFunction W) (w : W) : softmax (rankToScore κ) w = rankToPrior κ w / ∑ v : W, rankToPrior κ v

The softmax distribution with ranking scores is exactly the exponential prior (up to normalization).

softmax(rankToScore κ, 1)(w) = exp(-κ(w)) / Σ_v exp(-κ(v)) = rankToPrior(κ, w) / Σ_v rankToPrior(κ, v)

At α = 1, softmax with ranking scores IS the normalized exponential prior. At other α, it's a tempered version: softmax(rankToScore κ, α)(w) = exp(-α·κ(w)) / Σ_v exp(-α·κ(v)).

The Exact Tropical Homomorphism ([Spo88] §7)

[Spo88] §7 observes that ranking functions are the ordinal analogue of probability measures. This is not an analogy — it is an exact algebraic identity via the tropical semiring.

The tropical semiring Tropical ℕ has:

• Addition = min (the rank of a disjunction)
• Multiplication = + (the rank of a conjunction under independence)

The map ε^{·} (for 0 < ε < 1) is a homomorphism from the tropical semiring to (ℝ₊, max, ×):

• ε^{a * b} = ε^{a + b} = ε^a · ε^b (tropical × → real ×)
• ε^{a + b} = ε^{min(a,b)} = max(ε^a, ε^b) (tropical + → real max)

The only "approximation" is that real addition (Σ) approximates max in the ε → 0 limit. This is the dequantization: as ε → 0 (α → ∞), the sum Σ_w ε^{κ(w)} is dominated by its largest term max_w ε^{κ(w)}, and probabilistic inference degenerates to tropical (ranking) algebra.

theorem GoldszmidtPearl1996.exp_tropical_mul (ε : ℝ) (a b : Tropical ℕ) : ε ^ Tropical.untrop (a * b) = ε ^ Tropical.untrop a * ε ^ Tropical.untrop b

The exponential map sends tropical multiplication (= underlying +) to real multiplication: ε^{a ×_trop b} = ε^{a + b} = ε^a · ε^b.

This is exact, not approximate. It formalizes [Spo88] §7's observation that ranking independence (κ(A∩B) = κ(A) + κ(B)) corresponds to probabilistic independence (P(A∩B) = P(A)·P(B)).

theorem GoldszmidtPearl1996.exp_tropical_add (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (a b : Tropical ℕ) : ε ^ Tropical.untrop (a + b) = max (ε ^ Tropical.untrop a) (ε ^ Tropical.untrop b)

The exponential map sends tropical addition (= min) to real max: ε^{a +_trop b} = ε^{min(a,b)} = max(ε^a, ε^b) for 0 < ε ≤ 1.

This formalizes [Spo88] §7's observation that ranking disjunction (κ(A∪B) = min(κ(A), κ(B))) corresponds to the dominant term in P(A∪B) = P(A) + P(B) − P(A∩B).

theorem GoldszmidtPearl1996.independent_iff_tropical_mul {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ ψ : W → Prop) [DecidablePred φ] [DecidablePred ψ] [DecidablePred fun (w : W) => φ w ∧ ψ w] (hφ : ∃ (w : W), φ w) (hψ : ∃ (w : W), ψ w) (hφψ : ∃ (w : W), φ w ∧ ψ w) : κ.independent φ ψ hφ hψ hφψ ↔ Tropical.trop (κ.rankProp (fun (w : W) => φ w ∧ ψ w) hφψ) = Tropical.trop (κ.rankProp φ hφ) * Tropical.trop (κ.rankProp ψ hψ)

Ranking independence is tropical multiplicativity.

κ(φ ∧ ψ) = κ(φ) + κ(ψ) ↔ trop(κ(φ∧ψ)) = trop(κ(φ)) ×_trop trop(κ(ψ))

This is not an analogy: "P(A∩B) = P(A)·P(B)" and "κ(A∩B) = κ(A)+κ(B)" are literally the same equation in two semirings.

theorem GoldszmidtPearl1996.softmax_eq_tropical_ratio {W : Type u_1} [Fintype W] [Nonempty W] (κ : RankingFunction W) (α : ℝ) (w : W) : softmax (α • rankToScore κ) w = Real.exp (-α) ^ κ.rank w / ∑ v : W, Real.exp (-α) ^ κ.rank v

The softmax distribution is the tropical-to-probabilistic functor applied to ranking values, with ε = exp(-α).

softmax(-κ, α)(w) = exp(-α·κ(w)) / Σ_v exp(-α·κ(v)) = ε^{κ(w)} / Σ_v ε^{κ(v)} where ε = exp(-α)

As ε → 0 (α → ∞), the normalizing sum Σ_v ε^{κ(v)} is dominated by its largest term ε^{min_v κ(v)} = ε^0 = 1 (for rank-0 worlds). In this limit, the probabilistic sum degenerates to the tropical sum, and Bayesian inference becomes ranking-based reasoning.

Conditional Softmax Limit Theorem

The conditional limit theorem: as α → ∞, the conditional probability P_α(σ|φ) → 1 whenever ranking entailment κ ⊨ φ → σ holds.

This completes the RSA–ranking bridge:

• Softmax concentration shows the prior concentrates on rank-0 worlds
• The conditional limit shows the posterior (conditioned on φ) concentrates on σ-worlds

The proof uses exponential decay of non-minimal-rank worlds: under ranking entailment, every φ∧¬σ world has rank strictly above the minimum-rank φ∧σ world, so its softmax weight decays exponentially faster, driving P(σ|φ) → 1.

theorem GoldszmidtPearl1996.rankEntails_exists_sat {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ σ : W → Prop) [DecidablePred φ] [DecidablePred σ] (h : SystemZ.rankEntails κ φ σ) (hφ : ∃ (w : W), φ w) : ∃ (w : W), φ w ∧ σ w

rankEntails implies the existence of a φ∧σ witness.

noncomputable def GoldszmidtPearl1996.condProb {W : Type u_1} [Fintype W] (s : W → ℝ) (α : ℝ) (φ σ : W → Prop) [DecidablePred φ] [DecidablePred σ] [DecidablePred fun (w : W) => φ w ∧ σ w] : ℝ

Conditional probability of σ given φ under scores s at rationality α. P_α(σ|φ) = Σ_{w: φ∧σ} exp(α·s(w)) / Σ_{w: φ} exp(α·s(w))

Equations

• GoldszmidtPearl1996.condProb s α φ σ = (∑ w : W with φ w ∧ σ w, Real.exp (α * s w)) / ∑ w : W with φ w, Real.exp (α * s w)

theorem GoldszmidtPearl1996.condProb_tendsto_one {W : Type u_1} [Fintype W] [DecidableEq W] (κ : RankingFunction W) (φ σ : W → Prop) [DecidablePred φ] [DecidablePred σ] (h : SystemZ.rankEntails κ φ σ) (hφ : ∃ (w : W), φ w) : Filter.Tendsto (fun (α : ℝ) => condProb (rankToScore κ) α φ σ) Filter.atTop (nhds 1)

Conditional Softmax Limit Theorem. Under ranking entailment κ ⊨ φ → σ, the conditional probability P_α(σ|φ) converges to 1 as α → ∞.

This is the central theorem connecting RSA to default reasoning: an RSA listener with ranking-derived scores and infinite rationality draws exactly the conclusions that ranking entailment sanctions.

Bridge to RSA: κ^z as Infinite-Rationality Limit

[FG12]'s RSA framework uses softmax-based Bayesian inference with a finite rationality parameter α. [GP96]'s System Z uses ranking functions for qualitative default reasoning.

The two frameworks are endpoints of the same continuum: as α → ∞, softmax concentrates on the most normal (rank-0) worlds, recovering ranking-based entailment from probabilistic inference.

We demonstrate this concretely: the softmax distribution with scores derived from κ^z concentrates on birdFlies (the unique rank-0 world) as α → ∞. This means RSA's pragmatic listener with infinite rationality reasons exactly like System Z.

instance GoldszmidtPearl1996.instNonemptyTweetyWorld : Nonempty TweetyNixon.TweetyWorld

theorem GoldszmidtPearl1996.κz_unique_rank_zero (v : TweetyNixon.TweetyWorld) : v ≠ TweetyNixon.TweetyWorld.birdFlies → 0 < κ_z.rank v

birdFlies is the unique rank-0 world under κ^z.

theorem GoldszmidtPearl1996.κz_softmax_concentrates (w : TweetyNixon.TweetyWorld) : Filter.Tendsto (fun (α : ℝ) => softmax (α • rankToScore κ_z) w) Filter.atTop (nhds (if w = TweetyNixon.TweetyWorld.birdFlies then 1 else 0))

The softmax distribution softmax(-κ^z, α) concentrates on birdFlies as α → ∞. This is the core RSA–ranking bridge for the Tweety scenario: an RSA listener with infinite rationality assigns probability 1 to the most normal world.

theorem GoldszmidtPearl1996.minRank_birds_fly (w : TweetyNixon.TweetyWorld) : TweetyNixon.isBird w → κ_z.rank w = κ_z.rankProp TweetyNixon.isBird ⋯ → TweetyNixon.flies w

Under κ^z, all minimum-rank bird-worlds fly. This connects the ranking entailment birds_fly to the softmax limit: as α → ∞, the softmax listener restricted to bird-worlds assigns all probability to flying worlds.

theorem GoldszmidtPearl1996.minRank_penguins_dont_fly (w : TweetyNixon.TweetyWorld) : TweetyNixon.isPenguin w ∧ TweetyNixon.isBird w → κ_z.rank w = κ_z.rankProp (fun (w : TweetyNixon.TweetyWorld) => TweetyNixon.isPenguin w ∧ TweetyNixon.isBird w) ⋯ → ¬TweetyNixon.flies w

Under κ^z, all minimum-rank penguin-worlds don't fly. The specificity result — penguins override the general bird default — is precisely the α → ∞ limit of RSA inference restricted to the penguin domain.

theorem GoldszmidtPearl1996.condProb_birds_fly : Filter.Tendsto (fun (α : ℝ) => condProb (rankToScore κ_z) α TweetyNixon.isBird TweetyNixon.flies) Filter.atTop (nhds 1)

Conditional limit: "Do birds fly?" → probability 1. As α → ∞, the conditional probability P_α(flies|bird) → 1 under κ^z scores. This is the full conditional softmax limit theorem applied to the Tweety scenario.

theorem GoldszmidtPearl1996.condProb_penguins_dont_fly : Filter.Tendsto (fun (α : ℝ) => condProb (rankToScore κ_z) α (fun (w : TweetyNixon.TweetyWorld) => TweetyNixon.isPenguin w ∧ TweetyNixon.isBird w) fun (w : TweetyNixon.TweetyWorld) => ¬TweetyNixon.flies w) Filter.atTop (nhds 1)

Conditional limit: "Do penguin-birds fly?" → probability 0. As α → ∞, the conditional probability P_α(flies|penguin∧bird) → 0, because ranking entailment says penguin-birds don't fly. We prove this by showing P_α(¬flies|penguin∧bird) → 1.

Computed Consistency-Test

theorem GoldszmidtPearl1996.Δ_pb_computed : List.map Prod.snd (SystemZ.zPriorities Δ_pb) = [0, 1, 1]

The Consistency-Test (Fig. 2) computes the same Z-priorities as our manually-verified prioritized list: Z(r₁)=0, Z(r₂)=1, Z(r₃)=1.

System Z⁺: Variable-Strength Defaults (Definition 18)

System Z⁺ augments each rule with a strength parameter δ, requiring a wider gap between verifying and falsifying worlds. The Z⁺-priority of a rule accounts for δ, giving stronger rules higher priority and thus wider separation in the ranking.

def GoldszmidtPearl1996.sr₁ : SystemZ.StrengthRule TweetyNixon.TweetyWorld

Strength-augmented rules: δ₁=1, δ₂=1, δ₃=2. "Penguins don't fly" (r₃) is strongest.

Equations

• GoldszmidtPearl1996.sr₁ = { toDefaultRule := GoldszmidtPearl1996.r₁, strength := 1 }

def GoldszmidtPearl1996.sr₂ : SystemZ.StrengthRule TweetyNixon.TweetyWorld

Equations

• GoldszmidtPearl1996.sr₂ = { toDefaultRule := GoldszmidtPearl1996.r₂, strength := 1 }

def GoldszmidtPearl1996.sr₃ : SystemZ.StrengthRule TweetyNixon.TweetyWorld

Equations

• GoldszmidtPearl1996.sr₃ = { toDefaultRule := GoldszmidtPearl1996.r₃, strength := 2 }

def GoldszmidtPearl1996.Δ_pb_plus : SystemZ.StrengthKB TweetyNixon.TweetyWorld

Equations

• GoldszmidtPearl1996.Δ_pb_plus = [GoldszmidtPearl1996.sr₁, GoldszmidtPearl1996.sr₂, GoldszmidtPearl1996.sr₃]

def GoldszmidtPearl1996.zPlus_prioritized : List (SystemZ.DefaultRule TweetyNixon.TweetyWorld × ℕ)

Z⁺ priorities computed via the Z⁺_order procedure (Fig. 4) to satisfy δ-admissibility constraints. z⁺(r₁) = 1, z⁺(r₂) = 3, z⁺(r₃) = 4.

The constraint for r₃ (δ=2) is κ(penguinNoFly) + 2 < κ(penguinFlies). Since penguinNoFly falsifies r₁ giving rank z⁺(r₁)+1 = 2, we need 2 + 2 < z⁺(r₃) + 1, so z⁺(r₃) ≥ 4.

Note: z⁺(r₂) = 3 because the verifying world for r₂ (penguinNoFly) has κ = z⁺(r₁) + 1 = 2, so z⁺(r₂) = 2 + δ₂ = 2 + 1 = 3. r₂ is never falsified in TweetyWorld, so its priority doesn't affect ranks.

Equations

• GoldszmidtPearl1996.zPlus_prioritized = [(GoldszmidtPearl1996.r₁, 1), (GoldszmidtPearl1996.r₂, 3), (GoldszmidtPearl1996.r₃, 4)]

def GoldszmidtPearl1996.κ_plus : RankingFunction TweetyNixon.TweetyWorld

κ⁺: the Z⁺ ranking with wider gaps than κ^z.

• birdFlies: falsifies nothing → 0
• birdNoFly: falsifies r₁ (z⁺=1) → 2
• penguinFlies: falsifies r₃ (z⁺=4) → 5
• penguinNoFly: falsifies r₁ (z⁺=1) → 2

Equations

• GoldszmidtPearl1996.κ_plus = SystemZ.zRanking GoldszmidtPearl1996.zPlus_prioritized GoldszmidtPearl1996.κ_plus._proof_1

theorem GoldszmidtPearl1996.κplus_birdFlies : κ_plus.rank TweetyNixon.TweetyWorld.birdFlies = 0

theorem GoldszmidtPearl1996.κplus_birdNoFly : κ_plus.rank TweetyNixon.TweetyWorld.birdNoFly = 2

theorem GoldszmidtPearl1996.κplus_penguinFlies : κ_plus.rank TweetyNixon.TweetyWorld.penguinFlies = 5

theorem GoldszmidtPearl1996.κplus_penguinNoFly : κ_plus.rank TweetyNixon.TweetyWorld.penguinNoFly = 2

theorem GoldszmidtPearl1996.κplus_strength_admissible : SystemZ.strengthAdmissible κ_plus Δ_pb_plus

κ⁺ is δ-admissible relative to the strength rules.

theorem GoldszmidtPearl1996.κz_gap_too_small_for_sr₃ : κ_z.rank TweetyNixon.TweetyWorld.penguinNoFly + sr₃.strength ≥ κ_z.rank TweetyNixon.TweetyWorld.penguinFlies

κ^z's gap for r₃ is too small for δ₃=2: 1 + 2 ≥ 2. This motivates Z⁺ — the minimal ranking κ^z doesn't provide enough separation for variable-strength defaults.