Non-commutative logic. I: The multiplicative fragment (Q1964014)

The paper introduces a noncommutative \textit{extension} of the multiplicative fragment of linear logic (LL), called ``noncommutative logic'' (NL). When noncommutative LL was already studied, it was usually done in strictly noncommutative systems (which did not contain commutative LL). This is the first time that such a simple and elegant way to extend (multiplicative) LL by means of noncommutative connectives is proposed. The solution given by the authors relies on two main technical novelties: 1) the introduction of a new switching position for links in proof-structures (yielding non-cyclic trips in proof-structures) and the corresponding extension to NL of Girard's long trip correctness criterion; 2) the discovery of the notion of order variety, a ternary relation which is a particular case of cyclic order. A sequent of NL is a set of occurrences of formulas together with an order variety on this set, and with every rule of NL sequent calculus the sequent conclusion of the rule is (inductively) associated. One can also associate with every proof-net of NL an order variety, and everything works fine: with the sequent calculus proof \(\pi\) with conclusion the sequent \(\Gamma,\langle\alpha\rangle\), a proof-net \(R\) is associated, and the order variety associated with \(R\) is precisely \(\alpha\) (adequacy theorem). The converse (the sequentialization theorem) holds only in the cut-free case. There is no surprise in the cut-elimination procedure: it preserves correctness (but not the order variety). Of course, since sequentialization fails in the presence of cuts, a sequentializable proof-net might become non-sequentializable after some cut-elimination steps. However, due to the confluence and strong normalization properties of the procedure, we are sure to eventually obtain a unique sequentializable cut-free proof-net. A nice thing is that commutative (resp. cyclic) proof-nets of multiplicative LL are proof-nets of NL whose order variety is empty (resp. total), and a similar remark holds for commutative (resp. cyclic) sequents.