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

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.

Cited by in corpus (15)

• Normalisation Control in Deep Inference via Atomic Flows
• On the Proof Complexity of Deep Inference
• A System of Interaction and Structure IV: The Exponentials and Decomposition
• Extending a system in the calculus of structures with a self-dual quantifier
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• On noncommutative extensions of linear logic
• Interaction and Depth against Nondeterminism in Proof Search
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• An Analytic Propositional Proof System on Graphs
• Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
• Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference
• Complexity of correctness for pomset logic proof nets
• A Subatomic Proof System for Decision Trees
• Subatomic systems need not be subatomic
• A Semantic Proof of Generalised Cut Elimination for Deep Inference