Birnbaum's principles in Venn diagrams: Extended version with Lean verification
Jaime Enrique Lincovil Curivil, Alexandre Galvão Patriota
math.ST
Sep 22, 2026 · v1
TL;DR
Birnbaum's theorem relating likelihood, sufficiency, and conditionality principles is formalized and certified in Lean using a finite-sample statistical-relations framework.
Abstract
Birnbaum's theorem states that the sufficiency and conditionality principles jointly imply, and are implied by, the likelihood principle. To enable formal certification of the results in Lean, we make the conditionality relation explicit through a finite-sample formulation based on \cite{Evans2013}. We reformulate the theorem as a statement about classes of statistical procedures that preserve statistical relations, and show that the proof reduces to the propagation of evidential equality along chains of conditionality-related inference bases (experiment–observation pairs). The main results are illustrated by Venn diagrams, and a worked finite example exhibits two pairs of inference bases: one related by conditionality but not by sufficiency, and the other related by sufficiency but not by conditionality. For finite parameter spaces with at least two points, the class of likelihood-invariant procedures with codomain $[0,1]$ is strictly contained in the class of sufficiency-invariant procedures.
Problem
Birnbaum's theorem states that the sufficiency and conditionality principles jointly imply and are implied by the likelihood principle. The classical formulation resists formal certification because the conditionality relation is not made explicit.
Approach
The conditionality relation is made explicit through a finite-sample formulation based on Evans (2013). The theorem is reformulated as a statement about classes of statistical procedures that preserve statistical relations. The proof reduces to propagation of evidential equality along chains of conditionality-related inference bases, and the results are certified in Lean.
Results
For finite parameter spaces with at least two points, the class of likelihood-invariant procedures equals the class of conditionality-invariant procedures and is strictly contained in the class of sufficiency-invariant procedures. The joint formulation reduces to the closure identity L equals the closure of C union S.
