Goldszmidt and Pearl (1996): Qualitative Probabilities for Default Reasoning, Belief Revision, and Causal Modeling

This file formalizes the default-reasoning core of Goldszmidt and Pearl's paper, system Z and its variable-strength extension system Z⁺. A ranking function (Spohn's ordinal conditional function, read as the order of magnitude of an infinitesimal probability) is admissible for a knowledge base of rules φ → ψ when every world falsifying a rule is outranked by one verifying it. A rule is tolerated by the base when some world verifies it together with the material counterparts of all the rules; the Consistency-Test peels off the tolerated rules stratum by stratum, a stratum's index is the Z-priority of its rules, and the ranking κᶻ gives a world one more than the highest priority it falsifies. Two consequence relations are compared on the paper's Example 17: the cautious p-entailment, which holds in every admissible ranking, and z-entailment, which holds in κᶻ. Entailment in a ranking is the rational consequence relation RankingFunction.Entails, and a ranking is admissible exactly when it entails every rule. Rational monotony, in the sense of Lehmann and Magidor, holds in each admissible ranking, so z-entailment has it, while p-entailment is preferential but not rational (not_isRational_pEntails). Table 2's verdicts are theorems: z-entailment sanctions rule chaining and the discounting of an irrelevant feature where p-entailment is undecided (z_birds_airborne, p_birds_airborne_undecided), and neither inherits wings to the exceptional penguins.

System Z⁺ attaches a strength δ to each rule and asks a verifying world to lie δ + 1 ranks below every falsifying one. The coupled equations of the ranking κ⁺ and the priorities Z⁺ are satisfied by the priorities the paper computes for Example 24 under every choice of strengths (isZPlusOrdering_example24); penguins inherit wings exactly when the wing rule is firmer than the flying rule (zPlus_penguins_winged_iff), and the Nixon diamond of Example 26 is decided by the relative strengths alone (nixon_pacifist_iff).

Soft evidence for a proposition is read in two ways. A Type-J report fixes the final belief, and is Spohn's conditionalization RankingFunction.conditionα (Eq. (25)), which keeps the ranks given the proposition and given its negation and so ranks every proposition by Jeffrey's rule, Eq. (24) (RankingFunction.rank_conditionα_eq). A Type-L report shifts the belief by the evidence's strength: L-conditioning lifts the worlds outside the proposition by the strength and renormalizes. It commutes, and two reports for one proposition add their strengths (lCondition_comm, lCondition_lCondition). Its world ranks are those of Eq. (32), and it is Type-J conditioning at the firmness Eq. (30) gives the negation (lCondition_eq_conditionα). On the party of Example 28 the Type-L reading reproduces Fig. 6, while the Type-J reading leaves Mary's going at rank 1 where the paper reports 2 (typeJ_bill).

Implementation notes

Worlds are the truth assignments to the atoms of each example, given a Fintype instance through the product of Booleans so that tolerance, admissibility, and entailment decide. Uniqueness and minimality of κᶻ and κ⁺ (Theorems 16 and 21), the complexity analysis of soft evidence, and the paper's sections on belief revision and causal networks are not formalized.

References

• M. Goldszmidt and J. Pearl, Qualitative Probabilities for Default Reasoning, Belief Revision, and Causal Modeling (1996)
• W. Spohn, Ordinal Conditional Functions: A Dynamic Theory of Epistemic States (1988)
• D. Lehmann and M. Magidor, What Does a Conditional Knowledge Base Entail? (1992)
• E. W. Adams, The Logic of Conditionals: An Application of Probability to Deductive Logic (1975)

structure GoldszmidtPearl1996.Rule (W : Type u_2) : Type u_2

A default rule "if φ then normally ψ" on decidable predicates.

• ante : W → Prop
• cons : W → Prop
• decAnte : DecidablePred self.ante
• decCons : DecidablePred self.cons

def GoldszmidtPearl1996.Rule.Verified {W : Type u_1} (r : Rule W) (x : W) : Prop

The world satisfies the material counterpart φ ⊃ ψ of the rule.

Equations

• r.Verified x = (r.ante x → r.cons x)

def GoldszmidtPearl1996.Rule.Falsified {W : Type u_1} (r : Rule W) (x : W) : Prop

The world satisfies φ ∧ ¬ψ.

Equations

• r.Falsified x = (r.ante x ∧ ¬r.cons x)

@[instance_reducible]

instance GoldszmidtPearl1996.Rule.instDecidableVerified {W : Type u_1} (r : Rule W) (x : W) : Decidable (r.Verified x)

Equations

• r.instDecidableVerified x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.Rule.instDecidableFalsified {W : Type u_1} (r : Rule W) (x : W) : Decidable (r.Falsified x)

Equations

• r.instDecidableFalsified x = id inferInstance

@[reducible, inline]

abbrev GoldszmidtPearl1996.KnowledgeBase (W : Type u_2) : Type u_2

A knowledge base is a list of rules.

Equations

• GoldszmidtPearl1996.KnowledgeBase W = List (GoldszmidtPearl1996.Rule W)

def GoldszmidtPearl1996.Admissible {W : Type u_1} (κ : RankingFunction W) (Δ : KnowledgeBase W) : Prop

A ranking is admissible for the base when every world falsifying a rule is outranked by a world verifying it, so that κ(φ ∧ ψ) < κ(φ ∧ ¬ψ) (Definition 2).

Equations

• GoldszmidtPearl1996.Admissible κ Δ = ∀ r ∈ Δ, ∀ (x : W), r.Falsified x → ∃ (y : W), r.ante y ∧ r.cons y ∧ κ y < κ x

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidableAdmissibleOfFintype {W : Type u_1} [Fintype W] (κ : RankingFunction W) (Δ : KnowledgeBase W) : Decidable (Admissible κ Δ)

Equations

• GoldszmidtPearl1996.instDecidableAdmissibleOfFintype κ Δ = id inferInstance

theorem GoldszmidtPearl1996.Admissible.mono {W : Type u_1} {κ : RankingFunction W} {Δ Δ' : KnowledgeBase W} (h : Δ ⊆ Δ') (hκ : Admissible κ Δ') : Admissible κ Δ

def GoldszmidtPearl1996.Tolerated {W : Type u_1} (r : Rule W) (Δ : KnowledgeBase W) : Prop

A rule is tolerated by the base when some world verifies it together with the material counterparts of every rule of the base (Definition 3).

Equations

• GoldszmidtPearl1996.Tolerated r Δ = ∃ (x : W), r.ante x ∧ r.cons x ∧ ∀ r' ∈ Δ, r'.Verified x

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidableToleratedOfFintype {W : Type u_1} [Fintype W] (r : Rule W) (Δ : KnowledgeBase W) : Decidable (Tolerated r Δ)

Equations

• GoldszmidtPearl1996.instDecidableToleratedOfFintype r Δ = id inferInstance

def GoldszmidtPearl1996.zPrioritiesAux {W : Type u_1} [Fintype W] : ℕ → KnowledgeBase W → ℕ → List (Rule W × ℕ)

The Consistency-Test (Fig. 2) peels off the rules tolerated by what remains, stratum by stratum, and a stratum's index is the Z-priority of its rules. Each stratum of a consistent base removes a rule, so the number of rules bounds the iteration; rules that are never tolerated stay in the last stratum.

Equations

• One or more equations did not get rendered due to their size.
• GoldszmidtPearl1996.zPrioritiesAux x✝¹ [] x✝ = []
• GoldszmidtPearl1996.zPrioritiesAux 0 x✝¹ x✝ = List.map (fun (x : GoldszmidtPearl1996.Rule W) => (x, x✝)) x✝¹

def GoldszmidtPearl1996.zPriorities {W : Type u_1} [Fintype W] (Δ : KnowledgeBase W) : List (Rule W × ℕ)

The Z-priorities of a base, by the Consistency-Test.

Equations

• GoldszmidtPearl1996.zPriorities Δ = GoldszmidtPearl1996.zPrioritiesAux (List.length Δ) Δ 0

def GoldszmidtPearl1996.zRank {W : Type u_1} (rules : List (Rule W × ℕ)) (x : W) : ℕ

The rank of a world is one more than the highest priority among the rules it falsifies, and zero when it falsifies none (Definition 12 and Eq. 15).

Equations

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

def GoldszmidtPearl1996.zRanking {W : Type u_1} (rules : List (Rule W × ℕ)) (h : ∃ (x : W), zRank rules x = 0) : RankingFunction W

The ranking a prioritized base induces, given a world falsifying no rule.

Equations

• GoldszmidtPearl1996.zRanking rules h = { toFun := GoldszmidtPearl1996.zRank rules, exists_eq_zero' := h }

theorem GoldszmidtPearl1996.admissible_iff_forall_entails {W : Type u_1} {κ : RankingFunction W} {Δ : KnowledgeBase W} : Admissible κ Δ ↔ ∀ r ∈ Δ, κ.Entails {x : W | r.ante x} {x : W | r.cons x}

A ranking is admissible exactly when each rule's consequent follows from its antecedent in the ranking's consequence relation RankingFunction.Entails, the paper's Definition 7. By Principle (3) a consequent follows when its negation has positive rank given the antecedent (RankingFunction.entails_iff_condRank), equivalently when it holds in every most normal world of the antecedent (RankingFunction.entails_iff_forall_least).

def GoldszmidtPearl1996.PEntails {W : Type u_1} (Δ : KnowledgeBase W) (φ σ : Set W) : Prop

A proposition p-entails another when it entails it in every admissible ranking (Definition 8).

Equations

• GoldszmidtPearl1996.PEntails Δ φ σ = ∀ (κ : RankingFunction W), GoldszmidtPearl1996.Admissible κ Δ → κ.Entails φ σ

theorem GoldszmidtPearl1996.pEntails_of_mem {W : Type u_1} {Δ : KnowledgeBase W} {r : Rule W} (h : r ∈ Δ) : PEntails Δ {x : W | r.ante x} {x : W | r.cons x}

A rule is p-entailed by its own antecedent.

theorem GoldszmidtPearl1996.not_pEntails {W : Type u_1} {Δ : KnowledgeBase W} {κ : RankingFunction W} (hκ : Admissible κ Δ) {φ σ : Set W} (h : ¬κ.Entails φ σ) : ¬PEntails Δ φ σ

An admissible ranking in which σ does not follow from φ refutes p-entailment.

theorem GoldszmidtPearl1996.isPreferential_pEntails {W : Type u_1} (Δ : KnowledgeBase W) : Nonmonotonic.IsPreferential (PEntails Δ)

P-entailment is a preferential consequence relation, since each rule of system P holds in every admissible ranking.

System Z⁺ (section 3)

structure GoldszmidtPearl1996.StrengthRule (W : Type u_2) extends GoldszmidtPearl1996.Rule W : Type u_2

A rule with a strength δ.

• ante : W → Prop
• cons : W → Prop
• decAnte : DecidablePred self.ante
• decCons : DecidablePred self.cons
• strength : ℕ

@[reducible, inline]

abbrev GoldszmidtPearl1996.StrengthBase (W : Type u_2) : Type u_2

A base of variable-strength rules.

Equations

• GoldszmidtPearl1996.StrengthBase W = List (GoldszmidtPearl1996.StrengthRule W)

def GoldszmidtPearl1996.StrengthBase.flat {W : Type u_1} (Δ : StrengthBase W) : KnowledgeBase W

The flat base of a strength base consists of its rules without their strengths.

Equations

• Δ.flat = List.map (fun (x : GoldszmidtPearl1996.StrengthRule W) => x.toRule) Δ

def GoldszmidtPearl1996.StrengthAdmissible {W : Type u_1} (κ : RankingFunction W) (Δ : StrengthBase W) : Prop

A ranking is δ-admissible when every world falsifying a rule lies at least δ + 1 ranks above a world verifying it (Definition 18).

Equations

• GoldszmidtPearl1996.StrengthAdmissible κ Δ = ∀ r ∈ Δ, ∀ (x : W), r.Falsified x → ∃ (y : W), r.ante y ∧ r.cons y ∧ κ y + r.strength < κ x

theorem GoldszmidtPearl1996.strengthAdmissible_iff_flat {W : Type u_1} [Fintype W] (Δ : StrengthBase W) : (∃ (κ : RankingFunction W), StrengthAdmissible κ Δ) ↔ ∃ (κ : RankingFunction W), Admissible κ Δ.flat

A strength base admits a δ-admissible ranking exactly when its flat base admits an admissible one, since scaling a ranking by one more than the largest strength widens every gap (Theorem 19).

def GoldszmidtPearl1996.zPlusRank {W : Type u_1} (Δ : List (StrengthRule W × ℕ)) : W → ℕ

The rank a prioritized strength base induces (Eq. 15).

Equations

• GoldszmidtPearl1996.zPlusRank Δ = GoldszmidtPearl1996.zRank (List.map (fun (p : GoldszmidtPearl1996.StrengthRule W × ℕ) => (p.1.toRule, p.2)) Δ)

def GoldszmidtPearl1996.IsZPlusOrdering {W : Type u_1} [Fintype W] (Δ : List (StrengthRule W × ℕ)) : Prop

Priorities form a Z⁺-ordering when each rule's priority is its strength plus the least rank, under the ranking the priorities induce, of a world verifying it (Definition 20 and Eq. 16).

Equations

• GoldszmidtPearl1996.IsZPlusOrdering Δ = ∀ p ∈ Δ, IsLeast {n : ℕ | ∃ (x : W), p.1.ante x ∧ p.1.cons x ∧ n = GoldszmidtPearl1996.zPlusRank Δ x + p.1.strength} p.2

Example 17: the penguin base

structure GoldszmidtPearl1996.World : Type

A world of Example 17 is a truth assignment to bird, penguin, flies, winged, airborne, and the irrelevant feature red.

• b : Bool
• p : Bool
• f : Bool
• w : Bool
• a : Bool
• r : Bool

def GoldszmidtPearl1996.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidableEqWorld : DecidableEq World

Equations

• GoldszmidtPearl1996.instDecidableEqWorld = GoldszmidtPearl1996.instDecidableEqWorld.decEq

def GoldszmidtPearl1996.World.equivProd : World ≃ Bool × Bool × Bool × Bool × Bool × Bool

Worlds are the assignments to the six atoms.

Equations

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

@[instance_reducible]

instance GoldszmidtPearl1996.instFintypeWorld : Fintype World

Equations

• GoldszmidtPearl1996.instFintypeWorld = Fintype.ofEquiv (Bool × Bool × Bool × Bool × Bool × Bool) GoldszmidtPearl1996.World.equivProd.symm

def GoldszmidtPearl1996.bird (x : World) : Prop

Equations

• GoldszmidtPearl1996.bird x = (x.b = true)

def GoldszmidtPearl1996.penguin (x : World) : Prop

Equations

• GoldszmidtPearl1996.penguin x = (x.p = true)

def GoldszmidtPearl1996.flies (x : World) : Prop

Equations

• GoldszmidtPearl1996.flies x = (x.f = true)

def GoldszmidtPearl1996.winged (x : World) : Prop

Equations

• GoldszmidtPearl1996.winged x = (x.w = true)

def GoldszmidtPearl1996.airborne (x : World) : Prop

Equations

• GoldszmidtPearl1996.airborne x = (x.a = true)

def GoldszmidtPearl1996.red (x : World) : Prop

Equations

• GoldszmidtPearl1996.red x = (x.r = true)

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldBird : DecidablePred bird

Equations

• GoldszmidtPearl1996.instDecidablePredWorldBird x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldPenguin : DecidablePred penguin

Equations

• GoldszmidtPearl1996.instDecidablePredWorldPenguin x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldFlies : DecidablePred flies

Equations

• GoldszmidtPearl1996.instDecidablePredWorldFlies x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldWinged : DecidablePred winged

Equations

• GoldszmidtPearl1996.instDecidablePredWorldWinged x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldAirborne : DecidablePred airborne

Equations

• GoldszmidtPearl1996.instDecidablePredWorldAirborne x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredWorldRed : DecidablePred red

Equations

• GoldszmidtPearl1996.instDecidablePredWorldRed x = id inferInstance

def GoldszmidtPearl1996.r₁ : Rule World

Rule r₁ says that birds fly.

Equations

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

def GoldszmidtPearl1996.r₂ : Rule World

Rule r₂ says that penguins are birds.

Equations

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

def GoldszmidtPearl1996.r₃ : Rule World

Rule r₃ says that penguins do not fly.

Equations

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

def GoldszmidtPearl1996.r₄ : Rule World

Rule r₄ says that birds have wings.

Equations

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

def GoldszmidtPearl1996.r₅ : Rule World

Rule r₅ says that animals that fly are airborne.

Equations

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

def GoldszmidtPearl1996.Δpb : KnowledgeBase World

The base Δ_pb of Example 17.

Equations

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

theorem GoldszmidtPearl1996.tolerated_Δpb : Tolerated r₁ Δpb ∧ Tolerated r₄ Δpb ∧ Tolerated r₅ Δpb ∧ ¬Tolerated r₂ Δpb ∧ ¬Tolerated r₃ Δpb ∧ Tolerated r₂ [r₂, r₃] ∧ Tolerated r₃ [r₂, r₃]

r₁, r₄, and r₅ are tolerated by the whole base; r₂ and r₃ only by each other.

theorem GoldszmidtPearl1996.zPriorities_Δpb : List.map (fun (x : Rule World × ℕ) => x.2) (zPriorities Δpb) = [0, 0, 0, 1, 1]

The Consistency-Test labels r₁, r₄, r₅ with 0 and r₂, r₃ with 1.

def GoldszmidtPearl1996.κz : RankingFunction World

The ranking κᶻ of the penguin base.

Equations

• GoldszmidtPearl1996.κz = GoldszmidtPearl1996.zRanking (GoldszmidtPearl1996.zPriorities GoldszmidtPearl1996.Δpb) GoldszmidtPearl1996.κz._proof_2

theorem GoldszmidtPearl1996.admissible_κz : Admissible κz Δpb

Table 2, with a query (φ, σ) answered YES when σ follows from φ, NO when ¬σ does, and undecided when neither.

theorem GoldszmidtPearl1996.z_penguin_birds_dont_fly : κz.Entails {x : World | penguin x ∧ bird x} {x : World | ¬flies x}

The query "Do penguin-birds fly?" is answered NO under z-entailment.

theorem GoldszmidtPearl1996.p_penguin_birds_dont_fly : PEntails Δpb {x : World | penguin x ∧ bird x} {x : World | ¬flies x}

The query "Do penguin-birds fly?" is answered NO under p-entailment, by specificity in every admissible ranking. A most normal penguin-bird that flew would falsify r₃, and the world r₃ then places below it is a penguin-bird or, failing r₂, is outranked by one.

theorem GoldszmidtPearl1996.z_birds_not_penguins : κz.Entails {x : World | bird x} {x : World | ¬penguin x}

The query "Are birds typically penguins?" is answered NO under z-entailment.

theorem GoldszmidtPearl1996.p_birds_not_penguins : PEntails Δpb {x : World | bird x} {x : World | ¬penguin x}

The query "Are birds typically penguins?" is answered NO under p-entailment. A most normal bird that was a penguin would falsify r₁ or r₃, and either rule places a bird below it.

theorem GoldszmidtPearl1996.z_red_birds_fly : κz.Entails {x : World | red x ∧ bird x} {x : World | flies x}

The query "Do red birds fly?" is answered YES under z-entailment, which discounts the irrelevant feature.

theorem GoldszmidtPearl1996.p_red_birds_fly_undecided : ¬PEntails Δpb {x : World | red x ∧ bird x} {x : World | flies x} ∧ ¬PEntails Δpb {x : World | red x ∧ bird x} {x : World | ¬flies x}

The query "Do red birds fly?" is undecided under p-entailment. Adding the rule that red birds do not fly keeps the base consistent, and its ranking is admissible for Δ_pb; so is κᶻ, where they fly.

theorem GoldszmidtPearl1996.not_isRational_pEntails : ¬Nonmonotonic.IsRational (PEntails Δpb)

P-entailment from the penguin base is not rational. Birds fly, and birds are not normally other than red, yet red birds are not p-entailed to fly. Rational monotony holds in each admissible ranking, so z-entailment has it and p-entailment lacks it.

theorem GoldszmidtPearl1996.z_birds_airborne : κz.Entails {x : World | bird x} {x : World | airborne x}

The query "Are birds airborne?" is answered YES under z-entailment, by chaining r₁ and r₅.

theorem GoldszmidtPearl1996.p_birds_airborne_undecided : ¬PEntails Δpb {x : World | bird x} {x : World | airborne x} ∧ ¬PEntails Δpb {x : World | bird x} {x : World | ¬airborne x}

The query "Are birds airborne?" is undecided under p-entailment, since neither "birds are airborne" nor "birds are not airborne" makes the base inconsistent.

theorem GoldszmidtPearl1996.z_penguins_winged_undecided : ¬κz.Entails {x : World | penguin x} {x : World | winged x} ∧ ¬κz.Entails {x : World | penguin x} {x : World | ¬winged x}

The query "Are penguins winged animals?" is undecided under z-entailment, the exceptional subclass inheriting nothing from birds.

theorem GoldszmidtPearl1996.p_penguins_winged_undecided : ¬PEntails Δpb {x : World | penguin x} {x : World | winged x} ∧ ¬PEntails Δpb {x : World | penguin x} {x : World | ¬winged x}

The query "Are penguins winged animals?" is undecided under p-entailment.

Example 24: the penguin base with strengths

theorem GoldszmidtPearl1996.le_zRank_of_falsified {W : Type u_1} {rules : List (Rule W × ℕ)} {q : Rule W × ℕ} (hq : q ∈ rules) {x : W} (hx : q.1.Falsified x) : q.2 + 1 ≤ zRank rules x

A falsified rule bounds the rank from below by one more than its priority.

theorem GoldszmidtPearl1996.le_zPlusRank_of_falsified {W : Type u_1} {Δ : List (StrengthRule W × ℕ)} {q : StrengthRule W × ℕ} (hq : q ∈ Δ) {x : W} (hx : q.1.Falsified x) : q.2 + 1 ≤ zPlusRank Δ x

def GoldszmidtPearl1996.ΔpbPlus (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : List (StrengthRule World × ℕ)

In the paper's Z⁺-ordering for Δ⁺_pb the tolerated rules keep their strengths, and the penguin rules, whose verifying worlds must falsify r₁, sit at δ₁ + δᵢ + 1.

Equations

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

def GoldszmidtPearl1996.w₀ : World

The normal world is a flying, winged, airborne bird.

Equations

• GoldszmidtPearl1996.w₀ = { b := true, p := false, f := true, w := true, a := true, r := false }

def GoldszmidtPearl1996.w₁ : World

The most normal penguin is a winged, grounded bird.

Equations

• GoldszmidtPearl1996.w₁ = { b := true, p := true, f := false, w := true, a := true, r := false }

theorem GoldszmidtPearl1996.zPlusRank_w₀ (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : zPlusRank (ΔpbPlus δ₁ δ₂ δ₃ δ₄ δ₅) w₀ = 0

theorem GoldszmidtPearl1996.zPlusRank_w₁ (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : zPlusRank (ΔpbPlus δ₁ δ₂ δ₃ δ₄ δ₅) w₁ = δ₁ + 1

theorem GoldszmidtPearl1996.le_zPlusRank_of_penguin (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) {x : World} (hp : penguin x) : δ₁ + 1 ≤ zPlusRank (ΔpbPlus δ₁ δ₂ δ₃ δ₄ δ₅) x

Every penguin world ranks at least δ₁ + 1, because it falsifies r₂, r₃, or r₁.

theorem GoldszmidtPearl1996.isZPlusOrdering_example24 (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : IsZPlusOrdering (ΔpbPlus δ₁ δ₂ δ₃ δ₄ δ₅)

The paper's priorities satisfy Definition 20 for every choice of strengths.

def GoldszmidtPearl1996.κPlus (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : RankingFunction World

The ranking κ⁺ of Example 24.

Equations

• GoldszmidtPearl1996.κPlus δ₁ δ₂ δ₃ δ₄ δ₅ = { toFun := GoldszmidtPearl1996.zPlusRank (GoldszmidtPearl1996.ΔpbPlus δ₁ δ₂ δ₃ δ₄ δ₅), exists_eq_zero' := ⋯ }

theorem GoldszmidtPearl1996.zPlus_penguin_birds_dont_fly (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : (κPlus δ₁ δ₂ δ₃ δ₄ δ₅).Entails {x : World | penguin x ∧ bird x} {x : World | ¬flies x}

Penguin-birds do not fly under κ⁺ whatever the strengths, because the preference for r₃ over r₁ is a matter of specificity, not of the δ's (Theorem 25).

theorem GoldszmidtPearl1996.zPlus_penguins_winged_iff (δ₁ δ₂ δ₃ δ₄ δ₅ : ℕ) : (κPlus δ₁ δ₂ δ₃ δ₄ δ₅).Entails {x : World | penguin x} {x : World | winged x} ↔ δ₁ < δ₄

Penguins inherit wings under κ⁺ exactly when the wing rule is firmer than the flying rule.

Example 26: the Nixon diamond

structure GoldszmidtPearl1996.Nixon : Type

A world of Example 26 is a truth assignment to Quaker, Republican and pacifist.

• q : Bool
• r : Bool
• p : Bool

def GoldszmidtPearl1996.instDecidableEqNixon.decEq (x✝ x✝¹ : Nixon) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidableEqNixon : DecidableEq Nixon

Equations

• GoldszmidtPearl1996.instDecidableEqNixon = GoldszmidtPearl1996.instDecidableEqNixon.decEq

def GoldszmidtPearl1996.Nixon.equivProd : Nixon ≃ Bool × Bool × Bool

Equations

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

@[instance_reducible]

instance GoldszmidtPearl1996.instFintypeNixon : Fintype Nixon

Equations

• GoldszmidtPearl1996.instFintypeNixon = Fintype.ofEquiv (Bool × Bool × Bool) GoldszmidtPearl1996.Nixon.equivProd.symm

def GoldszmidtPearl1996.quaker (x : Nixon) : Prop

Equations

• GoldszmidtPearl1996.quaker x = (x.q = true)

def GoldszmidtPearl1996.republican (x : Nixon) : Prop

Equations

• GoldszmidtPearl1996.republican x = (x.r = true)

def GoldszmidtPearl1996.pacifist (x : Nixon) : Prop

Equations

• GoldszmidtPearl1996.pacifist x = (x.p = true)

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredNixonQuaker : DecidablePred quaker

Equations

• GoldszmidtPearl1996.instDecidablePredNixonQuaker x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredNixonRepublican : DecidablePred republican

Equations

• GoldszmidtPearl1996.instDecidablePredNixonRepublican x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredNixonPacifist : DecidablePred pacifist

Equations

• GoldszmidtPearl1996.instDecidablePredNixonPacifist x = id inferInstance

def GoldszmidtPearl1996.Δqr (δ₁ δ₂ : ℕ) : List (StrengthRule Nixon × ℕ)

Quakers are pacifists with strength δ₁, Republicans are not with strength δ₂; each rule is tolerated by the other, so each priority is its strength.

Equations

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

theorem GoldszmidtPearl1996.isZPlusOrdering_example26 (δ₁ δ₂ : ℕ) : IsZPlusOrdering (Δqr δ₁ δ₂)

def GoldszmidtPearl1996.κqr (δ₁ δ₂ : ℕ) : RankingFunction Nixon

The ranking κ⁺ of the Nixon diamond.

Equations

• GoldszmidtPearl1996.κqr δ₁ δ₂ = { toFun := GoldszmidtPearl1996.zPlusRank (GoldszmidtPearl1996.Δqr δ₁ δ₂), exists_eq_zero' := ⋯ }

theorem GoldszmidtPearl1996.nixon_pacifist_iff (δ₁ δ₂ : ℕ) : (κqr δ₁ δ₂).Entails {x : Nixon | quaker x ∧ republican x} {x : Nixon | pacifist x} ↔ δ₂ < δ₁

A Quaker Republican is a pacifist exactly when religious conviction outweighs political affiliation: no specificity decides the diamond, only the strengths.

Soft evidence (section 5)

noncomputable def GoldszmidtPearl1996.lCondition {W : Type u_1} (κ : RankingFunction W) (A : Set W) (L : ℕ) : RankingFunction W

L-conditioning on A with strength L answers a report that evidence of its own supports A to degree L (section 5.2). It lifts the worlds outside A by L and shifts the ranking back to start at 0 by subtracting min[κ(A); κ(¬A) + L].

Equations

• GoldszmidtPearl1996.lCondition κ A L = { toFun := fun (w : W) => (κ w + if w ∈ A then 0 else L) - (min (κ.rank A) (κ.rank Aᶜ + ↑L)).toNat, exists_eq_zero' := ⋯ }

theorem GoldszmidtPearl1996.lCondition_of_mem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {L : ℕ} {w : W} (hw : w ∈ A) : (lCondition κ A L) w = κ w - (min (κ.rank A) (κ.rank Aᶜ + ↑L)).toNat

theorem GoldszmidtPearl1996.lCondition_of_notMem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {L : ℕ} {w : W} (hw : w ∉ A) : (lCondition κ A L) w = κ w + L - (min (κ.rank A) (κ.rank Aᶜ + ↑L)).toNat

theorem GoldszmidtPearl1996.exists_lCondition_add {W : Type u_1} (κ : RankingFunction W) (A : Set W) (L : ℕ) : ∃ (c : ℕ), ∀ (w : W), (lCondition κ A L) w + c = κ w + if w ∈ A then 0 else L

Up to the constant that normalizes it, L-conditioning lifts the worlds outside A by L.

theorem GoldszmidtPearl1996.lCondition_comm {W : Type u_1} (κ : RankingFunction W) (A B : Set W) (L M : ℕ) : lCondition (lCondition κ A L) B M = lCondition (lCondition κ B M) A L

L-conditioning is commutative (section 5.2).

theorem GoldszmidtPearl1996.lCondition_lCondition {W : Type u_1} (κ : RankingFunction W) (A : Set W) (L M : ℕ) : lCondition (lCondition κ A L) A M = lCondition κ A (L + M)

Two pieces of evidence for the same proposition add their strengths (section 5.2).

theorem GoldszmidtPearl1996.lCondition_eq_aPart_of_mem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {L : ℕ} {w : W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (hw : w ∈ A) : (lCondition κ A L) w = κ.aPart A w + ((κ.rank A).toNat - ((κ.rank Aᶜ).toNat + L))

Eq. (32) on the worlds of A, where κ(ω | φ) is the A-part (RankingFunction.condRank_singleton) and max[0; x − y] is the truncated difference.

theorem GoldszmidtPearl1996.lCondition_eq_aPart_of_notMem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {L : ℕ} {w : W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (hw : w ∉ A) : (lCondition κ A L) w = κ.aPart Aᶜ w + ((κ.rank Aᶜ).toNat + L - (κ.rank A).toNat)

Eq. (32) on the worlds outside A.

theorem GoldszmidtPearl1996.lCondition_eq_conditionα {W : Type u_1} (κ : RankingFunction W) {A : Set W} {L : ℕ} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (h : (κ.rank A).toNat ≤ (κ.rank Aᶜ).toNat + L) : lCondition κ A L = κ.conditionα A hA ((κ.rank Aᶜ).toNat + L - (κ.rank A).toNat)

When A comes out with rank 0, L-conditioning is J-conditioning, Spohn's conditionalization of Eq. (25), at the firmness κ(¬A) + L − κ(A) that Eq. (30) gives the negation.

Example 28: Mary and Bill's party

structure GoldszmidtPearl1996.Party : Type

A world of Example 28 says whether Mary and whether Bill go to the party.

• m : Bool
• b : Bool

def GoldszmidtPearl1996.instDecidableEqParty.decEq (x✝ x✝¹ : Party) : Decidable (x✝ = x✝¹)

Equations

• GoldszmidtPearl1996.instDecidableEqParty.decEq { m := a, b := a_1 } { m := b, b := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidableEqParty : DecidableEq Party

Equations

• GoldszmidtPearl1996.instDecidableEqParty = GoldszmidtPearl1996.instDecidableEqParty.decEq

def GoldszmidtPearl1996.Party.equivProd : Party ≃ Bool × Bool

Equations

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

@[instance_reducible]

instance GoldszmidtPearl1996.instFintypeParty : Fintype Party

Equations

• GoldszmidtPearl1996.instFintypeParty = Fintype.ofEquiv (Bool × Bool) GoldszmidtPearl1996.Party.equivProd.symm

def GoldszmidtPearl1996.mary (x : Party) : Prop

Equations

• GoldszmidtPearl1996.mary x = (x.m = true)

def GoldszmidtPearl1996.bill (x : Party) : Prop

Equations

• GoldszmidtPearl1996.bill x = (x.b = true)

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredPartyMary : DecidablePred mary

Equations

• GoldszmidtPearl1996.instDecidablePredPartyMary x = id inferInstance

@[instance_reducible]

instance GoldszmidtPearl1996.instDecidablePredPartyBill : DecidablePred bill

Equations

• GoldszmidtPearl1996.instDecidablePredPartyBill x = id inferInstance

def GoldszmidtPearl1996.Δm : List (StrengthRule Party × ℕ)

The single rule r_m : M →² ¬B, if Mary goes then Bill will not, at the priority 2 that Definition 20 gives it. The paper prints Z⁺(r_m) = 4, but its Fig. 5 ranks M ∧ B at 3, as priority 2 does.

Equations

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

theorem GoldszmidtPearl1996.isZPlusOrdering_example28 : IsZPlusOrdering Δm

def GoldszmidtPearl1996.κm : RankingFunction Party

The ranking κ⁺ of Example 28, the left of Fig. 5.

Equations

• GoldszmidtPearl1996.κm = { toFun := GoldszmidtPearl1996.zPlusRank GoldszmidtPearl1996.Δm, exists_eq_zero' := GoldszmidtPearl1996.κm._proof_2 }

theorem GoldszmidtPearl1996.κm_apply (x : Party) : κm x = if mary x ∧ bill x then 3 else 0

noncomputable def GoldszmidtPearl1996.κm' : RankingFunction Party

The ranking κ⁺′ after evidence of strength 2 that Mary goes, read as a Type-J report.

Equations

• GoldszmidtPearl1996.κm' = GoldszmidtPearl1996.κm.conditionα {x : GoldszmidtPearl1996.Party | GoldszmidtPearl1996.mary x} GoldszmidtPearl1996.κm'._proof_1 2

theorem GoldszmidtPearl1996.κm'_apply (x : Party) : κm' x = if mary x then if bill x then 3 else 0 else 2

In the right of Fig. 5, the worlds without Mary rise to rank 2.

theorem GoldszmidtPearl1996.rank_κm'_bill : κm'.rank {x : Party | bill x} = 2

After the Type-J report on Mary, the belief that Bill stays home has strength 2.

theorem GoldszmidtPearl1996.rank_κm'_not_bill : κm'.rank {x : Party | bill x}ᶜ = 0

theorem GoldszmidtPearl1996.lCondition_κm'_apply (x : Party) : (lCondition κm' {x : Party | bill x} 2) x = if mary x ∧ bill x then 1 else if mary x ∨ bill x then 0 else 2

L-conditioning κ⁺′ on evidence of strength 2 that Bill goes lowers M ∧ B to 1 and ¬M ∧ B to 0, the right of Fig. 6.

theorem GoldszmidtPearl1996.fig6 : (lCondition κm' {x : Party | bill x} 2).rank {x : Party | bill x} = 0 ∧ (lCondition κm' {x : Party | bill x} 2).rank {x : Party | ¬mary x} = 0 ∧ (lCondition κm' {x : Party | bill x} 2).rank {x : Party | mary x ∧ bill x} = 1

The Type-L report on Bill brings back the initial ranks of Bill and Mary, κ⁺″(B) = 0 and κ⁺″(¬M) = 0, while lowering the disbelief in both going to κ⁺″(M ∧ B) = 1.

theorem GoldszmidtPearl1996.typeJ_bill : (κm'.conditionα {x : Party | bill x} ⋯ 2).rank {x : Party | bill x}ᶜ = 2 ∧ (κm'.conditionα {x : Party | bill x} ⋯ 2).rank {x : Party | mary x} = 1

Read as a Type-J report instead, the hunch that Bill goes makes his going believed with strength 2, but Mary's going keeps rank 1. The paper reports κ⁺″(M) = 2, which would need the prior to rank M ∧ B at 4 or more, and then the Type-L reading would leave κ⁺″(M ∧ B) above 1.