Conditional Plausibility and Probabilistic Update

[Hal03] axiomatizes conditional plausibility measures, generalizing Bayesian conditioning, Popper spaces, Jeffrey's rule, and imaging under a single algebraic framework (Cond1–Cond4).

This file formalizes:

1. Conditional probability measures (Popper space axioms P1–P4)
2. The ratio construction (Halpern Thm 3.3.1): FinAddMeasure → CondMeasure
3. Jeffrey's rule: update under uncertain evidence, packaged as a finitely additive measure (jeffreyMeasure)

Conditioning across linglib

Several conditioning operations elsewhere in linglib are instances of conditional plausibility: PMF.condProbSet (BayesianSemantics) is the same ratio construction as toCondMeasure; InfoState.update (Dynamic/Core/Update) is the eliminative special case where P(A|B) ∈ {0, 1}; Spohn ranking conditionalization ([Spo88], Core/Logic/RankingFunction) is its order-of-magnitude analogue. Bayesian conditioning is the point-partition special case of Jeffrey's rule (bayesian_is_jeffrey).

Conditional probability measure (Popper space)

structure ComparativeProbability.CondMeasure (W : Type u_1) extends ComparativeProbability.FinAddMeasure ℚ W : Type u_1

A conditional probability measure: P(A | B) axiomatized directly.

Extends FinAddMeasure with a conditional component satisfying Popper's axioms ([Hal03], Ch. 3, Cond1–Cond4). A set B is normal if P(B|B) ≠ 0; for normal B, P(B|B) = 1. The only abnormal set (for finite W with positive singletons) is ∅.

• mu : Set W → ℚ
• nonneg (A : Set W) : 0 ≤ self.mu A
• additive (A B : Set W) : Disjoint A B → self.mu (A ∪ B) = self.mu A + self.mu B
• total : self.mu Set.univ = 1
• condMu : Set W → Set W → ℚ

  Conditional measure: condMu A B = P(A | B)

• cond_nonneg (A B : Set W) : 0 ≤ self.condMu A B

  P1: non-negativity

• cond_norm (B : Set W) : self.condMu B B ≠ 0 → self.condMu B B = 1

  P2: normalization — P(B|B) = 1 for normal B

• cond_additive (A₁ A₂ B : Set W) : Disjoint A₁ A₂ → self.condMu (A₁ ∪ A₂) B = self.condMu A₁ B + self.condMu A₂ B

  P3: conditional additivity

• cond_chain (A B C : Set W) : self.condMu (A ∩ B) C = self.condMu A (B ∩ C) * self.condMu B C

  P4: chain rule — P(A ∩ B | C) = P(A | B ∩ C) · P(B | C)

• cond_inter (A B : Set W) : self.condMu A B = self.condMu (A ∩ B) B

  Conditioning sees only the part inside the evidence: P(A|B) = P(A ∩ B|B)

• cond_univ (A : Set W) : self.condMu A Set.univ = self.mu A

  Unconditional connection: P(A | Ω) = μ(A)

def ComparativeProbability.CondMeasure.condGe {W : Type u_1} (m : CondMeasure W) (A C B : Set W) : Prop

Conditional comparison: A ≿_B C iff P(A|B) ≥ P(C|B).

Equations

• m.condGe A C B = (m.condMu A B ≥ m.condMu C B)

def ComparativeProbability.CondMeasure.posterior {W : Type u_1} (m : CondMeasure W) (B : Set W) : Set W → ℚ

Posterior measure given evidence B: P_B(A) := P(A|B).

Equations

• m.posterior B A = m.condMu A B

theorem ComparativeProbability.CondMeasure.bayes {W : Type u_1} (m : CondMeasure W) (A B : Set W) : m.condMu A B * m.condMu B Set.univ = m.condMu B A * m.condMu A Set.univ

Bayes' theorem: P(A|B) · P(B) = P(B|A) · P(A). Follows from the chain rule applied in two directions: P(A ∩ B | Ω) = P(A | B) · P(B | Ω) = P(B | A) · P(A | Ω).

theorem ComparativeProbability.CondMeasure.condMu_univ_of_normal {W : Type u_1} (m : CondMeasure W) {B : Set W} (hB : m.condMu B B ≠ 0) : m.condMu Set.univ B = 1

For normal B, P(Ω|B) = 1.

Ratio construction (Halpern Theorem 3.3.1)

noncomputable def ComparativeProbability.FinAddMeasure.toCondMeasure {W : Type u_1} (m : FinAddMeasure ℚ W) : CondMeasure W

Construct conditional probability via the ratio P(A|B) = μ(A ∩ B)/μ(B).

[Hal03], Theorem 3.3.1: every finitely additive measure extends to a conditional measure satisfying P1–P4 via this construction. When μ(B) = 0, P(A|B) = 0 (B is "abnormal" in Popper's sense).

In Lean's ℚ arithmetic, division by zero yields 0, so the abnormal case is handled automatically.

Equations

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

Jeffrey's rule

structure ComparativeProbability.EvidencePartition (W : Type u_1) : Type u_1

An evidence partition: pairwise-disjoint cells covering the space, with new probability assignments summing to 1.

• cells : List (Set W)

  The partition cells

• weights : List ℚ

  New probability for each cell

• aligned : self.cells.length = self.weights.length

  Cells and weights are aligned

• disjointCells : List.Pairwise Disjoint self.cells

  Cells are pairwise disjoint

• exhaustive : List.foldr (fun (x1 x2 : Set W) => x1 ∪ x2) ∅ self.cells = Set.univ

  Cells cover the space

• weights_nonneg (q : ℚ) : q ∈ self.weights → 0 ≤ q

  Weights are non-negative

• weights_sum : self.weights.sum = 1

  Weights sum to 1

def ComparativeProbability.jeffreyUpdate {W : Type u_1} (m : CondMeasure W) (ev : EvidencePartition W) : Set W → ℚ

Jeffrey's rule ([Jef65]; [Hal03] §3.4): update with uncertain evidence, P'(A) = Σᵢ P(A | Eᵢ) · qᵢ.

Equations

• ComparativeProbability.jeffreyUpdate m ev A = (List.map (fun (p : Set W × ℚ) => m.condMu A p.1 * p.2) (ev.cells.zip ev.weights)).sum

theorem ComparativeProbability.jeffreyUpdate_nonneg {W : Type u_1} (m : CondMeasure W) (ev : EvidencePartition W) (A : Set W) : 0 ≤ jeffreyUpdate m ev A

theorem ComparativeProbability.jeffreyUpdate_additive {W : Type u_1} (m : CondMeasure W) (ev : EvidencePartition W) (A B : Set W) (hAB : Disjoint A B) : jeffreyUpdate m ev (A ∪ B) = jeffreyUpdate m ev A + jeffreyUpdate m ev B

theorem ComparativeProbability.jeffreyUpdate_total {W : Type u_1} (m : CondMeasure W) (ev : EvidencePartition W) (hnorm : ∀ E ∈ ev.cells, m.condMu E E ≠ 0) : jeffreyUpdate m ev Set.univ = 1

Jeffrey update is normalized when every cell is normal.

def ComparativeProbability.jeffreyMeasure {W : Type u_1} (m : CondMeasure W) (ev : EvidencePartition W) (hnorm : ∀ E ∈ ev.cells, m.condMu E E ≠ 0) : FinAddMeasure ℚ W

Jeffrey's rule yields a measure: for a partition of normal cells, the Jeffrey update is a finitely additive probability measure.

Equations

• ComparativeProbability.jeffreyMeasure m ev hnorm = { mu := ComparativeProbability.jeffreyUpdate m ev, nonneg := ⋯, additive := ⋯, total := ⋯ }

theorem ComparativeProbability.bayesian_is_jeffrey {W : Type u_1} (m : CondMeasure W) (B A : Set W) : m.condMu A B = jeffreyUpdate m { cells := [B, Bᶜ], weights := [1, 0], aligned := ⋯, disjointCells := ⋯, exhaustive := ⋯, weights_nonneg := ⋯, weights_sum := ⋯ } A

Bayesian conditioning is Jeffrey conditioning with the partition {B, Bᶜ} and weights 1, 0.

Conditional plausibility and epistemic comparison

theorem ComparativeProbability.condMeasure_reflexive_per_evidence {W : Type u_1} (m : CondMeasure W) (B : Set W) : Reflexive fun (A C : Set W) => m.condGe A C B

A conditional measure induces a conditional epistemic comparison: A ≿_B C iff P(A|B) ≥ P(C|B). This conditional comparison is reflexive for each fixed B.