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

HAL
open science

# Acyclicity and Coherence in Multiplicative Exponential Linear Logic

Michele Pagani

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

## To cite this version:

Michele Pagani. Acyclicity and Coherence in Multiplicative Exponential Linear Logic. Computer Science Logic. CSL 2006, EACSL, 2006, Szeged, Hungary. pp.531-545, 10.1007/11874683_35. hal-04670298

HAL Id: hal-04670298

https://hal.science/hal-04670298v1

Submitted on 12 Aug 2024

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Acyclicity and Coherence in Multiplicative Exponential Linear Logic
(Extended abstract with appendix)

Michele Pagani*

Dipartimento di Filosofia – Università Roma Tre
Via Ostiense 231 – 00124 – Roma
pagani@uniroma3.it

**Abstract.** We give a geometric condition that characterizes MELL proof structures whose interpretation is a clique in non-uniform coherent spaces: visible acyclicity.
We define the *visible paths* and we prove that the proof structures which have no visible cycles are exactly those whose interpretation is a clique.
It turns out that visible acyclicity has also nice computational properties, especially it is stable under cut reduction.

# 1 Introduction

Proof nets are a graph-theoretical presentation of linear logic proofs, that gives a more geometric account of logic and computation. Indeed, proof nets are in a wider set of graphs, that of *proof structures*. Specifically, proof nets are those proof structures which correspond to logically correct proofs, i.e. sequent calculus proofs.

A striking feature of the theory of proof nets is the characterization by ge-
ometric conditions of such a logical correctness. In multiplicative linear logic
(*MLL*) Danos and Regnier give (see [1]) a very simple correctness condition,
which consists in associating with any proof structure a set of subgraphs, called
*switchings*, and then in characterizing the proof nets as those structures whose
switchings are connected and acyclic.

Later Fleury and Retoré relax in [2] Danos-Regnier's condition, proving that acyclicity alone characterizes those structures which correspond to the proofs of *MLL* enlarged with the mix rule (Figure 4). More precisely, the authors define the *feasible paths* as those paths which are "feasible" in the switchings, then they prove that a proof structure is associated with a proof of *MLL* plus mix if and only if all its feasible paths are acyclic.

Proof structures are worthy since cut reduction is defined straight on them,
not only on proof nets. We can thus consider a concrete denotational semantics
for proof structures, as for example the relational semantics. Here the key notion
is that of *experiment*, introduced by Girard in [3]. Experiments allow to associate

<footnote>* This work has been partially supported by MIUR national project FOLLIA.</footnote>
with any proof structure (not only proof net) $\pi$ a set of points $[[\pi]]$ invariant under
the reduction of the cuts in $\pi$.

In [4] Bucciarelli and Ehrhard provide a notion of coherence between the
points of the relational semantics, so introducing *non-uniform coherent spaces*
and *non-uniform cliques*. Such spaces are called non-uniform since the web of
their exponentials does not depend on the coherence relation, as it does instead
in case of usual (uniform) coherent spaces (see [3]).<fnref n="1" />

Hence we have a geometrical notion – feasible acyclicity – dealing with logical
correctness, and a semantical one – clique – defined in the framework of coherent
spaces. Such notions are deeply related in *MLL*: from [3] it is known that for any
proof structure $\pi$, if $\pi$ is feasible acyclic then its interpretation $[[\pi]]$ is a clique;
conversely Retoré proves in [5] that for any cut-free $\pi$, if $[[\pi]]$ is a clique then $\pi$
is feasible acyclic.

Such results tighten the link between coherent spaces and multiplicative proof
nets: as a corollary we derive in [6] the full-completeness of coherent spaces for
*MLL* with mix.

What happens to this correspondence in presence of the exponentials, i.e. in
multiplicative exponential linear logic (*MELL*)?

The notion of feasible path can be easily extended to *MELL* (Definition 6). In this framework feasible acyclicity characterizes the proof structures which correspond to the proofs of *MELL* sequent calculus (Figure 3) enlarged with the rules of mix and daimon (Figure 4). However the link between feasible acyclicity and coherent spaces fails: there are proof structures which are associated with cliques even if they have feasible cycles (for example Figure 5).

The main novelty of our paper is to find out a geometrical condition on
*MELL* proof structures, which recovers the missed link with coherent spaces.
In Definition 7 we introduce the *visible paths*, which are an improvement of the
feasible paths in presence of exponentials. Then we prove in Theorems 9 and 10:

- for any *MELL* proof structure $\pi$, if $\pi$ is visible acyclic, then $[[\pi]]$ is a non-uniform clique;

- for any *MELL* cut-free proof structure $\pi$, if $[[\pi]]$ is a non-uniform clique then $\pi$ is visible acyclic.

Finally, it turns out that visible acyclicity has also nice computational proper-
ties, especially it is stable under cut reduction (Theorem 18), moreover it assures
confluence and strong normalization.

*Acknowledgments*. I would like to thank Lorenzo Tortora de Falco for his invaluable support and Paolo Di Giamberardino, whose Mémoire de D.E.A. has been the starting point of this work.

<footnote n="1">¹ Actually the difference between uniform and non-uniform spaces has a relevance only in presence of exponentials: in *MLL* we can speak simply of coherent spaces and cliques.</footnote>
## 2 Proof structures

The formulas of MELL are defined by the following grammar:

$$F ::= X | X^{\perp} | F \otimes F | F \otimes F | ?F | !F$$

As usual we set $(A \otimes B)^{\perp} = A^{\perp} \otimes B^{\perp}$, $(A \otimes B)^{\perp} = A^{\perp} \otimes B^{\perp}$, $(?F)^{\perp} = !F^{\perp}$ and $(!F)^{\perp} = ?F^{\perp}$. We denote by capital Greek letters $\Sigma, \Pi, \dots$ the multisets of formulas. We write $A_1 \odot \dots \odot A_{n-1} \odot A_n$ for $A_1 \odot (\dots \odot (A_{n-1} \odot A_n) \dots)$, where $\odot$ is $\otimes$ or $\otimes$.

Proof structures are directed graphs with boxes – highlighted subgraphs – and pending edges – edges without target. Edges are labeled by MELL formulas and nodes (called *links*) are labeled by MELL rules. Links are defined together with both an *arity* (the number of incident edges, called the *premises of the link*) and a *coarity* (the number of emergent edges, called the *conclusions of the link*). The links of MELL are $ax, cut, \otimes, \otimes, !, ?d, ?c, ?w$, as defined in Figure 1. The orientation of the edges will be always from top to bottom, so that we may omit the arrows of the edges.

<figure><img src="image_4.png" /><figcaption>Fig. 1. MELL links.</figcaption></figure>

**Definition 1 (Proof structure, [3]).** A proof structure $\pi$ is a directed graph whose nodes are MELL links and such that:

1. every edge is conclusion of exactly one link and premise of at most one link. The edges which are not premise of any link are the conclusions of the proof structure;

2. with every link $!o$ is associated a unique subgraph of $\pi$, denoted by $\pi^o$, satisfying condition 1 and such that one conclusion of $\pi^o$ is the premise of $o$ and all further conclusions of $\pi^o$ are labeled by $?-$formulas. $\pi^o$ is called the exponential box of $o$ (or simply the box of $o$) and it is represented by a dash frame. The conclusion of $o$ is called the principal door of $\pi^o$, the conclusions of $\pi^o$ labeled by $?-$formulas are called the auxiliary doors of $\pi^o$;
3. two exponential boxes are either disjoint or included one in the other.

The depth of a link in $\pi$ is the number of boxes in which it is contained. The depth of an edge $a$ is 0 in case $a$ is a conclusion of $\pi$, otherwise it is the depth of the link of which $a$ is premise.

The depth of $\pi$ is the maximum depth of its links, the size of $\pi$ is the number of its links, the cosize of $\pi$ is the number of its links ?c.

A link $l$ is terminal when either $l$ is $a$! and all the doors of $\pi^l$ are conclusions of $\pi$, or $l$ is not $a$! and all the conclusions of $l$ are conclusions of $\pi$.

Proof structures are denoted by Greek letters: $\pi, \sigma, \dots$, edges by initial Latin letters: $a, b, c, \dots$ and links by middle-position Latin letters: $l, m, n, o, \dots$. We write $a: A$ if $a$ is an edge labeled by the formula $A$.

A proof structure without cuts is called *cut-free*. The cut reduction rules are graph rewriting rules which modify a proof structure $\pi$, obtaining a proof structure $\pi'$ with the same conclusions as $\pi$. We do not give here the cut reduction rules, which are completely standard (see [3]). However we remark that at the level of proof structures there exist cuts, called *deadlocks*, which are irreducible. These are the cuts between the two premises of an axiom, and the cuts between two doors of an exponential box (see Figure 2).

<figure><img src="image_5.png" /><figcaption>**Fig. 2.** Examples of deadlocks.</figcaption></figure>

We denote by $\pi \rightsquigarrow \beta \pi'$ whenever $\pi'$ is the result of the reduction of a cut in $\pi$. As always, $\to_\beta$ is the reflexive and transitive closure of $\rightsquigarrow_\beta$ and $=_{\beta}$ is the symmetrical closure of $\to_\beta$.

# 3 Non-uniform coherent spaces

We recall that a *multiset* $v$ is a set of elements in which repetitions can occur. We denote multisets by square brackets, for example $[a, a, b]$ is the multiset containing twice $a$ and once $b$. The plus symbol $+$ denotes the disjoint union of multisets, whose neutral element is the empty multiset $\emptyset$. If $n$ is a number and $v$ a multiset, we denote by $nv$ the multiset $v + \dots + v$. The support of $v$, denoted by $\text{Supp}(v)$, is the set of elements of $v$, for example $\text{Supp}([a, a, b]) = \{a, b\}$.
If $\mathcal{C}$ is a set, by $M(\mathcal{C})$ (resp. $M_{fin}(\mathcal{C})$) we mean the set of all multisets (resp. finite multisets) of $\mathcal{C}$.

**Definition 2 (Non-uniform coherent space, [4]).** A non-uniform coherent space $\mathcal{X}$ is a triple $(|\mathcal{X}|, \mathcal{C}, \equiv)$, where $|\mathcal{X}|$ is a set, called the web of $\mathcal{X}$, while $\mathcal{C}$ and $\equiv$ are two binary symmetric relations on $|\mathcal{X}|$, such that for every $x, y \in \mathcal{X}$, $x \equiv y$ implies $x \mathcal{C} y$. $\mathcal{C}$ (resp. $\equiv$) is called the coherence (resp. the neutrality) of $\mathcal{X}$.

A clique of $\mathcal{X}$ is a subset $C$ of $|\mathcal{X}|$ such that for every $x, y \in C$, $x \mathcal{C} y$.

Remark the difference from Girard's (uniform) coherent spaces: we do not require the relation $\mathcal{C}$ to be also reflexive.

We will write $x \mathcal{C} y[\mathcal{X}]$ and $x \equiv y[\mathcal{X}]$ if we want to state explicitly which coherent space $\mathcal{C}$ and $\equiv$ refer to. We introduce the following notation, well-known in the framework of coherent spaces:

**strict coherence:** $x \mathcal{C} y[\mathcal{X}]$, if $x \mathcal{C} y[\mathcal{X}]$ and $x \not\equiv y[\mathcal{X}]$;

**incoherence:** $x \not\mathcal{C} y[\mathcal{X}]$, if not $x \mathcal{C} y[\mathcal{X}]$;

**strict incoherence:** $x \mathcal{C}^* y[\mathcal{X}]$, if $x \not\mathcal{C}^* y[\mathcal{X}]$ and $x \not\equiv y[\mathcal{X}]$.

Notice that we may define a non-uniform coherent space by specifying its web and two well chosen relations among $\equiv, \mathcal{C}, \mathcal{C}^*$.

Let $\mathcal{X}$ be a non-uniform coherent space, the non-uniform coherent model on $\mathcal{X}$ (nuCoł$^{\mathcal{X}}$) associates with formulas non-uniform coherent spaces, by induction on the formulas, as follows:

- with $X$ it associates $\mathcal{X}$;

- with $A^{\perp}$ it associates the following $A^{\perp}: |A^{\perp}| = |A|$, the neutrality and coherence of $A^{\perp}$ are as follows:

* $a \equiv a'[A^{\perp}]$ iff $a \equiv a'[A]$,

* $x \mathcal{C} y[A^{\perp}]$ iff $x \not\mathcal{C} y[A]$;

- with $A \otimes B$ it associates the following $A \otimes B: |A \otimes B| = |A| \times |B|$, the neutrality and coherence of $A \otimes B$ are as follows:

* $<a, b> \equiv <a', b'> [A \otimes B]$ iff $a \equiv a'[A]$ and $b \equiv b'[B]$,

* $<a, b> \mathcal{C} <a', b'> [A \otimes B]$ iff $a \mathcal{C} a'[A]$ and $b \mathcal{C} b'[B]$;

- with $!A$ it associates the following $!A: |!A| = M_{fin}(|A|)$, the strict incoherence and neutrality of $!A$ are as follows:

* $v \mathcal{C}^* u[!A]$ iff $\exists a \in v$ and $\exists a' \in u$, s.t. $a \mathcal{C}^* a'[A]$,

* $v \equiv u[!A]$ iff not $v \mathcal{C}^* u[!A]$ and there is an enumeration of $v$ (resp. of $u$) $v = [a_1, \dots, a_n]$ (resp. $u = [a'_1, \dots, a'_n]$), s.t. for each $i \le n$, $a_i \equiv a'_i[A]$.

Of course the space $A \otimes B$ is defined by $(A^{\perp} \otimes B^{\perp})^{\perp}$ as well as $?A$ is defined by $(!A^{\perp})^{\perp}$.

Remark that $!A$ may have elements strictly incoherent with themselves, i.e. $\mathcal{C}$ is not reflexive. For example, suppose $a, b$ are two elements in $A$ such that
a ~ b [A], then the multiset [a, b] is an element of !A such that [a, b] ~ [a, b] [!A].

For each proof structure $\pi$, we define the interpretation of $\pi$ in $\mathbf{nuCooh}^{\mathcal{X}}$, denoted by $\llbracket \pi \rrbracket_{\mathcal{X}}$, where the index $\mathcal{X}$ is omitted in case it is clear which coherent space is associated with $X$. $\llbracket \pi \rrbracket$ is defined by using the notion of experiment, introduced by Girard in [3].

We define an experiment $e$ on $\pi$ by induction on the exponential depth of $\pi$.<fnref n="2" />

**Definition 3 (Experiment).** A $\mathbf{nuCooh}^{\mathcal{X}}$ experiment $e$ on a proof structure $\pi$, denoted by $e : \pi$, is a function which associates with every link ! o at depth 0 a multiset $[e_1^o, \dots, e_k^o]$ (for $k \ge 0$) of experiments on $\pi^o$, and with every edge $a : A$ at depth 0 an element of $A$, s.t.:

- if $a, b$ are the conclusions (resp. the premises) of a link $ax$ (resp. cut) at depth 0, then $e(a) = e(b)$;

- if $c$ is the conclusion of a link $\mathcal{X}$ or $\otimes$ at depth 0 with premises $a, b$, then $e(c) = <e(a), e(b)>$;

- if $c$ is the conclusion of a link $?d$ with premise $a$, then $e(c) = [e(a)];$ if $c$ is the conclusion of a link $?c$ with premises $a, b$, then $e(c) = e(a) + e(b);$ if $c$ is the conclusion of a link $?w$, then $e(c) = \emptyset$;

- if $c$ is a door of a box associated with a link ! o at depth 0, let $a$ be the premise of o and $e(o) = [e_1^o, \dots, e_k^o]$. If $c$ is the principal door then $e(c) = [e_1^o(a), \dots, e_k^o(a)]$, if $c$ is an auxiliary door then $e(c) = e_1^o(c) + \dots + e_k^o(c)$;

If $c_1, \dots, c_n$ are the conclusions of $\pi$, then the result of $e$, denoted by $|e|$, is the element $<e(c_1), \dots, e(c_n)>$. The interpretation of $\pi$ in $\mathbf{nuCooh}^{\mathcal{X}}$ is the set of the results of its experiments:

$$ \llbracket \pi \rrbracket_{\mathcal{X}} = \{ |e| \text{ s.t. } e \text{ is a } \mathbf{nuCooh}^{\mathcal{X}} \text{ experiment on } \pi \} $$

The interpretation of a proof structure is invariant under cut reduction:

**Theorem 4 (Soundness of $\mathbf{nuCooh}^{\mathcal{X}}$).** For every proof structures $\pi, \pi', \pi =_{\beta} \pi'$ implies $\llbracket \pi \rrbracket_{\mathcal{X}} = \llbracket \pi' \rrbracket_{\mathcal{X}}$.

*Proof (Sketch).* It is a straightforward variant of the original proof given by Girard in [3] for proof nets. □

For concluding we explain why we choose the non-uniform variant of coherent spaces for proving our result.

The main difference between uniform and non-uniform coherent spaces is in the definition of the web of !A. The non-uniform web of !A contains all finite multisets of elements in A, while the uniform web of !A contains only those finite multisets whose support is a clique in A (see [3]).

<footnote n="2">² Definition 3 is slightly different from the usual one (see for example [7]), namely $e$ is defined only on the edges at depth 0 of $\pi$. Such a difference however does not play any crucial role in the proof of our result.</footnote>
Uniform webs thus have less elements than the non-uniform ones. Less elements means less experiments for proof structures. Indeed uniform experiments must satisfy besides the conditions of Definition 3 also a *uniformity condition*, namely the elements associated with edges of type !A (or ?A<sup>⊥</sup>) have to be in the uniform web of !A (see [7]).

Concerning our result, we believe that the experiment $e_\phi$, defined in the proof of Lemma 16, satisfies also the uniformity condition, but we haven't proved yet. Thus we conjecture that Theorem 10 holds also for uniform coherent spaces, but the proof should be quite harder. <fnref n="3" />

# 4 Paths and acyclicity

<figure><img src="image_6.png" /><figcaption>**Fig. 3.** MELL sequent calculus</figcaption></figure>

In Figure 3 we present the sequent calculus for MELL. As we noticed in the Introduction, sequent proofs can be translated into proof structures (see [3]). Such a translation is the gate to a geometry of logic and computation, since it makes possible to describe several properties of proofs by means of paths and graph-theoretical conditions such as connectivity or acyclicity.

In this paper, in particular, we consider paths with the following features:

**orientation:** a path is oriented, i.e. it crosses an edge $a$ either upward, from the link $a$ is conclusion to the link $a$ is premise, or downward, from the link $a$ is premise to the link $a$ is conclusion;

**black-box principle:** a path never crosses the frame of an exponential box, i.e. for a path a box is a node, whose emergent edges are the doors of the box.

**Definition 5 (Path).** An oriented edge is an edge together with a direction upward, denoted by $\uparrow a$, or downward, denoted by $\downarrow a$. We write $\downarrow a$ in case we

<footnote n="3">³ Uniform coherent spaces are special cases of non-uniform spaces, where $\equiv$ coincides with the identity. Denote by $[\pi]_{\mathcal{C}oh} \times$ (resp. $[\pi]_{nu\mathcal{C}oh} \times$) the uniform (resp. non-uniform) interpretation of $\pi$ based on a space $\mathcal{X}$. One can prove $[\pi]_{\mathcal{C}oh} \times \subseteq [\pi]_{nu\mathcal{C}oh} \times$. This means that if $[\pi]_{nu\mathcal{C}oh} \times$ is a clique so is $[\pi]_{\mathcal{C}oh} \times$, while the vice-versa does not hold in general. Hence remark that Theorem 10 (resp. Theorem 9) is stronger (resp. weaker) when it refers to $\mathcal{C}oh \times$ instead of $nu\mathcal{C}oh \times$.</footnote>
do not want to specify if we mean ↑ a or ↓ a. An oriented path (or simply path) from ↓ a₀ to ↓ aₙ is a sequence of oriented edges <↓ a₀, ..., ↓ aₙ > such that for any i < n, ↓ aᵢ, ↓ aᵢ₊₁ have the same depth and:

- if ↓ aᵢ =↑ aᵢ and ↓ aᵢ₊₁ =↑ aᵢ₊₁, then aᵢ is conclusion of a link l and aᵢ₊₁ is premise of l;

- if ↓ aᵢ =↑ aᵢ and ↓ aᵢ₊₁ =↓ aᵢ₊₁, then either aᵢ and aᵢ₊₁ are different conclusions of the same link ax l, or they are different doors of the same exponential box associated with a link ! l;

- if ↓ aᵢ =↓ aᵢ and ↓ aᵢ₊₁ =↓ aᵢ₊₁, then aᵢ is the premise of a link l and aᵢ₊₁ is conclusion of l;

- if ↓ aᵢ =↓ aᵢ and ↓ aᵢ₊₁ =↑ aᵢ₊₁, then aᵢ and aᵢ₊₁ are different premises of the same link l.

In any case we say that the path <↓ a₀, ..., ↓ aₙ > crosses the edges aᵢ, aᵢ₊₁ and the link l. We denote by * the concatenation of sequences of oriented edges.

A cycle is a path in which occurs twice ↓ a for an edge a.

Remark that aᵢ and aᵢ₊₁ must be different edges, i.e. we do not consider bouncing paths as <↑ a, ↓ a>.

We denote paths by Greek letters φ, τ, ψ, ... . We write ↓ a ∈ φ to mean that ↓ a occurs in φ.

## 4.1 Feasible paths

Feasible paths have been introduced by Fleury and Retoré in [2] as the paths "feasible" in a switching of a proof structure.

**Definition 6 (Feasible path, [2]).** A path is feasible whenever it does not contain two premises of the same link ⊗ or ?c.

A proof structure is feasible acyclic whenever it does not contain any feasible cycle.

Feasible acyclicity characterizes the proof structures which corresponds to the proofs of MELL sequent calculus enlarged by the rules of mix and daimon of Figure 4. The proofs of standard MELL instead are not easily characterizable by a geometrical condition, because of the weakening link. We do not enter in the details of the problem, for which we refer to [7].

$$ \frac{\vdash \Gamma \qquad \vdash \Delta \qquad \text{mix}}{\vdash \Gamma, \Delta} \qquad \vdash \text{dai} $$

<caption>Fig. 4. Mix and daimon rules</caption>

Let us compare feasible acyclicity and coherent spaces. As written before, they are tightly related in MLL by the following results:
**Girard's Theorem**, [3]: let $\pi$ be an MLL proof structure, $\mathcal{X}$ be a (uniform) coherent space. If $\pi$ is feasible acyclic, then $[[\pi]]_{\mathcal{X}}$ is a clique.

**Retoré's Theorem**, [5]: let $\pi$ be a cut-free MLL proof structure, $\mathcal{X}$ be a (uniform) coherent space with $x, y, z \in |\mathcal{X}|$ s.t. $x \prec y[\mathcal{X}]$ and $x \succ z[\mathcal{X}]$. If $[[\pi]]_{\mathcal{X}}$ is a clique, then $\pi$ is feasible acyclic.

However the situation changes in MELL: it is still true that any feasible acyclic proof structure is interpreted with a clique, but there are proof structures associated with cliques even if they have feasible cycles. For example take the proof structure $\pi$ of Figure 5.

<figure><img src="image_7.png" /><figcaption>**Fig. 5.** Example of feasible cycle invisible by coherent spaces.</figcaption></figure>

$\pi$ has the feasible cycle $<\uparrow a, \downarrow b, \uparrow a>$, nevertheless $[[\pi]]_{\mathcal{X}}$ is a clique for any coherent space $\mathcal{X}$. In fact, let $e_1, e_2$ be two experiments on $\pi$, we show that $|e_1| \subseteq |e_2| [((?\mathcal{I}\otimes?\mathcal{I})\succ!\mathcal{X})]$, where $I = X\succ X^\perp$. Suppose $e_1(o) = [e_1^1, \dots, e_1^n]$ and $e_2(o) = [e_2^1, \dots, e_2^m]$. Remark that for any experiments $e_i^l, e_j^h, e_i^l(a) \prec e_j^h(a)$ [$?\mathcal{I}$] as well as $e_i^l(b) \prec e_j^h(b)$ [$?\mathcal{I}$]. We split in two cases. In case $n = m$, then we deduce $e_1(a) \prec e_2(a)$ and $e_1(b) \prec e_2(b)$, hence $e_1(c) \prec e_2(c)$. Of course $e_1(d) \equiv e_2(d)$, thus $|e_1| \subseteq |e_2| [((?\mathcal{I}\otimes?\mathcal{I})\succ!\mathcal{X})]$. In case $n \neq m$, then $e_1(d) \prec e_2(d)$, thus $|e_1| \subseteq |e_2| [((?\mathcal{I}\otimes?\mathcal{I})\succ!\mathcal{X})]$. We conclude that $[[\pi]]$ is a clique.<fnref n="4" />

The failure of the correspondence between feasible acyclicity and coherent spaces shows that these latter read the exponential boxes in a different way than feasible paths do. Indeed the cycle $<\uparrow a, \downarrow b, \uparrow a>$ is due to the box associated with $o$: if we erase $o$ and the frame of its box, we would get a feasible acyclic proof structure. Coherent spaces do not read the boxes as feasible paths do, but it is not true that they do not read the boxes at all. For example, consider the proof structure $\pi'$ in figure 6.

$\pi'$ has the feasible cycle $<\uparrow a, \downarrow b, \uparrow a>$, which is due to the box of $o$, as in the example before. However in this case the cycle is visible by coherent spaces,

<footnote n="4">⁴ Remark that the same argument applies for usual Girard's coherent spaces.</footnote>
<figure><img src="image_8.png" /><figcaption>**Fig. 6.** Example of feasible cycle visible by coherent spaces.</figcaption></figure>

i.e. $[[\pi']]$ is not a clique. In fact, let $e_1, e_2$ be two experiments on $\pi'$, s.t. $e_1(o) = \emptyset$ and $e_2(o) = [e']$, for an experiment $e'$ on the box of $o$. Clearly $e_1(a) \sim e_2(a) [?\mathcal{I}]$, which implies $e_1(c) \sim e_2(c) [?\mathcal{I}\otimes?!\mathcal{X}]$.

## 4.2 Visible paths

Here is our main definition, that of visible paths (Definition 7).

Let $\phi$ be a path, $\pi^o$ be a box associated with a link! $o$. A passage of $\phi$ through $\pi^o$ is any sequence $<\uparrow a, \downarrow b>$ in $\phi$, for $a, b$ doors of $\pi^o$.

Notice that a feasible path can pass through an exponential box by means of any pair of its doors; the following definition forbids instead some of such passages:

**Definition 7 (Visible path).** Let $\pi$ be a proof structure. By induction on the depth of $\pi$, we define its visible paths:

- if $\pi$ has depth 0, then the visible paths of $\pi$ are exactly the feasible paths;

- if $\pi$ has depth $n+1$, let $\pi^o$ be a box associated with a link! $o$, $a$, $b$ be doors of $\pi^o$, we say that:

* $a$ is in the orbit of $o$ if either $a$ is the principal door or there is a visible path in $\pi^o$ from the premise of $o$ to $a$;

* $b$ leads to $a$ if either $b$ is in the orbit of $o$ or there is a visible path in $\pi^o$ from $a$ to $b$;

then a visible path in $\pi$ is a feasible path s.t. for any passage $<\uparrow a, \downarrow b>$ through an exponential box, $a$ leads to $b$.

A proof structure is visible acyclic whenever it does not contain any visible cycle.

Visible paths introduce two noteworthy novelties with respect to the feasible paths:
1. they partially break the black box principle: the admissible passages through an exponential box depend on what is inside the box, i.e. changing the contents of a box may alter the visible paths outside it;

2. they are sensitive to the direction: if $\phi$ is visible from $a$ to $b$, the same path done in the opposite direction from $b$ to $a$ may be no longer visible. For example recall the proof structure of Figure 6: the path $<\uparrow a, \downarrow b, \uparrow a>$ is visible, but $<\downarrow a, \uparrow b, \downarrow a>$ isn't, since $b$ does not lead to $a$.

Of course if $\pi$ is feasible acyclic then it is visible acyclic, but the converse does not hold. For example recall the proof structure of Figure 5, which is visible acyclic although it contains a feasible cycle. However it is remarkable that the two notions match in the polarized fragment of MELL, as we show in the following subsection.

## 4.3 Feasible and visible paths in polarized linear logic

The formulas of the polarized fragment of MELL are of two kinds, negatives ($N$) and positives ($P$), and are defined by the following grammar:

$$N ::= X \mid N \ominus N \mid ?P$$

$$P ::= X^{\perp} \mid P \otimes P \mid !N$$

A proof structure $\pi$ is polarized whenever all its edges are labeled by polarized formulas. An edge of $\pi$ is called positive (resp. negative) if it is labeled by a positive (resp. negative) formula.

The notion of polarization has a key role in proof theory since it is at the core of the translations of intuitionistic and classical logic into linear logic. We do not enter in the details, for which we refer to [8]. We limit ourself to notice the following proposition:

**Proposition 8.** Let $\pi$ be a polarized proof structure. $\pi$ is visible acyclic iff $\pi$ is feasible acyclic.

# 5 Visible acyclicity and coherent spaces

In this section we present the main theorems of the paper, stating the link between visible acyclicity and coherent spaces:

**Theorem 9.** Let $\pi$ be a MELL proof structure, $\mathcal{X}$ be a non-uniform coherent space.

If $\pi$ is visible acyclic, then $[[\pi]]_{\mathcal{X}}$ is a clique.

**Theorem 10.** Let $\pi$ be a cut-free MELL proof structure, $\mathcal{X}$ be a non-uniform coherent space with $x, y, z \in |\mathcal{X}|$ s.t. $x \frown y[\mathcal{X}]$, $x \frown z[\mathcal{X}]$ and $x \equiv x[\mathcal{X}]$.

If $[[\pi]]_{\mathcal{X}}$ is a clique, then $\pi$ is visible acyclic.

Subsection 5.1 (resp. 5.2) gives a sketch of the proof of Theorem 9 (resp. Theorem 10).
## 5.1 Proof of Theorem 9

Theorem 9 is an immediate consequence of the following lemma:

**Lemma 11.** Let $\pi$ be a visible acyclic proof structure. If $d: D$ is a conclusion of $\pi$ and $e_1, e_2$ are two experiments s.t. $e_1(d) \sim e_2(d) [D]$, then there is a visible path $\phi$ from $\uparrow d$ to a conclusion of $\pi \downarrow d': D'$ s.t. $e_1(d') \sim e_2(d') [D']$.

*Proof (Sketch).* Let $e_1(d) \sim e_2(d) [D]$. The lemma is proved by induction on the depth of $\pi$. The proof provides a procedure which defines a sequence of visible paths $\phi_1 \subset \phi_2 \subset \phi_3 \subset \dots$, such that $\phi_1$ is exactly $\langle\uparrow d\rangle$, and for each $\phi_j$:

1. $\phi_j$ is a visible path at depth 0;

2. for every edge $c: C$, if $\uparrow c \in \phi_j$ then $e_1(c) \sim e_2(c) [C]$, if $\downarrow c \in \phi_j$ then $e_1(c) \sim e_2(c) [C]$.

Since $\pi$ is visible acyclic, no $\phi_j$ is a cycle. Hence the sequence $\phi_1, \phi_2, \phi_3, \dots$ will meet eventually a conclusion $d'$ of $\pi$, so terminating in a path $\phi_k$ satisfying the lemma. $\square$

A straight consequence of Lemma 11 is that whenever $\pi$ is visible acyclic, the results of the experiments on $\pi$ are pairwise coherent, i.e. $\llbracket \pi \rrbracket$ is a clique.

We underline that the proof of Lemma 11 is a generalization in the framework of visible paths of the proof of the Compatibility Lemma (Lemma 3.18.1 in [3]).

## 5.2 Proof of Theorem 10

The proof of Theorem 10 is based on the key Lemma 16. In some sense Lemma 16 is the converse of Lemma 11: Lemma 11 associates with two experiments $e_1, e_2$ a visible path proving $|e_1| \unlhd |e_2|$; Lemma 16 instead is used in the proof of Lemma 17 to associate with a visible cycle (morally) two experiments s.t. $|e_1| \sim |e_2|$.

However Lemma 16 has to take care of a typical difficulty of the links ?c. In order to prove the lemma we need to manage the coherence/incoherence relationship between the values of $e_1$ and $e_2$. Unfortunately the links ?c soon make such a relationship unmanageable. In fact, if $l$ is a link ?c with conclusion $c$ and premises $a, b$, the incoherence $e_1(c) \sim e_2(c)$ holds if and only if $e_1(a) \sim e_2(a)$, $e_1(a) \sim e_2(b)$, $e_1(b) \sim e_2(a)$ and $e_1(b) \sim e_2(b)$ hold: such an exponential explosion of the number of incoherences soon becomes unmanageable.

Luckily there is a solution that avoids this problem. Namely we noticed that one of the two experiments $e_1, e_2$ can be chosen to be very simple, i.e. $e_1$ can be a $(x, n)$-simple experiment (see Definition 14). The key property of a $(x, n)$-simple experiment is that all of its possible values on an arbitrary edge of type $A$ are semantically characterized, precisely they are $(x, n)$-simple elements of $A$ with degree less or equal to $wn^d$, where $d$ is the depth of $\pi$ and $w$ is the cosize of $\pi$ (Definition 13 and Proposition 15). In this way we may define the second experiment $e_2$ not by looking at the particular value that $e_1$ takes on an edge of
type $\mathcal{A}$, but by referring in general to the $(x, n)$-simple elements of $\mathcal{A}$ with degree less or equal to $wn^d$. So whenever we consider the premises $a :?A, b :?B$ of a link $?c$, instead of taking care of the four incoherences $e_1(a) \not\sim e_2(a)$, $e_1(a) \not\sim e_2(b)$, $e_1(b) \not\sim e_2(a)$ and $e_1(b) \not\sim e_2(b)$, we will check only that for each $(x, n)$-simple element $v \in? \mathcal{A}$ with degree less or equal to $wn^d$, $v \not\sim e_2(a)$ and $v \not\sim e_2(b)$.

**Definition 12 ([7]).** Let $\mathcal{C}$ be the $\mathcal{nuCoH}^\mathcal{X}$ interpretation of a formula $\mathcal{C}$ and $v \in \mathcal{C}$. For every occurrence of a subformula $\mathcal{A}$ of $\mathcal{C}$ we define the projection of $v$ on $\mathcal{A}$ (denoted as $|v|_\mathcal{A}$) as the multiset defined by induction as follows:

- if $C = A$, then $|v|_A = [v]$;

- if $C = D \not\sim E$ or $C = D \otimes E$, $v =< v', v'' >$ and $A$ is a subformula of $D$ (resp. of $E$), then $|v|_A = |v'|_A$ (resp. $|v|_A = |v''|_A$);

- if $C =?D$ or $C =!D$, $v = [v_1, \dots, v_n]$ and $A$ is a subformula of $D$, then $|v|_A = |v_1|_A + \dots + |v_n|_A$.

**Definition 13.** Let $n \in \mathbb{N}$, $x$ be an element of a non-uniform coherent space $\mathcal{X}$ and $\mathcal{C}$ be the $\mathcal{nuCoH}^\mathcal{X}$ interpretation of a formula $\mathcal{C}$. An element $v \in \mathcal{C}$ is a $(x, n)$-simple element if:

1. for any atomic subformula $X, X^\perp$ of $C$, $\text{Supp}(|v|_X) = \text{Supp}(|v|_{X^\perp}) = \{x\}$;

2. for any $!$-subformula $!A$ of $C$, if $u \in |v|_!A$ then $u = n[u']$;

Moreover $v$ is stable if also:

3. for any $?$-subformula $?A$ of $C$, if $u \in |v|_{?A}$ then $u = n[u']$.

The degree of a $(x, n)$-simple element $v$, denoted by $d(v)$, is the number:

$$d(v) = \max \{m \mid \exists?A \text{ subform. of } C, \exists u \in |v|_{?A} \text{ s.t. } u = [u_1, \dots, u_m]\}$$

Remark that an element is $(x, n)$-simple in both $\mathcal{C}$ and $\mathcal{C}^\perp$ only if it is also stable. Moreover, notice that for any formula $\mathcal{C}$, there is only one stable $(x, n)$-simple element in $\mathcal{C}$.

**Definition 14 ([7]).** Let $\pi$ be a proof structure, $n \in \mathbb{N}$, $x$ be an element of a non-uniform coherent space $\mathcal{X}$. The $(x, n)$-simple experiment on $\pi$, denoted by $e_{(x,n)}^\pi$, is defined as follows (by induction on the depth of $\pi$):

- for each conclusion $a : A$ of an axiom at depth 0, $e_{(x,n)}^\pi(a) = s$, where $s$ is the stable $(x, n)$-simple element of $\mathcal{A}$;

- for each link $!o$ at depth 0, let $\pi^o$ be the box of $o$, $e_{(x,n)}^\pi(o) = n[e_{(x,n)}^\pi]$.

**Proposition 15.** Let $\pi$ be a proof structure of depth $d$ and cosize $w$. Let $e_{(x,n)}^\pi$ be the $(x, n)$-simple experiment on $\pi$. For any edge $c : C$ at depth 0, $e_{(x,n)}^\pi(c)$ is a $(x, n)$-simple element of $\mathcal{C}$ with degree at most $wn^d$.
**Lemma 16.** Let $\mathbf{nuCooh}^{\mathcal{X}}$ be defined from a coherent space $\mathcal{X}$ s.t. $\exists x, y, z \in \mathcal{X}$, $x \equiv x[\mathcal{X}], x \wedge y[\mathcal{X}]$ and $x \sim z[\mathcal{X}]$.

Let $\pi$ be a cut-free proof structure, $k$ be the maximal number of doors of a box of $\pi$. Let $\phi$ be a visible path at depth 0 from a conclusion $\uparrow$ to a conclusion $\downarrow b$, s.t. $\phi$ is not a cycle.

For any $n, m \in \mathbb{N}$, $m \ge n \ge k$, there is an experiment $e_{\phi} : \pi$, s.t. for any edge $c : C$ at depth 0 and any $(x, n)$-simple element $v$ in $C$ with degree less or equal $m$:

1. if there is $c'$ equal or above $c$ s.t. $\downarrow c' \in \phi$, then $e_{\phi}(c) \not\equiv v[C]$;

2. if $\downarrow c \notin \phi$, then $e_{\phi}(c) \preceq v[C]$.

*Proof (Sketch).* The lemma is proved by induction on the depth of $\pi$. The proof is divided in two steps: firstly, $e_{\phi}$ is defined by giving its values on the links $ax$ and $!$ at depth 0; secondly, $e_{\phi}$ is proved to satisfy conditions 1, 2 for any edge $c$, by induction on the number of edges at depth 0 above $c$. $\square$

**Lemma 17.** Let $\mathbf{nuCooh}^{\mathcal{X}}$ be defined from a coherent space $\mathcal{X}$ s.t. $\exists x, y, z \in \mathcal{X}$, $x \equiv x[\mathcal{X}], x \wedge y[\mathcal{X}]$ and $x \sim z[\mathcal{X}]$.

Let $\pi$ be a cut-free proof structure with conclusions $\Pi$, $k$ be the maximal number of doors of an exponential box in $\pi$. If $\pi$ has a visible cycle, then for any $n, m \in \mathbb{N}$, $m \ge n \ge k$, there is an experiment $e : \pi$, such that for any $(x, n)$-simple element $v$ in $\mathcal{V}\Pi$ with degree less or equal to $m$, $|e| \sim v[\mathcal{V}\Pi]$.

*Proof (Sketch).* The proof is by induction on the size of $\pi$. The induction step splits in seven cases, one for each type of link (except cut). The crucial case deals with the link $\otimes$, since removing it may erase visible cycles. In this case Lemma 16 will be used. $\square$

The proof of Theorem 10 is straight once we have Lemma 17. Let $\pi$ be a cut-free proof structure with conclusions $\Pi$, depth $d$, cosize $w$ and let $k$ be the maximal number of doors of a box of $\pi$. If $\pi$ has a visible cycle then by Lemma 17 there is an experiment $e : \pi$ such that for any $(x, n)$-simple element $v$ in $\mathcal{V}\Pi$ with degree less or equal to $m$, $|e| \sim v[\mathcal{V}\Pi]$, where $n = k, m = wn^d$.

Let $e_{(x,n)}^{\pi}$ be the $(x, n)$-simple experiment on $\pi$. By Proposition 15, $|e_{(x,n)}^{\pi}|$ is a $(x, n)$-simple element in $\mathcal{V}\Pi$ with degree less or equal to $m$. So $|e| \sim |e_{(x,n)}^{\pi}|[\mathcal{V}\Pi]$, i.e. $[\pi]_{\mathcal{X}}$ is not a clique in $\mathcal{V}\Pi$.

# 6 Visible acyclicity and cut reduction

It turns out that visible acyclicity has also nice computational properties, especially it is stable under cut reduction:

**Theorem 18 (Stability).** Let $\pi, \pi'$ be MELL proof structures. If $\pi \to \beta \pi'$ and $\pi$ is visible acyclic then $\pi'$ is visible acyclic.
Proof (Sketch). Indeed if $\pi \rightsquigarrow \beta \pi'$, then every visible cycle in $\pi'$ is the "residue" of a visible cycle in $\pi$. $\square$

Remark that a proof structure with deadlocks is not visible acyclic, hence Theorem 18 assures that the cut reduction of visible acyclic proof structures never produces deadlocks.

Moreover, visible acyclicity guarantees also confluence and strong normalization of $\to_\beta$. Here we give only the statements of the theorems, which will be treated in details in a forthcoming paper:

**confluence:** let $\pi$ be a visible acyclic MELL proof structure, if $\pi \to_\beta \pi_1$ and $\pi \to_\beta \pi_2$ then there is $\pi_3$ s.t. $\pi_1 \to_\beta \pi_3$ and $\pi_2 \to_\beta \pi_3$;

**strong normalization:** let $\pi$ be a visible acyclic MELL proof structure, there is no infinite sequence of proof structures $\pi_0, \pi_1, \pi_2, \dots$ s.t. $\pi_0 = \pi$ and $\pi_i \rightsquigarrow \beta \pi_{i+1}$.

<figure><img src="image_9.png" /><figcaption>Fig. 7. Counter-example of confluence of cut reduction on proof structures.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 8. Counter-example of strong normalization of cut reduction on proof structures.</figcaption></figure>

Remark that both confluence and strong normalization are false on proof structures with visible cycles. For example consider the proof structure $\pi$ in Figure 7. If you reduce the cut link $l$, then $m$ becomes a deadlock, while if you reduce the cut link $m$ then $l$ becomes a deadlock: i.e. $\pi$ is a counter-example to the confluence. Concerning strong normalization, consider the proof structure $\pi$ in Figure 8 and notice that reducing $m$, then $l$, then a residue of $m$, then a residue of $l$ and so on ... we get an infinite sequence of cut reductions.
References

1. Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic **28** (1989) 181-203

2. Fleury, A., Retoré, C.: The mix rule. Mathematical Structures in Computer Science **4(2)** (1994) 173-185

3. Girard, J.-Y.: Linear Logic. Theoretical Computer Science **50** (1987) 1-102

4. Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic **109** (2001) 205-241

5. Retoré, C.: A semantic characterization of the correctness of a proof net. Mathematical Structures in Computer Science **7(5)** (1997) 445-452

6. Pagani, M.: Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic. To appear in: Mathematical Structures in Computer Science

7. Tortora de Falco, L.: Réseaux, cohérence et expériences obsessionnelles. Thèse de doctorat, Université Paris VII (2000)

8. Laurent, O.: Étude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (2002)
# A Omitted proofs

## A.1 Proof of Proposition 8

*Proof (of Proposition 8).* The difficult part is the "only if" part. Suppose that $\pi$ has a feasible cycle, the proof that $\pi$ has also a visible cycle is an easy consequence of the following fact:

(*) if $\pi$ is a polarized proof structure with feasible cycles, then $\pi$ has a feasible cycle $\phi$ s.t.:

1. if $\uparrow a \in \phi$, then $a$ is positive;

2. if $\downarrow a \in \phi$, then $a$ is negative.

Let us prove (*). Suppose $\pi$ has a switching cycle $\phi$. Notice that $\phi$ must contain a positive edge $b$, since it must cross a link $\otimes$ or *cut*. Since $\phi$ is a cycle, we can suppose it starts and arrives in $b$. Moreover, since the feasible paths are independent of the direction of the path, we can suppose $\phi$ starts from $\uparrow b$.

Let $\downarrow a \in \phi$, we prove the conditions 1,2 of (*), by induction on the length of the subpath $\langle \uparrow b, \dots, \downarrow a \rangle$ of $\phi$. Let $\downarrow a'$ be the preceding edge of $\downarrow a$ in $\phi$.

1. if $\downarrow a = \uparrow a$, we prove that $a$ is positive. The proof splits in two cases:

- if $\downarrow a' = \uparrow a'$, then $a'$ is conclusion of a link $l$ and $a$ is premise of $l$. By induction $a'$ is positive, hence $l$ can be a link $\otimes$ or $!$. Since $a, a'$ have the same depth, $l$ is not a link $!$, hence $a$ is a premise of a link $\otimes$, i.e. it is positive;

- if $\downarrow a' = \downarrow a'$, then $a'$ and $a$ are different premises of the same link $l$. By induction $a'$ is negative, hence $l$ can be a link among *cut*, $\aleph$, $?c$. Since $\phi$ is switching, $l$ is not a link $\aleph$ or $?c$, hence $a$ is the positive premise of the cut whose negative premise is $a'$.

2. if $\downarrow a = \downarrow a$, we prove that $a$ is negative. The proof splits in two cases:

- if $\downarrow a' = \uparrow a'$, then either $a'$ and $a$ are different conclusions of the same axiom $l$, or they are different doors of the same exponential box associated with a link $!l$. By induction $a'$ is positive, thus either it is the positive conclusion of an axiom or it is the principal door of an exponential box. In both cases we deduce that $a$ is negative;

- if $\downarrow a' = \downarrow a'$, then $a'$ is the premise of a link $l$ and $a$ is conclusion of $l$. By induction $a'$ is negative, hence $l$ can be a link $\aleph$, $?c$, $?d$ or $!$. Since $a, a'$ have the same depth, $l$ is not a link $!$, hence $a$ is negative.

Once we have proved (*), let us suppose $\pi$ is a polarized feasible cyclic structure, let us prove that $\pi$ is visible cyclic.

Let $\phi$ be a feasible cycle satisfying 1,2 of (*). Let $\phi^*$ be the path obtained by reversing the direction of $\phi$. Of course $\phi$ is still feasible, we prove that it is indeed visible. Let $\langle \uparrow a, \downarrow b \rangle$ be a passage of $\phi^*$ through a box $\pi^o$. Since $\phi$ satisfies 1,2 then $b$ is positive, hence it is the principal door of $\pi^o$, that means $a$ leads to $b$. We conclude that $\phi^*$ is a visible cycle of $\pi$. $\square$
## A.2 Proof of Lemma 11

*Proof (of Lemma 11).* Let $e_1(d) \sim e_2(d)$ [$\mathcal{D}$]. We prove the lemma by induction on the exponential depth of $\pi$.

We define a sequence of visible paths $\phi_1 \subset \phi_2 \subset \dots \subset \phi_k$, such that $\phi_1$ is exactly $<\uparrow d>$, $\phi_k$ starts from $\uparrow d$ and ends in $\downarrow d'$, for a conclusion of $\pi$ $d'$, and for each $\phi_j$ among $\phi_1, \dots, \phi_k$:

1. $\phi_j$ is a visible path at depth 0;

2. for every edge $c: C$, if $\uparrow c \in \phi_j$ then $e_1(c) \sim e_2(c)$ [$\mathcal{C}$], if $\downarrow c \in \phi_j$ then $e_1(c) \wedge e_2(c)$ [$\mathcal{C}$].

Let us define $\phi_{j+1}$ from $\phi_j$, this last one supposed satisfying conditions 1 and 2. Let $c: C$ be the last edge of $\phi_j$. Then:

- in case $\downarrow c \in \phi_j$, by hypothesis $c$ is an edge of $\pi$ at depth 0 and $e_1(c) \wedge e_2(c)$ [$\mathcal{C}$]:

• if $c$ is a premise of a link $\mathcal{C}$ with conclusion $b: B$, then $e_1(b) \wedge e_2(b)$ [$\mathcal{B}$]. We define $\phi_{j+1} = \phi_j * <\downarrow b>$;

• if $c$ is a premise of a link $\otimes$ with conclusion $b: B$ and premises $c: C, a: A$, in case $e_1(b) \wedge e_2(b)$ [$\mathcal{B}$], we define $\phi_{j+1} = \phi_j * <\downarrow b>$; otherwise $e_1(a) \sim e_2(a)$ [$\mathcal{A}$], in this case we define $\phi_{j+1} = \phi_j * <\uparrow a>$;

• if $c$ is the premise of a link $?d$ with conclusion $b: ?C$, then $e_1(b) \wedge e_2(b)$ [$?C$]. We define $\phi_{j+1} = \phi_j * <\downarrow b>$;

• if $c$ is a premise of a link $?c$ with conclusion $b$, then both $c, b$ are of type $?B$ for a formula $B$, and $e_1(c) \subseteq e_1(b)$, $e_2(c) \subseteq e_2(b)$. Since $e_1(c) \wedge e_2(c)$ [$?B$], we deduce $e_1(b) \wedge e_2(b)$ [$?B$]. We define $\phi_{j+1} = \phi_j * <\downarrow b>$;

• if $c$ is a premise of a link $cut$ with premises $c: C, b: C^{\perp}$, then $e_1(b) \sim e_2(b)$ [$C^{\perp}$], so let $\phi_{j+1} = \phi_j * <\uparrow b>$;

• if $c$ is a conclusion of $\pi$, then we define $\phi_j$ as $\phi_k$.

Notice that $c$ cannot be the premise of a link $!$, since $c$ is at depth 0.

Clearly $\phi_{j+1}$ satisfies condition 2. Let us prove that it is visible.

At first, we prove that $\phi_{j+1}$ is a switching path. Let $b$ be the edge added to $\phi_j$ for defining $\phi_{j+1}$. If $b$ is a switching edge of a link $l$, then we prove that $\phi_j$ contains no premise of $l$. In fact suppose by absurdity that $\phi_j$ contains a premise of $l$, then it contains the conclusion $c$ of $l$ (recall $\phi_j$ is switching and $l$ is a link $\mathcal{C}$ or $?c$). Since $e_1(b) \wedge e_2(b)$ we deduce $e_1(c) \wedge e_2(c)$. Since $\phi_j$ meets condition 2, $\downarrow c \in \phi_j$. That is, $\phi_{j+1}$ has the following shape:

$$ \phi_{j+1} = \phi_j' * <\downarrow c> * \phi_j'' * <\downarrow b> $$

where no premise of $l$ is in $\phi_j''$. Hence $<\downarrow c> * \phi_j'' * <\downarrow b> \downarrow c$ is a visible cycle of $\pi$, which contradicts the visible acyclicity of $\pi$. We conclude that $b$ is not a switching edge of a link crossed by $\phi_j$, thus $\phi_{j+1}$ is switching.

At second, we prove that $\phi_{j+1}$ is a visible path, i.e. that all its passages though exponential boxes are allowed to visible paths. Actually remark that $\phi_{j+1}$ has the same passages though exponential boxes as $\phi_j$, thus the assertion is immediate from the visibility of $\phi_j$.
- in case $\uparrow c \in \phi_j$, by hypothesis $c$ is an edge of $\pi$ at depth 0 and $e_1(c) \sim e_2(c)$ [$C$]:

* if $c$ is the conclusion of a link $ax$ with conclusions $c: C, b: C^{\perp}$, then $e_1(b) \wedge e_2(b)$ [$C^{\perp}$]. We define $\phi_{j+1} = \phi_j * <\downarrow b>$;

* if $c$ is the conclusion of a link $\ominus$ or $\otimes$, then there is a premise $b: B$ s.t. $e_1(b) \wedge e_2(b)$ [$B$]. We define $\phi_{j+1} = \phi_j * <\uparrow b>$;

* if $c$ is the conclusion of a link $!o$, let $C=!A$, $a: A$ be the premise of $o$ and $\pi^o$ be the box of $o$. Since $e_1(c) \sim e_2(c)$ [$!A$], there are $e_1^o \in e_1(o)$, $e_2^o \in e_2(o)$ such that $e_1^o(a) \sim e_2^o(a)$ [$A$]. By induction hypothesis on $\pi^o$ and $e_1^o, e_2^o$, there is a conclusion $b: ?B$ of $\pi^o$ (i.e. an auxiliary door of $\pi^o$) and a visible path in $\pi^o$ from $\uparrow a$ to $\downarrow b$, s.t. $e_1^o(b) \wedge e_2^o(b)$ [$?B$].
Since $e_1^o(b) \subseteq e_1(b)$ and $e_2^o(b) \subseteq e_2(b)$, we deduce $e_1(b) \wedge e_2(b)$ [$?B$]. We define $\phi_{j+1} = \phi_j * <\downarrow b>$. Remark that $c$ leads to $b$;

* if $c$ is an auxiliary door of a box $\pi^o$ associated with a link $!o$, let $b: !B$ be the conclusion of $o$ and $a: B$ be its premise. We split in two cases:

* in case $e_1(b) \not\equiv e_2(b)$ [$!B$], then either $e_1(b) \wedge e_2(b)$ or $e_1(b) \wedge e_2(b)$. If $e_1(b) \wedge e_2(b)$ [$!B$], we set $\phi_{j+1} = \phi_j * <\downarrow b>$. Remark that $c$ leads to $b$, being this last one in the orbit of $o$.

If $e_1(b) \sim e_2(b)$ [$!B$], then there is $e_1^o \in e_1(o)$, $e_2^o \in e_2(o)$ s.t. $e_1^o(a) \sim e_2^o(a)$ [$B$]. By induction hypothesis on $\pi^o$ and $e_1^o, e_2^o$, there is a conclusion $b' : ?B'$ of $\pi^o$ and a visible path in $\pi^o$ from $\uparrow a$ to $\downarrow b'$, s.t. $e_1^o(b') \wedge e_2^o(b')$ [$?B'$]. Since $e_1^o(b') \subseteq e_1(b')$ and $e_2^o(b') \subseteq e_2(b')$, we deduce $e_1^o(b') \wedge e_2^o(b')$ [$?B'$]. Remark that since by hypothesis $e_1(c) \sim e_2(c)$ [$C$], we are sure that $b'$ and $c$ are different auxiliary doors of $\pi^o$. Moreover, notice that $c$ leads to $b'$, being this last one in the orbit of $o$. Define $\phi_{j+1} = \phi_j * <\downarrow b'>$.

* in case $e_1(b) \equiv e_2(b)$ [$!B$], then by definition of the neutrality there is an enumeration $e_1^1, \dots, e_1^l$ (resp. $e_2^1, \dots, e_2^l$) of the experiments of $\pi^o$ associated with $o$ by $e_1$ (resp. by $e_2$), s.t. for each $i \le l$, $e_1^i(a) \equiv e_2^i(a)$ [$B$]. Remark that $l > 0$, otherwise $e_1(c) \equiv e_2(c)$.

On the other hand, since $e_1(c) \sim e_2(c)$ [$C$] and $e_1(c) = e_1^1(c) + \dots + e_1^l(c)$, $e_2(c) = e_2^1(c) + \dots + e_2^l(c)$, there is an $h \le l$ s.t. $e_1^h(c) \sim e_2^h(c)$ [$C$].

Now we apply the induction hypothesis on $\pi^o$, $e_1^h, e_2^h$, so obtaining a conclusion $b' : B'$ of $\pi^o$ and a visible path from $\uparrow c$ to $\downarrow b'$ s.t. $e_1^h(b') \wedge e_2^h(b')$ [$B'$]. Remark that $b' \ne a$, since we are in the hypothesis that $e_1^h(a) \equiv e_2^h(a)$ [$B$]. Thus in particular $B' = ?D$ for a formula $D$. By $e_1^h(b') \wedge e_2^h(b')$ [$?D$], we deduce $e_1(b') \wedge e_2(b')$ [$?D$]. Hence we set $\phi_{j+1} = \phi_j * <\downarrow b'>$. Remark that $c$ leads to $b'$, since there is a visible path from $c$ to $b'$.

* if $c$ is the conclusion of a link $?d$ with premise $b: B$ at depth 0, then $e_1(b) \sim e_2(b)$ [$B$]. We define $\phi_{j+1} = \phi_j * <\uparrow b>$;

* if $c$ is the conclusion of a link $?c$ with premises at depth 0, then there is a premise $b: B$ s.t. $e_1(b) \wedge e_2(b)$ [$B$]. We define $\phi_{j+1} = \phi_j * <\uparrow b>$;

Remark that $c$ cannot be conclusion of link $?w$, since $e_1(c) \sim e_2(c)$ [$C$]. Of course $\phi_{j+1}$ meets condition 2, let us prove that it is a visible path. At first, remark that the proof that $\phi_{j+1}$ is a switching path is similar to the preceding case of $\downarrow c \in \phi_j$.
At second, notice that any time we have added to $\phi_{j+1}$ a passage through an exponential box (i.e. in the subcases where $c$ was a door of an exponential box) we have also proved that such a new passage is allowed to visible paths. From that we conclude that $\phi_{j+1}$ is a visible path.

Since $\pi$ is visible acyclic, no $\phi_j$ is a cycle. Hence the sequence $\phi_1, \phi_2, \phi_3, \dots$ will meet eventually a conclusion $d'$ of $\pi$, so terminating in a path $\phi_k$ satisfying the lemma. $\square$

### A.3 Proof of Lemma 16

Before proving Lemma 16 let us state the following proposition:

**Proposition 19.** Let $\mathcal{X}$ be a non-uniform coherent space, $x \in \mathcal{X}$ s.t. $x \equiv x[\mathcal{X}]$, $C$ be the $\mathbf{nuCoH}^{\mathcal{X}}$ interpretation of a formula $C$. For any $n \in \mathbb{N}$ and $(x, n)$-simple elements $v, v'$ of $C$, $v \rightsquigarrow v' [C]$.

*Proof.* By induction on $C$. $\square$

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

Now we prove Lemma 16:

*Proof (of Lemma 16).* Let $\mathcal{X}, \pi, k, \phi, n, m$ be as in the hypotheses of the lemma.

Notice that if $\exists x, y, z \in \mathcal{X}$, s.t. $x \equiv x[\mathcal{X}], x \frown y[\mathcal{X}]$ and $x \frown z[\mathcal{X}]$, then for any formula $C$, $\exists y_C, z_C \in C$ s.t. $y_C = z_{C^{\perp}}$ and for any $(x, n)$-simple element $v$ in $C$ with degree less or equal $m$: $v \frown y_C [C]$ and $v \frown z_C [C]$ (it can be easily proved by induction on $C$). From now on we fix for any formula $C$ such $y_C$ and $z_C$.

The proof of the lemma is by induction on the depth of $\pi$.

At first we define $e_{\phi}$ by giving its values on the links $ax$ and $!$ at depth 0:

**links $ax$:** let $a: A$ be a conclusion of an axiom at depth 0, then:

- if $\uparrow a \in \phi$, $e_{\phi}(a) = z_A$;

- if $\downarrow a \in \phi$, $e_{\phi}(a) = y_A$;

- otherwise $e_{\phi}(a) = s$, where $s$ is the stable $(x, n)$-simple element of $A$.

Notice that such a definition is consistent since $\phi$ is not a cycle, that is, if $\uparrow a \in \phi$ then $\downarrow a \notin \phi$, and vice-versa if $\downarrow a \in \phi$ then $\uparrow a \notin \phi$.

**links !:** let $o$ be a link ! at depth 0, $\pi^o$ be the box of $o$ and $<\uparrow a_1, \downarrow b_1>$, ..., $<\uparrow a_h, \downarrow b_h>$ be the passages of $\phi$ through $\pi^o$ (for $h \ge 0$). Remark that $h \le k \le n$, since $k$ is the maximal number of doors of a box of $\pi$ and $\phi$ is not a cycle.

Since $\phi$ is visible, for each $i \le h$, $a_i$ leads to $b_i$. We associate with each passage $<\uparrow a_i, \downarrow b_i>$ an experiment $e_{\phi_i}^o$ on $\pi^o$ as follows:

- if $\downarrow b_i$ is the principal door, then $e_{\phi_i}^o = e_{(x,n)}^o$;

- if $\downarrow b_i$ is an auxiliary door in the orbit of $o$, then let $\phi_i$ be a visible path in $\pi^o$ from the premise of $o$ to $\downarrow b_i$. By induction we may define an experiment $e_{\phi_i}$ on $\pi^o$ satisfying conditions 1,2 with respect to $\pi^o$ and $\phi_i$;
- if $\downarrow b_i$ is an auxiliary door not in the orbit of $o$, then let $\phi_i$ be a visible path in $\pi^o$ from $\uparrow a_i$ to $\downarrow b_i$. By induction we may define an experiment $e_{\phi_i}$ on $\pi^o$ satisfying condition 1,2 with respect to $\pi^o$ and $\phi_i$.

Finally we define $e_\phi$ on $o$ as follows:

- if $\phi$ does not pass through the orbit of $o$:

$$e_{\phi}(o) = [e_{\phi_1}, \dots, e_{\phi_h}] + (n - h) \left[ e_{(x,n)}^{\pi^o} \right]$$

- if $\phi$ passes through the orbit of $o$:

$$e_{\phi}(o) = [e_{\phi_1}, \dots, e_{\phi_h}] + (m + 1 - h) \left[ e_{(x,n)}^{\pi^o} \right]$$

At second we prove that $e_\phi$ satisfies the conditions 1, 2 of the theorem. Let $c: C$ be an edge of $\pi$ at depth 0, we prove 1, 2 by induction on the number of edges at depth 0 above $c$ (we write $c' \ge c$ whenever $c'$ is above or equal $c$).

**Base of induction:** if above $c$ there are no edges at depth 0, then $c$ is conclusion of a link among $ax$, $?w$, or it is a door of a box:

- if $c$ is conclusion of a link $ax$, then conditions 1, 2 are an immediate consequence of the definition of $e_\phi$ and propositions 19, 15;

- if $c$ is conclusion of a link $?w$, then notice that $\uparrow c \notin \phi$, since $\phi$ is a path between two conclusions of the proof structure $\pi$, i.e. $\phi$ neither starts nor stops in $c$. Hence condition 1 is immediately proved. For condition 2 remark that $e_\phi(c) = \emptyset$ and $\emptyset \not\sim v[?B]$ for any element $v \in B$;

- if $c$ is a principal door of a box $\pi^o$ associated with a link $!o$, let $b: B$ be the premise of $o$ (i.e. $C =!B$) and $v = n[v']$ be a $(x, n)$-simple element of $!B$ with degree less or equal $m$:

1. if $\exists c' \ge c, \uparrow c' \in \phi$, then clearly $c = c'$ (recall that $\phi$ is a path crossing only edges at depth 0). In this case $\phi$ passes through the orbit of $o$, so $e_\phi(c)$ has $m+1$ elements. Since $v$ has $n$ elements and $n \le m$, we deduce $e_\phi(c) \ne v$;

2. if $\downarrow c \notin \phi$, we split in two cases, depending if $\phi$ passes or not through the orbit of $o$:

* in case $\phi$ passes through the orbit of $o$, then it exists a visible path $\phi_i$ associated with a passage of $\phi$ through the orbit of $o$. Remark that $\uparrow b \in \phi_i$ (since $\downarrow c \notin \phi$), hence by definition of the experiment $e_{\phi_i}$ associated with $\phi_i$, we have both $e_{\phi_i}(b) \ne v'$ (by 1) and $e_{\phi_i}(b) \not\sim v'$ (by 2), i.e. $e_{\phi_i}(b) \sim v'$. Since $e_{\phi_i}(b) \in e_\phi(c)$, we deduce $e_\phi(c) \sim v$;

* in case $\phi$ does not pass through the orbit of $o$, then let $\phi_1, \dots, \phi_h$ ($h \ge 0$) be the visible paths associated with the passages of $\phi$ through $o$. Since $\phi$ does not pass through the orbit of $o$, for each $i \le h, \uparrow b \notin \phi_i$. Hence by definition of the experiment $e_{\phi_i}$ associated with $\phi_i$, we have $e_{\phi_i}(b) \sim v'$. Moreover recall that $e_{(x,n)}^{\pi^o}$ is the $(x, n)$-simple experiment on $\pi^o$. By proposition 15,
$e_{(x,n)}^{\pi^o}(b)$ is a $(x, n)$-simple element of $\mathcal{B}$, hence by proposition 19,
$e_{(x,n)}^{\pi^o}(b) \not\sim v'$. Finally, since $e_\phi(c) = [e_{\phi_1}(b), \dots, e_{\phi_h}(b)] + (n - h)$
$[e_{(x,n)}^{\pi^o}(b)]$, we deduce $e_\phi(c) \not\sim v$.

- if $c$ is an auxiliary door of a box $\pi^o$ associated with a link $! o$, let $v$ be a $(x, n)$-simple element of $\mathcal{C}$ with degree less or equal $m$:

1. if $\exists c' \ge c, \uparrow c' \in \phi$, then clearly $c' = c$ (recall that $\phi$ is a path crossing only edges at depth 0). In this case there is a door $d$ of $\pi^o$ s.t. $\langle \uparrow c, \downarrow d \rangle$ or $\langle \uparrow d, \downarrow c \rangle$ is a passage of $\phi$ through $o$. We split in two cases, depending if $\phi$ passes or not through the orbit of $o$:

* in case $\phi$ passes through the orbit of $o$, then $e_\phi(c)$ has at least $m+1$ elements, while $v$ has at most $m$ elements, being of degree less or equal $m$. Thus $e_\phi(c) \not\equiv v$;

* in case $\phi$ does not pass through the orbit of $o$, let $\phi_i$ be the visible path in $\pi^o$ between $c$ and $d$. Of course $\uparrow c \in \phi_i$, thus $e_{\phi_i}(c) \not\equiv v'$, for any $(x,n)$-simple element $v'$ of $\mathcal{C}$ with degree less or equal $m$. Now, suppose $e_\phi(c) \equiv v$ and let us prove a contradiction. Since $e_{\phi_i}(c) \subseteq e_\phi(c)$, there should be a subset $v' \subseteq v$ s.t. $e_{\phi_i}(c) \equiv v'$, but we have just proven $e_{\phi_i}(c) \not\equiv v'$, for any $(x,n)$-simple element $v'$ of $\mathcal{C}$ with degree less or equal $m$. Hence we conclude $e_\phi(c) \not\equiv v$;

2. if $\downarrow c \notin \phi$, let $\phi_1, \dots, \phi_h$ (for $h \ge 0$) be the visible paths in $\pi^o$
associated with the passages of $\phi$ through $o$. Since $\downarrow c \notin \phi$, then
for each $i \le h$, $\downarrow c \notin \phi_i$, thus by the definition of $e_{\phi_i}$, $e_{\phi_i}(c) \not\sim v$.
Moreover recall that $e_{(x,n)}^{\pi^o}$ is the $(x,n)$-simple experiment on $\pi^o$.
By proposition 15, $e_{(x,n)}^{\pi^o}(c)$ is a $(x,n)$-simple element of $\mathcal{C}$, hence
by proposition 19, $e_{(x,n)}^{\pi^o}(c) \not\sim v$. Finally, since $e_\phi(c) = e_{\phi_1}(c) + \dots +
e_{\phi_h}(c) + (n-h) [e_{(x,n)}^{\pi^o}(c)]$, we deduce $e_\phi(c) \not\sim v$.

**Induction step:** if above $c$ there are edges at depth 0, then $c$ is conclusion of
a link among $\mathcal{C}$, $\otimes$, $?d$, $?c$:

- if $c$ is conclusion of a link $\mathcal{C}$ with premises $a: A, b: B$, let $v = \langle v', v'' \rangle$
be a $(x, n)$-simple element of $\mathcal{C}$ with degree less or equal $m$:

1. if $\exists c' \ge c, \uparrow c' \in \phi$, then $\exists a' \ge a, \uparrow a' \in \phi$ or $\exists b' \ge b, \uparrow b' \in \phi$, thus
by induction $e_\phi(a) \not\equiv v'$ or $e_\phi(b) \not\equiv v''$. In both cases $e_\phi(c) \not\equiv v$;

2. if $\downarrow c \notin \phi$, then $\downarrow a \notin \phi$ and $\downarrow b \notin \phi$, thus by induction $e_\phi(a) \not\sim v'$ and $e_\phi(b) \not\sim v''$. Hence we deduce $e_\phi(c) \not\sim v$.

- if $c$ is conclusion of a link $\otimes$ with premises $a: A, b: B$, let $v = \langle v', v'' \rangle$ be a $(x, n)$-simple element of $\mathcal{C}$ with degree less or equal $m$:

1. if $\exists c' \ge c, \downarrow c' \in \phi$, then $e_\phi(c) \not\equiv v$ by the same argument as in the case of the link $\mathcal{C}$;

2. if $\downarrow c \notin \phi$, we split in three cases.
In case $\downarrow a \in \phi$, then $\uparrow b \in \phi$. Of course $\downarrow b \notin \phi$, hence by induction hypothesis 2, $e_\phi(b) \not\sim v''$. Moreover, by induction hypothesis 1 $e_\phi(b) \not\equiv v''$, thus $e_\phi(b) \not\sim v''$. By symmetrical arguments, if $\downarrow b \in \phi$, we deduce $e_\phi(a) \not\sim v'$. In both cases we have $e_\phi(c) \not\sim v$.
In case $↓ a, ↓ b \notin \phi$, then by induction $e_\phi(a) \asymp v'$ and $e_\phi(b) \asymp v''$, which implies $e_\phi(c) \asymp v$.

- if $c$ is conclusion of a link $?d$ then conditions 1,2 follow immediately by induction;

- if $c$ is conclusion of a link $?c$ with premises $a, b$, let $v$ be a $(x, n)$-simple element of $C$ with degree less or equal $m$:

1. if $∃c' \ge c, ↑ c' \in \phi$, then $∃a' \ge a, ↑ a' \in \phi$ or $∃b' \ge b, ↑ b' \in \phi$, thus by induction $e_\phi(a) \not\equiv v'$ or $e_\phi(b) \not\equiv v'$, for any $(x, n)$-simple element $v'$ of $C$ with degree less or equal $m$. From that we conclude $e_\phi(c) \not\equiv v$ by the same argument as in the case of $c$ auxiliary door of a box;

2. if $↓ c \notin \phi$, then $↓ a \notin \phi$ and $↓ b \notin \phi$, thus by induction $e_\phi(a) \asymp v$ and $e_\phi(b) \not\equiv v$. That is $e_\phi(c) \asymp v$.

□

## A.4 Proof of Lemma 17

*Proof (of Lemma 17).* Let $\mathcal{X}$, $\pi$, $k$, $n$, $m$ be as in the hypotheses of the lemma. We prove the lemma by induction on the size of $\pi$.

**Base of induction:** if $\pi$ has only links $ax$ and $?w$, then $\pi$ is visible acyclic, which is contrary to the hypotheses;

**Induction step:** if $\pi$ has a terminal link $l$ among $\mathcal{X}$, $\otimes$, $?d$, $?c$, $!$, then we split in five cases:

- if $l$ is a link $\mathcal{X}$ with conclusion $c: A\mathcal{X}B$ and premises $a: A, b: B$, define $\pi'$ from $\pi$ by erasing $l$ and its conclusion. Suppose $\Pi = A\mathcal{X}B, \Pi''$, hence $\Pi' = A, B, \Pi''$ are the conclusions of $\pi'$. Of course $\pi'$ has a visible cycle, thus by induction hypothesis there is an experience $e' : \pi'$, s.t. for any $(x, n)$-simple element $v'$ in $\mathcal{X}\Pi'$ with degree less or equal $m$, $|e'| \asymp v'$. We define $e : \pi$ as the straightforward extension of $e' : \pi'$ to the missing edge $c$, i.e. for any $\pi$ edge $d$ at depth 0:

$$e(d) = \begin{cases} e'(d) & \text{if } d \in \pi' \\ < e'(a), e'(b) > & \text{if } d = c \end{cases}$$

Let now $v$ be a $(x, n)$-simple element in $\mathcal{X}\Pi$ with degree less or equal to $m$. Since $\Pi = A\mathcal{X}B, \Pi''$, we may write $v = <v_1, v_2, v_3>$, where $v_1, v_2$ and $v_3$ are $(x, n)$-simple elements resp. in $\mathcal{A}, \mathcal{B}$ and $\Pi''$ with degree less or equal to $m$. By hypothesis $|e'| \asymp v$, hence of course $|e| \asymp v$;

- if $l$ is a link $\otimes$ with conclusion $c: A \otimes B$ and premises $a: A, b: B$, define $\pi'$ from $\pi$ by erasing $l$ and its conclusion. Suppose $\Pi = A \otimes B, \Pi''$, hence $\Pi' = A, B, \Pi''$ are the conclusions of $\pi'$.

In case $\pi'$ has a visible cycle, then the assertion follows by induction hypothesis like in the case $l$ is a $\mathcal{X}$.

In case $\pi'$ is visible acyclic, then all the visible cycles of $\pi$ crosses the link $l$ erased in $\pi'$. In this case there is a visible path $\phi$ in $\pi'$ from $↑ a$ to $↓ b$ or from $↑ b$ to $↓ a$, s.t. $\phi$ is not a cycle. Let us suppose $\phi$ is from $↑ a$
to $\downarrow b$ (the other case is symmetric). By lemma 16 there is an experiment $e' : \pi'$ s.t. for any $(x, n)$-simple elements $v_1$ and $v_3$ resp. in $\mathcal{A}$ and $\mathcal{A}\mathcal{P}\Pi'$ with degree less or equal $m$: $e'(a) \sim v_1$, and $< e'(c_1), \dots, e'(c_k) > \sim v_3$ (where $c_1, \dots, c_k$ are the conclusions of $\pi'$ different from $a, b$).

We define $e : \pi$ as the straightforward extension of $e' : \pi'$ to the missing edge $c$, i.e. for any $\pi$ edge $d$ at depth 0:

$$e(d) = \begin{cases} e'(d) & \text{if } d \in \pi' \\ < e'(a), e'(b) > & \text{if } d = c \end{cases}$$

Let now $v$ be a $(x, n)$-simple element in $\mathcal{A}\mathcal{P}\Pi$ with degree less or equal to $m$. Since $\Pi = A \otimes B, \Pi''$, we may write $v = \langle v_1, v_2 \rangle, v_3 \rangle$, where $v_1, v_2$ and $v_3$ are $(x, n)$-simple elements resp. in $\mathcal{A}, \mathcal{B}$ and $\Pi''$ with degree less or equal to $m$. By the hypothesis on $e'$ and the incoherence definition in the $\otimes$ space, we deduce $|e| \sim v$;

- if $l$ is a link $?d$, then the case follows straightforwardly by induction hypotheses;

- if $l$ is a link $?c$ with conclusion $c : ?B$ and premises $a : ?B, b : ?B$, define $\pi'$ from $\pi$ by erasing $l$ and its conclusion. Suppose $\Pi = ?B, \Pi''$, then $\pi'$ has conclusions $\Pi' = ?B, ?B, \Pi''$.

Of course $\pi'$ has a visible cycle, hence by induction there is an experiment $e' : \pi'$, s.t. for any $(x, n)$-simple element $v'$ in $\mathcal{A}\mathcal{P}\Pi'$ with degree less or equal to $m$, $|e'| \sim v'$.

We define $e : \pi$ as the immediate extension of $e' : \pi'$ to the missing edge $c$, i.e. for any $\pi$ edge $d$ at depth 0:

$$e(d) = \begin{cases} e'(d) & \text{if } d \in \pi' \\ e'(a) + e'(b) & \text{if } d = c \end{cases}$$

Let now $v$ be a $(x, n)$-simple element in $\mathcal{A}\mathcal{P}\Pi$ with degree less or equal to $m$. Since $\Pi = ?B, \Pi''$, we may write $v = \langle v_1, v_2 \rangle$, where $v_1$ (resp. $v_2$) is a $(x, n)$-simple element in $?B$ (resp. in $\mathcal{A}\mathcal{P}\Pi'$) with degree less or equal to $m$.

Firstly, let us prove $|e| \sim v [\mathcal{A}\mathcal{P}\Pi]$. Define $v' = \langle v_1, v_1, v_2 \rangle$, which is a $(x, n)$-simple element in $\mathcal{A}\mathcal{P}\Pi'$ with degree less or equal to $m$. By hypothesis $|e'| \sim v'$. Hence we deduce $|e| \sim v$.

Secondly, let us prove $|e| \not\equiv v$. Suppose $|e| \equiv v$ and let us prove a contradiction. Under such a supposition, $\exists v_a, v_b \subseteq v_1, e^o(a) \equiv v_a$ and $e^o(b) \equiv v_b$. Define $v' = \langle v_a, v_b, v_2 \rangle$ and remark that $v'$ is a $(x, n)$-simple element in $\mathcal{A}\mathcal{P}\Pi'$ with degree less or equal $m$. By the definition of the neutrality, $|e'| \equiv v'$, which is contrary to the hypothesis on $|e'|$. Thus we conclude $|e| \not\equiv v$;

- if $l$ is a link $!$, then let $\pi^l$ be the box of $l$, $a : !A$ (resp. $a' : A$) be the conclusion (resp. premise) of $l, b_1 : ?B_1, \dots, b_h : ?B_h$ be the auxiliary doors of $\pi^l$, $c_1 : C_1, \dots, c_t : C_t$ be the conclusions of $\pi$ which are not doors of $\pi^l$, i.e. $\Pi = !A, ?B_1, \dots, ?B_h, C_1, \dots, C_t$.

Define $\pi'$ from $\pi$ by substituting the link $l$ with its box $\pi^l$. Of course $\pi'$ has conclusions $\Pi' = A, ?B_1, \dots, ?B_h, C_1, \dots, C_t$.
Remark that $\pi'$ has a visible cycle, since no visible cycle of $\pi$ passes through the box of $l$, being $l$ terminal. By induction there is an experiment $e' : \pi'$, s.t. for any $(x, n)$-simple element $v'$ in $\mathcal{S}\Pi'$ with degree less or equal $m$, $|e'| \sim v'$.

We define $e : \pi'$ be the extension of $e'$ taking value $n$ [$e'$] on the link ! $l$, i.e. for any edge $d$ if $\pi$ at depth 0:

$$e(d) = \begin{cases} e'(d) & \text{if } d \text{ is not a door of } \pi^l \\ n[e'(a')] & \text{if } d = a \\ ne'(b_i) & \text{if } d = b_i \end{cases}$$

Remark that:

$$|e'| = \langle e'(a'), e'(b_1), \dots, e'(b_h), e'(c_1), \dots, e'(c_t) \rangle$$

$$|e| = \langle n[e'(a')], ne'(b_1), \dots, ne'(b_h), e'(c_1), \dots, e'(c_t) \rangle$$

Let now $v$ be a $(x, n)$-simple element in $\mathcal{S}\Pi$ with degree less or equal $m$. We may write:

$$v = \langle n[v_0], v_1, \dots, v_h, w_1, \dots, w_t \rangle$$

where $v_0, v_i$ for each $i \le h$ and $w_j$ for each $j \le t$ are $(x, n)$-simple elements resp. in $\mathcal{A}$, $\mathcal{B}_i$ and $\mathcal{C}_j$ with degree less or equal to $m$.

Firstly, let us prove $|e| \sim v[\mathcal{S}\Pi]$. Define $v' = \langle v_0, v_1, \dots, v_h, w_1, \dots, w_t \rangle$ and remark that $v'$ is a $(x, n)$-simple element in $\mathcal{S}\Pi'$ with degree less or equal to $m$. Thus by hypothesis $|e'| \sim v'[\mathcal{S}\Pi']$, which implies $|e| \sim v[\mathcal{S}\Pi]$. Secondly, let us prove $|e| \not\equiv v$. Suppose $|e| \equiv v$ and let us prove a contradiction. Under such a supposition, $e'(a) \equiv v_0$, for each $j \le t$, $e'(c_j) \equiv w_j$, and for each $i \le h$, $\exists v'_i \subseteq v_i$, $e^o(b_i) \equiv v'_i$. Define $v' = \langle v_0, v'_1, \dots, v'_h, w_1, \dots, w_t \rangle$ and remark that $v'$ is a $(x, n)$-simple element in $\mathcal{S}\Pi'$ with degree less or equal $m$. By the definition of the neutrality, $|e'| \equiv v'$, which is contrary to the hypothesis on $|e'|$. Thus we conclude $|e| \not\equiv v$.

□

## A.5 Proof of Theorem 18

A cut $l$ can be of the following type:

(ax): if one premise of $l$ is conclusion of an axiom;

(\mathcal{S}/\mathcal{\otimes})$: if the premises of $l$ are conclusions of resp. a $\mathcal{S}$ and a $\mathcal{\otimes}$;

(!/?d): if the premises of $l$ are conclusions of resp. a ! and a ?d at the same depth as $l$;

(!/?w): if the premises of $l$ are conclusions of resp. a ! and a ?w at the same depth as $l$;

(!/?c): if the premises of $l$ are conclusions of a ! and a ?c at the same depth as $l$;
(!#!/): if one premise of $l$ is conclusion of a ! and the other is an auxiliary door of an exponential box at the same depth as $l$.

The cut reduction rules are defined in Figure 9 (see [3] for the details).

**Definition 20.** Let $\pi \rightsquigarrow \beta \pi'$, any edge $a' : A$ of $\pi'$ comes from at most two (resp. at least one) edges of $\pi$, that we call the ancestors of $a'$. Remark that $a'$ has more than one ancestor only in case $\pi'$ is the result of a cut reduction (ax) and $a'$ is the superposition of a conclusion of the erased axiom and a premise of the erased cut.

Conversely, we define the residues of $a$ as those edges of $\pi'$ which have $a$ as ancestor. Remark that a can have 0, 1 or 2 residues, since the cut reduction can erase or duplicate part of $\pi$.

*Proof (of Theorem 18).* Let $\pi \rightsquigarrow \beta \pi'$, we prove that any visible cycle in $\pi'$ is the "residue" of a visible cycle in $\pi$. From that the theorem easily follows.

The proof splits in six cases, depending on which is the cut reduction step applied in $\pi \rightsquigarrow \beta \pi'$. We treat only the case of a (!#!/)-reduction, being the others straightforward.

Let $\pi'$ be the result of a (!#!/)-reduction of $\pi$, $<\uparrow a'_1, \dots, \uparrow a'_n>$ be a path of $\pi'$ which does not cross the cut $m, a_{n-1}, a_n$ be the (unique) ancestors in $\pi$ of resp. $a'_{n-1}$. We define by recursion on $n$ a path $\alpha(<\uparrow a'_1, \dots, \uparrow a'_n>)$ of $\pi$, as follows:

- if $\uparrow a'_{n-1} = \uparrow a'_{n-1}$ and $\uparrow a'_n = \uparrow a'_n$, then $a'_{n-1}$ is conclusion of a link $l$ and $a_n$ is premise of $l$. Define:

$$ \alpha(<\uparrow a'_1, \dots, \uparrow a'_n>) = r(<\uparrow a'_1, \dots, \uparrow a'_{n-2}, \uparrow a'_{n-1}>) * <\uparrow a_n> $$

- if $\uparrow a'_{n-1} = \uparrow a'_{n-1}$ and $\uparrow a'_n = \downarrow a'_n$, then either $a'_{n-1}$ and $a'_n$ are different conclusions of the same link $l$, or they are different doors of the same exponential box associated with a link $!l$. Let $o$ be the link $!$ whose box has been modified by the (!#!/)-reduction, as in Figure 9. We split in two cases:

* if $l \neq o$, define:

$$ \alpha(<\uparrow a'_1, \dots, \uparrow a'_n>) = \alpha(<\uparrow a'_1, \dots, \uparrow a'_{n-2}, \uparrow a'_{n-1}>) * <\downarrow a_n> $$

* if $l = o$, then we split further in two subcases:

* if $a_{n-1}, a_n$ are doors of the same box in $\pi$, define:

$$ \alpha(<\uparrow a'_1, \dots, \uparrow a'_n>) = \alpha(<\uparrow a'_1, \dots, \uparrow a'_{n-2}, \uparrow a'_{n-1}>) * <\downarrow a_n> $$

* if $a_{n-1}$ (resp. $a_n$) is a door of the box $\pi^o$ (resp. $\pi^u$) associated with the link $!o$ (resp. $u$) in $\pi$, define:

$$ \alpha(<\uparrow a'_1, \dots, \uparrow a'_n>) = \alpha(<\uparrow a'_1, \dots, \uparrow a'_{n-2}, \uparrow a'_{n-1}>) * <\downarrow b, \uparrow c, \downarrow a_n> $$
(ax) :

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

(⊗/⊗) :

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

(1/?d) :

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

(1/?w) :

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

(1/?c) :

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

(1/1) :

<figure><img src="image_17.png" /><figcaption>Fig. 9. Cut reduction of MELL</figcaption></figure>
* if $a_{n-1}$ (resp. $a_n$) is a door of the box $\pi^u$ (resp. $\pi^o$) associated with the link ! u (resp. o) in $\pi$, define:

$$ \alpha(<\downarrow a'_1, \dots, \downarrow a'_n>) = \alpha(<\downarrow a'_1, \dots, \downarrow a'_{n-2}, \uparrow a'_{n-1}>) * <\downarrow c, \uparrow b, \downarrow a_n> $$

- if $\downarrow a'_{n-1} = \downarrow a'_{n-1}$ and $\downarrow a'_n = \downarrow a'_n$, then $a'_{n-1}$ is the premise of a link $l$ and $a'_n$ is conclusion of $l$. Define:

$$ \alpha(<\downarrow a'_1, \dots, \downarrow a'_n>) = \alpha(<\downarrow a'_1, \dots, \downarrow a'_{n-2}, \downarrow a'_{n-1}>) * <\downarrow a_n> $$

- if $\downarrow a'_{n-1} = \downarrow a'_{n-1}$ and $\downarrow a'_n = \uparrow a'_n$, then $a'_{n-1}$ and $a'_n$ are different premises of the same link $l$. Remark that by hypothesis $l$ cannot be the cut $m$. Define:

$$ \alpha(<\downarrow a'_1, \dots, \downarrow a'_n>) = \alpha(<\downarrow a'_1, \dots, \downarrow a'_{n-2}, \downarrow a'_{n-1}>) * <\uparrow a_n> $$

It is simple to prove that if $<\downarrow a_1, \dots, \downarrow a'_n>$ is a (visible) cycle of $\pi'$, then $\alpha(<\downarrow a'_1, \dots, \downarrow a'_n>)$ is a (visible) cycle of $\pi$, from which follows the theorem. $\square$