A System of Interaction and Structure

TL;DR

This paper presents the BV logical system, extending linear logic with a non-commutative operator, achieved through the calculus of structures that enables deep inference and modular cut elimination.

Contribution

It introduces the calculus of structures as a new formalism to develop BV, a logic extending multiplicative linear logic with non-commutative operators.

Findings

The calculus of structures allows deep inference within logical structures.

BV is successfully formalized with modular cut elimination proof.

The approach overcomes challenges of non-commutative logic in sequent calculus.

Abstract

This paper introduces a logical system, called BV, which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far it is not achieved therein. It becomes very natural in a new formalism, called the calculus of structures, which is the main contribution of this work. Structures are formulae submitted to certain equational laws typical of sequents. The calculus of structures is obtained by generalising the sequent calculus in such a way that a new top-down symmetry of derivations is observed, and it employs inference rules that rewrite inside structures at any depth. These properties, in addition to allow the design of BV, yield a modular proof of cut elimination.