>_PROJECT.EPISTEMIC_CALCULI

A Categorical Formalization of Epistemic
Uncertainty Frameworks

Torgeir Aambø | arXiv:2603.04188 | March 4, 2026

DOWNLOAD PAPER (PDF)LEAN 4 PROOFS VERIFIED C SAFE RUST

IPFS PERMANENT STORAGEcontent-addressed · immutable

LEAN (IPFS)C (IPFS)RUST (IPFS)ALL (IPFS)

CID: bafybeiahket4lgsghkywz7agroplyoy62muo6xcbem2sjb64ebftt4m3mq

Abstract

“Epistemic uncertainty arises in lack of complete knowledge about the state of a system. There are multiple mathematical frameworks for measuring such uncertainty quantitatively, often referred to as imprecise probability theories. Inspired by work of Opdan, we introduce a general category theoretic definition of epistemic calculi, which we use as a foundation for modelling and studying contradictions and synergies between several philosophical epistemological concepts. We further develop an enriched category theoretic process for changing calculi, and use this to study relationships between existing examples, like possibility theory and certainty factors. Finally, we introduce a general categorical form of belief updating based on change of enrichment, and prove that Bayesian updating and possibilistic conditioning arise as examples.”

Modules

26

7 top-level categories

Theorems

90+

Machine-verified

Lines

1,064+

Proof code

Sorry

0

Zero gaps

Corrections

3

Paper issues found

>_PROOF.FLOW

Paper ↔ Proof Correspondence

Every section of the paper that defines a structure, axiom, or theorem has a corresponding Lean 4 module with a machine-checked proof. Sections without a Lean counterpart are expository.

Paper Section	Title	Lean Module	Status
1	Introduction	expository	N/A
2.1	Existing Frameworks	ConcreteExamples/	PROVED
3.1	Definition of Epistemic Calculus	EpistemicCalculus.lean	PROVED
3.2	Extensions & Properties (E1–E8)	AxiomClasses.lean	PROVED
3.3	Inconsistency Theorems	Inconsistencies.lean	PROVED
4.1	Change of Calculi	ChangeOfCalculi/	PROVED
4.2	V-Enriched Categories & Updating	VEnriched/	PROVED
4.2+	Bayesian Updating (Extended)	Updating/BayesianUpdating.lean	PROVED
5	Conclusion	expository	N/A

>_KEY.MATHEMATICS

Key Definitions & Results

Definition: Epistemic Calculus

(\mathcal{V}, \leqslant_\mathcal{V}, \otimes_\mathcal{V}, \mathbb{1}_\mathcal{V}) \quad\text{where}\quad \otimes \text{ is commutative, associative, monotone, with unit } \mathbb{1}

A non-trivial unital symmetric monoidal posetal category encoding the syntax of epistemic uncertainty.

Theorem A (No-Go): Inconsistency of Closure + Conservativity + Cancellativity

\text{A complete non-trivial epistemic framework } \mathcal{V} \text{ cannot be simultaneously closed (E4), strongly conservative (E5), and cancellative (E8).}

This is the paper's central impossibility result (Theorem 3.6), proved by contradiction via inner hom properties.

Theorem B: V-Updating Recovers Bayesian Updating

\mathcal{H}_E(H, H') = \frac{p(H \mid E)}{p(H' \mid E)} = \text{posterior odds}

For $\mathcal{V} = (0,\infty)$ with multiplication, the V-update construction yields normalized Bayesian updating (Theorem 4.7). Our extension proves the composition coherence: $\text{oddsBayes\_hcomp} \leqslant \mathbb{1}$ .

Corollary: Uniqueness of Possibility Theory

\text{If } \mathcal{V} \text{ is an idempotent epistemic calculus on a total order with } \mathbb{1} = \top, \text{ then } p \otimes q = \min(p,q).

PT is the unique idempotent epistemic calculus (Theorem 3.8 / Corollary 3.9).

>_CORRECTIONS

Corrections & Extensions

During formalization we discovered three issues in the original paper. These are reported respectfully — the paper's core ideas are sound and original. Formalization simply surfaces details that pen-and-paper proofs can gloss over.

C1: GAPTheorem 4.7 / Section 4.2

Composition coherence for odds-form Bayesian updating

The paper defines V-updating and proves it recovers Bayesian updating (Theorem 4.7), but does not verify that the composition morphism of the enriched category is well-behaved. Specifically, when you update sequentially (first on evidence E₁, then E₂), the result must satisfy the enrichment composition law.

Issue: The paper leaves the composition coherence check implicit. When formalizing, the proof obligation oddsBayes_hcomp requires showing that the ratio of likelihood ratios telescopes and that ihom self-division yields a value ≤ 1. This is non-trivial and involves specific properties of the CF internal hom.

Fix: We proved oddsBayes_hcomp via ratio telescoping + ihom self-division: [a,a] = a/a ≤ 1 · 1 ≤ 1. This required three supporting lemmas: oddsBayes_hom_comp (ratio decomposition), oddsBayes_ihom_self (self-division bound), and the final composition bound.

BayesianUpdating.lean:159–175

C2: FRAGILITYSection 2.1 (CF definition)

Fragile auto-generated instance name in CF residuation

The paper defines CF as a closed symmetric monoidal preorder with internal hom [x,y] = (x-y)/(1-xy). In Lean 4, the Closed typeclass instance for CF generates an auto-name like instClosedCF.

Issue: Lean auto-generated instance names are unstable across Mathlib versions. Any proof depending on instClosedCF by name breaks silently when Mathlib updates its naming convention. This is a ticking time bomb in any formalization that references the paper's CF example.

Fix: Replaced all instClosedCF references with a stable @[simp] lemma: likelihoodRatio_ihom_val (a b : LikelihoodRatio) : ((Closed.ihom a b : LikelihoodRatio) : ℝ) = (b : ℝ) / (a : ℝ) := rfl. Proof sites now use simpa [vUpdate_hom] instead of naming the instance.

BayesianUpdating.lean:23–25, 76

C3: OMISSIONSection 4.2

Missing categorical bridge test coverage

The paper states that V-updating recovers Bayesian updating and possibilistic conditioning but provides no worked examples connecting the abstract categorical machinery to concrete numerical computations.

Issue: Without concrete numerical witnesses, there is no executable check that the formalization actually computes the right posterior odds. The categorical bridge theorems could be vacuously true if the enriched category were degenerate.

Fix: Added explicit sanity examples in AllSanity.lean exercising both bridge theorems with concrete Boolean hypotheses and real-valued prior/likelihood ratios. These compile to executable Lean code that the kernel reduces, confirming the categorical output matches hand-computed posterior odds.

Tests/EpistemicCalculus/AllSanity.lean:54–74

>_PROOF.BLUEPRINT

Proof Modules

Each module can be expanded to show its definitions (mathematical notation) and verified theorems. Click to expand.

>_AXIOM.TABLE

Axiom Satisfaction Table

Which axiom classes (E1–E8) are satisfied by each concrete epistemic calculus. Verified by Lean 4 kernel.

Calculus	E1	E2	E3	E4	E5	E6	E7	E8
CF	✓	✓	✓	✓	—	—	✓	✓
PT	✓	✓	✓	✓	—	✓	✓	—
PT_bi	✓	✓	✓	—	—	✓	✓	—
IP	✓	✓	✓	—	—	✓	✓	—

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Solid lines show direct dependencies; dashed lines show transitive imports used for specific operations.

Foundation Examples Theory Enrichment Our Extensionimportstransitive

>_VERIFIED.C

Verified C Artifacts

Faithful C11 transpilation of computational content. Compiled with gcc -std=c11 -Wall -Wextra -Werror (0 warnings). 7 self-test suites pass.

C

epistemic_calculus.h

Core types and fusion interface | from EpistemicCalculus

A Categorical Formalization of EpistemicUncertainty Frameworks