A 2-Categorical Approach to Proof-Comparison

Abstract

This work is located in the area of mathematical logic and, more specifically, (categorical) proof theory, using methods from (higher order) category theory and algebra. Advances concerning the question when two (classical) proofs of the same formula are essentially the same are still quite modest. There is hence no generally agreed-upon answer to the question: "What is a proof?" This thesis aims to provide a framework for studying proofs of classical (propositional) logic. This is a problematic task, since models of classical logic easily "collapse" by equating any two proofs of the same statement. Furthermore, existing models (in particular categorical ones) are often too "coarse-grained" insofar as they impose various equalities on proofs which are, at the least, debatable. In this thesis, a model based on weak 2-categories (with additional structure) is defined. In that model proofs can be related in various degrees and particularly by something weaker than equality. Moreover, transformations between proofs can be expressed in the model. In the process of modelling, a concrete model is studied. This is given by a particular symmetric monoidal bicategory formed by fields, double vector spaces and linear maps. For that the theory of double vector spaces is evolved, including tensor products for them. It is shown that the 2-categorical model allows us to add various desired relations between classical proofs without collapse. The model is "flexible" in the sense of allowing different definitions of the notion of "proof". In particular, it can capture the process of linearisation (of proofs) and hence the transition from one definition of "proof" to another.

Date of Award	31 Dec 2014
Original language	English
Awarding Institution	The University of Manchester