Intuitionistic BV

Matteo Acclavio, Lutz Straßburger

► To cite this version:

Matteo Acclavio, Lutz Straßburger. Intuitionistic BV. TABLEAUX 2025 - 34th International Conference Automated Reasoning with Analytic Tableaux and Related Methods., Sep 2025, Reykjavik, Iceland. pp.414-432, 10.1007/978-3-032-06085-3_22. hal-05356081

HAL Id: hal-05356081

https://inria.hal.science/hal-05356081v1

Submitted on 10 Nov 2025

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>

Distributed under a Creative Commons Attribution 4.0 International License
# Intuitionistic BV

Matteo Acclavio¹[0000-0002-0425-2825] and
Lutz Straßburger²[0000-0003-4661-6540]

¹ Sussex University, Brighton, UK

² INRIA Saclay, Palaiseau, France

**Abstract.** We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

## 1 Introduction

The logic BV is a conservative extension of multiplicative linear logic with mix (MLL<sub>mix</sub>) with a self-dual non-commutative connective (⊠) called seq. It was introduced by Guglielmi in [11,13] in the attempt of providing cut-free deduction system for Retoré's *pomset* logic [20,22].<sup>3</sup> To this end, Guglielmi developed the deep inference formalism of the calculus of structures to deal with the limitations of the traditional proof systems based on Gentzen's work (sequent calculi and natural deduction). In fact, as shown by Tui in [26], the presence of the non-commutative connective ⊠ makes it impossible to define a cut-free sequent calculus for BV. Nonetheless, the logic BV has found applications in the formalisation of process algebras (e.g., [7] and [15,16]), in typing linear lambda calculus with explicit substitutions [23], and in describing quantum computations through *BV-categories* [5,24].

Our motivation for this work is to develop a proof-theoretic framework that could serve as a basis for the definition of type systems that treat *sequentiality* as a first-class citizen of the language. In this context, the logic BV appears to be a natural candidate, as it provides a non-commutative connective capable of expressing sequentiality.<sup>4</sup> However, BV is not intuitionistic, and thus cannot serve as a basis for type systems aligned with tradition of type theory developed for functional programming languages.

This leads us to the central question of this work: *Is it possible to define an intuitionistic version of BV?* More precisely, we are interested in a system

<footnote n="3"><sup>3</sup> The inclusion of BV in *pomset* has been known since the introduction of BV [25]. However, that this inclusion is strict has only been proven recently [19,18].</footnote>

<footnote n="4"><sup>4</sup> Indeed, the deep inference formalism was developed by Guglielmi after various attempts in defining sequent calculi including a logic operator modeling sequentiality [9,10].</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. Proof systems discussed in this paper. The ones in the boxes are new.</figcaption></figure>

that conservatively extends intuitionistic multiplicative linear logic (IMLL) and introduces a connective that internalizes sequentiality within the logic itself.

The biggest obstacle towards the definition of an intuitionistic variant of BV is the fact that in BV the unit $I$ is self-dual and is shared not only by the connectives $\otimes$ and $\ominus$, but also the new self-dual connective $\triangleleft$. It is well-known that intuitionistic multiplicative linear logic (IMLL) can be obtained by polarizing formulas in multiplicative linear logic (MLL). But the self-duality of the unit $I$ and the seq-connective $\triangleleft$ makes it difficult to extend this polarization to BV. Our solution to this problem is to make the unit $I$ only ‘half a unit’. That means that we no longer have $A \triangleleft I \equiv A \equiv I \triangleleft A$, but only $A \to A \triangleleft I$ and $A \to I \triangleleft A$.

In classical BV the triple $\langle \otimes, \ominus, I \rangle$ forms an *isomix category* [8], and the connective $\triangleleft$ is a *degenerate linear functor* (in the sense of [5]), that is, it validates the following implication.<fnref n="5" />

$$ ((A \triangleleft B) \otimes (C \triangleleft D)) \to ((A \otimes C) \triangleleft (B \otimes D)) \quad (1) $$

We define *intuitionistic BV (IBV)* by extending intuitionistic multiplicative linear logic (IMLL), where the triple $\langle \otimes, \ominus, I \rangle$ forms a symmetric monoidal closed structure, with a non-commutative connective $\triangleleft$ validating Equation (1) and the unit laws $A \to (I \triangleleft A)$ and $A \to (A \triangleleft I)$.<fnref n="6" />

*Contributions* We give a deep inference proof system for IBV (Sections 2 and 3), and we prove cut elimination via a *splitting lemma* (in Section 4). We argue that IBV is indeed the intuitionistic version of BV, by showing that (i) IBV is a conservative extension of IMLL (Section 5), and that (ii) the unit-free version of BV is a conservative extension of the unit-free version of IBV (Section 6).<fnref n="7" />

Finally, in Section 7, we present a weaker logic, called INML, in which the connective $\triangleleft$ is not associative. We give a cut-free sequent calculus for INML, which is obtained by considering a single-conclusion two-sided version of the sequent calculus for the *non-commutative multiplicative logic* (NML) from [2,3]. We prove that INML is another conservative extension of IMLL, which can be conservatively extended to NML and to IBV (see Figure 1).

Details of the proofs can be found in the extended version [4] of this paper.

<footnote n="5">⁵ The fact that the unit $I$ of the $\otimes$ and $\ominus$ is also the (left and right) unit for $\triangleleft$ is a consequence of the definition of degenerate linear functor [5].</footnote>

<footnote n="6">⁶ If $(I \triangleleft A) \to A$ and $(A \triangleleft I) \to A$ were valid in IBV, then the connectives $\otimes$ and $\triangleleft$ would collapse. See Proposition 18 for details.</footnote>

<footnote n="7">⁷ Note that BV is not conservative over MLL, because it is conservative over $MLL_{mix}$, and $MLL_{mix}$ is not conservative over MLL.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 2. Inference rules for system IBV</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 3. Additional rules for SIBV.</figcaption></figure>

## 2 Formulas and Inference Rules

We consider formulas generated from a countable set $\mathcal{A} = \{a, b, c, \dots\}$ of atoms, a unit $\mathbb{I}$, and the binary connectives implication $\to$, tensor $\otimes$, and seq $\triangleleft$:

$$ A, B := a \mid \mathbb{I} \mid A \otimes B \mid A \to B \mid A \triangleleft B \qquad a \in \mathcal{A} \qquad (2) $$

A formula is **unit-free** if it contains no occurrences of $\mathbb{I}$. In order to define the deep inference rules for our systems, we need to define **contexts**, which are formulas where one atom occurrence is replaced by a hole $[\cdot]$. In the intuitionistic setting we have to distinguish between **positive contexts**, denoted by $P[\cdot]$, and **negative contexts**, denoted by $N[\cdot]$, depending on the position of the ‘hole’:

$$ \begin{align} P[\cdot] &:= [\cdot] \mid P[\cdot] \otimes A \mid A \otimes P[\cdot] \mid A \to P[\cdot] \mid N[\cdot] \to A \mid P[\cdot] \triangleleft A \mid A \triangleleft P[\cdot] \tag{3} \\ N[\cdot] &:= N[\cdot] \otimes A \mid A \otimes N[\cdot] \mid A \to N[\cdot] \mid P[\cdot] \to A \mid N[\cdot] \triangleleft A \mid A \triangleleft N[\cdot] \nonumber \end{align} $$

The inference rules for the **system IBV** are shown in Figure 2. The reader familiar with classical BV might be surprised at the large number of inference rules. But note that (i) because we are in the intuitionistic setting, we need two
versions of each rule: one for positive contexts and one for negative contexts,<fnref n="8" />
(ii) because the $\neg\circ$ is not commutative, we need a left and a right version of each
s-rule (called *switch*), and (iii) because the $I$ is not a proper unit of the $\llcorner$, we
need the different versions of the ref- and sq-rules, which would just be instances
of the q↓-rule in classical BV.<fnref n="9" />

We use the ◦ and • decoration on the inference rules to indicate whether it
applies in a positive or negative context, respectively. Finally, the rules below the
dashed line have no such decoration, which indicates that they can be applied
in positive and negative contexts. Furthermore, we use dotted lines for the rules
to indicate that they correspond to what is usually given as equational theory
in classical BV. They comprise associativity, commutativity, unit-equations, and
currying.

From the inference rules, we can now define derivations. We are going to use
the *open deduction* style [12], and again, because of the intuitionistic setting,
we have *positive* and *negative derivations*, which are defined inductively as
follows:

$$
\begin{array}{l@{\qquad}l}
\text{Positive: } \mathcal{P}, \mathcal{Q} := \mathsf{A} & \left|
\begin{array}{@{}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{}}
  \mathcal{P} \otimes \mathcal{Q} & \mathcal{P} \triangleleft \mathcal{Q} & \mathcal{N} \neg \mathcal{P} & \mathcal{P} \underset{\mathsf{r}}{\overset{\mathcal{N}}{\smile}} & \mathcal{P} \underset{\mathsf{r}}{\vdots \mathcal{Q}} \\
  \multicolumn{1}{@{}c@{}}{\mathcal{P} \otimes \mathcal{Q}} & \multicolumn{1}{@{}c@{}}{\mathcal{P} \triangleleft \mathcal{Q}} & \multicolumn{1}{@{}c@{}}{\mathcal{N} \neg \mathcal{P}} & \multicolumn{1}{@{}c@{}}{\mathcal{P} \underset{\mathsf{r}}{\overset{\mathcal{N}}{\smile}} \mathcal{Q}} & \multicolumn{1}{@{}c@{}}{\mathcal{P} \underset{\mathsf{r}}{\vdots \mathcal{Q}}}
\end{array}
\right| \\[1.5em]
\text{Negative: } \mathcal{N}, \mathcal{M} := \mathsf{A} & \left|
\begin{array}{@{}c@{\quad}c@{\quad}c@{\quad}c@{\quad}c@{}}
  \mathcal{N} \otimes \mathcal{M} & \mathcal{N} \triangleleft \mathcal{M} & \mathcal{P} \neg \mathcal{N} & \mathcal{N} \underset{\mathsf{r}}{\overset{\mathcal{N}}{\smile}} & \mathcal{N} \underset{\mathsf{r}}{\vdots \mathcal{M}}
\end{array}
\right|
\end{array}
\qquad (4)
$$

where $A$ is the identity derivation with premise $A$ and conclusion $A$. The composition by $r$ is only allowed if the premise of $r$ is the conclusion of the derivation $\mathcal{P}$ (resp. $\mathcal{N}$), and the conclusion of $r$ is the premise of the derivation $\mathcal{Q}$ (resp. $\mathcal{M}$). Then the premise of the resulting derivation is the premise of $\mathcal{P}$ (resp. $\mathcal{N}$) and its conclusion is the conclusion of $\mathcal{Q}$ (resp. $\mathcal{M}$).

Let $X$ be a set of inference rules. We write $\begin{array}{c@{\quad}c} \mathcal{A} & \mathcal{A} \\ \mathcal{P} \parallel \mathsf{X} & \text{(resp. } \mathcal{N} \parallel \mathsf{X} \text{)} \\ \mathsf{B} & \mathsf{B} \end{array}$ for a positive

derivation $\mathcal{P}$ (resp. negative derivation $\mathcal{N}$) whose inference rules are all from $X$, whose premise is $A$ and whose conclusion is $B$. A *proof* of $A$ is a positive derivation $\mathcal{P}$ with premise $I$ and conclusion $A$, which may be denoted $\mathcal{P} \parallel \mathsf{X} \mathsf{A}$, and we write $\vdash_X A$ if there is a proof of $A$ in $X$. In the following, we will omit $X$ in derivations if $X = IBV$.

Consider now the inference rules in Figure 3. They are the up-versions of
the down-rules (i.e., the ones with a down-arrow in the name) of IBV. The rules
of IBV without an arrow in the name are part of both, the up- and the down-
fragment. We call **system SIBV** the union of the rules in Figures 2 and 3. The

<footnote n="8">⁸ This would correspond to rules on the left and rules on the right of the turnstile in the sequent calculus.</footnote>

<footnote n="9">⁹ See [17,18,21] for unit-free versions of BV, also having these rules.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 4. Derivability of $i_{\downarrow}^{\circ}$ in IBV.</figcaption></figure>

'S' in SIBV stands for symmetric, and we follow here the naming scheme that is common in deep inference [13,6,23].

Of course, in the next sections, we will show that the two systems SIBV and IBV are equivalent, i.e., prove the same formulas: $\vdash_{SIBV} A$ iff $\vdash_{IBV} A$.

*Remark 1.* It is common in deep inference, and in particular for BV, to consider formulas modulo an equivalence relation, covering associativity, commutativity, and units for the connectives. In our system, this would correspond to the rules marked with a dotted line in Figures 2 and 3. We chose not to do this in this paper because (i) the unit $\mathbb{I}$ is only half a unit for the $\triangleleft$ connective, and the rules $u_{\downarrow}^{\triangleleft}, u_{\uparrow}^{\triangleleft}, u_{\downarrow}^{\star}, u_{\uparrow}^{\star}$ would be needed anyway, (ii) it might be confusing to the reader to have implicit currying, and (iii) making everything explicit makes derivations easier to read.

## 3 Properties of the Systems

In this section we show some basic properties of IBV and SIBV. For this, consider the two rules

$$ i_{\downarrow}^{\circ} \xrightarrow{\mathbb{I}}_{A \to A} \circ \quad \text{and} \quad i_{\uparrow}^{\bullet} \xrightarrow{A \to A} \mathbb{I} \qquad (5) $$

called *identity* and *cut*. Their atomic versions $ai_{\downarrow}$ and $ai_{\uparrow}$ have already been shown in Figures 2 and 3.

**Lemma 2.** *We have the following results:*

1. $i_{\downarrow}^{\circ}$ is derivable in IBV;

2. $i_{\uparrow}^{\bullet}$ is derivable in SIBV;

3. $ai_{\uparrow}^{\bullet}, q_{\uparrow}^{\circ}, \text{ and } q_{\uparrow}^{\star}$ are derivable in IBV $\cup \{i_{\uparrow}^{\bullet}, u_{\uparrow}^{\star}, u_{\uparrow}^{\circ}\}$.

*Proof.* The first point is proven by induction on $A$ as shown in Figure 4. The second point is proven dually. For the third point, $ai_{\uparrow}^{\bullet}$ is a special case of $i_{\uparrow}^{\bullet}$, and derivability of $q_{\uparrow}^{\circ}$ and $q_{\uparrow}^{\star}$ follows via the derivations shown in Figure 5, where $P$ and $Q$ (resp. $R$ and $S$) are the premise and conclusion of $q_{\uparrow}^{\circ}$ (resp. $q_{\uparrow}^{\star}$). $\square$
<figure><img src="image_6.png" /><figcaption>Fig. 5. Using $i_{\uparrow}^{\bullet}$ to derive $q_{\uparrow}^{\circ}$ and $q_{\uparrow}^{\bullet}$</figcaption></figure>

**Lemma 3.** *The following are equivalent:*

1. $\vdash_{\text{IBV}} A \to B$;

2. $\vdash_{\text{IBV}} P[A] \to P[B]$ for any positive context $P[\cdot]$;

3. $\vdash_{\text{IBV}} N[B] \to N[A]$ for any negative context $N[\cdot]$;

*Proof.* Note that 1 is a special case of 2. We prove $1 \Rightarrow 2$ and $1 \Rightarrow 3$ and $2 \Leftrightarrow 3$ simultaneously by induction on the context, see (3). We show only two cases:

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

where we have to switch between 2 and 3 because in the cases $N[\cdot] = P[\cdot] \to C$ and $P[\cdot] = N[\cdot] \to C$ the left-hand side of the $\to$ has opposite polarity. $\square$

**Theorem 4 (Deduction Theorem).** Let A and B be formulas. Then

$$ \vdash_{\text{SIBV}} A \to B \iff \text{there is a derivation } \begin{array}{l} A \\ P \parallel_{\text{SIBV}} B \end{array}. $$

*Proof.* Via the following two derivations:

<figure><img src="image_8.png" /></figure>
**Corollary 5.** If $\vdash_{\mathrm{SIBV}} A \to B$, then

- there is a derivation in SIBV with premise $P[A]$ and conclusion $P[B]$ for
  any positive context $P[\cdot]$;

- there is a derivation in SIBV with premise $N[B]$ and conclusion $N[A]$ for
  any negative context $N[\cdot]$;

*Proof.* Consequence of the Deduction Theorem and Lemma 3. □

We conclude this section by proving that the *Modus Ponens* is a valid logical inference in SIBV.

**Corollary 6 (Modus Ponens).** Let A and B be formulas. If $\vdash_{\mathrm{SIBV}} A \to B$ and $\vdash_{\mathrm{SIBV}} A$, then $\vdash_{\mathrm{SIBV}} B$.

*Proof.* By hypothesis, we have a proof $\mathcal{P}_A$ with conclusion A, and the Deduction Theorem ensures the existence of a derivation $\mathcal{P}_{A \to B}$ with premise A and conclusion B. We conclude by composing ‘vertically’ the two derivations. □

# 4 Cut Elimination

In this section we show that the cut rule $i_\uparrow^\bullet$, given in (5), is admissible for IBV. To prove this, we will first show that the two systems SIBV and IBV are equivalent, that is, any formula provable in SIBV is also provable in IBV. In other words, we will show that all up-rules shown in Figure 3 are admissible for IBV. Then the admissibility of cut will follow from Lemma 2.

**Theorem 7.** The rules $u_\uparrow^\downarrow$, $u_\uparrow^\uparrow$, $u_\uparrow^\otimes$, $u_\uparrow^\circ$, $ai_\uparrow^\bullet$, $q_\uparrow^\circ$, and $q_\uparrow^\bullet$ are admissible for IBV.

**Corollary 8.** The systems SIBV and IBV are equivalent.

**Corollary 9.** The rule $i_\uparrow^\bullet$ is admissible for IBV.

It therefore remains to prove Theorem 7. For this, we will use a *splitting lemma* as common for deep inference systems [11,14,25,1]. But to our knowledge, this is the first version of a splitting lemma for an intuitionistic system, and there are certain subtleties, for example, the number of cases doubles, for the same reason as the number of inference rules doubles. Here is the statement of the general splitting lemma for IBV:

**Lemma 10 (Splitting).** Let A, B and K be formulas.

- If $\vdash_{\mathrm{IBV}} K \to (A \otimes B)$, then there are formulas $K_A$ and $K_B$ such that

$$ \begin{array}{ccc} K_A \otimes K_B & & \parallel \\ \mathbin{\parallel} & \text{and} & K_A \to A \\ K & & \parallel \\ & & K_B \to B \end{array} $$

- If $\vdash_{\mathrm{IBV}} (A \to B) \to K$, then there are formulas $K_A$ and $K_B$ such that

$$ \begin{array}{ccc} K_A \to K_B & & \parallel \\ \parallel & \text{and} & K_A \to A \\ K & & \parallel \\ & & B \to K_B \end{array} $$
- If $\vdash_{IBV} K \to (A \triangleleft B)$, then there are formulas $K_A$ and $K_B$ such that

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

- If $\vdash_{IBV} (A \triangleleft B) \to K$, then there are formulas $K_A$ and $K_B$ such that

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

*Proof.* The proof is by induction on the derivation, considering the bottom-most (non-dotted) rule instance in the derivation. In Figure 6 we show the most general forms of the non-trivial cases to take into account. In that figure, we abuse the dotted line notation to indicate that there might be more than one application of a 'dotted line' inference rule from Figure 2. More details are provided in [4]. □

We also need a version of splitting for the atoms.

**Lemma 11 (Atomic Splitting).** Let $a$ be an atom and $K$ a formula. Then:

1. if $\vdash_{IBV} K \to a$, then there is a negative derivation $\frac{a}{K}$;

2. if $\vdash_{IBV} a \to K$, then there is a positive derivation $\frac{a}{K}$.

*Proof.* Again, by induction on the derivation and a case analysis on the bottom-most rule instance. We have the following non-trivial cases:

$$s_L^\circ \frac{K_1 \otimes (K_2 \to a)}{(K_1 \to K_2) \to a}$$

$$s_R^\circ \frac{(a \to K_1) \otimes K_2}{a \to (K_1 \otimes K_2)}$$

$$sq_L^\circ \frac{(a \to K_1) \triangleleft K_2}{a \to (K_1 \triangleleft K_2)}$$

$$sq_R^\circ \frac{K_1 \to (a \to K_2)}{a \to (K_1 \triangleleft K_2)}$$

We conclude by applying the inductive hypothesis on the premise of the rule after remarking that, because of splitting, if $\vdash_{IBV} A \otimes B$ or $\vdash_{IBV} A \triangleleft B$, then $\vdash_{IBV} A$ and $\vdash_{IBV} B$ must hold. The derivations to prove the statement are recursively defined as follows:

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

□

In order to use the splitting lemmas for proving Theorem 7, we need to be able to employ them in arbitrary contexts. For this, we use the context reduction lemma.
$$ K_1 \dashv \left( \begin{array}{c} s_R^\circ \frac{(K_2 \dashv (A_2 \otimes B_2)) \otimes (A_1 \otimes B_1)}{K_2 \dashv ((A_2 \otimes B_2) \otimes (A_1 \otimes B_1))} \\ \hline (K_1 \otimes K_2) \dashv ((A_1 \otimes A_2) \otimes (B_1 \otimes B_2)) \end{array} \right) $$

Case 1

$$ K_1 \dashv \left( \begin{array}{c} s_L^\circ \frac{(A_1 \otimes B_1) \otimes ((A_2 \otimes B_2) \dashv K_2)}{((A_1 \otimes B_1) \dashv (A_2 \otimes B_2)) \dashv K_2} \\ \hline ((A_1 \otimes A_2) \dashv (B_1 \otimes B_2)) \dashv (K_1 \otimes K_2) \end{array} \right) $$

Case 2

$$ \left( \frac{s_L^\circ ((K_1 \dashv (A_1 \otimes B_1)) \dashv (A_2 \dashv B_2))}{(K_1 \otimes ((A_1 \otimes B_1) \dashv (A_2 \dashv B_2)))} \right) \bullet \dashv K_2 $$

Case 3

$$ \left( \frac{s_R^\circ \frac{(A_1 \otimes B_1) \dashv ((A_2 \dashv B_2) \otimes K_2)}{((A_1 \otimes B_1) \dashv (A_2 \dashv B_2)) \otimes K_2}}}{\bullet \dashv K_1} \right) \dashv K_1 $$

Case 4

$$ K_1 \dashv \left( \frac{q_\downarrow^\circ \frac{(K_2 \dashv A_1) \triangleleft (K_3 \dashv (A_3 \triangleleft B))}{(K_2 \triangleleft K_3) \dashv (A_1 \triangleleft (A_2 \triangleleft B))}}{(K_1 \otimes (K_2 \triangleleft K_3)) \dashv ((A_1 \triangleleft A_2) \triangleleft B)} \right) $$

Case 5 (left associativity)

$$ K_1 \dashv \left( \frac{q_\downarrow^\circ \frac{(K_2 \dashv (A \triangleleft B_1)) \triangleleft (K_3 \dashv B_2)}{(K_2 \triangleleft K_3) \dashv ((A \triangleleft B_1) \triangleleft B_2)}}{(K_1 \otimes (K_2 \triangleleft K_3)) \dashv (A \triangleleft (B_1 \triangleleft B_2))} \right) $$

Case 5 (right associativity)

$$ \left( \frac{q_\downarrow^\circ \frac{(A_1 \otimes K_1) \triangleleft ((A_2 \triangleleft B) \otimes K_2)}{(A_1 \triangleleft (A_2 \triangleleft B)) \dashv (K_1 \triangleleft K_2)} \bullet}{(A_1 \triangleleft A_2) \triangleleft B) \dashv ((K_1 \triangleleft K_2) \dashv K_3)} \right) \dashv K_3 $$

Case 6 (left associativity)

$$ \left( \frac{q_\downarrow^\circ \frac{((A \triangleleft B_1) \otimes K_1) \triangleleft (B_2 \otimes K_2)}{(A \triangleleft (B_1 \triangleleft B_2)) \dashv (K_1 \triangleleft K_2)} \bullet}{(A \triangleleft (B_1 \triangleleft B_2)) \dashv ((K_1 \triangleleft K_2) \dashv K_3)} \right) \dashv K_3 $$

Case 6 (right associativity)

$$ K_1 \dashv \left( \frac{q_\downarrow^\circ \frac{(A_1 \dashv K_2) \triangleleft ((A_2 \triangleleft B) \dashv K_3)}{((A_1 \triangleleft A_2) \triangleleft B) \dashv (K_2 \triangleleft K_3)}}{(A_1 \triangleleft A_2) \triangleleft B) \dashv (K_1 \dashv (K_2 \triangleleft K_3))} \right) $$

Case 7 (left associativity)

$$ K_1 \dashv \left( \frac{q_\downarrow^\circ \frac{((A \triangleleft B_1) \dashv K_2) \triangleleft (B_2 \dashv K_3)}{(A \triangleleft (B_1 \triangleleft B_2)) \dashv (K_2 \triangleleft K_3)}}{(A \triangleleft (B_1 \triangleleft B_2)) \dashv (K_1 \dashv (K_2 \triangleleft K_3))} \right) $$

Case 7 (right associativity)

<caption>Fig. 6. Cases for the splitting lemma.</caption>

**Lemma 12 (Context Reduction).** Let A be a formula, $P[\cdot]$ a positive context, and $N[\cdot]$ a negative context.

1. If $\vdash_{IBV} P[A]$, then there is a formula K and derivations

$$ \begin{array}{l} K \dashv X \\ \mathcal{P}_X \parallel \\ P[X] \end{array} \quad \text{and} \quad \begin{array}{l} \mathcal{P}_A \parallel \\ K \dashv A \end{array} \quad \text{for any formula X.} $$

2. If $\vdash_{IBV} N[A]$, then there is a formula K and derivations

$$ \begin{array}{l} X \dashv K \\ \mathcal{P}_X \parallel \\ N[X] \end{array} \quad \text{and} \quad \begin{array}{l} \mathcal{P}_A \parallel \\ A \dashv K \end{array} \quad \text{for any formula X.} $$

*Proof.* By induction on the structure of (positive and negative) contexts, see (3). Except for the trivial cases $P[\cdot] = H \dashv [\cdot]$ and $N[\cdot] = [\cdot] \dashv H$, the discussion of each case requires to apply the splitting lemma once to get derivations to be
<figure><img src="image_12.png" /><figcaption>**Fig. 7.** Derivations for admissibility of $ai_↑^•$ and $q_↑^•$. The case for $q_↑^•$ is similar. All subderivations exist by splitting and context reduction lemmas.</figcaption></figure>

used, together with the inductive case, to construct the derivations $\mathcal{P}_X$ and $\mathcal{N}_X$. More details are provided in [4]. □

*Proof (for Theorem 7).* We can remove all instances of the up-rules in a derivation, starting with a topmost one. Given such an instance $r↑$, we apply context reduction and splitting to the premise or $r↑$ (once for $u_↑^↓$, $u_↑^↓$, $u_↑^×$, $u_↑^−$, and twice for $ai_↑^•$, $q_↑^•$, $q_↑^•$). The derivations we obtained are then assembled to construct a derivation of the conclusion of $r↑$. For $ai_↑^•$ and $q_↑^•$, these derivations are shown in Figure 7. More details are given in [4]. □

# 5 From IMLL to IBV

In this section we show that IBV is a conservative extension of intuitionistic multiplicative linear logic (IMLL): every IMLL-formula that is provable in IBV is also provable in IMLL.

We assume the reader to be familiar with sequent calculi and cut-elimination. A *sequent* is a pair $\Gamma \vdash A$, where $\Gamma$ is a (possibly empty) set of occurrences of formulas, and $A$ is a formula. Figure 8 shows the inference rules of the sequent calculus for IMLL, and it's well known that it admits cut elimination.

**Theorem 13.** *The rule AX is derivable in IMLL.*

**Theorem 14.** *The rule cut is admissible IMLL.*
<figure><img src="image_13.png" /><figcaption>**Fig. 8.** Left: Rules for IMLL Right: The cut rule and the generalized axiom</figcaption></figure>

A formula interpretation of a sequent $B_1, \dots, B_n \vdash A$ is a formula of the shape $(B_1 \otimes \dots \otimes B_n) \dashv A$ for any bracketing of the $\otimes$. If $n=0$ then the unique formula interpretation is just $A$. Note that any two formula interpretations of a sequent are interderivable in IBV using the rules $com^\otimes$ and $asso^\otimes$. This allows us to define a sequent $\Gamma \vdash B$ to be derivable in IBV if any of its formula interpretations is derivable in IBV.

**Lemma 15.** Let $r$ be an inference rule of IMLL. If every premise of and instance of $r$ is derivable in IBV, then so is its conclusion.

*Proof.* For the rules $\mathbb{I}$ and $\otimes_{\mathbb{L}}$ this is trivial. For $ax$ it follows by a single instance of $ai_{\downarrow}$. For $\neg_{\Gamma}$, observe that a formula interpretation of its conclusion can be obtained via the *cur-rule* from a formula interpretation of its premise. Finally, for the rules $\neg_{\Gamma}$ and $\otimes_{R}$, formula interpretations of their conclusions are derived via the following derivations:

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

where $\mathcal{D}'$ are derivations of formula interpretations of their premises. $\square$

**Lemma 16.** (i) Let $r \in \text{IBV}$, and let $A$ and $B$ be formulas not containing any occurrence of $\mathbf{a}$. If $r \stackrel{A}{\underset{B}{\circ}}$ then $A \vdash B$ is derivable in IMLL, and if $r \stackrel{\bullet}{\underset{B}{\circ}}$ then $B \vdash A$ is derivable in IMLL. (ii) Let $P[\cdot]$ and $N[\cdot]$ be a positive and a negative $\mathbf{a}$-free context, respectively. If $A \vdash B$ is derivable in IMLL, then so are $P[A] \vdash P[B]$ and $N[B] \vdash N[A]$.

*Proof.* (i) Cases for the rule $u_{\downarrow}^{\otimes}$, $u_{\downarrow}^{\neg\otimes}$, $com^{\otimes}$, and $asso^{\otimes}$ are the standard derivations to prove that associativity and commutativity of $\otimes$, and the fact that $\mathbb{I}$ is the
<figure><img src="image_15.png" /><figcaption>Fig. 9. $ai_{\downarrow}$-rules for $IBV^{-}$.</figcaption></figure>

*Proof.* The implication $(A \otimes B) \dashv (A \triangleleft B)$ already holds in BV and IBV (it suffices to apply a $\text{ref}^{\bullet}$ and a $i^{\circ}_{\downarrow}$). For the other implication $(A \triangleleft B) \dashv (A \otimes B)$, assume we have $(\mathbb{I} \triangleleft A) \dashv A$ and $(A \triangleleft \mathbb{I}) \dashv A$ for every $A$. By Lemma 3, there should be negative derivations $\mathcal{D}_{\mathbb{I} \triangleleft A}$ and $\mathcal{D}_{\mathbb{I} \triangleleft \mathbb{I}}$ in SIBV with premise $A$ and conclusion $\mathbb{I} \triangleleft A$ and $A \triangleleft \mathbb{I}$ respectively, for any formula $A$. Then, we could construct a proof of $(A \triangleleft B) \dashv (A \otimes B)$ in IBV by applying up-rules elimination (Theorem 7) to the following derivation in SIBV:

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

□

# 6 From IBV to BV

One might expect that also BV is a conservative extension of IBV, in the same sense as MLL is a conservative extension of IMLL. Unfortunately, this is not true because of the collapse of the units in BV. However, if we look at the unit-free versions of the two systems, we can get our expected result. The unit-free version of IBV, denoted by **BV**⁻, is obtained from IBV (see Figure 2) by removing all versions of $u_{\downarrow}$ and by replacing the $ai_{\downarrow}$ by the rules shown in Figure 9.

Similarly, the **BV**⁻-formulas are the BV formulas without the unit, i.e., they are generated from the countable set $\mathcal{A}$ of atoms and the binary connectives par $(\ominus)$, tensor $(\otimes)$, and seq $(\triangleleft)$, using the following grammar:

$$ A, B := a \mid a^{\perp} \mid A \otimes B \mid A \ominus B \mid A \triangleleft B \qquad a \in \mathcal{A} \qquad (8) $$

We can define the negation $(\cdot)^{\perp}$ for all BV⁻-formulas via DeMorgan duality:

$$ a^{\perp\perp} = a \quad (A \otimes B)^{\perp} = A^{\perp} \ominus B^{\perp} \quad (A \ominus B)^{\perp} = A^{\perp} \otimes B^{\perp} \quad (A \triangleleft B)^{\perp} = A^{\perp} \triangleleft B^{\perp} $$

The inference rules for **system BV**⁻ are shown in Figure 10. It is the unit-free version of BV described in [17,19,18]. The rule ≡ is defined by the equations for associativity of the connectives $\otimes$, $\triangleleft$, and $\ominus$, and commutativity of $\otimes$ and $\ominus$.
<figure><img src="image_17.png" /><figcaption>**Fig. 10.** Rules for the system BV⁻. The side condition for the ≡-rule is that A and B are equivalent modulo the equivalence relation generated by the relation ≡, defined below the dashed line.</figcaption></figure>

We define an embedding (·)ᵇ from unit-free formulas (see Section 2) into BV⁻-formulas as follows:

$$a^b = a \quad (A \otimes B)^b = A^b \otimes B^b \quad (A \to B)^b = (A^b)^\perp \otimes B^b \quad (A \triangleleft B)^b = A^b \triangleleft B^b \quad (9)$$

This allows us to state the main theorem of this section.

**Theorem 19.** Let A be a unit-free formula. We have $\vdash_{\text{IBV}^-} A \text{ iff } \vdash_{\text{BV}^-} A^b$.

For proving it, we define two subsets of BV⁻-formulas, called **positive formulas** and **negative formulas**:

$$ \begin{array}{l} \text{positive: } A^\circ, B^\circ := a \mid A^\circ \otimes B^\circ \mid A^\bullet \otimes B^\circ \mid A^\circ \triangleleft B^\circ \\ \text{negative: } A^\bullet, B^\bullet := a^\perp \mid A^\circ \otimes B^\bullet \mid A^\bullet \otimes B^\bullet \mid A^\bullet \triangleleft B^\bullet \end{array} \qquad (10) $$

with $a \in \mathcal{A}$. Clearly, a BV⁻-formula can either be positive (e.g., $a \otimes a$) or negative (e.g., $a^\perp \otimes a^\perp$) or neither (e.g., $a^\perp \otimes a^\perp$), but never both. We call a BV⁻-formula that is neither positive nor negative **unpolarisable**.

**Lemma 20.** A BV⁻-formula A is positive iff it is in the image of (·)ᵇ.

*Proof.* By induction on A, proving at the same time that A is negative iff $A^\perp$ is in the image of (·)ᵇ. □

*Proof (for Theorem 19).* Let us first assume we have a derivation of A in IBV⁻. We can apply the mapping (·)ᵇ to every formula in that derivation and obtain a valid BV⁻ derivation. For the converse, it suffices to observe that all rules of BV⁻ either preserve the positive polarity of the whole formula (every proof starts with a positive atomic interaction), or break it. And no inference rule of BV⁻ can transform an unpolarisable formula back into one with positive polarity. Furthermore, enumerating all possible polarity-preserving assignments to the rules in Figure 10 yields the rules of IBV⁻.¹⁰ Now the result follows from Lemma 20. (See [4] for an alternative proof.) □
<figure><img src="image_18.png" /><figcaption>**Fig. 12.** **Left:** Rules for weakening and contraction in the sequent calculus and in deep inference. **Right:** Possible extensions of LJ with a non-commutative connective.</figcaption></figure>

**Theorem 24.** INML is a conservative extension of IMLL.

*Proof.* It suffices to remark that all rules in INML have the subformula property, so any proof of a $\triangleleft$-free formula in INML can only use rules in IMLL. $\square$

We now would like to show that NML is conservative over INML, but we encounter the same problems with the units as in BV. We therefore consider only unit-free formulas, and the unit-free version of NML, that we call **NML**$^-$, and which is shown in Figure 11.

**Theorem 25.** Let A be a unit-free formula. We have $\vdash_{INML} A \ iff \ \vdash_{NML-} A^b$.

*Proof.* This follows in the same way as (unit-free) MLL$_{mix}$ is conservative over unit-free IMLL. See [4] for more details. $\square$

We conclude this section by observing that the cut restricted to associativity of $\triangleleft$ is enough to obtain from INML a sequent calculus for IBV. To this end, we introduce the following **associative-cut** rules:

$$ \begin{array}{c} \text{a-cut}_L \frac{\Gamma \vdash (A \triangleleft B) \triangleleft C \quad A \triangleleft (B \triangleleft C), \Delta \vdash D}{\Gamma, \Delta \vdash D} \\ \text{a-cut}_R \frac{\Gamma \vdash A \triangleleft (B \triangleleft C) \quad (A \triangleleft B) \triangleleft C, \Delta \vdash D}{\Gamma, \Delta \vdash D} \end{array} \quad (12) $$

**Theorem 26.** Let A be a formula. Then $\vdash_{IBV} A \ iff \ \vdash_{INML \cup \{a-cut_L, a-cut_R\}} A$.

*Proof.* As before, it suffices to extend Lemmas 15 and 16. Note that for simulating $a-cut_L$ and $a-cut_R$ in IBV, we use $i^*_1$ and then apply Corollary 9. $\square$

**Remark 27.** A sequent calculus for BV could be obtained by adding to the cut-free sequent system NML with the unit from [2] the one-side version of the rule $a-cut_R$.

# 8 Conclusion and Future Work

In this paper, we have defined two logics, IBV and INML, which are the intuitionistic counterparts of the non-commutative logics BV and NML, respectively.
In order to show that both systems are conservative extensions of the multi-
plicative intuitionistic linear logic IMLL, for IBV we have implemented the first
splitting proof for an intuitionistic system, and for INML we have shown that
cut-elimination holds for the sequent system INML.

In future work, we will study extensions of our systems with contraction and weakening, in order to obtain conservative extensions of intuitionistic logic with a non-commutative connective. In particular, since one could see intuitionsitic logic as an extension of IMLL with the contraction and weakening rules, one could define a system NLJ = INML ∪ {w, c}, as well as extending IBV with the deep inference rules w•↓ and c•↓ corresponding to weakening and contraction (see Figure 12). Note that the deep inference versions of weakening and contraction can only be applied in a negative context, as the weakening and contraction can only be applied on the left-hand side of a sequent in sequent calculus.

These systems could be used as a framework for defining typing disciplines
for imperative programming languages in which the sequentiality of the order of
instructions is modeled with the new non-commutative connective.

References

1. Acclavio, M., Horne, R., Mauw, S., Straßburger, L.: A Graphical Proof Theory of Logical Time. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 22:1–22:25. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). https://doi.org/10.4230/LIPIcs.FSCD.2022.22

2. Acclavio, M., Manara, G.: Proofs as execution trees for the π-calculus (2024), https://arxiv.org/abs/2411.08847, arXiv Preprint 2411.08847

3. Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies. In: Vafeiadis, V. (ed.) Programming Languages and Systems. pp. 23–55. Springer Nature Switzerland, Cham (2025)

4. Acclavio, M., Strassburger, L.: Intuitionistic BV (extended version) (2025), https://arxiv.org/abs/2505.13284

5. Blute, R., Panangaden, P., Slavnov, S.: Deep inference and probabilistic coherence spaces. Applied Categorical Structures 20(3), 209–228 (2012). https://doi.org/10.1007/s10485-010-9241-0

6. Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNAI, vol. 2250, pp. 347–361. Springer (2001)

7. Bruscoli, P.: A purely logical account of sequentiality in proof search. In: International Conference on Logic Programming. pp. 302–316. Springer (2002)

8. Cockett, J.R.B., Seely, R.A.: Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory and Applications of categories 3(5), 85–131 (1997)

9. Guglielmi, A.: Concurrency and plan generation in a logic programming language with a sequential operator. In: ICLP. pp. 240–254. Citeseer (1994)

10. Guglielmi, A.: Sequentiality by linear implication and universal quantification. In: Desel, J. (ed.) Structures in Concurrency Theory. pp. 160–174. Springer London, London (1995)
11. Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8(1) (Jan 2007). https://doi.org/10.1145/1182613.1182614

12. Guglielmi, A., Gundersen, T., Parigot, M.: A Proof Calculus Which Reduces Syntactic Bureaucracy. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 135–150. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2010). https://doi.org/10.4230/LIPIcs.RTA.2010.135

13. Guglielmi, A., Straßburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) Computer Science Logic, CSL 2001. LNCS, vol. 2142, pp. 54–68. Springer-Verlag (2001)

14. Guglielmi, A., Straßburger, L.: A system of interaction and structure V: the exponentials and splitting. Math. Struct. Comput. Sci. 21(3), 563–584 (2011)

15. Horne, R., Tiu, A., Aman, B., Ciobanu, G.: Private Names in Non-Commutative Logic. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 59, pp. 31:1–31:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2016). https://doi.org/10.4230/LIPIcs.CONCUR.2016.31

16. Horne, R., Tiu, A., Aman, B., Ciobanu, G.: De Morgan dual nominal quantifiers modelling private names in non-commutative logic. ACM Trans. Comput. Logic 20(4) (jul 2019). https://doi.org/10.1145/3325821

17. Kahramanoğulları, O.: System BV without the equalities for unit. In: Aykanat, C., Dayar, T., Körpeoğlu, I. (eds.) 19th International Symposium on Computer and Information Sciences, ISCIS 2004. Lecture Notes in Computer Science, vol. 3280, pp. 986–995. Springer-Verlag (2004), http://www.doc.ic.ac.uk/~ozank/Papers/bvn.pdf

18. Nguyên, L.T.D., Straßburger, L.: A system of interaction and structure III: the complexity of BV and pomset logic. Log. Methods Comput. Sci. 19(4) (2023). https://doi.org/10.46298/LMCS-19(4:25)2023

19. Nguyên, L.T.D., Straßburger, L.: BV and Pomset Logic are not the same. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 216, pp. 3:1–3:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022). https://doi.org/10.4230/LIPIcs.CSL.2022.3

20. Retoré, C.: Réseaux et Séquents Ordonnés. Ph.D. thesis, Université Paris VII (1993)

21. Retoré, C.: Pomset logic as a calculus of directed cographs. In: Abrusci, V.M., Casadio, C. (eds.) Dynamic Perspectives in Logic and Linguistics, pp. 221–247. Bulzoni, Roma (1999), also available as INRIA Rapport de Recherche RR-3714

22. Retoré, C.: Pomset logic: The other approach to noncommutativity in logic. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics pp. 299–345 (2021)

23. Roversi, L.: Linear lambda calculus and deep inference. In: Proceedings of the 10th International Conference on Typed Lambda Calculi and Applications. p. 184–197. TLCA’11, Springer-Verlag, Berlin, Heidelberg (2011)

24. Simmons, W., Kissinger, A.: Higher-Order Causal Theories Are Models of BV-Logic. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 241, pp. 80:1–80:14.
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2022).
https://doi.org/10.4230/LIPIcs.MFCS.2022.80

25. Straßburger, L.: Linear Logic and Noncommutativity in the Calculus of Structures. Ph.D. thesis, Technische Universität Dresden (2003)

26. Tiu, A.F.: A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science 2(2), 1–24 (2006). https://doi.org/10.2168/LMCS-2(2:4)2006