Dominic Hughes - Selected Papers

Deep inference proof theory equals categorical proof theory minus coherence [pdf - ps - ps.gz - dvi - bibtex]
Unfinished draft, October 6, 2004.

This paper links deep inference proof theory, as studied by Guglielmi et al., to categorical proof theory in the sense of Lambek et al.. It observes how deep inference proof theory is categorical proof theory, minus the coherence diagrams/laws. Coherence yields a ready-made and well studied notion of equality on deep inference proofs. The paper notes a precise correspondence between the symmetric deep inference system for multiplicative linear logic (the linear fragment of SKSg) and the presentation of *-autonomous categories as symmetric linearly distributive categories with negation. Contraction and weakening in SKSg corresponds precisely to the presence of (co)monoids.