On noncommutative extensions of linear logic

TL;DR

This paper introduces semicommutative linear logic with noncommutative connectives, develops proof-net syntax, and provides a decorated sequent calculus that is sound, complete, and degenerates to Pomset logic, addressing the lack of sequent calculus formulations.

Contribution

It defines a new semicommutative linear logic with noncommutative connectives and presents a decorated sequent calculus that is cut-free, sound, and complete, including for Pomset logic.

Findings

Developed a syntax of proof-nets for semicommutative logic

Proved the decorated sequent calculus is cut-free, sound, and complete

Demonstrated degeneration to Pomset logic in specific cases

Abstract

Pomset logic introduced by Retor\'e is an extension of linear logic with a self-dual noncommutative connective. The logic is defined by means of proof-nets, rather than a sequent calculus. Later a deep inference system BV was developed with an eye to capturing Pomset logic, but equivalence of system has not been proven up to now. As for a sequent calculus formulation, it has not been known for either of these logics, and there are convincing arguments that such a sequent calculus in the usual sense simply does not exist for them. In an on-going work on semantics we discovered a system similar to Pomset logic, where a noncommutative connective is no longer self-dual. Pomset logic appears as a degeneration, when the class of models is restricted. Motivated by these semantic considerations, we define in the current work a semicommutative multiplicative linear logic}, which is multiplicative linear logic extended with two nonisomorphic noncommutative connectives (not to be confused with very different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets and show how this logic degenerates to Pomset logic. However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. We introduce decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to "degenerate" variations, including Pomset logic. Thus, in particular, we give a variant of sequent calculus formulation for Pomset logic, which is one of the key results of the paper.

Equations

$$A\otimes B⊢A<B⊢A\wp B.$$

$$⟨f,g⟩=\sum f(x)g(x).$$

$$S^{\perp }=\{v\in {\mathbf{R}}_{+}^X|\text{mbox}\forall u\in S\text{mbox}⟨v,u⟩\le 1\}.$$

$$A=(X,A),B=(Y,B)$$

$$A\multimap B=\Big{\{}F\in{\bf R}_{+}^{X\times Y}|\mbox{ }\forall u\in A\sum\limits_{x\in X}F(x,y)(x)u(x)\in B\Big{\}},$$

$$A\wp B=A^{\perp }⊸B,A\otimes B={(A^{\perp }\wp B^{\perp })}^{\perp }.$$

$$G\circ F(x,z)=\sum _{y\in Y}F(x,y)G(y,z).$$

$$A\oslash B=\Big{\{}\sum\limits_{i\in I}u_{i}\otimes v_{i}|\mbox{ }\forall i\in I\mbox{ }u_{i}\in A\mbox{ and }\sum\limits_{i\in I}v_{i}\in B\Big{\}}.$$

$$f\le g\text{mbox}iff\forall x\in Xf(x)\le g(x),$$

$$V={\mathbf{R}}^X$$

$${(A\vec{\otimes }B)}^{\perp }=A^{\perp }\vec{\wp }{B}^{\perp },{(A\vec{\wp }B)}^{\perp }=A^{\perp }\vec{\otimes }{B}^{\perp },$$

$$A\otimes B⊢A\vec{\otimes }B,\text{mbox}A\vec{\wp }B⊢A\wp B,$$

$$A\otimes B⊢A\vec{\otimes }B⊢A\vec{\wp }B⊢A\wp B.$$

$$N^{\perp }=\{X^{\perp }|\text{mbox}X\in N\}.$$

$$p$$

$$A^{\perp }$$

$$⊢\Gamma .$$

$$\Gamma ⊢\Delta$$

$$\Gamma =A_1,\dots ,A_n$$

$${\Gamma }^{\perp }=A_1^{\perp },\dots ,A_n^{\perp }.$$

$$A^{\perp }$$

$$A\otimes (B\vec{\wp }C)⊢(A\otimes B)\vec{\wp }C,\text{mbox}(A\wp B)\vec{\otimes }C⊢A\wp (B\vec{\otimes }C),$$

$$A\vec{\otimes }(B\wp C)⊢(A\vec{\otimes }B)\wp C,\text{mbox}(A\vec{\wp }B)\otimes C⊢A\vec{\wp }(B\otimes C),$$

$$A\vec{\otimes }(B\vec{\wp }C)⊢(A\vec{\otimes }B)\vec{\wp }C,\text{mbox}(A\vec{\wp }B)\vec{\otimes }C⊢A\vec{\wp }(B\vec{\otimes }C).$$

$$p^{\perp }$$

Full text

In an on-going work on semantics we discovered a system similar to Pomset logic, where a noncommutative connective is no longer self-dual. Pomset logic appears as a degeneration, when the class of models is restricted.

Motivated by these semantic considerations, we define in the current work a semicommutative multiplicative linear logic, which is multiplicative linear logic extended with two nonisomorphic noncommutative connectives (not to be confused with very different Abrusci-Ruet noncommutative logic). We develop a syntax of proof-nets and show how this logic degenerates to Pomset logic.

However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. We introduce decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to “degenerate” variations, including Pomset logic. Thus, in particular, we give a variant of sequent calculus formulation for Pomset logic, which is one of the key results of the paper.

1. Introduction

There is a number of noncommutative variations and extensions of linear logic known in literature, starting from Lambek calculus [Lam58], which historically precedes linear logic itself. Probably the best known and best behaved is cyclic linear logic of Yetter [Yet90]. Let us mention also noncommutative logic of Abrusci and Ruet [Abr91, AR99], which mixes cyclic logic and the ordinary, commutative linear logic. Another approach to combining commutative and noncommutative features is based on introducing exchange modalities in Lambek calculus [JEIdP19, dPE18].

The topic of the current paper, however, is somewhat far from the above systems. Rather, it is related to linear logic noncommutative extensions stemming from the seminal work [Ret97] of Retoré. Retoré found an extension of linear logic (technically speaking, of linear logic with the Mix rule) with a self-dual binary associative noncommutative connective seq or before, denoted as $<$, “intermediate” between times and par, so that in the corresponding logic it holds that

[TABLE]

(It seems though that there is no firm consensus on a standard notation for this connective; different works [Ret97, BPS12, GS11] use different symbols.)

The system found by Retoré, Pomset logic was based on semantics (it has a denotational model in the category of coherent spaces) and is defined by means of proof-nets. However a traditional Gentzen-style sequent calculus formulation was missing. Later, a deep inference system BV was designed [Gug07] to capture Pomset logic. Unfortunately, equivalence of systems was not proven and this still remains an open problem, although it is known that BV is contained in Pomset logic [Str03]. (In fact, rules of BV directly translate into a system of graph rewrite rules which transform proof-nets to proof-nets. This rewriting system itself was proposed in [Ret99].)

As for a sequent calculus formulation, in [Tiu06], it was proved that, in fact, no sequent calculus in the usual sense can capture these logics.

The system BV was subsequently extended [GS11] to accommodate linear logic exponentials, an extension with additive connectives was considered as well [Hor15]. Basically, BV together with other deep inference systems gave rise to a rather active research field111Consult http://alessio.guglielmi.name/res/cos/ for the current state..

1.1. Interpretation in probabilistic coherence spaces

Pomset logic was introduced in [Ret97] together with a denotational model in the category of coherent spaces, which satisfies quite strong completeness properties [Ret94a]. Since the system BV is contained in Pomset logic, it follows that BV can be modeled in coherent spaces as well. In [BPS12] an attempt was made to give a general category-theoretic axiomatization of BV, and an abstract notions of a BV category was introduced (although no kind of soundness result was proven).

In particular, a concrete example of a BV category was constructed in the setting of probabilistic coherence spaces (PCS).

PCS were first introduced in [Gir04] as a model for the multiplicative-additive linear logic, and later much studied in [DE11], where the model was extended to encompass exponentials. PCS can be seen as a “weighted” version of ordinary coherent spaces, where relations are replaced with nonnegative real-valued functions, and intersection is replaced with pairing of functions

[TABLE]

Thus, a probabilistic coherence space $A$ is a pair $A=(X,A)$, where $X$, the carrier, is a set, and $A\subseteq{\bf R}_{+}^{X}$ is a set of functions from $X$ to ${\bf R}_{+}$ coinciding with its bipolar $A^{\bot\bot}$, where the polar $S^{\bot}$ of any set $S\in{\bf R}_{+}^{X}$ is defined as

[TABLE]

(In the setting of [BPS12], the set $X$ was assumed to be finite.)

Then linear negation is interpreted in PCS by means of (2). Further, if

[TABLE]

are PCS, then the spaces $A\multimap B$, $A\otimes B$, $A\mathop{\wp}B$, all with the same carrier $X\times Y$, are defined by

[TABLE]

[TABLE]

Elements of the set $A\multimap B\subseteq{\bf R}_{+}^{X\times Y}$ become morphisms from $A$ to $B$, which are composed by means of the formula

[TABLE]

It turns out that there is also an associative noncommutative self-dual seq operation (denoted in [BPS12] as $\oslash$) on PCS, at least in the finite-dimensional case.

If $A=(X,A)$, $B=(Y,B)$ are PCS then the PCS $A\oslash B$ with the carrier $X\times Y$ is defined by

[TABLE]

(In the above formula, $I$ is an arbitrary finite index set, and we use the identification ${\bf R}^{X\times Y}\cong{\bf R}^{X}\otimes{\bf R}^{Y}$.)

It was shown that the seq operation satisfies basic properties of the seq connective in BV and makes the category of PCS a BV category.

1.2. PCS and partially ordered vector spaces

On the other hand, as it was articulated, for example, in [DE11], probabilistic coherence spaces can be seen as a special case of partially ordered vector spaces (POVS).

Indeed, for any set $X$, the set of functions ${\bf R}^{X}$ is partially ordered by

[TABLE]

and the subset ${\bf R}^{X}_{+}$ is the set of nonnegative elements, the nonnegative cone.

Then, a PCS $A=(X,A)$ can be described as a partially ordered vector space $V$ of a specific form

[TABLE]

together with a subset $A$ of its nonnegative cone.

Remarkably, it can be shown that in the finite-dimensional case the interpretation of multiplicative linear logic extends from PCS to general POVS more or less verbatim.

In an on-going work the author of this paper discovered that the above seq operation defined by (3) can also be extended to general finite-dimensional POVS. This will be shown in a forthcoming paper. However, this operation is no longer self-dual, and thus gives rise to two non-isomorphic (noncommutative associative) dual operations, which it seems reasonable to denote as $\mathop{\vec{\otimes}}$ and $\mathop{\vec{\wp}}$.

The two connectives degenerate into one, when condition (4) is imposed on every object $V$.

1.3. Semicommutative logic

The above discussion of semantics motivates out interest in constructing a logic with two dual noncommutative connectives, such that Pomset logic can be seen as its degenerate variant.

We call the system we propose semicommutative multiplicative linear logic. The principle (1) changes to

[TABLE]

[TABLE]

or, in presence of the Mix rule, to

[TABLE]

In this paper we define semicommutative logic by means of proof-nets and show how it “degenerates” into Pomset logic by first adding the Mix rule and then declaring the two noncommutative connectives isomorphic.

1.4. Decorated sequents

However, a more interesting problem than just finding yet another noncommutative logic is to find a sequent calculus for this logic. This is nontrivial; for example, it is proven that system BV does not admit sequent calculus formulation [Tiu06] at all. This result apparently applies as well to Pomset logic, which conjecturally is the same as BV (this is discussed in [PRS]). And semicommutative logic of this paper is closely related to these systems.

Thus it seems unreasonable to look for a formulation of semicommutative logic as a sequent calculus in the ordinary sense.

We consider decorated sequents, which are sequents equipped with an extra structure of a binary relation of reachability on formulas. We define a decorated sequent calculus for semicommutative logic and prove that it is cut-free, sound and complete. This is adapted to “degenerate” variations, including Pomset logic. Thus, in particular, we give a (sort of) sequent calculus formulation for Pomset logic, and this is one of the key results of the paper. (We say “sort of” sequent calculus, because decorated sequents are not sequents in the usual sense of the word.)

To conclude the introduction, we should remark on an important difference between semicommutative logic of this paper and some other noncommutative extensions of linear logic. Concretely, we want to avoid confusion with the above-mentioned system of Abrusci-Ruet [Abr91, AR99].

Formally, both systems have two pairs of multiplicative connectives, one commutative and one noncommutative. This may create a suspicion of some relation, which would be strange because Abrusci-Ruet noncommutative logic is a very complex and nontrivial construction compared with the semicommutative logic of this paper. However, a formal resemblance between the two systems is deceptive. In noncommutative logic the noncommutative pair of connectives is almost as “powerful” as the commutative one; both commutative and noncommutative par do define (different) linear implications. (On the sematic side: each pair corresponds to a separate $*$-autonomous structure on the modeling category, see [BLR02]). In semicommutative logic we have nothing of this kind. The noncommutative pair is just an extra bimonoidal structure with no particular power.

2. Semicommutative linear logic

We assume that the reader is familiar with multiplicative linear logic (MLL) (see [Gir95] for an introduction), including the variation with the Mix rule (MLL+Mix) [FR94], as well as with proof-nets and the Danos-Regnier criterion [DR89], both for MLL and MLL+Mix [FR94].

In this section we introduce semicommutative linear logic, a simple extension of MLL with two noncommutative connectives.

2.1. Language

The language of semicommutative linear logic (ScMLL) is that of MLL supplied with two new binary connectives $\mathop{\vec{\otimes}}$, $\mathop{\vec{\wp}}$.

More accurately, we assume that we are given a set $N$ of positive literals. We define then the set $N^{\bot}$ of negative literals as

[TABLE]

Elements of $N\cup N^{\bot}$ are called literals.

Formulas of ScMLL are defined by the following induction.

• •

Any $X\in N\cup N^{\bot}$ is a formula;

• •

if $X$, $Y$ are formulas, then $X\mathop{\wp}Y$, $X\otimes Y$, $X\mathop{\vec{\wp}}Y$ and $X\mathop{\vec{\otimes}}Y$ are formulas;

2.2. Proof-nets

We define semicommutative linear logic by means of proof-nets. As usual, we define proof-nets in two steps. First we define proof-structures.

Recall that a mixed graph $G$ is a triple $G=(V,E,A)$, where $V$ is a set of vertices, $E$, the set of undirected edges, is a set of two element subsets of $V$, and $A\subseteq V\times V$, the set of directed edges, is a set of ordered pairs of distinct elements of $V$. In plainer, but less accurate language, a mixed graph is a graph that may contain both directed and undirected edges.

A proof-structure $\rho$ is a mixed graph, whose vertices are labeled by ScMLL formulas, and some of whose vertices are selected as conclusions, built inductively by the following rules.

A graph with two vertices labeled by dual propositional symbols $p$ and $p^{\bot}$ connected by one undirected edge is a proof-structure with conclusions $p$, $p^{\bot}$.

[TABLE]

Such a proof-structure is called an axiom link.

A disjoint union of two proof-structures $\rho_{1}$ and $\rho_{2}$ is a proof-structure whose conclusions are those of $\rho_{1}$ or $\rho_{2}$.

If $\rho$ is a proof-structure whose set of conclusions contains two (vertices labeled by) formulas $A$ and $B$, then the labeled graph $\rho^{\prime}$ obtained from $\rho$ by attaching to $A$ and $B$ one of the following labeled graphs,

{mathpar} A$$B$$\otimes

A$$B$$\mathop{\wp}

A$$B$$\mathop{\vec{\otimes}}

A$$B$$\mathop{\vec{\wp}}

called, respectively, an $\otimes$-link, a $\mathop{\wp}$-link, a $\mathop{\vec{\otimes}}$-link, a $\mathop{\vec{\wp}}$-link, is a proof-structure. The new proof-structure $\rho^{\prime}$ has the same conclusions as $\rho$ except for $A$ and $B$, and one new conclusion, respectively $A\otimes B$, $A\mathop{\wp}B$, $A\mathop{\vec{\otimes}}B$, $A\mathop{\vec{\wp}}B$, depending on the link attached.

If $\rho$ is a proof-structure whose conclusions contain two (vertices labeled by) dual formulas $A$ and $A^{\bot}$, then the labeled graph $\rho^{\prime}$ obtained from $\rho$ by attaching to $A$ and $A^{\bot}$ the following graph, called a Cut-link,

[TABLE]

is a proof-structure. The new proof-structure $\rho^{\prime}$ has the same conclusions as $\rho$ except for $A$ and $A^{\bot}$.

Each $\otimes$-, $\mathop{\wp}$-, $\mathop{\vec{\otimes}}$- or $\mathop{\vec{\wp}}$-link has three vertices, one of which is called the conclusion of the link, and the two other, premises. For example for $A\otimes B$, the vertices labeled by $A$ and $B$ are premises, and the remaining one, the conclusion, similarly for other types. Also, observe that, in $\otimes$- and $\mathop{\wp}$-links, the edges forming the link are undirected.

A proof-structure without cut-links is called cut-free.

We use the following terminology below. A generalized $\mathop{\wp}$-link is a $\mathop{\wp}$-link or a $\mathop{\vec{\wp}}$-link, a generalized $\otimes$-link is a $\otimes$-link or a $\mathop{\vec{\otimes}}$-link, an ordered link is a $\mathop{\vec{\wp}}$-link or a $\mathop{\vec{\otimes}}$-link.

In order to define proof-nets we introduce more terminology. Recall that an elementary path in a graph is a path traversing each of its vertices exactly once. An elementary cycle is a cycle traversing exactly once each of its vertices except the starting and the ending one.

Now let $\rho$ be a proof-structure, and $\phi$ be an elementary path, respectively, elementary cycle, in $\rho$. A critical link on $\phi$ is an ordered link such that $\phi$ goes through its conclusion and both premises.

The path, respectively, cycle, $\phi$ is essentially directed, if it goes through all its critical links in the direction of arrows. (For example for a $\mathop{\vec{\wp}}$-link $A\mathop{\vec{\wp}}B$, the path $\phi$ should go as $A$—$A\mathop{\vec{\wp}}B$—$B$).

We now proceed to defining proof-nets. We use switchings in the style of Danos-Regnier criterion. A switching $\sigma$ of the proof-structure $\rho$ is a choice, for each generalized $\mathop{\wp}$-link, of one of the two edges forming the link. The first round of the switching $\sigma$ of the proof-structure $\rho$ is the undirected graph obtained from $\rho$ by erasing from each generalized $\mathop{\wp}$-link the edge chosen by $\sigma$ and forgetting directions of remaining edges. The second round of $\sigma$ is the directed graph obtained from $\rho$ by erasing, for each $\mathop{\wp}$-link the edge chosen by $\sigma$ (but not touching $\mathop{\vec{\wp}}$-links, and keeping directions of the edges).

{defi}

A proof-net is a proof-structure $\rho$, such that for any switching $\sigma$ the first round is connected and acyclic, and the second round has no essentially directed cycles.

A sequent $\Gamma$ is a multiset of ScMLL formulas.

{defi}

A sequent $\Gamma$ is derivable in ScMLL if there exists a proof-net $\rho$ whose multiset of conclusions is $\Gamma$. We say that $\rho$ is a proof-net of (the sequent) $\Gamma$. A formula $A$ is derivable in ScMLL if there exists a proof-net whose only conclusion is $A$.

When the sequent $\Gamma$ is derivable, we write

[TABLE]

We will also use a two-sided notation

[TABLE]

meaning that the sequent $\Gamma^{\bot},\Delta$ is derivable. Here, if

[TABLE]

then the sequent $\Gamma^{\bot}$ is defined as

[TABLE]

2.2.1. Examples

We give some examples and non-examples of proof-nets.

The following proof-structure is not a proof-net.

[TABLE]

The first round of any of the two possible switchings is indeed acyclic and connected. However, in the second round no edge is erased and we get a directed cycle.

The following is a proof-net.

[TABLE]

There is a cycle in the second round of any switching, but it is not essentially directed.

The following is not a proof-net.

[TABLE]

It passes the first round, however in the second round of any switching we get a cycle (shown dashed below). Observe that the cycle is not directed, but it is essentially directed.

[TABLE]

The following is a proof-net, as can be found by inspection.

[TABLE]

We collect some observations on principles derivable and non-derivable in ScMLL.

Remark 1**.**

The logic ScMLL contains MLL. The connectives $\mathop{\vec{\wp}}$ and $\mathop{\vec{\otimes}}$ in ScMLL are provably associative. ScMLL derives (5) and the following principles

[TABLE]

[TABLE]

[TABLE]

ScMLL does not derive $A\mathop{\vec{\otimes}}B\vdash B\mathop{\vec{\otimes}}A$. ∎

2.2.2. Commutative projections

Observe that the first round part of the above proof-net definition is just the Danos-Regnier criterion [DR89] for ordinary MLL proof-nets. In particular, it follows that, if in the proof-net $\rho$ we forget direction of edges and erase all arrows above connectives, we get a correct proof-net $\rho^{\prime}$ for an ordinary MLL.

Given a proof-net $\rho$ we define the commutative projection $\rho^{\prime}$ of $\rho$ as the proof-structure obtained from $\rho$ by making all edges undirected and replacing all $\mathop{\vec{\otimes}}$ links with $\otimes$ links, and all $\mathop{\vec{\wp}}$ links with $\mathop{\wp}$ links.

It is easy to see that thus obtained $\rho^{\prime}$ is a proof-net.

2.3. Cut-elimination

Lemma 2**.**

There is an algorithm transforming any proof-net with cut-links to a cut-free proof-net with the same conclusions.

Proof 2.1**.**

The algorithm is, of course, that of ordinary MLL as far as unordered links are concerned. Thus if a cut-link is between dual propositional symbols $p$, $p^{\bot}$, then, by the acyclicity condition for switchings in the first round, it necessarily has the form

[TABLE]

and can be replaced by an axiom link.

[TABLE]

If a cut-link is between two compound formulas, it is replaced by two cut-links between their subformulas.

The generic case is when the compound formulas are of the form $A\mathop{\vec{\otimes}}B$, $A^{\bot}\mathop{\vec{\wp}}B^{\bot}$. So assume that we have a proof-net $\rho$ with a cut-link as shown below.

[TABLE]

Let us denote the above subgraph of $\rho$ as $s$. The subgraph $s$ is replaced by a new subgraph $s^{\prime}$ consisting of two cut-links, as shown below.

[TABLE]

This gives us a new proof-structure $\rho^{\prime}$ and we need to check that $\rho^{\prime}$ is a proof-net.

Now, the first-round part of proof-net definition depends only on commutative projections. So $\rho^{\prime}$ satisfies the first-round part if $\rho$ does, because for their commutative projections this is a reduction of ordinary MLL proof-nets, and this takes proof-nets to proof-nets. So we only need to care about the second-round part.

So assume that for some switching $\sigma$ of $\rho^{\prime}$ there is an essentially directed cycle $\phi$ in the second round. Let us denote the common part of $\rho$ and $\rho^{\prime}$ as $\tilde{\rho}$. I.e. $\tilde{\rho}$ is $\rho^{\prime}$ without the cut-links between $A$ an $A^{\bot}$ and between $B$ and $B^{\bot}$. Let $\tilde{\sigma}$ be the switching of $\rho$, obtained by restricting $\sigma$ to $\tilde{\rho}$ and extending this to $\rho$ in an arbitrary way. (The extension consists in choosing one of the two edges in the $\mathop{\vec{\wp}}$-link between $A^{\bot}$ and $B^{\bot}$, and it does not play role in the second round anyway.)

The cycle $\phi$ must pass through $s^{\prime}$, otherwise the cycle is present already in $\rho$ for the switching $\tilde{\sigma}$. Let us consider all possibilities.

The cycle $\phi$ does not meet $A$. Then $\phi$ consists of an essentially directed path $\phi_{0}$ in $\tilde{\rho}$ between $B$ and $B^{\bot}$ and the cut-link. Then $\phi_{0}$ together with the path $B-A\mathop{\vec{\otimes}}B-\mbox{Cut}-A^{\bot}\mathop{\vec{\wp}}B^{\bot}-B^{\bot}$ create an essentially directed cycle for $\tilde{\sigma}$ in $\rho$ in the second round. So $\rho$ is not a proof-net.

The cycle $\phi$ meets $A$ and enters $s^{\prime}$ through $A$ (remember that $\phi$ has direction). Let $X$ be the vertex of $s^{\prime}$ such that $\phi$ passes through $X$ before entering $A$ and does not go through any vertex of $s^{\prime}$ between $X$ and $A$. Then there is an essentially directed path $\phi_{0}$ from $X$ to $A$ in $\tilde{\rho}$. There are three possibilities for $X$: $X$ can be $A^{\bot}$, $B$ or $B^{\bot}$. In all three possible cases the essentially directed $\phi_{0}$ is completed to an essentially directed cycle for $\tilde{\sigma}$ in the second round by attaching an essentially directed path from $A$ to $X$ in $s$. Again, it follows that $\rho$ is not a proof-net.

The cycle meets $A$ and leaves $s^{\prime}$ through $A$. Then $\phi$ enters $s^{\prime}$ through $A^{\bot}$. Similarly to the preceding paragraph, let $X$ be the vertex of $s^{\prime}$ passed by $\phi$ before $A^{\bot}$. Then there is an essentially directed path $\phi_{0}$ from $X$ to $A^{\bot}$ in $\tilde{\rho}$. Again we consider all three possibilities for $X$, and each of them gives rise to an essentially directed cycle for $\tilde{\sigma}$ in the second round. Hence $\rho$ is not a proof-net.

It follows that such $\sigma$ and $\phi$ do not exist and $\rho^{\prime}$ is a proof-net. The case of a cut-link between formulas $A\mathop{\wp}B$ and $A\otimes B$ is treated similarly.

Corollary 3**.**

A sequent is derivable in ScMLL iff it is derivable by means of a cut-free proof-net.

ScMLL is a conservative extension of MLL. ∎

In the next section we give a sequent calculus formulation of ScMLL.

3. Sequent calculus

We want now to formulate ScMLL as a sequent calculus.

There are, however, strong arguments that an adequate formulation of semicommutative logic in the language of ordinary sequents is impossible. Indeed, this impossibility has been shown for the system BV [Tiu06] and apparently applies as well to Pomset logic (see [PRS]), which is believed to be equivalent to BV (inclusion of BV in Pomset logic is proven in [Str03]). And Pomset logic is closely related to ScMLL.

On the other hand, for noncommutative logics it is quite customary to use sequents with an extra structure. For example, cyclic linear logic [Yet90] uses cyclically ordered sequents, and Abrusci-Ruet’s noncommutative logic [AR99] uses sequents with a complicated additional structure of order variety. Retoré in his attempts to formulate a sequent calculus for Pomset logic considered partially ordered sequents [Ret97]. Following this tradition we consider sequents decorated with an extra structure of binary relation.

3.1. Decorated sequents

We will consider decorated sequents, which are sequents equipped with a certain extra structure of reachability relation.

In order to make definitions more concise, we introduce the following terminology. Given a sequent $\Gamma$, a vector in $\Gamma$ is any finite nonempty sequence of distinct elements of $\Gamma$. Vectors will systematically be denoted with boldface letters. For a vector ${\bf X}$ we denote the size of ${\bf X}$ as $|{\bf X}|$. The empty sequence is denoted as ${\bf\Lambda}$.

{defi}

A decorated sequent is a pair $(\Gamma,\rightrightarrows)$, where $\Gamma$ is a sequent, and $\rightrightarrows$ is a binary relation of reachability between vectors in $\Gamma$ satisfying the following properties:

1. (1)

${\bf\Lambda}\rightrightarrows{\bf\Lambda}$; 2. (2)

if ${\bf X}\rightrightarrows{\bf Y}$ then $|{\bf X}|=|{\bf Y}|$; 3. (3)

if $(X_{1},\ldots,X_{n})\rightrightarrows(Y_{1}\ldots,Y_{n})$ then $(X_{\sigma(1)},\ldots,X_{\sigma(n)})\rightrightarrows(Y_{\sigma(1)}\ldots,Y_{\sigma(n)})$ for any permutation $\sigma\in S_{n}$; 4. (4)

if ${\bf X}\rightrightarrows{\bf Y}$ then ${\bf X}$ and ${\bf Y}$ have no common element.

When ${\bf X}\rightrightarrows{\bf Y}$ we say that ${\bf Y}$ is reachable from ${\bf X}$. If ${\bf Y}$ is not reachable from ${\bf X}$ we write

[TABLE]

We define also reachability between formulas by considering formulas as single element vectors. Any decorated sequent whose underlying sequent is $\Gamma$ is called a decoration of $\Gamma$. We systematically abuse notation by denoting both the decoration $(\Gamma,\rightrightarrows)$ and its underlying sequent as $\Gamma$.

Now let $\rho$ be a proof-net and $\Gamma$ be a decorated sequent.

{defi}

We say that $\rho$ is a proof-net of $\Gamma$ when the following holds:

1. (1)

the multiset of conclusions of $\rho$ is the underlying sequent of $\Gamma$, 2. (2)

if

[TABLE]

are vectors in $\Gamma$ with no common element, then it holds that ${\bf X}\rightrightarrows{\bf Y}$ iff for some switching of $\rho$ in the second round there exist pairwise nonintersecting essentially directed paths from $X_{i}$ to $Y_{i}$, $i=1,\ldots,n$.

A decorated sequent $\Gamma$ is derivable in ScMLL if there is a proof-net of $\Gamma$.

It is easy to see that an ordinary sequent is derivable in ScMLL iff some its decoration is derivable in ScMLL.

Remark 4**.**

Let $\Gamma$ be an ordinary sequent and $\rho$ be a proof-net of $\Gamma$. Then there exist unique reachability relation $\rightrightarrows$ on vectors in $\Gamma$ such that $\rho$ is a proof-net of the decorated sequent $(\Gamma,\rightrightarrows)$.

Proof 3.1**.**

The relation $\rightrightarrows$ is defined by condition (ii) of Definition 3.1.

If $\rho$ is a proof-net of an ordinary sequent $\Gamma$ and the reachability relation $\rightrightarrows$ is defined on $\Gamma$ by condition (ii) of Definition 3.1 as in the above proof, then we say that $(\Gamma,\rightrightarrows)$ is the * decoration of $\Gamma$ in $\rho$*.

Remark 5**.**

It can be observed that reachability relations that actually occur in derivable decorated sequents are far from being arbitrary. For example, if $\Gamma$ is an MLL sequent (i.e. $\Gamma$ does not use $\mathop{\vec{\otimes}}$ or $\mathop{\vec{\wp}}$ connectives), and $\rho$ is a proof-net of $\Gamma$, then the decoration of $\Gamma$ in $\rho$ has necessarily total reachability relation. That is, any two vectors in $\Gamma$ of equal size and with no common element are reachable from each other.

It might be interesting to understand which reachability relations actually do occur. Unfortunately, we cannot say anything definite on this subject.

The main usage of reachability is the following.

Remark 6**.**

Assume that $\Gamma$ is a decorated sequent and $\rho$ is a proof-net of $\Gamma$.

Let $X,Y$ be formulas of $\Gamma$. Then $Y$ is not reachable from $X$ iff the proof-structure $\rho^{\prime}$ obtained from $\rho$ by attaching a $\mathop{\vec{\wp}}$-link between $X$ and $Y$ is a proof-net.

Proof 3.2**.**

Let $\sigma$ be a switching of $\rho^{\prime}$. It is immediate that the first round is connected and acyclic, otherwise the original $\rho$ is not a proof-net.

Assume that there is an essentially directed cycle $\phi$ in the second round of $\sigma$. Then $\phi$ passes through the conclusion link $X\mathop{\vec{\wp}}Y$, otherwise $\rho$ is not a proof-net. By removing this link from $\phi$ we obtain an essentially directed path from $Y$ to $X$, hence $X\rightrightarrows Y$. The other direction is similar.

3.1.1. First level of sequent rules

Now we want to write a sequent calculus for decorated sequents. Every rule will have two levels: the first level is how the underlying sequents are changed, the second, how the reachability relations are changed.

We first list the level of sequents. Here, the rules are basically, those of ordinary MLL, sometimes with arrows added above connectives. {mathpar} \inferrule ⊢A,A^⊥   (Axiom) \inferrule⊢Γ,A

⊢A^⊥,Δ⊢Γ,Δ   (Cut) \inferrule⊢Γ,A

⊢B,Δ⊢Γ,A⊗B,Δ   (⊗)

\inferrule⊢Γ,A,B⊢Γ,A℘B   (℘) \inferrule⊢Γ,A ⊢B,Δ⊢Γ,A →⊗B,Δ   (→⊗) \inferrule⊢Γ,A,B (where B／⇉A)⊢Γ,A→℘B   (→℘)

Let us make it clear how we read rules on the first level. For each rule in the above list it is understood that the premises are decorated sequents, whereas the conclusion is an ordinary sequent.

Now we will translate rules in the above list to operations on proof-nets. More specifically, to each rule

[TABLE]

we assign an operation, which, given proof-nets $\rho_{1},\ldots,\rho_{n}$ of the decorated sequents $\Theta_{1},\ldots,\Theta_{n}$, transforms them into a proof-net $\rho$ of the (ordinary) sequent $\Theta$.

Moreover, the decoration of $\Theta$ in $\rho$ depends only on $\Theta_{1},\ldots,\Theta_{n}$ and does not depend on $\rho_{1},\ldots,\rho_{n}$. Then rules for computing this decoration of $\Theta$ from knowledge of $\Theta_{1},\ldots,\Theta_{n}$ form the second level of $(R)$. Translation goes as follows.

Axioms translate to proof-links.

If $\rho_{1}$, $\rho_{2}$ are proof-nets with conclusions $\Gamma,A$ and $A^{\bot},\Delta$ respectively, then putting $\rho_{1}$, $\rho_{2}$ together and connecting their respective conclusions $A,A^{\bot}$ with a Cut-link produces a proof-structure, which is easily seen to be a proof-net. This is the translation of the Cut rule.

Similarly, if $\rho_{1}$, $\rho_{2}$ are proof-nets with conclusions $\Gamma,A$ and $B,\Delta$ respectively, then putting $\rho_{1}$, $\rho_{2}$ together and connecting their respective conclusions $A,B$ with a $\otimes$-link gives proof-net. This is the translation of the $(\otimes)$ rule. The $(\mathop{\vec{\otimes}})$ rule is treated in exactly the same way, with $\otimes$-link changed to $\mathop{\vec{\otimes}}$-link.

If $\rho$ is a proof-net with conclusions $\Gamma,A,B$, then attaching to conclusions $A,B$ a $\mathop{\wp}$-link gives a proof-net again. This is the translation of the $(\mathop{\wp})$ rule.

Finally, if $\rho$ is a proof-net of a decorated sequent $\Gamma,A,B$, and $A$ is not reachable from $B$, then by Remark 6, attaching to conclusions $A,B$ a $\mathop{\vec{\wp}}$-link gives a proof-net as well again. This is the translation of the $(\mathop{\vec{\wp}})$ rule.

Let us find the second level of rules.

3.1.2. Second level of the ($\mathop{\vec{\wp}}$) rule

Let $\Theta$ be a decorated sequent, whose underlying sequent is $\Gamma,A,B$. Assume that $\rho$ is a proof-net of $\Theta$, and let $\rho^{\prime}$ be obtained from $\rho$ by attaching a $\mathop{\vec{\wp}}$-link between $A$ and $B$. Let

[TABLE]

be two vectors in the sequent $\Gamma,A\mathop{\vec{\wp}}B$, which have no element in common.

We need to figure out under which conditions there is a switching of $\rho^{\prime}$ such that in the second round there exist pairwise nonintersecting essentially directed paths $\phi_{i}$ from $X_{i}$ to $Y_{i}$, $i=1,\ldots,n$. We consider possibilities case-by-case.

• •

Assume that $A\mathop{\vec{\wp}}B\not\in{\bf X}$, $A\mathop{\vec{\wp}}B\not\in{\bf Y}$, and none of $\phi_{1},\ldots,\phi_{n}$ meets $A$ or $B$. Then all $\phi_{1},\ldots,\phi_{n}$ lie entirely in $\rho$, and since $\rho$ is a proof-net of $\Theta$ it follows that ${\bf X}\rightrightarrows{\bf Y}$ in $\Theta$.

• •

Assume that $A\mathop{\vec{\wp}}B\in{\bf Y}$, and some of $\phi_{1},\ldots,\phi_{n}$ meets $A$. So we have $A\mathop{\vec{\wp}}B=Y_{j}$ for some $j$. Thus in the second round of $\rho$ there is an essentially directed path from $X_{j}$ to $A\mathop{\vec{\wp}}B$. Since the paths $\phi_{1},\ldots,\phi_{n}$ are pairwise non-intersecting, it follows $\phi_{i}$ does not meet $A\mathop{\vec{\wp}}B$ unless $i=j$. In particular, none of these paths meets $B$. (If there were such a path, then one of its endpoints would be $A\mathop{\vec{\wp}}B$.)

Then, restricting to $\rho$, we get in $\rho$ an essentially directed path from $X_{j}$ to $A$. It follows that

[TABLE]

in $\Theta$.

• •

Assume that $A\mathop{\vec{\wp}}B\in{\bf Y}$, and some of $\phi_{1},\ldots,\phi_{n}$ meets $B$. Then, just as above, we get

[TABLE]

in $\Theta$.

• •

Assume that $A\mathop{\vec{\wp}}B\in{\bf X}$, and some of $\phi_{1},\ldots,\phi_{n}$ meets $A$. Then, just as above, we get

[TABLE]

in $\Theta$.

• •

Assume that $A\mathop{\vec{\wp}}B\in{\bf X}$, and some of $\phi_{1},\ldots,\phi_{n}$ meets $B$. Then, just as above, we get

[TABLE]

in $\Theta$.

• •

Finally, assume that $A\mathop{\vec{\wp}}B\not\in{\bf X}$, $A\mathop{\vec{\wp}}B\not\in{\bf Y}$, and some of $\phi_{1},\ldots,\phi_{n}$ meets $A$ or $B$. If the path $\phi_{j}$ from $X_{j}$ to $Y_{j}$ meets $A$ or $B$, then it meets $A\mathop{\vec{\wp}}B$. Indeed, the endpoints of $\phi_{j}$ are conclusions of $\rho^{\prime}$, so neither $A$ nor $B$ can be a conclusion of $\phi_{j}$. Furthermore, the link $A\mathop{\vec{\wp}}B$ is not an endpoint of $\phi_{j}$, so it is a critical link of $\phi_{j}$. Then, since $\phi_{j}$ is essentially directed, it follows that it has the form $X_{j}\ldots,A,A\mathop{\vec{\wp}}B,B,\ldots,Y_{j}$. Then, restricting to $\rho$, we get in $\rho$ essentially directed paths from $X_{j}$ to $A$ and from $B$ to $Y_{j}$. It follows that

[TABLE]

in $\Theta$.

• •

There are no other possibilities.

The decoration of $\Gamma,A\mathop{\vec{\wp}}B$ in $\rho^{\prime}$ is read from the above exhausting list.

Using property (iii) in the definition 3.1, the rules for computing the decoration can be written in a more compact form.

Rule $(\mathop{\vec{\wp}})$, second level:

Reachability on $\Gamma,A\mathop{\vec{\wp}}B$ is the smallest relation satisfying properties (i)–(iv) of Definition 3.1 and the following conditions:

• •

If ${\bf X}\rightrightarrows{\bf Y}$ in $\Theta$, then ${\bf X}\rightrightarrows{\bf Y}$ in $\Theta^{\prime}$.

• •

If $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A)$ or $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},B)$ in $\Theta$, then $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A\mathop{\vec{\wp}}B)$ in $\Theta^{\prime}$. Here $A,B\not\in({\bf X^{\prime}},{\bf Y},X)$.

• •

If $({\bf X},A)\rightrightarrows({\bf Y^{\prime}},Y)$ or $({\bf X},B)\rightrightarrows({\bf Y^{\prime}},Y)$ in $\Theta$, then $({\bf X},A\mathop{\vec{\wp}}B)\rightrightarrows({\bf Y^{\prime}},Y)$ in $\Theta^{\prime}$. Here $A,B\not\in({\bf X},{\bf Y^{\prime}},Y)$.

• •

If $({\bf X^{\prime}},X,B)\rightrightarrows({\bf Y^{\prime}},A,Y)$ in $\Theta$, then $({\bf X^{\prime}},X)\rightrightarrows({\bf Y^{\prime}},Y)$ in $\Theta^{\prime}$.

3.1.3. Second level of sequent rules

Second level for other rules is computed by a case-by-case analysis as in the preceding section. We simply write down the result. For each sequent rule, reachability relation on the conclusion is the smallest relation satisfying properties (i)–(iv) and the following conditions.

**The axioms: **

$A\rightrightarrows A^{\bot}$, $A^{\bot}\rightrightarrows A$.

**The $\mathop{\vec{\wp}}$-rule: **

If ${\bf X}\rightrightarrows{\bf Y}$ in the premise, then ${\bf X}\rightrightarrows{\bf Y}$ in the conclusion.

If $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A)$ or $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},B)$ in the premise, then in the conclusion $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A\mathop{\vec{\wp}}B)$. Here $A,B\not\in({\bf X^{\prime}},{\bf Y},X)$.

If $({\bf X},A)\rightrightarrows({\bf Y^{\prime}},Y)$ or $({\bf X},B)\rightrightarrows({\bf Y^{\prime}},Y)$ in the premise, then $({\bf X},A\mathop{\vec{\wp}}B)\rightrightarrows({\bf Y^{\prime}},Y)$ in the conclusion. Here $A,B\not\in({\bf X},{\bf Y^{\prime}},Y)$.

If $({\bf X^{\prime}},X,B)\rightrightarrows({\bf Y^{\prime}},A,Y)$ in the premise then $({\bf X^{\prime}},X)\rightrightarrows({\bf Y^{\prime}},Y)$ in the conclusion.

**The $\otimes$-rule: **

If we have in the first premise ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$, and in the second premise ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$, then in the conclusion $({\bf X_{1}},{\bf X_{2}})\rightrightarrows({\bf Y_{1}},{\bf Y_{2}})$. Here we suppose $A\not\in({\bf X_{1}},{\bf Y_{1}})$, $B\not\in({\bf X_{2}},{\bf Y_{2}})$.

If we have in the first premise $({\bf X_{1}},X)\rightrightarrows({\bf Y_{1}},A)$, and in the second premise $({\bf X_{2}},B)\rightrightarrows({\bf Y_{2}},Y)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $X\not\in({\bf X_{1}},{\bf Y_{1}})$, $Y\not\in({\bf X_{2}},{\bf Y_{2}})$.

Similarly, if in the first premise $({\bf X_{1}},A)\rightrightarrows({\bf Y_{1}},Y)$, and in the second premise $({\bf X_{2}},X)\rightrightarrows({\bf Y_{2}},B)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $Y\not\in({\bf X_{1}},{\bf Y_{1}})$, $X\not\in({\bf X_{2}},{\bf Y_{2}})$

If we have in the first premise $({\bf X_{1}},X)\rightrightarrows({\bf Y_{1}},A)$, and in the second premise ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},A\otimes B)$. Here we suppose $X\not\in({\bf X_{1}},{\bf Y_{1}})$, $B\not\in({\bf X_{2}},{\bf Y_{2}})$.

If in the first premise ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$, and in the second premise $({\bf X_{2}},X)\rightrightarrows({\bf Y_{2}},B)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},A\otimes B)$. Here we suppose $A\not\in({\bf X_{1}},{\bf Y_{1}})$, $X\not\in({\bf X_{2}},{\bf Y_{2}})$.

Similarly, if in the first premise $({\bf X_{1}},A)\rightrightarrows({\bf Y_{1}},Y)$, and in the second premise ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},A\otimes B)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $Y\not\in({\bf X_{1}},{\bf Y_{1}})$, $B\not\in({\bf X_{2}},{\bf Y_{2}})$.

If in the first premise ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$, and in the second premise $({\bf X_{2}},B)\rightrightarrows({\bf Y_{2}},Y)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},A\otimes B)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $A\not\in({\bf X_{1}},{\bf Y_{1}})$, $Y\not\in({\bf X_{2}},{\bf Y_{2}})$.

**The $\mathop{\wp}$-rule: **

If ${\bf X}\rightrightarrows{\bf Y}$ in the premise, then ${\bf X}\rightrightarrows{\bf Y}$ in the conclusion.

If $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A)$ or $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},B)$ in the premise, then in the conclusion $({\bf X^{\prime}},X)\rightrightarrows({\bf Y},A\mathop{\wp}B)$. Here $A,B\not\in({\bf X^{\prime}},{\bf Y},X)$.

If $({\bf X},A)\rightrightarrows({\bf Y^{\prime}},Y)$ or $({\bf X},B)\rightrightarrows({\bf Y^{\prime}},Y)$ in the premise, then $({\bf X},A\mathop{\wp}B)\rightrightarrows({\bf Y^{\prime}},Y)$ in the conclusion. Here $A,B\not\in({\bf X},{\bf Y^{\prime}},Y)$.

**The $\mathop{\vec{\otimes}}$-rule: **

See the preceding section.

If we have in the first premise $({\bf X_{1}},X)\rightrightarrows({\bf Y_{1}},A)$, and in the second premise $({\bf X_{2}},B)\rightrightarrows({\bf Y_{2}},Y)$, then we have $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$ in the conclusion. Here we suppose $Y\not\in({\bf X_{2}},{\bf Y_{2}})$, $X\not\in({\bf X_{1}},{\bf Y_{1}})$.

If we have in the first premise $({\bf X_{1}},X)\rightrightarrows({\bf Y_{1}},A)$, and in the second premise ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},A\mathop{\vec{\otimes}}B)$. Here we suppose $X\not\in({\bf X_{1}},{\bf Y_{1}})$.

If in the first premise ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$, and in the second premise $({\bf X_{2}},X)\rightrightarrows({\bf Y_{2}},B)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},A\mathop{\vec{\otimes}}B)$. Here we suppose $A\not\in({\bf X_{1}},{\bf Y_{1}})$, $X\not\in({\bf X_{2}},{\bf Y_{2}})$.

If we have in the first premise $({\bf X_{1}},A)\rightrightarrows({\bf Y_{1}},Y)$, and in the second premise ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},A\mathop{\vec{\otimes}}B)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $Y\not\in({\bf X_{1}},{\bf Y_{1}})$, $B\not\in({\bf X_{2}},{\bf Y_{2}})$.

If in the first premise ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$, and in the second premise $({\bf X_{2}},B)\rightrightarrows({\bf Y_{2}},Y)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},A\mathop{\vec{\otimes}}B)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. We suppose here $A\not\in({\bf X_{2}},{\bf Y_{2}})$, $Y\not\in({\bf X_{2}},{\bf Y_{2}})$.

**The Cut rule: **

If we have in the first premise $({\bf X_{1}},X)\rightrightarrows({\bf Y_{1}},A)$, and in the second premise $({\bf X_{2}},A^{\bot})\rightrightarrows({\bf Y_{2}},Y)$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $Y\not\in{\bf X_{2}},{\bf Y_{2}}$, $X\not\in({\bf X_{1}},{\bf Y_{1}})$.

Similarly, if in the first premise $({\bf X_{1}},A)\rightrightarrows({\bf Y_{1}},Y)$, and in the second premise $({\bf X_{2}},X)\rightrightarrows({\bf Y_{2}},A^{\bot})$, then in the conclusion $({\bf X_{1}},{\bf X_{2}},X)\rightrightarrows({\bf Y_{1}},{\bf Y_{2}},Y)$. Here we suppose $Y\not\in{\bf X_{1}},{\bf Y_{1}}$, $X\not\in({\bf X_{2}},{\bf Y_{2}})$.

Now, by the very construction, any decorated sequent calculus derivation of a decorated sequent $\Gamma$ translates into a proof-net of $\Gamma$. This implies soundness of the (decorated) sequent calculus.

Lemma 7**.**

If a decorated sequent $\Theta$ is derivable in the decorates sequent calculus above, then it is derivable in ScMLL.

3.2. Completeness

Now we are going to prove completeness of the decorated sequent calculus. Similarly to the case of proof-nets there is the commutative projection map from decorated sequent calculus proofs to ordinary MLL sequent calculus proofs, obtained by erasing all arrows above connectives, and forgetting decorations. In more details, and restricting to cut-free proofs:

• •

an ScMLL formula $F$ is mapped to an MLL formula $F^{\prime}$ by replacing each $\mathop{\vec{\otimes}}$, respectively, $\mathop{\vec{\wp}}$ connective to $\otimes$, respectively, $\mathop{\wp}$ connective;

• •

an ScMLL sequent $\Theta=F_{1},\ldots,F_{n}$ is mapped to the MLL sequent $F_{1}^{\prime},\ldots,F_{n}^{\prime}$;

• •

a decorated sequent calculus proof $\sigma$ of $\Gamma$ is mapped to an MLL sequent calculus proof $\sigma^{\prime}$ of $\Gamma^{\prime}$ by induction. Axiom is mapped to itself. A decorated sequent calculus proof obtained from proofs $\sigma_{1}$, $\sigma_{2}$ by the $(\otimes)$ or $(\mathop{\vec{\otimes}})$ rule is mapped to the MLL proof obtained from $\sigma_{1}$, $\sigma_{2}$ by the $(\otimes)$ rule. A decorated sequent calculus proof obtained from a proof $\sigma_{0}$ by the $(\mathop{\wp})$ or $(\mathop{\vec{\wp}})$ rule is mapped to the MLL proof obtained from $\sigma_{0}$ by the $(\mathop{\wp})$ rule.

Also, recall from the preceding section that any decorated sequent calculus derivation translates to an ScMLL proof-net. Similarly, an MLL sequent derivation translates to an MLL proof-net. In both cases we denote the proof-net obtained from a derivation $\sigma$ as $T(\sigma)$.

Lemma 8**.**

There is a sequentialization map from cut-free proof-nets to cut-free ScMLL sequent proofs which sends a proof-net $\rho$ of a decorated sequent $\Theta$ to a decorated sequent calculus derivation $\pi(\rho)$ of $\Theta$.

Proof 3.3**.**

There exists a sequentialization map sending a cut-free MLL proof-net of a sequent $\Gamma$ to a cut-free MLL derivation of $\Gamma$. Let us denote this map as $\pi$. Then for any MLL proof-net $\rho$ we have $T\circ\pi(\rho)=\rho$.

Now let $\rho$ be a cut-free ScMLL proof-net of a decorated sequent $\Gamma$, and let $\rho^{\prime}$ be its commutative projection. Then we have an MLL sequent calculus derivation $s=\pi(\rho^{\prime})$ of $\Theta^{\prime}$. By induction on $s$ we show that there exists a decorated sequent calculus derivation $\sigma$ of $\Theta$ such that the commutative projection $\sigma^{\prime}=s$ and the translation $T(\sigma)=\rho$.

If $s$ is an axiom, then $\rho=\rho^{\prime}$ is an axiom link, and we take $\sigma=s$.

Let $s$ be obtained from an MLL derivation $s_{0}$ by the $(\mathop{\wp})$ rule as follows

[TABLE]

Then the MLL proof-net $T(s)=\rho^{\prime}$ is obtained from $T(s_{0})$ by attaching an $\mathop{\wp}$-link. It follows that $\Theta^{\prime}=\Gamma_{0},A\mathop{\wp}B$ and

[TABLE]

or

[TABLE]

for some $\Gamma,A,B$ such that $\Gamma_{0}=\Gamma^{\prime}$, $A_{0}=A^{\prime}$, $B_{0}=B^{\prime}$.

By induction hypothesis there exists a decorated sequent calculus derivation $\sigma_{0}$ of $\Gamma,A,B$. If (7) holds, we obtain $\sigma$ from $\sigma_{0}$ by the $(\mathop{\wp})$ rule. If (8) holds, then formulas $A$, $B$ are connected with a $\mathop{\vec{\wp}}$-link in $\rho$. Then by Remark 6 $A$ is not reachable from $B$, and we can apply the $(\mathop{\vec{\wp}})$ rule to $\sigma_{0}$, which gives the desired $\sigma$. Remaining steps are similar.

We define $\pi(\rho)=\sigma$.

4. Variations of the logic

We now proceed to “degenerate” variations of ScMLL. Our final goal is to obtain a version with self-dual $\mathop{\vec{\wp}}$, which turns out equivalent to Pomset logic.

4.1. Adding Mix

Recall that the system MLL+Mix is obtained from MLL by adding the Mix rule

[TABLE]

See [FR94] for a syntax of proof-nets.

We want to add this rule to ScMLL to get the system ScMLL+Mix. The proof-structures for ScMLL+Mix are the same as for ScMLL. The definition of proof-nets is relaxed in the first-round part, right as in the familiar case of Danos-Regnier criterion for MLL+Mix [FR94]. {defi} An ScMLL+Mix proof-net is a proof-structure $\rho$, such that for any switching $\sigma$ the first round is acyclic, and the second round has no essentially directed cycles.

The decorated sequent calculus for ScMLL+Mix is also the same as for ScMLL, supplied with a decorated version of Mix rule.

{defi}

In the decorated sequent calculus the Mix rule is defined by (9) supplied with the following second level part.

Reachability relation on the conclusion of (9) is the smallest relation satisfying properties (i)–(iv) of Definition 3.1 and the condition

• •

if ${\bf X_{1}}\rightrightarrows{\bf Y_{1}}$ in the first premise, and ${\bf X_{2}}\rightrightarrows{\bf Y_{2}}$ in the second premise, then $({\bf X_{1}},{\bf X_{2}})\rightrightarrows({\bf Y_{1}},{\bf Y_{2}})$ in the conclusion.

All above constructions and results for ScMLL go as well for ScMLL with minor variations, which are straightforward.

We summarise in the following

Theorem 9**.**

There is an algorithm transforming any ScMLL proof-net with cut-links to a cut-free ScMLL proof-net of the same sequent.

A sequent is derivable in ScMLL+Mix iff it is derivable by means of a cut-free proof-net.

ScMLL+Mix is a conservative extension of MLL+Mix. A sequent $\Gamma$ is derivable in ScMLL+Mix iff some its decoration is derivable in ScMLL+Mix sequent calculus iff some its decoration is derivable in the cut-free ScMLL+Mix sequent calculus. ∎

Observe that using the Mix rule we can derive not only the “commutative” Mix principle

[TABLE]

but its “noncommutative” version as well

[TABLE]

A proof-net for (10) is the following one.

[TABLE]

Observe that this is not a proof-net for ScMLL, because the first round of any of its switchings is not connected.

In the spirit of Remark 1 let us summarize.

Remark 10**.**

The logic ScMLL+Mix contains ScMLL. ScMLL+Mix derives (6).

ScMLL+Mix still does not derive $A\mathop{\vec{\otimes}}B\vdash B\mathop{\vec{\otimes}}A$. ∎

4.2. Self-dual $\mathop{\vec{\wp}}$. Retoré logic

Having Mix, we can add one more “level of degeneracy” and obtain a consistent system with $\mathop{\vec{\otimes}}$ and $\mathop{\vec{\wp}}$ declared isomorphic. This system turns out equivalent to Pomset logic of Retoré, and it seems fair to call it Retoré logic (RL).

Now, having two distinct connectives $\mathop{\vec{\otimes}}$ and $\mathop{\vec{\wp}}$ which are exactly equivalent leads to very uneconomical definitions, where lot of things are just repeated twice. Therefore we define the language of RL as that of MLL supplied with one additional connective $\mathop{\vec{\wp}}$.

Furthermore we redefine linear negation for RL. Linear negation in RL is defined as in MLL, supplied with the rule

[TABLE]

Remark 11**.**

The reason we keep notation $\mathop{\vec{\wp}}$ for the unique noncommutative connective of RL is that we want to use commutative projections, just as in the case of ScMLL. And projecting the noncommutative connective to $\mathop{\wp}$ produces correct proof-nets for MLL+Mix.

Proof-structures for RL are defined formally as proof-structures for ScMLL without $\mathop{\vec{\otimes}}$-links. We should keep in mind, however, that RL proof-structures have cut-links different from ScMLL proof-structures, because the negation is different. Indeed, for a formula $A=F\mathop{\vec{\wp}}G$, the cut-link

[TABLE]

looks as the following,

[TABLE]

and such a link does not exist in ScMLL.

With this in mind, definition of an RL proof-net is the same as Definition 4.1 of ScMLL+Mix proof-net, with words “ScMLL+Mix” replaced with “RL”.

The sequent calculus is defined formally by the rules of ScMLL+Mix in the language without $\mathop{\vec{\otimes}}$ (hence there is no $\mathop{\vec{\otimes}}$ rule). But, again, we should keep in mind that individual instances of the Cut-rule are different from those in ScMLL+Mix, because the negation is different.

The results and constructions for ScMLL and ScMLL+Mix go for RL as well with minor variations. In particular, the correspondence between cut-free proof-nets and cut-free sequent proofs is obtained for free, because the cut-free part of RL (both on the proof-nets side and on the decorated sequents side) is literally the same as the cut-free part of ScMLL+Mix in the language without $\mathop{\vec{\otimes}}$. The only point that may deserve some attention is cut-elimination for proof-nets.

Lemma 12**.**

There is an algorithm transforming any RL proof-net with cut-links to a cut-free RL proof-net with the same conclusions.

Proof 4.1**.**

Again, the algorithm is that of ordinary MLL as far as unordered links are concerned.

The new case is when the cut-link is between formulas $A\mathop{\vec{\wp}}B$, $A^{\bot}\mathop{\vec{\wp}}B^{\bot}$. This is replaced by two cut-links, between $A$ and $A^{\bot}$ and between $B$ and $B^{\bot}$.

We need to check that this step transforms proof-nets to proof-nets. But now we should consider the first-round part as well: we cannot refer to commutative projections, because there is no such a reduction step in the commutative logic.

Thus, let $\rho$ be an RL proof-net with a cut-link between $A\mathop{\vec{\wp}}B$ and $A^{\bot}\mathop{\vec{\wp}}B^{\bot}$, and let the proof-structure $\rho^{\prime}$ be obtained from $\rho$ by a one-step reduction.

Assume that for some switching $\sigma$ of $\rho^{\prime}$ there is a cycle $\phi$ in the first round. Observe then that $\phi$ has no critical links (indeed, there are no $\mathop{\vec{\otimes}}$-links, and for any $\mathop{\vec{\wp}}$-link, one edge is erased by $\sigma$). Hence $\phi$ is essentially directed, even stronger: it is essentially directed for both possible choices of its direction. Then, removing from $\phi$ the cut-links between $A,A^{\bot}$ and $B,B^{\bot}$ (the path $\phi$ must pass through at least one of these links) we obtain at least one essentially directed path $\phi_{0}$ in $\rho\cap\rho^{\prime}$, connecting two vertices in the set $A,A^{\bot},B,B^{\bot}$. But this gives rise to an essentially directed cycle in the second round for any switching of $\rho$ that agrees with $\sigma$ on $\rho\cap\rho^{\prime}$. Which is impossible.

The second-round part goes exactly as in Lemma 2 for ScMLL.

Again we summarize with a theorem.

Theorem 13**.**

A sequent is derivable in RL iff it is derivable by means of a cut-free proof-net.

RL is a conservative extension of MLL+Mix.

A sequent $\Gamma$ is derivable in RL iff some its decoration is derivable in RL sequent calculus iff some its decoration is derivable in the cut-free RL sequent calculus.

In the next section we show that RL is equivalent to Pomset logic. As a consequence, RL decorated sequent calculus gives a sequent calculus formulation of Pomset logic, which is one of the key results of the paper.

5. Relationship with Pomset logic

5.1. R&B proof-nets and Pomset logic

We define Pomset logic [Ret97] in the language of RL, i.e. MLL plus one self-dual connective $\mathop{\vec{\wp}}$, by means of special proof-nets. (Retoré in [Ret97] uses notation $<$ for the noncommutative connective)

Again proof-nets are defined in two steps.

An R&B proof-structure is a mixed graph whose edges have one of the two types, regular or bold, some regular edges may be directed, and whose vertices are labeled by formulas, connectives or symbols “Cut”. Some vertices, labeled by formulas are conclusions.

Proof-structures are built inductively by the following rules.

A graph with two vertices labeled by dual propositional symbols $p$ and $p^{\bot}$ connected by one undirected bold edge is a proof-structure with conclusions $p$, $p^{\bot}$, an axiom link.

[TABLE]

A disjoint union of two proof-structures $\rho_{1}$ and $\rho_{2}$ is a proof-structure whose conclusions are those of $\rho_{1}$ or $\rho_{2}$.

If $\rho$ is a proof-structure whose conclusions contain two (vertices labeled by) formulas $A$ and $B$, then a new proof-structure $\rho^{\prime}$ can be obtained, by attaching to $A$ and $B$ one of the following graphs,

[TABLE]

respectively, $\otimes$-link, $\mathop{\wp}$-link, and $\mathop{\vec{\wp}}$-link.

In each of the above links, the edge connecting the vertex labeled by the connective to the vertex labeled by the conclusion is bold, and all other edges are regular. In $\otimes$- and $\mathop{\wp}$-link all edges are undirected, and in the $\mathop{\vec{\wp}}$-link with conclusion $A\mathop{\vec{\wp}}B$, the only directed edge is the regular edge from $A$ to $B$. The new proof-structure $\rho^{\prime}$ has the same conclusions as $\rho$ except for $A$ and $B$, and one new conclusion, respectively $A\otimes B$, $A\mathop{\wp}B$, or $A\mathop{\vec{\wp}}B$, depending on the link attached.

If $\rho$ is a proof-structure whose conclusions contain two (vertices labeled by) dual formulas $A$ and $A^{\bot}$, then a new proof-structure $\rho^{\prime}$ can be obtained, by attaching the following graph, a Cut-link,

[TABLE]

which is similar to a $\otimes$-link.

The new proof-structure $\rho^{\prime}$ has the same conclusions as $\rho$ except for $A$ and $A^{\bot}$.

An alternating path in the proof-structure $\rho$ is a directed path whose edges alternate: …-regular-bold-regular-…An alternating elementary circuit (a.e. circuit) in the proof-structure $\rho$ is an alternating path whose endpoint vertices coincide, and which traverses all its other vertices exactly once.

{defi}

An R&B proof-net is a proof-structure that has no a.e. circuit.

{defi}

A sequent $\Gamma$ is derivable in Pomset logic if there exists an R&B proof-net whose multiset of conclusions is $\Gamma$. A formula $A$ is derivable in Pomset logic if there exists an R&B proof-net whose only conclusion is $A$.

The following is proven in [Ret97]. {thmC}[[Ret97]] A sequent is derivable in Pomset logic iff it is derivable by means of a cut-free R&B proof-net.

Pomset logic is a conservative extension of MLL+Mix. ∎

We are going to prove that Pomset logic is equivalent to RL. For that purpose, in the next section we introduce alternative proof-nets for RL, which make this equivalence more transparent.

5.2. Retoré proof-nets for Retoré logic

It turns out that proof-nets for RL can be defined in a simpler way, using switchings with only one round.

{defi}

A Retoré switching of an RL proof-structure is a graph obtained by:

1. (1)

for each $\mathop{\wp}$-link, erasing one of the two edges forming the link, 2. (2)

for some of $\mathop{\vec{\wp}}$-links, erasing one of the two edges forming the link and making the remaining edge undirected.

{defi}

A Retoré proof-net is an RL proof-structure such that for any Retoré switching the resulting graph has no elementary directed cycles.

Lemma 14**.**

An RL proof-structure $\rho$ is an RL proof-net iff it is a Retoré proof-net.

Proof 5.1**.**

Assume that for some Retoré switching of $\rho$ there is an elementary directed cycle $\phi$. Define an ordinary switching $\sigma$ of $\rho$ by choosing, for each $\mathop{\wp}$-link traversed by $\phi$ and for each $\mathop{\vec{\wp}}$-link traversed by $\phi$ and not critical for $\phi$, the edge that is not traversed by $\phi$ and extending this to the whole of $\rho$ in an arbitrary way. If $\phi$ has no critical links, then $\phi$ is a cycle in the first round of $\sigma$. Otherwise $\phi$ is an essentially directed cycle in the second round. Hence $\rho$ is not a proof-net

Assume that $\rho$ is not a proof-net. Then there exists a switching $\sigma$ of $\rho$ with either a cycle in the first round, or an essentially directed cycle in the second round.

If there is a cycle $\phi$ in the first round, then define a Retoré switching by erasing all edges, chosen by $\sigma$. The cycle $\phi$ is directed for this Retoré switching (because it traverses only undirected edges).

If there is an essentially directed cycle in the second round, define a Retoré switching by erasing, for each $\mathop{\wp}$-link and for each $\mathop{\vec{\wp}}$-link not critical for $\phi$, the edge chosen by $\sigma$. The cycle $\phi$ is directed in this Retoré switching. Hence $\rho$ is not a Retoré proof-net.

Corollary 15**.**

A sequent $\Gamma$ is derivable in RL iff there exists a Retoré proof-net with conclusions $\Gamma$ iff there exists a cut-free Retoré proof-net with conclusions $\Gamma$.

With the above Corollary, we are ready to establish equivalence of RL and Pomset logic.

5.3. Equivalence of systems

Clearly there is one-to-one correspondence between R&B proof-structures and RL proof-structures, as there is such a correspondence on the level of links. To show equivalence of RL and Pomset logic, it is sufficient to show that this correspondence takes proof-nets to proof-nets. And, thanks to cut-elimination, we may restrict our attention to cut-free proof-nets.

So, let $\rho$ be an RL proof-net, and let $\hat{\rho}$ be the corresponding R&B proof-structure.

Lemma 16**.**

If for some Retoré switching $\sigma$ of $\rho$ there is an elementary directed cycle in $\sigma$, then there is an a.e. circuit $\hat{\phi}$ in $\hat{\rho}$.

Proof 5.2**.**

Without loss of generality we may assume that in all $\mathop{\vec{\wp}}$-links not critical for $\phi$ one of the edges is erased by $\sigma$.

We introduce the following terminology. A turn in $\phi$ is a $\otimes$- or $\mathop{\vec{\wp}}$-link, such that $\phi$ traverses both its premises and conclusion in the order: one premise — conclusion — the other premise; we identify such a link with a directed subpath of $\phi$. A monotone edge of $\phi$ is any edge of $\phi$ that is not in a turn and is not an axiom link. A monotone path in $\phi$ is any subpath of $\phi$ consisting of monotone edges.

Note that the only directed edges of $\phi$ occur in turns, more precisely, in its critical $\mathop{\vec{\wp}}$-links. A monotone path has no directed edges, so it has two possible orientations. We call a monotone path downward if the direction is chosen from formulas of lower complexity to formulas of higher complexity, otherwise it is upward.

The cycle $\phi$ has a representation as a concatenation of directed paths: …— axiom link — downward path — turn — upward path — axiom link — …

We are going to translate subpaths of $\phi$ to alternating paths in $\hat{\phi}$ satisfying the following conditions.

• •

A downward subpath is translated to an alternating path whose first edge is regular and whose last edge is bold, and which does not have directed edges.

• •

An upward subpath is translated to an alternating path whose first edge is bold and whose last edge is regular, and which does not have directed edges.

• •

An axiom link is translated to an axiom link (which is bold).

• •

A turn is translated to a regular edge.

• •

If the last vertex of the subpath $\alpha$ is the first vertex of the subpath $\beta$, then the same holds for their translations $\hat{\alpha}$ and $\hat{\beta}$: the last vertex of $\hat{\alpha}$ is the first vertex of $\hat{\beta}$.

It is clear that the translated subpaths, when concatenated, produce an a.e. circuit in $\hat{\rho}$. The translation goes as follows.

Axiom links of $\rho$ are translated to their images in $\hat{\rho}$ in the obvious way.

A downward edge has one of the three possible forms

[TABLE]

These are translated to alternating paths, respectively,

[TABLE]

in $\hat{\rho}$. A downward path is translated edge by edge. The case of an upward path is mirror symmetric.

A turn has one of the two possible forms:

[TABLE]

or

[TABLE]

For the first case: the vertices $A$ and $B$ in $\hat{\rho}$ are adjacent to a $\otimes$-link, hence they are connected by an undirected regular edge. This gives the translation.

For the second case, the vertices $A$ and $B$ in $\hat{\rho}$ are adjacent to a $\mathop{\vec{\wp}}$-link, hence they are connected by a directed regular edge $A-B$. (Note that the direction of the regular edge in $\hat{\rho}$ in the obvious sense agrees with the direction of the turn in $\rho$.) This, again, gives the translation.

The converse is similar, but somewhat easier, because in $\rho$ we do not have to care about alternation of edges.

Lemma 17**.**

If in $\hat{\rho}$ there is an a.e. circuit $\phi$, then there exists some Retoré switching $\sigma$ of $\rho$ with an elementary directed cycle.

Proof 5.3**.**

Note that for each $\mathop{\wp}$-link or $\mathop{\vec{\wp}}$-link in $\hat{\rho}$ the cycle $\phi$ traverses at most one of its regular edges, otherwise in $\phi$ there are two regular edges in a row. (Actually the same holds for $\otimes$-links as well, but we do not need this observation.)

We define a Retoré switching $\sigma$ of $\rho$ as follows.

Assume there is a $\mathop{\wp}$-link in $\hat{\rho}$ with conclusion $A\mathop{\wp}B$ traversed by $\phi$. In the corresponding $\mathop{\wp}$-link in $\rho$ erase the edge $A-A\mathop{\wp}B$, if $\phi$ goes through $B-\mathop{\wp}$, and erase $B-A\mathop{\wp}B$, if $\phi$ goes through $A-\mathop{\wp}$.

Assume there is a $\mathop{\vec{\wp}}$-link in $\hat{\rho}$ with conclusion $A\mathop{\vec{\wp}}B$ traversed by $\phi$. In the corresponding $\mathop{\vec{\wp}}$-link in $\rho$ erase the edge $A-A\mathop{\vec{\wp}}B$, if $\phi$ goes through $B-\mathop{\vec{\wp}}$, and erase $B-A\mathop{\vec{\wp}}B$, if $\phi$ goes through $A-\mathop{\vec{\wp}}$. Do not erase anything, if $\phi$ goes through $A-B$.

It is straightforward that $\phi$ translates to a directed cycle in this switching of $\rho$.

This gives us the following.

Corollary 18**.**

Pomset logic and RL are equivalent.

We conclude with one of the key results of the paper.

Corollary 19**.**

The sequent calculus for RL is sound and complete for Pomset logic.

Remark 20**.**

It is worth noting that we could have given an alternative proof of equivalence between RL and Pomset logic by showing directly that the sequent calculus for RL is sound and complete for Pomset logic. For that, we need to interpret reachability in decorated sequents as: $(X_{1},\ldots,X_{n})\rightrightarrows(Y_{1},\ldots,Y_{n})$ iff in the corresponding R&B proof-net there are pairwise nonintersecting alternating paths from $X_{i}$ to $Y_{i}$, $i=1,\ldots,n$, starting and ending with bold edges. Then we can mimic soundness and completeness proofs for RL of this paper.

On the other hand, we can argue that the formalism of Retoré proof-nets that we use is an interesting alternative to original R&B proof-nets. This formalism seems closer to a more common presentation of MLL proof-nets as in [Gir95], and the correctness criterion appears as a simple generalization of the familiar Danos-Regnier criterion

6. Conclusion and further work

We defined a system of semicommutative linear logic, which is a non-commutative extension of multiplicative linear logic, by means or proof-nets and by means of decorated sequent calculus. We then constructed Retoré logic as a degenerate variant and showed that its equivalent to Pomset logic. As a consequence, we found an alternative presentation of Pomset logic in terms of Retoré prof-nets and as a decorated sequent calculus.

The system ScMLL was discovered by the author semantically. Two non-isomorphic dual noncommutative connectives arise when the construction of [BPS12] for modeling Retoré’s noncommutative connective in probabilistic coherent spaces is generalized to a wider class of partially ordered vector spaces. This will be shown in a forthcoming paper.

The question of general category-theoretic axiomatization remains open. This applies to RL (Pomset logic) as well. An attempt of categorical axiomatization of the deep inference system BV (conjecturally equivalent to Pomset logic) has been done in [BPS12], however no kind of soundness was proven in that work.

The problem of equivalence of BV and Pomset logic itself is a sufficiently long standing open question related to the subject of the current paper. The author would like to believe that having now a sequent calculus, we can somehow progress with this problem.

Finally, there is a wide field for work on extending semicommutative logic to additive and exponential fragments. An interesting question is if there are any new modalities associated to the new connectives. (In Pomset logic there is, indeed, a self-dual modality for the self-dual “before” [Ret94b].)

Acknowledgment

The author is grateful to Lutz Strassburger for comments and useful discussions.