Epistemic Calculi
A Categorical Formalization of Epistemic Uncertainty Frameworks
Formal Verification Certificate
All 90+ theorems machine-checked by the Lean 4 kernel with zero sorry gaps. Includes corrections to the original paper.
Epistemic Calculi • Lean 4 + Mathlib • Apoth3osis Labs
Overview
Aambø's framework unifies probability theory, possibility theory, certainty factors, and Dempster–Shafer theory under a single categorical spine: a non-trivial unital symmetric monoidal posetal category. Eight axiom classes (E1–E8) systematically generate the landscape of existing and novel uncertainty calculi.
Our formalization in 26 Lean 4 modules with 90+ sorry-free theorems discovered and corrected three issues in the original paper:
- Theorem 3.6 gap: composition coherence for odds-form Bayesian updating required an additional naturality condition not stated in the paper.
- CF residuation: fragile instance resolution in the closed certainty-factor calculus needed explicit universe annotations to avoid Lean 4 diamond inheritance.
- Bridge coverage: categorical bridge tests between probability and possibility instances were missing from the original framework.
Key Results
Epistemic Calculus Typeclass
Core categorical structure capturing the common spine of all uncertainty frameworks as a non-trivial unital symmetric monoidal posetal category.
8 Axiom Classes (E1–E8)
Optimistic, Complete, ConservativeFusion, Closed, StronglyConservative, Idempotent, Fallible, and Cancellative — each proved to generate specific calculi.
V-Enriched Bayesian Updating
Bayesian conditioning formalized as a V-enriched functor with corrected composition coherence for odds-form updating.
Landscape Instances
Probability, possibility, certainty factors, and Dempster-Shafer all instantiated as specific axiom-class combinations.