Linear realisability on untyped nets

Adrien Ragot*

ragot@lipn.univ-paris13.fr

Université Sorbonne Paris Nord

France

Thomas Seiller†

thomas.seiller@cnrs.fr

CNRS

France

Lorenzo Tortora de Falco

Universitá Roma Tre

Italy

ABSTRACT

We present a new realisability model based on orthogonality for Linear Logic in the context of nets – untyped proof structures with generalized axiom. We show that it adequately models second order multiplicative linear logic.

As usual, not all realizers are representations of a proof, but we identify specific types (sets of nets closed under bi-orthogonality) that capture exactly the proofs of a given sequent thus proving a completeness theorem. Furthermore these types are orthogonal's of finite sets; this ensures the existence of a correctness criterion that runs in finite time.

CCS CONCEPTS

• *Theory of computation* → *Linear logic; Proof theory; Program semantics*.

KEYWORDS

Linear Logic, Realisability, Proof nets, Second order quantification

ACM Reference Format:

Adrien Ragot, Thomas Seiller, and Lorenzo Tortora de Falco. 2018. Linear realisability on untyped nets. In *Proceedings of Make sure to enter the correct conference title from your rights confirmation emai* (Conference acronym 'XX). ACM, New York, NY, USA, 30 pages. https://doi.org/XXXXXXX.XXXXXXX

# 1 INTRODUCTION

Realisability is a technique that extracts the computational content of proofs [12]. It was first introduced in 1945 by Kleene for Heyting Arithmetic – an Intuitionistic axiomatization of arithmetic – based on the codes of Gödel’s partial recursive functions [9]. Fixing an untyped computational model, the methodology of Realisability is based on two aspects:

* Types are given a computational status: the interpretation of a type<fnref n="1" /> A is a set of programs [[A]], which behave similarly – its elements are called realizers of A. The interpretation process however is not unique and is parametrized by an

interpretation basis $\mathcal{B}$, thus a same formula $A$ may be interpreted by different sets of programs $[[A]]_{\mathcal{B}}$ or $[[A]]_{\mathcal{B}'}$.

* A co-compiler, a simple process transforming the proofs of the realized proof system into programs is defined, introducing a non trivial predicate on programs, namely, some programs represent a proof, the correct programs, while others do not, the incorrect programs.

For instance, whenever the computational model is a freely-generated language equipped with a binary relation capturing program execution, correct programs are well-formed terms.

Two properties are of interest for an interpretation basis $\mathcal{B}$: Completeness stating for any formula $A$ any program in the type $[[A]]_{\mathcal{B}}$ is a proof of $A$. Hence completeness provides a procedure to assert whether a program is correct or not. Adequacy which ensure that the co-compiler process and the interpretations are coherent, stating that each proof of $A$ is a realizer of $A$. Whenever both properties hold this means that the elements of the interpretation of a formula $A$ are exactly its corresponding correct programs; the programs which are correctly typeable by $A$.

For most interpretations completeness does not hold; not all realizers are correct programs thus not all realizers represent a proof. In fact, it was revealed by realisability models based on orthogonality that the presence of incorrect programs is crucial to give a computational status to correctness.

This can be traced back to the introduction of classical realizability by Jean Louis Krivine [10] aiming at extending realisability techniques from intuistionnistic to classical logic, proposing a model based on orthogonality. Krivine’s construction is based on an extension of the untyped lambda calculus, but, in order to capture a given context (stack) to potentially restore it later, the syntax is not only extended with the call/cc operator but also with a countably infinite set of stack constants. In that context the correct programs are those who do not contain stack constants. The orthogonality relation is understood as a notion of test: a program (here a $\lambda$-term) follows a specification if it passes (e.g. is orthogonal to) the adequate tests (here they are stacks). This is how orthogonality is used to define the interpretation of types (as the set of terms passing a given set of tests). From the point of view of orthogonality, the presence of "incorrect" terms is essential, as it introduces in the syntax semantic information [13] that can be used to test correct (and incorrect) terms.

In parallel with the work of Krivine, similar realisability constructions have been introduced by Jean-Yves Girard in order to interpret Linear Logic. While the orthogonality construction was clearly put forth in Ludics [7], the ideas and first occurrences can be traced back to the first model of geometry of interaction (GOI) [4], which is restricted to multiplicative linear logic, and interprets proofs as permutations. Furthermore, in a series of recent papers

<footnote>*The author is supported by a VINCI PhD fellowship from the Franco-Italian Université.</footnote>

<footnote>†The author is partially supported by the ANR-22-CE48-0003-01 project DySCo.</footnote>

<footnote n="1">¹Equivalently, having the Curry-Howard correspondence in mind, A is a formula.</footnote>

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.</footnote>

<footnote>Conference acronym 'XX, June 03–05, 2018, Woodstock, NY</footnote>

<footnote>© 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM.</footnote>

<footnote>ACM ISBN 978-1-4503-XXXX-X/18/06</footnote>

<footnote>https://doi.org/XXXXXXX.XXXXXXX</footnote>

<footnote>59</footnote>

<footnote>60</footnote>

<footnote>61</footnote>

<footnote>62</footnote>

<footnote>63</footnote>

<footnote>64</footnote>

<footnote>65</footnote>

<footnote>66</footnote>

<footnote>67</footnote>

<footnote>68</footnote>

<footnote>69</footnote>

<footnote>70</footnote>

<footnote>71</footnote>

<footnote>72</footnote>

<footnote>73</footnote>

<footnote>74</footnote>

<footnote>75</footnote>

<footnote>76</footnote>

<footnote>77</footnote>

<footnote>78</footnote>

<footnote>79</footnote>

<footnote>80</footnote>

<footnote>81</footnote>

<footnote>82</footnote>

<footnote>83</footnote>

<footnote>84</footnote>

<footnote>85</footnote>

<footnote>86</footnote>

<footnote>87</footnote>

<footnote>88</footnote>

<footnote>89</footnote>

<footnote>90</footnote>

<footnote>91</footnote>

<footnote>92</footnote>

<footnote>93</footnote>

<footnote>94</footnote>

<footnote>95</footnote>

<footnote>96</footnote>

<footnote>97</footnote>

<footnote>98</footnote>

<footnote>99</footnote>

<footnote>100</footnote>

<footnote>101</footnote>

<footnote>102</footnote>

<footnote>103</footnote>

<footnote>104</footnote>

<footnote>105</footnote>

<footnote>106</footnote>

<footnote>107</footnote>

<footnote>108</footnote>

<footnote>109</footnote>

<footnote>110</footnote>

<footnote>111</footnote>

<footnote>112</footnote>

<footnote>113</footnote>

<footnote>114</footnote>

<footnote>115</footnote>

<footnote>116</footnote>
[15–19], Thomas Seiller proposed a combinatorial approach to the Geometry of Interaction, *interaction graphs*, which specialises to all the previous ‘geometries’ of interaction proposed by Girard, and constructs the types of Linear Logic via a realisability method involving orthogonality within the computational model of interaction graphs. However, proofs are interpreted in these models as abstract objects (generalisations of dynamical systems) and remain far from the general intuition of what a proof is, this makes the co-compiler hard to reverse and so completeness results are lacking.

The goal of our work is to explore the question of completeness for realisability models of linear logic (LL). To do so, we work in the context of nets – essentially the proof structures introduced by Girard [5]. Since their introduction, proof structures have been known to represent proofs of LL (meaning a co-compiler is known), and several *correctness criteria*, e.g. procedures to assert whether a proof structure represents a proof, have been provided. The missing piece to perform realisability in this context is a way to interpret formulas as types; this will be based on orthogonality relying on the computational rules on proof structures, rewriting rules generalizing cut-elimination on proof trees. Furthermore this work will relate correctness criteria with completeness results, for instance in this paper the Danos Regnier criterion [3] applied to a would-be proof $\pi$ yields a set of “tests” whose interaction with $\pi$ by cut elimination will allow to determine whether or not $\pi$ is indeed a proof.

It will be necessary to consider generalized axiom (daimon) rules; the correctness of a multiplicative net with binary daimons (which can be identified with axioms) can be tested by the Danos Regnier criterion, this criterion can be performed via orthogonality with some nets that we'll call *tests* however these nets may have non binary daimons making it necessary to work in the $\mathbb{MLL}^{\mathbb{X}}$ fragment (Figure 3). See for instance below the net in figure 1a represents a proof in $\mathbb{MLL}$ while its two tests – the nets in figure 1b and 1c – represent proofs of $\mathbb{MLL}^{\mathbb{X}}$. The orthogonality will consists of making the two nets interact by placing a cut between their output, if the resulting reduces to a net made of a single daimon link with no output the nets are orthogonal (essentially this means that no cycles or disconnections have appeared during cut elimination defined in definition 2.132.15). In particular in the figure 1 the orthogonality between the net and its tests will involve only cuts of the form $(\mathbb{X}/\mathbb{X})$ or $(\otimes/\mathfrak{X})$ – later on defined as homogeneous cuts (definition 2.13). A folklore result which we prove in theo-

<figure><img src="image_1.png" /><figcaption>(a) An MLL proof-net. (b) First test for 1a. (c) Second test for 1a. Figure 1: Daimons are needed to construct tests for MLL nets.</figcaption></figure>

rem 5.7 ensures that any multiplicative test represents proofs of $\mathbb{MLL}^{\mathbb{X}}$. However, to construct the interpretation of multiplicative second-order formulas the use of the incorrect terms is necessary. Realisability naturally provides interpretations for the universal (resp. existential) second order quantifiers as an intersection (resp. union) on the set of all types. For instance we want a binary daimon to behave like an axiom, it can introduce any pair of dual formulas

$A, A^{\perp}$. Recall that our objects are however untyped therefore this means that the binary daimon should belong to any interpretation $[[A, A^{\perp}]_B$, that is to be orthogonal to any pair of orthogonal nets. In particular orthogonality should hold with incorrect nets and this is necessary to obtain an adequate interpretation of MLL since the daimon behave well with any correct net. In the figure 2 below the binary daimon interacts with a net containing a cycle and a net containing a disconnection – these error will cancel each other making the orthogonality relation hold.

<figure><img src="image_2.png" /><figcaption>Figure 2: Nets and second order quantification.</figcaption></figure>

The presence of incorrect nets enables adequacy for nets with second order quantifiers ($\mathbb{MLL}_2$) – with a dummy version of cut elimination. For instance the net in figure 2b realizes the formula $\forall X(X, X^{\perp})$ but it does not realise the formula $(\forall XX), X^{\perp}$.

Importantly we will identify interpretations basis $\mathcal{B}$ such that for any formula $[[A]]_B$ is the orthogonal of a finite set. This ensures that asserting if a net realizes $A$ or not is decidable in finite time. Furthermore these basis can be complete and adequate and so this provides a way to test correctness in finite time, in other words a correctness criterion. This will be true for the realisability model of $\mathbb{MLL}_2$ hinting towards a correctness criterion for that fragment (this is what we explore in the last section). To handle second order in an untyped setting we define nets with pointers and and define a contractibility criterion (Danos [2]) which generalizes the formulation provided by curien in [1] for multiplicatives. This new criterion somehow breaks down correctness for second order nets into three independent pieces (1) the existential witness in the net must be coherent (2) the net must be multiplicatively e.g. pass the tests of Danos Regnier (3) the net must be sequentializable in the sense of a contractibility reduction which read backward provides the reconstruction of a proof.

Specifically the first (1) step is required in an untyped setting: an existential quantifier isn't allowed to abstract two distinct formulas. This is illustrated in figure 2c where two universal quantifiers are binding distinct formulas X and Y and the existential quantifier abstracts both X and Y and creates a conclusion which would be typed by $\exists Z.Z \otimes Z$, we forbid this kind of scenario as we want an existential to substitute exactly one formula with a propositional variable, hence the conclusion of the existential quantifier should correspond to a formula $\exists Z.Z \otimes Y$ or $\exists Z.X \otimes Z$ (resulting in an incorrect net).

*Ouline of the paper.* In Section 2, we recall the general notion of hypergraph and we adapt it to our framework: a multiplicative net is a (particular) ordered hypergraph that can be understood as an untyped version of the notion of proof-structure ([5]). Indeed, it is possible to perform cut elimination on these nets, and the main novelty here is the presence of daimon links (denoted by $\mathbf{X}$ and already present in the literarture, see for example [7]) yielding the non homogeneous cut elimination steps $(\otimes/\mathbf{X})$ and $(\mathfrak{X}/\mathbf{X})$, this
last step being non deterministic (see remark 11). The intuition is that a $\mathbf{\star}$-link with $n$ conclusions represents an agent whose logical correctness is not guaranteed, but which is capable to interact correctly with $n$ other agents.

Section 3 introduces our realisability model, based on the interaction between nets (definition 3.1) and the consequent notion of orthogonality: two nets are orthogonal when their interaction yields a $\mathbf{\star}$-link without conclusions (definition 3.4). One can thus define the orthogonal of a set of nets and the crucial notion of type, a set of net equals to its bi-orthogonal (definition 3.5). The set of types is stable with respect to constructions allowing to interpret MLL formulas in the very spirit of realisability: a formula is interpreted as a set of nets with a similar behaviour (belonging to the same type interpreting the formula).

Adequacy for MLL and MLL$^{\mathbf{\star}}$ follows in Section 4: a net coming from a proof of a formula $A$ in MLL or MLL$^{\mathbf{\star}}$ always belongs to the interpretation of $A$ (theorem 4.3).

Let us say some words on our path to completeness of MLL$^{\mathbf{\star}}$ and MLL proven in Section 5. We are naturally led to introduce the notion of test (definition 5.6) and to prove that a test of a formula $A$ is a proof of $A^{\perp}$ (theorem 5.7) which allows to characterize proofs as those nets with a good interaction with their tests (theorem 5.8), in a Danos-Regnier style. This last result and adequacy yield completeness for MLL$^{\mathbf{\star}}$ (theorem 5.10). The MLL case (theorem 5.13) follows once the intuition that the conclusion of an MLL axiom is any pair of dual formulas is taken in consideration: the proof relies on the definition of the intersection and the union type (definition 5.11).

With Section 6 we smoothly move to the second order case: we introduce a first version of the quantifier links, that are here only unary links with no pointers. Cut elimination immediately extends to these new nets. We can thus define the interpretation of second order formulas as types (definition 6.1) and prove adequacy for this first version of second order nets (teorem 6.2): a proof of a formula $A$ in MLL$_2$ always belongs to the interpretation of $A$.

In Section 7 we introduce the notion of computable type (definition 7.1): the fundamental point is that one can check in finite time whether or not a given net belongs to such a type. We then notice that computability is preserved by the previously defined constructions on types (propositions 7.2 and 7.3), so that one can interpret MLL$_2$ formulas with computable types. This paves the way to the possibility of defining a new correctness criterion for MLL$_2$ (remark 28).

In Section 8 we present a new correctness criterion for untyped second order multiplicative linear logic, more precisely for MLL$_2^{\mathbf{\star}}$. To handle quantifiers (remaining untyped!) we add pointers to hypergraphs. There are pointers both for existential and universal quantifiers but with a different intended meaning: universal pointers indicate that the pointed location contains a formula which uses the quantified variable while the target of existential pointers are necessarily above the corresponding existential link and indicate positions of existential witnesses. The notion of pointed tree (definition 8.1) guarantees the uniformity of existential witnesses, a particularly delicate point in the absence of types: any two targets of the same existential link need to be coherent (definition 8.6). We then define a list of contraction rules (definition 8.7) allowing to characterize MLL$_2^{\mathbf{\star}}$-proofs (theorem 8.9).

# 2 UNTYPED NETS

## 2.1 Directed hypergraph

Throughout this document we fix a set Pos of elements called positions. Given a set $X$ we will let $\mathcal{P}_{\leq}(X)$ denote the set of totally ordered finite subsets of $X$.

**Definition 2.1.** Suppose given a set $L$ of labels. A directed (L-labelled) hypergraph is a tuple $(V, E, s, t, \ell)$ where $V$ is a set of positions, and $E$ is a set of elements called links, $s: E \to \mathcal{P}_{\leq}(V)$ is the source map, $t: E \to \mathcal{P}_{\leq}(V)$ is the target map, and $\ell: E \to L$ is the labelling map.

Given a link $e \in E$, since the finite sets $t(e)$ and $s(e)$ are ordered we will represent them as sequences: they are respectively called the target and the source sets of $e$. A source of $e$ is an element of its source set $s(e)$, a target of $e$ is an element of its target set. The set of targets and sources of $e$ is the domain of the link $e$. We will use superscripts to denote sequences of positions $(\bar{p}, \bar{q}, \bar{u}, \dots)$. A link is a loop when its target set and source set are not disjoint.

**Remark 1.** Along this work we assume all the hypergraphs to be loop-free e.g. containing only links which are not loops.

Given an hypergraph $\mathcal{H}$ having $E$ as set of links, we denote $s(\mathcal{H})$ (resp. $t(\mathcal{H})$) the set of all positions which are source (resp. target) of at least one link:

$$s(\mathcal{H}) = \bigcup_{e \in E} s(e), \quad t(\mathcal{H}) = \bigcup_{e \in E} t(e).$$

A conclusion/output (resp. a premise/input) of a directed hypergraph $\mathcal{H}$ is a position which is the source of no link in $\mathcal{H}$, e.g. an element of $V \setminus s(\mathcal{H})$ (resp. in $V \setminus t(\mathcal{H})$). The set of conclusions (resp. premises) of an hypergraph $\mathcal{H}$ is denoted out($\mathcal{H}$) (resp. in($\mathcal{H}$)).

The size of a directed hypergraph is the number of its link. An hypergraph is finite when it contains a finite number of links and positions.

A position $p$ is isolated in an hypergraph $\mathcal{H}$ if $p$ is both an output and an input of $\mathcal{H}$, e.g. it belongs to no link as an input nor as an output.

**Notation 1.** A link $e$ will be written as $\langle u \succ_I v \rangle$ where $s(e) = u$, $t(e) = v$, and $\ell(e) = l$. With this notation, a directed labelled hypergraph with no isolated position can always be written as a formal sum

$$\sum_{e \in E} \langle s(e) \succ_I \ell(e) \rangle t(e).$$

**Notation 2.** We write $u \cdot v$ the concatenation of sequences.

Given $u = (u_1, \dots, u_n)$ a sequence of element in a set $X$ and an integer $i \in \{1, \dots, n\}$, we denote by $u_{<i}$ (resp. $u_{>i}$) the sequence $(u_1, \dots, u_{i-1})$ (resp. $(u_{i+1}, \dots, u_n)$).

Moreover, given two potentially empty sequences $u$ and $v$ we denote by $u[i \leftarrow v]$ the sequence $u_{<i} \cdot v \cdot u_{>i}$. We can generalize this notation as follow

$$u[i_1 \leftarrow v_1, \dots, i_n \leftarrow v_n] = (\dots (u[i_1 \leftarrow v_1]) \dots) [i_n \leftarrow v_n].$$

**Definition 2.2 (Initial and final links).** A link is initial (resp. final) when it has no input (resp. no output). A position is initial (resp. final) when it belongs to the domain of an initial (resp. final) link.
$$A, B := X, X^{\perp} | A \otimes B | A \otimes B | \forall XA | \exists XA. \quad \overline{A, A^{\perp}}^{\text{ax}} \xrightarrow{\Gamma} \mathcal{H} \quad \overline{\Gamma, A, A^{\perp}}^{\text{cut}} \xrightarrow{\Gamma, A, A^{\perp}} \overline{\Gamma, \Delta, A^{\perp}}^{\text{cut}} \xrightarrow{\Gamma, A, B} \overline{\Gamma, A, B} \xrightarrow{\Gamma, A, B, \Delta} \overline{\Gamma, B, A, \Delta}^{\text{ex}} \xrightarrow{\Gamma, A} \overline{\Gamma, \exists XA} \exists \quad \overline{\Gamma, A}^{\forall XA} \forall$$

<caption>Figure 3: The rules (⊗, ⊗, ≀≀, cut, ex) define the MLL<sup>⊗</sup> proof system. Adding to MLL<sup>⊗</sup> the quantifier rules (∀, ∃) constitutes MLL<sub>2</sub><sup>⊗</sup>. Substituting the daimon rule (⊗) with the axiom rule (ax) in MLL<sup>⊗</sup> (resp. MLL<sub>2</sub><sup>⊗</sup>) results in MLL (resp. MLL<sub>2</sub>).</caption>

**Example 2.3.** For instance a link $\langle \triangleright a, b, c \rangle$ is an initial link. And in the hypergraph $\langle \triangleright a, b, c \rangle + \langle a \triangleright d \rangle + \langle \triangleright e \rangle + \langle e \triangleright \rangle$ the set of initial positions are $\{a, b, c, e\}$, while $e$ is the only final position belonging to the final link $\langle e \triangleright \rangle$.

A link is terminal when its outputs are conclusions – thus a final link is a terminal link.

## 2.2 Sum of hypergraphs

Hypergraphs enjoy a natural notion of sum based on the disjoint union of the set of links.

**Notation 3.** Given a function $f: X \to E$ and $X_0 \subseteq X$ we denote the restriction of $f$ to $X_0$ by $f|_{X_0}$ or simply $f|_{X_0}$.

Given two disjoint sets $X_0$ and $X_1$ and two functions $f: X_0 \to E$ and $g: X_1 \to E$ we denote $f \uplus g$ the function which takes an element $x$ of $X_0 \uplus X_1$ and returns $f(x)$ if $x \in X_0$ or $g(x)$ if $x \in X_1$.

**Definition 2.4.** Given two hypergraphs $\mathcal{H}_1 = (V_1, E_1, t_1, s_1)$ and $\mathcal{H}_2 = (V_2, E_2, t_2, s_2)$. The sum of $\mathcal{H}_1$ and $\mathcal{H}_2$ is defined as:

$$\mathcal{H}_1 + \mathcal{H}_2 = (V_1 \cup V_2, E_1 \uplus E_2, t_1 \uplus t_2, s_1 \uplus s_2).$$

**Remark 2.** Whenever $\mathcal{H}_1 = (V_1, E_1, t_1, s_1)$ and $\mathcal{H}_2 = (V_2, E_2, t_2, s_2)$ are such that $E_1 \cap E_2 \neq \emptyset$, we will abusively write their sum as $\mathcal{H}_1 + \mathcal{H}_2 = (V_1 \cup V_2, E_1 \uplus E_2, t_1 \uplus t_2, s_1 \uplus s_2)$, using implicitly the isomorphism between $E_1 \uplus E_2$ and $E_1 \cup E_2$ which exists in this case, since up to renaming the set of links of two hypergraphs can always be considered to be disjoint.

**Remark 3.** Vertices may overlap in a sum (as we take the union of vertex sets rather than the disjoint union). As a consequence, a position may be input (or output) of several distinct links.

As mentioned above, we can therefore describe hypergraphs as sums of simple hypergraphs; namely those that contain only one link. Indeed, an hypergraph consisting of two links $\langle a_1, \dots, a_i \triangleright \ell b_1, \dots, b_j \rangle$ and $\langle a'_1, \dots, a'_i \triangleright \ell' b'_1, \dots, b'_j \rangle$ is in fact equal to the sum of the single-link hypergraphs $\langle a_1, \dots, a_i \triangleright \ell b_1, \dots, b_j \rangle$ and $\langle a'_1, \dots, a'_i \triangleright \ell' b'_1, \dots, b'_j \rangle$. By induction on the number of links, this formally shows that $\mathcal{H} = \sum_{e \in E} \langle s(e) \triangleright_{\ell(e)} t(e) \rangle$ when considering an hypergraphs with no isolated positions.

**Remark 4.** The sum of hypergraphs enjoys the properties of an abelian monoid; associativity, commutativity, and a neutral element which is the empty hypergraph.

We will also use extensively the notion of parallel composition or parallel sum of hypergraphs, an analogue of the union-graph of two simple graphs.

**Definition 2.5 (Parallel sum).** Given $\mathcal{H}_1 = (V_1, E_1, t_1, s_1)$ and $\mathcal{H}_2 = (V_2, E_2, t_2, s_2)$ two hypergraphs we define their parallel sum as: $\mathcal{H}_1 \parallel \mathcal{H}_2 = (V_1 \uplus V_2, E_1 \uplus E_2, t_1 \uplus t_2, s_1 \uplus s_2)$.

**Remark 5.** The parallel sum of two hypergraphs $\mathcal{H}_1$ and $\mathcal{H}_2$ corresponds to a regular sum whenever the sets of vertices are disjoint. Just like the sum, parallel composition can always be performed between two hypergraphs up to renaming their vertex sets.

## 2.3 Ordered Hypergraphs

An arrangement of a directed hypergraph $\mathcal{H}$ is a total order $<_{\text{a}}$ on its set of conclusions, equivalently, the order may be identified as a bijection $a: \{1, \dots, \text{card}(\text{out}(\mathcal{H}))\} \to \text{out}(\mathcal{H})$.

**Definition 2.6 (Ordered hypergraph).** An ordered hypergraph is a pair $(\mathcal{H}, a)$ of an hypergraph together with an arrangement. The arrangement $a$ is denoted $a(\mathcal{H})$.

**Notation 4.** Given a finite and ordered hypergraph $(\mathcal{H}, a)$ with $n$ conclusions for an integer $1 \le i \le n$, we denote $a(i)$ by $\mathcal{H}(i)$ whenever there is no ambiguity.

**Notation 5.** A segment of $\mathbb{N}$ is denoted $[n; n + k]$ and corresponds to set of integers $i$ such that $n \le i \le n + k$. For any integer $k$ we denote $\text{tr}_k : \mathbb{N} \to \mathbb{N}, n \mapsto n + k$.

Given a partial function $f: \mathbb{N} \to E$ with a finite domain of cardinality $n$ and ordered as $i_1 < i_2 < \dots < i_n$, we denote $f \parallel$ the total function of type $[1; n] \to E$ such that $f(m) = f(i_m)$ for any integer $1 \le m \le n$.

In particular given a restricted function $f|_{X_0}$ we denote $f|_{X_0} \parallel$ by $f \parallel_{X_0}$. Furthermore, we denote $f \parallel_{X_0}^c$ by $f \parallel_{X_0}$ meaning the function $f$ to which we have removed the element of $X_0$ from its domain and rearrange the domain of $f$ to be a segment of $\mathbb{N}$.

Given $f: [1; n] \to E$ and $g: [1; m] \to E$ two functions defined on segments and with a common domain, we denote by $f \sqcup g$ their sum with translation, namely the disjoint functional sum of $f \uplus g \circ \text{tr}_{-n} \uplus [n+1; n+m])$. The sum with translation is not a commutative operation.

**Definition 2.7.** Two hypergraphs $\mathcal{H}_1$ and $\mathcal{H}_2$ are summable whenever their target sets and source sets are disjoint, e.g.

$$t(\mathcal{H}_1) \cap t(\mathcal{H}_2) = \emptyset \quad \text{and} \quad s(\mathcal{H}_1) \cap s(\mathcal{H}_2) = \emptyset$$

**Remark 6.** A position $p$ can occur in two summable hypergraphs only if $p$ is a target in $\mathcal{H}_1$ and a source in $\mathcal{H}_2$ – or the converse – or whenever $p$ is isolated in (at least) one of the two hypergraphs.

Since the conclusions of an hypergraphs with no isolated points are targets, summable hypergraphs have arrangements $a_1$ and $a_2$ with disjoint codomains. As a consequence, their disjoint sum function $a_1 \sqcup a_2$ remains a bijection.

**Definition 2.8 (Arrangement of the sum of ordered hypergraphs).** Given two summable ordered hypergraphs $\mathcal{H}_1$ and $\mathcal{H}_2$. The arrangement $a(\mathcal{H}_1 + \mathcal{H}_2)$ of there sum is;

$$a(\mathcal{H}_1 + \mathcal{H}_2) = a(\mathcal{H}_1) \parallel s(\mathcal{H}_2) \sqcup a(\mathcal{H}_2) \parallel s(\mathcal{H}_1)$$

**Remark 7.** Given two summable hypergraphs since $s(\mathcal{H}_1)$ and $s(\mathcal{H}_2)$ are disjoint the arrangement $a(\mathcal{H}_1 + \mathcal{H}_2)$ is equal to

$$a(\mathcal{H}_1) \sqcup a(\mathcal{H}_2) \parallel s(\mathcal{H}_1) \cup s(\mathcal{H}_2).$$

**Remark 8.** The ordered sum of ordered hypergraphs $\mathcal{H}_1$ and $\mathcal{H}_2$ given as $(\mathcal{H}_1 + \mathcal{H}_2, a(\mathcal{H}_1) + a(\mathcal{H}_2))$ is – unlike the standard sum of hypergraphs – not commutative.

However an hypergraph with no conclusions commutes with any other ordered hypergraph under the ordered sum. Furthermore
internal sub-hypergraphs commute for the ordered sum, an hyper-
graph $\mathcal{H}_0 \subset \mathcal{H}_1 + \mathcal{H}_2$ included in a sum and such that none of the
conclusion of $\mathcal{H}_0$ is a conclusion of $\mathcal{H}_1 + \mathcal{H}_2$ commutes with any
link in the sum $\mathcal{H}_1 + \mathcal{H}_2$. More precisely, in an hypergraph $\mathcal{H}$ given
as a sum $\sum_{e \in E} \langle se \triangleright_t te \rangle$, each link $e$ commutes with any link of $E$
if $e$ is not terminal or $e$ has no conclusion.

**2.4 Properties of hypergraphs**

**Definition 2.9.** We say a hypergraph $\mathcal{H} = (V, E, t, s)$ is:

• surjective whenever $t(\mathcal{H}) = V$.

• source-disjoint if the sets $s(e)$ for $e \in E$ are pairwise disjoint.

• target-disjoint if the sets $t(e)$ for $e \in E$ are pairwise disjoint.

If $\mathcal{H}$ is both surjective and target-disjoint, we will say it is full. In this case, the sets $t(e)$ for $e \in E$ define a partition of $V$.

Up to this point we have allowed any kind of link to occur in an
hypergraph. We now restrict the discussion to untyped multiplica-
tive nets in which only considered specific sets of links:

• *Generalized axioms*: links of the form $e = \langle \triangleright p_1, p_2, \dots, p_n \rangle$;

• *Cuts*: links of the form $e = \langle p_1, p_2 \triangleright \rangle$.

• *Connectives*: links of the form $e = \langle p_1, p_2, \dots, p_n \triangleright a \rangle$.

In particular, we will restrict in the next section to binary con-
nectives only, with the additional restriction that those binary con-
nectives should be labelled either by $\otimes$ or $\mathcal{Y}$. As a consequence,
the hypergraphs considered will closely resemble multiplicative
linear logic proof nets, with two important points of divergence:
the absence of typing, and the presence of generalised axioms.

Note that these restrictions leave a number of questions open
for future investigations. For instance, one can wonder how a gen-
eralized cut of the form $\langle a, b, c \triangleright \rangle$ would behave.

**2.5 Multiplicative nets**

We now fix the set of labels as the set made of the *daimon* (Ξ) the tensor (⊗) the parr (⊠) and the (cut) symbol.

**Definition 2.10.** A *multiplicative module* is an ordered hypergraph (*H*, *a*) where *H* is source-disjoint and target-disjoint, and such that Ξ-labelled links have no inputs, cut-labelled links have exactly two inputs and no outputs, ⊗- and Σ-labelled links have exactly two inputs and one output.

In other words, $\mathcal{H}$ is a sum of links of the form:

$$
\langle \triangleright_{\mathbf{X}} p_1, \dots, p_n \rangle, \langle p_1, p_2 \triangleright p \rangle, \langle p_1, p_2 \triangleright_{\mathcal{Y}} p \rangle, \langle p_1, p_2 \triangleright_{\text{cut}} \rangle.
$$

Whenever there is no ambiguity we might relax the notation:
$\langle \triangleright p_1, \dots, p_n \rangle$ will denote $\langle \triangleright_{\mathbf{X}} p_1, \dots, p_n \rangle$, and $\langle p_1, p_2 \triangleright \rangle$ will denote $\langle p_1, p_2 \triangleright_{\text{cut}} \rangle$.

Definition 2.11. A *multiplicative net* is a surjective multiplicative module.

**Notation 6.** We will denote Mod the set of multiplicative modules and Net the set of multiplicative nets.

**Notation 7.** Given an integer $n$ we denote by $\mathbf{\Sigma}_n$ any multiplicative net consisting of a single daimon link with $n$ outputs, e.g. isomorphic$^2$ to $\langle \triangleright_{\mathbf{X}} p_1, \dots, p_n \rangle$.

**2.6 Homogeneous cut elimination**

The set of untyped nets we have defined comes with its very own
notion of computation, which corresponds to some graph rewriting.
The computation is called the *cut elimination* and to describe it
roughly consists in removing the cut links. How to remove a cut
link will depend on what this link is attached to, this defines the
type of the cut, we give it a clear definition in the following.

**Definition 2.12 (Types of cut).** Given a multiplicative net $S$ the type of cut link $c = \langle p, q \triangleright \rangle$ occuring in $S$ is the pair of labels of the links of output $p$ and $q$. Thus there are 6 types of cuts (up to symmetry). More precisely, we distinguish:

• *multiplicative cuts*, of type $(\otimes/\mathcal{Y})$;

• *clash* cuts, of type $(\otimes/\otimes)$ or $(\mathcal{Y}/\mathcal{Y})$;

• *glueing* cuts, of type $(\mathbf{\Sigma}/\mathbf{\Sigma})$;

• non-homogeneous cuts, of type $(\otimes/\mathbf{\Sigma})$ or $(\mathcal{Y}/\mathbf{\Sigma})$, they are respectively called *reversible* and *irreversible* cuts.

**Remark 9.** A cut to which we can assign a type forms a *redex*, whenever a redex occurs in an hypergraph $\mathcal{H}$ the links which define the redex commute with any link contained in $\mathcal{H}$ under the ordered sum – as in remark 8– this allows us to define cut-elimination as a local rewriting of redexes.

**Definition 2.13 (homogeneous cut elimination).** The relation of homogeneous cut elimination on multiplicative nets is the rewriting relation defined as the contextual closure of the following:

$$
\langle \triangleright_{\mathbf{X}} \bar{p} \rangle + \langle \triangleright_{\mathbf{X}} \bar{q} \rangle + \langle p_i, q_j \triangleright \rangle \rightarrow \langle \triangleright_{\mathbf{X}} \bar{p} [i \leftarrow \epsilon] \cdot \bar{q} [j \leftarrow \epsilon] \rangle \\
\langle p_1, p_2 \triangleright p \rangle + \langle q_1, q_2 \triangleright \mathcal{Y} q \rangle + \langle p, q \triangleright \rangle \rightarrow \langle p_1, q_1 \triangleright \rangle + \langle p_2, q_2 \triangleright \rangle
$$

**Remark 10.** The commutation of a cut link $\langle p, q \triangleright_{\text{cut}} \rangle$ is the link $\langle q, p \triangleright_{\text{cut}} \rangle$. The input of a cut link $\langle p, q \triangleright_{\text{cut}} \rangle$ are ordered, however this plays no role during cut elimination, the redex of a cut link $\langle p, q \triangleright_{\text{cut}} \rangle$ or $\langle q, p \triangleright_{\text{cut}} \rangle$ are the same upto the commutation of cutlinks.

The following result is easily established, in particular using that
the number of links strictly decreases during homogeneous cut
elimination.

**PROPOSITION 2.14.** *Homogeneous cut elimination is confluent and strongly normalizing.*

**2.7 Non homogeneous cut elimination**

**Definition 2.15 (Non-homogeneous cut elimination).** The non homogeneous reduction is denoted $\rightarrow_{nh}$, and defined as the extension of the homogeneous cut-elimination with the following rules:

• A redex $\langle \triangleright_{\mathbf{X}} \bar{p} \rangle + \langle p_i, q \triangleright_{\text{cut}} \rangle + \langle q_1, q_2 \triangleright_{\mathcal{Y}} q \rangle$ reduces to $\langle \triangleright_{\mathbf{X}} \bar{u}, r_1 \rangle + \langle \triangleright_{\mathbf{X}} \bar{v}, r_2 \rangle + \langle r_1, q_1 \triangleright_{\text{cut}} \rangle + \langle r_2, q_2 \triangleright_{\text{cut}} \rangle$, where $\bar{u}, \bar{v}$ are such that $\bar{u} \cdot \bar{v}$ is a reordering of $\bar{p}[i \leftarrow \epsilon]$, and $r_1, r_2$ are fresh positions.

• A redex $\langle \triangleright_{\mathbf{X}} \bar{p} \rangle + \langle p_i, q \triangleright_{\text{cut}} \rangle + \langle p_1, p_2 \triangleright \bar{p} \rangle$ reduces to $\langle \triangleright_{\mathbf{X}} \bar{u} \rangle + \langle r_1, q_1 \triangleright_{\text{cut}} \rangle + \langle r_2, q \triangleright_{\text{cut}} \rangle$, where $r_1, r_2$ are fresh positions and $u = \bar{p}_{<i} \cdot r_1 \cdot r_2 \cdot \bar{p}_{>i}$.

**Remark 11.** From the interactive viewpoint daimon links behave like proof nets ([5]) and they are able to interact with any net. As a consequence, the non homogeneous cut-eliminations simulates proof search in the sequent calculus.

<footnote n="2">²The notion of isomorphism between hypergraphs is recalled in the appendix, see definition B.1.</footnote>
<figure><img src="image_3.png" /><figcaption>**Figure 4: Rules for the homogeneous cut elimination and non homogeneous cut-elimination.**
The non-homogeneous cut elimination of a daimon against a $\mathfrak{A}$-link is non deterministic, $\{q_1^1, \dots, q_{n_1}^1\}$, $\{q_1^2, \dots, q_{n_2}^2\}$ is a partition of $\{q_1, \dots, q_n\}$.
On the left hand side of each reduction rule one can find the different types of cuts of definition 2.12.</figcaption></figure>

$$ \overline{\Gamma, A^{\perp} \otimes B^{\perp}}^{\star} \rightarrow \frac{\overline{\Delta_1, A^{\perp}}^{\star} \overline{\Delta_2, B^{\perp}}^{\star}}{\Gamma, A^{\perp} \otimes B^{\perp}} \otimes \overline{\Gamma, A^{\perp} \overline{\gamma} B^{\perp}}^{\star} \rightarrow \frac{\overline{\Gamma, A^{\perp} \overline{\gamma} B^{\perp}}^{\star}}{\Gamma, A^{\perp} \overline{\gamma} B^{\perp}} \overline{\gamma} $$

This is where the non determinism comes from, in particular the rule eliminating the $(\star/\mathfrak{A})$ cuts corresponds to proof search on a formula of the form $A \otimes B$, going from bottom to top the $\otimes$-introduction rules splits the context $\Gamma$, which isn't a deterministic process. Simultaneously, some of the different possible reductions will, play the role of the switchings used in correctness criteria [3]. These intuitions will be important in understanding further results.

A consequence of non determinism is the loss of confluence for cut-elimination; since splitting the context is irreversible, see for instance the reduction of the net in figure 2.

# 3 REALISABILITY MODEL

## 3.1 Interaction of nets

**Definition 3.1 (Interaction between nets).** The interface of two nets $S$ and $R$ is an injective and functional relation on $\text{out}(S) \times \text{out}(R)$. An interface is total whenever it is defined for all conclusions of $S$.

An interface between two nets $(S, p_1 < \dots < p_n)$ and $(R, q_1 < \dots < q_m)$ is regular whenever it contains only pair of the form $(p_i, q_i)$. The identity interface is the relation, denoted $\text{id}_n$, defined when $n = m$ by $\text{id}_n = \{(p_i, q_i) | 1 \le i \le n\}$. The projective interface of size $k \le n$ is the regular interface between $S$ and $R$ that is defined exactly for the elements of $\{p_1, \dots, p_k\}$ we denote it $\text{pr}_k$.

The interaction of the nets $S$ and $T$ along the interface $\sigma$, is denoted $S ::_{\sigma} T$ and corresponds to

$$ S ::_{\sigma} T \triangleq S + T + \sum_{(p,q) \in \sigma} \langle p, q \triangleright_{\text{cut}} \rangle. $$

**Notation 8.** For the purpose of readability given two nets $S$ and $T$ with respective conclusions $p_1, \dots, p_n$ and $q_1, \dots, q_k$, say $m = \min(n, k)$, we will denote the interaction $S ::_{\text{pr}_m} T$ by $S :: T$, whenever there is no ambiguity.

For instance if $S$ and $T$ have the same number of conclusion, $S :: T$ denotes $S ::_{\text{id}} T$.

**Notation 9.** Given $\sigma \subseteq \text{out}(S) \times \text{out}(T+R)$ an interface between a net $S$ and a sum of nets $T \parallel R$. The notation $\sigma | T$ will denote the interface which relates conclusion of $S$ to conclusion of $T$ given as $\sigma \cap \text{out}(S) \times \text{out}(T)$. Obviously this also defines $\sigma | R$.

**PROPOSITION 3.2 (INTERACTION AS AN ACTION).** Given $S, T$ and $R$ three multiplicative nets, and $\sigma$ an interface between $S$ and $T \parallel R$. $S ::_{\sigma} (T \parallel R)$ is equal to $(S ::_{\sigma|T} T) ::_{\sigma|R} R$.

**Definition 3.3.** A net $S$ fails cut elimination when it has no reduction to $\langle \triangleright_{\star} \rangle$.

**Remark 12.** Failure of cut elimination is preserved by anti-reduction. Moreover, clashing cuts are preserved during cut elimination, thus a net containing such a cut fails cut elimination.

## 3.2 Orthogonality

**Definition 3.4 (Orthogonality).** Two nets $S_1$ and $S_2$ are orthogonal if there exists an interface $\sigma$ such that $S_1 ::_{\sigma} S_2 \rightarrow^{*} \star_0$.<fnref n="3" /> In that case we write $S_1 \perp S_2$.

**Remark 13.** Since cuts are asymmetric, namely $\langle p, q \triangleright_{\text{cut}} \rangle$ and $\langle q, p \triangleright_{\text{cut}} \rangle$ are distinct the interaction $S :: T$ and $T :: S$ are not the same nets. However this has no consequence on cut elimination, because the reduction steps are defined up to commutation of the input of a cut link thus $S :: T$ reduces to $\star_0$ if and only if $T :: S$ does. As expected the relation of orthogonality is symmetric.

**Remark 14.** Since cut elimination preserves the conclusions of a net, two nets may only be orthogonal when they have the same number of conclusion. Furthermore if two nets are orthogonal, there exists a reordering of the conclusions of $S_1$ such that the orthogonality is witnessed by the identity interface.

**Definition 3.5 (Type).** Given a set $A$ of multiplicative nets, we define the orthogonal of $A$ as $A^{\perp} = \{P | \forall R \in A, P \perp A\}$. A type $A$ is a set of multiplicative nets such that $A^{\perp} = A$.<fnref n="4" />

**Remark 15.** Two nets which are orthogonal have the same number of output. As a consequence two orthogonal types which are non empty, must contain nets with the same number of outputs.

**Notation 10.** We will denote by $\#S$ the number of outputs of $S$. For a type $A$ we let $\#A$ denote the number of outputs of the nets in $A$.

**Remark 16.** There cannot be simultaneously a net with a terminal $\mathfrak{A}$ (or $\otimes$) link in its $i$-th position in $A$ and $A^{\perp}$: their interaction contains a clashing cut and by remark 12 it would fail cut elimination, meaning the nets cannot be orthogonal.

**PROPOSITION 3.6 (SYMMETRY OF TYPES).** For any type $A$ with one conclusion; (1) there exists a net $S$ with a terminal $\mathfrak{A}$-link that belongs to $A$ or $A^{\perp}$, and (2) there exists a net $S$ with a terminal $\otimes$-link that belongs to $A$ or $A^{\perp}$.

<footnote n="3">³Note that, we require the existence of such a reduction, not all reductions need to behave this way.</footnote>

<footnote n="4">⁴Equivalently, a type is a set $A$ such that $A = B^{\perp}$ for some set $B$, see, for instance, [8].</footnote>
## 3.3 Construction on Types

**Definition 3.7 (Constructions on types).** Given two sets of nets A and B their functional composition denoted $A \succ B$, and their parallel composition denoted $A \parallel B$ are defined as follows:

$$ 
\begin{aligned}
A \succ B &\triangleq \{S \mid \text{for any } \bar{a} \in A^{\perp}, S \coloneqq \bar{a} \in B \text{ and } \#S \ge \#A\}, \\
A \parallel B &\triangleq \{a \parallel b \mid a \in A, b \in B\}^{\perp\perp}.
\end{aligned}
 $$

**Remark 17.** The side condition that $\#S \ge \#A$ is to avoid ambiguous situation where potentially A contains a net $T$ which has more conclusions than $S$. In that case in $S \coloneqq T$ the remaining conclusions are conclusions of $T$ hence for some other net $U$ the interaction ($S \coloneqq T$) $\coloneqq U$ isn't $S \coloneqq (T \parallel U)$ but $T \coloneqq (S \parallel U)$ (upto commutation of the input of cuts between $S$ and $T$). With this condition the interaction ($S \coloneqq T$) $\coloneqq U$ when $T \in A^{\perp}$ and $U \in B^{\perp}$ is the net $S \coloneqq (T \parallel U)$.

**PROPOSITION 3.8 (DUALITY).** Given two types A and B: (A $\parallel$ B)$^{\perp}$ = A$^{\perp}$ $\succ$ B$^{\perp}$ and (A $\succ$ B)$^{\perp}$ = A$^{\perp}$ $\parallel$ B$^{\perp}$.

**Remark 18.** The duality of the constructions – proposition 3.8 – ensures that the set of types is closed under the $\parallel$ and $\succ$ operations. Furthermore the set of types is also closed under any intersection however it isn't closed under union, this will influence the definition of intersection and union type 5.11.

**PROPOSITION 3.9 (ASSOCIATIVITY).** Given A, B and C three types we have the following commutations:

* (A $\parallel$ B) $\parallel$ C is equal to A $\parallel$ (B $\parallel$ C).

* (A $\succ$ B) $\succ$ C is equal to A $\succ$ (B $\succ$ C).

**PROOF.** It is clear that the parallel construction is associative. Hence its dual construction, the composition, is associative too. $\square$

**Definition 3.10 (Sequential constructions on types).** Given A and B two types with one conclusion, we define their tensor product (denoted $\otimes$) and their compositional product (denoted $\mathcal{Y}$):

$$ 
\begin{aligned}
A \otimes B &\triangleq \{S + \langle S(1), S(2) \succcurlyeq p \rangle \mid S \in A \parallel B\}^{\perp\perp}, \\
A \mathcal{Y} B &\triangleq \{S + \langle S(1), S(2) \succcurlyeq \mathcal{Y} p \rangle \mid S \in A \succ B\}^{\perp\perp},
\end{aligned}
 $$

where $p$ denotes a fresh position.

**PROPOSITION 3.11 (DUALITY).** Given A and B two types with one conclusion, $(A \otimes B)^{\perp} = A^{\perp} \succcurlyeq B^{\perp}$ and $(A \mathcal{Y} B)^{\perp} = A^{\perp} \otimes B^{\perp}$.

## 3.4 Interpretation of formulas

We interpret formulas and hypersequent of multiplicative and second order multiplicative linear logic. We will respectively denote MLL and $\text{MLL}_2$ the multiplicative and second order multiplicative fragments of Linear Logic. On the other $\text{MLL}^*$ will denote the multiplicative fragment with generalized axiom, as found in [1].

The definition of formulas and proofs of $\text{MLL}_2$ (and MLL) is standard and can be found in [11]. The notion of hypersequent we use is similar to the tree-hypersequents used in some modal logics, for instance in [14]. Namely our hypersequent are constructed by a simple induction; they are either a formula A, or $H_1, H_2$, or $H_1 \parallel H_2$ where $H_1$ and $H_2$ are hypersequents.

**Definition 3.12 (Interpretation Basis).** An interpretation basis $\mathcal{B}$ is a function that associate with each atomic proposition X a type $[[X]]_{\mathcal{B}}$, the interpretation of X, such that:

* Each net in $[[X]]_{\mathcal{B}}$ has one conclusion.

* For any atomic proposition X, we have $[[X^{\perp}]]_{\mathcal{B}} \subseteq [[X]]_{\mathcal{B}}^{\perp}$.

**Definition 3.13 (Interpretation of an hyper-sequent).** Given an interpretation basis $\mathcal{B}$, the interpretation of a formula is lifted from atomic formulas to any formula of MLL and any hypersequent of MLL formulas by induction;

$$ [[A \otimes B]]_{\mathcal{B}} \triangleq [[A]]_{\mathcal{B}} \otimes [[B]]_{\mathcal{B}}. $$

$$ [[H_1, H_2]]_{\mathcal{B}} \triangleq [[H_1]]_{\mathcal{B}} \succ [[H_n]]_{\mathcal{B}}. $$

$$ [[A \mathcal{Y} B]]_{\mathcal{B}} \triangleq [[A]]_{\mathcal{B}} \mathcal{Y} [[B]]_{\mathcal{B}}. $$

$$ [[H_1 \parallel H_2]]_{\mathcal{B}} \triangleq [[H_1]]_{\mathcal{B}} \parallel [[H_n]]_{\mathcal{B}}. $$

**Definition 3.14 (Realizer).** A multiplicative net *realizes* – with respect to an interpretation basis $\mathcal{B}$ – an hypersequent $\mathcal{H}$ of MLL formulas whenever it belongs to $[[\mathcal{H}]]_{\mathcal{B}}$.

**Notation 11.** Given a hypersequent $\mathcal{H}$, $S \Vdash_{\mathcal{B}} \mathcal{H}$ denotes the assertion $S \in [[\mathcal{H}]]_{\mathcal{B}}$. Whenever there is no ambiguity the notation $S \Vdash_{\mathcal{B}} \mathcal{H}$ (resp. $[[\mathcal{H}]]_{\mathcal{B}}$) may be relaxed to $S \Vdash \mathcal{H}$ (resp. $[[\mathcal{H}]]$).

# 4 ADEQUACY

As we mentioned in the introduction realisability models comes with a simple process transforming sequent calculus proofs into programs (in our case nets). In the case of Proof structures (e.g. nets) that process is well-known. Proof structures have been introduced by Jean Yves Girard in his seminal paper [5] and provide a natural way to represent the proofs of linear logic up to "irrelevant" permutations of their deduction rules. The nets which represent a proof, called *proof nets*, or *correct nets*, are inductively defined on the size of the sequent calculus proof they represent. For second order multiplicative linear logic the definition can for instance be found in [5, 6] and easily adapts to our framework.

**Notation 12.** Let $\mathfrak{B}$ denote one of the proof system under consideration, namely MLL, $\text{MLL}^*$ or later on $\text{MLL}_2, \text{MLL}_2^*$. Let $S$ be a multiplicative net, we denote $S \vdash_{\mathfrak{B}} \Gamma$ whenever there exists a proof $\pi$ in $\mathfrak{B}$ such that $S$ is the representation of $\pi$ in Net.

Furthermore we let $\langle\Gamma : \mathfrak{B}\rangle$ denote the set of all the nets $S \vdash_{\mathfrak{B}} \Gamma$.

**Definition 4.1 (Approximable type and basis).** A type with one conclusion is *approximable* whenever it contains the net $\star_1$. Let $X$ be a propositional variable, an interpretation basis is; (1) *standard* in $X$ whenever $[[X]]_{\mathcal{B}}^{\perp} = [[X^{\perp}]]_{\mathcal{B}}$; (2) *approximable* in $X$ whenever both $[[X]]_{\mathcal{B}}$ and $[[X^{\perp}]]_{\mathcal{B}}$ are approximable.

An interpretation basis is: (1) *regular* whenever it is standard or approximable in any propositional variable; (2) *approximable* when it maps atomic formulas to approximable types.

**Remark 19.** A type A is approximable if and only if $\{\star_1\}^{\perp\perp} \subseteq A$ which is also equivalent to $A^{\perp} \subseteq \{\star_1\}^{\perp}$.

**Remark 20.** An approximable interpretation basis is regular.

**PROPOSITION 4.2.** For any types with one output $A \subseteq B^{\perp}$; $\star_2$ belongs to $A^{\perp} \succ B^{\perp}$.

**THEOREM 4.3.** Let $S$ be a multiplicative net, $\mathcal{B}$ an interpretation basis, and $\Gamma$ a sequent:

* if $\mathcal{B}$ is regular, then $S \vdash_{\text{MLL}} \Gamma \Rightarrow S \Vdash_{\mathcal{B}} \Gamma$,

* if $\mathcal{B}$ is approximable, then $S \vdash_{\text{MLL}^*} \Gamma \Rightarrow S \Vdash_{\mathcal{B}} \Gamma$.
# 5 COMPLETENESS

## 5.1 Test of a formula

**Definition 5.1 (Support of a daimon).** For a daimon link $d = \langle \triangleright_{\mathfrak{A}} p_1, \dots, p_n \rangle$ we define its support as $s(d) = \{p_1, \dots, p_n\}$. For a sum of daimon links $D = d_1 + \dots + d_k$, we define its support $s(D) = \{s(d_1), \dots, s(d_n)\}$.

**Definition 5.2 (switching).** The switching rewriting, denoted $\to_{\mathfrak{A}}$, is the non-deterministic rewriting given by

$$ \begin{align*} \langle \bar{p} \triangleright_l \bar{q}_1, p_1, \bar{q}_2 \rangle + \langle p_1, p_2 \triangleright_{\mathfrak{A}} p \rangle &\to_{\mathfrak{A}}^l \langle \bar{p} \triangleright_l \bar{q}_1, p, \bar{q}_2 \rangle \\ \langle \bar{p} \triangleright_l \bar{q}_1, p_2, \bar{q}_2 \rangle + \langle p_1, p_2 \triangleright_{\mathfrak{A}} p \rangle &\to_{\mathfrak{A}}^r \langle \bar{p} \triangleright_l \bar{q}_1, p, \bar{q}_2 \rangle \end{align*} $$

The detached position of a switching rewriting is $p_2$ (resp. $p_1$) in the $\to_l^r$ (resp. $\to_r^l$) case of the rewriting. Each switching of a net $S$ equipped with an order $u = (p_1, \dots, p_n)$ on its conclusions, produces a net $S'$ with conclusions ordered as $u \cdot q$ where $q$ is the detached position of the switching step.

A switching of a net $S$ is a normal form of $S$ with respect to the switching rewriting.

**Remark 21.** A normal form for the switching rewriting is a net which contains no $\mathfrak{A}$-link.

**Definition 5.3.** A position $p$ is above a position $q$ in a net $S$ if there exists a directed path from $p$ to $q$.

Given a position $q$ we denote $q \upharpoonright^i S$ the set of initial positions which are above $q$ in $S$.

**Remark 22.** Given a net $S$ with conclusions $p_1, \dots, p_n$ the sets $p_1 \upharpoonright^i S, \dots, p_n \upharpoonright^i S$ form a partition of the initial positions of $S$. We denote this partition $\upharpoonright^i S$.

**Notation 13.** Given a net $S$ we write $S^{\mathfrak{A}}$ the net made of its $\mathfrak{A}$-links.

**Notation 14.** Given $\Gamma = (A_1, \dots, A_n)$ the representative of a sequent we denote by $\Gamma(i)$ the formula $A_i$. We denote a net $S$ by $S[p_1, \dots, p_n]$ whenever the conclusion of $S$ are ordered as $p_1, \dots, p_n$.

**Definition 5.4 (Witness of a sequent).** A net $S$ is a witness of a sequent $\Gamma$, denoted $S \vdash \Gamma$, when:

* If $\Gamma$ is a sequent of $n$ atomic formulas, $S = \mathfrak{A}_n$;

* If $S \vdash A, B, \Gamma$, then $S + \langle S(1), S(2) \triangleright \otimes p \rangle \vdash A \otimes B, \Gamma$.

* If $S \vdash A, B, \Gamma$, then $S + \langle S(1), S(2) \triangleright_{\mathfrak{A}} p \rangle \vdash A \mathfrak{A} B, \Gamma$.

* If $S[\bar{p}_1, q_1, \bar{p}_2] \vdash \Gamma, A, B, \Delta$, then $S[\bar{p}_1, q_2, q_1, \bar{p}_2] \vdash \Gamma, B, A, \Delta$.

**Remark 23.** A cut-free proof net $S \vdash \Gamma$ is in particular a witness $S \vdash \Delta$ of a sequent $\Delta$ such that $\theta\Delta = \Gamma$ for some substitution $\theta$. However a net $S \vdash \Gamma$ may not be a proof net and could contain cycles or disconnections: the witness condition only provide information on multiplicative connectives constituting the net $S$. This information is crucial in order to apply the test of a formula $A$: orthogonality with the tests of $A$ coincides with correctness for any nets $S \vdash A$.

**Definition 5.5 (Inversion).** Given a net $S$ the inversion of $S$ denoted $\bar{S}$ corresponds to $S$ in which the $\mathfrak{A}$ and $\otimes$ labels have been inverted.

**Remark 24.** Whenever $S$ witnesses a sequent $A_1, \dots, A_n$ then $\bar{S}$ witnesses $A_1^{\perp}, \dots, A_n^{\perp}$.

**Definition 5.6 (Test of a formula).** A cut-free net $T$ is a test of a formula $A$ if (1) $T$ is a witness of $A^{\perp}$ and (2) there exists a switching $\sigma\bar{T}$ of the net $\bar{T}$ such that $\upharpoonright^i \sigma\bar{T} = \text{supp}(T^{\mathfrak{A}})$.

We denote by tests($A$) the set of tests of $A$.

**THEOREM 5.7 (CORRECTNESS OF TESTS).** Any test of a formula $A$ is a proof in MLL$^{\mathfrak{A}}$ of the negation $A^{\perp}$.

**PROOF SKETCH.** Consider a test of the formula $A$, meaning a net $T$ which witness $A^{\perp}$ and such that $\text{supp}(T^{\mathfrak{A}}) = \upharpoonright^i \sigma\bar{T}$. We will assume that $T$ is not correct and show it implies that $T^{\mathfrak{A}}$ isn't correct, which is absurd. To conclude we perform a series of transformation preserving correctness on $T^{\mathfrak{A}}$ which results in $T$:

(1) First, perform some $\eta$-expansions from $T^{\mathfrak{A}}$ to obtain a witness of $A, A^{\perp}$ that we denote $W$.

(2) Perform the switching on the syntactical part $A$ in $W$ obtaining a net $W'$ with $n+1$ conclusions.

(3) Make the $n$ conclusions of the switching interact with $T^{\mathfrak{A}}$.

(4) The switching of $A$ is made only of tensor links thus the cut-elimination results in some daimons $D$ which have for support the partition of the switching $\text{supp}(D) = \upharpoonright^i \sigma A$.

(5) After eliminating the remaining glueing cuts the partitions goes above $A^{\perp}$, we obtain a net $T$ witnessing $A^{\perp}$ and such that $\text{supp}(T^{\mathfrak{A}}) = \text{supp}(D) = \upharpoonright^i \sigma A$. $\square$

**THEOREM 5.8 (DANOS REGNIER TESTS, [3]).** Given a cut-free net $S \vdash A_1, \dots, A_n$, the two following assertions are equivalent:

* $S \vdash_{\text{MLL}^{\mathfrak{A}}} A_1, \dots, A_n$;

* $S$ is orthogonal to tests($A_1$) $\| \dots \| \text{ tests} (A_n)$.

## 5.2 Intersection Types and Completeness

**Definition 5.9 (self dual type).** A type $A$ is self-dual whenever $A \subseteq A^{\perp}$. An interpretation basis is self-dual when it maps any propositional variable to a self dual type.

**Notation 15.** A substitution $\theta: \mathcal{V} \to \mathcal{F}_{\text{MLL}}$ can be lifted to formulas by the induction $\theta A \Box B = \theta A \Box \theta B$ where $\Box$ is a symbol $\mathfrak{A}$ or $\otimes$. Furthermore substitutions can be lifted to hypersequent by $\theta H_1, H_2 = \theta H_1, \theta H_2$ and $\theta H_1 \parallel H_2 = \theta H_1 \parallel \theta H_2$.

Given two hypersequents we denote $\Delta \leq \Gamma$ whenever there exists a substitution $\theta$ such that $\theta\Delta = \Gamma$.

**Remark 25.** Given a net $S$ since daimon rules may introduce any sequent, whenever $S \vdash_{\text{MLL}^{\mathfrak{A}}} \Delta$ and $\Delta \leq \Gamma$ it follows that $S \vdash_{\text{MLL}^{\mathfrak{A}}} \Gamma$.

**THEOREM 5.10 (MLL$^{\mathfrak{A}}$ COMPLETENESS).** Let $S$ be a cut-free net and $\Gamma$ be a sequent. For any self dual and approximable interpretation basis $\mathcal{B}$, if $S$ belongs to $[\Gamma]_{\mathcal{B}}$ then $S$ represents a proof of $\Gamma$ in MLL$^{\mathfrak{A}}$.

**PROOF SKETCH.** Let $\Gamma = A_1, \dots, A_n$ be a sequent. Consider a net $S$ a cut free net in $[\Gamma]_{\mathcal{B}}$, since the basis is self-dual the syntactical part of $S$ is borned by $\Gamma$, hence $S \vdash \Delta$ such that $\theta\Delta \leq \Gamma$ for some substitution $\theta$. $S$ belonging to the interpretation of $\Gamma$ equivalently means:

$$ S \perp [A_1^{\perp}] \parallel \dots \parallel [A_n^{\perp}]. $$

By adequacy for any index $i$, $[A_i^{\perp}: \text{MLL}^{\mathfrak{A}}] \subseteq [A_i^{\perp}]$. Furthermore $\Delta \leq \Gamma$ hence $\Delta = B_1, \dots, B_n$ such that $B_i \leq A_i$ for each $i$ and thus $B_i^{\perp} \leq A_i^{\perp}$. As a consequence $[B_i^{\perp}: \text{MLL}^{\mathfrak{A}}] \subseteq [A_i^{\perp}: \text{MLL}^{\mathfrak{A}}]$. Finally from theorem 5.7 we have tests($B_i$) $\subseteq [B_i^{\perp}: \text{MLL}^{\mathfrak{A}}]$. Hence we conclude

$$ S \perp \text{tests}(B_1^{\perp}) \parallel \dots \parallel \text{tests}(B_n^{\perp}). $$
Since $S \vdash \Delta$ by theorem 5.8 we conclude $S \vdash_{\text{MLL}\star} \Delta$ and so using
remark 25, $S \vdash_{\text{MLL}\star} \Gamma$. $\square$

**Notation 16.** Given an interpretation basis $\mathcal{B}$ and a type $A$ we let $\mathcal{B}\{X \mapsto A\}$ denote the basis which maps $X$ to $A$, $X^{\perp}$ to $A^{\perp}$ and any propositional $Y$ that isn't $X$ or its dual to $[[Y]]_{\mathcal{B}}$.

**Definition 5.11 (Intersection and union type).** Let $\mathcal{B}$ be an interpretation basis, and $\Omega$ a set of types with one output. Given $\Gamma$ a sequent of MLL formulas and $X$ a propositional variable the intersection type and union type on $\Omega$ of $\Gamma$ in $X$ w.r.t. to $\mathcal{B}$ are defined as follows:

$$ [[\bigcap_{X \in \Omega} \Gamma]]_{\mathcal{B}} \triangleq \bigcap_{R \in \Omega} [[\Gamma]]_{\mathcal{B}\{X \mapsto R\}}, \quad [[\bigcup_{X \in \Omega} \Gamma]]_{\mathcal{B}} \triangleq \left( \bigcup_{R \in \Omega} [[\Gamma]]_{\mathcal{B}\{X \mapsto R\}} \right)^{\perp\perp} $$

**Remark 26.** We can naturally consider the intersection and unions on types that are not build by sequential operations, for instance on parallel composition of types or on functional composition of types. For example the following type;

$$ \bigcap_{R \in \Omega} [[A_1]]_{\mathcal{B}\{X \mapsto R\}} \parallel \cdots \parallel [[A_n]]_{\mathcal{B}\{X \mapsto R\}}. $$

**Definition 5.12.** A net is proof like whenever its daimon links are only of the form $\langle \triangleright_{\star} p_1, p_2 \rangle$, e.g isomorphic to $\star_2$.

**THEOREM 5.13.** Let $S$ be a cut-free and proof-like net, $\Gamma$ be a sequent and $\Omega$ denote the set of all types with one output. For any self dual and approximable interpretation basis $\mathcal{B}$, if $S$ belongs to $\bigcap_{X \in \Upsilon} [[\bigcap_{X \in \Omega} \Gamma]]_{\mathcal{B}}$ then $S$ represents a proof of $\Gamma$ in MLL.

# 6 ADEQUACY AT (PRE-)SECOND ORDER

We now present how our approach can be extended to second order linear logic MLL₂, and provide an adequate model for MLL₂. The hypergraphs are now built with the multiplicative links of definition 2.10 to which we add two new kind of unary connective links, namely $\langle p \triangleright \forall q \rangle$ and $\langle p \triangleright \exists q \rangle$ which respectively corresponds to universal and existential quantification. In that context, the modules and nets are hypergraphs build from this wider set of links which follow the same specification as for multiplicative nets (see the definitions 2.10 and 2.11).

Furthermore we need to extend cut elimination in the presence of these new links, for now we give a dummy version of cut elimination similar to the elimination in the multiplicative case, namely the cuts $(\forall \lor \exists)$ and $(\exists \lor \star)$ and $(\forall \lor \star)$ can be eliminated as follow, while the other kind of cut are treated as clashing cuts;

* $\langle p \triangleright \forall p' \rangle + \langle p', q' \triangleright \text{cut} \rangle + \langle q \triangleright \exists q' \rangle \to \langle p, q \triangleright \text{cut} \rangle$.

* $\langle p \triangleright \forall p' \rangle + \langle p', q \triangleright \text{cut} \rangle + \langle \triangleright_{\star} q \rangle \to \langle p, q \triangleright \text{cut} \rangle$.

* $\langle p \triangleright \exists p' \rangle + \langle p', q \triangleright \text{cut} \rangle + \langle \triangleright_{\star} q \rangle \to \langle p, q \triangleright \text{cut} \rangle$.

**Definition 6.1 (realizers of MLL₂).** Let $\mathcal{B}$ be an interpretation basis. The set of realizers of a formula $A$ of MLL₂ is defined by adding the two following cases to definition 3.13 (the net $S$ has one conclusion):

$$ \begin{aligned} [[\forall X A]] &\triangleq \{S + \langle S(1) \triangleright \forall q \rangle \mid S \in [[\bigcap_{X \in \Omega} A]]^{\perp\perp} \\ [[\exists X A]] &\triangleq \{S + \langle S(1) \triangleright \exists q \rangle \mid S \in [[\bigcup_{X \in \Omega} A]]^{\perp\perp} \end{aligned} $$

**Remark 27.** Proposition 4.2 ensures that $\star_2$ belongs to $A \succ A^{\perp}$ for any type $A$. In particular for any interpretation basis $\mathcal{B}$ it belongs

to the intersection $\bigcap_{R \in \Omega} ([[X]]_{\mathcal{B}\{X \mapsto R\}} \succ [[X^{\perp}]]_{\mathcal{B}\{X \mapsto R\}})$ and is the only cut free net occurring in that intersection.

This implies that $\langle \triangleright_{\star} p_1, p_2 \rangle + \langle p_1, p_2 \triangleright_{\star} p \rangle$ belongs to

$$ \bigcap_{R \in \Omega} ([[X]]_{\mathcal{B}\{X \mapsto R\}} \succ \mathcal{N} \parallel [[X^{\perp}]]_{\mathcal{B}\{X \mapsto R\}}) $$

Hence, by definition this net extended with a universal quantifier link is an element of $[[\forall X, X \succ X^{\perp}]]_{\mathcal{B}}$.

**THEOREM 6.2 (ADEQUACY FOR MLL₂).** Given $S$ a proof in MLL₂ of a sequent $\Gamma$. For any regular interpretation basis $\mathcal{B}$, $S \in [[\Gamma]]_{\mathcal{B}}$.

# 7 COMPUTABILITY OF TYPES

This section shows that the adequate model we constructed enjoys a property of finiteness, namely each type is the orthogonal of a finite set. As mentioned in the introduction, this hints towards a correctness criterion for MLL₂ which will be the object of the last section. Given a type $A$ and a type $S$ how difficult is to assert that $S$ belongs to $A$. Orthogonality provides a natural tool to talk about the computability of such a problem. Given a sequent $\Gamma = A_1, \dots, A_n$ we denote $\Gamma$ the sequent $A_1^{\perp}, \dots, A_n^{\perp}$.

**Definition 7.1.** A type $A$ is *computable* whenever there exists a finite set $B$ such that $A = B^{\perp}$. A type $A$ is *syntactically computable* if for each sequent $\Gamma$ there exists a finite set $A^{\perp}(\Gamma)$ of nets witnessing $\Gamma$ such that, for any net $S$ witnessing $\Gamma$; $S \in A \Leftrightarrow S \perp A^{\perp}(\Gamma)$.

**Remark 28.** A computable type $A = B^{\perp}$ is a type such that the statement $S \in A$ can be decided interactively by testing the orthogonality with each element of the finite set $B$.

This notion is strongly related to the correctness criterion of proof nets [5]; given a sequent $\Gamma$ and a proof system $\mathfrak{P}$ the computability of the set $\{\Gamma : \mathfrak{P}\} = B^{\perp}$ provides a way to assert in finite time<fnref n="5" /> if a net $S$ is a proof net of $\Gamma$ or not.<fnref n="6" />

**PROPOSITION 7.2.** The functional composition $A \succ B$ and the parallel composition $A \parallel B$ of two syntactically computable types are syntactically computable.

**PROPOSITION 7.3.** The union $(\bigcup_{i \in I} A_i)^{\perp\perp}$ of a family of computable types is computable. The intersection $\bigcap_{i \in I} A_i$ of a finite family of computable types is computable.

**Notation 17.** We write abusively $\star$ the type $\{\star_1\}^{\perp\perp}$ and define the following particular types:

$$ \otimes_{\star} = \{\langle \triangleright_{\star} p_1, p_2 \rangle + \langle p_1, p_2 \triangleright \otimes p \rangle\}^{\perp\perp} $$

$$ \mathcal{N}_{\star} = \{\langle \triangleright_{\star} p_1 \rangle + \langle \triangleright_{\star} p_2 \rangle + \langle p_1, p_2 \triangleright \mathcal{N} p \rangle\}^{\perp\perp} $$

**PROPOSITION 7.4.** Let $\omega$ be the set of types $\{\otimes_{\star}, \mathcal{N}_{\star}, \star, \star^{\perp}\}$ and $\mathcal{B}$ be a basis which maps any $X$ to $\star$. For any hyper-sequent $\mathcal{H}$:

$$ [[\bigcap_{X \in \omega} \mathcal{H}]]_{\mathcal{B}} = [[\bigcap_{X \in \Omega} \mathcal{H}]]_{\mathcal{B}}. $$

<footnote n="5">⁵However there can be a high complexity cost in order to decide $B$.</footnote>

<footnote n="6">⁶In particular, in the case of MLL$\star$ using the theorem 5.8 we have shown that the nets which represent a cut-free proof of a formula $F$ are the cut-free elements of a type $A$ which are orthogonal to a finite set tests($F$), the set of tests of $F$, see definition 5.6.</footnote>
**Remark 29.** Since the set $\omega$ is a finite set, the previous propositions
implies that for an approximable and self dual basis, the intersection
type $\llcorner \cap_{X \in \Omega} \mathcal{H} \rrcorner_B$ is computable.

**Remark 30.** The preservation of computability of the preconstruc-
tions $\parallel, >, \cap$ and $\cup$ naturally extend to the preservation of com-
putability for the construction on types, namely $\aleph, \otimes, \forall$ and $\exists$. In
the case quantifiers this is because (1) a daimon link against a $\exists$ link
can match the reduction of a $\forall$ link against $\exists$ link, and vice versa,
and (2) the dummy elimination rules introduced for the elimination
of the quantifier links can always be performed first during cut
elimination, e.g. they commute to the left during cut elimination.

## 8 SECOND ORDER NETS

Confirming the hint of the existence of correctness criterion for
second order multiplicative linear logic nets provided by the finite-
ness of the union and intersection types, this section is dedicated
to the definition of a novel correctness criterion for $\mathrm{MLL}_2^{\mathcal{X}}$ nets,
e.g. nets with exists-link and forall-links.

The criterion we present is based on the contractibility criterion for MLL (Danos [2]) as formulated in [1]. Our criterion is distinct from Girard’s [6] for several reasons; (1) It is designed for untyped proof structures of $\mathrm{MLL}_2^{\mathcal{X}}$, (2) we are not bound to Girard’s restriction of the criterion to proof structures having only closed formulas as conclusions. Furthermore, the contractibility criterion always reduces the size of the net and enjoys a quadratic complexity. As a consequence, increasing the number of dependencies of a universal quantifier do not increase the number of switchings (and so the time complexity) exponentially (which is the case in Girard’s criterion).

In this section we introduce hypergraphs equipped with pointers,
ers, in order to handle second order quantification and to inter-
pret proofs of $\mathrm{MLL}_2^{\mathcal{X}}$. The challenge in the definition is to add
quantifiers while keeping an untyped setting. Pointers are used to
reintroduce exactly the needed information to deal with quantifiers
(which is usually implicitly given by types).

In previous sections, the vertices of an hypergraph belonged to
a set positions $\mathcal{P}$. In order to handle pointers we enrich the set of
positions as $\mathcal{P} \cup \mathcal{P}^*$ where the elements of $\mathcal{P}^*$ are called pointer
points or pointer positions. We will usually denote pointer ports as
p, q, s, ... . The elements of $\mathcal{P} \cup \mathcal{P}^*$ are called positions, while ele-
ments of $\mathcal{P}$ will be called regular positions. A pointer or pointer-link
is an link with one source which is a pointer port and one target
which is a position, and the label p. Moreover, we will distinguish
between existential and universal pointers. We will denote a univer-
sal (resp. existential) pointer $\langle s \triangleright_p t \rangle$ by $\langle s \xrightarrow{\vee} t \rangle$ (resp. $\langle s \xrightarrow{\exists} t \rangle$).
A pointer structure is an hypergraph made only of pointers. An
hypergraph with pointers P is an hypergraph $\mathcal{H}$ summed with a
pointer structure P. A pointer belongs to an hypergraph $\mathcal{H}$ when
its source and target are positions of $\mathcal{H}$.

As for multiplicative nets, we define *modules* for second order
multiplicative linear logic as sums of the following links:

$$
\begin{align*}
\langle p, q \triangleright_{\text{cut}} \rangle \quad & \langle \triangleright_{\mathcal{X}} \bar{p} \rangle \quad \langle p_1, p_2 \triangleright_{\otimes} p \rangle \quad \langle p_1, p_2 \triangleright_{\mathcal{X}} p \rangle \\
& \langle p \triangleright_{\forall} q, s \rangle \quad \langle p \triangleright_{\exists} q, s \rangle \quad \langle s \xrightarrow{\vee} t \rangle \quad \langle s \xrightarrow{\exists} t \rangle.
\end{align*}
$$

Pointer positions are involved exclusively in existential, uni-
versal, and pointer links. We distinguish universal and existential

pointer links and the semantics of these pointers pointers will be
distinct. A pre-net is a module $\mathcal{H}$ with pointers P such that:

* Existential pointers sources are pointer positions involved in existential links, and their target lies above their sources, i.e. there exists a directed path from the target to the source; moreover, given two existential links $e_1$ and $e_2$ with respective pointer positions $s_1$ and $s_2$ such that $e_2$ is above $e_1$ a pointer of source $s_1$ cannot point on a position which is above the target of a pointer of source $s_2$;

* Universal pointers sources are pointer positions involved in universal links, and their targets are either conclusions of $\mathcal{X}$ links or pointer positions of existential links;

* A given position is the target of at most one existential pointer link;

* $\mathcal{H}$ is target-disjoint, source-disjoint, and target-surjective.

**Remark 31.** In a second order net $\mathcal{H} + \mathcal{P}$ only the underlying hypergraph $\mathcal{H}$ need to be target and source disjoint, pointers have no such restriction in particular two pointers may have the same source such as $\langle s \to t \rangle$ and $\langle s \to t' \rangle$ while occurring in the same net. Similarly two distinct pointers may share their target, this may occur for instance when two distinct $\forall$ links point to the same position, indicating it should contain a formula depending on the two corresponding quantified variables. Similarly, a $\forall$ pointer link may share its target with an $\exists$ pointer link, indicating that the existential witness in that position contains the universally quantified propositional variable.

## 8.1 Trees, pointers, and approximations

Pre-nets still lack an important property ensured by types: that all
existential witnesses are the same. Without this property, we would
allow an existential quantifier to point to two distinct witnesses
with different principal connectives. We overcome the challenge of
expressing this constraint without introducing types by defining
a notion of coherence between positions in a pre-net. Intuitively
coherent positions are positions which can host a unifying witness.

In order to formulate properly this constraint, we need to introduce the notion of *tree with pointers*. Along this section a tree is a tree with pointers.

**Definition 8.1.** Given a position $p$, trees with pointers of conclusion $p$ or $p$-trees are inductively defined as follows:

* A unary link $\langle \triangleright_{\mathcal{X}}, p \rangle$ is a $p$-tree;

* If $S$ is $p$-tree disjoint with $S'$ a $p'$-tree and $q$ is a fresh position, then $S \cup S' + \langle p, p' \triangleright \otimes q \rangle$ and $S \cup S' + \langle p, p' \triangleright \mathcal{X} q \rangle$ is a $q$-tree;

* If $S$ is a $p$-tree, $q$ is a fresh regular position and $s$ a fresh pointer position, then $S + \langle p \triangleright \forall q, s \rangle$ and $S + \langle p \triangleright \exists q, s \rangle$ is a $q$-tree.

* If $S$ is a $p$-tree, $t$ is a regular position in $S$, and $s$ is a pointer position:

- if $s$ is conclusion of an $\exists$ link, then $S + \langle s \xrightarrow{\exists} t \rangle$ is a $p$-tree;

- if $s$ is not conclusion of an $\exists$ link (hence possibly a fresh pointer position) and $p'$ is either the conclusion of a $\mathcal{X}$ link or the pointer position of an $\exists$ link, then $S + \langle s \xrightarrow{\forall} t \rangle$ is a $p$-tree.

1103

1104

1105

1106

1107

1108

1109

1110

1111

1112

1113

1114

1115

1116

1117

1118

1119

1120

1121

1122

1123

1124

1125

1126

1127

1128

1129

1130

1131

1132

1133

1134

1135

1136

1137

1138

1139

1140

1141

1142

1143

1144

1145

1146

1147

1148

1149

1150

1151

1152

1153

1154

1155

1156

1157

1158

1159

1160
Given a pre-net $\mathcal{H} + \mathbf{P}$ and a position $p$, we now define in a straightforward way the tree (with pointers) above $p$ in $\mathcal{H} + \mathbf{P}$. This will then be used to define the syntactic tree above the vertex, including the pointers of $\forall$ links that may point to vertices in that syntactic tree.

**Definition 8.2.** Given a pre-net $\mathcal{H} + \mathbf{P}$ and a position $p$, the tree (with pointers) above $p$ in $\mathcal{H} + \mathbf{P}$, written $S_{\mathcal{H}+\mathbf{P}}(p)$, is defined as the largest $p$-tree $S$ that is contained in $\mathcal{H} + \mathbf{P}$ when its daimon links are removed.

We now define a notion of approximation on trees. We first need to introduce useful notations that will simplify statements.

**Definition 8.3.** Given a pre-net $\mathcal{H} + \mathbf{P}$ and a position $p$, we define $P_{\forall}(\rightarrow p)$ (resp. $P_{\exists}(\rightarrow p)$) as the set of all universal (resp. existential) pointer links in $\mathbf{P}$ of target $p$. We similarly define $P_{\forall}(p \rightarrow)$ (resp. $P_{\exists}(p \rightarrow)$) as the set of all universal (resp. existential) pointer links in $\mathbf{P}$ of source $p$.

**Notation 18.** Given $p$ and $q$ two positions we denote $[p := q]$ the function which takes a position $s$ and returns $q$ if $s = p$ and returns $s$ otherwise. We adopt an infix notation $s[p := q]$ to denote the image of $s$ under $[p := q]$. We lift these functions to pointer links, given a link $\langle s \rightarrow t \rangle$ defining $\langle s \rightarrow t \rangle [p := q]$ as $\langle s[p := q] \rightarrow t[p := q] \rangle$. Furthermore we lift this notation to sets of pointers $X$ so that $X[p := q]$ denotes the images of the elements of $X$ under $[p := q]$.

**Definition 8.4.** The approximation relation $<$ on trees is defined as the transitive closure of the relation shown in Figure 5, where in the first two lines the positions $p, q$ do not appear in left hand tree and in the last two lines the positions $p, s$ do not appear in left hand tree. Note that when pointers are renamed, two pointers may become equal. In this case, only one link is kept.

A set of trees $S_1, \dots, S_k$ is coherent when there exists a tree $\mathcal{R}$, a witness, such that $S_i < \mathcal{R}$ up to a renaming of positions.

We note that verifying that a set of trees $S_1, \dots, S_n$ or respective conclusion $p_1, \dots, p_n$ is coherent is not as costly as it could be thought at first sight. On can simply compare the tree from their conclusions while bookkeeping renamings of positions. Inductively, one performs the following steps:

* check if there exists a type of link such that all $p_i$ are either targets of this type of link (type c) or target of a $\mathbf{X}$ link (type a) and deduce needed renamings (e.g. that $p_1, \dots, p_n$ should be identified);

* check if the sets $P_{\exists}(\rightarrow p_i)$ are all equal (up to renaming);

* check if the sets $P_{\forall}(\rightarrow p_i)$ for $p_i$ of type a are equal (up to renaming), and bookkeep one of them to check, when available, that it is equal, for each $p_i$ of type c, to

$$ \cup_{r'} \text{ above } p_i P_{\forall}(\rightarrow r') \setminus \cup_{r'} \text{ above } p_i P_{\forall}(r' \rightarrow). $$

The algorithm just described can furthermore be used to construct a witness, which in fact is minimal.

**LEMMA 8.5.** Given a coherent set of trees $S_1, \dots, S_k$, there exists a minimal witness, noted $\text{Wit}(S_1, \dots, S_k)$.

We are now ready to define nets as pre-nets for which $\exists$ links possess a witness.

**Definition 8.6.** A pre-net $\mathcal{H} + \mathbf{P}$ is a net if for all link $\langle p \succcurlyeq q, s \rangle$ in $\mathcal{H}$, the set of trees $S = \{S_{\mathcal{H}+\mathbf{P}}(r) \mid r \in P_{\exists}(s \rightarrow)\}$ is coherent. The minimal witness $\text{Wit}(S)$ is called the minimal witness of the link $\langle p \succcurlyeq q, s \rangle$, and sometimes abusively written as $\text{Wit}(\langle p \succcurlyeq q, s \rangle)$.

## 8.2 Contractibility criterion

The next step is to define the notion of contraction for second order nets which will be used to define the correctness criterion.

**Definition 8.7.** The contraction relation on second order nets is defined by the contextual closure of the following reduction steps (rules are shown in Figure 7 where we replaced sums by sets to ease readability, and illustrated in Figure 6):

* If $P_{\forall}(\rightarrow p) \neq \emptyset$ and $P_{\exists}(\rightarrow p) \neq \emptyset$, we write $\langle s \xrightarrow{\exists} p \rangle$ the unique element of $P_{\exists}(\rightarrow p)$ and we can apply the pointers rule (Figure 7e);

* The tensor (Figure 7a) and parr rule (Figure 7b) can be applied without any side condition.

* If $P_{\forall}(\rightarrow p)$ is empty, we can apply the existential rule (Figure 7c);

* If either $P_{\forall}(s \rightarrow)$ is empty or contains only the pointer link $\langle s \rightarrow p \rangle$, we can apply the universal rule (Figure 7d).

Note that two pointers may become equal after applying a rule. In this case, only one link is kept.

Multiplicative rules for contractibility can be understood as Curien's contractibility rules for MLL [1], extended to handle pointers. This rewriting of pointers in the net is crucial: the existential pointers which were on premisses are destroyed (we lose the information of the existential witness), whereas the universal pointers are moved to the conclusion of the contracted link - keeping track of the dependence. The existential link contraction can always be performed, and removes any pointers targetting its pointer position: this is the only rule erasing universal pointers. The universal link contraction can only be performed when no pointers exists from this link to a position that is not above it. This intuitively corresponds to the usual condition on the context in the universal quantifier introduction rule. The last rule is the essential one: if a conclusion $p$ of a daimon link is at the same time the target of an existential pointer and the target of (possibly multiple) universal pointers, we move the universal pointers to the pointer position of the existential link pointing to $p$. This records the dependence of the existential witness on the universal quantifiers.

**Definition 8.8.** A net $\mathcal{H} + \mathbf{P}$ with $n$ conclusions is contractible if there exists a sequence of contractibility reduction rules ending on $\mathbf{X}_n$, i.e. $S \xrightarrow{c} \mathbf{X}_n$.

**Remark 32.** The contractibility rewriting preserves the number of conclusions of a net. During contraction steps, the number of links always decreases except in the case of Figure 7e in which the number of universal pointers pointing to a regular position decrease; this makes the rewriting strongly normalizing.

We are now ready to state the main theorem of this Section: the contractibility correctness criterion for second order nets.

**Remark 33.** Our way of dealing with existential quantifiers in nets forces witnesses to appear as principal formulas in the proof. Consequently, not all sequent calculus proofs are represented directly in

1219

1220

1221

1222

1223

1224

1225

1226

1227

1228

1229

1230

1231

1232

1233

1234

1235

1236

1237

1238

1239

1240

1241

1242

1243

1244

1245

1246

1247

1248

1249

1250

1251

1252

1253

1254

1255

1256

1257

1258

1259

1260

1261

1262

1263

1264

1265

1266

1267

1268

1269

1270

1271

1272

1273

1274

1275

1276
$$ \langle \Delta_{\star} r \rangle + P_{\vee}(\rightarrow p)[p := r] + P_{\vee}(\rightarrow q)[q := r] < \langle \Delta_{\star} p \rangle + P_{\vee}(\rightarrow p) + P_{\exists}(\rightarrow p) + \langle \Delta_{\star} q \rangle + P_{\vee}(\rightarrow q) + P_{\exists}(\rightarrow q) + \langle p, q \Delta_{\star} r \rangle $$

$$ \langle \Delta_{\star} r \rangle + P_{\vee}(\rightarrow p)[p := r] + P_{\vee}(\rightarrow q)[q := r] < \langle \Delta_{\star} p \rangle + P_{\vee}(\rightarrow p) + P_{\exists}(\rightarrow p) + \langle \Delta_{\star} q \rangle + P_{\vee}(\rightarrow q) + P_{\exists}(\rightarrow q) + \langle p, q \Delta_{\otimes} r \rangle $$

$$ \langle \Delta_{\star} r \rangle + P_{\vee}(\rightarrow p)[p := r] < \langle \Delta_{\star} p \rangle + P_{\vee}(\rightarrow p) + P_{\exists}(\rightarrow p) + \langle p \Delta_{\exists} q, s \rangle + P_{\vee}(\rightarrow s) $$

$$ \langle \Delta_{\star} r \rangle + P_{\vee}(\rightarrow p)[p := r] < \langle \Delta_{\star} p \rangle + P_{\vee}(\rightarrow p) + P_{\exists}(\rightarrow p) + \langle p \Delta_{\vee} q, s \rangle + P_{\vee}(\rightarrow s) $$

<figure><img src="image_4.png" /><figcaption>Figure 6: Contraction rules illustrated</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 7: Contraction rules</figcaption></figure>

our syntax. Proofs introducing existential quantifiers with a witness appearing only as a subformula (e.g. a subformula of an axiom's conclusion) need to be partially $\eta$-expanded for all witnesses to appear as principal formulas. With this mild requirement, we can show that second order nets represent second order sequent calculus.

**THEOREM 8.9 (CONTRACTIBILITY CRITERION).** Given a net $\mathcal{H} + P$, the following assertions are equivalent:

(1) $\mathcal{H} + P$ is contractible and its

(2) $\mathcal{H} + P$ is sequentialisable: there exists a proof $\pi$ in MLL$_2$$^*$ of a sequent $\Gamma$ such that $\mathcal{H} + P$ represents $\pi$,

**PROOF SKETCH.** To show 1 $\Rightarrow$ 2, we start from a contractible net and consider the sequence of rules leading to the final $\star$ rule. We then argue that each reduction rule can be followed in reverse: if the reduct is sequentialisable, then the redex is. Formally, we show that a contractible net is the interpretation of any sequent with the right structure, where the structure describes constraints on the formulas: dependencies on some variables, syntactical structure.

The initial step is straightforward: a net $\star_n$ is the interpretation of the proof of $\vdash A_1, \dots, A_n$ using one daimon rule, for any set of formulas $A_1, \dots, A_n$.

Now, if a net $R$ represent the proof of any sequent $\vdash \Gamma$ with constraints, and $R$ is obtained from $R'$ through a tensor rule constructing a daimon of conclusions $P, A_1, \dots, A_k, B_1, \dots, B_m$, one can then impose the additional structural constraint $P = A \otimes B$ imposing that $P$ has a tensor as principal formula. The rule application furthermore allows to recover dependency constraints from the universal pointers: if $P$ depended on the universal variables $X_1, \dots, X_p$, the rule can be used to redirect those dependencies to $A$ and $B$. Lastly, the rule may have deleted an existential pointer: in

that case, we recover structural constraints as the pointed formula should be equal to the existential witness of the source.

A similar argument can be followed for the parr, universal, and existential rules. We get from the rule application a structural constraint on the formulas involved, as well as information from the pointers.

Lastly, the pointers rule allows to recover the universal dependencies of witnesses, leading to structural constraints; however the redex and the reduct represent the same MLL$_2$ proofs.

**To show 2 $\Rightarrow$ 1,** we proceed by induction on the proof $\pi$, looking at its last rule. Whenever the last rule is daimon rule the implication directly follows. If the last rule is a $\mathcal{R}$- or $\otimes$-rule the induction hypothesis allows us to conclude as in [1].

In the following, we let given a proof $\pi$ in MLL$_2$$^*$ we let $\langle\langle\pi\rangle\rangle$ denote a net which represents $\pi$. If the last rule is the introduction of $\exists$-connective then $S$ is of the form $\langle\langle\pi_0\rangle\rangle + \langle p \Delta_{\exists} q, s \rangle + P_{\exists}(s \rightarrow)$, the new existential link points to the positions which corresponds to the abstracted formula by the quantifier. By induction $\langle\langle\pi_0\rangle\rangle \rightarrow_c \langle\Delta_{\star} \bar{p}, p\rangle$ hence $S \rightarrow \langle\Delta_{\star} \bar{p}, p\rangle + \langle p \Delta_{\exists} q, s \rangle + P_{\exists}(s \rightarrow)$ and the remaining pointers can only be in $P_{\exists}(s \rightarrow)$. Indeed we can perform a contraction step and reduce the net to $\langle\Delta_{\star} \bar{p}, q\rangle$ meaning that $S$ is contractible.

If the last rule is a universal quantification, $S = \langle\langle\pi_0\rangle\rangle + \langle p \Delta_{\forall} q, s \rangle + P_{\vee}(s \rightarrow)$ eventually the new link points to positions of $\langle\langle\pi_0\rangle\rangle$, but since the quantified variable cannot appear in the context the pointers occur above a position which is pointed by an exists link. As a consequence performing the same contraction as for $\langle\langle\pi_0\rangle\rangle \rightarrow \langle\Delta_{\star} \bar{p}, p\rangle$ together with some more rerouting contraction we obtain $S \rightarrow \langle\Delta_{\star} \bar{p}, p\rangle + \langle p \Delta_{\forall} q | + \rangle P_{\vee}(s \rightarrow)$ and the remaining
1393

1394

1395

1396

1397

1398

1399

1400

1401

1402

1403

1404

1405

1406

1407

1408

1409

1410

1411

1412

1413

1414

1415

1416

1417

1418

1419

1420

1421

1422

1423

1424

1425

1426

1427

1428

1429

1430

1431

1432

1433

1434

1435

1436

1437

1438

1439

1440

1441

1442

1443

1444

1445

1446

1447

1448

1449

1450

pointers may only point to *p*, hence the contraction rule be applied
and *S* reduce to ⟨▷★, p̄, q⟩ and so is contractible. ☐

REFERENCES

[1] Pierre-Louis Curien. 2005. Introduction to linear logic and ludics, part II. CoRR abs/cs/0501039 (2005). arXiv:cs/0501039 http://arxiv.org/abs/cs/0501039 1452

[2] Vincent Danos. 1990. *La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du Lambda-calcul)*. Ph. D. Dissertation. http://www.theses.fr/1990PA077188 Thèse de doctorat dirigée par Girard, Jean-Yves Mathématiques Paris 7 1990. 1453

[3] Vincent Danos and Laurent Regnier. 1989. The structure of multiplicatives. *Archive for Mathematical Logic* 28, 3 (01 10 1989), 181–203. https://doi.org/10.1007/BF01622878 1456

[4] Jean-Yves Girard. 1987. Multiplicatives. In *Logic and Computer Science: New Trends and Applications*, G. Lolli (Ed.). Rosenberg & Sellier, 11–34. 1459

[5] Jean-Yves Girard. 1987. Linear logic. *Theoretical Computer Science* 50, 1 (1987), 1–101. https://doi.org/10.1016/0304-3975(87)90045-4 1460

[6] Jean-Yves Girard. 1991. Quantifiers in linear logic II. *Nuovi problemi della logica e della filosofia della scienza* 2 (1991), 1. 1461

[7] Jean-Yves Girard. 2001. Locus Solum: From the Rules of Logic to the Logic of Rules. In *Computer Science Logic*, Laurent Fribourg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 38–38. 1463

[8] Jean-Baptiste Joinet and Thomas Seiller. 2021. From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl's theory of ideal elements. *Kagaku tetsugaku* 53, 2 (2021), 65–93. https://doi.org/10.4216/jpssj.53.2_65 1465

[9] S. C. Kleene. 1945. On the interpretation of intuitionistic number theory. *The Journal of Symbolic Logic* 10, 4 (1945), 109–124. https://doi.org/10.2307/2269016 1467

[10] Jean-Louis Krivine. 2005. Realizability in classical logic. *Panoramas et synthèses* 27 (2005), 197–229. https://hal.science/hal-00154500 1469

[11] Yves Lafont. 1996. The undecidability of second order linear logic without exponentials. *The Journal of Symbolic Logic* 61, 2 (1996), 541–548. https://doi.org/10.2307/2275674 1470

[12] Alexandre Miquel. 2009. De la formalisation des preuves à l'extraction de programmes. *Habilitation at Université Paris Diderot* (2009). https://www.fing.edu.uy/~amiquel/publis/hdr.pdf 1472

[13] Alberto Naibo, Mattia Petrolo, and Thomas Seiller. 2016. *On the Computational Meaning of Axioms*. Springer International Publishing, Cham, 141–184. https://doi.org/10.1007/978-3-319-26506-3_5 1474

[14] Francesca Poggiolesi. 2009. The Method of Tree-hypersequents for Modal Propositional Logic. In *Towards Mathematical Philosophy*, David Makinson, Jacek Malinowski, and Heinrich Wansing (Eds.). Trends in logic, Vol. 28. Springer, 31–51. https://doi.org/10.1007/978-1-4020-9084-4_3 Paper from the Studia Logica conference Trends in Logic IV. 1477

[15] Thomas Seiller. 2012. Interaction Graphs: Multiplicatives. *Annals of Pure and Applied Logic* 163, 12 (2012), 1808–1837. https://doi.org/10.1016/j.apal.2012.04.005 1480

[16] Thomas Seiller. 2013. Interaction Graphs: Exponentials. *Log. Methods Comput. Sci.* 15 (2013). 1481

[17] Thomas Seiller. 2015. Interaction Graphs: Full Linear Logic. CoRR abs/1504.04152 (2015). arXiv:1504.04152 http://arxiv.org/abs/1504.04152 1483

[18] Thomas Seiller. 2016. Interaction Graphs: Additives. *Annals of Pure and Applied Logic* 167, 2 (2016), 95–154. https://doi.org/10.1016/j.apal.2015.10.001 1485

[19] Thomas Seiller. 2017. Interaction Graphs: Graphings. *Annals of Pure and Applied Logic* 168, 2 (2017), 278–320. https://doi.org/10.1016/j.apal.2016.10.007 1487

1451

1452

1453

1454

1455

1456

1457

1458

1459

1460

1461

1462

1463

1464

1465

1466

1467

1468

1469

1470

1471

1472

1473

1474

1475

1476

1477

1478

1479

1480

1481

1482

1483

1484

1485

1486

1487

1488

1489

1490

1491

1492

1493

1494

1495

1496

1497

1498

1499

1500

1501

1502

1503

1504

1505

1506

1507

1508
## CONTENTS

1509

1510

1511

1512

1513

1514

1515

1516

1517

1518

1519

1520

1521

1522

1523

1524

1525

1526

1527

1528

1529

1530

1531

1532

1533

1534

1535

1536

1537

1538

1539

1540

1541

1542

1543

1544

1545

1546

1547

1548

1549

1550

1551

1552

1553

1554

1555

1556

1557

1558

1559

1560

1561

1562

1563

1564

1565

1566

Abstract 1

1 Introduction 1

2 Untyped nets 3

2.1 Directed hypergraph 3

2.2 Sum of hypergraphs 4

2.3 Ordered Hypergraphs 4

2.4 Properties of hypergraphs 5

2.5 Multiplicative nets 5

2.6 Homogeneous cut elimination 5

2.7 Non homogeneous cut elimination 5

3 Realisability model 6

3.1 Interaction of nets 6

3.2 Orthogonality 6

3.3 Construction on Types 7

3.4 Interpretation of formulas 7

4 Adequacy 7

5 Completeness 8

5.1 Test of a formula 8

5.2 Intersection Types and Completeness 8

6 Adequacy at (pre-)second order 9

7 Computability of Types 9

8 Second order nets 10

8.1 Trees, pointers, and approximations 10

8.2 Contractibility criterion 11

References 13

Contents 14

A Second order multiplicative linear logic 14

A.1 Formulas 14

A.2 Sequents and Hypersequents 15

A.3 Proofs 15

B Complements to section 2 15

B.1 Complements to section 2.1 15

B.2 Complements to section 2.2 15

C Complements to section 3 16

C.1 Proofs of section 3.1 16

C.2 Rewriting properties of nets 16

C.3 Proofs of section 3.3 18

D Complements to section 4 19

D.1 Proof Nets 19

D.2 The Merge Operator 19

D.3 Proofs of section 4 20

E Complements to section 5 22

E.1 Proof of Theorem 5.8 – Reformulating Danos Regnier 22

E.2 Correctness of Tests 23

E.3 Decomposition 23

E.4 Contracted, open and self dual Types 24

E.5 Truncation Lemma 24

E.6 Proofs of section 5.2 25

F Complements to section 6 25

G Complements to section 7 26

G.1 Measures of Types 26

G.2 Properties of Intersection and Union 27

G.3 Proofs of Section 7 28

# A SECOND ORDER MULTIPLICATIVE LINEAR LOGIC

1567

1568

1569

1570

1571

1572

1573

1574

1575

1576

1577

1578

1579

1580

1581

1582

1583

1584

1585

1586

1587

1588

1589

1590

1591

1592

1593

1594

1595

1596

1597

1598

1599

1600

1601

1602

1603

1604

1605

1606

1607

1608

1609

1610

1611

1612

1613

1614

1615

1616

1617

1618

1619

1620

1621

1622

1623

1624

We recall the basic notions of formulas and proofs for second order multiplicative linear logic (denoted MLL₂) – and thus also of its sub-fragment; multiplicative linear logic (denoted MLL). We define the notion of hypersequent used for realizers. Furthermore we also give the denition of the proof system MLL* e.g. the multiplicative fragment with generalized axiom.

## A.1 Formulas

We assume that we are given a set of propositional variables $V$ together with an involution $(\cdot)^{\perp}: V \to V: X \mapsto X^{\perp}$ on the propositional variables.

**Definition A.1 (formulas of MLL₂).** The formulas of second order multiplicative linear logic are defined as follows:

$$A, B ::= X, X^{\perp} \mid A \otimes B \mid A \otimes B \mid \forall X A \mid \exists X A$$

The involution $(\cdot)^{\perp}$ is lifted to formulas using de Morgan laws:

$$(A \otimes B)^{\perp} \triangleq A^{\perp} \otimes B^{\perp} \quad (\forall X A)^{\perp} \triangleq \exists X A^{\perp}$$

$$(A \otimes B)^{\perp} \triangleq A^{\perp} \otimes B^{\perp} \quad (\exists X A)^{\perp} \triangleq \forall X A^{\perp}$$

**Remark 34.** The formulas of the multiplicative fragment of linear logic are the formulas of MLL₂ which contain no quantifiers. In other words the formulas generated by the following induction;

$$A, B ::= X, X^{\perp} \mid A \otimes B \mid A \otimes b$$

**Definition A.2 (Substitution).** The substitution of a propositional variable $X$ by a formula $F$ of MLL in a formula $A$ of MLL₂, is denoted $A[X \leftarrow F]$, and is defined inductively:

$$X[X \leftarrow F] \triangleq F$$

$$Y[X \leftarrow F] \triangleq Y$$

$$(A \otimes B)[X \leftarrow F] \triangleq A[X \leftarrow F] \otimes B[X \leftarrow F]$$

$$(A \otimes B)[X \leftarrow F] \triangleq A[X \leftarrow F] \otimes B[X \leftarrow F]$$

$$(\forall X A)[X \leftarrow F] \triangleq \forall X A$$

$$(\forall Y A)[X \leftarrow F] \triangleq \forall Y A[X \leftarrow F]$$

$$(\exists X A)[X \leftarrow F] \triangleq \exists X A$$

$$(\exists Y A)[X \leftarrow F] \triangleq \exists Y A[X \leftarrow F]$$

Where $Y$ is a propositional variable that is distinct from $X$, i.e. $X \neq Y$.

**PROPOSITION A.3 (SUBSTITUTION AND NEGATION COMMUTE).** Given $A$ and $F$ two formulas respectively from MLL₂ and MLL, together with $X$ a propositional variable.

$$A[X \leftarrow F]^{\perp} = A^{\perp}[X \leftarrow F]$$

**Definition A.4.** The universally (resp. existentially) bounded variables of a MLL₂ formula is given by induction;

$$U(X) \triangleq \emptyset \qquad E(X) \triangleq \emptyset$$

$$U(A \otimes B) \triangleq U(A) \cup U(B) \qquad E(A \otimes B) \triangleq E(A) \cup E(B)$$

$$U(A \otimes B) \triangleq U(A) \cup U(B) \qquad E(A \otimes B) \triangleq E(A) \cup E(B)$$

$$U(\forall X A) \triangleq U(A) \cup \{X\} \qquad E(\forall X A) \triangleq E(A)$$

$$U(\exists X A) \triangleq U(A) \qquad E(\exists X A) \triangleq E(A) \cup \{X\}$$

A propositional variable is *bounded* in a formula $F$ whenever it's universally or existentially bounded in $F$.
**Definition A.5 (α-equivalence).** Two formulas of MLL₂ are α-equivalent which we denote $F \equiv_\alpha G$ if they have the same main connective and satisfy one of the inductive cases:

$$
\begin{align*}
& X \equiv_\alpha Y \quad \Leftrightarrow \quad X = Y \text{ or } X = Y^\perp \\
& A \not\sim B \equiv_\alpha A' \not\sim B' \quad \Leftrightarrow \quad A \equiv_\alpha A' \text{ and } B \equiv_\alpha B' \\
& A \otimes B \equiv_\alpha A' \otimes B' \quad \Leftrightarrow \quad A \equiv_\alpha A' \text{ and } B \equiv_\alpha B' \\
& \forall X A \equiv_\alpha \forall Y A' \quad \Leftrightarrow \quad A \equiv_\alpha A' [Y \leftarrow X] \\
& \exists X A \equiv_\alpha \exists Y A' \quad \Leftrightarrow \quad A \equiv_\alpha A' [Y \leftarrow X]
\end{align*}
$$

**Remark 35.** formulas of the second order multiplicative fragment of linear logic are consider modulo α-equivalence, in order to avoid that a formula occurs both free and bounded in a same formula. Any formula *F* containing variables that are simultaneously bounded and free is α-equivalent to a formula where variables cannot be both free and bounded. Intuitively this is because α-equivalence allows to rename bounded variables occuring in *F* by any other propositional variables, thus we may chose a propositional variable that does not occur yet in *F*.

For instance in the formula $F \triangleq X \not\sim \exists X.X^\perp$ the propositional variable $X$ occurs both free and bounded but $F$ is $\alpha$-equivalent to $X \not\sim \exists Y.Y$. Indeed $\exists X.X^\perp$ and $\exists Y.Y$ are $\alpha$-equivalent since $X^\perp$ and $Y[Y \leftarrow X] = X$ are by definition $\alpha$-equivalent.

**Remark 36.** By working modulo $\alpha$-equivalence we can assume that propositional variables cannot be simultaneously universally and existentially bounded. This is because we may rename any bounded propositional variable with a fresh propositional variable, in particular, this implies that distinct quantifiers can always bind distinct propositional variables.

## A.2 Sequents and Hypersequents

**Definition A.6 (hypersequent).** A hypersequent $\mathcal{H}$ of MLL₂ formulas (resp. MLL) is an inductively defined structure as follows;

$$ \mathcal{H}_1, \mathcal{H}_2 ::= A \mid \mathcal{H}_1, \mathcal{H}_2 \mid \mathcal{H}_1 \parallel \mathcal{H}_2 $$

Where $A$ is any formula of MLL₂ (resp. MLL).

**Remark 37.** Note that the hypersequents we consider in that work are not only of the form $\Gamma_1 || \dots || \Gamma_n$ where each $\Gamma_i$ is a sequent. For instance, $A, (B \parallel C)$ is a possible hypersequent.

**Definition A.7 (Sequent).** A sequent is a multiset of formula i.e. a map $\Gamma : \mathcal{F}_{\text{MLL}} \to \mathbb{N}$ of finite support. The *representant* of a sequent $\Gamma$ is a sequence of MLL formulas $\gamma : (A_1, \dots, A_n)$ such that

$$ \Gamma = \bar{\gamma} : A \mapsto \text{card}\{1 \le i \le n \mid A_i = A\}. $$

Given $\Gamma = (A_1, \dots, A_n)$ the *representant* of a sequent we denote by $\Gamma(i)$ the formula $A_i$. The *size* of a sequent $\Gamma$ denoted $|\Gamma|$ is the number of formulas it contains, e.g. the length of its *representants* (as sequences of formulas).

**Remark 38.** We will use the notion of sequent loosely, implicitly, a sequent will be given by one of its *representant* e.g. a sequence a formulas.

**Definition A.8 (Flattening of an hypersequent).** The *flattening* of an hypersequent, denoted $\downarrow \mathcal{H}$, is defined inductively;

$$
\begin{align*}
\downarrow A &\triangleq A. \\
\downarrow (\mathcal{H}_1, \mathcal{H}_2) &\triangleq \downarrow \mathcal{H}_1, \downarrow \mathcal{H}_2. \\
\downarrow (\mathcal{H}_1 \parallel \mathcal{H}_2) &\triangleq \downarrow \mathcal{H}_1, \downarrow \mathcal{H}_2.
\end{align*}
$$

## A.3 Proofs

**Definition A.9.** A proof in MLL₂ of a sequent $\Gamma$ of formulas in MLL₂ is a tree of root $\Gamma$ constructed by the following rules;

$$
\begin{array}{c}
\frac{\Gamma, A \ \Delta, A^{\perp}}{A, A^{\perp} \ \alpha x} \quad \frac{\Gamma, A \ \Delta, A^{\perp}}{\Gamma, \Delta} \ \text{cut} \quad \frac{\Gamma, A \ \Delta, B}{\Gamma, \Delta, A \otimes B} \otimes \quad \frac{\Gamma, A, B}{\Gamma, A \not\sim B} \not\sim \\
\frac{\Gamma, A}{\Gamma, \exists X A} \quad \exists \quad \frac{\Gamma, A}{\Gamma, \forall X A} \quad \forall \\
\frac{\Gamma, A \ \Delta, A^{\perp}}{\Gamma, \Delta} \quad \frac{\Gamma, A \ \Delta, B}{\Gamma, \Delta, A \otimes B} \otimes \quad \frac{\Gamma, A, B}{\Gamma, A \not\sim B} \not\sim \frac{\Gamma, A, B, \Delta}{\Gamma, B, A, \Delta} \frac{\Delta}{\Gamma, B, A, \Delta} \ \text{ex}
\end{array}
$$

The universal quantifier rule ($\forall$) can only be applied whenever $X$ does not occur free in $\Gamma$.

**Remark 39.** The proofs of MLL are the trees constructed only using the first rows.

**Definition A.10.** A proof in MLL$^{\star}$ of a sequent $\Gamma$ of formulas in MLL$^{\star}$ is a tree of root $\Gamma$ constructed by the following rules;

$$
\frac{\Gamma, A \ \Delta, A^{\perp}}{\Gamma^{\star}} \quad \frac{\Gamma, A \ \Delta, B}{\Gamma, \Delta, A \otimes B} \otimes \quad \frac{\Gamma, A, B}{\Gamma, A \not\sim B} \not\sim \frac{\Gamma, A, B, \Delta^{\star}}{\Gamma, B, A, \Delta^{\star}} \frac{\Delta^{\star}}{\Gamma^{\star}} \text{ex}
$$

The daimon rule ($\star$) can introduce any kind of sequent.

**Remark 40.** The proofs of MLL are the trees constructed using only the first row of the definition A.9. Equivalently they are proofs of MLL$^{\star}$ such that the daimon rule introduces only sequents of the form $A, A^{\perp}$.

**Remark 41.** The presence of the exchange rule is equivalent to assuming that each of the rule may be applied to any of the formulas in the sequents – not necessarily only to the last or first formulas.

# B COMPLEMENTS TO SECTION 2

## B.1 Complements to section 2.1

We recall the notion of homomorphism and isomorphism between hypergraphs.

**Definition B.1 (Homomorphism and isomorphisms of hypergraphs).**

An homomorphism between two (labelled) hypergraphs $\mathcal{H}_1 = (V_1, E_1, s_1, t_1, \ell_1)$ and $\mathcal{H}_2 = (V_2, E_2, s_2, t_2, \ell_2)$ is a pair of bijective maps $\langle f^V, f^E \rangle$, such that

* (COMMUTATION) For any edge $e_1$ of $\mathcal{H}_1, s_2(f^E(e_1)) = f^V(s_1(e_1))$,

i.e. the following diagram commutes:

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

* (LABEL-PRESERVING) The function $f^E$ preserves the labels

of the links, i.e. for any link $e$ in $\mathcal{H}_1; \ell(e) = \ell(f^E(e))$

The homomorphism is an isomorphism if both $f^V$ and $f^E$ are bijective.

## B.2 Complements to section 2.2

In that section we recall how multiplicative nets (e.g. multiplicative proof structures using the original terminology from [5]) may be defined inductively.

**PROPOSITION B.2.** An ordered hypergraph is a multiplicative net if and only if it belongs to the following inductively defined set: Net:
• $(\langle \Delta_{\otimes} p_1, \dots, p_n \rangle, p_1 < \dots < p_n)$ belongs to Net.

• If $(S, a)$ belongs to Net with $a = (p_1, \dots, p_n)$ then for any $i \in \{1, \dots, n-1\}$ and fresh position $p$, $(S + \langle p_i, p_{i+1} \Delta \otimes p \rangle, a')$ and $(S + \langle p_i, p_{i+1} \Delta \otimes p \rangle, a')$ belong to Net, where $a' = a[i \leftarrow p, i+1 \leftarrow \epsilon]$.

• If $(S, a)$ belongs to Net with $a = (p_1, \dots, p_n)$ then for any $i \in \{1, \dots, n-1\}$, $(S + \langle p_i, p_{i+1} \Delta_{\text{cut}} \rangle, a')$ belongs to Net, where $a' = a[i \leftarrow \epsilon, i \leftarrow \epsilon]$.

• If $(S, a)$ belongs to Net with $a = (p_1, \dots, p_n)$, then for any $i \in \{1, \dots, n-1\}$ the net $(S, a')$ belongs to Net, where $a' = a[i \leftarrow p_{i+1}, i+1 \leftarrow p_i]$.

• If $(S_1, a)$ and $(S_2, b)$ belong to Net and have disjoint positions i.e. $V_1 \cap V_2 = \emptyset$. then their sum $(S_1 + S_2, a \cdot b)$ belongs to Net.

PROOF. $1 \Rightarrow 2$. Assume that $(S, a)$ is a multiplicative net and we want to show it belongs to Net. To do so we will operate by induction on the number of links in $S$.

- If $S$ has only one link, since $S$ is surjective all its position must be the target of some link. Thus $S$ can only be of the form $\langle \Delta_{\otimes} p_1, \dots, p_n \rangle$, the order $a$ may then be any total order on $p_1, \dots, p_n$.

By definition $(S, a_0)$ is in Net when $a_0 = (p_1, \dots, p_n)$. Then by doing exchanges we can rearrange the sequence $a_0$ into any sequence on $\{p_1, \dots, p_n\}$ in particular in $a$. Since Net is stable under this operation, this concludes that $(S, a)$ is in Net.

- $S$ may be a sum of daimons, again the previous argument will work.

- $S$ may contain a terminal binary link such as $l_1 ::= \langle p_1, p_2 \Delta \otimes p \rangle$ or $l_2 ::= \langle p_1, p_2 \Delta \otimes p \rangle$ or $l_3 ::= \langle p_1, p_2 \Delta_{\text{cut}} \rangle$. Thus $S$ is of the form $S' + l_i$, and in that case $S'$ has conclusions $p_1, p_2, q_1, \dots, q_k$. The order on the conclusion of $S'$ may be any. We can call the induction hypothesis on $S'$ and claim that $(S', a')$ belong to Net. Then $(S, a'[p_1 \leftarrow p, p_2 \leftarrow \epsilon])$ (the case for cut is similar) is by construction still in the class. Note that $a'[p_1 \leftarrow p, p_2 \leftarrow \epsilon]$ is made of the conclusions of $S$ thus after a series of exchange it can be reorganized as any sequence $a$ on the conclusion of $S$, so we can conclude.

2 $\Rightarrow$ 1. We will do so by the induction given by the definition of Net.

- If $S$ is daimon $\langle \Delta_{\otimes} p_1, \dots, p_n \rangle$ with the order $(p_1, \dots, p_n)$ It is surjective, affine and linear so indeed it is a multiplicative net.

- If $S_1$ and $S_2$ are two affine linear are surjective nets, note that their disjoint sum (i.e. we assume $V_1 \cap V_2 = \emptyset$) will still be surjective affine and linear.

- If we assume that $(S, a)$ is a multiplicative net then performing an exchange will still make it a multiplicative net.

- If we add one terminal link to $S$ note that surjectivity is preserved because the added position $p$ belongs to the target of the new link. Furthermore linearity is preserved because the position of $S$ don't become the target of any new link. Then affine property is preserved because the points that now belong to a new source where conclusions in $S$, thus it still true that any position belongs to at most the source of one link.

# C COMPLEMENTS TO SECTION 3

## C.1 Proofs of section 3.1

Definition C.1 (Functional and injective relation). A binary relation between two sets $A$ and $B$ is a subset of $A \times B$. A binary relation $\mathcal{R} \subset A \times B$ is

• functional whenever for any $(a, b) \in \mathcal{R}$ there is no other pair $(a, b')$ with $b \neq b'$ that belongs to $\mathcal{R}$.

• injective whenever for any $(a, b) \in \mathcal{R}$ there is no other pair $(a', b)$ with $q \neq q'$ that belongs to $\mathcal{R}$.

A relation $\mathcal{R}$ is defined on an element $a \in A$ whenever there exists $b \in B$ such that $(a, b) \text{ belongs to } \mathcal{R}$.

Remark 42. Equivalently to the definition 3.1 an interface between two nets $S$ and $T$ of respective conclusions $p_1, \dots, p_n$ and $q_1, \dots, q_k$. as partial injective maps $\sigma : \{p_1, \dots, p_n\} \to \{q_1, \dots, q_k\}$. However the notion of map is highly asymmetrical thus we cannot express easily the property of commutativity without mentioning the inverse of the map $\sigma$.

On the other hand, working with the previous definition, given $S$ and $T$ two nets and $\sigma$ an interface between $S$ and $T$, the interaction along $\sigma$ is a commutative operation, e.g. $S \coloneqq_{\sigma} T$ is equal to $T \coloneqq_{\sigma} R$.

PROPOSITION 3.2 (INTERACTION AS AN ACTION). Given $S, T$ and $R$ three multiplicative nets, and $\sigma$ an interface between $S$ and $T \parallel R$. $S \coloneqq_{\sigma} (T \parallel R)$ is equal to $(S \coloneqq_{\sigma|T} R) \coloneqq_{\sigma|R} R$.

PROOF. of proposition 3.2. First simply unfold the definition;

$$S \coloneqq_{\sigma} (T + R) \triangleq S + T + R \sum_{(p,q) \in \sigma} \langle p, q \Delta_{\text{cut}} \rangle.$$

Now note that the interface $\sigma$ is partitioned in two sets, the positions that are related to conclusions of $R$ and the positions that are related to conclusions of $T$. Thus the sum can be rewritten as:

$$\sum_{(p,q) \in \sigma} \langle p, q \Delta_{\text{cut}} \rangle = \sum_{(p,q) \in \sigma | T} \langle p, q \Delta_{\text{cut}} \rangle + \sum_{(p,q) \in \sigma | R} \langle p, q \Delta_{\text{cut}} \rangle.$$

Hence since the sum is commutative and associative the interaction $S \coloneqq_{\sigma} (T + R)$ is equal to the following,

$$S + \sum_{(p,q) \in \sigma | T} \langle p, q \Delta_{\text{cut}} \rangle + T + \sum_{(p,q) \in \sigma | R} \langle p, q \Delta_{\text{cut}} \rangle + R.$$

The first part of this expression corresponds to $S \coloneqq_{\sigma|T} T$. To conclude note that since $\sigma | R$ relates conclusions of $S$ to conclusion of $R$ and since out$(S \coloneqq_{\sigma|T} T)$ contains out$(R)$, it follows that $\sigma | R$ is an interface between $S \coloneqq_{\sigma|T} T$ and $R$. Thus $S \coloneqq_{\sigma} (T + R)$ is equal to $S \coloneqq_{\sigma|T} T \coloneqq_{\sigma|R}$.

## C.2 Rewriting properties of nets

PROPOSITION C.2 (NON-DETERMINISTIC NON HOMOGENEOUS CUT ELIMINATION COMMUTES TO THE RIGHT). Given $S$ some net containing a non homogeneous cut link $c$ of a daimon link against a $\mathcal{R}$-link. The diagram below commutes, for any cut kind of cut link $c'$;

$$\begin{tikzcd}
S \arrow[r, "c"] \arrow[d, "c'"'] & S_1 \arrow[d, "c"] \\
S'_1 - \arrow[r, "-c"] & S_2
\end{tikzcd}$$

1799

1800

1801

1802

1803

1804

1805

1806

1807

1808

1809

1810

1811

1812

1813

1814

1815

1816

1817

1818

1819

1820

1821

1822

1823

1824

1825

1826

1827

1828

1829

1830

1831

1832

1833

1834

1835

1836

1837

1838

1839

1840

1841

1842

1843

1844

1845

1846

1847

1848

1849

1850

1851

1852

1853

1854

1855

1856
Where the dotted arrows are the existence of a reduction.

PROOF. First note that the commutation of the cut elimination steps always hold whenever the two cuts involve a different part of the net. Furthermore if $c'$ is a multiplicative cut the commutation holds. Thus $c'$ is a glueing or non homogeneous cut involving the same daimon link as c. Let us treat each cases;

* In the first case, in all generality the reduction will be of the form:

$$ 
\begin{align*}
\langle\Delta\otimes p_1, \dots, p_n\rangle &+ \langle r_1, r_2 \Delta\nabla r\rangle + \langle\Delta\otimes q_1, \dots, q_k\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q_1 \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, p_2, A\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle\Delta\otimes q_1, \dots, q_k\rangle + \langle p_1^1, r_2 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, q_1, \dots, q_k, A\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle p_1^1, r_2 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle
\end{align*}
$$

By consistently choosing the partition during the elimination of the cut c this can be matched by first starting with the elimination of the glueing cut $c'$.

$$ 
\begin{align*}
\langle\Delta\otimes p_1, \dots, p_n\rangle &+ \langle r_1, r_2 \Delta\nabla r\rangle + \langle\Delta\otimes q_1, \dots, q_k\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q_1 \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1, q_1, \dots, q_k, \dots, p_n\rangle + \langle r_1, r_2 \Delta\nabla r\rangle + \langle p_1, r \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, q_1, \dots, q_k, A\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle
\end{align*}
$$

* In the first non homogeneous case the redex is of the following form:

$$ \langle\Delta\otimes p_1, \dots, p_n\rangle + \langle r_1, r_2 \Delta\nabla r\rangle + \langle q_1, q_2 \Delta\otimes q\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q \Delta\text{cut}\rangle. $$

After one step of cut elimination this becomes in all generality, given that $A = \{a_1, \dots, a_k\}$ and $B = \{b_1, \dots, b_l\}$ partition $p_2, \dots, p_n$,

$$ \langle\Delta\otimes p_1^1, p_2, A'\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle q_1, q_2 \Delta\otimes q\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle $$

Without loss of generality assume that $p_2$ occurs in the class $A = \{p_2\} \cup A'$, then after one step of cut elimination this becomes;

$$ \langle\Delta\otimes p_1^1, p_2^1, p_2^2, A'\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle + \langle p_2^1, q_1 \Delta\text{cut}\rangle + \langle p_2^2, q_2 \Delta\text{cut}\rangle. $$

Indeed one can obtain the same redex by first eliminating $c'$, when eliminating the $\mathfrak{Z}$-link we need to make a consistent choice e.g. the partition of $p_1^2, p_2^2, \dots, p_n$ made of the two classes $B$ and $A' \cup \{p_1^2, p_2^2\}$:

$$ 
\begin{align*}
\langle\Delta\otimes p_1, \dots, p_n\rangle &+ \langle r_1, r_2 \Delta\nabla r\rangle + \langle q_1, q_2 \Delta\otimes q\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1, p_2^1, p_2^2, \dots, p_n\rangle + \langle r_1, r_2 \Delta\nabla r\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2^1, q_1 \Delta\text{cut}\rangle + \langle p_2^2, q_2 \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, p_2^1, p_2^2, A'\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle + \langle p_2^1, q_1 \Delta\text{cut}\rangle + \langle p_2^2, q_2 \Delta\text{cut}\rangle \\
\rightarrow & S'_{1} - c \rightarrow S_2 \\
\rightarrow & S'_{2} - c \rightarrow S_3
\end{align*}
$$

* In the non homogeneous second case both cuts are made of $\mathfrak{Z}$-links against a daimon thus in all generality a reduction is of the following form form;

$$ 
\begin{align*}
\langle\Delta\otimes p_1, \dots, p_n\rangle &+ \langle r_1, r_2 \Delta\nabla r\rangle + \langle q_1, q_2 \Delta\nabla q\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, p_2, A\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle q_1, q_2 \Delta\nabla q\rangle + \langle p_2, q \Delta\text{cut}\rangle + \langle p_1^1, A'\rangle + \langle p_1^2, A'\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, p_2^1, A_1\rangle + \langle\Delta\otimes p_2^1, A_2\rangle + \langle\Delta\otimes p_1^2, B\rangle + \langle p_2^1, q_1 \Delta\text{cut}\rangle + \langle p_2^2, q_2 \Delta\text{cut}\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_1^2, r_2 \Delta\text{cut}\rangle
\end{align*}
$$

Indeed starting by eliminating the cut $c'$ we can obtain the same redex by making consistent choices in the partitions:

$$ 
\begin{align*}
\langle\Delta\otimes p_1, \dots, p_n\rangle &+ \langle r_1, r_2 \Delta\nabla r\rangle + \langle q_1, q_2 \Delta\nabla q\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2, q \Delta\text{cut}\rangle \\
\rightarrow & \langle\Delta\otimes p_1^1, p_2, A_1 \cup B\rangle + \langle\Delta\otimes p_1^2, A_2\rangle + \langle r_1, r_2 \Delta\nabla r\rangle + \langle p_1, r \Delta\text{cut}\rangle + \langle p_2^1, q_1 \Delta\text{cut}\rangle + \langle p_2^2, q_2 \Delta\text{cut}\rangle + \langle p_1^1, r_1 \Delta\text{cut}\rangle + \langle p_2^1, r_2 \Delta\text{cut}\rangle \\
\rightarrow & S'_{1} - c \rightarrow S_2 \\
\rightarrow & S'_{2} - c \rightarrow S_3
\end{align*}
$$

PROPOSITION C.3 (DETERMINISTIC NON HOMOGENEOUS CUT ELIMINATION COMMUTES TO THE LEFT). Given $S$ some net containing a non homogeneous cut link $c$ of a daimon link against a $\otimes$-link. The diagram below commutes, for any cut kind of cut link $c'$;

$$ 
\begin{array}{ccc}
S & \xrightarrow{c'} & S_1 \\
\downarrow & & \downarrow \\
S'_{1} & -c' & S_2
\end{array}
$$

Where the dotted arrows are the existence of a reduction.

We reason as in the proof for proposition C.2, if the two cuts involved different link of the net we conclude. Furthermore if $c'$ is an homogeneous cut the proposition hold. Thus we assume that $c$ and $c'$ are both non-homogeneous and involve the same daimon link.

* If $c'$ is also a tensor link its clear that the elimination of the two cuts commute.

* If $c'$ is a $\mathfrak{Z}$-link we can call the previous proposition C.2 on the cut $c'$, claiming that its elimination commutes on the right with any step of cut elimination. In particular any elimination of $c'$ followed by any elimination of $c$ can be matched by an elimination of $c$ followed by an elimination of $c'$. Thus we conclude.

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

PROPOSITION C.4 (GENERAL RIGHT COMMUTATION). For any net $S$ containing an irreversible cut $c$, and given $\alpha^*$ a series of cut elimination

$$ 
\begin{array}{ccc}
S & \xrightarrow{c} & S_1 \\
\downarrow & & \downarrow \\
S'_{1} & -c & S_2
\end{array}
$$

PROOF. This follows from a simple induction on $\alpha^*$. If $\alpha^*$ is made of only one cut the proposition C.2 gets us the conclusion. Otherwise we decompose the sequence of reductions as $\alpha^* = \beta \cdot \beta^*$ and by applying the proposition C.2 we obtain the following diagram.

1915

1916

1917

1918

1919

1920

1921

1922

1923

1924

1925

1926

1927

1928

1929

1930

1931

1932

1933

1934

1935

1936

1937

1938

1939

1940

1941

1942

1943

1944

1945

1946

1947

1948

1949

1950

1951

1952

1953

1954

1955

1956

1957

1958

1959

1960

1961

1962

1963

1964

1965

1966

1967

1968

1969

1970

1971

1972
1973

1974

1975

1976

1977

1978

1979

1980

1981

1982

1983

1984

1985

1986

1987

1988

1989

1990

1991

1992

1993

1994

1995

1996

1997

1998

1999

2000

2001

2002

2003

2004

2005

2006

2007

2008

2009

2010

2011

2012

2013

2014

2015

2016

2017

2018

2019

2020

2021

2022

2023

2024

2025

2026

2027

2028

2029

2030

□

**Remark 43.** Moreover, following a similar method, we can easily establish that multiplicative glueing and clashing cuts commute to the left with any kind of cut.

This means that whenever two net $S$ and $T$ are orthogonal and a reversible cut $c$ occurs in $S :: T$ we can chose to start the reduction the reduction $S :: T \to (\Delta_{\otimes})$ by eliminating $c$. Thus the redex $R$ of $S :: T$ obtained after eliminating $c$ still verifies that $R \to (\Delta_{\otimes})$.

**PROPOSITION C.5 (GENERAL LEFT COMMUTATION).** For any net $S$ containing a reversible cut $c$, and given $\alpha^*$ a series of cut elimination of cuts occuring in $S$ then the following diagram commutes;

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

**PROOF.** As for the previous proposition it follows from a simple induction on $\alpha^*$. If $\alpha^*$ is made of only one cut the proposition C.3 gets us to conclude. Otherwise we decompose the sequence of reductions as $\alpha^* = \beta^* \cdot \beta$ and by applying the proposition C.3 together with the induction hypothesis we obtain the following diagram.

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

□

**Definition C.6 (Simulation).** A net $S$ simulates a net $T$, if for any reduction $T \to R$ there exists a reduction $S \to^* R$. We denote this by $S > T$.

Two nets $S$ and $T$ are *bisimilar* whenever $S > T$ and $T > S$.

A matching of two nets $S$ and $T$ is a pair $(p, q)$ of a conclusion of $S$ and a conclusion of $T$. A net $S$ simulates a net $T$ in a matching $(p, q)$ for a link $l = \langle t_1, \dots, t_n \Delta_l q_1, \dots, q_k \rangle$ whenever there exists a conclusion $q_i$ such that $S \coloneqq p, q_i$ $l$ simulates $T \coloneqq p, q_i$ $l$. We denote $S >^{p,q}_l T$.

**PROPOSITION C.7 (STANDARD SIMULATION).** The following simulations hold;

* $\langle \Delta_{\otimes} \vec{p}, p_1, p_2 \rangle + \langle p_1, p_2 \Delta_{\otimes} p \rangle \sim_{\otimes, \Delta_{\otimes}}^{p,q} \langle \Delta_{\otimes} \vec{p}, q \rangle$.

* $\langle \Delta_{\otimes} \overline{p_1, p_1} \rangle + \langle \Delta_{\otimes} \overline{p_2, p_2} \rangle + \langle p_1, p_2 \Delta_{\otimes} p \rangle \sim_{\Delta_{\otimes}}^{p,q} \langle \Delta_{\otimes} \overline{p_1, p_2, q} \rangle$.

* $\langle \Delta_{\otimes} \overline{p_1, p_1} \rangle + \langle \Delta_{\otimes} \overline{p_2, p_2} \rangle + \langle p_1, p_2 \Delta_{\otimes} p \rangle <_{\Delta_{\otimes}}^{p,q} \langle \Delta_{\otimes} \overline{p_1, p_2, q} \rangle$.

### C.3 Proofs of section 3.3

**PROPOSITION 3.6 (SYMMETRY OF TYPES).** For any type $A$ with one conclusion; (1) there exists a net $S$ with a terminal $\mathfrak{2}\mathfrak{3}$-link that belongs to $A$ or $A^{\perp}$, and (2) there exists a net $S$ with a terminal $\otimes$-link that belongs to $A$ or $A^{\perp}$.

**PROOF.** of proposition 3.6. First let us note that there cannot be only nets with daimon conclusion in $A \cup A^{\perp}$.

Assume that it is the case. Then $S :: S'$ reduces to $\langle \Delta_{\otimes} \rangle$. The redex corresponding to the glueing cut can be made into a multiplicative one.

Thus one of the two assertions must hold. To conclude we will show that they are equivalent.

1. Assume that some net $S$ exists with a terminal $\otimes$ belongs to say $A$ without loss of generality. If a net with a terminal $\mathfrak{2}\mathfrak{3}$ belongs to $A$ we can conclude. Assume otherwise e.g. only nets with terminal tensor link or daimon link belong to $A$.

Assume in order to reach a contradiction, that only net with terminal daimon link occur in $A^{\perp}$,

Let $R$ be a net of $A^{\perp}$, e.g. for any net $S$ in $A$ the interaction $S :: R$ reduces to $\langle \Delta_{\otimes} \rangle$. Consider $T = R + \langle p_1, p_2 \Delta_{\otimes} p \rangle$ where the position $p$ the conclusion of $R$, has been dupplicated, and connected to the same daimon link.

The successful $S :: R \to \langle \Delta_{\otimes} \rangle$ reduction needs at some point to eliminate the reversible cut $c$. But proposition C.3 ensure that the elimination of reversible cuts commutes on the left; thus the successful reduction may be rearranged as $S :: R \to S' :: R' \to \langle \Delta_{\otimes} \rangle$. where $S' :: R'$ is the redex obtained after eliminating the reversible cut $c$ in $S :: R$.

Note that $S :: T$ also reduces to $S' :: R'$ after eliminating the reversible cut $c$, hence it reduces to $\langle \Delta_{\otimes} \rangle$. This shows that $S \perp T$ for any $A$ meaning $T$ is in $A^{\perp}$.

2. Assume that some net $S$ exists in with a terminal $\mathfrak{2}\mathfrak{3}$ belongs to, say $A$ without loss of generality. Again we assume that in $A^{\perp}$ only nets with a terminal daimon link exists. Let $R$ be some net in $A^{\perp}$ then consider $T = R + \langle \Delta_{\otimes} p_1 \rangle + \langle \Delta_{\otimes} p_2, \overline{p_1} \rangle + \langle p_1, p_2 \Delta_{\otimes} p \rangle$ where $p$ the conclusion of $R$ has been dupplicated and connected to distinct daimon links.

For any net $S$ belonging to $A$ with a terminal $\mathfrak{2}\mathfrak{3}$ link since the irreversible cuts commute to the right the interaction $S :: R$ may reduce to $\langle \Delta_{\otimes} \rangle$ by eliminating the irreversible cut $c$ as late as possible. In particular after eliminating the cuts with the sequence $\alpha^*$ it becomes $S' + R' + \text{red}$, where $S' \text{ and } R'$ are cut free and the redex with the irreversible cut only remain. Hence $S' + R' + \text{red} \to \langle \Delta_{\otimes} \rangle$.

Furthermore by eliminating the cuts as in the sequence $\alpha^*$ the interaction $S :: T$ reduces to $S' :: R' :: \text{red}_1$. The redexes $\text{red}_1$ can match the reduction of the redex red hence if $S' :: R' + \text{red}$ reduce to $\langle \Delta_{\otimes} \rangle$ then so does $S :: R + \text{red}_1$. As a consequence if $S$ is orthogonal to $R$ then $S$ is also orthogonal to $T$. We conclude that $T$ belongs to $A^{\perp}$. □

**PROPOSITION 3.8 (DUALITY).** Given two types $A$ and $B$: $(A \parallel B)^{\perp} = A^{\perp} \succ B^{\perp}$ and $(A \succ B)^{\perp} = A^{\perp} \parallel B^{\perp}$.

**PROOF.** of proposition 3.8 Consider a net $S$ orthogonal to $A \parallel B$ then for any $a$ in $A$ and $b$ in $B$ the interaction $S :: (a \parallel b)$ reduces to $\mathfrak{A}_0$.

Since $S :: (a \parallel b)$ is equal to $S :: a :: b$ and that the orthogonality hold for any pair $(a, b)$, in particular for any net $b$ in $B$ the interaction $(S :: a) :: b$ reduce to $\mathfrak{A}_0$. This means that $S :: a$ is orthogonal to $B$ hence for any $a$ in $A$ the interaction $S :: a$ belongs to $B^{\perp}$. Since $A = (A^{\perp})^{\perp}$ By definition this means $S$ belongs to $A^{\perp} \succ B^{\perp}$.

On the other consider a net $S$ in $A^{\perp} \succ B^{\perp}$ is such that for any $a$ in $A = (A^{\perp})^{\perp}$ the interaction $S :: a$ belongs to $B^{\perp}$ e.g. is orthogonal to $B$ and so for any $b$ in $B$ the interaction $S :: a :: b$ reduce to $\mathfrak{A}_0$.

2031

2032

2033

2034

2035

2036

2037

2038

2039

2040

2041

2042

2043

2044

2045

2046

2047

2048

2049

2050

2051

2052

2053

2054

2055

2056

2057

2058

2059

2060

2061

2062

2063

2064

2065

2066

2067

2068

2069

2070

2071

2072

2073

2074

2075

2076

2077

2078

2079

2080

2081

2082

2083

2084

2085

2086

2087

2088
2205

**PROPOSITION D.3.** Given $S$ and $T$ two orthogonal nets then $S \bowtie \mathfrak{X}_1 :: T$ reduces to $\mathfrak{X}_1$.

2206

2207

2208

2209

2210

2211

2212

2213

2214

2215

2216

2217

2218

2219

2220

2221

2222

2223

2224

2225

2226

2227

2228

2229

2230

2231

2232

2233

2234

2235

2236

2237

2238

2239

2240

2241

2242

2243

2244

2245

2246

2247

2248

2249

2250

2251

2252

2253

2254

2255

2256

2257

2258

2259

2260

2261

2262

* The cases $(0, i)$ are straightforward. Only glueing cuts occur and these cuts commute to the left. Furthermore, eliminating a glueing cut decreases the size of the net.

* For the cases $(c, i)$ make the number of connectives decrease by performing a step of cut elimination, in particular three cases occurs corresponding to the possible cut eliminated, $(\mathfrak{X}/\otimes)$, $(\mathfrak{Y}/\mathfrak{X})$ or $(\otimes/\mathfrak{X})$. We will treat only the cases where the connective occurs in $S$; it is easy to adapt the following proof for the case when the connectives occurs in $T$.

- Say that $S :: T$ occurs a multiplicative cut thus the two nets may be written as $S_0 + \alpha :: T_0 + \beta$ where $\alpha$ is the $\mathfrak{Y}$ link and $\beta$ the $\otimes$ link. Since multiplicative cut commutes to the left and since $S :: T$ reduces to $\langle\Delta_{\mathfrak{X}}\rangle$ we can ensure that the multiplicative redex $S_0 :: T_0$ reduces also to $\langle\Delta_{\mathfrak{X}}\rangle$ e.g. $S_0$ and $T_0$ are orthogonal. Furthermore note that $S_0+\alpha \bowtie \mathfrak{X}_1 :: T_0+\beta$ corresponds to $S_0 \bowtie \mathfrak{X}_1 + \alpha :: T_0 + \beta$ and so after a step of cut elimination reduces to $S_0 \bowtie \mathfrak{X}_1 :: T_0$. Since $S_0 \perp T_0$ and that the number of connectives as decreased, we can apply the induction hypothesis and ensure that $S_0 \bowtie \mathfrak{X}_1 :: T_0$ reduces to $\mathfrak{X}_1$ hence it is also true for $S \bowtie \mathfrak{X}_1 :: T$.

- Say that a non-homogeneous cut $(\mathfrak{X}/\mathfrak{Y})$ occurs in the interaction of $S :: T$ and assume the tensor link occurs in $S$. Then the interaction can be written as $S_0 + \alpha :: T$ after eliminating that reversible cut we obtain the ent $S_0 :: T'$ where $T'$ is $T$ with a duplicated output, and we have $S_0 \perp T'$. Furthermore $S_0 + \alpha \bowtie \mathfrak{X}_1 :: T$ reduces to $S_0 \bowtie \mathfrak{X}_1 :: T'$ applying the induction hypothesis this reduces to $\mathfrak{X}_1$.

- Say that only cuts $(\mathfrak{X}/\mathfrak{Y})$ occurs in the interaction of $S :: T$ (if not we can fall back onto one of the previous cases) and assume the $\mathfrak{Y}$-links occurs in $S$. Furthermore let us denote $S_r$ the redex of $S$ in which all reversible cuts have been eliminated, similarly $T_r$ denotes such a redex for $T$. Then $S \perp T$ if and only if $S_r \perp T_r$, $S_r$ may be written as $S_r^* + \alpha$ where $\alpha$ is one of its terminal $\mathfrak{Y}$-link. Then eliminating the cut involving $\alpha$ the net $S_r :: T_r$ reduces to $S_r^* :: T'_r$ where $T'_r$ is $T_r$ in which one of its daimon as been splitted. Since in $S_r :: T_r$ there are only irreversible cuts it follows that $S_r \perp T_r$ imples $S_r^* \perp T'_r$.

Then note that the reversible form of $S \bowtie \mathfrak{X}_1$ corresponds to $S_r \bowtie \mathfrak{X}_1$ thus, $S \bowtie \mathfrak{X}_1 :: T$ reduces to $S_r \bowtie \mathfrak{X}_1 :: T_r$. Furthermore $S_r \bowtie \mathfrak{X}_1 :: T_r$ reduces to $S_r^* \bowtie \mathfrak{X}_1 :: T'_r$ and so by induction to $\mathfrak{X}_1$, and so we conclude. $\square$

**PROPOSITION D.4 (MERGES BELONGS TO THE COMPOSITIONAL CONSTRUCTION).** Given $A$ and $B$ two types;

$$ (A \bowtie B)^{\perp} \subseteq A \cdot B. $$

2263

2264

2265

2266

**PROOF.** Consider $S$ a net in $A \bowtie B$. $S$ may therefore be written as $a \bowtie b$ for two elements $a \in A$ and $b \in B$. The net $a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle + \langle p, q \Delta_{\text{cut}}\rangle \langle\Delta_{\mathfrak{X}} q\rangle \bowtie b$ reduces to $a \bowtie b$ by a glueing cut, since the glueing cut can always be perfomed first, an orthogonal net to $a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle + \langle p, q \Delta_{\text{cut}}\rangle \langle\Delta_{\mathfrak{X}} q\rangle \bowtie b$ is a net orthogonal to $a \bowtie b$.

2267

2268

2269

2270

2271

Now consider $\bar{a}$ some net in $A^\perp$. Since $a :: \bar{a}$ reduces to $\langle\Delta_{\mathfrak{X}}\rangle$, by proposition D.3 $a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle :: \bar{a}$ reduces to $\langle\Delta_{\mathfrak{X}} p\rangle$. Similarly $b \bowtie \langle\Delta_{\mathfrak{X}} q\rangle :: \bar{b}$ reduces to $\langle\Delta_{\mathfrak{X}} q\rangle$. Since cut elimination is local;

2272

2273

2274

2275

2276

2277

2278

2279

2280

2281

2282

2283

2284

2285

2286

2287

2288

$$ \begin{align*} a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle + \langle p, q \Delta_{\text{cut}}\rangle \langle\Delta_{\mathfrak{X}} q\rangle \bowtie b :: (\bar{a} \parallel \bar{b}) \\ = (a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle :: \bar{a}) + \langle p, q \Delta_{\text{cut}}\rangle (\langle\Delta_{\mathfrak{X}} q\rangle \bowtie b :: \bar{b}) \\ \rightarrow \langle\Delta_{\mathfrak{X}} p\rangle + \langle p, q \Delta_{\text{cut}}\rangle + \langle\Delta_{\mathfrak{X}} q\rangle \\ \rightarrow \langle\Delta_{\mathfrak{X}}\rangle \end{align*} $$

This shows that $a \bowtie \langle\Delta_{\mathfrak{X}} p\rangle + \langle p, q \Delta_{\text{cut}}\rangle \langle\Delta_{\mathfrak{X}} q\rangle \bowtie b :: (\bar{a} \parallel \bar{b})$ reduces to $\mathfrak{X}_0$ and thus so does $a \bowtie b :: (\bar{a} \parallel \bar{b})$ since the last glueing cut of the reduction may as been performed as first due to the commutation results. This shows that $a \bowtie b$ is orthogonal to $A^\perp \parallel B^\perp$ and so belongs to $A \bowtie B$. Hence we have shown the inclusion $A \bowtie B \subseteq A \bowtie B$ and therefore $(A \bowtie B)^{\perp} \subseteq A \bowtie B$ since the right member of the inclusion is closed under bi-orthogonal. $\square$

**PROPOSITION D.5.** For any integer $n$ the daimon link $\mathfrak{X}_n$ belongs to $\{\mathfrak{X}_1\}^{\perp} \supsetneq \dots \supsetneq \{\mathfrak{X}_1\}^{\perp}$ (composition of $n$ components).

2289

2290

2291

2292

2293

2294

2295

2296

2297

2298

**PROOF.** By induction. For the base case note that $\mathfrak{X}_1$ belongs to $\{\mathfrak{X}_1\}^{\perp}$ for any net. Now if we assume $\mathfrak{X}_n$ belongs to the composition of size $n$ that is $\{\mathfrak{X}_1\}^{\perp} \supsetneq \dots \supsetneq \{\mathfrak{X}_1\}^{\perp}$ since $\mathfrak{X}_1$ belongs to $\{\mathfrak{X}_1\}^{\perp}$ the previous proposition ensure that $\mathfrak{X}_n \bowtie \mathfrak{X}_1$ belongs to the composition of size $n+1$ of $\{\mathfrak{X}_1\}^{\perp} \supsetneq \dots \supsetneq \{\mathfrak{X}_1\}^{\perp}$. But $\mathfrak{X}_n \bowtie \mathfrak{X}_1$ is exactly $\mathfrak{X}_{n+1}$ which allows us to conclude. $\square$

2299

## D.3 Proofs of section 4

**Notation 20.** We denote by $\mathfrak{X}_2$ a daimon with two outputs e.g. $\langle\Delta_{\mathfrak{X}} p_1, p_2\rangle$. Given an integer $n$ we denote $I_{\mathfrak{X}}^n$ the sum $\sum_{1 \le i \le n} \langle\Delta_{\mathfrak{X}} p_i, q_i\rangle$ with the order $(p_1 < \dots < p_n < q_1 < \dots < q_n)$ on the conclusions. In particular $I_{\mathfrak{X}}^1$ corresponds to $\mathfrak{X}_2$.

2300

2301

2302

2303

2304

**LEMMA D.6.** For any orthogonal nets $S_1$ and $S_2$ with $n$ output $(I_{\mathfrak{X}}^n :: S_1) :: S_2 \rightarrow^* \langle\Delta\rangle$.

2305

2306

2307

**PROOF.** We do so by induction on the size of the nets. If the nets are made only of daimon this is trivial. $\square$

2308

2309

**PROPOSITION 4.2.** For any types with one output $A \subseteq B^\perp$; $\mathfrak{X}_2$ belongs to $A^\perp \supset B^\perp$.

2310

2311

2312

**PROOF.** This is a special case of the previous lemma when $n = 2$ the interface $I_{\mathfrak{X}}^2$ is $\mathfrak{X}$.

2313

2314

2315

Given two types such that $A \subseteq B^\perp$ note that any pair of net $S \in A$ and $T \in B$ will satisfies $S \perp T$ and thus $\mathfrak{X}_2$ will be orthogonal to $A \parallel B$ and so belong to $A^\perp \supset B^\perp$. $\square$

2316

2317

2318

**Remark 45.** In particular for any type $A, \mathfrak{X}_2$ belongs to $A \supset A^\perp$.

2319

2320
**COROLLARY D.7.** For any interpretation basis $\mathcal{B}$, if $\mathcal{B}$ is standard in $X$, $\mathcal{X}_2$ belongs to $[[X, X^{\perp}]_{\mathcal{B}}]$.

**PROOF.** If the basis $\mathcal{B}$ is standard in $X$ we have the inclusion $[[X]]_{\mathcal{B}}^{\perp} \subseteq [[X^{\perp}]_{\mathcal{B}}]$, which implies by the previous proposition, that $\mathcal{X}_2$ belongs to $[[X]]_{\mathcal{B}}^{\perp\perp} \succ [[X^{\perp}]_{\mathcal{B}}]$ and so since we deal with types to $[[X]]_{\mathcal{B}} \succ [[X^{\perp}]_{\mathcal{B}}]$. $\square$

**Definition D.8 (Constraint).** A constraint is a set of sequents of multiplicative formulas. A sequent satisfies a constraint $\Gamma$ if it belongs to $\mathcal{C}$.

**Remark 46.** For instance the axiom rule of MLL only introduces sequents which belong to the constraint $\{A, A^{\perp} | A \in \mathcal{F}_{\text{MLL}}\}$. On the other hand the constraint for MLL$^{\mathcal{X}}$ corresponds to the set of all sequents.

**Notation 21.** Given a constraint $\Gamma$ we denote $S \vdash_{\Gamma} \Gamma$ whenever $S$ represents a proof of $\Gamma$ in MLL$^{\mathcal{X}}$ such that the daimon rules introduces only sequents in $\mathcal{C}$.

**Definition D.9 (Adequate interpretation basis).** An interpretation basis $\mathcal{B}$ is adequate with a constraint $\mathcal{C}$ on MLL sequents whenever for any sequent $\Gamma = A_1, \dots, A_n$ satisfying the constraint $\mathcal{C}$ the daimon with $n$ outputs realizes $\Gamma$.

**PROPOSITION D.10 (SOUNDNESS).** Given an adequate interpretation basis $\mathcal{B}$ with respect to a constraint $\mathcal{C}$, for any multiplicative net $S$ and a sequent $\Gamma$,

$$S \vdash_{\Gamma} \Gamma \Rightarrow S \Vdash_{\mathcal{B}} \Gamma.$$

**PROOF.** of Proposition D.10. We proceed by induction on the size of the proof that $S$ represents.

**BASE** If the proof is of size one then $S$ is made only of one daimon link. Furthermore by assumption $S \vdash_{\Gamma} \Gamma$, since the basis $\mathcal{B}$ is sound with respect to the constraint this implies that $S \Vdash_{\mathcal{B}} \Gamma$.

**IND-1** Assume that the last rule in the represented proof is a $\mathcal{N}$-rule. Thus the sequent is of the form $\Gamma, A \mathcal{N} B$, and by assumption $S \vdash_{\Gamma} A \mathcal{N} B$.

Assume without loss of generality that the active formula in the last rule is $A \mathcal{N} B$. Say the conclusion of $S$ are ordered as $q_1, \dots, q_n, p$ then since $p$ is given the type $A \mathcal{N} B$ and that this formula is active; it must be that $S$ is of the form $S' + \langle p_1, p_2 \succcurlyeq \mathcal{N} p \rangle$ such that $S' \vdash_{\Gamma} A, B$.

Calling the induction hypothesis we can deduce $S' \Vdash_{\mathcal{B}} \Gamma$, $A, B$. By definition, this is equivalent that for any $\gamma$ in $[[\Gamma]]_{\mathcal{B}}^{\perp}$, we have $S' :: \gamma \Vdash_{\mathcal{B}} A, B$, indeed it follows that $S' :: \gamma + \langle p_1, p_2 \succcurlyeq \mathcal{N} p \rangle \Vdash_{\mathcal{B}} A \mathcal{N} B$.

Furthermore interaction and sum commute hence, $S' :: \gamma + \langle p_1, p_2 \succcurlyeq \mathcal{N} p \rangle = S' + \langle p_1, p_2 \succcurlyeq \mathcal{N} p \rangle :: \gamma$ and so corresponds to $S :: \gamma$. Since this hold for any $\gamma \in [[\Gamma]]_{\mathcal{B}}^{\perp}$ this allows us to conclude that $S \Vdash_{\mathcal{B}} \Gamma, A \mathcal{N} B$.

**IND-2** Assume that the represented proof by $S$ as for last rule the introduction of a tensor. The proved sequent is of the form $\Gamma, A \otimes B, \Delta$ where $A \otimes B$ is the active formula in the last rule.

Thus $S$ is of the form $S_1 \otimes S_2$ where $S_1 \vdash_{\Gamma} A$ and $S_2 \vdash_{\Gamma} \Delta, B$.

Calling the induction hypothesis we obtain $S_1 \Vdash_{\mathcal{B}} \Gamma, A$ and $S_2 \Vdash_{\mathcal{B}} \Delta, B$. Thus for any $\gamma \in [[\Gamma]]_{\mathcal{B}}$ and $\delta \in [[\Delta]]_{\mathcal{B}}$ $S_1 :: \gamma \Vdash_{\mathcal{B}} A$ and $S_2 :: \delta \Vdash_{\mathcal{B}} B$. In particular this means that the tensor union of the two nets $S_1 :: \gamma + S_2 :: \delta + \langle p_1, p_2 \succcurlyeq p \rangle$ is in $[[A]]_{\mathcal{B}} \otimes [[B]]_{\mathcal{B}}$ and thus in $[[A] \otimes B]]_{\mathcal{B}}$.

Note that $S_1 :: \gamma + S_2 :: \delta + \langle p_1, p_2 \succcurlyeq p \rangle$ corresponds to $S_1 + S_2 + \langle p_1, p_2 \succcurlyeq p \rangle :: \gamma \parallel \delta$. Thus $S_1 + S_2 + \langle p_1, p_2 \succcurlyeq p \rangle :: \gamma \parallel \delta \Vdash_{\mathcal{B}} A \otimes B$. Since this hold for any $\gamma$ and $\delta$ we conclude that $S_1 + S_2 + \langle p_1, p_2 \succcurlyeq p \rangle \Vdash_{\mathcal{B}} \Gamma, \Delta, A \otimes B$ e.g. $S \Vdash_{\mathcal{B}} \Gamma, \Delta, A \otimes B$. $\square$

**PROPOSITION D.11.** Given $\mathcal{B}$ an approximable basis for any formula $A$ of MLL the type $[[A]]_{\mathcal{B}}$ is approximable.

**PROOF.** By induction on $A$. In the case where $A$ is atomic this follows from the definition.

* For a formula $A \otimes B$. Let us show $\mathcal{X}_1$ is orthogonal to $[[A \otimes B]]_{\mathcal{B}}^{\perp}$. The interpretation $[[A \otimes B]]_{\mathcal{B}}^{\perp}$ corresponds to $([A]_{\mathcal{B}} \otimes [[B]_{\mathcal{B}}]^{\perp})^{\perp}$ and so $[[A]]_{\mathcal{B}}^{\perp} \succcurlyeq [[B]]_{\mathcal{B}}^{\perp}$. By induction $[[A]]_{\mathcal{B}}$ and $[[B]]_{\mathcal{B}}$ are both approximable. In other words, $[[A]]_{\mathcal{B}}^{\perp} \subset \{\mathcal{X}_1\}^{\perp}$ and $[[B]]_{\mathcal{B}}^{\perp} \subset \{\mathcal{X}_1\}^{\perp}$.

To be orthogonal to $[[A]]_{\mathcal{B}}^{\perp} \succcurlyeq [[B]]_{\mathcal{B}}^{\perp}$ is to be orthogonal to the nets $S + \langle p_1, p_2 \succcurlyeq p \rangle$ where $S$ belongs to $[[A]]_{\mathcal{B}}^{\perp} \succ [[B]]_{\mathcal{B}}^{\perp}$. After one step of cut elimination $\mathcal{X}_1 :: S + \langle p_1, p_2 \succcurlyeq p \rangle$ reduces to $\mathcal{X}_2 :: S$ which is $\mathcal{X}_1 \parallel \mathcal{X}_1 :: S$. Since, by induction, $\mathcal{X}_1$ belongs to $[[A]]_{\mathcal{B}}^{\perp\perp}$ $S :: \mathcal{X}_1$ belongs to $[[B]]_{\mathcal{B}}^{\perp}$. By induction, $[[B]]_{\mathcal{B}}^{\perp}$ is orthogonal to $\mathcal{X}_1$ hence $S :: \mathcal{X}_1 :: \mathcal{X}_1$ reduces to $\langle \succcurlyeq \mathcal{X}_1 \rangle$.

* Now consider a formula of the form $A \mathcal{N} B$. Again let us show that $\mathcal{X}_1$ is orthogonal to $[[A \mathcal{N} B]]_{\mathcal{B}}^{\perp}$ e.g. to $[[A]]_{\mathcal{B}}^{\perp} \otimes [[B]]_{\mathcal{B}}^{\perp}$. To be orthogonal to that type is to be orthogonal to the nets $\bar{a} \parallel \bar{b} + \langle p_1, p_2 \succcurlyeq p \rangle$. After one step of cut elimination $\mathcal{X}_1 :: \bar{a} \parallel \bar{b} + \langle p_1, p_2 \succcurlyeq p \rangle$ reduces to $\mathcal{X}_2 :: \bar{a} \parallel \bar{b}$. But $\mathcal{X}_2$ is $\mathcal{X}_1 \bowtie \mathcal{X}_1$ and by induction both $[[A]]_{\mathcal{B}}$ and $[[A]]_{\mathcal{B}}$ contains $\mathcal{X}_1$ thus $[[A]]_{\mathcal{B}} \succ [[B]]_{\mathcal{B}}$ contains $\mathcal{X}_2$. Equivalently this means that $\mathcal{X}_2$ is orthogonal to $[[A]]_{\mathcal{B}} \succ \parallel [[B]]_{\mathcal{B}}^{\perp}$, hence $\mathcal{X}_2 \perp \bar{a} \parallel \bar{b}$. This concludes to show that $\mathcal{X}_1$ belongs to $[[A \mathcal{N} B]]_{\mathcal{B}}$.

**THEOREM 4.3.** Let $S$ be a multiplicative net, $\mathcal{B}$ an interpretation basis, and $\Gamma$ a sequent:

* if $\mathcal{B}$ is regular, then $S \vdash_{\text{MLL}} \Gamma \Rightarrow S \Vdash_{\mathcal{B}} \Gamma$,

* if $\mathcal{B}$ is approximable, then $S \vdash_{\text{MLL}^{\mathcal{X}}} \Gamma \Rightarrow S \Vdash_{\mathcal{B}} \Gamma$.

**PROOF.** of Theorem 4.3. We must treat two cases namely that of MLL and of MLL$^{\mathcal{X}}$. The proposition D.10 ensure that to conclude it is enough to show the base case of the induction.

* For MLL$^{\mathcal{X}}$, note that if $\mathcal{B}$ is approximable then any interpretation $[[A]]_{\mathcal{B}}$ is approximable e.g. contains $\mathcal{X}_1$. We can reformulate this as $\{\mathcal{X}_1\}^{\perp\perp} \subseteq [[A]]_{\mathcal{B}}$. As a consequence since the construction on types preserve inclusion $\{\mathcal{X}_1\}^{\perp\perp} \succ \dots \succ \{\mathcal{X}_1\}^{\perp\perp}$ is included in $[[A_1]]_{\mathcal{B}} \succ \dots \succ [[A_n]]_{\mathcal{B}}$ for any sequent $A_1, \dots, A_n$. Using proposition D.5 this implies that $\mathcal{X}_n$ is contained in that type e.g. in $[[A_1, \dots, A_n]]_{\mathcal{B}}$.

2379

2380

2381

2382

2383

2384

2385

2386

2387

2388

2389

2390

2391

2392

2393

2394

2395

2396

2397

2398

2399

2400

2401

2402

2403

2404

2405

2406

2407

2408

2409

2410

2411

2412

2413

2414

2415

2416

2417

2418

2419

2420

2421

2422

2423

2424

2425

2426

2427

2428

2429

2430

2431

2432

2433

2434

2435

2436
* In the case of MLL by the corollary D.7 $\star_2$ belongs to $[[X, X^{\perp}]_{\mathcal{B}}$ for any basis. $\square$

# E COMPLEMENTS TO SECTION 5

## E.1 Proof of Theorem 5.8 – Reformulating Danos Regnier

*Definition E.1 (Switching graph).* Given a multiplicative which does not contain $\mathfrak{N}$-links, we can associate a undirected graph denoted $G(S)$ as follow;

* A vertex of $G(S)$ is either a position of the net $S$, or a daimon or a cut link.

* There is an edge between two vertices whenever;

- The two vertex $u$ and $v$ are positions of $S$ and belong to the same tensor link.

- $u$ is a cut link and $v$ is an input of $u$ (or vice versa).

- $u$ is a daimon link and $v$ is an output of $u$ (or vice versa).

*Definition E.2.* Given $E$ a set and $X$ and $Y$ two partitions of $E$. The graph induced by $X$ and $Y$ is the graph $G(X, Y) = (V, E, b)$ such that;

* The vertex of $G(X, Y)$ are the classes of $X$ and $Y$.

* The edges of the graph are exactly the elements of $E$.

* The border of an edge $e \in E$ is the pair $\{c, c'\}$ of the class $c$ in $X$ containing $e$ and the class $c'$ in $Y$ containing $e$.

Two partitions $X$ and $Y$ of a set $E$ are *orthogonal* whenever their induced graph is acyclic and connected.

Then the classical results of Danos Regnier [3] can be stated as follows, either mentioning the acyclic and connected switching graphs, or the orthogonality of the induced partitions.

**THEOREM E.3.** Given a multiplicative net $S$ the propositions are equivalent;

* $S$ is correct.

* For any switching $\sigma S$ of $S$ the graph $G(\sigma S)$ is acyclic and connected.

* For any switching $\sigma S$ the partitions $sS^\star$ and $\uparrow \sigma S$ are orthogonal.

*Definition E.4 (image of a partition).* Given a partition $P = \{C_1, \dots, C_n\}$ of a set $X$ and a function $f: X \to Y$ the image of $P$ by $f$ is the set $\{f(C_1), \dots, f(C_n)\}$, it is denoted $f(P)$.

**PROPOSITION E.5 (BIJECTIONS PRESERVE PARTITIONS).** Given $f: X \to Y$ a bijection between two sets. For any partition $P$ of $X$ the image $f(P)$ is still a partition.

*Definition E.6 (Image of a partition).* An image of a set $\{p_1, \dots, p_n\}$ of positions is denoted $X^\star$ and is a a daimon $\langle \Delta^\star, p_1, \dots, p_n \rangle$. The image of a partition $P = X_1, \dots, X_k$ of a set of positions $X$, is denoted $P^\star$, and corresponds to the sum $X_1^\star + \dots + X_k^\star$.

**Remark 47.** The image of a set of position is *not unique* since the order of the output of the daimon link may be reordered. As a consequence the image of a partition is also not unique.

**PROPOSITION E.7.** Given two partitions $P$ and $Q$ of a set of positions $X$. The two assertions are equivalent;

* The partitions $P$ and $Q$ are orthogonal.

* Given a set $Y$ disjoint from $X$, and $\sigma: X \to Y$ a bijection, The interaction $P^{\star} ::_{\sigma} Q^{\star}$ reduces to $\langle \Delta^{\star}, \star \rangle$. In particular, $P^{\star}$ and $Q^{\star}$ are orthogonal.

**PROOF.** By induction on the size of the set $X$. $\square$

**PROPOSITION E.8.** Given two cut free nets $S$ and $T$ witnessing respectively $A_1, \dots, A_n$ and $A_1^\perp, \dots, A_n^\perp$. The assertions are equivalent;

* $S$ and $T$ are orthogonal.

* $S^\star$ and $T^\star$ are orthogonal.

**PROOF.** The multiplicative cuts get eliminated and can always be performed first due to the commutation results. Furthermore since the nets witness dual formulas no non homogeneous cut will occur. $\square$

**COROLLARY E.9.** Given $S$ a net witnessing $A$. For a switching $\sigma S$ of $S$, the assertions are equivalent;

* The partitions $s(S^\star)$ and $\sigma S$ are orthogonal.

* $S$ is orthogonal to any net $T$ witnessing $A^\perp$ and such that $T^\star = (\sigma S)^\star$.

Using this corollary and the established result of Danos Regnier we obtain the following;

**PROPOSITION E.10.** Given $S$ a multiplicative net with one conclusion witnessing $A$. The assertions are equivalent;

* $S$ is correct.

* $S$ is orthogonal to tests($A$).

We can indeed generalize this result the case where $S$ has multiple conclusions, as usual we do this by transformin the net with multiple conclusions in a net with one conclusion by adding a bunch of $\mathfrak{N}$-links.

*Definition E.11 (General connectives).* A generalized $\mathfrak{N}$-link on the positions $p_1, \dots, p_n$ is a module denoted $\langle p_0, \dots, p_n \Delta^{\mathfrak{N}} p \rangle$ and defined by the following induction;

* $\langle p_0, p_1 \Delta^{\mathfrak{N}_1} p \rangle = \langle p_0, p_1 \Delta^{\mathfrak{N}} p^1 \rangle$.

* For any $n > 0$ we defined $\langle p_1, \dots, p_{n+2} \Delta^{\mathfrak{N}_{n+1}} p \rangle = \langle p^{n-1}, p_n \Delta^{\mathfrak{N}_n} p \rangle + \langle p^n, p_{n+1} \Delta^{\mathfrak{N}} p^{n+1} \rangle$.

Similarly we defined the generalized tensor links $\langle p_0, \dots, p_n \Delta^{\otimes n} p \rangle$.

**PROPOSITION E.12.** Let $S$ be a net with conclusions $p_0, \dots, p_n, q_1, \dots, q_k$. Let $S_1, \dots, S_n, T_1, \dots, T_k$ be $n$ nets with one conclusion the assertions are equivalent;

(1) $S \perp S_1 \parallel \dots \parallel S_n \parallel T_1 \parallel \dots \parallel T_k$.

(2) $S+\langle p_0, \dots, p_n \Delta^{\mathfrak{N}_n} p \rangle \perp S_1+\dots+S_n+\langle S_1(1), \dots, S_n(1) \Delta^{\otimes n} p \rangle \parallel T_1 \parallel \dots \parallel T_k$.

**PROOF.** By a simple induction of the size of the generalized $\mathfrak{N}$-connective. $\square$

This easily leads to a proof of the Danos Regnier theorem as stated in section 5.

**THEOREM 5.8 (DANOS REGNIER TESTS, [3]).** Given a cut-free net $S \sim A_1, \dots, A_n$, the two following assertions are equivalent:

* $S \vdash_{\text{MLL}\star} A_1, \dots, A_n$;

* $S$ is orthogonal to tests($A_1$) $\parallel \dots \parallel$ tests($A_n$).
## E.2 Correctness of Tests

**Definition E.13.** Given a net $S$ and $\sigma S$ one of its switching, the node measure of $S$ in $\sigma$ is the number of nodes of the graph $G(\sigma S)$ respectively the edge measure of $S$ in $\sigma$ is the number of egdes of the graph $G(\sigma S)$. We respectively denotes them $N(\sigma S)$ and $E(\sigma S)$.

**PROPOSITION E.14.** Given a net $S$ for any switching $\sigma S$ and $\sigma S'$; $N(\sigma S) = N(\sigma' S)$ and $E(\sigma S) = E(\sigma' S)$

**Remark 48.** As a consequence we can defined the node measure and edge measure of a net $S$ as the node measure and edge measure of one of its switching. We denote it by $N(S)$ and $E(S)$.

**PROPOSITION E.15.** Given a graph $G = (V, E)$ such that $card(V) - card(E) = 1$ the assertions are equivalent;

* $G$ is acyclic.

* $G$ is connected.

**PROPOSITION E.16.** Whenever a graph $G = (V, E)$ is acyclic and connected we have $card(V) - card(E) = 1$.

**THEOREM E.17.** Cut-elimination preserves correctness.

**PROOF.** Note that the step of cut elimination preserve connectedness of the switching graphs, and furthermore that they preserve the measure $N(S) - E(S)$ thus the proposition E.15 allows us to conclude. $\square$

**PROPOSITION E.18.** The switching rewriting $\rightarrow \mathcal{N}$ preserves correctness.

**PROOF.** Indeed since whenever $S \rightarrow \mathcal{N} S'$ the switching of $S'$ are include in the switching of $S$. Thus if all the switching of $S$ are acyclic and connected it is also true in particular for those of $S'$ $\square$

**PROPOSITION E.19.** Eta-expansion preserves correctness.

**PROOF.** Note that the obtained net preserve connection, furthermore the measure $N(S) - E(S)$ is preserved. $\square$

**PROPOSITION E.20.** For any two correct nets $S$ and $T$ if $T$ has one output, the interaction $S :: T$ remains correct.

**PROOF.** Indeed in the interaction $S :: T$ the connectivity is preserved. Furthermore $N(S) + N(T) + 1 - (E(S) + E(T) + 2)$ is equal to $3 - 2$ and so is equal to 1. $\square$

**Definition E.21 (Syntax tree).** A net $N$ is a representation of an MLL formula $F$, when it satisfies the inductive condition:

* Whenever $F$ is an atomic formula, $N$ is an hypergraph consisting of only one position $p$.

* Given that $\square = \otimes$ or $\square = \mathcal{N}$; whenever $F = F_1 \square F_2$, for any nets $N_1$ and $N_2$ the net $N_1 + N_2 + \langle p_1, p_2 \triangleright l p \rangle$ is a representation of $F$ if $N_1$ represents $F_1$ and has for conclusion $p_1$, $N_2$ representing $F_2$ and has for conclusion $p_2$, and the label $l$ corresponds to $\square$, while $p$ is a fresh position.

A syntax tree is the representation of a formula. Given a formula $A$ we denote syn($A$) the set of representations of $A$.

**PROPOSITION E.22.** Given a net $r$ with $n$ conclusions that is the sum of the syntactical representation of formulas containing only tensors. $r :: \sum_{1 \le i \le n} \star_1$ reduces to $\uparrow r^\star + \sum_{1 \le i \le n} \langle p_i, q_i \triangleright \text{cut} \rangle$.

**THEOREM 5.7 (CORRECTNESS OF TESTS).** Any test of a formula $A$ is a proof in MLL$\star$ of the negation $A^\perp$.

**PROOF.** of Theorem 5.7. Consider a formula $A$ of MLL. Consider the correct net $\star_2 = \langle \triangleright \star_1 p_1, p_2 \rangle$ and perform a bunch of eta expansion to obtain a correct net $S$ witness $A^\perp$, $A$. In that case $S$ is of the form $r + r' + \sum_{1 \le i \le m} \langle \triangleright \star_1 r_i, r'_i \rangle$ where $r$ is a representation of $A$ and $r'$ is a representation of $A^\perp$ and the $r_i$'s are the initial positions of $r$ and similarly for the $r'_i$'s. Perform a bunch of switching rewriting witnessing $A$ e.g. on the connectives above $p_2$. We obtain a net $S'$ which remains correct with conclusion $p_1, q_1, \dots, q_k$. Now make $S'$ interact with unary daimons on its conclusion $q_1, \dots, q_k$, e.g. consider

$$T = S' :: \{q_i \mapsto t_i, 1 \le i \le n\} \sum_{1 \le i \le k} \langle \triangleright \star_1 t_i \rangle.$$

Again this transformation preserve correctness, thus $T$ is correct. Now since cut elimination preserve correctness any redex of $T$ will be correct. In particular these cuts reduces to the partitions of $\uparrow (\sigma A)$, e.g. we obtain,

$$r + \sum_{1 \le i \le m} \langle \triangleright \star_1 r_i, r'_i \rangle + \sum_{1 \le i \le n} \langle r'_i, q_i \triangleright \text{cut} \rangle (\uparrow r')^\star.$$

After reducing the gluing we obtain a net of the form $r+(\uparrow r')^\star$ where $r$ and $r'$ are representations of dual formulas. This net is correct again since cut elimination preserve correctness. This net is a test of $A^\perp$ hence we have showed that any test of $A^\perp$ is correct and we can conclude. $\square$

## E.3 Decomposition

**PROPOSITION E.23.** Given two sets of nets $A$ and $B$;

* $A \parallel B = A^{\perp\perp} \parallel B^{\perp\perp}$.

* $A \succ B = A^{\perp\perp} \succ B^{\perp\perp}$.

* $A \prec B = A^{\perp\perp} \prec B^{\perp\perp}$.

* $A \otimes B = A^{\perp\perp} \otimes B^{\perp\perp}$.

**PROOF.** We treat each cases independently.

* By duality, $(A \parallel B)^\perp = A^\perp \succ B^\perp$. While $(A^{\perp\perp} \parallel B^{\perp\perp})^\perp = A^{\perp\perp\perp} \succ B^{\perp\perp\perp}$ e.g. tri-orthogonality corresponds to orthogonality [8] this is $A^\perp \succ B^\perp$ and so $(A \parallel B)^\perp$.

The two orthogonal of the two types are equal thus they are equal $A \parallel B = A^{\perp\perp} \parallel B^{\perp\perp}$.

* Say a net belongs to $A \succ B$ equivalently it belongs to $(A^\perp \parallel B^\perp)^\perp$ which since tri-orthogonal is orthogonality is $(A^{\perp\perp\perp} \parallel B^{\perp\perp\perp})^\perp$ which is $A^{\perp\perp} \succ B^{\perp\perp}$.

* Note that $A \prec B$ is equal to $(A^\perp \otimes B^\perp)^\perp$ and thus to $(A^{\perp\perp\perp} \otimes B^{\perp\perp\perp})^\perp$ which is exactly $A^{\perp\perp} \prec B^{\perp\perp}$.

* Similarly to the previous case. $\square$

**PROPOSITION E.24 (DECOMPOSITION).** Let $\mathcal{B}$ be an interpretation basis, $\mathcal{H}$ be an hypersequent, $A, B$ two formulas and $S$ be a multiplicative net.

* If $S = S_0 + l$ has a terminal $\mathcal{N}$ link $l$ above its last conclusion and $S \in [\mathcal{H}, A, \mathcal{N} \mathcal{B}]_\mathcal{B}$; then $S_0$ belongs to $[\mathcal{H}, A, B]_\mathcal{B}$

* If $S = S_0 + l$ has a terminal $\mathcal{N}$ link $l$ above its last conclusion and $S \in [\mathcal{H} \parallel A, \mathcal{N} \mathcal{B}]_\mathcal{B}$; then $S_0$ belongs to $[\mathcal{H} \parallel (A, B)]_\mathcal{B}$

2611

2612

2613

2614

2615

2616

2617

2618

2619

2620

2621

2622

2623

2624

2625

2626

2627

2628

2629

2630

2631

2632

2633

2634

2635

2636

2637

2638

2639

2640

2641

2642

2643

2644

2645

2646

2647

2648

2649

2650

2651

2652

2653

2654

2655

2656

2657

2658

2659

2660

2661

2662

2663

2664

2665

2666

2667

2668

2669
• If $S = S_0 + l$ has a terminal $\otimes$ link $l$ above its last conclusion and $S \in [\mathcal{H}, A \otimes B]_B$; then $S_0$ belongs to $[\mathcal{H}, (A \| B)]_B$

• If $S = S_0 + l$ has a terminal $\otimes$ link $l$ above its last conclusion and $S \in [\mathcal{H} \| A \otimes B]_B$; then $S_0$ belongs to $[\mathcal{H} \| A \| B]_B$

PROOF. • Consider $S$ a net with a terminal $\mathfrak{N}$-link $l$ decomposing $S = S_0 + l$ such that $l$ outputs the only conclusion of $S$. Say $S$ belongs to $[A \mathfrak{N} B]_B$ equivalently $S$ is orthogonal to $[A]_B^{\perp} \otimes [B]_B^{\perp}$, since a multiplicative cut can always be performed first this implies that $S_0$ is orthogonal to $[A]_B^{\perp} \| [B]_B^{\perp}$ thus $S_0$ belongs to $[A]_B, [B]_B$. This reasoning easily adapts to $[\mathcal{H}, A, B]_B$.

• The reasonment for a net in $[A \otimes B]_B$ is similar and also easily adapts to the case $[\mathcal{H}, A \otimes B]_B$.

• Consider on the other hand a net $S$ in $[\mathcal{H} \| A \otimes B]_B$, such that $S = S_0 + l$ where $l$ is a tensor link and outputs the last conclusion of $S$. Equivalently $S$ is a net orthogonal to $[\mathcal{H}]_B^{\perp}, [A \otimes B]_B^{\perp}$ e.g. $[\mathcal{H}]_B^{\perp}, [A]_B^{\perp} \otimes [B]_B^{\perp}$. Since the multiplicative cut commute to the left and using proposition E.23 it follows that $S_0$ is orthogonal to $[\mathcal{H}]_B^{\perp}, [A]_B^{\perp}, [B]_B^{\perp}$. Equivalently $S_0$ belongs to $[\mathcal{H}]_B \| [A]_B \| [B]_B$.

• Similarly we treat the case $[\mathcal{H} \| A \mathfrak{N} B]_B$.

## E.4 Contracted, open and self dual Types

**Definition E.25 (Contracted type).** A type $A$ is contracted whenever for any $S$ in $A$, there exists a sequent $\Gamma$ made only of atomic formulas such that $S < \Gamma$.

**Remark 49.** A type $A$ is contracted equivalently whenever any net in $A$ cannot have connectives has terminal link.

**Definition E.26 (type interface).** A type interface is a sequence $(s_1, \dots, s_n)$ of symbols $s_i$ which belong to $\{\mathfrak{N}, \mathfrak{N}, \otimes\}$. The type interface of a net $S$ with conclusions $(p_1, \dots, p_n)$ is the sequence $(s_1, \dots, s_n)$ where each $s_i$ is the label of the link which outputs $p_i$.

A type interface $s$ is coherent with a type $A$ whenever there exists a net $S$ in $A$ with interface $s$. A sequence $(X_1, \dots, X_n)$ of subsets $X_i$ of $\{\mathfrak{N}, \mathfrak{N}, \otimes\}$ is coherent with a type $A$ whenever any interface $(s_1, \dots, s_n)$ with $s_i \in X_i$ is coherent with $A$.

**Definition E.27 (Open type).** A type is open whenever it is coherent with $(\{\mathfrak{N}, \otimes\}, \dots, \{\mathfrak{N}, \otimes\})$.

**Proposition E.28.** Given two open types $A$ and $B$;

• Their functional composition $A \succ B$ is still open.

• Their parallel composition $A \| B$ is still open.

PROOF. Indeed the parallel $A \| B$ remains open since it contains in particular the nets of the form $a \| b$ with $a \in A$ and $b \in B$. Similarly this remains true for $A \succ B$ since it contains the merge $A \triangleright B$ (see the appendix D.2). □

**Proposition E.29.** Whenever a type $A$ is open its dual is contracted.

PROOF. Since a net $S$ in $A^{\perp}$ is orthogonal to any net in $A$ in order to avoid clashing cuts the outputs of $S$ cannot be the outputs of connectives. □

**Proposition E.30.** A self dual type has only nets with no connectives has conclusions.

PROOF. A net $S$ in a self dual type $A$ must verify $S \perp S$. If $S$ has a terminal connective then the interaction $S :: S$ gives rise to a clashing cut and cut elimination fails. □

**Proposition E.31.** The orthogonal of a self dual type $A$ with one output is an open type.

PROOF. Since $A$ is self dual it contains no net which have a terminal connective. By the proposition 3.6 this means that $A^{\perp}$ must contain nets with $\mathfrak{N}$ link and $\otimes$ link as conclusions. Thus $A^{\perp}$ is an open type. □

**Remark 50.** The previous proposition E.30 together with proposition 3.6 implies in particular that there cannot be any type $A$ that is invariant under orthogonality, e.g. such that $A = A^{\perp}$. In particular this means that the inclusion $A \subseteq A^{\perp}$ of a self dual type is always strict.

**Proposition E.32.** Given a self dual interpretation basis $\mathcal{B}$ for any atomic hypersequent $\mathcal{H}$ the type $[\mathcal{H}]_B$ is open.

PROOF. This follows from proposition E.28 and proposition E.31 by induction on the size of the hypersequent. □

## E.5 Truncation Lemma

Recall that a *substitution* is a map $\theta$ which maps propositional variables to formulas. Naturally substitutions can be lifted by induction to formulas and to sequents; $\theta(A\Box B) \triangleq \theta A\Box\theta B$ and $\theta(\Gamma, A) = \theta(\Gamma)$, $\theta A$. A sequent $\Gamma$ is an *instance* of a sequent $\Delta$ whenever there exists a substitution $\theta$ such that $\theta\Delta = \Gamma$. In that case we denote $\Delta \leq \Gamma$.

**Definition E.33 (Approximation of a sequent).** A net $S$ is an (sub)-approximation of a sequent $\Gamma$, denoted $S < \Gamma$, if it witnesses a sequent $\Delta \leq \Gamma$.

There is a simple inductive process to associate a sequent $\downarrow \mathcal{H}$ to an hypersequent $\mathcal{H}$; $\downarrow A \triangleq A$ while $\downarrow \mathcal{H}_1, \mathcal{H}_2 \triangleq \downarrow \mathcal{H}_1, \downarrow \mathcal{H}_2$ and $\downarrow \mathcal{H}_1 \| \mathcal{H}_2 \triangleq \downarrow \mathcal{H}_1, \downarrow \mathcal{H}_2$.

**Remark 51.** A sequent that is the truncation of a sequent of $n$ formulas must also contain $n$ formulas.

Furthermore, if two representation of sequents $\Gamma = A_1, \dots, A_n$ and $\Delta = B_1, \dots, B_n$ are such that $\Delta \leq \Gamma$ this implies that for each index $1 \leq i \leq n$ we have $B_i \leq A_i$ specifically $A_i[X_1 \mapsto F_1, \dots, X_k \mapsto F_k] = B_i$.

**Lemma E.34 (TRUNCATION).** Let $\mathcal{B}$ be a self dual basis. For any net $S$; $S \in [\mathcal{H}]_B \Rightarrow S < \downarrow \mathcal{H}$.

PROOF. of lemma E.34. By induction on the hypersequent using the measure $(c, n)$ where $c$ is the number of connectives in the hypersequent and $n$ is the size of the hypersequent.

• If the hypersequent is made of one atomic formula $X$ then $S \in [X]_B$ implies that $S$ belongs to a contracted type, e.g. the outputs of $S$ are outputs of a daimon. This by definition means $S < X$.
2785

2786

2787

2788

2789

2790

2791

2792

2793

2794

2795

2796

2797

2798

2799

2800

2801

2802

2803

2804

2805

2806

2807

2808

2809

2810

2811

2812

2813

2814

2815

2816

2817

2818

2819

2820

2821

2822

2823

2824

2825

2826

2827

2828

2829

2830

2831

2832

2833

2834

2835

2836

2837

2838

2839

2840

2841

2842

* Say the hypersequent is made only of atomic formulas. The hypersequent may be of the form $H_1, H_2$ then $[[H_1, H_2]]_B = ([[H_1]]_B^\perp \parallel [[H_2]]_B^\perp)^\perp$ since, $[[H_1]]_B^\perp$ and $[[H_2]]_B^\perp$ are open types their parallel composition remains an open type. $[[H_1, H_2]]_B$ is the orthogonal of an open type hence it is a contracted type. Thus any sequent in that type as outputs which comes from a daimon link and thus is the approximation of any sequent of size $n$ in particular $S < \downarrow H$. We do a similar reasonment when $H = H_1 \parallel H_2$.

* Case of non-atomic hypersequent with a virgula as main connective. Assume that $S$ has a terminal connective link, say the hypersequent is of the form $H, A \not\sim B$ such that $S = S_0 + l$ where $l$ is a $\not\sim$-link and is the last conclusion of $S$. By proposition E.24 it follows that $S_0$ belongs to $[[H, A, B]]_B$ the measure of that hypersequent as decreased and so we apply the induction hypothesis; $S_0 < \downarrow (H, A, B)$ indeed it follows that $S < \downarrow (H, A, \not\sim B)$. A similar argument works for an hypersequent of the form $H, A \otimes B$.

* Case of non-atomic hypersequent with a parallel as main connective. On the other hand say $S$ belongs to the interpretation $[[H \parallel A \not\sim B]]_B$ then it is orthogonal to $[[H]]_B^\perp \succ [[A \not\sim B]]_B^\perp$ and thus $S_0$ is orthogonal to $[[H]]_B^\perp \succ [[A, B]]_B^\perp$. Equivalently using proposition E.24 $S_0$ belongs to $[[H \parallel A, B]]_B$ the size of the hypersequent as decreased and so we can apply the induction hypothesis; $S_0 < \downarrow (H, A, B)$ and thus $S < \downarrow (H, A, \not\sim B)$. A similar argument works for an hypersequent of the form $H \parallel A \otimes B$. Similarly we treat the case of $H, A \otimes B$.

□

## E.6 Proofs of section 5.2

**PROPOSITION E.35.** Let $S$ a multiplicative net and $\Delta$ and $\Gamma$ two sequents such that $\Delta \le \Gamma$;

$$S \upharpoonright_{\text{MLL}^*} \Delta \Rightarrow S \upharpoonright_{\text{MLL}^*} \Gamma.$$

**PROOF.** This is done by induction on the represented proof by $S$, specifically by looking at the last rule of the proof. The inductions steps are trivial. The base case hold since the daimon rule may introduce any sequents whenever it introduces $\Delta$ it may as well introduce a sequent of the same size, say $\Gamma$. □

□

**PROPOSITION E.36.** Given a net $S$ and a sequent $\Gamma$. If $S < \Gamma$ then there exists a truncation $\Delta$ of $S$ such that $S \vdash \Delta$.

**Notation 22.** Given a proof system $S$ (which would be either MLL, MLL$^*$ or MLL$_2$ here), for a sequent $\Gamma$ in MLL$_2$ we denote by $[[\Gamma : S]]$ the set of nets which represent a proof in $S$ of the sequent $\Gamma$.

**Remark 52.** Proposition E.35 implies that whenever $A \le B$ the set $[[A : \text{MLL}^*]]$ is contained in $[[B : \text{MLL}^*]]$.

**THEOREM 5.10 (MLL$^*$ COMPLETENESS).** Let $S$ be a cut-free net and $\Gamma$ be a sequent. For any self dual and approximable interpretation basis $B$, if $S$ belongs to $[[\Gamma]]_B$ then $S$ represents a proof of $\Gamma$ in MLL$^*$.

**PROOF.** of Theorem 5.10. Since the basis is self dual any net $S$ in $[[\Gamma]]_B$ is an approximation of $\downarrow \Gamma$ by the lemma E.34, since $\Gamma$ is a simple sequent, this means $S$ is an approximation of $\Gamma$. This means

using proposition E.36 that $S$ is the witness of a sequent $\Delta$ such that $\Delta \le \Gamma$. Denote $\Gamma = A_1, \dots, A_n$ and $\Delta = B_1, \dots, B_n$.

Furthermore $S$ belongs to $[[\Gamma]]_B$ which equivalently means that,

$$S \perp [[A_1^\perp]]_B \parallel \dots \parallel [[A_n^\perp]]_B.$$

Since adequacy is true for MLL$^*$ (theorem 4.3), for any index $i$ the interpretation $[[A_i^\perp]]_B$ contains the proofs of $A_i^\perp$ therefore,

For any index $i$ using the remark 52 since $B_i \le A_i$ it follows that $B_i^\perp \le A_i^\perp$ and thus $[[B_i^\perp : \text{MLL}^*]]_B \subseteq [[A_i^\perp : \text{MLL}^*]]_B$.

$$S \perp [[B_1^\perp : \text{MLL}^*]]_B \parallel \dots \parallel [[B_n^\perp : \text{MLL}^*]]_B.$$

In particular we have shown that the tests of a formula $F$ are proofs of $F^\perp$ thus tests($B_i$) $\subseteq [[B_i^\perp : \text{MLL}^*]]_B$ for any index $i$. Hence,

$$S \perp \text{tests}(B_1) \parallel \dots \parallel \text{tests}(B_n).$$

Since $S$ is a witness of $\Delta$ we conclude using proposition ?? that $S \upharpoonright_{\text{MLL}} \Delta$. In particular using the proposition E.35 it follows that $S \upharpoonright_{\text{MLL}} \Gamma$. □

**PROOF.** of Theorem 5.13 Since the basis is self dual and approximable the theorem 5.10 ensure that $S$ is a proof in MLL$^*$ of $\Gamma$. To conclude it remains to show that the binary daimons realise only sequents of the form $X, X^\perp$.

Indeed consider a binary daimon $\star_2$ from the proposition 4.2 it belongs to $A \succ A^\perp$ for any type $A$. Thus it belongs to $[[\cap_{X \in \Omega} X, X^\perp]]_B$. But indeed $S$ does not belongs to $[[\cap_{Y \in \Omega} \cap_{X \in \Omega} X, Y]]_B$ since then $S$ belongs to $A \succ A$ for any type. Chosing $A$ with the right measure $\star_2$ cannot belong to $A \succ A$ and thus $S$ does not belong $[[\cap_{Y \in \Omega} \cap_{X \in \Omega} X, Y]]_B$. This show that the binary daimons of $S$ realise only sequents of the form $X, X^\perp$ hence $\star_2$ is a proof of MLL, this indeed is preserved by induction. □

□

□

## F COMPLEMENTS TO SECTION 6

**PROPOSITION F.1.** Let $H$ be an hyper-sequent and $X$ be a propositional variable. If $X$ does not occur free in $H$ then for any type with one conclusion $R$; $[[H]]_B = [[H]]_{B(X \mapsto R)}$.

**PROOF.** of proposition F.1. By induction on the couple $(c, n)$ where $c$ is the number of connectives in $H$ and $n$ is the size of the hypersequent. Consider $R$ some type with one output.

* Base case (0, 1) e.g. hypersequent made of one formula. Note that $[[Y]]_{B(X \mapsto R)}$ is equal to $[[Y]]_B$ by definition.

* We show that whenever the property hold for $(c, n)$ and $(c', n')$ it holds for $(c + c', n + n')$. To do so we show the parallel operator and virgula's of hypersequent preserve the property.

Say $H = H_1 \parallel H_1$ then $[[H_1 \parallel H_2]]_{B(X \mapsto R)}$ corresponds to $[[H_1]]_{B(X \mapsto R)} \parallel [[H_2]]_{B(X \mapsto R)}$ by induction hypothesis on $H_1$ and $H_2$ this is equal to $[[H_1]]_B \parallel [[H_2]]_B$ which is $[[H_1 \parallel H_2]]_B$. Similarly we treat the case $H = H_1, H_2$

* Show that connectives can be decomposed, increasing the size of the hypersequent but decreasing $c$. We show that if the property hold for the cases $(c, 1)$ and $(c', 1)$ it holds for the cases $(c + c', 1 + 1)$.

Say the hypersequent is $[[A \not\sim B]]_{B(X \mapsto R)}$; if a net $S = S_0 + l$ where $l$ denotes the $\not\sim$-link which outputs the only conclusion belongs to $[[A \not\sim B]]_{B(X \mapsto R)}$ then $S_0$ belongs

2843

2844

2845

2846

2847

2848

2849

2850

2851

2852

2853

2854

2855

2856

2857

2858

2859

2860

2861

2862

2863

2864

2865

2866

2867

2868

2869

2870

2871

2872

2873

2874

2875

2876

2877

2878

2879

2880

2881

2882

2883

2884

2885

2886

2887

2888

2889

2890

2891

2892

2893

2894

2895

2896

2897

2898

2899

2900
$[[A, B]]_{\mathcal{B}}(X \mapsto R)$ applying induction hypothesis this is equal to $[[A, B]]_{\mathcal{B}}$ and thus $S$ belongs to $[[A \mathfrak{N} B]]_{\mathcal{B}}$.

If $S$ has for its last conclusion $p$ the output of a daimon link then we can add a $\mathfrak{N}$-link to $S$ and duplicate the conclusion $p$ obtaining $S+l$ and ensure that $S+l$ belongs to $[[A \mathfrak{N} B]]_{\mathcal{B}}$. Then since a daimon link can simulate a well-formed $\mathfrak{N}$-link below a daimon this implies that $S$ belongs to $[[A \mathfrak{N} B]]_{\mathcal{B}}$. For the case of $[[A \otimes B]]_{\mathcal{B}}(X \mapsto R)$ the argument is similar.

* The base together with the third case allow us to show the property hold for any hypersequent of measure $(c, 1)$. This together with the first and second case allows us to show it hold for any hypersequent of measure $(c, n)$.

□

**THEOREM 6.2 (ADEQUACY FOR MLL<sub>2</sub>).* Given $S$ a proof in MLL<sub>2</sub> of a sequent $\Gamma$. For any regular interpretation basis $\mathcal{B}$, $S \in [[\Gamma]]_{\mathcal{B}}$.

**PROOF.** of Theorem 6.2. Assume $S$ represents a proof $\pi$ of $\Gamma$. We proceed by induction on $\pi$ looking at the last rule of $\pi$.

* If $\pi$ is an axiom rule then $\pi$ is a proof of a sequent $A, A^{\perp}$ for some formula $A$. On the other hand $S$ is of the form $\langle \triangleright_{\mathfrak{A}}, p, q \rangle$ e.g. corresponds to $\mathfrak{A}_2$. The proposition 4.2 ensures that $\mathfrak{A}_2$ belongs to $A \to A^{\perp}$ for any type $A$ hence it belongs to $[[X, X^{\perp}]_{\mathcal{B}}$ for any basis $\mathcal{B}$.

* If the last rule of $\pi$ is the introduction of a $\mathfrak{N}$ connective or a tensor connective we reason as in the proof of MLL adequacy.

* If the last rule of $\pi$ is an existential quantifier, then $S$ can be decomposed as $S_0 + l$ where $l$ is the existential link corresponding to the last rule of $\pi$. Then $S$ is a proof of $\Gamma, \exists X A$ and $S_0$ is a proof of $\Gamma, A$.

$S_0$ is a representation of a smaller proof than $S$, thus we can apply the induction hypothesis on $S_0$ and claim that $S_0$ belongs to $[[\Gamma, A]]_{\mathcal{B}}$ for any basis $\mathcal{B}$. This means that for any $\gamma$ in $[[\Gamma]^{\perp}_{\mathcal{B}}$ the interaction $S_0 :: \gamma$ belongs to $[[A]]_{\mathcal{B}}$. Therefore $S_0 :: \gamma$ belongs to $\cup_{R \in \Omega} [[A]]_{\mathcal{B}}(X \mapsto R)$ and so to

$$(\cup_{R \in \Omega} [[A]]_{\mathcal{B}}(X \mapsto R))^{\perp\perp}$. As a consequence $S_0 :: \gamma + l$ e.g. $S_0 + l :: \gamma$ which is $S :: \gamma$, belongs to $[[\exists X A]]_{\mathcal{B}}$.

Since $\gamma$ range in $[[\Gamma]^{\perp}_{\mathcal{B}}$ we can conclude that $S$ belongs $[[\Gamma, \exists X A]]_{\mathcal{B}}$. Indeed this hold for any interpretation basis $\mathcal{B}$.

* If the last rule of $\pi$ is the introduction of a universal quantifier. Then $S$ can be decomposed as $S_0 + l$ where $l$ is the link corresponding to the universal quantification. $S_0$ is a proof of $\Gamma, A$ and furthermore since we can apply a universal quantification, $X$ does not occur free in $\Gamma$.

Applying the induction hypothesis $S_0$ belongs to $[[\Gamma, A]]_{\mathcal{B}}$ for any basis $\mathcal{B}$. In particular for any type $R$, the net $S_0$ belongs to $[[\Gamma, A]]_{\mathcal{B}}(X \mapsto R)$. This means that $S_0$ belongs to the intersection $\cap_{R \in \Omega} [[\Gamma, A]]_{\mathcal{B}}(X \mapsto R)$ which is $\cap_{R \in \Omega} [[\Gamma]]_{\mathcal{B}}(X \mapsto R) > [[A]]_{\mathcal{B}}(X \mapsto R)$.

As a consequence, for any type $R$, for any net $\gamma$ in $[[\Gamma]^{\perp}_{\mathcal{B}}(X \mapsto R)$ the interaction $S_0 :: \gamma$ belongs to $[[A]]_{\mathcal{B}}(X \mapsto R)$. Since the universal quantification can be applied $X$ does not occur free in the sequent $\Gamma$ and thus calling proposition F.1 $[[\Gamma]^{\perp}_{\mathcal{B}}(X \mapsto R)$ is equal to $[[\Gamma]^{\perp}_{\mathcal{B}}$. Thus we have showed that $S_0$ belongs to $[[\Gamma]]_{\mathcal{B}} > [[A]]_{\mathcal{B}}(X \mapsto R)$ for any type $R$. Hence $S_0$ belongs to

$[[\Gamma]]_{\mathcal{B}} > \cap_{R \in \Omega} [[A]]_{\mathcal{B}}(X \mapsto R)$ which is $[[\Gamma, \cap_{X \in \Omega} A]]_{\mathcal{B}}$. We can therefore conclude that $S$ belongs to $[[\Gamma, \forall X A]]_{\mathcal{B}}$.

□

# G COMPLEMENTS TO SECTION 7

## G.1 Measures of Types

**Definition G.1.** The size of an interface $\sigma \subseteq \text{out}(S) \times \text{out}(T)$ is its cardinal.

**Definition G.2.** A measure is a map $\mu : \text{Mod} \to \mathbb{R}$ which is invariant under cut elimination. The weight of a measure is the value of $\mu(\mathfrak{A}_0)$, we denote it $w(\mu)$. The measure of an interface $\sigma$ is the measure of the module $\sum_{(p,q) \in \sigma} \langle p, q \triangleright_{\text{cut}} \rangle$, it is denoted $\mu(\sigma)$. A measure is;

* linear whenever $\mu(S \parallel T) = \mu(S) + \mu(T)$, for any modules $S$ and $T$.

* stable whenever two interface $\sigma$ and $\sigma'$ of the same size have the same measure $\mu(\sigma) = \mu(\sigma')$.

**PROPOSITION G.3.** Given a linear and stable measure $\mu$, for any two nets $S$ and $T$ with $n$ outputs;

$$S \perp T \Rightarrow \mu(S) + \mu(T) + \mu(id_n) = w(\mu).$$

**PROPOSITION G.4.** Given a linear and stable measure $\mu$, and a type $A$ such that $A$ and $A^{\perp}$ are both non empty;

* All the nets in $A$ have the same measure.

* All the nets in $A^{\perp}$ have the same measure.

**PROOF.** For any pair of nets $S$ and $T$ which belongs respectively to $A$ and $A^{\perp}$ the equality hold $\mu(S) + \mu(T) + \mu(id_n) = w(\mu)$. Thus $\mu(S) = w(\mu) - (\mu(T) + \mu(id_n))$ and this must hold for any net in $A$, thus the measure is invariant on $A$.

Similarly any net in $A^{\perp}$ must verify $\mu(T) = w(\mu) - (\mu(S) + \mu(id_n))$. This means that $\mu$ is also invariant on $A^{\perp}$. □

**Definition G.5 (compatible measures).** Two nets $S$ and $T$ with $n$ outputs have compatible measures whenever;

$$\mu(S) + \mu(T) + \mu(id_n) = w(\mu)$$

The analogue notion is also defined for types.

**Definition G.6 (balanced type).** A type $A$ is balanced when $A$ and $A^{\perp}$ are both non empty. The measure $\mu(A)$ of a balanced type is the (unique) measure of the nets it contains. A balanced type is symmetrical whenever $\mu(A) = \mu(A^{\perp})$.

**Remark 53.** A symmetrical type $A$ with $n$ outputs must have the measure $1/2 \times (w(\mu) - \mu(id_n))$

**Definition G.7 (Separator).** A set of types $\{\mathcal{B}, \mathcal{B}^{\perp}\}$ is a separator for a measure $\mu$, whenever $\mathcal{B}$ is an asymmetrical balanced type.

**PROPOSITION G.8.** Let $\omega$ be a separator, and $\Gamma = \Delta, X^k, X^{\perp k'}$ a sequent where $X$ does not occur free in $\Delta$.

Given a daimon link $\mathfrak{A}_n = \langle \triangleright_{\mathfrak{A}}, p_1, \dots, p_n \rangle$ if $\mathfrak{A}_n$ belongs to $[[\cap_{X \in \omega} \Gamma]]_{\mathcal{B}}$ then $\Gamma$ contains the same number of atomic variable $X$ and $X^{\perp}$.

2959

2960

2961

2962

2963

2964

2965

2966

2967

2968

2969

2970

2971

2972

2973

2974

2975

2976

2977

2978

2979

2980

2981

2982

2983

2984

2985

2986

2987

2988

2989

2990

2991

2992

2993

2994

2995

2996

2997

2998

2999

3000

3001

3002

3003

3004

3005

3006

3007

3008

3009

3010

3011

3012

3013

3014

3015

3016
**PROOF.** Say $\omega = \{\mathbf{B}, \mathbf{B}^{\perp}\}$. We denote $k$ (resp. $k'$) the number of occurence of $X$ (resp. $X^{\perp}$) in $\Gamma$. By assumption $\mathbf{X}_n$ belongs to $[\Gamma]\mathcal{B}\{\mathbf{X}_n\}$ and so it is orthogonal to $[A_1]\mathcal{B}\{\mathbf{X}_1\} \| \cdots \| [A_n]\mathcal{B}\{\mathbf{X}_n\}$. The measure of that set is the sum $\sum_{1 \le i \le n} \mu([A_i]\mathcal{B}\{\mathbf{X}_i\})$ indeed this writting $\Gamma$ as $B_1, \dots, B_m, X^k, X^{\perp k'}$ where each $B_i$ is a formula that does not contain free occurences of $X$ or $X^{\perp}$, the previous sum is equal to,

$$ \sum_{1 \le i \le m} \mu(\llbracket B_i \rrbracket_{\mathcal{B}\{X \mapsto B\}}) + k \times \mu(\llbracket X \rrbracket_{\mathcal{B}\{X \mapsto B\}}) + k' \times \mu(\llbracket X^{\perp} \rrbracket_{\mathcal{B}\{X \mapsto B\}}) $$

Which indeed is

$$ \sum_{1 \le i \le m} \mu(\llbracket B_i \rrbracket_{\mathcal{B}\{X \mapsto B\}}) + k \times \mu(\mathbf{B}) + k' \times \mu(\mathbf{B}^{\perp}) $$

Since $X$ does not occur free in $B_1, \dots, B_n$ calling proposition F.1, in particular this is equal to

$$ \sum_{1 \le i \le m} \mu(\llbracket B_i \rrbracket_{\mathcal{B}}) + k \times \mu(\mathbf{B}) + k' \times \mu(\mathbf{B}^{\perp}) $$

Furthtermore $\mathbf{X}_n$ also belongs to $[\Gamma]\mathcal{B}\{\mathbf{X}_n\}$, applying the same argument this means that its measure is also equal to;

$$ \sum_{1 \le i \le m} \mu(\llbracket B_i \rrbracket_{\mathcal{B}}) + k \times \mu(\mathbf{B}^{\perp}) + k' \times \mu(\mathbf{B}). $$

Since the two sums must be equal it follows that

$$ k \times \mu(\mathbf{B}^{\perp}) + k' \times \mu(\mathbf{B}) = k \times \mu(\mathbf{B}) + k' \times \mu(\mathbf{B}^{\perp}) $$

and thus

$$ k' \times \mu(\mathbf{B}) - k' \times \mu(\mathbf{B}^{\perp}) = k \times \mu(\mathbf{B}) - k \times \mu(\mathbf{B}^{\perp}) $$

Indeed we can rewrite this

$$ k \times (\mu(\mathbf{B}) - \mu(\mathbf{B}^{\perp})) = k' \times (\mu(\mathbf{B}) - \mu(\mathbf{B}^{\perp})) $$

Since the type $\mathbf{B}$ is asymmetrical the difference of the measure is not null it follows that we can divide both sides by the differences of the measure and conclude $k = k'$. In other words in $\Gamma$ the propositional variable $X$ occurs as many times as $X^{\perp}$ occurs.

**Remark 54.** The previous proposition in particular applies to any sequent constituted only of propositional variable. In fact this generalizes to any atomic hypersequent of the form $\Gamma_1 \parallel \cdots \parallel \Gamma_n$. This is because $[\cap_{X \in \omega} \mathcal{H}_1 \parallel \mathcal{H}_2]\mathcal{B}$ is equal to $[\cap_{X \in \omega} \mathcal{H}_1]\mathcal{B} \parallel [\cap_{X \in \omega} \mathcal{H}_2]\mathcal{B}$ so a simple induction can be performed.

**Definition G.9.** The switching measure of a net $S$ corresponds to the integer $N(S) - E(S)$ where $N(S)$ is the number of nodes of the switching graphs of $S$ and $E(S)$ is the number of edges of the switching graphs of $S$.

**PROPOSITION G.10.** The switching measure is a linear and stable measure of weight 1.

## G.2 Properties of Intersection and Union

**PROPOSITION G.11.** Given $(A_i)_{i \in I}$ a family of types;

* The intersection $\cap_{i \in I} A_i$ is still a type.

* $(\cup_{i \in I} A_i)^{\perp}$ is equal to $\cap_{i \in I} A_i^{\perp}$.

* $(\cap_{i \in I} A_i)^{\perp}$ is equal to $(\cup_{i \in I} A_i^{\perp})^{\perp}$.

**PROOF.** We treat each point independently;

* For any index $i$ the intersection $\cap_{i \in I} A_i$ is included in the type $A_i$. Since orthogonality invert the inclusion of sets this implies $A_i^{\perp}$ is contained in $(\cap_{i \in I} A_i)^{\perp}$.

Therefore a net $S$ which is orthogonal to $(\cap_{i \in I} A_i)^{\perp}$, is also orthogonal to $A_i^{\perp}$ for any index $i \in I$. This means that $S$ belongs to $A_i^{\perp}$ which since we consider a family of types is exactly $A_i$.

Thus we showed that $(\cap_{i \in I} A_i)^{\perp}$ is included in $\cap_{i \in I} A_i$. Since the other inclusion always hold we conclude.

* Let $S$ be a net in $\cap_{i \in I} A_i^{\perp}$. For any index $i$ and any net $a$ in $A_i$ the net $S$ is orthogonal to $a$. This shows that $S$ belongs to $(\cup_{i \in I} A_i)^{\perp}$ and thus the first inclusion hold.

On the other hand let $S$ be a net orthogonal to $\cup_{i \in I} A_i$ then in particular for any type $A_i$ the net $S$ is orthogonal to $A_i$ and so belong to $A_i^{\perp}$. This means that $S$ belongs to $\cap_{i \in I} A_i^{\perp}$.

* This is a direct consequence of the previous point. $(\cap_{i \in I} A_i)^{\perp}$ corresponds to $(\cap_{i \in I} A_i^{\perp})^{\perp}$ and thus to $(\cup_{i \in I} A_i^{\perp})^{\perp}$. □

**PROPOSITION G.12.** Given $(A_i)_{i \in I}$ a family of sets of nets with the same number of outputs;

* $(\cap_{i \in I} A_i)^{\perp}$ is equal to $(\cap_{i \in I} A_i^{\perp})^{\perp}$.

* $(\cup_{i \in I} A_i)^{\perp}$ is equal to $(\cup_{i \in I} A_i^{\perp})^{\perp}$.

**PROOF.** We treat both cases independently;

* The inclusions $A_i \subseteq A_i^{\perp}$ always hold thus the intersections are included $\cap_{i \in I} A_i \subseteq \cap_{i \in I} A_i^{\perp}$. Since orthogonality inverts inclusion it follows that $(\cap_{i \in I} A_i^{\perp})^{\perp} \subseteq (\cap_{i \in I} A_i)^{\perp}$. On the other hand, consider $S$ a net orthogonal to $(\cap_{i \in I} A_i)$ e.g. belonging to $\cup_{i \in I} A_i^{\perp}$. Hence, for any index $i$, $S$ is orthogonal to $A_i$, in particular then $S$ is orthogonal to any net which belong to $\cap_{i \in I} A_i$.

Thus any net orthogonal to $(\cap_{i \in I} A_i)^{\perp}$ is orthogonal to $S$. Hence we have showed the inclusion $(\cup_{i \in I} A_i^{\perp})^{\perp} \subseteq (\cap_{i \in I} A_i)^{\perp}$. Since orthogonality inverts inclusion this yields the inclusion $(\cap_{i \in I} A_i)^{\perp} \subseteq (\cup_{i \in I} A_i^{\perp})^{\perp}$.

Hence using the previous point we obtained,

$$ (\cap_{i \in I} A_i)^{\perp} = (\cup_{i \in I} A_i^{\perp})^{\perp} = (\cap_{i \in I} A_i^{\perp})^{\perp} $$

* One of the inclusion is trivial namely $(\cup_{i \in I} A_i)^{\perp}$ contains $(\cup_{i \in I} A_i^{\perp})^{\perp}$.

On the other hand say a net $S$ belongs to $(\cup_{i \in I} A_i)^{\perp}$, then for any index $i$ the net $S$ is orthogonal to $A_i$, and so belongs to $A_i^{\perp}$. Since this is true for any index $i$ this means that $S$ belongs to $\cap_{i \in I} A_i^{\perp}$ which corresponds to $(\cap_{i \in I} A_i^{\perp})^{\perp}$ and thus to $(\cup_{i \in I} A_i^{\perp})^{\perp}$. Thus we have shown:

$$ (\cup_{i \in I} A_i)^{\perp} = (\cup_{i \in I} A_i^{\perp})^{\perp}. $$
3133

3134

3135

3136

3137

3138

3139

3140

3141

3142

3143

3144

3145

3146

3147

3148

3149

3150

3151

3152

3153

3154

3155

3156

3157

3158

3159

3160

3161

3162

3163

3164

3165

3166

3167

3168

3169

3170

3171

3172

3173

3174

3175

3176

3177

3178

3179

3180

3181

3182

3183

3184

3185

3186

3187

3188

3189

3190

**Remark 55.** A consequence of proposition G.11 is that the intersections of types are still types. Thus this set-theoretic operation is a valid construction on types. Later on, intersections (and unions) will appear in order to define the realizers of quantified formulas.

**Remark 56.** The (finite) union of types on the contrary is not guaranteed to still be a type. For instance in the case of two types A and B that don't cover the whole set of nets, and such that their orthogonals don't intersects.

The inclusion of $A \cup B$ in $(A \cup B)^{\perp\perp}$ is always guaranteed. On the other hand, using proposition G.11 the opposite inclusion would mean in particular that $(A^{\perp} \cap B^{\perp})^{\perp}$ is included in $A \cup B$. Using our assumption that would mean that $\emptyset^{\perp}$ is included in the union of A and B. Since $\emptyset^{\perp}$ is the whole set of nets this would mean that $A \cup B$ covers the whole set of nets, this goes against our assumption.

As a consequence we cannot have a 'De Morgan' law for set-constructions e.g. the equality of $(A \cap B)^{\perp}$ and $A^{\perp} \cup B^{\perp}$. Since on one hand $(A \cap B)^{\perp}$ is guaranteed to be a type while $A^{\perp} \cup B^{\perp}$ can fail to be a type.

**Remark 57.** Finally we point out that the proposition G.11 affirms that for two types $(A^{\perp} \cup B^{\perp})^{\perp}$ corresponds to $A^{\perp \perp} \cap B^{\perp \perp}$ and thus to $A \cap B$. Applying orthogonality this yields that $(A \cap B)^{\perp}$ corresponds to $(A^{\perp} \cup B^{\perp})^{\perp \perp}$.

## G.3 Proofs of Section 7

*Definition G.13 (computable type).* A type is computable whenever there exists a finite set B such that $A = B^{\perp}$.

**PROPOSITION 7.2.** *The functional composition $A \succ B$ and the parallel composition $A \parallel B$ of two syntactically computable types are syntactically computable.*

**OF THE FIRST STATEMENT.** Consider two types A and B which are finitely testable, this means there exists two finite sets of nets $X_A$ and $X_B$ such that $A = X_A^{\perp}$ and $B = X_B^{\perp}$. The following set of nets is still finite and of cardinality $card(X_A) \times card(X_B)$;

$$X = \{a \mid b \mid a \in X_A, b \in X_B\}$$

Furthermore $X^{\perp}$ corresponds to the orthogonal $(X_A \parallel X_B)^{\perp}$. By duality this type is equal to $X_A^{\perp} \succ X_B^{\perp}$ identifying A and B this corresponds to $A \succ B$. $\square$

**Notation 23.** Given a sequent $\Gamma = A_1, \dots, A_n$ we denote $\Gamma$ the sequent $\overline{A_1}, \dots, \overline{A_n}$.

**PROPOSITION 7.2.** *The functional composition $A \succ B$ and the parallel composition $A \parallel B$ of two syntactically computable types are syntactically computable.*

**OF THE SECOND STATEMENT.** Consider S with conclusion $p_1, \dots, p_n, q_1, \dots, q_m$ some net in $A \parallel B$ witnessing $\Gamma, \Delta$ such that the n first conclusions correspond to $\Gamma$ and the remaining conclusions correspond to $\Delta$.

Consider the set $A(\Gamma) \succ B(\Delta)$. for any net T in that merge the interaction S :: T is made only of glueing and multiplicative cuts. If S is orthogonal to $A(\Gamma) \succ B(\Delta)$, the conclusions $p_i$ and $q_i$ of S are not related by a daimon link. Otherwise a cycle can be created while interacting with a well chosen merge. Hence S can be written as $a(p_1, \dots, p_n) \parallel b(q_1, \dots, q_m)$. Given some merge $a' \succ b'$ then $a' \succ b'$ :: (a \parallel b) can be rewritten as $a' :: a \succ b'$ :: b.

Since the cuts involved in that interaction are all reversible we can ensure that a is orthogonal to $A(\Gamma)$ and b is orthogonal to $B(\Delta)$. $\square$

3191

3192

3193

3194

3195

3196

3197

3198

3199

3200

3201

3202

3203

3204

3205

3206

3207

3208

3209

3210

3211

3212

3213

3214

3215

3216

3217

3218

3219

3220

3221

3222

3223

3224

3225

3226

3227

3228

3229

3230

3231

3232

3233

3234

3235

3236

3237

3238

3239

3240

3241

3242

3243

3244

3245

3246

3247

3248

**PROPOSITION G.14.** *Given $(A_i)_{i \in I}$ a family of sets of nets with the same number of outputs;*

* $(\cap_{i \in I} A_i)^{\perp}$ is equal to $(\cap_{i \in I} A_i^{\perp \perp})^{\perp}$.

* $(\cup_{i \in I} A_i)^{\perp}$ is equal to $(\cup_{i \in I} A_i^{\perp \perp})^{\perp}$.

**PROOF.** We treat both cases independently;

* The inclusions $A_i \subseteq A_i^{\perp \perp}$ always hold thus the intersections are included $\cap_{i \in I} A_i \subseteq \cap_{i \in I} A_i^{\perp \perp}$. Since orthogonality inverts inclusion it follows that $(\cap_{i \in I} A_i^{\perp \perp})^{\perp} \subseteq (\cap_{i \in I} A_i)^{\perp}$. On the other hand, consider S a net orthogonal to $\cup_{i \in I} A_i^{\perp}$ hence for any index i, S is orthogonal to $A_i$, in particular then S is orthogonal to any net which belong to $\cap_{i \in I} A_i$. Thus any net orthogonal to $(\cap_{i \in I} A_i)^{\perp}$ is orthogonal to S. Hence we have showed the inclusion $(\cup_{i \in I} A_i^{\perp})^{\perp} \subseteq (\cap_{i \in I} A_i)^{\perp \perp}$. Since orthogonality inverts inclusion this yields the inclusion $(\cap_{i \in I} A_i)^{\perp} \subseteq (\cup_{i \in I} A_i^{\perp})^{\perp \perp}$. Hence using the previous point we obtained,

$$ (\cap_{i \in I} A_i)^{\perp} = (\cup_{i \in I} A_i^{\perp})^{\perp \perp} = (\cap_{i \in I} A_i^{\perp \perp})^{\perp} $$

* One of the inclusion is trivial namely $(\cup_{i \in I} A_i)^{\perp}$ contains $(\cap_{i \in I} A_i^{\perp \perp})^{\perp}$. On the other hand say a net S belongs to $(\cup_{i \in I} A_i)^{\perp}$, then for any index i the net S is orthogonal to $A_i$, and so belongs to $A_i^{\perp}$. Since this is true for any index i this means that S belongs to $\cap_{i \in I} A_i^{\perp}$ which corresponds to $(\cap_{i \in I} A_i^{\perp})^{\perp \perp}$ and thus to $(\cup_{i \in I} A_i^{\perp \perp})^{\perp}$. Thus we have shown:

$$ (\cup_{i \in I} A_i)^{\perp} = (\cup_{i \in I} A_i^{\perp \perp})^{\perp} $$

**PROPOSITION 7.3.** *The union $(\cup_{i \in I} A_i)^{\perp \perp}$ of a family of computable types is computable. The intersection $\cap_{i \in I} A_i$ of a finite family of computable types is computable.*

**PROOF.** of proposition 7.3. We treat both cases independently.