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

TL;DR

The paper proves that ${\mathsf{BV}}$ and pomset logic are not the same: every ${\mathsf{BV}}$ theorem is a pomset-logic theorem, but not vice versa, with a concrete counterexample. It analyzes provability complexity, showing ${\mathsf{BV}}$-provability is ${\mathbf{NP}}$-complete while pomset-logic provability is ${\mathbf{\Sigma_2^p}}$-complete, and explains why a Cook–Reckhow-style deductive system cannot exist for pomset logic. The work also connects sequent-calculus approaches (Retoré’s and Slavnov’s proposals) to the complexity results and demonstrates that Retoré’s cut-sequent calculus for pomset logic is sound and complete for ${\mathsf{BV}}$. In addition to the main containment result, the paper provides a comprehensive preliminaries framework (graphs, relations, and proof nets) that clarifies the structure and complexity of each logic, guiding future exploration of sequent systems for both logics.

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 $Σ_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.

Figures (3)

• Figure 1: The equations defining $\equiv$.
• Figure 2: Inductive definition of RBt̅rees (which are not quite trees in the sense of graph theory, though they resemble the syntax trees of formulas). The root vertex is at the bottom.
• Figure 3: Two treel̅ike RBp̅renets for the formula $\mathopen {\hbox{$\langle$}} a \mathbin{\triangleleft} a\mathclose{\hbox{$\rangle$}} \mathbin{\bindnasrepma} \mathopen {\hbox{$\langle$}} a^\bot \mathbin{\triangleleft} a^\bot\mathclose{\hbox{$\rangle$}}$. The left one is a correct proof net, while the right one contains an æc̅ycle involving the 4 topmost matching edges.

Theorems & Definitions (63)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Remark 2.7
• Definition 2.8
• Proposition 2.9
• Proposition 2.10