New paper: Classical categories and deep inference

Dear all,

The draft of my paper concerning categorical models and deep inference 
(submitted to LICS '05) is
now available at
     http:\\www.cs.bath.ac.uk/~csprim/lics2.pdf .

Please let me know what you think, and if there is anything which is 
unclear.

Thanks,

Richard McKinley
University of Bath


Title: Classical Categories and deep inference

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¨uhrmann
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.