The Semantics of Classical Proofs
Final Report to EPSRC.
People
Implemented Tools
Here is an small classical proofs applet, written by Jules Bean, that allows you to construct classical sequent calculus proofs interactively, that constructs the corresponding Robinson-style proof net, and executes your chosen cut-reductions according to the inequalities of Führmann-Pym order-enriched categorical models. Enjoy!
Some Papers
Abstract Deep inference is a proof-theoretic notion in which proof rules apply arbitrarily deeply inside a formula. We show that the essense of deep inference is the bifunctorality of the connectives. We demonstrate that, when given an inequational theory that models cut-reduction, a deep inference calculus for classical logic (SKSg) is a categorical model of the classical sequent calculus LK in the sense of Führmann and Pym. We uncover a mismatch between this notion of cut-reduction and the usual notion of cut in SKSg. Viewing SKSg as a model of the sequent calculus uncovers new insights into the Craig interpolation lemma and intuitionistic provablility.
Abstract It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show how these models illuminate cut-reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.
Last updated 18 January, 2005: added Section 3.3.1, on the duality of the monoids and comonoids. Submitted to a journal.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarized briefly herein, we have provided a class of models called classical categories which is sound and complete and avoids this collapse by interpreting cut-reduction by a poset-enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product.
In this article, which is self-contained, we present an improved axiomatization of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models called Dummett categories. Examples include, besides the classical categories above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic, by applying it to obtain a classical category from a Dummett category.
Along the way, we gain detailed insights into the changes that proofs undergo during cut-elimination in the presence of weakening and contraction.
Abstract. It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show hoe these models illuminate cut-reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.
Abstract It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. Starting from a convenient formulation of the well-known categorical semantics of linear classical sequent proofs, we give models of weakening and contraction that do not collapse. Cut-reduction is interpreted by a partial order between morphisms. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination. We show soundness and completeness via initial models built from proof nets, and describe models built from sets and relations.
Last updated 7 March, 2005.
Abstract.This paper introduces a notion of proof net for classical logic, provides a static correctness condition for these nets, and analyses the connection between nets and conventional sequent calculus. The main surprise of the paper is that there are no surprises at the static level. Subsequent work reveals that there are few at the dynamic either.
Abstract. We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give a more refined, but necessarily complex, analysis of how connectives may be characterised abstractly. Finally we explain the consequences of insisting on more familiar categorical behaviour.