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

Lê Thành Dũng Nguyên, Lutz Straßburger

► To cite this version:

Lê Thành Dũng Nguyên, Lutz Straßburger. A System of Interaction and Structure III: The Complexity of BV and Pomset Logic. Logical Methods in Computer Science, 2023, 9 (4), 10.46298/LMCS-19(4:25)2023 . hal-03909547v2

HAL Id: hal-03909547

https://inria.hal.science/hal-03909547v2

Submitted on 10 Jan 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Lê Thành Dũng Nguyên, Lutz Straßburger

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

## To cite this version:

Lê Thành Dũng Nguyên, Lutz Straßburger. A System of Interaction and Structure III: The Complexity of BV and Pomset Logic. Logical Methods in Computer Science, 2023, 9 (4), 10.46298/LMCS-19(4:25)2023 . hal-03909547v2

HAL Id: hal-03909547

https://inria.hal.science/hal-03909547v2

Submitted on 10 Jan 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
# A SYSTEM OF INTERACTION AND STRUCTURE III: THE COMPLEXITY OF SYSTEM BV AND POMSET LOGIC*

LÊ THÀNH DÙNG (TITO) NGUYỄN ◦ a AND LUTZ STRASSBURGER ◦ b

**ABSTRACT.** Pomset logic and BV are both logics that extend multiplicative linear logic (with mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same.

In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in Pomset logic is $\Sigma_2^P$-complete. We also make some observations with respect to possible sequent systems for the two logics.

## CONTENTS

<table><tr><td>1. Introduction</td><td>2</td></tr><tr><td>2. Preliminaries on Pomset Logic and BV</td><td>4</td></tr><tr><td>2.1. Formulas, Duality and Sequents</td><td>4</td></tr><tr><td>2.2. Dicographs, Relation Webs and Series-Parallel Orders</td><td>6</td></tr><tr><td>2.3. Perfect Matchings, RB-digraphs and Alternating Elementary Cycles</td><td>9</td></tr><tr><td>2.4. Pomset Logic, Proof Nets and Balanced Formulas</td><td>11</td></tr><tr><td>2.5. System BV and the Calculus of Structures</td><td>14</td></tr><tr><td>2.6. Unit-Free Versions of BV and SBV</td><td>16</td></tr><tr><td>2.7. SBVu and Dicograph Inclusions</td><td>18</td></tr></table>

*Key words and phrases:* proof nets, deep inference, pomset logic, system BV, cographs, dicographs, series-parallel orders, relation webs.

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

<footnote>a Laboratoire de l'informatique du parallélisme (LIP), École normale supérieure de Lyon, France
*e-mail address:* nltd@nguyentito.eu</footnote>

<footnote>b Inria Saclay & Laboratoire d'informatique de l'École polytechnique (LIX), Palaiseau, France</footnote>

<footnote>* This article extends our previous CSL 2022 paper [NS22] with a substantial amount of new material. It has been invited to a special issue of LMCS.</footnote>

<footnote>L. T. D. Nguyễn was supported by the LambdaComb project (ANR-21-CE48-0017) while working at École polytechnique and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" operated by the French National Research Agency (ANR).</footnote>
# A SYSTEM OF INTERACTION AND STRUCTURE III: THE COMPLEXITY OF SYSTEM BV AND POMSET LOGIC*

LÊ THÀNH DŨNG (TITO) NGUYỄN ◦ a AND LUTZ STRASSBURGER ◦ b

**ABSTRACT.** Pomset logic and BV are both logics that extend multiplicative linear logic (with mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same.

In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in Pomset logic is $\Sigma_2^P$-complete. We also make some observations with respect to possible sequent systems for the two logics.

## CONTENTS

<table><tr><td>1. Introduction</td><td>2</td></tr><tr><td>2. Preliminaries on Pomset Logic and BV</td><td>4</td></tr><tr><td>2.1. Formulas, Duality and Sequents</td><td>4</td></tr><tr><td>2.2. Dicographs, Relation Webs and Series-Parallel Orders</td><td>6</td></tr><tr><td>2.3. Perfect Matchings, RB-digraphs and Alternating Elementary Cycles</td><td>9</td></tr><tr><td>2.4. Pomset Logic, Proof Nets and Balanced Formulas</td><td>11</td></tr><tr><td>2.5. System BV and the Calculus of Structures</td><td>14</td></tr><tr><td>2.6. Unit-Free Versions of BV and SBV</td><td>16</td></tr><tr><td>2.7. SBVu and Dicograph Inclusions</td><td>18</td></tr></table>

*Key words and phrases:* proof nets, deep inference, pomset logic, system BV, cographs, dicographs, series-parallel orders, relation webs.

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

<footnote>a Laboratoire de l'informatique du parallélisme (LIP), École normale supérieure de Lyon, France
*e-mail address:* nltd@nguyentito.eu</footnote>

<footnote>b Inria Saclay & Laboratoire d'informatique de l'École polytechnique (LIX), Palaiseau, France</footnote>

<footnote>* This article extends our previous CSL 2022 paper [NS22] with a substantial amount of new material. It has been invited to a special issue of LMCS.</footnote>

<footnote>L. T. D. Nguyễn was supported by the LambdaComb project (ANR-21-CE48-0017) while working at École polytechnique and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" operated by the French National Research Agency (ANR).</footnote>
<table><tr><td>3. Comparing BV and Pomset Logic</td><td>20</td></tr><tr><td>3.1. BV is Contained in Pomset Logic</td><td>20</td></tr><tr><td>3.2. Pomset Logic is not Contained in BV</td><td>23</td></tr><tr><td>4. Complexity of Provability</td><td>28</td></tr><tr><td>4.1. Preliminaries on Complexity Theory and Boolean Formulas</td><td>28</td></tr><tr><td>4.2. BV is NP-Complete (and how to Generalize Membership in NP)</td><td>30</td></tr><tr><td>4.3. Correctness of Pomset Logic Proof Nets is coNP-Complete</td><td>32</td></tr><tr><td>4.4. Finding Alternating Elementary Cycles is NP-Hard</td><td>35</td></tr><tr><td>4.5. Pomset Logic Provability is Σ<sub>2</sub><sup>P</sup>-Complete</td><td>39</td></tr><tr><td>5. Back to the Sequent Calculus</td><td>43</td></tr><tr><td>5.1. Retoré's Sequent Calculus with Cuts is Equivalent to BV</td><td>44</td></tr><tr><td>5.2. A Refinement of Tiu's Argument</td><td>47</td></tr><tr><td>5.3. A Complexity-Theoretic Obstacle to Sequent Calculi for Pomset Logic</td><td>49</td></tr><tr><td>5.4. A Reconstruction of Slavnov's Calculus</td><td>50</td></tr><tr><td>6. Conclusion</td><td>53</td></tr><tr><td>6.1. Related topics</td><td>53</td></tr><tr><td>6.2. Open problems</td><td>55</td></tr><tr><td>References</td><td>56</td></tr></table>

# 1. INTRODUCTION

There are two ways to put this paper into perspective. First, it is the third paper in a series of five papers: the first two [Gug07, Tiu06] introduce a logic called system BV, prove cut elimination for it, and show that deep inference is necessary for having a cut-free deductive system for BV; and the last two [SG11, GS11] study system NEL, a conservative extension of BV with the exponentials of linear logic. The second way to look at this paper is that it finally answers the longstanding open question whether BV and pomset logic [Ret21] are the same.

Pomset logic has been discovered by Christian Retoré [Ret93, Ret97a] through the study of coherence spaces which form a semantics of proofs for linear logic [Gir87], by observing<fnref n="1" /> that next to the two operations ⊗ (tensor or multiplicative conjunction) and ⊺ (par or multiplicative disjunction) on coherence spaces there are two other operations ◁ and ▷, which are non-commutative, obey A ▁ B = B ▷ A, and are self-dual, i.e., ⟨A ▁ B⟩⊥ = A⊥ ▁ B⊥. Furthermore, there are canonical linear maps from A ⊗ B to A ▁ B, and from A ▁ B to A ⊺ B. From this semantic observation, Retoré derived a *proof net* syntax, i.e., a graph-like representation of proofs together with a combinatorial *correctness criterion* that distinguishes actual proofs among the considered space of graphs, together with a cut elimination theorem. However, he could not provide a sound and complete cut-free sequent calculus for this logic.

System BV was found by Alessio Guglielmi [Gug07, Gug99]<fnref n="2" /> through a syntactic investigation of the connectives of pomset logic and a graph theoretic study of series-parallel

<footnote n="1">¹According to Retoré (cf. http://www.lirmm.fr/~retore/PRESENTATIONS/pomset4michele.pdf), this semantic observation is due to Girard.</footnote>

<footnote n="2">²The initial ideas of the inference rules have also been present in [Ret99b] even though not formulated as a proof system admitting cut-elimination.</footnote>
<table><tr><td>3. Comparing BV and Pomset Logic</td><td>20</td></tr><tr><td>3.1. BV is Contained in Pomset Logic</td><td>20</td></tr><tr><td>3.2. Pomset Logic is not Contained in BV</td><td>23</td></tr><tr><td>4. Complexity of Provability</td><td>28</td></tr><tr><td>4.1. Preliminaries on Complexity Theory and Boolean Formulas</td><td>28</td></tr><tr><td>4.2. BV is NP-Complete (and how to Generalize Membership in NP)</td><td>30</td></tr><tr><td>4.3. Correctness of Pomset Logic Proof Nets is coNP-Complete</td><td>32</td></tr><tr><td>4.4. Finding Alternating Elementary Cycles is NP-Hard</td><td>35</td></tr><tr><td>4.5. Pomset Logic Provability is Σ<sub>2</sub><sup>P</sup>-Complete</td><td>39</td></tr><tr><td>5. Back to the Sequent Calculus</td><td>43</td></tr><tr><td>5.1. Retoré's Sequent Calculus with Cuts is Equivalent to BV</td><td>44</td></tr><tr><td>5.2. A Refinement of Tiu's Argument</td><td>47</td></tr><tr><td>5.3. A Complexity-Theoretic Obstacle to Sequent Calculi for Pomset Logic</td><td>49</td></tr><tr><td>5.4. A Reconstruction of Slavnov's Calculus</td><td>50</td></tr><tr><td>6. Conclusion</td><td>53</td></tr><tr><td>6.1. Related topics</td><td>53</td></tr><tr><td>6.2. Open problems</td><td>55</td></tr><tr><td>References</td><td>56</td></tr></table>

# 1. INTRODUCTION

There are two ways to put this paper into perspective. First, it is the third paper in a series of five papers: the first two [Gug07, Tiu06] introduce a logic called system BV, prove cut elimination for it, and show that deep inference is necessary for having a cut-free deductive system for BV; and the last two [SG11, GS11] study system NEL, a conservative extension of BV with the exponentials of linear logic. The second way to look at this paper is that it finally answers the longstanding open question whether BV and pomset logic [Ret21] are the same.

Pomset logic has been discovered by Christian Retoré [Ret93, Ret97a] through the study of coherence spaces which form a semantics of proofs for linear logic [Gir87], by observing<fnref n="1" /> that next to the two operations ⊗ (tensor or multiplicative conjunction) and ⊺ (par or multiplicative disjunction) on coherence spaces there are two other operations ◁ and ▷, which are non-commutative, obey A ▁ B = B ▷ A, and are self-dual, i.e., ⟨A ▁ B⟩⊥ = A⊥ ▁ B⊥. Furthermore, there are canonical linear maps from A ⊗ B to A ▁ B, and from A ▁ B to A ⊺ B. From this semantic observation, Retoré derived a proof net syntax, i.e., a graph-like representation of proofs together with a combinatorial correctness criterion that distinguishes actual proofs among the considered space of graphs, together with a cut elimination theorem. However, he could not provide a sound and complete cut-free sequent calculus for this logic.

System BV was found by Alessio Guglielmi [Gug07, Gug99]<fnref n="2" /> through a syntactic investigation of the connectives of pomset logic and a graph theoretic study of series-parallel

<footnote n="1">¹According to Retoré (cf. http://www.lirmm.fr/~retore/PRESENTATIONS/pomset4michele.pdf), this semantic observation is due to Girard.</footnote>

<footnote n="2">²The initial ideas of the inference rules have also been present in [Ret99b] even though not formulated as a proof system admitting cut-elimination.</footnote>
orders and cographs. The difficulty of presenting this combination of commutative and non-
commutative connectives in the sequent calculus triggered the development of the *calculus of
structures* [GS01], the first proper deep inference proof formalism.<fnref n="3" />

This leads to the strange situation that we have two logics, pomset logic and BV, which
are both conservative extensions of multiplicative linear logic with mix (MLL+mix) [FR94]
with a noncommutative connective $\triangleleft$ such that $A \otimes B \vdash A \triangleleft B$ and $A \triangleleft B \vdash A \otimes B$, and which
both obey a cut elimination result—the only difference being that pomset logic only had a
proof net syntax but no deductive proof system, and BV only had a deductive proof system
but no proof nets. This naturally led to the conjecture that both logics are the same [Str03b].

In this paper we show that this conjecture is false. It can easily be shown [Str03b, Str03a, Ret99b] that every theorem in BV is also a theorem of pomset logic, and for the sake of clarity, we also give a proof in this paper (in Section 3.1). However, the converse is not true, and we give an example of a formula that is a theorem of pomset logic but not provable in BV (in Section 3.2).

This naturally leads to the question of complexity. Do both logics have the same or
different complexity? It has been observed in [Kah08] that provability in BV is **NP**-complete.
The reason is that **NP**-hardness is inherited from MLL+mix, and containment in **NP** follows
from the fact that the size of every proof in BV is polynomial in the size of the conclusion,
and the correctness of such a proof can be checked in time which is linear in the size of the
proof (see Section 4.2 for more details). However, provability in pomset logic is $\Sigma_2^P$-complete.
Even though the size of a pomset logic proof net is polynomial in the size of its conclusion,
checking correctness of such a proof net is **coNP**-complete. The details for these results are
discussed in Sections 4.3–4.5.

This complexity result explains why it is impossible to give a deductive proof system
(in the sense of Cook and Reckhow [CR79]) for pomset logic. Nonetheless, there is a recent
proposal by Slavnov [Sla19] for a decorated sequent calculus for pomset logic. We look at
this calculus in Section 5.4 and relate it to our complexity result. Before that, we show in
Section 5.1 that the sequent calculus with cut, that Retoré proposed for pomset logic is in
fact a sound and complete sequent calculus for BV.<fnref n="4" />

In summary, the paper makes the following contributions:

* In Section 2, we give a gentle and easy accessible introduction to pomset logic and BV. We unify the notation and terminology, and present some important properties, that will be needed in later sections.

* In Section 3, we are showing that BV is properly contained in pomset logic, by showing that every theorem of BV is a theorem of pomset logic, but not vice versa. These results have already been presented in [NS22], of which this article is an extended version.

* In Section 4, we are discussing the complexity of pomset logic and BV. More precisely, we are recalling Kahramanoğulları's result on the **NP**-completeness of BV, and we show that checking correctness of a pomset logic proof is **coNP**-complete and that provability in pomset logic is $\Sigma_2^P$-complete.

* Finally, in Section 5, we come back to the sequent calculus, discussing the difficulties that the two logics pose, and how they can or cannot be overcome.

<footnote n="3">³An introductory survey on deep inference can be found in [ATS19].</footnote>

<footnote n="4">⁴In fact, in various publications on pomset logic, Retoré proposes different sequent calculi (one in his PhD thesis [Ret93, Chapitre 8], one in [Ret97a, Section 7], and more recently another on in [Ret21]); we work here with the one in [Ret21].</footnote>
orders and cographs. The difficulty of presenting this combination of commutative and non-
commutative connectives in the sequent calculus triggered the development of the *calculus of
structures* [GS01], the first proper deep inference proof formalism.<fnref n="3" />

This leads to the strange situation that we have two logics, pomset logic and BV, which
are both conservative extensions of multiplicative linear logic with mix (MLL+mix) [FR94]
with a noncommutative connective $\triangleleft$ such that $A \otimes B \vdash A \triangleleft B$ and $A \triangleleft B \vdash A \otimes B$, and which
both obey a cut elimination result—the only difference being that pomset logic only had a
proof net syntax but no deductive proof system, and BV only had a deductive proof system
but no proof nets. This naturally led to the conjecture that both logics are the same [Str03b].

In this paper we show that this conjecture is false. It can easily be shown [Str03b, Str03a, Ret99b] that every theorem in BV is also a theorem of pomset logic, and for the sake of clarity, we also give a proof in this paper (in Section 3.1). However, the converse is not true, and we give an example of a formula that is a theorem of pomset logic but not provable in BV (in Section 3.2).

This naturally leads to the question of complexity. Do both logics have the same or
different complexity? It has been observed in [Kah08] that provability in BV is **NP**-complete.
The reason is that **NP**-hardness is inherited from MLL+mix, and containment in **NP** follows
from the fact that the size of every proof in BV is polynomial in the size of the conclusion,
and the correctness of such a proof can be checked in time which is linear in the size of the
proof (see Section 4.2 for more details). However, provability in pomset logic is $\Sigma_2^P$-complete.
Even though the size of a pomset logic proof net is polynomial in the size of its conclusion,
checking correctness of such a proof net is **coNP**-complete. The details for these results are
discussed in Sections 4.3–4.5.

This complexity result explains why it is impossible to give a deductive proof system
(in the sense of Cook and Reckhow [CR79]) for pomset logic. Nonetheless, there is a recent
proposal by Slavnov [Sla19] for a decorated sequent calculus for pomset logic. We look at
this calculus in Section 5.4 and relate it to our complexity result. Before that, we show in
Section 5.1 that the sequent calculus with cut, that Retoré proposed for pomset logic is in
fact a sound and complete sequent calculus for BV.<fnref n="4" />

In summary, the paper makes the following contributions:

* In Section 2, we give a gentle and easy accessible introduction to pomset logic and BV.
  We unify the notation and terminology, and present some important properties, that will
  be needed in later sections.

* In Section 3, we are showing that BV is properly contained in pomset logic, by showing that every theorem of BV is a theorem of pomset logic, but not vice versa. These results have already been presented in [NS22], of which this article is an extended version.

* In Section 4, we are discussing the complexity of pomset logic and BV. More precisely, we are recalling Kahramanoğulları's result on the **NP**-completeness of BV, and we show that checking correctness of a pomset logic proof is **coNP**-complete and that provability in pomset logic is $\Sigma_2^P$-complete.

* Finally, in Section 5, we come back to the sequent calculus, discussing the difficulties that the two logics pose, and how they can or cannot be overcome.

<footnote n="3">³An introductory survey on deep inference can be found in [ATS19].</footnote>

<footnote n="4">⁴In fact, in various publications on pomset logic, Retoré proposes different sequent calculi (one in his PhD thesis [Ret93, Chapitre 8], one in [Ret97a, Section 7], and more recently another on in [Ret21]); we work here with the one in [Ret21].</footnote>
<figure><img src="image_3.png" /><figcaption>FIGURE 1. The equations defining $≡$.</figcaption></figure>

## 2. PRELIMINARIES ON POMSET LOGIC AND BV

In this section we will introduce the two logics, BV and pomset logic, together with some basic underlying graph theoretical and proof theoretical concepts. Even though pomset logic was discovered through the study of coherence semantics, we will here only discuss its syntax, as coherence spaces are not needed for the results of this paper.

**2.1. Formulas, Duality and Sequents.** The formulas of pomset logic and BV are in this paper denoted by capital Latin letters $A, B, C, \dots$ and are generated from propositional variables $a, b, c, \dots$, their duals $a^{\perp}, b^{\perp}, c^{\perp}, \dots$ and the unit $\mathbb{I}$ via the three binary connectives tensor $\otimes$, par $\prec$, and seq $\triangleleft$. We shall also be led to consider terms built with those connectives whose leaves are taken in arbitrary sets, which justifies the following more general definition.

**Definition 2.1.** The generalized formulas over the set $X$ are generated by the grammar

$$ A, B ::= \mathbb{I} \mid x \mid (A \otimes B) \mid [A \prec B] \mid \langle A \triangleleft B \rangle \quad \text{where } x \in X $$

A generalized formula is *linear* when it contains at most one occurrence of each $x \in X$.

We fix a countable set $V = \{a, b, c, \dots\}$ of propositional variables. To each variable $a$ we injectively associate a dual $a^{\perp}$; we write $V^{\perp} = \{a^{\perp} \mid a \in V\}$, and require that $V \cap V^{\perp} = \emptyset$. An *atom* is either a variable (*positive atom*) or the dual of a variable (*negative atom*). A *formula* is a generalized formula over the set of atoms $V \cup V^{\perp}$.

**Definition 2.2.** The size of a generalized formula $A$ over the set $X$, denoted by $|A|$, is the number of occurrences of elements of $X$ in $A$.

For better readability of large formulas, we use here different kinds of parentheses for the different connectives.<fnref n="5" /> In the following, we omit outermost parentheses for better readability.

**Definition 2.3.** We define the relation $≡$ on generalized formulas to be the smallest congruence generated by the rules of Figure 1. Those correspond to associativity of $\otimes, \prec, \triangleleft$, commutativity of $\otimes, \prec$, and unit equations ($\mathbb{I}$ behaves as unit for all three connectives).

As usual in the linear logic tradition, negation is defined not as a connective but as a mapping from formulas to formulas. Note that this does not make sense for generalized formulas.

**Definition 2.4.** The involutive (linear) negation or duality $(-)^{\perp}$ is extended from propositional variables to formulas by taking De Morgan's laws as its inductive definition:

$$ (a^{\perp})^{\perp} = a \quad \mathbb{I}^{\perp} = \mathbb{I} \quad (A \otimes B)^{\perp} = A^{\perp} \prec B^{\perp} \quad [A \prec B]^{\perp} = A^{\perp} \otimes B^{\perp} \quad \langle A \triangleleft B \rangle^{\perp} = A^{\perp} \triangleleft B^{\perp} $$

The first clause means that linear negation defines a fixed-point-free involution on the set of atoms. The last clause is what we mean when we say that seq is self-dual; note that the right-hand side is indeed $A^{\perp} \triangleleft B^{\perp}$ and not $B^{\perp} \triangleleft A^{\perp}$.<fnref n="6" />

<footnote n="5">⁵Note that this is redundant and carries no additional meaning. The only use is better readability.</footnote>

<footnote n="6">⁶In that respect, pomset logic and BV are different from other non-commutative variants of linear logic where $\otimes$ and $\prec$ are non-commutative with $(A \otimes B)^{\perp} = B^{\perp} \prec A^{\perp}$, see Section 6.1.</footnote>
<figure><img src="image_4.png" /><figcaption>FIGURE 1. The equations defining $≡$.</figcaption></figure>

## 2. PRELIMINARIES ON POMSET LOGIC AND BV

In this section we will introduce the two logics, BV and pomset logic, together with some basic underlying graph theoretical and proof theoretical concepts. Even though pomset logic was discovered through the study of coherence semantics, we will here only discuss its syntax, as coherence spaces are not needed for the results of this paper.

**2.1. Formulas, Duality and Sequents.** The formulas of pomset logic and BV are in this paper denoted by capital Latin letters $A, B, C, \dots$ and are generated from propositional variables $a, b, c, \dots$, their duals $a^{\perp}, b^{\perp}, c^{\perp}, \dots$ and the unit $\mathbb{I}$ via the three binary connectives tensor $\otimes$, par $\diamond$, and seq $\triangleleft$. We shall also be led to consider terms built with those connectives whose leaves are taken in arbitrary sets, which justifies the following more general definition.

**Definition 2.1.** The generalized formulas over the set $X$ are generated by the grammar

$$A, B ::= \mathbb{I} \mid x \mid (A \otimes B) \mid [A \diamond B] \mid \langle A \triangleleft B \rangle \quad \text{where } x \in X$$

A generalized formula is *linear* when it contains at most one occurrence of each $x \in X$.

We fix a countable set $V = \{a, b, c, \dots\}$ of propositional variables. To each variable $a$ we injectively associate a dual $a^{\perp}$; we write $V^{\perp} = \{a^{\perp} \mid a \in V\}$, and require that $V \cap V^{\perp} = \emptyset$. An *atom* is either a variable (*positive atom*) or the dual of a variable (*negative atom*). A *formula* is a generalized formula over the set of atoms $V \cup V^{\perp}$.

**Definition 2.2.** The size of a generalized formula $A$ over the set $X$, denoted by $|A|$, is the number of occurrences of elements of $X$ in $A$.

For better readability of large formulas, we use here different kinds of parentheses for the different connectives.<fnref n="5" /> In the following, we omit outermost parentheses for better readability.

**Definition 2.3.** We define the relation $≡$ on generalized formulas to be the smallest congruence generated by the rules of Figure 1. Those correspond to associativity of $\otimes, \diamond, \triangleleft$, commutativity of $\otimes, \diamond$, and unit equations ($\mathbb{I}$ behaves as unit for all three connectives).

As usual in the linear logic tradition, negation is defined not as a connective but as a mapping from formulas to formulas. Note that this does not make sense for generalized formulas.

**Definition 2.4.** The involutive (linear) negation or duality $(-)^{\perp}$ is extended from propositional variables to formulas by taking De Morgan's laws as its inductive definition:

$$(a^{\perp})^{\perp} = a \quad \mathbb{I}^{\perp} = \mathbb{I} \quad (A \otimes B)^{\perp} = A^{\perp} \diamond B^{\perp} \quad [A \diamond B]^{\perp} = A^{\perp} \otimes B^{\perp} \quad \langle A \triangleleft B \rangle^{\perp} = A^{\perp} \triangleleft B^{\perp}$$

The first clause means that linear negation defines a fixed-point-free involution on the set of atoms. The last clause is what we mean when we say that seq is self-dual; note that the right-hand side is indeed $A^{\perp} \triangleleft B^{\perp}$ and not $B^{\perp} \triangleleft A^{\perp}$.<fnref n="6" />

<footnote n="5">⁵Note that this is redundant and carries no additional meaning. The only use is better readability.</footnote>

<footnote n="6">⁶In that respect, pomset logic and BV are different from other non-commutative variants of linear logic where $\otimes$ and $\diamond$ are non-commutative with $(A \otimes B)^{\perp} = B^{\perp} \diamond A^{\perp}$, see Section 6.1.</footnote>
We will also need the notion of sequent in pomset logic. While traditional sequent calculi use multisets<fnref n="7" /> of formulas as sequents, pomset logic is thus named because its sequents are partially ordered multisets of formulas. While Retoré's early work [Ret93, Ret97a] involved arbitrary partial orders, we consider here the simplified version from [Ret21] where sequents are equipped with series-parallel orders. We shall define those orders in the next subsection (see Proposition 2.32 and Remark 2.33); for now, let us just say that those orders admit a syntactic description that we give here.

**Definition 2.5.** We denote a sequent in pomset logic by capital Greek letters Γ, Δ, ... and they are generated as follows:

$$ \Gamma, \Delta ::= \emptyset | A | [\Gamma, \Delta] | \langle\Gamma; \Delta\rangle $$

where Ø stands for the empty sequent and A can be any formula. As before, we use different kinds of brackets for better readability. Furthermore, we consider sequents equal modulo commutativity of [·, ·] and associativity of <·;·>, and the unit laws for the empty sequent:

$$ [\Gamma, \Delta] = [\Delta, \Gamma] \qquad [\Gamma, \emptyset] = \Gamma \qquad \langle\Gamma; \emptyset\rangle = \Gamma = \langle\emptyset; \Gamma\rangle $$

$$ [\Gamma, [\Delta, \Lambda]] = [\Gamma, \Delta, \Lambda] = [[\Gamma, \Delta], \Lambda] \qquad \langle\Gamma; \langle\Delta; \Lambda\rangle\rangle = \langle\Gamma; \Delta; \Lambda\rangle = \langle\langle\Gamma; \Delta\rangle; \Lambda\rangle $$

In the remainder of this paper we will always omit redundant brackets.

**Definition 2.6.** A sequent is called flat iff it does not contain the <·;·> constructor. Therefore, flat sequents can be described by multisets of formulas.

**Remark 2.7.** Pomset logic is not the only system that features “non-flat” sequents with two distinct connectives. Another famous example is the logic BI of bunched implications [OP99].

The operations [·, ·] and <·;·> serve as counterparts on sequents to the connectives ⊎ and ◁ on formulas (just as the sequent ⊢ A, B, C morally means A ∨ B ∨ C in classical logic). It is then natural to define a collapse operation<fnref n="8" /> from sequents into formulas.

**Definition 2.8.** We say that a formula A corresponds to a sequent Γ when:

* either Γ = A;

* or, inductively, there exist B and C that correspond respectively to Δ and Λ such that

- either A = B ⊎ C and Γ = [Δ, Λ];

- or A = B ◁ C and Γ = <Δ; Λ>.

We shall also say that Γ corresponds to A in this case.

For instance, a ⊎ a⊥ and a⊥ ⊎ a both correspond to [a, a⊥], but any formula also corresponds to itself as a singleton sequent. Working modulo ≡, we have:

**Proposition 2.9.** If the formulas A and B both correspond to a sequent Γ, then A ≡ B.

In the other direction, the same formula may correspond to multiple sequents. That is no longer the case, however, for a more restricted relation between “generalized sequents” over a set X, i.e. Γ, Δ ::= Ø | X | [Γ, Δ] | <Γ; Δ> modulo the same equations as Definition 2.5, and generalized ⊗-free formulas modulo ≡ over X. This relation, obtained by replacing the base case of the inductive Definition 2.8 by “Γ = x for x ∈ X”, is bijective. When X is taken to be the set of usual formulas, this gives us:

<footnote n="7">⁷This holds for commutative logics. Indeed, using multisets is equivalent to using lists and adding the exchange rule to the system.</footnote>

<footnote n="8">⁸This can be seen as the multiplication of the monad that sends X to the generalized formulas over X.</footnote>
We will also need the notion of sequent in pomset logic. While traditional sequent calculi use multisets<fnref n="7" /> of formulas as sequents, pomset logic is thus named because its sequents are partially ordered multisets of formulas. While Retoré's early work [Ret93, Ret97a] involved arbitrary partial orders, we consider here the simplified version from [Ret21] where sequents are equipped with series-parallel orders. We shall define those orders in the next subsection (see Proposition 2.32 and Remark 2.33); for now, let us just say that those orders admit a syntactic description that we give here.

**Definition 2.5.** We denote a sequent in pomset logic by capital Greek letters Γ, Δ, ... and they are generated as follows:

$$ \Gamma, \Delta ::= \emptyset | A | [\Gamma, \Delta] | \langle\Gamma; \Delta\rangle $$

where $\emptyset$ stands for the empty sequent and $A$ can be any formula. As before, we use different kinds of brackets for better readability. Furthermore, we consider sequents equal modulo commutativity of $[\cdot, \cdot]$ and associativity of $\langle\cdot; \cdot\rangle$, and the unit laws for the empty sequent:

$$ [\Gamma, \Delta] = [\Delta, \Gamma] \qquad [\Gamma, \emptyset] = \Gamma \qquad \langle\Gamma; \emptyset\rangle = \Gamma = \langle\emptyset; \Gamma\rangle $$

$$ [\Gamma, [\Delta, \Lambda]] = [\Gamma, \Delta, \Lambda] = [[\Gamma, \Delta], \Lambda] \qquad \langle\Gamma; \langle\Delta; \Lambda\rangle\rangle = \langle\Gamma; \Delta; \Lambda\rangle = \langle\langle\Gamma; \Delta\rangle; \Lambda\rangle $$

In the remainder of this paper we will always omit redundant brackets.

**Definition 2.6.** A sequent is called flat iff it does not contain the $\langle\cdot; \cdot\rangle$ constructor. Therefore, flat sequents can be described by multisets of formulas.

**Remark 2.7.** Pomset logic is not the only system that features “non-flat” sequents with two distinct connectives. Another famous example is the logic BI of bunched implications [OP99].

The operations $[\cdot, \cdot]$ and $\langle\cdot; \cdot\rangle$ serve as counterparts on sequents to the connectives $\mathcal{C}$ and $\triangleleft$ on formulas (just as the sequent $\vdash A, B, C$ morally means $A \lor B \lor C$ in classical logic). It is then natural to define a collapse operation<fnref n="8" /> from sequents into formulas.

**Definition 2.8.** We say that a formula $A$ corresponds to a sequent $\Gamma$ when:

* either $\Gamma = A$;

* or, inductively, there exist $B$ and $C$ that correspond respectively to $\Delta$ and $\Lambda$ such that

- either $A = B \mathcal{C} C$ and $\Gamma = [\Delta, \Lambda]$;

- or $A = B \triangleleft C$ and $\Gamma = \langle\Delta; \Lambda\rangle$.

We shall also say that $\Gamma$ corresponds to $A$ in this case.

For instance, $a \mathcal{C} a^{\perp}$ and $a^{\perp} \mathcal{C} a$ both correspond to $[a, a^{\perp}]$, but any formula also corresponds to itself as a singleton sequent. Working modulo $\equiv$, we have:

**Proposition 2.9.** If the formulas $A$ and $B$ both correspond to a sequent $\Gamma$, then $A \equiv B$.

In the other direction, the same formula may correspond to multiple sequents. That is no longer the case, however, for a more restricted relation between “generalized sequents” over a set $X$, i.e. $\Gamma, \Delta ::= \emptyset | X | [\Gamma, \Delta] | \langle\Gamma; \Delta\rangle$ modulo the same equations as Definition 2.5, and generalized $\mathcal{C}$-free formulas modulo $\equiv$ over $X$. This relation, obtained by replacing the base case of the inductive Definition 2.8 by “$\Gamma = x$ for $x \in X$”, is bijective. When $X$ is taken to be the set of usual formulas, this gives us:

<footnote n="7">⁷This holds for commutative logics. Indeed, using multisets is equivalent to using lists and adding the exchange rule to the system.</footnote>

<footnote n="8">⁸This can be seen as the multiplication of the monad that sends $X$ to the generalized formulas over $X$.</footnote>
**Proposition 2.10.** A sequent is the same as a generalized ⊗-free formula over the set of formulas, modulo ≡, writing Ø, [Γ, Δ] and ⟨Γ; Δ⟩ instead of I, Γ ⊎ Δ and Γ ⋄ Δ respectively.

## 2.2. Dicographs, Relation Webs and Series-Parallel Orders.
In [Ret97a], Retoré presents proof nets for pomset logic as RB-digraphs, that is, directed graphs equipped with perfect matchings, extending his reformulation of MLL+mix proof nets as undirected RB-graphs [Ret03]. We recall these notions below.

**Definition 2.11.** A digraph $\mathcal{G} = (V_G, R_G)$ consists of a finite set of vertices $V_G$ and a set of edges $R_G \subseteq V_G^2 \setminus \{(u, u) | u \in V_G\}$. A labeled digraph is a digraph $\mathcal{G}$ equipped with a map $\ell: V_G \to \mathcal{L}$ assigning each vertex $v$ of $V_G$ a label $\ell(v) \in \mathcal{L}$ in the label set $\mathcal{L}$. If $\mathcal{L}$ is the set $V \cup V^{\perp}$ of atoms, we speak of an atom-labeled digraph.

**Definition 2.12.** An isomorphism between two digraphs $\mathcal{G}$ and $\mathcal{H}$ is a bijection on vertices $f: V_G \stackrel{\sim}{\to} V_{\mathcal{H}}$ such that $f(R_G) = R_{\mathcal{H}}$, where $f(R_G) = \{(f(u), f(v)) | (u, v) \in R_G\}$. As usual, if such an $f$ exists, $\mathcal{G}$ and $\mathcal{H}$ are said to be isomorphic. Furthermore, if $\mathcal{G}$ and $\mathcal{H}$ are endowed with the vertex labelings $\ell_G$ and $\ell_{\mathcal{H}}$ respectively, and $\ell_G = \ell_{\mathcal{H}} \circ f$, then we say that $f$ is an isomorphism of labeled digraphs.

**Definition 2.13.** For a given digraph $\mathcal{G} = (V_G, R_G)$ we define the following four sets:

$$R_G^{\otimes} = \{(u, v) | (u, v) \in R_G \text{ and } (v, u) \in R_G\}$$

$$R_G^{\triangleleft} = \{(u, v) | (u, v) \in R_G \text{ and } (v, u) \notin R_G\}$$

$$R_G^{\triangleright} = \{(u, v) | (u, v) \notin R_G \text{ and } (v, u) \in R_G\}$$

$$R_G^{\mathcal{G}} = \{(u, v) | (u, v) \notin R_G \text{ and } (v, u) \notin R_G \text{ and } u \neq v\}$$

Note that these sets can be seen as binary relations and as sets of edges in the graph. We will use them interchangeably in both settings.

**Proposition 2.14.** For every digraph $\mathcal{G} = (V_G, R_G)$ we have that the relations $R_G^{\otimes}, R_G^{\triangleleft}, R_G^{\triangleright}, R_G^{\mathcal{G}}$ are pairwise disjoint and $R_G^{\otimes} \cup R_G^{\triangleleft} \cup R_G^{\triangleright} \cup R_G^{\mathcal{G}} = V_G \times V_G \setminus \{(u, u) | u \in V_G\}$. Furthermore, we have that $(u, v) \in R_G^{\triangleleft}$ iff $(v, u) \in R_G^{\triangleright}$.

**Remark 2.15.** Conversely, a set $V$ and four binary relations $R^{\otimes}, R^{\triangleleft}, R^{\triangleright}, R^{\mathcal{G}}$, such that

(1) $R^{\otimes}, R^{\triangleleft}, R^{\triangleright}, R^{\mathcal{G}}$ are pairwise disjoint,

(2) $R^{\otimes}$ and $R^{\mathcal{G}}$ are symmetric,

(3) $R^{\triangleleft} = (R^{\triangleright})^{-1}$,

(4) $R^{\otimes} \cup R^{\triangleleft} \cup R^{\triangleright} \cup R^{\mathcal{G}} = V \times V \setminus \{(v, v) | v \in V\}$

uniquely determine a digraph $(V, R^{\triangleleft} \cup R^{\otimes})$.

**Notation 2.16.** Following [Ret97a], when drawing digraphs, we use (red/regular) arrows to denote edges in $R_G^{\triangleleft}$ (and $R_G^{\triangleright}$), and arrow-free edges for $R_G^{\otimes}$. For $R_G^{\otimes}$ we use no lines at all, as in the following five examples:

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

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

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

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

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

This allows us to see $(V_G, R_G^{\otimes})$ and $(V_G, R_G^{\mathcal{G}})$ as undirected graphs.
**Proposition 2.10.** A sequent is the same as a generalized ⊗-free formula over the set of formulas, modulo ≡, writing Ø, [Γ, Δ] and ⟨Γ; Δ⟩ instead of I, Γ ⊎ Δ and Γ ◁ Δ respectively.

**2.2. Dicographs, Relation Webs and Series-Parallel Orders.** In [Ret97a], Retoré presents proof nets for pomset logic as RB-digraphs, that is, directed graphs equipped with perfect matchings, extending his reformulation of MLL+mix proof nets as undirected RB-graphs [Ret03]. We recall these notions below.

**Definition 2.11.** A digraph $\mathcal{G} = (V_G, R_G)$ consists of a finite set of vertices $V_G$ and a set of edges $R_G \subseteq V_G^2 \setminus \{(u, u) | u \in V_G\}$. A labeled digraph is a digraph $\mathcal{G}$ equipped with a map $\ell: V_G \to \mathcal{L}$ assigning each vertex $v$ of $V_G$ a label $\ell(v) \in \mathcal{L}$ in the label set $\mathcal{L}$. If $\mathcal{L}$ is the set $V \cup V^{\perp}$ of atoms, we speak of an atom-labeled digraph.

**Definition 2.12.** An isomorphism between two digraphs $\mathcal{G}$ and $\mathcal{H}$ is a bijection on vertices $f: V_G \cong V_{\mathcal{H}}$ such that $f(R_G) = R_{\mathcal{H}}$, where $f(R_G) = \{(f(u), f(v)) | (u, v) \in R_G\}$. As usual, if such an $f$ exists, $\mathcal{G}$ and $\mathcal{H}$ are said to be isomorphic. Furthermore, if $\mathcal{G}$ and $\mathcal{H}$ are endowed with the vertex labelings $\ell_G$ and $\ell_{\mathcal{H}}$ respectively, and $\ell_G = \ell_{\mathcal{H}} \circ f$, then we say that $f$ is an isomorphism of labeled digraphs.

**Definition 2.13.** For a given digraph $\mathcal{G} = (V_G, R_G)$ we define the following four sets:

$$R_G^{\otimes} = \{(u, v) | (u, v) \in R_G \text{ and } (v, u) \in R_G\}$$

$$R_G^{\triangleleft} = \{(u, v) | (u, v) \in R_G \text{ and } (v, u) \notin R_G\}$$

$$R_G^{\triangleright} = \{(u, v) | (u, v) \notin R_G \text{ and } (v, u) \in R_G\}$$

$$R_G^{\mathcal{G}} = \{(u, v) | (u, v) \notin R_G \text{ and } (v, u) \notin R_G \text{ and } u \neq v\}$$

Note that these sets can be seen as binary relations and as sets of edges in the graph. We will use them interchangeably in both settings.

**Proposition 2.14.** For every digraph $\mathcal{G} = (V_G, R_G)$ we have that the relations $R_G^{\otimes}, R_G^{\triangleleft}, R_G^{\triangleright}, R_G^{\mathcal{G}}$ are pairwise disjoint and $R_G^{\otimes} \cup R_G^{\triangleleft} \cup R_G^{\triangleright} \cup R_G^{\mathcal{G}} = V_G \times V_G \setminus \{(u, u) | u \in V_G\}$. Furthermore, we have that $(u, v) \in R_G^{\triangleleft}$ iff $(v, u) \in R_G^{\triangleright}$.

**Remark 2.15.** Conversely, a set $V$ and four binary relations $R^{\otimes}, R^{\triangleleft}, R^{\triangleright}, R^{\mathcal{G}}$, such that

(1) $R^{\otimes}, R^{\triangleleft}, R^{\triangleright}, R^{\mathcal{G}}$ are pairwise disjoint,

(2) $R^{\otimes}$ and $R^{\mathcal{G}}$ are symmetric,

(3) $R^{\triangleleft} = (R^{\triangleright})^{-1}$,

(4) $R^{\otimes} \cup R^{\triangleleft} \cup R^{\triangleright} \cup R^{\mathcal{G}} = V \times V \setminus \{(v, v) | v \in V\}$

uniquely determine a digraph $(V, R^{\triangleleft} \cup R^{\otimes})$.

**Notation 2.16.** Following [Ret97a], when drawing digraphs, we use (red/regular) arrows to denote edges in $R_G^{\triangleleft}$ (and $R_G^{\triangleright}$), and arrow-free edges for $R_G^{\otimes}$. For $R_G^{\otimes}$ we use no lines at all, as in the following five examples:

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

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

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

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

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

This allows us to see $(V_G, R_G^{\otimes})$ and $(V_G, R_G^{\mathcal{G}})$ as undirected graphs.
Let us now relate (generalized) formulas and digraphs.

**Definition 2.17.** Let $\mathcal{G} = (V_G, R_G)$ and $\mathcal{H} = (V_\mathcal{H}, R_\mathcal{H})$ be disjoint digraphs (i.e. $V_G \cap V_\mathcal{H} = \emptyset$). We can define the following operations that correspond to the connectives of pomset logic and BV:

$$ \mathcal{G} \otimes \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H}) $$

$$ \mathcal{G} \triangleleft \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H} \cup V_G \times V_\mathcal{H}) $$

$$ \mathcal{G} \otimes \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H} \cup (V_G \times V_\mathcal{H}) \cup (V_\mathcal{H} \times V_G)) $$

**Definition 2.18.** The mapping $\llbracket \cdot \rrbracket$ from linear generalized formulas over a set $X$ to digraphs with vertices in $X$ is defined inductively as follows:

$$ \llbracket \mathbb{I} \rrbracket = \emptyset \qquad \llbracket x \rrbracket = \bullet_x \qquad \llbracket A \otimes B \rrbracket = \llbracket A \rrbracket \otimes \llbracket B \rrbracket \qquad \llbracket A \triangleleft B \rrbracket = \llbracket A \rrbracket \triangleleft \llbracket B \rrbracket \qquad \llbracket A \otimes B \rrbracket = \llbracket A \rrbracket \otimes \llbracket B \rrbracket $$

where $\emptyset$ is an abbreviation for the empty graph ($\emptyset, \emptyset$) and $\bullet_x = (\{x\}, \emptyset)$ is the unique digraph that has $x$ as its single vertex. Note that linearity of formulas is required to fulfill the disjointness assumption of the previous definition.

**Definition 2.19.** If $A$ is a generalized formula over a set $X$ that is not assumed to be linear, we may translate it to a digraph as follows. Choose a linear generalized formula $A'$, a set $Y$ and a map $\ell: Y \to X$ such that $A$ is obtained from $A'$ by the substitution induced by $\ell$. Then the labeled digraph $(\llbracket A' \rrbracket, \ell)$ corresponds to $A$. We may write it $\llbracket A \rrbracket$, keeping in mind that it is only defined up to isomorphism of labeled digraphs.

**Proposition 2.20.** For every linear generalized formula $A$ we have$^9$ $|A| = |V_{\llbracket A \rrbracket}|$.

**Example 2.21.** The last digraph in Equation (2.1) is $\llbracket \langle (b \otimes a) \triangleleft d \rangle \otimes c \rrbracket$.

The point of the map $\llbracket \cdot \rrbracket$ is that it gives an intrinsic representation of (generalized) formulas modulo $\equiv$, as the following property shows.

**Theorem 2.22** [Gug07, Theorem 2.2.9]. For any two generalized formulas $A$ and $B$ over some set $X$, we have $A \equiv B$ if and only if $\llbracket A \rrbracket$ and $\llbracket B \rrbracket$ are isomorphic labeled digraphs. If $A$ and $B$ are linear, this can be stated as $A \equiv B \iff \llbracket A \rrbracket = \llbracket B \rrbracket$.

In [Gug07], this property is stated in terms of “structures” and “relation webs”. The former are just formulas modulo $\equiv$ while the latter are digraphs defined through a quadruple of relations as in Remark 2.15. Further discussion of relation webs will take place later in this subsection (Definition 2.28).

An immediate consequence of Theorem 2.22, combined with Proposition 2.9, is that we can also translate sequents into labeled digraphs.

**Corollary 2.23.** The extension of the map $\llbracket \cdot \rrbracket$ to sequents by

$$ \llbracket \Gamma, \Delta \rrbracket = \llbracket \Gamma \rrbracket \otimes \llbracket \Delta \rrbracket \quad \text{and} \quad \llbracket \langle \Gamma; \Delta \rangle \rrbracket = \llbracket \Gamma \rrbracket \triangleleft \llbracket \Delta \rrbracket $$

is well-defined up to isomorphism of labeled digraphs. Furthermore, if the formula $A$ corresponds to the sequent $\Gamma$ according to Definition 2.8, then $\llbracket A \rrbracket$ and $\llbracket \Gamma \rrbracket$ are isomorphic.

**Example 2.24.** The last digraph in Equation (2.1) is also $\llbracket \langle (b \otimes a; d) \rangle, c \rrbracket$.

<footnote>$^9$Recall that the notation $|A|$ has been introduced in Definition 2.2.</footnote>
Let us now relate (generalized) formulas and digraphs.

**Definition 2.17.** Let $\mathcal{G} = (V_G, R_G)$ and $\mathcal{H} = (V_\mathcal{H}, R_\mathcal{H})$ be disjoint digraphs (i.e. $V_G \cap V_\mathcal{H} = \emptyset$). We can define the following operations that correspond to the connectives of pomset logic and BV:

$$ \mathcal{G} \rightleftharpoons \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H}) $$

$$ \mathcal{G} \triangleleft \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H} \cup V_G \times V_\mathcal{H}) $$

$$ \mathcal{G} \otimes \mathcal{H} = (V_G \cup V_\mathcal{H}, R_G \cup R_\mathcal{H} \cup (V_G \times V_\mathcal{H}) \cup (V_\mathcal{H} \times V_G)) $$

**Definition 2.18.** The mapping $[[\cdot]]$ from linear generalized formulas over a set $X$ to digraphs with vertices in $X$ is defined inductively as follows:

$$ [[\mathbb{I}]] = \emptyset \quad [[x]] = \bullet_x \quad [[A \rightleftharpoons B]] = [[A]] \rightleftharpoons [[B]] \quad [[A \triangleleft B]] = [[A]] \triangleleft [[B]] \quad [[A \otimes B]] = [[A]] \otimes [[B]] $$

where $\emptyset$ is an abbreviation for the empty graph ($\emptyset, \emptyset$) and $\bullet_x = (\{x\}, \emptyset)$ is the unique digraph that has $x$ as its single vertex. Note that linearity of formulas is required to fulfill the disjointness assumption of the previous definition.

**Definition 2.19.** If $A$ is a generalized formula over a set $X$ that is not assumed to be linear, we may translate it to a digraph as follows. Choose a linear generalized formula $A'$, a set $Y$ and a map $\ell: Y \to X$ such that $A$ is obtained from $A'$ by the substitution induced by $\ell$. Then the labeled digraph ($[[A']], \ell$) corresponds to $A$. We may write it $[[A]]$, keeping in mind that it is only defined up to isomorphism of labeled digraphs.

**Proposition 2.20.** For every linear generalized formula $A$ we have$^9$ $|A| = |V_{[[A]]}|$.

**Example 2.21.** The last digraph in Equation (2.1) is $[[\langle(b \otimes a) \triangleleft d\rangle \rightleftharpoons c]]$.

The point of the map $[[\cdot]]$ is that it gives an intrinsic representation of (generalized) formulas modulo $\equiv$, as the following property shows.

**Theorem 2.22** [Gug07, Theorem 2.2.9]. For any two generalized formulas $A$ and $B$ over some set $X$, we have $A \equiv B$ if and only if $[[A]]$ and $[[B]]$ are isomorphic labeled digraphs. If $A$ and $B$ are linear, this can be stated as $A \equiv B \iff [[A]] = [[B]]$.

In [Gug07], this property is stated in terms of “structures” and “relation webs”. The former are just formulas modulo $\equiv$ while the latter are digraphs defined through a quadruple of relations as in Remark 2.15. Further discussion of relation webs will take place later in this subsection (Definition 2.28).

An immediate consequence of Theorem 2.22, combined with Proposition 2.9, is that we can also translate sequents into labeled digraphs.

**Corollary 2.23.** The extension of the map $[[\cdot]]$ to sequents by

$$ [[[\Gamma, \Delta]]] = [[\Gamma]] \rightleftharpoons [[\Delta]] \quad \text{and} \quad [[\langle\Gamma; \Delta\rangle]] = [[\Gamma]] \triangleleft [[\Delta]] $$

is well-defined up to isomorphism of labeled digraphs. Furthermore, if the formula $A$ corresponds to the sequent $\Gamma$ according to Definition 2.8, then $[[A]]$ and $[[\Gamma]]$ are isomorphic.

**Example 2.24.** The last digraph in Equation (2.1) is also $[[[\langle b \otimes a; d \rangle, c]]]$.

<footnote>$^9$Recall that the notation $|A|$ has been introduced in Definition 2.2.</footnote>
The next interesting question is how we can characterize the graphs that are translations of formulas or sequents. In fact, they form the class of *directed cographs* (which we shall abbreviate as “dicograph” as in [Ret21], cf. Def. 2.27); we refer to [BG18, Section 11.6] for a survey. It admits three characterizations that have been found independently in [BdGR97, Gug07, CP06]. They all rely on the notion of induced subgraph.

**Definition 2.25.** Let $\mathcal{G} = (V_G, R_G)$ be a digraph and let $V_H \subseteq V_G$. The *subdigraph of* $\mathcal{G}$ *induced by* $V_H$ is $\mathcal{H} = (V_H, R_H)$ where $R_H = R_G \cap (V_H \times V_H)$. In this case we also say that $\mathcal{H}$ is an *induced subgraph of* $\mathcal{G}$ and denote that by $\mathcal{H} \subseteq \mathcal{G}$. If additionally $V_H \subsetneq V_G$ then we write $\mathcal{H} \subset \mathcal{G}$.

We give detailed statements for the characterizations from [BdGR97, Gug07] below, for the sake of completeness, and to show that they are very similar.

**Definition 2.26.** An undirected graph is $\mathbf{P}_4$-free if it does not contain a $\mathbf{P}_4$ (shown on the left below) as induced subgraph, and a directed graph is $\mathbf{N}$-free if it does not contain an $\mathbf{N}$ (shown on the right below) as induced subgraph.

$$ \text{[Diagram]} \qquad (2.2) $$

**Definition 2.27** [BdGR97, Prop. 5.3]. A *dicograph* is a digraph $\mathcal{G} = (V_G, R_G)$ such that

(1) the undirected graph $(V_G, R_G^{\otimes})$ is $\mathbf{P}_4$-free,

(2) the directed graph $(V_G, R_G^{\downarrow})$ is $\mathbf{N}$-free, and

(3) the relation $R_G$ is weakly transitive:

• if $(u, v) \in R_G^{\downarrow}$ and $(v, w) \in R_G$ then $(u, w) \in R_G$, and

• if $(u, v) \in R_G$ and $(v, w) \in R_G^{\downarrow}$ then $(u, w) \in R_G$.

**Definition 2.28** [Gug07, Theorem 2.2.4]. A *relation web* is a tuple $(V, R^{\uparrow}, R^{\downarrow}, R^{\uparrow\downarrow}, R^{\otimes})$ obeying the four conditions in Remark 2.15 together with the following conditions:

(5) the relations $R^{\uparrow}$ and $R^{\downarrow}$ are transitive,

(6) *Triangular property*: for any $R_1, R_2, R_3 \in \{R^{\uparrow} \cup R^{\downarrow}, R^{\uparrow\downarrow}, R^{\otimes}\}$, it holds:

if $(u, v) \in R_1$ and $(v, w) \in R_2$ and $(w, u) \in R_3$ then $R_1 = R_2$ or $R_2 = R_3$ or $R_3 = R_1$,

(7) *Square property*: $(V, R^{\uparrow\downarrow})$ and $(V, R^{\uparrow\uparrow})$ are $\mathbf{P}_4$-free, and $(V, R^{\downarrow})$ is $\mathbf{N}$-free.

**Theorem 2.29.** Let $\mathcal{G}$ be a digraph. Then the following are equivalent:

(1) There is a linear generalized formula A with $\mathcal{G} = [A]$.

(2) $\mathcal{G}$ is a dicograph.

(3) $(V_G, R_G^{\uparrow\downarrow}, R_G^{\downarrow\uparrow}, R_G^{\uparrow\uparrow}, R_G^{\downarrow\downarrow})$ is a relation web.

The equivalence $1 \iff 2$ has been shown in [BdGR97, Section 5], while the equivalence $1 \iff 3$ can be found in [Gug07, Theorems 2.2.4 and 2.2.7]. A direct proof of $2 \iff 3$ is a straightforward exercise, that we encourage our readers to do by themselves.

Let us also briefly mention the characterization of dicographs from [CP06], that uses forbidden induced subgraphs as its only condition.

**Theorem 2.30** [CP06, Thm. 2]. There exists a set $F$ of 8 isomorphism classes of digraphs such that the class of digraphs whose induced subgraphs are not in $F$ coincides with the class inductively generated by the operations of Definition 2.17 starting from single-vertex graphs.

It follows from the definitions that this inductively generated class corresponds to the first item of Theorem 2.29, so this is indeed a characterization of dicographs.
The next interesting question is how we can characterize the graphs that are translations of formulas or sequents. In fact, they form the class of *directed cographs* (which we shall abbreviate as “dicograph” as in [Ret21], cf. Def. 2.27); we refer to [BG18, Section 11.6] for a survey. It admits three characterizations that have been found independently in [BdGR97, Gug07, CP06]. They all rely on the notion of induced subgraph.

**Definition 2.25.** Let $\mathcal{G} = (V_G, R_G)$ be a digraph and let $V_H \subseteq V_G$. The *subdigraph of* $\mathcal{G}$ induced by $V_H$ is $\mathcal{H} = (V_H, R_H)$ where $R_H = R_G \cap (V_H \times V_H)$. In this case we also say that $\mathcal{H}$ is an *induced subgraph of* $\mathcal{G}$ and denote that by $\mathcal{H} \subseteq \mathcal{G}$. If additionally $V_H \subsetneq V_G$ then we write $\mathcal{H} \subset \mathcal{G}$.

We give detailed statements for the characterizations from [BdGR97, Gug07] below, for the sake of completeness, and to show that they are very similar.

**Definition 2.26.** An undirected graph is $\mathbf{P}_4$-free if it does not contain a $\mathbf{P}_4$ (shown on the left below) as induced subgraph, and a directed graph is $\mathbf{N}$-free if it does not contain an $\mathbf{N}$ (shown on the right below) as induced subgraph.

$$ \text{[Diagram]} \qquad (2.2) $$

**Definition 2.27** [BdGR97, Prop. 5.3]. A *dicograph* is a digraph $\mathcal{G} = (V_G, R_G)$ such that

(1) the undirected graph $(V_G, R_G^{\otimes})$ is $\mathbf{P}_4$-free,

(2) the directed graph $(V_G, R_G^{\triangleleft})$ is $\mathbf{N}$-free, and

(3) the relation $R_G$ is weakly transitive:

• if $(u, v) \in R_G^{\triangleleft}$ and $(v, w) \in R_G$ then $(u, w) \in R_G$, and

• if $(u, v) \in R_G$ and $(v, w) \in R_G^{\triangleleft}$ then $(u, w) \in R_G$.

**Definition 2.28** [Gug07, Theorem 2.2.4]. A *relation web* is a tuple $(V, R^{\otimes}, R^{\triangleleft}, R^{\triangleright}, R^{\otimes})$ obeying the four conditions in Remark 2.15 together with the following conditions:

(5) the relations $R^{\triangleleft}$ and $R^{\triangleright}$ are transitive,

(6) *Triangular property*: for any $R_1, R_2, R_3 \in \{R^{\triangleleft} \cup R^{\triangleright}, R^{\otimes}, R^{\otimes}\}$, it holds:

if $(u, v) \in R_1$ and $(v, w) \in R_2$ and $(w, u) \in R_3$ then $R_1 = R_2$ or $R_2 = R_3$ or $R_3 = R_1$,

(7) *Square property*: $(V, R^{\otimes})$ and $(V, R^{\otimes})$ are $\mathbf{P}_4$-free, and $(V, R^{\triangleleft})$ is $\mathbf{N}$-free.

**Theorem 2.29.** Let $\mathcal{G}$ be a digraph. Then the following are equivalent:

(1) There is a linear generalized formula A with $\mathcal{G} = [A]$.

(2) $\mathcal{G}$ is a dicograph.

(3) $(V_G, R_G^{\otimes}, R_G^{\triangleleft}, R_G^{\triangleright}, R_G^{\otimes})$ is a relation web.

The equivalence $1 \iff 2$ has been shown in [BdGR97, Section 5], while the equivalence $1 \iff 3$ can be found in [Gug07, Theorems 2.2.4 and 2.2.7]. A direct proof of $2 \iff 3$ is a straightforward exercise, that we encourage our readers to do by themselves.

Let us also briefly mention the characterization of dicographs from [CP06], that uses forbidden induced subgraphs as its only condition.

**Theorem 2.30** [CP06, Thm. 2]. There exists a set $F$ of 8 isomorphism classes of digraphs such that the class of digraphs whose induced subgraphs are not in $F$ coincides with the class inductively generated by the operations of Definition 2.17 starting from single-vertex graphs.

It follows from the definitions that this inductively generated class corresponds to the first item of Theorem 2.29, so this is indeed a characterization of dicographs.
**Corollary 2.31.** Let $\mathcal{G} = (V_G, R_G)$ be a dicograph. Then any induced subdigraph of $\mathcal{G}$ is also a dicograph.

*Proof.* This is because the induced subgraph relation $\sqsubseteq$ is transitive.

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

An important special case of relation webs is when $R^{\otimes} = \emptyset$.

**Proposition 2.32.** Let $\mathcal{G}$ be a digraph. The following are equivalent:

(1) There is a linear generalized formula $A$ that does not contain $\otimes$ and such that $\mathcal{G} = [[A]]$.

(2) $\mathcal{G}$ is a dicograph and $R_{\mathcal{G}}^{\otimes} = \emptyset$, i.e. all edges are unidirectional.

Furthermore, when these conditions hold, $\mathcal{G} = (V_{\mathcal{G}}, R_{\mathcal{G}}^{\downarrow})$. For a fixed $V_{\mathcal{G}}$, the possible values for $R_{\mathcal{G}}^{\downarrow}$ are exactly those for which $\mathcal{G}$ is $\mathbf{N}$-free and $R_{\mathcal{G}}^{\uparrow}$ is transitive. Such relations are called series-parallel orders<fnref n="10" /> in the literature.

*Proof.* Let $A$ be a linear generalized formula. By structural induction on $A$, one can see that $R_{[[A]]}^{\otimes} = \emptyset$ if and only if $A$ is $\otimes$-free. The claimed equivalence then follows from the case of general dicographs we saw earlier. And by definition, $R_{\mathcal{G}}^{\downarrow}$ contains all the unidirectional edges of $\mathcal{G}$. The characterization as $\mathbf{N}$-free partial orders is just the specialization of either Definition 2.27 or Definition 2.28, but it is in fact an old classical result [VTL82, Section 4] (see also [Mö89]).

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

The operations $\triangleleft$ and $\otimes$ on digraphs (Definition 2.17) are respectively the “series composition” and “parallel composition” of partial orders. For more on series-parallel orders, see the beginning of [BG18, Section 11.6] which points to many further references.

**Remark 2.33.** Combining Propositions 2.10 and 2.32, we see that sequents are equivalent to series-parallel posets labeled by formulas up to label-preserving isomorphism, i.e. to series-parallel *partially ordered multisets* (pomsets) of formulas, as claimed in the previous subsection.

**Remark 2.34.** Another noteworthy special case of dicographs is those with $R_{\mathcal{G}}^{\downarrow} = R_{\mathcal{G}}^{\uparrow} = \emptyset$; they are the digraphs of the form $[[A]]$ where $A$ does not contain $\triangleleft$. They correspond to a class of *undirected graphs* called *cographs*, that can be defined equivalently as $\mathbf{P}_4$-free graphs (see [CLB81]). Cographs therefore provide a representation of $\mathbf{MLL+mix}$ formulas that can be used to build proof nets (analogously to the next two sections for pomset logic), see [Ret99a, Ret03].

The class of “directed cographs” has been given this name independently by [Ret99b] and [CP06]. This arguably attests that it is a natural generalization of cographs.

## 2.3. Perfect Matchings, RB-digraphs and Alternating Elementary Cycles.
We have just seen representation of formulas as graphs. In this subsection and the next one, we recall how to graphically represent pomset logic proofs as well. This requires a few graph-theoretic definitions first.

Recall that an undirected graph is 1-regular if every vertex is incident to exactly one edge, and a perfect matching of some undirected graph is a 1-regular spanning subgraph (so the notion of perfect matching is usually defined relatively to some ambient graph). As a

<footnote n="10">¹⁰Strictly speaking, series-parallel orders are a special case of *partial orders*, i.e. *reflexive* and *transitive relations*, whereas $R_G^{\downarrow}$ is *irreflexive* and *transitive*. So it is the reflexive closure of $R_G^{\downarrow}$ which is a series-parallel order, but we often harmlessly identify (reflexive) posets with the corresponding (irreflexive) digraphs.</footnote>
**Corollary 2.31.** Let $\mathcal{G} = (V_G, R_G)$ be a dicograph. Then any induced subdigraph of $\mathcal{G}$ is also a dicograph.

*Proof.* This is because the induced subgraph relation $\sqsubseteq$ is transitive.

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

An important special case of relation webs is when $R^{\otimes} = \emptyset$.

**Proposition 2.32.** Let $\mathcal{G}$ be a digraph. The following are equivalent:

(1) There is a linear generalized formula $A$ that does not contain $\otimes$ and such that $\mathcal{G} = [[A]]$.

(2) $\mathcal{G}$ is a dicograph and $R_G^{\otimes} = \emptyset$, i.e. all edges are unidirectional.

Furthermore, when these conditions hold, $\mathcal{G} = (V_G, R_G^{\downarrow})$. For a fixed $V_G$, the possible values for $R_G^{\downarrow}$ are exactly those for which $\mathcal{G}$ is $\mathbf{N}$-free and $R_G^{\uparrow}$ is transitive. Such relations are called series-parallel orders<fnref n="10" /> in the literature.

*Proof.* Let $A$ be a linear generalized formula. By structural induction on $A$, one can see that $R_{[[A]]}^{\otimes} = \emptyset$ if and only if $A$ is $\otimes$-free. The claimed equivalence then follows from the case of general dicographs we saw earlier. And by definition, $R_G^{\downarrow}$ contains all the unidirectional edges of $\mathcal{G}$. The characterization as $\mathbf{N}$-free partial orders is just the specialization of either Definition 2.27 or Definition 2.28, but it is in fact an old classical result [VTL82, Section 4] (see also [Mö89]).

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

The operations $\triangleleft$ and $\otimes$ on digraphs (Definition 2.17) are respectively the “series composition” and “parallel composition” of partial orders. For more on series-parallel orders, see the beginning of [BG18, Section 11.6] which points to many further references.

**Remark 2.33.** Combining Propositions 2.10 and 2.32, we see that sequents are equivalent to series-parallel posets labeled by formulas up to label-preserving isomorphism, i.e. to series-parallel *partially ordered multisets* (pomsets) of formulas, as claimed in the previous subsection.

**Remark 2.34.** Another noteworthy special case of dicographs is those with $R_G^{\downarrow} = R_G^{\uparrow} = \emptyset$; they are the digraphs of the form $[[A]]$ where $A$ does not contain $\triangleleft$. They correspond to a class of *undirected graphs* called *cographs*, that can be defined equivalently as $\mathbf{P}_4$-free graphs (see [CLB81]). Cographs therefore provide a representation of $\mathbf{MLL+mix}$ formulas that can be used to build proof nets (analogously to the next two sections for pomset logic), see [Ret99a, Ret03].

The class of “directed cographs” has been given this name independently by [Ret99b] and [CP06]. This arguably attests that it is a natural generalization of cographs.

## 2.3. Perfect Matchings, RB-digraphs and Alternating Elementary Cycles.
We have just seen representation of formulas as graphs. In this subsection and the next one, we recall how to graphically represent pomset logic proofs as well. This requires a few graph-theoretic definitions first.

Recall that an undirected graph is 1-regular if every vertex is incident to exactly one edge, and a perfect matching of some undirected graph is a 1-regular spanning subgraph (so the notion of perfect matching is usually defined relatively to some ambient graph). As a

<footnote n="10">¹⁰Strictly speaking, series-parallel orders are a special case of *partial orders*, i.e. *reflexive* and *transitive relations*, whereas $R_G^{\downarrow}$ is *irreflexive* and *transitive*. So it is the reflexive closure of $R_G^{\downarrow}$ which is a series-parallel order, but we often harmlessly identify (reflexive) posets with the corresponding (irreflexive) digraphs.</footnote>
slight abuse of language, we use “perfect matching” in this paper to designate a directed
counterpart to 1-regular graphs.

**Definition 2.35.** We say that a digraph $\mathcal{G} = (V_G, E_G)$ is a *perfect matching* when

(1) any vertex has exactly one outgoing edge in $E_G$ and exactly one incoming edge in $E_G$, i.e., for every $u \in V_G$ there is a single pair $(v, w) \in V_G^2$ such that $(u, v) \in E_G$ and $(w, u) \in E_G$, and

(2) all edges are bidirectional, i.e. for all $u, v \in V_G$, we have that $(u, v) \in E_G$ iff $(v, u) \in E_G$. This means, in particular, that in the previous item, $v = w$.

**Definition 2.36.** An *RB-digraph* $\mathcal{G} = (V_G, R_G, B_G)$ is a triple where $(V_G, R_G)$ is an arbitrary digraph and $(V_G, B_G)$ is a perfect matching. We call the edges in $B_G$ the *matching edges* or *B-edges*, and those in $R_G$ the *non-matching edges* or *R-edges*. We say that $\mathcal{G}$ is an *RB-dicograph* iff $(V_G, R_G)$ is a dicograph.

Following Definition 2.12, we define an *isomorphism* between $\mathcal{G}$ and another RB-digraph $\mathcal{H} = (V_{\mathcal{H}}, R_{\mathcal{H}}, B_{\mathcal{H}})$ to be a bijection $f: V_G \xrightarrow{\sim} V_{\mathcal{H}}$ such that $f(R_G) = R_{\mathcal{H}}$ and $f(B_G) = B_{\mathcal{H}}$. This extends in the only sensible way to a notion of isomorphism between labeled RB-digraphs.

**Notation 2.37.** In all figures representing RB-digraphs, we will (following [Ret99b]) draw the matching edges **bold and blue**, while the non-matching edges will be drawn **regular and red**.

**Example 2.38.** Here are six examples of RB-digraphs.

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

In the first two, the underlying digraphs are not dicographs. But the other four examples
are RB-dicographs.

**Definition 2.39.** Let $\mathcal{G} = (V_G, E_G)$ be a digraph and $n \in \mathbb{N}$ with $n \ge 2$. An *elementary path* of length $n$ in $\mathcal{G}$ is a sequence of vertices $u_0, \dots, u_n \in V_G$ *without repetitions* such that $(u_i, u_{i+1}) \in E_G$ for all $i \in \{0, \dots, n-1\}$ (so the length counts the number of edges, not of vertices). An *elementary cycle* is defined in the same way except there is the single repetition $u_n = u_0$ (so the length of an elementary cycle is both its number of vertices and its number of edges).

An *alternating elementary path* (or *æ-path*) in an RB-digraph $(V_G, R_G, B_G)$ is an elementary path $u_0, \dots, u_n$ in the digraph $(V_G, R_G \cup B_G)$ such that<fnref n="11" />:

• either $(u_i, u_{i+1}) \in R_G$ when $i$ is odd and $(u_i, u_{i+1}) \in B_G$ when $i$ is even,

• or $(u_i, u_{i+1}) \in R_G$ when $i$ is even and $(u_i, u_{i+1}) \in B_G$ when $i$ is odd.

An *alternating elementary cycle* (or *æ-cycle*) in $(V_G, R_G, B_G)$ is an elementary cycle of even length in $(V_G, R_G \cup B_G)$ that satisfies the above alternation condition. Morally, the parity condition ensures that the cycle also alternates between $(u_{n-1}, u_n)$ and $(u_1, u_2)$, or equivalently that the “change of base points” $u'_i = u_{i+k \mod n}$ sends æ-cycles to æ-cycles.

**Example 2.40.** The first and the fifth graph in Example 2.38 do not contain an æ-cycle. In all other graphs in that example, the four vertices form an æ-cycle.

<footnote n="11">¹¹One could be tempted to simplify this definition by saying that for any two consecutive edges, one is in $R_G$ and the other in $B_G$; the issue, however, is that $R_G$ and $B_G$ are not required to be disjoint.</footnote>
slight abuse of language, we use “perfect matching” in this paper to designate a directed
counterpart to 1-regular graphs.

**Definition 2.35.** We say that a digraph $\mathcal{G} = (V_G, E_G)$ is a *perfect matching* when

(1) any vertex has exactly one outgoing edge in $E_G$ and exactly one incoming edge in $E_G$, i.e., for every $u \in V_G$ there is a single pair $(v, w) \in V_G^2$ such that $(u, v) \in E_G$ and $(w, u) \in E_G$, and

(2) all edges are bidirectional, i.e. for all $u, v \in V_G$, we have that $(u, v) \in E_G$ iff $(v, u) \in E_G$. This means, in particular, that in the previous item, $v = w$.

**Definition 2.36.** An *RB-digraph* $\mathcal{G} = (V_G, R_G, B_G)$ is a triple where $(V_G, R_G)$ is an arbitrary digraph and $(V_G, B_G)$ is a perfect matching. We call the edges in $B_G$ the *matching edges* or *B-edges*, and those in $R_G$ the *non-matching edges* or *R-edges*. We say that $\mathcal{G}$ is an *RB-dicograph* iff $(V_G, R_G)$ is a dicograph.

Following Definition 2.12, we define an *isomorphism* between $\mathcal{G}$ and another RB-digraph $\mathcal{H} = (V_{\mathcal{H}}, R_{\mathcal{H}}, B_{\mathcal{H}})$ to be a bijection $f: V_G \stackrel{\sim}{\to} V_{\mathcal{H}}$ such that $f(R_G) = R_{\mathcal{H}}$ and $f(B_G) = B_{\mathcal{H}}$. This extends in the only sensible way to a notion of isomorphism between labeled RB-digraphs.

**Notation 2.37.** In all figures representing RB-digraphs, we will (following [Ret99b]) draw the matching edges **bold and blue**, while the non-matching edges will be drawn **regular and red**.

**Example 2.38.** Here are six examples of RB-digraphs.

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

In the first two, the underlying digraphs are not dicographs. But the other four examples
are RB-dicographs.

**Definition 2.39.** Let $\mathcal{G} = (V_G, E_G)$ be a digraph and $n \in \mathbb{N}$ with $n \ge 2$. An *elementary path* of length $n$ in $\mathcal{G}$ is a sequence of vertices $u_0, \dots, u_n \in V_G$ *without repetitions* such that $(u_i, u_{i+1}) \in E_G$ for all $i \in \{0, \dots, n-1\}$ (so the length counts the number of edges, not of vertices). An *elementary cycle* is defined in the same way except there is the single repetition $u_n = u_0$ (so the length of an elementary cycle is both its number of vertices and its number of edges).

An *alternating elementary path* (or *æ-path*) in an RB-digraph $(V_G, R_G, B_G)$ is an elementary path $u_0, \dots, u_n$ in the digraph $(V_G, R_G \cup B_G)$ such that<fnref n="11" />:

• either $(u_i, u_{i+1}) \in R_G$ when $i$ is odd and $(u_i, u_{i+1}) \in B_G$ when $i$ is even,

• or $(u_i, u_{i+1}) \in R_G$ when $i$ is even and $(u_i, u_{i+1}) \in B_G$ when $i$ is odd.

An *alternating elementary cycle* (or *æ-cycle*) in $(V_G, R_G, B_G)$ is an elementary cycle of even length in $(V_G, R_G \cup B_G)$ that satisfies the above alternation condition. Morally, the parity condition ensures that the cycle also alternates between $(u_{n-1}, u_n)$ and $(u_1, u_2)$, or equivalently that the “change of base points” $u'_i = u_{i+k \mod n}$ sends æ-cycles to æ-cycles.

**Example 2.40.** The first and the fifth graph in Example 2.38 do not contain an æ-cycle. In all other graphs in that example, the four vertices form an æ-cycle.

<footnote n="11">¹¹One could be tempted to simplify this definition by saying that for any two consecutive edges, one is in $R_G$ and the other in $B_G$; the issue, however, is that $R_G$ and $B_G$ are not required to be disjoint.</footnote>
The existence or non-existence of æ-cycles in RB-dicographs will play a central role in this paper. We note in passing that in the classical theory of matchings in *undirected graphs*, the absence of æ-cycles admits alternative characterizations and entails deep structural properties, which have been applied to MLL+mix proof nets [Ret03, Ngu20].

**Definition 2.41.** Let $u_0, \dots, u_{n-1}, u_n = u_0$ be an elementary cycle in $\mathcal{G} = (V_G, E_G)$. An edge $(v, w) \in E_G$ is a chord for this cycle when $v = u_i$ and $w = u_j$ for some $i, j \in \{0, \dots, n-1\}$ such that $i \not= j + 1 \pmod n$ and $j \not= i + 1 \pmod n$. That is, both vertices $v$ and $w$ occur in the cycle but the edges $(v, w)$ and $(w, v)$ are not part of the cycle. A cycle is chordless if it does not admit any chord in $\mathcal{G}$. A chordless æ-cycle in an RB-digraph $(V_G, R_G, B_G)$ is an æ-cycle which has no chord in the total digraph $(V_G, R_G \cup B_G)$. Note that since $B_G$ is a perfect matching, if an æ-cycle admits a chord, then this chord is necessarily in $R_G \setminus B_G$.

**Example 2.42.** In Example 2.38, the æ-cycles in the second and sixth graph admit chords. The æ-cycles in the third and fourth graph are chordless.

**2.4. Pomset Logic, Proof Nets and Balanced Formulas.** A proof in multiplicative linear logic (MLL) is given by its conclusion (a formula or a sequent) and an *axiom linking*. This can be drawn as a graph, which consists of the formula tree (or sequent forest) with additional edges representing the axiom links, i.e., connecting those leaves of the tree which are matched by an axiom in the proof. In order to distinguish the actual proofs in the set of all such graphs, a so-called *correctness criterion* is employed, and the graphical structures that obey this criterion are called *proof nets*.

In [Ret97a], Retoré generalized this idea from the formulas/sequents of MLL to those that we introduced in Section 2.1. There exist many different equivalent correctness criteria for MLL, and one of Retoré's main achievements was to figure out which criterion allows for a generalization to include the seq connective $\triangleleft$. There are in fact two such criteria, and their versions for MLL and MLL+mix have been presented in [Ret03]. They are both based on RB-graphs, and we are now going to give an exposition of their extension to RB-digraphs, as presented in [Ret97a, Ret99b, Ret21].

First, the notion of axiom linking is the same as for MLL.

**Definition 2.43.** A *pomset logic pre-proof* of a formula or a sequent is an involution $\ell$ on its set of atom occurrences such that an atom is always mapped to its dual. This $\ell$ is also called an *axiom linking*.

**Example 2.44.** The sequent $[a^{\perp} \succcurlyeq a^{\perp}, a \otimes a]$ has two possible axiom linkings.

Throughout this paper, the class of formulas for which there is a single possible choice of axiom linking will play an important role.

**Definition 2.45.** A formula is *balanced* if every propositional variable that occurs in A occurs exactly once positively and exactly once negatively. (Equivalently, a formula is balanced when it is *linear* and its set of occurring atoms is closed under duality.) Using the correspondence of Definition 2.8, this extends to a notion of *balanced sequent*. A balanced formula *A* uniquely determines an axiom linking on A, that we denote by $\ell(A)$. Similarly, we write $\ell(\Gamma)$ for the unique axiom linking on a balanced sequent $\Gamma$.<fnref n="12" />

<footnote n="12">¹²Balanced formulas for classical logic are discussed in detail in [Str12, Section 7].</footnote>
The existence or non-existence of æ-cycles in RB-dicographs will play a central role in this paper. We note in passing that in the classical theory of matchings in *undirected graphs*, the absence of æ-cycles admits alternative characterizations and entails deep structural properties, which have been applied to MLL+mix proof nets [Ret03, Ngu20].

**Definition 2.41.** Let $u_0, \dots, u_{n-1}, u_n = u_0$ be an elementary cycle in $\mathcal{G} = (V_G, E_G)$. An edge $(v, w) \in E_G$ is a chord for this cycle when $v = u_i$ and $w = u_j$ for some $i, j \in \{0, \dots, n-1\}$ such that $i \not= j + 1 \pmod n$ and $j \not= i + 1 \pmod n$. That is, both vertices $v$ and $w$ occur in the cycle but the edges $(v, w)$ and $(w, v)$ are not part of the cycle. A cycle is chordless if it does not admit any chord in $\mathcal{G}$. A chordless æ-cycle in an RB-digraph $(V_G, R_G, B_G)$ is an æ-cycle which has no chord in the total digraph $(V_G, R_G \cup B_G)$. Note that since $B_G$ is a perfect matching, if an æ-cycle admits a chord, then this chord is necessarily in $R_G \setminus B_G$.

**Example 2.42.** In Example 2.38, the æ-cycles in the second and sixth graph admit chords. The æ-cycles in the third and fourth graph are chordless.

**2.4. Pomset Logic, Proof Nets and Balanced Formulas.** A proof in multiplicative linear logic (MLL) is given by its conclusion (a formula or a sequent) and an *axiom linking*. This can be drawn as a graph, which consists of the formula tree (or sequent forest) with additional edges representing the axiom links, i.e., connecting those leaves of the tree which are matched by an axiom in the proof. In order to distinguish the actual proofs in the set of all such graphs, a so-called *correctness criterion* is employed, and the graphical structures that obey this criterion are called *proof nets*.

In [Ret97a], Retoré generalized this idea from the formulas/sequents of MLL to those that we introduced in Section 2.1. There exist many different equivalent correctness criteria for MLL, and one of Retoré's main achievements was to figure out which criterion allows for a generalization to include the seq connective $\triangleleft$. There are in fact two such criteria, and their versions for MLL and MLL+mix have been presented in [Ret03]. They are both based on RB-graphs, and we are now going to give an exposition of their extension to RB-digraphs, as presented in [Ret97a, Ret99b, Ret21].

First, the notion of axiom linking is the same as for MLL.

**Definition 2.43.** A *pomset logic pre-proof* of a formula or a sequent is an involution $\ell$ on its set of atom occurrences such that an atom is always mapped to its dual. This $\ell$ is also called an *axiom linking*.

**Example 2.44.** The sequent $[a^{\perp} \succcurlyeq a^{\perp}, a \otimes a]$ has two possible axiom linkings.

Throughout this paper, the class of formulas for which there is a single possible choice of axiom linking will play an important role.

**Definition 2.45.** A formula is *balanced* if every propositional variable that occurs in A occurs exactly once positively and exactly once negatively. (Equivalently, a formula is balanced when it is *linear* and its set of occurring atoms is closed under duality.) Using the correspondence of Definition 2.8, this extends to a notion of *balanced sequent*. A balanced formula *A* uniquely determines an axiom linking on A, that we denote by $\ell(A)$. Similarly, we write $\ell(\Gamma)$ for the unique axiom linking on a balanced sequent $\Gamma$.<fnref n="12" />

<footnote n="12">¹²Balanced formulas for classical logic are discussed in detail in [Str12, Section 7].</footnote>
As we have seen in the previous subsections, one can represent a formula as a dicograph, where the atom occurrences are the vertices and the edges are determined by the connectives. More traditionally, one can also associate a syntax tree to a formula. Each of these two graphical representations has an associated correctness criterion, based on æ-cycles in RB-digraphs. We now present those two criteria, starting with dicographs.

**Definition 2.46.** Let $\Gamma$ be a sequent and $\ell$ be an axiom linking for $\Gamma$. The cographic RB-prenet of $\Gamma$ and $\ell$, denoted by $\rho(\Gamma, \ell)$, is the RB-dicograph $\mathcal{G} = (V_G, E_G, B_G)$ where $(V_G, E_G) = [\Gamma]$, and we have $(x, y) \in B_G$ iff the atom occurrences in $\Gamma$ that correspond to $x$ and $y$ are mapped to each other by the axiom linking $\ell$.

**Example 2.47.** The sequent $[\langle a; a \rangle, \langle a^{\perp}; a^{\perp} \rangle]$ admits two possible axiom linkings, and the two corresponding cographic RB-prenets are the fourth and the fifth graph in Example 2.38.

**Definition 2.48.** If $A$ is a balanced formula, we write $([A])$ for the cographic RB-prenet $\rho(A, \ell(A))$, i.e., $([A]) = (V_A, R_A, B_A)$, where $(V_A, R_A) = [A]$ and $B_A$ is the matching associated to $\ell(A)$.

**Proposition 2.49.** Every RB-dicograph is isomorphic to some $([A])$ where $A$ is a balanced formula.

*Proof*. Let $\mathcal{G} = (V_G, R_G, B_G)$ be given. We can label the vertices in $V_G$ with distinct atoms, such that two atoms are dual if and only if they are matched by $B_G$. Then $A$ exists by Theorem 2.29, since $(V_G, R_G)$ is a dicograph. $\square$

**Definition 2.50.** A cographic RB-prenet is *correct* if it does not contain any chordless æ-cycle. A correct cographic RB-prenet is also called a *cographic RB-net*.

**Definition 2.51.** A sequent $\Gamma$ is *provable in pomset logic* if there is an axiom linking $\ell$ for $\Gamma$, such that $\rho(\Gamma, \ell)$ is correct. In that case, $\rho(\Gamma, \ell)$ (or simply $\ell$) is a *pomset logic proof* of $\Gamma$.

**Example 2.52.** The last two graphs in Example 2.38 are pomset logic proofs for the balanced formulas $\langle a \triangleleft b \rangle \rightleftharpoons \langle a^{\perp} \triangleleft b^{\perp} \rangle$ and $[a \rightleftharpoons a^{\perp}] \otimes [b \rightleftharpoons b^{\perp}]$, respectively.

The following theorem says that pomset logic is a conservative extension of MLL+mix.

**Theorem 2.53** [Ret03, Theorem 7] (see also Remark 2.34). Let $\Gamma$ be a flat sequent without any occurrence of $\triangleleft$, and let $\ell$ be an axiom linking for $\Gamma$. Then $\ell$ is the axiom linking of an MLL+mix sequent proof iff $\rho(\Gamma, \ell)$ is correct.

The second correctness criterion, that we are going to show now, is more in the tradition of other known correctness criteria for MLL+mix, as it works on a structure that is directly derived from the formula trees. More precisely, we define inductively for each formula $C$ its RB-tree, denoted as $\mathcal{T}_{\text{RB}}(C)$, as shown in Figure 2. Technically speaking this not a tree in the graph-theoretical sense, but we use the name as it carries the structure of the formula tree.

If we have a sequent $\Gamma$, then $\mathcal{T}_{\text{RB}}(\Gamma)$ is obtained from the RB-trees of the formulas in $\Gamma$ which are connected at the roots via the edges corresponding to the series-parallel order of the sequent structure (see the discussion following Proposition 2.32). In order to obtain an RB-digraph, we need to add the $B$-edges corresponding to the linking $\ell$. We denote this RB-digraph by $\tau(\Gamma, \ell)$ and call it the *tree-like RB-prenet* of $\Gamma$ and $\ell$.

**Example 2.54.** The two graphs in Figure 3 show the two tree-like RB-prenets, corresponding to the two axiom linkings for $\langle a \triangleleft a \rangle \rightleftharpoons \langle a^{\perp} \triangleleft a^{\perp} \rangle$.
As we have seen in the previous subsections, one can represent a formula as a dicograph, where the atom occurrences are the vertices and the edges are determined by the connectives. More traditionally, one can also associate a syntax tree to a formula. Each of these two graphical representations has an associated correctness criterion, based on æ-cycles in RB-digraphs. We now present those two criteria, starting with dicographs.

**Definition 2.46.** Let $\Gamma$ be a sequent and $\ell$ be an axiom linking for $\Gamma$. The cographic RB-prenet of $\Gamma$ and $\ell$, denoted by $\rho(\Gamma, \ell)$, is the RB-dicograph $\mathcal{G} = (V_G, E_G, B_G)$ where $(V_G, E_G) = [\Gamma]$, and we have $(x, y) \in B_G$ iff the atom occurrences in $\Gamma$ that correspond to $x$ and $y$ are mapped to each other by the axiom linking $\ell$.

**Example 2.47.** The sequent $[\langle a; a \rangle, \langle a^{\perp}; a^{\perp} \rangle]$ admits two possible axiom linkings, and the two corresponding cographic RB-prenets are the fourth and the fifth graph in Example 2.38.

**Definition 2.48.** If $A$ is a balanced formula, we write $([A])$ for the cographic RB-prenet $\rho(A, \ell(A))$, i.e., $([A]) = (V_A, R_A, B_A)$, where $(V_A, R_A) = [A]$ and $B_A$ is the matching associated to $\ell(A)$.

**Proposition 2.49.** Every RB-dicograph is isomorphic to some $([A])$ where $A$ is a balanced formula.

*Proof*. Let $\mathcal{G} = (V_G, R_G, B_G)$ be given. We can label the vertices in $V_G$ with distinct atoms, such that two atoms are dual if and only if they are matched by $B_G$. Then $A$ exists by Theorem 2.29, since $(V_G, R_G)$ is a dicograph. $\square$

**Definition 2.50.** A cographic RB-prenet is *correct* if it does not contain any chordless æ-cycle. A correct cographic RB-prenet is also called a *cographic RB-net*.

**Definition 2.51.** A sequent $\Gamma$ is *provable in pomset logic* if there is an axiom linking $\ell$ for $\Gamma$, such that $\rho(\Gamma, \ell)$ is correct. In that case, $\rho(\Gamma, \ell)$ (or simply $\ell$) is a *pomset logic proof* of $\Gamma$.

**Example 2.52.** The last two graphs in Example 2.38 are pomset logic proofs for the balanced formulas $\langle a \triangleleft b \rangle \rightleftharpoons \langle a^{\perp} \triangleleft b^{\perp} \rangle$ and $[a \rightleftharpoons a^{\perp}] \otimes [b \rightleftharpoons b^{\perp}]$, respectively.

The following theorem says that pomset logic is a conservative extension of MLL+mix.

**Theorem 2.53** [Ret03, Theorem 7] (see also Remark 2.34). Let $\Gamma$ be a flat sequent without any occurrence of $\triangleleft$, and let $\ell$ be an axiom linking for $\Gamma$. Then $\ell$ is the axiom linking of an MLL+mix sequent proof iff $\rho(\Gamma, \ell)$ is correct.

The second correctness criterion, that we are going to show now, is more in the tradition of other known correctness criteria for MLL+mix, as it works on a structure that is directly derived from the formula trees. More precisely, we define inductively for each formula $C$ its RB-tree, denoted as $\mathcal{T}_{\text{RB}}(C)$, as shown in Figure 2. Technically speaking this not a tree in the graph-theoretical sense, but we use the name as it carries the structure of the formula tree.

If we have a sequent $\Gamma$, then $\mathcal{T}_{\text{RB}}(\Gamma)$ is obtained from the RB-trees of the formulas in $\Gamma$ which are connected at the roots via the edges corresponding to the series-parallel order of the sequent structure (see the discussion following Proposition 2.32). In order to obtain an RB-digraph, we need to add the $B$-edges corresponding to the linking $\ell$. We denote this RB-digraph by $\tau(\Gamma, \ell)$ and call it the *tree-like RB-prenet* of $\Gamma$ and $\ell$.

**Example 2.54.** The two graphs in Figure 3 show the two tree-like RB-prenets, corresponding to the two axiom linkings for $\langle a \triangleleft a \rangle \rightleftharpoons \langle a^{\perp} \triangleleft a^{\perp} \rangle$.
<figure><img src="image_12.png" /><figcaption>FIGURE 2. Inductive definition of RB-trees (which are not quite trees in the sense of graph theory, though they resemble the syntax trees of formulas). The root vertex is at the bottom.</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>FIGURE 3. Two tree-like RB-prenets for the formula $\langle a \triangleleft a \rangle \otimes \langle a^{\perp} \triangleleft a^{\perp} \rangle$. The left one is a correct proof net, while the right one contains an æ-cycle involving the 4 topmost matching edges.</figcaption></figure>

Below we give an alternative, more formal definition of $\tau(\Gamma, \ell)$.

**Definition 2.55.** Let A be a formula. We define two *unfoldings* of A, denoted by $A^b$ and $A^\sharp$, to be flat sequents which are obtained as follows. For each non-atomic subformula occurrence B of A, we introduce a fresh propositional variable $z_B$. If A is atomic, then $A^b = A$ and $A^\sharp = \emptyset$. Otherwise $A^b = [z_A, A^\sharp]$ and $A^\sharp$ is defined inductively as follows:

$$ 
\begin{align} 
\mathbb{I}^{\sharp} &= z_{\mathbb{I}}^{\perp} \notag \\ 
[B \otimes C]^{\sharp} &= [z_{B \otimes C}^{\perp} \otimes [z_B \otimes z_C], B^{\sharp}, C^{\sharp}] \tag{2.3} \\ 
\langle B \triangleleft C \rangle^{\sharp} &= [z_{B \triangleleft C}^{\perp} \otimes \langle z_B \triangleleft z_C \rangle, B^{\sharp}, C^{\sharp}] \notag \\ 
(B \otimes C)^{\sharp} &= [z_{B \otimes C}^{\perp} \otimes (z_B \otimes z_C), B^{\sharp}, C^{\sharp}] \notag 
\end{align} 
$$

Let $\Gamma$ be a sequent, and let $A_1, \dots, A_n$ be the formula occurrences of $\Gamma$. Then we define $\Gamma^b = [\Gamma_0, A_1^\sharp, \dots, A_n^\sharp]$, where $\Gamma_0$ is $\Gamma$ with every $A_i$ replaced by $z_{A_i}$.

**Remark 2.56.** It is important to note that in Definition 2.55 every subformula occurrence gets a fresh variable, in particular, in Equation (2.3) every occurrence of $\mathbb{I}$ in A is assigned
<figure><img src="image_13.png" /><figcaption>FIGURE 2. Inductive definition of RB-trees (which are not quite trees in the sense of graph theory, though they resemble the syntax trees of formulas). The root vertex is at the bottom.</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>FIGURE 3. Two tree-like RB-prenets for the formula $\langle a \triangleleft a \rangle \otimes \langle a^{\perp} \triangleleft a^{\perp} \rangle$. The left one is a correct proof net, while the right one contains an æ-cycle involving the 4 topmost matching edges.</figcaption></figure>

Below we give an alternative, more formal definition of $\tau(\Gamma, \ell)$.

**Definition 2.55.** Let A be a formula. We define two *unfoldings* of A, denoted by $A^b$ and $A^\sharp$, to be flat sequents which are obtained as follows. For each non-atomic subformula occurrence B of A, we introduce a fresh propositional variable $z_B$. If A is atomic, then $A^b = A$ and $A^\sharp = \emptyset$. Otherwise $A^b = [z_A, A^\sharp]$ and $A^\sharp$ is defined inductively as follows:

$$ 
\begin{align} 
\mathbb{I}^{\sharp} &= z_{\mathbb{I}}^{\perp} \notag \\ 
[B \otimes C]^{\sharp} &= [z_{B \otimes C}^{\perp} \otimes [z_B \otimes z_C], B^{\sharp}, C^{\sharp}] \tag{2.3} \\ 
\langle B \triangleleft C \rangle^{\sharp} &= [z_{B \triangleleft C}^{\perp} \otimes \langle z_B \triangleleft z_C \rangle, B^{\sharp}, C^{\sharp}] \notag \\ 
(B \otimes C)^{\sharp} &= [z_{B \otimes C}^{\perp} \otimes (z_B \otimes z_C), B^{\sharp}, C^{\sharp}] \notag 
\end{align} 
$$

Let $\Gamma$ be a sequent, and let $A_1, \dots, A_n$ be the formula occurrences of $\Gamma$. Then we define $\Gamma^b = [\Gamma_0, A_1^\sharp, \dots, A_n^\sharp]$, where $\Gamma_0$ is $\Gamma$ with every $A_i$ replaced by $z_{A_i}$.

**Remark 2.56.** It is important to note that in Definition 2.55 every subformula occurrence gets a fresh variable, in particular, in Equation (2.3) every occurrence of $\mathbb{I}$ in A is assigned
a fresh $z_\llcorner$, and these variables have to be indexed accordingly. Then the graph $\mathcal{T}_{\text{RB}}(\Gamma)$ is in fact $[\Gamma^\flat]$ equipped with a $B$-edge for every fresh $z-z^\perp$ pair. When drawn as in Figure 3, we label the vertical $B$-edges with the corresponding subformula $A$, and the lower vertex represents $z_A$ and the upper vertex $z_A^\perp$.

**Definition 2.57.** Let $\Gamma$ be a sequent and $\ell$ an axiom linking for $\Gamma$. We define the linking $\ell^\flat$ for $\Gamma^\flat$ to be the linking obtained from $\ell$ by mapping each fresh $z_A$ to $z_A^\perp$, and vice versa. Then the *tree-like RB-prenet* of $\Gamma$ and $\ell$ is defined as $\tau(\Gamma, \ell) = \rho(\Gamma^\flat, \ell^\flat)$.

The correctness criterion for tree-like RB-prenets is exactly the same as for cographic RB-prenets, except that in a tree-like RB-prenet every æ-cycle is automatically chordless. Therefore we have the following definition.

**Definition 2.58.** A tree-like RB-prenet is *correct* if and only if it does not contain any æ-cycle. A correct tree-like RB-prenet is also called a *tree-like RB-net*.

**Example 2.59.** In Figure 3, the left RB-prenet is correct, while the one on the right is not.

In [Ret99b], Retoré has shown the equivalence of the two correctness criteria.

**Theorem 2.60** [Ret99b, Theorem 7]. For every sequent $\Gamma$ and linking $\ell$, we have that $\rho(\Gamma, \ell)$ is correct if and only if $\tau(\Gamma, \ell)$ is correct.

In the remainder of this paper we will use the term *pomset logic proof net*, or *proof net* for short, for correct prenets of both kinds, i.e., for cographic RB-nets and tree-like RB-nets. This is justified, as the two can be trivially transformed into each other in linear time.

Pomset logic proof nets can easily be extended with cut. A *cut* in a sequent is a formula of the shape $C \otimes C^\perp$. Then the cut elimination theorem can be stated as follows:

**Theorem 2.61** [Ret97a, Theorem 7]. Let $\Gamma$ be a sequent formed by the formulas $A_1, \dots, A_n$, $C_1 \otimes C_1^\perp, \dots, C_k \otimes C_k^\perp$, and let $\Gamma'$ be obtained from $\Gamma$ by removing $C_1 \otimes C_1^\perp, \dots, C_k \otimes C_k^\perp$. If there is a *pomset logic proof net* for $\Gamma$, then there is also one for $\Gamma'$.

**2.5. System BV and the Calculus of Structures.** *System BV*, introduced by Guglielmi in [Gug99, Gug07], is a deductive system for the formulas defined in Section 2.1. It is defined in the formalism called the *calculus of structures*, and it works similar to a rewriting system, modulo the equational theory defined in Figure 1.

The inference rules of *system BV* and its symmetric version *system SBV* are shown in Figure 4. These rules have to be read as rewriting rule schemes, meaning that (1) the variable *a* can be substituted by any atom, and the variables *A*, *B*, *C*, *D* can be substituted by any formula, and that (2) the rules can be applied inside any (positive) context.

More formally, a *context* $S\{\cdot\}$ is a formula which contains exactly one occurrence of the hole $\{\cdot\}$ in place of an atom:

$$S\{\cdot\} ::= \{\cdot\} | S\{\cdot\} \otimes A | A \otimes S\{\cdot\} | S\{\cdot\} \triangleleft A | A \triangleleft S\{\cdot\} | S\{\cdot\} \otimes A | A \otimes S\{\cdot\}$$

Given a context $S\{\cdot\}$ and a formula *A*, we write $S\{A\}$ to denote the formula that is obtained from $S\{\cdot\}$ by replacing the hole $\{\cdot\}$ with *A*.

**Example 2.62.** Let the context $S\{\cdot\} = \langle a \triangleleft \{\cdot\} \triangleleft b \rangle \otimes (c \otimes a^\perp)$ and the formula $A = c^\perp \otimes d$ be given. Then $S\{A\} = \langle a \triangleleft (c^\perp \otimes d) \triangleleft b \rangle \otimes (c \otimes a^\perp)$.
a fresh $z_\llcorner$, and these variables have to be indexed accordingly. Then the graph $\mathcal{T}_{\text{RB}}(\Gamma)$ is in fact $[\Gamma^\flat]$ equipped with a $B$-edge for every fresh $z-z^\perp$ pair. When drawn as in Figure 3, we label the vertical $B$-edges with the corresponding subformula $A$, and the lower vertex represents $z_A$ and the upper vertex $z_A^\perp$.

**Definition 2.57.** Let $\Gamma$ be a sequent and $\ell$ an axiom linking for $\Gamma$. We define the linking $\ell^\flat$ for $\Gamma^\flat$ to be the linking obtained from $\ell$ by mapping each fresh $z_A$ to $z_A^\perp$, and vice versa. Then the tree-like RB-prenet of $\Gamma$ and $\ell$ is defined as $\tau(\Gamma, \ell) = \rho(\Gamma^\flat, \ell^\flat)$.

The correctness criterion for tree-like RB-prenets is exactly the same as for cographic RB-prenets, except that in a tree-like RB-prenet every $\ae$-cycle is automatically chordless. Therefore we have the following definition.

**Definition 2.58.** A tree-like RB-prenet is *correct* if and only if it does not contain any $\ae$-cycle. A correct tree-like RB-prenet is also called a *tree-like RB-net*.

**Example 2.59.** In Figure 3, the left RB-prenet is correct, while the one on the right is not.

In [Ret99b], Retoré has shown the equivalence of the two correctness criteria.

**Theorem 2.60** [Ret99b, Theorem 7]. For every sequent $\Gamma$ and linking $\ell$, we have that $\rho(\Gamma, \ell)$ is correct if and only if $\tau(\Gamma, \ell)$ is correct.

In the remainder of this paper we will use the term *pomset logic proof net*, or *proof net* for short, for correct prenets of both kinds, i.e., for cographic RB-nets and tree-like RB-nets. This is justified, as the two can be trivially transformed into each other in linear time.

Pomset logic proof nets can easily be extended with cut. A *cut* in a sequent is a formula of the shape $C \otimes C^\perp$. Then the cut elimination theorem can be stated as follows:

**Theorem 2.61** [Ret97a, Theorem 7]. Let $\Gamma$ be a sequent formed by the formulas $A_1, \dots, A_n$, $C_1 \otimes C_1^\perp, \dots, C_k \otimes C_k^\perp$, and let $\Gamma'$ be obtained from $\Gamma$ by removing $C_1 \otimes C_1^\perp, \dots, C_k \otimes C_k^\perp$. If there is a pomset logic proof net for $\Gamma$, then there is also one for $\Gamma'$.

**2.5. System BV and the Calculus of Structures.** *System BV*, introduced by Guglielmi in [Gug99, Gug07], is a deductive system for the formulas defined in Section 2.1. It is defined in the formalism called the *calculus of structures*, and it works similar to a rewriting system, modulo the equational theory defined in Figure 1.

The inference rules of *system BV* and its symmetric version *system SBV* are shown in Figure 4. These rules have to be read as rewriting rule schemes, meaning that (1) the variable $a$ can be substituted by any atom, and the variables $A, B, C, D$ can be substituted by any formula, and that (2) the rules can be applied inside any (positive) context.

More formally, a *context* $S\{\cdot\}$ is a formula which contains exactly one occurrence of the hole $\{\cdot\}$ in place of an atom:

$$S\{\cdot\} ::= \{\cdot\} | S\{\cdot\} \otimes A | A \otimes S\{\cdot\} | S\{\cdot\} \triangleleft A | A \triangleleft S\{\cdot\} | S\{\cdot\} \otimes A | A \otimes S\{\cdot\}$$

Given a context $S\{\cdot\}$ and a formula $A$, we write $S\{A\}$ to denote the formula that is obtained from $S\{\cdot\}$ by replacing the hole $\{\cdot\}$ with $A$.

**Example 2.62.** Let the context $S\{\cdot\} = \langle a \triangleleft \{\cdot\} \triangleleft b \rangle \otimes (c \otimes a^\perp)$ and the formula $A = c^\perp \otimes d$ be given. Then $S\{A\} = \langle a \triangleleft (c^\perp \otimes d) \triangleleft b \rangle \otimes (c \otimes a^\perp)$.
<figure><img src="image_14.png" /><figcaption>FIGURE 4. System BV (the first two columns) and SBV (all 3 columns).</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>FIGURE 5. A proof in BV. We highlight the principal subformula in the conclusion of each rule instance. Furthermore, instances of $\equiv$ are left implicit and are omitted. For example, in the premise of the bottommost $ai\downarrow$, we have $\langle c^\perp \triangleleft e^\perp \triangleleft f^\perp \rangle \equiv \langle c^\perp \triangleleft (\mathbb{I} \otimes \langle e^\perp \triangleleft f^\perp \rangle) \rangle$, involving the equations of unit for $\otimes$, and associativity of $\triangleleft$. Another example is the conclusion of the second $q\downarrow$ from the top, where we have $e^\perp \otimes b^\perp \otimes \langle e \triangleleft b \rangle \equiv \langle \mathbb{I} \triangleleft [b^\perp \otimes e^\perp] \rangle \otimes \langle e \triangleleft b \rangle$, involving the equations of associativity and commututativity of $\otimes$, and unit for $\triangleleft$.</figcaption></figure>

If $\mathfrak{r} \frac{A}{B}$ is an inference rule and $S\{\cdot\}$ a context, then $\mathfrak{r} \frac{S\{A\}}{S\{B\}}$ is an instance of the rule. A (proof) system is a set of inference rules. We write $s\|\delta$, or more concisely $A \vdash_S^\delta B$, if there is a derivation from $A$ to $B$ using only rules from the system $S$, and that derivation is named $\delta$. If in that situation $A = \mathbb{I}$, then we write it as $S\|\delta_B$ or simply as $\vdash_S^\delta B$ and call $\delta$ a *proof of* $B$. In this case we say that $B$ is *provable* in $S$. We also omit the annotation $\delta$ when we want to assert the mere existence of a derivation or proof, without giving it a name.

Figure 5 shows an example for a proof in BV.
<figure><img src="image_15.png" /><figcaption>FIGURE 4. System BV (the first two columns) and SBV (all 3 columns).</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>FIGURE 5. A proof in BV. We highlight the principal subformula in the conclusion of each rule instance. Furthermore, instances of $\equiv$ are left implicit and are omitted. For example, in the premise of the bottommost $ai_↓$, we have $\langle c^⊥ \triangleleft e^⊥ \triangleleft f^⊥ \rangle \equiv \langle c^⊥ \triangleleft (\mathbb{I} \otimes \langle e^⊥ \triangleleft f^⊥ \rangle) \rangle$, involving the equations of unit for $\otimes$, and associativity of $\triangleleft$. Another example is the conclusion of the second $q_↓$ from the top, where we have $e^⊥ \otimes b^⊥ \otimes \langle e \triangleleft b \rangle \equiv \langle \mathbb{I} \triangleleft [b^⊥ \otimes e^⊥] \rangle \otimes \langle e \triangleleft b \rangle$, involving the equations of associativity and commututativity of $\otimes$, and unit for $\triangleleft$.</figcaption></figure>

If $\mathfrak{r} \frac{A}{B}$ is an inference rule and $S\{\cdot\}$ a context, then $\mathfrak{r} \frac{S\{A\}}{S\{B\}}$ is an instance of the rule. A (proof) system is a set of inference rules. We write $s\|\delta$, or more concisely $A \vdash_S^\delta B$, if there is a derivation from $A$ to $B$ using only rules from the system $S$, and that derivation is named $\delta$. If in that situation $A = \mathbb{I}$, then we write it as $S\|\delta_B$ or simply as $\vdash_S^\delta B$ and call $\delta$ a *proof of* $B$. In this case we say that $B$ is *provable in* $S$. We also omit the annotation $\delta$ when we want to assert the mere existence of a derivation or proof, without giving it a name.

Figure 5 shows an example for a proof in BV.
We now recall some basic properties of BV and SBV. First, observe that the rules $ai_↓$ (called *atomic interaction down* or *axiom*) and $ai_↑$ (called *atomic interaction up* or *cut*) are in atomic form. Their general forms

$$ i_↓ \frac{\mathbb{I}}{A \otimes A^{\perp}} \quad \text{and} \quad i_↑ \frac{A \otimes A^{\perp}}{\mathbb{I}} \qquad (2.4) $$

are derivable.

**Definition 2.63.** An inference rule $r$ is derivable in a system $S$ iff for every instance $r \frac{A}{B}$ there is a derivation $A \vdash_S B$. An inference rule $r$ is admissible for a system $S$ iff for every proof $\vdash_{S \cup \{r\}} A$ there is a proof $\vdash_S B$.

**Proposition 2.64.** *The rule $i_↓$ is derivable in BV, and the rule $i_↑$ is derivable in SBV.*

The proof is standard and can be found in many papers (e.g., [Gug07, GS01, ATS19]).
We are now going to state the cut elimination property for BV.

**Definition 2.65.** Two system $S_1$ and $S_2$ are equivalent if they prove the same formulas.

**Theorem 2.66 [GS01, Gug07].** *Systems BV and SBV are equivalent.*

A proof of this result can be found in [Gug07] and in [Str03b].

**Theorem 2.67 [GS01, Gug07].** *The general cut rule $i_↑$ is admissible for BV.*

This is an immediate corollary of Proposition 2.64 and Theorem 2.66. Finally, the relation between BV and SBV can be strengthened to the following statement:

**Corollary 2.68.** *For any two formulas A and B, we have $\vdash_{BV} A^{\perp} \otimes B$ iff $A \vdash_{SBV} B$.*

**2.6. Unit-Free Versions of BV and SBV.** One of the main reasons to study cut-free systems is to have a deductive system that is suitable for doing proof search. However, due to the versatility of the unit $\mathbb{I}$ in formulas, proof search in plain BV as it is shown in Figure 4 is not practical. In order to reduce the non-determinism in BV, Kahramanoğulları proposed in [Kah04] a unit-free version of BV which is better suited for proof search. As this system is also easier to handle for some results we show in this paper, we introduce BVu below. For didactic reasons, we also introduce its symmetric version SBVu.

The formulas for BVu are the same as defined in Section 2.1, except that we do not allow any occurrence of the unit $\mathbb{I}$. This means that we have to restrict the equivalence defined in Figure 1 to the unit-free formulas. We define the relation $\equiv'$ to be the smallest congruence generated by

$$ \begin{align} A \otimes (B \otimes C) &\equiv' (A \otimes B) \otimes C & A \otimes B &\equiv' B \otimes A \notag \\ A \otimes [B \otimes C] &\equiv' [A \otimes B] \otimes C & A \otimes B &\equiv' B \otimes A \tag{2.5} \\ A \triangleleft \langle B \triangleleft C \rangle &\equiv' \langle A \triangleleft B \rangle \triangleleft C \notag \end{align} $$

The inference rules for BVu and SBVu are then shown in Figure 6. Note that the rule $ai_↓$ has no premise. It is an axiom that is used exactly once in a *proof* which in BVu or SBVu is a derivation without premise (as the unit $\mathbb{I}$ is not present and cannot take this role). Likewise, the rule $ai_↑$ has no conclusion. It is used exactly once in a *refutation*, which is a derivation with empty conclusion.

We have the following immediate results.
We now recall some basic properties of BV and SBV. First, observe that the rules $ai_↓$ (called *atomic interaction down* or *axiom*) and $ai_↑$ (called *atomic interaction up* or *cut*) are in atomic form. Their general forms

$$ i_↓ \frac{\mathbb{I}}{A \otimes A^{\perp}} \quad \text{and} \quad i_↑ \frac{A \otimes A^{\perp}}{\mathbb{I}} \qquad (2.4) $$

are derivable.

**Definition 2.63.** An inference rule $r$ is derivable in a system $S$ iff for every instance $r \frac{A}{B}$ there is a derivation $A \vdash_S B$. An inference rule $r$ is admissible for a system $S$ iff for every proof $\vdash_{S \cup \{r\}} A$ there is a proof $\vdash_S B$.

**Proposition 2.64.** The rule $i_↓$ is derivable in BV, and the rule $i_↑$ is derivable in SBV.

The proof is standard and can be found in many papers (e.g., [Gug07, GS01, ATS19]). We are now going to state the cut elimination property for BV.

**Definition 2.65.** Two system $S_1$ and $S_2$ are equivalent if they prove the same formulas.

**Theorem 2.66 [GS01, Gug07].** Systems BV and SBV are equivalent.

A proof of this result can be found in [Gug07] and in [Str03b].

**Theorem 2.67 [GS01, Gug07].** The general cut rule $i_↑$ is admissible for BV.

This is an immediate corollary of Proposition 2.64 and Theorem 2.66. Finally, the relation between BV and SBV can be strengthened to the following statement:

**Corollary 2.68.** For any two formulas $A$ and $B$, we have $\vdash_{BV} A^{\perp} \otimes B$ iff $A \vdash_{SBV} B$.

**2.6. Unit-Free Versions of BV and SBV.** One of the main reasons to study cut-free systems is to have a deductive system that is suitable for doing proof search. However, due to the versatility of the unit $\mathbb{I}$ in formulas, proof search in plain BV as it is shown in Figure 4 is not practical. In order to reduce the non-determinism in BV, Kahramanoğulları proposed in [Kah04] a unit-free version of BV which is better suited for proof search. As this system is also easier to handle for some results we show in this paper, we introduce BVu below. For didactic reasons, we also introduce its symmetric version SBVu.

The formulas for BVu are the same as defined in Section 2.1, except that we do not allow any occurrence of the unit $\mathbb{I}$. This means that we have to restrict the equivalence defined in Figure 1 to the unit-free formulas. We define the relation $\equiv'$ to be the smallest congruence generated by

$$ \begin{align} A \otimes (B \otimes C) &\equiv' (A \otimes B) \otimes C & A \otimes B &\equiv' B \otimes A \notag \\ A \otimes [B \otimes C] &\equiv' [A \otimes B] \otimes C & A \otimes B &\equiv' B \otimes A \tag{2.5} \\ A \triangleleft \langle B \triangleleft C \rangle &\equiv' \langle A \triangleleft B \rangle \triangleleft C \notag \end{align} $$

The inference rules for BVu and SBVu are then shown in Figure 6. Note that the rule $ai_↓$ has no premise. It is an axiom that is used exactly once in a *proof* which in BVu or SBVu is a derivation without premise (as the unit $\mathbb{I}$ is not present and cannot take this role). Likewise, the rule $ai_↑$ has no conclusion. It is used exactly once in a *refutation*, which is a derivation with empty conclusion.

We have the following immediate results.
<figure><img src="image_16.png" /><figcaption>FIGURE 6. System BVu (first 3 columns) and system SBVu (all 5 columns).</figcaption></figure>

**Proposition 2.69.** Let A and B be unit-free formulas. We have $A \vdash_{SBVu} B$ iff $A \vdash_{SBV} B$.

*Proof.* If we have a derivation $A \vdash_{SBVu} B$, then we immediately have a derivation $A \vdash_{SBV} B$, as every rule in SBVu (except for $ai^o\downarrow$ and $ai^o\uparrow$) is derivable in SBV. Conversely, assume we have a derivation $A \vdash_{SBV} B$. Then, in $\delta$, the unit $\mathbb{I}$ can occur. Let $\delta'$ be obtained from $\delta$ by deleting the unit $\mathbb{I}$ everywhere. Then every instance of the rule $\equiv$ becomes an instance of $\equiv'$; every instance of $q\downarrow$ becomes an instance of $q_2\downarrow$ or $q_3^L\downarrow$ or $q_3^R\downarrow$ or $q_4\downarrow$ or trivial (i.e., premise and conclusion of the rule instance become equal); and similarly for $s$ and $q\uparrow$. However, an instance of $ai\downarrow$ can become an instance of $ai^\otimes\downarrow$ or $ai^\otimes\uparrow$ or $ai^\otimes\downarrow$ (which are in SBVu), or $ai^\otimes\uparrow$ which is shown on the left below. Similarly, an instance of $ai\uparrow$ can become an instance of $ai^\otimes\uparrow$ or $ai^\otimes\downarrow$, or $ai^\otimes\uparrow$, or $ai^\otimes\downarrow$ which is shown on the right below:

$$ai^\otimes\downarrow \frac{B}{a \otimes a^\perp \otimes B} \qquad ai^\otimes\uparrow \frac{a \otimes a^\perp \otimes B}{B} \qquad (2.6)$$

These rules are not in SBVu, but they can be derived with $\{ai^\otimes\downarrow, s_2\}$ and $\{ai^\otimes\uparrow, s_2\}$, respectively. $\square$

**Proposition 2.70** [Kah04]. *The systems BVu and BV are equivalent.*

*Proof.* First, if we have a proof $\vdash_{BVu} A$ then we can simply replace the top instance of $ai^o\downarrow$ by $ai\downarrow$ and have a proof of BV. Conversely, a proof in BV can be transformed into a proof of BVu by replacing the axiom $ai^o\downarrow$ by a $ai\downarrow$ and then following the same procedure as in the previous proof. $\square$

From these propositions we can immediately obtain the cut elimination results for BVu via the corresponding results for BV:

**Corollary 2.71.** *The systems BVu and SBVu are equivalent.*

**Corollary 2.72.** For any two unit-free formulas we have that $\vdash_{BVu} A^\perp \otimes B$ iff $A \vdash_{SBVu} B$.

**Corollary 2.73.** *The general cut rules*

$$i^{\otimes\uparrow} \frac{(A \otimes A^{\perp}) \otimes B}{B} \qquad i^{\otimes\uparrow} \frac{A \otimes A^{\perp} \otimes B}{B} \qquad i^{\downarrow\uparrow} \frac{(A \otimes A^{\perp}) \triangle B}{B} \qquad i^{\downarrow\uparrow} \frac{B \triangle (A \otimes A^{\perp})}{B} \qquad (2.7)$$

are admissible for BVu.
<figure><img src="image_17.png" /><figcaption>FIGURE 6. System BVu (first 3 columns) and system SBVu (all 5 columns).</figcaption></figure>

**Proposition 2.69.** Let A and B be unit-free formulas. We have $A \vdash_{SBVu} B$ iff $A \vdash_{SBV} B$.

*Proof.* If we have a derivation $A \vdash_{SBVu} B$, then we immediately have a derivation $A \vdash_{SBV} B$, as every rule in SBVu (except for $ai^o\downarrow$ and $ai^o\uparrow$) is derivable in SBV. Conversely, assume we have a derivation $A \vdash_{SBV} B$. Then, in $\delta$, the unit $\mathbb{I}$ can occur. Let $\delta'$ be obtained from $\delta$ by deleting the unit $\mathbb{I}$ everywhere. Then every instance of the rule $\equiv$ becomes an instance of $\equiv'$; every instance of $q\downarrow$ becomes an instance of $q_2\downarrow$ or $q_3^L\downarrow$ or $q_3^R\downarrow$ or $q_4\downarrow$ or trivial (i.e., premise and conclusion of the rule instance become equal); and similarly for $s$ and $q\uparrow$. However, an instance of $ai\downarrow$ can become an instance of $ai^\otimes\downarrow$ or $ai^\otimes\downarrow$ or $ai^\otimes\uparrow$ (which are in SBVu), or $ai^\otimes\downarrow$ which is shown on the left below. Similarly, an instance of $ai\uparrow$ can become an instance of $ai^\otimes\uparrow$ or $ai^\otimes\uparrow$, or $ai^\otimes\uparrow$ which is shown on the right below:

$$ai^\otimes\downarrow \frac{B}{a \otimes a^\perp \otimes B} \qquad ai^\otimes\uparrow \frac{a \otimes a^\perp \otimes B}{B} \qquad (2.6)$$

These rules are not in SBVu, but they can be derived with $\{ai^\otimes\downarrow, s_2\}$ and $\{ai^\otimes\uparrow, s_2\}$, respectively. $\square$

**Proposition 2.70** [Kah04]. *The systems BVu and BV are equivalent.*

*Proof.* First, if we have a proof $\vdash_{BVu} A$ then we can simply replace the top instance of $ai^o\downarrow$ by $ai\downarrow$ and have a proof of BV. Conversely, a proof in BV can be transformed into a proof of BVu by replacing the axiom $ai^o\downarrow$ by a $ai\downarrow$ and then following the same procedure as in the previous proof. $\square$

From these propositions we can immediately obtain the cut elimination results for BVu via the corresponding results for BV:

**Corollary 2.71.** *The systems BVu and SBVu are equivalent.*

**Corollary 2.72.** For any two unit-free formulas we have that $\vdash_{BVu} A^\perp \otimes B$ iff $A \vdash_{SBVu} B$.

**Corollary 2.73.** *The general cut rules*

$$i^{\otimes\uparrow} \frac{(A \otimes A^{\perp}) \otimes B}{B} \qquad i^{\otimes\uparrow} \frac{A \otimes A^{\perp} \otimes B}{B} \qquad i^{\downarrow\uparrow} \frac{(A \otimes A^{\perp}) \triangleleft B}{B} \qquad i^{\downarrow\uparrow} \frac{B \triangleleft (A \otimes A^{\perp})}{B} \qquad (2.7)$$

are admissible for BVu.
**Remark 2.74.** Our version of BVu is slightly different from the one by Kahramanoğulları. In [Kah04] the rule $s_2$ is absent, and instead the rule $ai^{\otimes\downarrow}$ shown in Equation (2.6) is part of the system. We chose our variation because it is better suited for the results of this paper (e.g. Theorem 2.78 and the proofs in Section 3). But it is easy to see that the two variants of BVu are equivalent: first, as we have mentioned above, the rule $ai^{\otimes\downarrow}$ is derivable in ${ai^{\otimes\downarrow}, s_2}$, and second, the rule $s_2$ is admissible if $ai^{\otimes\downarrow}$ is present. This can be seen by an easy induction on the size of the derivation. However, note that the same trick does not work for the rule $q_2\downarrow$. This rule cannot be shown admissible, as the formula $\langle a \triangleleft [b \otimes c] \rangle \otimes \langle [a^{\perp} \otimes b^{\perp}] \triangleleft c^{\perp} \rangle$ is not provable in BVu without $q_2\downarrow$.

**Remark 2.75.** The logical rules of SBVu, i.e., the bottom two lines in the Figure 6, have already been studied by Retoré in [Ret99b], as a rewrite system on digraphs to generate theorems of pomset logic. We will study the relation between pomset logic and BV/BVu in the next section.

In some sections of this paper we also need a variant of BVu that we call BVû and that is obtained from BVu by restricting rules $q_2\downarrow$ and $s_2$ to cases where neither A nor B has a $\otimes$ as main connective, i.e., we replace $q_2\downarrow$ and $s_2$ by $\hat{q}_2\downarrow$ and $\hat{s}_2$, respectively:

$$ \hat{q}_2\downarrow \frac{A \triangleleft B}{A \otimes B} \qquad \hat{s}_2 \frac{A \otimes B}{A \otimes B} \qquad \begin{array}{l} \text{where } A \not\equiv' C \otimes D \text{ and } B \not\equiv' C \otimes D \text{ for} \\ \text{any formulas } C \text{ and } D. \end{array} \qquad (2.8) $$

and similarly, by restricting the rules $q_3^\perp\downarrow$, $q_3^R\downarrow$, and $s_3$ to cases where C does not have a $\otimes$ as main connective, i.e., these three rules are replaced by $\hat{q}_3^\perp\downarrow$, $\hat{q}_3^R\downarrow$, and $\hat{s}_3$, respectively:

$$ \hat{q}_3^\perp\downarrow \frac{[A \otimes C] \triangleleft B}{\langle A \triangleleft B \rangle \otimes C} \qquad \hat{q}_3^R\downarrow \frac{A \triangleleft [B \otimes C]}{\langle A \triangleleft B \rangle \otimes C} \qquad \hat{s}_3 \frac{[A \otimes C] \otimes B}{(A \otimes B) \otimes C} \qquad \begin{array}{l} \text{where } C \not\equiv' D \otimes E \text{ for} \\ \text{any formulas } D \text{ and } E. \end{array} \qquad (2.9) $$

**Proposition 2.76.** The systems BVu and BVû are equivalent.

*Proof.* Any derivation in BVû is also a derivation in BVu. Conversely, the rules $q_2\downarrow$ and $s_2$ and $s_3$ are derivable with ${\hat{q}_2\downarrow, \hat{q}_3^\perp\downarrow, \hat{q}_3^R\downarrow, \equiv'}$ and ${\hat{s}_2, \hat{s}_3, \equiv'}$ and ${\hat{s}_3, \equiv'}$, respectively, as shown below:

$$ \begin{align*} \hat{q}_3^R\downarrow & \frac{[A' \otimes A''] \triangleleft [B' \otimes B'']}{\langle [A' \otimes A''] \triangleleft B' \rangle \otimes B''} \\ \hat{q}_3^\perp\downarrow & \frac{\langle A' \triangleleft B' \rangle \otimes A'' \otimes B''}{A' \otimes B' \otimes A'' \otimes B''} \\ \hat{q}_2\downarrow & \equiv' \frac{A' \otimes B' \otimes A'' \otimes B''}{[A' \otimes A''] \otimes [B' \otimes B'']} \\ & \equiv', \hat{s}_3, \equiv' \frac{[A' \otimes A''] \otimes [B' \otimes B'']}{([A' \otimes A''] \otimes B') \otimes B''} \\ & \qquad \hat{s}_3 \frac{([A' \otimes C', C'']) \otimes B}{([A' \otimes C'] \otimes C'') \otimes B} \\ & \qquad \hat{s}_3 \frac{([A' \otimes C'] \otimes B) \otimes C''}{([A' \otimes C'] \otimes B) \otimes C''} \\ & \equiv' \frac{([A \otimes B) \otimes C'] \otimes C''}{(A \otimes B) \otimes [C'' \otimes C'')} \\ & \qquad \hat{s}_3 \frac{([A \otimes B) \otimes C'] \otimes C''}{(A \otimes B) \otimes [C'' \otimes C'')} \\ & \equiv' \frac{([A \otimes C'] \otimes C'')}{([A' \otimes A''] \otimes B') \otimes B''} \\ & \qquad \hat{s}_2 \frac{([A' \otimes B'] \otimes A'' \otimes B'')}{A' \otimes B' \otimes A'' \otimes B''} \\ & \qquad \hat{s}_2 \frac{([A' \otimes C'] \otimes C'')}{[A' \otimes A''] \otimes [B' \otimes B'']} \\ & \equiv' \frac{[A' \otimes A''] \otimes [B' \otimes B'']}{[A' \otimes A''] \otimes [B' \otimes B'']}. \end{align*} $$

and similarly, the rules $q_3^\perp\downarrow$ and $q_3^R\downarrow$ are derivable in ${\hat{q}_3^\perp\downarrow, \equiv'}$ and ${\hat{q}_3^R\downarrow, \equiv'}$, respectively. $\square$

**2.7. SBVu and Dicograph Inclusions.** To wrap up these long preliminaries, we recall here some useful results that also provide some motivation for the rules of SBV and SBVu. The starting observation is that the non-interaction rules preserve the atoms of a formula, so they can be seen as digraph rewriting rules preserving the set of vertices. The following results, due to Béchet, de Groote and Retoré [BdGR97], elucidate the combinatorial meaning of this rewriting system.

First, let us consider the case of unit-free formulas *without the tensor connective* $\otimes$. Recall that according to Proposition 2.32, such formulas modulo $\equiv'$ correspond to *series-parallel orders* on their atom occurrences.
**Remark 2.74.** Our version of BVu is slightly different from the one by Kahramanoğulları. In [Kah04] the rule $s_2$ is absent, and instead the rule $a^i \otimes \downarrow$ shown in Equation (2.6) is part of the system. We chose our variation because it is better suited for the results of this paper (e.g. Theorem 2.78 and the proofs in Section 3). But it is easy to see that the two variants of BVu are equivalent: first, as we have mentioned above, the rule $a^i \otimes \downarrow$ is derivable in ${a^i \otimes \downarrow, s_2}$, and second, the rule $s_2$ is admissible if $a^i \otimes \downarrow$ is present. This can be seen by an easy induction on the size of the derivation. However, note that the same trick does not work for the rule $q_2 \downarrow$. This rule cannot be shown admissible, as the formula $\langle a \triangleleft [b \otimes c] \rangle \otimes \langle [a^{\perp} \otimes b^{\perp}] \triangleleft c^{\perp} \rangle$ is not provable in BVu without $q_2 \downarrow$.

**Remark 2.75.** The logical rules of SBVu, i.e., the bottom two lines in the Figure 6, have already been studied by Retoré in [Ret99b], as a rewrite system on digraphs to generate theorems of pomset logic. We will study the relation between pomset logic and BV/BVu in the next section.

In some sections of this paper we also need a variant of BVu that we call BVû and that is obtained from BVu by restricting rules $q_2 \downarrow$ and $s_2$ to cases where neither A nor B has a $\otimes$ as main connective, i.e., we replace $q_2 \downarrow$ and $s_2$ by $\hat{q}_2 \downarrow$ and $\hat{s}_2$, respectively:

$$ \hat{q}_2 \downarrow \frac{A \triangleleft B}{A \otimes B} \qquad \hat{s}_2 \frac{A \otimes B}{A \otimes B} \qquad \text{where } A \not\equiv' C \otimes D \text{ and } B \not\equiv' C \otimes D \text{ for} \\ \text{any formulas } C \text{ and } D. \qquad (2.8) $$

and similarly, by restricting the rules $q_3^\perp \downarrow$, $q_3^R \downarrow$, and $s_3$ to cases where C does not have a $\otimes$ as main connective, i.e., these three rules are replaced by $\hat{q}_3^\perp \downarrow$, $\hat{q}_3^R \downarrow$, and $\hat{s}_3$, respectively:

$$ \hat{q}_3^\perp \downarrow \frac{[A \otimes C] \triangleleft B}{\langle A \triangleleft B \rangle \otimes C} \qquad \hat{q}_3^R \downarrow \frac{A \triangleleft [B \otimes C]}{\langle A \triangleleft B \rangle \otimes C} \qquad \hat{s}_3 \frac{[A \otimes C] \otimes B}{(A \otimes B) \otimes C} \qquad \text{where } C \not\equiv' D \otimes E \text{ for} \\ \text{any formulas } D \text{ and } E. \qquad (2.9) $$

**Proposition 2.76.** The systems BVu and BVû are equivalent.

*Proof.* Any derivation in BVû is also a derivation in BVu. Conversely, the rules $q_2 \downarrow$ and $s_2$ and $s_3$ are derivable with ${\hat{q}_2 \downarrow, \hat{q}_3^\perp \downarrow, \hat{q}_3^R \downarrow, \equiv'}$ and ${\hat{s}_2, \hat{s}_3, \equiv'}$ and ${\hat{s}_3, \equiv'}$, respectively, as shown below:

$$ \begin{align*} \hat{q}_3^R \downarrow & \frac{[A' \otimes A''] \triangleleft [B' \otimes B'']}{\langle [A' \otimes A''] \triangleleft B' \rangle \otimes B''} \\ \hat{q}_3^L \downarrow & \frac{\langle A' \triangleleft B' \rangle \otimes A'' \otimes B''}{A' \otimes B' \otimes A'' \otimes B''} \\ \hat{q}_2 \downarrow & \equiv' \frac{A' \otimes B' \otimes A'' \otimes B''}{[A' \otimes A''] \otimes [B' \otimes B'']} \\ & \equiv', \hat{s}_3, \equiv' \frac{[A' \otimes A''] \otimes [B' \otimes B'']}{([A' \otimes A''] \otimes B') \otimes B''} \\ & \equiv' \frac{\hat{s}_3}{(A' \otimes B') \otimes A'' \otimes B''} \\ & \equiv' \frac{\hat{s}_2}{A' \otimes B' \otimes A'' \otimes B''} \\ & \equiv' \frac{\hat{s}_3}{[A \otimes C', C'')] \otimes B} \\ & \equiv' \frac{\hat{s}_3}{([A \otimes C'] \otimes C'')] \otimes B} \\ & \equiv' \frac{\hat{s}_3}{([A \otimes C'] \otimes B) \otimes C''} \\ & \equiv' \frac{\hat{s}_3}{[(A \otimes B) \otimes C'] \otimes C''} \\ & \equiv' \frac{\hat{s}_3}{(A \otimes B) \otimes [C'' \otimes C'')} \end{align*} $$

and similarly, the rules $q_3^\perp \downarrow$ and $q_3^R \downarrow$ are derivable in ${\hat{q}_3^\perp \downarrow, \equiv'}$ and ${\hat{q}_3^R \downarrow, \equiv'}$, respectively. $\square$

**2.7. SBVu and Dicograph Inclusions.** To wrap up these long preliminaries, we recall here some useful results that also provide some motivation for the rules of SBV and SBVu. The starting observation is that the non-interaction rules preserve the atoms of a formula, so they can be seen as digraph rewriting rules preserving the set of vertices. The following results, due to Béchet, de Groote and Retoré [BdGR97], elucidate the combinatorial meaning of this rewriting system.

First, let us consider the case of unit-free formulas *without the tensor connective* $\otimes$. Recall that according to Proposition 2.32, such formulas modulo $\equiv'$ correspond to *series-parallel orders* on their atom occurrences.
**Theorem 2.77** [BdGR97, Propositions 3.2 and 4.1] (reformulated). Let A and B be two unit-free and tensor-free linear generalized formulas over some set X. Then the inclusion of edges $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ holds if and only if $A \vdash B$ in the fragment of BVu where the interaction rules and the rules involving tensors have been excluded: $\{\equiv', q_2\downarrow, q_3^L\downarrow, q_3^R\downarrow, q_4\downarrow\}$.

Equivalently, this is also the non-interaction non-tensor fragment of SBVu, since all the rules of SBVu that are not in BVu contain tensors.

*Proof.* Let us explain how to connect this reformulation to the original statement in [BdGR97]. In the latter, the inclusion $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ is characterized by a rewriting system on series-parallel orders whose rules are listed in [BdGR97, Definition 3.1]. Observe that, among those rules:

* (a), (b), (c) and (d) correspond to $q_2\downarrow$, $q_3^R\downarrow$, $q_3^L\downarrow$, $q_4\downarrow$ respectively;

* (e) and (h) express the reflexivity and transitivity of the rewriting relation, which corresponds to the fact that a derivation is a sequence of zero, one or more inference rules;

* the remaining rules, namely (f) and (g), express the contextual closure of the rules, whose counterpart in our setting is deep inference, i.e. the possibility of instantiating a rule in a context $S\{\cdot\}$.

There remains a subtlety: we must use the $\equiv'$ rule to turn formulas into equivalent ones on which other rules may be applied, whereas this is left implicit in the setting of [BdGR97] (since $\equiv'$ on formulas corresponds to equality of dicographs). The fact that $\equiv'$ suffices is due to the fact that “the algebraic representation of any [series-parallel] order is unique modulo the associativity of $\triangleleft, \triangleright$ and the commutativity of $\triangleright$” (a quote from [BdGR97, §2] where we adapted the notations for the connectives). □

Next, we turn to unit-free formulas that may contain tensors; their associated graphs are all dicographs. One would then expect the non-interaction fragment of SBVu to characterize dicograph inclusion. However, this is not quite so, since one rule must be added.

**Theorem 2.78** [BdGR97, §5] (rephrased). Let A and B be two unit-free linear generalized formulas over a set X. Then the inclusion of edges $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ holds if and only if $A \vdash B$ in the fragment of SBVu without the interaction rules, plus the following additional rule:

$$ \text{ws} \frac{[A \triangleright B] \otimes [C \triangleright D]}{(A \otimes C) \triangleright (B \otimes D)} \quad (\text{weak switch}) $$

**Remark 2.79.** In [BdGR97, §5], it is suggested that the proof of Theorem 2.77 can be carried over to give a proof of Theorem 2.78. This is not immediately true. Consider for example $A = (a \otimes b) \triangleleft c$ and $B = a \triangleleft [b \triangleright c]$. Clearly $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$, so there must be a derivation from A to B. To construct this derivation, the proof in [BdGR97] proceeds by induction on $|V_{\llbracket A \rrbracket}| = |V_{\llbracket B \rrbracket}|$ and makes a case analysis on the main connectives of A and B. In our case it is $\triangleleft$ for both. But the argument that works for series-parallel orders does not work for dicographs in general. In our example, we have to go through $a \triangleleft b \triangleleft c$. However with some adjustments, the proof does go through. Since this paper is already quite long, we refrain from giving the details, as they are quite straightforward, once the aforementioned problem is observed.

**Remark 2.80.** We shall see in Section 3.1 that the rules of BV preserve pomset logic correctness. As Retoré noticed [Ret99b, §5], this is not the case for the weak switch rule, and this provides one justification for excluding it from SBV.
**Theorem 2.77** [BdGR97, Propositions 3.2 and 4.1] (reformulated). Let A and B be two unit-free and tensor-free linear generalized formulas over some set X. Then the inclusion of edges $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ holds if and only if $A \vdash B$ in the fragment of BVu where the interaction rules and the rules involving tensors have been excluded: $\{\equiv', q_2\downarrow, q_3^L\downarrow, q_3^R\downarrow, q_4\downarrow\}$.

Equivalently, this is also the non-interaction non-tensor fragment of SBVu, since all the rules of SBVu that are not in BVu contain tensors.

*Proof.* Let us explain how to connect this reformulation to the original statement in [BdGR97]. In the latter, the inclusion $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ is characterized by a rewriting system on series-parallel orders whose rules are listed in [BdGR97, Definition 3.1]. Observe that, among those rules:

* (a), (b), (c) and (d) correspond to $q_2\downarrow, q_3^R\downarrow, q_3^L\downarrow, q_4\downarrow$ respectively;

* (e) and (h) express the reflexivity and transitivity of the rewriting relation, which corresponds to the fact that a derivation is a sequence of zero, one or more inference rules;

* the remaining rules, namely (f) and (g), express the contextual closure of the rules, whose counterpart in our setting is deep inference, i.e. the possibility of instantiating a rule in a context $S\{\cdot\}$.

There remains a subtlety: we must use the $\equiv'$ rule to turn formulas into equivalent ones on which other rules may be applied, whereas this is left implicit in the setting of [BdGR97] (since $\equiv'$ on formulas corresponds to equality of dicographs). The fact that $\equiv'$ suffices is due to the fact that “the algebraic representation of any [series-parallel] order is unique modulo the associativity of $\triangleleft, \triangleright$ and the commutativity of $\triangleright$” (a quote from [BdGR97, §2] where we adapted the notations for the connectives). □

Next, we turn to unit-free formulas that may contain tensors; their associated graphs are all dicographs. One would then expect the non-interaction fragment of SBVu to characterize dicograph inclusion. However, this is not quite so, since one rule must be added.

**Theorem 2.78** [BdGR97, §5] (rephrased). Let A and B be two unit-free linear generalized formulas over a set X. Then the inclusion of edges $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$ holds if and only if $A \vdash B$ in the fragment of SBVu without the interaction rules, plus the following additional rule:

$$ \text{ws} \frac{[A \triangleright B] \otimes [C \triangleright D]}{(A \otimes C) \triangleright (B \otimes D)} \quad (\text{weak switch}) $$

**Remark 2.79.** In [BdGR97, §5], it is suggested that the proof of Theorem 2.77 can be carried over to give a proof of Theorem 2.78. This is not immediately true. Consider for example $A = (a \otimes b) \triangleleft c$ and $B = a \triangleleft [b \triangleright c]$. Clearly $R_{\llbracket A \rrbracket} \supseteq R_{\llbracket B \rrbracket}$, so there must be a derivation from A to B. To construct this derivation, the proof in [BdGR97] proceeds by induction on $|V_{\llbracket A \rrbracket}| = |V_{\llbracket B \rrbracket}|$ and makes a case analysis on the main connectives of A and B. In our case it is $\triangleleft$ for both. But the argument that works for series-parallel orders does not work for dicographs in general. In our example, we have to go through $a \triangleleft b \triangleleft c$. However with some adjustments, the proof does go through. Since this paper is already quite long, we refrain from giving the details, as they are quite straightforward, once the aforementioned problem is observed.

**Remark 2.80.** We shall see in Section 3.1 that the rules of BV preserve pomset logic correctness. As Retoré noticed [Ret99b, §5], this is not the case for the weak switch rule, and this provides one justification for excluding it from SBV.
Another argument, which is more intrinsic to BV, is that $BV + ws$ does not admit cut-elimination, or equivalently, that $SBV + ws$ is not conservative over $BV + ws$. The exclusion of the weak switch for this reason is explained as a deliberate design choice by Guglielmi in the discussion concerning “conservation laws” at the beginning of [Gug07, §3].

**Remark 2.81.** By analogy with the previous subsection, we could show that the non-interaction fragment of $SBVu + ws$ is equivalent over unit-free formulas to $\{\equiv, q\downarrow, q\uparrow, ws\}$ with units (indeed, the usual switch is an instance of the weak switch when one of the formulas is set to a unit). Then, Theorem 2.78 above becomes equivalent to [Gug07, Conjecture 3.3.3], which states that $\{\equiv, q\downarrow, q\uparrow, ws\}$ characterizes dicograph inclusion. In other words, that conjecture had been proved before it was stated.

### 3. COMPARING BV AND POMSET LOGIC

In this section we investigate the relation between the two logics, BV and pomset logic. We have already seen in Section 2.1 that every formula uniquely determines a dicograph. Furthermore, by inspecting the rules of BV in Figure 4, one can see that the rule $\equiv$ does not change that dicograph, and that the rules $s$ and $q\downarrow$ only change the set of edges but not the set of vertices of the corresponding dicograph. Additionally, every instance of $ai\downarrow$ removes one pair of dual atoms, and in a proof of BV, every atom occurring in the conclusion has to be removed by exactly one instance of $ai\downarrow$ in the proof.

This means that every BV proof $\delta$ uniquely determines an axiom linking $\ell(\delta)$ for its conclusion, and hence by definition also a pomset logic pre-proof, which in turn, by Definition 2.46, determines a cographic RB-prenet.

In Section 3.1 we are going to show that every cographic RB-prenet that is obtained from a BV proof in such a way is indeed correct, and therefore every theorem of BV is also a theorem of pomset logic.

Then, in Section 3.2 we show that the converse does not hold, i.e., there are theorems of pomset logic that are not theorems of BV. We do this by presenting a formula that is provable in pomset logic but not in BV.

**3.1. BV is Contained in Pomset Logic.** In this section we do not only show that every theorem of BV is also a theorem of pomset logic, but also that every proof in BV uniquely determines a pomset logic proof net with the same conclusion.

The proof that we present here uses the basic idea from [Str03b] that has also been used in [Str03a]. In [Ret99b], Retoré presents an alternative method.

To begin, let $\delta$ be a BV proof of a formula A. We denote by $\llbracket\delta\rrbracket = \rho(A, \ell(\delta))$ the cographic RB-prenet generated from $\delta$ as described above (see Definition 2.46). Then the main result of this section is the following.

**Theorem 3.1.** For every BV proof $\delta$, the cographic RB-prenet $\llbracket\delta\rrbracket$ is correct.

The basic idea of the proof for this theorem is to proceed by way of contradiction, showing that for every possible application of an inference rule of BV, whenever the RB-prenet of the conclusion is incorrect, then already the premise of that rule instance must be incorrect. Since the premise of every proof is $\mathbb{I}$ (which is correct) we obtain our desired result. In order to make this argument formally precise and in order to keep the involved case analysis managable we need to introduce some more concepts.
Another argument, which is more intrinsic to BV, is that $BV + ws$ does not admit cut-elimination, or equivalently, that $SBV + ws$ is not conservative over $BV + ws$. The exclusion of the weak switch for this reason is explained as a deliberate design choice by Guglielmi in the discussion concerning “conservation laws” at the beginning of [Gug07, §3].

**Remark 2.81.** By analogy with the previous subsection, we could show that the non-interaction fragment of $SBVu + ws$ is equivalent over unit-free formulas to $\{\equiv, q\downarrow, q\uparrow, ws\}$ with units (indeed, the usual switch is an instance of the weak switch when one of the formulas is set to a unit). Then, Theorem 2.78 above becomes equivalent to [Gug07, Conjecture 3.3.3], which states that $\{\equiv, q\downarrow, q\uparrow, ws\}$ characterizes dicograph inclusion. In other words, that conjecture had been proved before it was stated.

### 3. COMPARING BV AND POMSET LOGIC

In this section we investigate the relation between the two logics, BV and pomset logic. We have already seen in Section 2.1 that every formula uniquely determines a dicograph. Furthermore, by inspecting the rules of BV in Figure 4, one can see that the rule $\equiv$ does not change that dicograph, and that the rules $s$ and $q\downarrow$ only change the set of edges but not the set of vertices of the corresponding dicograph. Additionally, every instance of $ai\downarrow$ removes one pair of dual atoms, and in a proof of BV, every atom occurring in the conclusion has to be removed by exactly one instance of $ai\downarrow$ in the proof.

This means that every BV proof $\delta$ uniquely determines an axiom linking $\ell(\delta)$ for its conclusion, and hence by definition also a pomset logic pre-proof, which in turn, by Definition 2.46, determines a cographic RB-prenet.

In Section 3.1 we are going to show that every cographic RB-prenet that is obtained from a BV proof in such a way is indeed correct, and therefore every theorem of BV is also a theorem of pomset logic.

Then, in Section 3.2 we show that the converse does not hold, i.e., there are theorems of pomset logic that are not theorems of BV. We do this by presenting a formula that is provable in pomset logic but not in BV.

**3.1. BV is Contained in POMSET Logic.** In this section we do not only show that every theorem of BV is also a theorem of pomset logic, but also that every proof in BV uniquely determines a pomset logic proof net with the same conclusion.

The proof that we present here uses the basic idea from [Str03b] that has also been used in [Str03a]. In [Ret99b], Retoré presents an alternative method.

To begin, let $\delta$ be a BV proof of a formula $A$. We denote by $\llbracket\delta\rrbracket = \rho(A, \ell(\delta))$ the cographic RB-prenet generated from $\delta$ as described above (see Definition 2.46). Then the main result of this section is the following.

**Theorem 3.1.** For every BV proof $\delta$, the cographic RB-prenet $\llbracket\delta\rrbracket$ is correct.

The basic idea of the proof for this theorem is to proceed by way of contradiction, showing that for every possible application of an inference rule of BV, whenever the RB-prenet of the conclusion is incorrect, then already the premise of that rule instance must be incorrect. Since the premise of every proof is $\mathbb{I}$ (which is correct) we obtain our desired result. In order to make this argument formally precise and in order to keep the involved case analysis managable we need to introduce some more concepts.
First observe that every RB-dicograph uniquely determines a balanced formula, up to renaming of variables and equivalence under $≡$. This gives us immediately the following proposition.

**Proposition 3.2.** Let $\delta$ be a proof in BV. Then there is a balanced formula $A$, that is provable in BV and such that $\llbracket A \rrbracket$ and $\llbracket \delta \rrbracket$ are isomorphic.

*Proof.* Let $B$ be the conclusion of $\delta$. Then $A$ is obtained from $B$ by renaming all variable occurrences such that the result is balanced and the linking is preserved. $\square$

**Definition 3.3.** Let $A$ and $B$ be generalized formulas over a set $X$. We call $B$ a pseudo-subformula of $A$, written as $B \subseteq A$, if it is equivalent under $≡$ to some $A'$ that can be obtained from $A$ by replacing some occurrences of elements of $X$ (in the case of usual formulas, some atom occurrences) in $A$ by $\mathbb{I}$. If $B \subseteq A$ and $B \not\equiv A$, then we say that $B$ is a proper pseudo-subformula of $A$, and write it as $B \supseteq A$.

**Example 3.4.** We have the pseudo-subformula relation

$$ \langle a \triangleleft d \rangle \otimes (b \otimes b) \sqsubseteq \langle (a \otimes b) \triangleleft d \triangleleft e \rangle \otimes (b \otimes [(e \otimes f) \otimes \langle a \triangleleft b \rangle]) $$

coming from the equivalence

$$ \langle a \triangleleft d \rangle \otimes (b \otimes b) \equiv \langle (a \otimes \mathbb{I}) \triangleleft d \triangleleft \mathbb{I} \rangle \otimes (b \otimes [(\mathbb{I} \otimes \mathbb{I}) \otimes \langle \mathbb{I} \triangleleft b \rangle]) $$

The following proposition explains our choice to denote both pseudo-subformulas and induced subgraphs (Definition 2.25) by $\sqsubseteq$.

**Proposition 3.5.** Let $A$ and $B$ be linear generalized formulas (this is the case, for instance, when $A$ and $B$ are balanced usual formulas). We have that $B \subseteq A$ if and only if $\llbracket B \rrbracket \subseteq \llbracket A \rrbracket$, and $B \supseteq A$ if and only if $\llbracket B \rrbracket \supseteq \llbracket A \rrbracket$.

*Proof.* Let $X = V_{\llbracket A \rrbracket}$. By definition, the induced subgraphs $\mathcal{H} \subseteq \llbracket A \rrbracket$ are in bijection with the subsets $Y \subseteq X$ via $V_{\mathcal{H}} = Y$. Let $A_{\llbracket Y \rrbracket}$ be the formula obtained from $A$ by replacing every $x \in X \setminus Y$ by $\mathbb{I}$; from the inductive definition of $\llbracket \cdot \rrbracket$ one can check that $\llbracket A_{\llbracket Y \rrbracket} \rrbracket = \mathcal{H}$. To conclude, apply Theorem 2.22 to handle the equivalence $≡$ that appears in the definition of pseudo-subformula. $\square$

**Lemma 3.6.** Let $A$ be a balanced formula (Definition 2.45) and $B$ be a balanced pseudo-subformula of $A$. If $A$ is provable in BV, then so is $B$.

*Proof.* Let $\delta$ be the proof of $A$ in BV, and let $\delta'$ be obtained by replacing all atoms that do not occur in $B$ in every line of $\delta$ by $\mathbb{I}$. Then $\delta'$ is a valid derivation of $B$ in BV. $\square$

**Definition 3.7.** Let $H$ be a balanced formula and $\mathcal{H} = \llbracket H \rrbracket$. We say that $H$ is a (balanced) cycle when the RB-dicograph $\mathcal{H}$ admits a chordless $\ae$-cycle that visits all vertices<fnref n="13" /> and either $|V_{\mathcal{H}}| = 2$ or $R_{\mathcal{H}} \cap B_{\mathcal{H}} = \emptyset$. The size $|H|$ of a balanced cycle $H$ is its size as a formula (Definition 2.2). In particular, we have $|H| = |V_{\mathcal{H}}|$.

**Proposition 3.8.** A formula $H$ is a balanced cycle if and only if there are pairwise distinct atoms $a_1, \dots, a_n$ for some $n \ge 1$, such that $H \equiv L_1 \otimes L_2 \otimes \dots \otimes L_n$, where $L_1 = a_n^{\perp} \otimes a_1$ or $L_1 = a_n^{\perp} \triangleleft a_1$, and for every $i \in \{2, \dots, n\}$ we have $L_i = a_{i-1}^{\perp} \otimes a_i$ or $L_i = a_{i-1}^{\perp} \triangleleft a_i$.

*Proof.* This follows almost immediately from the definitions. $\square$

<footnote n="13">¹³An elementary cycle in a digraph that visits all vertices is generally called a *Hamiltonian cycle*.</footnote>
First observe that every RB-dicograph uniquely determines a balanced formula, up to renaming of variables and equivalence under $≡$. This gives us immediately the following proposition.

**Proposition 3.2.** Let $\delta$ be a proof in BV. Then there is a balanced formula $A$, that is provable in BV and such that $\llbracket A \rrbracket$ and $\llbracket \delta \rrbracket$ are isomorphic.

*Proof.* Let $B$ be the conclusion of $\delta$. Then $A$ is obtained from $B$ by renaming all variable occurrences such that the result is balanced and the linking is preserved. $\square$

**Definition 3.3.** Let $A$ and $B$ be generalized formulas over a set $X$. We call $B$ a pseudo-subformula of $A$, written as $B \subseteq A$, if it is equivalent under $≡$ to some $A'$ that can be obtained from $A$ by replacing some occurrences of elements of $X$ (in the case of usual formulas, some atom occurrences) in $A$ by $\mathbb{I}$. If $B \subseteq A$ and $B \not\supseteq A$, then we say that $B$ is a proper pseudo-subformula of $A$, and write it as $B \subset A$.

**Example 3.4.** We have the pseudo-subformula relation

$$ \langle a \triangleleft d \rangle \otimes (b \otimes b) \sqsubseteq \langle (a \otimes b) \triangleleft d \triangleleft e \rangle \otimes (b \otimes [(e \otimes f) \otimes \langle a \triangleleft b \rangle]) $$

coming from the equivalence

$$ \langle a \triangleleft d \rangle \otimes (b \otimes b) \equiv \langle (a \otimes \mathbb{I}) \triangleleft d \triangleleft \mathbb{I} \rangle \otimes (b \otimes [(\mathbb{I} \otimes \mathbb{I}) \otimes \langle \mathbb{I} \triangleleft b \rangle]) $$

The following proposition explains our choice to denote both pseudo-subformulas and induced subgraphs (Definition 2.25) by $\sqsubseteq$.

**Proposition 3.5.** Let $A$ and $B$ be linear generalized formulas (this is the case, for instance, when $A$ and $B$ are balanced usual formulas). We have that $B \subseteq A$ if and only if $\llbracket B \rrbracket \subseteq \llbracket A \rrbracket$, and $B \supseteq A$ if and only if $\llbracket B \rrbracket \supseteq \llbracket A \rrbracket$.

*Proof.* Let $X = V_{\llbracket A \rrbracket}$. By definition, the induced subgraphs $\mathcal{H} \subseteq \llbracket A \rrbracket$ are in bijection with the subsets $Y \subseteq X$ via $V_{\mathcal{H}} = Y$. Let $A_{\llbracket Y \rrbracket}$ be the formula obtained from $A$ by replacing every $x \in X \setminus Y$ by $\mathbb{I}$; from the inductive definition of $\llbracket \cdot \rrbracket$ one can check that $\llbracket A_{\llbracket Y \rrbracket} \rrbracket = \mathcal{H}$. To conclude, apply Theorem 2.22 to handle the equivalence $≡$ that appears in the definition of pseudo-subformula. $\square$

**Lemma 3.6.** Let $A$ be a balanced formula (Definition 2.45) and $B$ be a balanced pseudo-subformula of $A$. If $A$ is provable in BV, then so is $B$.

*Proof.* Let $\delta$ be the proof of $A$ in BV, and let $\delta'$ be obtained by replacing all atoms that do not occur in $B$ in every line of $\delta$ by $\mathbb{I}$. Then $\delta'$ is a valid derivation of $B$ in BV. $\square$

**Definition 3.7.** Let $H$ be a balanced formula and $\mathcal{H} = \llbracket H \rrbracket$. We say that $H$ is a (balanced) cycle when the RB-dicograph $\mathcal{H}$ admits a chordless $\ae$-cycle that visits all vertices<fnref n="13" /> and either $|V_{\mathcal{H}}| = 2$ or $R_{\mathcal{H}} \cap B_{\mathcal{H}} = \emptyset$. The size $|H|$ of a balanced cycle $H$ is its size as a formula (Definition 2.2). In particular, we have $|H| = |V_{\mathcal{H}}|$.

**Proposition 3.8.** A formula $H$ is a balanced cycle if and only if there are pairwise distinct atoms $a_1, \dots, a_n$ for some $n \ge 1$, such that $H \equiv L_1 \otimes L_2 \otimes \dots \otimes L_n$, where $L_1 = a_n^{\perp} \otimes a_1$ or $L_1 = a_n^{\perp} \triangleleft a_1$, and for every $i \in \{2, \dots, n\}$ we have $L_i = a_{i-1}^{\perp} \otimes a_i$ or $L_i = a_{i-1}^{\perp} \triangleleft a_i$.

*Proof.* This follows almost immediately from the definitions. $\square$

<footnote n="13">¹³An elementary cycle in a digraph that visits all vertices is generally called a *Hamiltonian cycle*.</footnote>
**Definition 3.9.** We say that a balanced formula *A* contains a cycle if it has a pseudo-subformula *B* ⊑ *A* that is a cycle (or equivalently, if ⟨*[A]⟩ contains a chordless æ-cycle).

We are now ready to state and prove the main lemma, which is at the heart of the proof of Theorem 3.1.

**Lemma 3.10.** Let $\mathfrak{r} \frac{Q}{P}$ be an instance of an inference rule in BVû. If $P$ is a balanced cycle then $Q$ contains a cycle. If $\mathfrak{r} \neq \equiv'$ then the size of the cycle in $Q$ is strictly smaller than $|P|$.

*Proof.* By Proposition 3.8 we have that $P \equiv' L_1 \oslash L_2 \oslash \dots \oslash L_n$, where $L_1 = a_n^{\perp} \otimes a_1$ or $L_1 = a_n^{\perp} \triangleleft a_1$, and for every $i \in \{2, \dots, n\}$ we have $L_i = a_{i-1}^{\perp} \otimes a_i$ or $L_i = a_{i-1}^{\perp} \triangleleft a_i$, with all $a_i$ being pairwise distinct. We proceed by case analysis on the rule $\mathfrak{r}$. First observe that by Proposition 3.8 the rules $a_i^{\otimes \downarrow}$, $a_i^{\triangleleft \downarrow}$, $a_i^{\triangleleft \downarrow}$ cannot be applied to $P$ (seen bottom up), and if $\mathfrak{r} = \equiv'$, then $Q$ trivially contains a cycle, whose size is equal to $|P|$. Now assume $\mathfrak{r}$ is

* $\mathfrak{q}_4 \downarrow \frac{[A \oslash C] \triangleleft [B \oslash D]}{\langle A \triangleleft B \rangle \oslash \langle C \triangleleft D \rangle}$ : Without loss of generality, assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = a_{i-1}^{\perp}$ and $D = a_i$ for some $i \in \{2, \dots, n\}$. Then

$$Q \equiv' \langle [a_n^{\perp} \oslash a_{i-1}^{\perp}] \triangleleft [a_1 \oslash a_i] \rangle \oslash L_2 \oslash \dots \oslash L_{i-1} \oslash L_{i+1} \oslash \dots \oslash L_n$$

which contains the cycle $\langle a_n^{\perp} \triangleleft a_i \rangle \oslash L_{i+1} \oslash \dots \oslash L_n$.

* $\hat{\mathfrak{q}}_3 \downarrow \frac{[A \oslash C] \triangleleft B}{\langle A \triangleleft B \rangle \oslash C}$ : Without loss of generality, we assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = L_i$ for some $i \in \{2, \dots, n\}$. Then $Q \equiv' \langle [a_n^{\perp} \oslash L_i] \triangleleft a_1 \rangle \oslash L_2 \oslash \dots \oslash L_{i-1} \oslash L_{i+1} \oslash \dots \oslash L_n$, which contains the cycle $\langle a_{i-1}^{\perp} \triangleleft a_1 \rangle \oslash L_2 \oslash \dots \oslash L_{i-1}$.

* $\hat{\mathfrak{q}}_3 \uparrow \frac{A \triangleleft [B \oslash C]}{\langle A \triangleleft B \rangle \oslash C}$ : As before, without loss of generality, we assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = L_i$ for some $i \in \{2, \dots, n\}$. Then the cycle $\langle a_n^{\perp} \triangleleft a_i \rangle \oslash L_{i+1} \oslash \dots \oslash L_n$ is contained in $\langle a_n^{\perp} \triangleleft [a_1 \oslash L_i] \rangle \oslash L_2 \oslash \dots \oslash L_{i-1} \oslash L_{i+1} \oslash \dots \oslash L_n \equiv' Q$.

* $\hat{\mathfrak{q}}_2 \downarrow \frac{A \triangleleft B}{A \oslash B}$ : We can assume that $A = L_i$ and $B = L_j$ for some $i, j \in \{1, \dots, n\}$. There are two subcases:

- $i < j$: Then $Q = \langle L_i \triangleleft L_j \rangle \oslash L_1 \oslash \dots \oslash L_{i-1} \oslash L_{i+1} \oslash \dots \oslash L_{j-1} \oslash L_{j+1} \oslash \dots \oslash L_n$ which contains the cycle $L_1 \oslash \dots \oslash L_{i-1} \oslash \langle a_{i-1}^{\perp} \triangleleft a_j \rangle \oslash L_{j+1} \oslash \dots \oslash L_n$.

- $j < i$: Then $Q = \langle L_i \triangleleft L_j \rangle \oslash L_1 \oslash \dots \oslash L_{j-1} \oslash L_{j+1} \oslash \dots \oslash L_{i-1} \oslash L_{i+1} \oslash \dots \oslash L_n$ which contains the cycle $\langle a_{i-1}^{\perp} \triangleleft a_j \rangle \oslash L_{j+1} \oslash \dots \oslash L_{i-1}$.

* $\hat{s}_3 \frac{[A \oslash C] \oslash B}{(A \oslash B) \oslash C}$ : This case is analogous to the case $\hat{\mathfrak{q}}_3 \downarrow$ above.

* $\hat{s}_2 \frac{A \oslash B}{A \oslash B}$ : This case is analogous to the case $\hat{\mathfrak{q}}_2 \downarrow$ above.

In all cases the size of the cycle in $Q$ is strictly smaller than $|Q| = |P|$. $\square$

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

**Lemma 3.11.** Let $P$ be a balanced formula that contains a cycle. Then $P$ is not provable in BV.

*Proof.* Let $H$ be the cycle in $P$, and let $n = |H|$ be its size. We proceed by induction on $n$. Note that $n$ has to be even. For $n = 2$, we have that $H \equiv a^{\perp} \triangleleft a$ or $H \equiv a^{\perp} \otimes a$ for some
**Definition 3.9.** We say that a balanced formula *A* contains a cycle if it has a pseudo-subformula *B* ⊑ *A* that is a cycle (or equivalently, if ⟨*[A]⟩ contains a chordless æ-cycle).

We are now ready to state and prove the main lemma, which is at the heart of the proof of Theorem 3.1.

**Lemma 3.10.** Let $\mathfrak{r} \frac{Q}{P}$ be an instance of an inference rule in BVû. If $P$ is a balanced cycle then $Q$ contains a cycle. If $\mathfrak{r} \neq \equiv'$ then the size of the cycle in $Q$ is strictly smaller than $|P|$.

*Proof.* By Proposition 3.8 we have that $P \equiv' L_1 \succ L_2 \succ \dots \succ L_n$, where $L_1 = a_n^{\perp} \otimes a_1$ or $L_1 = a_n^{\perp} \triangleleft a_1$, and for every $i \in \{2, \dots, n\}$ we have $L_i = a_{i-1}^{\perp} \otimes a_i$ or $L_i = a_{i-1}^{\perp} \triangleleft a_i$, with all $a_i$ being pairwise distinct. We proceed by case analysis on the rule $\mathfrak{r}$. First observe that by Proposition 3.8 the rules $\mathfrak{a}_i^{\otimes \downarrow}$, $\mathfrak{a}_i^{\triangleleft \downarrow}$, $\mathfrak{a}_i^{\triangleleft \downarrow}$ cannot be applied to $P$ (seen bottom up), and if $\mathfrak{r} = \equiv'$, then $Q$ trivially contains a cycle, whose size is equal to $|P|$. Now assume $\mathfrak{r}$ is

* $\mathfrak{q}_4 \downarrow \frac{[A \succ C] \triangleleft [B \succ D]}{\langle A \triangleleft B \rangle \succ \langle C \triangleleft D \rangle}$ : Without loss of generality, assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = a_{i-1}^{\perp}$ and $D = a_i$ for some $i \in \{2, \dots, n\}$. Then

$$Q \equiv' \langle [a_n^{\perp} \succ a_{i-1}^{\perp}] \triangleleft [a_1 \succ a_i] \rangle \succ L_2 \succ \dots \succ L_{i-1} \succ L_{i+1} \succ \dots \succ L_n$$

which contains the cycle $\langle a_n^{\perp} \triangleleft a_i \rangle \succ L_{i+1} \succ \dots \succ L_n$.

* $\hat{\mathfrak{q}}_3 \downarrow \frac{[A \succ C] \triangleleft B}{\langle A \triangleleft B \rangle \succ C}$ : Without loss of generality, we assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = L_i$ for some $i \in \{2, \dots, n\}$. Then $Q \equiv' \langle [a_n^{\perp} \succ L_i] \triangleleft a_1 \rangle \succ L_2 \succ \dots \succ L_{i-1} \succ L_{i+1} \succ \dots \succ L_n$, which contains the cycle $\langle a_{i-1}^{\perp} \triangleleft a_1 \rangle \succ L_2 \succ \dots \succ L_{i-1}$.

* $\hat{\mathfrak{q}}_3 \uparrow \frac{A \triangleleft [B \succ C]}{\langle A \triangleleft B \rangle \succ C}$ : As before, without loss of generality, we assume that $A = a_n^{\perp}$ and $B = a_1$ and $C = L_i$ for some $i \in \{2, \dots, n\}$. Then the cycle $\langle a_n^{\perp} \triangleleft a_i \rangle \succ L_{i+1} \succ \dots \succ L_n$ is contained in $\langle a_n^{\perp} \triangleleft [a_1 \succ L_i] \rangle \succ L_2 \succ \dots \succ L_{i-1} \succ L_{i+1} \succ \dots \succ L_n \equiv' Q$.

* $\hat{\mathfrak{q}}_2 \downarrow \frac{A \triangleleft B}{A \succ B}$ : We can assume that $A = L_i$ and $B = L_j$ for some $i, j \in \{1, \dots, n\}$. There are two subcases:

- $i < j$: Then $Q = \langle L_i \triangleleft L_j \rangle \succ L_1 \succ \dots \succ L_{i-1} \succ L_{i+1} \succ \dots \succ L_{j-1} \succ L_{j+1} \succ \dots \succ L_n$ which contains the cycle $L_1 \succ \dots \succ L_{i-1} \succ \langle a_{i-1}^{\perp} \triangleleft a_j \rangle \succ L_{j+1} \succ \dots \succ L_n$.

- $j < i$: Then $Q = \langle L_i \triangleleft L_j \rangle \succ L_1 \succ \dots \succ L_{j-1} \succ L_{j+1} \succ \dots \succ L_{i-1} \succ L_{i+1} \succ \dots \succ L_n$ which contains the cycle $\langle a_{i-1}^{\perp} \triangleleft a_j \rangle \succ L_{j+1} \succ \dots \succ L_{i-1}$.

* $\hat{s}_3 \frac{[A \succ C] \otimes B}{(A \otimes B) \succ C}$ : This case is analogous to the case $\hat{\mathfrak{q}}_3 \downarrow$ above.

* $\hat{s}_2 \frac{A \otimes B}{A \succ B}$ : This case is analogous to the case $\hat{\mathfrak{q}}_2 \downarrow$ above.

In all cases the size of the cycle in $Q$ is strictly smaller than $|Q| = |P|$. $\square$

**Lemma 3.11.** Let $P$ be a balanced formula that contains a cycle. Then $P$ is not provable in BV.

*Proof.* Let $H$ be the cycle in $P$, and let $n = |H|$ be its size. We proceed by induction on $n$. Note that $n$ has to be even. For $n = 2$, we have that $H \equiv a^{\perp} \triangleleft a$ or $H \equiv a^{\perp} \otimes a$ for some
atom a. By way of contradiction, assume P is provable in BV. By Lemma 3.6, H is also provable in BV, which is impossible. For the inductive case let now $n > 2$. As before, we have by Lemma 3.6 that H is provable in BV. By Proposition 2.70 and Proposition 2.76, H is provable in BVû. Let $\delta$ be that proof in BVû. Let now Q be the premise of the bottom-most rule instance r of $\delta$ that is not a $\equiv'$ (i.e., the conclusion of r is $H' \equiv' H$ and $Q \not\equiv' H$). By Lemma 3.10, Q contains a cycle whose size is smaller than n. By induction hypothesis Q is not provable in BV, and therefore also not provable in BVû, which is a contradiction to the existence to $\delta$. □

We can now complete the proof of Theorem 3.1.

*Proof of Theorem 3.1.* Let $\delta$ be a proof in BV. By Proposition 3.2, there is a balanced formula P, such that $\llbracket P \rrbracket = \llbracket \delta \rrbracket$, and such that P is provable in BV. Now assume, by way of contradiction, that $\llbracket \delta \rrbracket$ is incorrect. That means that $\llbracket \delta \rrbracket$ contains a chordless æ-cycle, or equivalently, that P contains a cycle. By Lemma 3.11, P is not provable in BV. Contradiction. □

## 3.2. Pomset Logic is not Contained in BV.
In this section we present a formula that is provable in pomset logic, i.e., has a correct pomset logic proof net, but that is not provable in BV. From what has been said in the previous section, it follows that if such a formula exists then there is also a balanced such formula. The formula we discuss in this section is the formula Q shown below:<fnref n="14" />

$$Q = (\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle) \otimes (\langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle) \otimes \langle a^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle \quad (3.1)$$

or equivalently, the flat sequent

$$\Gamma_Q = [\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle, \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle, a^{\perp} \triangleleft h^{\perp}, e^{\perp} \triangleleft b^{\perp}, g^{\perp} \triangleleft d^{\perp}, c^{\perp} \triangleleft f^{\perp}] \quad (3.2)$$

Since the formula Q (resp. the sequent $\Gamma_Q$) is balanced, there is a unique axiom linking and therefore a unique cographic RB-prenet and a unique tree-like RB-prenet. In Figure 7, we show the tree-like RB prenet for $\Gamma_Q$, and on the left of Figure 8 we show the cographic RB-prenet, which is the same for Q and $\Gamma_Q$.

To see that these are provable in pomset logic, we have to show that the RB-prenets do not contain chordless æ-cycles. For this we focus on the tree-like RB-prenet, because in tree-like RB-prenets all æ-paths (and therefore also all æ-cycles) are chordless. Hence, it suffices to show that there are no æ-cycles.

Observe that the B-edges corresponding to the roots of the formulas in $\Gamma_Q$ cannot participate in an æ-cycle because they have no adjacent R-edge at the bottom. We can therefore remove each of these B-edges, together with the two adjacent R-edges at the top. The resulting graph is shown on the right of Figure 8.

Another simplification we can do without affecting the æ-cycles is replacing the two B-edges labeled $a \triangleleft b$ and $c \triangleleft d$, together with the connecting R-edge by a single B-edge, and similarly for the two B-edges $g \triangleleft h$ and $e \triangleleft f$. The result is shown on the left of Figure 9.

Finally, observe that there is no æ-cycle that passes trough the two B-edges labeled b and a. The reason is that the directed R-edge between them has the opposite direction of the two adjacent R-edges on the other endpoints of these B-edges. Thus, we can collapse

<footnote n="14">¹⁴We will explain in Remark 3.15 how this formula has been found.</footnote>
atom a. By way of contradiction, assume P is provable in BV. By Lemma 3.6, H is also provable in BV, which is impossible. For the inductive case let now $n > 2$. As before, we have by Lemma 3.6 that H is provable in BV. By Proposition 2.70 and Proposition 2.76, H is provable in BVû. Let $\delta$ be that proof in BVû. Let now Q be the premise of the bottom-most rule instance r of $\delta$ that is not a $\equiv'$ (i.e., the conclusion of r is $H' \equiv' H$ and $Q \not\equiv' H$). By Lemma 3.10, Q contains a cycle whose size is smaller than n. By induction hypothesis Q is not provable in BV, and therefore also not provable in BVû, which is a contradiction to the existence to $\delta$. □

We can now complete the proof of Theorem 3.1.

*Proof of Theorem 3.1.* Let $\delta$ be a proof in BV. By Proposition 3.2, there is a balanced formula P, such that $\llbracket P \rrbracket = \llbracket \delta \rrbracket$, and such that P is provable in BV. Now assume, by way of contradiction, that $\llbracket \delta \rrbracket$ is incorrect. That means that $\llbracket \delta \rrbracket$ contains a chordless æ-cycle, or equivalently, that P contains a cycle. By Lemma 3.11, P is not provable in BV. Contradiction. □

## 3.2. Pomset Logic is not Contained in BV.
In this section we present a formula that is provable in pomset logic, i.e., has a correct pomset logic proof net, but that is not provable in BV. From what has been said in the previous section, it follows that if such a formula exists then there is also a balanced such formula. The formula we discuss in this section is the formula $Q$ shown below:<fnref n="14" />

$$Q = (\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle) \otimes (\langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle) \otimes \langle a^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle \quad (3.1)$$

or equivalently, the flat sequent

$$\Gamma_Q = [\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle, \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle, a^{\perp} \triangleleft h^{\perp}, e^{\perp} \triangleleft b^{\perp}, g^{\perp} \triangleleft d^{\perp}, c^{\perp} \triangleleft f^{\perp}] \quad (3.2)$$

Since the formula $Q$ (resp. the sequent $\Gamma_Q$) is balanced, there is a unique axiom linking and therefore a unique cographic RB-prenet and a unique tree-like RB-prenet. In Figure 7, we show the tree-like RB prenet for $\Gamma_Q$, and on the left of Figure 8 we show the cographic RB-prenet, which is the same for $Q$ and $\Gamma_Q$.

To see that these are provable in pomset logic, we have to show that the RB-prenets do not contain chordless æ-cycles. For this we focus on the tree-like RB-prenet, because in tree-like RB-prenets all æ-paths (and therefore also all æ-cycles) are chordless. Hence, it suffices to show that there are no æ-cycles.

Observe that the B-edges corresponding to the roots of the formulas in $\Gamma_Q$ cannot participate in an æ-cycle because they have no adjacent R-edge at the bottom. We can therefore remove each of these B-edges, together with the two adjacent R-edges at the top. The resulting graph is shown on the right of Figure 8.

Another simplification we can do without affecting the æ-cycles is replacing the two B-edges labeled $a \triangleleft b$ and $c \triangleleft d$, together with the connecting R-edge by a single B-edge, and similarly for the two B-edges $g \triangleleft h$ and $e \triangleleft f$. The result is shown on the left of Figure 9.

Finally, observe that there is no æ-cycle that passes trough the two B-edges labeled $b$ and $a$. The reason is that the directed R-edge between them has the opposite direction of the two adjacent R-edges on the other endpoints of these B-edges. Thus, we can collapse

<footnote n="14">¹⁴We will explain in Remark 3.15 how this formula has been found.</footnote>
<figure><img src="image_18.png" /><figcaption>FIGURE 7. The tree-like RB-prenet for the sequent $\Gamma_Q$ in Equation (3.2)</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>FIGURE 8. Left: The cographic RB-prenet for $Q$ in Equation (3.1) and $\Gamma_Q$ in Equation (3.2)
Right: A simplification of the tree-like RB-prenet in Figure 7</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>FIGURE 9. Two further simplifications of the graph on the right of Figure 8</figcaption></figure>
<figure><img src="image_18.png" /><figcaption>FIGURE 7. The tree-like RB-prenet for the sequent $\Gamma_Q$ in Equation (3.2)</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>FIGURE 8. Left: The cographic RB-prenet for $Q$ in Equation (3.1) and $\Gamma_Q$ in Equation (3.2)
Right: A simplification of the tree-like RB-prenet in Figure 7</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>FIGURE 9. Two further simplifications of the graph on the right of Figure 8</figcaption></figure>
these two edges (and the adjacent “triangle”) to a single vertex. The same can be done for the pairs $c/d$ and $g/h$ and $e/f$. We end up with the RB-graph on the right of Figure 9.

**Proposition 3.12.** The formula $Q$ and the sequent $\Gamma_Q$ shown in Equation (3.1) and Equation (3.2) above are provable in pomset logic.

*Proof.* In the paragraphs above, we have argued that the tree-like RB-prenet in Figure 7 has an æ-cycle if and only if the RB-digraph on the right of Figure 9 has an æ-cycle. Now it is easy to see that this graph has no æ-cycle. Hence, tree-like RB-prenet for $\Gamma_Q$ is correct. $\square$

Let us now show that the formula $Q$ is not provable in BV. To do so we will show that whenever a BV inference has as conclusion $Q$ then its premise defines an incorrect RB-prenet in pomset logic, and is therefore not provable in pomset logic. Since by Theorem 3.1 all BV proofs induce correct pomset proof nets, we can conclude that those premises are not BV-provable, therefore there is no way to build a BV-proof of $Q$.

The main difficulty here is to make sure that we do not overlook any case when checking all possible inferences that have $Q$ as conclusion. Since the unit $\mathbb{I}$ can make these kind of arguments difficult to check, we use here $BV\hat{u}$. Now observe that $Q$ has no subformula of the form $x \prec x^\perp$. This means we only have to consider the non-axiom rules of $BV\hat{u}$.

To cut down the number of cases to consider, we take advantage of the symmetries of $Q$. Let us first look at the automorphisms, i.e., permutations of the variables that results in a formula $Q'$ with $Q' \equiv Q$, which means $\llbracket Q' \rrbracket = \llbracket Q \rrbracket$. The following are automorphisms:

$$ (\alpha) \quad a \leftrightarrow c, b \leftrightarrow d, e \leftrightarrow g, f \leftrightarrow h $$

$$ (\beta) \quad a \mapsto e, b \mapsto f, c \mapsto g, d \mapsto h, e \mapsto c, f \mapsto d, g \mapsto a, h \mapsto b $$

The action of these automorphisms on the subformulas of $Q$ of the form $x^\perp \triangleleft y^\perp$ is transitive: $\alpha(a^\perp \triangleleft h^\perp) = c^\perp \triangleleft f^\perp$, $\beta(a^\perp \triangleleft h^\perp) = e^\perp \triangleleft b^\perp$ and $\alpha \circ \beta(a^\perp \triangleleft h^\perp) = g^\perp \triangleleft d^\perp$.

Another useful symmetry is not quite an automorphism: it is the following anti-automorphism:

$$ (\gamma) \quad a \leftrightarrow h, b \leftrightarrow g, c \leftrightarrow f, d \leftrightarrow e $$

that sends $Q$ to its “conjugate” $Q^\dagger$ defined inductively as follows:

$$ x^\dagger = x \text{ when } x \text{ is an atom} \quad (B \odot C)^\dagger = C^\dagger \odot B^\dagger \text{ for } \odot \in \{\prec, \otimes, \triangleleft\} $$

Note that the reversal of the arguments only matters for the non-commutative connective $\triangleleft$, and $\llbracket Q^\dagger \rrbracket$ is the same as $\llbracket Q \rrbracket$, except that all directed $R$-edges have the opposite direction. Thus, conjugacy preserves provability both in pomset logic (reversing the direction of all cycles in the correctness criterion) and in system $BV\hat{u}$ (the inference rules are closed under conjugacy, with $\hat{q}_3^\perp \triangleleft$ and $\hat{q}_3^R \triangleleft$ being swapped).

We will now go through all the rules of $BV\hat{u}$ and check all possible applications. Using a similar argument as in the proof of Lemma 3.10, we will see that in each case there is a cycle in the resulting premise.

* $\mathfrak{q}_4 \triangleleft \frac{[A \prec C] \triangleleft [B \prec D]}{\langle A \triangleleft B \rangle \prec \langle C \triangleleft D \rangle}$: Because of the action of the automorphisms $\alpha/\beta$, we can without loss of generality assume that $A = a^\perp$ and $B = h^\perp$. There are three subcases:

- $C = e^\perp$ and $D = b^\perp$. We get the cycle $(e \otimes h) \prec \langle e^\perp \triangleleft h^\perp \rangle$ in the premise of the $\mathfrak{q}_4 \triangleleft$-application.

- $C = g^\perp$ and $D = d^\perp$. We get the cycle $(a \otimes d) \prec \langle a^\perp \triangleleft d^\perp \rangle$ in the premise of the $\mathfrak{q}_4 \triangleleft$-application.
these two edges (and the adjacent “triangle”) to a single vertex. The same can be done for the pairs $c/d$ and $g/h$ and $e/f$. We end up with the RB-graph on the right of Figure 9.

**Proposition 3.12.** The formula $Q$ and the sequent $\Gamma_Q$ shown in Equation (3.1) and Equation (3.2) above are provable in pomset logic.

*Proof.* In the paragraphs above, we have argued that the tree-like RB-prenet in Figure 7 has an æ-cycle if and only if the RB-digraph on the right of Figure 9 has an æ-cycle. Now it is easy to see that this graph has no æ-cycle. Hence, tree-like RB-prenet for $\Gamma_Q$ is correct. $\square$

Let us now show that the formula $Q$ is not provable in BV. To do so we will show that whenever a BV inference has as conclusion $Q$ then its premise defines an incorrect RB-prenet in pomset logic, and is therefore not provable in pomset logic. Since by Theorem 3.1 all BV proofs induce correct pomset proof nets, we can conclude that those premises are not BV-provable, therefore there is no way to build a BV-proof of $Q$.

The main difficulty here is to make sure that we do not overlook any case when checking all possible inferences that have $Q$ as conclusion. Since the unit $I$ can make these kind of arguments difficult to check, we use here $BV\hat{u}$. Now observe that $Q$ has no subformula of the form $x \prec x^\perp$. This means we only have to consider the non-axiom rules of $BV\hat{u}$.

To cut down the number of cases to consider, we take advantage of the symmetries of $Q$. Let us first look at the automorphisms, i.e., permutations of the variables that results in a formula $Q'$ with $Q' \equiv Q$, which means $\llbracket Q' \rrbracket = \llbracket Q \rrbracket$. The following are automorphisms:

$$ (\alpha) \quad a \leftrightarrow c, b \leftrightarrow d, e \leftrightarrow g, f \leftrightarrow h $$

$$ (\beta) \quad a \mapsto e, b \mapsto f, c \mapsto g, d \mapsto h, e \mapsto c, f \mapsto d, g \mapsto a, h \mapsto b $$

The action of these automorphisms on the subformulas of $Q$ of the form $x^{\perp} \triangleleft y^{\perp}$ is transitive: $\alpha(a^{\perp} \triangleleft h^{\perp}) = c^{\perp} \triangleleft f^{\perp}, \beta(a^{\perp} \triangleleft h^{\perp}) = e^{\perp} \triangleleft b^{\perp}$ and $\alpha \circ \beta(a^{\perp} \triangleleft h^{\perp}) = g^{\perp} \triangleleft d^{\perp}$.

Another useful symmetry is not quite an automorphism: it is the following anti-automorphism:

$$ (\gamma) \quad a \leftrightarrow h, b \leftrightarrow g, c \leftrightarrow f, d \leftrightarrow e $$

that sends $Q$ to its “conjugate” $Q^\dagger$ defined inductively as follows:

$$ x^{\dagger} = x \text{ when } x \text{ is an atom} \quad (B \odot C)^{\dagger} = C^{\dagger} \odot B^{\dagger} \text{ for } \odot \in \{\prec, \otimes, \triangleleft\} $$

Note that the reversal of the arguments only matters for the non-commutative connective $\triangleleft$, and $\llbracket Q^\dagger \rrbracket$ is the same as $\llbracket Q \rrbracket$, except that all directed $R$-edges have the opposite direction. Thus, conjugacy preserves provability both in pomset logic (reversing the direction of all cycles in the correctness criterion) and in system $BV\hat{u}$ (the inference rules are closed under conjugacy, with $\hat{q}_3^\perp \triangleleft$ and $\hat{q}_3^R \triangleleft$ being swapped).

We will now go through all the rules of $BV\hat{u}$ and check all possible applications. Using a similar argument as in the proof of Lemma 3.10, we will see that in each case there is a cycle in the resulting premise.

* $\mathfrak{q}_4 \triangleleft \frac{[A \prec C] \triangleleft [B \prec D]}{\langle A \triangleleft B \rangle \prec \langle C \triangleleft D \rangle}$: Because of the action of the automorphisms $\alpha/\beta$, we can without loss of generality assume that $A = a^{\perp}$ and $B = h^{\perp}$. There are three subcases:

- $C = e^{\perp}$ and $D = b^{\perp}$. We get the cycle $(e \otimes h) \prec \langle e^{\perp} \triangleleft h^{\perp} \rangle$ in the premise of the $\mathfrak{q}_4 \triangleleft$-application.

- $C = g^{\perp}$ and $D = d^{\perp}$. We get the cycle $(a \otimes d) \prec \langle a^{\perp} \triangleleft d^{\perp} \rangle$ in the premise of the $\mathfrak{q}_4 \triangleleft$-application.
- $C = c^{\perp}$ and $D = f^{\perp}$. We get the cycle $(b \otimes c) \otimes (e \otimes h) \otimes \langle c^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $q_4$-application.

* $\hat{q}_3^L \frac{[A \otimes C] \triangleleft B}{\langle A \triangleleft B \rangle \otimes C}$: As before, because of the symmetries of $Q$, we only need to consider the case where $A = a^{\perp}$ and $B = h^{\perp}$. There are now five subcases of how to match $C$:

- $C = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$. We get the cycle $(e \otimes h) \otimes \langle b \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $\hat{q}_3^L$-application.

- $C = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $h \triangleleft h^{\perp}$ in the premise of the $\hat{q}_3^L$-application.

- $C = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e \otimes h) \otimes \langle e^{\perp} \triangleleft h^{\perp} \rangle$ in the premise of the $\hat{q}_3^L$-application.

- $C = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $(b \otimes d) \otimes (e \otimes h) \otimes \langle d^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $\hat{q}_3^L$-application.

- $C = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $(f \otimes h) \otimes \langle f^{\perp} \triangleleft h^{\perp} \rangle$ in the premise of the $\hat{q}_3^L$-application.

* $\hat{q}_3^R \frac{A \triangleleft [B \otimes C]}{\langle A \triangleleft B \rangle \otimes C}$: Similar to $\hat{q}_3^L$, by conjugacy.

* $\hat{q}_2 \frac{A \triangleleft B}{A \otimes B}$: The possible values for the ordered pair $(A, B)$ are all pairs of distinct formulas in the sequent $\Gamma_Q$ in Equation (3.2). We first look at the case $A = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ and $B = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. Here we get the cycle $\langle d \triangleleft g \rangle \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle$ in the premise. The case $A = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$ and $B = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ is symmetric to the this one via the automorphism $\beta$. Otherwise, either $A$ or $B$ (or both) have the form $x^{\perp} \triangleleft y^{\perp}$. It suffices to treat all the cases $R = x^{\perp} \triangleleft y^{\perp}$. This is because conjugation exchanges the roles of $A$ and $B$ in the $q_2$-rule, and $Q$ is equal to its own conjugate up to the variable renaming performed by $\gamma$. We may also without loss of generality assume that $A = a^{\perp} \triangleleft h^{\perp}$; as before, this relies on the transitive action of the automorphisms of $Q$ on the $x^{\perp} \triangleleft y^{\perp}$ that it contains. There are now five cases for $B$:

- $B = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$. We get the cycle $a^{\perp} \triangleleft a$ in the premise.

- $B = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $h^{\perp} \triangleleft h$ in the premise.

- $B = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e \otimes h) \otimes \langle h^{\perp} \triangleleft e^{\perp} \rangle$ in the premise.

- $B = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $(a \otimes d) \otimes \langle a^{\perp} \triangleleft d^{\perp} \rangle$ in the premise.

- $B = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $(f \otimes h) \otimes \langle h^{\perp} \triangleleft f^{\perp} \rangle$ in the premise.

* $\hat{s}_3 \frac{[A \otimes C] \otimes B}{(A \otimes B) \otimes C}$: There are two possibilities to match $A \otimes B$: either with $\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ or with $\langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. Due to the commutativity of $\otimes$, we have four possibilities to match $A$ and $B$. Due to the symmetries discussed above, we only need to consider the case where $A = a \triangleleft b$ and $B = c \triangleleft d$. There are now five cases how to match $C$:

- $C = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $(f \otimes c) \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle$ in the premise.

- $C = a^{\perp} \triangleleft h^{\perp}$. We get the cycle $(h^{\perp} \otimes c) \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle \otimes (f \otimes h)$ in the premise.

- $C = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e^{\perp} \otimes d) \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle \otimes (e \otimes g)$ in the premise.

- $C = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $d^{\perp} \otimes d$ in the premise.

- $C = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $c^{\perp} \otimes c$ in the premise.

* $\hat{s}_2 \frac{A \otimes B}{A \otimes B}$: This case is already subsumed by the case for $\hat{q}_2$.

In this way, we have completed the proof of the following proposition.

**Proposition 3.13.** The formula $Q$ shown in Equation (3.1) is not provable in BV.
- $C = c^{\perp}$ and $D = f^{\perp}$. We get the cycle $(b \otimes c) \otimes (e \otimes h) \otimes \langle c^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $q_4$-application.

• $\hat{\mathfrak{q}}_{3\downarrow} \frac{[A \otimes C] \triangleleft B}{\langle A \triangleleft B \rangle \otimes C}$ : As before, because of the symmetries of $Q$, we only need to consider the case where $A = a^{\perp}$ and $B = h^{\perp}$. There are now five subcases of how to match $C$:

- $C = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$. We get the cycle $(e \otimes h) \otimes \langle b \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $\hat{\mathfrak{q}}_{3\downarrow}^\perp$-application.

- $C = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $h \triangleleft h^{\perp}$ in the premise of the $\hat{\mathfrak{q}}_{3\downarrow}^\perp$-application.

- $C = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e \otimes h) \otimes \langle e^{\perp} \triangleleft h^{\perp} \rangle$ in the premise of the $\hat{\mathfrak{q}}_{3\downarrow}^\perp$-application.

- $C = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $(b \otimes d) \otimes (e \otimes h) \otimes \langle d^{\perp} \triangleleft h^{\perp} \rangle \otimes \langle e^{\perp} \triangleleft b^{\perp} \rangle$ in the premise of the $\hat{\mathfrak{q}}_{3\downarrow}^\perp$-application.

- $C = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $(f \otimes h) \otimes \langle f^{\perp} \triangleleft h^{\perp} \rangle$ in the premise of the $\hat{\mathfrak{q}}_{3\downarrow}^\perp$-application.

• $\hat{\mathfrak{q}}_{3\downarrow}^R \frac{A \triangleleft [B \otimes C]}{\langle A \triangleleft B \rangle \otimes C}$ : Similar to $\hat{\mathfrak{q}}_{3\downarrow}^\perp$, by conjugacy.

• $\hat{\mathfrak{q}}_{2\downarrow} \frac{A \triangleleft B}{A \otimes B}$ : The possible values for the ordered pair $(A, B)$ are all pairs of distinct formulas in the sequent $\Gamma_Q$ in Equation (3.2). We first look at the case $A = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ and $B = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. Here we get the cycle $\langle d \triangleleft g \rangle \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle$ in the premise. The case $A = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$ and $B = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ is symmetric to the this one via the automorphism $\beta$. Otherwise, either $A$ or $B$ (or both) have the form $x^{\perp} \triangleleft y^{\perp}$. It suffices to treat all the cases $R = x^{\perp} \triangleleft y^{\perp}$. This is because conjugation exchanges the roles of $A$ and $B$ in the $q_2$-rule, and $Q$ is equal to its own conjugate up to the variable renaming performed by $\gamma$. We may also without loss of generality assume that $A = a^{\perp} \triangleleft h^{\perp}$; as before, this relies on the transitive action of the automorphisms of $Q$ on the $x^{\perp} \triangleleft y^{\perp}$ that it contains. There are now five cases for $B$:

- $B = \langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$. We get the cycle $a^{\perp} \triangleleft a$ in the premise.

- $B = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $h^{\perp} \triangleleft h$ in the premise.

- $B = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e \otimes h) \otimes \langle h^{\perp} \triangleleft e^{\perp} \rangle$ in the premise.

- $B = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $(a \otimes d) \otimes \langle a^{\perp} \triangleleft d^{\perp} \rangle$ in the premise.

- $B = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $(f \otimes h) \otimes \langle h^{\perp} \triangleleft f^{\perp} \rangle$ in the premise.

• $\hat{s}_3 \frac{[A \otimes C] \otimes B}{(A \otimes B) \otimes C}$ : There are two possibilities to match $A \otimes B$: either with $\langle a \triangleleft b \rangle \otimes \langle c \triangleleft d \rangle$ or with $\langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. Due to the commutativity of $\otimes$, we have four possibilities to match $A$ and $B$. Due to the symmetries discussed above, we only need to consider the case where $A = a \triangleleft b$ and $B = c \triangleleft d$. There are now five cases how to match $C$:

- $C = \langle e \triangleleft f \rangle \otimes \langle g \triangleleft h \rangle$. We get the cycle $(f \otimes c) \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle$ in the premise.

- $C = a^{\perp} \triangleleft h^{\perp}$. We get the cycle $(h^{\perp} \otimes c) \otimes \langle c^{\perp} \triangleleft f^{\perp} \rangle \otimes (f \otimes h)$ in the premise.

- $C = e^{\perp} \triangleleft b^{\perp}$. We get the cycle $(e^{\perp} \otimes d) \otimes \langle g^{\perp} \triangleleft d^{\perp} \rangle \otimes (e \otimes g)$ in the premise.

- $C = g^{\perp} \triangleleft d^{\perp}$. We get the cycle $d^{\perp} \otimes d$ in the premise.

- $C = c^{\perp} \triangleleft f^{\perp}$. We get the cycle $c^{\perp} \otimes c$ in the premise.

• $\hat{s}_2 \frac{A \otimes B}{A \otimes B}$ : This case is already subsumed by the case for $\hat{\mathfrak{q}}_{2\downarrow}$.

In this way, we have completed the proof of the following proposition.

**Proposition 3.13.** The formula $Q$ shown in Equation (3.1) is not provable in BV.
**Theorem 3.14.** The theorems of BV form a proper subset of the theorems of pomset logic.

*Proof.* This follows immediately from Propositions 3.12 and 3.13. □

<figure><img src="image_21.png" /><figcaption>(A) A tree-like RB-prenet for a linear version of the medial rule of system SKS (cf. Remark 3.15). Note that it does *not* satisfy the MLL+mix correctness criterion, and therefore also not the pomset criterion.</figcaption></figure>

<figure><img src="image_22.png" /><figcaption>(C) The $R$-edges on top are now directed, corresponding to $a^{\perp} \triangleleft h^{\perp}, b^{\perp} \trianglerightneq e^{\perp}, d^{\perp} \trianglerightneq g^{\perp}, c^{\perp} \triangleleft f^{\perp}$. This modification validates the pomset logic correctness criterion, but the resulting sequent is not provable in BV.</figcaption></figure>

<caption>(D) Adding more $R$-edges does preserve provability in pomset logic, but showing that the resulting sequent is not provable in BV is easier now, as every possible rule application breaks pomset correctness.</caption>

<caption>FIGURE 10. From the medial of SKS to our counterexample (cf. Remark 3.15)</caption>

**Remark 3.15.** Let us end this section by some explanation of how the formula $Q$ has been found. Our starting point was the so-called medial rule from system SKS [BT01], a
**Theorem 3.14.** The theorems of BV form a proper subset of the theorems of pomset logic.

*Proof.* This follows immediately from Propositions 3.12 and 3.13. □

<figure><img src="image_21.png" /><figcaption>(A) A tree-like RB-prenet for a linear version of the medial rule of system SKS (cf. Remark 3.15). Note that it does not satisfy the MLL+mix correctness criterion, and therefore also not the pomset criterion.</figcaption></figure>

<figure><img src="image_22.png" /><figcaption>(C) The R-edges on top are now directed, corresponding to $a^{\perp} \triangleleft h^{\perp}, b^{\perp} \trianglerightneq e^{\perp}, d^{\perp} \trianglerightneq g^{\perp}, c^{\perp} \triangleleft f^{\perp}$. This modification validates the pomset logic correctness criterion, but the resulting sequent is not provable in BV.</figcaption></figure>

<caption>(D) Adding more R-edges does preserve provability in pomset logic, but showing that the resulting sequent is not provable in BV is easier now, as every possible rule application breaks pomset correctness.</caption>

<caption>FIGURE 10. From the medial of SKS to our counterexample (cf. Remark 3.15)</caption>

**Remark 3.15.** Let us end this section by some explanation of how the formula $Q$ has been found. Our starting point was the so-called medial rule from system SKS [BT01], a
formulation of classical logic in the calculus of structures:

$$ \frac{m}{[A \lor B] \land [D \lor C]} \qquad (3.3) $$

It corresponds to the classical sequent $(A \land D) \lor (B \land C) \vdash [A \lor B] \land [D \lor C]$, which can be rewritten by De Morgan's laws as $\vdash [\neg A \lor \neg D] \land [\neg B \lor \neg C]$, $[A \lor B] \land [D \lor C]$. By replacing the classical connectives and instantiating the formulas $A, B, C, D$ with distinct atoms, we get the sequent $[(a^{\perp} \otimes d^{\perp}) \otimes (b^{\perp} \otimes c^{\perp})$, $(a \otimes b) \otimes (d \otimes c)]$ which is not provable in linear logic. This can be immediately seen by inspecting its RB-prenet, shown in Figure 10a, which contains several (chordless) æ-cycles.

Then, on the right of that “medial RB-prenet”, in Figure 10b, we replace the $B$-edges corresponding to the atoms by a pair of $B$-edges connected by an (undirected) $R$-edge. This does not affect provability, as no æ-cycles are added or removed. Then, in Figure 10c, we give these new $R$-edges a direction. By choosing the right direction, we can break all æ-cycles, which means the result becomes correct with respect to the pomset logic correctness criterion. But the resulting formula (or sequent) remains unprovable in BV. To simplify the proof of non-provability in BV, we added further $R$-edges, as shown in Figure 10d, that do not break provability in pomset logic. It is easy to see that the RB-prenet in Figure 10d is an intermediate step between the one in Figure 7 and the one on the right in Figure 8.

In Example 4.18 we shall see that Figure 10c is also related to a construction that we use for complexity-theoretic purposes; more than that, we shall explain how complexity considerations allowed us to restrict the search space for a formula separating pomset logic from BV.

## 4. COMPLEXITY OF PROVABILITY

After having established that BV and pomset logic are not the same, the next natural question is whether they have the same or different provability complexity. It had already been established before that BV is NP-complete. We recall the proof here and establish a slightly more general result. Then we discuss the complexity of pomset logic and show that already checking the correctness of a pomset logic proofnet is coNP-complete. Based on this observation, we can then show that provability in pomset logic is $\Sigma_2^P$-complete.

### 4.1. Preliminaries on Complexity Theory and Boolean Formulas.
We assume that the reader is familiar with (see for instance the reference textbook [AB09, Chapter 2])

* the complexity classes $P, NP$ and $coNP$;

* the notions, for a complexity class $C$, of $C$-hard and $C$-complete problems (defined, as usual, with respect to many-to-one polynomial time reductions for all $C$ that we shall consider – though weaker reductions should also work).

$NP$ and $coNP$ form the first level of the polynomial hierarchy [AB09, Chapter 5], and we shall also be concerned with its second level which contains the classes $\Sigma_2^P$ and $\Pi_2^P$. These are dual in the same way that $NP$ and $coNP$ are: a decision problem is in $\Pi_2^P$ if and only if its negation is in $\Sigma_2^P$.

To show that a problem is in $\Sigma_2^P$, the most convenient way is perhaps to use the definition in terms of oracle machines.
formulation of classical logic in the calculus of structures:

$$ \frac{m}{[A \lor B] \land [D \lor C]} \qquad (3.3) $$

It corresponds to the classical sequent $(A \land D) \lor (B \land C) \vdash [A \lor B] \land [D \lor C]$, which can be rewritten by De Morgan's laws as $\vdash [\neg A \lor \neg D] \land [\neg B \lor \neg C]$, $[A \lor B] \land [D \lor C]$. By replacing the classical connectives and instantiating the formulas $A, B, C, D$ with distinct atoms, we get the sequent $[(a^{\perp} \otimes d^{\perp}) \otimes (b^{\perp} \otimes c^{\perp})$, $(a \otimes b) \otimes (d \otimes c)]$ which is not provable in linear logic. This can be immediately seen by inspecting its RB-prenet, shown in Figure 10a, which contains several (chordless) æ-cycles.

Then, on the right of that “medial RB-prenet”, in Figure 10b, we replace the $B$-edges corresponding to the atoms by a pair of $B$-edges connected by an (undirected) $R$-edge. This does not affect provability, as no æ-cycles are added or removed. Then, in Figure 10c, we give these new $R$-edges a direction. By choosing the right direction, we can break all æ-cycles, which means the result becomes correct with respect to the pomset logic correctness criterion. But the resulting formula (or sequent) remains unprovable in BV. To simplify the proof of non-provability in BV, we added further $R$-edges, as shown in Figure 10d, that do not break provability in pomset logic. It is easy to see that the RB-prenet in Figure 10d is an intermediate step between the one in Figure 7 and the one on the right in Figure 8.

In Example 4.18 we shall see that Figure 10c is also related to a construction that we use for complexity-theoretic purposes; more than that, we shall explain how complexity considerations allowed us to restrict the search space for a formula separating pomset logic from BV.

## 4. COMPLEXITY OF PROVABILITY

After having established that BV and pomset logic are not the same, the next natural question is whether they have the same or different provability complexity. It had already been established before that BV is NP-complete. We recall the proof here and establish a slightly more general result. Then we discuss the complexity of pomset logic and show that already checking the correctness of a pomset logic proofnet is coNP-complete. Based on this observation, we can then show that provability in pomset logic is $\Sigma_2^P$-complete.

### 4.1. Preliminaries on Complexity Theory and Boolean Formulas.
We assume that the reader is familiar with (see for instance the reference textbook [AB09, Chapter 2])

* the complexity classes $P, NP$ and $coNP$;

* the notions, for a complexity class $C$, of $C$-hard and $C$-complete problems (defined, as usual, with respect to many-to-one polynomial time reductions for all $C$ that we shall consider – though weaker reductions should also work).

$NP$ and $coNP$ form the first level of the polynomial hierarchy [AB09, Chapter 5], and we shall also be concerned with its second level which contains the classes $\Sigma_2^P$ and $\Pi_2^P$. These are dual in the same way that $NP$ and $coNP$ are: a decision problem is in $\Pi_2^P$ if and only if its negation is in $\Sigma_2^P$.

To show that a problem is in $\Sigma_2^P$, the most convenient way is perhaps to use the definition in terms of oracle machines.