Symmetric Normalisation for Intuitionistic Logic

ABSTRACT. We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first system is a direct adaptation of the sequent calculus to the deep inference setting, and we provide a procedure for cut elimination, similar to the one from the sequent calculus, using on non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with DeMorgan duality: each inference rule has a dual rule, cut being dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries.