Documentation

Linglib.Core.Logic.RankingFunction

Ranking Functions and Iterated Belief Revision #

@cite{halpern-2003} @cite{darwiche-pearl-1997} @cite{spohn-1988}

Ranking functions (ordinal conditional functions, OCFs) provide a qualitative, ordinal approach to belief revision that serves as the quantitative semantics for System P + Rational Monotonicity.

@cite{spohn-1988} introduced ranking functions as ordinal-valued measures of disbelief. We restrict to ℕ-valued rankings, following the simplification noted in Note 16 of the paper. κ(w) = 0 means w is maximally plausible (believed possible), while higher ranks indicate greater implausibility. The normalization condition — some world has rank 0 — ensures the belief state is non-vacuous.

Key Results #

  1. Ranking → Plausibility: Every ranking function induces a plausibility ordering (§1), which in turn yields a preferential consequence relation satisfying System P.

  2. Connectedness: Because ℕ is totally ordered, the induced plausibility ordering is connected (any two worlds are comparable), so Rational Monotonicity holds.

  3. A-part (Def. 5): κ(w|A) = κ(w) - κ(A) extracts the relative ranking within A-worlds, shifted so the best A-world has rank 0.

  4. A,α-conditionalization (Def. 6): The revision operation parameterized by firmness α. Higher α = firmer belief in the evidence.

  5. Independence (Def. 8): κ(B ∩ C) = κ(B) + κ(C) when B,C are independent — the ordinal analogue of probabilistic independence.

  6. Darwiche-Pearl Postulates: Ranking conditioning satisfies the iterated revision postulates C1–C4 (§2), which AGM alone does not constrain.

See Phenomena.DefaultReasoning.Studies.Spohn1988 for a verified concrete instance demonstrating evidence strength, commutativity (Theorem 4), and the connection to NormalityOrder.

Bridge to Probability (@cite{spohn-1988} §7) #

Ranking conditioning is the ordinal analogue of Bayesian conditioning. The structural parallel (min/+ for ordinals mirrors product/sum for probabilities):

Probability (ℚ, ·, Σ)Ranking (ℕ, min, +)
P(A) = Σ_{w∈A} P(w)κ(A) = min_{w∈A} κ(w)
P(AB) = P(A∩B)/P(B)
P(A∩B) = P(A)·P(BA)
P(A∩B) = P(A)·P(B) (indep.)κ(A∩B) = κ(A) + κ(B) (indep.)

See ConditioningMode.ranking in Core/Scales/EpistemicScale/Conditional.lean for the conditioning-mode classification.

A ranking function (ordinal conditional function) on worlds.

κ : W → ℕ assigns each world a degree of disbelief. Normalization: some world has rank 0 (the agent considers at least one world possible).

@cite{spohn-1988}, Definition 4 uses ordinals in the general case; we restrict to ℕ following Note 16 of the paper.

  • rank : W

    The rank (degree of disbelief) of each world

  • normalized : ∃ (w : W), self.rank w = 0

    At least one world has rank 0

Instances For
    noncomputable def Core.Logic.Ranking.RankingFunction.rankProp {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] (hsat : ∃ (w : W), φ w) :

    The rank of a proposition: the minimum rank among worlds satisfying it. Requires the proposition to be satisfiable.

    κ(φ) = min { κ(w) | φ w }

    Equations
    Instances For
      noncomputable def Core.Logic.Ranking.RankingFunction.aPart {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] ( : ∃ (w : W), φ w) (w : W) :

      The A-part of κ: the ranking restricted to A-worlds, shifted so the most plausible A-world has rank 0.

      @cite{spohn-1988}, Definition 5: κ(w|A) = κ(w) - κ(A) for w ∈ A. This is the primitive from which conditioning derives.

      Equations
      Instances For
        theorem Core.Logic.Ranking.RankingFunction.rankProp_dichotomy {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] [DecidablePred fun (w : W) => ¬φ w] ( : ∃ (w : W), φ w) (hNφ : ∃ (w : W), ¬φ w) :
        κ.rankProp φ = 0 κ.rankProp (fun (w : W) => ¬φ w) hNφ = 0

        @cite{spohn-1988}, Theorem 2(a): For any proposition, either it or its negation has rank 0 (or both).

        Normalization propagates from worlds to propositions: the rank-0 world satisfies either φ or ¬φ, making that side's rankProp = 0. This is the ordinal analogue of P(A) + P(Ā) = 1.

        theorem Core.Logic.Ranking.RankingFunction.rankProp_union {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ ψ : WProp) [DecidablePred φ] [DecidablePred ψ] [DecidablePred fun (w : W) => φ w ψ w] ( : ∃ (w : W), φ w) ( : ∃ (w : W), ψ w) :
        κ.rankProp (fun (w : W) => φ w ψ w) = min (κ.rankProp φ ) (κ.rankProp ψ )

        @cite{spohn-1988}, Theorem 2(b): The rank of a disjunction is the minimum of the disjuncts' ranks.

        κ(A ∪ B) = min(κ(A), κ(B)) for any non-empty A, B. This is because κ takes the minimum over worlds, and the minimum over a union equals the min of the minima over each part.

        This is the ordinal analogue of P(A ∪ B) = P(A) + P(B) for disjoint events (and ≤ for overlapping ones).

        A ranking function induces a plausibility ordering: w is at least as plausible as v iff κ(w) ≤ κ(v).

        Smoothness follows from the well-orderedness of ℕ: every non-empty subset of ℕ has a minimum, so among the φ-worlds with rank ≤ κ(w), we can find a minimal one.

        Equations
        Instances For

          The preferential consequence relation induced by a ranking function. Composes toPlausibilityOrder with PlausibilityOrder.toPreferential.

          Equations
          Instances For

            Ranking functions induce connected (total) plausibility orderings: for any two worlds, one is at least as plausible as the other.

            This follows from ℕ being linearly ordered. Connectedness is what distinguishes ranked models from merely preferential models and is what makes Rational Monotonicity hold.

            noncomputable def Core.Logic.Ranking.RankingFunction.conditionα {W : Type u_1} [Fintype W] [DecidableEq W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] ( : ∃ (w : W), φ w) (hNφ : ∃ (w : W), ¬φ w) (α : ) :

            A,α-conditionalization: revise κ by evidence φ with firmness α.

            @cite{spohn-1988}, Definition 6: κ_{A,α}(w) = κ(w|A) for w ∈ A, and α + κ(w|Ā) for w ∈ Ā. The parameter α controls how firmly the evidence is believed:

            • α = 0: neutral update (evidence doesn't change relative plausibility of ¬φ-worlds vs φ-worlds)
            • α > 0: φ-worlds become more plausible than ¬φ-worlds by at least α ranks
            • Large α: very firm belief in the evidence

            @cite{goldszmidt-pearl-1996} call this J-conditioning (after Jeffrey); the operation is identical under the name change α = j.

            Requires both φ and ¬φ to be satisfiable (matching Spohn's requirement that A ∉ {∅, W}).

            Equations
            Instances For

              Ranking functions satisfy Rational Monotonicity.

              Because ℕ is totally ordered, the induced plausibility ordering is ranked (any two worlds are comparable). For ranked models, Rational Monotonicity holds: if φ | χ and ¬(φ | ¬ψ), then (φ ∧ ψ) |~ χ.

              Proof sketch: From ¬(φ | ¬ψ), there exists a minimal φ-world v satisfying ψ. Since ℕ is total, every minimal (φ∧ψ)-world has rank ≤ rank of any φ-world. So minimal (φ∧ψ)-worlds are among the minimal φ-worlds, and since φ | χ, they satisfy χ.

              The belief set of a ranking function: propositions true at all rank-0 worlds. These are the agent's current beliefs.

              Equations
              Instances For
                noncomputable def Core.Logic.Ranking.RankingFunction.revise {W : Type u_1} [Fintype W] [DecidableEq W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] ( : ∃ (w : W), φ w) (hNφ : ∃ (w : W), ¬φ w) :

                Spohn revision: α-conditionalization with canonical firmness α = κ(¬φ) + 1.

                This is the standard belief-revision operator for ranking functions (@cite{spohn-1988}). The firmness is determined by the current ranking, not a free parameter: the agent revises just firmly enough to make φ believed (the success postulate).

                C1 and C2 hold for conditionα with arbitrary α, β. C3 and C4 require the canonical firmness — a counterexample with α = β = 1 on a 4-world ranking shows the universally-quantified version is false.

                Equations
                Instances For

                  Darwiche-Pearl postulate C1: if φ → ψ then (κ *{ψ,β} ) *{φ,α} = κ *_{φ,α}. Revising first by a weaker ψ (with any firmness β), then by a stronger φ that entails it (with any firmness α), yields the same result as revising directly by φ with firmness α.

                  For ranking conditioning: if every φ-world is a ψ-world, then conditioning on ψ first doesn't change the relative ranks among φ-worlds after subsequent φ-conditioning.

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

                    Darwiche-Pearl postulate C2: if φ → ¬ψ then (κ *{ψ,β} ) *{φ,α} = κ *_{φ,α}. If φ and ψ are incompatible, revising by ψ first doesn't affect the outcome of subsequent revision by φ.

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

                      Darwiche-Pearl postulate C3: if ψ ∈ beliefSet(κ * φ), then ψ ∈ beliefSet((κ * ψ) * φ). If ψ is believed after revising by φ, then revising first by ψ preserves this.

                      Uses the canonical revise operator (firmness = κ(¬φ) + 1). The version with arbitrary firmness parameters is false — see the revise docstring.

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

                        Darwiche-Pearl postulate C4: if ¬ψ ∉ beliefSet(κ * φ), then ¬ψ ∉ beliefSet((κ * ψ) * φ). If ¬ψ is not believed after revising by φ, then revising first by ψ doesn't make ¬ψ believed either.

                        Uses the canonical revise operator (firmness = κ(¬φ) + 1).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem Core.Logic.Ranking.RankingFunction.rankProp_le_rank {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] (hsat : ∃ (w : W), φ w) (w : W) (hw : φ w) :
                          κ.rankProp φ hsat κ.rank w

                          rankProp is ≤ any satisfying world's rank.

                          Theorem: Ranking conditioning satisfies C1.

                          When φ → ψ, conditioning κ on ψ shifts all ψ-worlds (including all φ-worlds) down by κ(ψ). Then conditioning on φ shifts the φ-worlds down by the new κ_ψ(φ) = κ(φ) - κ(ψ). Net shift for φ-worlds: κ(w) - κ(ψ) - (κ(φ) - κ(ψ)) = κ(w) - κ(φ), which equals direct conditioning on φ.

                          Theorem: Ranking conditioning satisfies C2.

                          When φ and ψ are disjoint, φ-worlds are ¬ψ-worlds. After conditioning on ψ with firmness β, φ-worlds are shifted up by β + (A-part relative to ¬ψ). Subsequent conditioning on φ normalizes away this shift: the relative ordering among φ-worlds depends only on their original ranks.

                          Theorem: Ranking conditioning satisfies C3.

                          If w is rank-0 in (κ*ψ)*φ but ¬ψ w, then κ'(w) = κ(w) + 1 (¬ψ-worlds are penalized by revise). But the hypothesis gives a witness v₀ with φ v₀, ψ v₀, κ(v₀) = κ(φ), so κ'(v₀) = κ(v₀) − κ(ψ) ≤ κ(φ) ≤ κ(w) < κ(w) + 1 = κ'(w), contradicting w being rank-minimal among φ-worlds in κ'.

                          Theorem: Ranking conditioning satisfies C4.

                          The hypothesis gives v₀ with rank 0 in κφ and ψ v₀. We show v₀ also has rank 0 in (κψ)*φ: since ψ v₀, κ'(v₀) = κ(v₀) − κ(ψ), and this is minimal among φ-worlds in κ' because φ∧ψ-worlds have κ' ≥ κ(φ) − κ(ψ) = κ'(v₀) and φ∧¬ψ-worlds have κ' = κ(w) + 1 > κ(φ) ≥ κ'(v₀).

                          def Core.Logic.Ranking.RankingFunction.independent {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ ψ : WProp) [DecidablePred φ] [DecidablePred ψ] [DecidablePred fun (w : W) => φ w ψ w] ( : ∃ (w : W), φ w) ( : ∃ (w : W), ψ w) (hφψ : ∃ (w : W), φ w ψ w) :

                          Two propositions are independent with respect to κ iff κ(φ ∩ ψ) = κ(φ) + κ(ψ).

                          @cite{spohn-1988}, Definition 8 (simplified from σ-fields to propositions). This is the ordinal analogue of probabilistic independence P(A ∩ B) = P(A) · P(B): where probability uses multiplication, ranking uses addition.

                          Equations
                          Instances For
                            noncomputable def Core.Logic.Ranking.RankingFunction.lCondition {W : Type u_1} [Fintype W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] (h0 : ∃ (w : W), φ w κ.rank w = 0) (l : ) :

                            L-conditioning: shift-based belief revision.

                            @cite{goldszmidt-pearl-1996}, Eqs. 29–30: L-conditioning with l ≥ 0 keeps φ-worlds at their original rank and shifts ¬φ-worlds up by l. Unlike J-conditioning (conditionα), L-conditioning is commutative: κ_{A,l₁}{B,l₂} = κ{B,l₂}_{A,l₁}.

                            This is the κ(φ) = 0 specialization of the general L-conditioning (G&P Eq. 32). The general form subtracts κ(φ) from all worlds first, but the precondition h0 : ∃ w, φ w ∧ κ.rank w = 0 guarantees κ(φ) = 0, so the subtraction vanishes for φ-worlds.

                            Equations
                            Instances For
                              theorem Core.Logic.Ranking.RankingFunction.revise_success {W : Type u_1} [Fintype W] [DecidableEq W] (κ : RankingFunction W) (φ : WProp) [DecidablePred φ] ( : ∃ (w : W), φ w) (hNφ : ∃ (w : W), ¬φ w) :
                              φ (κ.revise φ hNφ).beliefSet

                              AGM success postulate (K*2): after revision by φ, the evidence φ is believed (all rank-0 worlds satisfy φ).

                              @cite{goldszmidt-pearl-1996} §6: ranking revision satisfies the AGM postulates. The proof is direct: ¬φ-worlds receive rank ≥ α = κ(¬φ) + 1 ≥ 1, so they cannot be rank-0 in the revised ranking.