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.

翻译：Pomset 逻辑与 BV 都是通过引入第三种自对偶且非交换的连接词，来扩展乘法线性逻辑（包含 Mix）的逻辑系统。其中，Pomset 逻辑源于相干空间与证明网的研究，而 BV 则源于串并联序、余图与证明系统的研究。这两种逻辑均具备切割可容许性，但都无法在相继式演算中实现这一性质。Pomset 逻辑的可证明性可通过证明网正确性判据进行检验，而 BV 则通过深度推理证明系统完成检验。长期以来存在一种猜想：这两种逻辑本质相同。本文证明该猜想是错误的。此外，我们研究了这两种逻辑的复杂度，发现二者存在巨大差距：BV 的可证明性问题是 NP 完全的，而 Pomset 逻辑的可证明性问题则是 Σ₂ᵖ 完全的。我们还针对这两种逻辑可能的相继式系统做出了一些观测。