Categorical models of first-order classical proofs
Richard McKinley · 2006
This thesis introduces the notion of a classical doctrine: a semantics for proofs in firstorder classical logic derived from the classical categories of Fuhrmann and Pym, using Lawvere's notion of hyperdoctrine. We introduce a hierarchy of classes of model, increasing in the strength of cut-reduction theory they model; the weakest captures cut reduction, and the strongest gives De Morgan duality between quantifiers as an isomorphism. Whereas classical categories admit the elimination of logical cuts as equalities, (and cuts against structural rules as inequalities), classical doctrines admit certain logical cuts as inequalities only. This is a result of the additive character of the quantifier introduction rules, as is illustrated by a concrete model based on families of sets and relations, using an abstract Geometry of Interaction construction. We establish that each class of models is sound and complete with respect to the relevant cut-reduction theory on proof nets based on those of Robinson for propositional classical logic. We show also that classical categories and classical doctrines are not only a class of models for the sequent calculus, but also for deep inference calculi due to Brunnler for classical logic. Of particular interest are the local systems for classical logic, which we show are modelled by categorical models with an additional axiom forcing monoidality of certain functors; these categorical models correspond to multiplicative presentations of the sequent calculus with additional additive features. Acknowledgements There are many without whom this work would languish unfinished. I must begin by thanking David Pym for introducing to me the core ideas in this work, and for the guidance he has provided. In matters both sacred and profane, both integra...