Conditional Plausibility and Probabilistic Update

@cite{halpern-2003} @cite{jeffrey-1965}@cite{halpern-2003} 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
4. Conditioning modes: classifying the update operations across linglib

Conditioning Unification

Four conditioning operations in linglib are instances of conditional plausibility:

Module	Operation	Mode
EpistemicScale/Conditional	condMu A B	Bayesian (ratio)
BayesianSemantics	FinitePMF.prob	Bayesian (marginalization)
Dynamic/Core/Update	InfoState.update s φ	Eliminative
SDS/MeasureTheory	(placeholder)	Continuous Bayesian

The eliminative mode is the special case where P(A|B) ∈ {0, 1}: each world either survives or is eliminated.

inductive Core.Scale.ConditioningMode : Type

Classification of conditioning modes used across linglib.

• eliminative: keep only worlds satisfying evidence. The resulting measure is 0/1-valued. (Dynamic/Core/Update.lean)
• bayesian: P(A|B) = P(A ∩ B)/P(B). Standard ratio conditioning. (BayesianSemantics.lean, this file)
• jeffrey: update with uncertain evidence over a partition. Generalizes Bayesian: P'(A) = Σᵢ P(A|Eᵢ) · q(Eᵢ).

• eliminative : ConditioningMode
• bayesian : ConditioningMode
• jeffrey : ConditioningMode
• ranking : ConditioningMode

instance Core.Scale.instDecidableEqConditioningMode : DecidableEq ConditioningMode

Equations

• Core.Scale.instDecidableEqConditioningMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Scale.instBEqConditioningMode : BEq ConditioningMode

Equations

• Core.Scale.instBEqConditioningMode = { beq := Core.Scale.instBEqConditioningMode.beq }

def Core.Scale.instBEqConditioningMode.beq : ConditioningMode → ConditioningMode → Bool

Equations

• Core.Scale.instBEqConditioningMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Scale.instReprConditioningMode : Repr ConditioningMode

Equations

• Core.Scale.instReprConditioningMode = { reprPrec := Core.Scale.instReprConditioningMode.repr }

def Core.Scale.instReprConditioningMode.repr : ConditioningMode → ℕ → Std.Format

Equations

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

structure Core.Scale.CondMeasure (W : Type u_1) extends Core.Scale.FinAddMeasure W : Type u_1

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

Extends FinAddMeasure with a conditional component satisfying Popper's axioms (@cite{halpern-2003}, 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) : (∀ x ∈ A, x ∉ 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) : (∀ x ∈ A₁, x ∉ 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_univ (A : Set W) : self.condMu A Set.univ = self.mu A

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

def Core.Scale.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 Core.Scale.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 Core.Scale.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 | Ω).

noncomputable def Core.Scale.FinAddMeasure.toCondMeasure {W : Type u_1} (m : FinAddMeasure W) : CondMeasure W

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

@cite{halpern-2003}, 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

• m.toCondMeasure = { toFinAddMeasure := m, condMu := fun (A B : Set W) => m.mu (A ∩ B) / m.mu B, cond_nonneg := ⋯, cond_norm := ⋯, cond_additive := ⋯, cond_chain := ⋯, cond_univ := ⋯ }

structure Core.Scale.EvidencePartition (W : Type u_1) : Type u_1

An evidence partition: a finite collection of mutually exclusive, exhaustive propositions with new probability assignments.

• 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

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

  Weights are non-negative

• weights_sum : self.weights.sum = 1

  Weights sum to 1

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

Jeffrey's rule: update a conditional measure with uncertain evidence.

Given a partition {E₁,..., Eₙ} with new probabilities q₁,..., qₙ: P'(A) = Σᵢ P(A | Eᵢ) · qᵢ

This generalizes Bayesian conditioning: standard conditioning on E is the special case where qₑ = 1 and all other qᵢ = 0.

@cite{jeffrey-1965}, The Logic of Decision; @cite{halpern-2003} §3.4.

Equations

• Core.Scale.jeffreyUpdate m ev A = List.foldl (fun (acc : ℚ) (x : Set W × ℚ) => match x with | (E, q) => acc + m.condMu A E * q) 0 (ev.cells.zip ev.weights)

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

theorem Core.Scale.bayesian_is_jeffrey {W : Type u_1} (m : CondMeasure W) (B : Set W) (_hB : m.condMu B B ≠ 0) (A : Set W) : m.condMu A B = jeffreyUpdate m { cells := [B], weights := [1], aligned := ⋯, weights_nonneg := ⋯, weights_sum := ⋯ } A

Bayesian conditioning is Jeffrey conditioning with a point partition.

theorem Core.Scale.condMeasure_systemW_per_evidence {W : Type u_1} (m : CondMeasure W) (B : Set W) : EpistemicAxiom.R 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 satisfies reflexivity and monotonicity (System W axioms) for each fixed B.

def Core.Scale.CondMeasure.inducedCondGe {W : Type u_1} (m : CondMeasure W) (A C B : Set W) : Prop

A conditional measure extends to a conditional comparison on propositions: A is conditionally at least as likely as C given B iff P(A|B) ≥ P(C|B). This is the conditional version of FinAddMeasure.inducedGe.

Equations

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