A System of Interaction and Structure II: The Need for Deep Inference

TL;DR

This paper explores the logic BV, an extension of MLL with a non-commutative operator, demonstrating that deep inference is essential for its expressiveness and cannot be restricted without losing capabilities.

Contribution

It shows that deep inference is crucial for the logic BV, enabling expressiveness not achievable with traditional sequent calculus approaches.

Findings

Deep inference is necessary for the full expressiveness of BV.

Restrictions on inference depth reduce the logic's expressiveness.

BV extends MLL with a self-dual non-commutative operator in a simple formalism.

Abstract

This paper studies properties of the logic BV, which is an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. BV is presented in the calculus of structures, a proof theoretic formalism that supports deep inference, in which inference rules can be applied anywhere inside logical expressions. The use of deep inference results in a simple logical system for MLL extended with the self-dual non-commutative operator, which has been to date not known to be expressible in sequent calculus. In this paper, deep inference is shown to be crucial for the logic BV, that is, any restriction on the ``depth'' of the inference rules of BV would result in a strictly less expressive logical system.