# Type Isomorphisms for Multiplicative-Additive Linear Logic

Rémi Di Guardia, Olivier Laurent

► To cite this version:

Rémi Di Guardia, Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. pp.2, 10.4230/LIPIcs.FSCD.2023.26 . hal-04082204v2

HAL Id: hal-04082204

https://hal.science/hal-04082204v2

Submitted on 29 Jun 2023

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
# Type Isomorphisms for Multiplicative-Additive Linear Logic

Rémi Di Guardia ☐

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France

Olivier Laurent ☐

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France

## Abstract

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [2]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [10]. We then use the sequent calculus to extend our results to full MALL (including all units).

**2012 ACM Subject Classification** Theory of computation → Linear logic

**Keywords and phrases** Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products

**Related Version** Conference version: https://doi.org/10.4230/LIPIcs.FSCD.2023.26

**Funding** This work was performed within the framework of the LABEX MILYON (ANR-10-LABX- 0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), and supported by the projects DyVerSe (ANR-19-CE48-0010), QuaReMe (ANR-20-CE48-0005) and ReCiProg (ANR-21-CE48-0019), all operated by the French National Research Agency (ANR). This work was also supported by the IRN Linear Logic.

## 1 Introduction

The question of type isomorphisms consists in trying to understand when two types in a type system (or two formulas in a logic) are “the same”. The general question can be described in category theory: two objects *A* and *B* are isomorphic ($A \simeq B$) if there exist morphisms $A \xrightarrow{f} B$ and $B \xrightarrow{g} A$ such that $f \circ g = \text{id}_B$ and $g \circ f = \text{id}_A$. *f* and *g* are the underlying isomorphisms. Given a (class of) category, the question is then to find equations characterizing when two objects *A* and *B* are isomorphic (in all instances of the class). The focus here is on pairs of isomorphic objects rather than on the isomorphisms themselves. For example, in the class of cartesian categories, one finds the following isomorphic objects: $A \times B \simeq B \times A$, $(A \times B) \times C \simeq A \times (B \times C)$ and $A \times \top \simeq A$. Regarding type systems and logics, one can instantiate the categorical notion. For instance in typed $\lambda$-calculi: two types *A* and *B* are isomorphic if there exist two $\lambda$-terms $M : A \to B$ and $N : B \to A$ such that $\lambda x : B.(M(Nx)) =_{\beta\eta} \lambda x : B.x$ and $\lambda x : A.(N(Mx)) =_{\beta\eta} \lambda x : A.x$ where $=_{\beta\eta}$ is $\beta\eta$-equality. This corresponds to isomorphic objects in the syntactic category generated by terms up to $=_{\beta\eta}$. Similarly, type isomorphisms can also be considered in logic, following what happens in the $\lambda$-calculus through the Curry-Howard correspondence: simply replace $\lambda$-terms with proofs, types with formulas, $\beta$-reduction with cut-elimination and $\eta$-expansion with axiom-expansion. In this way, type isomorphisms are studied in a wide range of theories, such as category theory [16], $\lambda$-calculus [4] and proof theory [2]. They may be used to develop practical tools, such as search in a library of a functional programming language [14].

Following the definition, it is usually easy to prove that the type-isomorphism relation is
a congruence. It is then natural to look for an equational theory generating this congruence. Testing whether or not two types are isomorphic is then much easier. An equational theory $\mathcal{T}$ is called *sound* with respect to type isomorphisms if types equal up to $\mathcal{T}$ are isomorphic. It is called *complete* if it equates any pair of isomorphic types. Given a (class of) category, a type system or a logic, our goal is to find an associated sound and complete equational theory for type isomorphisms. This is not always possible as the induced theory may not be finitely axiomatisable (see for instance [6]).

Soundness is usually the easy direction as it is sufficient to exhibit pairs of terms corresponding to each equation. The completeness part is often harder, and there are in the literature two main approaches to solve this problem. The first is a semantic method, relying on the fact that if two types are isomorphic then they are isomorphic in all (denotational) models. One thus looks for a model in which isomorphisms can be computed (more easily than in the syntactic model) and are all included in the equational theory under consideration (this is the approach used in [16, 12] for example). Finding such a model simple enough for its isomorphisms to be computed, but still complex enough not to contain isomorphisms absent in the syntax is the difficulty. The second method is the syntactic one, which consists in studying isomorphisms directly in the syntax. The analysis of pairs of terms composing to the identity should provide information on their structure and then on their type so as to deduce the completeness of the equational theory (see for example [4, 2]). The easier the equality ($=_{\beta\eta}$ for example) between proof objects can be computed, the easier the analysis of isomorphisms will be.

We place ourselves in the framework of linear logic (LL) [7], the underlying question being “is there an equational theory corresponding to the isomorphisms between formulas in this logic?”. LL is a very rich logic containing three classes of propositional connectives: multiplicative, additive and exponential ones. The multiplicative and additive families provide two copies of each classical propositional connective: two copies of conjunction ($\otimes$ and $\&$), of disjunction ($\not\wedge$ and $\oplus$), of true ($1$ and $\top$) and of false ($\bot$ and $0$). The exponential family is constituted of two modalities `!` and `?` bridging the gap between multiplicatives and additives through four isomorphisms `!(A & B) \simeq !A \otimes !B`, `?((A \oplus B) \simeq ?A \not\wedge ?B`, `$!\top \simeq 1$` and `$?0 \simeq \bot$`. In the multiplicative fragment (MLL) of LL (using only $\otimes$, $\not\wedge$, `1` and `$\bot$`, and corresponding to `*`-autonomous categories), the question of type isomorphisms was answered positively using a syntactic method based on proof-nets by Balat and Di Cosmo [2]: isomorphisms emerge from associativity and commutativity of the multiplicative connectives $\otimes$ and $\not\wedge$, as well as neutrality of the multiplicative units `1` and `$\bot$`. The question was also solved for the polarized fragment of LL by one of the authors using game semantics [12]. It is conjectured that isomorphisms in full LL correspond to those in its polarized fragment (Table 1 together with the four exponential equations above). As a step towards solving this conjecture, we prove the type isomorphisms in the multiplicative-additive fragment (MALL) of LL are generated by the equational theory of Table 1 (and this applies at the same time to the class of `*`-autonomous categories with finite products).

This situation is much richer than in the multiplicative fragment since isomorphisms include not only associativity, commutativity and neutrality, but also the distributivity of the multiplicative connective $\otimes$ (resp. $\not\wedge$) over the additive $\oplus$ (resp. $\&$) as well as the associated annihilation laws for the additive unit `0` (resp. `$\top$`) over the multiplicative connective $\otimes$ (resp. $\not\wedge$). Using a semantic approach looks difficult as most of the known models of MALL immediately come with unwanted isomorphisms not valid in the syntax: `$\top \otimes A \simeq \top$` in coherent spaces for example [7]. For this reason we use a syntactic method. We follow the approach by Balat and Di Cosmo [2] based on proof-nets. Indeed, proof-nets provide a very
<table><caption>Table 1 Type isomorphisms in MALL</caption><thead><tr><th></th><th>A ⊗ B = B ⊗ A</th><th>A ℘ B = B ℘ A</th><th>A ⊕ B = B ⊕ A</th><th>A &amp; B = B &amp; A</th></tr></thead><tbody><tr><th>Commutativity</th><td>A ⊗ (B ⊗ C) = (A ⊗ B) ⊗ C</td><td>A ℘ (B ℘ C) = (A ℘ B) ℘ C</td><td>A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C</td><td>A &amp; (B &amp; C) = (A &amp; B) &amp; C</td></tr><tr><th>Associativity</th><td>A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C</td><td>A ℘ (B ℘ C) = (A ℘ B) ℘ C</td><td>A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C</td><td>A &amp; (B &amp; C) = (A &amp; B) &amp; C</td></tr><tr><th>Distributivity</th><td>A ⊗ (B ⊕ C) = (A ⊗ B) ⊕ (A ⊗ C)</td><td>A ℘ (B ℘ C) = (A ℘ B) ℘ C</td><td>A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ (A ⊕ C)</td><td>A &amp; (B &amp; C) = (A &amp; B) &amp; (A &amp; C)</td></tr><tr><th>Neutrality</th><td>A ⊗ 1 = A</td><td>A ℘ ⊥ = A</td><td>A ⊕ 0 = A</td><td>A &amp; ⊤ = A</td></tr><tr><th>Annihilation</th><td>A ⊗ 0 = 0</td><td>A ℘ ⊤ = ⊤</td><td></td><td></td></tr></tbody></table>

good syntax for linear logic where studying composition of proofs by cut, cut-elimination and identity of proofs is very natural. However, already in [2] some trick had to be used to deal with units as proof-nets are working perfectly only in the unit-free multiplicative fragment of linear logic. If one puts units aside, there is a notion of proof-nets incorporating both multiplicative and additive connectives in such a way that cut-free proofs are represented in a *canonical* way, and cut-elimination can be dealt with in a parallel manner. This is the syntax of proof-nets introduced by Hughes & Van Glabbeek in [10].

Our proof of the completeness of the equational theory of Table 1 goes in two steps. First we adapt, in Section 3, the proof of Balat & Di Cosmo [2] to the setting of Hughes & Van Glabbeek's proof-nets [10]. This requires a precise analysis of the structure of proof-nets because of the richer structure induced by the presence of the additive connectives. The situation is much more complex than in the multiplicative setting since for example sub-formulas can be duplicated through distributivity equations, breaking a linearity property crucial in [2]. Once this is solved, it remains to add units (Section 4). By lack of a good-enough notion of proof-nets for MALL including units, we go back to the sequent calculus to deal with units on top of the results obtained for the unit-free fragment. This goes through a characterization of the equality of proofs up to cut-elimination and axiom-expansion by means of rule commutations. A result which is not surprising, but never proved before for MALL as far as we know, and rather tedious to settle. Using it, we analyse the behaviour of units inside isomorphisms to conclude that they can be replaced with fresh atoms, once formulas are simplified appropriately. We can conclude by means of the unit-free case. Finally, seeing MALL as a category, we extend our result to conclude that Table 1 (together with $A \to B \simeq A^{\perp} \mathfrak{N} B$, De Morgan's laws and involutivity of negation) provides the equational theory of isomorphisms valid in all $\star$-autonomous categories with finite products (Section 5).

Full proofs are given in appendix.

# 2 Definitions and preliminary results

## 2.1 Multiplicative-Additive Linear Logic

The multiplicative-additive fragment of linear logic [7], denoted by MALL, has formulas given by the following grammar, where $X$ belongs to a given enumerable set of *atoms*:

$$A, B := X \mid X^{\perp} \mid A \otimes B \mid A \mathfrak{N} B \mid 1 \mid \perp \mid A \& B \mid A \oplus B \mid \top \mid 0$$

Orthogonality $(\cdot)^{\perp}$ expands into an involution on arbitrary formulas through $X^{\perp\perp} = X$ on an atom $X$, $1^{\perp} = \perp$, $\perp^{\perp} = 1$, $\top^{\perp} = 0$, $0^{\perp} = \top$ and De Morgan's laws $(A \otimes B)^{\perp} = B^{\perp} \mathfrak{N} A^{\perp}$, $(A \mathfrak{N} B)^{\perp} = B^{\perp} \otimes A^{\perp}$, $(A \& B)^{\perp} = B^{\perp} \oplus A^{\perp}$, $(A \oplus B)^{\perp} = B^{\perp} \& A^{\perp}$. The *non-commutative* De Morgan's laws are the good notion of duality, as shown in the context of cyclic linear logic where this leads to planar proof-nets [1]. This choice in our setting will often result in planar graphs on our illustrations, with axiom links not crossing each others.
4 Type Isomorphisms for Multiplicative-Additive Linear Logic

Sequents are lists of formulas of the form $\vdash A_1, \dots, A_n$. Sequent calculus rules are:<fnref n="1" />

$$ \begin{array}{ccc} \frac{}{\vdash A^{\perp}, A} & ax & \frac{}{\vdash \Gamma} \quad \frac{}{\vdash \sigma(\Gamma)} \quad ex \quad \frac{}{\vdash A, \Gamma} \quad \frac{}{\vdash A^{\perp}, \Delta} \quad \frac{}{\vdash \Gamma, \Delta} \quad \text{cut} \\ \frac{\vdash A, \Gamma \quad \vdash B, \Delta}{\vdash A \otimes B, \Gamma, \Delta} \quad \otimes & & \frac{\vdash A, B, \Gamma}{\vdash A \nparallel B, \Gamma} \quad \nparallel & \frac{}{\vdash 1} \quad 1 & \frac{}{\vdash \Gamma} \quad \frac{}{\vdash \perp, \Gamma} \quad \perp \\ \frac{\vdash A, \Gamma \quad \vdash B, \Gamma}{\vdash A \& B, \Gamma} \quad \& & \frac{\vdash A, \Gamma \quad \vdash A \oplus B, \Gamma}{\vdash A \oplus B, \Gamma} \quad \oplus 1 & \frac{\vdash B, \Gamma \quad \vdash A \oplus B, \Gamma}{\vdash A \oplus B, \Gamma} \quad \oplus 2 & \frac{}{\vdash \top, \Gamma} \quad \top \end{array} $$

In practice we consider exchange rules as incorporated in the conclusion of the rule above, thus dealing with rules like: $\frac{}{\vdash A, B, \Gamma, \Delta} \nparallel$. In this spirit, when we write $\frac{}{\vdash \Gamma, A \nparallel B, \Delta} \nparallel$, we mean that the appropriate permutation is also incorporated in the rule above.

The main difference with the multiplicative fragment of linear logic (MLL) is the `&-rule`, which introduces some sharing of the context $\Gamma$. From this comes the notion of a *slice* [7, 8] which is a partial proof missing some additive component. Slices are obtained by using the same rules as proofs except for the `&-rule` which is replaced by its two sliced versions:

$$ \frac{\vdash A, \Gamma}{\vdash A \& B, \Gamma} \&_1 \qquad \frac{\vdash B, \Gamma}{\vdash A \& B, \Gamma} \&_2 $$

By *unit-free MALL*, we mean the restriction of MALL to formulas not involving the units 1, $\perp$, $\top$ and 0, and as such without the 1, $\perp$ and $\top$-rules. When speaking of a *positive formula*, we mean a formula with main connective $\otimes$ or $\oplus$, a unit 1 or 0, or an atom $X$. A *negative formula* is one with main connective $\nparallel$ or `&`, a unit $\perp$ or $\top$, or a negated atom $X^{\perp}$.

## 2.2 Linear isomorphisms

**► Definition 1 (Isomorphism).** Two formulas $A$ and $B$ are isomorphic, denoted $A \simeq B$, if there exist proofs $\pi$ of $\vdash A^{\perp}, B$ and $\pi'$ of $\vdash B^{\perp}, A$ whose composition by cut over $B$ (resp. $A$) is equal to the axiom on $\vdash A^{\perp}, A$ (resp. $\vdash B^{\perp}, B$) up to axiom-expansion and cut-elimination. (Axiom-expansion and cut-elimination for MALL are recalled in Appendix A.)

Because of the analogy with the $\lambda$-calculus and since there will be no ambiguity, we use the notation $=_{\beta\eta}$ for equality of proofs up to cut-elimination ($\beta$) and axiom-expansion ($\eta$). Similarly, $=_{\beta}$ is equality up to cut-elimination only. We use the notations $\pi \overset{B}{\rightleftharpoons} \pi'$ for the proof obtained by adding a cut on $B$ between $\pi$ and $\pi'$, and $A \stackrel{\pi, \pi'}{\cong} B$ when $\pi$ and $\pi'$ define an isomorphism between $A$ and $B$, that is when $\pi \overset{B}{\rightleftharpoons} \pi' =_{\beta\eta} \text{id}_A$ and $\pi \overset{A}{\rightleftharpoons} \pi' =_{\beta\eta} \text{id}_B$ (where $\text{id}_A$ is the axiom-expansion of the proof of $\vdash A^{\perp}, A$ containing just an axiom rule).

We aim to prove that two MALL (resp. unit-free MALL) formulas are isomorphic if and only if they are equal in the equational theory $\mathcal{E}$ (resp. $\mathcal{E}^\dagger$) defined as follows.

**► Definition 2 (Equational theories).** We denote by $\mathcal{E}$ the equational theory given on Table 1 on Page 3, while $\mathcal{E}^\dagger$ denotes the part not involving units, i.e. with commutativity, associativity and distributivity only.

Given an equational theory $\mathcal{T}$, the notation $A =_{\mathcal{T}} B$ means that formulas $A$ and $B$ are equal in the theory $\mathcal{T}$. As often, the soundness part is easy (but tedious) to prove.

**► Theorem 3 (Isomorphisms soundness, see Lemma 3 in [12]).** If $A =_{\mathcal{E}} B$ then $A \simeq B$.

<footnote n="1">¹ With $A$ and $B$ arbitrary formulas, $\Gamma$ and $\Delta$ contexts (i.e. lists of formulas) and $\sigma$ a permutation.</footnote>
All the difficulty lies in the proof of the other implication, completeness, on which the
rest of this work focuses.

## 2.3 Axiom-expansion

A first simplification is that we can reduce the definition of isomorphisms to proofs with
expanded axioms only, no more using the $η$ relation. Given an MALL proof $π$, we denote by
$η(π)$ the $η$-normal form of $π$, i.e. the proof obtained by expanding iteratively all $ax$-rules in
$π$ (axiom-expansion is confluent and strongly normalizing, see Appendix B.1).

**► Proposition 4 (Reduction to axiom-expanded proofs).** Let $π$ and $ω$ be MALL proofs such that $π =_{βη} ω$. Then $η(π) =_{β} η(ω)$ with, in this sequence, only proofs in $η$-normal form.

Thus, we will from now on consider only proofs with expanded axioms, manipulated
through composition by cut and cut-elimination. To prove completeness, we start with the
unit-free case by using a syntactic approach based on the proof-nets from Hughes & Van
Glabbeek [10], which are a more canonical representation of proofs [11].

## 2.4 Proof-nets for unit-free MALL

We use the definition of unit-free MALL proof-net from [10]. Other definitions exist, see the
original one from Girard [8], or others such as [5, 9]. Still, the definition we take is one of
the most satisfactory, from the point of view of canonicity and cut-elimination for instance
(see [10, 11], or the introduction of [9] for a comparison of alternative definitions). We recall
here quickly this definition of proof-nets. Please refer to [10] for more details.

A sequent is seen as its syntactic forest with as internal vertices its connectives and as
leaves the atoms of its formulas. We always identify a formula $A$ with its syntactic tree $T(A)$.
A *cut pair* is a formula $A * A^{\perp}$, for a formula $A$; the connective $*$ is unordered. A *cut sequent* $[\Sigma] \Gamma$ is composed of a list $\Sigma$ of cut pairs and a sequent $\Gamma$. When $\Sigma = \emptyset$ is empty, we denote it simply by $\Gamma$. When we write a $\mathfrak{N}\&$-vertex, we mean a $\mathfrak{N}$- or $\&$-vertex (a *negative vertex*); similarly a $\otimes\&$-vertex is a $\otimes$- or $\&$-vertex (a *positive vertex*). An *additive resolution* of a cut sequent $[\Sigma] \Gamma$ is any result of deleting zero or more cut pairs from $\Sigma$ and one argument subtree of each additive connective ($\&$ or $\oplus$) of $\Sigma \cup \Gamma$. A *$\&$-resolution* of a cut sequent $[\Sigma] \Gamma$ is any result of deleting one argument subtree of each $\&$-connective of $\Sigma \cup \Gamma$.

An (*axiom*) *link* on $[\Sigma] \Gamma$ is an unordered pair of complementary leaves in $\Sigma \cup \Gamma$ (labeled with $X$ and $X^{\perp}$). A *linking* $\lambda$ on $[\Sigma] \Gamma$ is a set of links on $[\Sigma] \Gamma$ such that the sets of the leaves of its links form a partition of the set of leaves of an additive resolution of $[\Sigma] \Gamma$, additive resolution which is denoted $[\Sigma] \Gamma \upharpoonright \lambda$.

A set of linkings $\Lambda$ on $[\Sigma] \Gamma$ toggles a $\&$-vertex $W$ if both arguments (called *premises*) of $W$ are in $[\Sigma] \Gamma \upharpoonright \Lambda := \bigcup_{\lambda \in \Lambda} [\Sigma] \Gamma \upharpoonright \lambda$. We say a link $a$ *depends on* a $\&$-vertex $W$ in $\Lambda$ if there exist $\lambda, \lambda' \in \Lambda$ such that $a \in \lambda \setminus \lambda'$ and $W$ is the only $\&$-vertex toggled by $\{\lambda; \lambda'\}$. The graph $G_{\Lambda}$ is defined as $[\Sigma] \Gamma \upharpoonright \Lambda$ with the edges from $\bigcup \Lambda$ and enriched with jump edges $l \to W$ for each leaf $l$ and each $\&$-vertex $W$ such that there exists $a \in \lambda \in \Lambda$, between $l$ and some $l'$, with $a$ depending on $W$ in $\Lambda$. When $\Lambda = \{\lambda\}$ is composed of a single linking, we shall simply denote $G_{\lambda} = G_{\{\lambda\}}$ (which is the graph $[\Sigma] \Gamma \upharpoonright \lambda$ with the edges from $\lambda$ and no jump edge).

A *switch edge* of a $\mathfrak{N}\&$-vertex $N$ is an in-edge of $N$, i.e. an edge between $N$ and one of its premises or a jump to $N$. A *switching cycle* is a cycle with at most one switch edge of each $\mathfrak{N}\&$-vertex. A *$\mathfrak{N}$-switching* of a linking $\lambda$ is any subgraph of $G_{\lambda}$ obtained by deleting a switch edge of each $\mathfrak{N}$-vertex; denoting by $\phi$ this choice of edges, the subgraph it yields is $G_{\phi}$.
<figure><img src="image_2.png" /><figcaption>■ **Figure 1** Graphs from an example of a proof-net: from left to right $G_{\lambda_1}$, $G_{\lambda_2}$ and $G_{\{\lambda_1;\lambda_2\}}$</figcaption></figure>

**► Definition 5 (Proof-net).** A unit-free MALL proof-net $\theta$ on a cut sequent $[\Sigma] \Gamma$ is a set of linkings satisfying:

(P0) Cut: Every cut pair of $\Sigma$ has a leaf in $\theta$.

(P1) Resolution: Exactly one linking of $\theta$ is on any given $\&$-resolution of $[\Sigma] \Gamma$.

(P2) MLL: For every $\mathcal{N}$-switching $\phi$ of every linking $\lambda \in \theta$, $G_\phi$ is a tree.

(P3) Toggling: Every set $\Lambda \subseteq \theta$ of two or more linkings toggles a $\&$-vertex that is in no switching cycle of $G_\Lambda$.

These conditions are called the *correctness criterion*. Condition (P0) is here to prevent unused $\ast$-vertices. A *cut-free* proof-net is one without $\ast$-vertices (it respects (P0) trivially). Condition (P1) is a correctness criterion for ALL proof-nets [10] and (P2) is the Danos-Regnier criterion for MLL proof-nets [3]. However, (P1) and (P2) together are insufficient for cut-free MALL proof-nets, hence the last condition (P3) taking into account interactions between the slices (see also [5] for a similar condition for example). Sets composed of a single linking $\lambda$ are not considered in (P3), but by (P2) the graph $G_\lambda$ has no switching cycle.

An example of proof-net, illustrated on Figure 1, is the following. On the cut sequent $[X_5 * X_6^\perp] X_1 \& X_2^\perp, X_3 \oplus X_4^\perp$ (where each $X_i$ is an occurrence of the same atom $X$), set $\lambda_1 = \{(X_1, X_6^\perp), (X_4^\perp, X_5)\}$ and $\lambda_2 = \{(X_2^\perp, X_3)\}$. One can check $\{\lambda_1; \lambda_2\}$ is a proof-net.

In the particular setting of isomorphisms, we mainly consider proof-nets with two conclusions. This allows to define a notion of duality on leaves and connectives. Consider a cut sequent containing both $A$ and $A^\perp$. For $V$ a vertex in (the syntax tree $T(A)$ of) $A$, we denote by $V^\perp$ the corresponding vertex in $A^\perp$. As expected, $V^\perp = V$. This also respects orthogonality for formulas on leaves: given a leaf $l$ of $A$, labeled by a formula $X$, the label of $l^\perp$ is $X^\perp$. We can also define a notion of duality on premises: given a premise of a vertex $V \in T(A)$, the dual premise of $V^\perp$ is the corresponding premise in $T(A^\perp)$. In other words, if in $L - V - R$ we consider the premise $L$ then in $R^\perp - V^\perp - L^\perp$ its dual premise is $L^\perp$.

**► Definition 6 (Composition).** Given proof-nets $\theta$ and $\vartheta$ of respective conclusions $[\Sigma] \Gamma$, $A$ and $[\Xi] \Delta$, $A^\perp$, the composition over $A$ of $\theta$ and $\vartheta$ is the proof-net $\theta \bowtie^A \vartheta = \{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \vartheta\}$, with conclusions $[\Sigma, \Xi, A * A^\perp] \Gamma, \Delta$.

For example, see Figure 7 with a composition of the proof-nets on Figure 5.

**► Definition 7 (Cut-elimination).** Let $\theta$ be a set of linkings on a cut sequent $[\Sigma] \Gamma$, and $A * A^\perp$ a cut pair in $\Sigma$. Define the elimination of $A * A^\perp$ (or of the cut $\ast$ between $A$ and $A^\perp$) as:

(a) If $A$ is an atom, delete $A * A^\perp$ from $\Sigma$ and replace any pair of links $(l, A)$, $(A^\perp, m)$ ($l$ and $m$ being other occurrences of $A^\perp$ and $A$ respectively) with the link $(l, m)$.

(b) If $A = A_1 \otimes A_2$ and $A^\perp = A_2^\perp \mathcal{N} A_1^\perp$ (or vice-versa), replace $A * A^\perp$ with two cut pairs $A_1 * A_1^\perp$ and $A_2 * A_2^\perp$. Retain all original linkings.

(c) If $A = A_1 \& A_2$ and $A^\perp = A_2^\perp \oplus A_1^\perp$ (or vice-versa), replace $A * A^\perp$ with two cut pairs $A_1 * A_1^\perp$ and $A_2 * A_2^\perp$. Delete all inconsistent linkings, namely those $\lambda \in \theta$ such that in $[\Sigma] \Gamma \vdash \lambda$ the children $\&$ and $\oplus$ of the cut do not take dual premises. Finally, "garbage collect" by deleting any cut pair $B * B^\perp$ for which no leaf of $B * B^\perp$ is in any of the remaining linkings.
See Figure 8 for a result on applying steps (b) and (c) to the proof-net of Figure 7.

► **Proposition 8** (Proposition 5.4 in [10]). *Eliminating a cut in a proof-net yields a proof-net.*

► **Theorem 9** (Theorem 5.5 in [10]). *Cut-elimination of proof-nets is strongly normalizing and confluent.*

A linking $\lambda$ on a cut sequent $[\Sigma] \Gamma$ matches if, for every cut pair $A * A^{\perp}$ in $\Sigma$, any given leaf $l$ of $A$ is in $[\Sigma] \Gamma \upharpoonright \lambda$ if and only if $l^{\perp}$ of $A^{\perp}$ is in $[\Sigma] \Gamma \upharpoonright \lambda$. A linking matches if and only if, when cut-elimination is carried out, the linking never becomes inconsistent, and thus is never deleted. This allows defining *Turbo Cut-elimination* [10], eliminating a cut in a single step by removing inconsistent linkings.

### 3 Completeness for unit-free MALL

Our method relates closely to the one used by Balat and Di Cosmo in [2]. We work on proof-nets, as they highly simplify the problem by representing proofs up to rule commutations [11]. We start by transposing the study of unit-free MALL isomorphisms to proof-nets of a particular shape, called *bipartite full* (Sections 3.1 and 3.2). Then, we use the distributivity isomorphisms to reduce the problem to special formulas, called *distributed*, allowing to consider even more constrained proof-nets (Section 3.3). These are the key differences with the proof in MLL from [2], where some properties are given for free as there are no slice nor distributivity isomorphism. From this point the problem is similar to unit-free MLL, with commutativity and associativity only. We conclude as in [2]: restricting the problem to so-called *non-ambiguous* formulas, isomorphisms are easily characterized (Section 3.4).

#### 3.1 Reduction to proof-nets

We desequationalize a unit-free MALL proof $\pi$ (with expanded axioms) into a proof-net $\mathcal{R}(\pi)$ by induction on $\pi$ using the steps detailed on Figure 2, following [10] with the notation $\theta \triangleright [\Sigma] \Gamma$ for "$\theta$ is a set of linkings on the cut sequent $[\Sigma] \Gamma$". As identified in Section 5.3.4 of [10], desequationalizing with both *cut* and *&-rules* is complex, for cuts can be shared (or not) when translating a *&-rule*:
$$ \frac{\theta \triangleright [\Sigma, \Xi] A, \Gamma \qquad \theta \triangleright [\Sigma, \Phi] B, \Gamma}{\theta \cup \theta \triangleright [\Sigma, \Xi, \Phi] A \& B, \Gamma} \quad \& \quad . $$
We choose to never share cuts ($\Sigma = \emptyset$), thus desequationalization is a function. The cost being that the following $\&$-*cut* commutation yields different proof-nets (contrary to the other commutations, see [11]).

$$ \frac{\frac{\pi_1}{\vdash A, B, \Gamma} \quad \frac{\pi_2}{\vdash A, C, \Gamma} \quad \frac{\pi_3}{\vdash A, B \& C, \Gamma} \quad \& \quad \frac{\pi_1}{\vdash A, B, \Gamma} \quad \frac{\pi_3}{\vdash A^{\perp}, \Delta} \quad \text{cut}}{\vdash B \& C, \Gamma, \Delta} \quad \& \quad \frac{\pi_1}{\vdash A, B, \Gamma} \quad \frac{\pi_3}{\vdash A^{\perp}, \Delta} \quad \text{cut} \quad \frac{\pi_2}{\vdash A, C, \Gamma} \quad \frac{\pi_3}{\vdash A^{\perp}, \Delta} \quad \text{cut}}{\vdash B, \Gamma, \Delta} \quad \& \quad \frac{\pi_2}{\vdash C, \Gamma, \Delta} \quad \&} $$

► **Theorem 10** (Sequentialization, Theorem 5.9 in [10]). *A set of linkings on a cut sequent is a translation of a MALL proof if and only if it is a proof-net.*

► **Definition 11** (Identity proof-net). *We call identity proof-net of a unit-free MALL formula $A$, the proof-net corresponding to the proof id$_A$ (the axiom-expansion of $\frac{\pi_1}{\vdash A^{\perp}, A} ax}$. *.*

► **Theorem 12** (Simulation Theorem). *Let $\pi$ and $\varpi$ be unit-free MALL proof trees (with expanded axioms). If $\pi =_{\beta} \varpi$, then $\mathcal{R}(\pi) =_{\beta} \mathcal{R}(\varpi)$.*

A notion of isomorphism $A \cong_B B$ can be defined directly on proof-nets: $\theta$ and $\vartheta$ are two cut-free proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$ such that $\theta \stackrel{B}{\rightleftharpoons} \vartheta$ and $\vartheta \stackrel{A}{\rightleftharpoons} \theta$ reduce by cut-elimination to identity proof-nets. Using the Simulation Theorem, we obtain:
$$ \frac{\overline{\{((X, X^{\perp}))\} \triangleright [\emptyset] X, X^{\perp}} ax}{\theta \triangleright [\Sigma] \Gamma} \quad \frac{ex}{\theta \triangleright [\Sigma] \sigma(\Gamma)} $$

$$ \frac{\theta \triangleright [\Sigma] A, \Gamma \qquad \vartheta \triangleright [\Xi] A^{\perp}, \Delta}{\{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \vartheta\} \triangleright [\Sigma, \Xi, A * A^{\perp}] \Gamma, \Delta} \quad \text{cut} $$

$$ \frac{\theta \triangleright [\Sigma] A, \Gamma \qquad \vartheta \triangleright [\Xi] B, \Delta}{\{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \vartheta\} \triangleright [\Sigma, \Xi] A \otimes B, \Gamma, \Delta} \otimes \frac{\theta \triangleright [\Sigma] A, B, \Gamma}{\theta \triangleright [\Sigma] A \otimes B, \Gamma} \cong $$

$$ \frac{\theta \triangleright [\Xi] A, \Gamma \qquad \vartheta \triangleright [\Phi] B, \Gamma}{\theta \cup \vartheta \triangleright [\Xi, \Phi] A \& B, \Gamma} \& \quad \frac{\theta \triangleright [\Sigma] A, \Gamma \qquad \theta \triangleright [\Sigma] A \oplus B, \Gamma}{\theta \triangleright [\Sigma] A \oplus B, \Gamma} \oplus_1 \frac{\theta \triangleright [\Sigma] B, \Gamma}{\theta \triangleright [\Sigma] A \oplus B, \Gamma} \oplus_2 $$

We use the implicit tracking of formula occurrences downwards through the rules.

<figure><img src="image_3.png" /><figcaption>Figure 2 Inductive definition of the translation of unit-free MALL proof trees to sets of linkings</figcaption></figure>

**▶ Theorem 13 (Type isomorphisms in proof-nets).** Let $A$ and $B$ be two unit-free MALL formulas. If $A \cong B$ then there exist two proof-nets $\theta$ and $\vartheta$ such that $A^{\theta, \vartheta} \cong B$.

## 3.2 Reduction to bipartite full proof-nets

**▶ Definition 14 (Full, Ax-unique, Bipartite proof-net).** A cut-free proof-net is called full if any of its leaves has (at least) one link on it. Furthermore, if for any leaf there exists a unique link on it (possibly shared among several linkings), then we call this proof-net ax-unique.

A cut-free proof-net is bipartite if it has two conclusions, $A$ and $B$, and each of its links is between a leaf of $A$ and a leaf of $B$ (no link between leaves of $A$, or between leaves of $B$).

We show identity proof-nets are bipartite ax-unique, and isomorphisms are bipartite full.

Using an induction on the formula $A$, we can prove the following results on the identity proof-net of $A$ (see Figure 3 for a graphical intuition).

**▶ Proposition 15.**

(i) An identity proof-net is bipartite ax-unique.

(ii) The axiom links of an identity proof-net are exactly the $(l, l^{\perp})$, for any leaf $l$.

(iii) In the identity proof-net of $A$, exactly one linking is on any given additive resolution of the conclusion $A$.

Neither fullness, ax-uniqueness nor bipartiteness is preserved by cut anti-reduction. A counter-example is given on Figure 4, with a non bipartite proof-net and a non full one whose composition reduces to the identity proof-net (bipartite ax-unique by Proposition 15(i)).<fnref n="2" />
However, if both compositions yield identity proof-nets, we get bipartiteness and fullness.

<footnote n="2">² This example gives a retraction between $(A \not\cong A^{\perp}) \otimes B$ and $((A \not\cong A^{\perp}) \otimes B) \oplus B$ in MALL which is not an isomorphism (as is the retraction between $A$ and $(A \not\to A) \to A = (A \otimes A^{\perp}) \not\cong A$ in MLL).</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 4 Non bipartite proof-net (top-left), non full proof-net (top-right) and one of their composition yielding the identity proof-net (bottom) (jump edges not represented)</figcaption></figure>

**Lemma 16.** Let $\theta$ and $\theta'$ be cut-free proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, such that $\theta' \stackrel{A}{\rightleftharpoons} \theta$ reduces to the identity proof-net of $B$. For any linking $\lambda \in \theta$, there exists $\lambda' \in \theta'$ such that $\lambda \cup \lambda'$ matches in the composition over $B$ of $\theta$ and $\theta'$, $\theta \stackrel{B}{\rightleftharpoons} \theta'$.

**Proof.** Let us consider a linking $\lambda \in \theta$, and call $\mathcal{C}$ the choices of premise on additive connectives of $B$ that $\lambda$ makes. We search some $\lambda' \in \theta'$ making the dual choices of premise on additive connectives of $B^{\perp}$ compared to $\mathcal{C}$. Consider the composition of $\theta$ and $\theta'$ over $A$. It reduces to the identity proof-net of $B$ by hypothesis. By Proposition 15(iii), there exists a unique linking in the identity proof-net of $B$ corresponding to $\mathcal{C}$. Furthermore, the linkings of the identity proof-net are derived from the $\mu \cup \mu'$ for $\mu$ a linking of $\theta$ and $\mu'$ one of $\theta'$, with $\mu \cup \mu'$ matching for a cut over $A$: a linking in the identity proof-net is a linking of the form $\mu \cup \mu'$ where axiom links $(l, m) \in \mu$ and $(m^{\perp}, l^{\perp}) \in \mu'$ are replaced with $(l, l^{\perp})$, with $l$ a leaf of $B$ and $m$ one of $A^{\perp}$ (because an identity proof-net has only links of the form $(l, l^{\perp})$ by Proposition 15(ii)). Therefore, there exist $\mu \in \theta$ and $\mu' \in \theta'$ such that $\mu$ makes the choices $\mathcal{C}$ on $B$ and $\mu \cup \mu'$ matches for the composition of $\theta$ and $\theta'$ over both $A$ and $B$. But $\lambda$ makes the same choices $\mathcal{C}$ on $B$ as $\mu$: $\lambda \cup \mu'$ also matches for a cut over $B$. $\quad \blacksquare$

**Corollary 17.** Assuming $A^{\theta, \theta'} \simeq B$, $\theta$ and $\theta'$ are bipartite.

**Proof.** We proceed by contradiction: w.l.o.g. there is a link $a$ in some linking $\lambda \in \theta$ which is between leaves of $A^{\perp}$. By Lemma 16 there exists $\lambda' \in \theta'$ such that $\lambda \cup \lambda'$ matches for a cut over $B$. Whence $a$, which does not involve leaves of $B$, belongs to a linking of the composition where cuts have been eliminated (it belongs to the linking resulting from $\lambda \cup \lambda'$). But this reduction yields a bipartite proof-net by Proposition 15(i), a contradiction. $\quad \blacksquare$

**Lemma 18.** Assume $\theta$ and $\theta'$ are cut-free proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, and that their composition over $B$ yields the identity proof-net of $A$. Then any leaf of $A^{\perp}$ (resp. $A$) has (at least) one axiom link on it in $\theta$ (resp. $\theta'$).

**Theorem 19.** Assuming $A^{\theta, \theta'} \simeq B$, $\theta$ and $\theta'$ are bipartite full.

**Proof.** By Corollary 17, $\theta$ and $\theta'$ are bipartite, and thanks to Lemma 18, they are full. $\quad \blacksquare$
<figure><img src="image_5.png" /></figure>

## 3.3 Distribution

In general, isomorphisms do not yield ax-unique proof-nets. A counter-example is distributivity: $A \otimes (B \oplus C) \cong (A \otimes B) \oplus (A \otimes C)$, see Figure 5. Nonetheless, distributivity equations are the only ones in $\mathcal{E}^\dagger$ not giving ax-unique proof-nets. We will restrict our study to so-called distributed formulas. Once formulas are distributed, distributivity isomorphisms can be ignored, and isomorphisms between distributed formulas happen to be bipartite ax-unique.

**Definition 20 (Distributed formula).** An MALL formula is distributed if it does not have any sub-formula of the form $A \otimes (B \oplus C)$, $(A \oplus B) \otimes C$, $A \otimes 1$, $1 \otimes A$, $A \oplus 0$, $0 \oplus A$, $A \otimes 0$, $0 \otimes A$ or their duals $(C \& B) \not\cong A$, $C \not\cong (B \& A)$, $\perp \not\cong A$, $A \not\cong \perp$, $\top \& A$, $A \& \top$, $\top \not\cong A$, $A \not\cong \top$ (where A, B and C are any formulas).

**Remark.** This notion is stable by duality: if A is distributed, so is $A^\perp$.

**Proposition 21.** If $\mathcal{E}$ is complete for isomorphisms between distributed formulas, then it is complete for isomorphisms between arbitrary formulas.

We mostly use the correctness criterion through the fact we can sequentialize, i.e. recover a proof tree from a proof-net by Theorem 10. However, in order to prove ax-uniqueness, we make a direct use of the correctness criterion to deduce geometric properties of proof-nets. This part of the proof takes benefits from the specificities of this syntax. We begin with two preliminary results. For $\Lambda$ a set of linkings and $W$ a $\&$-vertex, $\Lambda^W$ denote the set of all linkings in $\Lambda$ whose additive resolution does not contain the right argument of $W$.

**Lemma 22 (Lemma 4.32 in [10], adapted).** Let $\omega$ be a jump-free switching cycle in a proof-net $\theta$. There exists a subset of linkings $\Lambda \subseteq \theta$ such that $\omega \subseteq \mathcal{G}_\Lambda$, $\omega \not\subseteq \mathcal{G}_{\Lambda^W}$ and for any $\&$-vertex $W$ toggled by $\Lambda$, there exists an axiom link $a \in \omega$ depending on $W$ in $\Lambda$.

For $U$ and $V$ vertices in a tree, their first common descendant is the vertex of the tree which is a descendant of both $U$ and $V$ and which has no descendant respecting this property (with a tree represented with its root at the bottom, which is a descendant of the leaves).

**Lemma 23.** Let $\theta$ be a proof-net of conclusions $\Gamma, A$. If there is a jump edge $l \xrightarrow{j} W$ with $l, W \in T(A)$ and $W$ not a descendant of $l$, then their first common descendant $C$ is a $\mathcal{N}$.

**Proof.** As there is a jump $l \xrightarrow{j} W$, there exist linkings $\lambda, \lambda' \in \theta$ such that $W$ is the only $\&$ toggled by $\{\lambda; \lambda'\}$, and a link $a \in \lambda \setminus \lambda'$ using the leaf $l$. In particular, the jump $l \xrightarrow{j} W$ is in $\mathcal{G}_{\{\lambda; \lambda'\}}$. For $l$ and $W$ are both in the additive resolution of $\lambda$, both premises of $C$ are in the additive resolution of $\lambda$, thus $C$ cannot be an additive connective, so not a $\&$ nor a $\oplus$-vertex.

Assume by contradiction that $C$ is a $\otimes$. Call $\delta$ the path in $T(A)$ from $W$ to $C$, and $\mu$ the one from $C$ to $l$ (see Figure 6). Then, $(l \xrightarrow{j} W)\delta\mu$ is a switching cycle in $\mathcal{G}_{\{\lambda; \lambda'\}}$. According to (P3), there exists a $\&$ toggled by $\{\lambda; \lambda'\}$ not in any switching cycle of $\mathcal{G}_{\{\lambda; \lambda'\}}$. A contradiction, for $W$ is the only $\&$ toggled by $\{\lambda; \lambda'\}$. Whence, $C$ can only be a $\mathcal{N}$. ◀
<figure><img src="image_6.png" /><figcaption>■ **Figure 6** Illustration of the proof of Lemma 23</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>■ **Figure 7** Proof-nets from Figure 5 composed by cut on $(A \otimes B) \oplus (A \otimes C)$</figcaption></figure>

Now, let us prove that isomorphisms of distributed formulas are bipartite *ax*-unique. We will consider proof-nets corresponding to an isomorphism that we cut and where we eliminate all cuts not involving atoms. To give some intuition, let us consider the non-*ax*-unique proof-nets of Figure 5. Composing them together by cut on $(A \otimes B) \oplus (A \otimes C)$ gives the proof-net illustrated on Figure 7. Reducing all cuts not involving atoms yields the proof-net on Figure 8, that we call an *almost reduced composition*. We stop there because of the switching cycle produced by the two links on *A* (dashed in blue on Figure 8), less visible in the non-reduced composition of Figure 7. However, reducing all cuts gives the identity proof-net, which has no switching cycle: during these reductions, both links on *A* are merged. By using *almost reduced composition*, we are going to prove that links preventing *ax*-uniqueness yield switching cycles, and moreover that these cycles are due to non-distributed formulas only.

► **Definition 24 (Almost reduced composition).** *Take $\theta$ and $\theta'$ cut-free proof-nets of respective conclusions A, B and $B^\perp$, C. The almost reduced composition over B of $\theta$ and $\theta'$ is the proof-net resulting from the composition over B of $\theta$ and $\theta'$ where we repeatedly reduce all cuts not involving atoms (i.e. not applying step (a) of Definition 7).*

Let us fix *A* and *B* two unit-free MALL (not necessarily distributed yet) formulas as well as $\theta$ and $\theta'$ such that $A \stackrel{\theta, \theta'}{\cong} B$. By Theorem 19, $\theta$ and $\theta'$ are bipartite full. We denote by $\vartheta$ the almost reduced composition over *B* of $\theta$ and $\theta'$. Here, we can extend our duality on vertices and premises (defined in Section 2.4) to links.

<figure><img src="image_8.png" /><figcaption>■ **Figure 8** An almost reduced composition of the proof-nets on Figure 5</figcaption></figure>
<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /><figcaption>Figure 9 Illustration of Lemma 25</figcaption></figure>

**Lemma 25.** Given $l$ a leaf of $A$ (resp. $A^{\perp}$) and $m$ one of $B^{\perp}$ (resp. $B$), there is an axiom link $a = (l, m)$ in some linking $\lambda \in \mathcal{V}$ if and only if there is an axiom link $(l^{\perp}, m^{\perp})$ in the same linking $\lambda$, that we will denote $a^{\perp} = (l^{\perp}, m^{\perp})$ (see Figure 9).

**Proof.** By symmetry, assume $(l, m) \in \lambda \in \mathcal{V}$. As the cut $m * m^{\perp}$ belongs to the additive resolution of $\lambda$ (for $m$ is inside), $m^{\perp}$ is a leaf in this resolution. Thus, there is a link $(m^{\perp}, l') \in \lambda$ for some leaf $l'$, which necessarily belongs to $A$ by bipartiteness of $\theta'$. It stays to prove $l' = l^{\perp}$. If we were to eliminate all cuts in $\mathcal{V}$, we would get the identity proof-net on $A$ by hypothesis. But eliminating the cut $m * m^{\perp}$ yields a link $(l, l')$, which is not modified by the elimination of the other atomic cuts. By Proposition 15(ii), $l' = l^{\perp}$ follows. ◀

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

**Lemma 26.** Let $\lambda$ be a linking of $\mathcal{V}$, and $V$ an additive vertex in its additive resolution. Then $V^{\perp}$ is also inside, with as premise kept the dual premise of the one kept for $V$.

**Lemma 27.** Let $W$ and $P$ be respectively a $\&$-vertex and a $\oplus$-vertex in $\mathcal{V}$, with $W$ an ancestor of $P$. Then for any axiom link $a$ depending on $W$ in $\mathcal{V}$, $a$ also depends on $P^{\perp}$ in $\mathcal{V}$.

**Proof.** There exist linkings $\lambda, \lambda' \in \mathcal{V}$ such that $W$ is the only $\&$ toggled by $\{\lambda; \lambda'\}$ and $a \in \lambda \backslash \lambda'$. We consider a linking $\lambda_{P^{\perp}}$ defined by taking an arbitrary $\&$-resolution of $\lambda$ where we choose the other premise for $P^{\perp}$ (and arbitrary premises for $\&$-vertices introduced this way): by (P1), there exists a unique linking on it. By Lemma 26, the additive resolutions of $\lambda$ and $\lambda_{P^{\perp}}$ (resp. $\lambda$ and $\lambda'$) differ exactly on ancestors of $P$ and $P^{\perp}$ (resp. $W$ and $W^{\perp}$). Thus, the additive resolutions of $\lambda'$ and $\lambda_{P^{\perp}}$ also differ exactly on ancestors of $P$ and $P^{\perp}$, for $W$ is an ancestor of $P$. In particular, $\{\lambda; \lambda_{P^{\perp}}\}$, as well as $\{\lambda'; \lambda_{P^{\perp}}\}$, toggles only $P^{\perp}$. If $a \in \lambda_{P^{\perp}}$, then $a$ depends on $P^{\perp}$ in $\{\lambda'; \lambda_{P^{\perp}}\}$. Otherwise, $a$ depends on $P^{\perp}$ in $\{\lambda; \lambda_{P^{\perp}}\}$. ◀

The key result to use distributivity is that a positive vertex “between” a leaf $l$ and a $\&$-vertex $W$ in the same tree prevents them from interacting, i.e. there is no jump $l \xrightarrow{j} W$.

**Lemma 28.** Let $l \xrightarrow{j} W$ be a jump edge in $\mathcal{V}$, with $l$ not an ancestor of $W$ and $l, W \in T(A^{\perp})$ (resp. $T(A)$). Denoting by $N$ the first common descendant of $l$ and $W$, there is no positive vertex in the path between $N$ and $W$ in $T(A^{\perp})$ (resp. $T(A)$).

**Proof.** Let $P$ be a vertex on the path between $N$ and $W$ in $T(A^{\perp})$. By Lemma 23, $N$ is a $\mathcal{Y}$-vertex. We prove by contradiction that $P$ can neither be a $\oplus$ nor a $\otimes$-vertex.

Suppose $P$ is a $\oplus$-vertex. By Lemma 27, $a$ depends on $P^{\perp}$, and so does $a^{\perp}$ through Lemma 25: there is a jump edge $l^{\perp} \xrightarrow{j} P^{\perp}$. Applying Lemma 23, the first common descendant of $l^{\perp}$ and $P^{\perp}$, which is $N^{\perp}$, is a $\mathcal{Y}$-vertex: a contradiction as it is a $\otimes$-vertex.

Assume now $P$ to be a $\otimes$-vertex. As there is a jump $l \xrightarrow{j} W$, there exist linkings $\lambda, \lambda' \in \mathcal{V}$ and a leaf $m$ of $B$ such that $W$ is the only $\&$ toggled by $\{\lambda; \lambda'\}$ and $a = (l, m) \in \lambda \backslash \lambda'$. For $P$ is a $\otimes$, there is a leaf $p$ which is an ancestor of $P$ in the additive resolution of $\lambda$, from a different
<figure><img src="image_12.png" /><figcaption>Figure 10 Switching cycle containing W if P is a ⊗-vertex in the proof of Lemma 28</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 11 Almost reduced composition ϑ of θ and θ' by cut over B in the proof of Theorem 29</figcaption></figure>

premise of P than W; it is used by a link $b = (p, q) \in \lambda^3$ (see Figure 10). Then the switching cycle $l \xrightarrow{j} W \to P \leftarrow p \xrightarrow{b} q \to * \leftarrow q^{\perp} \xrightarrow{b^{\perp}} p^{\perp} \to P^{\perp} \to N^{\perp} \leftarrow l^{\perp} \xrightarrow{a^{\perp}} m^{\perp} \to * \leftarrow m \xrightarrow{a} l$ (dashed in blue on Figure 10) belongs to $G_{\{\lambda; \lambda'\}}$. Contradiction: W, the only & toggled by $\{\lambda; \lambda'\}$, cannot be in any switching cycle of $G_{\{\lambda; \lambda'\}}$ by (P3). ◀

**▶ Theorem 29.** *Assuming $A^{\theta, \theta'} \cong B$ with A and B distributed, $\theta$ and $\theta'$ are bipartite ax-unique.*

**Proof.** We already know that $\theta$ and $\theta'$ are bipartite full thanks to Theorem 19. We reason by contradiction and assume w.l.o.g. that $\theta$ is not ax-unique: there exist a leaf $l$ of $A^{\perp}$ and two distinct leaves $l_0$ and $l_1$ of B with links $a = (l, l_0)$ and $b = (l, l_1)$ in $\theta$. We consider $\vartheta$ the almost reduced composition of $\theta$ and $\theta'$ over B, depicted on Figure 11. By Lemma 16, $a$ and $b$ are also links in $\vartheta$ (for the linkings they belong to in $\theta$ have matching linkings in $\theta'$, and we did not eliminate atomic cuts). Using Lemma 25, we have in $G_{\vartheta}$ a switching cycle $\omega = l \xrightarrow{a} l_0 \to * \leftarrow l_0^{\perp} \xrightarrow{a^{\perp}} l^{\perp} \xrightarrow{b^{\perp}} l_1^{\perp} \to * \leftarrow l_1 \xrightarrow{b} l$.

Let $\Lambda$ be a set of linkings given by Lemma 22 applied to $\omega$. As there are two distinct links on $l$ in $\omega \subseteq G_{\Lambda}$, $\Lambda$ contains at least two linkings. By (P3), there exists $W$ a & toggled by $\Lambda$ that is not in any switching cycle of $G_{\Lambda}$. By Lemma 22, $a, a^{\perp}, b$ or $b^{\perp}$ depends on $W$. So $a$ or $b$ depends on $W$ by Lemma 25; w.l.o.g. $a$ depends on $W$. The vertex $W$ belongs to either $T(A)$ or $T(A^{\perp})$: up to considering $a^{\perp}$ instead of $a$, $W$ is in $T(A^{\perp})$. Remark $l$ is not an ancestor of $W$: if it were, by symmetry assume it is a left-ancestor. Whence $a$ and $b$ belong to $\Lambda^W$, so $a^{\perp}$ and $b^{\perp}$ too (Lemma 25); thus $\omega \subseteq G_{\Lambda^W}$, contradicting Lemma 22. By Lemma 23, the first common descendant $N$ of $l$ and $W$ in $T(A^{\perp})$ is a $\mathcal{N}$. There is a $\otimes \oplus$ on the path between the $\mathcal{N}$ $N$ and its ancestor the $\& W$ in $T(A^{\perp})$, for there is no sub-formula of the shape $-(\&-)'$ in the distributed $A^{\perp}$. This contradicts Lemma 28. ◀

<footnote n="3">³ With $q \neq m$, as $a$ and $b$ are two distinct links in the same linking $\lambda$.</footnote>
## 3.4 Non-ambiguous formulas & Completeness for unit-free MALL

Once our study is restricted to bipartite *ax-unique* proof-nets, we can also restrict formulas.

**Definition 30 (Non-ambiguous formula).** A formula *A* is said non-ambiguous if each atom in *A* occurs at most once positive and once negative.

**Remark.** This means all leaves in *A* are distinct. If *A* is non-ambiguous, so is $A^{\perp}$.

For instance, $X \& X^{\perp}$ is non-ambiguous, whereas $(A \otimes B) \oplus (A \otimes C)$ is ambiguous. The reduction to non-ambiguous formulas requires to restrict to distributed formulas first: in $(A \otimes B) \oplus (A \otimes C) \simeq A \otimes (B \oplus C)$ we need the two occurrences of *A* to factorize. The two following results are a direct adaptation of Section 3 in [2].

**Corollary 31 (Reduction to distributed non-ambiguous formulas).** The set of couples of distributed formulas *A* and *B* such that $A \stackrel{\theta, \vartheta}{\simeq} B$ is the set of instances (by a substitution on atoms) of couples of distributed non-ambiguous formulas *A'* and *B'* such that $A'^{\rho', \vartheta'} \stackrel{\theta', \vartheta'}{\simeq} B'$.

**Corollary 32.** Let *A* and *B* be non-ambiguous formulas. If there exist bipartite proof-nets $\theta$ and $\vartheta$ of respective conclusions $A^{\perp}$, *B* and $B^{\perp}$, *A*, then $A \stackrel{\theta, \vartheta}{\simeq} B$.

We then prove the completeness of $\mathcal{E}^{\dagger}$ for unit-free MALL by reasoning as in Section 4 of [2] (with some more technicalities for we reorder not only $\mathfrak{S}$-vertices but also $\&$-vertices).

**Theorem 33 (Isomorphisms completeness for unit-free MALL).** Given *A* and *B* two unit-free MALL formulas, if $A \simeq B$, then $A =_{\mathcal{E}^{\dagger}} B$.

# 4 Completeness for MALL with units

We now consider full MALL, with units, and show how to reduce it to the unit-free case. We solve this addition purely in sequent calculus showing that, for distributed formulas, multiplicative and additive units can be replaced by fresh atoms.

A key property of proof-nets is to define a quotient of sequent calculus proofs up to rule commutations [11] (see Appendix A for rule commutations in MALL). Because no such notion of proof-nets exist with units, we are forced to stay in the sequent calculus, meaning that we have to deal with possible rule commutations. As a key example, cut-elimination in proof-nets is confluent and leads to a unique normal form. This is not true in the sequent calculus and we need to relate the different possible cut-free proofs obtained by cut-elimination.

**Theorem 34 (Confluence up to rule commutations).** If $\pi_1$ and $\pi_2$ are cut-free proofs obtained by cut-elimination from the same proof $\pi$, then $\pi_1$ and $\pi_2$ are equal up to rule commutations.

This result is not surprising but has not already been proved as far as we know for it is rather tedious to establish. It is an important general result about sequent calculus which we are convinced should hold for full linear logic. It can be lifted to $\beta\eta$-equality of proofs.

**Theorem 35.** Let $\pi$ and $\varpi$ be $\beta\eta$-equal MALL proofs. Then, letting $\pi'$ (resp. $\varpi'$) be a result of expanding all axioms and then eliminating all cuts in $\pi$ (resp. $\varpi$), $\pi'$ is equal to $\varpi'$ up to rule commutations.

After these general properties, let us move to the question of type isomorphisms. We need to analyse the behaviour of units in proofs equal to $\mathrm{id}_A$ up to rule commutations. We only do so for a *distributed* formula *A* as we have already seen it is enough in Section 3.3.
**Proposition 36.** Let $\pi$ be a proof equal, up to rule commutations, to $\text{id}_A$ with $A$ distributed. The $\top$-rules of $\pi$ are of the shape $\vdash\top,0\top$ (with $\top$ in $A$ being the dual of $0$ in $A^\perp$, or vice-versa) and $\bot$-rules and $1$-rules come by pairs separated with $\oplus_i$-rules only, called a $1/\oplus/\bot$-pattern: $$ \frac{\vdash\bot\bot}{\vdash\top F} \rho $$ where $\rho$ is a sequence of $\oplus_i$-rules (with $\bot$ in $A$ being the dual of $1$ in $A^\perp$, or vice-versa). Moreover, there are no sequent in $\pi$ of the shape $\vdash B \& C$.

**Proof.** The key idea is to find properties of $\text{id}_A$ preserved by all rule commutations and ensuring the properties described in the statement. For any sequent $S$ in the proof:

(1) the formulas of $S$ are distributed;

(2) if $\top$ is a formula of $S$, then $S = \vdash\top,0$;

(3) if $\bot$ is a formula of $S$, then $S = \vdash\bot,F$ with $F$ given by the following grammar $F := 1 \mid F \oplus D \mid D \oplus F$, where the distinguished $1$ is the dual of $\bot$ in $A^\perp$ if $\bot$ a sub-formula of $A$ (or vice-versa), $D$ is any formula, and the sub-proof of $\pi$ above $S$ is a sequence of $\oplus_i$ rules leading to the distinguished $1$;

(4) if $B \& C$ is a formula of $S$, then $S = \vdash B \& C, F$ with $F$ given by the following grammar $F := C^\perp \oplus B^\perp \mid F \oplus D \mid D \oplus F$, where the distinguished $C^\perp \oplus B^\perp$ is the dual of $B \& C$ in $A^\perp$ if $B \& C$ a sub-formula of $A$ (or vice-versa), $D$ is any formula, and in the sub-proof of $\pi$ above $S$ the $\oplus$-rules of the distinguished $C^\perp \oplus B^\perp$ are a $\oplus_2$-rule in the left-branch of the $\&$-rule of $B \& C$, and a $\oplus_1$-rule in its right branch;

(5) if $S$ contains several negative formulas or several positive formulas, then its negative formulas are $\mathfrak{S}$-formulas.

See Appendix D.2.

These properties are preserved by cut anti-reduction.

**Lemma 37.** If $A^{\pi, \pi'} \simeq B$ with $\pi$ and $\pi'$ cut-free then all $\top$-rules in $\pi$ and $\pi'$ are of the form $\vdash\top,0\top$ and all $\bot$-rules and $1$-rules belong to $1/\oplus/\bot$-patterns.

Moving each $\bot$-rule up to the associated $1$-rule (which can be done up to $\beta\eta$-equality) allows us to consider units as fresh atoms introduced by $ax$-rules and to apply Theorem 33.

**Theorem 38 (Isomorphisms completeness with units).** If $A \simeq B$ then $A =_\epsilon B$.

# 5 Star-autonomous categories with finite products

We prove here that the equational theory $\mathcal{E}$ (along $A \dashv B \simeq A^\perp \mathfrak{S} B$, De Morgan's laws and involutivity of negation) also corresponds to the isomorphisms present in all $\star$-autonomous categories with finite products. For the historical result of how linear logic can be seen as a category, see [15].

We establish this result from the one on MALL, first proving that MALL (with proofs considered up to $\beta\eta$-equality) defines a $\star$-autonomous category with finite products (Section 5.1). Then, we conclude using a semantic method (Section 5.2).

## 5.1 MALL as a star-autonomous category with finite products

The logic MALL, with proofs taken up to $\beta\eta$-equality, defines a $\star$-autonomous category with finite products, that we will call MALL. Indeed, we can define it as follows.
Objects of MALL are formulas of MALL, while its morphisms from A to B are proofs of $\vdash A^{\perp}, B$, considered up to $\beta\eta$-equality.<fnref n="4" /> One can check that a proof of MALL is an isomorphism if and only if, when seen as a morphism, it is an isomorphism in MALL.

We define a bifunctor $\otimes$ on MALL, associating to formulas (i.e. objects) A and B the formula $A \otimes B$ and to proofs (i.e. morphisms) $\pi_0$ and $\pi_1$ respectively of $\vdash A_0^{\perp}, B_0$ and $\vdash A_1^{\perp}, B_1$ the following proof of $\vdash (A_0 \otimes A_1)^{\perp}, B_0 \otimes B_1$:

$$ \frac{\frac{\pi_0}{\vdash A_0^{\perp}, B_0} \qquad \frac{\pi_1}{\vdash A_1^{\perp}, B_1}}{\frac{\vdash A_1^{\perp}, A_0^{\perp}, B_0 \otimes B_1}{\vdash A_1^{\perp}, \mathfrak{R} A_0^{\perp}, B_0 \otimes B_1}} \otimes \mathfrak{R} $$

One can check that (MALL, $\otimes$, 1, $\alpha$, $\lambda$, $\rho$, $\gamma$) forms a symmetric monoidal category, where 1 is the 1-formula, $\alpha$ are isomorphisms of MALL associated to $(A \otimes B) \otimes C \simeq A \otimes (B \otimes C)$ seen as a natural isomorphism of MALL, and similarly for $\lambda$ with $1 \otimes A \simeq A$, $\rho$ with $A \otimes 1 \simeq A$, and $\gamma$ with $A \otimes B \simeq B \otimes A$.

Furthermore, define $A \dashv B := A^{\perp} \mathfrak{R} B$ and $ev_{A,B}$ as the following morphism from $(A \dashv B) \otimes A$ to $B$ (i.e. a proof of $\vdash A^{\perp} \mathfrak{R} (B^{\perp} \otimes A), B$):

$$ \frac{\frac{\vdash B^{\perp}, B}{\vdash A^{\perp}, B^{\perp} \otimes A, B} ax \qquad \frac{\vdash A^{\perp}, A}{\vdash A^{\perp} \mathfrak{R} (B^{\perp} \otimes A), B} ax}{\vdash 1 \qquad \frac{\frac{\vdash A^{\perp}, A}{\vdash A^{\perp}, \perp, A} \perp \qquad \frac{\vdash A^{\perp}, \mathfrak{R} \perp, A}{\vdash A^{\perp} \mathfrak{R} \perp, A} \mathfrak{R}}{\vdash 1 \otimes (A^{\perp} \mathfrak{R} \perp), A} \otimes \mathfrak{R}} $$

It can be checked that MALL is a symmetric monoidal closed category with as exponential object $(A \dashv B, ev_{A,B})$ for objects A and B.

Moreover, one can also check that $\perp$ is a dualizing object for this category, making MALL a $\star$-autonomous category. This relies on the following morphism from $(A \dashv \perp) \dashv \perp$ to A (which is an inverse of the curryfication of $ev_{A,\perp}$):

$$ \frac{\frac{\overline{\vdash A^{\perp}, A}}{\vdash 1} ax}{\frac{\overline{\vdash A^{\perp}, \perp, A}}{\vdash 1 \otimes (A^{\perp} \mathfrak{R} \perp), A} \perp} \otimes \mathfrak{R} $$

Finally, $\top$ is a terminal object of MALL, and $A \& B$ is the product of objects A and B, with as projections $\pi_A$ and $\pi_B$ the following morphisms respectively from $A \& B$ to A and from $A \& B$ to $B$:

$$ \frac{\overline{\frac{\vdash A^{\perp}, A}{\vdash B^{\perp} \oplus A^{\perp}, A}} ax}{\vdash 2} \quad \text{and} \quad \frac{\overline{\frac{\vdash B^{\perp}, B}{\vdash B^{\perp} \oplus A^{\perp}, B}} ax}{\vdash 1} \oplus_1 \mathfrak{R} $$

Therefore, MALL is a $\star$-autonomous category with finite products [15].

## 5.2 Isomorphisms of star-autonomous categories with finite products

We take the same notations as in the previous section (& for product, ...). One can easily check that isomorphisms in a $\star$-autonomous category with finite products form a congruence (as all binary connectives define bifunctors), and that $\mathcal{E}$ is sound (i.e. that equations defining

<footnote n="4">⁴ We recall that $(\cdot)^{\perp}$ is defined by induction, making it an involution.</footnote>
<figure><img src="image_14.png" /></figure>

<figure><img src="image_15.png" /><figcaption>Table 2 De Morgan's isomorphisms</figcaption></figure>

$\mathcal{E}$ in Table 1 on Page 3 are isomorphisms in any $\star$-autonomous category with finite products). Moreover the isomorphisms of Table 2 (which are equalities in MALL) also hold in any $\star$-autonomous category with finite products.

Completeness follows by Theorem 38 (isomorphisms in MALL are exactly those given by $\mathcal{E}$) and from the fact that two objects definable in the language of $\star$-autonomous categories with finite products are equal in MALL if and only if they are related by the equational theory generated by Table 2. For example, one can deduce $(A \dashv \bot) \dashv \bot \simeq (A^\perp \dashv \bot)^\perp \dashv \bot \simeq (A^\perp \dashv \bot)^\perp \simeq 1 \otimes A^\perp \simeq A^\perp \simeq A$ (the last equation being derivable by induction on $A$). Henceforth, isomorphisms valid in all $\star$-autonomous categories with finite products are included in $\mathcal{E}$ enriched with Table 2.

**► Theorem 39 (Isomorphisms in $\star$-autonomous categories with finite products).** $\mathcal{E}$ enriched with Table 2 is a sound and complete equational theory for isomorphisms in $\star$-autonomous categories with finite products.

# 6 Conclusion

Extending the result of Balat and Di Cosmo in [2], we give an equational theory characterising type isomorphisms in multiplicative-additive linear logic with units as well as in $\star$-autonomous categories with finite products: the one described on Table 1 on Page 3 (together with Table 2 for $\star$-autonomous categories). Looking at the proof, we get as a sub-result that isomorphisms for ALL (resp. unit-free ALL) are given by the equational theory $\mathcal{E}$ (resp. $\mathcal{E}^\dagger$) restricted to ALL formulas (and more generally this applies to any fragment of MALL, thanks to the sub-formula property). Proof-nets were a major tool to prove completeness, as notions like fullness and $ax$-uniqueness are much harder to define and manipulate in sequent calculus. However, we could not use them for taking care of the (additive) units, because there is no known appropriate notion of proof-nets. We have thus been forced to develop (some parts of) the theory of cut-elimination, axiom-expansion and rule commutations for the sequent calculus of MALL with units.

The immediate question to address is the extension of our results to the characterization of type isomorphisms for full propositional linear logic, thus including the exponential connectives. This is clearly not immediate since the interaction between additive and exponential connectives is not well described in proof-nets.

A more general problem is the study of type retractions (where only one of the two compositions yields an identity) which is also much more difficult (see for example [13]). The question is mostly open in the case of linear logic. Even in multiplicative linear logic (where there is for example a retraction between $A$ and $(A \dashv A) \dashv A = (A \otimes A^\perp) \dashv A$ which is not an isomorphism, and where the associated proof-nets are not bipartite), no characterization is known. In the multiplicative-additive fragment, the problem looks even harder, with more retractions; for instance the one depicted on Figure 4, but there also is a retraction between $A$ and $A \oplus A$.
References

1 Michele Abrusci and Elena Maringelli. A new correctness criterion for cyclic proof nets. *Journal of Logic, Language and Information*, 7:449–459, 1998. doi:10.1023/A:1008354130493.

2 Vincent Balat and Roberto Di Cosmo. A linear logical view of linear type isomorphisms. In Jörg Flum and Mario Rodríguez-Artalejo, editors, *Computer Science Logic*, volume 1683 of Lecture Notes in Computer Science, pages 250–265. Springer, 1999.

3 Vincent Danos and Laurent Regnier. The structure of multiplicatives. *Archive for Mathematical Logic*, 28:181–203, 1989.

4 Roberto Di Cosmo. *Isomorphisms of Types*. Progress in Theoretical Computer Science. Birkhäuser, 1995.

5 Paolo Di Giamberardino. Jump from parallel to sequential proofs: Additives, 2011. https://hal.science/hal-00616386.

6 Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In *Proceedings of the seventeenth annual symposium on Logic In Computer Science*, pages 147–156, Copenhagen, July 2002. IEEE, IEEE Computer Society Press.

7 Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

8 Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, *Logic and Algebra*, volume 180 of Lecture Notes In Pure and Applied Mathematics, pages 97–124, New York, 1996. Marcel Dekker. doi:10.1201/9780203748671-4.

9 Willem Heijltjes and Dominic Hughes. Conflict nets: Efficient locally canonical MALL proof nets. In *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 437–446. ACM Press, July 2016. doi:10.1145/2933575.2934559.

10 Dominic Hughes and Rob van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. *ACM Transactions on Computational Logic*, 6(4):784–842, 2005. doi:10.1145/1094622.1094629.

11 Dominic Hughes and Rob van Glabbeek. MALL proof nets identify proofs modulo rule commutation, 2016. https://arxiv.org/abs/1609.04693.

12 Olivier Laurent. Classical isomorphisms of types. *Mathematical Structures in Computer Science*, 15(5):969–1004, October 2005.

13 Laurent Regnier and Pawel Urzyczyn. Retractions of types with many atoms, 2002. http://arxiv.org/abs/cs/0212005.

14 Mikael Rittri. Using types as search keys in function libraries. *Journal of Functional Programming*, 1(1):71–89, 1991.

15 Robert Seely. Linear logic, ⋆-autonomous categories and cofree coalgebras. *Contemporary mathematics*, 92, 1989.

16 Sergei Soloviev. The category of finite sets and cartesian closed categories. *Journal of Soviet Mathematics*, 22(3):1387–1400, 1983.
<table><tbody><tr><td>η - ⊗</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash A \otimes B, B^{\perp} \eta A^{\perp}}$</div><div style="padding-top: 1px;">$\overline{\vdash A \otimes B, B^{\perp} \eta A^{\perp}}$</div></div> ax</td><td>$\eta \to$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash A^{\perp}, A}$</div><div style="padding-top: 1px;">$\overline{\vdash B^{\perp}, B}$</div></div> ax<br><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash A \otimes B, A^{\perp}, B^{\perp}}$</div><div style="padding-top: 1px;">$\overline{\vdash A \otimes B, B^{\perp} \eta A^{\perp}}$</div></div> ax<br><div style="text-align: center;">$\eta \to$</div></td></tr><tr><td>& - ⊕</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash A \oplus B, B^{\perp} \& A^{\perp}}$</div><div style="padding-top: 1px;">$\overline{\vdash A \oplus B, B^{\perp} \& A^{\perp}}$</div></div> ax</td><td>$\eta \to$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash B, B^{\perp}}$</div><div style="padding-top: 1px;">$\overline{\vdash A \oplus B, B^{\perp}}$</div></div> ax<br><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\oplus_2$</div><div style="padding-top: 1px;">$\overline{\vdash A \oplus B, B^{\perp} \oplus_2}$</div></div> ax<br><div style="text-align: center;">$\oplus_1$</div><div style="text-align: center;">$\&$</div></td></tr><tr><td>⊥ - 1</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash 1, \perp}$</div><div style="padding-top: 1px;">$\overline{\vdash 1, \perp}$</div></div> ax</td><td>$\eta \to$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash 1}$</div><div style="padding-top: 1px;">$\overline{\vdash 1, \perp}$</div></div> 1<br><div style="text-align: center;">$\perp$</div></td></tr><tr><td>⊤ - 0</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash 0, \top}$</div><div style="padding-top: 1px;">$\overline{\vdash 0, \top}$</div></div> ax</td><td>$\eta \to$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 1px;">$\overline{\vdash 0, \top}$</div><div style="padding-top: 1px;">$\top$</div></div></td></tr></tbody></table>

<figure><img src="image_16.png" /><figcaption>Table 3 Axiom-expansion in the sequent calculus of MALL</figcaption></figure>

In appendix are first described transformations of proofs: axiom-expansion $\xrightarrow{\eta}$, cut-elimination $\xrightarrow{\beta}$ and rule commutations $=_{c}$ (Appendix A). Then come proofs of various sections of the paper: about reduction to axiom-expanded proofs (Appendix B), completeness for unit-free MALL (Appendix C) and for full MALL (Appendix D). Proofs are given in the order their results appear in the main part.

## A Transformations of sequent calculus proofs in MALL

* **Definition 40.** In the sequent calculus of MALL, we call axiom-expansion the rewriting system $\xrightarrow{\eta}$ described on Table 3.

* **Definition 41.** In the sequent calculus of MALL, we call cut-elimination the rewriting system $\xrightarrow{\beta}$ described on Tables 4 and 5 (up to commuting the two branches of a cut-rule).<fnref n="5" />

* **Definition 42.** In the sequent calculus of MALL, we call rule commutation the equational theory $=_{c}$ described on Tables 6 and 7. This corresponds to rule commutations in cut-free MALL; in particular, in a $\top - \otimes$ permutation we assume the created or erased sub-proof to be cut-free.

We denote the reflexive transitive closure of $\xrightarrow{\eta}$ (resp. $\xrightarrow{\beta}$, $=_{c}$) by $\xrightarrow{\eta^*}$ (resp. $\xrightarrow{\beta^*}$, $=_{c}^*$).

## B Proofs for the reduction to axiom-expanded proofs

This appendix contains proofs for the results stated in Section 2.3.

### B.1 Axiom-expansion is confluent and strongly normalizing

* **Proposition 43.** The relation $\xrightarrow{\eta}$ is confluent and strongly normalizing.

$$ \frac{\frac{\frac{\pi_1}{\vdash A, \Gamma} \quad \frac{\pi_2}{\vdash B, \Delta} \quad \frac{\pi_3}{\vdash B^{\perp}, A^{\perp}, \Sigma} \quad \frac{\pi_1}{\vdash A, \Gamma} \quad \frac{\pi_3}{\vdash B^{\perp}, A^{\perp}, \Sigma}}{\vdash A \otimes B, \Gamma, \Delta} \otimes \frac{\vdash B^{\perp} \eta A^{\perp}, \Sigma}}{\vdash \Gamma, \Delta, \Sigma} \eta \xrightarrow{\beta} \frac{\pi_2}{\vdash B, \Delta} \quad \frac{\pi_1}{\vdash A, \Gamma} \quad \frac{\pi_3}{\vdash B^{\perp}, \Gamma, \Sigma}}{\vdash \Gamma, \Delta, \Sigma} \text{ cut} $$

<footnote n="5">⁵ Another possible key case would be the following:</footnote>

<footnote>This case can be simulated with the given $\eta - \otimes$ key case and a cut-cut commutative case.</footnote>
<table><tbody><tr><td>ax</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">ax</div><div style="padding-top: 2px;">$\vdash A^{\perp}, A$</div></div><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\vdash A, \Gamma$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div></td></tr><tr><td>$\mathfrak{Y} - \otimes$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash B, \Delta$</div></div> $\otimes$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash B^{\perp}, A^{\perp}, \Sigma$</div></div> $\otimes$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\mathfrak{Y}$</div><div style="padding-top: 2px;">$\vdash B^{\perp}, \mathfrak{Y}^{\perp}, \Sigma$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash B, \Delta$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash B^{\perp}, A^{\perp}, \Sigma$</div></div> cut</td></tr><tr><td>& - $\otimes 1$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A_1, \Gamma$</div></div><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A_2, \Gamma$</div></div> &amp; <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A_2^{\perp}, \Delta$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A_1^{\perp} \oplus A_1^{\perp}, \Delta$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A_2, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A_2^{\perp}, \Delta$</div></div> cut</td></tr><tr><td>& - $\otimes 2$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A_1, \Gamma$</div></div><div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A_2, \Gamma$</div></div> &amp; <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A_1^{\perp}, \Delta$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A_1, \Gamma$</div></div> $\oplus 2$ cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A_1, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A_1^{\perp}, \Delta$</div></div> cut</td></tr><tr><td>$\perp - 1$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi$</div><div style="padding-top: 2px;">$\vdash \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash 1$</div></div> $\perp$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi$</div><div style="padding-top: 2px;">$\vdash \Gamma, \perp$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi$</div><div style="padding-top: 2px;">$\vdash \Gamma$</div></div></td></tr></tbody></table>

(No $\alpha \perp - 0$ key case as there are no rule for 0.)

<table><caption>Table 4 Cut-elimination in sequent calculus (key cases)</caption><tbody><tr><td>$\mathfrak{Y} - \text{cut}$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, C, \Gamma$</div></div> $\mathfrak{Y}$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> $\mathfrak{Y}$ cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, C, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash B, C, \Gamma, \Delta$</div></div> cut</td></tr><tr><td>$\otimes - \text{cut} - 1$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash C, \Delta$</div></div> $\otimes$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Sigma$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Sigma$</div></div> cut <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash C, \Delta$</div></div> $\otimes$</td></tr><tr><td>$\otimes - \text{cut} - 2$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, C, \Delta$</div></div> $\otimes$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Sigma$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, C, \Delta$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash C, \Delta, \Sigma$</div></div> cut</td></tr><tr><td>& - \text{cut}$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, C, \Gamma$</div></div> &amp; <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, C, \Gamma$</div></div> cut</td></tr><tr><td>$\oplus_i - \text{cut}$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B_i, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, B_1 \oplus B_2, \Gamma$</div></div> $\oplus_i$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B_i, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut</td></tr><tr><td>$\perp - \text{cut}$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A, \perp, \Gamma$</div></div> $\perp$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash \perp, \Gamma, \Delta$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut</td></tr><tr><td>$\top - \text{cut}$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, \top, \Gamma$</div></div> $\top$ <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Delta$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash \top, \Gamma, \Delta$</div></div> $\top$</td></tr><tr><td>cut - cut</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash B^{\perp}, \Delta$</div></div> cut <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Sigma$</div></div> cut</td><td>$\beta$</td><td>$\rightarrow$</td><td><div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_1$</div><div style="padding-top: 2px;">$\vdash A, B, \Gamma$</div></div> <div style="display: inline-block; vertical-align: middle; text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_3$</div><div style="padding-top: 2px;">$\vdash A^{\perp}, \Sigma$</div></div> cut <div style="text-align: center;"><div style="border-bottom: 1px solid black; padding-bottom: 2px;">$\pi_2$</div><div style="padding-top: 2px;">$\vdash B^{\perp}, \Delta$</div></div> cut</td></tr></tbody></table>

(No $ax - \text{cut}$ nor $1 - \text{cut}$ nor $0 - \text{cut}$ commutative cases as the $ax$ and $1$-rules have no context and there are no rule for 0.)

<caption>Table 5 Cut-elimination in sequent calculus (commutative cases)</caption>
<figure><img src="image_17.png" /><figcaption>Table 6 Rule commutations involving a unit rule</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Figure 12 Diagrams of Lemmas 44 (left and center) and 45 (right, ENF means in $\eta$-normal form)</figcaption></figure>

**Proof.** Strong normalization follows from the fact that a $\xrightarrow{\eta}$ step strictly decreases the sum of the sizes of the formulas on which an ax-rule is applied.

We use Newman's Lemma to deduce confluence from strong normalization and local confluence. Observe that two steps $\varpi \leftarrow \pi \xrightarrow{\eta} \phi$ always commute or cancel each other, i.e. $\varpi = \phi$ or there exists $\varphi$ such that $\varpi \xrightarrow{\eta} \varphi \leftarrow \eta \xrightarrow{\eta} \phi$; hence local confluence of $\xrightarrow{\eta}$.

## B.2 Proof of Proposition 4

We set $a(\pi \xrightarrow{\beta^*} \varpi)$ the multiset of the sizes of the formulas in the ax key cases of these $\xrightarrow{\beta}$ reductions. By $\xrightarrow{\beta^n}$ we mean a sequence of $n \xrightarrow{\beta}$ steps, and similarly for $\xrightarrow{\eta}$.

**Lemma 44.** Let $\pi, \varpi$ and $\phi$ be MALL proofs such that $\varpi \xrightarrow{\beta} \pi \xrightarrow{\eta} \phi$. Then there exists $\varphi$ such that $\varpi \xrightarrow{\eta^*} \varphi \leftarrow \beta \xrightarrow{\beta} \phi$ or there exist $\varphi_1$ and $\varphi_2$ such that $\phi \xrightarrow{\eta^*} \varphi_1 \xrightarrow{\beta^*} \varphi_2 \xleftarrow{\eta^*} \varpi$. Furthermore, $a(\phi \xrightarrow{\beta} \varphi) = a(\pi \xrightarrow{\beta} \varpi)$ in the first case and $a(\varphi_1 \xrightarrow{\beta^*} \varphi_2) < a(\pi \xrightarrow{\beta} \varpi)$ in the second one. (See Figure 12 for diagrams corresponding to these cases.)

**Proof.** Call $r$ the ax-rule that $\pi \xrightarrow{\eta} \phi$ expands, and $A$ its formula. If the cut-elimination step is not an ax key case using $r$, then the two steps commute and there exists $\varphi$ such that $\phi \xrightarrow{\beta} \varphi$ and $\varpi \xrightarrow{\eta} \varphi$ (or $\varpi \xrightarrow{\eta} \cdot \xrightarrow{\eta} \varphi$ if $r$ belongs to a sub-proof duplicated by the $\xrightarrow{\beta}$ step, or $\varpi = \varphi$ if it belongs to a sub-proof erased by the $\xrightarrow{\beta}$ step). In particular, $a(\phi \xrightarrow{\beta} \varphi) = a(\pi \xrightarrow{\beta} \varpi)$ for they use the same rules.
Otherwise, the cut-elimination step is an *ax* key case on *r*, with a *cut-rule* we call *c* and a sub-proof *ρ* in the other branch of *c* that the one leading to *r*. Starting from *φ*, consider the rules introducing *A*<sup>⊥</sup> in (all slices of) *ρ*. If any of them are *ax-rules*, then these are necessarily on the formula *A*; expand those *ax-rules*, in both *φ* and *ω* (keep the same name for proofs *π*, *ω* and *ρ* by abuse). Then, in *φ*, commute the *cut-rule* *c* with rules of *ρ* until reaching the rules introducing *A*<sup>⊥</sup> in all slices (which are rules of the main connective of *A* or ⊤-rules). Applying the corresponding key cases or ⊤-cut commutative case (first commuting with a rule of the expanded axiom *r* if *A* is a positive formula), then the *ax* key cases on strict sub-formulas of *A* yields *ω*. During these *ax* key cases, we cut on sub-formulas of *A*, so on formulas of a strictly smaller size. Therefore $\phi \stackrel{\eta^*}{\longrightarrow} \beta^* \longrightarrow \eta^* \omega$, with $a(\beta^* \longrightarrow \cdot) < a(\pi \longrightarrow \omega)$. ◀

► **Remark.** Cut-elimination $\stackrel{\beta}{\longrightarrow}$ preserves being in $\eta$-normal form.

**Lemma 45.** Let $\pi, \omega$ and $\phi$ be proofs such that $\omega \stackrel{\eta^*}{\longrightarrow} \pi \stackrel{\beta^*}{\longrightarrow} \phi$, with $\omega$ an $\eta$-normal proof. There exists an $\eta$-normal proof $\varphi$ such that $\omega \stackrel{\beta^*}{\longrightarrow} \varphi \stackrel{\eta^*}{\longrightarrow} \phi$. This is depicted on Figure 12.

**Proof.** We have $\omega \stackrel{\eta^m}{\longleftarrow} \pi \stackrel{\beta^n}{\longrightarrow} \phi$. We reason by induction on the lexicographic order of the triple $(a(\pi \stackrel{\beta^*}{\longrightarrow} \phi), n, m)$. If $n=0$ or $m=0$, then the result trivially holds.

Consider the case $n+1$ and $m+1$. Therefore, $\omega \stackrel{\eta^m}{\longleftarrow} \iota \stackrel{\eta}{\longrightarrow} \pi \stackrel{\beta}{\longrightarrow} \kappa \stackrel{\beta^n}{\longrightarrow} \phi$. We apply Lemma 44 on $\iota \stackrel{\eta}{\longrightarrow} \pi \stackrel{\beta}{\longrightarrow} \kappa$, yielding $\varphi$ such that $\iota \stackrel{\beta}{\longrightarrow} \varphi \stackrel{\eta^*}{\longrightarrow} \phi$ with $a(\iota \stackrel{\beta}{\longrightarrow} \varphi) = a(\pi \stackrel{\beta}{\longrightarrow} \kappa)$ or $\varphi_1$ and $\varphi_2$ such that $\iota \stackrel{\eta^*}{\longrightarrow} \varphi_1 \stackrel{\beta^*}{\longrightarrow} \varphi_2 \stackrel{\eta^*}{\longrightarrow} \kappa$ with $a(\varphi_1 \stackrel{\beta^*}{\longrightarrow} \varphi_2) < a(\pi \stackrel{\beta}{\longrightarrow} \kappa)$. Both of these cases, and the reasonings we will apply, are illustrated on the diagrams of Figure 13.

Assume to be in the first case. Applying the induction hypothesis on $\omega \stackrel{\eta^m}{\longleftarrow} \iota \stackrel{\beta}{\longrightarrow} \varphi$, with $\omega$ in $\eta$-normal form, $a(\iota \stackrel{\beta}{\longrightarrow} \varphi) = a(\pi \stackrel{\beta}{\longrightarrow} \kappa) \le a(\pi \stackrel{\beta^*}{\longrightarrow} \phi)$, $1 \le n+1$ and $m<m+1$, there exists an $\eta$-normal proof $\nu$ such that $\omega \stackrel{\beta^*}{\longrightarrow} \nu \stackrel{\eta^*}{\longrightarrow} \varphi$. We now apply the induction hypothesis on $\nu \stackrel{\eta^*}{\longrightarrow} \varphi \stackrel{\eta^*}{\longrightarrow} \kappa \stackrel{\beta^n}{\longrightarrow} \phi$, with $\nu$ in $\eta$-normal form, $a(\kappa \stackrel{\beta^n}{\longrightarrow} \phi) \le a(\pi \stackrel{\beta^*}{\longrightarrow} \phi)$ and $n < n+1$. We obtain an $\eta$-normal proof $\mu$ such that $\nu \stackrel{\beta^*}{\longrightarrow} \mu \stackrel{\eta^*}{\longrightarrow} \phi$. This concludes the first case.

Consider the second case. Using the confluence of $\stackrel{n}{\longrightarrow}$ on $\omega \stackrel{\eta^m}{\longleftarrow} \iota \stackrel{\eta^*}{\longrightarrow} \varphi_1$ (Proposition 43), with $\omega$ in $\eta$-normal form, yields $\omega \stackrel{\eta^*}{\longrightarrow} \varphi_1$. We then apply the induction hypothesis on $\omega \stackrel{\eta^*}{\longrightarrow} \varphi_1 \stackrel{\beta^*}{\longrightarrow} \varphi_2$, with $\omega$ in $\eta$-normal form and $a(\varphi_1 \stackrel{\beta^*}{\longrightarrow} \varphi_2) < a(\pi \stackrel{\beta^*}{\longrightarrow} \phi)$. This yields an $\eta$-normal proof $\nu$ such that $\omega \stackrel{\beta^*}{\longrightarrow} \nu \stackrel{\eta^*}{\longrightarrow} \varphi_2$. We use the induction hypothesis again, this time on $\nu \stackrel{\eta^*}{\longrightarrow} \varphi_2 \stackrel{\eta^*}{\longrightarrow} \kappa \stackrel{\beta^n}{\longrightarrow} \phi$, with $\nu$ in $\eta$-normal form, $a(\kappa \stackrel{\beta^n}{\longrightarrow} \phi) \le a(\pi \stackrel{\beta^*}{\longrightarrow} \phi)$ and $n < n+1$. We obtain an $\eta$-normal proof $\mu$ with $\nu \stackrel{\beta^*}{\longrightarrow} \mu \stackrel{\eta^*}{\longrightarrow} \phi$, solving the second case. ◀

**Proposition 4 (Reduction to axiom-expanded proofs).** Let $\pi$ and $\omega$ be MALL proofs such that $\pi =_{\beta\eta} \omega$. Then $\eta(\pi) =_{\beta} \eta(\omega)$ with, in this sequence, only proofs in $\eta$-normal form.

**Proof.** We reason by induction on the length of the sequence $\pi =_{\beta\eta} \omega$. If it is of null length, then $\pi = \omega$ and $\eta(\pi) = \eta(\omega)$. Otherwise, we have a proof $\phi$ such that $\pi - \phi =_{\beta\eta} \omega$ with $\phi \in \{\stackrel{\beta}{\longrightarrow}; \stackrel{\eta^*}{\longrightarrow}; \stackrel{\eta}{\longrightarrow}\}$. By induction hypothesis, $\eta(\phi) =_{\beta} \eta(\omega)$ using only proofs in $\eta$-normal form. We distinguish cases according to $\pi - \phi$.

If $\pi \stackrel{\beta}{\longrightarrow} \phi$, then as $\eta(\pi) \stackrel{\eta^*}{\longrightarrow} \pi$ we can apply Lemma 45 to obtain an $\eta$-normal proof $\varphi$ such that $\eta(\pi) \stackrel{\beta^*}{\longrightarrow} \varphi \stackrel{\eta^*}{\longrightarrow} \phi$. Thus, $\varphi = \eta(\phi)$, so $\eta(\pi) \stackrel{\beta^*}{\longrightarrow} \eta(\phi) =_{\beta} \eta(\omega)$ and the result holds.

Similarly, if $\pi \stackrel{\beta}{\longrightarrow} \phi$ then, as $\phi \stackrel{\eta^*}{\longrightarrow} \eta(\phi)$, there exists an $\eta$-normal proof $\varphi$ such that $\pi \stackrel{\eta^*}{\longrightarrow} \varphi \stackrel{\beta^*}{\longrightarrow} \eta(\phi)$ (Lemma 45). Thus $\varphi = \eta(\pi)$, and $\eta(\pi) \stackrel{\beta^*}{\longrightarrow} \eta(\phi) =_{\beta} \eta(\omega)$.

Finally, if $\pi \stackrel{\eta}{\longrightarrow} \phi$ or $\pi \stackrel{\eta^*}{\longrightarrow} \phi$, then $\eta(\pi) = \eta(\varphi) =_{\beta} \eta(\omega)$ and the conclusion follows. ◀
<figure><img src="image_19.png" /><figcaption>■ **Figure 13** Diagrams of the cases of the proof of Lemma 45 (ENF means in $\eta$-normal form)
In blue are uses of Lemma 44, in green of confluence of $\xrightarrow{\eta}$ and in red of the induction hypothesis.</figcaption></figure>

### C Proofs for the completeness for unit-free MALL

This appendix contains proofs of results stated in Section 3 and leading to the proof of completeness for unit-free MALL. All the sequent calculus proofs we consider in this section have expanded axioms.

#### C.1 Proof of the Simulation Theorem (Theorem 12)

**► Definition 46 (<$).** Let $\theta$ and $\vartheta$ be MALL proof-nets. We denote $\theta \triangleleft \vartheta$ if there exists a $*$-vertex $C$ in $\theta$ such that the syntax forest of $\vartheta$ is the syntax forest of $\theta$ where the syntax tree of $C$ is duplicated into the syntax trees of $C_0$ and $C_1$ (which are different occurrences of $C$), $\theta = \theta_0 \sqcup \theta_1^6$ and $\vartheta = \vartheta_0 \sqcup \vartheta_1$, with $\vartheta_i = \theta_i$ up to assimilating $C_i$ with $C$ (for $i \in \{0; 1\}$).

**► Lemma 47 (Simulation - $\beta$).** Let $\pi$ and $\varpi$ be unit-free MALL proof trees such that $\pi \xrightarrow{\beta} \varpi$. We have $R(\pi) = R(\varpi)$, $R(\pi) \xrightarrow{\beta} R(\varpi)$ or $R(\pi) \triangleleft R(\varpi)$.

**Proof.** We reason by cases according to the step $\pi \xrightarrow{\beta} \varpi$. Recall that we desequentialize by separating all cuts, and use the notations for steps from Definition 7. If $\pi \xrightarrow{\beta} \varpi$ is an $ax$ (resp. $\mathcal{Y} \to \otimes$, $\& \to \oplus$) key case, then using a step (a) (resp. (b), (c)), $R(\pi) \xrightarrow{\beta} R(\varpi)$. If it is a $\mathcal{Y} \to$ cut, $\otimes \to$ cut - 1, $\oplus_1 \to$ cut or $\oplus_2 \to$ cut commutative case, then $R(\pi) = R(\varpi)$. Finally, in a $\& \to$ cut commutative case, we duplicate the cut-rule: $R(\pi) \triangleleft R(\varpi)$. $\quad$

**► Lemma 48 ($\triangleleft \subseteq =_\beta$).** Let $\theta$ and $\theta'$ be proof-nets such that $\theta \triangleleft \theta'$. Then $\theta =_\beta \theta'$.

**Proof.** By Definition 46 of $\triangleleft$, there exists a $*$-vertex $C$ in $\theta$, with $\theta = \theta_0 \sqcup \theta_1$, such that $\theta'$ is $\theta$ where the syntax tree of $C$ is duplicated into $C_0$ and $C_1$, and linkings in $\theta_0$ (respectively $\theta_1$) use $C_0$ (respectively $C_1$) as $C$.

We reason by induction on the size of the formula $A$ of $C$ (and also $C_0$ and $C_1$); w.l.o.g. $A$ is positive. Applying a step of cut-elimination on $C$ in $\theta$ yields a proof-net $\Theta$. On the other hand, a step of cut-elimination on $C_0$ and $C_1$ in $\theta'$ yields $\Theta'$. If $A$ is an atom, then we applied step (a), and we find $\Theta = \Theta'$.

If $A$ is a $\otimes$-formula, i.e. $A = A_0 \otimes A_1$, then we applied step (b) and produced cuts $A_0 * A_0^\perp$ and $A_1 * A_1^\perp$ in $\Theta$, and two occurrences of these cuts in $\Theta'$. Thus, $\Theta \triangleleft \Xi \triangleleft \Theta'$ with $\Xi$ the

<footnote n="6">⁶ The symbol $\sqcup$ means a union $\cup$ which happens to be between disjoint sets.</footnote>
proof-net $\Theta$ where the cut on $A_0$ is duplicated. By induction hypothesis, $\Theta =_{\beta} \Xi =_{\beta} \Theta'$. It follows $\theta =_{\beta} \theta'$ as $\theta \xrightarrow{\beta} \Theta =_{\beta} \Theta' \leftarrow^{\beta} \cdot \leftarrow^{\beta} \theta'$.

Finally, if $A$ is a $\oplus$-formula with $A = A_0 \oplus A_1$, then we used step (c), producing cuts $A_0 * A_0^\perp$ and $A_1 * A_1^\perp$ in $\Theta$, and two occurrences of these cuts in $\Theta'$. Remark that inconsistent linkings in $\theta'$ for these steps are exactly those of $\theta$, and therefore the same cuts are garbage collected. Whence, $\Theta \triangleleft \cdot \triangleleft \Theta'$, $\Theta \triangleleft \Theta'$ or $\Theta = \Theta'$ (according to the number of cuts garbage collected). In all cases, using the induction hypothesis we conclude $\theta =_{\beta} \theta'$.

◀

**Remark.** Another proof of Lemma 48, using the Turbo Cut-elimination procedure and no induction, is possible. We use the Turbo Cut-elimination procedure on $C$ in $\theta$, yielding a proof-net $\Theta$; we also use it in $\theta'$ on $C_0$ then $C_1$, yielding $\Theta'$. Whence, $\theta \xrightarrow{\beta^*} \Theta$ and $\Theta' \leftarrow^{\beta^*} \theta'$. It stays to prove that $\Theta = \Theta'$. Remark that $\Theta$ and $\Theta'$ can only differ by their linkings, for they have the same syntax forest. Notice that a linking in $\theta_i$, $i \in \{0; 1\}$, matches for $C$ in $\theta$ if and only if it matches for $C_i$ in $\theta'$ (because this linking uses $C_i$ as $C$). Thence, the same linkings stay in $\Theta$ and $\Theta'$, and $\Theta = \Theta'$ follows.

**Theorem 12 (Simulation Theorem).** Let $\pi$ and $\varpi$ be unit-free MALL proof trees (with expanded axioms). If $\pi =_{\beta} \varpi$, then $R(\pi) =_{\beta} R(\varpi)$.

*Proof.* This is a corollary of Lemmas 47 and 48.

◀

## C.2 Proof of the Reduction to proof-net Theorem (Theorem 13)

We call $\mathcal{B}(\theta)$ the $\beta$-normal form of the proof-net $\theta$, with all cuts eliminated.

**Lemma 49.** Let $\pi, \varpi$ and $\rho$ be unit-free MALL proof trees of respective sequents $\vdash A, \Gamma$, $\vdash A^\perp, \Delta$ and $\vdash \Gamma, \Delta$. Assume $\pi \stackrel{A}{\rightleftharpoons} \varpi =_{\beta} \rho$. Then $\mathcal{B}(R(\pi)) \stackrel{A}{\rightleftharpoons} \mathcal{B}(R(\varpi))$ reduces, after fully eliminating the cut on $A$, to $\mathcal{B}(R(\rho))$.

*Proof.* By the Simulation Theorem (Theorem 12), $R(\pi \stackrel{A}{\rightleftharpoons} \varpi) =_{\beta} R(\rho)$. By definition of $R$ (Section 3.1), $R(\pi \stackrel{A}{\rightleftharpoons} \varpi) = R(\pi) \stackrel{A}{\rightleftharpoons} R(\varpi)$, so by Theorem 9 $\mathcal{B}(R(\pi) \stackrel{A}{\rightleftharpoons} R(\varpi)) = \mathcal{B}(R(\rho))$. Moreover, by confluence of cut-elimination (Theorem 9), $\mathcal{B}(R(\pi) \stackrel{A}{\rightleftharpoons} R(\varpi))$ can be obtained by taking the $\beta$-normal forms of $R(\pi)$ and $R(\varpi)$, composing them over $A$ and reducing this cut. In other words, $\mathcal{B}(R(\pi) \stackrel{A}{\rightleftharpoons} R(\varpi)) = \mathcal{B}(\mathcal{B}(R(\pi)) \stackrel{A}{\rightleftharpoons} \mathcal{B}(R(\varpi)))$, and the result follows.

◀

**Theorem 13 (Type isomorphisms in proof-nets).** Let $A$ and $B$ be two unit-free MALL formulas. If $A \simeq B$ then there exist two proof-nets $\theta$ and $\vartheta$ such that $A^{\theta, \vartheta} \cong B$.

*Proof.* By Definition 1 of an isomorphism and Proposition 4, there exist unit-free MALL proofs $\pi$ and $\varpi$, respectively of $\vdash A^\perp, B$ and $\vdash B^\perp, A$, such that $\pi \stackrel{B}{\rightleftharpoons} \varpi =_{\beta} \text{id}_A$ and $\varpi \stackrel{A}{\rightleftharpoons} \pi =_{\beta} \text{id}_B$. By Lemma 49 and as $R(\text{id}_A)$ is cut-free, $\mathcal{B}(\mathcal{B}(R(\pi)) \stackrel{B}{\rightleftharpoons} \mathcal{B}(R(\varpi))) = \mathcal{B}(R(\text{id}_A)) = R(\text{id}_A)$. Similarly, $\mathcal{B}(\mathcal{B}(R(\varpi)) \stackrel{A}{\rightleftharpoons} \mathcal{B}(R(\pi))) = R(\text{id}_B)$. Thus, there exist cut-free proof-nets $\theta := \mathcal{B}(R(\pi))$ and $\vartheta := \mathcal{B}(R(\varpi))$ whose composition over $B$ (resp. $A$) yields after cut-elimination the identity proof-net of $A$ (resp. $B$).

◀

## C.3 Proofs of the properties of identity proof-nets from Proposition 15

We prove each result separately.

**Lemma 50.** The axiom links of an identity proof-net are exactly the $(l, l^\perp)$, for any leaf $l$.

*Proof.* By induction on the formula (see Figure 3 on Page 8).

◀
**Corollary 51.** An identity proof-net is bipartite ax-unique.

**Proof.** This follows from Lemma 50.

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

**Lemma 52.** Let $\lambda$ be a linking of an identity proof-net and $V$ an additive vertex in its additive resolution. Then $V^{\perp}$ is also inside with, as premise kept, the dual premise of the one kept for $V$.

**Proof.** Assume w.l.o.g. that the left premise of $V$ is kept in $\lambda$. There is a left-ancestor $l$ of $V$ in the additive resolution of $\lambda$, hence with a link $a \in \lambda$ on it. By Lemma 50, $a = (l, l^{\perp})$. As $l^{\perp}$ is a right-ancestor of $V^{\perp}$, the conclusion follows.

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

**Lemma 53.** In the identity proof-net of $A$, exactly one linking is on any given additive resolution of the conclusion $A$.

**Proof.** Consider such an additive resolution $R$. There is an associated $\&$-resolution $R'$ of $A^{\perp}$, $A$ by taking the choices of premise of $R$ on $A$ and, for a $\&$-vertex $W$ of $A^{\perp}$, taking the dual premise chosen in $R$ for $W^{\perp}$. By Lemma 52, a linking $\lambda$ is on $R$ if and only if it is on $R'$. Meanwhile, by (P1) there is a unique linking $\lambda$ on $R'$; thus the same holds on $R$. ◀

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

### C.4 Proof of Lemma 18

**Lemma 18.** Assume $\theta$ and $\theta'$ are cut-free proof-nets of respective conclusions $A^{\perp}$, $B$ and $B^{\perp}$, $A$, and that their composition over $B$ yields the identity proof-net of $A$. Then any leaf of $A^{\perp}$ (resp. $A$) has (at least) one axiom link on it in $\theta$ (resp. $\theta'$).

**Proof.** Towards a contradiction, assume w.l.o.g. a leaf $l$ of $A^{\perp}$ has no link on it in $\theta$. Then, the composition over $B$ of $\theta$ and $\theta'$ has no link on $l$ either. And reducing cuts cannot create links using $l$, for it only takes links $(l, m)$ and $(m, n)$ to merge them into $(l, m)$. However, the identity proof-net of $A$ is ax-unique by Proposition 15(i), thence full: contradiction. ◀

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

### C.5 Proof of Proposition 21

**Proposition 21.** If $\mathcal{E}$ is complete for isomorphisms between distributed formulas, then it is complete for isomorphisms between arbitrary formulas.

**Proof.** The following rewriting system is strongly normalizing, with as normal forms distributed formulas, and each rule corresponds to a valid equality in the theory $\mathcal{E}$ (see Table 1):

<table><thead><tr><th>A &otimes; (B &oplus; C)<br>(A &oplus; B) &otimes; C</th><th>&rarr;</th><th>(A &otimes; B) &oplus; (A &otimes; C)<br>(A &otimes; C) &oplus; (B &otimes; C)</th><th>(C &amp; B) &not; A<br>C &not; (B &amp; A)</th><th>&rarr;</th><th>(C &not; A) &amp; (B &not; A)<br>(C &not; B) &amp; (C &not; A)</th></tr></thead><tbody><tr><td>A &otimes; 1 &rarr; A</td><td></td><td>1 &otimes; A &rarr; A</td><td>A &not; &perp; &rarr; A</td><td></td><td>&perp; &not; A &rarr; A</td></tr><tr><td>A &oplus; 0 &rarr; A</td><td></td><td>0 &oplus; A &rarr; A</td><td>A &amp; &top; &rarr; A</td><td></td><td>&top; &amp; A &rarr; A</td></tr><tr><td>A &otimes; 0 &rarr; 0</td><td></td><td>0 &otimes; A &rarr; 0</td><td>A &not; &top; &rarr; &top;</td><td></td><td>&top; &not; A &rarr; &top;</td></tr></tbody></table>

Consider an isomorphism $A \simeq B$ between two arbitrary formulas $A$ and $B$. Let $A_d$ and $B_d$ be associated distributed formulas, obtained as normal forms of the above rewriting system. As this rewriting system is included in $\mathcal{E}$, we have $A =_{\mathcal{E}} A_d$ and $B =_{\mathcal{E}} B_d$.

By soundness of $\mathcal{E}$ (Theorem 3) and as linear isomorphism is a congruence, we deduce $A_d \simeq A \simeq B \simeq B_d$. The completeness hypothesis on $\mathcal{E}$ for distributed formulas yields $A_d =_{\mathcal{E}} B_d$, and thus $A =_{\mathcal{E}} A_d =_{\mathcal{E}} B_d =_{\mathcal{E}} B$. ◀

<figure><img src="image_24.png" /></figure>
## C.6 Proof of Lemma 22

**Lemma 22 (Lemma 4.32 in [10], adapted).** Let $\omega$ be a jump-free switching cycle in a proof-net $\theta$. There exists a subset of linkings $\Lambda \subseteq \theta$ such that $\omega \subseteq \mathcal{G}_{\Lambda}$, $\omega \not\subseteq \mathcal{G}_{\Lambda w}$ and for any $\&$-vertex $W$ toggled by $\Lambda$, there exists an axiom link $a \in \omega$ depending on $W$ in $\Lambda$.

**Proof.** The proof of this lemma uses some facts from [10] reproduced verbatim here. For $\Lambda$ a set of linkings and $W$ a $\&$-vertex, $\Lambda^W$ denote the set of all linkings in $\Lambda$ whose additive resolution does not contain the right argument of $W$. Write $\lambda \stackrel{W}{=} \lambda'$ if linkings $\lambda, \lambda' \in \theta$ are either equal or $W$ is the only $\&$ toggled by $\{\lambda, \lambda'\}$. A subset $\Lambda$ of a proof-net $\theta$ is saturated if any strictly larger subset toggles more $\&$ than $\Lambda$. It is straightforward to check that:

(S1) If $\Lambda$ is saturated and toggles $W$, then $\Lambda^W$ is saturated.

(S2) If $\Lambda$ is saturated and toggles $W$ and $\lambda \in \Lambda$, then $\lambda \stackrel{W}{=} \lambda_W$ for some $\lambda_W \in \Lambda^W$.

Let us now prove our lemma. Take $\Lambda$ a minimal saturated subset of $\theta$ with $\mathcal{G}_{\Lambda}$ containing $\omega$. Since $\Lambda$ is minimal, $\omega \not\subseteq \mathcal{G}_{\Lambda w}$ (using (S1)), so some edge $e$ of $\omega$ is in $\mathcal{G}_{\Lambda}$ but not in $\mathcal{G}_{\Lambda w}$. We claim that, without loss of generality, $e$ is an axiom link. If it is indeed the case, then $e \in \lambda \in \Lambda$ and $e \notin \lambda_W$ for $e \notin \Lambda^W$, so $e$ depends on $W$ in $\Lambda$ (using (S2)). We now prove our claim by eliminating other possibilities step by step.

Without loss of generality, $e$ is an edge from a leaf $l$ to some $X$, because for any other edge $Y \to X$ in $\omega$ we have $l \to Z_1 \to \dots \to Z_n = Y \to X$ in $\omega$ for some leaf $l$, and $Y \to X$ is in $\mathcal{G}_{\Lambda w}$ whenever $l \to Z_1$ is in $\mathcal{G}_{\Lambda w}$.

Still without loss of generality, $e$ is not an edge in a syntax tree. Indeed, in such a case $e \notin \mathcal{G}_{\Lambda w}$ implies $l \notin \mathcal{G}_{\Lambda w}$. As $e$ belongs to the switching cycle $\omega$, let us look at the other edge in this cycle with endpoint $l$, say $e'$. As $l \notin \mathcal{G}_{\Lambda w}$, we also have $e' \notin \mathcal{G}_{\Lambda w}$. Remark that $e'$ cannot be an edge in a syntax tree, for only one such edge has for endpoint the leaf $l$, namely $e$. We can replace $e$ with $e'$ to assume $e$ is not an edge in a syntax tree.

As $\omega$ is jump-free, $e$ cannot be a jump edge. The sole possibility is $e$ being a link.

## C.7 Proof of Lemma 26

**Lemma 26.** Let $\lambda$ be a linking of $\vartheta$, and $V$ an additive vertex in its additive resolution. Then $V^{\perp}$ is also inside, with as premise kept the dual premise of the one kept for $V$.

**Proof.** Assume w.l.o.g. that the left premise of $V$ is kept in $\lambda$. There is a left-ancestor $l$ of $V$ in the additive resolution of $\lambda$, hence with a link $a \in \lambda$ on it. By Lemma 25, we have $a^{\perp} \in \lambda$, using $l^{\perp}$. As $l^{\perp}$ is a right-ancestor of $V^{\perp}$, the conclusion follows.

## C.8 Proof of Corollary 31

This proof follows very closely the one for MLL of Balat & Di Cosmo (Section 3 in [2]).

In the following, we will call *substitution* the usual operation $[A_1/X_1, \dots, A_n/X_n]$ of replacement of the propositional atoms $X_i$ of a formula by the formulas $A_i$. We will consider substitutions extended to proof-nets, i.e. if $\sigma$ is a substitution and $\theta$ a proof-net, $\sigma(\theta)$ will be the proof-net obtained from $\theta$ by replacing all formulas $F_j$ appearing in it by $\sigma(F_j)$. We will also use a more general notion, *renaming*, that may replace different occurrences of the same atom by different formulas in a proof-net, i.e. substitute on leaves instead of atoms.

**Definition 54 (Renaming).** An application $\alpha$ from the set of leaves of a proof-net $\theta$ to a set of atoms is a renaming if $\alpha(\theta)$, the graph obtained by substitution of each label of a leaf $l$ of $\theta$ by $\alpha(l)$, is a proof-net.
Remark that if $\theta$ is bipartite ax-unique, then the definition of $\alpha$ only on leaves in one conclusion of $\theta$ is sufficient to define a renaming $\alpha$ on $\theta$. This is because every leaf of the other conclusion is linked to exactly one leaf in this conclusion, and no leaves in a given conclusion are linked together. Note also that if the conclusions of $\theta$ are ambiguous formulas, then two different occurrences of the same atom can be renamed differently, unlike what happens in the case of substitutions.

**Theorem 55 (Renaming preserves isomorphisms).** For $A$ and $B$ distributed formulas, assume $A \stackrel{\theta, \theta'}{\cong} B$, with $\theta$ and $\theta'$ proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$. If $\alpha$ is a renaming of the leaves of $\theta$, then there exists $\alpha'$, a renaming of the leaves of $\theta'$, such that $\alpha'(\tilde{A}) \stackrel{\alpha'(\theta), \alpha'(\theta')}{\cong} \alpha(B)$; more precisely:

- $\alpha'(\theta')$ is a proof-net

- $\alpha(A^{\perp}) = \alpha'(A)^{\perp}$ and $\alpha'(B^{\perp}) = \alpha(B)^{\perp}$

- the composition of $\alpha(\theta)$ and $\alpha'(\theta')$ by cut over $\alpha(B)$ (resp. $\alpha'(A)$) gives the identity proof-net of $\alpha'(A)$ (resp. $\alpha(B)$).

**Proof.** We first define $\alpha'$. By Theorem 29, $\theta'$ is bipartite ax-unique, so it is sufficient to define $\alpha'$ only on the occurrences of $B^{\perp}$, i.e. to define $\alpha'(B^{\perp})$. We set $\alpha'(B^{\perp}) = \alpha(B)^{\perp}$. Then the composition of $\alpha(\theta)$ and $\alpha'(\theta')$ by cut over $\alpha(B)$ is a proof-net. Since cut-elimination does not depend on labels, this composition reduces to an identity proof-net with conclusions $\alpha(A^{\perp}), \alpha'(A)$. An induction, on the number of connectives of $\alpha(A)$, shows that this is the identity proof-net of $\alpha(A^{\perp})$. Thus $\alpha(A^{\perp}) = \alpha'(A)^{\perp}$. But then, the composition of $\alpha'(\theta')$ and $\alpha(\theta)$ by cut over $\alpha'(A)$ is a proof-net, that reduces to an identity net (since cut-elimination does not depend on labels), that is the identity proof-net of $\alpha(B)$. Hence, $\alpha'(\tilde{A}) \stackrel{\alpha'(\theta), \alpha'(\theta')}{\cong} \alpha(B)$. ◀

**Lemma 56 (Distributed ambiguous isomorphic formulas).** Let $A$ and $B$ be distributed formulas, such that $A$ is ambiguous and $A \stackrel{\theta, \theta'}{\cong} B$. There exists a substitution $\sigma$ and distributed formulas $A'$ and $B'$, non-ambiguous, such that $A = \sigma(A')$, $B = \sigma(B')$ and $A'^{\theta, \theta'} \cong B'$ for some proof-nets $\theta$ and $\theta'$.

**Proof.** The proof-nets $\theta$ and $\theta'$ are bipartite ax-unique (Theorem 29), with conclusions $B^{\perp}, A$ and $A^{\perp}, B$ respectively. One can define a renaming $\alpha$ such that $\alpha(A)$ has distinct atoms (i.e. no atom of $\alpha(A)$ occurs twice in $\alpha(A)$, even one positively and one negatively), for it is sufficient to define $\alpha$ only on leaves of $A$. In particular, $\alpha(A)$ is non-ambiguous. Then, Theorem 55 gives an algorithm for defining a renaming $\alpha'$ such that $\alpha'(\tilde{A}) \stackrel{\alpha'(\theta), \alpha'(\theta')}{\cong} \alpha(B)$, with in particular $\alpha'(A^{\perp}) = \alpha(A)^{\perp}$ and $\alpha(B^{\perp}) = \alpha'(B)^{\perp}$. Pose $A' := \alpha'(A)$ and $B' := \alpha(B)$, hence $\tilde{A} \stackrel{\alpha'(\theta), \alpha'(\theta')}{\cong} B'$ and $\alpha(\theta)$ has for conclusions $B'^{\perp}, A'$. Formulas $A'$ and $B'$ are distributed, as renaming acts only on leaves.

On $\alpha(\theta)$ one can define a renaming $\alpha^{-1}$ such that $\alpha^{-1}(A') = A$, hence $\alpha^{-1}(B'^{\perp}) = B^{\perp}$. Since $\alpha(\theta)$ is bipartite ax-unique, it is equivalent to define $\alpha^{-1}$ on $\alpha(\theta)$ or only on leaves of $A'$. Because all atoms of $A'$ are distinct, two distinct leaves of $A'$ correspond to distinct atoms of $A'$. One can then define a substitution $\sigma$ on atoms of $A'$ by $\sigma(X) = \alpha^{-1}(l(X))$, with $l(X)$ the unique leaf of $A'$ with label $X$. Thus, $\theta = \alpha^{-1}(\alpha(\theta)) = \sigma(\alpha(\theta))$: in particular, $\sigma(A') = A$ and $\sigma(B'^{\perp}) = B^{\perp}$, so $\sigma(B') = B$. Finally, $A'$ and $B'$ are distributed non-ambiguous formulas such that $\tilde{A} \stackrel{\alpha(\theta), \alpha(\theta')}{\cong} B'$, $A = \sigma(A')$ and $B = \sigma(B')$. ◀

**Corollary 31 (Reduction to distributed non-ambiguous formulas).** The set of couples of distributed formulas $A$ and $B$ such that $A \stackrel{\theta, \theta'}{\cong} B$ is the set of instances (by a substitution on atoms) of couples of distributed non-ambiguous formulas $A'$ and $B'$ such that $A'^{\beta, \beta'} \cong B'$.
**Proof.** We show each inclusion separately. Let $A$ and $B$ be two distributed formulas such that $A \stackrel{\theta, \vartheta}{\cong} B$. If $A$ or $B$ is ambiguous, then $A$ and $B$ are instances of two non-ambiguous distributed formulas $A'$ and $B'$ such that $A'^{\beta', \beta'} \stackrel{\vartheta', \vartheta'}{\cong} B'$. Otherwise, $A$ and $B$ are non-ambiguous and the result holds.

Conversely, let $A'$ and $B'$ be distributed non-ambiguous formulas such that $A'^{\vartheta', \vartheta'} \stackrel{\beta', \beta'}{\cong} B'$, and $\sigma$ a substitution on atoms of $A'$ (so also on atoms of $B'$). Let $\theta'$ and $\vartheta'$ are bipartite $ax$-unique proof-nets (Theorem 29). The substitution $\sigma$ defines on $\theta'$ a renaming $\alpha$ (any substitution can be seen as a renaming). Let $\alpha'$ be the renaming defined on $\vartheta'$, associated to $\alpha$ in Theorem 55. Since $\sigma(A'^{\perp}) = \alpha(A'^{\perp}) = (\alpha'(A'))^{\perp}$, $\alpha'$ is also the renaming induced by $\sigma$ on $\vartheta'$. As $\alpha'(A'^{\beta', \beta'}) \stackrel{\alpha', \alpha}{\cong} \sigma(B')$ by Theorem 55, it follows $\sigma'(A'^{\beta', \beta'}) \stackrel{\alpha', \alpha}{\cong} \sigma(B')$. $\quad \blacksquare$

### C.9 Proof of Corollary 32

**Lemma 57.** Let $\theta$ and $\vartheta$ be bipartite proof-nets of respective conclusions $A, B$ and $B^{\perp}, C$. Their composition over $B$ reduces to a bipartite proof-net.

**Proof.** The resulting proof-net has for conclusions $A, C$. The only links in the new proof-net that were not in $\theta$ nor $\vartheta$ are those resulting from the replacement of a pair of links $(l, m)$ and $(m^{\perp}, n)$ with a link $(l, n)$, where $m$ is a leaf of $B$. By bipartiteness of $\theta$ and $\vartheta$, it follows $l$ is a leaf of $A$ and $n$ one of $C$, so the new axiom link is between a leaf of $A$ and one of $C$. $\quad \blacksquare$

**Lemma 58.** Let $\theta$ be a bipartite proof-net of conclusions $A^{\perp}, A$, with $A$ a non-ambiguous formula. Axiom links of $\theta$ are of the form $(l^{\perp}, l)$ for $l$ a leaf of $A$.

**Proof.** Let $a$ be an axiom link of $\theta$. By bipartiteness, it uses a leaf $l$ of $A$ and a leaf $m$ of $A^{\perp}$. Denote by $X$ the label of $l$, whence the label of $m$ is $X^{\perp}$. However, the only leaf of $A^{\perp}$ with label $X^{\perp}$ is $l^{\perp}$, because $A^{\perp}$ is non-ambiguous. Thus, $m = l^{\perp}$ and $a = (l, l^{\perp})$. $\quad \blacksquare$

**Lemma 59.** Let $\theta$ be a bipartite proof-net of conclusions $A^{\perp}, A$, with $A$ a non-ambiguous formula. Take a linking $\lambda \in \theta$ and an additive vertex $V$ in its additive resolution. The vertex $V^{\perp}$ is in the additive resolution of $\lambda$, and $\lambda$ keeps for $V^{\perp}$ the dual premise it keeps for $V$.

**Proof.** As $V$ is in the additive resolution $(A^{\perp}, A) \upharpoonright \lambda$ of $\lambda$, one of its ancestor leaves, say $l$, is in $(A^{\perp}, A) \upharpoonright \lambda$: there is a link $a \in \lambda$ on it. By Lemma 58, $a = (l, l^{\perp})$. But $l^{\perp}$ is an ancestor of $V^{\perp}$, so $V^{\perp}$ is in $(A^{\perp}, A) \upharpoonright \lambda$, with as premise the dual premise chosen for $V$. $\quad \blacksquare$

**Lemma 60.** Let $A$ be a non-ambiguous formula, $\theta$ and $\theta'$ bipartite proof-nets of conclusions $A^{\perp}, A$. Then $\theta = \theta'$.

**Proof.** Take $\lambda \in \theta$ a linking. It is on some $\&$-resolution $R$ of $A^{\perp}, A$. By (P1), there exists a unique linking $\lambda' \in \theta'$ on $R$. We have to prove $\lambda = \lambda'$. They have the same additive resolution, for their choice on a $\oplus$-vertex $P$ is determined by the premise taken for the $\&$-vertex $P^{\perp}$, which is in $R$ (Lemma 59). They have the same axiom links on this additive resolution, because any leaf on it is linked to its dual (Lemma 58). Therefore, $\lambda = \lambda'$, so $\theta \subseteq \theta'$. By symmetry, the same reasoning yields $\theta' \subseteq \theta$, thus $\theta = \theta'$. $\quad \blacksquare$

**Corollary 61.** Let $A$ be a non-ambiguous formula. There is exactly one bipartite proof-net of conclusions $A^{\perp}, A$: the identity proof-net of $A$.

**Proof.** This follows from Proposition 15(i) and Lemma 60. $\quad \blacksquare$
<figure><img src="image_25.png" /></figure>

<figure><img src="image_26.png" /><figcaption>Figure 14 Illustration of the proof of Lemma 64</figcaption></figure>

**Theorem 62** (Bipartite proof-nets for non-ambiguous formulas). Let $\theta$ and $\theta'$ be bipartite proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, with $A$ a non-ambiguous formula. Then their composition over $B$ reduces to the identity proof-net of $A$.

*Proof.* By Lemma 57, the composition of $\theta$ and $\theta'$ by cut reduces to a bipartite proof-net, of conclusions $A^{\perp}, A$. By Corollary 61, this can only be the identity proof-net of $A$. ◀

**Corollary 32.** Let $A$ and $B$ be non-ambiguous formulas. If there exist bipartite proof-nets $\theta$ and $\vartheta$ of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, then $A^{\vartheta, \vartheta} \simeq_B B$.

*Proof.* By Theorem 62 both compositions yields identity proof-nets, whence $A^{\vartheta, \vartheta} \simeq_B B$. ◀

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

## C.10 Isomorphisms completeness for unit-free MALL (Theorem 33)

**Definition 63** (Sequentializing vertex). A terminal (i.e. with no descendant) non-leaf vertex $V$ in a proof-net $\theta$ is called sequentializing if, depending on its kind:

- $\otimes\*-vertex$: the removal of $V$ in $G_{\theta}$ has two connected components.

- $\oplus$-vertex: the left or right syntax tree of $V$ does not belong to $G_{\theta}$ (i.e. has no link on any of its leaves in $G_{\theta}$).

- $\mathcal{N}\&-vertex$: a terminal $\mathcal{N}\&-vertex$ is always sequentializing.

It is easy to check that removing a sequentializing vertex produces proof-net(s). The sequentialization theorem affirms there exists a sequentializing vertex in a proof-net.

**Lemma 64.** In a bipartite full proof-net with conclusions $A_l \odot A_r, B$, where $\odot \in \{\otimes; \oplus\}$, the root of $A_l \odot A_r$ is not sequentializing.

*Proof.* Let $l$ be a leaf of $A_l$ and $r$ one of $A_r$. By bipartiteness and fullness, there are leaves $m$ and $s$ of $B$ with axiom links $(l, m)$ and $(r, s)$ in the proof-net (see Figure 14). As there is a path in $T(B)$ between $m$ and $s$, whether $\odot = \oplus$ or $\odot = \otimes$, it is not sequentializing. ◀

**Lemma 65** (Reordering $\mathcal{N}$-vertices). Let $\theta$ be a bipartite ax-unique proof-net of conclusions $A = A_l \mathcal{N} A_r$ and $B = B_l \odot B_r$ with $\odot \in \{\otimes; \oplus\}$ and $A$ a distributed formula. Then $\odot = \otimes$ and there exist two bipartite ax-unique proof-nets of respective conclusions $A'_l, B_l$ and $A'_r, B_r$ where $A'_l \mathcal{N} A'_r$ is equal to $A_l \mathcal{N} A_r$ up to associativity and commutativity of $\mathcal{N}$.

*Proof.* We remove all terminal (hence sequentializing) $\mathcal{N}$-vertices, all in $A$, without modifying the linkings. The resulting graph is a proof-net of conclusions $A_1, \dots, A_n, B_l \odot B_r$ (see Figure 15). The roots of the new trees $A_i$ cannot be $\&$-vertices because $A$ is distributed: so they are $\otimes\oplus$-vertices or atoms. These $\otimes\oplus$-vertices are not sequentializing, since by bipartiteness and fullness every leaf of each $A_i$ is connected to the formula $B_l \odot B_r$ (reasoning
<figure><img src="image_28.png" /></figure>

<figure><img src="image_29.png" /><figcaption>**Figure 15** Proof-net of Lemma 65 with all terminal ℘-vertices removed</figcaption></figure>

as in the proof of Lemma 64). Thus, the sequentializing vertex of this proof-net is necessarily $B_l \odot B_r$. It follows $\odot = \otimes$, because all leaves of $B$ are connected to leaves in $A_1, \dots, A_n$, so if $\odot = \oplus$ then $B_l \odot B_r$ cannot be sequentializing. Removing the sequentializing $B_l \otimes B_r$ gives two proof-nets, with a bipartition of the $A_i$ into two classes: those linked to leaves of $B_l$ and the others linked to leaves of $B_r$. We recover from these proof-nets bipartite ax-unique ones by adding ℘-vertices under the $A_i$ in an arbitrary order, yielding formulas $A_l'$ (with those linked to $B_l$) and $A_r'$ (with those linked to $B_r$). As we only removed and put back ℘-vertices, $A_l' \not\to A_r'$ is equal to $A_l \not\to A_r$ up to associativity and commutativity of ℘. ◀

**Lemma 66** (Reordering &-vertices). Let $\theta$ be a bipartite ax-unique proof-net of conclusions $A = A_l \& A_r$ and $B = B_l \oplus B_r$ with $A$ a distributed formula. Then there exist two bipartite ax-unique proof-nets of respective conclusions $A_l', B_l$ and $A_r', B_r$ where $A_l' \& A_r'$ is equal to $A_l \& A_r$ up to associativity and commutativity of &. ◁

**Proof.** We remove all terminal &-vertices in the proof-net, then all terminal ℘-vertices, all in $A$. The resulting graphs are proof-nets $\theta_i$ (for terminal negative vertices are sequentializing), of conclusions $A_1^i, \dots, A_{n_i}^i, B_l \oplus B_r$ for the $i$-th proof-net. An illustration is Figure 15, except we have several of these proof-nets, having in common exactly $T(B)$. As in the proof of Lemma 65, the roots of the new trees $A_j^i$ cannot be negative vertices because the formula $A$ is distributed: so they are $\otimes \amalg$-vertices or atoms. These $\otimes \amalg$-vertices cannot be sequentializing, since by bipartiteness and fullness every leaf of $A_j^i$ is connected to the formula $B_l \oplus B_r$ (reasoning as in the proof of Lemma 64). Thus, the sequentializing vertex of these proof-nets is necessarily $B_l \oplus B_r$, we can remove it: for a given $i$, all $A_j^i$ are linked only to either $B_l$ or $B_r$. We put back the ℘-vertices we removed, in the very same order. We then put back the &-vertices we removed, but in another order: we put together all $\theta_i$ linked to $B_l$, and all those to $B_r$, yielding two proof-nets of conclusions $B_l, A_l'$ and $B_r, A_r'$. These proof-nets are bipartite ax-unique ones (because adding and removing ℘ does not modify the linkings, and & is disjoint union of linkings). We indeed have $A_l' \& A_r'$ equal to $A_l \& A_r$ up to associativity and commutativity of &, because we only reordered &-vertices. ◁

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

We conclude by induction on the size $s(A)$ of $A$, which is its number of connectives (thus unaffected by commutation and associativity of connectives).

**Theorem 33** (Isomorphisms completeness for unit-free MALL). Given $A$ and $B$ two unit-free MALL formulas, if $A \simeq B$, then $A =_{\varepsilon\uparrow} B$.
**Proof.** By Theorem 13, there exist proof-nets $\theta$ and $\vartheta$ such that $A \stackrel{\theta, \vartheta}{\cong} B$. We prove the following stronger result: if $A \stackrel{\theta, \vartheta}{\cong} B$ for some proof-nets $\theta$ and $\vartheta$, then $A =_{\mathcal{E}^\dagger} B$. We assume $A$ and $B$ to be distributed and non-ambiguous formulas by Proposition 21 and Corollary 31. We reason by induction on the size of $A$, $s(A)^7$.

If $A$ and $B$ are atoms (i.e. of null size), then $A = B$ and the property holds. Otherwise, $A^{\perp}$ and $B$ are both non atomic. By Theorem 29, $\theta$ and $\vartheta$ are bipartite ax-unique; they have respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$. By Lemma 64, one of the formulas $A^{\perp}, B$ is negative, otherwise neither the root of $A^{\perp}$ nor $B$ is sequentializing in $\theta$, contradicting sequentialization (Theorem 10). A symmetric reasoning on $\vartheta$ implies that the other formula is positive. Assume w.l.o.g. that $B = B_0 \odot B_1$ is positive (i.e. $\odot \in \{\otimes; \oplus\}$) and $A^{\perp}$ negative. We distinguish cases according to the kind of the roots of $A^{\perp}$ and $B$, considering the proof-net $\theta$. If $B$ a $\otimes$-formula and $A$ a $\&$-formula, we instead consider $\vartheta$ of conclusions $B^{\perp}, A$, where $A$ is a $\oplus$-formula and $B^{\perp}$ a $\aleph$-formula. Whence, either $A^{\perp}$ is a $\aleph$-formula, or $B$ and $A^{\perp}$ are respectively a $\oplus$-formula and a $\&$-formula.

In the first (resp. second) case, by Lemma 65 (resp. Lemma 66) $\odot = \otimes$ (in the first case only) and there exist two bipartite ax-unique proof-nets $\theta_0$ and $\theta_1$ of respective conclusions $A'_0^{\perp}, B_0$ and $A'_1^{\perp}, B_1$, with $A'^{\perp} = A'_1^{\perp} \aleph A'_0^{\perp}$ (resp. $A'^{\perp} = A'_1^{\perp} \& A'_0^{\perp}$) equal to $A^{\perp}$ up to associativity and commutativity of $\aleph$ (resp. $\&$). In particular, $A'^{\perp} =_{\mathcal{E}^\dagger} A^{\perp}$, and $s(A'_0)$ and $s(A'_1)$ are both less than $s(A)$. To conclude, we only need bipartite proof-nets $\vartheta_0$ and $\vartheta_1$ of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. We will then apply Corollary 32 to obtain $A'_0 \stackrel{\vartheta_0, \vartheta_0}{\cong} B_0$ and $A'_1 \stackrel{\vartheta_1, \vartheta_1}{\cong} B_1$. Thence, by induction hypothesis, $A'_0 =_{\mathcal{E}^\dagger} B_0$ and $A'_1 =_{\mathcal{E}^\dagger} B_1$, thus $A' =_{\mathcal{E}^\dagger} B$.<fnref n="8" /> As $A =_{\mathcal{E}^\dagger} A'$, we will finally conclude $A =_{\mathcal{E}^\dagger} B$.

Thus, we look for two bipartite proof-nets of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. As $A \stackrel{\theta, \vartheta}{\cong} B$, and $A \simeq A'$ by soundness of $\mathcal{E}^\dagger$ (Theorem 3), it follows using Theorem 13 that $A'^{\oplus, \vartheta'} \stackrel{\Theta'}{\cong} B$ for some proof-nets $\Theta$ and $\Theta'^{\cdot 9}$. Furthermore, $\Theta$ is a bipartite ax-unique proof-net (Theorem 29) of conclusions $B^{\perp}, A'$, i.e. of conclusions $B_1^{\perp} \odot^{\perp} B_0^{\perp}, A'_0 \odot A'_1$ with $(\odot^{\perp}, \odot) \in \{(\aleph, \otimes); (\& , \oplus)\}$. We had a bipartite ax-unique proof-net $\theta_0$ of conclusions $A'_0^{\perp}, B_0$, therefore the atoms or negated atoms of $B_0$ are exactly those of $A'_0$. Similarly, the atoms and negated atoms of $B_1$ are exactly those of $A'_1$. Whence, no atom nor negated atom of $B_0$ (resp. $B_1$) is one of $A'_1$ (resp. $A'_0$), for otherwise an atom or negated atom of $A_0$ (resp. $A_1$) also occurs in $A'_1$ (resp $A'_0$), contradicting non-ambiguousness of $A'$. This implies that axiom links in $\Theta$ must be between leaves of $B_0^{\perp}$ and $A'_0$, and between leaves of $B_1^{\perp}$ and $A'_1$. Therefore, once we sequentialize the negative root $\odot^{\perp}$ of $B^{\perp}$ in $\Theta$, the positive root $\odot$ of $A'$ is sequentializing. After sequentializing both, we obtain two bipartite ax-unique proof-nets, of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. ◀

D Proofs for the completeness for full MALL

This appendix contains proofs of results stated in Section 4 and leading to the proof of completeness for full MALL. In all this section, by proof we mean a sequent calculus proof of MALL, we never consider proof-nets.

<footnote n="7">⁷ Remark that $s(A) = s(B)$, because $\theta$ is bipartite ax-unique (Theorem 29), thence $A$ and $B$ have the same number of atoms, so of connectives as they are all binary ones.</footnote>

<footnote n="8">⁸ The formula $A'$ is distributed for it is equal up to associativity and commutativity to the distributed $A$. Whence, $A'_0$ and $A'_1$ are also distributed.</footnote>

<footnote n="9">⁹ One can easily check that isomorphisms in proof-nets form equivalence classes on formulas.</footnote>
## D.1 Proof of Theorems 34 and 35

**Definition 67.** We define the weight $w(\pi)$ of a proof $\pi$ by induction:

$$ \text{w} \left( \vdash A^{\perp}, A \middle| ax \right) = 1. $$

$$ \text{w} \left( \frac{\pi}{\vdash A, \Gamma} \frac{\varpi}{\vdash A^{\perp}, \Delta} \middle| \text{cut} \right) = w(\pi) + w(\varpi) $$

$$ \text{w} \left( \frac{\pi}{\vdash A, \Gamma} \frac{\varpi}{\vdash B, \Delta} \middle| \text{cut} \right) = w(\pi) + w(\varpi) + 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash A, B, \Gamma} \middle| \text{cut} \right) = w(\pi) + 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash 1} \middle| 1 \right) = 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash \Gamma} \middle| \text{cut} \right) = w(\pi) + 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash A, \Gamma} \frac{\varpi}{\vdash B, \Gamma} \middle| \text{cut} \right) = \max(w(\pi), w(\varpi)) + 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash A_i, \Gamma} \middle| \text{cut} \right) = w(\pi) + 1 $$

$$ \text{w} \left( \frac{\pi}{\vdash \Gamma} \middle| \text{cut} \right) = 1 $$

**Definition 68.** A block $\mathfrak{B}$ of cut-rules in a proof $\pi$ is a maximal set of cut-rules in $\pi$ such that all of these rules are a premise of another rule in the set, or use as premise the conclusion of a rule in the set. A block can also be seen as a maximal sub-proof composed of cut-rules only.

We call measure $|\mathfrak{B}|$ of a block $\mathfrak{B}$ of cut-rules in a proof $\pi$ the weight of its root cut-rule, i.e. $|\mathfrak{B}| = \sum_i w(\pi_i)$ where the $\pi_i$ are the sub-proofs whose conclusions are the premises of the cut-rules of $|\mathfrak{B}|$, premises which are not the conclusion of a cut-rule.

The measure $|c|$ of a cut-rule $c$ in a proof $\pi$ is the measure of the block it belongs to.

The measure $|\pi|$ of a proof $\pi$ is the multiset of the measures of its cut-rules.

**Remark.** A block $\mathfrak{B}$ of $n$ cut-rules in a proof $\pi$ has its measure $|\mathfrak{B}|$ appearing $n$ times in $|\pi|$, once for each of its cut-rules.

**Lemma 69.** If $\pi \xrightarrow{\beta} \varpi$ then $|\pi| \ge |\varpi|$, with equality if and only if the $\xrightarrow{\beta}$ step is a cut-cut commutative step.

**Proof.** It suffices to compute the measure before and after each cut-elimination step. $\quad \blacksquare$

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

We denote by $\xrightarrow{\bar{\beta}}$ a $\xrightarrow{\beta}$ step other than a cut-cut commutation. Also note $\sim_c$ the equivalence closure of cut-cut commutation (which is already a symmetric relation).

**Lemma 70.** *Cut-elimination not involving the cut-cut commutation in MALL sequent calculus is strongly normalizing. In particular, cut-elimination is weakly normalizing.*

**Proof.** As long as there exists a cut-rule, we can choose to do a $\xrightarrow{\bar{\beta}}$ step (for instance by considering a cut-rule with no other cut-rule above it). This strictly decreases the measure of the proof by Lemma 69, ensuring termination. $\quad \blacksquare$

<figure><img src="image_32.png" /></figure>
<figure><img src="image_33.png" /></figure>

<figure><img src="image_34.png" /><figcaption>Figure 16 Diagrams of Lemmas 72, 73, and 74 (from left to right)</figcaption></figure>

We recall $=c$ is one rule commutation of cut-free MALL, i.e. which is not a commutation involving a cut-rule nor a $\top - \otimes$ commutation creating or deleting a sub-proof containing a cut-rule. We denote $=c^*$ the equivalence closure of $=c$.

**Lemma 71.** If $\pi =_c \varpi$ with a rule commutation not involving a $\top$-rule, then $|\pi| = |\varpi|$.

**Proof.** It suffices to compute the measure for both sides of each such rule commutation. ◀

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

**Lemma 72.** Let $\pi_1, \pi_2$ and $\pi_3$ be proofs such that $\pi_1 =_c \pi_2 \xrightarrow{\beta} \pi_3$. Then, there exist $\varpi_1$ and $\varpi_2$ such that $\pi_1 \xrightarrow{\beta^*} \varpi_1 =_c^* \varpi_2 \xleftarrow{\beta^*} \pi_3$ (diagrammatically represented on Figure 16). Furthermore, all proofs in the sequence $\varpi_1 =_c^* \varpi_2$ have measures strictly smaller than $\max(|\pi_1|, |\pi_2|)$.

**Proof.** A first general case is when the $\pi_1 =_c \pi_2$ and $\pi_2 \xrightarrow{\beta} \pi_3$ steps involve only distinct rules, and the rules of one are neither erased nor duplicated by the other. Then they commute and we have $\pi_1 \xrightarrow{\beta} \varpi_1 =_c \pi_3$ using the same steps in the other order. The result on measures follows by Lemma 69.

Assume these steps use distinct rules, but $\pi_1 =_c \pi_2$ duplicates a sub-proof containing the rules of $\pi_2 \xrightarrow{\beta} \pi_3$ (this can happen if the $=c$ step is a $\& - \otimes$ commutative case). Then, by doing the $\xrightarrow{\beta}$ step first, with $\pi_1 \xrightarrow{\beta} \varpi_1$, we can do the $=c$ step after, yielding $\varpi_1 =_c \varpi_2$, with $\varpi_2$ being $\pi_3$ where we did the $\xrightarrow{\beta}$ step on both duplicated occurrences and not just one. Therefore, we have $\pi_3 \xrightarrow{\beta} \varpi_2$ by doing this step on the other duplicated occurrence. We conclude $\pi_1 \xrightarrow{\beta} \varpi_1 =_c \varpi_2 \xleftarrow{\beta} \pi_3$, and $|\varpi_1| < |\pi_1|, |\varpi_2| < |\pi_3| < |\pi_2|$ by Lemma 69.

Now, consider the case where the two steps still involve distinct rules, but the $\pi_2 \xrightarrow{\beta} \pi_3$ step duplicates a sub-proof containing the rules of $\pi_1 =_c \pi_2$ (which may happen if $\pi_2 \xrightarrow{\beta} \pi_3$ is a $\&$-cut commutative case). Then, by doing the $\xrightarrow{\beta}$ step first, yielding $\pi_1 \xrightarrow{\beta} \varpi_1$, we need to do the $=c$ step twice, once for each occurrence, to recover $\pi_3$: we get $\pi_1 \xrightarrow{\beta} \varpi_1 =_c \varpi_2 =_c \pi_3$. The result on measures follows by Lemma 69 and because we duplicate the step $=c$, so $|\varpi_2| \le \max(|\varpi_1|, |\pi_3|) < \max(|\pi_1|, |\pi_2|)$.

Another general case is when the rules involved in the two steps are distinct, but the $\xrightarrow{\beta}$ step eliminates a subtree containing the rules of the $=c$ step (this can arise when using a $\& - \oplus_i$ key case or a $\top - \text{cut}$ commutative case). In this case, doing first the $\xrightarrow{\beta}$ step directly yields $\pi_3$: $\pi_1 \xrightarrow{\beta} \pi_3$, with $|\pi_3| < |\pi_1|$. A $=c$ step cannot erase a sub-proof containing the rules of a $\xrightarrow{\beta}$ step, for the only possible case for this is a $\top - \otimes$ commutative case, and we assumed in this case that the sub-proof erased (or created) is cut-free.
From now on, we suppose not to be in such situations, meaning both steps involve (at least) one common rule. This rule cannot be a *cut* one, for there are no commutations involving a *cut*-rule in $=c$. We distinguish cases according to the kind of $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$.

If $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is an *ax* key case. As an *ax*-rule never commutes, the two steps share no rule.

If $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is a $\mathfrak{N} \otimes \mathfrak{N}$-key case. In this case, $\pi_2$ and $\pi_3$ are the following proofs:

$$ \frac{\rho_1 \quad \rho_2 \quad \rho_3}{\frac{\vdash A, \Gamma}{\vdash A \otimes B, \Gamma, \Delta} \otimes \frac{\vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash B^{\perp} \mathfrak{N} A^{\perp}, \Sigma} \mathfrak{N}} \xrightarrow{\rho_1 \quad \rho_2 \quad \rho_3} \frac{\frac{\vdash A, \Gamma}{\vdash A^{\perp}, \Delta, \Sigma} \text{cut}}{\frac{\vdash \Gamma, \Delta, \Sigma}{\rho_4}} \xrightarrow{\rho_1 \quad \rho_2 \quad \rho_3} \frac{\frac{\vdash B, \Delta}{\vdash B^{\perp}, A^{\perp}, \Sigma} \text{cut}}{\frac{\vdash A^{\perp}, \Delta, \Sigma}{\rho_4}} \text{cut} $$

By our assumption, $\pi_1 =_c \pi_2$ was a step pushing down the $\otimes$ or $\mathfrak{N}$-rule, and up some non *cut*-rule *r*. We can in $\pi_1$ commute the *cut*-rule up and *r* down (as *r* cannot introduce the formula on which we cut). This yields a proof $\varpi_1$ such that $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1$ with this commutative step, and $\varpi_1 \xrightarrow{\bar{\beta}} \varpi_3$ using the same step as in $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$, unless *r* is a $\top$-rule, case we will discuss in a second step, and if *r* is a $\&$-rule we do it on both occurrences, obtaining $\varpi_1 \xrightarrow{\bar{\beta}} \varpi_2 \xrightarrow{\bar{\beta}^*} \varpi_3$. Thus, except if *r* is a $\top$-rule, we have $\varpi_1 \xrightarrow{\bar{\beta}^*} \varpi_3$. Then, in $\varpi_3$ we can commute *r* up above one or two (according to its original position) of the *cut*-rules created by this key case, yielding $\pi_3$ using one or two $\xleftarrow{\bar{\beta}}$ step. Therefore, $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xrightarrow{\bar{\beta}^*} \varpi_3 \xleftarrow{\bar{\beta}^*} \pi_3$.

Now, let us consider the case where the other rule *r* in the $=c$ step is a $\top$-rule, say above the $\otimes$ formula (the case where it is above the $\mathfrak{N}$ is similar). The proof $\pi_1$ is

$$ \frac{\rho_3}{\frac{\vdash A \otimes B, \Gamma, \Delta}{\vdash \Gamma, \Delta, \Sigma} \top \frac{\vdash B^{\perp}, A^{\perp}, \Sigma}{\vdash B^{\perp} \mathfrak{N} A^{\perp}, \Sigma} \mathfrak{N}} \xrightarrow{\rho_3} \frac{\frac{\vdash \Gamma, \Delta, \Sigma}{\rho_4}}{\frac{\vdash \Gamma, \Delta, \Sigma}{\rho_4}} \text{cut} \quad \text{First executing a commutative } \top - \text{cut} \xrightarrow{\bar{\beta}} $$

step in $\pi_1$ using this rule, we obtain $\varpi_1 = \frac{\vdash \Gamma, \Delta, \Sigma}{\rho_4} \top$. Using one or two $\top - \text{cut}$ commutations yields $\pi_3$, by putting the $\top$-rule in the corresponding $\rho_i$ it was in $\pi_2$. Whence, $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xleftarrow{\bar{\beta}^*} \pi_3$. Similarly, if *r* is commuted with the $\mathfrak{N}$-rule, we obtain $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xleftarrow{\bar{\beta}} \pi_3$. This concludes the study when $=c$ is a commutation with the $\otimes$ or $\mathfrak{N}$-rule.

In both subcases, the result on measures follows by Lemma 69.

If $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is a $\& \oplus_i$ key case. This case is similar to the previous one, in simpler as we create one new *cut*-rule and not two. We have $\pi_2$ the following proof:

$$ \frac{\rho_2 \quad \rho_1 \quad \rho_3}{\frac{\vdash A_2, \Gamma}{\vdash A_2 \& A_1, \Gamma} \& \frac{\vdash A_i^{\perp}, \Delta}{\vdash A_1^{\perp} \oplus A_2^{\perp}, \Delta} \oplus_i \frac{\vdash \Gamma, \Delta}{\rho_4}} \text{cut} $$

and $\pi_3$ the next one:

$$ \frac{\rho_i \quad \rho_3}{\frac{\vdash A_i, \Gamma}{\vdash \Gamma, \Delta} \text{cut}} \frac{\vdash A_i^{\perp}, \Delta}{\rho_4} $$
The $\pi_1 =_c \pi_2$ step was a commutation pushing down the $\&$ or $\oplus_i$-rule, and another non-cut-rule $r$ up. We can first commute $r$ and the cut-rule, yielding $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1$. Applying the key case then yields $\varpi_1 \xrightarrow{\bar{\beta}} \varpi_3$, unless $r$ is a $\top$-rule, case we will discuss in a second step, and if $r$ is a $\&$-rule we can do it on both occurrences, obtaining $\varpi_1 \xrightarrow{\bar{\beta}} \varpi_2 \xrightarrow{\bar{\beta}} \varpi_3$. Then, in $\varpi_3$, we can commute $r$ up above the cut-rule created by this key case, yielding $\pi_3$. Therefore, $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xrightarrow{\bar{\beta}^*} \varpi_3 \xrightarrow{\bar{\beta}} \pi_3$ (if $r$ is not a $\top$-rule).

Now, let us consider the case where the other rule $r$ in the $=c$ step is a $\top$-rule, above the $\&$ or $\oplus$ formula. First executing a $\top$-cut commutative step in $\pi_1$ using this rule, we obtain $\varpi_1 = \frac{\vdash \Gamma, \Delta}{\varpi_3}$. Then, a $\top$-cut commutation yields $\pi_3$ by putting the $\top$-rule in the corresponding $\rho_i$ it was in $\pi_2$. Whence, $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xrightarrow{\bar{\beta}} \pi_3$.

In both subcases, the result on measures follows by Lemma 69.

**If $\pi_2 \xrightarrow{\beta} \pi_3$ is a $\perp$-1 key case.** This case is also similar to the $\mathcal{N} \otimes \beta$ key case, in simpler form as there are less sub-proofs. We have $\pi_2 = \frac{\frac{\rho_1}{\vdash \Gamma}}{\frac{\vdash \perp, \Gamma}{\rho_2}} \perp$ cut and $\pi_3 = \frac{\rho_1}{\vdash \Gamma}$. 

The 1-rule does not commute, so the $\pi_1 =_c \pi_2$ step was a commutation pushing down the $\perp$-rule, and another non-cut-rule $r$ up. We can first commute $r$ and the cut-rule, yielding $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1$. Applying the key case then yields $\varpi_1 \xrightarrow{\bar{\beta}} \pi_3$, unless $r$ is a $\top$-rule, case we will discuss in a second step, and if $r$ is a $\&$-rule we can do it on both occurrences, obtaining $\varpi_1 \xrightarrow{\bar{\beta}^*} \pi_3$.

Now, let us consider the case where the other rule $r$ in the $=c$ step is a $\top$-rule, above the $\perp$-formula. Applying a $\top$-cut commutative step in $\pi_1$ using this rule, we directly obtain $\pi_3$. Whence, $\pi_1 \xrightarrow{\bar{\beta}} \pi_3$.

In both subcases, the result on measures follows by Lemma 69.

**If $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is a commutative case.** We have $\pi_1 =_c \pi_2$ and $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ having exactly one rule in common, for the cut-rule does not belong to the commutations in $=c$ and a commutative cut-elimination case involves two rules. Thus, the $=c$ step involves the rule $r$ that will be commuted down in the $\xrightarrow{\beta}$ step, and call $s$ the other rule involved in $=c$. These rules $r$ and $s$ are not cut-rules. The proof $\pi_1$ has from top to bottom $r, s$ and $cut, \pi_2$ has $s, r$ and $cut$, and $\pi_3$ has $s, cut$ and $r$. Assume for the moment neither $r$ nor $s$ is a $\top$-rule.

If the cut-rule commutes with $s$, we first commute $s$-cut then $r$-cut, yielding $\pi_1 \xrightarrow{\bar{\beta}} \varpi_1 \xrightarrow{\bar{\beta}^*} \varpi_3$ (the $\xrightarrow{\bar{\beta}^*}$ being of length one, except if $s$ is a $\&$-rule, in which case we need to do the $r$-cut commutation for both occurrences). The proof $\varpi_3$ has from top to bottom cut, $r$ and $s$. We then commute $r$ with $s$ and then $s$ with cut (twice if $r$ is a $\&$-rule), yielding $\varpi_3 =_c \varpi_4 \xrightarrow{\bar{\beta}^*} \pi_3$. The result on measures is a consequence of Lemma 69.

Otherwise, $s$ is a rule introducing the formula on which we cut. We first reduce in the same way all cut-rules in the branch of the cut-rule not containing $s$, yielding $\varpi_1$ from $\pi_1$ through $\pi_1 \xrightarrow{\bar{\beta}^*} \varpi_1$ and $\varpi_7$ from $\pi_3$ through $\pi_3 \xrightarrow{\bar{\beta}^*} \varpi_7$; they share this sub-proof, and we use the strong normalization of $\xrightarrow{\beta}$ (Lemma 70). Denote by $s^\perp$ the rule introducing the dual formula of $s$ (i.e. the other formula on which we cut), and by $\rho$ the rules in $\varpi_1$ (and $\varpi_3$) between $s^\perp$ and the cut-rule. By commuting the cut-rule above all rules in $\rho$, we have $\varpi_1 \xrightarrow{\bar{\beta}^*} \varpi_2$ with $\varpi_2$ having the cut-rule between $s$ and $s^\perp$. Doing the same commutations
**Lemma 73.** Let $\pi_t, \pi_l$ and $\pi_r$ be MALL proofs such that $\pi_l \stackrel{\bar{\beta}}{\leftarrow} \pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_r$. Then there exist $\varpi_l$ and $\varpi_r$ such that $\pi_l \stackrel{\beta^*}{\rightarrow} \varpi_l =_c^* \varpi_r \stackrel{\bar{\beta}^*}{\leftarrow} \pi_r$ (diagrammatically represented on Figure 16). Furthermore, the sequence $\varpi_l =_c^* \varpi_r$ contains proofs of measure at most $\max(|\pi_l|, |\pi_r|)$.

**Proof.** This proof is similar to the one of Lemma 72. In all cases, the exhibited sequence $=^*_c$ will have length 0 or 1, thus the result on measures will follow by Lemma 69.

If the $\pi_l \stackrel{\bar{\beta}}{\leftarrow} \pi_t$ and $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ steps involve only distinct rules then, taking into account that rules of one may be duplicated or erased by the other step, we have a proof $\varpi$ such that $\pi_l \stackrel{\beta^*}{\rightarrow} \varpi \stackrel{\bar{\beta}^*}{\leftarrow} \pi_r$. From now on, we assume not to be in this case, meaning both steps involve (at least) one common rule. We distinguish cases according to the kinds of the $\stackrel{\bar{\beta}}{\rightarrow}$ steps.

**If both steps are key or $\top$-cut commutative cases.** As the two reductions share a rule, it must be the cut-rule. If $\pi_l = \pi_r$ we are done, otherwise we have above this cut rule two rules of kind $ax$ or $\top$. We can check that each of these critical pairs leads to the same resulting proof from any choice of cut-elimination, unless both cases are $\top$-cut commutative cases, in which case the results are equal up to a $\top$-$\top$ commutation. Thus $\pi_l = \pi_r$ or $\pi_l =_c \pi_r$.

**If one step is a key or $\top$-cut commutative step and the other a commutative step other than $\top$-cut.** By symmetry, assume $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ is the key or $\top$-cut step. If the cut-rules involved in these cases are distinct, then doing the commutative step cannot prevent doing the key one, so both steps commute and we have a proof $\varpi$ such that $\pi_l \stackrel{\beta^*}{\rightarrow} \varpi \stackrel{\bar{\beta}^*}{\leftarrow} \pi_r$ (taking into account that rules of one may be duplicated or erased by the other step).

Now, assume both reductions involve a same cut-rule. The key case must be an $ax$ key case or a $\top$-cut commutative case, for otherwise the commutative step cannot share a rule with it (because the commutative step cannot be a cut-cut case). We can still do this key step after the commutation (maybe twice in case of duplication), recovering $\pi_r$ if it is an $ax$-key case or a proof equal to a $\top$-commutation in the $\top$-cut case (we need the $\top$-rule to absorb with the rule sent below the cut-rule during the commutative step). Thus:

- $\pi_l \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ ($ax$-key case and not a $\&$-cut commutative case)

- $\pi_l \stackrel{\bar{\beta}}{\rightarrow} \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ ($ax$-key case and $\&$-cut commutative case)

- $\pi_l \stackrel{\bar{\beta}}{\rightarrow} =_c \pi_r$ ($\top$-cut commutative case and not a $\&$-cut commutative case)

- $\pi_l \stackrel{\bar{\beta}}{\rightarrow} \stackrel{\bar{\beta}}{\rightarrow} =_c \pi_r$ ($\top$-cut commutative case and $\&$-cut commutative case)

**If both steps are not key nor $\top$-cut commutative steps.** Here again, as the two reductions share a rule, it must be the cut-rule. If $\pi_l \neq \pi_r$, then in $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_l$ we sent a rule from a branch of the cut below it, and in $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ we do similarly on the other branch. We can do the commutation of $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_r$ in $\pi_l$, and similarly the one of $\pi_t \stackrel{\bar{\beta}}{\rightarrow} \pi_l$ in $\pi_r$ (maybe twice in case of a duplication). The two resulting proofs differ exactly by the order of the two rules below the cut-rule, so are equal up to a commutation of these rules (which are not $\top$-rules by hypothesis). Thus, $\pi_l = \pi_r$ or $\pi_l \stackrel{\beta^*}{\rightarrow} =_c \pi_r \stackrel{\bar{\beta}^*}{\leftarrow} \pi_r$. ◀

**Lemma 74.** Let $\pi_1, \pi_2$ and $\pi_3$ be proofs such that $\pi_1 \sim_c \pi_2 \stackrel{\bar{\beta}}{\rightarrow} \pi_3$. Then there exist $\varpi_1$ and $\varpi_2$ such that $\pi_1 \stackrel{\bar{\beta}}{\rightarrow} \varpi_1 \stackrel{\beta^*}{\rightarrow} \varpi_2 \stackrel{\bar{\beta}^*}{\leftarrow} \pi_3$ (diagrammatically represented on Figure 16).

**Proof.** Remember a *block* of cut-rules is a maximal set of cut-rules in a proof such that all of these rules are a premise of another rule in the set, or use as premise the conclusion of
a rule in the set (Definition 68). We begin by observing that two *cut – cut* commutations in different blocks always commute (remark a *cut – cut* commutation cannot duplicate nor erase a sub-proof). Call $\mathfrak{B}$ the block containing the (unique) *cut*-rule $c$ of $\pi_2$ involved in $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$. This allows to decompose $\pi_1 \sim_c \pi_2$ into $\pi_1 \sim_c \mathfrak{B}_0, \bar{\omega}_1 \sim_c \mathfrak{B}_1, \bar{\omega}_2 \dots \bar{\omega}_n \sim_c \mathfrak{B}_n, \pi_2$, with $\sim_c \mathfrak{B}_i$ composed uniquely of *cut – cut* commutations between rules of a same block $\mathfrak{B}_i$, all $\mathfrak{B}_i$ being disjoint and different from $\mathfrak{B}$, except $\mathfrak{B}_0 = \mathfrak{B}$ (we can always add an empty sequence of commutations if needed).

Given commutations in another block $\mathfrak{B}'$ than $\mathfrak{B}$, if $\rho \sim_c \mathfrak{B}'$ $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ then there exists $\rho'$ such that $\rho \xrightarrow{\bar{\beta}} \rho' \sim_c \mathfrak{B}'$ $\pi_3$. Indeed, no commutation in $\rho \sim_c \mathfrak{B}'$ $\pi_2$ involves a rule of the $\xrightarrow{\bar{\beta}}$ step. If the $\xrightarrow{\bar{\beta}}$ step does not erase nor duplicate a sub-proof containing the block $\mathfrak{B}'$, then we have the result by first doing the $\xrightarrow{\bar{\beta}}$ step, then commutations of $\sim_c \mathfrak{B}'$. If the $\xrightarrow{\bar{\beta}}$ step erases the block $\mathfrak{B}'$, then $\rho \xrightarrow{\bar{\beta}} \pi_3$, which is a particular case of the previous one with $\sim_c \mathfrak{B}'$ being equality. Finally, if $\xrightarrow{\bar{\beta}}$ duplicates $\mathfrak{B}'$, then we need to do each *cut – cut* commutation twice to recover $\pi_3$. Thus, applying this reasoning successively on blocks $\mathfrak{B}_i$ from $\mathfrak{B}_n$ to $\mathfrak{B}_1$ yields $\pi_1 \sim_c \mathfrak{B}_0, \bar{\omega}_1 \xrightarrow{\bar{\beta}} \pi_3' \sim_c \mathfrak{B}_1, \bar{\omega}_2' \dots \bar{\omega}_n' \sim_c \mathfrak{B}_n, \pi_3$. It suffices now to prove there exist $\kappa$ and $\kappa'$ such that $\pi_1 \xrightarrow{\bar{\beta}} \kappa \xrightarrow{\beta^*} \kappa' \xleftarrow{\beta^*} \pi_3'$. Indeed, seeing $\sim_c$ as a particular case of $\xrightarrow{\beta^*}$ allows to have $\pi_3' \xleftarrow{\beta^*} \pi_3$, leading to the conclusion.

Whence, we consider proofs such that $\pi_1 \sim_c \mathfrak{B}$ $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ where $\xrightarrow{\bar{\beta}}$ involves a *cut*-rule in the block $\mathfrak{B}$, and prove there exist $\kappa$ and $\kappa'$ such that $\pi_1 \xrightarrow{\bar{\beta}} \kappa \xrightarrow{\beta^*} \kappa' \xleftarrow{\beta^*} \pi_3$. Call $r$ one of the non-*cut*-rules involved in $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ (i.e. another rule than $c$). In $\pi_1$, there is a *cut*-rule $c_0$ below $r$, belonging to $\mathfrak{B}$. If $c_0 = c$ and this result holds for all possible choices of $r$, then we can first do $\xrightarrow{\bar{\beta}}$ in $\pi_1$, then *cut – cut* commutations inside the rest of the block $\mathfrak{B}$ to obtain $\pi_3$: we have $\pi_1 \xrightarrow{\bar{\beta}} \cdot \xrightarrow{\beta^*} \pi_3$, and we are done. Thus, assume we choose an $r$ such that $c_0 \neq c$.

If $r$ and $c_0$ commute (with a commutative $\xrightarrow{\bar{\beta}}$ step), then we can do this commutation, yielding some proof $\kappa$ from $\pi_1$. We can then commute *cut*-rules to bring $c$ below $r$ and execute the corresponding $\xrightarrow{\bar{\beta}}$ step, yielding some proof $\kappa'$. Observe then that in $\pi_3$ commuting the rule $c_0$ up until reaching $r$, then commuting it up with $r$ and with $c_0$ (or instead with any *cut*-rules created by the $\xrightarrow{\bar{\beta}}$ step between $c$ and $r$ if it is a key or $\perp$-*cut* commutative step) yields $\kappa'$. We then have $\pi_1 \xrightarrow{\bar{\beta}} \kappa \xrightarrow{\beta^*} \kappa' \xleftarrow{\beta^*} \pi_3$.

Suppose now that $r$ and $c_0$ do not commute. This means $r$ is a rule introducing the formula $A_0$ on which $c_0$ cuts. This also implies that the $\pi_2 \xrightarrow{\bar{\beta}} \pi_3$ is not a key step, because $r$ cannot introduce the formula $A$ on which $c$ cuts. Call $\rho$ the sub-proof of $\pi_1$ above $c_0$ in the branch not leading to $r$. This is also the sub-proof of $\pi_3$ above $c_0$ in the same branch, up to bringing $c_0$ on top of the block $\mathfrak{B}$ by some $\xrightarrow{\beta^*}$ steps first ($c$ does not belong to this branch as it commuted with $r$). We reduce all *cut*-rules in $\rho$ using only $\xrightarrow{\bar{\beta}}$ steps (using Lemma 70), in the same way in both $\pi_1$ and $\pi_3$, obtaining a cut-free proof $\rho'$, in $\pi_1'$ and $\pi_3'$ respectively. In particular, we have $\pi_1 \xrightarrow{\beta^*} \pi_1'$ and $\pi_3 \xrightarrow{\beta^*} \pi_3'$.

Call $r^{\perp}$ the rule in $\rho'$ introducing the formula $A_0^{\perp}$ (which is a rule of the main connective of $A^{\perp}$ or an $ax$ or $\perp$-rule), and $\tau$ the sequence of rules in $\rho'$ between $c_0$ and $r^{\perp}$. We commute in $\pi_1'$ (resp. $\pi_3'$) rules of $\tau$ with $c_0$, yielding $\pi_1' \xrightarrow{\beta^*} \pi_1''$ (resp. $\pi_3' \xrightarrow{\beta^*} \pi_3''$) as $\tau$ is cut-free, obtaining a proof with $c_0$ having on its premises rules $r$ and $r^{\perp}$.

We can now apply a key or $\perp$-*cut* commutative case on $c_0$, yielding $\pi_1'' \xrightarrow{\bar{\beta}} \pi_1'''$ and
<figure><img src="image_36.png" /></figure>

<figure><img src="image_37.png" /><figcaption>**Figure 17** Diagram of the case $n \neq \emptyset$ and $k = 0$ in the proof of Proposition 75
Hypotheses are depicted in black; in red is an application of Lemma 74; in green of Lemma 73; blue parts correspond to using the induction hypothesis on the underlined proofs along to Lemma 70.</figcaption></figure>

$\pi_3'' \xrightarrow{\bar{\beta}} \pi_3'''$. Observe that $\pi_1'''$ and $\pi_3'''$ differ only by the fact that in $\pi_1'''$ the cut-rule $c$ is below, in the block $\mathfrak{B}$, while it is above the rules created by the key case on $c_0$ (or erased if it was $\top$ - cut commutative case) in $\pi_3'''$. We can commute it up in $\mathfrak{B}$ in $\pi_1'''$, then commute it with any rules created by the case on $c_0$ to recover $\pi_3'''$. Whence $\pi_1 \xrightarrow{\bar{\beta}^*} \pi_1' \xrightarrow{\bar{\beta}^*} \pi_1'' \xrightarrow{\bar{\beta}} \pi_1''' \xrightarrow{\beta^*} \pi_3''' \xleftarrow{\bar{\beta}} \pi_3'' \xleftarrow{\bar{\beta}^*} \pi_3' \xleftarrow{\bar{\beta}^*} \pi_3$, and in particular $\pi_1 \xrightarrow{\bar{\beta}} \cdot \xrightarrow{\beta^*} \pi_3''' \xleftarrow{\beta^*} \pi_3$. ◀

**Proposition 75.** Let $\pi$ and $\varpi$ be proofs such that $\pi =_c^* \varpi$. For any normal form $\pi'$ (resp. $\varpi'$) for cut-elimination of $\pi$ (resp. $\varpi$), $\pi' =_c^* \varpi'$.

**Proof.** We denote by $n$ the maximum of the measures of the proofs on the sequence $\pi =_c^* \varpi$, and $k$ the length of this sequence (i.e. its number of proofs minus 1). We prove the result by induction on the lexicographic order of $(n, k)$.

If $n = \emptyset$, then $\pi$ and $\varpi$ are cut-free, thus their only normal form are themselves and $\pi =_c^* \varpi$. Thus, assume from now on that $n > \emptyset$, thus $\pi$ has a cut and therefore $\varpi$ has a cut too (as $=_c$ preserves having a cut-rule).

Assume $k = 0$, and take $\pi'$ (resp. $\varpi'$) a normal form of $\pi$ (resp. $\varpi$). Therefore, $\pi' \stackrel{\beta^*}{\leftarrow} \pi = \varpi \stackrel{\beta^*}{\rightarrow} \varpi'$. As $n \neq \emptyset$, one of the $\xrightarrow{\beta}$ step in $\pi \xrightarrow{\beta^*} \pi'$ (resp. $\pi \xrightarrow{\beta^*} \varpi'$) is a $\xrightarrow{\bar{\beta}}$ step. Consider a sequence leading to the first such $\xrightarrow{\bar{\beta}}$ step: we have $\pi' \stackrel{\beta^*}{\leftarrow} \rho' \stackrel{\bar{\beta}}{\rightarrow} \rho \sim_c \pi \sim_c \kappa \xrightarrow{\bar{\beta}} \kappa' \xrightarrow{\beta^*} \varpi'$, thus $\pi' \stackrel{\beta^*}{\leftarrow} \rho' \stackrel{\bar{\beta}}{\rightarrow} \rho \sim_c \kappa \xrightarrow{\bar{\beta}} \kappa' \xrightarrow{\beta^*} \varpi'$. The reasoning we will do is illustrated on the diagram of Figure 17. Proving the result for $\rho'$ and $\kappa'$ is enough to yield $\pi' =_c^* \varpi'$. Applying Lemma 74, $\rho' \xrightarrow{\beta^*} \iota_1 \stackrel{\beta^*}{\leftarrow} \iota_3 \xrightarrow{\bar{\beta}} \iota_4 =_c^* \iota_5 \stackrel{\beta^*}{\leftarrow} \kappa'$, with proofs in $\iota_4 =_c^* \iota_5$ of measure at most $\max(|\iota_3|, |\kappa'|)$. However, $n = |\pi| = |\kappa| > |\kappa'|$, $n = |\rho| > |\rho'|$ and $n = |\kappa| > |\iota_3|$ by Lemma 69. Therefore, $n > \max(|\iota_3|, |\kappa'|)$ and the sequence $\iota_4 =_c^* \iota_5$ has proofs of measures strictly smaller than $n$, and $\rho'$, $\kappa'$ and $\iota_3$ are sequences of null length of measure strictly smaller than $n$. By induction hypothesis, we obtain that normal forms of $\iota_4$ and $\iota_5$ are related by $=_c^*$, and similarly between normal forms of $\rho'$, between normal forms of $\kappa'$ and between normal forms of $\iota_3$. But normal forms of $\iota_5$ are included in normal forms of $\kappa'$, those of $\iota_4$ in those of $\iota_3$, and those of $\iota_1$ in those of $\rho'$ and $\iota_3$. Therefore, by taking a normal form $\iota'_i$ of $\iota_i$ through Lemma 70, we have $\pi' =_c^* \iota'_1$ as normal forms of $\rho'$ are equal up to $=_c^* \iota'_1 =_c^* \iota'_4$ as normal forms of $\iota_3$ are equal up to $=_c^* \iota'_4 =_c^* \iota'_5$ as normal forms of $\iota_4$ and those of $\iota_3$ are equal up to $=_c^* \iota'_5 =_c^* \varpi'$.
<figure><img src="image_38.png" /><figcaption>Figure 18 Diagram of the case $n \neq \emptyset$ and $k = 1$ in the proof of Proposition 75</figcaption></figure>

Hypotheses are depicted in black; in red is an application of Lemma 74; in green of Lemma 72; blue parts correspond to using the induction hypothesis on the underlined proofs along to Lemma 70.

as normal forms of $\kappa'$ are equal up to $=^*_c$. Therefore, $\pi' =^*_c \iota'_1 =^*_c \iota'_4 =^*_c \iota'_5 =^*_c \bar{\omega}'$ and we conclude $\pi' =^*_c \bar{\omega}'$.

Suppose now that $k = 1$, thus $\pi =_c \bar{\omega}$. Take $\pi'$ (resp. $\bar{\omega}'$) a normal form of $\pi$ (resp. $\bar{\omega}$). As $n \neq \emptyset$, one of the $\xrightarrow{\beta}$ step in $\pi \xrightarrow{\beta^*} \pi'$ is a $\xrightarrow{\bar{\beta}}$ step. We set $\pi \sim_c \rho \xrightarrow{\bar{\beta}} \rho' \xrightarrow{\beta^*} \pi'$. A diagram representing the proof of this case is depicted on Figure 18. Applying Lemma 74, $\rho' \xrightarrow{\beta^*} \iota_1 \xleftarrow{\beta^*} \iota_2 \xleftarrow{\bar{\beta}} \pi$. We then use Lemma 72 to have $\iota_2 \xrightarrow{\bar{\beta}^*} \iota_3 =^*_c \iota_4 \xleftarrow{\beta^*} \bar{\omega}$, with the sequence $\iota_3 =^*_c \iota_4$ having proofs of measure strictly smaller than $\max(|\pi|, |\bar{\omega}|) \le n$. By Lemma 69, $|\rho'| < |\rho| = |\pi|$ and $|\iota_2| < |\pi| \le n$. Furthermore, $\bar{\omega}$ can be seen as an empty sequence of $\bar{\omega} =^*_c \bar{\omega}$ of measure at most $n$. By induction hypothesis, we obtain that normal forms of $\iota_3$ and $\iota_4$ are related by $=^*_c$, and similarly between normal forms of $\rho'$, between normal forms of $\iota_2$ and between normal forms of $\bar{\omega}$. But normal forms of $\iota_1$ are included in normal forms of $\rho'$ and of $\iota_2$, those of $\iota_3$ in those of $\iota_2$, and those of $\iota_4$ in those of $\bar{\omega}$. Therefore, by taking a normal form $\iota'_i$ of $\iota_i$ through Lemma 70, we have $\pi' =^*_c \iota'_1$ as normal forms of $\rho'$ are equal up to $=^*_c$, $\iota'_1 =^*_c \iota'_3$ as normal forms of $\iota_2$ are equal up to $=^*_c$, $\iota'_3 =^*_c \iota'_4$ as normal forms of $\iota_3$ and those of $\iota_4$ are equal up to $=^*_c$, $\iota'_4 =^*_c \bar{\omega}'$ as normal forms of $\bar{\omega}$ are equal up to $=^*_c$. Therefore, $\pi' =^*_c \iota'_1 =^*_c \iota'_3 =^*_c \iota'_4 =^*_c \bar{\omega}'$ and we conclude $\pi' =^*_c \bar{\omega}'$.

Lastly, we have $k > 1$. We have $\pi =_c \rho =^*_c \bar{\omega}$. Take $\pi'$ (resp. $\rho'$, $\bar{\omega}'$) a normal form of $\pi$ (resp. $\rho$, $\bar{\omega}$) (Lemma 70). By induction hypothesis on $\rho =^*_c \bar{\omega}$ of length $k-1$ and maximum measure at most $n$, it follows that $\rho' =^*_c \bar{\omega}'$. Similarly on $\pi =_c \rho$ of length $1 < k$ and maximum measure at most $n$, we obtain $\pi' =^*_c \rho'$. Thus, $\pi' =^*_c \bar{\omega}'$. $\quad \blacksquare$

**Theorem 34 (Confluence up to rule commutations).** If $\pi_1$ and $\pi_2$ are cut-free proofs obtained by cut-elimination from the same proof $\pi$, then $\pi_1$ and $\pi_2$ are equal up to rule commutations.

*Proof.* This is a particular case of Proposition 75 with $\pi = \bar{\omega}$.

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

**Theorem 35.** Let $\pi$ and $\bar{\omega}$ be $\beta\eta$-equal MALL proofs. Then, letting $\pi'$ (resp. $\bar{\omega}'$) be a result of expanding all axioms and then eliminating all cuts in $\pi$ (resp. $\bar{\omega}$), $\pi'$ is equal to $\bar{\omega}'$ up to rule commutations.

*Proof.* We have $\pi =_{\beta\eta} \bar{\omega}$, so $\eta(\pi) =_{\beta} \eta(\bar{\omega})$ by Proposition 4. This sequence can be decomposed into $\eta(\pi) = \mu_0 \xleftarrow{\beta^*} \nu_1 \xrightarrow{\beta^*} \mu_1 \xleftarrow{\beta^*} \nu_2 \xrightarrow{\beta^*} \mu_2 \xleftarrow{\beta^*} \nu_3 \dots \nu_n \xrightarrow{\beta^*} \mu_n = \eta(\bar{\omega})$ for some proofs $\nu_i$ and $\mu_i$. Each $\mu_i$ has a normal form $\mu'_i$ (by Lemma 70, choosing $\mu'_0 = \pi'$ and $\mu'_n = \bar{\omega}'$). Theorem 34 applied to $\nu_i$ yields $\mu'_{i-1} =^*_c \mu'_i$, see the diagram on Figure 19. Thence $\pi' = \mu'_0 =^*_c \mu'_n = \bar{\omega}'$. $\quad \blacksquare$

<figure><img src="image_40.png" /></figure>
<figure><img src="image_41.png" /></figure>

<figure><img src="image_42.png" /><figcaption>Figure 19 Diagram of the proof of Theorem 35
In black are hypotheses; in blue are applications of Lemma 70; in red are uses of Theorem 34.</figcaption></figure>

## D.2 Proof of Proposition 36

**Proposition 36.** Let $\pi$ be a proof equal, up to rule commutations, to $\text{id}_A$ with $A$ distributed. The $\top$-rules of $\pi$ are of the shape $\vdash\top, 0\top$ (with $\top$ in $A$ being the dual of $0$ in $A^\perp$, or vice-versa) and $\bot$-rules and $1$-rules come by pairs separated with $\oplus_i$-rules only, called a $1/\oplus/\bot$-pattern: $$ \frac{\frac{\vdash 1}{\vdash\top, F} \rho}{\vdash\bot, F} \bot $$ where $\rho$ is a sequence of $\oplus_i$-rules (with $\bot$ in $A$ being the dual of $1$ in $A^\perp$, or vice-versa). Moreover, there are no sequent in $\pi$ of the shape $\vdash B \& C$.

**Proof.** We prove a stronger property: any sequent $S$ of a proof $\pi$ obtained through a sequence of rule commutations of cut-free MALL from $\text{id}_A$ for a distributed formula $A$ respects:

(1) the formulas of $S$ are distributed;

(2) if $\top$ is a formula of $S$, then $S = \vdash\top, 0$;

(3) if $\bot$ is a formula of $S$, then $S = \vdash\bot, F$ with $F$ given by the following grammar $F := 1 \mid F \oplus D \mid D \oplus F$, where the distinguished $1$ is the dual of $\bot$ in $A^\perp$ if $\bot$ a sub-formula of $A$ (or vice-versa), $D$ is any formula, and the sub-proof of $\pi$ above $S$ is a sequence of $\oplus_i$ rules leading to the distinguished $1$;

(4) if $B \& C$ is a formula of $S$, then $S = \vdash B \& C, F$ with $F$ given by the following grammar $F := C^\perp \oplus B^\perp \mid F \oplus D \mid D \oplus F$, where the distinguished $C^\perp \oplus B^\perp$ is the dual of $B \& C$ in $A^\perp$ if $B \& C$ a sub-formula of $A$ (or vice-versa), $D$ is any formula, and in the sub-proof of $\pi$ above $S$ the $\oplus$-rules of the distinguished $C^\perp \oplus B^\perp$ are a $\oplus_2$-rule in the left-branch of the $\&$-rule of $B \& C$, and a $\oplus_1$-rule in its right branch;

(5) if $S$ contains several negative formulas or several positive formulas, then its negative formulas are $\mathfrak{A}$-formulas.

Remark that (5) is a corollary of properties (2), (3) and (4). As we have in $=c$ no commutations with a *cut-rule* (in particular no *cut* — $\top$ commutation) and no $\top - \otimes$ commutation creating a sub-proof with a *cut-rule*, it follows $\pi$ is cut-free and has the sub-formula property, making (1) trivially true. We will prove that the fully expanded axiom respects properties (2), (3) and (4), and that they are preserved by any rule commutation of $=c$.

**The fully expanded axiom respects the properties** We prove it by induction on the distributed formula $A$. Notice that sub-formulas of $A$ are also distributed. By symmetry, assume $A$ is positive.

If $A \in \{X, 1, 0\}$ where $X$ is an atom, then:

$$ \text{id}_A \in \left\{ \vdash X^\perp, X \mid ax ; \frac{\vdash 1}{\vdash\bot, 1} \bot ; \frac{\vdash\top, 0}{\vdash\top, 0\top} \right\} $$

Each of these proofs respects (2), (3) and (4).

Assume the result holds for $B$ and $C$, and that $A = B \otimes C$. The proof $\text{id}_A$ is:
$$ \frac{\frac{\mathrm{id}_B}{\vdash B^{\perp}, B} \quad \frac{\mathrm{id}_C}{\vdash C^{\perp}, C} \quad \bigcirc} {\frac{\vdash B^{\perp}, C^{\perp}, B \otimes C}{\vdash B^{\perp}, \mathfrak{N} C^{\perp}, B \otimes C}} \mathfrak{N} $$

We have to prove the sequents $\vdash B^{\perp}, C^{\perp}, B \otimes C$ and $\vdash B^{\perp}, \mathfrak{N} C^{\perp}, B \otimes C$ respect the properties. The latter respects (2), (3) and (4) trivially for its has neither a $\top$, $\perp$ nor & formula. As $B^{\perp}, \mathfrak{N} C^{\perp}$ is distributed, it follows that neither $B^{\perp}$ not $C^{\perp}$ can be a $\top$, $\perp$ or & formula, and as such the former sequent also respects the properties.

Suppose $A = B \oplus C$ with sequents of $B$ and $C$ respecting the properties. Now, $\mathrm{id}_A$ is:

$$ \frac{\frac{\mathrm{id}_C}{\vdash C^{\perp}, C} \quad \frac{\mathrm{id}_B}{\vdash B^{\perp}, B} \quad \bigcirc_1} {\vdash C^{\perp}, B \oplus C \oplus_2 \quad \vdash B^{\perp}, B \oplus C} \& $$

The sequent $\vdash C^{\perp} \& B^{\perp}, B \oplus C$ respects (2), (3) and (4), as the $\oplus$ is the dual of the $\&$. By symmetry, we show the properties are also fulfilled by $\vdash B^{\perp}, B \oplus C$, and they will be respected by $\vdash C^{\perp}, B \oplus C$ with a similar proof. As the formulas are distributed, $B^{\perp}$ cannot be a $\top$ formula. If $B^{\perp}$ is not a $\perp$ nor & formulas, then (2), (3) and (4) hold for $\vdash B^{\perp}, B \oplus C$. If it is, then using that $\vdash B^{\perp}, B$ respects (3) and (4), it follows that in $B \oplus C$ is also of the required shape, as $B$ was.

**Every possible rule commutation preserves the properties** We show it for each rule commutation, using every time the notations from Tables 6 and 7 in Definition 42, on Pages 22 and 21. By symmetry, we treat only one case for $\otimes - \otimes, \mathfrak{N} - \otimes, \& - \otimes$ and $\oplus_i - \otimes$ commutations.

**$\top$-commutations** Using properties (1) and (2), we cannot do any commutation between a $\top$-rule and a $\mathfrak{N}, \otimes, \&$, $\oplus_i, \perp$ or $\top$-rule, so no commutations at all involving a $\top$-rule (we supposed to not consider commutations with cut-rules exactly for this case).

**$\perp$-commutations** Using properties (1) and (3), we cannot do any commutation between a $\perp$-rule and a $\mathfrak{N}, \otimes, \&$ or $\perp$-rule. A commutation between a $\perp$ and a $\oplus_i$-rule preserves property (3): we have by hypothesis $\Gamma$ empty and $A_1 \oplus A_2$ of the right shape. It also respects (2) and (4) trivially.

**$C^{\mathfrak{N}}$ commutation** We have to show the properties for $\vdash A_1, A_2, B_1, \mathfrak{N} B_2, \Gamma$. As $\vdash A_1, \mathfrak{N} A_2, B_1, \mathfrak{N} B_2, \Gamma$ respects them, negative formulas of $\Gamma$ are $\mathfrak{N}$-formulas by (5). By distributivity, if $A_1$ (or $A_2$) is a negative formula, then it must be a $\mathfrak{N}$ one. Thus, $\vdash A_1, A_2, B_1, \mathfrak{N} B_2, \Gamma$ fulfills (2), (3) and (4).

**$C^{\oplus_i}$ commutation** We have to show the properties for $\vdash A_i, B_1 \oplus B_2, \Gamma$. As $\vdash A_1 \oplus A_2, B_1 \oplus B_2, \Gamma$ respects them, negative formulas of $\Gamma$ are $\mathfrak{N}$-formulas by (5). If $A_i$ is positive or a $\mathfrak{N}$, then we are done. Otherwise, as $\vdash A_i, B_j, \Gamma$ fulfills the properties, it follows $\Gamma$ is empty and $B_j$ of the desired shape. By (1), $B_j$ is not 0, thus $A_i$ is not $\top$. Whether $A_i$ is $\perp$ or $\&$, the sequent $\vdash A_i, B_1 \oplus B_2$ respects the properties.

**$C^{\otimes}$ commutation** We have to show the properties for $\vdash A_1 \otimes A_2, B_1, \Gamma, \Delta$. As $\vdash A_1 \otimes A_2, B_1 \otimes B_2, \Gamma, \Delta, \Sigma$ respects them, negative formulas of $\Gamma$ and $\Delta$ are $\mathfrak{N}$-formulas by (5). If $B_1$ is positive or a $\mathfrak{N}$, then we are done. Otherwise, as $\vdash A_2, B_1, \Delta$ fulfills the properties, it follows $\Delta$ is empty and $B_1$ of the desired shape, so $B_1$ is a 0, 1 or $\oplus$-formula. This is impossible as $B_1 \otimes B_2$ is distributed by (1).

**$C^{\&}, C^{\&}, C^{\mathfrak{N}}, C^{\&}, C^{\otimes}$ and $C^{\otimes}$ commutations** These cases are impossible by property (4).
is a failure since the selected sub-formulas of $A \oplus B$ and its dual do not match. Given two slices $s$ and $r$ with respective conclusions $\vdash A, \Gamma$ and $\vdash A^{\perp}, \Delta$, their composition by cut $s \underset{A}{\dashv} r$ reduces either to a slice or to a failure. Given two sets of slices $S_1$ (all with conclusion $\vdash A, \Gamma$) and $S_2$ (all with conclusion $\vdash A^{\perp}, \Gamma$), their composition $S_1 \underset{A}{\dashv} S_2$ is the set of all slices obtained by composing a slice in $S_1$ with a slice in $S_2$. Given a set of slices $S$, its normal form is the set of all cut-free slices obtained by reducing the cuts in the slices of $S$. This can give an empty set if all slices in $S$ lead to failures during reduction.

**Lemma 77.** Let $\pi_1$ and $\pi_2$ be cut-free proofs whose composition over $A$ reduces to a cut-free proof $\varpi$. The normal form of $S(\pi_1) \underset{A}{\dashv} S(\pi_2)$ is $S(\varpi)$. Moreover, for each $s \in S(\varpi)$, there exist $s_1 \in S(\pi_1)$ and $s_2 \in S(\pi_2)$ such that $s_1 \underset{A}{\dashv} s_2$ reduces to $s$, and $s_1$ and $s_2$ make dual choices on the additive connectives of $A$.

**Proof.** We can check that each cut-elimination steps preserves the set of slices. Moreover, if a slice is obtained by making distinct choices on the dual occurrences of an additive connective of a cut formula, then it reduces (in possibly many steps) to a failure. ◀

**Lemma 78.** Let $\pi_1$ and $\pi_2$ be cut-free proofs of $\vdash \Gamma$ with $\top$-rules only of the shape $\vdash \top, 0 \top$. Assume that $\pi_1 =_c^* \pi_2$, where in this sequence there are no rule commutations involving a $\top$-rule. Then for each slice $s_1 \in S(\pi_1)$, there exists a unique $s_2 \in S(\pi_2)$ such that $s_1$ and $s_2$ make the same choices for additive connectives in $\Gamma$.

**Proof.** This can be easily checked for each possible equation in $=_{c}$.

**Lemma 79.** Given a choice $C$ of premise for additive connectives of $A$ (but not $A^{\perp}$), there exists a unique slice of $S(id_A)$ on it, which furthermore makes on $A^{\perp}$ the dual choices of $C$.

**Proof.** Direct induction on $A$, following the definition of $id_A$ on Table 3. ◀

**Lemma 80.** Let $\pi$ and $\pi'$ be cut-free MALL proofs respectively of $\vdash A^{\perp}, B$ and $\vdash B^{\perp}, A$, whose composition over $A$ reduces to $id_B$ up to rule commutation. Set $\rho$ the proof obtained by eliminating all cuts in the composition of $\pi$ and $\pi'$ over $B$, without using any ax or $\perp - 1$ key case as well as $\top$-cut commutative case. Then for any slice $s$ of $\pi$, there exists a slice $s'$ of $\pi'$ such that $s \cup s'$ has the same 0-ary rules as a slice of $\rho$.

**Proof.** Take $s \in S(\pi)$, and denote by $C$ the choices made in $s$ on $\&$ and $\oplus$ connectives of the formula $B$. Any slice of $\rho$ has for 0-ary rules the ones of $r \cup r'$ for $r \in S(\pi)$ and $r' \in S(\pi')$ such that $r'$ makes choices on $B$ corresponding to the dual of those of $r$ on $B^{\perp}$ (using Lemma 77). Call $\rho'$ a cut-free proof resulting from cut-elimination of the composition of $\pi$ and $\pi'$ over $A$; by hypothesis, $\rho' =_c^* id_B$. By Lemma 79, there is a (unique) slice of $id_B$ with choices $C$ on $B$ and dual choices $C^{\perp}$ on $B^{\perp}$. Applying Proposition 36 and Lemma 78, there is a slice $r'$ of $\rho'$ with choices $C$ and $C^{\perp}$. According to Lemma 77, we have slices $t \in S(\pi)$ and $t' \in S(\pi')$ whose composition reduces to $r'$. In particular, $t$ makes choices $C$ on $B$ and $t'$ choices $C^{\perp}$ on $B^{\perp}$. Therefore, $t'$ makes on $B^{\perp}$ the dual choices of $s$ on $B$, and as such the composition of $s$ and $t'$ reduces to a slice of $\rho$. ◀

**Remark.** Lemma 80 is the analogue of Lemma 16 in sequent calculus.

Lemma 80 will be used to prove that $\& - \oplus_i$ key cases during cut-elimination do not erase 0-ary rules. More precisely, given $A \stackrel{\pi, \pi'}{\cong} B$ and considering a 0-ary rule $t$ (typically a $\top$- or 1-rule) in $\pi$, we use this lemma to say that $t$ is still in the reduction of $\pi \underset{A}{\dashv} \pi'$ before applying any ax, $\perp - 1$ or $\top$-cut case. This is done by taking a slice $t$ belongs to, then
finding an associated slice such that normalization of the composition is not a failure thanks
to the lemma, and thus the resulting slice belongs to the normal form.

**Lemma 37.** If $A^{\pi_2\pi'}B$ with $\pi$ and $\pi'$ cut-free then all $\top$-rules in $\pi$ and $\pi'$ are of the form $\vdash\top, 0\top$ and all $\bot$-rules and 1-rules belong to $1/\oplus/\bot$-patterns.

**Proof.** Consider $t$ a $\top$-rule $\vdash\Gamma, \Delta\top$ in $\pi$, with $\Gamma$ occurrences of sub-formulas of $A^\bot$ and $\Delta$ of $B$. Call $s$ the slice it belongs to. By Lemma 80 and Proposition 36, there exists $s' \in S(\pi')$ such that $s \bowtie^B s'$ reduces to a slice in which the only $\top$-rules are $\vdash\top, 0\top$ rules, with $\top$ being the dual occurrence of 0. Along the reduction, $t$ is either preserved and $\Gamma$ as well, or $t$ is absorbed by another $\top$-rule and $\Gamma$ stays in the context of a $\top$-rule. As in the resulting proof $\top$ and 0 are not both sub-formula of $A^\bot$, it follows $\Gamma$ is a subsequent of $\top$ or of 0. By symmetry (cutting on the other formula), $\Delta$ is too. Moreover, $\Gamma$ or $\Delta$ must contain a $\top$. Thus, $\top$-rules in $\pi$ are of the form $\vdash\top\top$, $\vdash\top, 0\top$ or $\vdash\top, \top$.

Assume there is a $\vdash\top\top$ rule in $\pi$, with $\top$ a sub-formula of $A^\bot$. Again it belongs to a slice whose reduction leads to a slice containing only $\top$-rules of the form $\vdash\top, 0\top$. This is not possible since the $\vdash\top\top$ rule cannot be absorbed by a $\top$-cut commutation for it has no context in $B$.

Suppose now there is a $\vdash\top, \top, \top$ rule in $\pi$. When such a rule is absorbed by another $\top$-rule in a $\top$-cut commutation, the resulting $\top$-rule still has (at least) two $\top$-formulas. But when reaching the normal form, we only have $\top$-rules with one $\top$-formula: contradiction. We conclude that all $\top$-rules in $\pi$ are of the form $\vdash\top, 0\top$.

We now prove the part of the lemma for $\bot$-rules. For this we will need the following result: (*) there are no sequent of the shape $\vdash D \& E$ in $\pi$. Assume w.l.o.g. $D \& E$ is a sub-formula of $A^\bot$, and let $s$ be a slice containing it (i.e. one of its two parts). By Lemma 80, there exists a slice $s' \in S(\pi')$ such that $s \bowtie^B s'$ reduces to a slice satisfying Proposition 36. Since $D \& E$ is a sub-formula of $A^\bot$, it is not cut and the rule $\&_i$ introducing $D \& E$ in $s$ remains in the normal form. This contradicts Proposition 36 since any $\&$-rule must have a non-empty context.

Set $F := 1 | F \oplus D | D \oplus F$ (with $D$ an arbitrary formula). In $\pi$, we look at a possible rule $r$ below a sequent $\vdash F$. It cannot be a $\otimes$-rule by distributivity, nor a $\aleph$-rule has the sequent has a unique formula, or a $\&$-rule due to (*). If $r$ is a $\oplus_i$-rule, then we keep a sequent $\vdash F$, and if it is a $\bot$-rule then it is one of the required shape.

As a consequence, each 1-rule is followed by some $\oplus_i$-rules and possibly a $\bot$-rule (let us call a $1/\oplus$-pattern a 1-rule followed by a maximal such sequence of $\oplus_i$-rules). If a $1/\oplus$-pattern stops without a $\bot$-rule below it, we have only one formula in the conclusion sequent of the proof: impossible as $\pi$ is a proof of $\vdash A^\bot, B$. Thus, the $\bot$-rule exists and to each 1-rule we can associate a $\bot$-rule leading to $1/\oplus/\bot$-pattern. Henceforth, there are at least as many $\bot$-rules as 1-rules.

Now, in the normal forms, the number of 1-rules is the same as the number of $\bot$-rules. Consider a $\bot$-rule $r$ which is erased during normalization by cut over $B$, and let $s$ be a slice containing it. By Lemma 80, there exists a slice $s' \in S(\pi')$ such that $s \bowtie^B s'$ reduces to a slice of the normal form. If $r$ disappears, it must be through a $\bot - 1$ key case which also erases a 1-rule (it cannot be through a $\top - cut$ commutative case as $\top$-rules are of the shape $\vdash\top, 0\top$). Furthermore, if we duplicate a 1-rule then it is on top of a $1/\oplus/\bot$-pattern and thus we duplicate a $\bot$-rule as well. As a consequence, (number of $\bot$-rules - number of 1-rules) can only increase during the reduction. We conclude the number of $\bot$-rules is equal to the number of 1-rules in $\pi$, and thus every $\bot$-rule belongs to a $1/\oplus/\bot$-pattern. $\quad$
## D.4 Proof of Theorem 38

**► Proposition 81.** Taking proofs $\pi$ and $\varpi$ such that $\pi =_c^* \varpi$, we have $\pi =_{\beta\eta} \varpi$.

*Proof.* By giving the reductions for each equality. For example:

$$ \frac{\frac{\pi}{\vdash A_1, A_2, B_1, B_2, \Gamma} \quad \frac{\overline{\vdash A_2^\perp, A_2}}{\overline{\vdash A_1^\perp, A_1}} ax \quad \frac{ax}{\vdash A_1^\perp, A_1} \otimes \overline{\vdash A_2^\perp \otimes A_1^\perp, A_1, A_2}}{\vdash A_1 \not\Vdash A_2, B_1 \not\Vdash B_2, \Gamma} \quad \frac{\not\Vdash \overline{\vdash A_2^\perp \otimes A_1^\perp, A_1 \not\Vdash A_2}}{\overline{\vdash A_1^\perp \otimes A_1^\perp, A_1 \not\Vdash A_2}} \not\Vdash \overline{\text{cut}}} \quad \vdash A_1 \not\Vdash A_2, B_1 \not\Vdash B_2, \Gamma $$

reduces to both

$$ \frac{\frac{\pi}{\vdash A_1, A_2, B_1, B_2, \Gamma} \quad \frac{\not\Vdash \overline{\vdash A_2, B_1, B_2, \Gamma}}{\vdash A_1 \not\Vdash A_2, B_1 \not\Vdash B_2, \Gamma} \not\Vdash} \quad \text{and} \quad \frac{\pi}{\vdash A_1, A_2, B_1, B_2, \Gamma} \quad \frac{\not\Vdash \overline{\vdash A_1, A_2, B_1 \not\Vdash B_2, \Gamma}}{\vdash A_1 \not\Vdash A_2, B_1 \not\Vdash B_2, \Gamma} \not\Vdash} $$

(according to whether the *cut-rule* is first commuted with the $\not\Vdash$-rule on its left or on its right), thus the $C_{\not\Vdash}^\gamma$ commutation is included in $=_{\beta}$. ◀

**► Theorem 38 (Isomorphisms completeness with units).** If $A \simeq B$ then $A =_\varepsilon B$.

*Proof.* We can assume $A$ and $B$ to be distributed (Proposition 21). As $A \simeq B$, there are proofs $\pi$ and $\varpi$ respectively of $\vdash A^\perp$, $B$ and $\vdash B^\perp$, $A$, whose composition over $B$ (resp. $A$) is equal to the axiom on $\vdash A^\perp$, $A$ (resp. $\vdash B^\perp$, $B$) up to $\beta\eta$-equality. We assume w.l.o.g. $\pi$ and $\varpi$ to be cut-free proofs, and work only with axiom-expanded proofs thanks to Proposition 4.

Using Theorem 35, we have $\pi \bowtie_B \varpi \xrightarrow{\beta^*} \cdot =_c^* \text{id}_A$ and $\pi \bowtie_A \varpi \xrightarrow{\beta^*} \cdot =_c^* \text{id}_B$. By Lemma 37, $\pi$ and $\varpi$ have $\top$-rules only of the shape $\overline{\vdash \top, 0}^\top$ and $\bot$ and 1-rules in $1/\oplus/\bot$-patterns. Using $\bot$-commutations to move each $\bot$-rule just below the 1-rule above it, we build $\pi'$ and $\varpi'$ such that $\pi'$ and $\varpi'$ have $\top$-rules only of the shape $\overline{\vdash \top, 0}^\top$, $\bot$ and 1-rules of the form $\overline{\vdash 1}^1 \bot$, $\pi =_c^* \pi'$ and $\varpi =_c^* \varpi'$. Whence, $\pi' \bowtie_B \varpi' =_c^* \pi \bowtie_A \varpi$ and $\pi' \bowtie_A \varpi' =_c^* \pi \bowtie_A \varpi$. By Theorem 35, for any normal form $\rho$ of $\pi' \bowtie_B \varpi'$ (resp. $\pi' \bowtie_A \varpi'$), $\rho =_c^* \text{id}_A$ (resp. $\rho =_c^* \text{id}_B$).

We reduce cuts in $\pi' \bowtie_B \varpi'$ (and similarly in $\pi' \bowtie_A \varpi'$) in the following way. First, observe that when a $\top$-rule is above a *cut-rule*, then it is necessarily in a $\frac{\overline{\vdash \top, 0}^\top}{\vdash \top, \Gamma}$ $\frac{\phi}{\vdash \top, \Gamma}$ cut sub-proof, that we can reduce into $\overline{\phi}{\overline{\vdash \top, \Gamma}}$ (because in this case $\phi = \overline{\vdash \top, 0}^\top$). Secondly, when a *cut-rule* has above one of its (let say left) premises a $\bot$-rule (necessarily with a 1-rule above, a property we are going to preserve through our reduction strategy):

■ If it is of the shape $\frac{\overline{\vdash 1}^1}{\vdash 1, \bot}$ $\bot$ $\frac{\phi}{\vdash 1, \Gamma}$ cut, we commute this *cut-rule* with the rules of $\phi$ until we reach the 1-rule introducing 1 and we reduce the obtained *cut-rule* $\frac{\overline{\vdash 1}^1}{\vdash 1, \bot}$ $\bot$ $\frac{\overline{\vdash 1}^1}{\vdash 1}$ cut into $\overline{\vdash 1}^1$. What we get is exactly $\phi$.
■ If it is of the shape $\frac{\overline{\vdash 1} 1}{\vdash \perp, 1} \perp \frac{\phi}{\vdash \perp, \Gamma} \text{ cut}$, we commute the cut-rule with the rules of $\phi$ until we reach the $\perp$-rule introducing $\perp$ and we reduce the obtained cut-rule $\frac{\overline{\vdash 1} 1}{\vdash \perp, 1} \perp \frac{\vdash \Delta}{\vdash \perp, \Delta} \perp \text{ cut}$ into $\frac{\vdash \Delta}{\vdash \perp, \Delta} \perp$ (with $\Delta = 1$). What we get is exactly $\phi$.

This strategy allows reaching a normal form $\rho$, with $\top$-rules only of the shape $\overline{\vdash \top, 0} \top$ and $\perp$ and 1-rules of the form $\frac{\overline{\vdash 1} 1}{\vdash \perp, 1} \perp$ (this is preserved by our strategy). Furthermore, call $\sigma$ the substitution replacing $\top, 0, \perp$ and 1-formulas respectively by $X^{\perp}, X, Y^{\perp}$ and $Y$, for $X$ and $Y$ fresh atoms. We can reach $\sigma(\rho)$ by cut-elimination from $\sigma(\pi')^{\sigma(B)} \bowtie \sigma(\pi')$, for the reductions we did on units could as well have been done by $ax$-key cases. Moreover, $\sigma(\mathrm{id}_A) = \mathrm{id}_{\sigma(A)}$, and in $\rho =_c^* \mathrm{id}_A$ we can assume not to commute any $\perp$-rule (for we start and end with 1-rules and $\perp$-rules in $\frac{\overline{\vdash 1} 1}{\vdash \perp, 1} \perp$ shapes only, and such commutations could only move the $\perp$-rule below or above some $\oplus_i$-rules according to Proposition 36). Thus, $\sigma(\rho) =_c^* \mathrm{id}_{\sigma(A)}$. Using Proposition 81, it follows $\sigma(\rho) =_{\beta\eta} \mathrm{id}_{\sigma(A)}$, and therefore $\sigma(\pi')^{\sigma(B)} \bowtie \sigma(\pi') =_{\beta\eta} \mathrm{ax}_{\sigma(A)}$ with $\mathrm{ax}_{\sigma(A)}$ the $ax$-rule on $\sigma(A)$. A similar result holding for a cut over $A$, we have $\sigma(A) \simeq \sigma(B)$, these formulas being unit-free. By Theorem 33, $\sigma(A) =_{\epsilon} \sigma(B)$. We conclude $A =_{\epsilon} B$ by substituting $X$ by 0 and $Y$ by 1 (as $X$ and $Y$ were fresh). ◀