A 2-Categorical Approach to Proof-Comparison

UoM administered thesis: Phd

  • Authors:
  • Roman Krenický


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.


Original languageEnglish
Awarding Institution
    Award date31 Dec 2014