A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Abstract

Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same. In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in pomset logic is ${\Sigma }_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.

References in corpus (10)

• A System of Interaction and Structure
• A System of Interaction and Structure II: The Need for 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
• An Analytic Propositional Proof System on Graphs
• Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
• Pomset logic: the other approach to non commutativity in logic
• Coherent Interaction Graphs
• Graphical Proof Theory I: Sequent Systems on Undirected Graphs

Cited by in corpus (1)

• A Semantic Proof of Generalised Cut Elimination for Deep Inference