Categorical proof theory is an interdisciplinary field employing the categorical machinery to provide an abstract conceptual formalization for the notion of a proof. In this short course, we will first use the intuitive understanding of the deductive systems to introduce categories and some categorical constructions. Then, we will focus on the propositional language and provide a categorical interpretation for the propositional proofs, opening up a window to read many mathematical constructions including the computable and continuous functions as the different realizations of the propositional proofs. Then, we will investigate the soundness and completeness of this interpretation with respect to different concrete categories. Finally, we will move to the first-order setting and use the categorical interpretation of the arithmetical proofs to establish some non-trivial consistency results for alternative arithmetical theories. We will also use the interpretation to extract the computational content of the proofs. For instance, we will provide a characterization for the computable functions whose totality are provable in Peano arithmetic. Despite what it may sound, we will not assume any familiarity with the categorical or proof-theoretical concepts other than the very basic logical notions. Any other required notion will be explained throughout the lectures themselves.

The course is composed of 18 parts. See below the schedule: