§67.5 **Example** (Incorrect cut-elimination). We have the following reduction $S \rightsquigarrow^* S'$ of proof-structure:

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

The proof-structure $S$ is translated into $\Phi_S^{\text{comp}} :=$

$$[+5(\mathbf{1} \cdot X), +6(\mathbf{1} \cdot X)] + [+5(\mathbf{r} \cdot X), +6(\mathbf{r} \cdot X)] + [-5(X), -6(X)]$$

with the following dependency graph $\mathfrak{D}[\Phi_S^{\text{comp}}]$:

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

The cycles in $\mathfrak{D}[\Phi_S^{\text{comp}}]$ can be unfolded and it yields infinitely many saturated correct diagrams, all actualising into $[\cdot]$. We have $\mathbf{AEx}(\Phi_S^{\text{comp}}) = \sum_{i=1}^{\infty} [\cdot] = \mathbf{AEx}(\Phi_{S'}^{\text{comp}})$.

§67.6 In order to prove what we simulate correctly cut-elimination with execution of constellations, we will need to consider structural equivalences of constellations because there is an implicit re-addressing of atoms, as shown in Example 67.3.

§67.7 **Definition** (Structurally equivalent constellations). We say that two constellations $\Phi$ and $\Phi'$ are *structurally equivalent w.r.t. two sets of colours* $C$ and $D$, written $\Phi \simeq_S^{C,D} \Phi'$, when there is a bijection $\varphi : I_\Phi \to I_{\Phi'}$ such that $|I_{\Phi[i]}| = |I_{\varphi(\Phi[i])}|$ for all $i \in I_\Phi$. It is extended on rays and we require that $\Phi[i][j] \bowtie \Phi[i'][j']$ if and only if $\varphi(\Phi[i][j]) \bowtie \varphi(\Phi[i'][j'])$ for all $i \in I_\Phi$ and $j \in I_{\Phi[i]}$.

§67.8 **Example.** For instance $[X, +f(X)] + [-f(a)]$ and $[Y, -g(Y)] + [+g(h(X, X))]$ are structurally equivalent constellation. None of them are structurally equivalent to $[+f(X)] + [-f(a)]$.
<figure><img src="image_117.png" /><figcaption>(a) Case of an ax/cut cut with $v_0$ not connected to a cut.</figcaption></figure>

<figure><img src="image_118.png" /><figcaption>(b) Case of an ax/cut cut with $v_0$ connected to a cut.</figcaption></figure>

<figure><img src="image_119.png" /><figcaption>(c) Case of an ax/cut cut with $v_0$ connected to a cut.</figcaption></figure>

<caption>Figure 67.1: Illustration of the simulation of cut-elimination. We have $\mathcal{R}$ on the left-hand side and $\mathcal{S}$ on the right-hand side.</caption>
§67.9 **Lemma** (Simulation of cut-elimination). Let $\mathcal{R} := (V, E, \text{in}, \text{out}, \ell_E)$ be a proof-structure. If $\mathcal{R} \leadsto \mathcal{S}$ by eliminating $e_{\text{cut}}$, then $\text{AEx}(\Phi_{\mathcal{R}}^{\text{comp}}) \simeq_S \text{AEx}(\Phi_{\mathcal{S}}^{\text{comp}})$.

*Proof.* We show that we have $\llcorner \text{CSatDiags}(\Phi_{\mathcal{R}}^{\text{comp}}) \simeq \llcorner \text{CSatDiags}(\Phi_{\mathcal{S}}^{\text{comp}})$. By definition of proof-structures, we must have $\text{in}(e_{\text{cut}}) = (v_1, v_2)$ for $v_1, v_2 \in V$. Those vertices must be conclusions of some hyperedges $e_1, e_2 \in E$. By case analysis on $\ell_E(e_1)$ and $\ell_E(e_2)$. The cases are illustrated in Figure 67.1.

◇ **Ax/cut case** Assume $e_{\text{cut}}$ is an ax/cut cut with $\ell_E(e_1) = \text{ax}$ such that $\text{out}(e_1) = (v_0, v_1)$. There are two cases depending on if $v_0$ is related to another cut (which influences the presence of polarity in the translation of $v_0$).

• Assume $v_0$ is not related to a cut. This case is illustrated in Figure 67.1a. We have that $v_2$ must be conclusion of some proof-structure $\mathcal{R}'$ by definition of proof-structure (it cannot be related to a cut because cuts only relate premises). After cut-elimination, we expect to obtain $\mathcal{R}'$ in which $v_0$ is identified with $v_2$ (we can replace $v_2$ by $v_0$ for instance).

In $\Phi_{\mathcal{R}}^{\text{comp}}$, we have an axiom $[v_0(X), +v_1(X)]$, a cut $[-v_1(X), -v_2(X)]$, and $\Phi_{\mathcal{R}'}^{\text{comp}}$ in which there are rays $+v_2(t_1)$, ..., $+v_2(t_n)$ for all atoms reachable from the conclusion $v_2$ (by the translation of proof-structures). Those latter rays must be part of some star $\phi_i := [+v_2(t_i), r_i]$ for some ray $r_i$ by definition (because only axioms and cuts are translated, and they become binary stars). We then expect $\Phi_{\mathcal{S}}^{\text{comp}}$ to be $\Phi_{\mathcal{R}'}^{\text{comp}}\{v_2(t_i) := v_0(t_i)\}$, in which $\{v_2(t_i) := v_0(t_i)\}$ means that the rays $+v_2(t_i)$ are replaced by $v_0(t_i)$.

We reason on all diagrams $(G_\delta, \delta)$ of $\Phi_{\mathcal{R}}^{\text{comp}}$ which include $e_{\text{cut}}$ and $e_1$ (which is an axiom), i.e. if $G_\delta := (V_\delta, E_\delta, \text{end}_\delta)$ then there are some adjacent vertices $u, u' \in V_\delta$ such that $\delta(u) = [v_0(X), +v_1(X)]$ and $\delta(u') = [-v_1(X), -v_2(X)]$. By confluence of diagram contraction (cf. Corollary 49.36), we can contract edges in any order. We contract the link between $u$ and $u'$ and obtain (by fusion) a new star $[v_0(X), -v_2(X)]$, i.e. $(G_\delta, \delta) \rightsquigarrow (G_{\delta'}, \delta')$ with $G_{\delta'} := (V_{\delta'}, E_{\delta'}, \text{end}_{\delta'})$, $w \in V_{\delta'}$ and $\delta'(w)$ corresponding to $[v_0(X), -v_2(X)]$. This star $[v_0(X), -v_2(X)]$ is linked to the stars $\phi_i$ of $\Phi_{\mathcal{R}'}^{\text{comp}}$. By contracting this latter edge, we obtain $\sum_{i=1}^n [v_0(t_i), r_i]$ in a diagram $(G_{\delta''}, \delta'')$ such that $(G_{\delta'}, \delta') \rightsquigarrow (G_{\delta''}, \delta'')$. All other edges of $(G_{\delta''}, \delta'')$ and all other diagrams are exactly constructed from edges of $\mathfrak{D}[\Phi_{\mathcal{S}}^{\text{comp}}]$. It follows that $\Phi_{\mathcal{R}}^{\text{comp}}$ and $\Phi_{\mathcal{S}}^{\text{comp}}$ have the same diagrams, and in particular the same correct and saturated diagrams, i.e. $\llcorner \text{CSatDiags}(\Phi_{\mathcal{R}}^{\text{comp}}) \simeq \llcorner \text{CSatDiags}(\Phi_{\mathcal{S}}^{\text{comp}})$.

• Now assume $v_0$ is subject to a cut $e'_{\text{cut}} \in \text{Cuts}(\mathcal{R})$ such that $\text{out}(e'_{\text{cut}}) = (v'_0, v_0)$ for some $v'_0$ conclusion of a sub-proof-structure $\mathcal{R}_0$. This case is illustrated in Figure 67.1b. The vertex $v'_0$ is conclusion of some proof-structure $\mathcal{R}_1$ and the vertex $v_2$ is conclusion of some proof-structure $\mathcal{R}_2$. After cut-elimination, we obtain the cut $e'_{\text{cut}}$ between $v'_0$ and $v_0$ which is identified with $v_2$.
A difference with the previous case is that the vertex $v_0$ is translated into
$+v_0(X)$ since it is subject to a cut. We have that $\Phi_{\mathcal{R}}^{\text{comp}}$ contains an axiom
$[+v_0(X), +v_1(X)]$, two cuts $[-v'_0(X), -v_0(X)] + [-v_1(X), -v_2(X)]$, the con-
stellation $\Phi_{\mathcal{R}_1}^{\text{comp}}$ with rays $+v'_0(u_1), \dots, +v'_0(u_m)$ for all atoms reachable from
$v'_0$ and the constellation $\Phi_{\mathcal{R}_2}^{\text{comp}}$ with rays $+v_2(t_1), \dots, +v_2(t_n)$ for all atoms
reachable from $v_2$. As in the previous case, those rays $+v_2(t_i)$ must be part of
some star $\phi_i := [+v_2(t_i), r_i]$ for some ray $r_i$. After cut-elimination, we expect
$\Phi_S^{\text{comp}}$ to be $\Phi_{\mathcal{R}_1}^{\text{comp}} \uplus \Phi_{\mathcal{R}_2}^{\text{comp}}\{+v_2(t_i) := +v_0(t_i)\} + [-v'_0(X), -v_0(X)]$.

We apply exactly the same reasoning and the same diagram contractions are
in the previous case and obtain a diagram $(G_{\delta''}, \delta'')$ except that instead of
having stars $\phi_i := [v_0(t_i), r_i]$, we have stars $\phi'_i := [+v_0(t_i), r_i]$. We obtain
exactly $\Phi_{\mathcal{R}_1}^{\text{comp}} \uplus \Phi_{\mathcal{R}_2}^{\text{comp}}\{+v_2(t_i) := +v_0(t_i)\} + [-v'_0(X), -v_0(X)]$. All extensions
or other diagrams are those of $\Phi_S^{\text{comp}}$. It follows that $\Phi_{\mathcal{R}}^{\text{comp}}$ and $\Phi_S^{\text{comp}}$ have the
same diagrams.

Assume $e_{\text{cut}}$ is an ax/cut cut with $\ell_E(e_1) = \text{ax}$ such that $\text{out}(e_1) = (v_0, v_1)$. There
are two cases depending on if $v_0$ is related to another cut (which influences the
presence of polarity in the translation of $v_0$).

◇ **Par/tensor case** Assume $e_{\text{cut}}$ is a $\mathcal{Y}/\otimes$ cut with $\ell_E(e_1) = \mathcal{Y}$ and $\ell_E(e_2) = \otimes$ with $\text{in}(e_1) = (\vec{v_1}, \vec{v_1})$ and $\text{in}(e_2) = (\vec{v_2}, \vec{v_2})$. This case is illustrated in Figure 67.1c. The vertices $\vec{v_1}, \vec{v_1}, \vec{v_2}$, and $\vec{v_2}$ are conclusion of some proof-structure $\mathcal{R}'$. The resulting proof-structure after cut-elimination is $\mathcal{S} := (V', E', \text{in}', \text{out}', \ell_E')$ where $V' = V - \{v_1, v_2\}$, $E' = (E - \{e_{\text{cut}}\}) \cup \{e_{\text{cut}}^1, e_{\text{cut}}^2\}$ (we duplicated the cut $e_{\text{cut}}$) such that $\text{in}'(e_{\text{cut}}^1) = (\vec{e_1}, \vec{e_2})$, $\text{in}'(e_{\text{cut}}^2) = (\vec{e_1}, \vec{e_2})$ with $\text{in}'(x) = \text{in}(x)$ otherwise and $\text{out}'(x) = \text{out}(x)$.

We have that $\Phi_{\mathcal{R}}^{\text{comp}}$ corresponds to $\Phi_{\mathcal{R}'}^{\text{comp}} + [-v_1(X), -v_2(X)]$. The constellation $\Phi_{\mathcal{R}'}^{\text{comp}}$ contains rays $+v_1(\mathbf{1} \cdot t_i)$, $+v_1(\mathbf{r} \cdot u_i)$, $+v_2(\mathbf{1} \cdot v_i)$ and $+v_2(\mathbf{r} \cdot w_i)$ respectively coming from stars $\phi_i^1 := [+v_1(\mathbf{1} \cdot t_i), r_i^1]$, $\phi_i^2 := [+v_1(\mathbf{r} \cdot u_i), r_i^2]$, $\phi_i^3 := [+v_2(\mathbf{1} \cdot v_i), r_i^3]$ and $\phi_i^4 := [+v_1(\mathbf{r} \cdot t_i), r_i^4]$ (by definition of proof-structure). The constellation $\Phi_S^{\text{comp}}$ obtained after cut-elimination should be $\Phi_{\mathcal{R}'}^{\text{comp}}$ in which all terms $+v_1(\mathbf{1} \cdot t_i)$, $+v_1(\mathbf{r} \cdot u_i)$, $+v_2(\mathbf{1} \cdot v_i)$, $+v_2(\mathbf{r} \cdot w_i)$ are respectively replaced by $+\vec{v}_1(t)$, $+\vec{v}_1(t)$, $+\vec{v}_2(t)$ and $+\vec{v}_2(t)$. We also have the cuts $[-\vec{v}_1(X), -\vec{v}_2(X)] + [-\vec{v}_1(X), -\vec{v}_2(X)]$. Because of this replacement of function symbol, we cannot expect to have exactly $\Phi_S^{\text{comp}}$ after executing $\Phi_{\mathcal{R}}^{\text{comp}}$. We can only expect structural equivalence by $\simeq_S$. We hence show that the diagrams of $\Phi_{\mathcal{R}}^{\text{comp}}$ and those of $\Phi_S^{\text{comp}}$ are equal up to a change of symbols.

We reason on the diagrams of $\Phi_{\mathcal{R}}^{\text{comp}}$ which contain the cut $[-v_1(X), -v_2(X)]$ and
the stars $\phi_i^k$ for $i \in \{1, 2, 3, 4\}$. It is possible to construct two diagrams ($G_{\delta}^1, \delta_1$)
and ($G_{\delta}^2, \delta_2$) defined by $G_{\delta}^1 := (V_1, E_1, \mathbf{end}_1)$ and $G_{\delta}^2 := (V_2, E_2, \mathbf{end}_2)$ with:
• some $u, u' \in V_1$ with $\delta(u) = \delta(u') = [-v_1(X), -v_2(X)]$, some $u_i^1, u_i^3 \in V_1$ with $\delta(u_i^k)$ corresponding to $\phi_i^k$ and edges $e_i^1, e_i^3 \in E_1$ with $\mathrm{end}_1(e_i^1) = \{u, e_i^1\}$ and $\mathrm{end}_1(e_i^3) = \{u', e_i^3\}$.

• some $u, u' \in V_2$ with $\delta(u) = \delta(u') = [-v_1(X), -v_2(X)]$, some $u_i^2, u_i^4 \in V_1$ with $\delta(u_i^k)$ corresponding to $\phi_i^k$ and edges $e_i^2, e_i^4 \in E_2$ with $\mathrm{end}_2(e_i^2) = \{u, e_i^2\}$ and $\mathrm{end}_2(e_i^4) = \{u', e_i^4\}$.

Notice that we duplicated the cut into two vertices $u$ and $u'$ in order to satisfy the given constraints of term unification. The homomorphisms $\delta_1$ and $\delta_2$ are defined in the unique possible way. Those diagrams can be reunited or not depending on the other rays in $\mathcal{R}'$. We do not even need to do diagram contractions. We update $\delta(u)$ and $\delta(u')$ in both diagrams so that $\delta(u)$ and $\delta(u')$ respectively correspond to $[-\vec{v_1}(X), -\vec{v_2}(X)]$ and $[-\vec{v_1}(X), -\vec{v_2}(X)]$. In order to preserve the links induced by edges, we must replaced $+v_1(\mathbf{1} \cdot t_i)$, $+v_1(\mathbf{r} \cdot u_i)$, $+v_2(\mathbf{1} \cdot v_i)$, $+v_2(\mathbf{r} \cdot w_i)$ by $+\vec{v_1}(t)$, $+\vec{v_1}(t)$, $+\vec{v_2}(t)$ and $+\vec{v_2}(t)$ respectively. We obtain exactly diagrams which could be constructed in $\Phi_S^{\mathrm{comp}}$. All other edges must come from $\Phi_{\mathcal{R}'}^{\mathrm{comp}}$. It follows that all extensions of $(G_\delta^k, \delta_k)$ with $k \in \{1, 2\}$ or other diagrams not relating the edges and vertices of $\mathcal{R}$ previously mentioned must be constructed with edges of $\Phi_{\mathcal{R}'}^{\mathrm{comp}}$ in both $\Phi_{\mathcal{R}}^{\mathrm{comp}}$ and $\Phi_S^{\mathrm{comp}}$. It follows that they both have the same diagrams and hence the same correct and saturated diagrams (up to renaming of target stars for $\delta_1$ and $\delta_2$ while preserving connexions between rays). We finally have $\llcorner \mathrm{CSatDiags}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) \simeq \llcorner \mathrm{CSatDiags}(\Phi_S^{\mathrm{comp}})$. $\square$

**§67.10 Theorem (Simulation of reduction for proof-nets).** For an MLL+MIX proof-net $\mathcal{R}$ such that $\mathcal{R} \rightsquigarrow^* S$ with $S$ in normal form, we have $\mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) \simeq_S \Phi_S^{\mathrm{ax}}$.

*Proof.* By induction on the number $n$ of steps of cut-elimination.

◇ **Base case** Assume $n = 0$. It means that $\mathcal{R}$ is already in normal form ($\mathcal{R} \rightsquigarrow_0 \mathcal{R}$). Hence it has no cut and we trivially have $\Phi_{\mathcal{R}}^{\mathrm{comp}} = \Phi_{\mathcal{R}}^{\mathrm{ax}}$, hence $\mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) = \mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{ax}}) = \Phi_{\mathcal{R}}^{\mathrm{ax}}$.

◇ **Induction case** Assume $n = n' + 1$. By induction hypothesis, if $\mathcal{R} \rightsquigarrow^{n'} S$ then $\mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) = \Phi_S^{\mathrm{ax}}$. We have to show that if we have $\mathcal{R}_0 \rightsquigarrow \mathcal{R} \rightsquigarrow^{n'} S$ then $\mathrm{AEx}(\Phi_{\mathcal{R}_0}^{\mathrm{comp}}) = \Phi_S^{\mathrm{ax}}$. By Lemma 67.9 and $\mathcal{R}_0 \rightsquigarrow \mathcal{R}$, we have $\mathrm{AEx}(\Phi_{\mathcal{R}_0}^{\mathrm{comp}}) \simeq_S \mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}})$. By $\mathcal{R} \rightsquigarrow^{n'} S$ and the induction hypothesis, we have $\mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) = \Phi_S^{\mathrm{ax}}$. By transitivity of equality (up to the structural equivalence $\simeq_S$), we have $\mathrm{AEx}(\Phi_{\mathcal{R}_0}^{\mathrm{comp}}) \simeq_S \mathrm{AEx}(\Phi_{\mathcal{R}}^{\mathrm{comp}}) = \Phi_S^{\mathrm{ax}}$. $\square$

<figure><img src="image_120.png" /></figure>
## 68 Simulation of Danos-Regnier correctness test

**§68.1** The simulation of Danos-Regnier correctness is a direct translation of the approach of proofs as partitions of a set (cf. Section 37). Danos-Regnier tests (correctness hypergraphs without axioms) are translated by a constellation which simply reproduces the hypergraph structure of the test. In particular, it has no dynamics and is just designed to be plugged to a vehicle. For instance, the 3-ary tensor link relating two inputs $u, v$ to one output $w$ becomes a 3-ary star $[-u(X), -v(X), +w(X)]$. We translate conclusions of the whole proof-structure by uncoloured rays.

**§68.2** To make tests more readable, they will sometimes be written as *blocks* with inputs (rays of polarity $-$) above and outputs below (rays of polarity $+$). For instance, $[-u(X), -v(X), +w(X)]$ becomes $\begin{bmatrix} -u(X), -v(X) \\ +w(X) \end{bmatrix}$. Links are then connected like tiles or bricks, as in sequent calculus.

**§68.3** **Definition (MLL test).** Let $S$ be a proof-structure and $\varphi$ one of its switchings. The test associated with $S^\varphi$ is the constellation defined by

$$ \Phi_S^\varphi := \Phi_S^{\text{cut}} \uplus \sum_{v \in V^{S^\varphi}} v^\star. $$

where the translation $v^\star$ of a vertex $v$ conclusion of an hyperedge $e$ is defined as follows:

* if $\ell_E(e) = \text{ax}$ then $v^\star = \begin{bmatrix} -\text{addr}_S(v) \\ +v(X) \end{bmatrix}$;

* if $\ell_E(e) = \mathfrak{N}_L$ and $\text{in}(e) = (u, w)$ then $v^\star = \begin{bmatrix} -u(X) \\ +v(X) \end{bmatrix} + \begin{bmatrix} -w(X) \\ +v(X) \end{bmatrix}$;

* if $\ell_E(e) = \mathfrak{N}_R$ and $\text{in}(e) = (u, w)$ then $v^\star = \begin{bmatrix} -u(X) \\ +v(X) \end{bmatrix} + \begin{bmatrix} -w(X) \\ +v(X) \end{bmatrix}$;

* if $\ell_E(e) = \otimes$ and $\text{in}(e) = (u, w)$ then $v^\star = \begin{bmatrix} -u(X), -w(X) \\ +v(X) \end{bmatrix}$;

* if $v \in \text{Concl}(S)$ then $v^\star = \begin{bmatrix} -v(X) \\ v(X) \end{bmatrix}$.

**§68.4** Tests for a proof-structure $S$ are actually designed so that $\mathfrak{D}[\Phi_S^\varphi]$ is isomorphic to $S^\varphi$ without axioms, as illustrated in Figure 68.1. The point is that when constructing the union of a vehicle with a test, we obtain a constellation with a dependency graph structurally corresponding to a Danos-Regnier correctness hypergraph (cf. Definition 30.16). However, there is a minor technical problem. Imagine that we have a
<figure><img src="image_121.png" /><figcaption>Figure 68.1: Dependency graph of the constellation corresponding to Switching 2 in Figure 30.9.</figcaption></figure>

vehicle [+3(1·X), +3(r·X)] corresponding to a $\mathfrak{N}$ on two atoms, and a test corresponding to a switching $\mathfrak{N}_L$ with [-3(1·X), +1(X)] + [-3(r·X), +2(X)] + [-1(X), +3(X)] + [-2(X)] + [-3(X), 3(X)]. The problem is that the conclusion [-3(X), 3(X)] can technically interfere and connect with the vehicle. We only want the stars [-3(1·X), +1(X)] and [-3(r·X), +2(X)] to connect with atoms of the vehicle.

§68.5 Girard's solution is to use different colours to distinguish terms coming from the vehicle and terms coming from tests. We can do that by wrapping addresses +u(t) and -u(t) with a colour +v and -v to obtain +v(+u(t)) and -v(-u(t)). With these wrapped addresses, the other rays of the test cannot interact with the vehicle.

§68.6 I find this solution too cumbersome to write so I choose to *pre-execute* tests to obtain compact tests exactly translating partitions over the set of atoms, as in Section 37. Such compact tests are made of stars for each connected components linking inputs for atoms to unpolarised outputs corresponding to conclusions. In other words, the internal structure of tests does not matter, what is important is only the *visible interface* of tests and their organisation in terms of reunion/separation. For instance, the test of Figure 68.1 simply becomes:

$$ \begin{bmatrix} -5(1 \cdot X) & -5(r \cdot X) \\ 5(X) & \end{bmatrix} + \begin{bmatrix} -6(1 \cdot X) \\ \end{bmatrix} + \begin{bmatrix} -6(r \cdot X) \\ 6(X) \end{bmatrix}. $$

§68.7 The idea of the simulation of logical correctness is that we would like to make tests interact with a fully positively polarised vehicle to reproduce a Danos-Regnier correctness hypergraph (more precisely, the interaction between two partitions as in Section 37). In stellar resolution, testing is done with execution and we would like to obtain $[v_1(X), ..., v_n(X)]$ with $\text{Concl}(S) = \{v_1, ..., v_n\}$, ensuring all conclusions can be reached
<figure><img src="image_122.png" /><figcaption>Figure 68.2: Incorrect correctness hypergraph for a proof-structure $\mathcal{S}$ and its translation. Notice that the cycle is turned into a computational cycle (a loop in a program).</figcaption></figure>

(several connected components induce several stars in the normal form) only once (cycles are designed to produce several $v_i(X)$), hence the associated correctness hypergraph $\Phi_{\mathcal{S}}^{\varphi}$ is connected and acyclic as required by correctness criteria for MLL.

**§68.8 Example.** If we consider the test:

$$ \begin{bmatrix} -5(\mathbf{1} \cdot X) & -5(\mathbf{r} \cdot X) \\ 5(X) & \end{bmatrix} + \begin{bmatrix} -6(\mathbf{1} \cdot X) \\ \end{bmatrix} + \begin{bmatrix} -6(\mathbf{r} \cdot X) \\ 6(X) \end{bmatrix} $$

of Figure 68.1, we can plug it by union of constellation with the vehicle $[+5(\mathbf{1} \cdot X), +6(\mathbf{1} \cdot X)] + [+5(\mathbf{r} \cdot X), +6(\mathbf{r} \cdot X)]$ and obtain:

$$ [+5(\mathbf{1} \cdot X), +6(\mathbf{1} \cdot X)] + [+5(\mathbf{r} \cdot X), +6(\mathbf{r} \cdot X)] + \begin{bmatrix} -5(\mathbf{1} \cdot X) & -5(\mathbf{r} \cdot X) \\ 5(X) & \end{bmatrix} + \begin{bmatrix} -6(\mathbf{1} \cdot X) \\ \end{bmatrix} + \begin{bmatrix} -6(\mathbf{r} \cdot X) \\ 6(X) \end{bmatrix} $$

The first star $[+5(\mathbf{1} \cdot X), +6(\mathbf{1} \cdot X)]$ reunites the two first blocks and we obtain:

$$ [+5(\mathbf{r} \cdot X), +6(\mathbf{r} \cdot X)] + \begin{bmatrix} -5(\mathbf{r} \cdot X) \\ 5(X) \end{bmatrix} + \begin{bmatrix} -6(\mathbf{r} \cdot X) \\ 6(X) \end{bmatrix} $$

The star $[+5(\mathbf{r} \cdot X), +6(\mathbf{r} \cdot X)]$ of the vehicle reunites the two last blocks of the test and we obtain $[5(X), 6(X)]$. If the vehicle is “too small” or “too big”, it leaves unpolarised ray either in the test or in the vehicle. If we had a star $[+5(\mathbf{1} \cdot X), +5(\mathbf{r} \cdot X)]$ in the vehicle, it would form a cycle with the first block. This cycle yields infinitely many stars $[5(X)] + [5(X)] + ...$ by unfolding the cycle to construct as many cyclic diagrams as we wish.

**§68.9 The need for visible incorrectness.** Before expressing logical correctness in stellar resolution, I would like to mention an interesting error in Girard's original definition. In his original paper [Gir17, Section 2.3], Girard forbids cyclic diagrams and the empty star. However, if we accept his definition, cyclic proof-structures $\mathcal{S}$ will be reduced into the empty constellation $\emptyset$. But if we put such proof-structure next to a correct proof-structure $\mathcal{R}$, we have that $\mathcal{S} \uplus \mathcal{R}$ is correct. This not what we want.
<figure><img src="image_123.png" /><figcaption>Figure 68.3: Example of a correct and saturated cyclic diagram for the constellation from Figure 68.2 actualising into $[3(X_9), 3(X_{10})]$. The cycle can be extended infinitely many times by adding copies of three stars of the constellation.</figcaption></figure>

§68.10 I give more details about this problem. We write $\mathbf{AEx[RT]}$ for the execution restricted to tree-shaped diagrams used by Girard which applies the operator $\frown$ and $\searrow$. If we consider the correctness hypergraph of Figure 68.2, infinitely many diagrams can be constructed because of the loop in its dependency graph (an example of loop unfolding is given in Figure 68.3) but all the corresponding diagrams have free polarised rays. Such diagrams are erased by the operator $\frown$. Therefore, $\mathbf{AEx[RT]}(\Phi_S^{ax} \uplus \Phi_S^{\varphi}) = \emptyset$.

§68.11 The solution adopted in this thesis is to make incorrect proofs visible in the normal form. Our definition of execution makes this possible. Cycles yield cyclic diagrams, which are accepted. Since proof-structures are always translated into constellations with trivial equations, such diagrams can always be extended into cyclic diagrams which will be evaluated into infinitely many stars (as in Figure 68.3). This makes incorrectness visible in the output of execution.

§68.12 This problem is actually not new and already existed in previous GoI models. For instance, in Seiller's works, it was necessary to be able to detect cycles. The problem has been solved with a notion of *wager* which is a value associated with proofs indicating the presence of cycles but we were able to simulate this idea by modifying the notion of execution instead.

§68.13 We can now finally state the Danos-Regnier correctness criterion in stellar resolution.

§68.14 **Proposition.** If a connected multiplicative correctness hypergraph $S^\varphi$ has no conclusion then it is cyclic.
*Proof.* Since $S^\varphi$ has no conclusion, all vertices are source of exactly one hyperedge. By the definition of proof-structure, all vertices are target of exactly one hyperedge. Hence, all vertices have a degree at least 2. Assume there is no cycle. Since the hypergraph is connected, it must be tree-shaped. It follows that there is at least one leaf, *i.e.* a vertex of degree 1 which is incident to only one edge. However, this contradicts the fact that all vertices have a degree at least 2. □

**§68.15 Definition (Full head polarisation).** Let $\Phi$ be a constellation defined in a coloured signature $(V, F, \mathbf{ar}, \subset, [\cdot])$. Its full head polarisation is a constellation $\Phi^+$ defined by $I_+ := I_\Phi$, $\Phi^+[i] := \Phi[i]$ and:

* $\Phi[i][j] = f(r_1, ..., r_k)$ then, $\Phi^+[i][j] := +f(r_1, ..., r_k)$;

* $\Phi[i][j] = -c(r_1, ..., r_k)$ then, $\Phi^+[i][j] := +c(r_1, ..., r_k)$;

* $\Phi[i][j] = +c(r_1, ..., r_k)$ then, $\Phi^+[i][j] := +c(r_1, ..., r_k)$

where $F = F_0 \uplus F_- \uplus F_+$, $\{f, c\} \subseteq F_0$, $-c \in F_-$ and $+c \in F_+$.

**§68.16 Definition.** If $\Phi := [1(X), +2(X)] + [+3(X), +4(X)]$ then $\Phi^+ := [+1(X), +2(X)] + [+3(X), +4(X)]$.

**§68.17 Lemma (Structural equivalence of correctness hypergraphs).** Let $S^\varphi := (V, E, \mathbf{end}, \ell)$ be a correctness hypergraph for a switching $\varphi$ and let

$$ \mathcal{D}[\Phi_S^{\mathbf{ax}} \uplus \mathbf{AEx}(\Phi_S^{\varphi})] := (V_{\mathcal{D}}, E_{\mathcal{D}}, \mathbf{end}_{\mathcal{D}}) $$

be the dependency graph of its translation using Definition 69.15. There is a bijection $\rho: V \to V_{\mathcal{D}}$ preserving adjacency.

*Proof.* First, a way to understand the connexions in $\mathcal{D}[\Phi_S^{\mathbf{ax}} \uplus \mathbf{AEx}(\Phi_S^{\varphi})]$ is that they have the same connexions as $\mathcal{D}[\Phi_S^{\mathbf{ax}} \uplus \Phi_S^{\varphi}]$ except that rays of $\Phi_S^{\mathbf{ax}}$ cannot be connected to rays of $\Phi_S^{\varphi}$ except for the rays $-\mathbf{addr}_S(v)$.

Let $v \in V$ be a vertex representing a formula. Assume it is a conclusion of an hyperedge $e \in E$ (it is always the case by definition of proof-structure). If $\ell(e) \in \{\mathbf{ax}, \otimes\}$ or $e \in \mathbf{Concl}(S)$ then $\rho(v) := v^\star$ (cf. Definition 69.15). If $\ell(e) = \mathfrak{N}_L$ (resp. $\ell(e) = \mathfrak{N}_R$) then $\rho(v)$ is the left (resp. right) star of $v^\star$. Assume we have $v$ and $v'$ adjacent. A case analysis of all possible situations of adjacency shows that $\rho$ preserves adjacency. Moreover, $\rho$ associates vertices in a unique way. Without loss of generality, we consider the case of $v \in V$ conclusion of a hyperedge $e \in E$ with $\ell(e) = \otimes$ with a premise $v' \in V$ conclusion of
an axiom. Hence we have end(e) = {v, v', w} for some w ∈ V. The vertices v and v' will be translated into some star [−addr_S(v'), +v'(X)] and [−v'(X), −w(X), +v(X)]. The two stars can be linked along the rays +v'(X) and −v'(X) making them adjacent. □

§68.18 **Corollary.** Let $S^{\varphi}$ be a correctness hypergraph for a switching $\varphi$ and let $\mathfrak{D}[\Phi_S^{\varphi}]$ be the dependency graph of its translation by Definition 69.15.

We have that $S^{\varphi}$ is connected or acyclic if and only if $\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})$ is.

*Proof.* By Lemma 68.17, since we have a bijection $\rho$ preserving adjacency, we also preserve reachability and paths in the test. It follows that the set of cycles and connected components in $\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})$ is isomorphic to the cycles and connected components of $\mathfrak{D}[\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})]$. □

§68.19 **Theorem (Stellar correctness criterion).** A proof-structure $S$ such that $\text{Concl}(S) = \{v_1, \dots, v_n\}$ is MLL-certifiable (cf. Definition 30.3) if and only if for all switchings $\varphi$, we have:

$$AEx(\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})) = [v_1(X), \dots, v_n(X)].$$

*Proof.* We show two implications.

◇ (⇒) Assume $S$ is MLL-certifiable. Then there exists a vertex labelling $\ell$ making $S$ an MLL proof-net. By the Danos-Regnier correctness criterion (cf. Theorem 30.17), it means that for all switching $\varphi$ of $S$, we have a correctness hypergraph $S^{\varphi}$ which is connected and acyclic. By Corollary 68.18, $\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})$ must be connected and acyclic as well. In Definition 69.15, we see that all connexions in tests are between rays of identical underlying terms and that all rays are deterministic, making them perfect in the sense of Definition 62.15. It follows that $\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})$ is perfect. By the perfection lemma (cf. Lemma 62.16), we have a unique diagram. It is then sufficient to use a compression strategy as in Definition 63.2, i.e. we directly apply fusion between stars of the constellation. By pre-execution of $\Phi_S^{\varphi}$ we obtain a compact test translating the partition interpretation of Section 37. What axioms and cuts do is simply merging some blocks of the test together. The only rays left in the actualisation of the only diagram of $\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})$ are the unpolarised conclusions of the test, that is $v_1(X), \dots, v_n(X)$. We obtain the normal form $[v_1(X), \dots, v_n(X)]$.

◇ (←) Assume $AEx(\Phi_S^{\varphi} \unlhd AEx(\Phi_S^{\varphi})) = [v_1(X), \dots, v_n(X)]$. Assume by contradiction that $S^{\varphi}$ has at least two connected components. Assume that a component has no conclusion (because of cuts). Then, by Proposition 68.14, there is a cycle yielding infinitely many closed diagrams normalising into the empty star []. Hence, all
connected components must have free rays corresponding to conclusions. By the independence of connected component (cf. Lemma 62.17), we can independently execute each connected component. Since they correspond to deterministic and exact subconstellations, the normalisation produces the constellation $\phi_1+\dots+\phi_k$ for the $k$ connected components. It contradicts the hypothesis that we normalise into a single star. Therefore, $S^\varphi$ must be connected. Now, assume by contradiction that $S^\varphi$ is cyclic. The cycle can either yield a closed diagram actualising into the empty star [] or pass through a conclusion and produce infinitely many stars containing conclusion rays. In both case, the normalisation is different from $[v_1(X), \dots, v_n(X)]$, contradicting the hypothesis. Therefore, $S^\varphi$ must also be acyclic. This proves that $S^\varphi$ must be a tree for any switching $\varphi$, i.e. that $S$ is MLL-certifiable.

§68.20 The following corollary extends the logical correctness to MLL+MIX and suggests a more general variant which also captures MLL.

§68.21 **Corollary.** Let $S$ be a proof-structure and $\Phi := \Phi_S^{\text{ax}} \uplus \text{Ex}(\Phi_S^{\varphi})$ be the constellation corresponding to the correctness hypergraph $S^{\varphi}$ for some switching $\varphi$. We have:

* $S^\varphi$ is acyclic $\Leftrightarrow \mathcal{D}[\Phi]$ is acyclic $\Leftrightarrow |\text{Ex}(\Phi)| < \infty$;

* $S^\varphi$ is connected and acyclic $\Leftrightarrow \mathcal{D}[\Phi]$ is a deterministic tree $\Leftrightarrow |\text{Ex}(\Phi)| = 1$;

* $S^\varphi$ is connected and acyclic $\Leftrightarrow \Phi$ normalises into the star of its uncoloured rays.

*Proof.* The first equivalence of each point are direct consequences of Corollary 68.18. It only remains to show the last equivalences.

* If $\mathcal{D}[\Phi]$ is acyclic, then by Corollary 62.13, $|\text{Ex}(\Phi)| < \infty$ because $\Phi$ is finite. Now assume that $|\text{Ex}(\Phi)| < \infty$. The proof of Theorem 68.19 shows that the presence of cycles in correctness hypergraphs is linked to the generation of infinitely many correct saturated diagrams. Hence it cannot be both cyclic and strongly normalising and has to be acyclic.

* We start from the previous point and consider the additional property of connectedness. If $\mathcal{D}[\Phi]$ is also connected, then by perfection of $\Phi$ (cf. Definition 62.15), there is a single star in the normal form. Conversely, if $\Phi$ normalises into a single star, its dependency graph must be both connected and acyclic, otherwise we would end up with either several stars (cf. Theorem 68.19) or infinitely many correct saturated diagrams (since cycles are related to non-termination as stated in the previous point).

* The third case corresponds to an alternative characterisation of correct proof-structures. Assume $S^\varphi$ is connected and acyclic. Then $\mathcal{D}[\Phi]$ is a deterministic tree by the previous point. By definition, uncoloured rays are the only free rays in $\Phi$.
Since $\Phi$ is exact, it must produce a unique diagram corresponding to the cover tree of $\mathfrak{D}[\Phi]$. By definition, such a diagram reduces into the star of its free rays, hence the star of its uncoloured rays. Now, assume $\Phi$ normalises into the star of its uncoloured rays. The reasoning is the same as for the previous point.

□

§68.22 The problem of tests with cuts. There is a problem with cuts. Imagine that we have the proof-structure of Figure 66.2. Its executed test for $\mathfrak{N}_L$ is the constellation:

$$ \begin{bmatrix} -7(1 \cdot X), -8(1 \cdot X), -8(r \cdot X) \end{bmatrix} + \begin{bmatrix} -7(1 \cdot X) \end{bmatrix} + \begin{bmatrix} -3(X) \\ 3(X) \end{bmatrix} + \begin{bmatrix} -6(X) \\ 6(X) \end{bmatrix}. $$

But if we execute the constellation corresponding to this proof-structure in order to simulate cut-elimination, we obtain a constellation $[3(X), 6(X)]$ representing the normal form after cut-elimination. When fully polarised with $[+3(X), +6(X)]$ in order to test it for MLL correctness, it cannot even pass the test above. Hence, the fact of passing a test is not preserved by reduction as if we were reducing a $\lambda$-term $t$ into $u$, could assert $t: A$ but not $u: A$ (no preservation of typing, also called “subject reduction”).

§68.23 Conversely, imagine that we have the following tests for axioms:

$$ \begin{bmatrix} +3(X) \\ 3(X) \end{bmatrix} + \begin{bmatrix} +6(X) \\ 6(X) \end{bmatrix}. $$

It works for $[3(X), 6(X)]$ but not for the vehicle of the proof of Figure 66.2. As if a test for $\vdash A, A^\perp$ could not validate proof-structures containing cuts. It is like having to evaluate a $\lambda$-term of type $\vdash A \to A$ in order to even typecheck it and say that it behaves like an identity function. If the term is very big then it makes no sense to do that to simply associate a type. Imagine pushing a car to its limits in order to say that it can work as expected and that it is ready to be sold.

§68.24 However, this problem should not be seen as a limitation or a design defect. Consistently with the philosophy of transcendental syntax and the distinction between Usine and Usage, correctness tests should be applied on *cut-free* proof-structures only. It is only after that we can guarantee with more or less certainty that our cut-free objects will interact correctly by cut.

§68.25 Separating program (tested) and specification (test). A remark that I got several times is “you are trying to relate correctness criteria with program testing but your test is actually dependent of the program (vehicle)”. Yes, this is true. If you look at the definition of test in Definition 68.3, the translation of atoms in the test uses addresses of atoms in axioms. It is as if we were designing specific specifications for each programs instead of generic ones. Actually, the problem is that program (vehicle) and test are *intertwined* in proof-structures (as explained in Section 44). It is possible to define
tests directly from a sequent (corresponding to a specification), hence independently of a proof-structure (program) as we will see in the next section (Usine interpretation).

§68.26 **Finiteness of correctness checking.** Despite all the previous "marketing" of finiteness of reasoning in Chapter 6, we can see that in our definitions, cut-elimination and correctness checking can loop if we try to implement it with concrete or interactive execution. Loops in proof-structures always involve equations between terms containing common variables. For instance, $\phi := [+1(X), +2(X)] + [-1(X), -2(X), 3(X)]$ can be reduced to $\phi' := [+2(X), -2(X), 3(X)]$. In $\phi$, the connexion between $+1(X)$ and $-1(X)$ makes variables distinct (by $\alpha$-unification). However, in $\phi'$, the connexion between $+2(X)$ and $-2(X)$ involve exactly the same variable because they are part of the same star. It means that loops can be detected by looking for equations involving exactly the same variables. It is up to us to make such diagrams incorrect. We can also, like Girard, choose to consider only tree-shaped diagrams but Thomas Seiller and I wanted something more flexible (also because it is computationally more expressive as illustrated in Chapter 8).

## 69 Construction of multiplicative formulas

§69.1 As explained in Section 43, formulas should be defined as sets of constellations w.r.t. an orthogonality relation between constellations. In this section, I present the Usine and Usage interpretation of formulas in the case of stellar resolution.

§69.2 Corollary 68.21 suggests three orthogonality relations we call $\perp_{fin}$, $\perp^1$ and $\perp^R$ but others can be designed depending on what we want.

§69.3 **Convention.** In this section, we write Ex for AEx.

§69.4 **Definition (Orthogonality).** We define binary relations of orthogonality between two constellations $\Phi_1$ and $\Phi_2$ w.r.t. a set of colours $C \subseteq F_+ \uplus F_-$:

* $\Phi_1 \perp_C^{fin} \Phi_2$ when $|\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2)| < \infty$;

* $\Phi_1 \perp_C^1 \Phi_2$ when $|\mathrm{AEx}_C(\Phi_1 \uplus \Phi_2)| = 1$;

* $\Phi_1 \perp_C^R \Phi_2$ when $\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2) = \{\mathrm{Roots}(\Phi_1 \uplus \Phi_2)\}$ where $\mathrm{Roots}(\Phi)$ is the star of uncoloured rays in $\Phi$.

The orthogonal of a set of constellations $\mathbf{A}$ is defined by:

$$ \mathbf{A}^{\perp C} := \{\Phi \mid \forall \Phi' \in \mathbf{A}, \Phi \perp_C \Phi'\} $$

for a relation of orthogonality $\perp$.
§69.5 The orthogonality $⊥^R$ will be our favourite since it is very close to the correctness criterion used in stellar resolution. In particular, it forces a full connexion between vehicle and test, as in the proof-as-partitions approach. The other criteria are more lax. In particular, it is possible to have constellations which do not correspond to proof-structures in the orthogonal of tests. It can however be seen as a feature as well<fnref n="1" />.

§69.6 In order to allow typing for partial evaluations, the orthogonality relation $⊥_C$ has to be parametrised by a set of colours $C$ but we omit this parameter when considering all colours in $F$.

§69.7 The orthogonality $⊥^{fin}$ will define a fully complete model of MLL+MIX, while $⊥^1$ and $⊥^R$ (which captures more directly the correctness criterion for MLL) will define a fully complete model of MLL. However, those notions of orthogonality share most of the properties needed, and we therefore use the generic notation $⊥$ in the following to state results valid for all of them.

§69.8 **Lemma** (Invariance of orthogonality under execution). Let $\Phi$ and $\Phi'$ be constellations such that $\mathcal{R}_C(\Phi, \Phi') = \emptyset$ for a set of colours $C \subseteq F_+ \uplus F_-$. We have $\Phi \perp_C \Phi'$ if and only if $\mathbf{Ex}_C(\Phi) \perp_C \Phi'$ for $\perp_C \in \{\perp_C^1, \perp_C^{fin}, \perp_C^R\}$.

*Proof.* These relations are satisfied when $P(\mathbf{Ex}_C(\Phi \uplus \Phi'))$ is satisfied for some property $P$. By the lemma of partial pre-execution (cf. Lemma 64.9), we have $\mathbf{Ex}_C(\mathbf{Ex}_C(\Phi) \uplus \Phi') = \mathbf{Ex}_C(\Phi \uplus \Phi')$. Hence we have $P(\mathbf{Ex}_C(\Phi \uplus \Phi'))$ if and only if $P(\mathbf{Ex}_C(\mathbf{Ex}_C(\Phi) \uplus \Phi'))$, meaning that we have $\Phi \perp_C \Phi'$ if and only if $\mathbf{Ex}_C(\Phi) \perp \Phi'$. $\square$

§69.9 **Remark.** This does not invalidate the problem presented in Paragraph 68.22 despite the appearance because if we had cuts in $\Phi$, then both cuts and a test $\Phi'$ would want to connect with rays of $\Phi$. This contradicts the precondition $\mathcal{R}_C(\Phi, \Phi') = \emptyset$.

Usine interpretation

§69.10 In this section, we construct formulas by generalising logical correctness. In the Usine interpretation, we are interested in effective verification. I refer to Section 43 for the philosophy of Usine.

§69.11 **Definition** (Type label). A *type (label)* is an object $A$ associated to a finite set of constellations $\mathbf{Tests}(A)$ called its *tests*. We say that a constellation $\Phi$ is of type $A$ w.r.t. $⊥$ if and only if $\Phi \in \mathbf{Tests}(A)^{\perp}$.

<footnote n="1">¹I believe this is the opinion of Thomas Seiller.</footnote>
§69.12 Type labels appear in model checking [BK08]: given an automata $\Phi$ (or labelled transition system), we would like to know whether it satisfies a specification $S$ (often written as a formula of a logic called LTL or CTL). It is then possible to check if $\Phi$ satisfies $S$ by turning $\neg S$ into an automaton $\Phi_{\neg S}$ and verifying if $\mathcal{L}(\Phi) \cap \mathcal{L}(\Phi_{\neg S}) = \emptyset$, by analysing paths of the state graph of the automaton [HR04, Section 3.6.3]. This is similar to how we turn a sequent $\vdash \Gamma$ into a set of tests (defined as constellations) allowing us to label/certify a constellation as a proof of $A$. Moreover, the Danos-Regnier's tests can also be considered as proofs of $A^{\perp}$.

§69.13 The purpose of having finite set of tests is to make type checking computable. However, this only happens under some conditions such as the orthogonality relation being decidable. Even under these conditions, it is possible to “trick” tests so to create infinite loops and make effective type checking impossible. It shows that we need to consider testing w.r.t. a specific class of objects (for instance the universe of proof-structures) so to prevent such tricks to happen, consistently with the idea of *epidictics* explained in Section 44. In this restricted case, orthogonality is decidable as we can check for the presence of cycles in dependency graphs in finite time.

§69.14 The definition of orthogonality and interactive testing leads to a reformulation of correctness criterion, showing that MLL sequents define type labels by themselves, independently of a proof-structure. This is based on the fact that the bottom part of proof-structure corresponds to the syntax tree of a sequent which is already a sort of pre-typing constraining cut-elimination. By constructing a syntax hypergraph from a sequent, Definition 68.3 can be used.

§69.15 **Definition (Test of a sequent).** Let $\vdash \Gamma$ be a sequent of MLL where $\Gamma \subseteq \mathcal{F}_{\text{MLL}}$ and all variables are distinct. We define the syntax tree of an MLL formula $A$ inductively:

* $ST(X_i)$ and $ST(X_i^{\perp})$ are vertices labelled by $X_i$ and $X_i^{\perp}$ respectively;

* $ST(A \otimes B)$ is an hyperedge labelled by $\otimes$ linking the conclusion of $ST(A)$ and $ST(B)$ as sources and having a vertex labelled by $A \otimes B$ as target;

* $ST(A \not\otimes B)$ is an hyperedge labelled by $\not\otimes$ linking the conclusion of $ST(A)$ and $ST(B)$ as sources and having a vertex labelled by $A \not\otimes B$ as target.

The syntax hypergraph $ST(\vdash \Gamma)$ of $\vdash \Gamma$ is defined as the hypergraph disjoint union of all $ST(A_i)$ for $A_i \in \Gamma$. A switching (cf. Definition 30.16) $\varphi$ still applies on $ST(\vdash \Gamma)$ as for correction hypergraphs. We write $ST(\vdash \Gamma)^{\varphi}$ for the switching $\varphi$ applied on the syntax hypergraph $ST(\vdash \Gamma)$.

The test associated with the sequent $\vdash \Gamma$ and the switching $\varphi$ is defined as the constellation $\text{Test}(\vdash \Gamma)^{\varphi}$ such that $I_{\text{Test}(\vdash \Gamma)^{\varphi}} := V^{ST(\vdash \Gamma)^{\varphi}}$ (it is indexed by vertices of the syntax tree) and $\text{Test}(\vdash \Gamma)^{\varphi}[v] := v^{\star}$.

The set of tests associated with the sequent $\vdash \Gamma$ is defined by $\text{Tests}(\vdash \Gamma) := \{\text{Test}(\vdash \Gamma)^{\varphi} \mid \varphi \text{ is a switching of } ST(\vdash \Gamma)\}$.
<figure><img src="image_124.png" /><figcaption>Figure 69.1: We expect this proof-structure to be able to pass any test of Tests($\vdash X_1 \otimes X_2$, $X_1^\perp \not\cong X_2^\perp$). However, since the function symbols used in tests are not compatible with the ones of the proof-structure, we need a conversion of function symbols to allow interaction.</figcaption></figure>

§69.16 **Example.** We give the compact (executed) form of tests coming from some sequents with a given switching:

$$ \text{Tests}(\vdash A, A^{\perp})^{\varphi} := \left[ \begin{array}{c} -A(X) \\ A(X) \end{array} \right] + \left[ \begin{array}{c} -A^{\perp}(X) \\ A^{\perp}(X) \end{array} \right]; $$

$$ \text{Tests}(\vdash A^{\perp} \not\cong B^{\perp}, A \otimes B)^{\varphi} \quad (\varphi(\mathfrak{R}) = \mathfrak{R}_L) := $$

$$ \left[ \begin{array}{c} -A^{\perp}(X) \\ (A^{\perp} \not\cong B^{\perp})(X) \end{array} \right] + \left[ \begin{array}{c} -B^{\perp}(X) \end{array} \right] + \left[ \begin{array}{c} -A(X), -B(X) \\ (A \otimes B)(X) \end{array} \right]; $$

$$ \text{Tests}(\vdash A^{\perp} \not\cong B^{\perp}, A \otimes B)^{\varphi} \quad (\varphi(\mathfrak{R}) = \mathfrak{R}_R) := $$

$$ \left[ \begin{array}{c} -A^{\perp}(X) \\ \left(A^{\perp} \not\cong B^{\perp}\right)(X) \end{array} \right] + \left[ \begin{array}{c} -B^{\perp}(X) \\ (A \otimes B)(X) \end{array} \right]. $$

§69.17 We defined MLL sequents as type labels in the sense of Definition 69.11. However, there is a minor technical problem: arbitrary constellations may not match with the tests we defined because of a difference of function symbols, as illustrated in Figure 69.1.

§69.18 A solution is to use binary stars to rename some rays and allow a connexion. This corresponds to a sort of generalised cut allowing a trivial connexion between two rays. I call these stars *adapters* in reference to adapter cables (for instance HDMI to VGA or USB-C to USB-A).

§69.19 **Definition (Adapter).** Let $\Phi$ be a constellation. An *adapter* for $\Phi$ is a star $[r, r']$ where $op(r)$ and $op(r')$ are polarised rays of $\Phi$ such that $op(r) \not\prec op(r')$ (hence we artificially link two rays which could not be linked by using a star $[r, r']$).

§69.20 Notice that the translation of atomic formulas in Definition 69.15 actually corresponds to adapters between a vehicle and a test, hence tests were already independent of vehicles but hardwired adapters were linking vehicle and test in a proof-structure. This dependency is only artificial and appears when considering proof-structures as an entity which cannot be decomposed. This is the difference between soldered switches in keyboards and hot-swappable switches which can be replaced. In Figure 68.1 for instance,
the negative rays on the top are residuals of adapters which enforces a connexion with the vehicle.

"Transcendental syntax's Usine is proof-net theory without soldering components."

§69.21 **Proposition** (Correspondence between proof-structure tests and sequent tests). Let $\mathcal{S}$ be a cut-free proof-structure. For all switching $\varphi$ of $\mathcal{S}$, there exists an MLL sequent $\vdash \Gamma$ and a constellation of adapters $\Phi$ such that $\mathrm{Ex}(\Phi_{\mathcal{S}}^{\varphi}) = \mathrm{Ex}(\mathrm{Test}(\vdash \Gamma)^{\varphi} \uplus \Phi)$.

*Proof.* The constellation $\Phi_S^\varphi$ corresponds to the syntax forest of a sequent with exactly one premise removed for each $\mathcal{N}$ vertex. Hence, it naturally induces a sequent $\vdash \Delta$ and we define $\Gamma := \Delta$. The constellation $\mathrm{Test}(\vdash \Gamma)^\varphi$ structurally corresponds to $\Phi_S^\varphi$ without the upper rays $-u_i(t_i)$ which allows connexion with the vehicle $\Phi_S^{\mathrm{ax}}$. Apart from that, they both use the same translation function $(\cdot)^{\star}$ on vertices for correctness hypergraphs. Assume we have a star $[-v(t), +w(X)]$ translating the atom $w$ linked to some star $[-w(X), ...]$ in $\mathrm{Test}(\vdash \Gamma)^\varphi$. During the execution, they will merge into $[-v(t), ...]$. However, it is possible to construct $\Phi$ so to reproduce this step with an adapter $[-v(t), +A(X)]$ (by definition, the star $[-A(x), ...]$ which is isomorphic to $[-w(x), ...]$ must be present in $\Phi_S^\varphi$). Moreover, because of the structural equivalence between the two constellations, they only differ by conjugation. It is then possible to extend $\Phi$ so that $\mathrm{Test}(\vdash \Gamma)^\varphi$ is turned exactly into $\Phi_S^\varphi$. It follows that the two constellations must have the same normal form. $\square$

§69.22 **Definition** (Typing). We say that a constellation $\Phi$ is of type $\vdash \Gamma$, written $\vdash \Phi : \Gamma$ when $\Phi \in \mathrm{Ex}(\Phi_{\vdash \Gamma}^{\varphi} \uplus \Phi_{\mu})^{\perp}$ for a set of adapters $\Phi_{\mu}$ and all switchings $\varphi$ of $\vdash \Gamma$.

§69.23 **Proposition** (Reformulation of logical correctness). A cut-free proof-structure $\mathcal{S}$ is MLL-certifiable if and only if there exists a sequent $\vdash \Gamma$ and a constellation of adapters $\Phi$ such that $\vdash \Phi_S^{\mathrm{ax}} : \Gamma$ with $\perp \in \{\perp^1, \perp^R\}$. The same statement holds for MLL+MIX $w.r.t. \perp^{\mathrm{fin}}$.

*Proof.* By Proposition 69.21, there exist some sequent $\vdash \Gamma$ such that $\Phi_S^\varphi$ is simulated by $\Phi \uplus \mathrm{Test}(\vdash \Gamma)^\varphi$ for some constellation of adapters $\Phi$. By invariance of orthogonality under execution (cf. Lemma 69.8), this connexion is equivalent to a connexion between $\Phi_S^{\mathrm{ax}}$ and $\Phi_S^\varphi$. The orthogonality $\Phi_S^{\mathrm{ax}} \in \mathrm{Tests}(\vdash \Gamma)^\perp$ and the same statement for MLL+MIX ($w.r.t. \perp^{\mathrm{fin}}$) both hold by a direct consequence of Corollary 68.21. $\square$

§69.24 **Example.** From the sequent $\vdash A, A^{\perp}$, we can generate the only test $\begin{bmatrix} -A(X) \\ A(X) \end{bmatrix} + \begin{bmatrix} -A^{\perp}(X) \\ A^{\perp}(X) \end{bmatrix}$. It can be plugged to the vehicle $[+1(X), +2(X)]$ by using the adapters $[-1(X), +A(X)] + [-2(X), +A^{\perp}(X)]$. The normal form of the whole constellation is
$[A(X), A^{\perp}(X)]$, as expected.

§69.25 **The shape of vehicles.** Notice that in our interpretation, there is no assumption of the shape of vehicles. We are interested in constellations orthogonal to all tests of a given sequent. Consider the orthogonality $\perp^R$. If we have the two tests of Tests($\perp$-A$^{\perp}$ $\mathfrak{R}$ B$^{\perp}$, A $\otimes$ B) given in Example 69.16, it can be linked to the expected vehicle (with adapters applied):

$$[(A^{\perp} \mathfrak{R} B^{\perp})(\mathbf{l} \cdot X), +(A \otimes B)(\mathbf{l} \cdot X)] + [(A^{\perp} \mathfrak{R} B^{\perp})(\mathbf{r} \cdot X), +(A \otimes B)(\mathbf{r} \cdot X)]$$

but this also logically wrong vehicle would pass the test as well:

$$[(A^{\perp} \mathfrak{R} B^{\perp})(\mathbf{l} \cdot X), +(A \otimes B)(\mathbf{r} \cdot X)] + [(A^{\perp} \mathfrak{R} B^{\perp})(\mathbf{r} \cdot X), +(A \otimes B)(\mathbf{l} \cdot X)].$$

It means that we need another restriction to say that we would like to link “dual atoms”. These additional restrictions are not explored here because they corresponds to second-order considerations (epidictics).

§69.26 However, independently of sequents, there are some correct shapes of vehicles that we wish for and which can be made explicit. We say that those correctly shaped vehicles are *well-formed*. They are the ones which will be put against tests of sequents.

§69.27 **Definition (Well-formed vehicle).** Let $\Phi$ be a constellation defined in a coloured signature $(V, F, \mathbf{ar}, \prec, \lrcorner)$ with $F := F_0 \uplus F_+ \uplus F_-$. It is a *well-formed vehicle* if it is:

1. finite;

2. only made of binary stars $[f_i(t_i), f_j(t_j)]$;

3. all rays are disjoint, i.e. not $\alpha$-unifiable (this is actually a condition that Girard required for constellations in general [Gir17]);

4. for each $f_k$, we have $f_k \in F_+ \uplus F_0$;

5. there is at least one $f_k$ such that $f_k \in F_+$;

6. all $t_k$ are stacks of directions constructed in the following grammar:

$$t ::= X | \mathbf{l} \cdot t | \mathbf{r} \cdot X.$$

## Usage interpretation

§69.28 I refer to Section 43 for more details about the philosophy of Girard's Usage. Constellations are grouped into arbitrary sets called *pre-behaviours*, giving rise a notion of formula and *behaviours* will correspond to actual formulas of linear logic.
§69.29 **Definition (Pre-behaviour)**. A pre-behaviour **A** is a set of constellations.

§69.30 **Definition (Behaviour)**. A pre-behaviour **A** is a behaviour when there exists a pre-behaviour **B** such that $\mathbf{A} = \mathbf{B}^{\perp}$.

§69.31 **Lemma (Invariance of typing under execution)**. Let $\Phi$ be a constellation and $\mathbf{A}$ a behaviour such that $\mathfrak{m}_C(\Phi, \Phi') = \emptyset$ for all $\Phi' \in \mathbf{A}^{\perp}$. We have $\Phi \in \mathbf{A}$ if and only if $\mathrm{Ex}_C(\Phi) \in \mathbf{A}$.

*Proof.* If $\mathbf{A}$ is a behaviour then $\mathbf{A} = \mathbf{A}^{\perp\perp}$, meaning that $\mathbf{A}$ is characterised by some tests $\mathbf{A}^{\perp}$. Hence we have to show that $\Phi \perp_C \Phi'$ such that $\mathfrak{m}_C(\Phi, \Phi') = \emptyset$ for any $\Phi' \in \mathbf{A}^{\perp}$ if and only if $\mathrm{Ex}(\Phi) \perp_C \Phi'$. This is the consequence of the invariance of orthogonality under execution (cf. Lemma 69.8). □

§69.32 **Proposition (Bi-orthogonal closure)**. A pre-behaviour $\mathbf{A}$ is a behaviour if and only if $\mathbf{A} = \mathbf{A}^{\perp\perp}$.

*Proof.* The proof can be found in the literature [JS21, Proposition 15]. □

§69.33 **Definition (Disjointness of behaviours)**. Let $\mathbf{A}$ and $\mathbf{B}$ be two behaviours and a set of colours $C \subseteq F_+ \uplus F_-$. They are disjoint when for all $\Phi_A \in \mathbf{A}$ and $\Phi_B \in \mathbf{B}$, we have $\mathfrak{m}_C(\Phi_A, \Phi_B) = \emptyset$.

§69.34 When two behaviours $\mathbf{A}$ and $\mathbf{B}$ are disjoint, for any pair of constellations $\Phi_A \in \mathbf{A}$ and $\Phi_B \in \mathbf{B}$, there is no path from one constellation to the other in $\mathfrak{D}[\Phi_A \uplus \Phi_B]$.

§69.35 **Definition (Pre-tensor)**. Let $\mathbf{A}$ and $\mathbf{B}$ be disjoint pre-behaviours. We define their pre-tensor by $\mathbf{A} \odot \mathbf{B} = \{\Phi_1 \uplus \Phi_2 \mid \Phi_1 \in \mathbf{A}, \Phi_2 \in \mathbf{B}\}$.

§69.36 **Definition (Tensor)**. Let $\mathbf{A}$ and $\mathbf{B}$ be disjoint behaviours. We define their tensor by

$$ \mathbf{A} \otimes \mathbf{B} = (\mathbf{A} \odot \mathbf{B})^{\perp\perp}. $$

§69.37 The pre-tensor is the natural definition of tensor product pairing constellations of two pre-behaviours. The real tensor product adds a bi-orthogonal closure $(\cdot)^{\perp\perp}$ in order to ensure that we get a behaviour (it is not necessarily the case without the closure, depending on the orthogonality we consider). It is indeed a generalisation of the usual tensor because, depending on the orthogonality relation, its orthogonal can contain way more than what we expect from proof-structures because of the huge space of objects provided by stellar resolution. In case $\mathbf{A} \odot \mathbf{B} = \mathbf{A} \otimes \mathbf{B}$, we say that *internal completeness* holds for tensor.
<figure><img src="image_125.png" /><figcaption>Figure 69.2: Counter-example of non-associativity which is variant of Figure 64.1. We have $\mathrm{Ex}_{\{c\}}(\Phi_1 \uplus \Phi_2) = [1 \cdot X]$ and $\mathrm{Ex}_{\{c\}}(\mathrm{Ex}_{\{c\}}(\Phi_1 \uplus \Phi_2) \uplus \Phi_3) = [-c(\mathbf{r} \cdot X)] + [1 \cdot X]$, but $\mathrm{Ex}_{\{c\}}(\Phi_1 \uplus \mathrm{Ex}_{\{c\}}(\Phi_2 \uplus \Phi_3)) = [-c(1 \cdot X)] + [\mathbf{r} \cdot X]$ which is different.</figcaption></figure>

§69.38 **Proposition** (Commutativity and associativity of tensor). Given $\mathbf{A}, \mathbf{B}, \mathbf{C}$ pairwise disjoint behaviours, we have (1) $\mathbf{A} \otimes \mathbf{B} = \mathbf{B} \otimes \mathbf{A}$ and (2) $\mathbf{A} \otimes (\mathbf{B} \otimes \mathbf{C}) = (\mathbf{A} \otimes \mathbf{B}) \otimes \mathbf{C}$.

*Proof.* (1) By the definition of tensor, we have $\Phi_1 \uplus \Phi_2 \in \mathbf{A} \otimes \mathbf{B}$ when $\Phi_1 \uplus \Phi_2 \in \{\Phi_1 \uplus \Phi_2 | \Phi_1 \in \mathbf{A}, \Phi_2 \in \mathbf{B}\}^{\perp\perp}$. We also have $\Phi_2 \uplus \Phi_1 \in \mathbf{B} \otimes \mathbf{A}$. But since $\Phi_1 \uplus \Phi_2 = \Phi_2 \uplus \Phi_1$ by commutativity of multiset disjoint union, we obtain $\mathbf{A} \otimes \mathbf{B} = \mathbf{B} \otimes \mathbf{A}$. (2) In the same fashion, by using the associativity of multiset disjoint union, we obtain $\mathbf{A} \otimes (\mathbf{B} \otimes \mathbf{C}) = (\mathbf{A} \otimes \mathbf{B}) \otimes \mathbf{C}$. $\square$

§69.39 The other connectives are then defined by interactive testing, e.g. the elements of $\mathbf{A} \not\otimes \mathbf{B}$ are the elements passing the tests of $\mathbf{A}^{\perp} \otimes \mathbf{B}^{\perp}$. This is why we can speak about *interactive types*.

§69.40 **Definition** (Par and linear implication). Let $\mathbf{A}, \mathbf{B}$ be disjoint behaviours. We define:

$$ \mathbf{A} \not\otimes \mathbf{B} = (\mathbf{A}^{\perp} \otimes \mathbf{B}^{\perp})^{\perp} \quad \text{and} \quad \mathbf{A} \not\to \mathbf{B} = \mathbf{A}^{\perp} \not\otimes \mathbf{B}. $$

§69.41 **Remark** (Implicit exchange). The commutativity and associativity of $\otimes$ are preserved for $\not\otimes$: we have $\mathbf{A} \not\otimes \mathbf{B} = (\mathbf{A}^{\perp} \otimes \mathbf{B}^{\perp})^{\perp} = (\mathbf{B}^{\perp} \otimes \mathbf{A}^{\perp})^{\perp} = \mathbf{B} \not\otimes \mathbf{A}$. This corresponds to the fact that the exchange rule is implicit in linear logic.

§69.42 In Figure 69.2, we can see that associativity fails when execution is treated as a binary operator on constellations. As in partial pre-execution (cf. Section 64), we need a restriction on the interaction between constellations. A technical precondition is defined for the associativity, and *trefoil property* [Sei16a, Theorem 40] is stated as a corollary (cf. Section 65).

§69.43 **Theorem** (Associativity of (pairwise) execution). Choose a set of colours $C \subseteq F_+ \uplus F_-$. For constellations $\Phi_1, \Phi_2$ and $\Phi_3$ such that $\cap_C(\Phi_1, \Phi_2, \Phi_3) = \emptyset$, we have:

$$ \mathrm{Ex}_C(\Phi_1 \uplus \mathrm{Ex}_C(\Phi_2 \uplus \Phi_3)) = \mathrm{Ex}_C(\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2) \uplus \Phi_3). $$
*Proof.* Assume we have $\mathfrak{m}_C(\Phi_1, \Phi_2, \Phi_3) = \emptyset$. Hence, by definition, no ray is shared by the three constellations. Let $P(i, j)$, be the set of paths reaching $(\Phi_1 \uplus \Phi_2 \uplus \Phi_3)[i][j]$ in $\mathfrak{D}[\Phi_1 \uplus \Phi_2 \uplus \Phi_3; A]$. By the previous statement, these paths traverse at most two constellations in $\{\Phi_1, \Phi_2, \Phi_3\}$. By using the reasoning of the proof of partial pre-execution (cf. Lemma 64.9), the paths $P(i, j)$ traversing $\Phi_2$ and $\Phi_3$ can be reduced with no effect on other connexions (since no rays are shared). Hence, the stars of $\Phi_1$ can connect to the stars of $\mathrm{Ex}_C(\Phi_2 \uplus \Phi_3)$ in the same way as in $\Phi_2 \uplus \Phi_3$. It follows that $\mathrm{Ex}_C(\Phi_1 \uplus \mathrm{Ex}_C(\Phi_2 \uplus \Phi_3)) = \mathrm{Ex}_C(\Phi_1 \uplus \Phi_2 \uplus \Phi_3)$. By the same reasoning, we also have $\mathrm{Ex}_C(\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2) \uplus \Phi_3) = \mathrm{Ex}_C(\Phi_1 \uplus \Phi_2 \uplus \Phi_3)$, hence execution is associative. $\square$

**§69.44 Theorem (Trefoil Property for execution-based orthogonality).** Let $C \subseteq F_+ \uplus F_-$ be a set of colours. For constellations $\Phi_1, \Phi_2, \Phi_3$ and for $i, j, k \in \{1, 2, 3\}$ such that $\mathfrak{m}_C(\Phi_1, \Phi_2, \Phi_3) = \emptyset$, we have:

$$ \Phi_1 \perp_C \mathrm{Ex}_C(\Phi_2 \uplus \Phi_3) \quad \text{if and only if} \quad \mathrm{Ex}_C(\Phi_1 \uplus \Phi_2) \perp_C \Phi_3. $$

*Proof.* Assume that $P$ is a property corresponding to the orthogonality relation $\perp$ based on execution, i.e. we have $\Phi_1 \perp_C \Phi_2$ if and only if $P(\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2))$. The statement can be rewritten as follows: $P(\mathrm{Ex}_C(\Phi_1 \uplus \mathrm{Ex}_C(\Phi_2 \uplus \Phi_3)))$ if and only if $P(\mathrm{Ex}_C(\mathrm{Ex}_C(\Phi_1 \uplus \Phi_2) \uplus \Phi_3))$. This is a direct consequence of the associativity (cf. Theorem 69.43). $\square$

**§69.45** It is then possible to recover the adjunction property that the trefoil property generalises (cf. Section 65).

**§69.46 Corollary (Adjunction).** Choose a set of colours $C \subseteq F_+ \uplus F_-$. For all constellations $\Phi_f, \Phi_a$ and $\Phi_b$ such that $\mathfrak{m}_C(\Phi_a, \Phi_b) = \emptyset$, we have:

$$ \Phi_f \perp_C \Phi_a \uplus \Phi_b \quad \text{if and only if} \quad \mathrm{Ex}_C(\Phi_f \uplus \Phi_a) \perp_C \Phi_b. $$

*Proof.* By symmetry of orthogonality relations and invariance of orthogonality under execution (cf. Lemma 69.8), we have $\Phi_f \perp_C \Phi_a \uplus \Phi_b$ if and only if $\Phi_f \perp_C \mathrm{Ex}_C(\Phi_a \uplus \Phi_b)$. In order to conclude with the trefoil property, it remains to show the precondition, i.e. that we have $\mathfrak{m}_C(\Phi_f, \Phi_a, \Phi_b) = \emptyset$. We assumed $\mathfrak{m}_C(\Phi_a, \Phi_b) = \emptyset$, meaning that no variable were shared by both $\Phi_a$ and $\Phi_b$. It follows that a variable cannot be shared by $\Phi_f, \Phi_a$ and $\Phi_b$ at the same time because otherwise, it would be shared by $\Phi_a$ and $\Phi_b$ as well. $\square$

**§69.47** As explained in Section 65, the adjunction allows to show that the behaviour $\mathbf{A} \dashv \mathbf{B}$ corresponding to linear implication has a functional behaviour. This is a necessary condition for the definition of linear logic.
§69.48 **Proposition** (Alternative linear implication). Let **A**, **B** be two disjoint behaviours.
We have **A** $
rightarrow$ **B** = {$\Phi_f$ | $\forall$ $\Phi_a \in **A**$, Ex($\Phi_f$ $unrightarrow$ $\Phi_a$) $in** **B**}.

Proof. By Definition 69.40, we have $\mathbf{A} \to \mathbf{B} = (\mathbf{A} \otimes \mathbf{B}^{\perp})^{\perp}$. We have $\Phi_f \in \mathbf{A} \to \mathbf{B}$ if and only if for all $\Phi_a \in \mathbf{A}$, $\mathrm{Ex}(\Phi_f \unrightarrow \Phi_a) \in \mathbf{B}$. Since $\mathbf{B}$ is a behaviour, by Definition 69.30, there exists $\Phi_{b'} \in \mathbf{B}^{\perp}$ such that $\mathrm{Ex}(\Phi_f \unrightarrow \Phi_a) \perp \Phi_{b'}$. By the adjunction (cf. Corollary 69.46), $\Phi_f \perp (\Phi_a \unrightarrow \Phi_{b'})$, hence $\Phi_f \in (\mathbf{A} \otimes \mathbf{B}^{\perp})^{\perp}$. The proof only relies on equivalences hence a bi-inclusion is proved. $\square$

**70 Soundness and completeness**

§70.1 In this section:

• Girard's adequacy between Usine and Usage presented in Section 43 is formalised;

• more classic results such as soundness and completeness w.r.t. proof-net theory are presented.

**Adequacy between Usine and Usage**

§70.2 In this subsection, our favourite orthogonality relation which will be mentioned is $\perp^R$
which require that the normal form is the star of roots (unpolarised rays) coming from
the two interacting constellations.

§70.3 As explained in Section 43, in transcendental syntax, the process of execution is able to express both cut-elimination and correctness testing. What changes is the shape of objects which interact:

• with cut-elimination, two vehicles interact;

• with correctness testing, a vehicle and a (compact) test interact.

The orthogonality relation $\perp^R$ formalises the two situations. We already know how it
captures MLL correctness but it also works for cut-elimination. What is a “correct”
interaction by cut-elimination? When the two vehicles $\Phi$ and $\Phi'$ interacting only leave
the star of uncoloured rays which were not related to cuts (that all rays related to cuts
have been eliminated), in other words when $\Phi \perp^R \Phi'$. In the same fashion of mixing
correctness and cut-elimination, plugging two vehicles by axiomatic cuts can be seen as
plugging a vehicle and a sort of test (which coincides with another vehicle) by using cuts
as adapters as shown in Figure 70.1.
<figure><img src="image_126.png" /><figcaption>(a) Proof-structure view.</figcaption></figure>

$$ \begin{array}{ccc} & [+1(X), +2(X)] & \\ [+1(X), +2(X)] + [3(X), +4(X)] + [+5(X), 6(X)] & \rightsquigarrow & \begin{bmatrix} -1(X) \\ +4(X) \end{bmatrix} + \begin{bmatrix} -2(X) \\ +5(X) \end{bmatrix} \\ [-1(X), -4(X)] + [-2(X), +5(X)] & & \begin{bmatrix} -4(X) \\ 3(X) \end{bmatrix} + \begin{bmatrix} -5(X) \\ 6(X) \end{bmatrix} \end{array} $$

(b) Constellation view in cut-elimination style (left) and block style for correctness testing (right).

Figure 70.1: Cut-elimination between two vehicles (on the left) seen as testing (on the right). Exactly as for testing, we expect to obtain the roots by execution. The cuts correspond to adapters. We see that the cut-elimination corresponding to testing an axiom against the only test of $\vdash A, A^{\perp}$. The free rays explicitly becomes roots of the test.

**§70.4 The meaning of cut-elimination.** Cut-elimination can then be reformulated. Its meaning is that every interaction between vehicles is valid (normalises into the star of roots). More formally: for all well-formed vehicles $\Phi, \Phi'$, we have $\Phi \perp^R \Phi'$. This is not always the case. A trivial example is to consider a case where cut-elimination fails (cf. Example 67.5). The two proof-structures interacting are indeed well-formed but we do not normalise into the star of roots. This is where correctness tests are needed.

**§70.5 Theorem (Multiplicative adequacy).** Let $\Phi$ and $\Phi'$ be two well-formed vehicles. If $\vdash \Phi' : \Gamma$ and $\Phi : \Gamma^{\perp}$, then $\Phi \perp^R \Phi' \dashv \Psi$ where $\Psi$ is a constellation of fully negative adapters (representing cuts).

*Proof.* This is another formulation of Theorem 67.10. □

**§70.6** Adequacy corresponds to a relation between Usine and Usage because the shape of objects given by Usine tests guarantees the use of objects (behaving like proof-structures). More precisely, Usine tests are also related to Usage's behaviours because if $\vdash \Phi : \Gamma$ then, $\Phi \in [[\vdash \Gamma]]$, meaning that a constellation passing the tests of $\vdash \Gamma$ behaves like an object of the idealised type $[[\vdash \Gamma]]$. This implies that $\text{Tests}(\vdash \Gamma)^{\perp} \subseteq [[\vdash \Gamma]]$.
A complete model of MLL+MIX

§70.7 We can also choose to prove more traditional properties of soundness and completeness w.r.t. proof-structures. This shows that we correctly captured the behaviour of proof-structures, their cut-elimination and their correctness. We start by associating a behaviour to formulas.

§70.8 Formula labels are interpreted by behaviours where distinct behaviours are associated with occurrences of variables by a function called *basis of interpretation*. Following previous works of Seiller [Sei12a, Definition 46], the behaviours corresponding to formula labels are *localised* formulas: they are defined using the same grammar as MLL formulas, except that variables are of the form $X_i(t)$, where $t$ is a term (here representing the path address described in Definition 66.7) used to distinguish occurrences of a same atomic formula $X_i$. Two behaviours $X_i(t)$ and $X_i(u)$ with $t \neq u$ represent the same atom at different locations and should correspond to the same behaviour modulo application of an adapter.

§70.9 **Definition (Basis of interpretation).** A *basis of interpretation* is a function $\Omega$ producing a behaviour $\Omega(A, i, t)$ when given a formula $A \in \mathcal{F}_{\text{MLL}}$, a natural number $i$ (index of occurrence) and a term $t \in \text{Addr}_x(S)$ (cf. Definition 66.7). A *basis of interpretation* has to satisfy the condition that $\text{Ex}(\Omega(A, i, t) + [+A(t), +B(u)]) = \Omega(B, j, u)$ when $i = j$ and otherwise $\Omega(A, i, t)$ and $\Omega(B, j, u)$ are disjoint, such that $A + \phi = \{\Phi + \phi \mid \Phi \in A\}$ for a behaviour $A$ and a star $\phi$.

§70.10 **Definition (Interpretation of MLL formulas).** Given a basis of interpretation $\Omega$, a formula $C$ representing the conclusion of a sequent, and an MLL formula occurrence $A$ identified by a unique unary function symbol $A(X)$ (cf. Definition 66.7). We define the *interpretation* $[[A, t]]_{\Omega}$ along $\Omega$ and a term $t$ (encoding the address of $A$ w.r.t. a conclusion $C$) inductively:

* $[[C, X_i, t]]_{\Omega} = \Omega(C, i, t);$

* $[[C, X_i^{\perp}, t]]_{\Omega} = \Omega(C, i, t)^{\perp};$

* $[[C, A \otimes B, t]]_{\Omega} = [[C, A, 1 \cdot t]]_{\Omega} \otimes [[C, B, \mathbf{r} \cdot t]]_{\Omega};$

* $[[C, A \mathfrak{R} B, t]]_{\Omega} = [[C, A, 1 \cdot t]]_{\Omega} \mathfrak{R} [[C, B, \mathbf{r} \cdot t]]_{\Omega}.$

We write $[[C]]$ for $[[C, C, X]]$ and extend the interpretation to sequents with:

$$[[\vdash C_1, \dots, C_n]]_{\Omega} := [[C_1]]_{\Omega} \mathfrak{R} \dots \mathfrak{R} [[C_n]]_{\Omega}.$$

§70.11 **Remark.** The interpretation of an axiom under an basis of interpretation $\Omega$ is defined by $[[\vdash X_1, X_1^{\perp}]]_{\Omega} = [[X_1]]_{\Omega} \mathfrak{R} [[X_1^{\perp}]] = \Omega(X_1, 1, X) \mathfrak{R} \Omega(X_1^{\perp}, 1, X)^{\perp}.$

§70.12 We prove soundness and completeness for MLL+MIX. Theorem 68.19 shows that asking for a strongly normalising union between vehicle and test corresponds to MLL+MIX
correctness. This is the key ingredient in the proof of completeness. In this section, we consider the orthogonality $⊥^{fin}$ exclusively.

§70.13 Instead of the usual soundness property, we prove an extension called full soundness [Sei12a, Theorem 55] which takes cut-elimination into account. In terms of the adequacy used in realisability interpretations, proving the soundness property corresponds to showing that $\vdash \Phi : \Gamma$ implies $[\vdash \Gamma]_{\Omega}$ for some basis of interpretation $\Omega$, except that for $\vdash \Phi : \Gamma$ we only consider constellations coming from proof-nets.

§70.14 **Lemma.** Let $A, B$ be MLL formulas, $\Gamma = C_1, \dots, C_n, \Delta = D_1, \dots, D_m$ be sets of MLL formulas and $\Omega$ be a basis of interpretation. We have $([\vdash \Gamma]_{\Omega} \not\to [A]_{\Omega}) \otimes ([\vdash \Delta]_{\Omega} \not\to [B]_{\Omega}) \subseteq ([\vdash \Gamma]_{\Omega} \not\to [\vdash \Delta]_{\Omega} \not\to [A \otimes B]_{\Omega})$.

*Proof.* The idea is to show $([C_1^{\perp} \otimes \dots \otimes C_n^{\perp}]_{\Omega} \to [A]_{\Omega}) \otimes ([D_1^{\perp} \otimes \dots \otimes D_m^{\perp}]_{\Omega} \to [B]_{\Omega}) \subseteq ([C_1^{\perp} \otimes \dots \otimes C_n^{\perp}]_{\Omega} \otimes ([D_1^{\perp} \otimes \dots \otimes D_m^{\perp}]_{\Omega}) \to [A \otimes B]_{\Omega}$ which is equivalent to $([C]_{\Omega} \to [A]_{\Omega}) \otimes ([D]_{\Omega} \to [B]_{\Omega}) \subseteq ([C]_{\Omega} \otimes [D]_{\Omega}) \to [A \otimes B]_{\Omega}$ for $C := C_1^{\perp} \otimes \dots \otimes C_n^{\perp}$ and $D := D_1^{\perp} \otimes \dots \otimes D_m^{\perp}$. Assume we have two functions $\Phi_{C,A} \in [C]_{\Omega} \to [A]_{\Omega}$ and $\Phi_{D,B} \in [D]_{\Omega} \to [B]_{\Omega}$. We can construct their disjoint union $\Phi_{C,A} \uplus \Phi_{D,B} \in ([C]_{\Omega} \to [A]_{\Omega}) \otimes ([D]_{\Omega} \to [B]_{\Omega})$. If we provide to $\Phi_{C,A} \uplus \Phi_{D,B}$ an argument $\Phi \in [C]_{\Omega} \otimes [D]_{\Omega}$, then since $C$ and $D$ are disjoint, each function $\Phi_{C,A}$ and $\Phi_{D,B}$ will take their argument separately and produce $\Phi' \in [A \otimes B]_{\Omega}$. Therefore, $\Phi_{C,A} \uplus \Phi_{D,B} \in ([C]_{\Omega} \otimes [D]_{\Omega}) \to [A \otimes B]_{\Omega}$. $\square$

§70.15 **Lemma.** If $\mathbf{A}$ is a pre-behaviour then $\mathbf{A}^{\perp} \neq \emptyset$.

*Proof.* Any constellation with only uncoloured rays strongly normalise with any constellation so it is always part of the orthogonal of a pre-behaviour. $\square$

§70.16 **Lemma.** If $\mathbf{A}$ is a behaviour and $\Phi \in \mathbf{A}$ then $|\mathrm{Ex}(\Phi)| < \infty$.

*Proof.* Assume we have a behaviour $\mathbf{A}$ and a constellation $\Phi \in \mathbf{A}$. By definition of behaviour, we have $\mathbf{A} = \mathbf{A}^{\perp\perp}$. By Lemma 70.15 there must be some $\Phi' \in \mathbf{A}^{\perp}$ such that $\Phi \uplus \Phi'$ is strongly normalising. Assume $\Phi$ is not strongly normalising. Then, $\Phi$ can produce infinitely many *saturated* correct diagrams. Such diagrams cannot be extended with stars of $\Phi'$ in $\Phi \uplus \Phi'$ because they are in disjoint union, hence these infinitely many saturated diagrams are preserved and $\Phi \uplus \Phi'$ cannot be strongly normalising, which is contradictory. Therefore, $\Phi$ must be strongly normalising. $\square$

§70.17 **Theorem (Full soundness for MLL+MIX).** Let $\vdash \mathcal{S} : \Gamma$ be an MLL+MIX proof-net and $\Omega$ a basis of interpretation. We have $\mathrm{Ex}(\Phi_S^{\mathrm{comp}}) \in [\vdash \Gamma]_{\Omega}$.

*Proof.* We start with the case of cut-free proofs normalising into themselves. The proof is done by induction on the proof-net structure of $\mathcal{S}$.
• Assume we have $\vdash S : X_i, X_i^\perp$. We would like to show that $\Phi_S^{ax} \in [[X_i]]_\mathcal{R}[[X_i^\perp]]_\Omega = [[X_i, X_i, X]]_\Omega \mathcal{R} [[X_i^\perp, X_i, X]]_\Omega^\perp = \Omega(X_i, i, X) \mathcal{R} \Omega(X_i^\perp, i, X)^\perp = (\Omega(X_i, i, X)^\perp \otimes \Omega(X_i^\perp, i, X))^\perp$. Let $\Phi_1 \uplus \Phi_2 \in \Omega(X_i, i, X)^\perp \otimes \Omega(X_i^\perp, i, X)$ with $\Phi_1 \in \Omega(X_i, i, X)^\perp$ and $\Phi_2 \in \Omega(X_i^\perp, i, X)$. It is sufficient to show that $|\mathrm{Ex}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax})| < \infty$, i.e. that the axiom strongly normalises with its tests. By Definition 70.9 since we have $\Phi_S^{ax} = [+X_i(X), +X_i^\perp(X)]$, we have $\mathrm{Ex}(\Phi_S^{ax} \uplus \Phi_2) \in \Omega(X_i, i, X)$ which is orthogonal to $\Phi_1$. By orthogonality, it follows that $|\mathrm{Ex}(\Phi_1 \uplus \mathrm{Ex}(\Phi_2 \uplus \Phi_S^{ax}))| < \infty$. Now, by definition of tensor,

• Assume we have $\vdash S : \Gamma, \Delta, A \otimes B$ coming from $\vdash S_1 : \Gamma, A$ and $\vdash S_2 : \Delta, B$. We have to show $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \mathcal{R} [[\vdash \Delta]]_\Omega \mathcal{R} [[A \otimes B]]_\Omega$. By induction hypothesis, we have $\Phi_{S_1}^{ax} \in [[\vdash \Gamma, A]]_\Omega = [[\vdash \Gamma]]_\Omega \mathcal{R} [[A]]_\Omega$ and $\Phi_{S_2}^{ax} \in [[\vdash \Delta, B]]_\Omega = [[\vdash \Delta]]_\Omega \mathcal{R} [[B]]_\Omega$. By a conjugation $\mu$ such that $\Phi_{S_1}^{ax}$ and $\Phi_{S_2}^{ax}$ are made distinct, we can relocate the atoms and obtain a constellation $\Phi_\mu \in ([[\vdash \Gamma]]_\Omega \mathcal{R} [[A]]_\Omega) \otimes ([[\vdash \Delta]]_\Omega \mathcal{R} [[B]]_\Omega)$ such that $\Phi_\mu = \mu(\Phi_{S_1}^{ax}) \uplus \Phi_{S_2}^{ax}$. Now, by the definition of tensor for proof-structures, we have a preservation of axioms and $\Phi_S^{ax}$ equivalent to $\Phi_\mu$ up to conjugation (and this conjugation could be chosen for $\mu$). By Lemma 70.14, we have $(([[\vdash \Gamma]]_\Omega \mathcal{R} [[A]]_\Omega) \otimes ([[\vdash \Delta]]_\Omega \mathcal{R} [[B]]_\Omega)) \subseteq [[\vdash \Gamma]]_\Omega \mathcal{R} [[\vdash \Delta]]_\Omega \mathcal{R} [[A \otimes B]]_\Omega$, hence $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \mathcal{R} [[\vdash \Delta]]_\Omega \mathcal{R} [[A \otimes B]]_\Omega$.

• Assume we have $\vdash S : \Gamma, A \mathcal{R} B$ coming from $\vdash S' : \Gamma, A, B$. We would like to show that $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \mathcal{R} [[A]]_\Omega \mathcal{R} [[B]]_\Omega$. This directly follows from the induction hypothesis and the fact that we have $[[\vdash \Gamma, A, B]]_\Omega = [[\vdash \Gamma]]_\Omega \mathcal{R} [[A]]_\Omega \mathcal{R} [[B]]_\Omega$ by definition.

• Assume we have $\vdash S : \Gamma, \Delta$ coming from $\vdash S_1 : \Gamma$ and $\vdash S_2 : \Delta$ (by using the MIX rule). We have to show $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \mathcal{R} [[\vdash \Delta]]_\Omega$ knowing that the induction hypothesis states that $\Phi_{S_1}^{ax} \in [[\vdash \Gamma]]_\Omega$ and $\Phi_{S_2}^{ax} \in [[\vdash \Delta]]_\Omega$. Since the MIX rule only places two proofs next to each other, we have $\Phi_S^{ax} = \Phi_{S_1}^{ax} \uplus \Phi_{S_2}^{ax}$ by definition. By definition of tensor, we have $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \otimes [[\vdash \Delta]]_\Omega$. It remains to show that $A \otimes B \subseteq A \mathcal{R} B$ in general, which would imply $\Phi_S^{ax} \in [[\vdash \Gamma]]_\Omega \mathcal{R} [[\vdash \Delta]]_\Omega$. We have $A \mathcal{R} B \subseteq (A^\perp \otimes B^\perp)^\perp$, hence we have to show that $A \otimes B \subseteq (A^\perp \otimes B^\perp)^\perp$. Let $\Phi_1 \uplus \Phi_2 \in A \otimes B$ and $\Phi'_1 \uplus \Phi'_2 \in A^\perp \otimes B^\perp$. We know that $\Phi_1 \perp \Phi'_1$ and $\Phi_2 \perp \Phi'_2$. We have $\Phi_1 \uplus \Phi_2 \perp \Phi'_1 \uplus \Phi'_2$, i.e. that $\Phi_1 \uplus \Phi_2 \uplus \Phi'_1 \uplus \Phi'_2$ is strongly normalising. In particular, we cannot have a crossed infinite interaction between $\Phi_1$ and $\Phi'_2$ or between $\Phi_2$ and $\Phi'_1$ because otherwise one constellation would have to not be strongly normalising (because a strongly normalising constellation produces finitely many saturated diagrams which cannot be extended so to make an infinite execution) but this would contradict Lemma 70.16.

If the proof has cuts, then by Theorem 67.10, we can execute its translation (a constellation) so that the normal form corresponds to the normal form of the proof. This proof is necessarily cut-free, hence the case of cut-free proofs also applies to this case. $\square$

§70.18 **Lemma.** Let $\Omega$ be a basis of interpretation and $\vdash \Gamma$ an MLL sequent. Then, we have $\mathrm{Tests}(\vdash \Gamma) \subseteq [[\vdash \Gamma]]_\Omega^{\perp\mathrm{fin}}$.
*Proof.* Assume we have Test($\vdash \Gamma$)$\varphi \in$ Tests($\vdash \Gamma$) for a switching $\varphi$ of $\vdash \Gamma$. The proof is done by induction on $\vdash \Gamma$.

* If $\Gamma = \{A_1, ..., A_n\}$ where the $A_i$ are formulas $X_i$ or $X_i^{\perp}$, then there is a single switching $\varphi$. Because typing is invariant under execution, we can consider a simplification of tests by fusion Ex(Test($\vdash \Gamma$)$\varphi$) = $\sum_{i=1}^n [-A_i(t_i), A_i(X)]$ where $t_i$ is the expected encoding of the address of the atom $A_i$. We would like to show that Test($\vdash \Gamma$)$\varphi \in$ $[[\vdash A_1, ..., A_n]]_{\Omega}^{\perp} = [[A_1, A_1, t_1]]_{\Omega}^{\perp} \otimes ... \otimes [[A_n, A_n, t_n]]_{\Omega}^{\perp}$. We show that $[-A_i(t_i), A_i(X)] \in$ $[[A_i, A_i, t_i]]_{\Omega}^{\perp}$. Let $\Phi_i \in$ $[[A_i, A_i, t_i]]_{\Omega}$. Because $[[A_i, A_i, t_i]]_{\Omega}$ is a behaviour, we can use Lemma 70.16 and infer that $|\mathrm{Ex}(\Phi_i)| < \infty$. Adding $[-A_i(t_i), A_i(X)]$ to a strongly normalising constellation cannot cause divergence, hence we must have $[-A_i(t_i), A_i(X)] \perp \Phi_i$ and $[-A_i(t_i), A_i(X)] \in$ $[[A_i, A_i, t_i]]_{\Omega}^{\perp}$. Now, since Test($\vdash \Gamma$)$\varphi$ is made of a disjoint union of constellations of $[[A_i, A_i, t_i]]_{\Omega}^{\perp}$, it follows that Test($\vdash \Gamma$)$\varphi \in$ $[[\vdash A_1, ..., A_n]]_{\Omega}^{\perp}$.

* If $\vdash \Gamma$ is $\vdash \Delta$, $A \not\sim B$, then a switching $\varphi$ of $\vdash \Delta$, $A \not\sim B$ is a switching $\bar{\varphi}$ of $\vdash \Delta$, $A, B$ extended with a left or right selection of premise between $A$ and $B$, both linked by a $\not\sim$ connective. By the induction hypothesis, we have Test($\vdash \Delta, A, B)^{\bar{\varphi}} \in$ $[[\vdash \Delta, A, B]]_{\Omega} = [[\vdash \Delta]]_{\Omega} \not\sim [[A]]_{\Omega} \not\sim [[B]]_{\Omega}$ and we would like to show that Test($\vdash \Delta, A \not\sim B)^{\bar{\varphi}} \in$ $[[\vdash \Delta, A \not\sim B]]_{\Omega} = [[\vdash \Delta]]_{\Omega} \not\sim [[A \not\sim B]]_{\Omega} = [[\vdash \Delta]]_{\Omega} \not\sim [[A \not\sim B, A, l \cdot X]]_{\Omega} \not\sim [[A \not\sim B, B, r \cdot X]]_{\Omega}$. The constellation Test($\vdash \Delta, A, B)^{\bar{\varphi}}$ uses terms $A(t)$ and $B(u)$ but when we add a $\not\sim$ link between $A$ and $B$, these terms are relocated relatively to the conclusion $A \not\sim B$ and we obtain $(A \not\sim B)(l \cdot t)$ and $(A \not\sim B)(r \cdot u)$. Since they only differ by a conjugation, the two tests will react in the same way with respects to strong normalisation, i.e. Test($\vdash \Delta, A, B)^{\bar{\varphi}} \in$ $[[\vdash \Delta]]_{\Omega}^{\perp} \otimes [[A]]_{\Omega}^{\perp} \otimes [[B]]_{\Omega}^{\perp}$ $\perp$ implies Test($\vdash \Delta, A \not\sim B)^{\varphi} \in$ $[[\vdash \Delta]]_{\Omega}^{\perp} \otimes [[A \not\sim B]]_{\Omega}^{\perp}$).

* If $\vdash \Gamma$ is $\vdash \Delta$, $A \otimes B$, a switching of $\vdash \Gamma$ is a switching of $\vdash \Delta$, $A, B$ extended to the additional $\otimes$ connective linking $A$ and $B$, and Test($\vdash \Delta, A \otimes B)$$\varphi$ can be defined from Test($\vdash \Delta, A, B)$$\varphi$ by removing the uncoloured rays $A(x)$ and $B(x)$, and adding new stars $[-A(X), -B(X), +(A \otimes B)(X)]+[-(A \otimes B)(X), (A \otimes B)(X)]$. One can show that $[[\vdash \Delta, A \otimes B]]_{\Omega}$ is generated (in the sense of bi-orthogonal closure) by a pre-behaviour $E$, i.e. that $[[\vdash \Delta, A \otimes B]]_{\Omega} = E^{\perp\perp}$ for some $E$, similarly to how $A \otimes B$ is generated by a bi-orthogonal closure on the pre-tensor $A \odot B$ (cf. Definition 69.35). In this pre-behaviour $E$, the rays coming from $A$ are disjoint from the rays coming from $B$ (because of the requirement of exclusion of interaction). By using the induction hypothesis Tests($\vdash \Delta, A, B) \subseteq [[\vdash \Delta, A, B]]_{\Omega}^{\perp\mathrm{fin}}$, this shows the result since this implies that Test($\vdash \Delta, A \otimes B)$$\varphi \in E^{\perp\mathrm{fin}}$ and Test($\vdash \Delta, A \otimes B)$$\varphi \in E^{\perp\perp\perp} = [[\vdash \Delta, A \otimes B]]_{\Omega}^{\perp}$ since it is known that $X^{\perp} = X^{\perp\perp}$ in general for any pre-behaviour $X$ [JS21, Corollary 9].

☐
We note this set $\vdash\Gamma$. A constellation $\Phi$ is *proof-like w.r.t.* an MLL sequent $\vdash \Gamma$ if it is
well-formed and $\mathrm{IdRays}\Phi = \vdash\Gamma$.

§70.20 **Example.** A constellation which is proof-like w.r.t. $\vdash X_1 \perp \mathcal{R} X_2^\perp$, $X_1 \otimes X_2$ is
$$ [+(X_1^\perp \mathcal{R} X_2^\perp)(\mathbf{1} \cdot X), +(X_1 \otimes X_2)(\mathbf{1} \cdot X)] + [+(X_1^\perp \mathcal{R} X_2^\perp)(\mathbf{r} \cdot X), +(X_1 \otimes X_2)(\mathbf{r} \cdot X)]. $$
However, even the wrong linking
$$ [+(X_1^\perp \mathcal{R} X_2^\perp)(\mathbf{1} \cdot X), +(X_1^\perp \mathcal{R} X_2^\perp)(\mathbf{r} \cdot X)] + [+(X_1 \otimes X_2)(\mathbf{1} \cdot X), +(X_1 \otimes X_2)(\mathbf{r} \cdot X)] $$
is proof-like as well.

§70.21 **Theorem (Completeness for MLL+MIX).** If a constellation $\Phi \in [\vdash \Gamma]_{\Omega}$ is proof-like w.r.t. $\vdash \Gamma$, then there exists an MLL+MIX proof-net $\vdash S : \Gamma$ such that $\Phi = \Phi_S^{ax}$.

*Proof.* A proof-like constellation $\Phi \in [\vdash \Gamma]_{\Omega}$ can always be considered as the interpretation of a proof-structure with only axioms; we can then construct a proof-structure $S$ by considering the union of the latter with $ST(\vdash \Gamma)$ by placing the axioms on the right places in $ST(\vdash \Gamma)$ (at this point, the linking can still be wrong). Since $\Phi \in [\vdash \Gamma]_{\Omega}$ we can use Lemma 70.18 and infer that for all switchings $\varphi$ of $\vdash \Gamma$ (equivalently, of $S$), Test($\vdash \Gamma$) = $\Phi_S^{\varphi} \perp \Phi$, excluding “wrong linking”. By Corollary 68.21, it follows that $S$ is acyclic, *i.e.* satisfies the correctness criterion for MLL+MIX. Therefore, $S$ must be a proof-net of vehicle $\Phi$. $\square$

A complete model of MLL

§70.22 The soundness property actually holds for MLL with the same arguments as for the previous section whether we use $\perp^1$ or $\perp^R$ as orthogonality relation. In this section, we only mean $\perp^1$ or $\perp^R$ whenever $\perp$ is written.

§70.23 **Theorem (Full soundness for MLL).** Let $\vdash S : \Gamma$ be an MLL proof-net and $\Omega$ a basis of interpretation. We have $\mathrm{Ex}(\Phi_S^{\mathrm{comp}}) \in [\vdash \Gamma]_{\Omega}$.

*Proof.* The idea of the proof is exactly the same as for Theorem 70.17. The only difference is in the axiom case. We need to show that $\mathrm{Ex}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax}) = \mathrm{Roots}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax})$ (respectively, $|\mathrm{Ex}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax})| = 1$). However, the properties of the basis of interpretation ensures that $\Phi_2 \uplus \Phi_S^{ax}$ will be orthogonal to $\Phi_1$. Hence $\mathrm{Ex}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax}) = \mathrm{Roots}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax})$ (respectively, $|\mathrm{Ex}(\Phi_1 \uplus \Phi_2 \uplus \Phi_S^{ax})| = 1$). $\square$

§70.24 The proof of Lemma 70.18 which is essential for the completeness property does not hold anymore because of a minor technical problem. This is because a general sequent $\vdash A_1, ..., A_n$ for $A_i$ being atomic formulas is used for the base case. This is valid for
MLL+MIX proof-nets since we only require acyclicity when testing with the switchings. However, this is not a correct base case for MLL proof-nets which are more demanding by requiring connectedness. We need to start from a single axiom and therefore, induction could be done on the MLL sequent calculus instead by considering provable formulas in MLL. This would be sufficient to get a completeness result. However, instead of restricting to correct formulas, which would identify $\llbracket \vdash \Gamma \rrbracket_\Omega$ and a subset of Tests($\vdash \Gamma$)$^\perp$ corresponding to proof-structures, it is sufficient to identify $\llbracket \vdash \Gamma \rrbracket_\Omega$ and Tests($\vdash \Gamma$)$^\perp$ directly. We would then have to prove Tests($\vdash \Gamma$) $\subseteq$ Tests($\vdash \Gamma$)$^{\perp\perp}$ which is always true in general [JS21, Proposition 7]. We do so by considering a notion of strict interpretation.

§70.25 **Definition (Strict interpretations).** We define the two strict interpretations for a given basis of interpretation $\Omega$ and an MLL sequent $\vdash \Gamma$:

$$ \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{1} = \text{Tests}(\vdash \Gamma)^{\perp 1} \text{ and } \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{R} = \text{Tests}(\vdash \Gamma)^{\perp R}. $$

§70.26 **Theorem (Completeness for MLL).** If a constellation $\Phi \in \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{R}$ (respectively $\Phi \in \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{1}$) is proof-like w.r.t. a provable sequent $\vdash \Gamma$ of MLL, then there exists an MLL proof-net $\vdash S : \Gamma$ such that $\Phi = \Phi_{S}^{ax}$.

*Proof.* The proof begins like the proof of completeness for multiplicative linear logic extended with the MIX rule (cf. Theorem 70.21) and reach the construction of a proof-structure with axioms translated into $\Phi$. Now, $\Phi \in \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{R}$ (respectively $\Phi \in \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{1}$) implies that, in particular, $\Phi$ passes the Danos-Regnier correctness test for MLL (by Corollary 68.21). Therefore, the proof-structure we constructed must be correct. $\square$

§70.27 Notice that if we have a constellation $\Phi \in \langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{X}$ for some $\Omega$, MLL sequent $\vdash \Gamma$ and $X \in \{1, R\}$, its Danos-Regnier tests $\Phi_1, ..., \Phi_n$ are constellations of $(\langle\langle \vdash \Gamma \rangle\rangle_{\Omega}^{X})^{\perp}$. This formalises the intuition in proof-nets that tests are sort of proofs of the dual.

# 71 The case of multiplicative units

§71.1 Until now, I ignored neutral elements because they were problematic but it is still possible to say few (speculative) things about them.

§71.2 We try to look for behaviours corresponding to neutral elements for $\otimes$ and $\otimes\Sigma$ respectively. It is possible to define a pre-behaviour $\perp$ called a pole (cf. Section 22) such that $\Phi \perp \Phi'$ if and only if $\text{Ex}(\Phi \oplus \Phi') \in \perp$ for an execution-based orthogonality $\perp$ and $\perp$ must be closed under anti-evaluation (cf. Section 22), i.e. if $\Phi \in \perp$ and $\text{Ex}(\Phi') = \Phi$, then $\Phi' \in \perp$. For instance, if we consider $\perp^R$, then $\perp$ is the set of all constellations normalising into a single uncoloured star. The pole will be useful for a definition of neutral elements.
§71.3 A natural choice of behaviour for the neutral element of $\otimes$ w.r.t. $\perp^R$ is the pre-behaviour $\{\emptyset\}$ only containing the empty constellation since $\Phi \uplus \emptyset = \Phi$ for any constellation $\Phi$. Fortunately, it is a behaviour.

§71.4 **Proposition.** The pre-behaviour $\{\emptyset\}$ is a behaviour.

*Proof.* A constellation of $\{\emptyset\}^{\perp}$ must self-normalise into the set of its roots since $\emptyset$ has not effect when in interaction with another constellation. We have $\{\emptyset\}^{\perp} = \perp$. Now, a constellation $\Phi \in \perp^{\perp}$ is a constellation such that when it interacts with a constellation $\Phi' \in \perp^{\perp}$, we have $\text{Ex}(\Phi \uplus \Phi') \in \perp$. We can theoretically imagine that $\Phi$ has rays linked to $\Phi$ but this is impossible because $\Phi'$ is self-normalising into an element of $\perp$ by constructing a saturated diagram which cannot be extended and which must be present in the normal form. Actually, $\Phi$ must be the empty constellation because otherwise we would get more than the star of roots. Therefore, $\perp^{\perp} = \{\emptyset\}^{\perp\perp} = \{\emptyset\}$. $\square$

§71.5 **Definition (One).** We define the behaviour $\mathbf{1} := \{\emptyset\} = \perp^{\perp}$.

§71.6 **Proposition.** We have $\mathbf{A} \otimes \mathbf{1} = \mathbf{A}$ for any behaviour $\mathbf{A}$.

*Proof.* By definition, we have $\mathbf{A} \otimes \mathbf{1} = \{\Phi_A \uplus \emptyset \mid \Phi_A \in \mathbf{A}\}^{\perp\perp} = \{\Phi_A \mid \Phi_A \in \mathbf{A}\}^{\perp\perp} = \mathbf{A}^{\perp\perp} = \mathbf{A}$. $\square$

§71.7 As for bottom, as usual in linear logic, we define it as $\mathbf{1}^{\perp} = \perp$.

§71.8 **Proposition.** The pre-behaviour $\mathbf{1}^{\perp} = \{\emptyset\}^{\perp} = \perp$ is a behaviour.

*Proof.* Since it is known that $\mathbf{A}^{\perp} = \mathbf{A}^{\perp\perp\perp}$ for any behaviour $\mathbf{A}$ [JS21, Corollary 9], it follows that $\mathbf{1}^{\perp}$ (and thus $\{\emptyset\}^{\perp}$) is a behaviour. $\square$

§71.9 **Definition (Bottom).** We define the behaviour $\llcorner := \mathbf{1}^{\perp}$.

§71.10 **Proposition.** We have $\mathbf{A} \not\simeq \mathbf{1} = \mathbf{A}$ for any behaviour $\mathbf{A}$ when considering $\perp^R$.

*Proof.* We have $\mathbf{A} \not\simeq \mathbf{1} = (\mathbf{A}^{\perp} \otimes \mathbf{1}^{\perp})^{\perp} = (\mathbf{A}^{\perp} \otimes \{\emptyset\}^{\perp\perp})^{\perp} = (\mathbf{A}^{\perp} \otimes \{\emptyset\})^{\perp} = \mathbf{A}^{\perp\perp} = \mathbf{A}$ (since $\mathbf{A}$ is a behaviour). $\square$
§71.11 **Proposition.** We have $\mathbf{A}^{\perp} = \mathbf{A} \dashv \bot$ for any behaviour $\mathbf{A}$ when considering $\bot^R$.

*Proof.* We have $\mathbf{A} \dashv \bot = \mathbf{A}^{\perp} \mathcal{Y} \bot$. Since $\bot$ is a neutral element for $\mathcal{Y}$, it follows that $\mathbf{A}^{\perp} \mathcal{Y} \bot = \mathbf{A}^{\perp}$. $\square$

§71.12 We defined interactive types for units which correspond to idealised neutral elements (Usage). Now, considering a constellation $\Phi$ in the wild, are we able to effectively tell whether it is in **1** (respectively $\bot$) or not (Usine).

§71.13 We consider $\bot^R$. In order to tell if $\Phi \in \bot$, we can use the fact that $\bot = \{\emptyset\}^{\perp}$. Hence, it is sufficient to consider the set of tests $\{\emptyset\}$. When testing $\Phi$ against the empty constellation $\emptyset$, if we have $\Phi \perp \emptyset$ then $\Phi \in \bot$. As for **1**, we just need to be able to tell if $\Phi = \emptyset$. This can be done with any constellation of $\mathbf{1}^{\perp} = \bot$.

§71.14 This provides a notion of correct constellations for multiplicative units. However, although they fulfil their role as constellations having the behaviour of neutral elements for multiplicative connectives, it is not quite the *real thing* as they do not exactly correspond to the units of proof-nets. In particular, if we look at the rule for $\bot$, the constant $\bot$ is introduced in a given context $\Gamma$ to which it is dependent. Hence, it will be disconnected when considering a switching in a correct proof-structure. This breaks the connectedness condition of the Danos-Regnier correctness criterion. The usual hack is to consider jumps (cf. Section 30) between $\bot$ nodes and either axioms or 1 nodes to represent the dependency between $\bot$ and its context. Girard's idea [Gir18a, Section 2.1.1] is to encode multiplicative units in second order linear logic because of this non-local dependency (cf. Section 44).

**72 Discussion: what is a multiplicative proof?**

§72.1 We consider the orthogonality $\bot^R$. Correctness tests characterise the shape of proofs and testing is done by checking if all stars collapse to a single star of uncoloured rays by edge contraction. If we look at the test for $\otimes$, it is a 3-ary star with two inputs and one output. It forces any constellation interacting with it to be made of two disjoint connected components. In other words, the test for $\otimes$ *reunites* proof-structures. As for $\mathcal{Y}$, the two tests $\mathcal{Y}_L$ and $\mathcal{Y}_R$ are made of two disjoint parts. They *separates* proof-structures. It seems that MLL proofs are about how some primitive data are organised in terms of reunion/separation.

§72.2 Typically, if we have an axiom (which is also an identity function) [+1(X), +2(X)], then it is possible to connect it with [+3(X)] by using a cut [-1(X), -3(X)] and obtain [+2(X)]. But we could also connect it with the cut [-2(X), -3(X)]. This emphasizes the equality $A \dashv B = B^{\perp} \dashv A^{\perp}$ of linear logic. But there are some other things we can notice:
• whether we have a proof of $X_1^\perp \not\exists X_1$ or $A^\perp \not\exists A^1$ for any multiplicative formula $A$, their translation is not so different: it is materialised by some binary star $[r, r']$ where $r$ and $r'$ are as complex (in their internal structure) as $A$ is;

• the difference between $X_1^\perp$ and $X_1$ looks rather artificial in stellar resolution. Both are translated into two different rays. It does not mean that negation does not exist but that it seems to be an external consideration over constellations.

All these remarks about the translation of multiplicative proofs constitute an analysis of MLL through stellar resolution.

**§72.3 Real multiplicatives.** Actually, we did not even get “real” multiplicative proof-structures since multiplicative proof-structures are known to be generic objects in which atomic formulas (which are variables) can be replaced by more complex formulas. Original MLL proof-structures are polymorphic. This shows that we need to add more structure over our interpretation but this is the role of Girard’s epidictics. The multiplicatives we got are sort of “first-order” multiplicatives free of external considerations.

**§72.4 Hidden duplication in MLL proof-structures.** In the geometry of interaction, what we do is representing MLL proofs by permutations over a set of atoms (dots, natural numbers, ...) where cuts are represented by partial injections linking some atoms. If we wanted to translate this situation into stellar resolution, we would only need constants. But this is *not* how it works in real proof-structures. In proof-net theory, the situation is more sophisticated: cuts are not links between atoms but links between *conclusion* or *whole* proof-structures, then cuts are duplicated and distributed to atoms. In our stellar interpretation of MLL proofs, this is done by internalising the complex shape of proof-structure directly into terms of rays, then in order to have the cut distributed to its two left premises and two right premises, we must use variables. This shows that technically speaking, MLL proof-net theory is not exactly duplication-free: it hides some non-linear behaviours directly related to how terms of the translation are designed (do we use constants? do we use variables? etc).
# Chapter 11

## Interpretation of intuitionistic implication

The interpretation of exponentials follows ideas already presented in Section 37. The idea is that we are looking for mechanisms of duplication and erasure in the model of computation itself (stellar resolution in our case). Formulas corresponding to the exponentials of linear logic are then specifications for these primitive behaviours: correctness tests (in the case of Usine) or behaviours (in the case of Usage). Richer computational behaviours related to duplication and erasure can then lead to alternative exponentials. In stellar resolution, duplication occurs when a ray (for instance $+c(X)$) is matchable with several other rays (for instance $-c(1)$ and $-c(2)$). Diagrams will duplicate stars to satisfy the constraints.

Instead of defining full exponentials as in MELL, Girard chooses to restrict the interpretation to *intuitionistic implication* [Gir17, Section 5], hence ? and ! only appear in $?A\not\forall B$ and $!A\otimes B$. New binary exponential connectives $A\times B := ?A\not\forall B$ and $A\otimes B := !A\otimes B$ are introduced for that purpose. We could equivalently consider intuitionistic implication $A \Rightarrow B$ and its dual $(A \Rightarrow B)^\perp$ instead.

This restriction is consistent with Girard's point of view (cf. Section 44) that full exponentials and multiplicative neutral elements are second-order constructions since from the formula 1 it is possible to define ! with $!A := A \otimes 1$. Despite this restriction, intuitionistic implication is sufficient to interpret simply typed $\lambda$-calculus.

In this chapter, I do not detail the interpretation as much as for MLL. In particular, no result of soundness or completeness are stated.

### 73 MLL with intuitionistic implication (MLL2I)

§73.1 The logic MLL2I defined in this section is simply MELL (cf. Section 27) with a different notation. Hence, there is no need to define cut-elimination for sequent calculus. We can simply unfold the notation and we work on MELL.
<figure><img src="image_127.png" /><figcaption>Figure 73.1: Multiplicative linear logic with intuitionistic implication (MLL2I).</figcaption></figure>

## MLL2I sequent calculus

§73.2 The connective ?A is written A and it only applies to formulas at top-level, i.e. on whole conclusions of the sequent and not subformulas. Exponentials connectives are ways to handle these underlined formulas.

§73.3 **Definition (MLL2I pre-formulas)**. We define the set of pre-formulas $\mathcal{F}_{\text{MLL2I}}^{\text{pre}}$ of MLL2I inductively by the following grammar:

$$ C, D = X_i | X_i^{\perp} | C \otimes D | C \not\otimes D | C \ominus D | C \times D \quad (i \in \mathbf{N}) $$

§73.4 **Definition (MLL2I formulas)**. We define the set of formulas $\mathcal{F}_{\text{MLL2I}}$ of 2MLL inductively by the following grammar for $C \in \mathcal{F}_{\text{MLL2I}}^{\text{pre}}$:

$$ A, B = C | \underline{C} $$

§73.5 The rules of MLL2I, shown in Figure 73.1 are derived from the restriction of MELL to the intuitionistic implication. Notice that the promotion rule is implicit because in the $\ominus$ rule, the left premise is $\vdash \underline{\Delta}, A$ which corresponds to $\vdash ?\Delta, !A$. In case we have a cut between a formula $A^{\perp} := ?B^{\perp}$ (for some $B$) and another formula $A$, it is implicit that $A := !B$. It is as if promotion was only accessible from $\ominus$.

§73.6 **Definition (Translation back to MELL formulas)**. We define a translation of a MLL2I formula $A$ into a corresponding MELL formulas $\lfloor A \rfloor$. If $A$ is a pre-formula $C$ then $\lfloor A \rfloor := \lfloor C \rfloor_{\text{pre}}$. If $A$ is an underlined pre-formula $\underline{C}$ then $\lfloor A \rfloor := ?\lfloor C \rfloor_{\text{pre}}$.

The translation of a pre-formula is defined by:

$$ \begin{align*} \lfloor X_i \rfloor_{\text{pre}} &:= X_i & \lfloor X_i^{\perp} \rfloor_{\text{pre}} &:= X_i^{\perp} & \lfloor C \otimes D \rfloor_{\text{pre}} &:= \lfloor C \rfloor_{\text{pre}} \otimes \lfloor D \rfloor_{\text{pre}} \\ \lfloor C \not\otimes D \rfloor_{\text{pre}} &:= \lfloor C \rfloor_{\text{pre}} \not\otimes \lfloor D \rfloor_{\text{pre}} & \lfloor C \times D \rfloor_{\text{pre}} &:= ?\lfloor C \rfloor_{\text{pre}} \not\otimes \lfloor D \rfloor_{\text{pre}} \end{align*} $$
$$ \frac{\frac{\vdash \underline{\Delta_1}, A \quad \vdash \Gamma'_1, \underline{\Delta_1}', B \quad \vdash \Gamma'_2, \underline{\Delta_2}, A^{\perp}, B^{\perp}}{\vdash \Gamma'_1, \underline{\Delta_1}, \underline{\Delta_1}', A \ominus B} \ominus \frac{\vdash \Gamma'_2, \underline{\Delta_2}, A^{\perp} \times B^{\perp}}{\vdash \Gamma'_1, \underline{\Delta_1}, \underline{\Delta_1}', \Gamma'_2, \underline{\Delta_2}}}{\vdash \Gamma'_1, \underline{\Delta_1}, \underline{\Delta_1}', \Gamma'_2, \underline{\Delta_2}} \stackrel{\text{cut}}{\rightsquigarrow} \frac{\vdash \underline{\Delta_1}, A \quad \vdash \Gamma'_1, \underline{\Delta_1}', B \quad \vdash \Gamma'_2, \underline{\Delta_2}, A^{\perp}, B^{\perp}}{\vdash \Gamma'_1, \underline{\Delta_1}, \underline{\Delta_1}', \Gamma'_2, \underline{\Delta_2}} \text{ cut} $$

$$ \frac{\frac{\vdash \Gamma_1, \underline{\Delta_1}}{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}} w \quad \vdash \underline{\Delta_2}, A}{\Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}} \text{ cut} \rightsquigarrow \frac{\vdash \Gamma_1, \underline{\Delta_1}}{\vdash \Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}, A} w $$

$$ \frac{\frac{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}}{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}} d \quad \vdash \underline{\Delta_2}, A}{\vdash \Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}} \text{ cut} \rightsquigarrow \frac{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp} \quad \vdash \underline{\Delta_2}, A}{\vdash \Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}} \text{ cut} $$

$$ \frac{\frac{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}, A^{\perp}}{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}} c \quad \vdash \underline{\Delta_2}, A}{\vdash \Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}} \text{ cut} \rightsquigarrow \frac{\vdash \Gamma_1, \underline{\Delta_1}, A^{\perp}, A^{\perp} \quad \vdash \underline{\Delta_2}, A}{\vdash \Gamma_1, \underline{\Delta_1}, \underline{\Delta_2}, A^{\perp}} \text{ cut} $$

(a) Cut-elimination for MLL2I

$$ [C \oslash D]_{\text{pre}} := ![C]_{\text{pre}} \otimes [D]_{\text{pre}} $$

§73.7 The cut-elimination rules for MLL2I, shown in Figure 73.2a are similar to usual exponential rules. In order to apply cut-elimination on a MLL2I sequent proof, we have to replaced all formulas A by $[A]$ and apply the usual rules of MELL. It is easy to show that this replacement preserves validity of the proof.

## MLL2I proof-structures

§73.8 The constructors for MLL2I proof-structures are given in Figure 73.3. The difference with the usual presentation with boxes is that we will have links between the left premise of $\ominus$ and other vertices of the proof-structure. These links represent the dependency between a box and its isolated sub-proof-structures of the context (the context $\Delta$ on the top of the sequent calculus rule for $\ominus$). Remark that it is not useful to link vertices which are already reachable from the left premise of $\ominus$ since it is already explicit that those vertices are in a box. An example of MLL2I proof-structure with such dependencies is given in Figure 73.4.

§73.9 **Definition (MLL2I proof-structure)**. An *MLL2I proof-structure* is defined by

$$ S = (V, E, \text{in}, \text{out}, \ell_E, \text{dep}) $$
<figure><img src="image_128.png" /><figcaption>Figure 73.3: MLL2I proof-structures hyperedge constructors.</figcaption></figure>

<figure><img src="image_129.png" /><figcaption>Figure 73.4: Example of MLL2I proof-structure with dependencies.</figcaption></figure>
where $(V, E, \mathbf{in}, \mathbf{out})$ is an ordered directed hypergraph (cf. Appendix C),

$$ \ell_E : E \to \{\otimes, \mathcal{Y}, \text{ax}, \text{cut}, \bowtie, \ominus, \text{w}, \text{d}, \text{c}\} $$

is a labelling map on hyperedges and dep : $V \to \mathcal{P}(V)$ associates vertices with left premises of a $\ominus$ hyperedge (it represents dependencies) A proof-structure is subject to these additional constraints:

* hyperedges satisfy the arities and labelling constraints shown in Figure 73.3;

* each vertex must be the target of exactly one hyperedge, and the source of at most one hyperedge;

* cut hyperedges must connect either:

- the conclusion of a $\mathcal{Y}$ hyperedge with the conclusion of a $\otimes$ hyperedge, or

- the conclusion of a $\bowtie$ hyperedge with the conclusion of a $\ominus$ hyperedge, or

- two atoms.

**§73.10 Definition (Exponential box).** Let $S := (V, E, \mathbf{in}, \mathbf{out}, \ell_E, \mathbf{dep})$ be an MLL2I proof-structure. We define the (exponential) box of a vertex by an injective function $\mathbf{box}: V \to \mathcal{P}(V) \times \mathcal{P}(E)$ associating to each left premise $v$ of a $\ominus$ hyperedge (there is some $e$ such that $\mathbf{out}(e) = v$ and $\ell_E(e) = \ominus$) a sub-proof-structure corresponding to all the vertices and edges connected (by non-oriented paths) to $v$ and all vertices of dep($v$).

**§73.11 Convention.** MLL2I proof-structures follow the same conventions and notations as in MLL proof-structures. In particular, $\bowtie$ and $\ominus$ hyperedges are structurally identical to $\mathcal{Y}$ and $\otimes$ hyperedges. Labelled proof-structures are also defined in the same way.

**§73.12 Definition (MLL2I cut-elimination).** Let $S := (V, E, \mathbf{in}, \mathbf{out}, \ell_E, \mathbf{dep})$ be an MLL2I proof-structure with a cut $e_{\text{cut}} \in E$ such that $\mathbf{in}(e_{\text{cut}}) = (v_1, v_2)$ with both $v_1$ and $v_2$ being conclusions of some hyperedges $e_1$ and $e_2$ such that $\ell_E(e_1) = (u_1, u_2)$ and $\ell_E(e_2) = (w_1, w_2)$. Assume $u_1$ is conclusion of some hyperedge $e_{\bowtie}$ and that we have $\mathbf{box}(w_1) = (V_b, E_b)$. There are several cases depending on $\ell_E(e_{\bowtie})$.

◇ **Weakening** Assume $\ell_E(e_{\bowtie}) = \mathbf{w}$ with $\mathbf{in}(e_{\bowtie}) = \emptyset$. We erase $w_1$, all its parents and dependent vertices. The elimination of $e_{\text{cut}}$ is a new proof-structure

$$ S' := (V', E', \mathbf{in}', \mathbf{out}, \ell_E, \mathbf{dep}') $$

with $V' := V - \{v_1, v_2, u_1, w_1\} - V_b$, $E' := (E - \{e_{\text{cut}}, e_1, e_2, e_{\bowtie}\} - E_b) \cup \{e'_{\text{cut}}\}$, $\mathbf{in}'(e'_{\text{cut}}) = (v_2, w_2)$ and $\mathbf{in}'(x) = \mathbf{in}(x)$ otherwise, dep' is dep with its domain restricted to $\text{dom}(\mathbf{dep}) - \mathbf{dep}(w_1)$.

◇ **Dereliction** Assume $\ell_E(e_{\bowtie}) = \mathbf{d}$ with $\mathbf{in}(e_{\bowtie}) = v_d$. We remove the dependencies of
$w_1$. The elimination of $e_{cut}$ is a new proof-structure

$$S' := (V', E', \mathbf{in}', \mathbf{out}', \ell_E, \mathbf{dep}')$$

with $V' := V - \{v_1, v_2\}$, $E' := (E - \{e_{cut}, e_1, e_2, e_\kappa\}) \cup \{e_{cut}^1, e_{cut}^2\}$, $\mathbf{in}'(e_{cut}^1) = (v_d, w_1)$, $\mathbf{in}'(e_{cut}^2) = (v_2, w_2)$ and $\mathbf{in}'(x) = \mathbf{in}(x)$ otherwise, $\mathbf{dep}'$ is $\mathbf{dep}$ with its domain restricted to $\mathbf{dom}(\mathbf{dep}) - \mathbf{dep}(w_1)$.

◇ **Contraction** Assume $\ell_E(e_\kappa) = \mathbf{c}$ with $\mathbf{in}(e_\kappa) = (v_c^1, v_c^2)$. We duplicate the dependencies. The elimination of $e_{cut}$ is a new proof-structure

$$S' := (V', E', \mathbf{in}', \mathbf{out}', \ell'_E, \mathbf{dep}')$$

with $V' := (V - \{v_1, v_2\}) \cup \sigma(V_b \cup \{w_1\})$ with $\sigma$ renaming vertices with fresh names, $E' := (E - \{e_{cut}, e_1, e_2, e_\kappa\} - \sigma(E_b)) \cup \{e_{cut}^{1,1}, e_{cut}^{1,2}, e_{cut}^2\}$ with $\sigma$ renaming edges with fresh names, $\mathbf{in}'(e_{cut}^{1,1}) = (v_c^1, w_1)$, $\mathbf{in}'(e_{cut}^{1,2}) = (v_c^2, \sigma(w_1))$, $\mathbf{in}'(e_{cut}^2) = (v_2, w_2)$ and $\mathbf{in}'(x) = \mathbf{in}(x)$ otherwise, $\mathbf{dep}'(\sigma(w_1)) = \sigma(\mathbf{dep}(w_1))$ and $\mathbf{dep}'(x) = \mathbf{dep}(x)$ otherwise and $\mathbf{out}'$ defined as expected.

# 74 Simulation of cut-elimination

§74.1 Mechanisms of duplication and erasure are already present in stellar resolution. It is similar to the fact that, in biology, we are observing and speaking about cell division.

§74.2 **Definition (Exponential basis of representation)**. The multiplicative basis of representation $\mathbb{B} = (V, F, \mathbf{ar}, \lfloor \cdot \rfloor)$ is extended with a binary function symbol $\bullet \in F$ with $\mathbf{ar}(\bullet) = 2$, considered left associative, i.e. $t \bullet u \bullet v := (t \bullet u) \bullet v$, variables $Y_i \in V$ for $i \in \mathbf{N}$ representing boxes and three constants $\mathbf{w}, \mathbf{c}, \mathbf{d} \in F$ such that $\mathbf{ar}(\mathbf{w}) = \mathbf{ar}(\mathbf{c}) = \mathbf{ar}(\mathbf{d}) = 0$. The symbol $\cdot$ has priority over $\bullet$, i.e. $t \cdot u \cdot v := (t \cdot u) \cdot v$ and $t \cdot u \cdot v := t \cdot (u \cdot v)$.

§74.3 **Remark (Inductive definition of MLL2I proof-structures)**. The inductive definition of proof-structure (cf. Remark 66.5) is extended with the two new connectives $\times$ and $\ominus$. We write $\mathbf{ETens}^{u,v}(S)$ (resp. $\mathbf{EPar}^{u,v}(S)$) for a proof-structure $S$ linked by $\ominus$ (resp. $\times$) hyperedge with premises $u$ and $v$.

In the same fashion, we introduce inductive constructions for structural rules: $\mathbf{W}(S)$ (nullary), $\mathbf{D}^u(S)$ (unary) and $\mathbf{C}^{u,v}(S)$ (binary).

§74.4 The idea is that given a multiplicative address $u(t)$ of a well-formed vehicle, it can be turned into a non-linear address with $u(t \bullet Y)$ for some fresh variable $Y$. The right part of $\bullet$ contains exponential information. It can then interact by cut with several copies of a same atom: $v(t \bullet (1 \cdot Y))$ and $v'(t \bullet (\mathbf{r} \cdot Y'))$.
**§74.5 Definition (Address of an atom).** We define the *path address* $pAddr_S(v)$ of an atom $v$ in a proof-structure $S$ inductively (cf. Remark 66.5):

• if $S \in \{\mathbf{Ax}_{v,*}, \mathbf{Ax}_{*,v}, W(S')\}$ then $pAddr_S(v) = X$;

• if $S = D^v(S')$ then $pAddr_S(v) = pAddr_{S'}(v) \bullet d$;

• if $S = C^{w'_1,w'_2}(S')$ and $pAddr_{S'}(w_i) = t \bullet u$ for $i \in \{1,2\}$ then $pAddr_S(w_1) = t \bullet (1 \cdot u)$ and $pAddr_S(w_2) = t \bullet (r \cdot u)$ such that $w'_i$ is a conclusion with $w_i$ above $w'_i$;

• if $S = S_1 \uplus S_2$ and $v \in V^{S_i}$ then $pAddr_S(v) = pAddr_{S_i}(v)$;

• if $S \in \{\mathbf{Par}^{v',*}(S'), \mathbf{Tens}^{v,*}(S'), \mathbf{EPar}^{v',*}(S')\}$ then $pAddr_S(v) = 1 \cdot pAddr_{S'}(v)$ such that $v'$ is a conclusion with $v$ above $v'$;

• if $S \in \{\mathbf{Par}^{*,v'}(S'), \mathbf{Tens}^{*,v'}(S'), \mathbf{EPar}^{*,v}(S')\}$ then $pAddr_S(v) = r \cdot pAddr_{S'}(v)$ such that $v'$ is a conclusion with $v$ above $v'$;

• if $S = \mathbf{ETens}^{w'_1,w'_2}(S')$, then for a fresh variable $Y_i \in V$ (representing a box),

– $pAddr_S(w_1) = (1 \cdot pAddr_{S'}(w_1)) \bullet Y_i$;

– $pAddr_S(w_2) = (r \cdot pAddr_{S'}(w_2)) \bullet Y_i$;

– we update the path address of all $u \in \mathbf{box}(w_i)$ from $pAddr_{S'}(u) = t \bullet u$ to $(t \bullet u) \bullet Y_i$

such that $w'_i$ is a conclusion with $w_i$ above $w'_i$.

• $pAddr_S(v) = pAddr_{S'}(v)$ otherwise.

The path address to $v$ is uniquely defined w.r.t. to a conclusion $c \in \mathbf{Concl}(S')$ where $S'$ is $S$ without cuts, i.e. $E^{S'} = E^S \setminus \mathbf{Cuts}(S)$ and the rest of $S$ is defined as in $S'$.

There are two cases depending on if $v$ is dependent (there is some vertex $u$ such that $v \in \mathbf{box}(u)$) or not.

• Assume that $v$ is independent. The *address* of $v$ is then defined as the term $\mathbf{addr}_S(v) := c(\mathbf{pAddr}_S(v))$.

• If there is some $u$ such that $v \in \mathbf{box}(u)$, then the address of $v$ is then defined as the term $\mathbf{addr}_S(v) := \mathbf{pAddr}_S(u)\{X := \mathbf{pAddr}_S(v)\}$.

**§74.6 Box/dependencies in stellar resolution.** The trick which simulates exponential boxes (or dependencies in the case of MLL2I) is that translation of proof-structures will be designed so that cut between a $\times$ and a $\ominus$ hyperedge will apply a cut between the left premise of $\times$ and the left premise of $\ominus$ together will all its dependencies, all thanks to term unification. Hence, all connexions (and thus operations) described by the left premise of $\times$ (erasure, duplication, dereliction or more) are locally applied to all elements of an exponential box (arguments of functions).
§74.7 **Erasure in stellar resolution.** Whenever a weakening is linked to the left premise of ⊑ by a cut, the box of this atom must be erased. Now, how to erase stars in a constellation? There exists two translations of weakening nodes. Girard's one and mine.

* Girard's solution is to not translate weakened atoms. Whenever a cut is connected to where the weakening link should be, since there is a hole with a polarised free ray which cannot be filled, it triggers the erasure of the diagram. We can reproduce this behaviour by using the operator $\llcorner$, as explained in Paragraph 52.6. We can choose to do that but then our execution becomes less flexible (this not necessarily a problem);

* my personal solution is to translate weakened atoms $u$ by a star (known as “black-hole” in my thesis):

$$[+u(t), +\omega(X), -\omega(f(X))]$$

where $t$ is the path address of $u$ and $\omega$ is a fresh symbol not appearing in the translation of the whole proof-structure. It triggers an infinite loop for any diagram connected to it and hence it becomes impossible to construct a saturated diagram. I do not claim that this is necessarily a better solution. A problem is that we introduce infinity but we can argue that such loops can be easily detected by modifying concrete or interactive execution.

Let $v$ be a weakened atom in a proof-structure $S$. We write $v^*$ its corresponding translation (either nothing or the star with black hole). In this thesis, I choose to use my solution, hence:

$$v^* := [\text{addr}_S(v), +\omega(X), -\omega(f(X))]$$

where $\omega$ does not appear in the translation of $S$.

§74.8 **Definition (Weakened atoms).** Let $S := (V, E, \text{in}, \text{out}, \ell_E, \text{dep})$ be a MLL2I proof-structure. Its set of weakened atoms is defined by $\text{Weak}(S) := \{u^* | \exists e \in E. \ell(e) = w, \text{out}(e) = u\}$.

§74.9 **Definition (Translation of the computational content of a proof).** The vehicle and the cuts of a MLL2I proof-structure $S$ are respectively defined by the following constellations:

$$\Phi_S^{\text{ax}} := \sum_{e \in \text{Ax}(S)} [\mu(\text{addr}_S(\vec{e})), \mu(\text{addr}_S(\vec{e}))] + \sum_{u \in \text{Weak}(S)} v^*,$$

$$\Phi_S^{\text{cut}} := \sum_{e \in \text{Cuts}(S)} [-\vec{e}(X), -\vec{e}(X)].$$

such that $\mu(c(t)) = +c(t)$ when $c = \vec{e}$ or $c = -\vec{e}$ for some $e \in \text{Cuts}(S)$ (it is related to a cut) and $\mu(x) = x$ otherwise. We define the computational content of $S$ as the constellation $\Phi_S^{\text{comp}} := \Phi_S^{\text{ax}} \uplus \Phi_S^{\text{cut}}$.
<figure><img src="image_130.png" /><figcaption>(a) Proof-structure representing the translation of the identity function of λ-calculus.</figcaption></figure>

<figure><img src="image_131.png" /><figcaption>(b) Proof-structure representing the translation of the left projection function λxy.x of λ-calculus.</figcaption></figure>

<caption>Figure 74.1: Examples of translations of MLL2I proof-structures. With Girard's translation, we would not have [+10(1·X), +ω(X), -ω(f(X))] and +11(1·X·Y₀) would be linked to nothing through the cut [-10(X), -11(X)].</caption>
§74.10 Examples of MLL2I proof-structures and their translation in stellar resolution are given in Figure 74.1. As for MLL, the idea is to execute interpretation of proof-structures in order to simulate their cut-elimination.

§74.11 **Theorem** (Simulation of MLL2I cut-elimination). For an MLL2I proof-net $\mathcal{R}$ such that $\mathcal{R} \rightsquigarrow^* \mathcal{S}$ with $\mathcal{S}$ in normal form, we have $\mathbf{AEx}(\Phi_{\mathcal{R}}^{\text{comp}}) \simeq_S \Phi_{\mathcal{S}}^{\text{ax}}$.

*Proof.* We sketch the proof without giving details. All multiplicative cases have already been treated in the stellar interpretation of MLL (cf. Lemma 67.9). The only new cut case for MLL2I corresponds to a cut between $\times$ and $\ominus$. It makes the left premises interact with the right ones as in a $\otimes/\nparallel$ cut-elimination. The right premises are multiplicative cases so we focus on the interaction between the left premises which connects boxes/dependencies with structural rules.

• If the left premise of $\times$ is conclusion of a weakening link $w$, then it is translated with a black hole which prevents any rays $+v(1 \cdot t_i \bullet Y_i)$ coming from the left premise of $\ominus$ (because of the path through the cut) to construct a saturated diagram. Hence all these stars are erased in the normal form. Those rays are exactly the translation of vertices of the box associated with the left premise of $\ominus$.

• If the left premise of $\times$ correspond to derelicted atoms $+u(t_i \bullet d)$ with interacts with left premises $-v(w_j \bullet Y_j)$ of $\ominus$ such that $t_i \rightsquigarrow w_j$, then variables $Y_j$ are replaced by $d$, linearising all rays $-v(w_j \bullet Y_j)$. Hence, all potential of duplication given by the variable $Y_j$ is cancelled with the constant 1. This corresponds to a box opening.

• Finally, if the left premise of $\times$ corresponds to $n$ copies $+u_1(t \bullet u_1), \dots, +u_n(t \bullet u_n)$, then they all match with the left premises $+v_1(w \bullet Y_1), \dots, +v_m(w \bullet Y_m)$ of $\ominus$ such that $t \rightsquigarrow w$. This triggers duplications of all the $v_i$ which are considered as part of the same box. Each $+v_i(w \bullet Y_i)$ is duplicated into $+v_1(w \bullet u_1), \dots, +v_n(w \bullet u_n)$ where the $u_i$ are copy identifiers induced by trees of contraction.

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

§74.12 **Example.** If we take the proof-structure of Figure 74.1b, the left premise of $\ominus$ will be entirely erased by a weakening link. Then the axiom between 1 and 2 will be connected to the output axiom between 9 and 8. The proof-structure encodes the term $(\lambda x.\lambda y.y)z$ reducing into $\lambda y.y$. As expected, the normal form of the proof structure is the axiom between 1 and 3 where 1 is made non-linear with dereliction.

## 75 Girard's original correctness criterion

§75.1 In the last paper of geometry of interaction [Gir13a], Girard suggested a correctness criterion for the interpretation of MLL2I in stellar resolution. In the first paper of transcendental syntax [Gir17, Section 5], he updated his criterion to a simpler criterion with switchings (as in Danos-Regnier correctness).
§75.2 This correctness criterion cannot be expressed directly with proof-structures (at least without changing the definition of proof-structures) since it deeply relies on mechanisms of stellar resolution. Moreover, I choose to not give a notion of MLL2I proof-net and consider MLL2I proof-structures as independent from the usual theory of linear logic. Hence we are not trying to simulate a specific correctness criterion. I simply describe Girard's correctness and informally explain its purpose. No adequacy result is stated but Girard sketched a proof in his paper [Gir17, Section 5.7].

§75.3 **Definition (MLL2I switching).** Let $\mathcal{S}$ be a MLL2I proof-structure. A MLL2I switching is defined as a MLL switching $\varphi$ extended with $\varphi(e) \in \{\ominus_X, \ominus_1\}$ when $\ell(e) = \ominus$ and $\varphi(e) \in \{\bowtie_L, \bowtie_R\}$ when $\ell(e) = \bowtie$.

§75.4 **Definition (MLL2I test).** Let $\mathcal{S}$ be a MLL2I proof-structure and $\varphi$ one of its switchings. The test associated with $\mathcal{S}^\varphi$ is the constellation defined by

$$ \Phi_S^\varphi := \Phi_S^{\text{cut}} \uplus \sum_{v \in V^{S\varphi}} v^\star. $$

We define the translation $v^\star$ of a vertex $v$ conclusion of an hyperedge $e$ as follows:

* if $v$ is conclusion of a d hyperedge of input itself below some $e$ such that $\ell(e) = \text{ax}$, then

$$ v^\star = \begin{bmatrix} -\text{addr}_S(v) \\ +v(X \bullet Y) \end{bmatrix}; $$

* if $\ell_E(e) = \ominus_X$ and $\text{in}(e) = (u, w)$ then $v^\star = \begin{bmatrix} -u(X \bullet X), -w(X) \\ +v(X) \end{bmatrix}$;

* if $\ell_E(e) = \ominus_1$ and $\text{in}(e) = (u, w)$ then $v^\star = \begin{bmatrix} -u(X \bullet 1), -w(X) \\ +v(X) \end{bmatrix}$;

* if $\ell_E(e) = \bowtie_L$ and $\text{in}(e) = (u, w)$ then

$$ v^\star = \begin{bmatrix} -u(X \bullet Y) \\ +v(X \bullet Y) \end{bmatrix} + \begin{bmatrix} -w(X), -\infty(X) \\ +\infty(X) \end{bmatrix}; $$

* if $\ell_E(e) = \bowtie_R$ and $\text{in}(e) = (u, w)$ then

$$ v^\star = \begin{bmatrix} -u(X \bullet Y) \end{bmatrix} + \begin{bmatrix} -u(X' \bullet Y') \end{bmatrix} + \begin{bmatrix} -w(X) \\ +v(X) \end{bmatrix} $$

where the star $[-u(X' \bullet Y')]$ is not used when $X'$ can be instantiated *exactly* to $X$, meaning that it is replaced by exactly the variable $X$ (name of variables are taken into account, unlike usual).

The other cases are the same as for the multiplicative case (cf. Definition 68.3).
**§75.5** Similarly to the multiplicative case, we require that the interaction $\mathrm{Ex}(\Phi_S^{\mathrm{ax}} \uplus \mathrm{Ex}(\Phi_S^{\varphi}))$ between a vehicle and a MLL2I test produces the star of roots $[v_1(X), \dots, v_n(X)]$ where $\{v_1, \dots, v_n\} \subseteq \mathrm{Concl}(S)$. We require that $v_1, \dots, v_n$ correspond to all linear conclusions not having addresses of the shape $X \bullet u_i$ for some $u_i$. My understanding of Girard's restriction is that we allow underlined conclusions in sequents but such conclusions can be erased or duplicated an arbitrary number of times and we cannot require a specific number of copies. Therefore, no conditions are required for non-linear conclusions.

**§75.6** **Left-exponential tensor case.** The purpose of the two tests for $\ominus$ is to check that the terms used have the right shape: we need that the left input is a non-linear atom of address $t \bullet Y$ where $Y$ does not appear in $t$. A non-linear atom $r := +u(t \bullet v)$ passes the two tests $\ominus_X$ and $\ominus_1$ when $t$ matches with $X$ and $v$ with both $X$ and $1$. First, $t$ must be variable because otherwise, in the two tests, it would be connected to the variable $X$ of $-u(X \bullet X)$ and $-u(X \bullet 1)$ which propagates a term to the conclusion which makes impossible to obtain all roots of the form $u'(X)$. Hence we have $r = +u(X' \bullet v)$. We must have the matchings $v \bowtie X$ (hence $v \bowtie X'$ and $X' \bowtie X$) and $v \bowtie 1$. The only way to have $v \bowtie 1$ is that either $v = 1$ or $v$ is a variable.

• If $v = 1$ then when $r = +u(X' \bullet 1)$ connected to $-u(X \bullet X)$ of the test of $\ominus_X$, the constant $1$ is propagated and we produce an output $+u'(1)$ which prevents us to obtain the exact star of roots as normal form. Therefore, we cannot have $v = 1$.

• If $v = Y$, then we have $r = +u(X' \bullet Y)$. In the test $\ominus_1$, it has to match with $-u(X \bullet 1)$. Hence $Y = 1$. If $X' = Y$ then, again, the constant $1$ will be propagated to a conclusion. Finally, $Y$ must be a variable different from $X'$.

**§75.7** **Left-exponential par case (right switching).** The test $\times_R$ is very similar to the test $\mathcal{Y}_R$. The difference is that we would like to cancel $n \in \mathbb{N}$ copies of non-linear atoms of the form $+u(t_i \bullet u_i)$. We would like to ensure that all $t_i$ are variables (the $u_i$ can be exponential copy identifiers). Girard's trick is to take the actual name of variables into account and to consider *coherent constellations* (which are introduced in his second paper on transcendental syntax [Gir16b] and not introduced here) which excludes some substitutions between stars. In our definition of test, this is expressed in the side condition of $\times_R$. Girard's trick enforces $t_i$ to be *exactly* $X$.

• Imagine that all $t_i$ are $X$. Then the test $\times_R$ behaves in the same way as a test $\mathcal{Y}_R$ because $X'$ can be instantiated to $X$ and hence the star $[-u(X' \bullet Y')]$ cannot be used.

• If one $t_i$ is different from $X$ then $X'$ cannot be instantiated to $X$ and the two stars $[-u(X \bullet Y)]$ and $[-u(X' \bullet Y')]$ are used. This duplicates the star $+u(t_i \bullet u_i)$ twice which alters the normal form which is expected to be the exact star of roots.

Personally, I do not like the trick used but I never took the time to think about another solution.
<figure><img src="image_133.png" /><figcaption>Figure 75.1: Two possible situations for the switching $\times_L$.</figcaption></figure>

**§75.8 Left-exponential par case (left switching).** The test $\times_L$ is more subtle. Girard requires that $\times_L$ is *cancelling*, meaning that any interaction with it normalises into the empty constellation $\emptyset$ (this is the main point which cannot really be represented with usual proof-structures and which takes advantage of the mechanisms of stellar resolution). The problem is that the current flows through the left premise but the left premise, which is non-linear, can be erased or duplicated. I changed Girard's definition by adding a black hole so that it is consistent with the execution I defined. Girard's original definition can be found in his paper [Gir17, Section 5.5]. The effect of the black hole is that any stars reaching $\begin{bmatrix} -w(X), -\infty(X) \\ +\infty(X) \end{bmatrix}$ will never be able to form a saturated diagram. The two possible situations are given in Figure 75.1.

* **Case 1** The star corresponding to $\times_L$ is connected to all (possible none) the copies of atoms $u_1, \dots, u_n$. Assume one of these atoms has a path leading to $v$ by a cut. We obtain a cycle and infinitely many correct diagrams. Execution is not strongly normalising in this case. Hence, the proof-structure is not correct.

* **Case 2** Assume we do not have the cycle of Case 1 and that some atoms among $u_1, \dots, u_n$ possibly have a path reaching an atom of $w$. If we wish to keep connectedness then all stars must be connected. Because of the star

$$[-w(X), +\infty(X), -\infty(X)]$$

of $\times_L$, all stars connected to an atom of $w$ (actually the whole constellation) will be erased because unable to produce a saturated diagram. The normal form is $\emptyset$.

By using the trick of black hole (Girard simply leaves a free polarised ray which destructs the whole diagram with the operator $\downarrow$, cf. Paragraph 62.5), we are able to keep connectedness (which was the main problems of exponentials). In particular, if there is no $u_i$, in Case 2 the black hole still erases everything and in Case 1, we loose connectedness since $w$ is isolated.

**§75.9 Example (Correct proof-structures).** The proof-structure representing the identity function in Section 74 has two switchings $\times_L$ and $\times_R$ for its only $\times$ link.
• The first test (right switching) is:

$$ 
\begin{bmatrix} -4(\mathbf{1} \cdot X \bullet \mathbf{d}) \\ +3(X \bullet Y) \end{bmatrix} + 
\begin{bmatrix} -4(\mathbf{r} \cdot X) \\ +2(X) \end{bmatrix} + 
\begin{bmatrix} -3(X \bullet Y) \\ +4(X) \end{bmatrix} + 
\begin{bmatrix} -3(X' \bullet Y') \\ +4(X) \end{bmatrix} + 
\begin{bmatrix} -4(X) \\ 4(X) \end{bmatrix} + 
\begin{bmatrix} -4(X) \\ 4(X) \end{bmatrix} 
$$

The test is executed into:

$$ 
\begin{bmatrix} -4(\mathbf{1} \cdot X \bullet \mathbf{d}) \\ +4(X \bullet Y) \end{bmatrix} + 
\begin{bmatrix} -4(\mathbf{r} \cdot X) \\ 4(X) \end{bmatrix} 
$$

We connected to the vehicle [+4(1·X·d), +4(r·X)] of Section 74, we obtain
[4(X)], as expected.

• the second test (left switching) is:

$$ 
\begin{bmatrix} -4(\mathbf{1} \cdot X \bullet \mathbf{d}) \\ +3(X \bullet Y) \end{bmatrix} + 
\begin{bmatrix} -4(\mathbf{r} \cdot X) \\ +2(X) \end{bmatrix} + 
\begin{bmatrix} -3(X \bullet Y) \\ +4(X \bullet Y) \end{bmatrix} + 
\begin{bmatrix} -2(X), -\infty(X) \\ +\infty(X) \end{bmatrix} + 
\begin{bmatrix} -4(X) \\ 4(X) \end{bmatrix} 
$$

It reduces into:

$$ 
\begin{bmatrix} -4(\mathbf{1} \cdot X \bullet \mathbf{d}) \\ 4(X) \end{bmatrix} + 
\begin{bmatrix} -4(\mathbf{r} \cdot X), -\infty(X) \\ +\infty(X) \end{bmatrix} 
$$

When connected to the vehicle [+4(1·X·d), +4(r·X)] of Section 74, we obtain
a connected constellation which normalises into ∅ because of the black hole using
the symbol ∞. This cancels the test, as expected.

**76 Discussion: what is a non-linear proof?**

§76.1 Non-linear proofs are proofs which are able to erase or duplicate some logical entities such as occurrences of labels representing formulas in sequent calculus. In proof-net theory, it would correspond to the duplication and erasure of some sub-proof-structures.

§76.2 When expressing duplication and erasure in stellar resolution, we have very general and alogical notions which can be used. Duplication is expressed by the fact that a ray can
be required by several other matchable rays. For instance, if we can have a ray $-1(X)$ compatible with two rays $+1(1)$ and $+1(r)$. The execution will duplicate $+1(X)$ to satisfy the two constraints. Now, what is exponential linear logic in regards to those "natural/primitive" non-linear mechanisms?

§76.3 It appears that exponentials (at least the intuitionistic implication) can be seen as a way to format those non-linear mechanisms. It is *one way* to behave non-linearly. We already knew that we could obtain several non-linear logics by changing the exponential rules of linear logic (to obtain soft linear logic or elementary linear logic for instance) but we can now even go outside of any primitive logical system. The only limit is the primitive computational mechanisms we consider.

§76.4 By formatting, I mean choosing a specific shape for objects. The rays we considered in the chapter are very specific: they have the shape $c(t \cdot u)$. This allows for the consideration of nested boxes. But we could also consider alternative non-linear formatting which could not (at least not naturally) exist if we were starting from linear logic as a primitive notion.
# Chapter 12

## Apodictic experiments

Now that we defined a few interpretations of proof-structures within stellar resolution, we will dive even more into the peculiarities of transcendental syntax. In this chapter, we explore the *apodictic* fragment of linear logic which is linear logic “with no external constraints” or “without system”. I refer to Section 44 for conceptual explanations about what Girard means by first-order logic (apodictic).

In apodictic linear logic, we are no more interested in reproducing known objects. We are trying to do (linear) logic with stellar resolution as elementary material by designing constellations and tests which define non-primitive logical concepts.

In his recent unpublished papers, Girard used the expression of “system-free logic” [Gir19, Gir20b]. But in what sense is all this “system-free”? A remark I often encountered is that linear logic is no more “system-free” than other systems: it is itself a logical system. This is indeed correct. Linear logic is a logical system since we suggested an interpretation of it into stellar resolution in the previous chapters but in transcendental syntax it is possible to speak about linear logic with no reference to a system. In particular, there is no notion of logical atomic variable, no primitive connectives and many connectives can co-exist<fnref n="1" />.

Everything in this chapter is my own interpretation of Girard’s ideas. I sometimes choose to change the original presentation according to my liking and understanding. Everything in this chapter is experimental since no true and complete development of these ideas has been suggested yet.

## 77 Logical constants

§77.1 According to Girard, proof-structures correspond to the first occurrence of first-order logic in his works. Proof-structures were initially defined with logical atoms as leaves. These atoms are substitutable objects which are all bound to a name. All atoms of

<footnote n="1">¹This is similar to the notion of function/procedure coming from modules/libraries in programming. It happens that some imported programs are incompatible but it may also be possible to make them compatible with a bit of hacking (you can also think of LaTeX packages as Girard himself does).</footnote>
same name can be replaced by a same proof-structure. In particular, proof-nets remain correct under substitution. But this replacement of variables is an *external* consideration of proof-structures. Proof-structures by themselves can be handled without substitutable atoms like non-generic objects (such as natural numbers). By doing so, we necessarily focus on the *individuality* of logical objects, independently of their generic meaning (usual logical objects are representatives of a class instead of individuals).

§77.2 In the stellar interpretation of proof-structures, atoms are simply translated as rays with nothing special about them. Because proof-structures can be handled as *it is*, with atoms which are simply points in space, Girard designed atomic formulas/behaviours to give a first-order status to these points. In the approach Girard calls *morphologism* [Gir18a, Section 1.1.2] (cf. Paragraph 39.2), formulas capture the shape of objects. There exists two natural constants we can imagine:

• フ (fu) which contains atomic constellations with a single objective polarised ray and

• フ (wo) which contains atomic constellations with a single subjective polarised ray.

Combinations of these constants will characterise proof-structures. For instance, フ ⊗ フ will be the type of proof-structures of shape $[r] + [r']$ where r and r' are objective rays. There is no restriction over unpolarised rays (roots).

§77.3 **Remark.** Because our variables were not substitutable in our previous stellar interpretation of MLL, we actually defined “apodictic MLL” or “system-free MLL” and not the “real” MLL coming from the MLL sequent calculusª.

**Objective constant**

§77.4 The idea (which has been imagined in Girard's second paper on transcendental syntax [Gir16b, Appendix A.3]) is to reproduce the behaviour of interactive partitions (cf. Section 37) in which only shape matters, not the semantic content. We would like to see rays as points and stars as sets of points. Points of two constellations can be linked bijectively and we expect the connexion to form a connected and acyclic graph. The logical constant corresponds to a single point. It can only be connected to another single point, hence it is *self-dual*, which is usually contradictory if we interpret orthogonality as a logical negation.

§77.5 We need to distinguish between objective and subjective points but also between linear and non-linear points. These principles did not exist with partitions but since they exist in stellar resolution, we would like to take them into account. In particular, we need adapters to connect rays of *same class*. Typically, it makes no sense in proof-net theory to connect a linear point with a non-linear one (although not recommended, it is still

<footnote>ªYes, after all these pages and more than 3 years of thesis, I did not even interpreted MLL, the simplest fragment of linear logic.</footnote>
possible in our case). In the definition below, I suggest a classification of rays. I tried
several naive definitions but none were satisfying so the right definition of an apodictic
fragment of linear logic is still open.

§77.6 **Definition (Ray order).** The order of a polarised ray $r$ is given by its number of distinct variables $ord(r) := |\mathit{vars}(r)|$.

§77.7 **Example.** The ray $+1$ is of order $0$, the ray $+1(X)$ of order $1$ and $+1(X \bullet Y)$ of order $2$.

§77.8 **Remark.** My previous interpretation of the weakening rule produces rays of order 1 but it should not be a problem to add a variable to make them of order 2 without affecting their computational behaviour.

§77.9 We first focus on rays of order 0 which are actually sufficient for MLL although we actually used rays of order 1. Rays of order 0 directly translate the interpretation of MLL into finite permutations and partitions over set of natural numbers.

§77.10 **Definition (Regular adapter).** Let $[r, s]$ be an adapter of a constellation $\Phi$. It is regular if:

• it is non-animist (cf. Definition 48.10), i.e. $r$ and $s$ are either both subjective or both objective;

• $ord(r) = ord(s)$.

§77.11 **Definition (Structural orthogonality).** Two constellations $\Phi$ and $\Phi'$ are *structurally orthogonal*, written $\Phi \perp^S \Phi'$ when $\Phi \perp^R \Phi' \oplus \Phi_\mu$ where $\Phi_\mu$ is a constellation of regular adapters linking rays of $\Phi$ to rays of $\Phi'$, and $|\pm \mathrm{IdRays}\Phi| = |\pm \mathrm{IdRays}\Phi'|$.

§77.12 In the case we interpret MLL with rays of order 1, the last requirement ensures that we do not end up in weird situations not corresponding to proof-structures, such as the star $[+1(X)]$ being orthogonal to the star $[-1(1 \cdot X), -1(r \cdot X), 3(X)]$ not having the shape of a test for atoms: the ray $+1(X)$ is required by two rays $-1(1 \cdot X)$ and $-1(r \cdot X)$, and it triggers a duplication leading to the expected normal form $3(X)$. In other words, rays (which can be seen as ports) of the two constellations should match in a bijective way. Moreover, it faithfully translates the interpretation of MLL with partitions of a set.

§77.13 **Definition (Fu).** We define the following pre-behaviour called *fu*:

$$ \mathcal{R} = \{ \{[r, r_1, \dots, r_k]\} \mid $$

$ord(r) = 0, r$ is polarised and objective, and all $r_i$ are uncoloured\}.
§77.14 **Proposition.** The pre-behaviour **R** is a self-dual behaviour, i.e. **R** = **R**⊥ = **R**⊥⊥.

Proof. Thanks to the condition of non-animism, all rays considered here must be objec-
tive because non-animist adapters preserve the class of rays. Consider a constellation
Φ := [r, r₁, ..., rₖ] ∈ **R**. We try to characterise the shape of constellations Φ' in **R**⊥.
By definition of ⊥<sup>S</sup>, Φ' must have a single coloured ray r'. If there are other stars,
they must be uncoloured and Φ ⊕ Φ<sub>μ</sub> ⊕ Φ' with the right constellation of adapters Φ<sub>μ</sub>
cannot normalise into a single star as needed for ⊥<sup>S</sup>. Hence Φ' only contains a single
star φ' containing r'. This star φ' can contain as many uncoloured rays as possible and
Φ ⊕ Φ<sub>μ</sub> ⊕ Φ' would still normalise into the star of uncoloured rays. Hence, Φ' must be
of the form [r', r'<sub>1</sub>, ..., r'<sub>l</sub>] for r<sub>1</sub>, ..., r'<sub>l</sub> uncoloured. It follows that Φ' ∈ **R**. But since it
fully characterises **R**⊥, we have **R** = **R**⊥. Since **R** = **R**⊥ we have (**R**⊥)⊥ = **R**⊥ = **R**,
proving that **R** is a behaviour.
□

**Subjective constant**

§77.15 The logical constant ℥ which is similar to ℥ except that it contains a subjective ray instead of an objective one.

§77.16 **Definition (Wo).** We define the following pre-behaviour called wo:

$$
\mathcal{R} = \{ \{[r, r_1, \dots, r_k]\} \mid \text{ord}(r) = 0, r \text{ is polarised and subjective, and all } r_i \text{ are uncoloured} \}.
$$

§77.17 **Proposition.** The pre-behaviour **R** is a self-dual behaviour, i.e. **R** = **R**⊥ = **R**⊥⊥.

Proof. Same proof as for **R** (cf. Proposition 77.14).

§77.18 In his French unpublished paper "La logique 2.0" [Gir18a], Girard suggests to define a test for ℥ with the brick $\begin{bmatrix} - ℥ ( - 1 \cdot X ) \\ ℥ ( X ) \end{bmatrix}$ which forces the orthogonal to have an internal colour. However, since I define ℥ as atomic constellation with ray of order 0, the corresponding test has to be $\begin{bmatrix} - ℥ ( - 1 ) \\ ℥ \end{bmatrix}$.

§77.19 **Example.** Formulas only using **R** yield objective stars. If we only use **R**, we have subjective stars. A typical case of animism is **R** ~ ℥ **R** which can be instantiated with [+1, +2(+c)] where [+1] ∈ **R** and [+2(+c)] ∈ **R**.
## Shape specification

§77.20 The purpose of logical constants is to specify the shape of proofs. Behaviours only using ル and リ as atoms show how the constellations they type must be shaped.

§77.21 Full tensor. A big problem we now face is that the tensor does not work anymore on the constants ル and リ because they are not disjoint with themselves and hence cannot be combined with the connective $\otimes$. It is still possible to design a new tensor which behaves as expected. I choose to keep the same symbol to make notations simpler. This tensor is always defined for any constellation.

§77.22 Definition (Full tensor). Let $\mathbf{A}$ and $\mathbf{B}$ be two behaviours (not necessarily disjoint). We define the full tensor by the following behaviour:

$$ \mathbf{A} \otimes \mathbf{B} := \{\Phi_A \uplus \Phi_B \mid \Phi_A \in \mathbf{A}, \Phi_B \in \mathbf{B}, \Phi_A \not\llcorner \Phi_B\}^{\perp\perp} $$

where $\Phi_A \not\llcorner \Phi_B$ means that for all rays $r_A$ in $\Phi_A$ and $r_B$ in $\Phi_B$, $r_A \not\llcorner r_B$.

§77.23 Proposition (Apodictic internal completeness). Let $\mathbf{A}$ and $\mathbf{B}$ be two closed behaviours only using ル and リ as atoms. We have that

$$ \mathbf{A} \otimes \mathbf{B} = \{\Phi_A \uplus \Phi_B \mid \Phi_A \in \mathbf{A}, \Phi_B \in \mathbf{B}, \Phi_A \not\llcorner \Phi_B\}. $$

*Proof.* We consider $\Phi_A \uplus \Phi_B \in \{\Phi_A \uplus \Phi_B \mid \Phi_A \in \mathbf{A}, \Phi_B \in \mathbf{B}, \Phi_A \not\llcorner \Phi_B\}$ where $\Phi_A$ and $\Phi_B$ have disjoint rays. By the definition of $\perp^S$, a constellation $\Phi \in \{\Phi_A \uplus \Phi_B \mid \Phi_A \in \mathbf{A}, \Phi_B \in \mathbf{B}, \Phi_A \not\llcorner \Phi_B\}^{\perp}$ must link rays of $\Phi_A \uplus \Phi_B$ so to have a tree by making bridges between $\Phi_A$ and $\Phi_B$. In particular, $\Phi_A \uplus \Phi_B$ has the same number of polarised rays as $\Phi$. If we try to characterise the shape of elements of $\mathbf{A} \otimes \mathbf{B}$ from that, we obtain the constellations separating back $\Phi$ in order to obtain disjoint components $\Phi'_A$ and $\Phi'_B$, hence exactly the elements of $\Phi_A \uplus \Phi_B \in \{\Phi_A \uplus \Phi_B \mid \Phi_A \in \mathbf{A}, \Phi_B \in \mathbf{B}, \Phi_A \not\llcorner \Phi_B\}$. $\square$

§77.24 The other connectives $\mathcal{R}$ and $\to$ are defined as usual (cf. Section 69).

§77.25 Example. We have the following constellations together with their shape in proof-net theory:

◇ Atom of proof-structure $[+1] \in ル$;

◇ Axiom $[+1, +2] \in (\mathbf{L} \otimes \mathbf{R})^{\perp} = \mathbf{L} \mathcal{R} \mathbf{R}$;

◇ Test for axiom $[-1, 1] + [-2, 2] \in ル \otimes リ$;

◇ Switching par left $[-1, 1] + [-2, 2] \in ル \otimes リ$;

◇ Switching par right $[-1] + [-2, 2] \in ル \otimes リ$;

◇ Tensor proof-structure $[+1] + [+2] \in ル \otimes リ$.
§77.26 Using the canonical basis of interpretation Ω(Λ, i, t) = Λ, it is possible to interpret all MLL formulas by multiplicative combinations of Λ. All MLL sequents using Λ are inhabited. It is then sufficient to use combinations of Λ to speak about constellations in a handy way without caring about the specific terms we use. Given a behaviour written with Λ and Θ, it is possible to extract a proof-structure (like how we synthesize circuits or programs from specifications) by an arbitrary selection of terms satisfying the conditions of ⊥<sup>S</sup>.

§77.27 **Implication and par.** Remark that we have Λ ⊢ Λ = Λ ⊢ ΘΛ, however this is not true that Λ ⊢ Θ = Λ ⊢ ΘΒ in general if we have complex formulas Α, Β ∉ {Λ, Θ} since negation exchanges ⊗ and Θ.

Order 0 multiplicative linear logic

§77.28 Because MLL could already be treated with natural numbers, it is sufficient to define MLL tests with rays of order 0. It is even more natural to do so.

§77.29 **Definition (Order 0 MLL test).** Since we are system-free, we define tests directly on switched formulas (cf. Definition 69.15), independently of proof-structures.

$$
\bullet \ (A \otimes B)^{\star} = \begin{bmatrix} -A, & -B \\ +(A \otimes B) & \end{bmatrix};
$$

$$
\bullet \ (A \mathfrak{R}_L B)^{\star} = \begin{bmatrix} -A \\ +(A \mathfrak{R} B) \end{bmatrix} + \begin{bmatrix} -B \end{bmatrix};
$$

$$
\bullet \ (A \mathfrak{R}_R B)^{\star} = \begin{bmatrix} -A \end{bmatrix} + \begin{bmatrix} -B \\ +(A \mathfrak{R} B) \end{bmatrix}.
$$

The definition is then extended to switched sequents with:

$$
(\vdash A_1, \dots, A_n)^{\star} := \sum_{i=1}^{n} (A_i^{\star} + \begin{bmatrix} -A_i \\ A_i \end{bmatrix}).
$$

§77.30 **Non-linear atoms.** Non-linear atoms used in exponentials can be constructed with ⊙ and ×. For instance, if we have Λ ⊗ Λ then the left premise is turned into a non-linear atom of order 2 of a type written !Λ. The formula !!Λ is of order 3 and so on.

**78 Expansional connectives**

§78.1 In his unpublished paper “La logique 2.0” [Gir18a], Girard imagined alternative exponentials called *expansionals*. Because we are system-free, we are able to freely design connectives by designing tests with constellations. By characterising mechanisms of duplication in stellar resolution, it is then possible to obtain exponential connectives which
could not exist in proof-net theory. In particular, it is possible to imagine several ways
to regulate duplication and obtain various sort of exponentials which may be connected
to computational complexity. I only give the Usine interpretation (with formula labels
and finite tests).

§78.2 Unlike exponentials, these new connectives handle duplication but only for atoms of order 1, while exponentials treat atoms of order $\ge 2$. The idea is that from a ray $+c(X)$ of order 1, it is possible to duplicate it by requiring it with two rays $-c(1 \cdot X)$ and $-c(r \cdot X)$. However, this way of duplicating is weaker than exponentials since we cannot consider nested boxes.

§78.3 Girard's expansionals are dual unary connectives $\downarrow A$ and $\uparrow A$ which can only be used together with multiplicative connectives, as with $\otimes$ and $\times$ (cf. Chapter 11). We have the two new constructions of formulas:

◇ **Node replication** $\downarrow A \otimes B$;

◇ **Node co-replication** $\uparrow A \not\otimes B$.

It is then possible to define a new sort of implication called *insinuation*:

$$
A \to B := \downarrow A \dashv B = \uparrow A \perp \mathfrak{N} B.
$$

§78.4 **Definition (Expansional switching).** We extend the notion of switching with the two following cases:

$$
\varphi(\uparrow) \in \{\uparrow_L, \uparrow_R\} \quad \text{and} \quad \varphi(\downarrow) \in \{\downarrow_f, \downarrow_g\}.
$$

§78.5 **Definition (Expansional test).** We define tests directly on switched formulas (cf. Definition 69.15), independently of proof-structures.

$$
\bullet \ (\downarrow A \otimes B)^{\star} = \begin{bmatrix} -A(X), & -B \\ +\downarrow A \otimes B & \end{bmatrix};
$$

$$
\bullet \ (\uparrow_L A \mathfrak{N} B)^{\star} = \begin{bmatrix} -A(X) \\ +(\uparrow A \mathfrak{N} B) \end{bmatrix} + \begin{bmatrix} -B, & -\infty(X) \\ +\infty(X) & \end{bmatrix};
$$

$$
\bullet (\uparrow_R A \mathfrak{N} B)^{\star} = \begin{bmatrix} -A(X) \end{bmatrix} + \begin{bmatrix} -B \\ +(\uparrow A \mathfrak{N} B) \end{bmatrix}.
$$

§78.6 The test for $\downarrow$ requires that the left premise of $\downarrow A \otimes B$ is of order 1. The test $\uparrow_L$ allows for a non-linear behaviour of the left premise and $\uparrow_R$ is the same as $\mathfrak{N}_R$. My tests are different from Girard's tests [Gir18a, Section 2.1.3] because I distinguish between several orders of rays. It is possible that my definition of expansional does not match with Girard's but I will not provide a further exploration of the subject.
§78.7 As we already did previously in Chapter 10, MLL can be defined with rays of order 1. In particular, although permutations and partitions for MLL are more naturally defined with rays of order 0, usual proof-structures are more natural with rays of order 1 because it is the variable X which allows the duplication of cuts. It shows that even in MLL, an elementary duplication occurs.

§78.8 **Remark about our definition of apodictic in regards to exponentials.** There is a problem with the presentation of apodictic linear logic I suggest in this chapter. Because I connect rays of same order, derelicted atoms (coming from the left premise of $\times$) and non-linear atoms corresponding to the output of a box (left premise of $\ominus$) are technically incompatible. I have no satisfying solution for that. We could say that all terms of address $t \bullet u$ are of same order and hence both a derelicted and other non-linear atoms would be of same order. But this we would give too much credit to the symbol $\bullet$. All this does not really matter since I simply want to present the idea so that it can be developed. It does not need to be perfect.

## 79 Visibility and non-classical truth

§79.1 Without diving into philosophical questions, what is truth? Girard suggested to characterise truth with two technical conditions. It is a predicate over formulas such that:

* there is a special behaviour 0 which is not true;

* it is preserved by execution (cut-elimination).

We can agree or disagree for philosophical reasons but this is still a way to start discussions in formal logic.

§79.2 **Classical truth.** Girard's truth is a property of *constellations* before even being a property of formulas. A classical way to define truth is to say that a constellation $\Phi$ is *true* when it passes some given tests (typically Danos-Regnier tests). Hence, truth depends on some subjective tests but also on what it means to be a "correct proof". Truth matches with provability providing we have a mature definition of proof. We say that a behaviour (representing a formula) is true when it contains a true constellation. Correctness criteria, even the weirdest one we can design, yield different notions of truth. We can say that truth is related to the *objective* relation between an entity and a specification, which although subjective, serves a purpose or represents the expression of a will.

§79.3 **Non-classical truth.** Whereas there is a classical way to define truth, there is also *non-classical ways* which challenge common sense. In his fourth paper on transcendental syntax [Gir20a], Girard suggested a notion of truth called *visibility* which implements the intuition of hidden and visible files (cf. Paragraph 40.6). But how to design a notion of truth? We should make clear what we absolutely want to make true and false (and the interesting part is to leave some gap on which there is no restriction). Typically,
we would like constellations of binary stars to be true since they correspond to axioms and we would like a special behaviour 0 to be false. The constant 0 is defined by using subjective rays which have a role in epidictics.

§79.4 **Epidictic and visibility.** As explained in Section 44, Girard’s second-order logic uses a vehicle together with a mould for existential witnesses. The vehicle is defined with *objective* rays whereas the mould is defined with *subjective* ones. Given a constellation “in the wild”, it is correct when it has no animist star: the objective and subjective part can be separated. To be consistent with this interpretation, we would like to make animist star a reason for falsity. Girard chose to base visibility on the Euler-Poincaré invariant which is a necessary condition for Danos-Regnier correctness but not a sufficient one<fnref n="2" />.

§79.5 **Proposition (Euler-Poincaré invariant).** Let $(V, E)$ be a bipartite multigraph (cf. Appendix C). If $|Cy|$ is the number of minimal cycles and $|CC|$ is the number of connected components, then we have $|V| - |E| + |Cy| - |CC| = 0$.

§79.6 Since we are interested in trees, we have $|CC| = 1$ and $|Cy| = 0$. We can divide $V$ into $V_1$ and $V_2$ since it is bipartite. Hence:

$$2(|V_1| + |V_2| - |E|) = 2|V_1| + 2|V_2| - 2|E| = (2|V_1| - |E|) + (2|V_2| - |E|) = 2.$$

§79.7 Considering that constellations corresponding to proof-structures and tests are related to partitions, the above equations induce a weight on objective constellations. A weight for subjective rays is designed in order to be consistent with our notion of truth.

§79.8 **Definition (Weight of a star).** The weight of a star $\phi$ with objective rays $o_i$ and subjective rays $s_j$ is defined by:

* $\omega([o_1, ..., o_n]) := 2 - n$ when it is fully objective, and

* $\omega([o_1, ..., o_n, s_1, ..., s_m]) := -n$ otherwise.

§79.9 **Definition (Weight of a constellation).** The weight of a constellation $\Phi$ is defined by:

$$\omega(\phi_1 + ... + \phi_n) := \sum_{i=0}^{n} \omega(\phi_i).$$

<footnote n="2">²It is not clear why he chose this invariant in particular but my current understanding is that: it satisfies the conditions of truth and it is odd enough. It also seems that he developed this truth notion to express Peano arithmetic in apodictic linear logic so this may be his original purpose. I once asked him why he did things like that and told him (probably impolitely) that is seemed rather arbitrary for something related to the foundations of logic. I don't know if I hurt his feelings but he ironically told me that Tarski was probably better since he calls true what is true.</footnote>
$$ \omega(\mathcal{R}) := 1 \qquad \omega(\mathcal{F}) := 0 \qquad \omega(\mathbf{A} \otimes \mathbf{B}) := \omega(\mathbf{A}) + \omega(\mathbf{B}) $$

$$ \omega(\mathbf{A}^{\perp}) := 2 - \omega(\mathbf{A}) \qquad \omega(\mathbf{A} \to \mathbf{B}) := \omega(\mathbf{B}) - \omega(\mathbf{A}) $$

$$ \omega(\mathbf{A} \mathcal{F} \mathbf{B}) := \omega(\mathbf{A}) + \omega(\mathbf{B}) \text{ (if both } \mathbf{A} \text{ and } \mathbf{B} \text{ contain } \mathcal{F}) $$

$$ \omega(\mathbf{A} \mathcal{F} \mathbf{B}) := \omega(\mathbf{A}) + \omega(\mathbf{B}) - 2 \text{ (otherwise)} $$

$$ \omega(\mathbf{A} \times \mathbf{B}) := \omega(\mathbf{A} \mathcal{F} \mathbf{B}) \qquad \omega(\mathbf{A} \otimes \mathbf{B}) := \omega(\mathbf{A} \otimes \mathbf{B}) $$

<caption>Figure 79.1: Weights of behaviours.</caption>

§79.10 **Example.** For instance, for a constellation $\Phi \in \mathcal{F} \otimes \mathcal{F}$, we would have $\omega(\Phi) = 2 \times 2 - 2 = 2$ and $\omega(\Psi) = 2 \times 1 - 2 = 0$ for $\Psi \in \mathcal{F} \mathcal{F} \mathcal{F}$. By the Euler-Poincaré invariant, it is then expected that the sum of the weight of two orthogonal constellations is 2.

§79.11 **Definition (Weight of a behaviour).** We define the weight of a behaviour $\mathbf{A}$ as the maximal weight of its constellations: $\omega(\mathbf{A}) := \max\{\omega(\Phi) \mid \Phi \in \mathbf{A}\}$.

§79.12 We obtain the weights of Figure 79.1 for behaviours. Now that we have a notion of weight, it is possible to define a behaviour **0** which is invisible (false). Interestingly, **0** is not empty, unlike the usual denotational interpretations where **0** is empty because it has no proofs. We have constellations but none are correct. In particular, this gives an interactional content to contradictions.

§79.13 **Definition (Zero).** The behaviour zero is defined by $0 := (\mathcal{F} \mathcal{F} \mathcal{F}) \otimes \mathcal{F}$.

§79.14 We can finally define visibility then prove that it corresponds to a notion of truth by satisfying the conditions given in the introduction of this section.

§79.15 **Definition (Visibility).** A constellation $\Phi$ is visible (true) when $\omega(\Phi) \ge 0$. The definition is extended to behaviours by saying that a behaviour $\mathbf{A}$ is visible when $\omega(\mathbf{A}) \ge 0$.

§79.16 Remark that, as expected, constellations of binary stars are visible because all binary objective stars are of weight 0 and the sum of all weights of the constellation is still 0. As for animist stars, by definition they have a weight at most -1. For every additional objective ray, the weight is lowered. For instance: $\omega(\mathcal{F} \mathcal{F} \mathcal{F}) = -1$, $\omega(\mathcal{F} \mathcal{F} \mathcal{F} \mathcal{F} \mathcal{F}) = -2$ and $\omega(\mathcal{F} \mathcal{F} \mathcal{F} \mathcal{F} \mathcal{F}) = -3$. Oddly enough, it is possible to make an animist constellation visible by using a tensor with visible constellations. For instance, we have $\omega((\mathcal{F} \mathcal{F} \mathcal{F}) \otimes \mathcal{F}) = 0$. We can also remark that all formulas using only $\mathcal{F}$ are always visible.
§79.17 **Proposition.** Visibility defines a truth notion: **0** is invisible and it is closed under cut-elimination for proof-structures.

*Proof.* We have $\omega(\mathfrak{0}) = \omega((\mathfrak{7}\intercal\mathfrak{7})\ominus\mathfrak{7}) = \omega(\mathfrak{7}\intercal\mathfrak{7}) + \omega(\mathfrak{7}) = \omega(\mathfrak{7}\intercal\mathfrak{7}) = \omega(\mathfrak{7}\intercal\mathfrak{7}) = \omega(\mathfrak{7}) + \omega(\mathfrak{7}) - 2 = 1 - 2 = -1 < 0$. Notice that it is the presence of animist star which makes **0** invisible. As for cut-elimination, consider that we have $\Phi$ made of binary stars only (since proof-structures are translated only with binary stars). We then have $\omega(\Phi) = 0$, meaning that $\Phi$ is visible. However, cut-elimination only reunites binary stars and hence preserves binarity. We have $\omega(\mathfrak{AEx}(\Phi)) = 0$ which makes $\mathfrak{AEx}(\Phi)$ visible. $\square$

§79.18 Now that we defined the additive contradiction **0**, it is possible to define the additive constant top by duality.

§79.19 **Definition (Top).** The behaviour $top$ is defined by $\top := \mathfrak{0}^{\perp} = (\mathfrak{7} \otimes \mathfrak{7}) \times \mathfrak{7}$.

§79.20 **Proposition.** $\top$ is visible.

*Proof.* We have $\omega((\mathfrak{7} \otimes \mathfrak{7}) \times \mathfrak{7}) = \omega(\mathfrak{7} \otimes \mathfrak{7}) + \omega(\mathfrak{7}) = \omega(\mathfrak{7} \otimes \mathfrak{7}) = \omega(\mathfrak{7}) + \omega(\mathfrak{7}) = \omega(\mathfrak{7}) = 1$. Hence $\top$ is visible. $\square$

§79.21 To be sure that we defined additive constants in the right way, we should check that they correspond to neutral elements for the additive connectives $\oplus$ and $\&$ but since they are defined in second-order, we leave these definitions unverified.

§79.22 We define a notation for tensor and par of logical constants [Gir20a, Section 4.1]. This definition will be useful to make explicit the weirdness of this notion of truth.

§79.23 **Definition (Fu sequence).** We define $\mathfrak{7}_n$ for $n \in \mathbb{Z}$ by:

* $\mathfrak{7}$ when $n = 1$;
* $\mathfrak{7} \otimes \mathfrak{7}_{n-1}$ when $n > 1$;
* $\mathfrak{7} \intercal \mathfrak{7}_{n+1}$ when $n < 1$.

§79.24 **Definition (Wo sequence).** We define $\mathfrak{7}_n$ for $n \in \mathbb{N}$ by:

* $\mathfrak{7}$ when $n = 0$;
* $\mathfrak{7}_n \otimes \mathfrak{7}$ otherwise.

§79.25 As presented in the fourth paper of transcendental syntax [Gir20a, Section 4.3], Figure 79.2 illustrates a “truth table” with counter-intuitive truth values.
<table><caption>Figure 79.2: Odd cases of non-classical truth. The value 1 represents visibility and 0 invisibility.</caption><thead><tr><th>A</th><th>B</th><th>A ⊗ B</th><th>A <i>&#x2610;</i> B</th><th>A<sup>&perp;</sup></th></tr></thead><tbody><tr><td>1</td><td>1</td><td></td><td>0</td><td>1</td></tr><tr><td>0</td><td>1</td><td>1</td><td>0</td><td></td></tr></tbody></table>

◇ **Case of tensor** If we have $\mathbf{A} := \mathfrak{R} \otimes \mathfrak{R}$ (which is not visible since $\omega(\mathfrak{R} \otimes \mathfrak{R}) = 0 + 0 - 2 = -2$) and $\mathbf{B} := \mathfrak{R} \otimes \mathfrak{R}$ (which is visible since $\omega(\mathfrak{R} \otimes \mathfrak{R}) = 1 + 1 = 2$), then we have $\omega(\mathbf{A} \otimes \mathbf{B}) = -2 + 2 = 0 \ge 0$ hence $\mathbf{A} \otimes \mathbf{B}$ is visible.

◇ **Case of par** As for $\mathfrak{R}$, we have $\mathfrak{R}_0 = \mathfrak{R} \otimes \mathfrak{R}$ of weight 0 (visible) but $\mathfrak{R}_0 \otimes \mathfrak{R}_0$ of weight $0 + 0 - 2 = -2$ is invisible. However, if we have $\mathbf{A} := \mathfrak{R}_{-1} = \mathfrak{R} \otimes \mathfrak{R}$ (weight $-1$) which is invisible and $\mathbf{B} := \mathfrak{R}_1 = \mathfrak{R}$ (weight 2) which is visible, then $\mathbf{A} \otimes \mathbf{B}$ is of weight $-1 + 2 - 2 = -1$, hence invisible.

◇ **Case of dual** Finally, for the orthogonal, if we have $\mathbf{A} := \mathfrak{R}_0 = \mathfrak{R} \otimes \mathfrak{R}$ (visible), then $\mathbf{A}^{\perp} = \mathfrak{R} \otimes \mathfrak{R} = \mathfrak{R}_2$, which is visible as well. Hence, orthogonality does not exchange visibility although it satisfies the condition of truth we wish for.

## 80 System-free arithmetic on relative numbers

§80.1 It is possible to define relative numbers as behaviours by using the logical constants.

§80.2 **Definition** (Encoding of relative numbers). Given $p \in \mathbb{Z}$, we define its encoding by a behaviour $[[p]]$ such that:

• $[[0]] := \mathfrak{R}$;

• $[[p]] := \mathfrak{R}_p \otimes \mathfrak{R}$ when $p > 0$;

• $[[p]] := \mathfrak{R}_{p+2} \otimes \mathfrak{R}$ when $p < 0$.

§80.3 **Example.** We have $[[ -1 ]] := \mathfrak{R} \otimes \mathfrak{R}$, $\top = [[ -1 ]] \Rightarrow [[ 0 ]] \text{ and } \mathbf{0} = \top^{\perp} = [[ -1 ]] \otimes [[ 0 ]]$. Also remark that $[[ -n ]] = [[ n ]]^{\perp}$.

§80.4 We present some properties which will be useful to reason about this interpretation of relative numbers.

§80.5 **Proposition.** The following statement holds:

1. $\mathbf{A} \equiv \mathfrak{R}_{\omega(\mathbf{A})}$ (this implies that $\omega(\llbracket p \rrbracket) = p$, i.e. encoded number is reflected in weight of encoding). The notation $\equiv$ is used for linear equivalence;

2. $\mathfrak{R}_m \otimes \mathfrak{R}_n \equiv \mathfrak{R}_{m+n}$ with $m, n > 0$;
<figure><img src="image_134.png" /><figcaption>Figure 81.1: Models of regulation for computational objects.</figcaption></figure>

3. $\mathfrak{R}_{n+2} \nsim \mathfrak{R} \equiv \mathfrak{R}_n$ with $n < 0$ (negative integers are equivalent to some $\mathfrak{R}_n$);

4. $\mathfrak{R}_m \otimes \mathfrak{R}_n \equiv \mathfrak{R}_{m+n}, \mathfrak{R}_m \nsim \mathfrak{R}_n \equiv \mathfrak{R}_{m+n-2}$ and $\mathfrak{R}_n^\perp \equiv \mathfrak{R}_{2-n}$ (combinations of $\mathfrak{R}$ can be contracted);

5. $\mathfrak{R}_m \otimes \mathfrak{R}_n \equiv \mathfrak{R}_m \nsim \mathfrak{R}_n \equiv \mathfrak{R}_{m+n}$ and $\mathfrak{R}_n^\perp \equiv \mathfrak{R}_{-n}$ (combinations of $\mathfrak{R}$ can be contracted);

6. $\mathfrak{R}_n$ and $\mathfrak{R}_{-n}$ are invisible for $n < 0$.

*Proof.* Stated in Girard's fourth paper on transcendental syntax [Gir20a, Section 4]. □

§80.6 **Arithmetic operations.** By relying on the properties of Proposition 80.5, it is possible to do elementary arithmetic operations on relative numbers:

• the constant $\mathfrak{R}$ corresponds to $[1]$;

• $[[n+1]] \equiv \mathfrak{R} \otimes [[n]]$ corresponds to the successor function;

• $[[n-1]] \equiv \mathfrak{R} \dashv [[n]]$ corresponds to the predecessor function;

• $[[n+m]] \equiv [[n]] \otimes [[m]]$ corresponds to addition;

• $[[n-m]] \equiv [[n]]^\perp \nsim [[m]] = [[n]] \dashv [[m]]$ corresponds to subtraction.

§80.7 **Example.** Equivalences are inferred from the properties of Proposition 80.5.

• $[[2+3]] = [[2]] \otimes [[3]] = (\mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R}) \otimes (\mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R}) \equiv \mathfrak{R}_2 \otimes \mathfrak{R}_3 \equiv \mathfrak{R}_5 \equiv \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} = [[5]].$

• $[[2-3]] = [[2]]^\perp \nsim [[3]] = (\mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R})^\perp \nsim (\mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R}) = (\mathfrak{R} \nsim \mathfrak{R} \otimes \mathfrak{R}) \nsim (\mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R} \otimes \mathfrak{R}) \equiv \mathfrak{R}_{-2} \nsim \mathfrak{R}_3 \equiv \mathfrak{R}_1 \equiv \mathfrak{R} \nsim \mathfrak{R} = [[-1]].$

# 81 Discussion: anarchy

§81.1 Apodictics is a state where computational objects express logic without the need for external regulation or control. However, this does not mean that external control should
be excluded: it becomes a choice, something put over what is unregulated. This makes
system-free formalisms such as apodictic transcendental syntax (Figure 81.1a) necessar-
ily more flexible than system-bounded formalisms such as usual logical systems (Fig-
ure 81.1b). Personally, the apodictic part of logic reminds me of decentralised systems
(typically, decentralised communication or cryptocurrencies).

§81.2 **Is apodictics sufficient.** Apodictics is about decentralised logic. Constellations live their live and the synthetics describes their behaviour with formulas or label them with tests. But is it sufficient to speak about logic? I do not have an answer. I believe that it may be sufficient but not satisfying. If logic is about an analysis and study of interaction then we first need a space of interacting entities then the ability to put words on it (the synthetics). But it is not all that matters. Typically, as imagined in Section 60, external control may be related to efficiency for computational power (algorithmic optimisation) but probably also for human readability and workability (tell me if I am wrong if I say that natural deduction is more convenient than reasoning with stellar resolution).

§81.3 Epidictics is exactly what apodictics lacks to express natural deduction. But adding epidictics is not exactly a “return to the outdated traditions”. Instead, it is a layer *over* a space of freely interacting computational objects with freedom at the bottom and authority at the top.
# Chapter 13

## Epidictic experiments

Epidictics, discussed in Section 44, is the part of logic which is generic/substitutable. For instance, in proof-structures, atoms correspond to variables which can be replaced by other proof-structures. There is currently no true theory of epidictics in the context of transcendental syntax. However, it is possible to sketch and think about some ideas already presented by Girard [Gir18b].

## 82 Genericity of proof-structures

§82.1 **Variables.** Two things have to be distinguished. First, the proof-structures we defined in stellar resolution are *apodictic*. They are self-sufficient objects with formula leaves which are simply translated as rays such as +1 for an atom 1. There is nothing special about such rays. But it is not exactly the proof-structures which are defined in the usual theory of proof-nets (or even proofs in proof theory) which are more complex. We usually require that atoms are substitutable, which means that atoms should actually be seen as variables which are *universally* quantified. Hence, to speak about usual proofs, we must think about an interpretation of quantifiers.

§82.2 For conceptual reasons explained in the third article of transcendental syntax [Gir18b, Section 5.1], alternative rules for quantifiers are considered. These rules should *declare* variables and then rules only manipulate variables which are declared<fnref n="1" />. In particular, it

$$ \frac{\beta_1, \dots, \beta_n, \alpha \vdash \Gamma, A}{\beta_1, \dots, \beta_n \vdash \Gamma, \forall \alpha.A} \quad \forall $$

$$ \frac{\beta_1, \dots, \beta_n \vdash \Gamma, \{\alpha := \sigma\}A}{\beta_1, \dots, \beta_n \vdash \Gamma, \exists \alpha.A} \quad \exists $$

Figure 82.1: Rules for quantifiers with declared variables. The left part of the sequent contains variables which are declared. We must have $vars\sigma \subseteq \{\beta_1, \dots, \beta_n\}$ in $\exists$ and $\alpha \notin vars\Gamma$ in $\forall$.

<footnote n="1">¹Some people think that Girard attributes this trick to himself but this does not seem to be the case. He is probably aware that such hacks already existed but he rarely quote other people in his recent papers.</footnote>
is not allowed to use a variable as a mathematical entity by itself which is assumed to
exist and have a content<fnref n="2" />. The rules for quantifiers are given in Figure 82.1.

§82.3 **Universal quantification.** In order to express the fact that a variable is generic, it must fit into the picture for any shape it can take. In the third article on transcendental syntax [Gir18b, Section 5.3], Girard suggests a definition in the case of MLL. A variable $\alpha$ is subject to three switchings $\forall_{id}$, $\forall_{\otimes}$ and $\forall_{\Sigma}$ for all the shapes $\alpha$ and its dual can have: that is, either an irreducible atom, a par or a tensor. Since it seems that we cannot distinguish between an atom and its negation, it is considered in the transcendental syntax that it must be a “human” choice (in the first paper of transcendental syntax, Girard even propose switchings with tests in order to enforce the presence of duality). By imposing dual atoms, we say that cuts (for instance) cannot connect any atoms but that we want some *specific* connexions. We will hence have adapters allowing the connexion of these three $\forall$ tests with atoms and their dual.

§82.4 **Existential quantifiers.** A proof of existential formula turns a sequent $\vdash \Gamma, \{\alpha := \sigma\}A$ (where $\alpha$ is a variable and $\sigma$ a term) into a sequent $\vdash \Gamma, \exists\alpha.A$. If we try to deconstruct such a proof, we obtain three parts: the specification $\vdash \Gamma, \exists\alpha.A$ which we want to prove, the proof itself which corresponds to a computational entity and the existential witness $\sigma$ located in the proof. These three components are translated into: a set of tests, a vehicle containing the computational content of $\sigma$ and another set of tests for $\sigma$. The existential witness (which cannot be inferred from the formula alone) comes with the vehicle together with its own tests. The materialisation of these tests for existential witness in stellar resolution is called *mould*. They are “pre-integrated” tests checking that the existential witness has the right shape.

§82.5 When translating application of existential rules in transcendental syntax, we must also
handle the substitution used in the premise. This is done by a hack which encodes sort
of explicit substitutions in stellar resolution [Gir18b, Section 5.2].

§82.6 **Encoding of terms.** As for the encoding of terms needed to represent existential witnesses. Girard’s solution is to encode terms by multiplicative combinations of $\mathcal{P}$ and equality between terms by linear equivalence. Applications of functions such as $f(a)$ will be treated as a pair $(f, a)$. We then require that the encoding is injective so that $f(t) = f(u)$ implies $t = u$. Actually, there are several solutions providing it satisfies the previous requirement. It does not matter which solution we choose since it is only a matter of representation<fnref n="3" />.

<footnote n="2">²This is actually what is done in some programming languages such as the C language. Variables are first declared (they exist) then defined (we give them a value).</footnote>

<footnote n="3">³As if we had the choice between a binary or hexadecimal encoding of integers.</footnote>
## 83 Usage interpretation of second-order linear logic

**§83.1** In the Usage interpretation, we are interested in the formation of behaviours. As in usual realisability interpretations, quantifiers can be handled by infinite unions and intersections (in Usage, we do not fear infinity). We allow variables $X, Y, Z, ...$ to appear in behaviours. A behaviour is valid only when it contains no variables. It is then possible to substitute a behaviour variable $X$ for a behaviour $T$.

**§83.2** **Definition (Epidictic architecture).** An epidictic architecture is a countable set of behaviours $\mathfrak{C}$ closed by a given set of connectives $C$, by adjunction and by composition, that is:

* for all $* \in C$ of arity $n$ and $A_1, ..., A_n \in \mathfrak{C}$, we have $*(A_1, ..., A_n) \in \mathfrak{C}$ where $*(A_1, ..., A_n)$ is the application of the $n$-ary connective $*$ with premises $A_1, ..., A_n$;

* for all $F, A, B \in \mathfrak{C}$, we have $F \perp A \otimes B = F(A) \perp B$ where

$$F(\mathbf{A}) = \{\mathrm{Ex}(\Phi_F \uplus \Phi_A) \mid \Phi_F \in F, \Phi_A \in \mathbf{A}\};$$

* if $A \dashv B \in \mathfrak{C}$ and $A \in \mathfrak{C}$, then $B \in \mathfrak{C}$.

We may need other conditions to obtain a satisfying definition but we will limit ourselves to those as we will not dive into the details.

**§83.3** The definitions for universal and existential quantification are defined in Girard's fourth paper on transcendental syntax [Gir20a, Section 5.2].

**§83.4** **Definition (Behaviour for universal quantification).** Let $\mathfrak{C}$ be an epidictic architecture. The behaviour $\forall X.A$ is defined by:

$$\forall X.A := \bigcap_{T \in \mathfrak{C}} \{X := T\}A$$

**§83.5** **Definition (Behaviour for existential quantification).** Let $\mathfrak{C}$ be an epidictic architecture. The behaviour $\exists X.A$ is defined by:

$$\exists X.A := (\bigcup_{T \in \mathfrak{C}} \{X := T\}A)^{\perp\perp}$$

**§83.6** Notice that we do not require a closure by bi-orthogonality. However, for the existential quantification which uses a union, we will need a closure as for the tensor of behaviours.

**§83.7** Once we have quantifiers, it is possible to encode the part of logic we did not have in the previous chapters. This encoding has already been mentioned by Girard in the context of System F [Gir11a, Section 12.B.2]. These encodings are also extended (but unproven)
to neutral elements in Lafont’s “Linear logic pages” [Laf99]. In Girard’s recent paper, an encoding of full exponentials is also suggested from neutral elements [Gir17, Section 5.1].

§83.8 **Additive connectives.** The additive connectives which have been ignored until now can be encoded with second-order quantifiers. We start from the connective $\oplus$ corresponding to the intuitionistic $\lor$ in natural deduction. An informal way to think about how the encoding should look like, is to think about what *specification* $\oplus$ should satisfy or how its behaviour (use) may be described. If we look at the rule $\lor E$ (cf. Figure 9.3), it says that for any $C$, if $A$ leads to $C$ and $B$ leads to $C$ then we should obtain $C$. This can be described by the second-order formula $\forall C (A \dashv\neg C) \Rightarrow (B \dashv\neg C) \Rightarrow C$. We obtain the following encoding of additive connectives using behaviours **A** and **B**:

$$ \mathbf{A} \oplus \mathbf{B} := \forall C. (\mathbf{A} \to C) \Rightarrow (\mathbf{A} \to C) \Rightarrow C $$

$$ \mathbf{A} \& \mathbf{B} := (\mathbf{A}^{\perp} \oplus \mathbf{B}^{\perp})^{\perp} $$

§83.9 **Additive neutral elements.** The additive neutral elements can be encoded by the following behaviours:

$$ \mathbf{0} := \forall X.X $$

$$ \mathbf{T} := \exists X.X. $$

If we consider that **0** represents contradiction and $\mathbf{T}$ absolute evidence, then $\exists X.X$ expressed the existence of a provable statement, i.e. of the possibility of an evidence. As for **0**, in usual semantics, we usually do not want everything to be provable$^4$, hence it is interpreted by the absurd statement that every statement is provable.

§83.10 **Full exponentials.** In this thesis, we only defined limited exponentials corresponding to the intuitionistic arrow $\Rightarrow$ and its linear negation. If we would like to define full exponential modalities ! and ? in order to recover the full power of linear logic, then it is possible to use second-order quantifiers together with $\Rightarrow$ as follows:

$$ !\mathbf{A} := \forall X. (\mathbf{A} \Rightarrow X) \to X $$

$$ ?\mathbf{A} := (!\mathbf{A})^{\perp}. $$

The formula $\forall X. (\mathbf{A} \Rightarrow X) \to X$ expressed the fact that **A** can freely be subject to a non-linear behaviour (duplication and erasure) in any context of the epidictic architecture considered.

§83.11 **Multiplicative neutral elements.** There is a known encoding of multiplicative neutral elements based on exponentials and additive neutral elements:

$$ \mathbf{1} := !\mathbf{T} $$

$$ \mathbf{\bot} := ?\mathbf{0}. $$

<footnote n="4">⁴Note that I consider “usual logic” in this case since we are in the epidictics. In the transcendental syntax, when free from any logical system, “being provable” corresponds to the ability to materialise a statement by the constellations of some behaviour. This is usually not a problem.</footnote>
<figure><img src="image_135.png" /><figcaption>Figure 84.1: Proof-nets of predicate calculus. They are mentioned in Girard’s blind spot [Gir11a, Section 11.C.3] and one of his article on quantifiers for linear logic [Gir91].</figcaption></figure>

**84 Usine in the case of predicate calculus: a sketch**

§84.1 Unfortunately, no serious development of the Usine interpretation for second-order logic has been given yet. In order to illustrate the interpretation of quantifiers, Girard suggests to look at predicate calculus instead which is (interestingly) interpreted as a restriction of second-order logic [Gir18b, Section 5] (Recall that in the transcendental syntax, “first” and “second” order are different from usual first and second-order logic).

§84.2 In the third article of transcendental syntax [Gir18b], Girard states a conceptual problem with first-order individuals, which are objects of the universe on which some *properties* apply. For instance, natural numbers, persons, programs etc. The problem is that nothing justify their existence: they purely come from our intuitive perception of logic. They exist because they allow us to express what we have in mind (which can indeed be satisfying enough depending on what we do).

§84.3 As mentioned by Girard, when considering first-order proof-nets (cf. Figure 84.1), predicates such as *P* and individuals such as *t* in ∀*x*.*A and *P*(*t*) play no role, computationally speaking. Actually, we could even remove predicates and individuals and only consider formulas. In other words, it is sufficient to consider everything as a property or statement. In transcendental syntax, since behaviours are considered, properties corresponding to individuals would express what kind of individual they are and this would be materialised by constellations corresponding to instance of that individual. An individual *f*(*a*) would be a specification saying “I am *f*(*a*)” and instead of a property *P*(*f*(*a*)) saying “the individual *f*(*a*) has the property *P*” we would have a statement saying “I’m an individual satisfying property *P*”. To have becomes “to be”. Predicates simply appear as an artificial way to manage allowed and forbidden interactions: social segregation again.

§84.4 **Quantification of predicate calculus.** We end up with a restriction of second-order logic in which quantification is restricted to a specific epidictic architecture encoding the set of all terms considered in a given universe. Hence, when considering tests for
the universal quantification $\forall x.A$, the shape of $x$ is expected to be of a specific shape corresponding to an encoding of term. The same idea applies to existential witnesses.

§84.5 **Encoding of terms.** A constant is of type $\mathcal{P}$. But in order to encode a function symbol $f$, we must be able to encode pairs of symbols. The term $f(a)$ then corresponds to the encoding of $(f, a)$. This encoding has to be *injective*, meaning that whenever $f(a) = f(b)$ then $a = b$ must follow. Girard suggested [Gir18b, Section 2.4] the following encoding inspired by set theory<fnref n="5" />:

$$< \mathbf{T}, \mathbf{U} >^* := (\mathbf{T} \mathcal{N} \mathbf{U}) \otimes (\mathbf{T} \mathcal{N} \mathbf{T} \mathcal{N} \mathbf{U}).$$

§84.6 **Encoding of variables.** As for variables they should be handled with explicit substitutions [Gir18b, Section 5.2]. A variable $\alpha$ is treated with a ray $\alpha(X)$ (the $X$ which is variable of stellar resolution should not be mistaken for a variable of predicate calculus). Variables occur either positively or negatively. Typically, when a variable $\alpha$ appears in the premise of an implication $A \to B$, then since $A \to B$ is implicitly $A \perp \mathcal{N} B$ hence $A$ and the variable $\alpha$ appearing inside are negated (recall that terms are interpreted by formulas). We hence have addresses $\alpha(t)$ and $\alpha^{\perp}(t)$ for a variable $\alpha$ and its linear negation $\alpha^{\perp}$. In order to relate variables with a formula, Girard design addresses so that $\alpha$ and $\alpha^{\perp}$ are sort of left and right branches of a formula $\forall \alpha.A$ in which they appear. We then have three sort of addresses:

* $\alpha(x) := (\forall \alpha.A)(1 \cdot X)$ referring to positive occurrences of $\alpha$ in $\forall \alpha.A$;

* $\alpha^{\perp}(x) := (\forall \alpha.A)(\mathbf{r} \cdot X)$ referring to negative occurrences of $\alpha$ in $\forall \alpha.A$;

* $(\forall \alpha.A)(\mathbf{c} \cdot X)$ referring to the formula $\forall \alpha.A$ itself (as for the interpretation of MLL atoms).

These definitions are also extended to existential quantification. For instance, in the formula $\forall \alpha.P(\alpha) \to P(c)$, we expect that both $P(\alpha)$ and $P(c)$ are multiplicative formulas with their own sub-addresses. We will have axioms with rays $(\forall \alpha.P(\alpha) \to P(c))(t)$ where $t$ an address referring to either an atom (as usual) or a variable of a term. In order to represent an explicit substitution $[\alpha := \sigma]$ where $\sigma$ is a term, it is possible to design a star which can interact with the rays encoding a variable and replace them by rays encoding $\sigma$ (such explicit substitutions can then be seen as constellations of adapters).

§84.7 **Equality.** An important predicate of predicate calculus is *equality* identifying individuals. Since everything boils down to formulas (there are no individuals), then equality between individuals (which are represented by multiplicative propositions) naturally becomes the linear equivalence $\equiv$. A famous criticism of Girard [Gir18b, Section 2] about the equality of predicate calculus, in its second-order form (cf. Paragraph 8.7), presupposes a specific space of properties, i.e. an implicit epidictic architecture. Indeed, when we say that $x = x$ when the two occurrences of $x$ have the same properties, that is

<footnote n="5">⁵In set theory, the pair $(x, y)$ can be represented by $\{\{x\}, \{x, y\}\}$.</footnote>
<figure><img src="image_136.png" /><figcaption>Figure 84.2: Vehicle and mould tested against a test for an existential formula. The conclusions of the test are 1, ..., n. Variables $Y_i$ can be either positive (a variable $Z_i$) or negative (a variable $Z_i^\perp$) and variables $X_i, X_i^\perp$ are occurrences of $X$ and $X^\perp$.</figcaption></figure>

$P(x) \Rightarrow P(x)$ for any predicate $P$, this looks absolutely trivial. However, imagine that we are in a computer in which the two copies of $x$ used are located in two different places in the computer memory. It is common in programming to have variables at different addresses but with an equivalent content. A property of computers which would distinguish the two copies of $x$ is to say that $P$ is “being located at address $\alpha$”. This property is excluded because we consider that logic does not live in the computer world but in a logical world we made up. But it is actually reasonable to consider such properties as we always do in computer science. Hence, in the transcendental syntax, no epidictic architecture is assumed but if we need one (to consider the usual “logical properties”) then we must make it explicit.

§84.8 **The mould.** A mould is a constellation-test specifying existential witnesses. If we look at the existential rule $\exists$ in Figure 82.1, we see that the existential witness $\sigma$ is subject to a substitution $\{\alpha := \sigma\}$ replacing a variable $\alpha$. Because variables appear either positively or negatively, so does the mould. Several choices of mould are possible. If $B$ is the formula we associate with $\sigma$ then the mould consists of tests for $B$ and for $B^\perp$ that I call *Tests$(B)$ and *Tests$(B^\perp)$. Positive occurrences $\alpha$ will be linked to *Tests$(B)$ and negative occurrences $\alpha^\perp$ to *Tests$(B^\perp)$.

§84.9 As explained before, what is now tested against a specification/set of tests is not simply a vehicle (computational entity) but a mix of a vehicle together with a mould: the tested comes with its own certificate. We then need to check the vehicle and its mould passes the tests. It is like checking tickets for a concert; some tickets can be fake but still be considered valid. Given a mix of a vehicle with its mould, there is no guarantee that the two parts of the mould are negation of each other. We have two requirements:

1. the tested must present a clear separation between vehicle (fully objective) and mould (fully subjective), what Girard calls an *épure*;

2. two parts of the mould should be distinguished, each being the negation of the other.
A way to ensure that the two parts of the mould are negation of each other, a natural
solution is to try to connect them with cuts and show a cut-elimination theorem. Al-
though it should work in some cases with the right epidictic architecture, it is known
that it is unprovable in general. The whole conception of the mould in the existential
rule is illustrated in Figure 84.2.

**85 Discussion: the theory of epidictic architectures**

§85.1 In this chapter, I sketched how quantification could be developed in transcendental syntax in order to express second order logic and predicate calculus. However, we still have no true theory of epidictics. It is not even clear what such a theory should be. But it should at least provide a way to characterise what a generic proof-structure is. We are in a free space of construction where it is *possible* to build proof-structures what it can be useful to *limit* the space to those proof-structures so to make generic reasoning possible: since the world is limited, I can know what are the possible shape of the unknown.

§85.2 **A return to...the meta?**. If analytics and synthetics are respectively matter (where we construct programs) and meaning (where we construct formulas) then epidictics (formatting synthetics) should be the space we construct logical languages or logical systems. It is then a sort of *meta-language* except that unlike previous meta-languages for logic, its purpose is not to justify but to limit the potential for efficiency. Transcendental syntax works with only 3 layers (analytics, synthetics, epidictics) without the need for an infinite hierarchy of semantics. Apodictics is simply the absence of the third layer.

§85.3 In my opinion, a way to tackle this question is to ask ourselves how we would implement transcendental syntax on a computer. Imagine that we have a programming language in which we can define constellations. It is also possible to freely design and build tests in order to work with proof and type checking. It is possible to mix tests from different logics. However, we sometimes would like to work with a specific logic and enable generic reasoning but also in order to build tests automatically from a notion of formula, among other things. But we also would like to tell what is a proof-structure is, that a vehicle has to be made in a specific way: with binary stars of pairwise disjoint terms which are either polarised with + or unpolarised. We need a way to express such structural and interactional constraints over constellations in a convenient and generic way.

§85.4 **A theory of social control.** It can be even trickier if we add models of computation on the top. I believe that epidictics should be able to answer questions such as “what is an automata?” (interactionally and structurally speaking). Remark that structure is deeply related to interaction/computational behaviour. Interactions of an object are limited by its structure and structure puts control over interaction. For instance, we could put some structural layer over constellations so that execution of automata will necessarily start on initial states and do computation in the “right direction”. We could forbid some interactions to happen for instance in circuits so that we first compute all
inputs before computing the output of gates. Such characterisations are what allows for generic reasoning. Although epidictics may look like an axiomatic theory of constraints, it is not exactly the case. The behaviour we force over the objects are only the behaviour we wish for because of some purpose in some system. It is a sort of *ethics*. We *want* our objects to behave in a specific way but they are free to interact in other ways when put against constellations outside of the system. Epidictics is a “guide” for computationals objects and not a system of constraints. Moreover, we can also change epidictics (or even remove it) without changing objects like how we can change a political regime.

**§85.5 Design plans.** Something I have in mind is that a potential epidictic language should probably be able to design “representative objects” from which constellations of a system are instantiated (it can be done with an homomorphism like how we extract diagrams from a dependency graph, in this case we would extract dependency graphs from an epidictic representative). Since only some specific constellations can be created, it induces a limitation of synthetics: only some behaviours can be considered, thus forming a logic. For instance, an epidictics which only allows typed polymorphic λ-terms to be created could be able to express natural deduction. It is like those design plans used to construct some objects or buildings. We need *concepts* and ways to produce those concepts. For instance, in the case of MLL proof-structures, the primitive concepts are axioms and formulas.

**§85.6 About type judgements.** As mentioned in the last part of the third article of transcendental syntax [Gir18b, Section 6.2], epidictics implicitly appears in Martin-Löf type theory (MLTT). In type theory, we usually have statements about types themselves. We have rules saying that $0: N$ (the term 0 is of type $N$, the type of natural numbers) and if $n: N$ then $s(n): N$. Now, we also have a rule concluding with $N: Type$, i.e. that $N$ is a valid type. For conjunction, we say that if $A: Type$ and $B: Type$ then $A \wedge B: Type$. This looks like a structuration of epidictics. One possible task for transcendental syntax is to give a clearer status for those type assertions in the light of the Usine/Usage interpretation and the computational justification of logical rules.

**§85.7** Girard finally concludes with the following sentence describing the current status of epidictics: "*At the present moment, epidictics is but a name on a blank area of the logical charts; hence a sort of new frontier for logic.*" [Gir18b, Section 6.2].
# Conclusion

## 86 Summary and contributions

§86.1 I would say that the main purpose of this thesis was to fill the gap between logic as it is today and the latest developments in linear logic. The gap was big. The Curry-Howard correspondence established a formal correspondence between logic and computation. However, the developments of computer science, although recent, went very fast. Maybe even too fast for logic. Logic has a lot of catch up and transcendental syntax is one of the first bricks for something bigger.

§86.2 **Contextualisation.** The first notable thing this thesis provides is contextualisation. Transcendental syntax does not come out of nowhere. It is part of a long story of people and ideas. In this thesis, it has been put in context and is seen as the natural successor of Girard's geometry of interaction (itself being a successor of the theory of proof-nets). It is also connected to known fields such as (classical) realisability (with ideas already explored by Colin Riba and Emmanuel Beffara) or the broad field of program testing. I had to reconstruct the story behind transcendental syntax so that it becomes more natural and accessible. As for the philosophical side, transcendental syntax can be seen as an answer to old questions regarding the justification of logical rules (something already mentioned by Paolo Pistone) that I explained in Paragraph 12.4. Actually, the geometry of interaction alone could serve as a satisfying answer but the transcendental syntax goes further by introducing finiteness of the conditions of possibility of reasoning but also a focus on the primitive shape of objects (which extends the Church-style typing of λ-calculus).

§86.3 **Illustration.** There is a big chapter (cf. Chapter 8) dedicated to the illustration of stellar resolution, the model of computation behind transcendental syntax. Automata, logic programs, tile systems and models of circuits are illustrated with simulation proofs and examples. I believe these illustrations to be more than mere encodings since they are very faithful to the original computational mechanisms of these models. Stellar resolution computes by resolving structured relations of constraints creating a sort of flow of information. This can be seen as a very elementary and primitive mechanism which underlies most (if not all) models of classical computation (cf. end of Chapter 8).

§86.4 **Formalisation.** The main contribution of this thesis is that it is the first formalisation of transcendental syntax:
* stellar resolution is formalised (cf. Chapter 7) and properties (cf. Chapter 9) about it are proven (in particular properties of confluence which are essential);

* several ways to execute constellations are defined (cf. Section 49, Section 50 and Section 51) and in particular, interactive execution can lead to natural implementations of stellar resolution;

* a model of MLL is given in Chapter 10, inspired by the treatment of multiplicatives in the geometry of interaction (cf. Chapter 5);

* simulation of cut-elimination and of the Danos-Regnier correctness criterion are proven (cf. Section 68);

* classical results such as completeness and soundness of several models of MLL are stated (cf. Section 70).

**§86.5 Extensions.** Few ideas of transcendental syntax which have been sketched by Girard are interpreted and extended. Although it is still informal, it is meant to be a possible inspiration for future works extending the initial formalisation of transcendental syntax given in this thesis. In particular, I give my own interpretation of Girard's apodictic (cf. Chapter 12) and epidictic (cf. Chapter 13) which are very vague notions. On a more technical side, I give a basis for a formal definition of exponentials (cf. Chapter 11) in transcendental syntax, which allows the possibility of defining "alternative exponentials" such as Girard's expansionals (cf. Section 78).

## 87 Horizons

**§87.1** When reading Girard's original articles on transcendental syntax, it may be difficult to understand what can be created out of it. The project may look rather shallow for some people. In this section, I expose several ideas of possible future works that I imagined without having the opportunity to develop them.

**§87.2 Remaining unsolved technical problems.** There are few completely technical problems left in this thesis, which could be solved but were not because of a lack of time or the presence of other priorities:

* there is no proper treatment of subjective rays. As shown in this thesis, internal polarities add a complex behaviour to constellations. In particular, some unpolarisised ray can become polarised. A proper treatment should include use cases for subjective rays together with an extended formal definition of execution and examples;

* as stated in Section 51, interactive execution with an interactive configuration $\Phi \vdash \Phi$ of reference constellation equal to its initial interaction space produce duplicates but the exact number of duplicates has not been characterised. The answer to this question (which is apparently a non-trivial problem on graphs) may allow us