Bayesian Confirmation Measures on PMF

[Fit99] [Fit07] [CFT08] [Edw92] [CM23]

Confirmation-theoretic aggregates over a PMF α. Three pieces:

1. Count-of-relevant-propositions countMeasure R: the function μ_R(w) = |{r ∈ R ∣ r(w)}| of [CM23], as an ℝ≥0∞-valued function on worlds.

2. Explanatory value sumLikelihoods p R φ = Σ_{e ∈ R} P(e ∣ φ) — [CM23]'s aggregate in its directly-evaluable form. The identity P.condExpect φ (countMeasure R) = sumLikelihoods P R φ is what underlies C&M's "expected utility = explanatory value" claim; it is not proved here — when a Studies file needs it, add it next to condExpect_indicator in Core.Probability.Finite.

3. Difference and likelihood-ratio measures (differenceMeasure, likelihoodRatio) from the [Fit99] plurality survey.

Scope

The log-based likelihood-ratio L(h, e) = log(P(e∣h)/P(e∣¬h)) is not defined: Real.log on ENNReal ratios is noncomputable and not decide-friendly. The un-logged likelihoodRatio is provided; log is order-preserving so >/< claims transfer.

[CFT08]'s Z, Kemeny-Oppenheim K, and the other measures from [Fit99] are not stocked here. Add them when a Studies file actually consumes them.

Mathlib's heavy MeasureTheory.condExp is the general measure-theoretic counterpart for the underlying conditional expectation; this file's Core.Probability.Finite.condExpect is the lightweight finite-PMF wrapper. See its docstring for the design rationale.

Count of relevant propositions (C&M's μ_R)

noncomputable def PMF.Confirmation.countMeasure {α : Type u_1} (R : Finset (Set α)) : α → ENNReal

μ_R(a) of [CM23]: the count of propositions r ∈ R that are true at a. ENNReal-valued so it composes with PMF arithmetic. Each r : Set α is an arbitrary predicate; Classical.dec discharges the per-element decidability that Finset.filter requires.

Equations

• PMF.Confirmation.countMeasure R a = ↑{x ∈ R | a ∈ x}.card

Explanatory value (C&M's sum of likelihoods)

noncomputable def PMF.Confirmation.sumLikelihoods {α : Type u_1} (p : PMF α) (R : Finset (Set α)) (φ : Set α) : ENNReal

Sum of likelihoods over an evidence-set R given hypothesis φ: Σ_{e ∈ R} P(e ∣ φ). [CM23]'s "explanatory value" in its directly-evaluable form.

Equations

• PMF.Confirmation.sumLikelihoods p R φ = ∑ e ∈ R, p.condProbSet φ e

Bayesian difference and likelihood-ratio measures

noncomputable def PMF.Confirmation.differenceMeasure {α : Type u_1} (p : PMF α) (h e : Set α) : ℝ

The difference measure D(h, e) = P(h ∣ e) − P(h) of [Fit99]. ℝ-valued because the subtraction would lose sign under ENNReal's truncated subtraction. Negative values indicate that e disconfirms h. Used by [CM23] §5 in the plausibility-requirement discussion.

Equations

• PMF.Confirmation.differenceMeasure p h e = (p.condProbSet e h).toReal - (p.probOfSet h).toReal

noncomputable def PMF.Confirmation.likelihoodRatio {α : Type u_1} (p : PMF α) (h e : Set α) : ENNReal

The un-logged likelihood-ratio P(e ∣ h) / P(e ∣ ¬h). Equals 1 on irrelevance, exceeds 1 on confirmation. [Fit07]'s L is the log of this; we keep the ratio for decide-checkability.

Equations

• PMF.Confirmation.likelihoodRatio p h e = p.condProbSet h e / p.condProbSet hᶜ e