*InCFL*<sub>ew</sub>' admits the cut rule, there exists a deduction with same premisses and conclusion in *InCFL*<sub>ew</sub>', which gives, according to **Lemma 6.2.1**, a deduction in *InCFL*<sub>ew</sub> with same premisses and conclusion as *D*.

## 7. BOOLEAN CASE

Here, we deal with the case which cumulates the properties of the intuitionistic and involutive cases. It is the analogue of the study of Boolean logic in the continuous setting. We first prove that the ordered topological space associated to any IC-algebra (**Theorem 5.3.4**) is actually just a topological space. Second, we show that the theory obtained to describe this Boolean Continuous Logic is equivalent to the theory of classical continuous logic (**Theorem 7.1.10**). Finally, we exhibit a sequent-style deductive system admitting the cut rule that describes this logic.

### 7.1. Boolean Continuous Algebras.

**Definition 7.1.1** ([21, p. 22]). A Boolean algebra is a Heyting algebra $\mathcal{B}$ such that, for all $x \in \mathcal{B}$, $\neg\neg x = x$.

**Theorem 7.1.2.** Let $\mathcal{L}$ be a commutative residuated complete lattice.

$\mathcal{L}$ is a Boolean algebra if and only if the negation on $USC(\mathcal{L})$ is involutive and $USC(\mathcal{L}) \models 2v \geq v \lor v$.

*Proof.* The claim is a consequence of the following one : $\mathcal{L}$ is a Boolean algebra if and only if the negation on $\mathcal{L}$ is involutive and $\otimes = \wedge$. The claim is true since, for all commutative residuated lattice $\mathcal{L}$, $\mathcal{L}$ is a Heyting algebra if and only if $\otimes = \wedge$ and for every Heyting algebra $\mathcal{L}$, $\mathcal{L}$ is a Boolean algebra if and only if its negation is involutive.

**Definition 7.1.3.** We denote by $T_{\text{class}}$ the theory $T_{\text{int}} \cup \{v \le (1 \div (1 \div v))\}$.

We denote by BC the class whose elements are the $USC(\mathcal{B})$ for $\mathcal{B}$ a complete Boolean algebra and call these algebras Boolean Continuous Algebras.

**Theorem 7.1.4.** For all model $A$ of $T_{\text{class}}$, there exists a complete Boolean algebra $\mathcal{B}$ such that the quotient of the Macneille completion of $A$ by $\simeq$ is isomorphic to $USC(\mathcal{B})$.

For all model $A$ of $T_{\text{class}}$, there exists a complete Boolean algebra $\mathcal{B}$ such that the quotient of $A$ by $\simeq$ embeds into $USC(\mathcal{B})$.

*Proof.* Let $A$ be a model of $T_{\text{class}}$. $A$ is a model of $T_{\text{int}}$, so, according to **Corollary 5.2.6**, there exists a locale $\mathcal{B}$ such that the quotient of the Macneille completion of $A$ by $\simeq$ is isomorphic to $USC(\mathcal{B})$. According to this same theorem, the quotient of $A$ by $\simeq$ also embeds into $USC(\mathcal{B})$. Finally, according to **Theorem 6.1.3**, this same locale is involutive, so $\mathcal{B}$ is a complete Boolean algebra.

**Corollary 7.1.5.** For all $\mathcal{L}$-terms $\varphi$ and $\psi$, the following assertions are equivalent:

(1) For all complete Boolean algebra $\mathcal{B}$, $USC(\mathcal{B}) \models \varphi \le \psi$.

(2) For all $n \in \mathbb{N}$, $\varphi \le \psi + \frac{1}{2^n}$ is consequence of $T_{\text{class}}$.

*Proof.* For all complete Boolean algebra $\mathcal{B}$, $USC(\mathcal{B})$ is a model of $T_{\text{int}}$ and satisfies $v \le 1 \div (1 \div v)$, so $USC(\mathcal{B})$ is a model of $T_{\text{class}}$. By Archimedeanity of every BC-algebra, we have that 2 implies 1.

Let $\varphi$ and $\psi$ be $\mathcal{L}$-terms both having $k$ free variables such that, for all complete Boolean algebra $\mathcal{B}$, $USC(\mathcal{B}) \models \varphi \le \psi$. Let $A$ be a model of $T_{\text{class}}$. According to **Theorem 7.1.4**, there exists a complete Boolean algebra $\mathcal{B}$ and a morphism $i: A \to USC(\mathcal{B})$ such that, for all $a$ and $b \in A$, $i(a) \le i(b) \Leftrightarrow \forall n \in \mathbb{N} a \le b + \frac{1}{2^n}$. For all $a \in A^k$ and $n \in \mathbb{N}$, since $i(\varphi(a)) \le i(\psi(a))$, $\varphi(a) \le$
$\psi(a) + \frac{1}{2^n}$. The class of all models of $T_{\text{class}}$ being complete for $T_{\text{class}}$, $\varphi \le \psi + \frac{1}{2^n}$ is consequence of $T$. $\square$

**Lemma 7.1.6.** Let $(X, \leq)$ be an intuitionistic Hausdorff ordered space. The set $Y$ of minimal elements of $X$ is closed.

*Proof.* Let $y \in \bar{Y}$.

Since $X$ is Hausdorff, $\{y\} = \bigcap_{U \text{ open, s.t. } y \in U} U$. Moreover, for all open $U$ such that $y \in U$, $y \in \overline{U \cap Y}$, so

$\{y\} = \bigcap_{U \text{ open, s.t. } y \in U} U \cap Y$. However, for all open $U$ such that $y \in U$, $U \cap Y \subset Y$, so $U \cap Y$ is

downward closed. Hence $\{y\}$ is downward closed, which proves that $y \in Y$. $\square$

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

**Lemma 7.1.7.** Let $(X, \leq)$ be a non-empty compact ordered space. The set $Y$ of minimal elements of $X$ is not empty.

*Proof.* Let $(X, \leq)$ be a non-empty compact ordered space. Let $E$ be the set of non empty chains on $X$.

$E$ is not empty because $X$ is not empty.

Let $\mathscr{C} \subset E$ be totally ordered by inclusion and assume $\mathscr{C}$ is not empty. Let $A = \bigcup_{C \in \mathscr{C}} C$. For all $C \in \mathscr{C}$, $C \subset A$. For all $x$ and $y \in A$, there exists $C \in \mathscr{C}$ such that $x$ and $y \in C$, so either $x \leq y$ or $y \leq X$. Thus, $A \in E$.

According to Zorn's lemma, $E$ admits a maximal element $C$.

Let $\mathscr{F} = \{A \subset X | A \cap C \neq \emptyset \text{ and } \forall x < y \in C (y \in A \Rightarrow x \in A)\}$. For all $A$ and $B \in \mathscr{F}$, there exists $x_1 \in A \cap C$ and $x_2 \in B \cap C$, so, since $C$ is a chain, $x_1 \in (A \cap B) \cap C$ or $x_2 \in A \cap B$ and thus $A \cap B \in \mathscr{F}$. Hence $\mathscr{F}$ is a prefilter, so, since $X$ is compact, the exists $x_0 \in \bigcap_{A \in \mathscr{F}} \bar{A}$. For all $x \in X$, if $x \leq x_0$, by maximality of $C$, $x \in C$, so $\downarrow \{x\} \in \mathscr{F}$ and thus $x_0 \leq x$.

$x$ is thus a minimal element of $X$.

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

**Theorem 7.1.8.** For all intuitionistic compact Hausdorff ordered topological space $X$, $C_{\searrow}^0(X) \models v \leq 1 \div (1 \div v)$ if and only if the order is the equality on $X$.

*Proof.* Let $(X, \leq)$ be an intuitionistic compact Hausdorff ordered topological space.

If the order is equality on $X$, then $C_{\searrow}^0(X) = C^0(X)$ and thus $C_{\searrow}^0(X) \models v \leq 1 \div (1 \div v)$.

Assume now that $C_{\searrow}^0(X) \models v \leq 1 \div (1 \div v)$. Let $Y$ be the set of minimal elements of $X$ and $x \in X$. Let us prove that $x \in Y$, and thus that every element of $X$ is minimal.

For all $f \in C_{\searrow}^0(X)$ and all $z \leq x$, since $\downarrow \{z\}$ admits minimal elements (Lemma 7.1.7),

$$ (1 \div f)(z) = \bigvee_{y \leq z} 1 \div f(y) \geq \bigvee_{\substack{y \in Y \\ y \leq z}} 1 \div f(y) = 1, $$

so $f(x) = (1 \div (1 \div f))(x) = \bigvee_{z \leq x} 1 \div (1 \div f)(z) = 0$. By Lemma 7.1.6, $Y$ is closed. Thus $Y$

is a downward closed subset and $\uparrow \{x\}$ is an upward closed subset, so, according to Lemma 2.3.18, $Y \cap \uparrow \{x\} \neq \emptyset$. Hence $x \in Y$. $\square$

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

**Corollary 7.1.9.** For all BC-algebra $A$, the order on $Sp(A)$ is the equality.
**Proof.** For all BC-algebra $A$, since $A$ is a Cauchy-complete Archimedean MC-algebra, according to **Theorem 5.3.4**, $A \simeq C_{\downarrow}^0(\mathrm{Sp}(A))$ and $\mathrm{Sp}(A)$ is compact and Hausdorff, so, according to **Theorem 7.1.8**, since $A \models v \le 1 \div (1 \div v)$, the order on $\mathrm{Sp}(A)$ is the equality. $\square$

We now recall the theory $T_c$ of classical logic, given in [6, p. 5]:

(A1) $a \div b \le a$

(A2) $(c \div a) \div (c \div b) \le b \div a$

(A3) $a \div (a \div b) \le b \div (b \div a)$

(A4) $a \div b \le \neg b \div \neg a$

(A5) $\frac{a}{2} \le a \div \frac{a}{2}$

(A6) $a \div \frac{a}{2} \le \frac{a}{2}$

**Theorem 7.1.10.** The Archimedean models of $T_c$ are exactly the Archimedean models of $T_{\mathrm{class}}$.

*Proof.* Since $T_{\mathrm{class}}$ axiomatizes $[0,1] = \mathrm{USC}(\{\emptyset\})$, and, according to [6, Fact 4.4], $\{[0,1]\}$ is complete for $T_c$, $T_c$ is a consequence of $T_{\mathrm{class}}$ with Archimedeanity.

Conversely, let $A$ be an Archimedean model of $T_{\mathrm{class}}$. According to **Corollary 7.1.9**, there exists an embedding $i: A \to C_{\downarrow}^0(\mathrm{Sp}(A))$. We will prove that subtraction is calculated pointwise in $C_{\downarrow}^0(\mathrm{Sp}(A))$. From this, we can easily deduce that (A1), (A2), (A3), (A4), (A5) et (A6) are satisfied by $C_{\downarrow}^0(\mathrm{Sp}(A))$, from which we can conclude that they are also satisfied by $A$.

Let us now prove that subtraction is calculated pointwise in $C_{\downarrow}^0(\mathrm{Sp}(A))$. For all $f$ and $g \in C_{\downarrow}^0(\mathrm{Sp}(A))$, $f \div g$ is the smallest non decreasing function above $x \mapsto f(x) \div g(x)$, which is non decreasing since the order on $\mathrm{Sp}(A)$ is the equality, so $f \div g: x \mapsto f(x) \div g(x)$. $\square$

**Corollary 7.1.11.** For all $n \in \mathbb{N}$, for all terms $\varphi$ and $\psi$ in the language $\mathcal{L}$, $[0,1] \models \varphi \le \psi$ if and only if for all complete Boolean algebra $\mathcal{B} \mathrm{USC}(\mathcal{B}) \models \varphi \le \psi$.

*Proof.* Indeed, the class $\{[0,1]\}$ is complete for $T_c$ with Archimedeanity, so is complete for $T_{\mathrm{class}}$ with Archimedeanity too, and thus, for all complete Boolean algebra $\mathcal{B} \mathrm{USC}(\mathcal{B}) \models \varphi \le \psi$. Reciprocally, $[0,1]$ is itself a BC-algebra. $\square$

**Corollary 7.1.12.** The definition of $\odot$ given in **Definition 5.3.7** coincide with the naive one, i.e., for all complete Boolean algebra $\mathcal{B}$ and all $f$ and $g \in \mathrm{USC}(\mathcal{B})$, $j(\frac{f}{2} + \frac{g}{2}) = 1 \div ((1 \div f) \div (1 \div g))$.

## 7.2. Cut Admissibility.
The language for sequent calculus in the intuitionistic case is the same as the one for *InCFL*<sub>ew</sub>, recalled in Figure 13. The language for the structures and formulas of sequent calculus in the involutive case, and its correspondence with the language $\mathcal{L}$ are given in Figure 11. As for the involutive case, we also consider the language $\mathcal{L}'_{\mathrm{inv}}$ which is $\mathcal{L}_{\mathrm{inv}}$ with the symbols of the Figure 12. We keep Notation 4.1.1.

Here again, we use a system similar to *InMGL* with several modalities but only one negation. We still work with the system *InMGL* ($\circ_2, \bullet_2, \circ_\alpha$) (Figure 8). In addition to the rules of *InMGL*($\circ_2, \bullet_2, \circ_\alpha$) (Figure 8), we add the structural rules given in Figure 13 and call the total system *InLJK*.

By following the same steps as in subsection 6.2, since all the rules added to obtain *InLJK* are analytic (cf. **Definition 8.1.2**), according to **Theorems 8.1.12 and 8.1.13**, the following two theorems are true.
<table><caption>FIGURE 11. Correspondence between structure symbols and $\mathcal{L}$</caption><thead><tr><th colspan="3">Left interpretation</th><th colspan="2">Right interpretation</th></tr><tr><th>structures</th><th>formulas</th><th>algebraic correspondent</th><th>formulas</th><th>algebraic correspondent</th></tr></thead><tbody><tr><td>,</td><td>+</td><td>+</td><td>⊗</td><td>1 - ((1 - __)+(1 - __))</td></tr><tr><td>ε</td><td>0</td><td>0</td><td>1</td><td>1</td></tr><tr><td>○<sub>2</sub></td><td>2</td><td>2</td><td>2</td><td>2</td></tr><tr><td>●<sub>2</sub></td><td>j<sub>*</sub></td><td>j<sub>*</sub></td><td>j</td><td>j</td></tr><tr><td>○<sub>α</sub></td><td>α</td><td>α</td><td>■<sub>α</sub></td><td>2v ∧ j<sub>*</sub>(v)</td></tr><tr><td>¬</td><td>¬</td><td>¬</td><td>¬</td><td>¬</td></tr></tbody></table>

<table><caption>FIGURE 12. Correspondence between the new structure symbols and $\mathcal{L}$</caption><thead><tr><th colspan="3">Left interpretation</th><th colspan="2">Right interpretation</th></tr><tr><th>structures</th><th>formulas</th><th>algebraic correspondent</th><th>formulas</th><th>algebraic correspondent</th></tr></thead><tbody><tr><td>●<sub>α</sub></td><td>α</td><td>α</td><td>■<sub>α</sub></td><td>2v ∧ j<sub>*</sub>(v)</td></tr><tr><td>~</td><td>~</td><td>~</td><td>~</td><td>~</td></tr></tbody></table>

<figure><img src="image_19.png" /><figcaption>FIGURE 13. InLJK</figcaption></figure>

**Theorem 7.2.1 (Completeness theorem).** The class BC is sound and complete for InLJK.

**Theorem 7.2.2 (Cut Admissibility theorem).** In the system InLJK, for all formulas $a_1, \dots, a_n$ and $b$ and $\{, \circ_2, \bullet_2, \circ_\alpha, \varepsilon\}$-term $G$ such that there exists a deduction of $G(a_1, \dots, a_n) \vdash b$ using the cut rule, there exists a deduction of $G(a_1, \dots, a_n) \vdash b$ not using the cut rule.

## 8. ANNEXES

The aim of the **Annexes** is to prove the cut-admissibility theorem 8.1.13 for it is useful to prove all other cut-admissibility theorems of this paper.

Let $F_m$ (resp. $InF_m$) be the set of formulas of the language $L = \{\underline{1}, \cdot, / , \setminus, \vee, \wedge, \diamond, \blacksquare\}$ (resp. $InL = \{\cdot, \vee, \wedge, \underline{1}, \diamond, \blacksquare, \sim, \neg\}$), where $\cdot, \vee, \wedge, \underline{1}$ and $/ $ are binary function symbols, $\diamond$ and $\blacksquare$ are unary
function symbols, $\mathbf{1}$ is a constant symbol and $\sim$ and $\neg$ are unary function symbols. We call variables in formulas *propositional* variables.

**Notation 8.1.1.** We recall that the *sequent space* $\mathcal{Sqt}$ is the algebra of $\{, \circ\}$-terms over $\mathbf{F}_m$. We now see $\mathbf{F}_m$ as embedded in $\mathcal{Sqt}$. We denote by small greek letters the elements of $\mathcal{Sqt}$ and call them *structures* and by latin letters the ones of $\mathbf{F}_m$. By capital greek letters, we mean a context. The *involutive sequent space* $\mathcal{InSqt}$ is the quotient of the algebra of $\{, \circ, \bullet, \sim, \neg, \varepsilon\}$-terms over $\mathbf{InF}_m$, where $\circ$ is a binary function symbol, $\bullet$, $\sim$, and $\neg$ are unary function symbols and $\varepsilon$ is a constant symbol by the following relations:

$$ (1) \quad \gamma \sim \neg = \gamma \neg \sim = \gamma $$

$$ (2) \quad (\odot \gamma) \sim = \odot (\gamma \sim) $$

$$ (3) \quad (\odot \gamma)^{\neg} = \odot (\gamma^{\neg}) $$

$$ (4) \quad (\gamma, \delta)^{\sim} = \delta^{\sim}, \gamma^{\sim} \text{ et } (\gamma, \delta)^{\neg} = \delta^{\neg}, \gamma^{\neg} $$

where $\odot$ denotes either $\circ$ or $\bullet$. We finally define $\square a = \sim \diamond \neg a$ and $\blacksquare = \sim \diamond \neg a$, for all $a \in \mathbf{InF}_m$ and the notations $\diamond$ either $\diamond$ or $\blacksquare$ and $\blacksquare$ denote $\blacksquare$ when $\odot$ denotes $\circ$ and $\square$ when $\odot$ denotes $\bullet$.

We give the rules of *MGL* and *InMGL*, following respectively [22] and [20]. They consist respectively of the rules of *GL* and *InGL*, which are recalled in *Figures* 14 and 16, to which are added the rules of *Figures* 15 and *Figures* 17.

<figure><img src="image_20.png" /><figcaption>FIGURE 14. *GL* rules</figcaption></figure>

<figure><img src="image_21.png" /><figcaption>FIGURE 15. *MGL* rules</figcaption></figure>

**Remark 8.1.1.** the following rules can easily be deduced from the ones of *InMGL*:

$$ \frac{\gamma \vdash \delta^{\neg}}{\delta \vdash \gamma^{\sim}} [\sim / \neg] \quad \frac{a \vdash \delta}{\square a \vdash \circ \gamma} \quad \frac{\gamma \vdash \circ a}{\gamma \vdash \square a} \quad \frac{a \vdash \delta}{\blacksquare a \vdash \bullet \gamma} \quad \frac{\gamma \vdash \bullet a}{\gamma \vdash \blacksquare a} $$

To these rules can be added the cut rules for *MGL* and *InMGL*:

$$ \frac{\gamma \vdash a}{\Gamma[\gamma] \vdash b} \quad \frac{\Gamma[a] \vdash b}{\gamma \vdash \delta} \quad \frac{\delta \vdash \beta}{\gamma \vdash \beta} \quad \text{(Cut)} $$

We now discuss in parallel the involutive and non involutive cases.
<figure><img src="image_22.png" /><figcaption>FIGURE 16. InGL rules</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>FIGURE 17. InMGL rules</figcaption></figure>

**Definition 8.1.2.** *Non involutive structural and analytic rules:*

We denote by $\Upsilon$ some terms on $\mathcal{S}qt$ for the language $\mathbf{L}$ and $A$ terms for $\mathbf{L}$ on $\mathbf{F}_m$.

A structural rule is a rule $r = \frac{\Gamma[\Upsilon_1] \vdash A_1 \quad \dots \quad \Gamma[\Upsilon_n] \vdash A_n}{\Gamma[\Upsilon_0] \vdash A_0}$ such that no symbol other than ",", $\circ$, or $\epsilon$ appears in any $\Upsilon_i$ nor $A_i$.

A rule be said analytic when it is a structural rule of the form $\frac{\Gamma[\Upsilon_1] \vdash A \quad \dots \quad \Gamma[\Upsilon_n] \vdash A}{\Gamma[\Upsilon_0] \vdash A}$ satisfying:

*Linearity :* $A$ is a formula variable and the variables of $\Upsilon_0$ are distinct.

*Separation :* A doesn't appear in $\Upsilon_0$.

*Inclusion :* The variables of the $\Upsilon_i$'s are among the ones of $\Upsilon_0$.

*Involutive structural and analytic rules:*

We now denote by $\Upsilon$ and $\Psi$ some terms on $\mathcal{I}n\mathcal{S}qt$ for the language $\mathbf{InL}$.

A structural rule is a rule $r = \frac{\Upsilon_1 \vdash \Psi_1 \quad \dots \quad \Upsilon_n \vdash \Psi_n}{\Upsilon_0 \vdash \Psi_0}$ such that no symbol other than ",", $\circ$, $\bullet$, $\epsilon$, $\sim$ and $\neg$ appears in any $\Upsilon_i$ nor $\Psi_i$.

A rule be said analytic when it is a structural rule of the form $\frac{\Upsilon_1 \vdash \Psi \quad \dots \quad \Upsilon_n \vdash \Psi}{\Upsilon_0 \vdash \Psi}$ satisfying:

*Linearity :* $\Psi$ is a structure variable and the variables of $\Upsilon_0$ are distinct.

*Separation :* $\Psi$ don't appear in $\Upsilon_0$.

*Inclusion :* The variables of the $\Upsilon_i$'s are among the ones of $\Upsilon_0$.

*Positivity :* No negation symbol appears in the rule.
**Remark 8.1.2.** Following [20], we could replace the positivity condition as follows: any $\Upsilon_i$ is $, , \circ, \bullet, \varepsilon$-terms on variables negated an even numbers of times. Since we won't need this extension, we leave the minor changes in the proofs to the reader.

Let $R$ be a set of analytic structural rules of **MGL** (*InMGL*).

**Definition 8.1.3.** From here on, we can endow $\mathcal{S}qt$ ($\mathcal{InS}qt$) with a binary relation $\vdash\subset \mathcal{S}qt \times \mathbf{F}_m$ ($\vdash\subset \mathcal{InS}qt \times \mathcal{InS}qt$) which is the smallest relation satisfying the rules of Figures 14 and 15 (Figures 16 and 17) and the rules of $R$ and call the resulting structure $\mathcal{S}qt_R$ ($\mathcal{InS}qt_R$). We denote by $\mathcal{S}qt_{cut,R}$ ($\mathcal{InS}qt_{cut,R}$) the sets $\mathcal{S}qt$ ($\mathcal{InS}qt$) endowed with the smallest relation $\vdash_{cut}$ satisfying the previous rules and (Cut).

**Definition 8.1.4.** We can define a preorder $\leq$ on $\mathcal{S}qt_R$ by $\gamma \leq \delta$ if and only if $\forall a \in \mathbf{F}_m \ \forall \Gamma \ \Gamma[\delta] \vdash a \Rightarrow \Gamma[\gamma] \vdash a$ and a preorder $\leq$ on $\mathcal{InS}qt_R$ by $\gamma \leq \delta$ if and only if $\forall \beta \in \mathcal{InS}qt \ \delta \vdash \beta \Rightarrow \gamma \vdash \beta$.

For all $X \subset \mathcal{S}qt$, let

$$j(X) = \{\gamma \in \mathcal{S}qt \mid \forall a \in \mathbf{F}_m \text{ and context } \Gamma, (\forall \delta \in X \ \Gamma[\delta] \vdash a) \Rightarrow \Gamma[\gamma] \vdash a\}.$$

For all $X \subset \mathcal{InS}qt$, let

$$j(X) = \{\gamma \in \mathcal{InS}qt \mid \forall \beta \in \mathcal{InS}qt, (\forall \delta \in X \ \delta \vdash \beta) \Rightarrow \gamma \vdash \beta\}.$$

**Lemma 8.1.5** ([11, p. 279], [20, p.1221]). $j$ is a closure operator on the set of subsets of $\mathcal{S}qt$ (*InSqt*).

**Lemma 8.1.6.** Every $j$-closed subset of $\mathcal{S}qt_R$ is downward closed.

We then define $\mathcal{S}qt_{R,+}$ (resp. $\mathcal{InS}qt_{R,+}$) as the set of $j$-closed subsets of $\mathcal{S}qt$ (resp. $\mathcal{InS}qt$)

and $g: \mathbf{F}_m \to \mathcal{S}qt_{R,+}$ (resp. $g: \mathbf{F}_m \to \mathcal{InS}qt_{R,+}$). We endow the set of $a \mapsto \{\gamma \in \mathcal{S}qt \mid \gamma \vdash a\}$ ($\delta \mapsto \{\gamma \in \mathcal{S}qt \mid \gamma \vdash \delta\}$).

subsets of $\mathcal{S}qt$ with the following structure:

(1) For all $X$ and $Y \subset \mathcal{S}qt$, $X, Y = \{\gamma, \delta \gamma \in X \text{ and } \delta \in Y\}$.

(2) For all $X \subset \mathcal{S}qt$, $\circ X = \{\circ \gamma, \gamma \in X\}$.

(3) $\varepsilon = \{\varepsilon\}$.

(4) For all $X$ and $Y \subset \mathcal{S}qt$, $X \wedge Y = X \cap Y$, $X \vee Y = j(X \cup Y)$.

(5) For all $X$ and $Y \subset \mathcal{S}qt$, $X \cdot Y = j(X, Y)$.

(6) For all $X \subset \mathcal{S}qt$, $\diamond X = j(\circ X)$.

(7) $\underline{1} = j(\varepsilon)$.

(8) For all $X$ and $Y \subset \mathcal{S}qt$, $X \setminus Y = \{\gamma \in \mathcal{S}qt \mid \forall \delta \in X \ \delta \cdot \gamma \in Y\}$, and $X/Y = \{\gamma \in \mathcal{S}qt \mid \forall \delta \in X \ \gamma \cdot \delta \in Y\}$

(9) For all $X \subset \mathcal{S}qt$, $\blacksquare X = \{\gamma \in \mathcal{S}qt \mid \circ \gamma \in X\}$.

This induces an $\mathbf{L}$-structure on $\mathcal{S}qt_{R,+}$.

**Lemma 8.1.7.** $j$ is a $\{, \circ, \varepsilon\}$-morphism from the subsets of $\mathcal{S}qt$ to $\mathcal{S}qt_{R,+}$.

*Proof.* Claim: $j$ is non-decreasing and, for all $X$ and $Y \subset \mathcal{S}qt$, $X \subset j(X)$, $j^2(X) = j(X)$, $\circ j(X) \subset j(\circ X)$ and $j(X), j(Y) \subset j(X, Y)$.

The facts that $j$ is non-decreasing and, for all $X \subset \mathcal{S}qt$, $X \subset j(X)$ are clear.
Let $X$ and $Y \subset \mathcal{S}qt$. Let $\gamma \in j^2(X)$. For all context $\Gamma$ and $a \in \mathbf{F}_m$ such that for all $\delta \in X$
$\Gamma[\delta] \vdash a$, and for all $\beta \in j(X)$, by definition of $j$, $\Gamma[\beta] \vdash a$, so, by definition of $j$ again, $\Gamma[\gamma] \vdash a$.
Thus $\gamma \in j(X)$.

Let $\gamma \in j(X)$. For all context $\Gamma$ and $a \in \mathbf{F}_m$ such that for all $\delta \in \circ X \Gamma[\delta] \vdash a$, and for all $\beta \in X, \Gamma[\circ\beta] \vdash a$, so, by definition of $j$, taking $\Gamma[\circ\_\_]$ as context, $\Gamma[\circ\gamma] \vdash a$. Thus $\circ\gamma \in j(\circ X)$.

Let $\gamma \in j(X)$ and $\delta \in j(Y)$. For all context $\Gamma$ and $a \in \mathbf{F}_m$ such that for all $\eta \in X, Y$
$\Gamma[\eta] \vdash a$, and for all $\alpha \in X$ and $\beta \in Y$, $\Gamma[\alpha, \beta] \vdash a$, so, by definition of $j$, taking $\Gamma[\_, \beta]$ as a
context $\Gamma[\gamma, \beta] \vdash a$ and then, taking $\Gamma[\gamma, \_\_]$ as a context, $\Gamma[\gamma, \delta] \vdash a$. Thus $\gamma, \delta \in j(X, Y)$, which
concludes the proof of the claim.

Thanks to the claim:

$j(X, Y) \subset j(j(X), j(Y)) = j(X) \cdot j(Y)$ and $j(X) \cdot j(Y) = j(j(X), j(Y)) \subset j^2(X, Y) = j(X, Y)$, so
$j(X, Y) = j(X) \cdot j(Y)$. $j(\circ X) \subset j(\circ j(X)) = \diamond j(X)$ and $\diamond j(X) = j(\circ j(X)) \subset j^2(\circ X) = j(\circ X)$, so
$j(\circ X) = \diamond j(X)$. Finally, $\underline{1} = j(\varepsilon)$. $\square$

We define the operators on $\mathcal{I}n\mathcal{S}qt_{R,+} \vee, \wedge, \underline{1}, \cdot$ and $\diamond$ and $\diamond$ in the same way. We
also define, for all $X \in \mathcal{I}n\mathcal{S}qt_{R,+}, \sim X = \{\gamma \in \mathcal{I}n\mathcal{S}qt \mid \forall \delta \in X \ \gamma \vdash \delta^{\sim}\}$ and
$\neg X = \{\gamma \in \mathcal{I}n\mathcal{S}qt \mid \forall \delta \in X \ \gamma \vdash \delta^{\neg}\}$.

**Lemma 8.1.8.** The set of $j$-closed subsets of $\mathcal{S}qt$ ($\mathcal{I}n\mathcal{S}qt$) is closed for these operations. Moreover,
**■** is right adjoint to $\diamond$ on $\mathcal{S}qt_{R,+}$, for all $X \in \mathcal{I}n\mathcal{S}qt_{R,+}, \sim \neg X = \neg \sim X = X$ and $\sim \diamond \neg$ is
right adjoint to $\diamond$ and $\sim \diamond \neg$ is right adjoint to $\diamond$.

*Proof.* According to [11, Lemma 5.4] and [20, Corollary 4.3], we only have to prove that:

(1) **$\blacksquare$ is well defined on $\mathcal{S}qt_{R,+}$ and right adjoint to $\diamond$ on it**

(2) $\sim \diamond \neg$ is right adjoint to $\diamond$ and $\sim \diamond \neg$ is right adjoint to $\diamond$.

(1) Let $X \subset \mathcal{S}qt$ be a $j$-closed set and let us show that $j(\blacksquare X) \subset \blacksquare X$. Let $\gamma \in j(\blacksquare X)$.

By definition of $j$, for all $a \in \mathbf{F}_m$ and context $\Delta$, if for all $\delta \in \mathcal{S}qt$ such that $\circ\delta \in X$
$\Delta[\delta] \vdash b$, then $\Delta[\gamma] \vdash a$. Thus, for all $a \in \mathbf{F}_m$ and context $\Gamma$, for all $\delta \in \mathcal{S}qt$ such
that $\circ\delta \in X$, since $\Gamma[\circ\delta] \vdash a$, taking $\Delta = \Gamma[\circ\_\_]$, $\Gamma[\circ\gamma] \vdash a$. Hence $\circ\gamma \in j(X) = X$, ie
$\gamma \in \blacksquare X$.

(2) Since, by [20, Lemma 4.2 (i)], for all $W$ and $Z \in \mathcal{S}qt_{R,+}$, $W \subset \sim Z \Leftrightarrow Z \subset \neg W$, for all $X$ and $Y \in \mathcal{I}n\mathcal{S}qt_{R,+}$,

$$
\begin{align*}
X \subset \sim \diamond \neg Y &\Leftrightarrow \diamond \neg Y \subset \neg X \\
&\Leftrightarrow \{\circ\gamma, \gamma \in \neg Y\} \subset \neg X && (\text{def. of } \diamond) \\
&\Leftrightarrow \forall \gamma \in \neg Y \forall \delta \in X \circ \gamma \vdash \delta^{\neg} && (\text{def. of } \neg) \\
&\Leftrightarrow \forall \delta \in X \forall \gamma \in \mathcal{I}n\mathcal{S}qt (\forall \alpha \in Y \gamma \vdash \alpha^{\neg} \Rightarrow \circ\gamma \vdash \delta^{\neg}) && (\text{def. of } \neg) \\
&\Leftrightarrow \forall \delta \in X \forall \gamma \in \mathcal{I}n\mathcal{S}qt (\forall \alpha \in Y \alpha \vdash \gamma^{\sim} \Rightarrow \delta \vdash (\circ\gamma)^{\sim}) && [\sim / \neg] \\
&\Leftrightarrow \forall \delta \in X \forall \gamma \in \mathcal{I}n\mathcal{S}qt (\forall \alpha \in Y \alpha \vdash \gamma^{\sim} \Rightarrow \bullet\delta \vdash \gamma^{\sim}) && [\circ / \bullet] \\
&\Leftrightarrow \forall \delta \in X \forall \gamma \in \mathcal{I}n\mathcal{S}qt (\forall \alpha \in Y \alpha \vdash \gamma \Rightarrow \bullet\delta \vdash \gamma) && \\
&\Leftrightarrow \diamond X \subset Y && (\text{def. of } \blacksquare).
\end{align*}
$$

The adjunction between $\diamond$ and $\sim \diamond \neg$ can be proven in the same way.

$\square$

We define $f$ as the unique **L-morphism** from $\mathbf{F}_m$ to $\mathcal{S}qt_{R,+}$ ($\mathcal{I}n\mathcal{S}qt_{R,+}$) such that, for every propositional variable $p$, $f(p) = g(p)$.
**Lemma 8.1.9.** For all $a \in \mathbf{F}_m$, $a \in f(a) \subset g(a)$.

*Proof.* The **MGL** case:

We prove it by induction over the formulas. For all propositional variable $p$, $p \in f(p) = \{\gamma \in \mathcal{S}qt \mid \gamma \vdash p\}$. Using [11, Theorem 5.11], there remains to prove that for all $a \in \mathbf{F}_m$, if $a \in f(a) \subset \{\gamma \in \mathcal{S}qt \mid \gamma \vdash a\}$, then $\diamond a \in f(\diamond a) \subset \{\gamma \in \mathcal{S}qt \mid \gamma \vdash \diamond a\}$ and $\Box a \in f(\Box a) \subset \{\gamma \in \mathcal{S}qt \mid \gamma \vdash \Box a\}$.

Let $a \in \mathbf{F}_m$ such that $a \in f(a) \subset \{\gamma \in \mathcal{S}qt \mid \gamma \vdash a\}$. Since $a \in f(a)$, by $[L\diamond]$, $\diamond a \le \circ a \in \diamond f(a) = f(\diamond a)$, so, by **Lemma 8.1.6**, $\diamond a \in f(\diamond a)$. Moreover, let $\gamma \in f(\diamond a) = \diamond f(a)$. By $[R\diamond]$, for all $\delta \in f(a) \subset g(a)$ we deduce $\circ \delta \vdash \diamond a$, so, by definition of $\diamond f(a)$, $\gamma \vdash \diamond a$, i.e. $\gamma \in g(\diamond a)$.

For all $b \in \mathbf{F}_m$ and $\Gamma$ such that $\Gamma[a] \vdash b$, by $[L\blacksquare]$, $\Gamma[\circ\blacksquare a] \vdash b$, so $\circ\blacksquare a \le a$, which gives, since $f(a)$ is downward closed and $a \in f(a)$, $\circ\blacksquare a \in f(a)$ and thus $\blacksquare a \in \blacksquare f(a) = f(\blacksquare a)$. Finally, for all $\gamma \in f(\blacksquare a) = \blacksquare f(a) \subset \blacksquare \{\delta \in \mathcal{S}qt \mid \delta \vdash a\}$, $\circ\gamma \vdash a$, so, by $[R\blacksquare]$, $\gamma \vdash \blacksquare a$. Hence $f(\blacksquare a) \subset \{\gamma \in \mathcal{S}qt \mid \gamma \vdash \blacksquare a\}$.

The **InMGL** case:

Note that the two statements of the **MGL** case remain valid with, mutatis mutandis, the same proof. So there only remains to prove that, for all $a \in \mathbf{F}_m$, if $a \in f(a) \subset g(a)$, then $\neg a \in \neg f(a) \subset g(\neg a)$ and $\sim a \in \sim f(a) \subset g(\sim a)$.

This has been proven in [20, Theorem 4.4]. □

For every $\{, \circ, \bullet, \varepsilon\}$-term $G$ (resp. $\{, \circ, \bullet, \sim, \neg, \varepsilon\}$-term), let's write $\overline{G}$ the corresponding $\{, \diamond, \blacksquare, \varepsilon\}$-term (resp. $\{, \diamond, \blacksquare, \sim, \neg, \varepsilon\}$-term), and for every $\gamma \in \mathcal{S}qt$ (resp. $\mathcal{InS}qt$), $\overline{\gamma}$ the corresponding formula.

**Definition 8.1.10.** We say that an *L-structure* (resp. *InL-structure*) $A$ satisfies an analytic structural rule $r = \frac{\Gamma[\Upsilon_1] \vdash a \quad \dots \quad \Gamma[\Upsilon_n] \vdash a}{\Gamma[\Upsilon_0] \vdash a} \in R$ if and only if $A$ satisfies the formula $r^\bullet$ where — is replaced by $\Rightarrow$, $\vdash$ by $\leq$, variables for structures by propositional variables and $\varepsilon$, $\cdot$, and $\circ$ are respectively replaced by $\underline{1}$, $\cdot$ and $\diamond$ (and $\bullet$ by $\diamond$). Define $R^\bullet = \{r^\bullet, r \in R\}$.

We denote by $\mathbf{T}_{\mathbf{MGL}}$ the following theory:

(1) $\{\underline{1}, \cdot, / , \setminus, \wedge, \vee\}$ is a residuated lattice structure

(2) $\diamond$ is left adjoint to $\blacksquare$.

We denote by $\mathbf{T}_{\mathit{InMGL}}$ the following theory:

(1) $\{\underline{1}, \cdot, / , \setminus, \wedge, \vee\}$ is a residuated lattice structure

(2) $\sim \diamond \neg$ is right adjoint to $\diamond$ and $\sim \diamond \neg$ is right adjoint to $\diamond$.

(3) $\sim \neg x = \neg \sim x = x$.

**Lemma 8.1.11** ((cf. [11, Lemma 5.20]). $\mathcal{S}qt_{R,+}$ ($\mathcal{InS}qt_{R,+}$) is a model of $\mathbf{T}_{\mathbf{MGL}}$ ($\mathbf{T}_{\mathit{InMGL}}$) that satisfies every $r \in R$.

*Proof.* According to **Lemma 5.20** of [11], $\mathcal{S}qt_{R,+}$ is a model of every axiom of $\mathbf{T}_{\mathbf{MGL}} \cup R^\bullet$ where no $\diamond$ or $\Box$ appears. Moreover, $\diamond$ is left adjoint to $\blacksquare$ thanks to $[L\blacksquare]$ and $[R\blacksquare]$.
Let $r = \frac{\Gamma[G_1(\gamma_1, \dots, \gamma_n)] \vdash a \quad \dots \quad \Gamma[G_k(\gamma_1, \dots, \gamma_n)] \vdash a}{\Gamma[G_0(\gamma_1, \dots, \gamma_n)] \vdash a}$ be an analytic rule, where the $G_i$s are $\{\,,\circ,\varepsilon\}$-terms satisfied by $\mathcal{S}qt_R$. Let $X_0, \dots, X_n \in \mathcal{S}qt_{R,+}$, such that $\overline{G_1}(X_1, \dots, X_n) \subset X_0, \dots, \overline{G_k}(X_1, \dots, X_n) \subset X_0$ and $(\gamma_i)_{1 \le i \le n} \in \prod_{i=1}^n X_i$.

For all $1 \le i \le k$, $G_i(X_1, \dots, X_n) \subset j(X_0)$, so, for all $a \in \mathbf{F}_m$ context $\Gamma$ such that for all $\delta \in X_0$ $\Gamma[\delta] \vdash a$, $\Gamma[G_1(\gamma_1, \dots, \gamma_n)] \vdash a$, $\dots$, $\Gamma[G_k(\gamma_1, \dots, \gamma_n)] \vdash a$, so, by $r$, $\Gamma[G_0(\gamma_1, \dots, \gamma_n)] \vdash a$. Hence $G_0(\gamma_1, \dots, \gamma_n) \in j(X_0) = X_0$. Since the variables $\gamma_1, \dots, \gamma_n$ are distinct, $\{G_0(\gamma_1, \dots, \gamma_n), \gamma_i \in X_i\} \subset X_0$. By Lemma 8.1.7, $\overline{G_0}(X_1, \dots, X_n) = j(\{G_0(\gamma_1, \dots, \gamma_n), \gamma_i \in X_i\})$, so we can conclude that $\overline{G_0}(X_1, \dots, X_n) \subset X_0$.

Since the analytic rules of **InMGL** do not contain $\neg$ or $\sim$, the proof also works in the **InMGL** case. $\square$

**Theorem 8.1.12 (Completeness theorem).** *The class of models of $\mathbf{T}_{\text{MGL}} \cup R^\bullet$ (resp. $\mathbf{T}_{\text{InMGL}} \cup R^\bullet$) is sound and complete both for $\mathbf{MGL} \cup R$ and $\mathbf{MGL} \cup R \cup \{(\text{Cut})\}$ (resp. $\mathbf{InMGL} \cup R$ and $\mathbf{InMGL} \cup R \cup \{(\text{Cut})\}$).*

*Proof. Soundness:*

Let $A$ be a model of $\mathbf{T}_{\text{MGL}} \cup R^\bullet$, $\mathbf{L}$-morphism $v: \mathbf{F}_m \to A$. Let us define $\vdash_v$ as follows: for all $\gamma \in \mathcal{S}qt$ and $b \in \mathbf{F}_m$, $\gamma \vdash_v b \Leftrightarrow v(\bar{\gamma}) \le v(b)$. We show that $\vdash_v$ satisfies all the rules satisfied by $\vdash_{\text{cut}}$ and so $\vdash_{\text{cut}} \subset \vdash_v$, ie, for all $\gamma \in \mathcal{S}qt$ and $b \in \mathbf{F}_m$, if $\gamma \vdash b$, then $v(\bar{\gamma}) \le v(b)$.

The fact that $\vdash_v$ satisfies the left and right introduction rules $[L.]$, $[R.]$, $[L \lor]$, $[R \lor_1]$, $[R \lor_2]$, $[L \land]$, $[R \land_1]$, $[R \land_2]$, $[L1]$ and $[R1]$ is an immediate consequence of $v(\bar{\cdot})$ sending $\circ$, $\lor$ on $\lor$, $\land$ on $\land$ and $\varepsilon$ on $\mathbb{1}$. Let us prove that $\vdash_v$ satisfies $[L.]$ and $[R.]$ as examples.

For all $a, b$ and $c \in \mathbf{F}_m$ and all context $\Gamma$, if $\Gamma[a, b] \vdash_c v$, then $v(\overline{\Gamma[a, b]}) \le v(c)$, ie $v(\overline{\Gamma[a \cdot b]}) \le v(c)$, ie $v(\Gamma[a \cdot b]) \le v(c)$, ie $\Gamma[a \cdot b] \vdash_c v$. Hence $\vdash_v$ satisfies $[L.]$.

For all $\gamma$ and $\delta \in \mathcal{S}qt$ and $a$ and $b \in \mathbf{F}_m$, if $\gamma \vdash_v a$ and $\Delta \vdash_v b$, then $v(\bar{\gamma}) \le v(a)$ and $v(\bar{\delta}) \le v(b)$, so $v(\bar{\gamma}, \bar{\delta}) = v(\bar{\gamma}) \cdot v(\bar{\delta}) \le v(a) \cdot v(b) = v(a \cdot b)$, ie $\gamma, \delta \vdash_v a \cdot b$. Hence $\vdash_v$ satisfies $[R.]$.

The fact that $\vdash_v$ satisfies $[R/]$ and $[R\backslash]$ is an immediate consequence of $\circ$ and $\backslash$ in $A$ being the right and left residual of $\circ$ and $v$ sending being a morphism for these symbols. Let us prove $[R/]$, as $[R\backslash]$ can be proven in the same way.

For all $\gamma \in \mathcal{S}qt$ and $a$ and $b \in \mathbf{F}_m$ such that $\gamma, a \vdash_v b$, $v(\bar{\gamma}) \cdot v(a) \le v(b)$, ie $v(\bar{\gamma}) \le v(b)/v(a) = v(b/a)$, ie $\gamma \vdash_v b/a$. Hence $\vdash_v$ satisfies $[R/]$.

Finally, there remains to prove that $\vdash_v$ satisfies $[L\backslash]$ and $[L/]$. Since the two proofs are analogous,

let us check that $\vdash_v$ satisfies $\frac{\Gamma[b] \vdash c \quad \gamma \vdash a}{\Gamma[b/a, \gamma] \vdash c}$ $[L/]$.

For this, we will use the fact that, for all context $\Gamma$, there exists $r_\Gamma: A \to A$ such that, for all $x$ and $y \in A$, $\bar{\Gamma}[x] \le y \Leftrightarrow x \le r_\Gamma[y]$, which can be proven by induction over the $\{\,,\circ,\varepsilon\}$-terms.

Let $\Gamma$ be a $\{\,,\circ,\varepsilon\}$-term, $\gamma \in \mathcal{S}qt$, $a, b$ and $c \in \mathbf{F}_m$ such that $\Gamma[b] \vdash_c a$ and $\gamma \vdash_v a$. $v(\overline{\Gamma[b]}) \le v(c)$ and $v(\bar{\gamma}) \le v(a)$, so $\bar{\Gamma}[v(b)] \le v(c)$, so $v(b) \le r_\Gamma[v(c)]$ and thus $v(b)/v(a) \cdot v(\bar{\gamma}) \le v(b)/v(a) \cdot v(a) \le v(b) \le r_\Gamma[v(c)]$, ie $\bar{\Gamma}[v(\gamma) \cdot v(a)/v(b)] \le v(c)$, which is equivalent to $v(\bar{\Gamma}[\gamma, a/b]) \le v(c)$, itself equivalent to $\Gamma[\gamma, a/b] \vdash_v c$. Hence $\vdash_v$ satisfies $[L/]$.

We have thus proven that $\vdash_v$ satisfies all the introduction rules of **MGL**.

Let $r \in R$. We can write $r = \frac{\Gamma[G_1(\gamma_1, \dots, \gamma_n)] \vdash a \quad \dots \quad \Gamma[G_k(\gamma_1, \dots, \gamma_n)] \vdash a}{\Gamma[G_0(\gamma_1, \dots, \gamma_n)] \vdash a}$. For all context $\Gamma$, $G_1, \dots, G_k$, $\{\,,\circ,\varepsilon\}$-terms of arity $n$, $\gamma_1, \dots, \gamma_n \in \mathcal{S}qt$ and $a \in \mathbf{F}_m$ such that $\Gamma[G_1(\gamma_1, \dots, \gamma_n)] \vdash_v a, \dots, \Gamma[G_k(\gamma_1, \dots, \gamma_n)] \vdash_v a$,

$$ \bar{\Gamma}[\overline{G_1}(v(\bar{\gamma}_1), \dots, v(\bar{\gamma}_n))] \le v(a), \dots, \bar{\Gamma}[\overline{G_k}(v(\bar{\gamma}_1), \dots, v(\bar{\gamma}_n))] \le v(a), $$
so, since A satisfies $R^\bullet$, $\bar{\Gamma}[\bar{G}_0(v(\bar{\gamma}_1), \dots, v(\bar{\gamma}_n))] \le v(a)$, ie $\Gamma[G_0(\gamma_1, \dots, \gamma_n)] \vdash_v a$. Hence $\vdash_v$ satisfies $r$.

We finally prove that $\vdash_v$ satisfies the cut rule. For all context $\Gamma$, $\gamma \in \mathcal{S}qt$, $a$ and $b \in \mathbf{F}_m$ such that $\gamma \vdash_v a$ and $\Gamma[a] \vdash_v b$, $v(\bar{\gamma}) \le v(a)$ and $\bar{\Gamma}[v(a)] \le v(b)$, so, since $\bar{\Gamma}$ is non-decreasing, $\bar{\Gamma}[v(\bar{\gamma})] \le v(b)$, ie $\Gamma[\gamma] \vdash_v b$. Thus, $\vdash_v$ satisfies the cut rule.

This concludes the proof of soundness of models of $T_{\mathbf{MGL}} \cup R^\bullet$ with respect to $\mathbf{MGL} \cup R \cup \{(\text{Cut})\}$. We can prove soundness of models of $T_{\text{InMGL}} \cup R^\bullet$ with respect to $\text{InMGL} \cup R \cup \{(\text{Cut})\}$ in the same way. From this soundness, one can deduce the soundness of the models of $T_{\mathbf{MGL}} \cup R^\bullet$ (resp. $T_{\text{InMGL}} \cup R^\bullet$) with respect to $\mathbf{MGL} \cup R$ (resp. $\text{InMGL} \cup R$).

**Completeness:**

Let us prove completeness for $T_{\mathbf{MGL}} \cup R^\bullet$. The proof for $T_{\text{InMGL}} \cup R^\bullet$ is the same and left to the reader.

Let $(a_1, \dots, a_n, b) \in \mathbf{F}_m^{n+1}$ and $G$ be a $\{, \circ, \varepsilon\}$-term such that $\bar{G}(a_1, \dots, a_n) \Rightarrow b$ is true in $T_{\mathbf{MGL}} \cup R^\bullet$. Since $\mathcal{S}qt_{R,+}$ is a model of $T_{\mathbf{MGL}} \cup R^\bullet$, $\bar{G}(f(a_1), \dots, f(a_n)) \subset f(b)$. However, according to **Lemma 8.1.9**, $f(b) \subset g(b)$ and for all $a \in \mathbf{F}_m$, $a \in f(a)$. Hence $G(a_1, \dots, a_n) \in \bar{G}(f(a_1), \dots, f(a_n)) \subset g(b)$, ie $G(a_1, \dots, a_n) \vdash b$. $\square$

**Corollary 8.1.13 (Cut Admissibility theorem).** For every $(a_1, \dots, a_n, b) \in \mathbf{F}_m^{n+1}$ and $\{, \circ, \varepsilon\}$-term $G$ such that $G(a_1, \dots, a_n) \vdash_{\text{cut}} b$, $G(a_1, \dots, a_n) \vdash b$.

*Proof.* For every $(a_1, \dots, a_n, b) \in \mathbf{F}_m^{n+1}$ and $\{, \circ, \varepsilon\}$-term $G$ such that $G(a_1, \dots, a_n) \vdash_{\text{cut}} b$, for all model $A$ of $T_{\mathbf{MGL}} \cup R^\bullet$ and $v: \mathbf{F}_m \to A$, thanks to the soundness with respect to $\mathbf{MGL} \cup R \cup \{(\text{Cut})\}$, $\bar{G}(v(a_1), \dots, v(a_n)) \subset v(b)$, so, thanks to completeness of models of $T_{\mathbf{MGL}} \cup R^\bullet$ with respect to $\mathbf{MGL} \cup R$, $G(a_1, \dots, a_n) \vdash b$. $\square$

Once again, it works the same way for the involutive case.

As a final remark, we can notice that adding a countable rule in analytic form still gives a system that enjoys cut elimination, soundness and completeness.

## REFERENCES

[1] M. Abbadini. "The Dual of Compact Ordered Spaces Is a Variety". In: *Theory and Applications of Categories* 34 (2019), pp. 1401–1439.

[2] B. Banaschewski. "Hüllensysteme und Erweiterung von Quasi-Ordnungen". In: *Zeitschrift für mathematische Logik und Grundlagen der Mathematik* 2 (Jan. 1956), pp. 117–130.

[3] B. Banaschewski. *The Real Numbers in Pointfree Topology*. Textos de Matemática 12. Coimbra: Departamento de Matemática da Universidade de Coimbra, 1997.

[4] B. Banaschewski & G. Bruns. "Categorical Characterization of the MacNeille Completion". In: *Archiv der Mathematik* 18:4 (Sep. 1967), pp. 369–377.

[5] B. Banaschewski, Javier Gutiérrez García & Jorge Picado. "Extended Real Functions in Point-free Topology". In: *Journal of Pure and Applied Algebra* 216:4 (Apr. 2012), pp. 905–922.

[6] I. Ben Yaacov & A. P. Pedersen. "A Proof of Completeness for Continuous First-Order Logic". In: *The Journal of Symbolic Logic* (2010), pp. 168–190.

[7] I. Ben Yaacov, A. Berenstein, C. Henson, & A. Usvyatsov. Model Theory for Metric Structures. *Model Theory With Applications To Algebra And Analysis*. 2 pp. 315-427 (2008)

[8] I. Ben Yaacov & A. Usvyatsov. "Continuous First Order Logic and Local Stability". In: *Transactions of the American Mathematical Society* 362:10 (Oct. 2010), pp. 5213–5259.

[9] L. E. J. Brouwer. "Intuitionism and Formalism". In: *Bulletin of the American Mathematical Society* 20:2 (Nov. 1913), pp. 81–96.

[10] C. C. Chang & H. J. Keisler. *Continuous Model Theory*. Princeton. Princeton University Press, 1966.
[11] A. Ciabattoni, N. Galatos & K. Terui. "Algebraic Proof Theory for Substructural Logics: Cut-Elimination and Completions". In: *Annals of Pure and Applied Logic* 163:3 (Mar. 2012), pp. 266-290.

[12] A. Ciabattoni, & R. Ramanayake, Bunched Hypersequent Calculi for Distributive Substructural Logics. *LPAR-21. 21st International Conference On Logic For Programming, Artificial Intelligence And Reasoning*. pp. 417-398

[13] B. A. Davey & H. A. Priestley. *Introduction to Lattices and Order*. 2. Cambridge: Cambridge University Press, 2002.

[14] J. Dunn, 'Gentzen System' for Positive Relevant Implication. *Journal Of Symbolic Logic*. **38** pp. 356-357 (1973)

[15] L. Esakia. *Heyting Algebras: Duality Theory*. 2nd Edition. Vol. 50. Trends in Logic 3. London: Springer International Publishing, Nov. 2019, pp. 68-98.

[16] I. Farah, B. Hart & D. Sherman. "Model Theory of Operator Algebras I: Stability". In: *Bulletin of the London Mathematical Society* 45:4 (2013), pp. 825-838.

[17] I. Farah, B. Hart & D. Sherman. "Model Theory of Operator Algebras II: Model Theory". In: *Israel Journal of Mathematics* 201:1 (Jan. 2014), pp. 477-505.

[18] I. Farah, B. Hart & D. Sherman. "Model Theory of Operator Algebras III: Elementary Equivalence and HI Factors". In: *Bulletin of the London Mathematical Society* 46:3 (Jun. 2014), pp. 609-628.

[19] M. Fitting. *Intuitionistic Logic Model Theory and Forcing*. North-Holland Publishing Company Amsterdam-London, Jan. 1969.

[20] N. Galatos & P. Jipsen. "Residuated Frames with Applications to Decidability". In: *Transactions of the American Mathematical Society* 365:3 (Oct. 2012), pp. 1219-1249.

[21] N. Galatos, P. Jipsen, T. Kowalski & H. Ono. *Residuated Lattices: An Algebraic Glimpse at Substructural Logics*. Vol. 151. Elsevier, 2007.

[22] N. Galatos & H. Ono. "Cut Elimination and Strong Separation for Substructural Logics: An Algebraic Approach". In: *Annals of Pure and Applied Logic* 161:9 (Jun. 2010), pp. 1097-1133.

[23] J. García Gutiérrez, T. Kubiak & J. Picado. "Lower and Upper Regularizations of Frame Semicontinuous Real Functions". In: *Algebra universalis* 60:2 (Mar. 2009), pp. 169-184.

[24] G. Gentzen. "Investigations into Logical Deduction". In: *American Philosophical Quarterly* 1:4 (1964), pp. 288-306.

[25] G. Gentzen. "Investigations into Logical Deduction: II". In: *American Philosophical Quarterly* 2:3 (1965), pp. 204-218.

[26] G. Gentzen. "Untersuchungen über das logische Schließen. I". In: *Mathematische Zeitschrift* 39:1 (Dec. 1935), pp. 176-210.

[27] G. Gentzen. "Untersuchungen über das logische Schließen. II". In: *Mathematische Zeitschrift* 39:1 (Dec. 1935), pp. 405-431.

[28] J. Gutiérrez García & J. Picado. "On the Algebraic Representation of Semicontinuity". In: *Journal of Pure and Applied Algebra* 210:2 (Aug. 2007), pp. 299-306.

[29] B. Hart, An Introduction to Continuous Model Theory. *Model Theory Of Operator Algebras*. pp. 83-132 (2023,7)

[30] A. Heyting. "Die formalen Regeln der intuitionistischen Logik. I, II, III". In: *Sitzungsbericht PreuBische Akademie der Wissenschaften Berlin, physikalisch-mathematische Klasse II* (1930).

[31] K. H. Hofmann. "Representations of Algebras by Continuous Sections". In: *Bulletin of the American Mathematical Society* 78:3 (1972), pp. 291-373.

[32] K. Hofmann, & K. Keimel, Sheaf Theoretical Concepts in Analysis: Bundles and Sheaves of Banach Spaces, Banach C(X)-Modules. *Applications Of Sheaves: Proceedings Of The Research Symposium On Applications Of Sheaf Theory To Logic, Algebra, And Analysis, Durham, July 9-21, 1977*. pp. 415-441 (1979)
[33] W. A. Howard. "The Formulae-as-Types Notion of Construction". In: *To HB Curry: essays on combinatory logic, lambda calculus and formalism* 44 (1980), pp. 479–490.

[34] P. Hájek. "Metamathematics of Fuzzy Logic". In: *Kluwer Academic Publishers, Dordrecht*. Trends in Logic - Studia Logica Library 4 (1998).

[35] P. T. Johnstone. *Sketches of an Elephant: A Topos Theory Compendium: Volume 2*. Oxford Logic Guides. Oxford, New York: Oxford University Press, Sep. 2002.

[36] S. Mac Lane & I. Moerdijk. *Sheaves in Geometry and Logic: A First Introduction to Topos Theory*. Universitext. New York, NY: Springer, 1994.

[37] H. M. Macneille. "Partially Ordered Sets". In: *Transactions of the American Mathematical Society* 42:3 (1937), pp. 416–460.

[38] J. Marquès. "Categorical Logic from the Perspective of Duality and Compact Ordered Spaces". PhD thesis. Nice: Université Côte d'Azur, 2023.

[39] G. E. Mints. "Cut-Elimination Theorem for Relevant Logics". In: *Journal of Soviet Mathematics* 6:4 (Oct. 1976), pp. 422–428.

[40] L. Nachbin. "Topology and Order". In: *Van Nostrand Co., Inc., Princeton, N.J.-Toronto, Ont.-London*. Van Nostrand Mathematical Studies 4 (1965).

[41] M. Okada. "Phase Semantic Cut-Elimination and Normalization Proofs of First- and Higher-Order Linear Logic". In: *Theoretical Computer Science* 227:1 (Sep. 1999), pp. 333–396.

[42] F. Paoli. *Substructural Logics: A Primer*. Vol. 13. Trends in Logic. Dordrecht: Springer Netherlands, 2002.

[43] J. Z. Reichman. "Semicontinuous Real Numbers in a Topos". In: *Journal of Pure and Applied Algebra* 28:1 (Apr. 1983), pp. 81–91.

[44] L. Santocanale. "Dualizing Sup-Preserving Endomaps of a Complete Lattice". In: *Electronic Proceedings in Theoretical Computer Science* 333 (Feb. 2021), pp. 335–346.

[45] M. Shulman. "Affine Logic for Constructive Mathematics". In: *Bulletin of Symbolic Logic* 28:3 (Sep. 2022), pp. 327–386.

[46] M. Theunissen & Y. Venema. "MacNeille Completions of Lattice Expansions". In: *Algebra universalis* 57:2 (Oct. 2007), pp. 143–193.