A System of Interaction and Structure IV: The Exponentials and Decomposition

Abstract

We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.

References in corpus (6)

• A System of Interaction and Structure II: The Need for Deep Inference
• Normalisation Control in Deep Inference via Atomic Flows
• Cirquent calculus deepened
• From Proof Nets to the Free *-Autonomous Category
• The three dimensions of proofs
• On the Proof Complexity of Deep Inference

Cited by in corpus (7)

• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• Extending a system in the calculus of structures with a self-dual quantifier
• On noncommutative extensions of linear logic
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• Linear lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference
• Flag: a Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces
• A Semantic Proof of Generalised Cut Elimination for Deep Inference