**Definition 4.1** [AB09, Section 5.5]. $\Sigma_2^P$ is $\mathbf{NP}$ extended with an $\mathbf{NP}$ oracle; this is usually written as $\Sigma_2^P = \mathbf{NP}^{\mathbf{NP}}$. In other words, a decision problem is in $\Sigma_2^P$ if and only if it can be solved by an $\mathbf{NP}$ algorithm that can call constant time subroutines for problems in $\mathbf{NP}$. Similarly, $\Pi_2^P$ is co$\mathbf{NP}$ extended with an $\mathbf{NP}$ oracle: $\Pi_2^P = \mathbf{coNP}^{\mathbf{NP}}$.

Conversely, to show hardness results, we use complete problems involving Boolean formulas. We consider a fixed set of (Boolean) variables. A literal is either $x$ or $\neg x$ for some variable $x$; a clause is a finite set of literals; a conjunctive normal form (CNF) is a finite set of clauses. The idea is that a CNF represents a Boolean formula, as in the following example:

$$ \{\{x, y, z\}, \{\neg x, y\}, \{\neg y, \neg z\}\} \rightsquigarrow (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z) $$

Consistent with this interpretation, a clause is said to be satisfied by some assignment from variables to Booleans in $\{\text{true}, \text{false}\}$ if it contains some literal $l$ such that for some variable $x$, either $l = x$ and $x$ is set to true, or $l = \neg x$ and $x$ is set to false; and an assignment is said to satisfy a CNF when it satisfies all its clauses. The celebrated Cook-Levin theorem states that finding a satisfying assignment for a CNF is $\mathbf{NP}$-complete. We recall its generalization to the first two levels of the polynomial hierarchy.

**Definition 4.2.** The problem CNF-SAT consists in deciding, given a CNF as input, whether it admits a satisfying assignment. It is generalized by $\forall\exists$-CNF-SAT, which takes as input

* a finite set of universal variables $X = \{x_1, \dots, x_n\}$,

* a finite set of existential variables $Y = \{y_1, \dots, y_m\}$, disjoint from $X$,

* and a CNF whose variables are included in $X \cup Y$,

the question being whether every partial assignment $X \to \{\text{true}, \text{false}\}$ can be extended to some assignment $X \cup Y \to \{\text{true}, \text{false}\}$ that satisfies the input CNF.

**Theorem 4.3** [Wra76, Cor. 6]. CNF-SAT is $\mathbf{NP}$-complete and $\forall\exists$-CNF-SAT is $\Pi_2^P$-complete.

As an example, the above-mentioned CNF $\{\{x, y, z\}, \{\neg x, y\}, \{\neg y, \neg z\}\}$, with the universal variables $\{x, y\}$ and the existential variable $\{z\}$, is a negative instance of $\forall\exists$-CNF-SAT since the corresponding quantified Boolean formula

$$ \forall x \forall y \exists z. (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z) $$

(where the quantifiers range over $\{\text{true}, \text{false}\}$) is false: for $x = \text{true}$ and $y = \text{false}$, there is no choice of $z$ that satisfies the clause $\neg x \lor y$. Let us conclude these preliminaries by mentioning that co$\mathbf{NP}$ and $\Sigma_2^P$ admit complete problems involving formulas in disjunctive normal forms.

**Remark 4.4.** There is a standard reduction from CNF-SAT to the case where all variables occur at least once positively and at least once negatively, which goes as follows. You can detect in polynomial time for which variables this is not the case, e.g. $x$ has only positive occurrences and $y$ has only negative occurrences. Then if you delete all clauses in which either $x$ or $\neg y$ appear (or both), this does not change whether the set of clauses is satisfiable (because if you set $x = \text{true}$ and $y = \text{false}$ you satisfy all deleted clauses and do not lose any degree of freedom for the remaining clauses). After this deletion maybe some other variable occurs with only one polarity, so you need to iterate that procedure. But as the number of iterations is bounded by the number of variables, this reduction is polynomial time.

Thus, this restriction of CNF-SAT is $\mathbf{NP}$-complete. For similar reasons, the instances of $\forall\exists$-CNF-SAT in which no atom appears with a single polarity are also $\Pi_2^P$-complete.
**Definition 4.1** [AB09, Section 5.5]. $\Sigma_2^P$ is $\mathbf{NP}$ extended with an $\mathbf{NP}$ oracle; this is usually written as $\Sigma_2^P = \mathbf{NP}^{\mathbf{NP}}$. In other words, a decision problem is in $\Sigma_2^P$ if and only if it can be solved by an $\mathbf{NP}$ algorithm that can call constant time subroutines for problems in $\mathbf{NP}$. Similarly, $\Pi_2^P$ is co$\mathbf{NP}$ extended with an $\mathbf{NP}$ oracle: $\Pi_2^P = \mathbf{coNP}^{\mathbf{NP}}$.

Conversely, to show hardness results, we use complete problems involving Boolean formulas. We consider a fixed set of (Boolean) variables. A literal is either $x$ or $\neg x$ for some variable $x$; a clause is a finite set of literals; a conjunctive normal form (CNF) is a finite set of clauses. The idea is that a CNF represents a Boolean formula, as in the following example:

$$ \{\{x, y, z\}, \{\neg x, y\}, \{\neg y, \neg z\}\} \rightsquigarrow (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z) $$

Consistent with this interpretation, a clause is said to be satisfied by some assignment from variables to Booleans in $\{\text{true}, \text{false}\}$ if it contains some literal $l$ such that for some variable $x$, either $l = x$ and $x$ is set to true, or $l = \neg x$ and $x$ is set to false; and an assignment is said to satisfy a CNF when it satisfies all its clauses. The celebrated Cook-Levin theorem states that finding a satisfying assignment for a CNF is $\mathbf{NP}$-complete. We recall its generalization to the first two levels of the polynomial hierarchy.

**Definition 4.2.** The problem CNF-SAT consists in deciding, given a CNF as input, whether it admits a satisfying assignment. It is generalized by $\forall\exists$-CNF-SAT, which takes as input

* a finite set of universal variables $X = \{x_1, \dots, x_n\}$,

* a finite set of existential variables $Y = \{y_1, \dots, y_m\}$, disjoint from $X$,

* and a CNF whose variables are included in $X \cup Y$,

the question being whether every partial assignment $X \to \{\text{true}, \text{false}\}$ can be extended to some assignment $X \cup Y \to \{\text{true}, \text{false}\}$ that satisfies the input CNF.

**Theorem 4.3** [Wra76, Cor. 6]. CNF-SAT is $\mathbf{NP}$-complete and $\forall\exists$-CNF-SAT is $\Pi_2^P$-complete.

As an example, the above-mentioned CNF $\{\{x, y, z\}, \{\neg x, y\}, \{\neg y, \neg z\}\}$, with the universal variables $\{x, y\}$ and the existential variable $\{z\}$, is a negative instance of $\forall\exists$-CNF-SAT since the corresponding quantified Boolean formula

$$ \forall x \forall y \exists z. (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z) $$

(where the quantifiers range over $\{\text{true}, \text{false}\}$) is false: for $x = \text{true}$ and $y = \text{false}$, there is no choice of $z$ that satisfies the clause $\neg x \lor y$. Let us conclude these preliminaries by mentioning that co$\mathbf{NP}$ and $\Sigma_2^P$ admit complete problems involving formulas in disjunctive normal forms.

**Remark 4.4.** There is a standard reduction from CNF-SAT to the case where all variables occur at least once positively and at least once negatively, which goes as follows. You can detect in polynomial time for which variables this is not the case, e.g. $x$ has only positive occurrences and $y$ has only negative occurrences. Then if you delete all clauses in which either $x$ or $\neg y$ appear (or both), this does not change whether the set of clauses is satisfiable (because if you set $x = \text{true}$ and $y = \text{false}$ you satisfy all deleted clauses and do not lose any degree of freedom for the remaining clauses). After this deletion maybe some other variable occurs with only one polarity, so you need to iterate that procedure. But as the number of iterations is bounded by the number of variables, this reduction is polynomial time.

Thus, this restriction of CNF-SAT is $\mathbf{NP}$-complete. For similar reasons, the instances of $\forall\exists$-CNF-SAT in which no atom appears with a single polarity are also $\Pi_2^P$-complete.
**4.2.** BV is NP-Complete (and how to Generalize Membership in NP). Let us first recall that the complexity of proof search in BV is already known.

**Theorem 4.5 (Kahramanoğulları [Kah08]).** *Provability in system BV is NP-complete.*

The **NP-hardness** part already applies to MLL+mix [Kah08, Corollary 4.5], which BV conservatively extends; we shall not dwell on this here. We will merely remark that while Kahramanoğulları proves that provability for MLL+mix is **NP-hard** using a syntactic analysis of the calculus of structures, one could presumably adapt the more traditional *phase semantics* methods used to study the hardness of other variants of linear logic in order to get an alternative proof.

Membership in **NP** is more interesting for us, since it demonstrates a complexity gap with the $\Sigma_2^P$-complete pomset logic (unless $NP = coNP$), as we already said. We recall here the proof that provability in $BV_u$ is in **NP** (the unit-free version is slightly more convenient), giving more details than [Kah08].

The first main argument is a bound on the length of proofs, relying on the following property.

**Definition 4.6.** We say that a rewriting system $\rightsquigarrow$ on unit-free formulas is *dicograph-monotone* when $\equiv' \subseteq \rightsquigarrow$ and for any $A \rightsquigarrow B$ such that $A \not\equiv' B$:

* either $\frac{B}{A}$ is an instance of an interaction rule of $BV_u$ (i.e., one of $ai^\circ \downarrow$, $ai^\otimes \downarrow$, $ai^\downarrow \downarrow$, $ai^\downarrow R \downarrow$);

* or $R_{\llbracket A \rrbracket} \subsetneq R_{\llbracket B \rrbracket}$ for a suitable identification of atom occurrences of $A$ and $B$ ensuring that we can consider the vertex sets $V_{\llbracket A \rrbracket}$ and $V_{\llbracket B \rrbracket}$ to be equal.

**Proposition 4.7.** $A \rightsquigarrow B \iff \frac{B}{A}$ in $BV_u$ defines a dicograph-monotone rewriting system.

*Proof.* This is a direct consequence of the easy direction (“if”) of Theorem 2.78. $\square$

<figure><img src="image_23.png" /></figure>

As discussed in Section 2.7, the rules of SBV are originally derived from a characterization of dicograph inclusion. Dicograph-monotonicity is therefore a fundamental aspect of the design of SBV, BV and their variants. We will discuss another example of this notion in Remark 4.12.

**Proposition 4.8.** Let $\rightsquigarrow$ be a dicograph-monotone relation and $\rightsquigarrow^*$ be its transitive closure. Then, for any $A \rightsquigarrow^* B$, there exists a path $A = C_1 \rightsquigarrow \dots \rightsquigarrow C_k = B$ with length $k = O(|A|^2)$.

*Proof.* Since $\equiv'$ is transitive by definition, if $C \rightsquigarrow D \rightsquigarrow E$ with $C \equiv' D \equiv' E$, then $C \rightsquigarrow E$ directly (by the assumption $\equiv' \subseteq \rightsquigarrow$). Thus, in the path of minimum length between $A$ and $B$, at least half of the rewrites $C_i \rightsquigarrow C_{i+1}$ satisfy $C_i \not\equiv' C_{i+1}$. Therefore, up to a factor of two (that gets absorbed in the $O(\cdot)$ notation), it suffices to bound the number of rewrites with $C_i \not\equiv' C_{i+1}$.

The definition of dicograph-monotonicity then gives us two cases. We claim that in both cases, $V_{\llbracket C_i \rrbracket}^2 \setminus R_{\llbracket C_i \rrbracket} \supsetneq V_{\llbracket C_{i+1} \rrbracket}^2 \setminus R_{\llbracket C_{i+1} \rrbracket}$. First, if $V_{\llbracket C_i \rrbracket} = V_{\llbracket C_{i+1} \rrbracket}$ and $R_{\llbracket C_i \rrbracket} \subsetneq R_{\llbracket C_{i+1} \rrbracket}$, then this is immediate. Otherwise, $C_i$ is inferred from $C_{i+1}$ by an interaction rule, and then $\llbracket C_{i+1} \rrbracket$ can be identified with an induced subgraph of $\llbracket C_i \rrbracket$ with two fewer vertices, resulting in a strict inclusion between the complement graphs as we wanted.

Therefore, the natural number $|V_{\llbracket C_i \rrbracket}^2 \setminus R_{\llbracket C_i \rrbracket}|$ strictly decreases at each rewriting step such that $C_i \not\equiv' C_{i+1}$. So, starting from $A$, the number of such steps is bounded by $|V_{\llbracket A \rrbracket}^2 \setminus R_{\llbracket A \rrbracket}| = O(|A|^2)$. (We see that our definition of dicograph-monotonicity is slightly stronger than what we truly need from the point of view of complexity.) $\square$

<figure><img src="image_24.png" /></figure>
**4.2.** BV is NP-Complete (and how to Generalize Membership in NP). Let us first recall that the complexity of proof search in BV is already known.

**Theorem 4.5 (Kahramanoğulları [Kah08]).** *Provability in system BV is NP-complete.*

The **NP-hardness part** already applies to MLL+mix [Kah08, Corollary 4.5], which BV conservatively extends; we shall not dwell on this here. We will merely remark that while Kahramanoğulları proves that provability for MLL+mix is **NP-hard** using a syntactic analysis of the calculus of structures, one could presumably adapt the more traditional *phase semantics* methods used to study the hardness of other variants of linear logic in order to get an alternative proof.

Membership in **NP** is more interesting for us, since it demonstrates a complexity gap with the $\Sigma_2^P$-complete pomset logic (unless $NP = coNP$), as we already said. We recall here the proof that provability in $BV_u$ is in **NP** (the unit-free version is slightly more convenient), giving more details than [Kah08].

The first main argument is a bound on the length of proofs, relying on the following property.

**Definition 4.6.** We say that a rewriting system $\rightsquigarrow$ on unit-free formulas is *dicograph-monotone* when $\equiv' \subseteq \rightsquigarrow$ and for any $A \rightsquigarrow B$ such that $A \not\equiv' B$:

* either $\frac{B}{A}$ is an instance of an interaction rule of $BV_u$ (i.e., one of $ai^\circ\downarrow$, $ai^\otimes\downarrow$, $ai^\downarrow\downarrow$, $ai^\downarrow R\downarrow$);

* or $R_{\llbracket A \rrbracket} \subseteq R_{\llbracket B \rrbracket}$ for a suitable identification of atom occurrences of $A$ and $B$ ensuring that we can consider the vertex sets $V_{\llbracket A \rrbracket}$ and $V_{\llbracket B \rrbracket}$ to be equal.

**Proposition 4.7.** $A \rightsquigarrow B \iff \frac{B}{A}$ in $BV_u$ defines a dicograph-monotone rewriting system.

*Proof.* This is a direct consequence of the easy direction (“if”) of Theorem 2.78. $\square$

<figure><img src="image_23.png" /></figure>

As discussed in Section 2.7, the rules of SBV are originally derived from a characterization of dicograph inclusion. Dicograph-monotonicity is therefore a fundamental aspect of the design of SBV, BV and their variants. We will discuss another example of this notion in Remark 4.12.

**Proposition 4.8.** Let $\rightsquigarrow$ be a dicograph-monotone relation and $\rightsquigarrow^*$ be its transitive closure. Then, for any $A \rightsquigarrow^* B$, there exists a path $A = C_1 \rightsquigarrow \dots \rightsquigarrow C_k = B$ with length $k = O(|A|^2)$.

*Proof.* Since $\equiv'$ is transitive by definition, if $C \rightsquigarrow D \rightsquigarrow E$ with $C \equiv' D \equiv' E$, then $C \rightsquigarrow E$ directly (by the assumption $\equiv' \subseteq \rightsquigarrow$). Thus, in the path of minimum length between $A$ and $B$, at least half of the rewrites $C_i \rightsquigarrow C_{i+1}$ satisfy $C_i \not\equiv' C_{i+1}$. Therefore, up to a factor of two (that gets absorbed in the $O(\cdot)$ notation), it suffices to bound the number of rewrites with $C_i \not\equiv' C_{i+1}$.

The definition of dicograph-monotonicity then gives us two cases. We claim that in both cases, $V_{\llbracket C_i \rrbracket}^2 \setminus R_{\llbracket C_i \rrbracket} \supsetneq V_{\llbracket C_{i+1} \rrbracket}^2 \setminus R_{\llbracket C_{i+1} \rrbracket}$. First, if $V_{\llbracket C_i \rrbracket} = V_{\llbracket C_{i+1} \rrbracket}$ and $R_{\llbracket C_i \rrbracket} \subseteq R_{\llbracket C_{i+1} \rrbracket}$, then this is immediate. Otherwise, $C_i$ is inferred from $C_{i+1}$ by an interaction rule, and then $\llbracket C_{i+1} \rrbracket$ can be identified with an induced subgraph of $\llbracket C_i \rrbracket$ with two fewer vertices, resulting in a strict inclusion between the complement graphs as we wanted.

Therefore, the natural number $|V_{\llbracket C_i \rrbracket}^2 \setminus R_{\llbracket C_i \rrbracket}|$ strictly decreases at each rewriting step such that $C_i \not\equiv' C_{i+1}$. So, starting from $A$, the number of such steps is bounded by $|V_{\llbracket A \rrbracket}^2 \setminus R_{\llbracket A \rrbracket}| = O(|A|^2)$. (We see that our definition of dicograph-monotonicity is slightly stronger than what we truly need from the point of view of complexity.) $\square$

<figure><img src="image_24.png" /></figure>
From this proposition, we immediately get:

**Corollary 4.9.** Any provable formula A in BVu has a proof of length $O(|A|^2)$ & size $O(|A|^3)$.

Here “size” refers to the complexity-theoretic notion of the number of bits it takes to write out the proof, hence the additional factor of $|A|$ accounting for the size of each intermediate formula in the derivation. Now that we know that we have short proofs, it remains to show that they can be checked efficiently.

**Proposition 4.10.** The validity of a proof in BVu can be checked in polynomial time. In other words, (our presentation of) BVu is a Cook–Reckhow proof system [CR79].

*Proof.* It suffices to show that the validity of each inference rule can be verified in polynomial time.

For instances of the $\equiv'$ rule, to check that $A \equiv' B$, one can apply a generic recipe for terms over associative and possibly commutative binary operators: compute hereditarily flattened and possibly sorted representations of A and B in polynomial time, and compare them, as sketched in the introduction of [Bas94] for example.

Let us now consider any other rule $r$ of BVu. There exist two formulas $A_r$ and $B_r$ such that the instances of these rules are precisely the inferences of the form

$$ \frac{S\{A_r[a_1 := C_1, \dots, a_k := C_k]\}}{S\{B_r[a_1 := C_1, \dots, a_k := C_k]\}} $$

where $S\{\cdot\}$ is a context, $\{a_1, \dots, a_k\}$ is the set of propositional variables that appear in either A or B (often both), and $[a_1 := C_1, \dots, a_k := C_k]$ denotes a parallel substitution of those variables by formulas. For instance, for $r = q_{2\downarrow}$, we may take $k = 2$, $A_{q_{2\downarrow}} = a_1 \triangleleft a_2$ and $B_{q_{2\downarrow}} = a_1 \triangleright a_2$.

Given two formulas A and B, our task is to decide in polynomial time whether one may infer B from A using the rule $r$. To do so, we first enumerate in polynomial time all the pairs $(S\{\cdot\}, A')$ such that $S\{A'\} = A$ (there are $O(|A|)$ many). For each of these pairs, we match $A'$ against the pattern $A_r$ in linear time; if this succeeds, we get a substitution such that $A_r[a_1 := C_1, \dots, a_k := C_k] = A'$. To conclude, we just have to test the equality $S\{B_r[a_1 := C_1, \dots, a_k := C_k]\} = B$. $\square$

**Remark 4.11.** In this proof, we have exploited the fact that the $\equiv'$ rules appear explicitly in our formal proofs. This differs from some traditional presentations of logics in the calculus of structures, which consider that the inference rules work over equivalence classes of formulas modulo $\equiv$ or $\equiv'$ (those classes are called *structures* in [Gug07]). In such a presentation with $\equiv'$ kept implicit, it is less obvious that proofs are still polynomial-time checkable.

Together, Proposition 4.9 and Proposition 4.10 tell us that BVu has polynomially bounded proofs that can be checked in polynomial time. This entails that provability is in NP. To extend the result from BVu to BV, note that for any formula A with units, there is a unit-free formula $A'$ such that $A \equiv A'$, which is computable from A in polynomial time, and then $\vdash_{BV} A \iff \vdash_{BVu} A'$.

**Remark 4.12.** Let us revisit Tiu’s result [Tiu06] on the incompleteness of “shallow systems” with respect to BV in the light of our complexity results. The main difference between shallow and deep inference is the lack of contextual closure of the rules in the former, i.e.

$$ \frac{B}{A} \iff r \frac{S\{B\}}{S\{A\}} $$
From this proposition, we immediately get:

**Corollary 4.9.** Any provable formula A in BVu has a proof of length $O(|A|^2)$ & size $O(|A|^3)$.

Here “size” refers to the complexity-theoretic notion of the number of bits it takes to write out the proof, hence the additional factor of $|A|$ accounting for the size of each intermediate formula in the derivation. Now that we know that we have short proofs, it remains to show that they can be checked efficiently.

**Proposition 4.10.** The validity of a proof in BVu can be checked in polynomial time. In other words, (our presentation of) BVu is a Cook–Reckhow proof system [CR79].

*Proof.* It suffices to show that the validity of each inference rule can be verified in polynomial time.

For instances of the $\equiv'$ rule, to check that $A \equiv' B$, one can apply a generic recipe for terms over associative and possibly commutative binary operators: compute hereditarily flattened and possibly sorted representations of A and B in polynomial time, and compare them, as sketched in the introduction of [Bas94] for example.

Let us now consider any other rule $r$ of BVu. There exist two formulas $A_r$ and $B_r$ such that the instances of these rules are precisely the inferences of the form

$$ \frac{S\{A_r[a_1 := C_1, \dots, a_k := C_k]\}}{S\{B_r[a_1 := C_1, \dots, a_k := C_k]\}} $$

where $S\{\cdot\}$ is a context, $\{a_1, \dots, a_k\}$ is the set of propositional variables that appear in either A or B (often both), and $[a_1 := C_1, \dots, a_k := C_k]$ denotes a parallel substitution of those variables by formulas. For instance, for $r = q_{2\downarrow}$, we may take $k = 2$, $A_{q_{2\downarrow}} = a_1 \triangleleft a_2$ and $B_{q_{2\downarrow}} = a_1 \triangleright a_2$.

Given two formulas A and B, our task is to decide in polynomial time whether one may infer B from A using the rule r. To do so, we first enumerate in polynomial time all the pairs $(S\{\cdot\}, A')$ such that $S\{A'\} = A$ (there are $O(|A|)$ many). For each of these pairs, we match $A'$ against the pattern $A_r$ in linear time; if this succeeds, we get a substitution such that $A_r[a_1 := C_1, \dots, a_k := C_k] = A'$. To conclude, we just have to test the equality $S\{B_r[a_1 := C_1, \dots, a_k := C_k]\} = B$. $\square$

**Remark 4.11.** In this proof, we have exploited the fact that the $\equiv'$ rules appear explicitly in our formal proofs. This differs from some traditional presentations of logics in the calculus of structures, which consider that the inference rules work over equivalence classes of formulas modulo $\equiv$ or $\equiv'$ (those classes are called *structures* in [Gug07]). In such a presentation with $\equiv'$ kept implicit, it is less obvious that proofs are still polynomial-time checkable.

Together, Proposition 4.9 and Proposition 4.10 tell us that BVu has polynomially bounded proofs that can be checked in polynomial time. This entails that provability is in NP. To extend the result from BVu to BV, note that for any formula A with units, there is a unit-free formula $A'$ such that $A \equiv A'$, which is computable from A in polynomial time, and then $\vdash_{BV} A \iff \vdash_{BVu} A'$.

**Remark 4.12.** Let us revisit Tiu's result [Tiu06] on the incompleteness of “shallow systems” with respect to BV in the light of our complexity results. The main difference between shallow and deep inference is the lack of contextual closure of the rules in the former, i.e.

$$ \frac{B}{A} \iff r \frac{S\{B\}}{S\{A\}} $$
One interpretation put forth for the results of [Tiu06] is that proof systems that can be translated into shallow systems, such as traditional sequent calculi, fail to capture BV and *pomset logic*<fnref n="15" /> because of the lack of deep inference.

We claim that in the case of pomset logic, there is an obstruction unrelated to the shallow vs deep distinction. Indeed, the definition for shallow systems in [Tiu06, §6] also enforces the condition that we called dicograph-monotonicity: observe that the relation $A \prec B$ given in [Tiu06, Definition 6.1] is equivalent to $R_{\llcorner A} \subset R_{\llcorner B}$. (Being able to state this is one reason for talking abstractly about rewriting systems instead of working directly in the calculus of structures.)

Therefore, by Proposition 4.8, any shallow system in this sense has polynomially bounded proofs; and if those proofs are also polynomial-time checkable then provability is in **NP**. Together with the result of the next section, this shows that these systems cannot capture pomset logic unless **NP** = **coNP**.

**4.3. Correctness of Pomset Logic Proof Nets is coNP-Complete.** As an intermediate step towards our eventual hardness result for provability in pomset logic, we first study the *correctness* problem: given a prenet (either tree-like or cographic), does it satisfy the correctness criterion, that is, is it an actual proof net? This can be seen as the special case of provability for *balanced* formulas, as we remarked before. Let us state our result right away.

**Theorem 4.13.** *The correctness problem for pomset logic proof nets is coNP-complete. More precisely, given a sequent $\Gamma$ and a pre-proof (or linking) $\ell$, it is coNP-complete to check the correctness of its cographic RB-prenet $\rho(\Gamma, \ell)$ or of its tree-like RB-prenet $\tau(\Gamma, \ell)$ (those two conditions being equivalent by Theorem 2.60).*

*Proof.* Let us show an equivalent reformulation: it is **NP**-complete to decide whether a pre-proof is *incorrect*. Membership in **NP** is immediate: one can build $\tau(\Gamma, \ell)$, whose *æ*-cycles provide witnesses for incorrectness by definition, in polynomial time; the size of those cycles is bounded by the number of vertices, and they can be checked in polynomial time. As for the proof of **NP**-hardness, it is done in two steps.

* We first show, via a polynomial time reduction, that incorrectness is as hard as finding *æ*-cycles in *arbitrary* RB-digraphs (Proposition 4.16 and Theorem 4.17).

* We then prove in the next subsection that the existence of *æ*-cycles for general RB-digraphs is **NP**-hard (Theorem 4.19). □

**Remark 4.14.** Assuming that $P \neq NP$, this refutes [Ret97a, Prop. 5] which claims that a “standard breadth search algorithm” can decide pomset proof net correctness in polynomial time. (The issue with this kind of argument is discussed in [Ngu20, §8.1].) This claim was meant to justify that “the proof net syntax is a sensible syntax by itself” [Ret97a, §3]: it is indeed part of the Cook-Reckhow definition of proof system [CR79], as already mentioned in Proposition 4.10, which says that the verification of BV derivations is in $P$.

We are now going to fill the steps outlined above to prove the **NP**-hardness part of Theorem 4.13. The reduction step extends the “proofification” construction from [Ngu20] that sends *undirected* perfect matchings to $MLL+mix$ pre-proof nets. For the sake of clarity,

<footnote n="15">¹⁵From [Tiu06, §1]: “We conjecture that [system BV and pomset logic] are actually the same logic. The result on the necessity of deep-inference of BV therefore explains to some extent the difficulty in the sequentialization of Pomset logic.”</footnote>
One interpretation put forth for the results of [Tiu06] is that proof systems that can be translated into shallow systems, such as traditional sequent calculi, fail to capture BV and *pomset logic*<fnref n="15" /> because of the lack of deep inference.

We claim that in the case of pomset logic, there is an obstruction unrelated to the shallow vs deep distinction. Indeed, the definition for shallow systems in [Tiu06, §6] also enforces the condition that we called dicograph-monotonicity: observe that the relation $A \prec B$ given in [Tiu06, Definition 6.1] is equivalent to $R_{\llcorner A} \subset R_{\llcorner B}$. (Being able to state this is one reason for talking abstractly about rewriting systems instead of working directly in the calculus of structures.)

Therefore, by Proposition 4.8, any shallow system in this sense has polynomially bounded proofs; and if those proofs are also polynomial-time checkable then provability is in **NP**. Together with the result of the next section, this shows that these systems cannot capture pomset logic unless **NP** = **coNP**.

**4.3. Correctness of Pomset Logic Proof Nets is coNP-Complete.** As an intermediate step towards our eventual hardness result for provability in pomset logic, we first study the *correctness* problem: given a prenet (either tree-like or cographic), does it satisfy the correctness criterion, that is, is it an actual proof net? This can be seen as the special case of provability for *balanced* formulas, as we remarked before. Let us state our result right away.

**Theorem 4.13.** *The correctness problem for pomset logic proof nets is coNP-complete. More precisely, given a sequent $\Gamma$ and a pre-proof (or linking) $\ell$, it is coNP-complete to check the correctness of its cographic RB-prenet $\rho(\Gamma, \ell)$ or of its tree-like RB-prenet $\tau(\Gamma, \ell)$ (those two conditions being equivalent by Theorem 2.60).*

*Proof.* Let us show an equivalent reformulation: it is **NP**-complete to decide whether a pre-proof is *incorrect*. Membership in **NP** is immediate: one can build $\tau(\Gamma, \ell)$, whose *æ*-cycles provide witnesses for incorrectness by definition, in polynomial time; the size of those cycles is bounded by the number of vertices, and they can be checked in polynomial time. As for the proof of **NP**-hardness, it is done in two steps.

* We first show, via a polynomial time reduction, that incorrectness is as hard as finding *æ*-cycles in *arbitrary* RB-digraphs (Proposition 4.16 and Theorem 4.17).

* We then prove in the next subsection that the existence of *æ*-cycles for general RB-digraphs is **NP**-hard (Theorem 4.19). □

**Remark 4.14.** Assuming that $P \neq NP$, this refutes [Ret97a, Prop. 5] which claims that a “standard breadth search algorithm” can decide pomset proof net correctness in polynomial time. (The issue with this kind of argument is discussed in [Ngu20, §8.1].) This claim was meant to justify that “the proof net syntax is a sensible syntax by itself” [Ret97a, §3]: it is indeed part of the Cook-Reckhow definition of proof system [CR79], as already mentioned in Proposition 4.10, which says that the verification of BV derivations is in $P$.

We are now going to fill the steps outlined above to prove the **NP**-hardness part of Theorem 4.13. The reduction step extends the “proofification” construction from [Ngu20] that sends *undirected* perfect matchings to $MLL+mix$ pre-proof nets. For the sake of clarity,

<footnote n="15">¹⁵From [Tiu06, §1]: “We conjecture that [system BV and pomset logic] are actually the same logic. The result on the necessity of deep-inference of BV therefore explains to some extent the difficulty in the sequentialization of Pomset logic.”</footnote>
we present our new reduction, with the same name, as a map from arbitrary RB-digraphs to balanced pomset logic sequents. Since the procedure makes arbitrary choices, the result is defined only up to atom renaming and modulo $≡$, but correctness and provability are indeed invariant for these equivalences.

The following definition (which is illustrated by Figure 11) makes use of the notation $R_G^⊗, R_G^<$, $R_G^{\ge}, R_G^{\le}$ introduced in Definition 2.13.

**Definition 4.15.** Let $\mathcal{G} = (V_G, R_G, B_G)$ be an RB-digraph. The proofification of $\mathcal{G}$, denoted by $\Pi(\mathcal{G})$, is the balanced (flat) sequent (defined only modulo $≡$ and variable renaming)

$$[C_{u_1} \otimes C_{v_1}, \dots, C_{u_m} \otimes C_{v_m}, D_{e_1}, \dots, D_{e_k}]$$

where:

* $\{(u_1, v_1), (v_1, u_1), \dots, (u_m, v_m), (v_m, u_m)\} = B_G$ and $\{e_1, \dots, e_k\} = R_G^<$, both of these being non-repeating enumerations;

* for $u \in V_G$, we let $C_u = a_{u,w_1} \succ \dots \succ a_{u,w_n}$ where $w_1, \dots, w_n$ is a non-repeating enumeration of the neighborhood of $u$, i.e. $\{(u, w_1), \dots, (u, w_n)\} = (\{u\} \times V_G) \cap (R_G^\otimes \cup R_G^<$ \cup R_G^{\ge})$, and
  - for each $\{u, v\} \subseteq V_G$ such that $(u, v) \in R_G^\otimes$ (equivalently, $(v, u) \in R_G^\otimes$), we give the names $a_{u,v}$ and $a_{v,u}$ to a fresh pair of dual atoms;

- for each $(u, v) \in R_G^<$ (equivalently, $(v, u) \in R_G^{\ge})$, we generate two fresh atoms $a_{u,v}$ and $a_{v,u}$ that are not dual;

* for $(u, v) \in R_G^<$, we let $D_{(u,v)} = a_{u,v}^\perp \triangleleft a_{v,u}^\perp$, using the above-defined atoms.

The ideas that were already present in [Ngu20, Section 3.2] are the use of *par* ($\succ$) to represent vertices, *tensor* ($\otimes$) for matching edges, and dual atoms for non-matching edges. The novelty here is how the *seq* ($\triangleleft$) connective of pomset logic serves to encode edge directions through the formulas $D_{(u,v)}$. It is immediate from the definition that:

**Proposition 4.16.** *Proofifications can be computed in polynomial time.*

Since a balanced sequent (or formula) uniquely defines a (tree-like or cographic) prenet, we can define the *correctness* of such a sequent (or formula), to be the correctness of the corresponding prenet.

**Theorem 4.17.** Let $\mathcal{G}$ be an RB-digraph and $\Pi(\mathcal{G})$ be its proofification. Then $\mathcal{G}$ admits an æ-cycle if and only if $\Pi(\mathcal{G})$ is incorrect.

*Proof.* By slightly adapting the reasoning found in [Ngu20, Proposition 3.9], one could show that the the æ-cycles in $\mathcal{G}$ are in bijection with those in the tree-like RB-prenet of $\Pi(\mathcal{G})$, and the theorem statement would then follow immediately. However, we find it more convenient here to work with the cographic RB-prenet $\llbracket\Pi(\mathcal{G})\rrbracket = \rho(\Pi(\mathcal{G}), \ell(\Pi(\mathcal{G})))$ (see Figure 11 for an example).

First, by unfolding the definitions, one can write the set of non-matching edges of $\llbracket\Pi(\mathcal{G})\rrbracket$ as the disjoint union $R_1 \cup R_2$ where

$$R_1 = \{(a_{u,v}, a_{x,y}) \mid (u, x) \in B_G \wedge (u, v), (x, y) \in R_G^\otimes \cup R_G^< \cup R_G^{\ge}\}$$

$$R_2 = \{(a_{u,v}^\perp, a_{v,u}^\perp) \mid (u, v) \in R_G \wedge (v, u) \notin R_G\}$$

Next, suppose that there exists an æ-cycle $u_0, \dots, u_{n-1}, u_n = u_0$ in $\mathcal{G}$, assuming without loss of generality that $(u_i, u_{i+1}) \in B_G$ when $i$ is even and $(u_i, u_{i+1}) \in R_G$ when $i$ is odd. Let us write $a[u, v] = a_{u,v}$ for readability. The aforementioned æ-cycle can be turned into the
we present our new reduction, with the same name, as a map from arbitrary RB-digraphs to balanced pomset logic sequents. Since the procedure makes arbitrary choices, the result is defined only up to atom renaming and modulo $≡$, but correctness and provability are indeed invariant for these equivalences.

The following definition (which is illustrated by Figure 11) makes use of the notation $R_G^⊗, R_G^<$, $R_G^{\triangleright}, R_G^{\triangleleft}$ introduced in Definition 2.13.

**Definition 4.15.** Let $\mathcal{G} = (V_G, R_G, B_G)$ be an RB-digraph. The proofification of $\mathcal{G}$, denoted by $\Pi(\mathcal{G})$, is the balanced (flat) sequent (defined only modulo $≡$ and variable renaming)

$$[C_{u_1} \otimes C_{v_1}, \dots, C_{u_m} \otimes C_{v_m}, D_{e_1}, \dots, D_{e_k}]$$

where:

* $\{(u_1, v_1), (v_1, u_1), \dots, (u_m, v_m), (v_m, u_m)\} = B_G$ and $\{e_1, \dots, e_k\} = R_G^<$, both of these being non-repeating enumerations;

* for $u \in V_G$, we let $C_u = a_{u,w_1} \succ \dots \succ a_{u,w_n}$ where $w_1, \dots, w_n$ is a non-repeating enumeration of the neighborhood of $u$, i.e. $\{(u, w_1), \dots, (u, w_n)\} = (\{u\} \times V_G) \cap (R_G^\otimes \cup R_G^<$ \cup R_G^{\triangleright})$, and
  - for each $\{u, v\} \subseteq V_G$ such that $(u, v) \in R_G^\otimes$ (equivalently, $(v, u) \in R_G^\otimes$), we give the names $a_{u,v}$ and $a_{v,u}$ to a fresh pair of dual atoms;

- for each $(u, v) \in R_G^<$ (equivalently, $(v, u) \in R_G^{\triangleright})$, we generate two fresh atoms $a_{u,v}$ and $a_{v,u}$ that are not dual;

* for $(u, v) \in R_G^<$, we let $D_{(u,v)} = a_{u,v}^\perp \triangleleft a_{v,u}^\perp$, using the above-defined atoms.

The ideas that were already present in [Ngu20, Section 3.2] are the use of *par* ($\succ$) to represent vertices, *tensor* ($\otimes$) for matching edges, and dual atoms for non-matching edges. The novelty here is how the *seq* ($\triangleleft$) connective of pomset logic serves to encode edge directions through the formulas $D_{(u,v)}$. It is immediate from the definition that:

**Proposition 4.16.** *Proofifications can be computed in polynomial time.*

Since a balanced sequent (or formula) uniquely defines a (tree-like or cographic) prenet, we can define the *correctness* of such a sequent (or formula), to be the correctness of the corresponding prenet.

**Theorem 4.17.** Let $\mathcal{G}$ be an RB-digraph and $\Pi(\mathcal{G})$ be its proofification. Then $\mathcal{G}$ admits an æ-cycle if and only if $\Pi(\mathcal{G})$ is incorrect.

*Proof.* By slightly adapting the reasoning found in [Ngu20, Proposition 3.9], one could show that the the æ-cycles in $\mathcal{G}$ are in bijection with those in the tree-like RB-prenet of $\Pi(\mathcal{G})$, and the theorem statement would then follow immediately. However, we find it more convenient here to work with the cographic RB-prenet $\llbracket\Pi(\mathcal{G})\rrbracket = \rho(\Pi(\mathcal{G}), \ell(\Pi(\mathcal{G})))$ (see Figure 11 for an example).

First, by unfolding the definitions, one can write the set of non-matching edges of $\llbracket\Pi(\mathcal{G})\rrbracket$ as the disjoint union $R_1 \cup R_2$ where

$$R_1 = \{(a_{u,v}, a_{x,y}) \mid (u, x) \in B_G \wedge (u, v), (x, y) \in R_G^\otimes \cup R_G^< \cup R_G^{\triangleright}\}$$

$$R_2 = \{(a_{u,v}^\perp, a_{v,u}^\perp) \mid (u, v) \in R_G \wedge (v, u) \notin R_G\}$$

Next, suppose that there exists an æ-cycle $u_0, \dots, u_{n-1}, u_n = u_0$ in $\mathcal{G}$, assuming without loss of generality that $(u_i, u_{i+1}) \in B_G$ when $i$ is even and $(u_i, u_{i+1}) \in R_G$ when $i$ is odd. Let us write $a[u, v] = a_{u,v}$ for readability. The aforementioned æ-cycle can be turned into the
<figure><img src="image_25.png" /><figcaption>FIGURE 11. An RB-digraph (left) and its proofification (below) together with the corresponding cographic RB-prenet (right). Note that $a_{w,x}$ and $a_{x,w}$ are defined to be dual atoms.</figcaption></figure>

following cycle in $\langle\langle\Pi(\mathcal{G})\rangle\rangle$, where $\to$ denotes a non-matching edge and $\Rightarrow$ denotes either a matching edge or an æ-path of length 3 starting and ending with matching edges:

$$a[u_0, u_{n-1}] \to a[u_1, u_2] \Rightarrow a[u_2, u_1] \to a[u_3, u_4] \Rightarrow \dots \to a[u_{n-1}, u_0] \Rightarrow a[u_0, u_{n-1}]$$

The fact that it is an æ-cycle is immediate. To show that $(\Pi(\mathcal{G}), \ell(\Pi(\mathcal{G})))$ is incorrect, we must also check that it is chordless, that is, we must rule out the possibility that any edge in $R_1 \cup R_2$ is a chord.

* Let $e = (a_{u,v}, a_{x,y}) \in R_1$, which means that $(u, x) \in B_G$. Suppose that $a_{u,v}$ is part of the cycle in $\langle\langle\Pi(\mathcal{G})\rangle\rangle$ (otherwise, $e$ is not a chord). Then $u$ is part of the original cycle in $\mathcal{G}$, i.e. $u = u_i$ for some $i \in \{0, \dots, n-1\}$. Since the cycle is $\mathcal{G}$ is alternating, $x = u_{i-1}$ or $x = u_{i+1}$ (with indexing modulo $n$) depending on the parity of $i$, and since it is elementary, this is the only time $x$ is visited. So there exists a unique $z \in V_G$ such that $a_{x,z}$ belongs to the cycle in $\langle\langle\Pi(\mathcal{G})\rangle\rangle$. We then have either $(a_{x,z}, a_{u,v}) \in R_1$ or $(a_{u,v}, a_{x,z}) \in R_1$. A case analysis depending on whether $z = y$ then shows that $e$ cannot be a chord.

* The endpoints of edges in $R_2$ are not incident to any other non-matching edges, so $R_2$ cannot provide any chord.

Conversely, one can show that any æ-cycle in $\langle\langle\Pi(\mathcal{G})\rangle\rangle$ induces in a canonical way an alternating cycle in $\mathcal{G}$, and if one starts from a chordless æ-cycle, then the resulting cycle is elementary. $\square$

Before moving to the last missing ingredient for the proof of Theorem 4.13, let us draw a connection with some previous material in this paper.
<figure><img src="image_25.png" /><figcaption>FIGURE 11. An RB-digraph (left) and its proofification (below) together with the corresponding cographic RB-prenet (right). Note that $a_{w,x}$ and $a_{x,w}$ are defined to be dual atoms.</figcaption></figure>

following cycle in $([\Pi(\mathcal{G})])$, where $\rightarrow$ denotes a non-matching edge and $\Rightarrow$ denotes either a matching edge or an æ-path of length 3 starting and ending with matching edges:

$$a[u_0, u_{n-1}] \rightarrow a[u_1, u_2] \Rightarrow a[u_2, u_1] \rightarrow a[u_3, u_4] \Rightarrow \dots \rightarrow a[u_{n-1}, u_0] \Rightarrow a[u_0, u_{n-1}]$$

The fact that it is an æ-cycle is immediate. To show that $(\Pi(\mathcal{G}), \ell(\Pi(\mathcal{G})))$ is incorrect, we must also check that it is chordless, that is, we must rule out the possibility that any edge in $R_1 \cup R_2$ is a chord.

* Let $e = (a_{u,v}, a_{x,y}) \in R_1$, which means that $(u, x) \in B_G$. Suppose that $a_{u,v}$ is part of the cycle in $([\Pi(\mathcal{G})])$ (otherwise, $e$ is not a chord). Then $u$ is part of the original cycle in $\mathcal{G}$, i.e. $u = u_i$ for some $i \in \{0, \dots, n-1\}$. Since the cycle is $\mathcal{G}$ is alternating, $x = u_{i-1}$ or $x = u_{i+1}$ (with indexing modulo $n$) depending on the parity of $i$, and since it is elementary, this is the only time $x$ is visited. So there exists a unique $z \in V_G$ such that $a_{x,z}$ belongs to the cycle in $([\Pi(\mathcal{G})])$. We then have either $(a_{x,z}, a_{u,v}) \in R_1$ or $(a_{u,v}, a_{x,z}) \in R_1$. A case analysis depending on whether $z = y$ then shows that $e$ cannot be a chord.

* The endpoints of edges in $R_2$ are not incident to any other non-matching edges, so $R_2$ cannot provide any chord.

Conversely, one can show that any æ-cycle in $([\Pi(\mathcal{G})])$ induces in a canonical way an alternating cycle in $\mathcal{G}$, and if one starts from a chordless æ-cycle, then the resulting cycle is elementary. $\square$

Before moving to the last missing ingredient for the proof of Theorem 4.13, let us draw a connection with some previous material in this paper.
**Example 4.18.** Consider the digraph with perfect matching on the right of Figure 9. Since it has no æ-cycle, its proofification below is a provable formula in pomset logic.

$$ [[a \rightleftharpoons b] \otimes [c \rightleftharpoons d], [e \rightleftharpoons f] \otimes [g \rightleftharpoons h], a^{\perp} \triangleleft h^{\perp}, e^{\perp} \triangleleft b^{\perp}, c^{\perp} \triangleleft f^{\perp}, g^{\perp} \triangleleft d^{\perp}] $$

This is very close to the counterexample presented in Section 3.2. In fact, we have already seen an abridged drawing for the corresponding proof net in that section, in Figure 10c. In general, our complexity results imply that unless **NP** = **coNP**, there must exist some proofification that is provable in pomset logic but not in BV, and this provides an explicit example. Furthermore, if we forget the edge directions in this graph (right of Figure 9) and then take its proofification, we get the “linear medial” of Remark 3.15 / Figure 10a.

**4.4. Finding Alternating Elementary Cycles is NP-Hard.** The technical heart of our proof of coNP-hardness for pomset proof net correctness is:

**Theorem 4.19. Deciding the existence of æ-cycles in RB-digraphs is NP-hard.**

We shall prove this by a many-one polynomial time reduction from the CNF-SAT problem described in Section 4.1. A more concise proof would have been possible by relying on a result on edge-colored digraphs [GLMM13, Theorem 5] (this is actually how we discovered the theorem, and this proof can be found in [Ngu19]). Nevertheless, our direct reduction, which is heavily inspired by<fnref n="16" /> [GLMM13], has two advantages: it shortens the chain of dependencies, and lends itself to being adapted into the $\Sigma_2^P$-hardness proof<fnref n="17" /> of our next subsection.

**In a nutshell.** Let us first give a rough idea of the proof, illustrated by figures on the CNF-SAT instance $(x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$.

We first build a digraph $G_{cl}$ (Figure 12a) with two distinguished vertices $s$ and $t$ such that paths from $s$ to $t$ are in bijection with choices of one literal per clause. To make this work, the graph contains one vertex for each literal occurrence.

Next, we build on the same set of vertices a digraph $G_{var}$ (Figure 12b) such that paths from $t$ to $s$ correspond bijectively to variable assignments in the following way: the path traverses all the literal occurrences set to false. The point is that if we manage to go from $s$ to $t$ with a path in $G_{cl}$, and then go back from $t$ to $s$ with a path in $G_{var}$ avoiding all vertices that were already visited, then the first path will only select literals set to true by the second path. This means that cycles visiting both $s$ and $t$ yield satisfying assignments and vice versa.

Finally, the tricky part is to reduce finding such a cycle with two prescribed vertices to finding an æ-cycle in an RB-digraph. This is done by a generic construction (Figure 13) that morally “superimposes” in some way these two graphs $G_{cl}$ and $G_{var}$. It requires a few additional conditions, among which the acyclicity of both $G_{cl}$ and $G_{var}$.

<footnote n="16">¹⁶One step in the proof of [GLMM13, Theorem 5] consists of adding edge directions to a reduction from digraphs to undirected 2-edge-colored graphs (called Häggkvist's transformation); morally, our reduction replaces this with a well-known correspondence between digraphs and undirected RB-graphs (something of this kind is implicit, for instance, in the use of the classical Ford-Fulkerson maximum flow algorithm to compute a maximum matching).</footnote>

<footnote n="17">¹⁷This is why we use a reduction from CNF-SAT, whereas the proof of [GLMM13, Theorem 5] consists of a reduction between two graph-theoretic problems—no Boolean formulas are mentioned anywhere in [GLMM13].</footnote>
**Example 4.18.** Consider the digraph with perfect matching on the right of Figure 9. Since it has no æ-cycle, its proofification below is a provable formula in pomset logic.

$$[[a \rightleftharpoons b] \otimes [c \rightleftharpoons d], [e \rightleftharpoons f] \otimes [g \rightleftharpoons h], a^{\perp} \triangleleft h^{\perp}, e^{\perp} \triangleleft b^{\perp}, c^{\perp} \triangleleft f^{\perp}, g^{\perp} \triangleleft d^{\perp}]$$

This is very close to the counterexample presented in Section 3.2. In fact, we have already seen an abridged drawing for the corresponding proof net in that section, in Figure 10c. In general, our complexity results imply that unless **NP** = **coNP**, there must exist some proofification that is provable in pomset logic but not in BV, and this provides an explicit example. Furthermore, if we forget the edge directions in this graph (right of Figure 9) and then take its proofification, we get the “linear medial” of Remark 3.15 / Figure 10a.

**4.4. Finding Alternating Elementary Cycles is NP-Hard.** The technical heart of our proof of coNP-hardness for pomset proof net correctness is:

**Theorem 4.19.** Deciding the existence of æ-cycles in RB-digraphs is NP-hard.

We shall prove this by a many-one polynomial time reduction from the CNF-SAT problem described in Section 4.1. A more concise proof would have been possible by relying on a result on edge-colored digraphs [GLMM13, Theorem 5] (this is actually how we discovered the theorem, and this proof can be found in [Ngu19]). Nevertheless, our direct reduction, which is heavily inspired by<fnref n="16" /> [GLMM13], has two advantages: it shortens the chain of dependencies, and lends itself to being adapted into the $\Sigma_2^P$-hardness proof<fnref n="17" /> of our next subsection.

**In a nutshell.** Let us first give a rough idea of the proof, illustrated by figures on the CNF-SAT instance $(x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$.

We first build a digraph $G_{cl}$ (Figure 12a) with two distinguished vertices $s$ and $t$ such that paths from $s$ to $t$ are in bijection with choices of one literal per clause. To make this work, the graph contains one vertex for each literal occurrence.

Next, we build on the same set of vertices a digraph $G_{var}$ (Figure 12b) such that paths from $t$ to $s$ correspond bijectively to variable assignments in the following way: the path traverses all the literal occurrences set to false. The point is that if we manage to go from $s$ to $t$ with a path in $G_{cl}$, and then go back from $t$ to $s$ with a path in $G_{var}$ avoiding all vertices that were already visited, then the first path will only select literals set to true by the second path. This means that cycles visiting both $s$ and $t$ yield satisfying assignments and vice versa.

Finally, the tricky part is to reduce finding such a cycle with two prescribed vertices to finding an æ-cycle in an RB-digraph. This is done by a generic construction (Figure 13) that morally “superimposes” in some way these two graphs $G_{cl}$ and $G_{var}$. It requires a few additional conditions, among which the acyclicity of both $G_{cl}$ and $G_{var}$.

<footnote n="16">¹⁶One step in the proof of [GLMM13, Theorem 5] consists of adding edge directions to a reduction from digraphs to undirected 2-edge-colored graphs (called Häggkvist's transformation); morally, our reduction replaces this with a well-known correspondence between digraphs and undirected RB-graphs (something of this kind is implicit, for instance, in the use of the classical Ford-Fulkerson maximum flow algorithm to compute a maximum matching).</footnote>

<footnote n="17">¹⁷This is why we use a reduction from CNF-SAT, whereas the proof of [GLMM13, Theorem 5] consists of a reduction between two graph-theoretic problems—no Boolean formulas are mentioned anywhere in [GLMM13].</footnote>
<figure><img src="image_26.png" /><figcaption>FIGURE 12. The reduction for the proof of Theorem 4.19 on the CNF ($x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$. The thick colored paths correspond: in $\mathcal{G}_{\text{cl}}$ (left), to selecting the literals $z, \neg x, \neg y$ in the successive clauses; in $\mathcal{G}_{\text{var}}$ (right), to the assignment $x = \text{false}, y = \text{false}, z = \text{true}$ which makes the selected literals true. Observe that the two paths do not share any intermediate vertex. It is also worth paying attention to the horizontal edge for $y$ on the right, that showcases how to handle multiple occurrences of a literal set to $\text{false}$.</figcaption></figure>

**Proof details.** For the remainder of this subsection, we fix an instance of CNF-SAT, presented formally as in Section 4.1: it is a finite ordered set of clauses $\{C_1, \dots, C_n\}$; each clause is a finite ordered set of literals $C_i = \{l_{i,1}, \dots, l_{i,m(i)}\}$; finally, each literal is either $x$ or $\neg x$ for some variable $x \in X = \{x_1, \dots, x_p\}$. Given this instance, we consider a set of vertices $V_{\text{occ}} = \{v_{i,j} \mid (i,j) \in I\}$ with one vertex for each literal occurrence (thus, $I = \{(i,j) \in \mathbb{N}^2 \mid 1 \le i \le n, 1 \le j \le m(i)\}$), plus two auxiliary vertices $s$ and $t$ (outside the set $V_{\text{occ}}$).

Recall that a digraph is said to be *acyclic* when it contains no cycles. An observation to keep in mind for the three following lemmas is that a path in an acyclic digraph is always elementary.

**Lemma 4.20** (see Figure 12a). *From the given CNF-SAT instance, one can build in polynomial time a directed graph $\mathcal{G}_{\text{cl}} = (V_{\text{occ}} \cup \{s, t\}, E_{\text{cl}})$ such that:*

* $\mathcal{G}_{\text{cl}}$ is acyclic, $s$ has no incoming edges and $t$ has no outgoing edges;

* each path from $s$ to $t$ in $\mathcal{G}_{\text{cl}}$ visits exactly the intermediate vertices $\{v_{i,j[i]} \mid 1 \le i \le n\}$ for some $j[1], \dots, j[n]$ with $1 \le j[i] \le m(i)$;

* conversely, every such choice of one literal per clause induces a unique path from $s$ to $t$, visiting exactly the corresponding vertices.
<figure><img src="image_26.png" /><figcaption>FIGURE 12. The reduction for the proof of Theorem 4.19 on the CNF ($x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$. The thick colored paths correspond: in $\mathcal{G}_{\text{cl}}$ (left), to selecting the literals $z, \neg x, \neg y$ in the successive clauses; in $\mathcal{G}_{\text{var}}$ (right), to the assignment $x = \text{false}, y = \text{false}, z = \text{true}$ which makes the selected literals true. Observe that the two paths do not share any intermediate vertex. It is also worth paying attention to the horizontal edge for $y$ on the right, that showcases how to handle multiple occurrences of a literal set to $\text{false}$.</figcaption></figure>

**Proof details.** For the remainder of this subsection, we fix an instance of CNF-SAT, presented formally as in Section 4.1: it is a finite ordered set of clauses $\{C_1, \dots, C_n\}$; each clause is a finite ordered set of literals $C_i = \{l_{i,1}, \dots, l_{i,m(i)}\}$; finally, each literal is either $x$ or $\neg x$ for some variable $x \in X = \{x_1, \dots, x_p\}$. Given this instance, we consider a set of vertices $V_{\text{occ}} = \{v_{i,j} \mid (i,j) \in I\}$ with one vertex for each literal occurrence (thus, $I = \{(i,j) \in \mathbb{N}^2 \mid 1 \le i \le n, 1 \le j \le m(i)\}$), plus two auxiliary vertices $s$ and $t$ (outside the set $V_{\text{occ}}$).

Recall that a digraph is said to be *acyclic* when it contains no cycles. An observation to keep in mind for the three following lemmas is that a path in an acyclic digraph is always elementary.

**Lemma 4.20** (see Figure 12a). *From the given CNF-SAT instance, one can build in polynomial time a directed graph $\mathcal{G}_{\text{cl}} = (V_{\text{occ}} \cup \{s, t\}, E_{\text{cl}})$ such that:*

* $\mathcal{G}_{\text{cl}}$ is acyclic, $s$ has no incoming edges and $t$ has no outgoing edges;

* each path from $s$ to $t$ in $\mathcal{G}_{\text{cl}}$ visits exactly the intermediate vertices $\{v_{i,j[i]} \mid 1 \le i \le n\}$ for some $j[1], \dots, j[n]$ with $1 \le j[i] \le m(i)$;

* conversely, every such choice of one literal per clause induces a unique path from $s$ to $t$, visiting exactly the corresponding vertices.
*Proof.* As illustrated in Figure 12a, we take:

$$E_{\text{cl}} = \{(s, v_{1,j}) \mid j \in \{1, \dots, m(1)\}\} \\ \cup \{(v_{i,j}, v_{i+1,j'}) \mid i \in \{1, \dots, n-1\}, j \in \{1, \dots, m(i)\}, j' \in \{1, \dots, m(i+1)\}\} \\ \cup \{(v_{n,j}, t) \mid j \in \{1, \dots, m(n)\}\}$$

It is straightforward to check that the required properties hold. For instance, the absence of cycles in $\mathcal{G}_{\text{cl}}$ is a consequence of the following fact: for all $(v_{i,j}, v_{i',j'}) \in E_{\text{cl}}$ we have $i < i'$. $\square$

**Lemma 4.21** (see Figure 12b). *From the given CNF-SAT instance, assuming without loss of generality that each variable has at least one positive and one negative occurrence (see Remark 4.4), one can build in polynomial time a digraph $\mathcal{G}_{\text{var}}$ such that:*

* $\mathcal{G}_{\text{var}} = (V_{\text{occ}} \cup \{s, t\}, E_{\text{var}})$ is acyclic, $t$ has no incoming edges and $s$ has no outgoing edges (note that the roles of $t$ and $s$ are reversed compared to $\mathcal{G}_{\text{cl}}$);

* for each path from $t$ to $s$, the set of intermediate vertices in $\mathcal{G}_{\text{var}}$ that it visits is of the form $\{v_{i,j} \mid (i, j) \in I, l_{i,j} \in \{\neg x \mid x \in Y\} \cup (X \setminus Y)\}$ for a unique set of variables $Y \subseteq X$;

* conversely, every such subset of variables corresponds to a (unique) path from $t$ to $s$.

One should see such a $Y \subseteq X$ above as an assignment $\chi_Y : X \to \{\text{true}, \text{false}\}$, with $Y = \chi_Y^{-1}(\{\text{true}\})$. So the vertices traversed correspond to the literals set to false.

*Proof.* Let us first describe what the paths starting from $t$ will look like once we have defined the digraph. First, we have to choose $l_1 \in \{x_1, \neg x_1\}$ and go to its first occurrence (first for the order induced by the clauses). Then as long as we are on an occurrence of $l_1$ which is not the last one, there is a single outgoing edge, and it leads to the next occurrence. Finally, once the last occurrence of $l_1$ is reached, we may go to the first occurrence of $l_2$ for some choice $l_2 \in \{x_2, \neg x_2\}$. And so on, until the last occurrence of either $x_p$ or $\neg x_p$ which finally allows us to arrive at $s$.

To enforce this, we define $E_{\text{var}}$ (as shown in Figure 12b) to consist of all the edges:

* $(v_{i,j}, v_{i',j'})$ such that $l_{i,j} = l_{i',j'} = l$ and the occurrence of $l$ in $C_{i'}$ is the successor of its occurrence in $C_i$, i.e. $i < i'$ and $i < i'' < i'$ $\implies$ $l \notin C_{i''}$;

* $(v_{i,j}, v_{i',j'})$ such that for some $(l_{i,j}, l_{i',j'}) \in \bigcup_{1 \le k \le p-1} (\{x_k, \neg x_k\} \times \{x_{k+1}, \neg x_{k+1}\})$, $C_i$ is the last clause containing a literal equal to $l_{i,j}$ while $C_{i'}$ is the first clause containing $l_{i',j'}$;

* $(t, v_{i,j})$ and $(t, v_{i',j'})$, where $l_{i,j} = x_1$, $l_{i',j'} = \neg x_1$ and $C_i, C_{i'}$ are the first clauses in which those literals appear respectively;

* $(v_{i,j}, s)$ and $(v_{i',j'}, s)$ for the last occurrences $l_{i,j}, l_{i',j'}$ of $x_p, \neg x_p$. $\square$

**Lemma 4.22** (see Figure 13). Let $\mathcal{G}_1 = (V, E_1)$ and $\mathcal{G}_2 = (V, E_2)$ be two directed graphs with the same vertex set $V$. Let $s, t \in V$. Assume that $\mathcal{G}_1$ and $\mathcal{G}_2$ are acyclic and that $s$ (resp. $t$) has no incoming edge in $\mathcal{G}_1$ (resp. $\mathcal{G}_2$) and no outgoing edge in $\mathcal{G}_2$ (resp. $\mathcal{G}_1$). Then one can build in polynomial time an RB-digraph $\mathcal{H}$ whose $\omega$-cycles are in bijection with the pairs $(P_1, P_2)$ where:

* $P_1$ is a path from $s$ to $t$ in $\mathcal{G}_1$;

* $P_2$ is a path from $t$ to $s$ in $\mathcal{G}_2$;

* $P_1 \setminus \{s, t\}$ and $P_2 \setminus \{s, t\}$ are vertex-disjoint.

*Proof.* Our construction of $\mathcal{H} = (V_{\mathcal{H}}, R_{\mathcal{H}}, B_{\mathcal{H}})$ associates to each original vertex a $B$-edge:

$$V_{\mathcal{H}} = \{s_1, s_2, t_1, t_2\} \cup \{v^p \mid v \in V, p \in \{\oplus, \ominus\}\} \quad \text{where } V' = V \setminus \{s, t\}$$

$$B_{\mathcal{H}} = \{(s_1, s_2), (s_2, s_1), (t_1, t_2), (t_2, t_1)\} \cup \{(v^p, v^q) \mid v \in V, (p, q) \in \{(\oplus, \ominus), (\ominus, \oplus)\}\}$$
*Proof.* As illustrated in Figure 12a, we take:

$$ 
\begin{aligned}
E_{\text{cl}} = & \{(s, v_{1,j}) \mid j \in \{1, \dots, m(1)\}\} \\
& \cup \{(v_{i,j}, v_{i+1,j'}) \mid i \in \{1, \dots, n-1\}, j \in \{1, \dots, m(i)\}, j' \in \{1, \dots, m(i+1)\}\} \\
& \cup \{(v_{n,j}, t) \mid j \in \{1, \dots, m(n)\}\}
\end{aligned}
$$

It is straightforward to check that the required properties hold. For instance, the absence of cycles in $G_{\text{cl}}$ is a consequence of the following fact: for all $(v_{i,j}, v_{i',j'}) \in E_{\text{cl}}$ we have $i < i'$. $\square$

**Lemma 4.21** (see Figure 12b). *From the given CNF-SAT instance, assuming without loss of generality that each variable has at least one positive and one negative occurrence (see Remark 4.4), one can build in polynomial time a digraph $G_{\text{var}}$ such that:*

* $G_{\text{var}} = (V_{\text{occ}} \cup \{s, t\}, E_{\text{var}})$ is acyclic, $t$ has no incoming edges and $s$ has no outgoing edges (note that the roles of $t$ and $s$ are reversed compared to $G_{\text{cl}}$);

* for each path from $t$ to $s$, the set of intermediate vertices in $G_{\text{var}}$ that it visits is of the form $\{v_{i,j} \mid (i,j) \in I, l_{i,j} \in \{\neg x \mid x \in Y\} \cup (X \setminus Y)\}$ for a unique set of variables $Y \subseteq X$;

* conversely, every such subset of variables corresponds to a (unique) path from $t$ to $s$.

One should see such a $Y \subseteq X$ above as an assignment $\chi_Y : X \to \{\text{true}, \text{false}\}$, with $Y = \chi_Y^{-1}(\{\text{true}\})$. So the vertices traversed correspond to the literals set to false.

*Proof.* Let us first describe what the paths starting from $t$ will look like once we have defined the digraph. First, we have to choose $l_1 \in \{x_1, \neg x_1\}$ and go to its first occurrence (first for the order induced by the clauses). Then as long as we are on an occurrence of $l_1$ which is not the last one, there is a single outgoing edge, and it leads to the next occurrence. Finally, once the last occurrence of $l_1$ is reached, we may go to the first occurrence of $l_2$ for some choice $l_2 \in \{x_2, \neg x_2\}$. And so on, until the last occurrence of either $x_p$ or $\neg x_p$ which finally allows us to arrive at $s$.

To enforce this, we define $E_{\text{var}}$ (as shown in Figure 12b) to consist of all the edges:

* $(v_{i,j}, v_{i',j'})$ such that $l_{i,j} = l_{i',j'} = l$ and the occurrence of $l$ in $C_{i'}$ is the successor of its occurrence in $C_i$, i.e. $i < i'$ and $i < i'' < i'$ $\implies$ $l \notin C_{i''}$;

* $(v_{i,j}, v_{i',j'})$ such that for some $(l_{i,j}, l_{i',j'}) \in \bigcup_{1 \le k \le p-1} (\{x_k, \neg x_k\} \times \{x_{k+1}, \neg x_{k+1}\})$, $C_i$ is the last clause containing a literal equal to $l_{i,j}$ while $C_{i'}$ is the first clause containing $l_{i',j'}$;

* $(t, v_{i,j})$ and $(t, v_{i',j'})$, where $l_{i,j} = x_1$, $l_{i',j'} = \neg x_1$ and $C_i, C_{i'}$ are the first clauses in which those literals appear respectively;

* $(v_{i,j}, s)$ and $(v_{i',j'}, s)$ for the last occurrences $l_{i,j}, l_{i',j'}$ of $x_p, \neg x_p$. $\square$

**Lemma 4.22** (see Figure 13). Let $G_1 = (V, E_1)$ and $G_2 = (V, E_2)$ be two directed graphs with the same vertex set $V$. Let $s, t \in V$. Assume that $G_1$ and $G_2$ are acyclic and that $s$ (resp. $t$) has no incoming edge in $G_1$ (resp. $G_2$) and no outgoing edge in $G_2$ (resp. $G_1$). Then one can build in polynomial time an RB-digraph $H$ whose $\omega$-cycles are in bijection with the pairs $(P_1, P_2)$ where:

* $P_1$ is a path from $s$ to $t$ in $G_1$;

* $P_2$ is a path from $t$ to $s$ in $G_2$;

* $P_1 \setminus \{s, t\}$ and $P_2 \setminus \{s, t\}$ are vertex-disjoint.

*Proof.* Our construction of $H = (V_H, R_H, B_H)$ associates to each original vertex a $B$-edge:

$$ V_H = \{s_1, s_2, t_1, t_2\} \cup \{v^p \mid v \in V, p \in \{\oplus, \ominus\}\} \quad \text{where} \quad V' = V \setminus \{s, t\} $$

$$ B_H = \{(s_1, s_2), (s_2, s_1), (t_1, t_2), (t_2, t_1)\} \cup \{(v^p, v^q) \mid v \in V, (p, q) \in \{(\oplus, \ominus), (\ominus, \oplus)\}\} $$
<figure><img src="image_27.png" /><figcaption>FIGURE 13. Example for the proof of Lemma 4.22. On the left, two digraphs are drawn on the same vertices. On the right, the RB-digraph obtained by applying the construction of Lemma 4.22 with the distinguished vertices $s$ and $t$. (We do not reuse the graphs in Figure 12 because the drawing of their “superposition” would be unreadable.) The pair of paths ($s \to u \to v \to t$, $t \to w \to s$) on the left corresponds to an æ-cycle on the right, whereas the “short-circuit” ($s \to u \to w$, $w \to s$) – which we want to exclude – corresponds to a cycle that is not alternating (the consecutive edges $u^{\ominus} \to w^{\oplus} \to s_2$ are both outside the matching).</figcaption></figure>

The non-matching edges are obtained from the original edges: writing $E_i$ for the set of edges of $G_i$ (for $i \in \{1, 2\}$), we take $R_H = R'_1 \cup R'_2$ where

$$R'_1 = \{(s_1, v^{\oplus}) \mid v \in V' \text{ such that } (s, v) \in E_1\} \cup \{(u^{\ominus}, t_1) \mid u \in V' \text{ such that } (u, t) \in E_1\} \\ \cup \{(u^{\ominus}, v^{\oplus}) \mid u, v \in V' \text{ such that } (u, v) \in E_1\}$$

$$R'_2 = \{(t_2, v^{\ominus}) \mid v \in V' \text{ such that } (t, v) \in E_2\} \cup \{(u^{\oplus}, s_2) \mid u \in V' \text{ such that } (u, t) \in E_2\} \\ \cup \{(u^{\oplus}, v^{\ominus}) \mid u, v \in V' \text{ such that } (u, v) \in E_2\}$$

so that $B$, $R'_1$ and $R'_2$ are pairwise disjoint.

Given a pair of paths $(P_1, P_2)$ with $P_1 = s \to u_1 \to \dots \to u_r \to t$ and $P_2 = t \to v_1 \to \dots \to v_q \to s$, as specified in the lemma statement, we can build an æ-cycle in $\mathcal{H}$, where ‘$\Rightarrow$’ denotes a matching edge:

$$s_1 \to u_1^{\oplus} \Rightarrow u_1^{\ominus} \to u_2^{\oplus} \Rightarrow \dots \Rightarrow u_r^{\ominus} \to t_1 \Rightarrow t_2 \to v_1^{\ominus} \Rightarrow v_1^{\oplus} \to v_2^{\ominus} \Rightarrow \dots \Rightarrow v_q^{\oplus} \to s_2 \Rightarrow s_1$$

It is alternating by construction, and it is elementary because $P_1$ and $P_2$ themselves are necessarily elementary (they are paths in acyclic digraphs).

Conversely, we want to extract such a pair of paths $(P_1, P_2)$ from any æ-cycle in $\mathcal{H}$. First, we claim that the RB-digraph $(V_H, R'_1, B)$ does not contain any æ-cycle. This is because any æ-path of length $\ge 2$ in it is strictly increasing for the following order: the lexicographic product of the transitive closure of $E_1$ — which, by acyclicity assumption on $G_1$, is a partial order — with the order on $\{\oplus, \ominus\}$ defined by $\oplus \le \ominus$. Likewise, $(V_H, R'_2, B)$ does not admit any æ-cycle either. Therefore, an æ-cycle in $\mathcal{H}$ must contain two edges $e_1 \in R'_1$ and $e_2 \in R'_2$.
<figure><img src="image_27.png" /><figcaption>FIGURE 13. Example for the proof of Lemma 4.22. On the left, two digraphs are drawn on the same vertices. On the right, the RB-digraph obtained by applying the construction of Lemma 4.22 with the distinguished vertices $s$ and $t$. (We do not reuse the graphs in Figure 12 because the drawing of their “superposition” would be unreadable.) The pair of paths ($s \to u \to v \to t$, $t \to w \to s$) on the left corresponds to an æ-cycle on the right, whereas the “short-circuit” ($s \to u \to w$, $w \to s$) – which we want to exclude – corresponds to a cycle that is not alternating (the consecutive edges $u^{\ominus} \to w^{\oplus} \to s_2$ are both outside the matching).</figcaption></figure>

The non-matching edges are obtained from the original edges: writing $E_i$ for the set of edges of $G_i$ (for $i \in \{1, 2\}$), we take $R_H = R'_1 \cup R'_2$ where

$$R'_1 = \{(s_1, v^{\oplus}) \mid v \in V' \text{ such that } (s, v) \in E_1\} \cup \{(u^{\ominus}, t_1) \mid u \in V' \text{ such that } (u, t) \in E_1\} \\ \cup \{(u^{\ominus}, v^{\oplus}) \mid u, v \in V' \text{ such that } (u, v) \in E_1\}$$

$$R'_2 = \{(t_2, v^{\ominus}) \mid v \in V' \text{ such that } (t, v) \in E_2\} \cup \{(u^{\oplus}, s_2) \mid u \in V' \text{ such that } (u, t) \in E_2\} \\ \cup \{(u^{\oplus}, v^{\ominus}) \mid u, v \in V' \text{ such that } (u, v) \in E_2\}$$

so that $B$, $R'_1$ and $R'_2$ are pairwise disjoint.

Given a pair of paths $(P_1, P_2)$ with $P_1 = s \to u_1 \to \dots \to u_r \to t$ and $P_2 = t \to v_1 \to \dots \to v_q \to s$, as specified in the lemma statement, we can build an æ-cycle in $\mathcal{H}$, where ‘$\Rightarrow$’ denotes a matching edge:

$$s_1 \to u_1^{\oplus} \Rightarrow u_1^{\ominus} \to u_2^{\oplus} \Rightarrow \dots \Rightarrow u_r^{\ominus} \to t_1 \Rightarrow t_2 \to v_1^{\ominus} \Rightarrow v_1^{\oplus} \to v_2^{\ominus} \Rightarrow \dots \Rightarrow v_q^{\oplus} \to s_2 \Rightarrow s_1$$

It is alternating by construction, and it is elementary because $P_1$ and $P_2$ themselves are necessarily elementary (they are paths in acyclic digraphs).

Conversely, we want to extract such a pair of paths $(P_1, P_2)$ from any æ-cycle in $\mathcal{H}$. First, we claim that the RB-digraph $(V_H, R'_1, B)$ does not contain any æ-cycle. This is because any æ-path of length $\ge 2$ in it is strictly increasing for the following order: the lexicographic product of the transitive closure of $E_1$ — which, by acyclicity assumption on $G_1$, is a partial order — with the order on $\{\oplus, \ominus\}$ defined by $\oplus \le \ominus$. Likewise, $(V_H, R'_2, B)$ does not admit any æ-cycle either. Therefore, an æ-cycle in $\mathcal{H}$ must contain two edges $e_1 \in R'_1$ and $e_2 \in R'_2$.
Given such an æ-cycle, let $\pi_1$ be the directed subpath starting with $e_1$ and ending with $e_2$, and $\pi_2$ be the complementary directed subpath starting with $e_2$ and ending with $e_1$. Then:

* $\pi_1$ contains a subpath $v_1 \xrightarrow{R'_1} v_2 \underset{B}{\implies} v_3 \xrightarrow{R'_2} v_4$. Since $v_2$ is the target of an edge in $E_1$, either $v_2 = t_2$ or $v_2 = v^\oplus$ for some $v \in V$. In the latter case, we have $v_3 = v^\ominus$, which is impossible for the source of an edge in $E_2$. Therefore $(v_2, v_3) = (t_1, t_2)$.

* $\pi_2$ contains a subpath $u_1 \xrightarrow{R'_2} u_2 \underset{B}{\implies} u_3 \xrightarrow{R'_1} u_4$. Similarly to the previous case, we conclude that $(u_2, u_3) = (s_2, s_1)$.

To recapitulate: the cycle must switch at some point from edges in $R'_1$ to edges in $R'_2$, and it must also switch back at some point; it can only do the former by crossing $(t_1, t_2) \in B$ and the latter by crossing $(s_2, s_1) \in B$. Therefore, this æ-cycle decomposes into an æ-path $P_1$ from $s_1$ to $t_1$ in $(V_H, R'_1, B)$ and an æ-path $P_2$ from $t_2$ to $s_2$ in $(V_H, R'_2, B)$, glued together by $(t_1, t_2) \in B$ and $(s_2, s_1) \in B$. These paths are vertex-disjoint because the æ-cycle that they form is, by definition of æ-cycle, elementary; they can be lifted to yield the desired pair of paths in $G_1$ and $G_2$. $\square$

We now combine these ingredients to reduce CNF-SAT to the directed æ-cycle problem.

*Proof of Theorem 4.19.* We apply the construction of the previous lemma to $G_{cl}$ and $G_{var}$ (with $V = V_{occ}$). An æ-cycle in the resulting RB-digraph corresponds to a path $P_{cl}$ from $s$ to $t$ in $G_{cl}$ plus a path $P_{var}$ from $t$ to $s$ in $G_{var}$, that are vertex-disjoint except at $s$ and $t$. We have to show that the existence of the latter is equivalent to that of an assignment that satisfies all the clauses.

Suppose that we are given such an assignment. First, there exists a unique path $P_{var}$ in $G_{var}$ that visits all literal occurrences set to **false** (Lemma 4.21). Since the assignment is satisfying, we may choose in each clause a literal set to **true**. This corresponds by Lemma 4.20 to a path $P_{cl}$ in $G_{cl}$. If some vertex of $V_{occ}$ were to appear in both $P_{var}$ and $P_{cl}$, it would mean that the corresponding literal is set both to **false** and to **true** simultaneously.

The converse direction proceeds by a similar reasoning. $\square$

**4.5. Pomset Logic Provability is $\Sigma_2^P$-Complete.** We are now in a position to treat our main complexity result:

**Theorem 4.23.** The provability problem of pomset logic is $\Sigma_2^P$-complete.

As in the case of correctness, we start with the membership part whose proof is easier than the hardness part.

**Proposition 4.24.** *Pomset logic provability is in $\Sigma_2^P$.*

*Proof.* The size of any pre-proof (i.e. axiom linking) is bounded by a polynomial in the size of its conclusion, and the correctness criterion is in coNP. Therefore, there is a $\Sigma_2^P = NP^{NP}$ algorithm that consists in first guessing non-deterministically a pre-proof whose conclusion is the input formula, then calling a NP oracle for incorrectness on this guess, and finally accepting whenever the oracle returns **false**. $\square$

To show the $\Sigma_2^P$-hardness of provability, we proceed analogously to the coNP-hardness proof for correctness, using a sequence of reductions

Boolean formula problem $\rightarrow$ graph-theoretic problem $\rightarrow$ pomset logic problem
Given such an æ-cycle, let $\pi_1$ be the directed subpath starting with $e_1$ and ending with $e_2$, and $\pi_2$ be the complementary directed subpath starting with $e_2$ and ending with $e_1$. Then:

* $\pi_1$ contains a subpath $v_1 \xrightarrow{R'_1} v_2 \underset{B}{\implies} v_3 \xrightarrow{R'_2} v_4$. Since $v_2$ is the target of an edge in $E_1$, either $v_2 = t_2$ or $v_2 = v^{\oplus}$ for some $v \in V$. In the latter case, we have $v_3 = v^{\ominus}$, which is impossible for the source of an edge in $E_2$. Therefore $(v_2, v_3) = (t_1, t_2)$.

* $\pi_2$ contains a subpath $u_1 \xrightarrow{R'_2} u_2 \underset{B}{\implies} u_3 \xrightarrow{R'_1} u_4$. Similarly to the previous case, we conclude that $(u_2, u_3) = (s_2, s_1)$.

To recapitulate: the cycle must switch at some point from edges in $R'_1$ to edges in $R'_2$, and it must also switch back at some point; it can only do the former by crossing $(t_1, t_2) \in B$ and the latter by crossing $(s_2, s_1) \in B$. Therefore, this æ-cycle decomposes into an æ-path $P_1$ from $s_1$ to $t_1$ in $(V_H, R'_1, B)$ and an æ-path $P_2$ from $t_2$ to $s_2$ in $(V_H, R'_2, B)$, glued together by $(t_1, t_2) \in B$ and $(s_2, s_1) \in B$. These paths are vertex-disjoint because the æ-cycle that they form is, by definition of æ-cycle, elementary; they can be lifted to yield the desired pair of paths in $G_1$ and $G_2$. $\square$

We now combine these ingredients to reduce CNF-SAT to the directed æ-cycle problem.

*Proof of Theorem 4.19.* We apply the construction of the previous lemma to $G_{cl}$ and $G_{var}$ (with $V = V_{occ}$). An æ-cycle in the resulting RB-digraph corresponds to a path $P_{cl}$ from $s$ to $t$ in $G_{cl}$ plus a path $P_{var}$ from $t$ to $s$ in $G_{var}$, that are vertex-disjoint except at $s$ and $t$. We have to show that the existence of the latter is equivalent to that of an assignment that satisfies all the clauses.

Suppose that we are given such an assignment. First, there exists a unique path $P_{var}$ in $G_{var}$ that visits all literal occurrences set to **false** (Lemma 4.21). Since the assignment is satisfying, we may choose in each clause a literal set to **true**. This corresponds by Lemma 4.20 to a path $P_{cl}$ in $G_{cl}$. If some vertex of $V_{occ}$ were to appear in both $P_{var}$ and $P_{cl}$, it would mean that the corresponding literal is set both to **false** and to **true** simultaneously.

The converse direction proceeds by a similar reasoning. $\square$

**4.5. Pomset Logic Provability is $\Sigma_2^P$-Complete.** We are now in a position to treat our main complexity result:

**Theorem 4.23.** The provability problem of pomset logic is $\Sigma_2^P$-complete.

As in the case of correctness, we start with the membership part whose proof is easier than the hardness part.

**Proposition 4.24.** *Pomset logic provability is in $\Sigma_2^P$.*

*Proof.* The size of any pre-proof (i.e. axiom linking) is bounded by a polynomial in the size of its conclusion, and the correctness criterion is in coNP. Therefore, there is a $\Sigma_2^P = NP^{NP}$ algorithm that consists in first guessing non-deterministically a pre-proof whose conclusion is the input formula, then calling a NP oracle for incorrectness on this guess, and finally accepting whenever the oracle returns **false**. $\square$

To show the $\Sigma_2^P$-hardness of provability, we proceed analogously to the coNP-hardness proof for correctness, using a sequence of reductions

Boolean formula problem $\longrightarrow$ graph-theoretic problem $\longrightarrow$ pomset logic problem
<figure><img src="image_28.png" /><figcaption>FIGURE 14. The paired $G_{var}$ built from $\forall x \forall y \exists z (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$ in the proof of Lemma 4.26 (compare with Figure 12b). The dashed edges represent the choice of a switching in which these edges are erased. The specific choice made here gives us three bits of information that can be interpreted as $x = \mathbf{false}$, ($x = \mathbf{true}$) $\Rightarrow$ ($y = \mathbf{true}$) and finally ($x = \mathbf{false}$) $\Rightarrow$ ($y = \mathbf{false}$) – recall that visiting a literal corresponds to setting it to $\mathbf{false}$ – which entails $x = y = \mathbf{false}$. The thick colored path materializes this assignment of the $\forall$-variables, and it is a prefix of all paths from $t$ to $s$ in this switching.</figcaption></figure>

Here, this pattern is instantiated with the $\Pi_2^P$-complete $\forall\exists$-CNF-SAT problem (cf. Section 4.1) to the left and *unprovability* in pomset logic to the right. For the auxiliary step in the middle, we use a problem formulated using “switchings” of “paired graphs”, as in the standard Danos–Regnier correctness criterion for MLL+mix [DR89, FR94].

**Definition 4.25.** A *paired digraph* is a directed graph $\mathcal{G}$ equipped with a set $\mathfrak{P}$ of unordered pairs of edges, such that the pairs are disjoint (if $p, p' \in \mathfrak{P}$, then $p \cap p' = \emptyset$) and paired edges have the same source (if $\{(u_1, v_1), (u_2, v_2)\} \in \mathfrak{P}$, then $u_1 = u_2$). An edge is *unpaired* if it is not an element of any pair in $\mathfrak{P}$. A *switching*<fnref n="18" /> of $(\mathcal{G}, \mathfrak{P})$ is a spanning subgraph of $\mathcal{G}$ that contains all unpaired edges and exactly one edge in each pair.

A *paired RB-digraph* is a tuple $(V_G, R_G, B_G, \mathfrak{P})$ such that $(V_G, R_G, B_G)$ is a RB-digraph and $(V_G, R_G, \mathfrak{P})$ is a paired digraph. Consistently with the above, we define a *switching* of $(V_G, R_G, B_G, \mathfrak{P})$ to be an RB-digraph of the form $(V_G, R', B_G, \mathfrak{P})$ where $R' \subseteq R_G$ contains all unpaired edges from $R_G$ and exactly one edge in each pair.

The reader familiar with proof nets might find it strange that we are mixing perfect matchings and paired graphs together: the former already play the role of expressing the correctness criterion, so what are the latter good for? The answer is that switchings will morally correspond to choices of axiom linkings: the possible proof nets whose conclusion is a given arbitrary (not necessarily balanced) formula only differ by which pairs of dual atoms are joined by axiom links. Without further ado, let us present our reductions.

**Lemma 4.26.** It is $\Pi_2^P$-hard to decide whether every *switching* of a *paired RB-digraph* contains at least one $\omega$-cycle.

*Proof.* We proceed by polynomial time reduction from $\forall\exists$-CNF-SAT (cf. Section 4.1). Consider an instance of this problem whose universal variables are $x_1, \dots, x_m$ (we will not need to

<footnote n="18">¹⁸The literature sometimes uses “switching” for a choice function on the set of edge pairs, rather than the digraph defined by this choice.</footnote>
<figure><img src="image_28.png" /><figcaption>FIGURE 14. The paired $G_{var}$ built from $\forall x \forall y \exists z (x \lor y \lor z) \land (\neg x \lor y) \land (\neg y \lor \neg z)$ in the proof of Lemma 4.26 (compare with Figure 12b). The dashed edges represent the choice of a switching in which these edges are erased. The specific choice made here gives us three bits of information that can be interpreted as $x = \mathbf{false}$, ($x = \mathbf{true}$) $\Rightarrow$ ($y = \mathbf{true}$) and finally ($x = \mathbf{false}$) $\Rightarrow$ ($y = \mathbf{false}$) – recall that visiting a literal corresponds to setting it to $\mathbf{false}$ – which entails $x = y = \mathbf{false}$. The thick colored path materializes this assignment of the $\forall$-variables, and it is a prefix of all paths from $t$ to $s$ in this switching.</figcaption></figure>

Here, this pattern is instantiated with the $\Pi_2^P$-complete $\forall \exists$-CNF-SAT problem (cf. Section 4.1) to the left and *unprovability* in pomset logic to the right. For the auxiliary step in the middle, we use a problem formulated using “switchings” of “paired graphs”, as in the standard Danos–Regnier correctness criterion for MLL+mix [DR89, FR94].

**Definition 4.25.** A *paired digraph* is a directed graph $\mathcal{G}$ equipped with a set $\mathfrak{P}$ of unordered pairs of edges, such that the pairs are disjoint (if $p, p' \in \mathfrak{P}$, then $p \cap p' = \emptyset$) and paired edges have the same source (if $\{(u_1, v_1), (u_2, v_2)\} \in \mathfrak{P}$, then $u_1 = u_2$). An edge is *unpaired* if it is not an element of any pair in $\mathfrak{P}$. A *switching*<fnref n="18" /> of $(\mathcal{G}, \mathfrak{P})$ is a spanning subgraph of $\mathcal{G}$ that contains all unpaired edges and exactly one edge in each pair.

A *paired RB-digraph* is a tuple $(V_G, R_G, B_G, \mathfrak{P})$ such that $(V_G, R_G, B_G)$ is a RB-digraph and $(V_G, R_G, \mathfrak{P})$ is a paired digraph. Consistently with the above, we define a *switching* of $(V_G, R_G, B_G, \mathfrak{P})$ to be an RB-digraph of the form $(V_G, R', B_G, \mathfrak{P})$ where $R' \subseteq R_G$ contains all unpaired edges from $R_G$ and exactly one edge in each pair.

The reader familiar with proof nets might find it strange that we are mixing perfect matchings and paired graphs together: the former already play the role of expressing the correctness criterion, so what are the latter good for? The answer is that switchings will morally correspond to choices of axiom linkings: the possible proof nets whose conclusion is a given arbitrary (not necessarily balanced) formula only differ by which pairs of dual atoms are joined by axiom links. Without further ado, let us present our reductions.

**Lemma 4.26.** It is $\Pi_2^P$-hard to decide whether every *switching* of a *paired RB-digraph* contains at least one $\omega$-cycle.

*Proof.* We proceed by polynomial time reduction from $\forall \exists$-CNF-SAT (cf. Section 4.1). Consider an instance of this problem whose universal variables are $x_1, \dots, x_m$ (we will not need to

<footnote n="18">¹⁸The literature sometimes uses “switching” for a choice function on the set of edge pairs, rather than the digraph defined by this choice.</footnote>
directly manipulate the CNF or the existential variables). We reuse the constructions $\mathcal{G}_{cl}$ and $\mathcal{G}_{var}$ of Lemmas 4.20 and 4.21, applying them to the CNF part of the input. Strictly speaking, the digraph $\mathcal{G}_{var}$ depends on the order of variables, and here we shall consider for convenience that the universal variables come before the existential ones, with the $i$-th variable being $x_i$ for $i \le m$.

The key idea is to distinguish a set $\mathfrak{P}$ of disjoint edge pairs in $\mathcal{G}_{var}$ (see Figure 14 for an example). Let $t$ and $s$ be its distinguished source and sink vertices. For $1 \le i \le m$, we write:

* $u_i$ (resp. $v_i$) for the vertex that corresponds to the first (resp. last) occurrence of $x_i$;

* $u_i^-$ (resp. $v_i^-$) for the vertex that corresponds to the first (resp. last) occurrence of $\neg x_i$.

(Here “first” and “last” mean the same thing as in the construction of $\mathcal{G}_{var}$ (Lemma 4.21): they are defined with respect to an arbitrary order on the set of clauses. To build $\mathcal{G}_{var}$, each variable must occur at least once positively and once negatively; this can be assumed without loss of generality for instances of $\forall \exists$-CNF-SAT. It is possible that $u_i = v_i$, but for $i \neq j$, we have $u_i \neq v_j$.) We take

$$ \mathfrak{P} = \left\{ (w, u_i), (w, u_i^-) \mid i \in \{1, \dots, m\}, w \in \left[ \begin{array}{ll} \{s\} & \text{when } i = 1 \\ \{v_{i-1}, v_{i-1}^-\} & \text{otherwise} \end{array} \right] \right\} $$

The reader may check that all edges that appear in $\mathfrak{P}$ are indeed edges in $\mathcal{G}_{var}$. Furthermore, it follows from the definition that the pairs are disjoint and any two paired edges have the same source. Therefore, $(\mathcal{G}_{var}, \mathfrak{P})$ is a paired digraph in the sense of Definition 4.25.

The point is that, as illustrated in Figure 14, for any switching $S$ of $(\mathcal{G}_{var}, \mathfrak{P})$, exactly one of $v_m$ and $v_m^-$ is reachable from $s$, and the path is unique – let us call it $\pi_S$. Each switching thus induces an assignment $\{x_1, \dots, x_m\} \to \{\text{true}, \text{false}\}$, which assigns $x_i$ to **false** when $\pi_S$ visits the vertices associated to $x_i$ (among which are $u_i$ and $v_i$), and to **true** otherwise (in which case the path necessarily visits $u_i^-$ and $v_i^-$); and the paths from $s$ to $t$ in the switching correspond to extending this assignment with values for the other (existential) variables. Moreover, this map from switchings to assignments of the universal variables is surjective (more precisely, each of the $2^m$ assignments is induced by exactly $2^{m-1}$ switchings among the total of $2^{2m-1}$ possible switchings).

Let us consider next the correspondence given by Lemma 4.21 between the paths from $t$ to $s$ and the assignments of all variables (both universal and existential). One can see that given such a path $\rho$ and a switching $S$, the following are equivalent:

* the edges of $\rho$ exist in $S$;

* $\pi_S$ is a prefix of $\rho$;

* the assignment that corresponds to $S$ (by the above discussion) is the restriction to the universal variables of the one that corresponds to $\rho$ (by Lemma 4.21).

From these observations, one can deduce, by a similar reasoning to the proof of Theorem 4.19, that the given $\forall \exists$-CNF-SAT instance is positive if and only if, for every switching $S$ of $(\mathcal{G}_{var}, \mathfrak{P})$, there exists a path from $s$ to $t$ in $\mathcal{G}_{cl}$ and a path from $t$ to $s$ in $S$ that do not share any intermediate vertex. To conclude, it suffices to reduce this to the desired problem on paired RB-digraphs by a suitable adaptation of Lemma 4.22, whose precise formulation is left to the reader. $\square$

**Theorem 4.27.** *Unprovability in pomset logic is $\Pi_2^P$-hard.*

*Proof.* We reduce the problem shown to be $\Pi_2^P$-hard by Lemma 4.26 to pomset logic unprovability by extending proofification to handle edge pairs. An example is given in Figure 15.
directly manipulate the CNF or the existential variables). We reuse the constructions $G_{cl}$ and $G_{var}$ of Lemmas 4.20 and 4.21, applying them to the CNF part of the input. Strictly speaking, the digraph $G_{var}$ depends on the order of variables, and here we shall consider for convenience that the universal variables come before the existential ones, with the $i$-th variable being $x_i$ for $i \le m$.

The key idea is to distinguish a set $\mathfrak{P}$ of disjoint edge pairs in $G_{var}$ (see Figure 14 for an example). Let $t$ and $s$ be its distinguished source and sink vertices. For $1 \le i \le m$, we write:

* $u_i$ (resp. $v_i$) for the vertex that corresponds to the first (resp. last) occurrence of $x_i$;

* $u_i^-$ (resp. $v_i^-$) for the vertex that corresponds to the first (resp. last) occurrence of $\neg x_i$.

(Here “first” and “last” mean the same thing as in the construction of $G_{var}$ (Lemma 4.21): they are defined with respect to an arbitrary order on the set of clauses. To build $G_{var}$, each variable must occur at least once positively and once negatively; this can be assumed without loss of generality for instances of $\forall \exists$-CNF-SAT. It is possible that $u_i = v_i$, but for $i \neq j$, we have $u_i \neq v_j$.) We take

$$ \mathfrak{P} = \left\{ (w, u_i), (w, u_i^-) \mid i \in \{1, \dots, m\}, w \in \left[ \begin{array}{ll} \{s\} & \text{when } i = 1 \\ \{v_{i-1}, v_{i-1}^-\} & \text{otherwise} \end{array} \right] \right\} $$

The reader may check that all edges that appear in $\mathfrak{P}$ are indeed edges in $G_{var}$. Furthermore, it follows from the definition that the pairs are disjoint and any two paired edges have the same source. Therefore, $(G_{var}, \mathfrak{P})$ is a paired digraph in the sense of Definition 4.25.

The point is that, as illustrated in Figure 14, for any switching $S$ of $(G_{var}, \mathfrak{P})$, exactly one of $v_m$ and $v_m^-$ is reachable from $s$, and the path is unique – let us call it $\pi_S$. Each switching thus induces an assignment $\{x_1, \dots, x_m\} \to \{\text{true}, \text{false}\}$, which assigns $x_i$ to **false** when $\pi_S$ visits the vertices associated to $x_i$ (among which are $u_i$ and $v_i$), and to **true** otherwise (in which case the path necessarily visits $u_i^-$ and $v_i^-$); and the paths from $s$ to $t$ in the switching correspond to extending this assignment with values for the other (existential) variables. Moreover, this map from switchings to assignments of the universal variables is surjective (more precisely, each of the $2^m$ assignments is induced by exactly $2^{m-1}$ switchings among the total of $2^{2m-1}$ possible switchings).

Let us consider next the correspondence given by Lemma 4.21 between the paths from $t$ to $s$ and the assignments of all variables (both universal and existential). One can see that given such a path $\rho$ and a switching $S$, the following are equivalent:

* the edges of $\rho$ exist in $S$;

* $\pi_S$ is a prefix of $\rho$;

* the assignment that corresponds to $S$ (by the above discussion) is the restriction to the universal variables of the one that corresponds to $\rho$ (by Lemma 4.21).

From these observations, one can deduce, by a similar reasoning to the proof of Theorem 4.19, that the given $\forall \exists$-CNF-SAT instance is positive if and only if, for every switching $S$ of $(G_{var}, \mathfrak{P})$, there exists a path from $s$ to $t$ in $G_{cl}$ and a path from $t$ to $s$ in $S$ that do not share any intermediate vertex. To conclude, it suffices to reduce this to the desired problem on paired RB-digraphs by a suitable adaptation of Lemma 4.22, whose precise formulation is left to the reader. $\square$

**Theorem 4.27.** *Unprovability in pomset logic is $\Pi_2^P$-hard.*

*Proof.* We reduce the problem shown to be $\Pi_2^P$-hard by Lemma 4.26 to pomset logic unprovability by extending proofification to handle edge pairs. An example is given in Figure 15.
Let $(V_G, R_G, B_G, \mathfrak{P})$ be a paired RB-digraph (we write $\mathcal{G} = (V_G, R_G, B_G)$). We assume without loss of generality that for every edge pair $\{(u, v), (u, w)\} \in \mathfrak{P}$, the opposite edges $(v, u)$ and $(w, u)$ are not present in the graph (otherwise, break $(v, u)$ up into a path of length three involving two new vertices, add the middle edge of this path to the matching, and similarly for $(w, u)$). Let us define the following flat sequent, which is not balanced in general (the description deliberately mirrors that of $\Pi(\mathcal{G})$ in Definition 4.15):

$$ \Gamma = [C_{u_1} \otimes C_{v_1}, \dots, C_{u_m} \otimes C_{v_m}, D_{e_1}, \dots, D_{e_k}, D'_{p_1}, \dots, D'_{p_l}] $$

where (using again the notation of Definition 2.13):

* $\{e_1, \dots, e_k\}$ is the set of unpaired edges, $\{(u_1, v_1), (v_1, u_1), \dots, (u_m, v_m), (v_m, u_m)\} = B_G$, and $\{p_1, \dots, p_l\} = \mathfrak{P}$, all these enumerations being non-repeating;

* the atoms involved in $\Gamma$ are created as follows:

- for each $\{u, v\} \subseteq V_G$ such that $(u, v) \in R_G^\otimes$ – according to the assumption w.l.o.g. we made above, both $(u, v)$ and $(v, u)$ are then unpaired – we give the names $a_{u,v}$ and $a_{v,u}$ to a fresh pair of dual atoms;

- for each edge $(u, v) \in R_G^\downarrow$ which is unpaired, we generate two fresh atoms $a_{u,v}$ and $a_{v,u}$ that are not dual;

- for each pair $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, we create two fresh atoms $a_{u,p}$, $b_p$ and we define $a_{v,u} = a_{w,u} = b_p$ (observe however that we do not define $a_{u,v}$ nor $a_{u,w}$);

* for $u \in V_G$, $C_u = \bigwedge_v a_{u,v} \otimes \bigwedge_p a_{u,p}$ where $v$ (resp. $p$) ranges over the vertices (resp. pairs) such that $a_{u,v}$ (resp. $a_{u,v}$) is defined according to the above;

* for $(u, v) \in R_G^\downarrow$, if $(u, v)$ is unpaired, then $D_{(u,v)} = a_{u,v}^\perp \triangleleft a_{v,u}^\perp$;

* finally, for $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, we set $D'_p = \langle a_{u,p}^\perp \triangleleft b_p^\perp \rangle \otimes b_p^\perp$.

This sequent $\Gamma$ that we just defined contains, for each pair $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, exactly two occurrences of $b_p$, designated as $a_{v,u}$ and $a_{w,u}$, and exactly two occurrences of $b_p^\perp$ in $D'_p$, that we will also name: $D'_p = \langle a_{u,p}^\perp \triangleleft c_{p\downarrow} \rangle \otimes c_{p\uparrow}$. So each pre-proof of $\Gamma$ induces a bijection between $\{a_{v,u}, a_{w,u}\}$ and $\{c_{p\downarrow}, c_{p\uparrow}\}$. Conversely, such a choice of bijection for each edge pair uniquely determines a corresponding axiom linking.

Let $\ell$ be a pre-proof of $\Gamma$. Let $s, t: \mathfrak{P} \to V_G$ be defined by $\ell(c_{p\uparrow}) = a_{t(p),s(p)}$ for all $p \in \mathfrak{P}$. We define the RB-digraph $S_\ell$ to be the switching where the edge $(s(p), t(p))$ has been deleted in each pair $p$. We can reformulate what we observed in the previous paragraph as the fact that $\ell \mapsto S_\ell$ is a bijection from axiom linkings for $\Gamma$ to switchings of our paired RB-digraph.

In the cographic RB-prenet $\rho(\Gamma, \ell)$, the vertex for $c_{p\uparrow}$ has no incident non-matching edge, so it cannot be involved in any æ-cycle. Since it is matched with $a_{t(p),s(p)}$, the latter also cannot occur in any æ-cycle. So the witnesses of incorrectness in $\rho(\Gamma, \ell)$, i.e. its chordless æ-cycles, must be entirely contained in the induced sub-RB-digraph that excludes $c_{p\uparrow}$ and $a_{t(p),s(p)}$ for all $p \in \mathfrak{P}$. Thanks to the correspondence between pseudo-subformulas and induced subgraphs (Proposition 3.5), one can write (an isomorphic copy of) this sub-RB-digraph as $\rho(\Gamma', \ell')$ where $\Gamma'$ is obtained from $\Gamma$ by substituting the aforementioned atom occurrences by $\mathbb{I}$, and $\ell'$ is a restriction of $\ell$; so $(\Gamma, \ell)$ is incorrect iff $(\Gamma', \ell')$ is.

The key property, that one can check from the definitions, is that $\Gamma'$ is balanced and equal up to atom renaming to the proofification $\Pi(S_\ell)$ (note for instance that if $(u, v) \in p \in \mathfrak{P}$ and $(u, v) \in R_{S_\ell}$ then the formula $D'_p$ in $\Gamma$ becomes $D_{(u,v)}$ in $\Pi(S_\ell)$ after substituting $c_{p\uparrow}$ by $\mathbb{I}$). Thus, by Theorem 4.17, $(\Gamma, \ell)$ is incorrect if and only if $S_\ell$ contains an æ-cycle. By definition of provability, and using the surjectivity of $\ell \mapsto S_\ell$, it follows that $\Gamma$ is unprovable if and only
Let $(V_G, R_G, B_G, \mathfrak{P})$ be a paired RB-digraph (we write $\mathcal{G} = (V_G, R_G, B_G)$). We assume without loss of generality that for every edge pair $\{(u, v), (u, w)\} \in \mathfrak{P}$, the opposite edges $(v, u)$ and $(w, u)$ are not present in the graph (otherwise, break $(v, u)$ up into a path of length three involving two new vertices, add the middle edge of this path to the matching, and similarly for $(w, u)$). Let us define the following flat sequent, which is not balanced in general (the description deliberately mirrors that of $\Pi(\mathcal{G})$ in Definition 4.15):

$$ \Gamma = [C_{u_1} \otimes C_{v_1}, \dots, C_{u_m} \otimes C_{v_m}, D_{e_1}, \dots, D_{e_k}, D'_{p_1}, \dots, D'_{p_l}] $$

where (using again the notation of Definition 2.13):

* $\{e_1, \dots, e_k\}$ is the set of unpaired edges, $\{(u_1, v_1), (v_1, u_1), \dots, (u_m, v_m), (v_m, u_m)\} = B_G$, and $\{p_1, \dots, p_l\} = \mathfrak{P}$, all these enumerations being non-repeating;

* the atoms involved in $\Gamma$ are created as follows:

- for each $\{u, v\} \subseteq V_G$ such that $(u, v) \in R_G^\otimes$ – according to the assumption w.l.o.g. we made above, both $(u, v)$ and $(v, u)$ are then unpaired – we give the names $a_{u,v}$ and $a_{v,u}$ to a fresh pair of dual atoms;

- for each edge $(u, v) \in R_G^\downarrow$ which is unpaired, we generate two fresh atoms $a_{u,v}$ and $a_{v,u}$ that are not dual;

- for each pair $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, we create two fresh atoms $a_{u,p}$, $b_p$ and we define $a_{v,u} = a_{w,u} = b_p$ (observe however that we do not define $a_{u,v}$ nor $a_{w,w}$);

* for $u \in V_G$, $C_u = \bigwedge_v a_{u,v} \otimes \bigwedge_p a_{u,p}$ where $v$ (resp. $p$) ranges over the vertices (resp. pairs) such that $a_{u,v}$ (resp. $a_{u,v}$) is defined according to the above;

* for $(u, v) \in R_G^\downarrow$, if $(u, v)$ is unpaired, then $D_{(u,v)} = a_{u,v}^\perp \triangleleft a_{v,u}^\perp$;

* finally, for $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, we set $D'_p = \langle a_{u,p}^\perp \triangleleft b_p^\perp \rangle \otimes b_p^\perp$.

This sequent $\Gamma$ that we just defined contains, for each pair $p = \{(u, v), (u, w)\} \in \mathfrak{P}$, exactly two occurrences of $b_p$, designated as $a_{v,u}$ and $a_{w,u}$, and exactly two occurrences of $b_p^\perp$ in $D'_p$, that we will also name: $D'_p = \langle a_{u,p}^\perp \triangleleft c_{p\downarrow} \rangle \otimes c_{p\uparrow}$. So each pre-proof of $\Gamma$ induces a bijection between $\{a_{v,u}, a_{w,u}\}$ and $\{c_{p\downarrow}, c_{p\uparrow}\}$. Conversely, such a choice of bijection for each edge pair uniquely determines a corresponding axiom linking.

Let $\ell$ be a pre-proof of $\Gamma$. Let $s, t: \mathfrak{P} \to V_G$ be defined by $\ell(c_{p\uparrow}) = a_{t(p),s(p)}$ for all $p \in \mathfrak{P}$. We define the RB-digraph $S_\ell$ to be the switching where the edge $(s(p), t(p))$ has been deleted in each pair $p$. We can reformulate what we observed in the previous paragraph as the fact that $\ell \mapsto S_\ell$ is a bijection from axiom linkings for $\Gamma$ to switchings of our paired RB-digraph.

In the cographic RB-prenet $\rho(\Gamma, \ell)$, the vertex for $c_{p\uparrow}$ has no incident non-matching edge, so it cannot be involved in any æ-cycle. Since it is matched with $a_{t(p),s(p)}$, the latter also cannot occur in any æ-cycle. So the witnesses of incorrectness in $\rho(\Gamma, \ell)$, i.e. its chordless æ-cycles, must be entirely contained in the induced sub-RB-digraph that excludes $c_{p\uparrow}$ and $a_{t(p),s(p)}$ for all $p \in \mathfrak{P}$. Thanks to the correspondence between pseudo-subformulas and induced subgraphs (Proposition 3.5), one can write (an isomorphic copy of) this sub-RB-digraph as $\rho(\Gamma', \ell')$ where $\Gamma'$ is obtained from $\Gamma$ by substituting the aforementioned atom occurrences by $\mathbb{I}$, and $\ell'$ is a restriction of $\ell$; so $(\Gamma, \ell)$ is incorrect iff $(\Gamma', \ell')$ is.

The key property, that one can check from the definitions, is that $\Gamma'$ is balanced and equal up to atom renaming to the proofification $\Pi(S_\ell)$ (note for instance that if $(u, v) \in p \in \mathfrak{P}$ and $(u, v) \in R_{S_\ell}$ then the formula $D'_p$ in $\Gamma$ becomes $D_{(u,v)}$ in $\Pi(S_\ell)$ after substituting $c_{p\uparrow}$ by $\mathbb{I}$). Thus, by Theorem 4.17, $(\Gamma, \ell)$ is incorrect if and only if $S_\ell$ contains an æ-cycle. By definition of provability, and using the surjectivity of $\ell \mapsto S_\ell$, it follows that $\Gamma$ is unprovable if and only
<figure><img src="image_29.png" /><figcaption>FIGURE 15. Example for the proof of Theorem 4.27.</figcaption></figure>

Left: a paired RB-digraph (compare Figure 11); the two non-matching edges coming out of $y$ are paired, and the dashed edge represents a choice of switching in which it is deleted.

Right: the cographic RB-prenet corresponding to this choice, with $p = \{(y, x), (y, z)\}$ (the dashed blue/bold edges display the matching that would correspond to the other possible choice). Note that we have $a_{x,y} = a_{z,y} = b_p$.

if every switching of the initial RB-graph admits an æ-cycle. According to Lemma 4.26, it is **NP**-hard to test the latter condition given the input Γ. Since Γ can be computed from our original paired RB-digraph in polynomial time, this concludes the proof. □

Proposition 4.24 and Theorem 4.27 together are what it means, by definition, for provability in pomset logic to be $\Sigma_2^P$-complete. Thus, we have established Theorem 4.23.

## 5. BACK TO THE SEQUENT CALCULUS

In this section we come back to the problem of finding a sequent calculus for BV and pomset logic, as this problem was the starting point for much of the research done on these two logics. The current state of the art on this topic is:

(1) Retoré [Ret93] presented a sequent calculus for pomset logic, for which he could show soundness, but not completeness and not cut elimination.<fnref n="19" />

(2) This difficulty motivated Gugliemi [Gug07] to develop system BV, which has a cut elimination proof in deep inference, but not in the sequent calculus. Then Tiu [Tiu06] has shown that “deepness” is necessary for BV and therefore there cannot be a sequent calculus for BV in which all rules are “shallow” (see also Remark 4.12).

(3) However, the formulas used by Tiu [Tiu06] to defy the sequent calculus can be proved in the cut-free version of Retoré's [Ret93] sequent calculus, using the *entropy rule*.

<footnote n="19">¹⁹In fact, in [Ret97a] and [Ret21] two variations of that sequent calculus are proposed, which both have the same problem.</footnote>
<figure><img src="image_29.png" /><figcaption>FIGURE 15. Example for the proof of Theorem 4.27.</figcaption></figure>

Left: a paired RB-digraph (compare Figure 11); the two non-matching edges coming out of $y$ are paired, and the dashed edge represents a choice of switching in which it is deleted.

Right: the cographic RB-prenet corresponding to this choice, with $p = \{(y, x), (y, z)\}$ (the dashed blue/bold edges display the matching that would correspond to the other possible choice). Note that we have $a_{x,y} = a_{z,y} = b_p$.

if every switching of the initial RB-graph admits an æ-cycle. According to Lemma 4.26, it is **NP**-hard to test the latter condition given the input Γ. Since Γ can be computed from our original paired RB-digraph in polynomial time, this concludes the proof. □

Proposition 4.24 and Theorem 4.27 together are what it means, by definition, for provability in pomset logic to be $\Sigma_2^P$-complete. Thus, we have established Theorem 4.23.

## 5. BACK TO THE SEQUENT CALCULUS

In this section we come back to the problem of finding a sequent calculus for BV and pomset logic, as this problem was the starting point for much of the research done on these two logics. The current state of the art on this topic is:

(1) Retoré [Ret93] presented a sequent calculus for pomset logic, for which he could show soundness, but not completeness and not cut elimination.<fnref n="19" />

(2) This difficulty motivated Gugliemi [Gug07] to develop system BV, which has a cut elimination proof in deep inference, but not in the sequent calculus. Then Tiu [Tiu06] has shown that “deepness” is necessary for BV and therefore there cannot be a sequent calculus for BV in which all rules are “shallow” (see also Remark 4.12).

(3) However, the formulas used by Tiu [Tiu06] to defy the sequent calculus can be proved in the cut-free version of Retoré's [Ret93] sequent calculus, using the *entropy rule*.

<footnote n="19">¹⁹In fact, in [Ret97a] and [Ret21] two variations of that sequent calculus are proposed, which both have the same problem.</footnote>
(4) In Remark 4.12 we also observed that our complexity results pose a much harder obstacle to a sequent calculus for pomset logic than the mere need of “deepness”.

(5) But recently, Slavnov [Sla19] presented a cut-free sequent calculus that is sound and complete for pomset logic.

This is, of course, confusing, as it seems contradictory. Does (3) mean that Tiu's [Tiu06] result is wrong? Does (5) mean that Retoré [Ret93] just did not try hard enough and the problem is solved? Does it mean that our complexity result about the $\Sigma_2^P$-completeness of pomset logic is wrong or that $\mathbf{NP} = \mathbf{coNP}$?

The answer to all these questions is, of course, “No”. And the purpose of this section is to clarify the confusion and work out the subtleties of possible sequent calculi for pomset logic and BV. More precisely we present the following results:

* We show that Retoré's sequent calculus with cut (the variant presented in [Ret21]) is equivalent to SBV. It is therefore a sequent calculus for BV and not for pomset logic.

* We present a formula^20 that is provable in BV but not in the cut-free version of Retoré's [Ret93] sequent calculus. Therefore, that sequent calculus does not admit cut elimination.

* We refine Tiu's [Tiu06] argument about the need for “deepness” in BV such that Retoré's entropy rule is no longer enough to prove the formulas used in the argument.

* We use our results from the previous section to make a complexity-theoretic argument to show that a “standard” sequent calculus for pomset logic is impossible.

* Finally, we discuss Slavnov's [Sla19] sequent calculus and exhibit how he circumvents this complexity-theoretic obstacle.

**5.1. Retoré's Sequent Calculus with Cuts is Equivalent to BV.** Recall that a pomset logic sequent can be seen as a $\otimes$-free generalized formula over a set of formula occurrences (see Proposition 2.10). Hence, we can define the graph of a sequent $\Gamma$ as in Definition 2.18. Let $G_\Gamma = (V_\Gamma, R_\Gamma)$ and $G_{\Gamma'} = (V_{\Gamma'}, R_{\Gamma'})$ be the graphs of sequents $\Gamma$ and $\Gamma'$, respectively. Then both are series-parallel orders (see Proposition 2.32), and we define

$$ \Gamma' \preceq \Gamma \quad \text{iff} \quad V_{\Gamma'} = V_{\Gamma} \quad \text{and} \quad R_{\Gamma'} \subseteq R_{\Gamma} \qquad (5.1) $$

i.e., both sequents contain the same formula occurrences, and the order induced by $\Gamma'$ is contained in the order induced by $\Gamma$. We are now ready to discuss Retoré's sequent calculus, shown in Figure 16.<fnref n="21" />

The $\otimes$-introduction rule and the $\triangleleft$-introduction rule simply express the correspondence between the structural/sequent level connectives and the logical/formula level connectives. Note that the $\otimes$-introduction rule and the cut rule can only be applied in flat contexts (but $\Gamma$ and $\Delta$ can be non-flat sequents). The standard mix-rule is derivable using the dimix- and entropy-rules.

Before embarking on the equivalence of this sequent calculus with BV, let us illustrate the added power of cuts. For this purpose, we recall an example sequent considered by Retoré and the second author:

$$ [a \otimes (c \triangleleft b^{\perp}), a^{\perp} \triangleleft f, c^{\perp} \triangleleft d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp}), e \triangleleft b] \qquad (5.2) $$

<footnote n="20">²⁰This formula has already been presented in [Ret21].</footnote>

<footnote n="21">²¹In this calculus, which is taken from [Ret21] sequents define SP-orders. In [Ret93], sequent can be arbitrary orders, and in [Ret97a], the entropy rule is missing.</footnote>
(4) In Remark 4.12 we also observed that our complexity results pose a much harder obstacle to a sequent calculus for pomset logic than the mere need of “deepness”.

(5) But recently, Slavnov [Sla19] presented a cut-free sequent calculus that is sound and complete for pomset logic.

This is, of course, confusing, as it seems contradictory. Does (3) mean that Tiu's [Tiu06] result is wrong? Does (5) mean that Retoré [Ret93] just did not try hard enough and the problem is solved? Does it mean that our complexity result about the $\Sigma_2^P$-completeness of pomset logic is wrong or that $NP = coNP$?

The answer to all these questions is, of course, “No”. And the purpose of this section is to clarify the confusion and work out the subtleties of possible sequent calculi for pomset logic and BV. More precisely we present the following results:

* We show that Retoré's sequent calculus with cut (the variant presented in [Ret21]) is equivalent to SBV. It is therefore a sequent calculus for BV and not for pomset logic.

* We present a formula^20 that is provable in BV but not in the cut-free version of Retoré's [Ret93] sequent calculus. Therefore, that sequent calculus does not admit cut elimination.

* We refine Tiu's [Tiu06] argument about the need for “deepness” in BV such that Retoré's entropy rule is no longer enough to prove the formulas used in the argument.

* We use our results from the previous section to make a complexity-theoretic argument to show that a “standard” sequent calculus for pomset logic is impossible.

* Finally, we discuss Slavnov's [Sla19] sequent calculus and exhibit how he circumvents this complexity-theoretic obstacle.

**5.1. Retoré's Sequent Calculus with Cuts is Equivalent to BV.** Recall that a pomset logic sequent can be seen as a $\otimes$-free generalized formula over a set of formula occurrences (see Proposition 2.10). Hence, we can define the graph of a sequent $\Gamma$ as in Definition 2.18. Let $G_\Gamma = (V_\Gamma, R_\Gamma)$ and $G_{\Gamma'} = (V_{\Gamma'}, R_{\Gamma'})$ be the graphs of sequents $\Gamma$ and $\Gamma'$, respectively. Then both are series-parallel orders (see Proposition 2.32), and we define

$$ \Gamma' \preceq \Gamma \quad \text{iff} \quad V_{\Gamma'} = V_{\Gamma} \quad \text{and} \quad R_{\Gamma'} \subseteq R_{\Gamma} \qquad (5.1) $$

i.e., both sequents contain the same formula occurrences, and the order induced by $\Gamma'$ is contained in the order induced by $\Gamma$. We are now ready to discuss Retoré's sequent calculus, shown in Figure 16.<fnref n="21" />

The $\otimes$-introduction rule and the $\langle \cdot, \cdot \rangle$-introduction rule simply express the correspondence between the structural/sequent level connectives and the logical/formula level connectives. Note that the $\otimes$-introduction rule and the cut rule can only be applied in flat contexts (but $\Gamma$ and $\Delta$ can be non-flat sequents). The standard mix-rule is derivable using the dimix- and entropy-rules.

Before embarking on the equivalence of this sequent calculus with BV, let us illustrate the added power of cuts. For this purpose, we recall an example sequent considered by Retoré and the second author:

$$ [a \otimes (c \triangleleft b^{\perp}), a^{\perp} \triangleleft f, c^{\perp} \triangleleft d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp}), e \triangleleft b] \qquad (5.2) $$

<footnote n="20">²⁰This formula has already been presented in [Ret21].</footnote>

<footnote n="21">²¹In this calculus, which is taken from [Ret21] sequents define SP-orders. In [Ret93], sequent can be arbitrary orders, and in [Ret97a], the entropy rule is missing.</footnote>
$$
\begin{array}{c} \text{axiom} \\ \frac{[a, a^{\perp}]}{\Gamma} \end{array} \quad \begin{array}{c} \text{dimix} \\ \frac{\Gamma \quad \Delta}{\langle \Gamma; \Delta \rangle} \end{array} \quad \begin{array}{c} \text{entropy} \\ \frac{\Gamma}{\Gamma'} \quad (\text{for } \Gamma' \preceq \Gamma) \end{array} \quad \begin{array}{c} \text{cut} \\ \frac{[\Gamma, A]}{[\Gamma, \Delta]} \end{array} \quad \begin{array}{c} \frac{[\Gamma, A]}{[A^{\perp}, \Delta]} \\ \frac{[A^{\perp}, \Delta]}{[\Gamma, \Delta]} \end{array} \\
\begin{array}{c} \text{⊗-intro} \\ \frac{\Gamma\{[A, B]\}}{\Gamma\{A \otimes B\}} \end{array} \quad \begin{array}{c} \text{←-intro} \\ \frac{\Gamma\{\langle A; B \rangle\}}{\Gamma\{A \triangleleft B\}} \end{array} \quad \begin{array}{c} \text{⊗-intro} \\ \frac{[\Gamma, A]}{[\Gamma, \Delta, A \otimes B]} \end{array}
$$

<caption>FIGURE 16. Retoré's sequent calculus, as presented in [Ret21, Figure 1]</caption>

$$
\begin{array}{c} \text{cut} \\ \frac{\pi_1 \text{ (below)} \qquad \pi_2 \text{ (below)}}{[a \otimes (c \triangleleft b^{\perp}), a^{\perp} \triangleleft f, c^{\perp} \triangleleft (e^{\perp} \triangleleft f^{\perp}), e \triangleleft b] \qquad [c \triangleleft (e \triangleleft f), c^{\perp} \triangleleft d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp})]} \\ \text{where } \pi_1 = \frac{\begin{array}{c} \text{axiom} \\ \frac{[a, a^{\perp}]}{\Gamma} \end{array}}{\begin{array}{c} \text{⊗-intro} \\ \frac{[a \otimes (c \triangleleft b^{\perp}), a^{\perp}, \langle c^{\perp}; e^{\perp} \rangle, \langle e; b \rangle]}{\Gamma} \end{array}} \qquad \frac{\begin{array}{c} \text{(axioms + dimix)} \\ \frac{\langle [c, c^{\perp}]; [e, e^{\perp}]; [b, b^{\perp}] \rangle}{[\langle c; b^{\perp} \rangle, \langle c^{\perp}; e^{\perp} \rangle; \langle e; b \rangle]} \end{array}}{\begin{array}{c} \text{entropy} \\ \frac{[c \triangleleft b^{\perp}, \langle c^{\perp}; e^{\perp} \rangle; \langle e; b \rangle]}{\Gamma} \end{array}} \qquad \frac{\begin{array}{c} \text{axiom} \\ \frac{[f, f^{\perp}]}{\Gamma} \end{array}}{\begin{array}{c} \text{dimix} \\ \frac{\begin{array}{c} \text{entropy} \\ \frac{\langle [a \otimes (c \triangleleft b^{\perp}), a^{\perp}, \langle c^{\perp}; e^{\perp} \rangle, \langle e; b \rangle]; [f, f^{\perp}] \rangle}{[a \otimes (c \triangleleft b^{\perp}), \langle a^{\perp}; f \rangle, \langle c^{\perp}; e^{\perp}; f^{\perp} \rangle, \langle e; b \rangle]} \end{array}}{\text{⊗-intro} \times 4 \frac{[a \otimes (c \triangleleft b^{\perp}), a^{\perp} \triangleleft f, c^{\perp} \triangleleft (e^{\perp} \triangleleft f^{\perp}), e \triangleleft b]}{\Gamma}} \end{array}} \end{array}
$$
$$
\text{and } \pi_2 = \frac{\begin{array}{c} \text{axiom} \\ \frac{[c, c^{\perp}]}{\Gamma} \end{array}}{\begin{array}{c} \text{dimix} \\ \frac{\begin{array}{c} \text{entropy} \\ \frac{\langle [c, c^{\perp}]; [e \triangleleft f, d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp})] \rangle}{[\langle c; e \triangleleft f \rangle, \langle c^{\perp}; d^{\perp} \rangle, d \otimes (e^{\perp} \triangleleft f^{\perp})]} \end{array}}{\text{⊗-intro} \times 2 \frac{[c \triangleleft (e \triangleleft f), c^{\perp} \triangleleft d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp})]}{\Gamma}} \end{array}} \qquad \frac{\begin{array}{c} \text{axiom} \\ \frac{[e \triangleleft f, e^{\perp} \triangleleft f^{\perp}]}{[d, d^{\perp}]} \end{array}}{\begin{array}{c} \text{axiom} \\ \frac{[d, d^{\perp}, d \otimes (e^{\perp} \triangleleft f^{\perp})]}{\Gamma} \end{array}}
$$

<caption>FIGURE 17. Proof of the formula from Figure 5 in Retoré's sequent calculus with cuts.</caption>

The corresponding formula of the sequent above has been shown to be provable in BV in
Figure 5, and its cographic RB-prenet may be found in [Ret21, Figure 10].

**Proposition 5.1** (Retoré & Straßburger [Ret21, Proposition 5]). *The sequent in (5.2) is not provable in Retoré's sequent calculus without cuts.*

The reason for this lies in the fact that in order to have a cut-free sequent proof, the
⊗-rule has to be applied to one of the two ⊗-formulas eventually. But the ⊗-rule is too
weak to split the context correctly. However, with cut, the sequent is provable, as shown in
Figure 17. We have therefore shown the following.

**Corollary 5.2.** *Cut-elimination does not hold for Retoré's sequent calculus.*
<figure><img src="image_30.png" /><figcaption>FIGURE 16. Retoré's sequent calculus, as presented in [Ret21, Figure 1]</figcaption></figure>

<figure><img src="image_31.png" /><figcaption>FIGURE 17. Proof of the formula from Figure 5 in Retoré's sequent calculus with cuts.</figcaption></figure>

The corresponding formula of the sequent above has been shown to be provable in BV in Figure 5, and its cographic RB-prenet may be found in [Ret21, Figure 10].

**Proposition 5.1** (Retoré & Straßburger [Ret21, Proposition 5]). The sequent in (5.2) is not provable in Retoré's sequent calculus without cuts.

The reason for this lies in the fact that in order to have a cut-free sequent proof, the ⊗-rule has to be applied to one of the two ⊗-formulas eventually. But the ⊗-rule is too weak to split the context correctly. However, with cut, the sequent is provable, as shown in Figure 17. We have therefore shown the following.

**Corollary 5.2.** *Cut-elimination does not hold for Retoré's sequent calculus.*
Let us now establish the equivalence between SBV and the sequent calculus in Figure 16. For this, we resort again to SBVu (see Proposition 2.69). We begin by showing that every formula that is provable in SBVu is also provable in Retoré's sequent calculus with cut.

**Lemma 5.3.** Let $[A, B]$ and $[C, D]$ be provable sequents. Then the sequents $[A \succ C, B \otimes D]$ and $[A \triangleleft C, B \triangleleft D]$ are also provable.

*Proof.* The following derivations work:

$$ \begin{array}{c} \begin{array}{c} \otimes\text{-intro} \\ \rightleftharpoons\text{-intro} \end{array} \quad \frac{\begin{array}{c} [A, B] \\ [A, C, B \otimes D] \end{array}}{\begin{array}{c} [C, D] \\ [A \succ C, B \otimes D] \end{array}} \quad \begin{array}{c} \text{dimix} \\ \text{entropy} \\ \rightleftharpoons\text{-intro} \\ \rightleftharpoons\text{-intro} \end{array} \quad \frac{\begin{array}{c} [A, B] \\ \langle [A, B]; [C, D] \rangle \\ [\langle A; C \rangle, \langle B; D \rangle] \\ [A \triangleleft C, \langle B; D \rangle] \\ [A \triangleleft C, B \triangleleft D] \end{array}}{\begin{array}{c} [C, D] \\ \langle [A, B]; [C, D] \rangle \\ [\langle A; C \rangle, \langle B; D \rangle] \\ [A \succ C, \langle B; D \rangle] \\ [A \triangleleft C, B \triangleleft D] \end{array}} \end{array} $$

For the derivation on the right, the validity of the entropy rule depends on an inclusion between series-parallel orders which can be mechanically verified. $\square$

**Lemma 5.4** (Non-atomic identity). For any formula $A$, the sequent $[A^{\perp}, A]$ is provable.

**Lemma 5.5.** Let $A$ and $B$ be formulas such that $[A^{\perp}, B]$ is provable, and $S\{\cdot\}$ be a context. Then $[S\{A\}^{\perp}, S\{B\}]$ is provable.

*Proof of Lemmas 5.4 and 5.5.* We prove that the following holds for any formula $A$:

(i) $[A^{\perp}, A]$ is provable;

(ii) for any formulas $B$ and $C$ such that $[B^{\perp}, C]$ is provable and any $\odot \in \{\otimes, \succ, \triangleleft\}$, the sequents $[(A \odot B)^{\perp}, A \odot C]$ and $[(B \odot A)^{\perp}, C \odot A]$ are provable.

Lemma 5.4 corresponds to item (i), while item (ii) entails Lemma 5.5 by a routine induction on the context $S\{\cdot\}$. The following observations suffice to prove (i) and (ii) simultaneously by induction on $A$ (invoking the axiom rule for the base case):

* for any given $A$, (i) implies (ii) as a direct consequence of Lemma 5.3;

* if $A$ satisfies (i) and $A'$ satisfies (ii), then by applying (ii) to $A'$ with $B = C = A$, we see that for any $\odot \in \{\otimes, \succ, \triangleleft\}$, the formula $A \odot A'$ satisfies (i). $\square$

**Lemma 5.6.** Let $\overline{A/B}$ be an instance of an inference rule in SBVu. With Then $[A^{\perp}, B]$ is provable in Retoré's sequent calculus without cuts.

*Proof.* Let us consider for instance the switch rule. We start by considering the case with atomic formulas $a, b, c$ and a trivial context $(S\{\cdot\} = \{\cdot\})$:

$$ s \frac{[a \succ c] \otimes b}{(a \otimes b) \succ c} $$

We prove the corresponding sequent (for the switch rule, the derivation involves only flat sequents and can therefore be carried out in MLL+mix):

$$ \begin{array}{c} \begin{array}{c} \overline{[a^{\perp}, a]} \\ \overline{[a^{\perp}, b^{\perp}, a \otimes b]} \end{array} & \begin{array}{c} \overline{[b^{\perp}, b]} \\ \overline{[c^{\perp}, c]} \end{array} \\ \begin{array}{c} \overline{[a^{\perp} \otimes c^{\perp}, b^{\perp}, a \otimes b, c]} \\ \overline{[a^{\perp} \otimes c^{\perp}, b^{\perp}, (a \otimes b) \succ c]} \end{array} & \overline{[(a^{\perp} \otimes c^{\perp}) \succ b^{\perp}, (a \otimes b) \succ c]} \end{array} $$
Thanks to Lemma 5.4, we can substitute formulas for atoms: for any A, B and C, the sequent [$(A^{\perp} \otimes C^{\perp}) \otimes B^{\perp}$, $(A \otimes B) \otimes C$] can be proved using the above derivation where axioms are replaced by appropriate subproofs of $[A^{\perp}, A]$, $[B^{\perp}, B]$ or $[C^{\perp}, C]$. Then, using Lemma 5.5, we may conclude that $[S\{[A \otimes C] \otimes B\}^{\perp}, S\{(A \otimes B) \otimes C\}]$ is provable for any context $S\{\cdot\}$.

This argument applies to all inference rules (except $a^i \vdash$, which has no premise, and therefore does not fit the pattern in the lemma statement). For each of these rules, it therefore suffices to treat the case with atomic formulas and trivial context.

For the $\equiv'$-rule, we can assume without loss of generality that each instance is an application of exactly one of the equalities in (2.5) (as each general instance of the $\equiv'$-rule can be replaced by a finite sequence of these special instances).

We have thus reduced the desired conclusion to a bounded search for cut-free proofs that we leave to the reader. □

**Theorem 5.7.** If a formula is provable in SBVu then it is also provable in Retoré's sequent calculus with cuts.

*Proof.* A proof of a formula A in SBVu must have the form

$$ \begin{array}{c} a^i \vdash \\ r_1 \frac{a \otimes a^{\perp}}{B_1} \\ r_2 \frac{\vdots}{B_n} \\ r_n \end{array} $$

where $B_n = A$; we also define $B_0 = a \otimes a^{\perp}$. For $i \in \{1, \dots, n\}$, the sequent $[B_{i-1}^{\perp}, B_i]$ is provable in Retoré's sequent calculus by Lemma 5.6. Furthermore, $a \otimes a^{\perp}$ also has a sequent calculus proof (an axiom rule followed by a $\otimes$-intro). By composing all these sequent proofs with the cut rule, one gets a proof of A. □

For the converse, observe that the axiom, dimix and $\otimes/\lhd$-intro rules are easy to simulate in BVu. The treatment of $\otimes$-intro is as usual (see [Str03b, Section 3.3.] or [Gug07, §5] for example), and cut is a $\otimes$-intro followed by $i\uparrow$ (which is admissible in SBVu). Furthermore, it is an immediate consequence of Theorem 2.77 that SBVu can also simulate the entropy rule. This is enough to prove the following theorem:

**Theorem 5.8.** If a sequent $\Gamma$ is provable in Retoré's sequent calculus with cuts, then a formula A that corresponds (see Definition 2.8) to $\Gamma$ is provable in SBVu.

**Corollary 5.9.** Retoré's sequent calculus with cuts is equivalent to BV.

**5.2. A Refinement of Tiu's Argument.** In [Tiu06], Tiu presents a sequence of formulas $S_0, S_1, S_2, \dots$ with the following properties:

(1) For each $n$, the formula $S_n$ is provable in BV.

(2) In order to prove $S_n$, a subformula at depth $2n$ has to be accessed first.

From this it follows, that there can be no *shallow* (i.e., all inference rules have a fixed maximum depth) cut-free proof system equivalent to BV. As most standard sequent calculi are shallow in that sense, the argument could be used to claim that there cannot be a "standard" cut-free sequent calculus for BV. However, Tiu's formulas also have the property
Thanks to Lemma 5.4, we can substitute formulas for atoms: for any A, B and C, the sequent [$(A^{\perp} \otimes C^{\perp}) \otimes B^{\perp}$, $(A \otimes B) \otimes C$] can be proved using the above derivation where axioms are replaced by appropriate subproofs of $[A^{\perp}, A]$, $[B^{\perp}, B]$ or $[C^{\perp}, C]$. Then, using Lemma 5.5, we may conclude that $[S\{[A \otimes C] \otimes B\}^{\perp}, S\{(A \otimes B) \otimes C\}]$ is provable for any context $S\{\cdot\}$.

This argument applies to all inference rules (except $a^i \vdash$, which has no premise, and therefore does not fit the pattern in the lemma statement). For each of these rules, it therefore suffices to treat the case with atomic formulas and trivial context.

For the $\equiv'$-rule, we can assume without loss of generality that each instance is an application of exactly one of the equalities in (2.5) (as each general instance of the $\equiv'$-rule can be replaced by a finite sequence of these special instances).

We have thus reduced the desired conclusion to a bounded search for cut-free proofs that we leave to the reader. □

**Theorem 5.7.** If a formula is provable in SBVu then it is also provable in Retoré's sequent calculus with cuts.

*Proof.* A proof of a formula A in SBVu must have the form

$$ \begin{array}{c} a^i \vdash \\ r_1 \frac{a \otimes a^{\perp}}{B_1} \\ r_2 \frac{\vdots}{B_n} \\ r_n \frac{\vdots}{B_n} \end{array} $$

where $B_n = A$; we also define $B_0 = a \otimes a^{\perp}$. For $i \in \{1, \dots, n\}$, the sequent $[B_{i-1}^{\perp}, B_i]$ is provable in Retoré's sequent calculus by Lemma 5.6. Furthermore, $a \otimes a^{\perp}$ also has a sequent calculus proof (an axiom rule followed by a $\otimes$-intro). By composing all these sequent proofs with the cut rule, one gets a proof of A. □

For the converse, observe that the axiom, dimix and $\otimes/\nolimits$-intro rules are easy to simulate in BVu. The treatment of $\otimes$-intro is as usual (see [Str03b, Section 3.3.] or [Gug07, §5] for example), and cut is a $\otimes$-intro followed by $i\uparrow$ (which is admissible in SBVu). Furthermore, it is an immediate consequence of Theorem 2.77 that SBVu can also simulate the entropy rule. This is enough to prove the following theorem:

**Theorem 5.8.** If a sequent $\Gamma$ is provable in Retoré's sequent calculus with cuts, then a formula A that corresponds (see Definition 2.8) to $\Gamma$ is provable in SBVu.

**Corollary 5.9.** Retoré's sequent calculus with cuts is equivalent to BV.

**5.2. A Refinement of Tiu's Argument.** In [Tiu06], Tiu presents a sequence of formulas $S_0, S_1, S_2, \dots$ with the following properties:

(1) For each $n$, the formula $S_n$ is provable in BV.

(2) In order to prove $S_n$, a subformula at depth $2n$ has to be accessed first.

From this it follows, that there can be no *shallow* (i.e., all inference rules have a fixed maximum depth) cut-free proof system equivalent to BV. As most standard sequent calculi are shallow in that sense, the argument could be used to claim that there cannot be a "standard" cut-free sequent calculus for BV. However, Tiu's formulas also have the property
(3) For each $n$, the formula $S_n$ is $\otimes$-free.

Since every $S_n$ contains only the $\mathcal{R}$ and $\triangleleft$ connectives, it can be proved in Retoré's calculus by first applying the $\mathcal{R}$ and $\triangleleft$ rules to transform the formula into a sequent with only atomic formulas. This sequent can then be derived from the axioms by only dimix instances and a single instance of the entropy rule.

This is not a contradiction, as the entropy rule is a deep rule (i.e., not shallow) in the sense above.<fnref n="22" /> However, it raises the question whether we can have a refinement of Retoré's sequent calculus that is complete for BV and obeys cut elimination, as this is no longer ruled out by Tiu's argument.

What we will show next is a sequence or formulas $R_0, R_1, R_2, \dots$, following the spirit of Tiu's construction, having properties (1) and (2) above, but not (3). Consequently, for proving them, a $\otimes$-subformula has to be accessed at arbitrary depth, without the possibility of globally splitting the context. This entails that a proper deep inference system is indeed needed, and a proof system in the sequent calculus layout is insufficient.

We start with the index set $I = \{0, 1\}^*$, i.e., the set of all finite words with the symbols 0 and 1. Then, our formulas are build from the propositional variables $\{a, b, c, y, z\} \times I$, written as $a_i$ with $i \in I$.

For an index $i \in I$ and two formulas $A$ and $B$, we define now inductively the formula $\xi_n(i, A, B)$ for each $n \in \mathbb{N}$:

$$ \xi_0(i, A, B) = ([a_i \mathcal{R} b_i \mathcal{R} A] \otimes y_i) \mathcal{R} \langle y_i^{\perp} \triangleleft c_i \rangle \mathcal{R} \langle a_i^{\perp} \triangleleft z_i \rangle \mathcal{R} (z_i^{\perp} \otimes [b_i^{\perp} \mathcal{R} c_i^{\perp} \mathcal{R} B]) $$

$$ \xi_{n+1}(i, A, B) = (\xi_n(i0, a_i, b_i \mathcal{R} A) \otimes y_i) \mathcal{R} \langle y_i^{\perp} \triangleleft c_i \rangle \mathcal{R} \langle a_i^{\perp} \triangleleft z_i \rangle \mathcal{R} (z_i^{\perp} \otimes \xi_n(i1, b_i^{\perp}, c_i^{\perp} \mathcal{R} B)) $$

We now define $R_n = \xi_n(0, \mathbb{I}, \mathbb{I})$.<fnref n="23" /> These formulas have the following properties:

**Claim 5.10.** For each $n$, the formula $R_n$ is provable in BV.

$$ A \mathcal{R} B $$

*Proof.* For every $n \in \mathbb{N}$ and $i \in I$, we have a derivation $\parallel \xi_n(i, A, B)$. This is constructed in the same way as in the proof of Lemma 7.4 in [Tiu06], using a derivation that is similar to the one in Figure 5. $\square$

**Claim 5.11.** The formulas $R_n$ are not provable in Retoré's sequent calculus without cuts.

*Proof.* The formula $R_0$ is a variation of the corresponding formula of the sequent (5.2), and the same argument applies. $\square$

Finally, we have:

**Claim 5.12.** A deep proof system is needed to prove the formulas $R_n$.

*Proof.* This is proved by the same argument as in [Tiu06]. In order to prove $R_n$, a $\otimes$ at depth $2n$ has to be accessed first, in order to remove the variable $y_i$ (or $z_i$) with an atomic interaction. $\square$

This strengthens Tiu's argument by using formulas involving also a $\otimes$, showing that rules like entropy are not enough to obtain a cut-free sequent style calculus for BV.

<footnote n="22">²²Technically speaking, the $\mathcal{R}$-intro and the $\triangleleft$-into rules are also deep in that sense, but they do not chance the RB-digraph associated to the sequent proof.</footnote>

<footnote n="23">²³The reader familiar with [Tiu06] might note that the only difference between our $\xi_n$ and Tiu's $\alpha_n$ is the addition of the variables $y_i$ and $z_i$ via the $\otimes$. In fact, $\xi_n$ can be derived from $\alpha_n$, but not the other way around.</footnote>
(3) For each $n$, the formula $S_n$ is $\otimes$-free.

Since every $S_n$ contains only the $\mathcal{S}$ and $\triangleleft$ connectives, it can be proved in Retoré's calculus by first applying the $\mathcal{S}$ and $\triangleleft$ rules to transform the formula into a sequent with only atomic formulas. This sequent can then be derived from the axioms by only dimix instances and a single instance of the entropy rule.

This is not a contradiction, as the entropy rule is a deep rule (i.e., not shallow) in the sense above.<fnref n="22" /> However, it raises the question whether we can have a refinement of Retoré's sequent calculus that is complete for BV and obeys cut elimination, as this is no longer ruled out by Tiu's argument.

What we will show next is a sequence or formulas $R_0, R_1, R_2, \dots$, following the spirit of Tiu's construction, having properties (1) and (2) above, but not (3). Consequently, for proving them, a $\otimes$-subformula has to be accessed at arbitrary depth, without the possibility of globally splitting the context. This entails that a proper deep inference system is indeed needed, and a proof system in the sequent calculus layout is insufficient.

We start with the index set $I = \{0, 1\}^*$, i.e., the set of all finite words with the symbols 0 and 1. Then, our formulas are build from the propositional variables $\{a, b, c, y, z\} \times I$, written as $a_i$ with $i \in I$.

For an index $i \in I$ and two formulas $A$ and $B$, we define now inductively the formula $\xi_n(i, A, B)$ for each $n \in \mathbb{N}$:

$$ \xi_0(i, A, B) = ([a_i \mathcal{S} b_i \mathcal{S} A] \otimes y_i) \mathcal{S} \langle y_i^{\perp} \triangleleft c_i \rangle \mathcal{S} \langle a_i^{\perp} \triangleleft z_i \rangle \mathcal{S} (z_i^{\perp} \otimes [b_i^{\perp} \mathcal{S} c_i^{\perp} \mathcal{S} B]) $$

$$ \xi_{n+1}(i, A, B) = (\xi_n(i0, a_i, b_i \mathcal{S} A) \otimes y_i) \mathcal{S} \langle y_i^{\perp} \triangleleft c_i \rangle \mathcal{S} \langle a_i^{\perp} \triangleleft z_i \rangle \mathcal{S} (z_i^{\perp} \otimes \xi_n(i1, b_i^{\perp}, c_i^{\perp} \mathcal{S} B)) $$

We now define $R_n = \xi_n(0, \mathbb{I}, \mathbb{I})$.<fnref n="23" /> These formulas have the following properties:

**Claim 5.10.** For each $n$, the formula $R_n$ is provable in BV.

$$ A \mathcal{S} B $$

*Proof.* For every $n \in \mathbb{N}$ and $i \in I$, we have a derivation $\parallel \xi_n(i, A, B)$. This is constructed in the same way as in the proof of Lemma 7.4 in [Tiu06], using a derivation that is similar to the one in Figure 5. $\square$

**Claim 5.11.** The formulas $R_n$ are not provable in Retoré's sequent calculus without cuts.

*Proof.* The formula $R_0$ is a variation of the corresponding formula of the sequent (5.2), and the same argument applies. $\square$

Finally, we have:

**Claim 5.12.** A deep proof system is needed to prove the formulas $R_n$.

*Proof.* This is proved by the same argument as in [Tiu06]. In order to prove $R_n$, a $\otimes$ at depth $2n$ has to be accessed first, in order to remove the variable $y_i$ (or $z_i$) with an atomic interaction. $\square$

This strengthens Tiu's argument by using formulas involving also a $\otimes$, showing that rules like entropy are not enough to obtain a cut-free sequent style calculus for BV.

<footnote n="22">²²Technically speaking, the $\mathcal{S}$-intro and the $\triangleleft$-into rules are also deep in that sense, but they do not chance the RB-digraph associated to the sequent proof.</footnote>

<footnote n="23">²³The reader familiar with [Tiu06] might note that the only difference between our $\xi_n$ and Tiu's $\alpha_n$ is the addition of the variables $y_i$ and $z_i$ via the $\otimes$. In fact, $\xi_n$ can be derived from $\alpha_n$, but not the other way around.</footnote>
**Remark 5.13.** However, Acclavio [Acc23] proposes a sequent system for a graphical logic (see also Section 6.1.5) that includes a “deep” tensor rule, that in our setting would have the following shape:

$$ \textcircled{\text{intro}}' \frac{[\Gamma, A] \quad [\Delta\{B\}]}{[\Gamma, \Delta\{A \otimes B\}]} $$

With this rule, [Acc23] shows cut elimination in the sequent calculus for a logic that before had only a deep inference proof system. Naturally, we conjecture that something similar might be possible for BV, but exploring this would have gone beyond the scope of this paper.

**5.3. A Complexity-Theoretic Obstacle to Sequent Calculi for Pomset Logic.** Let us now turn to pomset logic. We propose here a similar (and somewhat informal) complexity-theoretic explanation for why a cut-free sequent calculus for pomset logic is difficult to find, similar to Remark 4.12.

As described in [Ret21, Section 5], the origins of pomset logic in the coherence space semantics of linear logic suggest that $\triangleleft$ is meant to be a *multiplicative* connective, just like the multiplicative conjunction $\otimes$ and the multiplicative disjunction $\ominus$ (which give their names to the fragments MLL and MLL+mix of linear logic). Therefore, we would like to leverage some proof-theoretic property related to multiplicative connectives. Recall that the standard sequent calculus rules for $\otimes$ and for its *additive* counterpart & correspond to two possible introduction rules for the conjunction $\wedge$ in classical logic, respectively:

$$ \frac{\vdash \Gamma, A \quad \vdash \Delta, B \quad \vdash \Gamma, A \quad \vdash \Delta, A \wedge B}{\vdash \Gamma, \Delta, A \wedge B} \quad \text{and} \quad \frac{\vdash \Gamma, A \quad \vdash \Gamma, B \quad \vdash \Gamma, A \wedge B}{\vdash \Gamma, A \wedge B} $$

The difference is that the multiplicative rule *splits the context of the conclusion into disjoint parts among the premises* while the additive rule copies the same context in both premises. The same kind of management of the context occurs in the rules for the so-called “generalized multiplicative connectives” in the French-Italian linear logic tradition [DR89, AM20]. This leads us to the following definition.

**Definition 5.14.** A *multiplicative introduction rule* for an $n$-ary connective $\Phi$ is a rule whose instances obey the following property: there exist formulas $A_1, \dots, A_n$ and a multiset of formulas $M$ such that

* the multiset of formulas occurring in the premises — i.e. the sum of the multisets of formulas in each premise — is equal to$^{24}$ $\{A_1, \dots, A_n\} + M$;

* the multiset of formulas occurring in the conclusion equals $\Phi(A_1, \dots, A_n) + M$.

A *multiplicative structural rule* is one in which the premises (taken together) and the conclusion have the same formulas, taking multiplicity into account; this is an equality of multisets similar to the above.

A sequent calculus is *multiplicative* when all its rules are either an axiom rule, a multiplicative introduction rule or a multiplicative structural rule.

For this to make sense, there must be a way to associate to a sequent its multiset of formulas. This works both for flat sequents — which are already multisets — and for ordered sequents, and other kinds of generalized sequents are conceivable. The standard MLL+mix sequent calculus, as well as Retoré's calculus in the previous section and Slavnov's calculus in the next one, are all multiplicative.

<footnote>$^{24}$We abusively use the notation $\{\dots\}$ for a multiset rather than a set here.</footnote>
**Remark 5.13.** However, Acclavio [Acc23] proposes a sequent system for a graphical logic (see also Section 6.1.5) that includes a “deep” tensor rule, that in our setting would have the following shape:

$$ \textcircled{\text{intro}}' \frac{[\Gamma, A] \quad [\Delta\{B\}]}{[\Gamma, \Delta\{A \otimes B\}]} $$

With this rule, [Acc23] shows cut elimination in the sequent calculus for a logic that before had only a deep inference proof system. Naturally, we conjecture that something similar might be possible for BV, but exploring this would have gone beyond the scope of this paper.

**5.3. A Complexity-Theoretic Obstacle to Sequent Calculi for Pomset Logic.** Let us now turn to pomset logic. We propose here a similar (and somewhat informal) complexity-theoretic explanation for why a cut-free sequent calculus for pomset logic is difficult to find, similar to Remark 4.12.

As described in [Ret21, Section 5], the origins of pomset logic in the coherence space semantics of linear logic suggest that $\triangleleft$ is meant to be a *multiplicative* connective, just like the multiplicative conjunction $\otimes$ and the multiplicative disjunction $\ominus$ (which give their names to the fragments MLL and MLL+mix of linear logic). Therefore, we would like to leverage some proof-theoretic property related to multiplicative connectives. Recall that the standard sequent calculus rules for $\otimes$ and for its *additive* counterpart & correspond to two possible introduction rules for the conjunction $\wedge$ in classical logic, respectively:

$$ \frac{\vdash \Gamma, A \quad \vdash \Delta, B}{\vdash \Gamma, \Delta, A \wedge B} \quad \text{and} \quad \frac{\vdash \Gamma, A \quad \vdash \Gamma, B}{\vdash \Gamma, A \wedge B} $$

The difference is that the multiplicative rule *splits the context of the conclusion into disjoint parts among the premises* while the additive rule copies the same context in both premises. The same kind of management of the context occurs in the rules for the so-called “generalized multiplicative connectives” in the French-Italian linear logic tradition [DR89, AM20]. This leads us to the following definition.

**Definition 5.14.** A *multiplicative introduction rule* for an $n$-ary connective $\Phi$ is a rule whose instances obey the following property: there exist formulas $A_1, \dots, A_n$ and a multiset of formulas $M$ such that

* the multiset of formulas occurring in the premises — i.e. the sum of the multisets of formulas in each premise — is equal to$^{24}$ $\{A_1, \dots, A_n\} + M$;

* the multiset of formulas occurring in the conclusion equals $\Phi(A_1, \dots, A_n) + M$.

A *multiplicative structural rule* is one in which the premises (taken together) and the conclusion have the same formulas, taking multiplicity into account; this is an equality of multisets similar to the above.

A sequent calculus is *multiplicative* when all its rules are either an axiom rule, a multiplicative introduction rule or a multiplicative structural rule.

For this to make sense, there must be a way to associate to a sequent its multiset of formulas. This works both for flat sequents — which are already multisets — and for ordered sequents, and other kinds of generalized sequents are conceivable. The standard MLL+mix sequent calculus, as well as Retoré's calculus in the previous section and Slavnov's calculus in the next one, are all multiplicative.

<footnote>$^{24}$We abusively use the notation $\{\dots\}$ for a multiset rather than a set here.</footnote>
The relevance of this notion to us is a consequence in the spirit of proof complexity:

**Claim 5.15.** In a proof in a multiplicative sequent calculus, the total number of introduction rules is at most the total size of the formulas in the sequent being proved.

In many cases, there will also be a bound on the structural rules in proofs. For instance, the number of uses of multiplicative structural rules that require two or more premises, such as the mix rule, is also linearly bounded by the size of the conclusion formulas. Thus the following informal principle: a multiplicative sequent calculus with “reasonable” structural rules admits proofs with a polynomial number of inference rules.<fnref n="25" />

We also expect the correctness of these proofs to hinge only on the local validity of their inferences (unlike proof nets, whose global correctness criterion makes them hard to check). According to a similar reasoning as Remark 4.12, then, if such a multiplicative calculus were to capture pomset logic, it would be impossible to verify its inference rules in time polynomial in the size of the formulas, unless $NP = coNP$. This is arguably a strong restriction on the design of sequent calculi for pomset logic, such as the calculus in the next section.

**5.4. A Reconstruction of Slavnov's Calculus.** Let us now revisit the sound and complete proof system of [Sla19] for pomset logic in light of our above remarks. It uses *decorated sequents*, which are flat sequents (multisets of formulas) endowed with additional “decorations” (analogously to how Retoré's sequents can be seen as flat sequents decorated with series-parallel orders). The point is that in Slavnov's sequents, these decorations (defined in Definition 5.16 below) take up most of the space; their size may be *exponentially bigger* than the number of formulas in the sequent. This provides a good reason for inference rule checking to be superpolynomial in the total size of formulas — this is indeed necessary since this sequent calculus is, as we shall see, multiplicative and “reasonable” in the above sense.

For the sake of completeness, we describe briefly here Slavnov's system, specialized to pomset logic. The paper [Sla19] also introduces and deals with a related but different extension of MLL called “semicommutative MLL”, and it derives its sequent calculus for pomset logic from the one for semicommutative MLL. Our exposition avoids this detour. We also aim at giving a high-level idea of what makes the system work. We decompose our presentation of the system into three “levels” (inspired by the two-level treatment of [Sla19]).

**First level: preproofs on flat sequents.** First, consider the “old-fashioned” calculus on flat sequents whose rules are as follows:

$$ \text{axiom} \quad \frac{[a, a^{\perp}]}{\text{mix} \frac{\Gamma \quad \Delta}{[\Gamma, \Delta]}} \quad \text{\textcircled{3}} \quad \frac{[\Gamma, A] \quad [\Delta, B]}{[\Gamma, \Delta, A \otimes B]} \quad \text{\textcircled{4}} \quad \frac{[\Gamma, A, B]}{[\Gamma, A \odot B]} \quad \text{for } \odot \in \{\text{\textasciitilde}, \text{\textasciitilde} \} $$

In other words, this system extends the usual cut-free sequent calculus for MLL+mix with an introduction rule for $\langle \rangle$ which is exactly the same as for $\mathcal{G}$. Let us call *Slavnov pre-proofs* the derivation trees using these rules. Obviously, some formulas that are not valid in pomset logic, such as $(a \otimes b) \mathcal{G}$ $(a^{\perp} \langle \rangle b^{\perp})$, may admit Slavnov pre-proofs.

An important observation is that there is a canonical map from Slavnov pre-proofs to tree-like RB-prenets that preserves the conclusion sequent. It can be defined inductively by interpreting each of the inference rules as an operation on proof nets in the obvious way; for

<footnote n="25">²⁵This also applies to the *graphical proof system* of [AHS20, AHS22] that works on general graphs instead of cographs (which correspond to formulas, as discussed in Section 6.1.5).</footnote>
The relevance of this notion to us is a consequence in the spirit of proof complexity:

**Claim 5.15.** In a proof in a multiplicative sequent calculus, the total number of introduction rules is at most the total size of the formulas in the sequent being proved.

In many cases, there will also be a bound on the structural rules in proofs. For instance, the number of uses of multiplicative structural rules that require two or more premises, such as the mix rule, is also linearly bounded by the size of the conclusion formulas. Thus the following informal principle: a multiplicative sequent calculus with “reasonable” structural rules admits proofs with a polynomial number of inference rules.<fnref n="25" />

We also expect the correctness of these proofs to hinge only on the local validity of their inferences (unlike proof nets, whose global correctness criterion makes them hard to check). According to a similar reasoning as Remark 4.12, then, if such a multiplicative calculus were to capture pomset logic, it would be impossible to verify its inference rules in time polynomial in the size of the formulas, unless $NP = coNP$. This is arguably a strong restriction on the design of sequent calculi for pomset logic, such as the calculus in the next section.

**5.4. A Reconstruction of Slavnov's Calculus.** Let us now revisit the sound and complete proof system of [Sla19] for pomset logic in light of our above remarks. It uses *decorated sequents*, which are flat sequents (multisets of formulas) endowed with additional “decorations” (analogously to how Retoré's sequents can be seen as flat sequents decorated with series-parallel orders). The point is that in Slavnov's sequents, these decorations (defined in Definition 5.16 below) take up most of the space; their size may be *exponentially bigger* than the number of formulas in the sequent. This provides a good reason for inference rule checking to be superpolynomial in the total size of formulas — this is indeed necessary since this sequent calculus is, as we shall see, multiplicative and “reasonable” in the above sense.

For the sake of completeness, we describe briefly here Slavnov's system, specialized to pomset logic. The paper [Sla19] also introduces and deals with a related but different extension of MLL called “semicommutative MLL”, and it derives its sequent calculus for pomset logic from the one for semicommutative MLL. Our exposition avoids this detour. We also aim at giving a high-level idea of what makes the system work. We decompose our presentation of the system into three “levels” (inspired by the two-level treatment of [Sla19]).

**First level: preproofs on flat sequents.** First, consider the “old-fashioned” calculus on flat sequents whose rules are as follows:

$$ \begin{array}{c} \text{axiom} \\ \underline{[a, a^{\perp}]} \end{array} \quad \begin{array}{c} \text{mix} \\ \underline{\Gamma, \Delta}} \end{array} \quad \begin{array}{c} \otimes\text{-intro} \\ \underline{[\Gamma, A], [\Delta, B]} \end{array} \quad \begin{array}{c} \odot\text{-intro} \\ \underline{[\Gamma, A \otimes B]} \end{array} \quad \text{for } \odot \in \{\mathcal{G}, \mathcal{L}\} $$

In other words, this system extends the usual cut-free sequent calculus for MLL+mix with an introduction rule for $\mathcal{L}$ which is exactly the same as for $\mathcal{G}$. Let us call *Slavnov pre-proofs* the derivation trees using these rules. Obviously, some formulas that are not valid in pomset logic, such as $(a \otimes b) \mathcal{G} (a^{\perp} \mathcal{L} b^{\perp})$, may admit Slavnov pre-proofs.

An important observation is that there is a canonical map from Slavnov pre-proofs to tree-like RB-prenets that preserves the conclusion sequent. It can be defined inductively by interpreting each of the inference rules as an operation on proof nets in the obvious way; for

<footnote n="25">²⁵This also applies to the *graphical proof system* of [AHS20, AHS22] that works on general graphs instead of cographs (which correspond to formulas, as discussed in Section 6.1.5).</footnote>
instance the ⊗-intro rule corresponds to taking the union of two RB-prenets and adding a gadget for the newly added ⊗ connective (cf. Figure 2).

The goal of the “second level” of the proof system will then be to filter out Slavnov pre-proofs that translate into correct tree-like RB-nets.

(For MLL (resp. MLL+mix) sequent calculus proofs, i.e. Slavnov pre-proofs without the ◁-intro and mix rules (resp. the ◁-intro rule), it is well-known that the result of the translation is a correct MLL (resp. MLL+mix) proof net: in those cases, it corresponds to a “desequentialization” operation whose idea goes back to Girard’s original paper [Gir87].)

**Second level: decorations with “multi-reachability” information.** At this stage, it is natural to add data that keeps track of paths in RB-prenets, in order to reflect the correctness criterion.

**Definition 5.16.** A *decoration* on a flat sequent Γ is a set $\mathfrak{d}$ of sets of ordered pairs of formula occurrences. The pair $(\Gamma, \mathfrak{d})$ is then called a *decorated sequent*.

To each Slavnov pre-proof $\pi$ of a flat sequent Γ, we associate a decoration $\mathfrak{d}_{\pi}$ — and thus the decorated sequent $\mathfrak{S}_{\pi} = (\Gamma, \mathfrak{d}_{\pi})$ — as follows: first translate it into a tree-like RB-prenet $\mathcal{G}$, and then let the set $\{(A_1, B_1), \dots, (A_n, B_n)\} \in \mathfrak{d}_{\pi}$ whenever there exists a family of *pairwise disjoint* æ-paths $(P_i)_{i \in \{1, \dots, n\}}$ such that for each $i$ the path $P_i$ goes from the conclusion vertex of $\mathcal{G}$ corresponding to $A_i$ to the vertex corresponding to $B_i$.

The key property is now:

**Claim 5.17.** The decorated sequent corresponding to a Slavnov-pre-proof is entirely determined by the last rule and the decorated sequents corresponding to the sub-pre-proofs of the premises.

For instance, there exists a function $\mathfrak{F} \otimes$ such that given a proof $\pi$ equal to

$$ \text{⊗-intro} \xrightarrow{\substack{\pi_1 \\ [\Gamma, A]}} \text{⊗-intro} \xrightarrow{\substack{\pi_2 \\ [\Delta, B]}} \substack{[\Gamma, \Delta, A \otimes B]} $$

we have $\mathfrak{S}_{\pi} = \mathfrak{F} \otimes (\mathfrak{S}_{\pi_1}, \mathfrak{S}_{\pi_2}, A, B)$.<fnref n="26" /> To see why this claim holds, observe that a family of disjoint æ-paths between conclusions in the tree-like RB-prenet corresponding to $\pi$ consists of the union of:

* such a family in the prenet for $\pi_1$, not touching $A$;

* such a family in the prenet for $\pi_2$, not touching $B$;

* either the empty set, or a singleton containing one of the following:

- an æ-path between (the vertex for) some formula occurrence in $\Gamma$ and some other in $\Delta$ going through the RB-tree gadget for $A \otimes B$;

- an æ-path from some vertex from either $\Gamma$ or $\Delta$ to the conclusion vertex for $A \otimes B$;

- the reverse of either of the above two possibilities.

An explicit expression for $\mathfrak{F} \otimes$ can be obtained by reasoning along these lines. Similar (simpler) analyses can be carried out for the other connectives, and for the axiom and mix rules.

This allows us to lift each of the previous inference rules on flat sequents to a rule on decorated sequents, for example the decorated version of ⊗-intro would be

$$ \frac{\mathfrak{S} \qquad \mathfrak{S}'}{\mathfrak{F} \otimes (\mathfrak{S}, \mathfrak{S}', A, B)} \qquad \text{where } A \text{ (resp. } B) \text{ is a formula occurrence in } \mathfrak{S} \text{ (resp. } \mathfrak{S}') $$

<footnote n="26">²⁶Strictly speaking, the two last arguments point to formula occurrences in the conclusions of $\pi_1, \pi_2$.</footnote>
instance the ⊗-intro rule corresponds to taking the union of two RB-prenets and adding a gadget for the newly added ⊗ connective (cf. Figure 2).

The goal of the “second level” of the proof system will then be to filter out Slavnov pre-proofs that translate into correct tree-like RB-nets.

(For MLL (resp. MLL+mix) sequent calculus proofs, i.e. Slavnov pre-proofs without the ◁-intro and mix rules (resp. the ◁-intro rule), it is well-known that the result of the translation is a correct MLL (resp. MLL+mix) proof net: in those cases, it corresponds to a “desequentialization” operation whose idea goes back to Girard’s original paper [Gir87].)

**Second level: decorations with “multi-reachability” information.** At this stage, it is natural to add data that keeps track of paths in RB-prenets, in order to reflect the correctness criterion.

**Definition 5.16.** A *decoration* on a flat sequent Γ is a set $\mathfrak{d}$ of sets of ordered pairs of formula occurrences. The pair $(\Gamma, \mathfrak{d})$ is then called a *decorated sequent*.

To each Slavnov pre-proof $\pi$ of a flat sequent Γ, we associate a decoration $\mathfrak{d}_{\pi}$ — and thus the decorated sequent $\mathfrak{S}_{\pi} = (\Gamma, \mathfrak{d}_{\pi})$ — as follows: first translate it into a tree-like RB-prenet $\mathcal{G}$, and then let the set $\{(A_1, B_1), \dots, (A_n, B_n)\} \in \mathfrak{d}_{\pi}$ whenever there exists a family of *pairwise disjoint* æ-paths $(P_i)_{i \in \{1, \dots, n\}}$ such that for each $i$ the path $P_i$ goes from the conclusion vertex of $\mathcal{G}$ corresponding to $A_i$ to the vertex corresponding to $B_i$.

The key property is now:

**Claim 5.17.** The decorated sequent corresponding to a Slavnov-pre-proof is entirely determined by the last rule and the decorated sequents corresponding to the sub-pre-proofs of the premises.

For instance, there exists a function $\mathfrak{F} \otimes$ such that given a proof $\pi$ equal to

$$ \otimes\text{-intro} \frac{\frac{\pi_1}{[\Gamma, A]} \quad \frac{\pi_2}{[\Delta, B]}}{[\Gamma, \Delta, A \otimes B]} $$

we have $\mathfrak{S}_{\pi} = \mathfrak{F} \otimes (\mathfrak{S}_{\pi_1}, \mathfrak{S}_{\pi_2}, A, B)$.<fnref n="26" /> To see why this claim holds, observe that a family of disjoint æ-paths between conclusions in the tree-like RB-prenet corresponding to $\pi$ consists of the union of:

* such a family in the prenet for $\pi_1$, not touching $A$;

* such a family in the prenet for $\pi_2$, not touching $B$;

* either the empty set, or a singleton containing one of the following:

- an æ-path between (the vertex for) some formula occurrence in $\Gamma$ and some other in $\Delta$ going through the RB-tree gadget for $A \otimes B$;

- an æ-path from some vertex from either $\Gamma$ or $\Delta$ to the conclusion vertex for $A \otimes B$;

- the reverse of either of the above two possibilities.

An explicit expression for $\mathfrak{F} \otimes$ can be obtained by reasoning along these lines. Similar (simpler) analyses can be carried out for the other connectives, and for the axiom and mix rules.

This allows us to lift each of the previous inference rules on flat sequents to a rule on decorated sequents, for example the decorated version of $\otimes$-intro would be

$$ \frac{\mathfrak{S} \qquad \mathfrak{S}'}{\mathfrak{F} \otimes (\mathfrak{S}, \mathfrak{S}', A, B)} \qquad \text{where } A \text{ (resp. } B) \text{ is a formula occurrence in } \mathfrak{S} \text{ (resp. } \mathfrak{S}') $$

<footnote n="26">²⁶Strictly speaking, the two last arguments point to formula occurrences in the conclusions of $\pi_1, \pi_2$.</footnote>
These decorated inference rules can be read as a proof system, and we have:

**Claim 5.18.** The derivation trees generated by those rules are exactly the ones that can be obtained in the following way: start from a Slavnov pre-proof (with flat sequents) and for each node, replace its value by $\mathfrak{G}_\pi$ where $\pi$ is the sub-pre-proof rooted at that node.

Let us call these derivation trees *decorated pre-proofs*.

**Third level: side condition using the decorations.** At this point, we have obtained a new proof system that, in the end, proves the same flat sequents as the former Slavnov pre-proofs. So it is still unsound with respect to pomset logic. To remedy that, it remains to leverage the additional “multi-reachability” information provided by the decorations (in fact, we use only reachability by a single æ-path between two formulas).

**Claim 5.19.** A decorated pre-proof translates to a correct tree-like RB-net if and only if we have $\{(B, A)\} \notin \mathfrak{D}$ for every instance of a $\triangleleft$-intro rule in it of the form below:

$$ \frac{([\Gamma, A, B], \mathfrak{D})}{([\Gamma, A \triangleleft B], \mathfrak{D}')} $$

*Proof.* In the inductive translation of Slavnov pre-proofs to prenets, if the last rule is any other than $\triangleleft$-intro, then the sub-pre-proofs for its premises are all mapped to correct nets if and only if the translation of the whole pre-proof is itself a correct net. In fact, this is precisely why the desequentialization of MLL+mix sequent proofs into proof nets is sound, a well-known fact. However, for a $\triangleleft$-intro rule (using the above notations), the corresponding operation on tree-like RB-prenets may create new æ-cycles. From the shape of the RB-tree gadget associated to $\triangleleft$ (cf. Figure 2) one can see that such new cycles can only be composed of the directed edge of this gadget from A to B plus an æ-path from B to A in the prenet for the premise. The existence of the latter is precisely equivalent to $\{(B, A)\} \in \mathfrak{D}$. $\square$

Note that the assumption in the above claim only consists in purely local “side conditions” on inference rules, hence:

**Definition 5.20.** A *decorated proof* is a derivation tree in the system whose inference rules are those of decorated pre-proofs except that the $\triangleleft$-intro rule is subject to a *side condition*: it can only be applied to $([\Gamma, A, B], \mathfrak{D})$ (to introduce $A \triangleleft B$) when $\{(B, A)\} \notin \mathfrak{D}$.

The “if” part of Claim 5.19 can then be rephrased as the *soundness of the decorated proof system* for pomset logic.

Let us also sketch briefly a *completeness argument*. Given a correct pomset logic proof net $\mathcal{G}$, first consider a copy $\mathcal{G}'$ where every $\triangleleft$ has been turned into $\mathcal{G}$. This is still a correct net (replacing $\triangleleft$ by $\mathcal{G}$ removes an edge, so it can destroy æ-cycles, not create them), in fact $\mathcal{G}'$ is an MLL+mix proof net. There exists an MLL+mix sequent proof whose inductive translation (desequentialization) is $\mathcal{G}'$ — this is the *sequentialization theorem* (a result involving non-trivial combinatorics, originating in [Gir87]; see [Ret03, Ngu20] for a discussion of its “equivalence” with earlier results in mainstream graph theory). Next, in this sequentialization, replace the relevant occurrences of $\mathcal{G}$ by $\triangleleft$; we obtain a Slavnov pre-proof (since in this system the rule for $\triangleleft$ is the same as the MLL+mix rule for $\mathcal{G}$) which lifts uniquely to a decorated pre-proof. Finally, one must check that the latter satisfies the side conditions; this comes from the correctness of the pomset logic proof net $\mathcal{G}$ that we started with, plus the “only if” part of Claim 5.19.
These decorated inference rules can be read as a proof system, and we have:

**Claim 5.18.** The derivation trees generated by those rules are exactly the ones that can be obtained in the following way: start from a Slavnov pre-proof (with flat sequents) and for each node, replace its value by $\mathcal{G}_\pi$ where $\pi$ is the sub-pre-proof rooted at that node.

Let us call these derivation trees *decorated pre-proofs*.

**Third level: side condition using the decorations.** At this point, we have obtained a new proof system that, in the end, proves the same flat sequents as the former Slavnov pre-proofs. So it is still unsound with respect to pomset logic. To remedy that, it remains to leverage the additional “multi-reachability” information provided by the decorations (in fact, we use only reachability by a single æ-path between two formulas).

**Claim 5.19.** A decorated pre-proof translates to a correct tree-like RB-net if and only if we have $\{(B, A)\} \notin \mathcal{D}$ for every instance of a $\triangleleft$-intro rule in it of the form below:

$$ \frac{([\Gamma, A, B], \mathcal{D})}{([\Gamma, A \triangleleft B], \mathcal{D}')} $$

*Proof.* In the inductive translation of Slavnov pre-proofs to prenets, if the last rule is any other than $\triangleleft$-intro, then the sub-pre-proofs for its premises are all mapped to correct nets if and only if the translation of the whole pre-proof is itself a correct net. In fact, this is precisely why the desequentialization of MLL+mix sequent proofs into proof nets is sound, a well-known fact. However, for a $\triangleleft$-intro rule (using the above notations), the corresponding operation on tree-like RB-prenets may create new æ-cycles. From the shape of the RB-tree gadget associated to $\triangleleft$ (cf. Figure 2) one can see that such new cycles can only be composed of the directed edge of this gadget from A to B plus an æ-path from B to A in the prenet for the premise. The existence of the latter is precisely equivalent to $\{(B, A)\} \in \mathcal{D}$. $\square$

Note that the assumption in the above claim only consists in purely local “side conditions” on inference rules, hence:

**Definition 5.20.** A *decorated proof* is a derivation tree in the system whose inference rules are those of decorated pre-proofs except that the $\triangleleft$-intro rule is subject to a *side condition*: it can only be applied to $([\Gamma, A, B], \mathcal{D})$ (to introduce $A \triangleleft B$) when $\{(B, A)\} \notin \mathcal{D}$.

The “if” part of Claim 5.19 can then be rephrased as the *soundness of the decorated proof system* for pomset logic.

Let us also sketch briefly a *completeness argument*. Given a correct pomset logic proof net $\mathcal{G}$, first consider a copy $\mathcal{G}'$ where every $\triangleleft$ has been turned into $\mathcal{G}$. This is still a correct net (replacing $\triangleleft$ by $\mathcal{G}$ removes an edge, so it can destroy æ-cycles, not create them), in fact $\mathcal{G}'$ is an MLL+mix proof net. There exists an MLL+mix sequent proof whose inductive translation (desequentialization) is $\mathcal{G}'$ — this is the *sequentialization theorem* (a result involving non-trivial combinatorics, originating in [Gir87]; see [Ret03, Ngu20] for a discussion of its “equivalence” with earlier results in mainstream graph theory). Next, in this sequentialization, replace the relevant occurrences of $\mathcal{G}$ by $\triangleleft$; we obtain a Slavnov pre-proof (since in this system the rule for $\triangleleft$ is the same as the MLL+mix rule for $\mathcal{G}$) which lifts uniquely to a decorated pre-proof. Finally, one must check that the latter satisfies the side conditions; this comes from the correctness of the pomset logic proof net $\mathcal{G}$ that we started with, plus the “only if” part of Claim 5.19.
## 6. CONCLUSION

In the first paper of this series [Gug07], Guglielmi announced the task of the present one in the following way:

> It is still open whether the logic in this paper, called BV, is the same as pomset logic. We conjecture that it is actually the same logic, but one crucial step is still missing, at the time of this writing, in the equivalence proof. This paper is the first in a planned series of three papers dedicated to BV. [...] In the third part, some of my colleagues will hopefully show the equivalence of BV and pomset logic, this way explaining why it was impossible to find a sequent system for pomset logic.

Surprisingly, the hoped-for equivalence turned out to be false; in Section 3, we exhibited an explicit formula provable in pomset logic, but not in BV. What first led us to seek such a counter-example was the discovery of the complexity-theoretic hardness results of Section 4, according to which the conjectured equivalence would have implied $NP = coNP$. This, plus Slavnov's recent system [Sla19], put into question the established narrative about the impossibility of sequent calculi for pomset logic, so we revisited this topic in Section 5 (and showed in passing that an old sequent calculus with cuts was in fact equivalent to BV).

6.1. **Related topics.** As we hope that this paper may serve as a reference for readers who wish to get acquainted with BV and pomset logic (hence the lengthy Section 2), we will broadly survey here some works that are connected to these two systems, without limiting ourselves to provability or complexity-theoretic aspects.

6.1.1. *Applications and semantics of BV and pomset logic.* One of the first applications of self-dual non-commutativity was Reddy's Linear Logic Model of State [Red93]. This work, whose ultimate goal is to study mutable state in programming languages, introduces *LLMS*, which is an extension of intuitionistic$^{27}$ linear logic with some connectives, one of which is $\langle$. *LLMS* comes with a semantics in coherence spaces where the interpretation of $\langle$ coincides with that for pomset logic. The proof system for *LLMS* is a sequent calculus similar to Retoré's one (§5.1). It also admits a semantics in Dialectica categories [dP14, §4].

As for the proof nets of pomset logic, they have no known notion of categorical semantics; in fact, in light of the connections between categorical logic and deep inference [Hug04], it might be argued that any presentation of pomset logic as an “initial something-category” would amount to giving a deductive proof system for it. However the same connections make modeling BV categorically a straightforward matter, as has been done in [BPS12] where a new concrete semantics (probabilistic coherence spaces) is also given as an example of BV-category. There have been recent works relating BV and BV-categories to quantum causality [BGI$^+$14, SK22].

Finally, let us mention that Retoré and his collaborators have applied pomset logic to mathematical linguistics (see [Ret21, Section 7]). This provides an alternative to the usual approach in categorial grammars [MR12] which relies on the another kind of non-commutative logic that we shall cover next.

<footnote>$^{27}$In the context of linear logic, “intuitionistic” means that the sequents are two-sided with the right side being limited to a single formula. The sequents in [Red93] are of the form $\Gamma \vdash A$ where $\Gamma$ is what we call an ordered sequent.</footnote>
## 6. CONCLUSION

In the first paper of this series [Gug07], Guglielmi announced the task of the present one in the following way:

> It is still open whether the logic in this paper, called BV, is the same as pomset logic. We conjecture that it is actually the same logic, but one crucial step is still missing, at the time of this writing, in the equivalence proof. This paper is the first in a planned series of three papers dedicated to BV. [...] In the third part, some of my colleagues will hopefully show the equivalence of BV and pomset logic, this way explaining why it was impossible to find a sequent system for pomset logic.

Surprisingly, the hoped-for equivalence turned out to be false; in Section 3, we exhibited an explicit formula provable in pomset logic, but not in BV. What first led us to seek such a counter-example was the discovery of the complexity-theoretic hardness results of Section 4, according to which the conjectured equivalence would have implied $NP = coNP$. This, plus Slavnov's recent system [Sla19], put into question the established narrative about the impossibility of sequent calculi for pomset logic, so we revisited this topic in Section 5 (and showed in passing that an old sequent calculus with cuts was in fact equivalent to BV).

### 6.1. Related topics.
As we hope that this paper may serve as a reference for readers who wish to get acquainted with BV and pomset logic (hence the lengthy Section 2), we will broadly survey here some works that are connected to these two systems, without limiting ourselves to provability or complexity-theoretic aspects.

#### 6.1.1. *Applications and semantics of BV and pomset logic.*
One of the first applications of self-dual non-commutativity was Reddy's Linear Logic Model of State [Red93]. This work, whose ultimate goal is to study mutable state in programming languages, introduces *LLMS*, which is an extension of intuitionistic$^{27}$ linear logic with some connectives, one of which is $\langle$. *LLMS* comes with a semantics in coherence spaces where the interpretation of $\langle$ coincides with that for pomset logic. The proof system for *LLMS* is a sequent calculus similar to Retoré's one (§5.1). It also admits a semantics in Dialectica categories [dP14, §4].

As for the proof nets of pomset logic, they have no known notion of categorical semantics; in fact, in light of the connections between categorical logic and deep inference [Hug04], it might be argued that any presentation of pomset logic as an “initial something-category” would amount to giving a deductive proof system for it. However the same connections make modeling BV categorically a straightforward matter, as has been done in [BPS12] where a new concrete semantics (probabilistic coherence spaces) is also given as an example of BV-category. There have been recent works relating BV and BV-categories to quantum causality [BGI$^+$14, SK22].

Finally, let us mention that Retoré and his collaborators have applied pomset logic to mathematical linguistics (see [Ret21, Section 7]). This provides an alternative to the usual approach in *categorial grammars* [MR12] which relies on the another kind of non-commutative logic that we shall cover next.

<footnote>$^{27}$In the context of linear logic, “intuitionistic” means that the sequents are two-sided with the right side being limited to a single formula. The sequents in [Red93] are of the form $\Gamma \vdash A$ where $\Gamma$ is what we call an ordered sequent.</footnote>
6.1.2. *Other non-commutative variants of linear logic.* Linearity and non-commutativity first appeared in the study of typed λ-calculi in the Lambek calculus [Lam58], whose introduction was motivated by the aforementioned linguistic applications. We might thus consider it retrospectively as the first non-commutative logic, even though the *formulas-as-types correspondence*<fnref n="28" /> between typed λ-calculi and constructive logics was not known at the time. In the Lambek calculus, the order of arguments of a function matters: thus $A \dashv \neg B \dashv C \not\equiv B \dashv A \dashv C$ where $\dashv$ is the linear implication connective.

In a classical linear logic framework, where $A \dashv \neg B$ may be defined as $A^{\perp} \otimes B$, this translates into $A \otimes B \not\equiv B \otimes A$ – a non-commutativity in the literal sense. This entails the non-commutativity of its dual connective $\otimes$ and we have $(A \otimes B)^{\perp} = B^{\perp} \otimes A^{\perp}$. (In contrast, pomset logic keeps $\otimes$, $\perp$ commutative while adding the new connective $\lhd$, and the self-duality of $\lhd$ does not permute its arguments.) The standard system with those properties is *cyclic*<fnref n="29" /> *linear logic*; see [Yet90] for its sequent calculus and proof nets, [DG04] for a deep inference system and [AM19] for pointers to more recent work on cyclic MLL.

On λ-terms or proof nets, non-commutativity corresponds to a *planarity condition*; to our knowledge, this was first remarked by Girard in [Gir89, Section II.9] just after his discovery of linear logic [Gir87]. For more recent works pursuing such topological ideas, see e.g. [APR05, Abr07, Mel18]. In particular, renewed interest in the non-commutative linear λ-calculus has come from the discovery of a deep connection with the combinatorics of planar maps [ZG15], including bijective and enumerative aspects.

The aforementioned works consider proofs or λ-terms as static combinatorial objects, but they can also be seen as programs. In this perspective, unexpected computational consequences of non-commutativity in the λ-calculus have recently been uncovered in an automata-theoretic setting [NP20].

Finally, let us mention Abrusci and Ruet’s logic [AR99, Rue00] where commutative and non-commutative versions of the connectives $\otimes$ and $\perp$ coexist.

6.1.3. *Proof nets vs denotational semantics.* Pomset logic comes from trying to extract a syntactic correctness criterion from the coherence space semantics: the interpretation of a pre-proof net in coherence spaces can be defined by means of so-called experiments, and we want the result of the experiments to be a valid member of the semantics. (To be precise, we want the set of points obtained by experiments to form a clique.) For MLL+mix proof nets, Retoré showed that this condition is equivalent to correctness [Ret97b], and the correctness criterion for pomset proof nets was designed to extend this correspondence (this is discussed in [Ret97a]).

Pagani has applied a similar methodology to MELL (Multiplicative-Exponential Linear Logic) pre-proof nets: he shows in [Pag06] that the validity of coherence space experiments — using a certain “non-uniform” interpretation of the exponentials — is equivalent to a certain graph-theoretical condition, *visible acyclicity*, which is weaker than the usual correctness criterion for MELL+mix. This is later extended to differential interaction nets in [Pag12]; since coherence spaces are not a semantics of differential linear logic, the result of [Pag12] is formulated with respect to Ehrhard’s finiteness spaces instead.

<footnote n="28">²⁸Also known as “proofs-as-programs” or “Curry–Howard” correspondence.</footnote>

<footnote n="29">²⁹This is entirely unrelated to the so-called “cyclic proofs” (also known as “circular proofs”) for logics with fixed points or (co)inductive definitions, a trendy research topic at the time of writing.</footnote>
6.1.2. *Other non-commutative variants of linear logic.* Linearity and non-commutativity first appeared in the study of typed λ-calculi in the Lambek calculus [Lam58], whose introduction was motivated by the aforementioned linguistic applications. We might thus consider it retrospectively as the first non-commutative logic, even though the *formulas-as-types correspondence*<sup>28</sup> between typed λ-calculi and constructive logics was not known at the time. In the Lambek calculus, the order of arguments of a function matters: thus $A \dashv \neg B \dashv C \not\equiv B \dashv A \dashv C$ where $\dashv$ is the linear implication connective.

In a classical linear logic framework, where $A \dashv \neg B$ may be defined as $A^{\perp} \otimes B$, this translates into $A \otimes B \not\equiv B \otimes A$ – a non-commutativity in the literal sense. This entails the non-commutativity of its dual connective $\otimes$ and we have $(A \otimes B)^{\perp} = B^{\perp} \otimes A^{\perp}$. (In contrast, pomset logic keeps $\otimes$, $\perp$ commutative while adding the new connective $\lhd$, and the self-duality of $\lhd$ does not permute its arguments.) The standard system with those properties is *cyclic*<sup>29</sup> *linear logic*; see [Yet90] for its sequent calculus and proof nets, [DG04] for a deep inference system and [AM19] for pointers to more recent work on cyclic MLL.

On λ-terms or proof nets, non-commutativity corresponds to a *planarity condition*; to our knowledge, this was first remarked by Girard in [Gir89, Section II.9] just after his discovery of linear logic [Gir87]. For more recent works pursuing such topological ideas, see e.g. [APR05, Abr07, Mel18]. In particular, renewed interest in the non-commutative linear λ-calculus has come from the discovery of a deep connection with the combinatorics of planar maps [ZG15], including bijective and enumerative aspects.

The aforementioned works consider proofs or λ-terms as static combinatorial objects, but they can also be seen as programs. In this perspective, unexpected computational consequences of non-commutativity in the λ-calculus have recently been uncovered in an automata-theoretic setting [NP20].

Finally, let us mention Abrusci and Ruet's logic [AR99, Rue00] where commutative and non-commutative versions of the connectives $\otimes$ and $\perp$ coexist.

6.1.3. *Proof nets vs denotational semantics.* Pomset logic comes from trying to extract a syntactic correctness criterion from the coherence space semantics: the interpretation of a pre-proof net in coherence spaces can be defined by means of so-called experiments, and we want the result of the experiments to be a valid member of the semantics. (To be precise, we want the set of points obtained by experiments to form a clique.) For MLL+mix proof nets, Retoré showed that this condition is equivalent to correctness [Ret97b], and the correctness criterion for pomset proof nets was designed to extend this correspondence (this is discussed in [Ret97a]).

Pagani has applied a similar methodology to MELL (Multiplicative-Exponential Linear Logic) pre-proof nets: he shows in [Pag06] that the validity of coherence space experiments — using a certain “non-uniform” interpretation of the exponentials — is equivalent to a certain graph-theoretical condition, *visible acyclicity*, which is weaker than the usual correctness criterion for MELL+mix. This is later extended to differential interaction nets in [Pag12]; since coherence spaces are not a semantics of differential linear logic, the result of [Pag12] is formulated with respect to Ehrhard’s finiteness spaces instead.

<footnote n="28"><sup>28</sup>Also known as “proofs-as-programs” or “Curry-Howard” correspondence.</footnote>

<footnote n="29"><sup>29</sup>This is entirely unrelated to the so-called “cyclic proofs” (also known as “circular proofs”) for logics with fixed points or (co)inductive definitions, a trendy research topic at the time of writing.</footnote>
A similarity between correctness for pomset proof nets and visible acyclicity is that both involve *directed* edges and cycles. Thanks to this, it is straightforward to show that visible acyclicity is **coNP**-hard, by adapting the proof for pomset logic; however we do not know whether, conversely, it is in **coNP**.

Let us also mention Tranquili's *hypercorrectness* criterion for MALL (Multiplicative-Additive) pre-proof nets, coming from their semantics in hypercoherences [Tra08]. Here again the condition obtained is weaker than the usual correctness criterion — so there are hypercorrect MALL pre-proof nets that are not sequentializable. (Coherence spaces would allow even more non-sequentializable pre-proof nets, for instance a version of Berry's famous "Gustave function".)

6.1.4. *Extensions of BV.* Given that BV and pomset logic are “multiplicative” logics, it is natural to make extensions with other primitives, like the additives and exponentials of linear logic, or other modalities or quantifiers.

This has indeed been done, but so far only for BV. The first such extension was adding the exponential of linear logic to BV, leading to the logic NEL, which is studied in the fourth and fifth paper of this series [SG11, GS11].

In [Rov16], Roversi adds a self-dual binder to BV, in order to establish a correspondence to the linear λ-calculus, in the spirit of the *formulas-as-types* paradigm.

The next natural extension was adding the additives, leading to the logic MAV [Hor15], which has then been extended by nominal quantifiers (and standard first-order quantifiers) [HTAC19, HT19] in order to simulate private names in process algebras, as for example the π-calculus. This is in the line of research by Bruscoli [Bru02] who used BV to simulate reductions in CCS, following the *formulas-as-processes* paradigm.

6.1.5. *Beyond formulas.* The formulas-as-processes paradigm has recently motivated another line of research. The restrictions on digraphs, that define dicographs which correspond to formulas (see Definitions 2.27, 2.28 and Theorem 2.29) and that therefore make proof theory possible in the first place, are also an obstacle to the formulas-as-processes paradigm because there are processes that do contain the forbidden configurations in (2.2) in Definition 2.26, and do therefore not correspond to formulas. This suggests to define a proof system directly on the graphs instead of the formulas, and use the modular decomposition tree instead of the formula tree. This idea (first briefly mentioned in [NS18, Section 5]) has been explored in [AHS20, AHS22] and [CDW20] for undirected graphs and in [AHMS22] for digraphs. It turns out that if we drop the cograph/dicograph condition, there is a much larger space of possible proof systems, that still waits to be explored.

## 6.2. Open problems.
For a long time, it was believed that there was a canonical extension of MLL+mix with the connective $\triangleleft$ that had both a deductive proof system (BV) and proof nets with a simple correctness criterion (pomset logic). Now that we have refuted this, several questions arise:

* We might want to design truly well-behaved deductive proofs for pomset logic — given the obstructions that we have seen in this paper, this looks challenging. Slavnov's sequent calculus is a start, but it is not clear for us whether a cut-elimination procedure can be defined directly on it without going through a translation into proof nets. And even
A similarity between correctness for pomset proof nets and visible acyclicity is that both involve *directed* edges and cycles. Thanks to this, it is straightforward to show that visible acyclicity is **coNP**-hard, by adapting the proof for pomset logic; however we do not know whether, conversely, it is in **coNP**.

Let us also mention Tranquili's *hypercorrectness* criterion for MALL (Multiplicative-Additive) pre-proof nets, coming from their semantics in hypercoherences [Tra08]. Here again the condition obtained is weaker than the usual correctness criterion — so there are hypercorrect MALL pre-proof nets that are not sequentializable. (Coherence spaces would allow even more non-sequentializable pre-proof nets, for instance a version of Berry's famous "Gustave function".)

6.1.4. *Extensions of BV.* Given that BV and pomset logic are “multiplicative” logics, it is natural to make extensions with other primitives, like the additives and exponentials of linear logic, or other modalities or quantifiers.

This has indeed been done, but so far only for BV. The first such extension was adding the exponential of linear logic to BV, leading to the logic NEL, which is studied in the fourth and fifth paper of this series [SG11, GS11].

In [Rov16], Roversi adds a self-dual binder to BV, in order to establish a correspondence to the linear λ-calculus, in the spirit of the *formulas-as-types* paradigm.

The next natural extension was adding the additives, leading to the logic MAV [Hor15], which has then been extended by nominal quantifiers (and standard first-order quantifiers) [HTAC19, HT19] in order to simulate private names in process algebras, as for example the π-calculus. This is in the line of research by Bruscoli [Bru02] who used BV to simulate reductions in CCS, following the *formulas-as-processes* paradigm.

6.1.5. *Beyond formulas.* The formulas-as-processes paradigm has recently motivated another line of research. The restrictions on digraphs, that define dicographs which correspond to formulas (see Definitions 2.27, 2.28 and Theorem 2.29) and that therefore make proof theory possible in the first place, are also an obstacle to the formulas-as-processes paradigm because there are processes that do contain the forbidden configurations in (2.2) in Definition 2.26, and do therefore not correspond to formulas. This suggests to define a proof system directly on the graphs instead of the formulas, and use the modular decomposition tree instead of the formula tree. This idea (first briefly mentioned in [NS18, Section 5]) has been explored in [AHS20, AHS22] and [CDW20] for undirected graphs and in [AHMS22] for digraphs. It turns out that if we drop the cograph/dicograph condition, there is a much larger space of possible proof systems, that still waits to be explored.

## 6.2. Open problems.
For a long time, it was believed that there was a canonical extension of MLL+mix with the connective $\triangleleft$ that had both a deductive proof system (BV) and proof nets with a simple correctness criterion (pomset logic). Now that we have refuted this, several questions arise:

* We might want to design truly well-behaved deductive proofs for pomset logic — given the obstructions that we have seen in this paper, this looks challenging. Slavnov's sequent calculus is a start, but it is not clear for us whether a cut-elimination procedure can be defined directly on it without going through a translation into proof nets. And even
without insisting on the proof system being deductive, the requirement of tractable proof checking rules out proof nets by themselves (Remark 4.14).

* Our results might also be interpreted as suggesting that of the two logics, BV was the “right” one all along. Then it would be desirable to have a system of proof nets for BV. Perhaps it suffices to extend the correctness criterion of pomset logic so that it excludes more pre-proofs. If that were the case, then the problem of “BV-correctness” of pre-proof nets would be equivalent to the BV-provability problem for balanced formulas. This also raises the question of the complexity of the latter: **NP**-completeness would rule out **coNP** critera of the sort “there does not exist some bad structure (e.g. some kind of cycle) in the pre-proof net”. Alternatively, the right notion of proof net could involve not just the formula tree and axiom linking, but some extra structure too (maybe an order on the axiom linking?); there are some precedents for this in the theory of MLL proof nets with units (with many variants, recapitulated in [Hug12, Table 1]).

* More generally, now that we have two logics that (i) are built from the connectives $\rightleftharpoons, \leftarrow, \otimes$, (ii) are conservative over MLL+mix, and (iii) admit cut elimination, the question arises whether these are the only two or whether there is a hierarchy of such logics with increasing proof complexity.

During the research for this paper, another interesting question arose. We conjecture the following generalization of the construction of the formula in Section 3: given a balanced tautology of classical logic, one can always “make the axiom links directed” in some way (cf. Remark 3.15) to get a provable formula in pomset logic.

**Acknowledgments.** We would like to thank Christian Retoré for instructive discussions.

## REFERENCES

[AB09] Sanjeev Arora and Boaz Barak. *Computational Complexity: A Modern Approach*. Cambridge University Press, 2009. URL: https://theory.cs.princeton.edu/complexity/, doi:10.1017/CBO9780511804090.

[Abr07] Samson Abramsky. Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics. In Goong Chen, Louis Kauffman, and Samuel Lomonaco, editors, *Mathematics of Quantum Computation and Quantum Technology*, volume 20074453, pages 515–558. Chapman and Hall/CRC, September 2007. doi:10.1201/9781584889007.ch15.

[Acc23] Matteo Acclavio. Graphical Proof Theory I: Multiplicative Linear Logic Beyond Cographs. *CoRR*, abs/2305.12975, 2023. arXiv:2305.12975.

[AHMS22] Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In Amy P. Felty, editor, *7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)*, volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:25, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.22.

[AHS20] Matteo Acclavio, Ross Horne, and Lutz Straßburger. Logic beyond formulas: A proof system on graphs. In *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 38–52, New York, NY, USA, 2020. Association for Computing Machinery. doi: 10.1145/3373718.3394763.

[AHS22] Matteo Acclavio, Ross Horne, and Lutz Straßburger. An analytic propositional proof system on graphs. *Logical Methods in Computer Science*, 18(4), 2022. Extended journal version of [AHS20]. doi:10.46298/lmcs-18(4:1)2022.

[AM19] V. Michele Abrusci and Roberto Maieli. Proof nets for multiplicative cyclic linear logic and Lambek calculus. *Mathematical Structures in Computer Science*, pages 1–30, February 2019. doi:10.1017/S0960129518000300.
without insisting on the proof system being deductive, the requirement of tractable proof checking rules out proof nets by themselves (Remark 4.14).

* Our results might also be interpreted as suggesting that of the two logics, BV was the “right” one all along. Then it would be desirable to have a system of proof nets for BV. Perhaps it suffices to extend the correctness criterion of pomset logic so that it excludes more pre-proofs. If that were the case, then the problem of “BV-correctness” of pre-proof nets would be equivalent to the BV-provability problem for balanced formulas. This also raises the question of the complexity of the latter: **NP**-completeness would rule out **coNP** critera of the sort “there does not exist some bad structure (e.g. some kind of cycle) in the pre-proof net”. Alternatively, the right notion of proof net could involve not just the formula tree and axiom linking, but some extra structure too (maybe an order on the axiom linking?); there are some precedents for this in the theory of MLL proof nets with units (with many variants, recapitulated in [Hug12, Table 1]).

* More generally, now that we have two logics that (i) are built from the connectives $\rightleftharpoons, \leftarrow, \otimes$, (ii) are conservative over MLL+mix, and (iii) admit cut elimination, the question arises whether these are the only two or whether there is a hierarchy of such logics with increasing proof complexity.

During the research for this paper, another interesting question arose. We conjecture the following generalization of the construction of the formula in Section 3: given a balanced tautology of classical logic, one can always “make the axiom links directed” in some way (cf. Remark 3.15) to get a provable formula in pomset logic.

**Acknowledgments.** We would like to thank Christian Retoré for instructive discussions.

## REFERENCES

[AB09] Sanjeev Arora and Boaz Barak. *Computational Complexity: A Modern Approach*. Cambridge University Press, 2009. URL: https://theory.cs.princeton.edu/complexity/, doi:10.1017/CBO9780511804090.

[Abr07] Samson Abramsky. Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics. In Goong Chen, Louis Kauffman, and Samuel Lomonaco, editors, *Mathematics of Quantum Computation and Quantum Technology*, volume 20074453, pages 515–558. Chapman and Hall/CRC, September 2007. doi:10.1201/9781584889007.ch15.

[Acc23] Matteo Acclavio. Graphical Proof Theory I: Multiplicative Linear Logic Beyond Cographs. *CoRR*, abs/2305.12975, 2023. arXiv:2305.12975.

[AHMS22] Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In Amy P. Felty, editor, *7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)*, volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:25, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSCD.2022.22.

[AHS20] Matteo Acclavio, Ross Horne, and Lutz Straßburger. Logic beyond formulas: A proof system on graphs. In *Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 38–52, New York, NY, USA, 2020. Association for Computing Machinery. doi: 10.1145/3373718.3394763.

[AHS22] Matteo Acclavio, Ross Horne, and Lutz Straßburger. An analytic propositional proof system on graphs. *Logical Methods in Computer Science*, 18(4), 2022. Extended journal version of [AHS20]. doi:10.46298/lmcs-18(4:1)2022.

[AM19] V. Michele Abrusci and Roberto Maieli. Proof nets for multiplicative cyclic linear logic and Lambek calculus. *Mathematical Structures in Computer Science*, pages 1–30, February 2019. doi:10.1017/S0960129518000300.
[AM20] Matteo Acclavio and Roberto Maieli. Generalized Connectives for Multiplicative Linear Logic. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.CSL.2020.6.

[APR05] Jean-Marc Andreoli, Gabriele Pulcini, and Paul Ruet. Permutative logic. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 184–199. Springer, 2005. doi:10.1007/11538363_14.

[AR99] V. Michele Abrusci and Paul Ruet. Non-commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic, 101(1):29–64, 1999. doi:10.1016/S0168-0072(99)00014-7.

[ATS19] Andrea Aler Tubella and Lutz Straßburger. Introduction to Deep Inference. Lecture notes, August 2019. URL: https://hal.inria.fr/hal-02390267.

[Bas94] David A. Basin. A term equality problem equivalent to graph isomorphism. Information Processing Letters, 51(2):61–66, 1994. doi:10.1016/0020-0190(94)00084-0.

[BdGR97] Denis Béchet, Philippe de Groote, and Christian Retoré. A complete axiomatisation for the inclusion of series-parallel partial orders. In Hubert Comon, editor, Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of Lecture Notes in Computer Science, pages 230–240. Springer, 1997. doi:10.1007/3-540-62950-5_74.

[BG18] Jørgen Bang-Jensen and Gregory Z. Gutin, editors. Classes of Directed Graphs. Springer Monographs in Mathematics. Springer, 2018. doi:10.1007/978-3-319-71840-8.

[BGI$^+$14] Richard Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden, and Lutz Straßburger. A logical basis for quantum evolution and entanglement. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip Scott, editors, Categories and Types in Logic, Language, and Physics – Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, volume 8222 of Lecture Notes in Computer Science, pages 90–107. Springer, 2014. doi:10.1007/978-3-642-54789-8_6.

[BPS12] Richard Blute, Prakash Panangaden, and Sergey Slavnov. Deep inference and probabilistic coherence spaces. Applied Categorical Structures, 20(3):209–228, 2012. doi:10.1007/s10485-010-9241-0.

[Bru02] Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29 - August 1, 2002, Proceedings, volume 2401 of Lecture Notes in Computer Science, pages 302–316. Springer, 2002. doi:10.1007/3-540-45619-8_21.

[BT01] Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250 of Lecture Notes in Computer Science, pages 347–361. Springer, 2001. doi:10.1007/3-540-45653-8_24.

[CDW20] Cameron Calk, Anupam Das, and Tim Waring. Beyond formulas-as-cographs: an extension of boolean logic to arbitrary graphs. CoRR, abs/2004.12941, 2020. arXiv:2004.12941.

[CLB81] Derek G. Corneil, H. Lerchs, and L. Stewart Burlingham. Complement reducible graphs. Discrete Applied Mathematics, 3(3):163–174, 1981. doi:10.1016/0166-218X(81)90013-5.

[CP06] Christophe Crespelle and Christophe Paul. Fully dynamic recognition algorithm and certificate for directed cographs. Discrete Applied Mathematics, 154(12):1722–1741, 2006. doi:10.1016/j.dam.2006.03.005.

[CR79] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36–50, 1979. doi:10.2307/2273702.

[DG04] Pietro Di Gianantonio. Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity. In Computer Science Logic, volume 3210, pages 130–144, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-30124-0_13.

[dP14] Valeria de Paiva. Linear logic model of state revisited. Logic Journal of the IGPL, 22(5):791–804, 2014. doi:10.1093/jigpal/jzu013.

[DR89] Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28(3):181–203, 1989. doi:10.1007/BF01622878.