03/06/2004
Alessio Guglielmi (TU Dresden)
Deep inference and self-dual non-commutativity

Self-dual non-commutative logical operators are potentially useful for many applications, but they got a bad reputation among proof theorists. This is in part due to the difficulty of dealing with them with simple means. I will show how deep inference deals graciously with self-dual non-commutativity, in an extension of multiplicative linear logic called BV. A new technique called `splitting' is used for proving cut elimination in BV. I will also show a stunningly beautiful counterexample, due to Alwen Tiu, which establishes the need for deep inference: it is impossible to deal with BV in the sequent calculus or any other formalism based on shallow inference.