An Introduction to Categorical Proof Theory
Amirhossein Akbar Tabatabai
TL;DR
The work surveys categorical proof theory as a foundation for understanding proofs as mathematical objects rather than mere provability, linking Hilbert's program, Gentzen's consistency methods, and the development of category-theoretic semantics. It develops the BHK interpretation in a categorical setting, using variable sets, time, and natural transformations to model propositions and proofs, and extends this into higher-order and realizability frameworks. The text analyzes existence, equivalence, and identity problems under various BC/ABC/CCC structures, establishing freeness results (e.g., NJ,NM,Nc) and exploring classical categories, $\ast$-autonomous categories, and pumping in cloning/deleting via comonoids. Realizability and arithmetical theories are treated through recursive/continuous worlds, projective $\mathcal{C}$-sets, and NNOs, illustrating how constructive content and computational witnesses can be extracted or constrained in semantic models. Collectively, the chapter provides a cohesive, category-theoretic bridge between proof theory, type theory, and realizability, with implications for logic, computation, and the semantics of higher-order reasoning.
Abstract
These expanded lecture notes are based on a tutorial on categorical proof theory presented at the summer school associated with the conference "Topology, Algebra, and Categories in Logic 2021-2022." The chapter delves into various applications of categorical methods in proof theory. It is designed to be accessible, with no prior familiarity with category theory required. The necessary categorical background is introduced gradually, with a focus on the philosophical and informal aspects of proof. The only prerequisites are a basic understanding of logic, computability theory, topology, and ordered structures.