Exactness and Completeness in Enriched Category Theory

# Exactness and Completeness in Enriched Category Theory Amsterdam, Dec 13, 2025 *As an example of mathematics engineering, we will show how to refactor Birkhoff's completeness proof for equational logic along two dimensions. The first dimension consists of 'boilerplate' organizing notions such as terms, congruences, and substitutions. The second dimension parameterizes the construction by a notion of exactness in the category-theoretic sense (Barr exactness in the classical case). We will show how parameterization by a notion of exactness can lead to new Birkhoff style completeness theorems. This is joint work with Yiwen Ding.* --- ## Introduction Before starting the technical part, I want to explain why I talk about "**mathematics engineering**". First, let me say that at Chapman we have a doctoral program in [Mathematics, Philosophy, Physics](https://www.chapman.edu/scst/graduate/dsci-mpp.aspx) (**MPP**). (If you know potential applicants, ask them to get in touch.) One of the topics, we are investigating in MPP is the question whether, or in what sense, mathematics and computer science are converging. For example, the article by Commelin and Topaz "[Abstraction boundaries and spec driven development in pure mathematics](https://arxiv.org/pdf/2309.14870.pdf)" reporting about the Liquid Tensor Experiment initiated by Peter Scholze shows how modern collaborative mathematics makes use of SWE concepts such as interfaces, test suites, spec driven development, mathematical debt, refactoring, dependency graphs, version control systems and suggests that "metaprogramming, artificial intelligence, and type theory itself, will help resolve some of the remaining issues in the near future." ## Refactoring a Proof We refactor the proof of Birkhoff's completeness theorem for equational logic in the following way. 1. Def: $\text{Term}_\Sigma(X)$ 2. Def: $A\models \theta$, $A\models \Theta$ 3. Def: $A/\Theta$ defined as a colimit 4. Def: $A$ is *injective* wrt $B\to C$ 5. Prop: $A\models \Theta$ iff $A$ is injective wrt $\text{Term}_\Sigma(V) \to \text{Term}_\Sigma(V)/\Theta$ 6. Prop: $\Theta\models\theta$ iff $\theta$ is in the kernel of $\text{Term}_\Sigma(V) \to \text{Term}_\Sigma(V)/\Theta$ 7. Rem: kernel is a limit 8. Def: Semantic closure given by "kernel after quotient" 9. Def: Syntactic closure given by a proof system 10. Prop: Semantic closure = Syntactic closure 11. Cor: Completeness One can now get various completeness results (equational logic, inequational logic, quantale-enriched logic) by redefining the notions highlighted in red.