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

HAL
open science

# Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic

Michele Pagani

► To cite this version:

Michele Pagani. Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic. Mathematical Structures in Computer Science, 2007, 17 (2), pp.341-359. 10.1017/S0960129506005652. hal-04670082

HAL Id: hal-04670082

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

Submitted on 11 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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic

MICHELE PAGANI†

Dipartimento di Filosofia – Università Roma Tre
Via Ostiense 234 – 00146 Roma – Italy
pagani@uniroma3.it

Received 10 December 2005; Revised 10 May 2006

We study full completeness and syntactical separability of *MLL* proof nets with the mix rule. The general method we use consists first in addressing the two questions in the less restrictive framework of proof structures, and then in adapting the results to proof nets. At the level of proof structures, we find a semantical characterization of their interpretations in relational semantics, and we define an observational equivalence which is proved to be the equivalence induced by cut elimination. Hence, we obtain a semantical characterization (in coherent spaces) and an observational equivalence for the proof nets with the mix rule.

## 1. Introduction

In the *proofs-as-programs* paradigm a logical proof is a computational process which has to explicit the information implicit in the cut rules.

Such a process can be described from several points of view. From a syntax, a proof can be seen as a graph and the cut reduction rules as graph rewriting rules. From a denotational semantics, a proof can be interpreted as a function invariant under cut reduction. Finally from an observational semantics, a proof can be identified with its behavior with respect to a set of contexts and values.

Each of these points of view provides an equivalence between proofs. Broadly speaking, two proofs are syntactically equivalent when they are reducible to the same graph, in a denotational semantics when associated with the same invariant, observationally when given the same value for any context they are put in.

The question of comparing such points of view and their induced equivalences is a crucial one in modern logic.

When comparing a syntax to a denotational semantics we (mainly) deal with two questions: injectivity (or faithfullness) and surjectivity (or full completeness). A denotational
semantics is injective for a syntax if it interprets with different objects syntactically
non-equivalent proofs. The question of injectivity has been addressed in linear logic by
Tortora de Falco in (Tortora de Falco, 2003). On the other side a semantics is fully
complete for a syntax when it is possible to characterize those objects which are inter-
pretations of proofs. The first full completeness result in linear logic is due to Abramsky
and Jagadeesan in (Abramsky and Jagadeesan, 1994).

When comparing a syntax to an observational semantics we deal with the so-called separation problem. A syntax enjoys separation with respect to an observational semantics if for any two syntactically non-equivalent proofs there exists a context where they behave differently. At the beginning, separation was stated in pure λ-calculus by Morris in (Morris, 1968) as a corollary of Böhm theorem (Böhm, 1968): if $t, t'$ are two distinct $\beta\eta$-normal terms, then there exists a context $C []$ s.t. $C [t]$ is normalizable but $C [t']$ isn't. Later on, this kind of question has been studied by Statman for the simply typed λ-calculus in (Statman, 1983). In a more proof-theoretical framework, separation is a key property of Girard's ludics (Girard, 2001). Some works on separation has been done also in linear logic. The first one is (Mascari and Pedicini, 1994), in the framework of pure proof nets, while in the typed case there is a work by Matsuoka (Matsuoka, 2005), dealing with the separation of the implicational multiplicative linear logic fragment.

In the present paper we study all these questions in a simple case: the multiplicative fragment of linear logic (MLL). Our syntactical objects will be the proof nets, the denotational semantics will be relational and coherent semantics, and we define two observational equivalences between MLL proofs.

The set of proof nets is a subset of a wider set of graphs: the set of proof structures. More precisely, the proof nets are those proof structures which correspond to correct proofs. The very importance of proof structures is that cut reduction is directly defined on them, so we can speak of proof structures reducing to the same graph, as well as of denotational interpretations or observational behaviors of proof structures.

Our general method is to compare syntax, denotational and observational semantics at first at the level of proof structures, with less constraints, and later on to adapt the results to proof nets.

In Section 2 we recall the definition of proof structures and in Section 3 the definition of relational semantics. The main result of Section 3 is the semantical characterization of those sets which are interpretations of proof structures (Theorem 3.3). In Section 6 from this result and from a theorem by Retoré ((Retoré, 1997), here Theorem 6.2) we deduce an alternative proof (with respect to (Tan, 1997)) of the full completeness of coherent semantics with respect to the proof nets of *MLL* with mix (Corollary 6.1).

In Section 4 we introduce an observational equivalence between proof structures (Definition 4.1). The main result of this section is the separation theorem for *MLL* proof structures (Theorem 4.1). As corollaries we prove that the defined observational equivalence coincides with the equivalence induced by cut-elimination (Corollary 4.1) and that such an equivalence is a maximal congruence between proof structures (Corollary 4.2). In Section 7 we weaken the observational equivalence of Definition 4.1 reducing the admissible contexts (Definition 7.1) and we prove (Proposition 7.1) that concerning this weaker equivalence the separation of *MLL* does not hold.
<figure><img src="image_3.png" /><figcaption>Fig. 1. Multiplicative links.</figcaption></figure>

For simplicity, we restrict ourselves to the case of a unique pair of atomic formulas $X$ and $X^{\perp}$, however, all the results in the present paper still hold in the general case with slightly more technical definitions.

## 2. Proof structures

In this section we recall MLL proof structures and MLL cut reduction rules. The **formulas** of MLL are:

$$F ::= X \mid X^{\perp} \mid F \ominus F \mid F \otimes F$$

As always we set $(A \ominus B)^{\perp} = A^{\perp} \otimes B^{\perp}$ and $(A \otimes B)^{\perp} = A^{\perp} \ominus B^{\perp}$. We denote by capital Greek letters $\Sigma, \Pi, \dots$ the sets 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 $\ominus$ or $\otimes$.

Proof structures are oriented graphs (even empty) whose nodes are called **links** and whose edges are labeled by formulas of linear logic. When drawing a proof structure we represent edges oriented up-down so that we may speak of moving *downwardly* or *upwardly* in the graph. 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**). MLL links are the following (see Figure 1):

1. the **axiom** (ax-link), which has two conclusions labeled by dual atomic formulas, but no premise;

2. the **cut** (cut-link), which has two premises labeled by dual formulas but no conclusion;

3. the **par** ($\ominus$-link), which has two ordered premises and one conclusion. If the left premise is labeled by the formula $A$ and the right premise is labeled by the formula $B$, then the conclusion is labeled by the formula $A \ominus B$;

4. the **tensor** ($\otimes$-link), which has two ordered premises and one conclusion. If the left premise is labeled by the formula $A$ and the right premise is labeled by the formula $B$, then the conclusion is labeled by the formula $A \otimes B$.

Each edge is the conclusion of a unique link and the premise of at most one link. Edges which are not the premise of any link are the **conclusions** of the proof structure. If $\pi$ is a proof structure with conclusions $C_1, \dots, C_n$, we define the **closure of $\pi$ with conclusion $C_1 \ominus \dots \ominus C_n$** as the proof structure obtained from $\pi$ by adding the necessary $\ominus$-links below $C_1, \dots, C_n$.

Proof structures are denoted by Greek letters: $\pi, \sigma, \tau, \dots$, the edges by initial Latin letters: $a, b, c, \dots$ and the 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$.
<figure><img src="image_4.png" /><figcaption>Fig. 2. Axiom cut reduction 1.</figcaption></figure>

Remark that axioms introduce just atomic formulas: this is a common way to avoid the $\eta$-expansion rule (see for example (Tortora de Falco, 2003)).

We recall in the framework of proof structures the notion of congruent equivalence, defined by Girard in (Girard, 1991):

**Definition 2.1.** An equivalence $\equiv$ between proof structures is a **congruence** (or **is congruent**) when for all proof structures $\pi_1, \pi_2$, if $\pi_1 \equiv \pi_2$ then $\pi_1$ and $\pi_2$ have the same conclusions, and whenever $\pi'_1$ and $\pi'_2$ have been obtained from $\pi_1$ and $\pi_2$ by adding the same links, $\pi'_1 \equiv \pi'_2$.

The *cut-link* defines the composition between proof structures: if $\pi$ and $\sigma$ are two proof structures with conclusions respectively $\Pi, A$ and $\Sigma, A^{\perp}$, the **composition** of $\pi$ and $\sigma$ on $A, A^{\perp}$, denoted by $[\pi, \sigma]_{A,A^{\perp}}$, is the proof structure with conclusions $\Pi, \Sigma$ obtained by joining $\pi$ and $\sigma$ with a new *cut-link* with premises $A$ and $A^{\perp}$. We omit the indexes $A, A^{\perp}$ in case it is clear which are the premises of the cut.

A proof structure without cuts is called **cut-free**. The *MLL cut reduction rules* are graph rewriting rules which modify a proof structure $\pi$, obtaining a proof structure $\pi'$ with same conclusions as $\pi$. We denote the cut reduction relation between $\pi$ and $\pi'$ as $\pi \rightsquigarrow \beta \pi'$, recalling the $\beta$-reduction of $\lambda$-calculus.

Let $l$ be a cut in a proof structure, the premises of $l$ may be labeled either by dual atomic formulas $X$ and $X^{\perp}$, or by dual compound formulas $A \otimes B$ and $A^{\perp} \otimes B^{\perp}$. The cut reduction rule for $l$ is as follows:

- if $l$ has premises labeled by dual atomic formulas $X$ and $X^{\perp}$, let $m$ be the axiom of which a conclusion is the premise of $l$ labeled by $X$ and let $n$ be the axiom of which a conclusion is the premise of $l$ labeled by $X^{\perp}$. If $m \neq n$, then $l$ is reduced erasing $l, m, n$ and the $l$ premises, and later on linking the remained $m, n$ conclusions through a new axiom link (Figure 2). If $m = n$, then $l$ is reduced simply erasing $l, m$ and the $l$ premises (Figure 3);

- if $l$ has premises labeled by dual compound formulas $A \otimes B$ and $A^{\perp} \otimes B^{\perp}$, let $m$ be the par whose conclusion is the premise of $l$ labeled by $A \otimes B$ and let $n$ be the tensor whose conclusion is the premise of $l$ labeled by $A^{\perp} \otimes B^{\perp}$ (remember that compound formulas do not label conclusions of axioms). Let $a, b$ (resp. $a', b'$) be the left and right premises of $m$ (resp. of $n$). Then $l$ is reduced simply erasing $l, m, n$ and $l$ premises, and later on linking respectively $a, a'$ and $b, b'$ by two new cuts (Figure 4).

The reduction in Figure 3 is maybe unusual, indeed it has a dubious logical meaning. Yet we are not at logic level: we study the reduction rules just as rewriting rules for proof structures. In Section 5 we will upgrade to proof nets, the links will acquire a logical
<figure><img src="image_5.png" /><figcaption>Fig. 3. Axiom cut reduction 2.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 4. $\mathcal{A}/\mathcal{B}$ cut reduction.</figcaption></figure>

meaning as well as the reduction rules. In particular proof nets do not allow “vicious cuts” as the cut between the two conclusions of an axiom.

The reflexive and transitive closure of $\rightsquigarrow_{\beta}$ is denoted by $\rightarrow_{\beta}$. The symmetric closure of $\rightarrow_{\beta}$ is denoted by $=_{\beta}$ and called $\beta$-equivalence.

As it is known, $\rightarrow_{\beta}$ enjoys confluence and strong normalization$^{\dagger}$:

**Theorem 2.1 (Confluence).** For every proof structure $\pi_1, \pi_2$ and $\pi_3$, s.t. $\pi_1 \rightarrow \pi_2$ and $\pi_1 \rightarrow \pi_3$, there is a proof structure $\pi_4$, s.t. $\pi_2 \rightarrow \pi_4$ and $\pi_3 \rightarrow \pi_4$.

**Theorem 2.2 (Strong normalization).** For every proof structure $\pi$, there is no infinite sequence of proof structures $\pi_0, \pi_1, \pi_2, \dots$ s.t. $\pi_0 = \pi$ and $\pi_i \rightsquigarrow \pi_{i+1}$.

Confluence and strong normalization assure that in each equivalence class of $=_{\beta}$ there is one and only one cut-free proof structure. We remark that the only cut-free proof structure without conclusions is the empty graph, hence all the proof structures without conclusions are reduced to the empty graph.

It is well-known that the conclusions of a cut-free proof structure determine it up to the axioms: a cut-free proof structure with conclusions $C_1, \dots, C_n$ is the forest of the $n$ syntax trees of the formulas $C_1, \dots, C_n$ and a set of axioms linking in pairs such forest leaves.

### 3. Relational semantics

Relational semantics associates with MLL formulas sets and with proof structures relations, which are invariant under cut reduction.

<footnote>† Actually in (Girard, 1987), Girard proves that $\rightarrow_{\beta}$ is confluent and strong normalizing for proof nets. We remark that those proofs can be extended straightforwardly to the general case of proof structures.</footnote>
Let $\mathcal{X}$ be a set, a **relational model on $\mathcal{X}$** ($\mathcal{Rel}^{\mathcal{X}}$) associates with formulas sets, in the following way:

— $\mathcal{X}$ is associated with the atomic formulas $X, X^{\perp}$;

— if $A$ and $B$ are associated resp. with $A$ and $B$, then $A \times B$ is associated with $A \otimes B$ and $A \otimes B$.

We denote the elements of sets by final Latin letters $u, v, x, y, z \dots$, and the subsets by initial Greek letters $\alpha, \beta, \dots$.

For each proof structure $\pi$, we define the **interpretation of $\pi$ in $\mathcal{Rel}^{\mathcal{X}}$**, denoted by $\llbracket \pi \rrbracket_{\mathcal{X}}$, where the index $\mathcal{X}$ is omitted if it is clear which set is associated with the atomic formulas.

In case $\pi$ has no conclusion, let $\llbracket \pi \rrbracket$ set as undefined. Otherwise, let $c_1 : C_1, \dots, c_n : C_n$ be the conclusions of $\pi$, $\llbracket \pi \rrbracket$ is a subset of $C_1 \times \dots \times C_n$, which we define by using the notion of experiment. The experiments have been introduced by Girard in (Girard, 1987), and extensively studied in (Tortora de Falco, 2000) by Tortora de Falco.

**Definition 3.1 (Experiment).** A $\mathcal{Rel}^{\mathcal{X}}$ experiment $e$ on a proof structure $\pi$, denoted by $e : \pi$, is a function associating with every edge $a : A$ of $\pi$ an element of $A$, so that the following conditions are respected:

**axiom:** if $a, b$ are the conclusions of an $ax$-link, then $e(a) = e(b)$;

**cut:** if $a, b$ are the premises of a $cut$-link, then $e(a) = e(b)$;

**multiplicative:** if $c$ is the conclusion of a $\otimes$- or $\oplus$-link with premises $a$ and $b$, then $e(c) = \langle e(a), e(b) \rangle$.

Experiments can be viewed as $\pi$ edges decorations either from axioms to conclusions or vice-versa from conclusions to axioms: multiplicative condition determines an experiment either assigning values to the axioms, if cut-condition is satisfied, or assigning values to the conclusions and to the cuts of $\pi$, if axiom-condition is satisfied.

Let $\pi$ be a proof structure with conclusions $c_1 : C_1, \dots, c_n : C_n$ and $e : \pi$ be an experiment, then the **result of e** is the element $\langle e(c_1), \dots, e(c_n) \rangle$ of $C_1 \times \dots \times C_n$. The interpretation of $\pi$ in $\mathcal{Rel}^{\mathcal{X}}$ is the set of the results of all experiments on $\pi$:

$$ \llbracket \pi \rrbracket_{\mathcal{X}} = \{ \langle e(c_1), \dots, e(c_n) \rangle \mid e \text{ is a } \mathcal{Rel}^{\mathcal{X}} \text{ experiment on } \pi \} $$

For each formula $C$ we have on the one hand the proof structures with conclusion $C$, on the other hand the subsets of $C$, being $\llbracket \rrbracket_{\mathcal{X}}$ a function from the proof structures to the subsets of $C$. It is well known that$^{‡}$:

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

**Theorem 3.2 (Injectivity of $\llbracket \rrbracket_{\mathcal{X}}$).** If $\mathcal{X}$ is infinite, then for every proof structures $\pi, \pi', \llbracket \pi \rrbracket_{\mathcal{X}} = \llbracket \pi' \rrbracket_{\mathcal{X}}$ implies $\pi =_{\beta} \pi'$.

<footnote>‡ Actually in (Girard, 1987) (resp. (Tortora de Falco, 2003)) the author proves the semantical soundness (resp. injectivity) in the more restricted case of proof nets. We remark that those proofs can be extended straightforwardly to the general case of proof structures.</footnote>
The main result of this section is to characterize those subsets of $\mathcal{C}$, called complete subsets, which are the interpretations of proof structures with conclusion $\mathcal{C}$ (Theorem 3.3). In this way, $\llbracket \rrbracket_\mathcal{X}$ becomes a bijection between the cut-free proof structures with conclusion $\mathcal{C}$ and the complete subsets of $\mathcal{C}$.

To achieve Theorem 3.3 let us start from the proof of the injectivity of $\llbracket \rrbracket_\mathcal{X}$. Let $\pi$ be a cut-free proof structure with conclusion $\mathcal{C}$, we have already noticed that $\pi$ can be presented as a set of axioms linking the leaves of the syntax tree of $\mathcal{C}$. The proof of the injectivity of $\llbracket \rrbracket_\mathcal{X}$ mainly uses the fact that there exists $u \in \llbracket\pi\rrbracket_\mathcal{X}$ which codes all the pairs of dual leaves linked by an axiom of $\pi$. Indeed such an element $u$ is the result of an injective experiment, defined in (Tortora de Falco, 2000):

**Definition 3.2.** Let $\pi$ be a cut-free proof structure and $e : \pi$ be an experiment. $e$ is **injective** when for all formulas $A$ and edges $a, a'$ labeled by $A$, $e(a) \neq e(a')$.

We remark that, if $\mathcal{X}$ is infinite, any cut-free proof structure has injective experiments: simply take an injective assignment of values to the axioms of the proof structure.

The results of injective experiments are the most informative points of $\mathcal{C}$: we define a pre-order $\succeq$ on the elements of $\mathcal{C}$ (Definition 3.3), measuring how much information on proof structures is coded by an element; as expected, the results of injective experiments are maximal among the (balanced, see Definition 3.4) elements of $\mathcal{C}$. Conversely, in Lemma 3.1 we prove that all the maximals among the (balanced) elements of $\mathcal{A}$ are results of injective experiments.

In Lemma 3.2, we prove that for every proof structure $\pi$, the set $\llbracket\pi\rrbracket$ has the shape $\{v|u \succeq v\}$, where $u$ is the result of an injective experiment on $\pi$. Therefore we define the complete subsets of $\mathcal{C}$ as those subsets of the form $\{v|u \succeq v\}$, for a maximal $u$ among the (balanced) elements of $\mathcal{C}$. In this way we get a characterization for those subsets of $\mathcal{C}$ which are interpretations of proof structures (Theorem 3.3).

An element $u$ of a set $\mathcal{C}$ is a sequence of elements of the basic set $\mathcal{X}$ and the symbols `<, >`. We call the elements of $\mathcal{X}$ which are in $u$ the **atoms** of $u$. We remark that any element $u$ in $\mathcal{C}$ defines a labeling of the edges of the syntax tree of $\mathcal{C}$, in particular the atoms of $u$ will label the leaves of such a tree. An occurrence of an atom $x$ in $u$ is a **positive occurrence** if it labels a subformula $X$ of $\mathcal{C}$, it is a **negative occurrence** if it labels a subformula $X^\perp$ of $\mathcal{C}$.

Having given two elements $x, y \in \mathcal{X}$, we define $u[y/x]$ as the element of $\mathcal{C}$ obtained from $u$ by substituting $y$ for each occurrence of $x$. As always, we extend the definition to simultaneous substitutions $u[y_1/x_1, \dots, y_n/x_n]$.

**Definition 3.3.** Let $\mathcal{C}$ be an MLL formula, $\mathcal{C}$ its associated set and $u, u' \in \mathcal{C}$. We write $\mathbf{u} \succeq \mathbf{u}'$ if there is a substitution $[y_1/x_1, \dots, y_n/x_n]$ so that $u[y_1/x_1, \dots, y_n/x_n] = u'$. We set $\mathbf{u} \approx \mathbf{u}'$ if $u \succeq u'$ and $u' \succeq u$.

In general $\approx$ identifies the results of the experiments different just for a renaming of the values appointed to the conclusions of the axioms.

The following definition allows to take out from $\mathcal{C}$ those elements which cannot be in the interpretation of a proof structure:
**Definition 3.4.** An element $u \in C$ is **balanced**, if for every atom the number of its positive occurrences in $u$ is equal to the number of its negative occurrences.

The property of being balanced is stable under substitution: if $u$ is a balanced element, then $u[y_1/x_1, \dots, y_n/x_n]$ is balanced for every substitution $[y_1/x_1, \dots, y_n/x_n]$.

The pre-order $\succeq$ evaluates how much informative the elements of $C$ are. The results of injective experiments are balanced and maximal among the balanced elements of $C$. We prove the vice-versa in the next lemma:

**Lemma 3.1.** Let $\mathcal{X}$ be an infinite set, $C$ be a set associated with a formula $C$ in $\mathfrak{Rel}^{\mathcal{X}}$. Let $u \in C$ be a balanced element which is maximal among the balanced elements of $C$. There is a cut-free closed proof structure $\pi^u$ with conclusion $C$ and an injective experiment $e^u : \pi^u$ such that the result of $e^u$ is $u$.

*Proof.* From the $C$ tree we get $\pi^u$ up to the axioms. Since $u$ is balanced and maximal among the balanced elements and $\mathcal{X}$ is infinite, each atom $x$ of $u$ has exactly one positive and one negative occurrence in $u$, hence each atom $x$ defines a pair of leaves $X, X^{\perp}$ of the $C$ tree. We get $\pi^u$ by linking with axioms such pairs.

Clearly $u$ is the result of the injective experiment on $\pi^u$ which takes the value $x$ on the pair of edges of type $X, X^{\perp}$ associated with $x$ in $u$. $\square$

**Lemma 3.2.** Let $\mathcal{X}$ be an infinite set and $\pi$ be a closed cut-free proof structure with conclusion $C$. There is a balanced element $u$ in $[[\pi]]_{\mathcal{X}}$ maximal among the balanced elements of $C$. Moreover for any such balanced and maximal $u$, $[[\pi]]_{\mathcal{X}} = \{v|u \succeq v\}$.

*Proof.* Since $\mathcal{X}$ is infinite, there are injective experiments on $\pi$. Let $e : \pi$ be an injective experiment, and $u$ its result. Clearly $u$ is balanced and maximal among the balanced elements of $C$. Now, take any such $u$.

Let $a_1, \dots, a_n$ be the conclusions of type $X$ of the axioms of $\pi$. Let $e' : \pi$ be an experiment and $v$ its result. Clearly $v = u[e'(a_1)/e(a_1), \dots, e'(a_n)/e(a_n)]$, therefore $u \succeq v$.

Conversely, let $v \in C$ be so that $u \succeq v$, then there is a substitution $[y_1/e(a_1), \dots, y_n/e(a_n)]$, so that $v = u[y_1/e(a_1), \dots, y_n/e(a_n)]$. Let $e'$ be the experiment so that $e'(a_1) = y_1, \dots, e'(a_n) = y_n$, clearly $e'$ has $v$ as result. $\square$

**Definition 3.5.** A subset $\alpha \subset C$ is **complete** if there is a balanced element $u \in \alpha$ which is maximal among the balanced elements of $C$ and

$$ \alpha = \{v|u \succeq v\} $$

**Theorem 3.3.** Let $\mathcal{X}$ be an infinite set. Let $C$ be an MLL formula and $C$ its interpretation in $\mathfrak{Rel}^{\mathcal{X}}$. A subset of $C$ is the interpretation of a closed proof structure with conclusion $C$ if and only if it is complete.

*Proof.* Let $\alpha$ be a complete set of $C$. By its definition there is a balanced element $u \in \alpha$ which is maximal among the balanced elements of $C$ and $\alpha = \{v|u \succeq v\}$. By Lemma 3.1 there is a proof structure $\pi^u$ and an injective experiment $e^u : \pi^u$ so that the result of $e^u$ is $u$. By Lemma 3.2, $[[\pi^u]] = \alpha$.
<figure><img src="image_7.png" /><figcaption>Fig. 5. Observational values $\tilde{U}$ and $\Omega$.</figcaption></figure>

Conversely, let $\pi$ be a closed proof structure with conclusion $C$. By Lemma 3.2, $\llbracket \pi \rrbracket$ is complete. $\square$

**4. Observational equivalence of proof structures**

In Definition 4.1 we introduce an observational equivalence $\sim_B$ between proof structures. The main result of this section is Theorem 4.1 by which follows that $=_{\beta}$ and $\sim_B$ are the same equivalence (Corollary 4.1) and that such an equivalence is a maximal congruence (Corollary 4.2).

We choose as observational values the only two cut-free proof structures with conclusion $(X^{\perp} \otimes X^{\perp})\ominus(X\ominus X)$ (Figure 5). We denote the formula $(X^{\perp} \otimes X^{\perp})\ominus(X\ominus X)$ by $\mathbb{B}$, and the two cut-free proof structures with conclusion $\mathbb{B}$ resp. by $\tilde{U}$ and $\Omega$.

A proper axiom with conclusions $C_1, \dots, C_n$ is a link without premises but with $n$ conclusions labeled respectively by $C_1, \dots, C_n$. A context of type $C_1, \dots, C_n$ is a proof structure with conclusion $\mathbb{B}$ where proper axioms with conclusions $C_1, \dots, C_n$ can occur. We denote a context by $C$ [].

Let $\pi$ be a proof structure with conclusions $C_1, \dots, C_n$ and let $C$ [] be a context of the same type. By $C[\pi]$ we denote the proof structure with conclusion $\mathbb{B}$ obtained from $C$ [] substituting $\pi$ for each occurrence of the proper axiom.

**Definition 4.1.** Let $\pi_1, \pi_2$ be proof structures with conclusions $C_1, \dots, C_n$. We say that $\pi_1$ and $\pi_2$ are **observationally equal** (denoted by $\pi_1 \sim_B \pi_2$) if for all contexts $C$ [] of type $C_1, \dots, C_n$, $C[\pi_1] =_\beta C[\pi_2]$.

Clearly $\sim_B$ is a congruence. By Theorem 4.1 we prove that $\sim_B$ and $=_{\beta}$ are indeed the same equivalence (Corollary 4.1):

**Theorem 4.1 (Separation of MLL).** Let $\pi_1$ and $\pi_2$ be two closed proof structures with conclusion $C$. If $\pi_1 \neq_{\beta} \pi_2$, then there is a proof structure $\sigma$ with conclusion $C^{\perp}, \mathbb{B}$, such that $[\sigma, \pi_1] \to_{\beta} \tilde{U}$ and $[\sigma, \pi_2] \to_{\beta} \Omega$.

*Proof.* Let $\pi_1, \pi_2$ be two different cut-free proof structures with conclusion $C$. Let
$1,...,2n$ be an enumeration of the leaves of the syntax tree of $C$, so that the odd numbers enumerate the leaves labeled by $X$ and the even numbers those labeled by $X^\perp$.

We have already noticed that $\pi_1, \pi_2$ can be presented as bijections from the odd to the even numbers of $\{1,...,2n\}$. Since $\pi_1 \neq \pi_2$, there is an odd number $o \le 2n$ such that $\pi_1(o) = e$ and $\pi_2(o) = e'$ for $e \neq e'$.

We define the proof structure $\sigma$ with conclusions $C^\perp, \mathbb{B}$, such that $[\pi_1, \sigma] \to_\beta \tilde{U}$ and $[\pi_1, \sigma] \to_\beta \Omega$. The forest of the syntax trees of $C^\perp, \mathbb{B}$ has $2n+4$ leaves. The enumeration given above of the leaves of the syntax tree of $C$ induces an enumeration $1, ..., 2n, 2n+1, ..., 2n+4$ of the leaves of the forest, so that:

- the odd (resp. even) numbers in $\{1, ..., 2n\}$ enumerate the leaves labeled by $X^\perp$ (resp. $X$) above $C^\perp$;

- the odd (resp. even) numbers in $\{2n+1, ..., 2n+4\}$ enumerate the leaves labeled by $X$ (resp. $X^\perp$) above $\mathbb{B}$.

In particular we remark that $e, e'$ are now associated with leaves labeled by $X$ above $C^\perp$ and $o$ with a leaf labeled by $X^\perp$ above $C^\perp$, finally $2n+1$ and $2n+3$ (resp. $2n+2$ and $2n+4$) are the two leaves labeled by $X$ (resp. $X^\perp$) above $\mathbb{B}$.

$\sigma$ is any bijection between the leaves labeled by $X$ and those labeled by $X^\perp$, so that $\sigma(o) = 2n+1$, $\sigma(e) = 2n+2$ and $\sigma(e') = 2n+4$. Clearly we have that $[\sigma, \pi_1] \to_\beta \tilde{U}$ and $[\sigma, \pi_2] \to_\beta \Omega$. $\square$

**Corollary 4.1 (Equality of $\sim_{\mathbb{B}}$ and $=_{\beta}$).** Let $\pi_1$ and $\pi_2$ be two proof structures with same conclusions, $\pi_1 \sim_{\mathbb{B}} \pi_2$ iff $\pi_1 =_{\beta} \pi_2$.

*Proof*. Let $\pi_1$ and $\pi_2$ be two proof structures with same conclusions, we may suppose $\pi_1, \pi_2$ closed, since both $\sim_{\mathbb{B}}$ and $=_{\beta}$ are congruences. By the confluence of $=_{\beta}$, if $\pi_1 =_{\beta} \pi_2$ then $\pi_1 \sim_{\mathbb{B}} \pi_2$, the converse holds by Theorem 4.1. $\square$

**Corollary 4.2 (Maximality of $=_{\beta}$).** Let $\equiv$ be a congruence which contains $=_{\beta}$, then either $\equiv$ is equal to $=_{\beta}$ or $\equiv$ collapses.

*Proof.* Let $\equiv$ be a congruence containing $=_{\beta}$ and let us suppose that there are two distinct proof structures $\pi_1, \pi_2$ such that $\pi_1 \equiv \pi_2$ but $\pi_1 \neq_{\beta} \pi_2$. We prove $\tau_1 \equiv \tau_2$, for every proof structure $\tau_1, \tau_2$ with same conclusions.

Since $\equiv$ is a congruence we can suppose $\pi_1$ and $\pi_2$ to be closed with same conclusion $C$. Since $\pi_1 \neq_{\beta} \pi_2$, by Theorem 4.1 there is a proof structure $\sigma$ with conclusions $C^\perp, \mathbb{B}$, such that $[\pi_1, \sigma] \to_\beta \tilde{U}$ and $[\pi_2, \sigma] \to_\beta \Omega$. By the congruence of $\equiv$, we deduce $[\pi_1, \sigma] \equiv [\pi_2, \sigma]$, hence $\tilde{U} \equiv \Omega$.

Let $\tau_1, \tau_2$ be two distinct proof structures with same conclusions, we prove that $\tau_1 \equiv \tau_2$. Since $\equiv$ is a congruent extension of $=_{\beta}$, we can suppose $\tau_1, \tau_2$ to be cut-free and with only one conclusion $D$. Let $1,..., 2n$ be an enumeration of the leaves of the syntax tree of $D$, so that the odd numbers enumerate the leaves labeled by $X$ and the even numbers the ones labeled by $X^\perp$. Since $D$ has at least two distinct cut-free proof structures (i.e. $\tau_1, \tau_2$), $D$ has at least two occurrences of $X$ and two of $X^\perp$, i.e. $n \ge 2$.

We have already seen that $\tau_1, \tau_2$ can be presented as bijections from the odd to the even numbers of $\{1,...,2n\}$. Since $\tau_1 \neq \tau_2$, there is an odd number $o \le 2n$ such that
$\tau_1(o) \neq \tau_2(o)$, let us choose $o$ minimal and let $\tau_1(o) = e$, $\tau_2(o) = e'$ and $\tau_2^{-1}(e) = o'$. By minimality of $o$, $o < o'$.

Now, we define a proof structure $\sigma$ with conclusions $D^{\perp}, D, B^{\perp}$. The forest of the syntax trees of such conclusions has $2n + 2n + 4$ leaves. The above enumeration of the leaves of the syntax tree of $D$ induces an enumeration $1, \dots, 2n, 2n+1, \dots, 4n, 4n+1, \dots, 4n+4$ of the forest leaves, so that:

- the odd (resp. even) numbers in $\{1, \dots, 2n\}$ enumerate the leaves labeled by $X^{\perp}$ (resp. $X$) above $D^{\perp}$;

- the odd (resp. even) numbers in $\{2n+1, \dots, 4n\}$ enumerate the leaves labeled by $X$ (resp. $X^{\perp}$) above $D$;

- the odd (resp. even) numbers in $\{4n+1, \dots, 4n+4\}$ enumerate the leaves labeled by $X^{\perp}$ (resp. $X$) of the tree of $B^{\perp}$.

In particular we remark that $e$ and $e'$ are associated with leaves labeled by $X$ above $D^{\perp}$, while $2n + e$ and $2n + e'$ are associated with leaves labeled by $X^{\perp}$ above $D$, and finally $4n+1$ and $4n+3$ (resp. $4n+2$ and $4n+4$) are the two leaves labeled by $X$ (resp. $X^{\perp}$) above $B$.

We set $\sigma(e) = 4n+2$, $\sigma(e') = 4n+4$, $\sigma(2n+e) = 4n+1$, $\sigma(2n+e') = 4n+3$, and for all the others $i \le 2n$, $\sigma(i) = 2n+i$.

The peculiarity of $\sigma$ is that the action of $[\sigma, \mathcal{U}]$ is the identity, while the action of $[\sigma, \Omega]$ is the flip of $e$ and $e'$. More precisely, for any proof structure $\pi$ with conclusion $D$, $[[\sigma, \mathcal{U}], \pi] \to_{\beta} \pi$, while $[[\sigma, \Omega], \pi] \to_{\beta} \pi'$, where $\pi'$ is obtained from $\pi$ by flipping $e$ and $e'$. Moreover, by the congruence of $\equiv$ and the fact that $\mathcal{U} \equiv \Omega$, we have $[\sigma, \mathcal{U}] \equiv [\sigma, \Omega]$.

Now, by induction on $2n-o$ we prove that $\tau_1 \equiv \tau_2$:

- if $2n-o=1$, then $o=2n-1$ and $o'=2n$ and $\tau_1(o') = e'$. As we have remarked, $[[\sigma, \mathcal{U}], \tau_1] \to_{\beta} \tau_1$ and $[[\sigma, \Omega], \tau_1] \to_{\beta} \tau_2$. Since $[\sigma, \mathcal{U}] \equiv [\sigma, \Omega]$, we get $\tau_1 \equiv \tau_2$;

- if $2n-o > 1$. As we have remarked, $[[\sigma, \mathcal{U}], \tau_1] \to_{\beta} \tau_1$ and $[[\sigma, \Omega], \tau_1] \to_{\beta} \tau_3$, where $\tau_3$ is obtained from $\tau_1$ by flipping $e$ and $e'$. In particular $\tau_3(e') = o$, so that $\tau_2$ and $\tau_3$ at most differ on an $o'' > o$, thus, by induction hypothesis $\tau_3 \equiv \tau_2$. Therefore, $\tau_1 \equiv [[\sigma, \mathcal{U}], \tau_1] \equiv [[\sigma, \Omega], \tau_1] \equiv \tau_3 \equiv \tau_2$.

□

Relational semantics defines a congruence $\equiv_{\mathfrak{R}\mathcal{E}\mathfrak{I}}$ between proof structures, what means $\pi_1 \equiv_{\mathfrak{R}\mathcal{E}\mathfrak{I}} \pi_2$ if for all $\mathcal{X}, [[\pi_1]]_{\mathcal{X}} = [[\pi_2]]_{\mathcal{X}}$. By the soundness of the relational semantics we know that $=_{\beta} \subseteq \equiv_{\mathfrak{R}\mathcal{E}\mathfrak{I}}$. Now, by Corollary 4.2 we get the converse $\equiv_{\mathfrak{R}\mathcal{E}\mathfrak{I}} \subseteq =_{\beta}$, i.e. a proof of the injectivity of the relational semantics, alternative to that in (Tortora de Falco, 2003).

## 5. Proof nets

It is well known that MLL sequent calculus is defined by the following rules (Girard, 1987):
$$ \frac{\frac{\vdash X, X^{\perp}}{\vdash X, X^{\perp}} ax}{\frac{\vdash \Gamma, A, B}{\vdash \Gamma, A \otimes B}} \stackrel{\gamma}{\rightleftharpoons} \frac{\frac{\vdash \Gamma, A}{\vdash \Gamma, \Delta}}{\frac{\vdash \Gamma, A \otimes B}{\vdash \Gamma, \Delta, A \otimes B}} \otimes $$

which can be enlarged with the mix rule:

$$ \frac{\frac{\vdash \Gamma}{\vdash \Gamma, \Delta}}{\vdash \Gamma, \Delta} mix $$

In this paper we refer to the sequent calculus enlarged with the mix rule.

The MLL sequent calculus proofs can be translated into proof structures: there is a function, called **desequentialization**, which associates with a sequent proof *P* a proof structure (*P*)•. (*P*)• is defined by induction on *P* (see (Girard, 1987)):

- if *P* is an axiom with conclusions *X*, *X*<sup>⊥</sup>, then (*P*)• is an axiom link with conclusions *X*, *X*<sup>⊥</sup>;

- if *P* ends in a ⊗-rule, having as premise the subproof *P*′, then (*P*)• is obtained by adding to (*P*′)• the ⊗-link corresponding to the ⊗-rule;

- if *P* ends in a ⊗-rule (resp. *cut*-rule), with premises the subproofs *P*′ and *P*″, then (*P*)• is obtained by connecting (*P*′)• and (*P*″)• by means of the ⊗-link (resp. *cut*-link) corresponding to the ⊗-rule (resp. *cut*-rule);

- if *P* ends in a *mix*-rule, with premises the subproofs *P*′ and *P*″, then (*P*)• is obtained by taking the disjoint union of (*P*′)• and (*P*″)•.

A **proof net** is a proof structure associated with a sequent calculus proof. A unique proof net can be associated with several sequent calculus proofs: it yields an abstract representation of the sequent proofs modulo inessential commutation of rules (see (Bellin and de Wiele, 1995)). We highlight that both semantical injectivity and syntactical separability can be studied in linear logic thanks to such abstractions from inessential commutations.

As it is known, there are many geometrical characterizations of MLL proof nets, called **correctness criteria** (for example in (Girard, 1987) or (Danos and Regnier, 1989)). We recall here the criterion from (Danos and Regnier, 1989).

A **correctness graph** of a proof structure $\pi$ is a subgraph of $\pi$ which is obtained by erasing one premise for each $\otimes$-link. A proof structure is **correct** if all its correctness graphs are acyclic. Danos and Regnier prove in (Danos and Regnier, 1989) the following theorem:

**Theorem 5.1.** A proof structure is correct if and only if it is a proof net.

In Section 6 we recall a result by Retoré ((Retoré, 1997)), providing a semantical characterization of MLL correctness by means of coherent semantics. Such a result, together with Theorem 3.3, proves the correspondence between proof nets and complete cliques (Corollary 6.1).
**6. Coherent semantics**

A coherent space $\mathcal{X}$ is a couple $(|\mathcal{X}|, \mathcal{C})$, where $|\mathcal{X}|$ is a set, called the **web of** $\mathcal{X}$, and $\mathcal{C}$ is a binary relation in $|\mathcal{X}|$ which is reflexive and symmetric, called the **coherence of** $\mathcal{X}$. A **clique of** $\mathcal{X}$ is a subset of $|\mathcal{X}|$ whose elements are pairwise coherent.

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

- $x \mathcal{C} y$, if $x \mathcal{C} y$ and $x \neq y$;

- $x \mathcal{C} \tilde{y}$, if not $x \mathcal{C} y$;

- $x \mathcal{C} \tilde{y}$, if not $x \mathcal{C} y$.

Remark that we may define a coherent space specifying its web and one among its relations $\mathcal{C}, \mathcal{C}', \mathcal{C}^\prime, \mathcal{C}^\prime\mathcal{C}, \mathcal{C}^\prime\mathcal{C}^\prime$.

A coherent space is identified with a graph whose vertex set is $|\mathcal{X}|$ and whose edges set is the extension of $\mathcal{C}$.

Let $\mathcal{X}$ be a coherent space, a **coherent model on $\mathcal{X}$** ($\mathcal{Coh}^{\mathcal{X}}$) associates with MLL formulas coherent spaces, defined by induction on the formulas, as follows:

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

- with $A^{\perp}$ it associates $A^{\perp}$ defined as follows: $|A^{\perp}| = |A|$, the coherence of $A^{\perp}$ is the incoherence of $A$, i.e. $x \mathcal{C} y$ [$A^{\perp}$] iff $x \mathcal{C} \tilde{y}$ [$A$];

- with $A \otimes B$ it associates $A \otimes B$ defined as follows: $|A \otimes B| = |A| \times |B|$ and $<a, b> \mathcal{C} <a', b' >$ [$A \otimes B$] iff $a \mathcal{C} a'$ [$A$] and $b \mathcal{C} b'$ [$B$].

Of course, the space $A \mathcal{C} B$ is defined by $(A^{\perp} \otimes B^{\perp})^{\perp}$.

Remark that the web associated with a formula $A$ by $\mathcal{Coh}^{\mathcal{X}}$ is precisely the interpretation of $A$ in $\mathfrak{Rel}^{|\mathcal{X}|}$.

Let $\pi$ be a proof structure with conclusions $c_1 : C_1, \dots, c_n : C_n$, the **interpretation** of $\pi$ in $\mathcal{Coh}^{\mathcal{X}}$ is a subset of $|C_1 \mathcal{C} \dots \mathcal{C} n|$, denoted by $[[\pi]]_{\mathcal{X}}$, where the index $\mathcal{X}$ is omitted in case it is clear which coherent space is associated with $X$.

$[[\pi]]$ is defined exactly in the same way as in relational semantics (see Section 3). We have the same definitions concerning the **experiment $e$** on a proof structure $\pi$, its **result**, and the interpretation $[[\pi]]$. The relational interpretation of $\pi$ differs from the coherent one only in presence of exponentials: if $\pi$ is an MLL proof structure, $[[\pi]]_{\mathfrak{Rel}} = [[\pi]]_{\mathcal{Coh}}$.

What we achieve by introducing coherence is that the set $[[\pi]]_{\mathcal{X}}$ can be or not a clique. Girard proves in (Girard, 1987) that if $\pi$ is a proof net then $[[\pi]]_{\mathcal{X}}$ is a clique (Theorem 6.1). Retoré proves the converse for the cut-free proof nets (Theorem 6.2), hence the correctness of a cut-free proof structure corresponds to the pairwise coherence of the results of its experiments:

**Theorem 6.1.** If $\pi$ is a proof net then $[[\pi]]_{\mathcal{X}}$ is a clique.

**Theorem 6.2.** Let $\pi$ be a cut-free proof structure and $\mathcal{X}$ be a coherent space with at least $x, y, z$, such that $x \mathcal{C} y$ and $x \mathcal{C} \tilde{z}$. If $[[\pi]]_{\mathcal{X}}$ is a clique then $\pi$ is a proof net.

Since the web of a coherent space is a set, we can introduce the pre-order $\succeq$ (Definition 3.3) and the notion of **complete subset** (Definition 3.5) on webs exactly in the same way as we did with relational semantics.
If $\mathcal{A}$ is a coherent space, a **complete clique** of $\mathcal{A}$ is a complete subset of $|\mathcal{A}|$ which is a clique, then:

**Corollary 6.1.** Let $\mathcal{X}$ be a coherent space whose web is infinite and with $x, y, z$, such that $x \stackrel{\sim}{y}$ and $x \stackrel{\sim}{z}$. Let $C$ be an MLL formula and $C$ its interpretation in $\mathcal{Coh}^{\mathcal{X}}$.

A subset of $\mathcal{C}$ is the interpretation of a closed proof net with conclusion $C$ if and only if it is a complete clique.

*Proof.* Let $\alpha$ be a complete clique of $\mathcal{C}$. Since $\alpha$ is complete, by Theorem 3.3, there is a closed cut free proof structure $\pi$ with conclusion $C$ such that $[\pi] = \alpha$. Since $\alpha$ is a clique, by Theorem 6.2, $\pi$ is a proof net.

Conversely, if $\pi$ is a proof net, by Theorem 6.1 $[\pi]$ is a clique, and by Theorem 3.3 $[\pi]$ is complete. □

**7. Observational equivalence of proof nets**

The observational equivalence $\sim_{\mathbb{B}}$ (Definition 4.1) depends on the proof structures behaviors within all possible contexts. In this section we would like to restrict the observations just to the correct contexts.

At first, we remark that the only two proof structures $\mathcal{U}$ and $\Omega$ with conclusion $\mathbb{B}$ (Figure 5) are correct, therefore we can keep them as observational values. At second, we extend the correctness criterion to contexts. A **correctness graph** of a context is a subgraph obtained by erasing one premise for each $\mathcal{X}$-link. A context **is correct** if all its correctness graphs are acyclic.

**Definition 7.1.** Let $\pi_1, \pi_2$ be two proof nets with conclusions $C_1, \dots, C_n$. We say that $\pi_1$ and $\pi_2$ are **observationally weak equal** ($\pi_1 \sim_{\mathbb{B}}^w \pi_2$) if for all the correct contexts $C$ [] of type $C_1, \dots, C_n$, $C[\pi_1] =_{\beta} C[\pi_2]$.

Clearly $=_{\beta} \subseteq \sim_{\mathbb{B}}^w$. The main result of this section is Proposition 7.1, which states that $=_{\beta} \subsetneq \sim_{\mathbb{B}}^w$: there are proof nets which are observationally weak equal but not $\beta$-equivalent (hence, neither observationally equal).

Such a result does not clash with Corollary 4.2, stating that $=_{\beta}$ is a maximal congruence. It means that $\sim_{\mathbb{B}}^w$ is not a congruence when extended to proof structures. Indeed $\sim_{\mathbb{B}}^w$ is defined only between proof nets but not between proof structures in general, therefore if $\pi_1$ and $\pi_2$ are two observationally weak equal proof nets, and if $\pi'_1$ and $\pi'_2$ have been obtained from $\pi_1$ and $\pi_2$ by adding the same links, $\pi'_1 \not\sim_{\mathbb{B}}^w \pi'_2$ could happen simply because $\pi'_1$ and $\pi'_2$ are not correct.

Remark that in general a context can be quite complex, namely the proper axioms might be whenever and wherever we want them. Before attacking Proposition 7.1, it is thus convenient to restrain our observations to the simplest contexts, which are the proof nets themselves:

**Lemma 7.1 (Context lemma).** Let $\pi_1$ and $\pi_2$ be two proof nets with conclusions $C_1, \dots, C_n$. Let $\pi_1^*$ and $\pi_2^*$ be the two closures of $\pi_1, \pi_2$ with conclusion $C_1 \mathcal{X} \dots \mathcal{X} C_n$.
<figure><img src="image_8.png" /><figcaption>Fig. 6. Example of proof nets $\pi_1, \pi_2$ with conclusion $((X \otimes X)\mathcal{X}X)\mathcal{X}(X^{\perp} \otimes X^{\perp})\mathcal{X}X^{\perp}$.</figcaption></figure>

Then $\pi_1 \asymp_{\mathbb{B}}^{w} \pi_2$ iff there is a proof net $\sigma$ with conclusions $C_1^{\perp} \otimes \dots \otimes C_n^{\perp}, \mathbb{B}$, such that $[\pi_1^*, \sigma] \neq_{\beta} [\pi_2^*, \sigma]$.

*Proof.* The "if" part is immediate. Conversely, let $\pi_1$ and $\pi_2$ be two proof nets with same conclusions $C_1, \dots, C_n$ such that $\pi_1 \asymp_{\mathbb{B}} \pi_2$. We prove that there is a proof net $\sigma$ with conclusions $C_1^{\perp} \otimes \dots \otimes C_n^{\perp}, \mathbb{B}$, such that $[\pi_1^*, \sigma] \neq_{\beta} [\pi_2^*, \sigma]$.

By Definition 7.1, there is a correct context $C$ such that $C[\pi_1] \neq_{\beta} C[\pi_2]$. We enumerate by $1, \dots, k$ the occurrences of the proper axiom in $C$. For each $i \le k$, let $\sigma_i$ be the proof net obtained from $C$ substituting $\pi_1$ to the occurrences $1, \dots, i$ of the proper axiom and $\pi_2$ to the occurrences $i+1, \dots, k$. Clearly, $\sigma_0 = C[\pi_2] \neq_{\beta} C[\pi_1] = \sigma_k$, hence there is an $i$ such that $\sigma_i \neq_{\beta} \sigma_{i+1}$. $\sigma$ is obtained from $C$ in two steps. At first, we substitute $\pi_1$ to the occurrences $1, \dots, i$ of the proper axiom in $C$ and $\pi_2$ to the occurrences $i+2, \dots, k$. At second, we substitute the $i+1$-th occurrence of the proper axiom with the set of the $n$ axioms with conclusions respectively $C_1^{\perp}, C_1, \dots, C_n^{\perp}, C_n$ and we link the conclusions $C_1^{\perp}, \dots, C_n^{\perp}$ with tensors, so as to get a unique conclusion $C_1^{\perp} \otimes \dots \otimes C_n^{\perp}$.

Clearly $\sigma$ is correct, moreover $[\pi_1^*, \sigma] =_{\beta} \sigma_i \neq_{\beta} \sigma_{i+1} =_{\beta} [\pi_2^*, \sigma]$.

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

Now, let us prove that $\sim_{\mathbb{B}}^{w}$ is a strict extension of $=_{\beta}$:

**Proposition 7.1.** There are proof nets $\pi_1, \pi_2$ such that $\pi_1 \neq_{\beta} \pi_2$ and $\pi_1 \sim_{\mathbb{B}}^{w} \pi_2$.

*Proof.* Let $C$ be the formula $((X \otimes X)\mathcal{X}X)\mathcal{X}(X^{\perp} \otimes X^{\perp})\mathcal{X}X^{\perp}$, and $\pi_1, \pi_2$ be any two different cut-free proof nets with conclusion $C$ (take for example those in Figure 6).

Let us suppose $\pi_1 \asymp_{\mathbb{B}}^{w} \pi_2$ and let us prove the absurdity. By Lemma 7.1 there is a proof net $\sigma$ with conclusions $C^{\perp}, \mathbb{B}$, such that $[\pi_1, \sigma] \neq_{\beta} [\pi_2, \sigma]$. Since $\mathcal{U}$ and $\Omega$ are the only two cut-free proof nets with conclusion $\mathbb{B}$, we may suppose $[\pi_1, \sigma] \to_{\beta} \mathcal{U}$ and $[\pi_2, \sigma] \to_{\beta} \Omega$.

Let $\mathcal{X}$ be a coherent space with $x, y, z \in |\mathcal{X}|$, such that $x \mathcal{V} y, x \mathcal{V} z$ and $y \mathcal{V} z$: we will prove that $[[\sigma]]_{\mathcal{X}}$ is not a clique, hence contradicting Theorem 6.1.

We remark that $\langle\langle x, z \rangle, \langle x, z \rangle\rangle \in [[\mathcal{U}}]$ and $\langle\langle x, z \rangle, \langle z, x \rangle\rangle \in [[\Omega}}$, therefore there are $u \in [[\pi_1]]$ and $v \in [[\pi_2]]$ such that $\langle u, \langle\langle x, z \rangle, \langle x, z \rangle\rangle\rangle, \langle v, \langle\langle z, x \rangle, \langle z, x \rangle\rangle\rangle \in [[\sigma}}$.
<figure><img src="image_10.png" /><figcaption>Fig. 7. Non-correct proof structure $\sigma$ with conclusion $C^{\perp}, \mathbb{B}$.</figcaption></figure>

By Theorem 6.1, $\llbracket \pi_1 \rrbracket$ and $\llbracket \pi_2 \rrbracket$ are complete cliques, thus for all $u', v' \in |C|$, s.t. $u' \preceq u$ (resp. $v' \preceq v$), $u' \in \llbracket \pi_1 \rrbracket$ (resp. $v' \in \llbracket \pi_2 \rrbracket$). In particular, let $w_1, \dots, w_n$ be the atoms different from $z$ and $x$ in $u$ and $v$. We define $u' = u[x/w_1, \dots, x/w_n]$ (resp. $v' = v[x/w_1, \dots, x/w_n]$). Since $u' \preceq u$ (resp. $v' \preceq v$), $u' \in \llbracket \pi_1 \rrbracket$ (resp. $v' \in \llbracket \pi_2 \rrbracket$); moreover, since $\llbracket \sigma \rrbracket$ is a complete clique too and $\langle u', \langle\langle x, z \rangle, \langle x, z \rangle \rangle \preceq \langle u, \langle\langle x, z \rangle, \langle x, z \rangle \rangle$ (resp. $\langle v', \langle\langle x, z \rangle, \langle x, z \rangle \rangle \preceq \langle v, \langle\langle x, z \rangle, \langle z, x \rangle \rangle \rangle$), we have that $\langle u', \langle\langle x, z \rangle, \langle x, z \rangle \rangle$, $\langle v', \langle\langle x, z \rangle, \langle z, x \rangle \rangle \in \llbracket \sigma \rrbracket$.

Now, let us look at the atom $a$ (resp. $b$) of $u'$ (resp. $v'$) corresponding to the bold occurrence of $X$ in $C^{\perp} = ((X^{\perp} \otimes X^{\perp}) \otimes X^{\perp}) \otimes (X \otimes X) \otimes \mathbf{X}$.

If $a = x$ and $b = z$ (or vice-versa, $a = z, b = x$), then $a \sim b[X]$, which implies $u' \sim v' [C^{\perp}]$ by the definition of the coherent spaces associated with $C^{\perp}$. Moreover, $\langle\langle x, z \rangle, \langle x, z \rangle \rangle \sim \langle\langle x, z \rangle, \langle z, x \rangle \rangle [\mathbb{B}]$, by the definition of the coherent spaces associated with $\mathbb{B} = (X^{\perp} \otimes X^{\perp}) \otimes (X \otimes X)$. Thus, $\langle u', \langle\langle x, z \rangle, \langle x, z \rangle \rangle \sim \langle v', \langle\langle x, z \rangle, \langle z, x \rangle \rangle [C^{\perp} \otimes \mathbb{B}]$, i.e. $\llbracket \sigma \rrbracket$ is not a clique.

If $a = b$, let us suppose $a, b = x$ (the case $a, b = z$ being similar). In this case we consider $u'' = u'[y/z]$ and $v'' = v'[z/x, x/z]$. Since $\langle u', \langle\langle x, z \rangle, \langle x, z \rangle \rangle \approx \langle u'', \langle\langle x, y \rangle, \langle x, y \rangle \rangle$ (resp. $\langle v', \langle\langle x, z \rangle, \langle z, x \rangle \rangle \approx \langle v'', \langle\langle z, x \rangle, \langle z, x \rangle \rangle$), we deduce that $\langle u'', \langle\langle x, y \rangle, \langle x, y \rangle \rangle$, $\langle v'', \langle\langle z, x \rangle, \langle x, z \rangle \rangle \in \llbracket \sigma \rrbracket$. Since $x \sim z [X]$, we infer $u'' \sim v'' [C^{\perp}]$ by the definition of the coherent spaces associated with $C^{\perp}$. Moreover, $\langle\langle x, y \rangle, \langle x, y \rangle \rangle \sim \langle\langle z, x \rangle, \langle x, z \rangle \rangle [\mathbb{B}]$, by the definition of the coherent spaces associated with $\mathbb{B}$. Thus, $\langle u'', \langle\langle x, y \rangle, \langle x, y \rangle \rangle \sim \langle v'', \langle\langle z, x \rangle, \langle x, z \rangle \rangle [C^{\perp} \otimes \mathbb{B}]$, i.e. $\llbracket \sigma \rrbracket$ is not a clique. $\square$

We end this section with some remarks on the above proposition.

The failure of the equality between $=_{\beta}$ and $\sim_{\mathbb{B}}^w$ does not depend on the formula $\mathbb{B}$ chosen as the type for the observational values. Indeed for any formula $A$ we may denote by $\sim_A^w$ the observational weak equivalence defined by looking at the correct contexts with conclusion $A$ instead of $\mathbb{B}$, getting all the same $=_{\beta} \preceq \sim_A^w$.

In simple typed $\lambda$-calculus we can prove a separation theorem (analogous to Theorem
4.1) only if we substitute the atom X with more complex formulas (see (Statman, 1983) and (Joly, 2000)). One might thus think that Proposition 7.1 is due to the fact that we have not allowed the substitution of the atom X in Definition 7.1. It is not so. Actually the atom substitution is usefull in presence of exponentials (like in λ-calculus), but it is useless in a linear framework (like MLL). Indeed the proof of Proposition 7.1 can be easily extended to the case we allow the substitution of X with more complex MLL formulas.

The failure of the equality between $=\beta$ and $\sim_B^w$ is actually due to the lack of garbage collectors among the correct contexts. Proof structures have garbage collectors (the cyclic cuts, erased by $\beta$-reduction), hence we can prove Theorem 4.1, but the proof nets (which have to be correct) have not. For example recall the proof nets $\pi_1, \pi_2$ in Figure 6: $\pi_1$ and $\pi_2$ are separable by the non-correct proof structure in Figure 7, in fact $[\pi_1, \sigma] \to_\beta \mathcal{U}$ and $[\pi_2, \sigma] \to_\beta \Omega$. Remark that during the reductions of $[\pi_1, \sigma]$ and $[\pi_2, \sigma]$ we meet cyclic cuts.

In this framework there is an interesting result by Matsuoka in (Matsuoka, 2005), dealing with the intuitionistic multiplicative linear logic fragment (which corresponds to the linear λ-calculus with pairing). The author notices that such a fragment has correct garbage collectors; from that, he proves a separation theorem.

## 8. Concluding remarks

We have dealt with different equivalences between MLL proofs: the $\beta$-equivalence $=\beta$, the equivalences $\equiv_{Rel}$ and $\equiv_{coh}$ respectively induced by the relational and coherent semantics and the observational equivalences $\sim_B$ and $\sim_B^w$. By well-known inclusions, we see that $=\beta \subseteq \equiv_{Rel} = \equiv_{coh}$ and $=\beta \subseteq \sim_B \subseteq \sim_B^w$. Theorem 4.1 and Proposition 7.1 complete our knowledge as follows:

$$=\beta = \equiv_{Rel} = \equiv_{coh} = \sim_B \subseteq \sim_B^w$$

Moreover, Theorem 3.3 (resp. Corollary 6.1) links the cut-free proof structures (resp. proof nets) with the complete sets (resp. complete cliques) of relational (resp. coherent) semantics.

We set our analysis in the multiplicative fragment of linear logic, where the proof nets syntax is simple and clear. Our aim is to extend such analysis to wider fragments of linear logic. In particular:

* **MALL.** In (Hughes and van Glabbeek, 2003) Hughes and Van Glabbeek introduce a proof nets syntax for the multiplicative additive linear logic fragment (MALL). Such a syntax has provided an abstract representation for MALL cut-free proofs modulo inessential rule commutation, for the first time since the beginning of linear logic in 1986. An open problem is to find semantical notions corresponding to such MALL cut-free proof nets, as the analogue of the complete cliques for MLL cut-free proof nets.

In (Blute et al., 2005) Blute, Hamano and Scott actually prove that hypercoherent semantics provides a semantical notion for the cut-free MALL proof nets introduced
by Girard in (Girard, 1996). Unfortunately, Girard's proof nets fail to be canonical with respect to MALL sequent calculus: an host of such cut-free proof nets can correspond to the same cut-free MALL sequent proof. Anyway hypercoherent semantics might allow a characterization for Hughes and Van Glabbeek's proof nets too.

*MELL*. All the above defined equivalences become very complex in the multiplicative exponential linear logic fragment (*MELL*). In (Tortora de Falco, 2003) Tortora de Falco shows several counter-examples to the coherent semantics injectivity concerning *MELL* proof nets.

From the observational point of view, in (David and Py, 2001) David and Py show a counter-example to the separability of $\lambda\mu$-calculus. From such counter-example one can define, using the translation described in (Laurent, 2003), a pair of cut-free proof nets of the polarized fragment of *MELL* which are observationally indistinguishable (see (Pagani, 2006)). Up to now, the *MELL* proof nets syntax has been unable to provide canonical representatives neither for the observational equivalence nor for the equivalence induced by coherent semantics. The injectivity of relational semantics concerning *MELL* proof nets is still an open problem.

## Acknowledgements

I would like to thank Lorenzo Tortora de Falco for his invaluable support during my work on this paper and the referee for his useful comments.

## References

Abramsky, S. and Jagadeesan, R. (1994). Games and full completeness for multiplicative linear logic. *Journal of Symbolic Logic*, 59(2):543–574.

Bellin, G. and de Wiele, J. V. (1995). Subnets of proof-nets in MLL. In Girard, J.-Y., Lafont, Y., and Regnier, L., editors, *Advances in Linear Logic*, volume 222 of *London Mathematical Society Lecture Note Series*. Cambridge University Press.

Blute, R., Hamano, M., and Scott, P. (2005). Softness of Hypercoherences and MALL Full completeness. *Annals of Pure and Applied Logic*, 131:1–63.

Böhm, C. (1968). Alcune proprietà delle forme $\beta\eta$-normali nel $\lambda$-K-calcolo. *Pubblicazioni dell'IAC*, 696:1–19.

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

David, R. and Py, W. (2001). $\lambda\mu$-calculus and Böhm's theorem. *Journal of Symbolic Logic*, 66(1):407–413.

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

Girard, J.-Y. (1991). A new constructive logic: classical logic. *Mathematical Structures in Computer Science*, 1(3):255–296.

Girard, J.-Y. (1996). Proof-nets: the parallel syntax for proof-theory. In Ursini and Agliano, editors, *Logic and Algebra*, New York. Marcel Dekker.

Girard, J.-Y. (2001). Locus solum: From the rules of logic to the logic of rules. *Mathematical Structures in Computer Science*, 11(3):301–506.
Hughes, D. and van Glabbeek, R. (2003). Proof nets for unit-free multiplicative-additive linear logic. In *Proceedings of the eighteenth annual symposium on Logic In Computer Science*, pages 1–10. IEEE, IEEE Computer Society Press.

Joly, T. (2000). *Codages, séparabilité et représentation de fonctions en λ-calcul simplement typé et dans d'autres systèmes de types*. Thèse de doctorat, Université Paris VII.

Laurent, O. (2003). Polarized proof-nets and λµ-calculus. *Theoretical Computer Science*, 290(1):161–188.

Mascari, G. and Pedicini, M. (1994). Head linear reduction and pure proof net extraction. *Theoretical Computer Science*, 135(1):111–137.

Matsuoka, S. (2005). Weak typed Böhm theorem on IMLL. Submitted for publication. Available at: http://arxiv.org/abs/cs.LO/0410030.

Morris, J. H. (1968). *λ-calculus models of programming languages*. Ph.D. thesis, MIT.

Pagani, M. (2006). *Proof nets and cliques: towards the understanding of analytical proofs*. Ph.D. thesis, Università Roma Tre and Université Aix-Marseille II.

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

Statman, R. (1983). Completeness, invariance and λ-definability. *Journal of Symbolic Logic*, pages 17–26.

Tan, A. (1997). *Full completeness for models of linear logic*. Ph.D. thesis, University of Oxford.

Tortora de Falco, L. (2000). *Réseaux, cohérence et expériences obsessionsnelles*. Thèse de doctorat, Université Paris VII. Available at: http://www.logique.jussieu.fr/www.tortora/index.html.

Tortora de Falco, L. (2003). Obsessional experiments for linear logic proof-nets. *Mathematical Structures in Computer Science*, 13:799–855.