Ranking functions

This file defines ranking functions, Spohn's ordinal conditional functions with natural-number grades, their conditionalization, and the consequence relation they induce.

A ranking function grades the disbelief in each world, and some world has grade 0. The rank of a proposition is the least rank of its worlds, and ⊤ for the contradiction, so of a proposition and its negation one has rank 0, and the rank of a disjunction is the smaller of the two ranks. The rank of B given A is κ(A ∩ B) − κ(A), and ⊤ when A is impossible, so the rank of an intersection is a rank plus a conditional rank, which gives the chain rule and Bayes' rule for ranks. Conditionalization on a proposition at a firmness keeps the ranking within the proposition and within its negation, each shifted to start at 0, and lifts the negation by the firmness. It keeps the ranks given the proposition and given its negation, so it ranks every proposition by Jeffrey's rule.

A ranking function orders the worlds by rank, which makes it a ranked model in the sense of Lehmann and Magidor. A proposition B follows from A when the A-worlds of least rank are B-worlds, equivalently when Bᶜ has positive rank given A. This consequence relation is rational, and the beliefs of the ranking function, the propositions true at every world of rank 0, are the consequences of the tautology.

Main definitions

• RankingFunction W: a grading of disbelief W → ℕ with a world of grade 0.
• RankingFunction.rank: the rank of a proposition, in ℕ∞.
• RankingFunction.condRank: the rank of a proposition given another.
• RankingFunction.aPart, RankingFunction.conditionα: the ranking within a proposition, and conditionalization on a proposition at a firmness.
• RankingFunction.Entails: the consequence relation of the ranked model.

Main statements

• RankingFunction.rank_eq_zero_or_compl, RankingFunction.rank_union: of a proposition and its negation one has rank 0, and the rank of a disjunction is the smaller rank.
• RankingFunction.rank_conditionα_eq: conditionalization follows Jeffrey's rule.
• RankingFunction.entails_iff_condRank: a consequence is a proposition whose negation has positive rank given the premise.
• RankingFunction.isRational_entails: the consequence relation is rational.

Notation

• κ[B | A] for κ.condRank A B, the rank of B given A, in the scope RankingFunction.

References

• W. Spohn, Ordinal Conditional Functions: A Dynamic Theory of Epistemic States (1988)
• M. Goldszmidt and J. Pearl, Qualitative Probabilities for Default Reasoning, Belief Revision, and Causal Modeling (1996)
• D. Lehmann and M. Magidor, What Does a Conditional Knowledge Base Entail? (1992)
• J. Y. Halpern, Reasoning about Uncertainty (2003)

structure RankingFunction (W : Type u_1) : Type u_1

A ranking function is a grading of disbelief in worlds under which some world has grade 0.

• toFun : W → ℕ

  The grade of disbelief in each world. Apply the ranking function itself, κ w.

• exists_eq_zero' : ∃ (w : W), self.toFun w = 0

  Some world is not disbelieved. Use the lemma exists_eq_zero.

@[instance_reducible]

instance RankingFunction.instFunLikeNat {W : Type u_1} : FunLike (RankingFunction W) W ℕ

Equations

• RankingFunction.instFunLikeNat = { coe := RankingFunction.toFun, coe_injective := ⋯ }

@[simp]

theorem RankingFunction.coe_mk {W : Type u_1} (f : W → ℕ) (h : ∃ (w : W), f w = 0) : ⇑{ toFun := f, exists_eq_zero' := h } = f

theorem RankingFunction.ext {W : Type u_1} {κ κ' : RankingFunction W} (h : ∀ (w : W), κ w = κ' w) : κ = κ'

theorem RankingFunction.ext_iff {W : Type u_1} {κ κ' : RankingFunction W} : κ = κ' ↔ ∀ (w : W), κ w = κ' w

theorem RankingFunction.exists_eq_zero {W : Type u_1} (κ : RankingFunction W) : ∃ (w : W), κ w = 0

theorem RankingFunction.eq_of_forall_add_eq_add {W : Type u_1} {κ κ' : RankingFunction W} {c c' : ℕ} (h : ∀ (w : W), κ w + c = κ' w + c') : κ = κ'

Ranking functions whose grades differ by a constant are equal.

Ranks of propositions

noncomputable def RankingFunction.rank {W : Type u_1} (κ : RankingFunction W) (A : Set W) : ℕ∞

The rank of a proposition is the least rank of its worlds, and ⊤ for the contradiction.

Equations

• κ.rank A = ⨅ w ∈ A, ↑(κ w)

theorem RankingFunction.rank_le {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hw : w ∈ A) : κ.rank A ≤ ↑(κ w)

theorem RankingFunction.le_rank_iff {W : Type u_1} (κ : RankingFunction W) {A : Set W} {n : ℕ∞} : n ≤ κ.rank A ↔ ∀ w ∈ A, n ≤ ↑(κ w)

theorem RankingFunction.rank_eq_of_forall_le {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hw : w ∈ A) (h : ∀ v ∈ A, κ w ≤ κ v) : κ.rank A = ↑(κ w)

theorem RankingFunction.rank_anti {W : Type u_1} (κ : RankingFunction W) {A B : Set W} (h : A ⊆ B) : κ.rank B ≤ κ.rank A

@[simp]

theorem RankingFunction.rank_empty {W : Type u_1} (κ : RankingFunction W) : κ.rank ∅ = ⊤

theorem RankingFunction.exists_apply_eq_rank {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) : ∃ w ∈ A, ↑(κ w) = κ.rank A

The rank of a satisfiable proposition is attained.

theorem RankingFunction.rank_eq_top_iff {W : Type u_1} (κ : RankingFunction W) {A : Set W} : κ.rank A = ⊤ ↔ A = ∅

theorem RankingFunction.rank_ne_top {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) : κ.rank A ≠ ⊤

theorem RankingFunction.rank_union {W : Type u_1} (κ : RankingFunction W) (A B : Set W) : κ.rank (A ∪ B) = min (κ.rank A) (κ.rank B)

The rank of a disjunction is the smaller rank.

theorem RankingFunction.rank_eq_zero_iff {W : Type u_1} (κ : RankingFunction W) {A : Set W} : κ.rank A = 0 ↔ ∃ w ∈ A, κ w = 0

@[simp]

theorem RankingFunction.rank_univ {W : Type u_1} (κ : RankingFunction W) : κ.rank Set.univ = 0

theorem RankingFunction.rank_eq_zero_or_compl {W : Type u_1} (κ : RankingFunction W) (A : Set W) : κ.rank A = 0 ∨ κ.rank Aᶜ = 0

Of a proposition and its negation, one has rank 0.

theorem RankingFunction.toNat_rank_le {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hw : w ∈ A) : (κ.rank A).toNat ≤ κ w

Conditional ranks

noncomputable def RankingFunction.condRank {W : Type u_1} (κ : RankingFunction W) (A B : Set W) : ℕ∞

The rank of B given A is κ(B | A) = κ(A ∩ B) − κ(A), and ⊤ when A is impossible.

Equations

• κ[B | A] = if κ.rank A = ⊤ then ⊤ else κ.rank (A ∩ B) - κ.rank A

def RankingFunction.«term__[_|_]» : Lean.TrailingParserDescr

The rank of B given A is κ(B | A) = κ(A ∩ B) − κ(A), and ⊤ when A is impossible.

Equations

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

def RankingFunction.condRankUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander for the κ[B | A] notation.

Equations

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

theorem RankingFunction.condRank_of_ne_top {W : Type u_1} (κ : RankingFunction W) {A B : Set W} (hA : κ.rank A ≠ ⊤) : κ[B | A] = κ.rank (A ∩ B) - κ.rank A

theorem RankingFunction.condRank_of_eq_top {W : Type u_1} (κ : RankingFunction W) {A B : Set W} (hA : κ.rank A = ⊤) : κ[B | A] = ⊤

theorem RankingFunction.condRank_add_rank {W : Type u_1} (κ : RankingFunction W) (A B : Set W) : κ[B | A] + κ.rank A = κ.rank (A ∩ B)

The rank of A ∩ B is the rank of A plus the rank of B given A.

@[simp]

theorem RankingFunction.condRank_univ {W : Type u_1} (κ : RankingFunction W) (B : Set W) : κ[B | Set.univ] = κ.rank B

@[simp]

theorem RankingFunction.condRank_empty {W : Type u_1} (κ : RankingFunction W) (A : Set W) : κ[∅ | A] = ⊤

theorem RankingFunction.condRank_self {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : κ.rank A ≠ ⊤) : κ[A | A] = 0

theorem RankingFunction.condRank_eq_top_iff {W : Type u_1} (κ : RankingFunction W) {A B : Set W} (hA : κ.rank A ≠ ⊤) : κ[B | A] = ⊤ ↔ κ.rank (A ∩ B) = ⊤

theorem RankingFunction.condRank_union {W : Type u_1} (κ : RankingFunction W) (A B C : Set W) : κ[B ∪ C | A] = min κ[B | A] κ[C | A]

The rank of a disjunction given A is the smaller of the two ranks given A.

theorem RankingFunction.condRank_inter {W : Type u_1} (κ : RankingFunction W) (A B C : Set W) : κ[B ∩ C | A] = κ[B | A] + κ[C | A ∩ B]

The rank of B ∩ C given A is the rank of B given A plus the rank of C given A ∩ B.

theorem RankingFunction.condRank_eq_condRank_add_sub {W : Type u_1} (κ : RankingFunction W) {A B : Set W} (hA : κ.rank A ≠ ⊤) : κ[B | A] = κ[A | B] + κ.rank B - κ.rank A

Bayes' rule for ranks.

Conditionalization

noncomputable def RankingFunction.aPart {W : Type u_1} (κ : RankingFunction W) (A : Set W) (w : W) : ℕ

The A-part κ(w | A) = κ(w) − κ(A) of a ranking is the ranking within A, shifted so that its best world has rank 0.

Equations

• κ.aPart A w = κ w - (κ.rank A).toNat

theorem RankingFunction.condRank_singleton {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hw : w ∈ A) : κ[{w} | A] = ↑(κ.aPart A w)

The A-part of a world of A is its rank given A.

theorem RankingFunction.exists_aPart_eq_zero {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) : ∃ w ∈ A, κ.aPart A w = 0

noncomputable def RankingFunction.conditionα {W : Type u_1} (κ : RankingFunction W) (A : Set W) (hA : A.Nonempty) (α : ℕ) : RankingFunction W

The A,α-conditionalization of κ is its A-part on A and its Aᶜ-part lifted by the firmness α on Aᶜ, so that A comes to be believed with firmness α.

Equations

• κ.conditionα A hA α = { toFun := fun (w : W) => if w ∈ A then κ.aPart A w else α + κ.aPart Aᶜ w, exists_eq_zero' := ⋯ }

theorem RankingFunction.conditionα_of_mem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hA : A.Nonempty) (α : ℕ) (hw : w ∈ A) : (κ.conditionα A hA α) w = κ.aPart A w

theorem RankingFunction.conditionα_of_notMem {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} (hA : A.Nonempty) (α : ℕ) (hw : w ∉ A) : (κ.conditionα A hA α) w = α + κ.aPart Aᶜ w

@[simp]

theorem RankingFunction.rank_conditionα {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) (α : ℕ) : (κ.conditionα A hA α).rank A = 0

The conditionalized ranking holds A possible.

theorem RankingFunction.rank_conditionα_compl {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (α : ℕ) : (κ.conditionα A hA α).rank Aᶜ = ↑α

The conditionalized ranking believes A with firmness α.

theorem RankingFunction.rank_conditionα_of_subset {W : Type u_1} (κ : RankingFunction W) {A S : Set W} (hA : A.Nonempty) (α : ℕ) (hS : S ⊆ A) : (κ.conditionα A hA α).rank S = κ.rank S - κ.rank A

Within A, the conditionalized ranking ranks each proposition by its rank given A.

theorem RankingFunction.rank_conditionα_of_subset_compl {W : Type u_1} (κ : RankingFunction W) {A S : Set W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (α : ℕ) (hS : S ⊆ Aᶜ) : (κ.conditionα A hA α).rank S = ↑α + (κ.rank S - κ.rank Aᶜ)

Outside A, the conditionalized ranking ranks each proposition by the firmness plus its rank given Aᶜ.

theorem RankingFunction.condRank_conditionα {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) (α : ℕ) (B : Set W) : (κ.conditionα A hA α)[B | A] = κ[B | A]

Conditionalization on A leaves the ranks given A unchanged.

theorem RankingFunction.condRank_conditionα_compl {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (α : ℕ) (B : Set W) : (κ.conditionα A hA α)[B | Aᶜ] = κ[B | Aᶜ]

Conditionalization on A leaves the ranks given Aᶜ unchanged.

theorem RankingFunction.rank_conditionα_eq {W : Type u_1} (κ : RankingFunction W) {A : Set W} (hA : A.Nonempty) (hA' : Aᶜ.Nonempty) (α : ℕ) (B : Set W) : (κ.conditionα A hA α).rank B = min κ[B | A] (κ[B | Aᶜ] + ↑α)

After conditionalization on A at firmness α, a proposition's rank is the smaller of its rank given A and its rank given Aᶜ plus α, which is Jeffrey's rule in ranks.

The induced consequence relation

@[reducible]

def RankingFunction.toPreorder {W : Type u_1} (κ : RankingFunction W) : Preorder W

In the normality order of a ranking function, w is at least as normal as v when its rank is at most that of v.

Equations

• κ.toPreorder = Preorder.lift ⇑κ

theorem RankingFunction.wellFounded_toPreorder_lt {W : Type u_1} (κ : RankingFunction W) : WellFounded LT.lt

theorem RankingFunction.total_toPreorder {W : Type u_1} (κ : RankingFunction W) : Std.Total LE.le

theorem RankingFunction.mem_minimals_toPreorder {W : Type u_1} (κ : RankingFunction W) {A : Set W} {w : W} : w ∈ κ.toPreorder.minimals A ↔ w ∈ A ∧ ∀ v ∈ A, κ w ≤ κ v

The minimal worlds of a proposition are its worlds of least rank.

def RankingFunction.Entails {W : Type u_1} (κ : RankingFunction W) (A B : Set W) : Prop

B follows from A in κ when the A-worlds of least rank are B-worlds. This is the consequence relation of the ranked model κ.toPreorder.

Equations

• κ.Entails A B = Nonmonotonic.Entails κ.toPreorder A B

theorem RankingFunction.entails_iff_forall_least {W : Type u_1} (κ : RankingFunction W) {A B : Set W} : κ.Entails A B ↔ ∀ w ∈ A, (∀ v ∈ A, κ w ≤ κ v) → w ∈ B

theorem RankingFunction.entails_iff_exists_lt {W : Type u_1} (κ : RankingFunction W) {A B : Set W} : κ.Entails A B ↔ ∀ x ∈ A, x ∉ B → ∃ y ∈ A, y ∈ B ∧ κ y < κ x

B follows from A exactly when every A-world outside B is outranked by an A-world in B.

theorem RankingFunction.entails_iff_rank {W : Type u_1} (κ : RankingFunction W) {A B : Set W} : κ.Entails A B ↔ κ.rank A = ⊤ ∨ κ.rank (A ∩ B) < κ.rank (A \ B)

B follows from A exactly when A is impossible or A ∩ B is less disbelieved than A \ B.

theorem RankingFunction.entails_iff_condRank {W : Type u_1} (κ : RankingFunction W) {A B : Set W} : κ.Entails A B ↔ 0 < κ[Bᶜ | A]

B follows from A exactly when Bᶜ has positive rank given A.

@[instance_reducible]

instance RankingFunction.instDecidableEntailsOfFintypeOfDecidablePredMemSet {W : Type u_1} (κ : RankingFunction W) {A B : Set W} [Fintype W] [DecidablePred fun (x : W) => x ∈ A] [DecidablePred fun (x : W) => x ∈ B] : Decidable (κ.Entails A B)

Equations

• κ.instDecidableEntailsOfFintypeOfDecidablePredMemSet = decidable_of_iff (∀ x ∈ A, x ∉ B → ∃ y ∈ A, y ∈ B ∧ κ y < κ x) ⋯

theorem RankingFunction.isRational_entails {W : Type u_1} (κ : RankingFunction W) : Nonmonotonic.IsRational κ.Entails

The consequence relation of a ranking function is rational.

theorem RankingFunction.entails_univ_iff {W : Type u_1} (κ : RankingFunction W) {A : Set W} : κ.Entails Set.univ A ↔ ∀ (w : W), κ w = 0 → w ∈ A

The beliefs, the consequences of the tautology, are the propositions true at every world of rank 0.