• By equational reasoning with the previous propositions;

$$
\begin{align*}
\bigcap_{i \in I} \mathbf{A}_i &= \left( \bigcap_{i \in I} \mathbf{A}_i \right)^{\perp\perp} \\
&= \left( \bigcup_{i \in I} \mathbf{A}_i^{\perp} \right)^{\perp\perp} \\
&= \left( \bigcup_{i \in I} \mathbf{A}_i^{\perp} \right)^{\perp} \\
&= \left( \bigcup_{i \in I} t_i^{\perp\perp} \right)^{\perp} \\
&= \left( \bigcup_{i \in I} t_i \right)^{\perp}.
\end{align*}
$$

The cardinal of the union $\bigcup_{i \in I} t_i$ is bounded by $\sum_{i \in I} \mathrm{card}(t_i)$, hence since each $t_i$ is finite and since the set of indexes $I$ is finite that sum is finite and thus the cardinal of $\bigcup_{i \in I} t_i$ is also finite. The intersection $\bigcap_{i \in I} \mathbf{A}_i$ is the orthogonal of a finite set thus it is a computable type.

• Using the previous proposition we can obtain the following series of equalities;

$$
\begin{align*}
\left( \bigcup_{i \in I} \mathbf{A}_i \right)^{\perp\perp} &= \left( \bigcap_{i \in I} \mathbf{A}_i^{\perp} \right)^{\perp} \\
&= \left( \bigcap_{i \in I} t_i^{\perp\perp} \right)^{\perp} \\
&= \left( \bigcap_{i \in I} t_i \right)^{\perp}.
\end{align*}
$$

The cardinal of the intersection $\bigcap_{i \in I} t_i$ is bounded by $\min_{i \in I}$ since for any $i$ the cardinal of $t_i$ is finite then the minimum of the cardinals must also be finite. As a consequence $\bigcap_{i \in I} t_i$ has a finite cardinality. The union $(\bigcup_{i \in I} \mathbf{A}_i)^{\perp\perp}$ is the orthogonal of a finite set, hence it is a computable type.

Notation 24. Let A be a type we denote cf(A) the set of cut free nets in A.

Definition G.15. A type A is effective whenever $A^{\perp}$ is equal to $cf(A)^{\perp}$.

An interpretation basis is effective whenever it maps atomic formulas to effective types.

Remark 58. Equivalently a type A is effective whenever $A^{\perp\perp} = cf(A)^{\perp\perp}$.

PROPOSITION G.16. For any two effective types A and B the types A ⊗ B, A ⊗ B, A ⊗ B and A ⊗ B are still effective.

PROOF. This is a direct consequence from proposition E.23, not-
ing that an effective type A satisfies A = cf(A)⊥⊥.

PROPOSITION G.17. Given an effective interpretation basis $\mathcal{B}$ and $\Gamma$ some sequent the interpretation $[[\Gamma]]_{\mathcal{B}}$ is effective.

PROOF. This is easily obtained by induction on the size of the
sequent, using the proposition G.16.
□

*Remark 59.* A consequence of the previous theorem is that if a the set of cut free nets of two types $[[\Gamma]]_B$ and $[[\Gamma]]_B$ are equal then these types are equal.

PROPOSITION G.18. Given $(A_i)_{i \in I}$ a family of effective types, then $\bigcup_{i \in I} A_i$ and $\bigcap_{i \in I} A_i$ are effective types.

PROOF. This is a direct consequence of remark 58 and proposition G.14.
□

Notation 25. Given a formula A we define by induction the notation $A^n$ whenever $n$ is an integer;

• $A^0$ denotes the empty sequent.

• $A^{n+1}$ denotes $A^n$, $A$.

Notation 26. Let X be a propositional variable, we denote by C<sub>X</sub> the set of sequents of MLL of the form Γ, X<sup>n</sup>, X<sup>⊥</sup><sup>n</sup> for some integer n and such that Γ does not contain an occurence of X.

PROPOSITION G.19. For any propositional variable X any approximable basis B, and any net S

$$
S \vdash_{C_X} \Gamma \Rightarrow S \in [[\Gamma]]_B.
$$

PROOF. As for soundness in the case of MLL and MLL<sup>Σ</sup> we only need to prove the base case. Thus we need to prove that for any sequent Γ, X<sup>n</sup>, X<sup>⊥</sup><sup>n</sup> a daimon link Σ<sub>k+2n</sub> belongs to [[Γ, X<sup>n</sup>, X<sup>⊥</sup><sup>n</sup>]]<sub>B</sub> □

Remark 60. In particular this ensure that any net representing a proof of MLL<sup>Σ</sup> that introduce only sequents of C<sub>X</sub> belongs to [[∩<sub>X∈Ω</sub> Γ]]<sub>B</sub>, whenever <i>B</i> is an approximable basis.

Notation 27. Recall that a multiplicative net S is an ordered hyper-
graphs hence it is equipped with an order on its conclusion. When-
ever the conclusions of S are {p<sub>1</sub>, ..., p<sub>n</sub>} and (p<sub>σ(n)</sub>, ..., p<sub>σ(n)</sub>) is
an ordering of that set we denote S[(p<sub>σ(n)</sub>, ..., p<sub>σ(n)</sub>)] to explicitly
refer to the order of the conclusion of S as (p<sub>σ(n)</sub>, ..., p<sub>σ(n)</sub>).

Remark 61. Given an hypersequent *H* the size of the hypersequent *H* is equal to the number of conclusions the net in [[*H*]]<sub>*B*</sub> contains – this can be showed by a simple inclusion on *H*.

PROPOSITION G.20. Given S[p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub>] a net made of daimon links only. H<sub>1</sub>, H<sub>2</sub> and H<sub>3</sub> three hypersequents such that for each index 1 ≤ i ≤ n the size of H<sub>i</sub> is the size of the sequence p<sub>i</sub>.

If S[p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub>] belongs to [[H<sub>1</sub>, (H<sub>2</sub> || H<sub>3</sub>)]<sub>B</sub>] then S[p<sub>1</sub>, p<sub>2</sub>, p<sub>3</sub>] belongs to [[(H<sub>1</sub>, H<sub>2</sub>) || H<sub>3</sub>]]<sub>B</sub> or S[p<sub>1</sub>, p<sub>3</sub>, p<sub>2</sub>] ∈ [[(H<sub>1</sub>, H<sub>3</sub>) || H<sub>2</sub>]]<sub>B</sub>.

Remark 62. The previous proposition ensure that a net made of daimon links only belongs to some hypersequent *H* only if it belongs to an hypersequent of the form Γ<sub>1</sub> || ... || Γ<sub>n</sub> where each Γ<sub>i</sub> are sequents. This can be obtained by performing an induction on the number of non external parallel links in *H*. This together with the remark 54 provides a proof of the following proposition.

PROPOSITION G.21. Let $\omega$ be a separator (see appendix G.1). Given $\Gamma$ some sequent and $\mathcal{B}$ an approximable, self dual, and effective basis, denote $\mathcal{B}_X = \{[[X]]_\mathcal{B}, [[X^\perp]]_\mathcal{B}\}$.
For any cut free net S;

$$S \in \llbracket \bigcap_{X \in \omega \cup \mathcal{B}_X} \Gamma \rrbracket_B \Rightarrow S \vdash_{C_X} \Gamma.$$

PROOF. The net S belongs to $\llbracket \cap_{X \in \omega \cup \mathcal{B}_X} \Gamma \rrbracket_B$ thus in particular $S \in \llbracket \Gamma \rrbracket_B$. $\mathcal{B}$ is an approximable and self dual basis therefore by theorem 5.10, S represents a proof of $\Gamma$ in MLL$^{\star}$.

To conclude we must ensure the daimons of S only introduces sequents $\Delta$ which belongs to $C_X$. Any of the daimons of S must belong to a type $\llbracket \cap_{X \in \omega \cup \mathcal{B}_X} \Delta \rrbracket_B$ and so in particular $\llbracket \cap_{X \in \omega} \Delta \rrbracket_B$ where $\Delta$ is a sequent. We can apply therefore proposition G.8. $\square$

Remark 63. Proposition G.19 ensure that any cut-free proof in MLL$^{\star}$ introducing only sequents following the constraint $C_X$ is included in $\llbracket \cap_{X \in \Omega} \Gamma \rrbracket_B$, when $\Omega$ denote the set of all types.

Furthermore $\llbracket \cap_{X \in \Omega} \Gamma \rrbracket_B$ is necessarily included in $\llbracket \cap_{X \in \omega} \Gamma \rrbracket_B$ since $\omega \subset \Omega$. On the other hand the completeness result show that any cut free net in $\llbracket \cap_{X \in \omega} \Gamma \rrbracket_B$ is in fact a proof in MLL$^{\star}$ introducing only sequents following the constraint $C_X$.

This shows that the intersections $\llbracket \cap_{X \in \Omega} \Gamma \rrbracket_B$ and $\llbracket \cap_{X \in \omega} \Gamma \rrbracket_B$ contain the same cut free nets. As a consequence since these types are effective, they are equal.

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

$$\llbracket \cap_{X \in \omega} \mathcal{H} \rrbracket_B = \llbracket \cap_{X \in \Omega} \mathcal{H} \rrbracket_B.$$

PROOF. Using the previous remark. $\square$