Spohn (1988): Ordinal Conditional Functions: A Dynamic Theory of Epistemic States #
This file formalizes the theory of ordinal conditional functions of [Spo88] with
natural-number grades, the paper's Note 16, on the ranking functions of
Logic/RankingFunction.lean. Conditionalization on a proposition at a firmness is reversible:
conditionalizing again on the proposition at the firmness with which it was believed restores
the ranking, whether the first change conditionalized on the proposition or on its negation
(conditionα_conditionα, conditionα_compl_conditionα); and two conditionalizations commute
when the three cells they distinguish other than the joint negation have rank zero
(conditionα_comm). Generalized conditionalization by a ranking on the atoms of a subfield,
the deterministic counterpart of Jeffrey conditionalization, has conditionalization on a
proposition as its two-atom case (condition_firmness) and is reversed by conditionalizing on
the coarsening of the original ranking to the subfield (condition_condition_coarsen).
Independence of two subfields, the rank of an intersection of atoms being the sum of the ranks,
extends from atoms to all members of the fields (Independent.rank_inter), and it is
equivalent to conditional ranks being unconditional ranks and to the ranks of one field being
invariant under generalized conditionalization on the other (independent_iff_condRank,
independent_iff_condition). Conditional independence given a subfield satisfies the
contraction law of the paper's Theorem 11 and its mirror image (CondIndependentOn.inf,
CondIndependentOn.inf').
Implementation notes #
Complete subfields of the propositions over a set of worlds are partitions, Setoid W: the
atoms are the cells, the members are the propositions the partition decides, and the field two
subfields generate is their meet in the lattice of setoids. Over natural numbers every two
firmnesses commute and independence is symmetric, so the paper's two directions of
independence coincide. Simple conditional functions and well-ordered partitions with their
representation theorem, the independence of sequences of subfields, Theorem 13, whose
conclusion conditions on the intersection of two subfields, and the nonstandard-probability
homomorphism of Section 7 are not formalized.
References #
Reversibility and commutativity of conditionalization #
After conditionalizing on A at any firmness, conditionalizing on A at the firmness with
which A was believed restores the ranking (Theorem 3, first half).
After conditionalizing on the negation of A at any firmness, conditionalizing on A at
the firmness with which A was believed restores the ranking (Theorem 3, second half).
Conditionalizations on A and on B commute when the cells A ∩ B, A ∩ Bᶜ and
Aᶜ ∩ B all have rank zero (Theorem 4).
Generalized conditionalization #
The conditionalization of κ by a ranking l on the atoms of a subfield (Definition 7)
ranks each world by the rank of its atom under l plus its rank within the atom.
Equations
- Spohn1988.condition κ 𝔅 l = { toFun := fun (w : W) => l ⟦w⟧ + κ.aPart (𝔅.cell w) w, exists_eq_zero' := ⋯ }
Instances For
Within an atom, the conditionalized ranking starts at the atom's rank under l.
The two-atom ranking that believes A with firmness α.
Equations
- Spohn1988.firmness A hA α = { toFun := Quotient.lift (fun (w : W) => if w ∈ A then 0 else α) ⋯, exists_eq_zero' := ⋯ }
Instances For
Conditionalization on A at firmness α is generalized conditionalization by the two-atom
ranking believing A with firmness α (Theorem 5).
The coarsening of κ to a subfield ranks each atom by its rank under κ.
Equations
- Spohn1988.coarsen κ 𝔅 = { toFun := Quotient.lift (fun (w : W) => (κ.rank (𝔅.cell w)).toNat) ⋯, exists_eq_zero' := ⋯ }
Instances For
Generalized conditionalization is reversed by conditionalizing on the coarsening of the original ranking to the subfield (Theorem 6).
Independence #
ℭ is independent of 𝔅 with respect to κ (Definition 8) when every atom of 𝔅 meets
every atom of ℭ and the rank of their intersection is the sum of their ranks.
Equations
Instances For
Independence extends from atoms to all satisfiable members of the fields (Theorem 7).
On a satisfiable intersection, the conditional rank is a difference of natural numbers.
On satisfiable intersections, κ(X | A) = κ(Y | A) + κ(Z | A) says that
κ(A ∩ X) + κ(A) = κ(A ∩ Y) + κ(A ∩ Z).
Independence holds exactly when, for satisfiable members B of 𝔅 and C of ℭ, the
rank of C given B is the rank of C (Theorem 8, (a) and (b)).
Independence holds exactly when generalized conditionalization on any ranking of the atoms
of 𝔅 leaves the ranks of the satisfiable members of ℭ unchanged (Theorem 8, (a) and
(c)).
Conditional independence #
ℭ is independent of 𝔅 given A with respect to κ (Definition 10) when
κ(B ∩ C | A) = κ(B | A) + κ(C | A) for atoms B of 𝔅 and C of ℭ meeting A.
Equations
Instances For
ℭ is independent of 𝔅 given the subfield 𝔇 when it is so given each atom of 𝔇.
Equations
- Spohn1988.CondIndependentOn κ 𝔅 ℭ 𝔇 = ∀ (d : W), Spohn1988.CondIndependent κ 𝔅 ℭ (𝔇.cell d)
Instances For
If ℭ is independent of 𝔅 given 𝔇 + 𝔈 and 𝔇 is independent of 𝔅 given 𝔈, then
ℭ + 𝔇 is independent of 𝔅 given 𝔈 (Theorem 11).
If 𝔅 is independent of ℭ given 𝔇 + 𝔈 and of 𝔇 given 𝔈, then it is independent
of ℭ + 𝔇 given 𝔈 (Theorem 12).