Deep Inference and the Calculus of Structures

The calculus of structures is a new proof theoretical formalism, introduced by myself in 1999 and initially developed by members of my group in Dresden since 2000. It exploits a new symmetry made possible by deep inference. We can present deductive systems in the calculus of structures and analyse their properties, as we do in the sequent calculus, natural deduction and proof nets. Typical properties of interest are normalisation and cut elimination. There are now many researchers around the world developing deep inference and investigating its consequences on proof theory. This document gives an overview of this research effort. The main purpose of our new formalism is to allow a richer combinatorial analysis of proofs than the other formalisms do. We adopted two main ideas: inferences are symmetric between premises and conclusions, and they are deeply applicable inside expressions, what we call deep inference. As a consequence, it is convenient to deduce over structures, which are expressions intermediate between formulae and sequents. The calculus of structures generalises straightforwardly the sequent calculus, but it allows more freedom in the design of deductive systems. We can in fact design systems where all rules are atomic, or local, including contraction, promotion, all the additive rules and, most importantly, the