System Z: Constructing Rankings from Default Rules

@cite{goldszmidt-pearl-1996}

System Z constructs the unique minimal ranking function from a knowledge base of default rules. Given defaults like "birds fly" and "penguins don't fly", the Z-ordering stratifies rules by tolerance — which can be satisfied without violating the others — and κ^z assigns each world the lowest possible rank consistent with all constraints.

Key definitions

• DefaultRule W: a default rule φ → ψ (Bool predicates on worlds)
• KnowledgeBase W: a list of default rules
• tolerated: a rule is tolerated by Δ iff ∃ω verifying it + all material counterparts (Def. 3)
• admissible: κ satisfies all rules' ranking constraints (Def. 2)
• zRankValue: κ^z(ω) from Z-prioritized rules (Def. 12, Eq. 10)
• zRanking: wrap as RankingFunction
• rankEntails: consequence via a ranking (Def. 7)

Connection to RankingFunction

zRanking produces a RankingFunction W, connecting to all downstream infrastructure: toPlausibilityOrder, toPreferential, ranking_rationalMonotonicity, and the 95+ consumers of NormalityOrder.

Architecture

Default rules Δ = {φᵢ → ψᵢ}
    ↓ Consistency-Test (tolerance stripping)
Z-priority ordering on rules
    ↓ Definition 12
κ^z : RankingFunction W (minimal admissible ranking)
    ↓ toPlausibilityOrder
PlausibilityOrder → PreferentialConsequence (System P)

structure Core.Logic.SystemZ.DefaultRule (W : Type u_1) : Type u_1

A default rule "if φ then normally ψ", where φ and ψ are decidable predicates on worlds.

@cite{goldszmidt-pearl-1996}: rules are the basic unit of defeasible knowledge. The rule φ → ψ expresses that ψ is normally the case in the domain φ, admitting exceptions.

• ante : W → Bool

  Antecedent (domain of the default)

• cons : W → Bool

  Consequent (what normally holds)

@[reducible, inline]

abbrev Core.Logic.SystemZ.KnowledgeBase (W : Type u_1) : Type u_1

A knowledge base: a list of default rules.

Equations

• Core.Logic.SystemZ.KnowledgeBase W = List (Core.Logic.SystemZ.DefaultRule W)

def Core.Logic.SystemZ.DefaultRule.verified {W : Type u_1} (r : DefaultRule W) (w : W) : Bool

A world verifies a rule: satisfies the material counterpart φ ⊃ ψ. Equivalently, either the antecedent is false or the consequent holds.

Equations

• r.verified w = (!r.ante w || r.cons w)

def Core.Logic.SystemZ.DefaultRule.falsified {W : Type u_1} (r : DefaultRule W) (w : W) : Bool

A world falsifies a rule: satisfies φ ∧ ¬ψ. This is the world that violates the default expectation.

Equations

• r.falsified w = (r.ante w && !r.cons w)

def Core.Logic.SystemZ.tolerated {W : Type u_1} (r : DefaultRule W) (Δ : KnowledgeBase W) : Prop

@cite{goldszmidt-pearl-1996}, Definition 3 (Eq. 8). A rule α → β is tolerated by a knowledge base Δ iff there exists a world ω satisfying α ∧ β and the material counterpart of every rule in Δ.

Tolerance is the key to stratification: rules that can be satisfied without violating others are the least surprising (lowest Z-priority).

Equations

• Core.Logic.SystemZ.tolerated r Δ = ∃ (w : W), r.ante w = true ∧ r.cons w = true ∧ (List.all Δ fun (r' : Core.Logic.SystemZ.DefaultRule W) => r'.verified w) = true

def Core.Logic.SystemZ.admissible {W : Type u_1} (κ : Ranking.RankingFunction W) (Δ : KnowledgeBase W) : Prop

@cite{goldszmidt-pearl-1996}, Definition 2 (Eq. 7). A ranking κ is admissible relative to Δ iff for each rule φᵢ → ψᵢ, every world falsifying the rule is outranked by some world satisfying it.

Equivalently: κ(φᵢ ∧ ψᵢ) < κ(φᵢ ∧ ¬ψᵢ) — the most normal world satisfying the rule has strictly lower rank than the most normal world violating it.

Equations

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

def Core.Logic.SystemZ.zRankValue {W : Type u_1} (rules : List (DefaultRule W × ℕ)) (w : W) : ℕ

The κ^z value at a world, given Z-prioritized rules.

@cite{goldszmidt-pearl-1996}, Definition 12 (Eq. 10):

• κ^z(ω) = 0 if ω does not falsify any rule in Δ
• κ^z(ω) = max{Z(rᵢ) | ω falsifies rᵢ} + 1 otherwise

Each rule is paired with its Z-priority (computed by the Consistency-Test procedure, verified concretely in study files).

Equations

• Core.Logic.SystemZ.zRankValue rules w = match Core.Logic.SystemZ.zRankValue.maxFalsifiedPriority rules w with | none => 0 | some z => z + 1

def Core.Logic.SystemZ.zRankValue.maxFalsifiedPriority {W : Type u_1} : List (DefaultRule W × ℕ) → W → Option ℕ

Find the maximum Z-priority among rules falsified by world w.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.SystemZ.zRankValue.maxFalsifiedPriority [] x✝ = none

def Core.Logic.SystemZ.zRanking {W : Type u_1} (rules : List (DefaultRule W × ℕ)) (hnorm : ∃ (w : W), zRankValue rules w = 0) : Ranking.RankingFunction W

Build a RankingFunction from Z-prioritized rules.

The normalization proof ensures some world has rank 0, i.e., some world verifies all rules simultaneously. This world exists whenever the knowledge base is consistent.

Equations

• Core.Logic.SystemZ.zRanking rules hnorm = { rank := Core.Logic.SystemZ.zRankValue rules, normalized := hnorm }

def Core.Logic.SystemZ.rankEntails {W : Type u_1} (κ : Ranking.RankingFunction W) (φ σ : W → Bool) : Prop

@cite{goldszmidt-pearl-1996}, Definition 7 (Eq. 9). The consequence relation induced by a ranking κ: φ ⊨_κ σ iff the most normal world satisfying φ ∧ σ has strictly lower rank than the most normal world satisfying φ ∧ ¬σ.

Equivalently: every world satisfying φ ∧ ¬σ is outranked by some world satisfying φ ∧ σ.

Equations

• Core.Logic.SystemZ.rankEntails κ φ σ = ∀ (w : W), (φ w && !σ w) = true → ∃ (v : W), (φ v && σ v) = true ∧ κ.rank v < κ.rank w

def Core.Logic.SystemZ.pEntails {W : Type u_1} (Δ : KnowledgeBase W) (φ σ : W → Bool) : Prop

@cite{goldszmidt-pearl-1996}, Definition 8 (p. 66). σ is p-entailed by φ given Δ iff φ ⊨_κ σ holds in every consequence relation ⊨_κ induced by an admissible ranking κ.

p-entailment is conservative: it only draws conclusions that are safe across ALL admissible rankings. z-entailment (Definition 13) is bolder, using only the unique minimal ranking κ^z. Every p-entailed conclusion is z-entailed but not vice versa (Table 2).

Equations

• Core.Logic.SystemZ.pEntails Δ φ σ = ∀ (κ : Core.Logic.Ranking.RankingFunction W), Core.Logic.SystemZ.admissible κ Δ → Core.Logic.SystemZ.rankEntails κ φ σ

theorem Core.Logic.SystemZ.pEntails_implies_rankEntails {W : Type u_1} {Δ : KnowledgeBase W} {κ : Ranking.RankingFunction W} (hadm : admissible κ Δ) {φ σ : W → Bool} (h : pEntails Δ φ σ) : rankEntails κ φ σ

p-entailment implies z-entailment: if φ ⊨p σ then φ ⊨{κ^z} σ, since κ^z is one particular admissible ranking.

def Core.Logic.SystemZ.toleratedBool {W : Type u_1} [Fintype W] (r : DefaultRule W) (Δ : KnowledgeBase W) : Bool

Decidable tolerance check. Inlines the tolerated definition for Decidable instance synthesis on finite types.

Equations

• Core.Logic.SystemZ.toleratedBool r Δ = decide (∃ (w : W), r.ante w = true ∧ r.cons w = true ∧ (List.all Δ fun (r' : Core.Logic.SystemZ.DefaultRule W) => r'.verified w) = true)

def Core.Logic.SystemZ.zPrioritiesAux {W : Type u_1} [Fintype W] (remaining : KnowledgeBase W) (level fuel : ℕ) : List (DefaultRule W × ℕ)

Iterative tolerance stripping (Consistency-Test, Fig. 2). At each level, peels off tolerated rules and assigns them the current stratum number. fuel bounds iterations.

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.SystemZ.zPrioritiesAux [] level fuel = []
• Core.Logic.SystemZ.zPrioritiesAux remaining level 0 = List.map (fun (x : Core.Logic.SystemZ.DefaultRule W) => (x, level)) remaining

def Core.Logic.SystemZ.zPriorities {W : Type u_1} [Fintype W] (Δ : KnowledgeBase W) : List (DefaultRule W × ℕ)

Compute Z-priorities for all rules via the Consistency-Test (Fig. 2). Each rule is assigned its stratum number.

Equations

• Core.Logic.SystemZ.zPriorities Δ = Core.Logic.SystemZ.zPrioritiesAux Δ 0 (List.length Δ)

structure Core.Logic.SystemZ.StrengthRule (W : Type u_2) extends Core.Logic.SystemZ.DefaultRule W : Type u_2

A default rule with strength parameter δ. @cite{goldszmidt-pearl-1996}, Definition 18: higher δ demands a wider gap between verifying and falsifying worlds.

• ante : W → Bool
• cons : W → Bool
• strength : ℕ

  Strength parameter (δ ≥ 0)

@[reducible, inline]

abbrev Core.Logic.SystemZ.StrengthKB (W : Type u_2) : Type u_2

A knowledge base of variable-strength default rules.

Equations

• Core.Logic.SystemZ.StrengthKB W = List (Core.Logic.SystemZ.StrengthRule W)

def Core.Logic.SystemZ.StrengthKB.flat {W : Type u_2} (Δ : StrengthKB W) : KnowledgeBase W

Strip strength parameters to get the underlying KnowledgeBase.

Equations

• Δ.flat = List.map (fun (x : Core.Logic.SystemZ.StrengthRule W) => x.toDefaultRule) Δ

def Core.Logic.SystemZ.strengthAdmissible {W : Type u_1} (κ : Ranking.RankingFunction W) (Δ : StrengthKB W) : Prop

@cite{goldszmidt-pearl-1996}, Definition 18 (corrected). A ranking κ is δ-admissible relative to strength rules iff for each rule (φᵢ → ψᵢ, δᵢ), every falsifying world is outranked by at least δᵢ + 1 by some verifying world: κ(v) + δᵢ < κ(w) for some verifying v.

Note: Eq. 14 as printed has δ on the wrong side; the "equivalently κ(¬ψ|φ) > δ" clause and Fig. 3 confirm this corrected form.

Equations

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

theorem Core.Logic.SystemZ.toleratedBool_iff {W : Type u_1} [Fintype W] (r : DefaultRule W) (Δ : KnowledgeBase W) : toleratedBool r Δ = true ↔ tolerated r Δ

toleratedBool computes tolerated: the Bool decision procedure agrees with the Prop definition on finite types.

theorem Core.Logic.SystemZ.strength_consistent_iff_flat {W : Type u_1} [Fintype W] (Δ : StrengthKB W) : (∃ (κ : Ranking.RankingFunction W), strengthAdmissible κ Δ) ↔ ∃ (κ : Ranking.RankingFunction W), admissible κ Δ.flat

@cite{goldszmidt-pearl-1996}, Theorem 19: a strength knowledge base is δ-consistent (admits a δ-admissible ranking) iff its flat projection (ignoring strengths) is consistent (admits an ordinary admissible ranking).

(→) Drop strength terms: κ(v) + δ < κ(w) implies κ(v) < κ(w). (←) Scale the ranking by M = 1 + max{δᵢ}: the gap κ(v) < κ(w) becomes κ(v)·M + δ < (κ(v)+1)·M ≤ κ(w)·M for any δ < M.