# Cut-free Deductive System for Continuous Intuitionistic Logic

Guillaume Geoffroy

► To cite this version:

Guillaume Geoffroy. Cut-free Deductive System for Continuous Intuitionistic Logic. 2025. hal-05322841v5

HAL Id: hal-05322841

https://hal.science/hal-05322841v5

Preprint submitted on 4 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
CUT-FREE DEDUCTIVE SYSTEM FOR CONTINUOUS INTUITIONISTIC
LOGIC

GUILLAUME RAYMOND GEOFFROY

ABSTRACT. We introduce and develop propositional *continuous intuitionistic logic* and propositional *continuous affine logic* through the study of two classes of algebras, and provide sequent-style deductive systems with cut-admissibility for these logics. Our approach centres on AC-algebras, which are algebras *USC(L)* of sup-preserving functions from [0, 1] to an integral commutative residuated complete lattice *L* (in the intuitionistic case, *L* is a locale). We give an algebraic axiomatisation of AC-algebras in the language of continuous logic and prove, using the Macneille completion, that every Archimedean model embeds into some AC-algebra. We also show that (i) *USC(L)* satisfies $v+v = 2v$ exactly when *L* is a locale, (ii) involutiveness of negation in *USC(L)* corresponds to that in *L*, and that (iii) adding those conditions recovers classical continuous logic. For each variant—affine, intuitionistic, involutive, classical—we provide a sequent style deductive system and prove completeness and cut admissibility. This yields the first sequent style formulation of classical continuous logic enjoying cut admissibility.

<footnote>I warmly thank Yoann Dabrowski and Itaï Ben Yaacov for their wise advice and the avenues of reflexion they
provided me. I particularly thank Yoann Dabrowski for his proofreading. I also thank the Istituto Grothendieck for
hosting me at their expense during the Toposes in Mondovì conference, during which I was working on this article.</footnote>
CONTENTS

<table><tr><td>1. Introduction</td><td>1</td></tr><tr><td>2. Definition of the algebra USC(L) of the sup-preserving functions</td><td>4</td></tr><tr><td>2.1. Preliminaries</td><td>5</td></tr><tr><td>2.2. Definition of the commutative residuated complete lattice USC(L)</td><td>5</td></tr><tr><td>2.3. The structure inherited from [0, 1] by convolution</td><td>10</td></tr><tr><td>2.4. The Continuous Logic structure on USC(L)</td><td>20</td></tr><tr><td>3. Algebraic axiomatisation of AC-algebras</td><td>22</td></tr><tr><td>3.1. The three theories</td><td>22</td></tr><tr><td>3.2. Complete Archimedean models of T<sub>0</sub> and T<sub>1</sub></td><td>25</td></tr><tr><td>3.3. Models of T</td><td>32</td></tr><tr><td>4. Cut Admissibility for Affine Continuous Logic</td><td>40</td></tr><tr><td>5. Intuitionistic continuous logic</td><td>42</td></tr><tr><td>5.1. Topological Preliminaries</td><td>43</td></tr><tr><td>5.2. Algebraic axiomatisation of IC-algebras</td><td>45</td></tr><tr><td>5.3. Equivalence between IC-algebras and MC-algebras</td><td>48</td></tr><tr><td>5.4. Reduction of the axiomatisation of USC(L) to the axiomatisation of USC(X)</td><td>51</td></tr><tr><td>5.5. Cut Admissibility</td><td>53</td></tr><tr><td>6. Involutive case</td><td>54</td></tr><tr><td>6.1. Involutive Continuous Algebras</td><td>54</td></tr><tr><td>6.2. Cut Admissibility</td><td>56</td></tr><tr><td>7. Boolean case</td><td>59</td></tr><tr><td>7.1. Boolean Continuous Algebras</td><td>59</td></tr><tr><td>7.2. Cut Admissibility</td><td>61</td></tr><tr><td>8. Annexes</td><td>62</td></tr><tr><td>References</td><td>69</td></tr></table>

# 1. INTRODUCTION

On the one hand, Continuous Logic is a very prolific area of mathematics first introduced in [8] and its model theoretic framework was then developed in [7], [16], [17] and [18] (see also [29] for an introduction). By reinterpreting equality as distance and quantifiers as suprema and infima, it extends classical model-theoretic methods to encompass classes of complete metric structures, domains out of reach of classical first-order logic due to their lack of finitary axiomatisation. While model theory has historically focused on algebraic structures and their first-order theories, continuous first-order logic offers the necessary expressive tools to handle infinitary properties. For instance, it enables to study Hilbert spaces and probability algebras with classical tools of logic, interpreting independence as orthogonality or probabilistic independence depending on context. Contrary to previous attempts [10] and [34], the current framework of [7], that we follow, is more closely aligned with syntax and reasoning of classical logic, permitting broader access to foundational results such as compactness, Löwenheim-Skolem theorems, and omitting types theorems. In [6] is proven a completeness theorem for a Hilbert-style deductive system in Continuous Logic, which is, to the best of our knowledge, the sole try for a proof theory for Continuous Logic.
On the other hand, Intuitionistic Logic was first developed by Brouwer as a logical basis for constructivism [9] as opposed to the formalism of Hilbert. It is the logic obtained from classical logic by removing the principle of excluded middle, or equivalently the rule of *reductio ad absurdum*. However, it has, by now, found very important applications in computer science and proof assistants through the Curry-Howard correspondence [33]. The main mathematical use of Intuitionistic
Logic may be its application to the study of internal objects of toposes (whether elementary or Grothendieck) through Kripke-Joyal semantics [36]. A sequent calculus for it is well-known [26] and [27] (cf. [24] and [25] for english translations) and the completeness of the class of Heyting algebras and the class of Kripke propositional models are well established (for Heyting algebras, the original papers are [30], and a proof can be found in english in [15] and [19]; for completeness of Kripke semantics, see [19]). This article aims at defining the propositional theory of continuous intuitionistic logic.

A previous development of intuitionistic continuous logic had been set up by Jérémie Marquès in [38] under the name *Fuzzy Intuitionistic Logic* relying on a previous work of Marco Abbadini on a positive version of continuous logic [1]. In this paper, Abbadini started from compact ordered topological spaces, which were introduced by L. Nachbin in [40]. They are to topology and partial order what compact Hausdorff spaces are to topology. In [1], the author proved that the category of compact ordered spaces is dual to a category of algebras he called MC-algebras. To prove that MC-algebras form a variety, he gave a sophisticated axiomatisation of them. In [38], Jérémie Marquès introduced the notion of intuitionistic compact ordered spaces and showed that the duality in [1] restricts to a duality between MC-algebras with a residuation and intuitionistic compact ordered spaces. We will show that these algebras are the metrically complete algebras for our alternative approach to continuous intuitionistic logic.

In this paper, we aim at providing sequent style deductive systems for various kind of continuous logics and prove cut admissibility for these systems. In order to prove a cut admissibility theorem for the logics presented in this paper, we will rely on Algebraic Proof Theory. Algebraic Proof Theory was first theorised in [11] and finds its roots in [22] and [41]. Algebraic Proof Theory is a research program aimed at systematically interrelating proof-theoretic and algebraic methods, particularly in the study of substructural logics—understood as extensions of the full Lambek calculus, typically characterized by the absence of structural rules like exchange, weakening, and contraction. It builds on the discovery that the admissibility of the cut rule and subformula property correspond closely to algebraic properties of their semantic counterparts, which are subvarieties of FL-algebras also known as residuated lattices with an additional constant 0 [21]<fnref n="1" />. A key focus is on the transformation of some axioms into analytic structural rules for sequent calculi. It shows a strong link between cut admissibility and stability under Macneille completion. [20] also deals with involutive logics, thus enabling us to obtain a sequent calculus style system for classical continuous logic having the cut admissibility property.

Let us give the motivations of our work. The first objective of this article is to lay the ground work for an analysis of metric structures internal to Grothendieck toposes well handled by continuous logic when the topos is *Set*. Contrary to topological spaces, locales are internalisable into toposes. There are several objects of real numbers internal to a topos ([35], section D 4.7). However, the good notion of norm for internal *C*\*-algebras, Banach spaces and metric spaces in general ([31], [32], [43], [35]) is valued into the so-called semi-continuous real numbers. For a topological space *X*, this object of real numbers is the sheaf of upper semi-continuous functions into *R*, which externalisation is *USC*(*X*, *R*). It motivates the study of *USC*(*X*, *R*) and thus of *USC*(*X*, [0, 1]) that we'll simply denote by *USC*(*X*) and generalisations of this notion. For a locale *L*, the object that we'll call *USC*(*L*) is the natural expansion of *L* by [0, 1]. Indeed, as element of the category *Sup* of complete lattices and sup-preserving functions, *L* is isomorphic to *Sup*({0, 1}, *L*) which means it can be seen as expanded by {0, 1}. *USC*(*L*) = *Sup*([0, 1], *L*) is then the natural expansion of *L* above [0, 1]. The class of *USC*(*L*) for *L* a locale generalises the one of *USC*(*X*) for *X* a topological space as *USC*(*X*) is isomorphic to *USC*(*T*), where *T* is the topology of *X*.
In order to study these structures from a logical point of view, we will give an axiomatisation of the class *USC*(*L*). The language we retained is the one of continuous logic [6]. For cut admissibility

<footnote n="1">¹On contrary to [21], in this paper, the neutral element of a residuated lattice will always be the top one.</footnote>
purposes only, we add some unary symbols that are definable in the language of continuous logic. This approach differs from the one of [1] since, in order to study a positive version of continuous logic, he uses a symbol for the truncated addition one has in $[0,1]$ and a symbol for fusion. We only have a symbol for addition, fusion being definable using subtraction by a constant, thus giving a more natural way to think about our logic from an intuitionist point of view. In [1], the author studies MC-algebras and we show that every MC-algebra can be embedded into a $USC(\mathcal{L})$, for $\mathcal{L}$ a locale. Hence, having interpreted its language in ours, our theory is then a conservative extension of the one of [1]. Together with the cut admissibility property of the sequent calculus style system we give here, we can thus claim having found a sequent calculus style system for MC-algebras.
Let us provide further insight into the main results. In order to embrace logics for constructive mathematics besides intuitionistic and classic continuous logic and tackle logics of which the negation is involutive, we start the work in a generalised framework. In this setting, locales are replaced by residuated commutative complete lattices, which are supposed integral, also known as normal commutative quantales. The unary operations that were only introduced for cut admissibility purposes become here unavoidable, because multiplication by 2 may not be obtained as a sum. It turns out that, for $\mathcal{L}$ a residuated commutative complete lattice, the algebra $USC(\mathcal{L})$ satisfies $v \dashv v = 2v$ if and only if $\mathcal{L}$ is a locale (Corollary 5.2.4) and the negation of $USC(\mathcal{L})$ is involutive if and only if so is the one of $\mathcal{L}$ (Theorem 6.1.1). From here on, we derive the equivalence between our theory to which are added the assumptions $v \dashv v = 2v$ and of involutiveness of the negation and the theory of classical continuous logic. The involutive case, the intuitionistic case and the classical case are dealt with on their own.

In the general framework, as well as for each of the aforementioned particular cases, we provide a sequent calculus-style system, and we prove a cut admissibility theorem. We emphasize here that we obtained the first sequent calculus-style system for classical continuous logic that enjoys a cut admissibility theorem. In the intuitionistic case, our logic, from a proof theoretic point of view, lacks weakening but has distributivity. Contrary to the logics for which Bunched (hyper)sequent calculus is suited, where distributivity is required ([14], [39], [42], [12]), in our case, distributivity is a consequence of the other rules. We emphasize that our approach does not rely on bunched calculus, and the system presented here follows a sequent style in the sense that the only binary structure symbol is "", "". To achieve a proof of cut admissibility for all the logics discussed in this article, we introduce two systems in the section 8: **MGL** for the non involutive case and **InMGL** for the involutive one. We then introduce a new system for each logic studied here and prove a completeness theorem and a cut admissibility theorem. For Intuitionistic Continuous Logic, we call the system **LJK** and we prove the following two theorems

**Theorem A (Completeness theorem).** The classes *IC* and *MC* are both sound and complete for *LJK*.

**Theorem B (Cut Admissibility theorem).** In the system **LJK**, 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.

We now sketch a plan for our article. In section 2, we will define the set of upper semi-continuous functions ($USC(\mathcal{L})$) from a commutative residuated lattice $\mathcal{L}$ to $[0,1]$ and give it inherited structures from $[0,1]$ and $\mathcal{L}$. We will call them AC-algebras (**Definition 2.4.1**). They constitute an algebraic semantics for an affine continuous logic which is a continuous version of affine logic ([45]), also known as FL<sub>ew</sub>, or Intuitionistic Multiplicative Additive Linear Logic (IMALL) with weakening. We will study how properties are transferred from $\mathcal{L}$ to $USC(\mathcal{L})$ in subsection 2.2 and how properties are transferred from $[0,1]$ to $USC(\mathcal{L})$ in subsection 2.3. Then in section 3, we will give an algebraic axiomatisation **T** of these algebras and prove that
**Theorem C.** For all model $A$ of $\mathbf{T}$, there exists a commutative residuated complete lattice $\mathcal{L}$ such that the quotient of the Macneille completion of $A$ by the equivalence relation induced by the preorder $\preceq$ is isomorphic to $\mathrm{USC}(\mathcal{L})$.

For all model $A$ of $\mathbf{T}$, there exists a commutative residuated complete lattice $\mathcal{L}$ such that the quotient of $A$ by $\simeq$ embeds into $\mathrm{USC}(\mathcal{L})$.

To that end, in subsection 3.2, we will introduce two auxiliary theories and show that every complete Archimedean model of these theories is isomorphic to some AC-algebra. In subsection 3.3, we will prove **Theorem C** by showing that all complete Archimedean model of $\mathbf{T}$ is a model of the auxilliary theories. In section 4, we will then give a sequent-style cut-free deductive system for AC-algebras, prove the class of all AC-algebras is complete for this system and that this system has the cut admissibility property.

In section 5, we study the class of IC-algebras, that-is-to-say AC-algebras for which the underlying commutative residuated complete lattice a locale. The first subsection (subsection 5.1), is independent from the rest of the article and can be read on its own. It deals with (compact) ordered topological spaces. In the intuitionistic case, we actually axiomatize algebras whose Archimedean quotient (quotient by the $\simeq$ relation, **Notation 3.3.2**) embeds into some $\mathrm{USC}(X)$ for some topological space $X$. We first give an axiomatisation of IC-algebras in subsection 5.2, and then study their relationship with MC-algebras in subsection 5.4. We are finally able to prove that the class of all $\mathrm{USC}(X)$ for $X$ a topological space and the class of IC-algebras are equivalent in a wide language, namely $(\mathrm{USC}([0, 1]_u^n))_n \in \mathbb{N}$ (**Theorem 5.4.5**). Finally, in subsection 5.5, give a sequent-style cut-free deductive system for IC-algebras and prove the class of all IC-algebras is complete for this system and this system has the cut admissibility property.

In section 6, we study the property of involutiveness of the negation. We first prove that the negation of an AC-algebra is involutive if and only if this is the case for the negation of the underlying commutative residuated complete lattice (**Theorem 6.1.1**), which leads to an axiomatisation of these involutive AC-algebras. Finally, we give a sequent-style cut-free deductive system admitting the cut rule that describes involutive AC-algebras.

In section 7, we study involutive IC-algebras. They are the analogue of complete Boolean algebras in the continuous setting. We first show that the theory obtained to describe this Boolean Continuous Logic is equivalent to the theory of classical continuous logic (**Theorem 7.1.10**). Second, we prove that the ordered topological space associated to any IC-algebra (**Corollary 7.1.9**) is actually just a topological space, thus proving they are analogous to complete Boolean algebras. Finally, we exhibit a sequent-style cut-free deductive system admitting the cut rule that describes this logic.

Finally, in the section **Annexes 8**, we prove a cut-admissibility theorem (**Theorem 8.1.13**) which we rely on to prove all other cut-admissibility theorems of this paper.

## 2. DEFINITION OF THE ALGEBRA $\mathrm{USC}(\mathcal{L})$ OF THE SUP-PRESERVING FUNCTIONS

In this section, we want to define the main object of study of this article ($\mathrm{USC}(\mathcal{L})$), which is built upon $[0, 1]$ and commutative residuated lattices ($\mathcal{L}$), and give it inherited structures from $[0, 1]$ and the commutative residuated lattice $\mathcal{L}$. The definition of $\mathrm{USC}(\mathcal{L})$ is inspired by [3] and [5], which deal with the real numbers in pointfree topology. The language for this study is $\mathcal{L} = \{\top, \wedge, \oplus, \ominus, 2, \frac{1}{2}, j_*, j, \alpha, \emptyset, \underline{1}\}$, whose interpretation in $[0, 1]$ is defined in **Definition 2.1.3**. The language of commutative residuated lattices is $\mathcal{L}_{crl} = \{\wedge, \vee, \otimes, \to, \perp, \top\}$, whereas the one of $[0, 1]$ is $\mathcal{L}_{[0,1]} = \{\max, \min, \oplus, \ominus, 2, \frac{1}{2}, \emptyset, \underline{1}\}$. As we can see, the structure of $[0, 1]$ contains the one of a commutative residuated lattice. However, $\mathcal{L}_{crl}$ will act on $\mathrm{USC}(\mathcal{L})$ using the pointwise structure of $\mathcal{L}$ while $\mathcal{L}_{[0,1]}$ will act by convolution using $\otimes$ from $\mathcal{L}$. Hence, on contrary to expectations when comparing the interpretations of $\mathcal{L}_{crl}$ and $\mathcal{L}_{[0,1]}$, $\max$ is naturally interpreted as $\otimes$, because of the use of $\otimes$ in convolution. However, $\oplus$ and $\otimes$ are intertwinned in such a manner that we will be able to forget $\otimes$ and work with the language $\mathcal{L}$ (**Theorems 2.2.15, 2.4.3 and 2.4.4**). The aim
of this section is thus to determine how properties of $[0, 1]$ and $\mathcal{L}$ are transfered and transformed into properties of $USC(\mathcal{L})$.

## 2.1. Preliminaries.

**Notation 2.1.1.** We denote by $[0, 1]_u$ the set $[0, 1]$ endowed with the topology whose open sets are the $[0, q)$, $q \in [0, 1]$ and $[0, 1]$ itself. For all topological space $X$, we denote by $\mathcal{T}(X)$ the topology of $X$. We denote $\mathcal{T}([0, 1]_u)$ the topology of $[0, 1]_u$, and by $\mathcal{T}([0, 1]_u^n)$ the topology of $[0, 1]_u^n$. Note that $[0, 1]_u$ is sober.

**Definition 2.1.2.** A subset $D$ of an ordered set $X$ is sup-dense in $X$ if every $x \in X$ is the supremum of a part of $D$. We denote by $\mathcal{S}$ up the category of complete orders and sup-preserving functions.

Here comes the interpretation of $\mathcal{L}$ in $[0, 1]$.

**Definition 2.1.3.** Let $x$ and $y \in [0, 1]$.

$\max(x, y)$ is the maximum of $x$ and $y$

$$x+y = x+y = \min((x+y), 1)$$

$$2x = \min(x+x, 1) = x+x$$

$$j_*(x) = \frac{x}{2} + \frac{1}{2}$$

$$\alpha(x) = \max(\frac{x}{2}, j(x))$$

$$\underline{0} = 0$$

$\min(x, y)$ is the minimum of $x$ and $y$

$$x \div y = x \div y = \max((x - y), 0)$$

$$\frac{1}{2}(x) = \frac{x}{2}$$

$$j(x) = 2 \left( x \div \frac{1}{2} \right) = \max(x + x - 1, 0)$$

$$\underline{1} = 1$$

## 2.2. Definition of the commutative residuated complete lattice USC($\mathcal{L}$).

**2.2.1. Definition of the set underlying USC($\mathcal{L}$).** An upper semi-continuous function from a topological space $X$ to $[0, 1]$ is a continuous function from $X$ to $[0, 1]_u$, which, when $X$ is sober, equivalently is a morphism of locales from $\mathcal{T}([0, 1]_u)$ to the topology of $X$ [36, Proposition IX.3.2]. According to **Corollary 2.2.4**, it is also the same data as the one of a sup-preserving function from $[0, 1]$ to the topology of $X$. This idea, also presented in [23, Definition 3.1] and [28, Definition 4.4], together with **Corollary 2.2.4**, lead us to **Definition 2.2.6**.

**Notation 2.2.1.** We denote by $USC(X)$ the set of all upper semi-continuous functions from $X$ to $[0, 1]$ and by $f^*$ the sup-preserving function from $[0, 1]$ to the topology of $X$, that takes $q \in [0, 1]$ to $f^{-1}([0, q))$ for each $f \in USC(X)$.

**Definition 2.2.2.** A commutative residuated lattice is a lattice $\mathcal{L}$ endowed with a commutative monoid operation $\otimes$ whose neutral element is the top one, denoted by $\top$, and a binary operation $\leftarrow$ such that, for all $u, v$ and $w \in \mathcal{L}$, $u \otimes v \le w \Leftrightarrow u \le v \Leftrightarrow w$. $\leftarrow$ is called a residual. A commutative residuated complete lattice is a commutative residuated lattice whose order is complete.

A lax morphism of commutative residuated lattices $f: \mathcal{L} \to \mathcal{K}$ is an order-preserving function such that, for all $u$ and $v \in \mathcal{L}$, $f(u \otimes v) \ge f(u) \otimes f(v)$ and $f(\top) = \top$.

A lax morphism of commutative residuated complete lattices $f: \mathcal{L} \to \mathcal{K}$ is a sup-preserving function such that, for all $u$ and $v \in \mathcal{L}$, $f(u \otimes v) \ge f(u) \otimes f(v)$.

We denote the category of commutative residuated complete lattices and lax morphisms by $\mathcal{Crcl}$.

**Remark 2.2.1.** Residuated complete lattices are also called integral, or normal quantales.

For all this section, let $\mathcal{L}$ be a commutative residuated complete lattice, with internal implication $\rightarrow$, maximum $\top$ and minimum $\bot$.

**Lemma 2.2.3.** Let $D$ be sup-dense in $[0, 1]$, $n \in \mathbb{N}$ and $f: D_n \to \mathcal{L}$ and $g: D^n \to D$ be functions.
If $f$ is non-decreasing, then for all $q \in [0, 1]$, $f^u(q) = \bigvee_{p<qr \ge p} \bigwedge f(r) = \bigvee_{p<q} f(p)$.

Finally, if $f \in USC(\mathcal{L})$, for all $q \in [0, 1]$, $f^u(q) = \bigvee_{p<q} f(p) = f(q)$.

□

Let $\mathcal{D}$ denote the set of dyadic numbers in $[0, 1]$. According to **Corollary 2.2.4**, an upper semi-
continuous function from $\mathcal{L}$ to $[0, 1]$ is entirely characterised by its values on $q$, for $q \in \mathbb{Q} \cap [0, 1]$,
or $q \in \mathcal{D}$.

2.2.2. The pointwise induced structure from $\mathcal{L}$ on $USC(\mathcal{L})$. The aim of this construction is to obtain a commutative residuated complete lattice (Theorem 2.2.11) that satisfies some formulas that are true in $\mathcal{L}$ (Theorem 2.2.15).

To define the order, let us first recall that a function $f \in USC(X)$, for $X$ a sober topological space, is lower than a function $g \in USC(X)$ if and only if $g^*: [0, 1] \to \mathcal{T}(X)$ is lower than $f^*: [0, 1] \to \mathcal{T}(X)$ in the sense that for all $q \in [0, 1]$, $g^*(q) \subset f^*(q)$. Thus, we define the order on $USC(\mathcal{L})$ by $f \le g \Leftrightarrow \forall q \in [0, 1] \, g(q) \le f(q)$, for all $f$ and $g$ being in $USC(\mathcal{L})$. Notice that $\vee$ and $\wedge$ respectively correspond to the lower and upper bounds of two functions for the pointwise order induced by $\mathcal{L}$.

**Lemma 2.2.8** ([5, Proposition 1.1]). Let $f$ and $g \in USC(\mathcal{L})$, and $(f_i)_{i \in I} \in USC(\mathcal{L})^I$.

The maximum of $USC(\mathcal{L})$ is $\underline{1}: [0, 1] \to \mathcal{L}$ and its minimum is $\underline{0}: [0, 1] \to \mathcal{L}$.
$$ q \mapsto \perp 
\qquad q \mapsto \begin{cases} \perp & \text{if } q = 0 \\ \top & \text{otherwise} \end{cases} $$

The lower bound of $(f_i)_{i \in I}$ exists and assigns to each $q \in [0, 1]_< \bigvee_{i \in I} f_i(q)$.

The upper bound of $f$ and $g$ exists and assigns to each $q \in [0, 1]_< \bigvee_{p<q} f(p) \wedge g(p)$.

Hence $USC(\mathcal{L})$ is a complete lattice.

*Proof.* If $\underline{1}$ and $\underline{0}$ are sup-preserving, then, it is clear that they are respectively the maximum and minimum of $USC(\mathcal{L})$.

For all $(q_j)_{j \in J} \in [0, 1]^J$, $\bigvee_{j \in J} \underline{1}(q_j) = \perp = \underline{1} \left( \bigvee_{j \in J} q_j \right)$. For all $(q_j)_{j \in J} \in [0, 1]^J$, if $\bigvee_{j \in J} q_j > 0$ then there exists $j_0 \in J$ such that $q_{j_0} > 0$, so $\bigvee_{j \in J} \underline{0}(q_j) = \top = \underline{0} \left( \bigvee_{j \in J} q_j \right)$, and if $\bigvee_{j \in J} q_j = 0$ then $\bigvee_{j \in J} \underline{0}(q_j) = \perp = \underline{0} \left( \bigvee_{j \in J} q_j \right)$.

Thus, $\underline{1}$ and $\underline{0} \in USC(\mathcal{L})$.

Clearly, the function that assigns $\bigvee_{i \in I} f_i(q)$ to each $q \in [0, 1]$ preserves suprema. Thus, $q \mapsto \bigvee_{i \in I} f_i(q)$ is the lower bound of $(f_i)_{i \in I}$.

Since $\otimes$ is non-decreasing in each coordinate, for all $U, V, U'$ and $V' \in \mathcal{L}$,

$$ (U \otimes V) \wedge (U' \otimes V') \geq (U \wedge U') \otimes (V \wedge V'). $$

Let us denote by $f \wedge g$ the pointwise lower bound of $f$ and $g$. $(f \wedge g)^u \in USC(\mathcal{L})$. What we need to prove is that $(f \wedge g)^u$ is the actual upper bound of $f$ and $g$.

However, by **Lemma 2.2.7**, for all $h \in USC(\mathcal{L})$,

$$ h \ge f \text{ and } h \ge g \Leftrightarrow \forall q \in [0, 1] h(q) \le f(q) \wedge g(q) \Leftrightarrow h \ge f \wedge g^u. $$

□
**Definition 2.2.9.** $\otimes$ and $\to$ are defined on $USC(\mathcal{L})$ by, for all $f$ and $g \in USC(\mathcal{L})$, $f \otimes g: [0,1] \to \mathcal{L}$ and $f \to g: [0,1] \to \mathcal{L}$, $f \to g = (q \mapsto f(q) \to g(q))^u$.
$$q \mapsto f(q) \otimes g(q) \qquad q \mapsto \bigvee_{p<qr \ge p} f(r) \to g(r)$$

**Lemma 2.2.10.** For all $f$ and $g \in USC(\mathcal{L})$, $f \otimes g$ and $f \to g \in USC(\mathcal{L})$. Moreover, $\otimes$ is associative and commutative and its neutral element is $\emptyset$. Finally, $\to$ is the residual of $\otimes$ and satisfies, for all $f$ and $g \in USC(\mathcal{L})$, $(f \to g)(q) \le f(q) \to g(q)$.

*Proof.* Let $f, g$ and $h \in USC(\mathcal{L})$. For all $(q_i)_{i \in I} \in [0,1]^I$,

$$ \begin{aligned} (f \otimes g) \left( \bigvee_{i \in I} q_i \right) &= f \left( \bigvee_{i \in I} q_i \right) \otimes g \left( \bigvee_{i \in I} q_i \right) \\ &= \bigvee_{i,j \in I} f(q_i) \otimes g(q_j) \\ &\le \bigvee_{i,j \in I} f(q_i \vee q_j) \otimes g(q_i \vee q_j) \\ &\le \bigvee_{i \in I} f(q_i) \otimes g(q_i), \end{aligned} $$

so $(f \otimes g) \left( \bigvee_{i \in I} q_i \right) = \bigvee_{i \in I} f(q_i) \otimes g(q_i) = \bigvee_{i \in I} (f \otimes g)(q_i)$. Hence $f \otimes g \in USC(\mathcal{L})$.

$\otimes$ is clearly associative and commutative.

For all $q \in [0,1]$, $(\emptyset \otimes f)(q) = \top \otimes f(q) = f(q)$.

Since $f \to g = (q \mapsto f(q) \to g(q))^u$, according to **Lemma 2.2.7**:

- $f \to g \in USC(\mathcal{L})$,

- for all $q \in [0,1]$, $(f \to g)(q) \le f(q) \to g(q)$

- and, for all $h \in USC(\mathcal{L})$,

$$f \to g \le h \Leftrightarrow \forall q \in [0,1] h(q) \le f(q) \to g(q) \Leftrightarrow \forall q \in [0,1] f(q) \otimes h(q) \le g(q) \Leftrightarrow g \le f \otimes h.$$

□

We have thus proven the following theorem.

**Theorem 2.2.11.** $(USC(\mathcal{L}), \otimes, \to)$ with the reverse order is a commutative residuated complete lattice.

**Lemma 2.2.12.** For all $f$ and $g \in USC(\mathcal{L})$, for all $q \in [0,1]$,

(1) $(f \lor g) = (q \mapsto f(q) \land g(q))^u$,

(2) $(f \land g) = (q \mapsto f(q) \lor g(q))^u$,

(3) $f \otimes g = (q \mapsto f(q) \otimes g(q))^u$,

(4) $f \to g = (q \mapsto f(q) \to g(q))^u$,

(5) $\emptyset = (q \mapsto \top)^u$,

(6) $\underline{1} = (q \mapsto \bot)^u$.

*Proof.* Let $f$ and $g \in USC(\mathcal{L})$. The argument relies on **Lemma 2.2.7**.

(1) $q \mapsto f(q) \land g(q)$ is non-decreasing, so, for all $p \in [0,1]$,

$$(q \mapsto f(q) \land g(q))^u(p) = \bigvee_{r<p} f(r) \land g(r) = (f \lor g)(p).$$

(2) $f \land g: q \mapsto f(q) \lor g(q) \in USC(\mathcal{L})$, so $(f \land g)^u = f \land g$, i.e. $f \land g = (q \mapsto f(q) \lor g(q))^u$.

(3) $f \otimes g: q \mapsto f(q) \otimes g(q) \in USC(\mathcal{L})$, so $(f \otimes g)^u = f \otimes g$, i.e. $f \otimes g = (q \mapsto f(q) \otimes g(q))^u$.
(4) By definition of $f \to g$.

(5) For all $q \in [0, 1]$, $(q \mapsto \top)^u(q) = \bigvee_{p<q} \top = \emptyset(q)$.

(6) For all $q \in [0, 1]$, $(q \mapsto \bot)^u(q) = \bot = \mathbb{1}(q)$.

□

**Definition 2.2.13.** For the purpose of **Lemma 2.2.14** and **Theorem 2.2.15**, let $\mathcal{L}_{crl} = \{\otimes, \to, \vee, \wedge, \bot, \top\}$. We consider a countable set $\mathcal{V}$ of variables. Let $E$ denote the set of terms of $\mathcal{L}_{crl}$ and let's define $E_{lax}$ and $E_{colax}$ as follows:

$$E_{lax} = \{\varphi \in E \mid \forall f: \mathcal{V} \to USC(\mathcal{L}) \text{ and } q \in [0, 1] \ \varphi[f](q) \le \varphi[f(q)]\}$$

$$E_{colax} = \{\varphi \in E \mid \forall f: \mathcal{V} \to USC(\mathcal{L}) \text{ and } q \in [0, 1] \ \varphi[f](q) \ge \varphi[f(q)]\}.$$

**Remark 2.2.3.** Care must be taken when interpreting $\vee$ in $USC(\mathcal{L})$, that is $\wedge$, and vice-versa. Hence, for all terms $\varphi$ and $\psi$ of $\mathcal{L}_{crl}$, $(\varphi \vee \psi)[f](q) = (\varphi[f] \wedge \psi[f])(q) = \varphi[f](q) \vee \psi[f](q)$.

**Lemma 2.2.14.**

(1) $E_{colax}$ contains the variables and constants and is stable by $\otimes$ and $\vee$.

(2) $E_{lax}$ contains the variables and constants and is stable by $\otimes$, $\vee$ and $\wedge$.

(3) $E_{colax} \to E_{lax} \subset E_{lax}$ and $E_{lax} \to \bot \subset E_{colax}$.

*Proof.* To begin with, it is clear that both $E_{lax}$ and $E_{colax}$ contain the variables and constants. Let $f: \mathcal{V} \to USC(\mathcal{L})$. We here remind the reader that the interpretation of $\vee$ in $USC(\mathcal{L})$ is $\wedge$, and $\wedge$ is defined as the pointwise upper bound.

(1) Let $\varphi$ and $\psi \in E_{colax}$ and $q \in [0, 1]$.

$$(\varphi \otimes \psi)[f](q) = \varphi[f](q) \otimes \psi[f](q) \ge \varphi[f(q)] \otimes \psi[f(q)] = (\varphi \otimes \psi)[f(q)] \quad (\textbf{Definition 2.2.9}).$$

$$(\varphi \vee \psi)[f](q) = \varphi[f](q) \vee \psi[f](q) \ge \varphi[f(q)] \vee \psi[f(q)] = (\varphi \vee \psi)[f(q)] \quad (\text{by Lemma 2.2.8}).$$

(2) Let $\varphi$ and $\psi \in E_{colax}$ and $q \in [0, 1]$.

$$(\varphi \otimes \psi)[f](q) = \varphi[f](q) \otimes \psi[f](q) \le \varphi[f(q)] \otimes \psi[f(q)] = (\varphi \otimes \psi)[f(q)].$$

$$(\varphi \vee \psi)[f](q) = \varphi[f](q) \vee \psi[f](q) \le \varphi[f(q)] \vee \psi[f(q)] = (\varphi \vee \psi)[f(q)].$$

$$(\varphi \wedge \psi)[f](q) \le \varphi[f](q) \wedge \psi[f](q) \le \varphi[f(q)] \wedge \psi[f(q)] = (\varphi \wedge \psi)[f(q)].$$

(3) Let $\varphi \in E_{lax}$, $\psi \in E_{colax}$ and $q \in [0, 1]$.

$$(\psi \to \varphi)[f](q) \le \psi[f](q) \to \varphi[f](q) \le \psi[f(q)] \to \varphi[f(q)] \quad (\text{by Lemma 2.2.10}).$$

□

**Theorem 2.2.15.** Let $\varphi_0, \dots, \varphi_k \in E_{lax}$ and $\psi_0, \dots, \psi_k \in E_{colax}$.

If $\mathcal{L} \models (\psi_1 \le \varphi_1, \dots, \psi_k \le \varphi_k) \Rightarrow \varphi_0 \le \psi_0$, then

$$USC(\mathcal{L}) \models (\psi_1 \ge \varphi_1, \dots, \psi_k \ge \varphi_k) \Rightarrow \varphi_0 \ge \psi_0.$$

*Proof.* Let $f: \mathcal{V} \to USC(\mathcal{L})$, $q \in [0, 1]$, $\varphi_0, \dots, \varphi_k \in E_{lax}$ and $\psi_0, \dots, \psi_k \in E_{colax}$ such that $\mathcal{L} \models (\psi_1 \le \varphi_1, \dots, \psi_k \le \varphi_k) \Rightarrow \varphi_0 \le \psi_0$. Assume $USC(\mathcal{L}) \models \psi_1[f] \ge \varphi_1[f], \dots, \psi_k[f] \ge \varphi_k[f]$. For all $1 \le i \le k$, $\psi_i[f(q)] \le \psi_i[f](q) \le \varphi_i[f](q) \le \varphi_i[f(q)]$, so

$$\mathcal{L} \models (\psi_1[f(q)] \le \varphi_1[f(q)], \dots, \psi_k[f(q)] \le \varphi_k[f(q)].$$

Thus $\mathcal{L} \models \varphi_0[f(q)] \le \psi_0[f(q)]$. Hence, $\varphi_0[f](q) \le \varphi_0[f(q)] \le \psi_0[f](q) \le \psi_0[f](q)$.

$$\text{Hence } USC(\mathcal{L}) \models \varphi_0[f] \ge \psi_0[f].$$

□

We can also embed $\mathcal{L}$ into $USC(\mathcal{L})$.
**Definition 2.2.16.** To each $U \in \mathcal{L}$, we associate the 0-indicator $0_U: [0,1] \to \mathcal{L}$.
$$q \mapsto \begin{cases} U & \text{if } 1 > q > 0 \\ \perp & \text{if } q \not> 0 \end{cases}.$$

To each $f \in USC(\mathcal{L})$, we associate $U_f := f(1)$.

**Lemma 2.2.17.** For every $U \in \mathcal{L}$, $0_U \in USC(\mathcal{L})$, and, for all $f \in USC(\mathcal{L})$,
$$U_f \leq U \Leftrightarrow f \geq 0_U.$$

Moreover, for all $U \in \mathcal{L}$, $U_{0_U} = U$, so $U \mapsto 0_U$ is an order embedding of $\mathcal{L}$ into $USC(\mathcal{L})^{\text{op}}$ and $f \mapsto U_f$ is onto.

*Proof.* For every $U \in \mathcal{L}$ and $f \in USC(\mathcal{L})$,
$$U_f \leq U \Leftrightarrow \forall q \in [0,1] f(q) \leq U \Leftrightarrow \forall q \in [0,1] f(q) \leq 0_U(q) \Leftrightarrow f \geq 0_U.$$

Moreover, for all $U \in \mathcal{L}$, $U_{0_U} = 0_U(1) = U$. $\square$

**Lemma 2.2.18.** $\mathcal{L}^{\text{op}} \to USC(\mathcal{L})$ is an $\mathcal{L}_{\text{crl}}$-embedding.
$$U \mapsto 0_U$$

*Proof.* $0_{\perp} = 1$.

$$0_{\top} = 0.$$

Let $U$ and $V \in \mathcal{L}$ and $q > 0$. Since $q > 0$, $0_U(q) = U$ and $0_V(q) = V$.

$$0_{U \otimes V}(q) = U \otimes V = 0_U(q) \otimes 0_V(q) = (0_U \otimes 0_V)(q).$$

$$0_{U \wedge V}(q) = U \wedge V = 0_U(q) \wedge 0_V(q) = (0_U \vee 0_V)(q).$$

$$0_{U \vee V}(q) = U \vee V = 0_U(q) \vee 0_V(q) = (0_U \wedge 0_V)(q).$$

$$0_U \to 0_V(q) = \bigvee_{p<q} \bigwedge_{r \ge p} 0_U(r) \to 0_V(r) = \bigvee_{0<p<q} \bigwedge_{r \ge p} U \to V = U \to V = 0_{U \to V}(q). \quad \square$$

Now, we shall state a strong converse of **Theorem 2.2.15**, which is an immediate consequence of **Lemma 2.2.18**.

**Theorem 2.2.19.** For all terms $\varphi_0, \dots, \varphi_k$ and $\psi_0, \dots, \psi_k$ in the language $\mathcal{L}_{\text{crl}}$, if $USC(\mathcal{L})$ satisfies $(\psi_1 \ge \varphi_1, \dots, \psi_k \ge \varphi_k) \Rightarrow \varphi_0 \ge \psi_0$, then $\mathcal{L} \models (\psi_1 \le \varphi_1, \dots, \psi_k \le \varphi_k) \Rightarrow \varphi_0 \le \psi_0$.

## 2.3. The structure inherited from $[0,1]$ by convolution.

2.3.1. The action of $(USC([0, 1]_u^n))_n \in \mathbb{N}$ on $USC(\mathcal{L})$. Here, we want to give an interpretation of any upper semi-continuous function from $[0, 1]_u^n$ to $[0, 1]$, $n \in \mathbb{N}$, in $USC(\mathcal{L})$ and give some kind of formulas in this language that are true in $USC(\mathcal{L})$ if they are true in $[0, 1]$ (Theorem 2.3.10). To this purpose, we use a copairing-like notion. We will then aim at reducing the language to only a few symbols. Before getting to the heart of the matter, we need some notations.

**Notation 2.3.1.** We recall here that the topology of $[0,1]_u^n$ is denoted $\mathcal{T}([0,1]_u)$ and the topology of $[0,1]_u^n$ is denoted $\mathcal{T}([0,1]_u^n)$, for all $n \in \mathbb{N}$ (Notation 2.1.1).

Let $n \in \mathbb{N}$. For all $a \in USC([0,1]_u^n)$, let's denote by $a^*$ the sup-preserving function from $[0,1]$ to $\mathcal{T}([0,1]_u^n)$ induced by $a$, namely $a^*: [0,1] \to \mathcal{T}([0,1]_u^n)$.

$$q \mapsto a^{-1}([0, q])$$

For all term $\varphi$ in the language $(USC([0,1]_u^n))_n \in \mathbb{N}$, let $a_\varphi$ be its interpretation in $[0,1]$. For all $f \in USC(\mathcal{L})^n$, let $G(f) = (G(f_1), \dots, G(f_n))$ (cf. Corollary 2.2.4).

Finally, let $\mathcal{V}$ denote a countable set of variables. For all $v \in \mathcal{V}^n$ and $p: \mathcal{V} \to [0,1]$ and $f: \mathcal{V} \to USC(\mathcal{L})$, let $p_v = (p(v_1), \dots, p(v_n))$ and $f_v = (f(v_1), \dots, f(v_n))$.

**Definition 2.3.2.** Let $n \in \mathbb{N}$, $X_1, \dots, X_n$ be topological spaces, $\mathcal{K}$ be a commutative residual complete lattice and $f_1: \mathcal{T}(X_1) \to \mathcal{K}$, $\dots, f_n: \mathcal{T}(X_n) \to \mathcal{K}$ be morphisms of commutative residual complete lattices.
We define $cop(f_1, \dots, f_n): \mathcal{T}\left(\prod_{i=1}^{n} X_i\right) \to \mathcal{K}$.
$$U \mapsto \bigvee_{U_1 \times \dots \times U_n \subseteq U} f_1(U_1) \otimes \dots \otimes f_n(U_n)$$

**Lemma 2.3.3.** *cop*(*f*₁, ..., *f*ₙ) is the smallest lax morphism of commutative residuated complete lattices *g*: T(Πᵢ₁) → K such that, for all 1 ≤ *i* ≤ *n*,

$$g(X_1 \times \dots \times X_{i-1} \times U_i \times X_{i+1} \times \dots \times X_n) \geq f_i(U_i).$$

Moreover, for $g = cop(f_1, \dots, f_n)$, the preceding inequality is an equality.

*Proof.* We prove it for $n = 2$ only, the proof being the same in general.

Let $X_1$ and $X_2$ be topological spaces and $f_1: \mathcal{T}(X_1) \to \mathcal{K}$ and $f_2: \mathcal{T}(X_2) \to \mathcal{K}$ be morphisms of commutative residuated complete lattices. For all $U_1 \in \mathcal{T}(X_1)$ and $U_2 \in \mathcal{T}(X_2)$, $cop(f_1, f_2)(U_1 \times U_2) = f_1(U_1) \otimes f_2(U_2)$, so $cop(f_1, f_2)(U_1 \times X_2) = f_1(U_1)$ and $cop(f_1, f_2)(X_1 \times U_2) = f_2(U_2)$.

$cop(f_1, f_2)$ clearly preserves upper bounds.

For all $U$ and $V \in \mathcal{T}(X_1 \times X_2)$,

$$ \begin{align*} cop(f_1, f_2)(U \cap V) &= \bigvee_{U_1 \times U_2 \subseteq U \cap V} f_1(U_1) \otimes f_2(U_2) \\ &= \bigvee_{U_1 \times U_2 \subseteq UV_1 \times V_2 \subseteq V} f_1(U_1 \cap V_1) \otimes f_2(U_2 \cap V_2) \\ &\geq \bigvee_{U_1 \times U_2 \subseteq U} f_1(U_1) \otimes f_1(V_1) \otimes f_2(U_2) \otimes f_2(V_2) \\ &= cop(f_1, f_2)(U) \otimes cop(f_1, f_2)(V). \end{align*} $$

For all lax morphism of commutative residuated complete lattice $g: \mathcal{T}(X_1 \times X_2) \to \mathcal{K}$ such that, for all $U_1 \in \mathcal{T}(X_1)$ and $U_2 \in \mathcal{T}(X_2)$, $g(U_1 \times X_2) \geq f_1(U_1)$ and $g(X_1 \times U_2) \geq f_2(U_2)$, for all $U \in \mathcal{T}(X_1 \times X_2)$,

$$ \begin{align*} g(U) &= \bigvee_{U_1 \times U_2 \subseteq U} g(U_1 \times U_2) \\ &= \bigvee_{U_1 \times U_2 \subseteq U} g((U_1 \times X_2) \cap (X_1 \times U_2)) \\ &\geq \bigvee_{U_1 \times U_2 \subseteq U} g(U_1 \times X_2) \otimes g(X_1 \times U_2) \\ &\geq \bigvee_{U_1 \times U_2 \subseteq U} f_1(U_1) \otimes f_2(U_2) \\ &= cop(f_1, f_2)(U). \end{align*} $$

□

**Corollary 2.3.4.** For all $n \in \mathbb{N}$ and $f \in USC(\mathcal{L})^n$, $cop(G(f)) \in \mathcal{C}rcl(\mathcal{T}([0, 1]^n_u), \mathcal{L})$.

**Definition 2.3.5.** Let $n \in \mathbb{N}$ and $a \in USC([0, 1]^n_u)$.

We define the interpretation of $a$ in $USC(\mathcal{L})$ by, for all $f \in USC(\mathcal{L})^n$, $a(f) = cop(G(f)) \circ a^*$, i.e. for all $q \in [0, 1]$, $a(f)(q) = \bigvee_{i=1}^n G(f_i)(U_i) \otimes \dots \otimes G(f_n)(U_n)$.

$$\prod_{i=1}^{n} U_i \subseteq a^{-1}([0, q))$$
**Remark 2.3.1.** Notice that, if $\mathcal{L}$ is the topology of a topological space $X$, then, for all $f \in USC(X)^n$ cop($f_1^*, \dots, f_n^*$): $\mathcal{T}([0, 1]^n_u) \to \mathcal{L}$ is the map associated to $f: X \to [0, 1]^n$ through the isomorphism $USC(X) \simeq USC(\mathcal{L})$, and thus $a(f) = (a \circ f)^*$.

**Lemma 2.3.6.** Let $(a_i)_{i \in I} \in USC([0, 1]^n_u)^I$ and $f \in USC(\mathcal{L})^n$.

$$ \left( \bigwedge_{i \in I} a_i \right) (f) = \bigwedge_{i \in I} a_i(f). \quad \text{Thus, } a \mapsto a(f) \text{ is non-decreasing.} $$

*Proof.* For all $q \in [0, 1]$,

$$ \begin{aligned} \left( \bigwedge_{i \in I} a_i \right) (f)(q) &= \operatorname{cop}(G(f)) \left( \left( \bigwedge_{i \in I} a_i \right)^*(q) \right) = \operatorname{cop}(G(f)) \left( \bigvee_{i \in I} a_i^*(q) \right) \\ &= \bigvee_{i \in I} \operatorname{cop}(G(f))(a_i^*(q)) = \left( \bigwedge_{i \in I} a_i(f) \right) (q), \end{aligned} $$

$$ \text{so } \left( \bigwedge_{i \in I} a_i \right) (f) = \bigwedge_{i \in I} a_i(f). \quad \square $$

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

**Lemma 2.3.7.** For all $a \in USC([0, 1]^n_u)$ and $b_1 \in USC([0, 1]^k_1)$, $\dots, b_n \in USC(\mathcal{L})([0, 1]^k_1)$, for all $f \in USC(\mathcal{L})^{k_1} \times \dots \times USC(\mathcal{L})^{k_n}$,

$$ (a \circ (b_1, \dots, b_n))(f) = a(b_1(f_{1,1}, \dots, f_{1,k_1}), \dots, b_n(f_{n,1}, \dots, f_{n,k_n})). $$

*Proof.* Let $a \in USC([0, 1]^n_u)$, $b_1 \in USC([0, 1]^k_1)$, $\dots, b_n \in USC(\mathcal{L})([0, 1]^k_1)$ and $f \in USC(\mathcal{L})^{k_1} \times \dots \times USC(\mathcal{L})^{k_n}$. Let $f_i$ denote $(f_{i,1}, \dots, f_{i,k_i})$.

**Claim:** $\operatorname{cop}(G(f)) \circ \operatorname{cop}(b_1^{-1}, \dots, b_n^{-1}) = \operatorname{cop}(\operatorname{cop}(G(f_1)) \circ b_1^{-1}, \dots, \operatorname{cop}(G(f_n)) \circ b_n^{-1})$. Indeed, for all $U \in \mathcal{T}(\prod_{i=1}^n X_i)$,

$$ \begin{aligned} \operatorname{cop}(G(f)) \circ \operatorname{cop}(b_1^{-1}, \dots, b_n^{-1})(U) &= \operatorname{cop}(G(f)) \left( \bigcup_{\prod_{i=1}^n U_i \subset U} (b_1^{-1}(U_1) \times \dots \times b_n^{-1}(U_n)) \right) \\ &= \bigvee_{\prod_{i=1}^n U_i \subset U} \operatorname{cop}(G(f))(b_1^{-1}(U_1) \times \dots \times b_n^{-1}(U_n)) \\ &= \bigvee_{\prod_{i=1}^n U_i \subset U} \operatorname{cop}(G(f_1))(b_1^{-1}(U_1)) \otimes \dots \otimes \operatorname{cop}(G(f_n))(b_n^{-1}(U_n)) \\ &= \operatorname{cop}(\operatorname{cop}(G(f_1)) \circ b_1^{-1}, \dots, \operatorname{cop}(G(f_n)) \circ b_n^{-1})(U). \end{aligned} $$

By noticing that, $(a \circ (b_1, \dots, b_n))^{-1} = \operatorname{cop}(b_1^{-1}, \dots, b_n^{-1}) \circ a^{-1}$, we can conclude that, for all $q \in [0, 1]$,

$$ \begin{aligned} (a \circ (b_1, \dots, b_n))(f)(q) &= \operatorname{cop}(G(f)) \circ (a \circ (b_1, \dots, b_n))^{-1}([0, q)) \\ &= \operatorname{cop}(G(f)) \circ \operatorname{cop}(b_1^{-1}, \dots, b_n^{-1}) \circ a^{-1}([0, q)) \\ &= \operatorname{cop}(\operatorname{cop}(G(f_1)) \circ b_1^{-1}, \dots, \operatorname{cop}(G(f_n)) \circ b_n^{-1}) \circ a^*(q) \\ &= a(b_1(f_1), \dots, b_n(f_n))(q). \end{aligned} $$

<figure><img src="image_3.png" /></figure>
**Definition 2.3.8.** A term of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ is linear if any variable occurs at most once in it.

**Lemma 2.3.9.** Let $\varphi[v_1, \dots, v_n]$ and $\psi[v_1, \dots, v_n]$ be two terms of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ and $f: \mathcal{V} \to USC(\mathcal{L})$. Let $v = (v_1, \dots, v_n)$. $\varphi[f] \ge a_\varphi(f_v)$, with equality if $\varphi$ is linear (Notation 2.3.1) and $a_{\varphi \wedge \psi}(f_v) = a_\varphi(f_v) \wedge a_\psi(f_v)$.

*Proof.* By induction over the linear terms of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$. The proposition is true for constants and variables.

Let $a \in USC([0, 1]_u^n)$, $\varphi_1[v_{1,1}, \dots, v_{1,k_1}]$, $\dots$, $\varphi_n[v_{n,1}, \dots, v_{n,k_n}]$ be terms of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$, $f: \mathcal{V} \to USC(\mathcal{L})$. Assume that $\varphi_1[f] = a_{\varphi_1}(f_{v_1})$, $\dots$, $\varphi_n[f] = a_{\varphi_n}(f_{v_n})$ and that $a(\varphi_1, \dots, \varphi_n)$ is linear, i.e., for all $1 \le i, i' \le n$, $1 \le j \le k_i$ and $1 \le j' \le k_{i'}$, if $(i, j) \ne (i', j')$, then $v_{i,j} \ne v_{i',j'}$. By linearity of $a[u_1, \dots, u_n]$, for all $q \in [0, 1]^n$, $a_{a[u_1, \dots, u_n]}(q) = a(q_1, \dots, q_n)$, so, thanks to Lemma 2.3.7,

$$ 
\begin{align*}
a[\varphi_1/u_1, \dots, \varphi_n/u_n][f] &= a[\varphi_1[f_{v_1}]/u_1, \dots, \varphi_n[f_{v_n}]/u_n] \\
&= a[a_{\varphi_1}(f_{v_1})/u_1, \dots, a_{\varphi_n}(f_{v_n})/u_n] \\
&= a_{a[u_1, \dots, u_n]}(a_{\varphi_1}(f_{v_1}), \dots, a_{\varphi_n}(f_{v_n})) \\
&= a(a_{\varphi_1}(f_{v_1}), \dots, a_{\varphi_n}(f_{v_n})) \\
&= (a \circ (a_{\varphi_1}, \dots, a_{\varphi_n}))(f_v) \\
&= a_{a(\varphi_1, \dots, \varphi_n)}(f_v)
\end{align*}
$$

Hence, for all linear term $\varphi[v]$ of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ and $f: \mathcal{V} \to USC(\mathcal{L})$, $\varphi[f] = a_\varphi(f_v)$.

Let $\varphi[v_1, \dots, v_n]$ be a term of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$, $f: \mathcal{V} \to USC(\mathcal{L})$ and $q \in [0, 1]$. Let us denote by $k_i$ the number of occurrences of $v_i$ in $\varphi$, for all $1 \le i \le n$. Let also, for all $k \in \mathbb{N}$ and all set $u, ku$ denote the $k$-uple $(u, \dots, u)$. There exists a linear term $\varphi_0[u_{1,1}, \dots, u_{n,k_n}]$ such that $\varphi[v_1, \dots, v_n] = \varphi_0[k_1 v_1, \dots, k_n v_n]$.

$$ 
\begin{align*}
\varphi[f](q) &= \varphi_0[f_{v_1}/u_{1,1}, \dots, f_{v_1}/u_{1,k_1}, \dots, f_{v_n}/u_{n,1}, \dots, f_{v_n}/u_{n,k_n}](q) = a_{\varphi_0}(g)(q) \\
&= \bigvee_{\prod_{i=1}^k \prod_{j=1}^k U_{i,j} \subset a_{\varphi_0}(q)} \bigotimes_{i=1}^n \bigotimes_{j=1}^{k_i} G(f_{v_i})(U_{i,j}) \\
&\le \bigvee_{\prod_{i=1}^k \prod_{j=1}^k U_{i,j} \subset a_{\varphi_0}(q)} \bigotimes_{i=1}^n G(f_{v_i}) \left( \bigcap_{j=1}^{k_i} U_{i,j} \right) \tag{1} \\
&= \bigvee_{(*) \prod_{i=1}^k U_{i,j} \subset a_{\varphi_0}(q)} \bigotimes_{i=1}^n G(f_{v_i})(U_i) \\
&= a_\varphi(f_v)(q)
\end{align*}
$$

(*) is justified by the following : for all family of open subsets $(U_{i,j})_{\substack{1 \le i \le n \\ 1 \le j \le k_i}}$ of $[0, 1]$,

$$ \prod_{i=1}^{n} \prod_{j=1}^{k_i} U_{i,j} \subset a_{\varphi_0}^*(q) \Rightarrow \prod_{i=1}^{n} \prod_{j=1}^{k_i} U_{i,j} \subset a_{\varphi}^*(q) $$
and, for all family of open subsets of $[0, 1] (U_i)_{1\le i\le n}$,

$$ \prod_{i=1}^{n} U_i \subset a_{\varphi}(q) \Rightarrow \prod_{i=1}^{n} \prod_{j=1}^{k_i} U_i \subset a_{\varphi_0}^*(q). $$

Let $\psi[v]$ be another term of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$.

First of all, we notice that $a_{\varphi \wedge \psi} = a_{\varphi} \wedge a_{\psi}$. Thus,

$$ a_{\varphi \wedge \psi}(f_v)(q) = \hat{f}_v \circ (a_{\varphi} \wedge a_{\psi})^*(q) = \hat{f}_v(a_{\varphi}^*(q) \cup a_{\psi}^*(q)) = \hat{f}_v(a_{\varphi}^*(q)) \vee \hat{f}_v(a_{\psi}^*(q)) = a_{\varphi}(f_v) \wedge a_{\psi}(f_v)(q). \quad \square $$

**Remark 2.3.2.** If $\otimes = \wedge$, then inequality (1) is actually an equality and thus, for every term $\varphi[v]$ of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ and $f: \mathcal{V} \to USC(\mathcal{L})$, $\varphi[f] = a_{\varphi}(f_v)$.

We will crucially use the next result to give a conceptual proof of soundness in section 3. We here emphasize that some equations true in $[0, 1]$ become false in $USC(\mathcal{L})$, such as $\max(v, v) \le v$, which becomes $v \otimes v \le v$ as stated by **Lemma 2.3.22**, and may not be true in $USC(\mathcal{L})$.

**Theorem 2.3.10.** Let $\varphi_1[v], \dots, \varphi_n[v]$ and $\psi[v]$ be terms in the language $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ and assume that for all $1 \le i \le n$ $\varphi_i$ is linear.

$$ \text{Then, if } [0, 1] \models \bigwedge_{i=1}^{n} \varphi_i \le \psi, \text{ USC}(\mathcal{L}) \models \bigwedge_{i=1}^{n} \varphi_i \le \psi. $$

$$ \textbf{Proof.} \text{ Assume } [0, 1] \models \bigwedge_{i=1}^{n} \varphi_i \le \psi \text{ and let } f: \mathcal{V} \to USC(\mathcal{L}). $$

Remark 2.3.2 implies that for all $p: \mathcal{V} \to [0, 1]$, $a_{\bigwedge_{i=1}^{n} \varphi_i}(p_v) = \bigwedge_{i=1}^{n} \varphi_i[p] \le \psi[p] = a_{\psi}(p_v)$, so $a_{\bigwedge_{i=1}^{n} \varphi_i} \le a_{\psi}$. According to **Lemma 2.3.9** and **Lemma 2.3.6**,

$$ \left( \bigwedge_{i=1}^{n} \varphi_i \right) [f] = \bigwedge_{i=1}^{n} \varphi_i[f] = \bigwedge_{i=1}^{n} a_{\varphi_i}(f_v) = a_{\bigwedge_{i=1}^{n} \varphi_i}(f_v) \le a_{\psi}(f_v) \le \psi[f]. $$

$\square$

Seeing elements of $[0, 1]$ as functions from $[0, 1]^0$ to $[0, 1]$, we can then embed $[0, 1]$ into $USC(\mathcal{L})$.

**Definition 2.3.11.** To each $p \in [0, 1]$, we associate $\underline{p}: [0, 1] \to \mathcal{L}$ . We also recall that, following **Definition 2.3.5**, for all $p \in [0, 1]$, $p$ defines a function $USC(\mathcal{L})^0 \to USC(\mathcal{L})$. $\underline{p} \mapsto p(*)$

**Lemma 2.3.12.** Let $p \in [0, 1]$. We denote by $\underline{p} = p(*)$.

$$ \textbf{Proof.} \text{ For all } q \in [0, 1], p^*(q) = \begin{cases} \emptyset & \text{if } q > p \\ \emptyset & \text{otherwise} \end{cases}, \text{ so } p^*(q) = \begin{cases} \top & \text{if } q > p \\ \bot & \text{otherwise} \end{cases} = \underline{p}(q). \quad \square $$

**Lemma 2.3.13.** $[0, 1] \to USC(\mathcal{L})$ is a $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$-embedding. Moreover, for all $p$ and $q \in [0, 1]$, $\underline{p} \otimes \underline{q} = \underline{p} \vee \underline{q}$.
**Proof.** Let $a \in USC([0, 1]_u^n)$ and $p \in [0, 1]^n$.

$[0, 1] \models a[p] \le a(p)$ and $a[u_1, \dots, u_n]$ is linear, so $USC(\mathcal{L}) \models a[p] \le a(p)$, i.e. $a(p) \le a(p)$.

$[0, 1] \models a(p) \le a[p]$ and $a(p)$ is a constant and thus a linear term, so $USC(\mathcal{L}) \models a(p) \le a[p]$, i.e. $a(p) \le a(p)$. Hence $a(p) = a(p)$.

For all $p, q$ and $r \in [0, 1]$,

$$ \underline{p} \vee \underline{q}(r) = \bigvee_{r'<r} \underline{p}(r') \wedge \underline{q}(r') = \begin{cases} \top & \text{if } p \vee q < r \\ \bot & \text{otherwise} \end{cases} \quad \text{and} \quad \underline{p} \otimes \underline{q}(r) = \underline{p}(r) \otimes \underline{q}(r) = \begin{cases} \top & \text{if } p \vee q < r \\ \bot & \text{otherwise} \end{cases}. \quad \square $$

We shall now state and prove the strong converse of **Theorem 2.3.10**.

**Theorem 2.3.14.** For all terms $\varphi$ and $\psi$ of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$, if $USC(\mathcal{L}) \models \varphi \le \psi$, then $[0, 1] \models \varphi \le \psi$.

**Proof.** Let $\varphi$ and $\psi$ be terms of $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ such that $USC(\mathcal{L}) \models \varphi \le \psi$. Let $p: \mathcal{V} \rightarrow [0, 1]$.

$USC(\mathcal{L}) \models \varphi[p] \le \psi[p]$, so, according to **Lemma 2.3.13**, $USC(\mathcal{L}) \models \underline{a}_{\varphi}(p) \le \underline{a}_{\psi}(p)$. Hence, for all $q \in [0, 1]$, $q > \underline{a}_{\psi}(p) \Rightarrow q > \underline{a}_{\varphi}(p)$ and thus $\underline{a}_{\varphi}(p) \le \underline{a}_{\psi}(p)$, i.e. $[0, 1] \models \varphi[p] \le \psi[p]$. $\square$

### 2.3.2. Reduction to the language $\mathcal{L}_{[0,1]}$.

**Notation 2.3.15.** For all ordered topological spaces $(X, \le)$, let's denote by $C_{\nearrow}(X)$ the set of continuous non-decreasing functions from $X$ to $[0, 1]$, by $C^0(X)$ the set of continuous functions from $X$ to $[0, 1]$ and by $USC_{\searrow}(X)$ the set of non-decreasing upper semi-continuous functions from $X$ to $[0, 1]$.

**Definition 2.3.16.** An ordered topological space $(X, \le)$ is said Hausdorff if $\le$ is closed.

**Lemma 2.3.17.** Let $X$ be an ordered topological space and let's denote by $X_u$ the topological space whose underlying set is $X$ and whose topology is the set of all downward closed open sets of $X$.

$$ USC_{\searrow}(X) = USC(X_u). $$

**Proof.** For all $f \in USC_{\searrow}(X)$, for all $q \in [0, 1]$, $f^{-1}([0, q))$ is a downward closed open of $X$, so $f \in USC(X_u)$.

Let $f \in USC(X_u)$. For all $q \in [0, 1]$, $f^{-1}([0, q))$ is an open of $X$, so $f$ is upper semi-continuous.

Let $x \le y \in X$. For all $q > f(y)$, $y \in f^{-1}([0, q))$, which is downward closed, so $x \in f^{-1}([0, q))$, i.e. $f(x) < q$. Thus $f(x) \le f(y)$.

Hence $f \in USC_{\searrow}(X)$. $\square$

**Lemma 2.3.18 (Ordered version of Urysohn's Lemma, [40, Chapter I, Theorem 1]).** Let $X$ be a compact Hausdorff ordered topological space. For all downward closed subset $F$ and upward closed subset $G$ of $X$ such that $F \cap G = \emptyset$, there exists $f \in C_{\searrow}^0(X)$ such that $f|_F = 0$ and $f|_G = 1$.

**Lemma 2.3.19.** Let $X$ be a compact Hausdorff ordered topological space.

$$ USC_{\searrow}(X) = \{ \bigwedge A, A \subset C_{\searrow}^0(X) \}. $$

**Proof.** $C_{\searrow}^0(X) \subset USC_{\searrow}(X)$ and $USC_{\searrow}(X)$ is stable by lower bounds, so $\{\bigwedge A, A \subset C_{\searrow}^0(X)\} \subset USC_{\searrow}(X)$.

Let $f \in USC_{\searrow}(X)$, $x \in X$ and $q \in [0, 1]$ such that $q > f(x)$. $f^{-1}([q, 1])$ and $\{y \in X | y \le x\}$ are closed, $f^{-1}([q, 1])$ is upward closed, $\{y \in X | y \le x\}$ is downward closed and $f^{-1}([q, 1]) \cap \{x\} = \emptyset$, so, thanks to **Lemma 2.3.18**, there exists $g \in C_{\searrow}^0(X)$ such that $g(x) = 0$ and $g|_{(f^{-1}([q, 1]))} = 1$,

$$ \text{which gives } \underline{q} \dot{=} \underline{g} \ge f \text{ and } (\underline{q} \dot{=} \underline{g})(x) = q. \text{ Hence } f = \bigwedge_{h \in C_{\searrow}^0(X)} h. \quad \square $$
**Theorem 2.3.20.** There exists a unique family of lower-bounds-preserving functions $(\cdot: USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)})_{n \in \mathbb{N} \cup \{0\}}$ that is associative in the sense that, for all

$$a \in USC([0, 1]_u^n), (b_1, \dots, b_n) \in \prod_{i=1}^{n} USC([0, 1]_u^{k_i}) \text{ and } (f_{i,1}, \dots, f_{i,k_i})_{i \in [1,n]} \in USC(\mathcal{L})_{i=1}^{\sum k_i},$$

$$(a \circ (b_1, \dots, b_n)) \cdot (f_{1,1}, \dots, f_{n,k_n}) = a \cdot (b_1 \cdot (f_{1,1}, \dots, f_{1,k_1}), \dots, b_n \cdot (f_{n,1}, \dots, f_{n,k_n}))$$

and, for all $a \in C_{\succ}^0([0, 1]^n)$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = a(f)$.

*Proof.* By defining, for all $a \in USC([0, 1]_u^n)$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = a(f)$, we obtain a family of functions $(\cdot: USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)})_{n \in \mathbb{N} \cup \{0\}}$ satisfying the required properties.

Let now $(\cdot: USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)})_{n \in \mathbb{N} \cup \{0\}}$ be such a family of functions.

According to **Lemma 2.3.19**, since $[0, 1]^n$ is compact and Hausdorff, for all $a \in USC([0, 1]_u^n)$,

$$a = \bigwedge_{\substack{b \in C_{\succ}^0([0,1]^n) \\ b \ge a}} b, \text{ so, for all } f \in USC(\mathcal{L})^n, a \cdot f = \bigwedge_{\substack{b \in C_{\succ}^0([0,1]^n) \\ b \ge a}} (b \cdot f) = \bigwedge_{\substack{b \in C_{\succ}^0([0,1]^n) \\ b \ge a}} b(f) = a(f). \quad \square$$

**Notation 2.3.21.** We recall that, we have defined $j: [0, 1] \to [0, 1]$, that is a non-decreasing $x \mapsto 2(x - \frac{1}{2})$

continuous function and the maximum and minimum of two elements $x$ and $y$ of $[0, 1]$ are respectively denoted $\max(x, y)$ and $\min(x, y)$ (cf. **Definition 2.1.3**).

The interpretation of $(C_{\succ}^0([0, 1]^n))_{n \in \mathbb{N}}$ on $USC(\mathcal{L})$ gives us an interpretation of the language $\mathcal{L}_{[0,1]} = \{\min, \max, +, 2, \frac{1}{2}, j, \underline{0}, \underline{1}\}$ in $USC(\mathcal{L})$. The aim of this subsection is to prove that the action of $(C_{\succ}^0([0, 1]^n))_{n \in \mathbb{N}}$ on $USC(\mathcal{L})$ is entirely characterised by the interpretation of $\mathcal{L}_{[0,1]}$ in $USC(\mathcal{L})$ (**Theorem 2.3.26**). For this, we need a Stone-Weierstrass type theorem and metric on $USC(\mathcal{L})$. Before going any further, we need some calculatory results.

**Lemma 2.3.22.** Let $f$ and $g \in USC(\mathcal{L})$, $q$ and $q' \in [0, 1]$.

(1) $\max(f, g)(q) = f(q) \otimes g(q)$.

(2) $\min(f, g)(q) = f(q) \lor g(q) = (f \land g)(q)$.

(3) $(f \dot{+} g)(q) = \bigvee_{p \dot{+} r < q} f(p) \otimes g(r) = \bigvee_{p < q} f(p) \otimes g(q - p)$ and $\dot{+}$ admits a residual $\div$, defined by

$$(f \div g)(q) = \bigvee_{p < q} \bigwedge_{r \ge p} g(r - p) \dashrightarrow f(r).$$

(4) $(f \dot{+} q')(q) = f(q \div q') = (f \dot{+} q')(q)$.

(5) $(f \div q')(q) = (f \div q')(q) = j\left(\frac{f}{2} \div \frac{1-q'}{2}\right)(q)$.

(6) $(2f)(q) = f(\frac{q}{2})$ and $j_*(f)(q) = f(j(q))$.

*Proof.* Let $f$ and $g \in USC(\mathcal{L})$, $q$ and $q' \in (0, 1]$.

(1)

$$\begin{aligned} \max(f,g)(q) &= \bigvee_{U \times V \subset \max^*(q)} G(f)(U) \otimes G(g)(V) = \bigvee_{\max(p,r)<q} G(f)([0,p)) \otimes G(g)([0,r)) \\ &= \bigvee_{p<qr<q} f(p) \otimes g(r) = f(q) \otimes g(q). \end{aligned}$$
$$
(2) \qquad \begin{aligned}
\min(f,g)(q) &= \bigvee_{U \times V \subseteq \min^*(q)} G(f)(U) \otimes G(g)(V) \\
&= \bigvee_{\substack{U \subseteq [0,q) \\ \text{or } V \subseteq [0,q]}} G(f)(U) \otimes G(g)(V) \quad \text{(since the order on $[0,1]$ is total)} \\
&= \left( \bigvee_{U \subseteq [0,q)} G(f)(U) \otimes G(g)([0,1]) \right) \vee \left( \bigvee_{V \subseteq [0,q)} G(f)([0,1]) \otimes G(g)(V) \right) \\
&= f(q) \vee g(q).
\end{aligned}
$$

$$
(3) \quad (f \dot{\vdash} g)(q) = \bigvee_{U \vdash V \subseteq [0,q)} G(f)(U) \otimes G(g)(V) = \bigvee_{p<q} \bigvee_{r<q \dot{=} p} f(p) \otimes g(r) = \bigvee_{p<q} f(p) \otimes g(q-p).
$$

For all $h \in USC(\mathcal{L})$,

$$
\begin{align*}
f \leq g \dot{+} h &\Leftrightarrow \forall q \in [0,1] f(q) \geq \bigvee_{p \dot{=} r < q} g(p) \otimes h(r) \\
&\Leftrightarrow \forall q, p, r \in [0,1] \text{ s.t. } p \dot{=} r < q f(q) \geq g(p) \otimes h(r) \\
&\Leftrightarrow \forall q, p, r \in [0,1] \text{ s.t. } p \dot{=} r < q g(p) \Leftrightarrow f(q) \geq h(r) \\
&\Leftrightarrow \forall q, r \in [0,1] \bigwedge_{p < q \dot{=} r} g(p) \Leftrightarrow f(q) \geq h(r) \\
&\Leftrightarrow \forall q, r \in [0,1] g(q \dot{=} r) \Leftrightarrow f(q) \geq h(r) \\
&\Leftrightarrow \forall r \in [0,1] \bigwedge_{q \geq r} g(q \dot{=} r) \Leftrightarrow f(q) \geq h(r)
\end{align*}
$$

Thus, according to **Lemma 2.2.7**, since $r \mapsto \bigwedge_{q \ge r} g(q \rhd r) \rhd f(q)$ is non-decreasing, for all $r \in [0,1]$, $\bigvee_{p<r} \bigwedge_{q \ge p} g(q \rhd p) \rhd f(q) \ge h(r)$.

$$
(4) \qquad (f \dot{\vdash} q')(q) = \bigvee_{U \dot{=} q' \subseteq [0,q)} G(f)(U) = \bigvee_{p \dot{=} q' < q} f(p) = f(q \dot{=} q')
$$

(`_\dot{+}q')[v]` and `\dot{+}[v, q']` are two terms of arity one, therefore linear, so,
since `[0,1]` `=` `(`_\dot{+}q')[v]` = `\dot{+}[v, q']`, thanks to **Theorem 2.3.10,**
**USC(\(\mathcal{L}\))** `=` `(`_\dot{+}q')[v]` = `\dot{+}[v, q']` and so `f\dot{+}q'` = `f\dot{+}q'`.

$$
(5) \text{ (`_\dot{+}q')[v], } \text{ `\_\dot{+}[v, q'] and } j\left(\frac{v}{2} + \frac{1-q'}{2}\right) \text{ are three linear terms whose interpretations are equal in } [0,1], \text{ so, thanks to \textbf{Theorem 2.3.10}, } (f \text{ } \text{\_\dot{+}q'})(q) = (f \text{ } \text{\_\dot{+}q'})(q) = j\left(\frac{f}{2} + \frac{1-q'}{2}\right) \text{ (q).} \\
(6)
$$

$$
(2f)(q) = \bigvee_{2U \subseteq [0,q)} G(f)(U) = \bigvee_{2p < q} f(p) = f\left(\frac{q}{2}\right)
$$

and

$$
j_*(f)(q) = \bigvee_{j_*(U) \subseteq [0,q)} G(f)(U) = \bigvee_{j_*(p) < q} f(p) = f(j(q)).
$$

□
**Theorem 2.3.23** (Increasing version of Stone-Weierstrass theorem for lattices). Let $X$ be a compact topological space with at least two points endowed with an order $\leq$ and let $L$ be a sublattice of the lattice of continuous non-decreasing functions from $X$ to $[0, 1]$.

If, for all $y \not\leq x \in X$, $p \leq q \in [0, 1]$ and $\varepsilon > 0$, there exists $f \in L$ such that $|f(x) - p| < \varepsilon$ and $|f(y) - q| < \varepsilon$, then $L$ is dense in $C_{\lambda}^{0}(X)$.

*Proof.* Let $g \in C_{\lambda}^{0}(X)$ and $\varepsilon > 0$. Let $x \in X$.

For all $y \in X$, there exists $f \in L$ such that $|f(x) - g(x)| < \varepsilon$ and $|f(y) - g(y)| < \varepsilon$. Indeed, for all $y \neq x$, the assumption of the theorem gives such a function, and, since there are at least two points in $X$, if we take $y = x$, there exists $x' \neq x$ and the assumpion again gives such a function.

$X$ being compact, there exists $f_1, \dots, f_n \in L$ such that for all $i \in [1, n]$ $|f_i(x) - g(x)| < \varepsilon$ and
$$X = \bigcup_{i=1}^{n} (f_i - g)^{-1}((-\varepsilon, \varepsilon)). \text{ Thus, } \bigvee_{i=1}^{n} f_i(y) > g(y) - \varepsilon \text{ for all } y \in X, \bigvee_{i=1}^{n} f_i(x) < g(x) + \varepsilon \text{ and}$$
$$\bigvee_{i=1}^{n} f_i \in L.$$

This being true for every $x \in X$ and $X$ being compact, there exists $h_1, \dots, h_k \in L$ such that for all $j \in [1, k]$ and $y \in X$ $h_j(y) > g(y) - \varepsilon$ and $X = \bigcup_{j=1}^{k} (h_j - g)^{-1}((-1, \varepsilon))$. Thus, for all $x \in X$

$$\left| \left( \bigwedge_{j=1}^{k} h_j(x) \right) - g(x) \right| < \varepsilon, \text{ and } \bigwedge_{j=1}^{k} h_j \in L. \quad \square$$

We notice here that **Theorem 8.3 of [1]** is a corollary of **Theorem 2.3.23**.

**Corollary 2.3.24.** Let $n \in \mathbb{N}$.

The set $L_n = \{a \in C_{\lambda}^0([0, 1]^n) \mid a \text{ is a composition of max, min, } \dot{+}, 2\cdot, \dot{=}j, \underline{0}, \underline{1} \text{ and the projections}\}$ is dense in $C_{\lambda}^0([0, 1]^n)$.

*Proof.* For $n = 0$, $C_{\lambda}^0([0, 1]^n) = [0, 1]$, and, for all $d \in \mathcal{D}$, there exists $k$ and $m \in \mathbb{N}$ such that $d = \sum_{i=1}^{k} \frac{1}{2^m}$, so $d \in L_0$. Thus $L_0$ is dense in $C_{\lambda}^0([0, 1]^0)$.

Let $n \in \mathbb{N}$. $[0, 1]^n$ has at least two distinct points. Since $L_n$ is stable by max and min, $L_n$ is a lattice.

Let $x \not\leq y \in [0, 1]^n$, $p \leq q \in [0, 1]$ and $\varepsilon > 0$. There exists $i \in [1, n]$ such that $x_i < y_i$, $d_1 \in \mathcal{D} \cap [x_i, y_i)$, $k \in \mathbb{N}$ such that $2^k \geq \frac{1}{y_i - d_1}$, and $d_2$ and $d_3 \in \mathcal{D}$ such that $|d_2 - (q - p)| < \frac{\varepsilon}{2}$ and $|d_3 - p| < \frac{\varepsilon}{2}$.

We define $a: [0, 1]^n \to [0, 1]$

$\mathcal{D} \subset L_0$ and, for all $z \in [0, 1]$ and $d \in \mathcal{D}$, $z \div d = j(\frac{z}{2} + \frac{1-d}{2}) \in L_1$, so $a \in L_n$.

$$|a(x) - p| = |(\min((2^k(x_i \div a_1)), d_2) + d_3) - p| = |d_3 - p| < \frac{\varepsilon}{2} < \varepsilon.$$

$$\begin{aligned} |a(y) - q| &= |(\min((2^k(y_i \div a_1)), d_2) + d_3) - q| = |(d_2 + d_3) - q| \leq |d_2 + d_3 - q| \\ &\leq |(d_2 - (q - p)) + (d_3 - p)| \leq |d_2 - (q - p)| + |d_3 - p| < \varepsilon. \end{aligned}$$

Finally, thanks to **Theorem 2.3.23**, $[0, 1]^n$ being compact, $L_n$ is dense in $C_{\lambda}^0([0, 1]^n)$. $\square$

In order to deal with density, we need a metric on $USC(\mathcal{L})$.

**Lemma 2.3.25.** $[0, 1] \to USC(\mathcal{L})$ admits a left adjoint $\|\cdot\|$. Thus, for all $f \in USC(\mathcal{L})$ and $q \mapsto \underline{q}$
$q \in [0, 1]$, $\|f\| \leq q \Leftrightarrow f \leq \underline{q}$.
$d: \mathbf{USC}(\mathcal{L})^2 \to [0,1]$ defines a metric on $\mathbf{USC}(\mathcal{L})$.
$(f,g) \mapsto \max(\|f \div g\|, \|g \div f\|)$

**Proof.** Indeed, according to **Lemma 2.3.12**, for all $p \in [0,1]$, $\underline{p} = p(*)$ and according to **Lemma 2.3.6**, $[0,1] \to \mathbf{USC}(\mathcal{L})^{(\mathbf{USC}(\mathcal{L})^n)}$ preserves lower bounds, so $p \mapsto \underline{p}$ preserves lower bounds.

$p \mapsto \underline{p}$

Since $[0,1]$ is a complete order, $p \mapsto \underline{p}$ admits a left adjoint.

$d$ is clearly positive and symmetric. For all $f$ and $g \in \mathbf{USC}(\mathcal{L})$, if $d(f,g) = 0$, then $\|f \div g\| = 0$ and $\|g \div f\| = 0$, thus $f \le g$ and $g \le f$, that-is-to-say $f = g$.

Let $f, g$ and $h \in \mathbf{USC}(\mathcal{L})$. $f \le (f \div g) \div (g \div h) \div h$, so $(f \div h) \div (f \div g) \le g \div h$, which implies that $(f \div h) \div (f \div g) \le \|g \div h\|$. Thus $(f \div h) \div \|g \div h\| \le f \div g$, and so $f \div h \le \|f \div g\| \div \|g \div h\| = \|f \div g\| \div \|g \div h\|$. Hence $\|f \div h\| \le \|f \div g\| \div \|g \div h\|$, which is equivalent to $\|f \div h\| \le \|f \div g\| + \|g \div h\|$, since $\|f \div h\| \le 1$. In the same way, $\|h \div f\| \le \|h \div g\| + \|g \div f\|$.

Finally,

$$d(f, h) = \max(\|f \div h\|, \|h \div f\|) \\ \le \max(\|f \div g\| + \|g \div h\|, \|h \div g\| + \|g \div f\|) \\ \le d(f, g) + d(g, h).$$

□

The purpose of the structure on $\mathbf{USC}(\mathcal{L})$ is to obtain the following theorem.

**Theorem 2.3.26.** Let us endow $C^0(\mathbf{USC}(\mathcal{L})^n, \mathbf{USC}(\mathcal{L}))$, $n \in \mathbb{N} \cup \{0\}$, with the metric $d_\infty$ defined by $d_\infty(F, G) = \bigvee_{f \in \mathbf{USC}(\mathcal{L})^n} d(F(f), G(f))$, for all $(F, G) \in C^0(\mathbf{USC}(\mathcal{L})^n, \mathbf{USC}(\mathcal{L}))^2$.

There exists a unique family of continuous functions $(\cdot : C^0([0,1]^n) \to C^0(\mathbf{USC}(\mathcal{L})^n, \mathbf{USC}(\mathcal{L})) \}_{n \in \mathbb{N}}$ that is associative in the sense that, for all $a \in C^0([0,1]^n)$, $(b_1, \dots, b_n) \in \prod_{i=1}^n C^0([0,1]^{k_i})$ and $(f_{i,1}, \dots, f_{i,k_i})_{i \in [1,n]} \in \mathbf{USC}(\mathcal{L})^{\sum_{i=1}^n k_i}$,

$$(a \circ (b_1, \dots, b_n)) \cdot (f_{1,1}, \dots, f_{n,k_n}) = a \cdot (b_1 \cdot (f_{1,1}, \dots, f_{1,k_1}), \dots, b_n \cdot (f_{n,1}, \dots, f_{n,k_n}))$$

such that, for all $f$ and $g \in \mathbf{USC}(\mathcal{L})$:

(1) $\max \cdot (f,g) = f \otimes g$

(2) $\min \cdot (f,g) = f \wedge g$

(3) $\div \cdot (f,g) = f \div g$

(4) $2 \cdot f = 2f$

(5) $\frac{1}{2} \cdot f = \frac{f}{2}$

(6) $j \cdot f = j(f)$

Moreover, $\cdot$ are isometries, and, for every $n \in \mathbb{N}$, $a \in C^0([0,1]^n)$, $f \in \mathbf{USC}(\mathcal{L})^n$, $a \cdot f = a(f)$.

**Remark 2.3.3.** For every sublanguage $L$ of $(C^0([0,1]^n))_{n \in \mathbb{N}}$ containing $\mathcal{L}_{[0,1]}$, such as $\mathcal{L}$, **Theorem 2.3.26** works if one extends the list of axioms (1) to (6) to the symbols of $L$.

As a corollary of **Theorems 2.3.20 and 2.3.26**, we give the following theorem.

**Theorem 2.3.27.** Let us endow, for all $n \in \mathbb{N}$, $\mathbf{USC}([0,1]^n)$ with the supremum metric, and $\mathbf{USC}(\mathcal{L})^{(\mathbf{USC}(\mathcal{L})^n)}$ with the metric $d_\infty$ defined by $d_\infty(F, G) = \bigvee_{f \in \mathbf{USC}(\mathcal{L})^n} d(F(f), G(f))$, for all

$F$ and $G: \mathbf{USC}(\mathcal{L})^n \to \mathbf{USC}(\mathcal{L})$.
$(a, f) \mapsto a(f)$, as defined in 2.3.5, is the unique family of continuous and lower-bound-preserving functions $(\because: USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)})_{n \in \mathbb{N}}$ such that, for all $f$ and $g \in USC(\mathcal{L})$:

$$ (1) \max \cdot (f, g) = f \otimes g $$

$$ (2) \min \cdot (f, g) = f \wedge g $$

$$ (3) \dot{+} \cdot (f, g) = f \dot{+} g $$

$$ (4) 2 \cdot f = 2f $$

$$ (5) \frac{\dot{+}}{2} \cdot f = \frac{f}{2} $$

$$ (6) j \cdot f = j(f) $$

**Remark 2.3.4. Theorems 2.3.26 and 2.3.27** mean that there is a unique structure of module on $USC(\mathcal{L})$ over the operads $(C_{\lambda}^{0,}([0, 1]^n))_{n \in \mathbb{N}}$ and $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$ satisfying points (1) to (6). To prove **Theorems 2.3.26 and 2.3.27**, we use the following lemma.

**Lemma 2.3.28.** For all $n \in \mathbb{N}$, $USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)}$ is an isometry.
$$ a \mapsto a(\_) $$

*Proof.* Let $n \in \mathbb{N}$, $a$ and $b \in USC([0, 1]_u^n)$.

For all $q \in [0, 1]^n$, $a(q) = \underline{a(q)}$ and $b(q) = \underline{b(q)}$, so $d(a(q), b(q)) = d(\underline{a(q)}, \underline{b(q)}) = |a(q) - b(q)|$, and so

$$ \|a - b\|_{\infty} \le d_{\infty}(a \cdot \_, b \cdot \_.) $$

Let $f \in USC(\mathcal{L})^n$. $a \le (a \div b) \dot{+} b$, so $a(f) \le (a \div b)(f) \dot{+} b(f)$, which amounts to $a(f) \div b(f) \le (a \div b)(f)$. However, $f \le \|f\|$, so $(a \div b)(f) \le (a \div b)(\|f\|)$. Hence $d_{\infty}(a \cdot \_, b \cdot \_.) \le \|a - b\|_{\infty}$.

Hence, $a \mapsto a(\_)$ is an isometry. $\square$

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

*Proof of Theorem 2.3.26. Existence part :*

Let, for all $n \in \mathbb{N}$, $a \in C_{\lambda}^{0,}([0, 1]^n)$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = a(f)$. The associativity of $\cdot$ is what **Lemma 2.3.7** states. By virtue of **Lemma 2.3.28**, for all $n \in \mathbb{N}$, $C_{\lambda}^{0,}([0, 1]^n) \to C_{\lambda}^{0,}(USC(\mathcal{L})^n)$ is an isometry. This family of isometries tautologically satisfies axioms (1) to (6).

*Uniqueness part :*

Let now $L$ be a language and $\cdot$ be a family of functions as in **Theorem 2.3.26**. Let $n \in \mathbb{N}$ and $a \in C_{\lambda}^{0,}([0, 1]^n)$.

There exists $(a_k)_k \in \mathbb{N} \in L_n^{\mathbb{N}}$ such that $a_k \to a$. The $a_k$s being compositions of elements of $L$, and $\cdot$ preserving the composition, for all $f \in USC(\mathcal{L})^n$, $a_k \cdot f = a_k(f)$. $\cdot$ being continuous, for all $f \in USC(\mathcal{L})^n$, $(a \cdot f) = \lim a_k \cdot f = \lim a_k(f) = a(f)$. $\square$

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

*Proof of Theorem 2.3.27. Existence :*

By virtue of **Lemma 2.3.28**, for all $n \in \mathbb{N}$, $USC([0, 1]_u^n) \to USC(\mathcal{L})^{(USC(\mathcal{L})^n)}$ is continuous.
$$ a \mapsto a(\_) $$

This family of continuous functions tautologically satisfies axioms (1) to (6).

*Uniqueness :*

Let $\cdot$ be such a family of functions. By **Theorem 2.3.26**, for all $n \in \mathbb{N}$, $a \in C_{\lambda}^{0,}([0, 1]^n)$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = a(f)$. So, by **Theorem 2.3.20**, for all $n \in \mathbb{N}$, $a \in USC([0, 1]_u^n)$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = a(f)$. $\square$

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

**2.4. The Continuous Logic structure on USC(\mathcal{L}).** We remind the reader that the language we are finally interested in is $\mathcal{L} = \{\vee, \wedge, \dot{+}, \div, \dot{=} \_, 2, j_*, j, \alpha, \underline{0}, \underline{1}\}$.

In order to give a systematic way to translate any inequation in the language $\mathcal{L}_{crl}$ and $\mathcal{L}_{[0,1]}$ to an inequation in the language $\mathcal{L}$ such that if the former is universally satisfied by $USC(\mathcal{L})$, so is the latter, we have to replace $\otimes$ and $\to$ in formulas of $\mathcal{L}_{crl}$ (**Theorem 2.4.3**) and compare the interpretation of max from the language $\mathcal{L}_{[0,1]}$ to $\vee$ (**Theorem 2.4.4**).
**Definition 2.4.1.** The interpretation of $\dot{+}$, $2$, $\frac{1}{2}$, $2$, $j_*$, $j$, $\alpha$, $\emptyset$ and $\underline{1}$ is given by the interpretation of $\mathcal{L}$ in $[0, 1]$ (**Definition 2.3.5**). We call every $(\mathrm{USC}(\mathcal{L}), \vee, \wedge, \dot{+}, \div, 2, \frac{1}{2}, j_*, j, \alpha, \emptyset, \underline{1})$, for $\mathcal{L}$ a commutative residuated complete lattice, an Affine Continuous algebra, or AC-algebra.

**Lemma 2.4.2.** Let $f, g \in \mathrm{USC}(\mathcal{L})$ and $U, V \in \mathcal{L}$.
$$2\frac{f}{2} = f \text{ and, for all } q \in [0, 1], 2(g \to f)(q) \le 2g(q) \to 2f(q).$$
$$0_U \dot{+} 0_V = 0_{U \otimes V} \text{ and } 0_U \div 0_V = 0_{V \to U}.$$

*Proof.* For all $q \in (0, 1]$,

$$2\frac{f}{2}(q) = \frac{f}{2}\left(\frac{q}{2}\right) = \bigvee_{\frac{U}{2} \subset [0, \frac{q}{2}]} G(f)(U) = G(f)([0, q]) = f(q)$$

$$2(g \to f)(q) = (g \to f)\left(\frac{q}{2}\right) = \bigvee_{p < \frac{q}{2}} \bigwedge_{r \ge p} g(r) \to f(r) \le g\left(\frac{q}{2}\right) \to f\left(\frac{q}{2}\right) = 2g(q) \to 2f(q)$$

$$0_U \dot{+} 0_V(q) = \bigvee_{p < q} 0_U(p) \otimes 0_V(q - p) = \bigvee_{0 < p < q} 0_U(p) \otimes 0_V(q - p) = U \otimes V = 0_{U \otimes V}(q)$$

$$0_U \div 0_V(q) = \bigvee_{p < qr \ge p} 0_V(r) \to 0_U(r) = \bigvee_{0 < p < qr \ge p} 0_V(r) \to 0_U(r) = V \to U = 0_{V \to U}(q).$$

□

The following theorem is used in the proof of **Theorem 2.4.4**, but also independently of **Theorem 2.4.4**, in the proof of **Corollary 5.2.4**.

**Theorem 2.4.3.** For all $f$ and $g \in \mathrm{USC}(\mathcal{L})$,

$$\frac{f+g}{2} \le f \otimes g \le f \dot{+} g \text{ and } f \div g \le g \to f \le 2(f \div \frac{g}{2}).$$

*Proof.* Let $f$ and $g \in \mathrm{USC}(\mathcal{L})$ and $q \in [0, 1]$. $[0, 1] \models \frac{u+v}{2} \le \max(u, v)$ and $[0, 1] \models \max(u, v) \le u+v$, so, according to **Theorem 2.3.10** and **Lemma 2.3.22**, $\frac{f+g}{2} \le f \otimes g \le f \div g$.

For all $h \in \mathrm{USC}(\mathcal{L})$, $g \to f \le h \Leftrightarrow f \le g \otimes h \Rightarrow f \le g \dot{+} h \Leftrightarrow (f \div g) \le h$, so $f \div g \le g \to f$, and $f \div g \le h \Leftrightarrow f \le h \div g \Rightarrow f \le 2(h \otimes g) \Leftrightarrow g \to \frac{f}{2} \le h$, so $g \to \frac{f}{2} \le f \div g$. Since it is true for all $f$ and $g \in \mathrm{USC}(\mathcal{L})$, for all $f$ and $g \in \mathrm{USC}(\mathcal{L})$, $2(f \div g) \ge 2\left(g \to \frac{f}{2}\right) \ge 2g \to 2\frac{f}{2} = 2g \to f$. □

**Theorem 2.4.4.** Let $(\varphi_i[v])_{1 \le i \le n}$ and $\psi[v]$ be terms in the language $(\mathcal{L}_{[0,1]} \setminus \{\div\}) \cup \{j, j_*, \alpha\}$ and assume each $\varphi_i$ is linear. Let $\tilde{\varphi}_i$ be the $\mathcal{L}$-terms obtained by replacing every occurrence of $\max$ (resp. min) in $\varphi_i$ by $\vee$ (resp. $\wedge$) and $\bar{\psi}$ be the $\mathcal{L}$-term obtained by replacing every occurrence of $\max$ (resp. min) in $\varphi$ by $\dot{+}$ (resp. $\wedge$).

Then, $\mathrm{USC}(\mathcal{L}) \models \bigwedge_{i=1}^n \tilde{\varphi}_i \le \bar{\psi}$ if and only if $[0, 1] \models \bigwedge_{i=1}^n \varphi_i \le \psi$.

*Proof. Direct sense:* Thanks to **Theorem 2.3.10** and since, for all term $\varphi$ in $\mathcal{L}_{[0,1]}$ the interpretation of $\varphi$ in $\mathrm{USC}(\mathcal{L})$ is non-decreasing in every coordinate, it suffices to show that, for all $f$ and $g \in \mathrm{USC}(\mathcal{L})$, $f \vee g \le \max(f, g)$ and $\max(f, g) \le f \div g$.

Let $f$ and $g \in \mathrm{USC}(\mathcal{L})$ and $q \in [0, 1]$. $\max(f, g)(q) = f(q) \otimes g(q) \le f(q)$ and $\max(f, g)(q) = f(q) \otimes g(q) \le g(q)$, so $\max(f, g)(q) \le f(q) \wedge g(q) = (f \vee g)(q)$. According to **Lemma 2.3.22** and **Theorem 2.4.3**, $\max(f, g) = f \otimes g \le f \div g$.
**Converse sense:** According to **Lemma 2.3.13**, $q \mapsto \underline{q}$ is an $\mathcal{L} \cup \{j_*, \alpha\}$-embedding, so, if $\underline{USC}(\mathcal{L}) \models \bigwedge_{i=1}^n \tilde{\varphi}_i \le \bar{\psi}$, then, for all $p: \mathcal{V} \to [0, 1]$, $\underline{USC}(\mathcal{L}) \models \bigwedge_{i=1}^n \varphi_i[p] \le \underline{\psi}[p]$, so $\bigwedge_{i=1}^n \varphi_i[p] \le \psi[p]$ and thus $[0, 1] \models \bigwedge_{i=1}^n \varphi_i \le \psi$. $\square$

**Remark 2.4.1.** We end this subsection by noticing that, in the case where $\mathcal{L}$ is the topology $\mathcal{T}(X)$ of a topological space $X$, this pointwise structure is the one induced by the $(\vee, \wedge, \oplus, \ominus, 2, \frac{1}{2}, j_0, \underline{1})$-structure of $[0, 1]$ through the isomorphism $\underline{USC}(\mathcal{T}(X)) \cong \underline{USC}(X)$.

### 3. ALGEBRAIC AXIOMATISATION OF AC-ALGEBRAS

**3.1. The three theories.** Let us give an algebraic caracterisation of the $\underline{USC}(\mathcal{L})$ for $\mathcal{L}$ a complete residuated lattice. The language in which we express the axioms is $\mathcal{L}$, that we recall to be $\{\vee, \wedge, \oplus, \ominus, \frac{1}{2}, 2, j_*, j, \alpha, \underline{0}, \underline{1}\}$.

**Notation 3.1.1.** For all dyadic $d \in [0, 1)$, we define $\underline{d}$ as $\sum_{k=1}^{2^nd} \frac{j_*(\underline{0})}{2^{n-1}}$ where $n$ is the smallest non negative integer such that $2^nd \in \mathbb{N}$. Note that $\frac{1}{2} = j_*(\underline{0})$.

Here comes the list of axioms, the truth of which can be deduced from **Theorem 2.3.10** in every algebra of the form $\underline{USC}(\mathcal{L})$.

(1) $(\vee, \wedge, \oplus, \ominus, \underline{0}, \underline{1})$ is a bounded commutative residuated lattice structure:

(1.a) $(A, \vee, \wedge, \underline{0}, \underline{1})$ is a bounded lattice

(1.b) $(A, \oplus, \underline{0})$ is a commutative monoid

(1.c) $\ominus$ is the residual of $\oplus$: $w \le u \oplus v \Leftrightarrow w \ominus v \le u$

(2) croissance 2, $\frac{1}{2}$, $j_*$, $j$ and $\alpha$ non-decreasing.

(3) The adjunctions:

$$ (3.a.1) \quad \frac{2v}{2} \le v \qquad \text{and} \quad (3.a.2) \quad v \le 2\frac{v}{2} $$

$$ (3.b.1) \quad j \circ j_*(v) \le v \qquad \text{and} \quad (3.b.2) \quad v \le j_* \circ j(v) $$

(4) Defining axioms:

$$ (4.a.1) \quad 2(u \oplus v) \le 2u \oplus 2v \qquad \text{and} \quad (4.a.2) \quad 2u \oplus 2v \le 2(u \oplus v) $$

$$ (4.b.1) \quad j_*(2v \oplus u) \le v \oplus j_*(u) \qquad \text{and} \quad (4.b.2) \quad j_*(2v \oplus u) \ge v \oplus j_*(u) $$

$$ (4.c.1) \quad 2v \ge v \qquad \text{and} \quad (4.c.2) \quad j_*(v) \ge v $$

$$ (4.d.1) \quad v \le \alpha(2v \wedge j_*(v)) \qquad \text{and} \quad (4.d.2) \quad \alpha(2v \wedge j_*(v)) \le v $$

$$ (4.e.1) \quad 2\alpha(v) \wedge j_* \circ \alpha(v) \le v \qquad \text{and} \quad (4.e.2) \quad v \le 2\alpha(v) \wedge j_* \circ \alpha(v) $$

$$ (4.f.1) \quad 2j_*(\underline{0}) \ge \underline{1} \qquad \text{and} \quad (4.f.2) \quad 2v \le v \oplus v $$

$$ (4.g) \quad \text{for all } n \in \mathbb{N}^*, \alpha^n \circ j_*(\underline{0}) \oplus \alpha^n \circ j_*(\underline{0}) \le \alpha^{n-1} \circ j_*(\underline{0}) $$

(5) infinitesimals And the algebra of values is $[0, 1]$ up to infinitesimals:

$$ (5.a) \quad \text{for all dyadic number } d \in [0, 1] \text{ and } n \in \mathbb{N}, v \le \underline{d} + \alpha^n(v + \underline{1} - d) $$
$$ (5.b) \text{ for all } n \in \mathbb{N}, \bigwedge_{k=1}^{2^{n+1}-1} \left( 1 - \frac{k}{2^{n+1}} \right) + \alpha^{n+1} \left( v + \frac{k}{2^{n+1}} \right) \le v + \frac{1}{2^n} $$

(6) The two non-algebraic properties:

(6.a) completeness: the partial order is complete

(6.b) Archimedean: the lower bound of the family of $\frac{1}{2^n}$ is 0

We denote by **T** the theory consisting of axioms (1.a) to (5.b).

**Proposition 3.1.2.** For all $f$ and $g \in USC(\mathcal{L})$, $f+g = \bigwedge_{q,p \in [0,1]} \underline{q+p+0_{f(q)}+0_{g(p)}}$. Thus, for all $f \in USC(\mathcal{L})$, $f = \bigwedge_{q \in [0,1]} \underline{q+0_{f(q)}}$.

**Remark 3.1.1.** The equality $f = \bigwedge_{q \in [0,1]} \underline{q+0_{f(q)}}$ is a corollary of the equality $\bar{e}(f) = f^\wedge$ found in [44, p. 4].

*Proof.* For all $r \in [0, 1]$, thanks to Lemmas 2.4.2 and 2.3.13,

$$ \begin{aligned} \left( \bigwedge_{q,p \in [0,1]} \underline{q+p+0_{f(q)}+0_{g(p)}} \right) (r) &= \bigvee_{q,p \in [0,1]} \left( \underline{q+p+0_{f(q)} \otimes g(p)} \right) (r) \\ &= \bigvee_{q,p \in [0,1]} \bigvee_{r'+r''<r} \left( \underline{q+p}(r') \otimes (0_{f(q)} \otimes 0_{g(p)}) (r'') \right) \\ &= \bigvee_{q,p \in [0,1]} \bigvee_{0<r''<r'+r''<r} \bigvee \left( \underline{q+p(r')} \otimes (f(q) \otimes g(p)) \right) \\ &= \bigvee_{q,p \in [0,1]} \bigvee_{0<r''<r'+r''<r} f(q) \otimes g(p) \\ &= \bigvee_{q,p \in [0,1]} q+p<r' \\ &= \bigvee_{p+q<r} f(q) \otimes g(p) \\ &= (f+g)(r) \end{aligned} $$

□

**Lemma 3.1.3.** For every commutative residuated complete lattice $\mathcal{L}$, $USC(\mathcal{L})$ satisfies **T** and (6).

*Proof.* Clearly, $USC(\mathcal{L})$ satisfies axioms (1.c) and (2) and is complete and Archimedean. According to **Theorem 2.4.4**, $USC(\mathcal{L})$ satisfies axioms (1.a), (1.b), and axioms from (3.a.1) to (5.b), since they are satisfied by $[0, 1]$. □

We aim at proving the following theorem:

**Theorem 3.1.4.** Any complete Archimedean model of **T** is isomorphic to an AC-algebra.

For this, we will actually prove that all models of another axiomatisation, simpler but in a non-continuous language, are isomorphic to an AC-algebra, and prove it is a consequence of
the aforementioned theory **T**. This axiomatisation is given in the language $\mathcal{L}_1 = \{\preceq, +, -, 2, \frac{1}{2}, j_*, j, \alpha, \beta, l, l^*, (\underline{d})_d \in [0,1] \text{ dyadic}\}$. To define the new symbols on USC($\mathcal{L}$), we use the following lemma.

**Lemma 3.1.5.** Let $\varphi$ and $\psi: [0,1] \to [0,1]$ such that $\varphi$ is right adjoint to $\psi$. $\varphi \in USC([0,1])$ and, for all $f \in USC(\mathcal{L})$, $\varphi(f) = f \circ \psi$. Moreover, $f \mapsto (f \circ \varphi)^u$ is left adjoint to $\varphi(\_)$. Hence, if $\psi \in USC([0,1])$, for all $f \in USC(\mathcal{L})$, $\psi(f) = (f \circ \varphi)^u$.

Thus we can define $\psi(\_)$ for all $\psi: [0,1] \to [0,1]$ such that $\psi$ admits a right adjoint $\varphi$ by, for all $f \in USC(\mathcal{L})$, $\varphi(f) = (f \circ \varphi)^u$.

**Proof.** For all $x$ and $q \in [0,1]$, $\psi(x) < q \Leftrightarrow x < \varphi(q)$, so $\psi^*(q) = [0, \varphi(q))$. Thus, for all $f \in USC(\mathcal{L})$, $\varphi(f) = f \circ \psi$.

Let $f$ and $g \in USC(\mathcal{L})$.

$$ (f \circ \varphi)^u \le g \Leftrightarrow \begin{aligned}[t] & \forall q \in [0,1] f(\varphi(q)) \ge g(q) \\ & \Leftrightarrow \forall p \text{ and } q \in [0,1] \text{ s.t. } \varphi(q) < p f(p) \ge g(q) \\ & \Leftrightarrow \forall p \text{ and } q \in [0,1] \text{ s.t. } q < \psi(p) f(p) \ge g(q) \\ & \Leftrightarrow \forall p \in [0,1] f(p) \ge g(\psi(p)) \\ & \Leftrightarrow f \le \varphi(g). \end{aligned} $$

If $b \in USC([0,1])$, then, since the adjunction equations $a(b(v)) \ge v$ and $b(a(v)) \le v$ are satisfied by $[0,1]$, by virtue of **Theorem 2.3.10**, they are also satisfied by $USC(\mathcal{L})$ and thus $b(\_)$ is left adjoint to $a(\_)$, so, for all $f \in USC(\mathcal{L})$, $b(f) = (f \circ a)^u$. $\square$

**Remark 3.1.2.** $b(f) \ne f \circ a$ in general.

For all $q \in [0,1]$, let $l(q) = \begin{cases} 1 & \text{if } q=1 \\ 0 & \text{otherwise} \end{cases}$, which admits a left adjoint $l^*$ and let $\beta(q) = \alpha^{-1}(q)$.

**Lemma 3.1.5** enables to endowe each $USC(\mathcal{L})$ with an $\mathcal{L}_1$-structure, by defining $l^*$ and $\beta$ on it.

**Lemma 3.1.6.** For all commutative residuated complete lattice $\mathcal{L}$, $f \in USC(\mathcal{L})$, $l(f) = 0_{f(1)}$.

**Proof.** For all commutative residuated complete lattice $\mathcal{L}$, $f \in USC(\mathcal{L})$ and $q \in [0,1]$,

$$ l(f)(q) = f(l^*(q)) = \bigvee_{p<l^*(q)} f(p) = \bigvee_{l(p)<q} f(p) = 0_{f(1)}(q). $$

$\square$

The intermediate list of axioms, satisfied by every AC-algebra, by virtue of **Theorem 2.3.10**, is the following:

(1) $(\preceq, +, -, \underline{0}, \underline{1})$ is a bounded **preordered** monoid with residuation:

(2) $2, \frac{1}{2}, j_*, j, \alpha, l$ and $l^*$ are non-decreasing.

(3) The adjunctions: (3.a.1) to (3.b.2) and

3.c.1. $v \preceq \alpha \circ \beta(v)$, and 3.c.2. $\beta \circ \alpha(v) \preceq v$

3.d.1. $v \preceq l \circ l^*(v)$ and 3.d.2. $l^* \circ l(v) \preceq v$

(4) Defining axioms:

(a) $2(\underline{d}+l(v)) \simeq 2\underline{d}+l(v)$

(b) $j_*(\underline{d}+l(v)) \simeq j_*(\underline{d})+l(v)$
(c) $\alpha(\underline{d} \dot{+} l(v)) \simeq \alpha(d) \dot{+} l(v)$

(d) $l(\underline{d} \dot{+} l(v)) \simeq l(d) \dot{+} l(v)$

(e) $\underline{d} \dot{+} \underline{d}' \simeq \underline{d} \dot{+} \underline{d}'$

(5) + stabilizes the fixed points of l:

5.d. $l(l(u) \dot{+} l(v)) \simeq l(u) \dot{+} l(v)$

(6) And the algebra of values is $[0, 1]$ to infinitesimals:

6.c. for all dyadic number $d \in [0, 1]$, $v \le \underline{d} \dot{+} l(v \dot{+} \underline{1-d})$

6.d. for all $n \in \mathbb{N}$, $\bigwedge_{k=1}^{2^{n+1}-1} \left(1 - \frac{k-1}{2^{n+1}}\right) \dot{+} l\left(v \dot{+} \frac{k-1}{2^{n+1}}\right) \le v \dot{+} \frac{1}{2^n}$

(7) The two non-algebraic properties:

7.c completeness: there exists $\Lambda: \{E \subset A\} \to A$ such that, for all $E \subset A$ and $b \in A$, $\Lambda E \simeq b \Leftrightarrow \forall a \in E a \simeq b$

7.d Archimedean: for all $n \in \mathbb{N}$, $a \le \frac{1}{2^n} \Rightarrow a \le 0$

We denote by $\mathbf{T}_1$ the set of axioms (1) to (6), $\mathcal{L}_0$ the language $\{\leq, \dot{+}, \dot{-}, l, l^*, (d)_d \in [0,1] \text{ dyadic}\}$ and $\mathbf{T}_0$ the set of axioms of $\mathbf{T}_1$ that are formulas of $\mathcal{L}_0$, i.e. in which $2, \frac{1}{2}, j_*, j, \alpha$ and $\beta$ do not appear.

## 3.2. Complete Archimedean models of $\mathbf{T}_0$ and $\mathbf{T}_1$.

### 3.2.1. Complete Archimedean models of $\mathbf{T}_0$. We prove here that any complete Archimedean model of $\mathbf{T}_0$ is isomorphic to an AC-algebra (Theorem 3.2.2). In the following two subsections, we prove that any complete model of $\mathbf{T}$ can be edowed with a preorder that makes it an Archimedean model of $\mathbf{T}_0$. It is thus $\mathcal{L}_0$-isomorphic to an AC-algebra and we also prove that the extra structure is preserved by the isomorphism. Then, we will deal with non complete non Archimedean models of $\mathbf{T}$.

Let $A$ be a complete Archimedean model of $\mathbf{T}_0$. Let us denote by $\mathcal{D}$ the set of all the dyadic numbers in $[0, 1]$.

**Lemma 3.2.1.** For all $(d_i)_{i \in I} \in \mathcal{D}^I$ such that $\bigwedge_{i \in I} d_i \in \mathcal{D}$ and $a \in A$,

$$a \le \bigwedge_{i \in I} d_i \Leftrightarrow \forall i \in I \ a \le \underline{d_i}.$$

*Proof.* Let $(d_i)_{i \in I} \in \mathcal{D}^I$ such that $\bigwedge_{i \in I} d_i \in \mathcal{D}$ and $a \in A$. If for all $i \in I$ $d_i = 1$, then

$$\bigwedge_{i \in I} \underline{d_i} = \underline{1}, \text{ so } \bigwedge_{i \in I} d_i = \bigwedge_{i \in I} \underline{d_i}.$$

Otherwise, we can assume that, for all $i \in I$, $d_i < 1$. Since for all $i_0 \in I$, $\bigwedge_{i \in I} d_i \le d_{i_0}$, if $a \le \bigwedge_{i \in I} d_i$, then $a \le \underline{d_{i_0}}$.

Conversely, assume that, for all $i \in I$, $a \le \underline{d_i}$ and let $n \in \mathbb{N}$.
$$ (\bigwedge_{i \in I} d_i) \dot{+} \frac{1}{2^n} > (\bigwedge_{i \in I} d_i), \text{ so there exists } i_0 \in I \text{ such that } (\bigwedge_{i \in I} d_i) \dot{+} \frac{1}{2^n} > d_{i_0}. \text{ Thus, since } \\ (\bigwedge_{i \in I} d_i) \dot{+} \frac{1}{2^n} \in \mathcal{D}, a \preceq \underline{d_{i_0}} \preceq \overline{(\bigwedge_{i \in I} d_i) \dot{+} \frac{1}{2^n}} \simeq \overline{(\bigwedge_{i \in I} d_i) \dot{+} \frac{1}{2^n}}. \text{ Thus, since } A \text{ is Archimedean, } \\ a \preceq \underline{(\bigwedge_{i \in I} d_i)}. \quad \square $$

Since $[0, 1]$ is generated by lower bounds of elements of $\mathcal{D}$, there is a unique lower bounds-preserving extension of $\underline{=}^{}$ to $[0, 1]$, that we still denote $\underline{=}^{}$.

**Theorem 3.2.2.** The quotient of every complete Archimedean model of $T_0$ by the equivalence relation induced by its preorder is isomorphic to a USC($\mathcal{L}$) for some commutative residuated complete lattice $\mathcal{L}$.

*Proof.* First, define $\mathcal{L}(A) = \{e \in A | l(e) \simeq e\} / \simeq$, endowe it with the quotient order and the canonical surjection $\pi: \{e \in A | l(e) \simeq e\} \to \mathcal{L}(A)$ and call $\mathcal{L}(A)^{op}$ the set $\mathcal{L}(A)$ with the reversed order.

**Lemma 3.2.3.** (1) $\mathcal{L}(A)$ is complete and $\pi$ preserves lower bounds and thus admits a left adjoint, which is $\pi^*: \mathcal{L}(A) \to \{e \in A | l(e) \simeq e\}$. 
$$ U \mapsto \bigwedge \{e \in A | l(e) \simeq e \text{ and } U \le \pi(e)\} $$
Moreover $\pi \circ \pi^* = \mathrm{id}_{\mathcal{L}(A)}$ and $\pi^* \circ \pi \simeq \mathrm{id}_{\{e \in A | l(e) \simeq e\}}$.

(2) $\oplus$ induces a commutative and associative operation $\otimes$ on $\mathcal{L}(A)$ that admits a residual.

*Proof.* (1) Let $U \in \mathcal{L}$ and $(e_i)_i \in I \in \{e \in A | l(e) \simeq e\}^I$. There exists $e \in A$ such that $l(e) \simeq e$ and $\pi(e) = U$.

$\forall i \in I \ U \le \pi(e_i) \Leftrightarrow \forall i \in I \ e \le e_i \Leftrightarrow e \le \bigwedge_{i \in I} e_i \Leftrightarrow U \le \pi\left(\bigwedge_{i \in I} e_i\right)$. Hence, the lower bound of $(\pi(e_i))_{i \in I}$ is $\pi\left(\bigwedge_{i \in I} \pi(e_i)\right)$. Thus $\mathcal{L}(A)$ is complete and, for all $U \in \mathcal{L}$,

$$ \pi \circ \pi^*(U) = \bigwedge_{\substack{e \in A \\ l(e) \simeq e \text{ and } U \le \pi(e)}} \pi(e) = \bigwedge_{\substack{e \in A \\ l(e) \simeq e \text{ and } U=\pi(e)}} \pi(e) = U, $$

and, for all $e \in A$, $\pi^* \circ \pi(e) \simeq e$, because $\pi(\pi^* \circ \pi(e)) = \pi(e)$.

(2) For all $e$ and $e' \in A$ such that $l(e) = e$ and $l(e') = e'$, by 5.d., $l(e+e') = l(l(e)+l(e')) = l(e)+l(e') = e+e'$.

Since $+$ is non-decreasing, it induces an operation $\otimes: \mathcal{L}(A) \times \mathcal{L}(A) \to \mathcal{L}(A)$.

Clearly, $\otimes$ is commutative and associative and admits $\pi(\mathcal{D})$ as neutral element.

For all $(e_i)_i \in I \in A^I$ such that for all $i \in I$ $l(e_i) = e_i$ and $e \in A$ such that $l(e) = e$, 
$$ (\bigwedge_{i \in I} \pi(e_i)) \otimes \pi(e) = \pi\left(\left(\bigwedge_{i \in I} e_i\right) + e\right) = \pi\left(\bigwedge_{i \in I} (e_i+e)\right) = \bigwedge_{i \in I} \pi(e_i+e) = \bigwedge_{i \in I} (\pi(e_i) \otimes \pi(e)). $$

Thus $\otimes$ admits a residual.

$\square$

Then, we define $i: A \to \mathcal{L}(A)^{[0,1]_i}$ and $k: \mathrm{USC}(\mathcal{L}(A)^{op}) \to A$. 
$$ a \mapsto (q \mapsto \bigwedge_{\substack{d \in \mathcal{D} \\ d < q}} \pi \circ l(a + \underline{1-d})) \qquad f \mapsto \bigwedge_{d \in \mathcal{D}} \underline{d} + \pi^*(f(d)) $$

We prove, in order, the following statements.

(1) The image of $i$ is a subset of $\mathrm{USC}(\mathcal{L}(A)^{op})$, and we still call $i$ the induced map, and, for all $a \in A$ and $d \in \mathcal{D}$, $i(a)(d) = \pi \circ l(a + \underline{1-d})$.
(2) $k \circ i \simeq \mathrm{id}_A$.

(3) $i \circ k = \mathrm{id}_{\mathrm{USC}(\mathcal{L}(A)^{op})}$.

(4) $i$ and $k$ are non-decreasing.

(5) As soon as $i$ preserves $+$, $i$ preserves $\cdot$. As soon as $i$ preserves $l$, $i$ preserves $l^*$.

(6) $i$ preserves $+$, $l$ and the $\underline{d}$'s for $d \in \mathcal{D}$.

(1) For all $(q_i)_{i \in I} \in [0, 1]^I$ and $a \in A$,

$$ 
\begin{aligned}
i(a) \left( \bigvee_{i \in I} q_i \right) &= \bigwedge_{\substack{d \in \mathcal{D} \\ d < \bigvee_{i \in I} q_i}} \pi \circ l \left( a \dot{+} \frac{1-d}{d} \right) \\
&= \bigwedge_{(*) \substack{d \in \mathcal{D} \\ \exists i \in I \text{ s.t. } d < q_i}} \pi \circ l \left( a \dot{+} \frac{1-d}{d} \right) \\
&= \bigwedge_{i \in I} \bigwedge_{d \le q_i} \pi \circ l \left( a \dot{+} \frac{1-d}{d} \right) \\
&= \bigwedge_{i \in I} i(a)(q_i),
\end{aligned}
$$

(*) being a consequence of **Lemma 3.2.1**.

Hence, according to **Theorem 2.2.3**, $i(a) \in \mathrm{USC}(\mathcal{L}(A)^{op})$ for all $a \in A$.

Let $a \in A$ and $d \in \mathcal{D}$. Since $\pi$, $l$ and $+$ preserve lower bounds,

$$ 
\begin{aligned}
i(a)(d) &= \bigwedge_{\substack{d' \in \mathcal{D} \\ d' < d}} \pi \circ l \left( a \dot{+} \frac{1-d'}{d} \right) \\
&= \pi \circ l \left( \bigwedge_{\substack{d' \in \mathcal{D} \\ d' < d}} \left( a \dot{+} \frac{1-d'}{d'} \right) \right) \\
&= \pi \circ l \left( a \dot{+} \bigwedge_{\substack{d' \in \mathcal{D} \\ d' < d}} (1-d') \right) \\
&= \pi \circ l \left( a \dot{+} \frac{1-d}{d} \right).
\end{aligned}
$$

(2) By (6), for all $a \in A$ and $d \in \mathcal{D}$, $a \le \underline{d} + l(a + \frac{1-d}{d})$, i.e. $a \le \bigwedge_{d \in \mathcal{D}} \underline{d} + l(a + \frac{1-d}{d}) \simeq k \circ i(a)$, and, for all $n \in \mathbb{N}$, $a + \frac{1}{2^n} \simeq \bigwedge_{k=1}^{2^{n+1}-1} \frac{1 - \frac{k-1}{2^{n+1}}}{\underline{d} + l(v + \frac{k-1}{2^{n+1}})} \simeq \bigwedge_{d \in \mathcal{D}} \underline{d} + l(a + \frac{1-d}{d}) \simeq k \circ i(a)$, so, since $A$ is Archimedean, $a \simeq k \circ i(a)$.

(3) Let $f \in \mathrm{USC}(\mathcal{L}(A)^{op})$. For all $d \in [0, 1]$,
$$
\begin{align*}
l(k(f)\dot{+}\frac{1-d}{d}) &= l\left(\left(\bigwedge_{d' \in \mathcal{D}} \frac{d'}{d'}\dot{+}\pi^*(f(d'))\right)\dot{+}\frac{1-d}{d}\right) \\
&\stackrel{\text{3.d.1. and 3.d.2.}}{\approx} \bigwedge_{d' \in \mathcal{D}} l\left(\pi^*(f(d'))\dot{+}\frac{(1-d+d')\wedge 1}{d}\right) \\
&\stackrel{(4)d \text{ and } (4)e}{\approx} \bigwedge_{d' \in [0,1]} l\left(\pi^*(f(d'))\dot{+}\frac{l((1-d+d')\wedge 1)}{d}\right) \\
&= \bigwedge_{d' \in \mathcal{D}} \pi^*(f(d')),
\end{align*}
$$

so, thanks to **Lemma 3.2.3,**

$$
i(k(f))(d) = \pi \left( \bigwedge_{d' \in \mathcal{D}} \pi^*(f(d')) \right) = \bigwedge_{d' \in \mathcal{D}} \pi \circ \pi^*(f(d')) = \bigwedge_{d' \in \mathcal{D}} f(d') = f(d).
$$

(4) For all $a \le b \in A$ and all $d \in \mathcal{D}$, $i(a)(d) = \pi \circ l(a\dot{+}\frac{1-d}{d}) \le \pi \circ l(b\dot{+}\frac{1-d}{d}) = i(b)(d)$, and so $i(a) \le i(b)$.

For all $f \le g \in USC(\mathcal{L}(A)^{op})$, $k(f) = \bigwedge_{d \in \mathcal{D}} \frac{d}{d} \dot{+} \pi^*(f(d)) \preceq \bigwedge_{d \in \mathcal{D}} \frac{d}{d} \dot{+} \pi^*(g(d)) = k(g)$.

(5) Assume that $i$ preserves $\dot{+}$.

Then, for all $a$ and $b \in A$, and $f \in USC(\mathcal{L}(A)^{op})$,

$$
\begin{align*}
i(a) \div i(b) \le f &\Leftrightarrow i(a) \le i(b) + i \circ k(f) \\
&\Leftrightarrow i(a) \le i(b + k(f)) \\
&\Leftrightarrow a \le b + k(f) \\
&\Leftrightarrow a \div b \le k(f) \\
&\Leftrightarrow i(a \div b) \le f.
\end{align*}
$$

Assume that $i$ preserves $l$.

Then, for all $a$ and $b \in A$, and $f \in USC(\mathcal{L}(A)^{op})$,

$$
\begin{align*}
l^*(i(a)) \le f &\Leftrightarrow i(a) \le l(i(f)) \\
&\Leftrightarrow i(a) \le i(l(f)) \\
&\Leftrightarrow a \le l(f) \\
&\Leftrightarrow l^*(a) \le k(f) \\
&\Leftrightarrow i(l^*(a)) \le f.
\end{align*}
$$

(6) For all $d$ and $d' \in \mathcal{D}$,

$$
\begin{align*}
i(\underline{d})(d') &= \pi \circ l(\underline{d} \dot{+} 1 - d') \\
&= \pi \circ l\left(\frac{(1+d-d')\wedge 1}{d}\right) \\
&= \pi \circ l\left(\frac{(1+d-d')\wedge 1}{d}\right) \\
&= \begin{cases} \pi(1) & \text{if } d \ge d' \\ \pi(0) & \text{otherwise} \end{cases} \\
&= \underline{d}(d').
\end{align*}
$$
For all $a \in A$ and $d \in \mathcal{D}$,

$$i(l(a))(d) = l(l(a)\dot{+}\underline{1-d}) = l^2(a)\dot{+}\underline{l(1-d)} = l(a)\dot{+}\underline{1\ \div\ l^*(d)} = i(a)(l^*(d)) = l(i(a))(d).$$

For all $a$ and $b \in A$,

$$ 
\begin{align*}
a \dot{+} b &\approx \left( \bigwedge_{q \in \mathcal{D}} \underline{q} \dot{+} l(a \dot{+} \underline{1-q}) \right) \dot{+} \left( \bigwedge_{p \in \mathcal{D}} \underline{p} \dot{+} l(b \dot{+} \underline{1-p}) \right) \quad \text{by 3.2.3 (1)} \\
&\approx \bigwedge_{q,p \in \mathcal{D}} \underline{q} \dot{+} \underline{p} \dot{+} l(a \dot{+} \underline{1-q}) \dot{+} l(b \dot{+} \underline{1-p}) \quad \text{(1.c) and (4)e} \\
&\approx \bigwedge_{p,q \in \mathcal{D}} \underline{q} \dot{+} \underline{p} \dot{+} \pi^*(i(a)(q)) \dot{+} \pi^*(i(b)(p)) \quad \text{by definition of $i$} \\
&\approx \bigwedge_{p,q \in \mathcal{D}} \underline{q} \dot{+} \underline{p} \dot{+} \pi^*(i(a)(q) \otimes i(b)(p)) \quad \text{by 3.2.3 (2)} \\
&\approx \bigwedge_{p,q \in \mathcal{D}} \bigwedge_{r>p+q} \left( \underline{r} \dot{+} \pi^*(i(a)(q) \otimes i(b)(p)) \right) \\
&\approx \bigwedge_{r \in \mathcal{D}} \underline{r} \dot{+} \pi^* \left( \bigwedge_{p+q<r} \left( i(a)(q) \otimes i(b)(p) \right) \right) \quad \text{by (1.c)} \\
&\approx \bigwedge_{r \in \mathcal{D}} \underline{r} \dot{+} \pi^* \left( (i(a)\dot{+}i(b))(r) \right) \\
&\approx k(i(a)\dot{+}i(b))
\end{align*}
$$

$$\text{so } i(a \dot{+} b) = i(a) \dot{+} i(b).$$

□

**3.2.2.** *From $\mathbf{T}_0$ to $\mathbf{T}_1$. Now that we have proven any complete Archimedean model of $\mathbf{T}_0$ to be isomorphic to an AC-algebra, we prove that the extra structure of $\mathbf{T}_1$, which contains the extra structure of $\mathbf{T}$, is preserved by the isomorphisms between models of $\mathbf{T}_0$ and AC-algebras, and therefore that every complete Archimedean model of $\mathbf{T}_1$ is isomorphic to an AC-algebra (Corollary 3.2.8). Then, we will deal with non complete non Archimedean models of $\mathbf{T}$. Let $A$ be a complete*

Archimedean model of $\mathbf{T}_0$.

**Lemma 3.2.4.** *For all $\varphi$ and $\psi: [0,1] \to [0,1]$ such that $\varphi$ is right adjoint to $\psi$, for all $a \in A$,*

$$\bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a \dot{+} \underline{1-\psi(d)}) \approx \bigwedge_{d \in \mathcal{D}} \underline{\varphi(d)} \dot{+} l(a \dot{+} \underline{1-d}).$$

*Proof.* For all $a \in A$ and $d \in \mathcal{D}$, $d \ge \varphi(\psi(d))$, so $\underline{d} \dot{+} l(a \dot{+} \underline{1-\psi(d)}) \ge \underline{\varphi(\psi(d))} \dot{+} l(a \dot{+} \underline{1-\psi(d)})$ and $d \le \psi(\varphi(d))$, so $\underline{\varphi(d)} \dot{+} l(a \dot{+} \underline{1-d}) \ge l\varphi(d) \dot{+} l(a \dot{+} \underline{1-\psi(\varphi(d))})$. □

**Proposition 3.2.5.** *Let $\varphi$ and $\psi$ be two new function symbols of arity 1, $a_\varphi$ and $a_\psi$ be their interpretations in $[0,1]$ and define the following axioms*

(1) $\varphi$ and $\psi$ are non-decreasing

(2) $\psi \circ \varphi(v) \le v$

(3) $v \le \varphi \circ \psi(v)$
$$ (4) \quad \varphi(\underline{d} \dot{+} l(v)) \simeq \underline{a}_{\varphi}(d) \dot{+} l(a), \text{ d a dyadic in } [0, 1] $$

Assume 1, 2 and 3 are satisfied by $([0, 1], a_\varphi, a_\psi)$ (notice that 4 is satisfied by $[0, 1]$).
For every $\varphi_A: A \to A$, the following two statements are equivalent:

(1) there exists $\psi_A: A \to A$ such that $(A, \varphi_A, \psi_A)$ satisfies 1, 2, 3 and 4

(2) for all $a \in A$, $\varphi_A(a) \simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a \dot{+} 1 - a_\psi(d))$.

In this case, for all $a \in A$, $\psi_A(a) \simeq \bigwedge \{b \in A | a \preceq \varphi_A(b)\}$.

**Proof.** Assume that, for all $a \in A$, $\varphi_A(a) \simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a \dot{+} 1 - a_\psi(d))$. Then, for all $(a_i)_i \in I \in A^I$, $\varphi_A(\bigwedge_{i \in I} a_i) \simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(\bigwedge_{i \in I} a_i \dot{+} 1 - a_\psi(d)) \simeq \bigwedge_{i \in I} \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a_i \dot{+} 1 - a_\psi(d)) \simeq \bigwedge_{i \in I} \varphi_A(a_i)$. Let $\psi_A$ be defined as in **Proposition 3.2.5**. For all $a$ and $b \in A$, if $\varphi_A(b) \succeq a$, then $b \succeq \psi_A(a)$. Let now $a$ and $b \in A$ such that $\psi_A(a) \preceq b$. $\varphi_A(b) \succeq \varphi_A(\psi_A(a)) = \bigwedge \{\varphi_A(c), c \in A \text{ s.t. } a \preceq \varphi_A(c)\} \succeq a$. Thus $\varphi_A$ admits $\psi_A$ a left adjoint, i.e. $(A, \varphi_A, \psi_A)$ satisfies 1, 2 and 3. Finally, by (4)d and (4)e, for all $a \in A$ and $q \in [0, 1]$,

$$ \begin{aligned} \varphi_A(\underline{q} \dot{+} l(a)) &\simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(\underline{q} \dot{+} l(a) \dot{+} 1 - a_\psi(d)) \simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(l(a) \dot{+} 1 - (a_\psi(d) \div q)) \\ &\simeq \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a) \dot{+} l(1 - (a_\psi(d) \div q)) \simeq \bigwedge_{d \succeq a_\varphi(q) \text{ dyadic}} \underline{d} \dot{+} l(a) \simeq \underline{a}_\varphi(q) \dot{+} l(a). \end{aligned} $$

Hence $(A, \varphi_A, \psi_A)$ satisfies 4.

Assume now that there exists $\psi_A: A \to A$ such that $(A, \varphi_A, \psi_A)$ satisfies 1, 2, 3 and 4. Then, $\varphi_A$ preserves lower bounds up to $\simeq$, so, using **Lemma 3.2.4**, for all $a \in A$,

$$ \varphi_A(a) \underset{3.2.3(1)}{\simeq} \bigwedge_{d \in \mathcal{D}} \varphi_A(\underline{d} \dot{+} l(a \dot{+} 1 - d)) \underset{4}{\simeq} \bigwedge_{d \in \mathcal{D}} \varphi(d) \dot{+} l(a \dot{+} 1 - d) \underset{d \in \mathcal{D}}{\simeq} \bigwedge \underline{d} \dot{+} l(a \dot{+} 1 - \psi(d)). $$

□

**Lemma 3.2.6.** For all $\varphi$ and $\psi: [0, 1] \to [0, 1]$ such that $\varphi$ is right adjoint to $\psi$, for all commutative residuated complete lattice $\mathcal{L}$, 1, 2, 3 and 4 are satisfied by $(\mathrm{USC}(\mathcal{L}), \varphi, \psi)$, where $\varphi$ and $\psi$ are defined on $\mathrm{USC}(\mathcal{L})$ as in **Lemma 3.1.5**.

**Proof.** Let $a$ and $b: [0, 1] \to [0, 1]$ such that $a$ is right adjoint to $b$, and let $\mathcal{L}$ be a commutative residuated complete lattice. **Lemma 3.1.5** already proved 1, 2 and 3.

For all $f \in \mathrm{USC}(\mathcal{L})$, $d \in \mathcal{D}$ and $q \in [0, 1]$, according to **Lemmas 2.3.22 and 3.1.6**,

$$ \begin{aligned} \varphi(\underline{d} \dot{+} l(f))(q) &= (\underline{d} \dot{+} 0_{f(1)})(\psi(q)) \\ &= 0_{f(1)}(\psi(q) \div d) \\ &= 0_{f(1)}(q \div \varphi(d)) \\ &= (\varphi(d) \dot{+} l(f))(q). \end{aligned} $$

□

Thus, for any complete Archimedean model $A$ of $\mathrm{T}_0$ and $\varphi: [0, 1] \to [0, 1]$ admitting a left adjoint $\psi$, let's define $\varphi_A: A \to A$ and $\varphi_A: A \to A$.
$$ a \mapsto \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a \dot{+} 1 - \psi(d)) \qquad a \mapsto \bigwedge \{b \in A | a \preceq \varphi_A(b)\} $$
**Theorem 3.2.7.** Let $\varphi: [0, 1] \to [0, 1]$ such that $\varphi$ admits a left adjoint $\psi$. Let $A$ be complete Archimedean model of $T_0$ and $\mathcal{L}$ be the commutative residuated complete lattice associated to $A$ by **Theorem 3.2.2**. For every $\Phi: A \to A$, the following two statements are equivalent :

(1) the quotient of $(A, \Phi)$ by $\simeq$ is isomorphic to $(USC(\mathcal{L}), \varphi_{USC(\mathcal{L})})$

(2) $\Phi \simeq \varphi_A$.

In this case, the isomorphism also preserves $\psi$.

*Proof.* Assume first that $\Phi \simeq \varphi_A$.

Let $i$ and $k$ be as in the proof of **Theorem 3.2.2**. Let us also denote by $\bar{\varphi}$ and $\bar{\psi}$ the respective interpretations of $\varphi$ and $\psi$ in $USC(\mathcal{L}(A)^{op})$. For all $a \in A$,

$$k(\bar{\varphi}(i(a))) = \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} \pi^*(\bar{\varphi}(i(a))(d)) = \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} \pi^*(i(a)(\psi(d))) = \bigwedge_{d \in \mathcal{D}} \underline{d} \dot{+} l(a \dot{+} 1 - \psi(d)) \\ = \bigwedge_{d \in \mathcal{D}} \varphi(d) \dot{+} l(a \dot{+} 1 - d) = \varphi_A(a) \simeq \Phi(a),$$

so $i(\Phi(a)) = \bar{\varphi}(i(a))$.

Conversely, if the quotient of $(A, \Phi) \simeq$ is isomorphic to $(USC(\mathcal{L}), \varphi_{USC(\mathcal{L})})$, then the isomorphism preserves the lower bounds, so, by **Lemma 3.1.6**, it suffices to prove that, for every commutative residuated complete lattice $\mathcal{L}$ and $f \in USC(\mathcal{L})$, $\bar{\varphi}(f) = \bigwedge_{q \in [0,1]} \underline{q} \dot{+} 0_{f(\psi(q))}$. Let thus $\mathcal{L}$ be a

commutative residuated complete lattice and $f \in USC(\mathcal{L})$.

For all $p \in [0, 1]$,

$$(\bigwedge_{q \in [0,1]} \underline{q} \dot{+} 0_{f(q)}) (p) = \bigvee_{q \in [0,1]} \bigvee_{r<p} \underline{q}(r) \otimes 0_{f(q)}(p-r) = \bigvee_{q<r<p} 0_{f(q)}(p-r) = \bigvee_{q<p} f(q) = f(p).$$

Applying this to $\bar{\varphi}(f) = f \circ \psi$ gives $\bar{\varphi}(f) = \bigwedge_{q \in [0,1]} \underline{q} \dot{+} 0_{f(\psi(q))}$.

Assume now that the quotient of $(A, \Phi)$ by $\simeq$ is isomorphic to $(USC(\mathcal{L}), \bar{\varphi})$ and write $i$ the composition of such an isomorphism with the quotient map.

For all $a \in A$ and $f \in USC(\mathcal{L})$, there exists $b \in A$ such that $f = i(b)$ and thus,

$$\begin{align*} i(\psi_A(a)) &\le f &\Leftrightarrow i(\psi_A(a)) &\le i(b) \\ &\Leftrightarrow \psi_A(a) &\le b \\ &\Leftrightarrow a &\le \varphi_A(b) \\ &\Leftrightarrow i(a) &\le i(\varphi_A(b)) \\ &\Leftrightarrow i(a) &\le \bar{\varphi}(i(b)) \\ &\Leftrightarrow \bar{\psi}(i(a)) &\le f. \end{align*}$$

□

**Corollary 3.2.8.** For every complete Archimedean model $A$ of $T_1$, there exists $\mathcal{L}$ a commutative residuated complete lattice such that $A$ is isomorphic to $USC(\mathcal{L})$.

*Proof.* Let $A$ by a complete Archimedean model of $T_1$. It is a complete Archimedean model of $T_0$, so, according to **Theorem 3.2.2**, there exists $\mathcal{L}$ a commutative residuated complete lattice and $i: A \to USC(\mathcal{L})$ a surjective morphism such that, for all $a$ and $b \in A$, $a \preceq b \Leftrightarrow i(a) \le i(b)$. Since the interpretations of $(USC(\mathcal{L}), 2, \frac{1}{2})$, $(USC(\mathcal{L}), j_*, j)$, $(USC(\mathcal{L}), \alpha, \beta)$ and $(USC(\mathcal{L}), l, l^*)$
satisfies points 1 to 4 of **Proposition 3.2.5**, $2 \cdot = (2 \cdot)_A$, $j_* = j_{*A}$, $\alpha = \alpha_A$ and $l = l_A$. Hence, according to **Theorem 3.2.7**, $i$ preserves $2$, $j_*$, $\alpha$, $l$ and their left adjoints $\frac{1}{2}$, $j$, $\beta$ and $l^*$.

□

### 3.3. Models of $\mathbf{T}$.

**3.3.1. Complete models of $\mathbf{T}$**. Now that we have proven any complete Archimedean model of $\mathbf{T}_1$ to be isomorphic to an AC-algebra, we prove that any complete model of $\mathbf{T}$ can be endowed with a preorder that makes it a complete Archimedean model of $\mathbf{T}_1$. Therefore its quotient by the equivalence relation induced by the preorder is isomorphic to an AC-algebra (**Theorem 3.3.1**). Then, we will deal with non complete non Archimedean models of $\mathbf{T}$. In this section, we prove the following theorem.

**Theorem 3.3.1.** For all complete model $A$ of $\mathbf{T}$, there exists a commutative residuated complete lattice $\mathcal{L}$ such that $A/\simeq$ is isomorphic to $\mathrm{USC}(\mathcal{L})$.

Let us now assume $A$ to be a complete model of $\mathbf{T}$.

**Notation 3.3.2.** Define $\preceq$ on $A$ by: for all $a$ and $b \in A$, $a \preceq b \Leftrightarrow \forall n \in \mathbb{N} \ a \le b + \frac{1}{2^n}$ and $\simeq$ by $a \simeq b \Leftrightarrow a \preceq b$ and $b \preceq a$. Let's define $\mathcal{L}(A) = \{e \in A | 2e \simeq e\}$.

To this purpose, we will prove that, by defining $l: A \to A$ and $\beta: A \to A$, there $a \mapsto \bigvee_{e \in \mathcal{L}(A) \atop e \preceq a} e$ and $a \mapsto 2a \wedge j_*(a)$

exists $l^*: A \to A$ such that $(A, \preceq, \wedge, (\underline{d})_d \in \mathcal{D}, \dagger, \doteq, 2, \frac{1}{2}, j_*, j, \alpha, \beta, l, l^*)$ satisfies $\mathbf{T}_1$.

**Lemma 3.3.3.**

$$ (1) \quad \text{For all } n \in \mathbb{N}, \alpha^{n-1} \circ j_*(\underline{0}) = \frac{1}{2^n}. $$

$$ (2) \quad \text{For all dyadic } d \in [0,1] \text{ and } n \in \mathbb{N}^* \text{ such that } 2^nd \in \mathbb{N}, \underline{d} = \sum_{k=1}^{2^nd} \frac{1}{2^k}. $$

*Proof.* (1) By definition, $\frac{1}{2} = j_*(\underline{0})$.

Let $n \in \mathbb{N}$ such that $\alpha^{n-1} \circ j_*(\underline{0}) = \frac{1}{2^n}$. $\alpha^n \circ j_*(\underline{0}) = \alpha(\frac{1}{2^n}) = \frac{1}{2^{n+1}} \vee j(\frac{1}{2^n})$. However, $\frac{1}{2^n} \le \frac{1}{2} = j_*(\underline{0})$, so $j(\frac{1}{2^n}) \le 0 \le \frac{1}{2^{n+1}}$. Thus $\alpha^n \circ j_*(\underline{0}) = \frac{1}{2^{n+1}}$.

$$ (2) \quad \begin{gathered} \text{For all } n \in \mathbb{N}^*, \frac{1}{2^{n+1}} + \frac{1}{2^{n+1}} = \alpha^n \circ j_*(\underline{0}) + \alpha^n \circ j_*(\underline{0}) \le \frac{1}{2^n} \text{ and } \frac{1}{2^{n+1}} + \frac{1}{2^{n+1}} \ge 2\frac{1}{2^{n+1}} \ge \frac{1}{2^n} \\ \text{Hence, for all } n \in \mathbb{N}^*, \frac{1}{2^{n+1}} + \frac{1}{2^{n+1}} = \frac{1}{2^n}. \text{ Moreover, } \frac{1}{2} + \frac{1}{2} \ge 2\frac{1}{2} \ge 1, \text{ so } \frac{1}{2} + \frac{1}{2} = 1. \end{gathered} $$

Let $n \in \mathbb{N}^*$ such that $2^nd \in \mathbb{N}$. Let $n_0$ be the smallest non negative integer such that $2^{n_0}d \in \mathbb{N}$.

$$ \sum_{k=1}^{2^nd} \frac{1}{2^n} = \sum_{k=1}^{2^{n_0}d} \sum_{i=1}^{2^{n-n_0}} \frac{1}{2^{n_0}} = \sum_{k=1}^{2^{n_0}d} \frac{1}{2^{n_0}} = \underline{d}. $$

□

**Lemma 3.3.4.** Let $a \in A$ and $d \in \mathcal{D}$.

$$ (1) \quad 2j_*(a) = \underline{1}, \frac{a}{2} \le a, j(a) \le a, l(a) \preceq a. $$

$$ (2) \quad \text{For all } n \ge 0, j_*^n(a) + \frac{1}{2^n} \ge \underline{1}. $$
(3) $\alpha$ is invertible, of inverse $\beta$, and, for all $n \in \mathbb{N}$, $\alpha^n(a) = \bigvee_{k=0}^n \frac{j^k(a)}{2^{n-k}}$ and $\alpha^{-n}(a) = \bigwedge_{k=0}^n j_*^{n-k}(2^k a)$. Hence $\alpha(a) \le a$ and $\alpha^{-1}(a) \ge a$.

(4) Let $c \in A$. $\vdash c$, $2$, $\frac{1}{2}$, $j_*$, $j$, $\alpha$ and $\alpha^{-1}$ are non-decreasing for $\le$. $\vdash c$ is non-decreasing and $c \vdash$ is non-increasing for $\le$.
Moreover, for all $a \le b$, $l(a) \le l(b)$.

(5) For all $n \in \mathbb{N}$, $\alpha^n(a) \le j(a) + \frac{1}{2^n}$ and $2a \le \alpha^{-n}(a) + \frac{1}{2^n}$.

(6) $j(a) \simeq a \Leftrightarrow \alpha(a) \simeq a \Leftrightarrow \alpha^{-1}(a) \simeq a \Leftrightarrow 2a \simeq a$.

(7) $l(a)$ is a fixed point of $2$, $\alpha$ and $\alpha^{-1}$, so $l(a) \in \mathcal{L}(A)$ and $l(l(a)) = l(a)$.

(8) $\bigwedge_{n \in \mathbb{N}} \alpha^n(a) \le l(a) \le \bigwedge_{n \in \mathbb{N}} j^n(a)$, so $l(a) \simeq \bigwedge_{n \in \mathbb{N}} \alpha^n(a) \simeq \bigwedge_{n \in \mathbb{N}} j^n(a)$.

*Proof.* Let $a \in A$ and $d \in \mathcal{D}$.

(1) $2j_*(a) \ge 2j_*(\underline{0}) \ge \underline{1}$.
(4.f.1)

$a \le 2a$ by (4.c.1), so, by (3.a.1), $\frac{a}{2} \le a$.

$a \le j_*(a)$ by (4.c.2), so, by (3.b.1), $j(a) \le a$.

For all $n \in \mathbb{N}$ and $e \in \mathcal{L}(A)$ such that $e \le a$, $e \le a + \frac{1}{2^n}$, so $l(a) \le a + \frac{1}{2^n}$, i.e. $l(a) \le a$.

(2) We notice that, for all $n \in \mathbb{N}$,

$$2 \sum_{k=1}^{n} \frac{1}{2^{k+1}} \le \sum_{k=1}^{n} \frac{1}{2^{k+1}} + \sum_{k=1}^{n} \frac{1}{2^{k+1}} = \sum_{k=1}^{n} \frac{1}{2^{k+1}} + \frac{1}{2^{k+1}} = \sum_{k=1}^{n} \frac{1}{2^k}.$$

It suffices to prove, by induction on $n \ge 0$, that, for all $n \in \mathbb{N}$, $j_*^n(\underline{0}) \ge \sum_{k=1}^n \frac{1}{2^k}$ and

$$\sum_{k=1}^{n} \frac{1}{2^k} + \frac{1}{2^n} = \underline{1}.$$

$$j_*^0(\underline{0}) \ge \underline{0} = \sum_{k=1}^{0} \frac{1}{2^k} \text{ and } \sum_{k=1}^{0} \frac{1}{2^k} + \frac{1}{2^0} = \underline{1}.$$

For all $n \ge 0$, such that $j_*^n(\underline{0}) \ge \sum_{k=1}^n \frac{1}{2^k}$ and $\sum_{k=1}^n \frac{1}{2^{k+1}} + \frac{1}{2^n} = \underline{1}$,

$$j_*^{n+1}(\underline{0}) \ge j_* \left( \sum_{k=1}^{n} \frac{1}{2^k} \right) \ge j_* \left( 2 \sum_{k=1}^{n} \frac{1}{2^{k+1}} \right) \ge \sum_{k=1}^{n} \frac{1}{2^{k+1}} + \frac{1}{2} = \sum_{k=1}^{n+1} \frac{1}{2^k}$$

and

$$\sum_{k=1}^{n+1} \frac{1}{2^k} + \frac{1}{2^{n+1}} = \sum_{k=1}^{n} \frac{1}{2^k} + \frac{1}{2^{n+1}} + \frac{1}{2^{n+1}} \ge \sum_{k=1}^{n} \frac{1}{2^k} + 2 \frac{1}{2^{n+1}} \ge \sum_{k=1}^{n} \frac{1}{2^k} + \frac{1}{2^n} \ge \underline{1}.$$

Hence, for all $n \in \mathbb{N}$, $j_*^n(a) + \frac{1}{2^n} \ge j_*(\underline{0}) + \frac{1}{2^n} \ge \sum_{k=1}^n \frac{1}{2^k} + \frac{1}{2^n} = \underline{1}$.

(3) By induction on $n \ge 0$.

By (4.d.1) to (4.e.2), we already know that $\alpha$ is invertible and $\alpha^{-1}(a) = 2a \wedge j_*(a) = \beta(a)$.

Let $n \in \mathbb{N}$ such that $\alpha^{-n}(a) = \bigwedge_{k=0}^n j_*^{n-k}(2^k a)$.
$$
\begin{align*}
\alpha^{-(n+1)}(a) &= \alpha^{-1} \left( \bigwedge_{k=0}^{n} j_*^{n-k}(2^k a) \right) = \bigwedge_{k=0}^{n} 2j_*^{n-k}(2^k a) \wedge \bigwedge_{k=0}^{n} j_*^{n+1-k}(2^k a) \\
&= 2^{n+1}(a) \wedge \frac{1}{2} \wedge \bigwedge_{k=0}^{n} j_*^{n+1-k}(2^k a) = \bigwedge_{k=0}^{n+1} j_*^{n+1-k}(2^k a).
\end{align*}
$$

Hence, for all $n \in \mathbb{N}$, $\alpha^{-n}(a) = \bigwedge_{k=0}^{n} j_*^{n-k}(2^k a)$.

Thus, for all $n \in \mathbb{N}$, and $c \in A$,

$$
\begin{align*}
\alpha^n(a) \le c &\Leftrightarrow a \le \alpha^{-n}(c) \\
&\Leftrightarrow \forall 0 \le k \le n \ a \le j_*^{n-k}(2^k c) \\
&\Leftrightarrow \stackrel{(3.a.1)-(3.b.2)}{\Leftrightarrow} \forall 0 \le k \le n \ \frac{j_*^{n-k}(a)}{2^k} \le c \\
&\Leftrightarrow \bigvee_{k=0}^n \frac{j_*^{n-k}(a)}{2^k} \le c,
\end{align*}
$$

$$
\text{so } \alpha^n(a) = \bigvee_{k=0}^{n} \frac{j_*^{n-k}(a)}{2^k}.
$$

(4) Let $a$ and $b \in A$ and $n \in \mathbb{N}$ such that $a \le b + \frac{1}{2^n}$.

$$
\text{By (4.a.1), } 2a \le 2 \left(b + \frac{1}{2^n}\right) \le 2b + 2\frac{1}{2^n} = 2b + \frac{1}{2^{n-1}}.
$$

By (4.b.1), $j_*(a) \le j_* \left(b + \frac{1}{2^{n+1}}\right) \le j_*(b) + \frac{1}{2^n}$.

(4.a.2) is equivalent to $\frac{v+c}{2} \le \frac{v}{2} + \frac{u}{2}$, so $\frac{a}{2} \le \frac{b+c}{2} \le \frac{b}{2} + \frac{1}{2^{n+1}}$.

(4.b.2) is equivalent to $j(v+u) \le 2v+j(u)$, so $j(a) \le j\left(b+\frac{1}{2^{n+1}}\right) \le j(b)+\frac{1}{2^n}$.

$$
\alpha(a) \le \alpha \left( b + \frac{1}{2^{n+1}} \right) = \frac{b + \frac{1}{2^{n+1}}}{2} \lor j \left( b + \frac{1}{2^{n+1}} \right) \le \left( \frac{b}{2} + \frac{1}{2^n} \right) \lor \left( j(b) + \frac{1}{2^n} \right) \le \alpha(b) + \frac{1}{2^n}.
$$

$$
\alpha^{-1}(a) = 2a \wedge j_{*}(a) \le \left(2b + \frac{1}{2^n}\right) \wedge \left(j_{*}(b) + \frac{1}{2^n}\right) = 2b \wedge j_{*}(b) + \frac{1}{2^n} = \alpha^{-1}(b) + \frac{1}{2^n}.
$$

$$
a \div c \le \left(b + \frac{1}{2^n}\right) \div c \le \left(b \div c\right) + \frac{1}{2^n}.
$$

$$
c \div a \geq c \div \left(b + \frac{1}{2^n}\right) = c \div b + \frac{1}{2^n}.
$$

For all $e \in \mathcal{L}$ such that $e \preceq b$, $e \preceq a$, so $l(b) \le l(a)$.

Finally, by commutativity and associativity of $+$, for all $c \in A$, $b+c \le (a+c) + \frac{1}{2^n}$.

(5) Let $n \in \mathbb{N}$. For all $1 \le k \le n$, by (4.c.1) and (4.c.2), $j_*^{n-k}(2^k a) \ge 2^k a \ge 2a$, and $j_*^n(a) + \frac{1}{2^n} \ge 1 \ge 2a$, so $\alpha^{-n}(a) + \frac{1}{2^n} \ge 2a$. For all $0 \le k \le n-1$, by (3.a.1), (3.b.1), (4.c.1) and (4.c.2), $\frac{j_*^{n-k}(a)}{2^k} \le j^{n-k}(a) \le j(a)$, and $\frac{a}{2^n} \le \frac{1}{2^n} \le j(a) + \frac{1}{2^n}$, so $\alpha^n(a) \le j(a) + \frac{1}{2^n}$.

(6) $\alpha(a) \le a$, so, if $j(a) \simeq a$, then, for all $n \ge 0$, $\alpha(a) + \frac{1}{2^n} = (\frac{a}{2} \vee j(a)) + \frac{1}{2^n} \ge j(a) + \frac{1}{2^n} \ge a$, so $\alpha(a) \simeq a$.

$$
\alpha^{-1}(a) \ge a, \text{ so if } 2a \simeq a, \text{ then, for all } n \in \mathbb{N}, \alpha^{-1}(a) = 2a \wedge j_*(a) \le 2a \le a + \frac{1}{2^n}, \text{ so} \\
\alpha^{-1}(a) \simeq a.
$$

If $\alpha(a) \simeq a$, then, since $\alpha$ is continuous, for all $n \in \mathbb{N}$, $a \simeq \alpha^n(a) \le j(a) + \frac{1}{2^n}$, so $a \preceq j(a)$, i.e. $a \simeq j(a)$.
$\alpha^{-1}$ is continuous because $2 \cdot$ and $j_*$ are, so, if $\alpha^{-1}(a) \simeq a$, then, for all $n \in \mathbb{N}$, $a + \frac{1}{2^n} \simeq \alpha^{-n}(a) + \frac{1}{2^n} \ge 2a$, so $a \ge 2a$, i.e. $a \simeq 2a$.

Finally, $a \simeq \alpha(a) \Leftrightarrow \alpha^{-1}(a) \simeq \alpha(a)$, thanks to of $\alpha$ and $\alpha^{-1}$.

(7) Let $e \in \mathcal{L}(A)$ such that $e \preceq a$. $e \le l(a)$, so $\alpha(e) \le \alpha(l(a))$. However, according to point 6, $e \simeq \alpha(e)$, so $e \preceq \alpha(l(a))$. Hence, for all $n \in \mathbb{N}$, $l(a) \le \alpha(l(a)) + \frac{1}{2^n}$ and thus $l(a) \preceq \alpha(l(a))$. However, $\alpha(l(a)) \le l(a)$, so $\alpha(l(a)) \simeq l(a)$. Hence $\beta(l(a)) \simeq l(a)$ and $2l(a) \simeq l(a)$.

$2l(a) \in \mathcal{L}(A)$, so, since $2l(a) \simeq l(a) \preceq a$, $2l(a) \le l(a)$, i.e. $2l(a) = l(a)$. In the same way, $\beta(l(a)) = l(a)$ and thus $\alpha(l(a)) = l(a)$.

(8) From points 6 and 7, we can deduce that $j(l(a)) \simeq l(a)$. Hence, since $l(a) \preceq a$, for all $n \in \mathbb{N}$, $l(a) = j^n(l(a)) \preceq j^n(a)$, so $l(a) \preceq \bigwedge_{n \ge N} j^n(a)$. Since, for all $a \in A$, $j(a) \le \frac{a}{2} \lor j(a) =$

$\alpha(a), \bigwedge_{n \in \mathbb{N}} j^n(a) \le \bigwedge_{n \in \mathbb{N}} \alpha^n(a)$. Since $\alpha\left(\bigwedge_{n \in \mathbb{N}} \alpha^n(a)\right) = \bigwedge_{n \in \mathbb{N}} \alpha^{n+1}(a) = \bigwedge_{n \in \mathbb{N}} \alpha^n(a)$, and $\bigwedge_{n \in \mathbb{N}} \alpha^n(a) \le a$, $\bigwedge_{n \in \mathbb{N}} \alpha^n(a) \le l(a)$. $\square$

**Lemma 3.3.5.** For all $a$ and $b \in A$ and $d$ and $d' \in \mathcal{D}$,

(1) $\underline{d}+\underline{d}'=\underline{d}+\underline{d}'$.

(2) $2(\underline{d}+l(a)) = 2\underline{d}+l(a)$

(3) $j_*(\underline{d}+l(a)) = \underline{j_*(d)}+l(a)$

(4) $\alpha(\underline{d}+l(a)) = \underline{\alpha(d)}+l(a)$

(5) $l(\underline{d}+l(a)) = \underline{l(d)}+l(a)$

(6) $a \le \underline{d}+l(a+\underline{1-d})$ and for all $n \in \mathbb{N}$, $\bigwedge_{k=1}^{2^{n+1}} (1-\frac{k}{2^{n+1}}) + l(\underline{a+\frac{k}{2^{n+1}}}) \preceq \underline{a+\frac{1}{2^n}}$.

*Proof.* Let $a$ and $b \in A$ and $d$ and $d' \in [0, 1]$.

(1) Let $n$ be a non negative integer such that $2^n d$ and $2^n d' \in \mathbb{N}$.

$$ \underline{d}+\underline{d}' = \sum_{k=1}^{2^n d} \frac{1}{2^n} + \sum_{k=1}^{2^n d'} \frac{1}{2^n} = \sum_{k=1}^{2^n(d+d')} \frac{1}{2^n} = \underline{d}+\underline{d}' $$

(2) For all integer $n \ge 2$ such that $2^n d \in \mathbb{N}$, $2\frac{1}{2^n} = 2\frac{1}{2^{n-1}} = \frac{1}{2^{n-1}}$, and $2\frac{1}{2^n} \le \frac{1}{2^n} + \frac{1}{2^n} \le \frac{1}{2^{n-1}}$, so $2\frac{1}{2^n} = \frac{1}{2^{n-1}}$. $2\underline{d} = 2\sum_{k=1}^{2^n d} \frac{1}{2^n} = \sum_{k=1}^{2^n d} 2\frac{1}{2^n} = \sum_{k=1}^{2^{n-1}2d} \frac{1}{2^{n-1}} = 2\underline{d}$.

Thus, by (4.a.2), (4.a.1) and **Lemma 3.3.4** (7), $2(\underline{d}+l(a)) = 2\underline{d}+2l(a) = \underline{2d}+l(a)$.

(3) $j_*(\underline{d}+l(a)) = j_*\left(2\left(\frac{\underline{d}}{2}+l(a)\right)\right) = \frac{\underline{d}}{2}+l(a)+\frac{1}{2} = \frac{\underline{d}}{2}+\frac{1}{2}+l(a) = j_*(\underline{d})+l(a)$.

(4) Since $+$ admits a residual (cf. (1.c)), $+$ preserves lower bounds and so

$$ 2(\underline{d}+l(a)) \wedge j_*(\underline{d}+l(a)) = (2\underline{d}+l(a)) \wedge (\underline{j_*(d)}+l(a)) = (2\underline{d} \wedge \underline{j_*(d)})+l(a) = 2\underline{d} \wedge \underline{j_*(d)}+l(a). $$

Since, for all $x \in [0, 1]$, $2\alpha(x) \wedge j_* \circ \alpha(x) = x$,

$$ \alpha^{-1}(\underline{\alpha(d)}+l(a)) = 2(\underline{\alpha(d)}+l(a)) \wedge j_*(\underline{\alpha(d)}+l(a)) = 2\underline{\alpha(d)} \wedge \underline{j_* \circ \alpha(d)}+l(a) = \underline{d}+l(a), $$
so $\alpha(\underline{d}^\dagger+l(a)) = \alpha(d)^\dagger+l(a)$.

(5) If $d = 1$, then $l(\underline{d}^\dagger+l(a)) = \underline{1} = l(\underline{1}^\dagger+l(a))$. Assume that $q < 1$, ie $\bigwedge_{n \in \mathbb{N}} \alpha^n(d) = 0$. By Lemma 3.3.4 (8), $l(\underline{d}^\dagger+l(a)) \simeq \bigwedge_{n \in \mathbb{N}} \alpha^n(\underline{d}^\dagger+l(a)) \simeq \bigwedge_{n \in \mathbb{N}} \alpha^n(d)^\dagger+l(a)$ and thus, for all $k \in \mathbb{N}$, $l(\underline{d}^\dagger+l(a)) \le \frac{1}{2^k}^\dagger+l(a) \le \frac{1}{2^k}^\dagger+a$. Hence $l(\underline{d}^\dagger+l(a)) \le a$ and thus $l(\underline{d}^\dagger+l(a)) \le l(a) = l(d)^\dagger+l(a)$. However, $\underline{d}^\dagger+l(a) \ge l(a)$, so $l(\underline{d}^\dagger+l(a)) \ge l(l(a)) = l(a) = l(d)^\dagger+l(a)$.

(6) By (5.a), for all $n \in \mathbb{N}$, $a \le \underline{d}^\dagger+\alpha^n(a+\underline{1}-d)$, so, by Lemma 3.3.4 (8), $a \le \underline{d}^\dagger+l(a+\underline{1}-d)$. Similarly, using (5.b), for all $n \in \mathbb{N}$,

$$a^\dagger + \frac{1}{2^n} \ge \bigwedge_{k=1}^{2^{n+1}-1} \left(1 - \frac{k}{2^{n+1}}\right)^\dagger + \alpha^{n+1} \left(a^\dagger + \frac{k}{2^{n+1}}\right) \ge \bigwedge_{k=1}^{2^{n+1}-1} \left(1 - \frac{k}{2^{n+1}}\right)^\dagger + l\left(a^\dagger + \frac{k}{2^{n+1}}\right).$$

□

**Lemma 3.3.6.** Let $l^*: A \to A$. For all $a$ and $b \in A$, $l^*(a) \preceq b \Leftrightarrow a \preceq l(b)$, and $a \mapsto \bigvee_{n \in \mathbb{N}} \alpha^{-n}(a)$

$l(l(a)^\dagger+l(b)) = l(a)^\dagger+l(b).$

*Proof.* Let $a$ and $b \in A$.

$$l^*(a) \preceq b \Leftrightarrow \forall n \in \mathbb{N} \alpha^{-n}(a) \preceq b \Leftrightarrow \forall n \in \mathbb{N} a \preceq \alpha^n(b) \Leftrightarrow a \preceq l(b)$$

For all $a$ and $b \in A$, $2(l(a)^\dagger+l(b)) = 2l(a) + 2l(b) = l(a)^\dagger+l(b)$, so $l(a)^\dagger+l(b) \in \mathcal{L}(A)$, so, since $l(a)^\dagger+l(b) \preceq l(a)^\dagger+l(b)$, $l(l(a)^\dagger+l(b)) \ge l(a)^\dagger+l(b)$. However, $l(b)^\dagger + \bigwedge_{n \in \mathbb{N}} \frac{1}{2^n} \preceq l(b)$ and $l(b)^\dagger + \bigwedge_{n \in \mathbb{N}} \frac{1}{2^n} \in \mathcal{L}(A)$, so $l(b)^\dagger + \bigwedge_{n \in \mathbb{N}} \frac{1}{2^n} \le l(b)$. Hence

$$l(l(a)^\dagger+l(b)) \le l(a)^\dagger+l(b)^\dagger + \bigwedge_{n \in \mathbb{N}} \frac{1}{2^n} \le l(a)^\dagger+l(b).$$

□

*Proof of Theorem 3.3.1.* According to Lemmas 3.3.4, 3.3.5 and 3.3.6, since for all $a$ and $b \in A$, $a \le b \Rightarrow a \preceq b$, $\mathcal{A} = (A, \preceq, (\underline{d})_d \in \mathcal{D}, \dot{+}, \cdot, 2, \frac{1}{2}, j_*, j, \alpha, \beta, l, l^*)$ is a model of $\mathbf{T}_1$. Moreover, for all $a$ and $b \in A$ such that for all $n \in \mathbb{N}$ $a \preceq b+\frac{1}{2^n}$, for all $n \in \mathbb{N}$, $a \le b+\frac{1}{2^{n+1}}+\frac{1}{2^{n+1}} = b+\frac{1}{2^n}$, so $a \preceq b$. Thus, $\mathcal{A}$ is an Archimedean model of $\mathbf{T}_1$. Finally, since $\le$ is a complete order on $A$, we can consider $\bigwedge: \{E \subset A\} \to A$. For all $E \subset A$ and $b \in A$, $b \preceq \bigwedge E \Leftrightarrow \forall n \in \mathbb{N} b \le \bigwedge E+\frac{1}{2^n} \Leftrightarrow \forall n \in \mathbb{N} \forall a \in E b \le a+\frac{1}{2^n} \Leftrightarrow \forall a \in E b \preceq a$, so $\mathcal{A}$ is a complete model of $\mathbf{T}_1$. Hence, according to Corollary 3.2.8, there exists a residuated commutative complete lattice $\mathcal{L}$ such that $\mathcal{A} / \simeq \mathcal{L}_1$-isomorphic to $\mathcal{USC}(\mathcal{L})$. Let us denote by $i$ the isomorphism. We can show that $i$ preserves the binary lower bounds in the same way as we
show it preserves the binary upper bounds. For all $a, b$ and $c \in A$,

$$i(a \lor b) \leq i(c) \Leftrightarrow a \lor b \leq c$$

$$\Leftrightarrow \forall n \in \mathbb{N} \ a \lor b \leq c + \frac{1}{2^n}$$

$$\Leftrightarrow \forall n \in \mathbb{N} \ a \leq c + \frac{1}{2^n} \text{ and } b \leq c + \frac{1}{2^n}$$

$$\Leftrightarrow i(a) \leq i(c) \text{ and } i(b) \leq i(c)$$

$$\Leftrightarrow i(a) \lor i(b) \leq i(c).$$

Hence the $A/\simeq$ is $\mathcal{L}$-isomorphic to $\mathrm{USC}(\mathcal{L})$.

□

**Remark 3.3.1.** Since, for all commutative residuated complete lattice $\mathcal{L}$, $\frac{1}{2} = \frac{1}{2}$, $\frac{1}{2} \leq \frac{1}{2}$ is a consequence of $\mathbf{T}$.

3.3.2. General models of $\mathbf{T}$. Now that we have proven any complete model of $\mathbf{T}$ to be, up to a quotient, isomorphic to an AC-algebra, we prove that general models of $\mathbf{T}$ are, up to a quotient, embeddable into AC-algebras (Theorem C).

**Notation 3.3.7.** $u \preceq v \Leftrightarrow \forall n \in \mathbb{N} \ u \leq v + \frac{1}{2^n}$ and $u \simeq v \Leftrightarrow u \preceq v$ and $v \simeq u$.

To complete models of $\mathbf{T}$, we use the Macneille completion of an order whose construction was first given in [37, Definition 11.4].

**Definition 3.3.8** ([2], cf. also [4], and [13, Theorem 7041]). The Macneille completion of an ordered set $(X, \leq)$ is a complete ordered set $(\bar{X}, \leq)$ together with an non-decreasing function $\varphi: \bar{X} \to \bar{X}$ such that for every $x \in \bar{X}$, there exist $(y_i)_{i \in I} \in X^I$ and $(z_j)_{j \in J} \in X^J$ such that $\bigvee_{i \in I} \varphi(y_i) = x = \bigwedge_{j \in J} \varphi(z_j)$.

The aim of this section is to prove the **Theorem C**. What we have to prove is that the $\mathcal{L}$-structure can be extended to the Macneille completion and that it still satisfies the axioms of $\mathbf{T}$. First, a bit of preliminaries about the Macneille completion.

**Lemma 3.3.9.** The Macneille completion of the opposite of an ordered set is the opposite of its Macneille completion.

The binary case of the following lemma is proven in [46, Proposition 3.17].

**Lemma 3.3.10.** Let $n \in \mathbb{N}$, $X, X_1, \dots, X_n$ be ordered sets and $f: \prod_{i=1}^n X_i \to X$.

(1) There exists $\bar{f}: \prod_{i=1}^n \bar{X}_i \to \bar{X}$ preserving upper bounds in each coordinate such that $\bar{f} \circ (\varphi, \dots, \varphi) = \varphi \circ f$ if and only if there exist $g_1, \dots, g_n: \prod_{i=1}^n X_i \to \bar{X}$ such that, for all $1 \leq i \leq n$, for all $x \in \prod_{i=1}^n X_i$ and $y \in X$ $f(x) \leq y \Leftrightarrow \varphi(x_i) \leq g_i(x_1, \dots, x_{i-1}, y, x_{i+1}, \dots, x_n)$. Moreover, if it exists, $\bar{f}$ is unique.

(2) There exists $\bar{f}: \prod_{i=1}^n \bar{X}_i \to \bar{X}$ preserving lower bounds in each coordinate such that $\bar{f} \circ (\varphi, \dots, \varphi) = \varphi \circ f$ if and only if there exist $g_1, \dots, g_n: \prod_{i=1}^n X_i \to \bar{X}$ such that, for all $1 \leq i \leq n$, for all $x \in \prod_{i=1}^n X_i$ and $y \in X$ $f(x) \geq y \Leftrightarrow \varphi(x_i) \geq g_i(x_1, \dots, x_{i-1}, y, x_{i+1}, \dots, x_n)$.
Moreover, if it exists, $\bar{f}$ is unique.

Let now $A$ be a model of $\mathbf{T}$ and denote by $\varphi: A \to \bar{A}$ the canonical morphism from $A$ to its Macneille completion.

**Definition 3.3.11 ([46]).** On $\bar{A}$, we define $\vee$ and $\wedge$ to be the binary upper and lower bounds, $\mathbb{0}$ to be the bottom element and $\mathbb{1}$ to be the top one. Since $\dot{+}$, multiplication by 2, $j_*$, and $\alpha$ admit residual and adjoints, thanks to **Lemmas 3.3.10 and 3.3.9**, we can define the lower bound preserving functions $\dot{+}$, $\dot{-}$, $2\cdot$, $j_*$, $\alpha$ and $\beta$ on $\bar{A}$ as follows:
for all $(a_i)_{i \in I} \in A^I$ and $(b_j)_{j \in J} \in A^J$,

$$ (1) \quad \bigwedge_{i \in I} \varphi(a_i) \dot{+} \bigwedge_{j \in J} \varphi(b_j) = \bigwedge_{(i,j) \in I \times J} \varphi(a_i \dot{+} b_j) $$

$$ (2) \quad \bigvee_{i \in I} \varphi(a_i) \dot{-} \bigwedge_{j \in J} \varphi(b_j) = \bigvee_{(i,j) \in I \times J} \varphi(a_i \dot{-} b_j) $$

$$ (3) \quad 2 \bigwedge_{i \in I} \varphi(a_i) = \bigwedge_{i \in I} \varphi(2a_i) $$

$$ (4) \quad j_* \left( \bigwedge_{i \in I} \varphi(a_i) \right) = \bigwedge_{i \in I} \varphi(j_*(a_i)) $$

$$ (5) \quad \alpha \left( \bigwedge_{i \in I} \varphi(a_i) \right) = \bigwedge_{i \in I} \varphi(\alpha(a_i)) $$

We define $\dot{2}$ and $j$ as the respective adjoints of 2 and $j_*$.

**Lemma 3.3.12.** $\varphi$ is a morphism of $\mathcal{L}$-structures.

*Proof.* It suffices to prove that, $\varphi$ is a morphism for $\dot{2}$ and $j$. Both proofs follow the same steps, so we just prove that $\varphi$ preserves $\dot{2}$.
For all $a \in A$ and $b \in \bar{A}$,

$$ \begin{align*} \varphi\left(\frac{a}{2}\right) &\le b &\Leftrightarrow \varphi\left(\frac{a}{2}\right) &\le \bigwedge_{\substack{c \in A \\ \varphi(c) \le b}} \varphi(c) \\ &\Leftrightarrow \forall c \in A \text{ s.t. } \varphi(c) \le b, \varphi\left(\frac{a}{2}\right) &\le \varphi(c) \\ &\Leftrightarrow \forall c \in A \text{ s.t. } \varphi(c) \le b, \frac{a}{2} &\le c \\ &\Leftrightarrow \forall c \in A \text{ s.t. } \varphi(c) \le b, a &\le 2c \\ &\Leftrightarrow \forall c \in A \text{ s.t. } \varphi(c) \le b, \varphi(a) &\le 2\varphi(c) \\ &\Leftrightarrow \varphi(a) &\le \bigwedge_{\substack{c \in A \\ \varphi(c) \le b}} 2\varphi(c) \\ &\Leftrightarrow \varphi(a) &\le 2 \bigwedge_{\substack{c \in A \\ \varphi(c) \le b}} \varphi(c) \\ &\Leftrightarrow \frac{\varphi(a)}{2} &\le b. \end{align*} $$

□

**Remark 3.3.2.** This also proves that the upper bounds preserving operations induced by $j$ and $\dot{2}$ on $\bar{A}$ are left adjoint to $j_*$ and $2\cdot$.
To conclude the proof of **Theorem C**, we just have to prove next theorem.

**Theorem 3.3.13.** $\bar{A}$ is a complete model of $\mathbf{T}$.

An immediate corollary of **Theorem 3.3.13** is the following one.

**Corollary 3.3.14.** There exists a commutative residuated complete lattice $\mathcal{L}$ such that the quotient $\bar{A}/\simeq$ is isomorphic $\mathrm{USC}(\mathcal{L})$.

Here are two lemmas we need to prove **Theorem 3.3.13**.

**Lemma 3.3.15** ([46, Proposition 3.3]). The adjunction axioms between $\dagger$ and $\ddagger$ are satisfied by $\bar{A}$.

**Lemma 3.3.16.** Let $f$ and $g$ be two non-decreasing functions from $\bar{X}^n$ to $\bar{X}$ such that, for all $x \in X^n$, $f(x) \le g(x)$.

If $f$ preserves upper bounds in each coordinate or $g$ preserves lower bounds in each coordinate, then $f \le g$.

*Proof.* Let $(x_j)_{i \in J} \in X^n$.

Let us assume that $f$ preserves all upper bounds. Then

$$f\left(\bigvee_{j \in J} x_j\right) = \bigvee_{(j_i)_{1 \le i \le n} \in J^n} f(x_{1,j_1}, \dots, x_{n,j_n}) \le \bigvee_{1 \le i \le n} \bigvee_{j \in J} g(x_{1,j_1}, \dots, x_{n,j_n}) \le g\left(\bigvee_{j \in J} x_j\right).$$

The second case is symmetric. $\square$

*Proof of Theorem 3.3.13.* $\bar{A}$ is a complete bounded lattice and $\dagger$ admits a residual, so $\bar{A}$ is a commutative residuated complete lattice. The adjunction axioms (3.a.1), (3.a.2), (3.b.1) and (3.b.2) are satisfied by definition.

To prove that the other axioms of $\mathbf{T}$ are satisfied by $\bar{A}$, we notice that the axioms and schemes of axioms from (4.a.1) to (5.b) are of the form $f \le g$, where $f$ and $g$ are non-decreasing functions such that $g$ preserves lower bounds in each coordinate. Thus, **Lemma 3.3.16** enables to conclude that $\bar{A}$ satisfies $\mathbf{T}$. $\square$

*Proof of Theorem C.* By **Theorems 3.3.13 and 3.3.1**, there exists a commutative residuated lattice $\mathcal{L}$ and an isomorphism $i: \bar{A}/\simeq \to \mathrm{USC}(\mathcal{L})$. Let $\pi$ denote the quotient morphism from $\bar{A}$ to $\bar{A}/\simeq$ and $\varphi$ the inclusion morphism of $A$ into $\bar{A}$. The image of $i \circ \pi \circ \varphi$ is endowed with an $\mathcal{L}$-structure, which makes it the quotient of $A$ by $\simeq$. Hence, the quotient of $A$ by $\simeq$ is an $\mathcal{L}$-structure that embeds into $\mathrm{USC}(\mathcal{L})$. $\square$

**Theorem 3.1.4** is an immediate corollary of **Theorem 3.3.13**

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

(1) For all commutative residuated complete lattice $\mathcal{L}$, $\mathrm{USC}(\mathcal{L}) \models \varphi \le \psi$.

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

*Proof.* We already proved that the class of $\mathrm{USC}(\mathcal{L})$, for $\mathcal{L}$ a commutative residuated complete lattice is sound for $\mathbf{T}$. By Archimedeanity of every AC-algebra, we have that 2 implies 1.

Let $\varphi$ and $\psi$ be $\mathcal{L}$-terms both having $k$ free variables such that, for all commutative residuated complete lattice $\mathcal{L}$, $\mathrm{USC}(\mathcal{L}) \models \varphi \le \psi$. Let $A$ be a model of $\mathbf{T}$. According to **Theorem C**, there exists a commutative residuated lattice $\mathcal{L}$ and a morphism $i: A \to \mathrm{USC}(\mathcal{L})$ 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)) \leq i(\psi(a))$, $\varphi(a) \leq \psi(a) + \frac{1}{2^n}$. The class of models of $\mathbf{T}$ being complete for $\mathbf{T}$, for all $n \in \mathbb{N}$
$\varphi \leq \psi + \frac{1}{2^n}$ is consequence of $\mathbf{T}$. $\square$

4. CUT ADMISSIBILITY FOR AFFINE CONTINUOUS LOGIC

The purpose of this section is to exhibit a deductive system in a sequent-style calculus for the logic described by AC-algebras. For this, we define a language for structures (on the left side of the turnstile) and formulas, and give the correspondence with the language $\mathcal{L}$. Here can be seen the role of $\alpha$, which is to be a substitue to both $\dot{2}$ and $j$ whenever we need them on the left side of a turnstile.

The theorems stated in this section rely on **Theorems 8.1.12 and 8.1.13** proven in **Annexes 8**. In order to talk about cut elimination, we need to define a language for the structures and formulas of our sequent like calculus and give the correspondence with the language $\mathcal{L}$.

<table><caption>FIGURE 1. Correspondence between structure symbols and $\mathcal{L}$</caption><thead><tr><th colspan="3">Positive symbols</th><th colspan="2">Negative correspondent</th></tr><tr><th>structures</th><th>formulas</th><th>algebraic correspondent</th><th>formulas</th><th>algebraic notation</th></tr></thead><tbody><tr><td>,</td><td>+</td><td>+</td><td></td><td></td></tr><tr><td>ε</td><td>0</td><td>0</td><td>1</td><td>1</td></tr><tr><td></td><td>∧</td><td>∧</td><td>∨</td><td>∧</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></tbody></table>

**Notation 4.1.1.** For all $k \in \mathbb{N}$, let $k\gamma$ denote $\gamma, \dots, \gamma k$ times, and for every dyadic number in $[0, 1)$, $d = \frac{k}{2^n}$ with $k$ odd, let $\varepsilon_d$ denote $k \circ_{\alpha}^{n-1} \bullet_2 \varepsilon$. To be noticed, $\varepsilon_{\frac{1}{2}} = \bullet_2 \varepsilon$. We also define $\varepsilon_1$ as $\circ_2 \bullet_2 \varepsilon$.

The justification of these notations is the following: **Lemma 3.3.3** proves that, with the definition given in **Notation 3.1.1**, the interpretation of a dyadic $\frac{k}{2^n}$ in our language is $k\alpha^{n-1} \circ j_*(0)$. Moreover, axiom (4.f.1) ensures that $\underline{1} = 2j_*(\underline{0})$ and, for any algebra $A$ in the language $\mathcal{L} \setminus \{\underline{1}\}$ satisfying axioms (1.b) to (5.b) where $\underline{1}$ is replaced by $2j_*(\underline{0})$, by letting $\underline{1} = 2j_*(\underline{0})$, $A$ is now a model of $\mathbf{T}$.

The system **MGL** for modal full Lambek calculus can be applied with one or several modalities. We need six modalities and three structural symbols $\circ_2, \bullet_2$ and $\circ_\alpha$. We thus obtain a system **MGL** $(\circ_2, \bullet_2, \circ_\alpha)$ given by **GL** (from the **Appendix 8**) — understood with contexts of the extended language — and Figure 2. In addition to these rules, we add the structural rules given in Figure 3 and call the total system **CFL<sub>ew</sub>**.

<table><caption>FIGURE 2. Introduction Rules for Modalities</caption><tr><td>$[L 2] \frac{\Gamma[\circ_2 A] \vdash B}{\Gamma[2A] \vdash B}$</td><td>$[R 2] \frac{\gamma \vdash B}{\circ_2 \gamma \vdash 2B}$</td><td>$[L \dot{\frac{1}{2}}] \frac{\Gamma[A] \vdash B}{\Gamma[\circ_2 \frac{A}{2}] \vdash B}$</td><td>$[R \dot{\frac{1}{2}}] \frac{\circ_2 \gamma \vdash A}{\Gamma[\gamma] \vdash \frac{A}{2}}$</td></tr><tr><td>$[L j_*] \frac{\Gamma[\bullet_2 A] \vdash B}{\Gamma[j_*(A)] \vdash B}$</td><td>$[R j_*] \frac{\gamma \vdash B}{\bullet_2 \gamma \vdash j_*(B)}$</td><td>$[L j] \frac{\Gamma[A] \vdash B}{\Gamma[\bullet_2 j(A)] \vdash B}$</td><td>$[R j] \frac{\bullet_2 \gamma \vdash A}{\Gamma[\gamma \vdash j(A)]}$</td></tr><tr><td>$[L \alpha] \frac{\Gamma[\circ_\alpha A] \vdash B}{\Gamma[\alpha(A)] \vdash B}$</td><td>$[R \alpha] \frac{\gamma \vdash B}{\circ_\alpha \gamma \vdash \alpha(B)}$</td><td>$[L \blacksquare \alpha] \frac{\Gamma[A] \vdash B}{\Gamma[\circ_\alpha \blacksquare \alpha A] \vdash B}$</td><td>$[R \blacksquare \alpha] \frac{\circ_\alpha \gamma \vdash A}{\Gamma[\gamma] \vdash \blacksquare \alpha A}$</td></tr></table>
<figure><img src="image_7.png" /><figcaption>FIGURE 3. CFL<sub>ew</sub></figcaption></figure>

**Lemma 4.1.2.** *Algebraic models of CFL<sub>ew</sub> are the Archimedean models of the theory T.*

*Proof.* According to the soundness part of **Theorem 8.1.12**, the models of **CFL<sub>ew</sub>** are the residuated lattices satisfying, for each previous structural rule *r*, the formula in the language **L** where each structure variable has been replaced by a fresh new formula variable, — by ⇒, ⊢ by ≥, , by +, ○₂ by 2, ●₂ by *j*<sub>*</sub>, ○<sub>α</sub> by *α* and each *ε*<sub>*d*</sub> by *d* and the contexts have been removed.

**Example 4.1.1.** Let us take (3.a) as an example of axioms the rules of which are introduction rules, and (4.d) as an example of axioms the rules of which are structural rules.

$$
(3.a) : \frac{\Gamma[\circ_2 A] \vdash B}{\Gamma[2A] \vdash B} \quad \text{and} \quad \frac{\Gamma[A] \vdash B}{\Gamma[\circ_2 \frac{A}{2}] \vdash B} \quad \text{give} \quad \frac{A \vdash a}{\circ_2 \frac{A}{2} \vdash A} \quad \text{and} \quad \frac{A \vdash A}{\circ_2 A \vdash 2A}.
$$

$$
(4.d) : \text{First, } \frac{\Gamma[\gamma] \vdash A}{\Gamma[\circ_{\alpha} \circ_{2} \gamma] \vdash A} \text{ gives the formula } b \ge a \Rightarrow \alpha(2b) \ge a, \text{ which is equivalent to} \\
\alpha(2b) \ge b.
$$

Second, $\frac{\Gamma[\gamma] \vdash A}{\Gamma[\circ_{\alpha} \bullet_{2} \gamma] \vdash A}$ gives the formula $b \ge a \Rightarrow \alpha \circ j_{*}(b) \ge a$, which is equivalent to $\alpha \circ j_{*}(b) \ge b$. Thanks to the fact that $\alpha$ admits a left adjoint, these two formulas are in turn equivalent to the following one: $v \le \alpha(2v \wedge j_{*}(v))$ (4.d.1).

Third, $\frac{\Gamma[\circ_{\alpha}\circ_{2}\gamma \vdash A \qquad \Gamma[\circ_{\alpha}\bullet_{2}\gamma] \vdash A]}{\Gamma[\gamma] \vdash A}$ gives the formula $\alpha(2b) \ge a \& \alpha \circ j_{*}(b) \ge a \Rightarrow b \ge a$, which is equivalent to $b \ge \alpha(2b) \wedge \alpha \circ j_{*}(b)$. Since $\alpha$ admits a left adjoint, it is, in turn, equivalent to $\alpha(2v \wedge j_{*}(v)) \le v$ (4.d.2).

(2) and (3) can be treated the same way as (3.a) and (1.a), (4) and (5) can be treated the same way as (4.d). The only rule to which the previous methodology can't apply directly is (6.b) because it is infinitary. However, it is immediate that every model of this rule has equivalently the property
∀n ∈ N 1 2n ≥ v ⇒ 0 ≥ v, which is actually property (6.b). Hence models of **CFL<sub>ew</sub>** are exactly the Archimedean models of **T**. □

Since all the added rules are analytic (cf. **Definition 8.1.2**), according to **Theorems 8.1.12 and 8.1.13**, the following two theorems are true.

**Theorem 4.1.3** (Completeness theorem). *The class of USC($\mathcal{L}$), for $\mathcal{L}$ a complete commutative residuated lattice, is sound and complete for $CFL_{ew}$.*

**Theorem 4.1.4** (Cut Admissibility theorem).

In the system **CFL<sub>ew</sub>**, 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.

Finally, we prove a correspondence theorem between structural rules in the language of the system **GL** ([20, Table 1]) and structural rules in the language **CFL<sub>ew</sub>**.

**Definition 4.1.5** ([11, p.8 and Definition 4.3]). *Let us denote by $\mathcal{L}_{GL}$ the language $\{, \cdot, \varepsilon, 1, / , \setminus, \},$ which is the language in which $GL$ is expressed.*

A rule in the language $\mathcal{L}_{GL}$ is said analytic when it is an $\mathcal{L}_{GL}$-rule of the form
$$ \frac{\Gamma[\Upsilon_1] \vdash A \quad \dots \quad \Gamma[\Upsilon_n] \vdash A}{\Gamma[\Upsilon_0] \vdash A} $$
— where the $\Upsilon_i$s are $\{, \cdot, \varepsilon\}$-terms — 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$.

**Theorem 4.1.6.** Let $r = \frac{\Gamma[\Upsilon_1] \vdash A \quad \dots \quad \Gamma[\Upsilon_n] \vdash A}{\Gamma[\Upsilon_0] \vdash A}$ be an analytic $\mathcal{L}_{GL}$ rule and let's denote by $k_i$ the total number of times $\circ_2 2^{k_1 \vee \dots \vee k_n}$ times in front of $\Upsilon_0$ by $2^{k_1 \vee \dots \vee k_n}$.

$r_c$ is analytic and, for all commutative residuated complete lattice $\mathcal{L}$, $\mathcal{L}$ satisfies $r$ in the sense of **Definition 8.1.10** if and only if $\text{USC}(\mathcal{L})$ satisfies $r_c$ in the same sense.

*Proof.* The analyticity of $r_c$ is obvious.

Let $\mathcal{L}$ be a commutative residuated complete lattice and, for all $\mathcal{L}_{GL}$-term $\Upsilon$, let $\Upsilon^\circ$ denote the $\mathcal{L}_{crl}$-term where $\varepsilon$ and , are respectively replaced by $\top$ and $\otimes$, let $\Upsilon^\bullet$ denote the $\mathcal{L}$-term where $\varepsilon$ and , are respectively replaced by $\emptyset$ and $\vdash$.

Assume that $\mathcal{L}$ satisfies $r$, i.e. for all $U: \mathcal{V} \to \mathcal{L}$ and $V \in \mathcal{L}$, if $\Upsilon_1^\circ[U] \le V$ and ... and $\Upsilon_1^\circ[U] \le V$, then $\Upsilon_0^\circ[U] \le V$. $\mathcal{L} \models \Upsilon_1^\circ \vee \dots \vee \Upsilon_n^\circ \ge \Upsilon_0^\circ$. Since, for all $0 \le i \le n$ $\Upsilon_i$ is lax and colax, from **Theorems 2.2.15, 2.4.3** and the remark that, for all $h$ and $g \in \text{USC}(\mathcal{L})$, $\frac{h+g}{2} \le \frac{h}{2} + \frac{g}{2}$, we deduce that, for all $f: \mathcal{V} \to \text{USC}(\mathcal{L})$, $\frac{\Upsilon_1^\circ[f]}{2^{k_1}} \wedge \dots \wedge \frac{\Upsilon_0^\circ[f]}{2^{k_n}} \le \Upsilon_0^\circ[f]$. Finally, since for all $h$ and $g \in \text{USC}(\mathcal{L})$ and $k$ and $k' \in \mathbb{N}$, $\frac{h \wedge g}{2^{k \vee k'}} \le \frac{h}{2^k} \wedge \frac{g}{2^{k'}}$, for all $f: \mathcal{V} \to \mathcal{L}$, $\frac{\Upsilon_0^\circ[f] \wedge \dots \wedge \Upsilon_n^\circ[f]}{2^{k_1 \vee \dots \vee k_n}} \le \Upsilon_0^\circ[f]$, i.e. $\Upsilon_0^\circ[f] \wedge \dots \wedge \Upsilon_n^\circ[f] \le 2^{k_1 \vee \dots \vee k_n} \Upsilon_0^\circ[f]$.

Hence $\text{USC}(\mathcal{L})$ satisfies $r_c$.

Conversely, assume that $\text{USC}(\mathcal{L})$ satisfies $r_c$. Let $U: \mathcal{V} \to \mathcal{L}$.

Then, $\Upsilon_0^\circ[0_U] \wedge \dots \wedge \Upsilon_n^\circ[0_U] \le 2^{k_1 \vee \dots \vee k_n} \Upsilon_0^\circ[0_U] = \Upsilon_0^\circ[0_U]$, so, according to **Theorem 2.2.19**, $\Upsilon_0^\circ[U] \vee \dots \vee \Upsilon_n^\circ[U] \ge \Upsilon_0^\circ[U]$. Hence $\mathcal{L}$ satisfies $r$. □

## 5. INTUITIONISTIC CONTINUOUS LOGIC

We give a study of the case where the underlying commutative residuated complete lattice $\mathcal{L}$ is a locale. In this special case, we actually axiomatize algebras whose quotient by the $\simeq$ relation
(Notation 3.3.7) embeds into some USC(X) for some topological space X. To do this, we first need some preliminary results about ordered topological spaces. Second, we provide an axiomatisation for the algebras of the form USC(L) for L a locale, and, third, we show that the theory of the USC(L)—for L a locale—is the same as the one of the USC(X)—for X a topological space. To achieve this task, we build from any locale L a topological space X and an embedding from USC(L) to USC(X). Finally, we give a sequent-style deductive system admitting the cut rule for these algebras.

**5.1. Topological Preliminaries.** This subsection is independent of the preceding sections. We give some results about compact ordered topological spaces. Let (X, ≤) be an ordered topological space.

**Notation 5.1.1.** For all $A \subset X$, let $\downarrow A = \{x \in X \mid \exists a \in A \text{ s.t. } x \le a\}$ and $\uparrow A = \{x \in X \mid \exists a \in A \text{ s.t. } x \ge a\}$.

For all $f: X \to [0, 1]$, let's denote by $\downarrow f$ the smallest non-increasing function greater than $f$, $\uparrow f$ the smallest non-decreasing function greater than $f$, $\bar{f}$ is the smallest lower semi-continuous function greater than $f$ and $\odot$ is the greatest upper semi-continuous function smaller than $f$.

The next lemma gives caracterisations of the notion of intuitionistic space (cf. **Definition 5.3.2**), while drawing a parallel between being totally disconnected and being Hausdorff, between open sets and lower semi-continuous functions, and between clopen sets and continuous functions.

**Lemma 5.1.2.**

<figure><img src="image_8.png" /><figcaption>Diagram 1</figcaption></figure>

(7) Moreover, if $X$ is compact and Hausdorff, for all $A \subset X$, $\overline{\downarrow A} \subset \overline{\downarrow A}$ and, for all $f: X \to [0, 1]$, $\overline{\downarrow f} \le \underline{\downarrow f}$.

To prove **Lemma 5.1.2**, we need to prove some lemmas first.

First, from **Lemma 5.1.3**, we can deduce that (1), (1 bis), (1 ter) and (2 bis) are respectively equivalent to (5), (5 bis), (5 ter) and (6 bis), and we can prove (3) and (4).

**Lemma 5.1.3.**

(1) For all $A \subset X$, $\overline{1_A} = \overline{1_A}$, $\hat{1_A} = \hat{1_A}$, $\downarrow 1_A = \downarrow_{\subset A}$ and $\uparrow 1_A = \uparrow_{\subset A}$, so:

(1.a) A is open if and only if $1_A$ is lower semi-continuous,

(1.b) A is closed if and only if $1_A$ is upper semi-continuous,

(1.c) A is upward closed if and only if $1_A$ is non-decreasing,

(1.d) A is downward closed if and only if $1_A$ is non-increasing.

(2) For all $f: X \to [0, 1]$, $f = \bigvee_{q \in [0,1]} \mathbf{1}_{f^{-1}((q,1])} \div (1 \div q)$.
*Proof.* Point 1 is obvious.

Let $f: X \to [0, 1]$.

For all $q \in [0,1]$ and $x \in X$, if $\mathbf{1}_{f^{-1}((q,1])}(x) = 1$, then $x \in f^{-1}((q,1])$, so $f(x) > q = \mathbf{1}_{f^{-1}((q,1])} \doteq (1 \doteq q)$, so $f \ge \mathbf{1}_{f^{-1}((q,1])} \doteq (1 \doteq q)$. For all $x \in X$ and $q < f(x)$, $\mathbf{1}_{f^{-1}((q,1])}(x) \doteq (1 \doteq f(x)) = q$, so $f(x) = \bigvee_{q \in [0,1]} \mathbf{1}_{f^{-1}((q,1])} \doteq (1 \doteq q)$. $\square$

Second, we prove (1), (1 bis), (1 ter), (2), (2 bis) and (6) thanks to **Lemma 5.1.4**.

**Lemma 5.1.4.**

(1) For all $A$ and $B \subset X$, $\uparrow A \subset B^c \Leftrightarrow A \subset (\downarrow B)^c$.

(2) If $X$ is compact Hausdorff, for all $F \subset X$ closed, $\uparrow F$ is closed.

(3) if $X$ is compact and Hausdorff, $LSC(X) = \{\bigvee A, A \subset C^0(X)\}$.

*Proof.* (1) Assume that $\uparrow A \subset B^c$ and let $x \in A$. For all $y \in B$, if $x \le y$, then $y \in \uparrow A$ and so $y \in B^c$. Hence $x \in (\downarrow B)^c$.

Assume that $A \subset (\downarrow B)^c$ and let $x \in \uparrow A$. There exists $y \in A$ such that $x \ge y$. If $x \in B$, then $y \in \downarrow A$ and then $y \notin A$. Hence $x \in B^c$.

(2) Let $F \subset X$ closed. Denote by $\pi_1$ the projection on the first coordinate from $X^2$ to $X$. $\uparrow F = \pi_1(\ge \cap (X \times F))$. $\ge$ is closed in $X^2$ which is compact so $\ge$ is itself compact, and thus $X \times F$ is also compact. Since $\pi_1$ is continuous, $\uparrow F$ is compact and thus closed in $X$.

(3) According to **Lemma 2.3.19**, if we denote by $X^{op}$ the opposite order of $X$, $USC(X^{op}) = \{\bigwedge A, A \subset C^0(X)\}$, which is actually $LSC(X) = \{\bigvee A, A \subset C^0(X)\}$. $\square$

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

*Proof of Lemma 5.1.2.* We only have to prove (1), (1 bis), (1 ter), (2), (2 bis), (6) and (7) thanks to **Lemma 5.1.3**. As an example of application of **Lemma 5.1.3**, we also prove (3).

(1): Let $A \subset X$. Let $U = (\downarrow A)^c$.

$\downarrow A \subset \overline{\downarrow A}$, so $U = (\overline{\downarrow A})^c \subset (\downarrow A)^c$, which gives, according to **Lemma 5.1.4 1**, $\uparrow U \subset A^c$. By hypothesis, $\uparrow U \subset \overline{(A^c)} = (\bar{A})^c$. Thanks to **Lemma 5.1.4 1**, $U \subset (\downarrow \bar{A})^c$, and so $\downarrow \bar{A} \subset \overline{\downarrow A}$.

(1 bis): Let $U \subset X$ be open.

($\uparrow U)^c \subset (\uparrow U)^c$, so, according to **Lemma 5.1.4 1** applied to the opposite order, $\downarrow ((\uparrow U)^c) \subset U^c$, and thus $\downarrow ((\uparrow U)^c) \subset \downarrow ((\uparrow U)^c) \subset U^c$, by hypothesis. Hence $U \subset (\downarrow (\uparrow U)^c)^c$. Again by **Lemma 5.1.4 1**, $\uparrow U \subset (\overline{(\uparrow U)^c})^c$, i.e. $\overline{(\uparrow U)^c} \subset (\uparrow U)^c$.

(1 ter): Let $U \subset X$ be open. $(\overline{\uparrow U})^c \subset (\uparrow U)^c$, i.e. $(\uparrow U)^c$ is closed, i.e. $\uparrow U$ is open.

(2): Assume that $X$ is totally disconnected and that, for all clopen $C$, $\uparrow C$ is clopen. Then, for all $U \subset X$ open, $\uparrow U = \bigcup_{C \subset U \text{ clopen}} \uparrow C$, which is open.

(2 bis): Assume that $X$ is compact, Hausdorff and intuitionistic. For all clopen $C$ of $X$, $\uparrow C$ is open, and, thanks to **Lemma 5.1.4 2**, $\uparrow C$ is also closed.

(3): If, for all $f: X \to [0,1]$, $\downarrow \bar{f} \le \overline{\downarrow f}$, then, for all $A \subset X$, $\mathbf{1}_{\downarrow A} = \downarrow \overline{\mathbf{1}_A} \le \overline{\downarrow \mathbf{1}_A} = \mathbf{1}_{\overline{\downarrow A}}$, so $\overline{\downarrow A} \subset \mathbf{1}_{\overline{\downarrow A}}$.

Assume now that, for all $A \subset X$, $\downarrow \bar{A} \subset \mathbf{1}_{\overline{\downarrow A}}$ and let $f: X \to [0,1]$. Since $\downarrow$ and $\overline{\downarrow}$ preserve upper bounds, and commute with subtraction of constants,
$$
\begin{align*}
\downarrow \bar{f} &= \bigvee_{q \in [0,1]} \downarrow \overline{\mathbf{1}_{f^{-1}((q,1))} \cdot (1 \div q)} \\
&= \bigvee_{q \in [0,1]} \downarrow \overline{\mathbf{1}_{f^{-1}((q,1))}} \div (1 \div q) \\
&= \bigvee_{q \in [0,1]} \mathbf{1}_{\downarrow f^{-1}((q,1))} \div (1 \div q) \\
&\leq \bigvee_{q \in [0,1]} \mathbf{1}_{\downarrow f^{-1}((q,1))} \div (1 \div q) \\
&= \bigvee_{q \in [0,1]} \overline{\downarrow \mathbf{1}_{f^{-1}((q,1))}} \div (1 \div q) \\
&= \bigvee_{q \in [0,1]} \overline{\downarrow \mathbf{1}_{f^{-1}((q,1))}} \div (1 \div q) \\
&= \overline{\downarrow f}
\end{align*}
$$

(6): According to **Lemma 5.1.4 3**, for all $f \in LSC(X)$, $f = \bigvee_{\substack{g \in C^0(X) \\ g \le f}} g$, so $\uparrow f = \bigvee_{\substack{g \in C^0(X) \\ g \le f}} \uparrow g$,
which is lower semi-continuous by **Lemma 5.1.4 3** and because, for all $g \in C^0(X)$,
$\uparrow g \in C^0(X) \subset LSC(X)$.

(7): The two conclusions of (7) are equivalent, thanks to **Lemma 5.1.3**. Let us prove the first one.
Assume $X$ is compact and Hausdorff. Let $A \subset X$.

$\bar{A}$ is closed, so, according to **Lemma 5.1.4 2**, $\uparrow \bar{A}$ is also closed. Since $\uparrow A \subset \uparrow \bar{A}$, $\uparrow \bar{A} \subset \uparrow \bar{A}$. $\square$

**Corollary 5.1.5.** For all compact Hausdorff ordered topological space $X$ such that the upward closure of an open is open, and $f \in C^0(X)$, $\uparrow f$ is the smallest non-decreasing upper semi-continuous function greater than $f$.

*Proof.* Let $X$ be an compact Hausdorff ordered topological space $X$ such that the upward closure of an open is open and $f \in C^0(X)$. According to **Lemma 5.1.2 4** and 6 bis, $\uparrow f$ is continuous and thus upper semi-continuous. Moreover, for all non-decreasing upper semi-continuous function $g \ge f$, since $g$ is non-decreasing, $g \ge \uparrow f$, which proves the corollary. $\square$

## 5.2. Algebraic axiomatisation of IC-algebras.
We are here aiming at an axiomatisation of the class of USC($\mathcal{L}$) for $\mathcal{L}$ a locale.

**Notation 5.2.1.** We remind the reader of **Notation 2.3.15**: for all ordered topological space $(X, \le)$, we denote by $C_{\searrow}^0(X)$ the set of continuous increasing functions from $X$ to $[0, 1]$, by $C^0(X)$ the set of continuous functions from $X$ to $[0, 1]$ and by $USC_{\nearrow}(X)$ the set of non-decreasing upper semi-continuous functions from $X$ to $[0, 1]$.

**Definition 5.2.2.** We denote by $\mathbf{IC}$ the class whose elements are the $USC(\mathcal{L})$ for $\mathcal{L}$ a locale and call these algebras *Ituitionnistic Continuous Algebras*.

5.2.1. *Review of the algebra USC(*$\mathcal{L}$*)*. In the case where $\mathcal{L}$ is a locale, $USC(\mathcal{L})$ has nicer properties (Theorem 5.2.3).

Let $\mathcal{L}$ be a locale. $\mathcal{L}$ is a commutative residuated complete lattice, so $USC(\mathcal{L})$ has an $\mathcal{L}$-structure.
The lower bounds of two upper semi-continuous functions is simply taken pointwise and the sum
and difference of two upper semi-continuous functions $f$ and $g$ from $\mathcal{L}$ to $[0, 1]$ are

$$f \dot{+} g: [0, 1] \to \mathcal{L} \quad \text{and} \quad f \div g: [0, 1] \to \mathcal{L}$$
$$q \mapsto \bigvee_{p<q} f(p) \wedge g(q \div p) \qquad q \mapsto \bigvee_{p<q} \bigwedge_{r \in [0,1]} g(r \div p) \to f(r)$$

The supremum of $f$ and $g \in USC(\mathcal{L})$ is given by, for all $q \in [0, 1]$, $(f \vee g)(q) = \bigvee_{p<q} f(p) \wedge g(p)$.

As in **Lemma 2.3.22**, for all $f \in USC(\mathcal{L})$, $2f = f \circ \frac{1}{2}$ and $j_*(f) = f \circ j$. $f \mapsto \frac{1}{2}$ and $f \mapsto j(f)$ are respectively left adjoint to $j_*$ and $2$.

**Theorem 5.2.3.** Let $\varphi[v]$ and $\psi[v]$ be terms in the language $(USC([0, 1]_u^n))_{n \in \mathbb{N}}$.

Then, if $[0, 1] \models \varphi \leq \psi$, $USC(\mathcal{L}) \models \varphi \leq \psi$.

*Proof.* Assume $[0, 1] \models \varphi \leq \psi$ and let $f: \mathcal{V} \to USC(\mathcal{L})$.

*Remark 2.3.2* implies that for all $p: \mathcal{V} \to [0, 1]$, $a_\varphi(p_v) = \varphi[p] \leq \psi[p] = a_\psi(p_v)$, so $a_\varphi \leq a_\psi$.

According to *Remark 2.3.2* and **Lemma 2.3.6**,

$$\varphi[f] = a_{\varphi}(f_v) \leq a_{\psi}(f_v) = \psi[f].$$

□

**Corollary 5.2.4.** Let $\mathcal{L}$ be a commutative residuated complete lattice. The following assertions are equivalent:

(1) For all $f \in USC(\mathcal{L})$, $2f = f \dot{+} f$.

(2) $\mathcal{L}$ is a locale.

*Proof.* We remind the reader that the order on $USC(\mathcal{L})$ is the reverse pointwise order.

If $USC(\mathcal{L}) \models 2v \geq v \dot{+} v$, then, according to **Theorem 2.2.19**, $\mathcal{L} \models v \leq v \otimes v$ and, if $\mathcal{L} \models v \leq v \otimes v$, then, according to **Theorems 2.2.15 and 2.4.3**, $USC(\mathcal{L}) \models v \geq \frac{v \dot{+} v}{2}$, which is equivalent to $USC(\mathcal{L}) \models 2v \geq v \dot{+} v$.

Moreover, in a commutative residuated complete lattice, $v \leq v \otimes v$ and $u \wedge v = u \otimes v$ are equivalent. Indeed, the latter obviously implies the former, and, if for all $V \in \mathcal{L}$, $V \leq V \otimes V$, then for all $U$ and $V \in \mathcal{L}$, $U \wedge V \leq (U \wedge V) \otimes (U \wedge V) \leq U \otimes V$, so, since $U \otimes V \leq U \otimes \top = U$ and $U \otimes V \leq \top \otimes V = V$, $U \otimes V = U \wedge V$.

□

**Remark 5.2.1.** We end this subsection by noticing that, in the case where $\mathcal{L}$ is the topology $\mathcal{T}$ of a topological space $X$, this structure is the one induced by the $\mathcal{L}$-structure of $USC(X)$ through the bijection $USC(\mathcal{T}) \simeq USC(X)$.

5.2.2. *The caracterisation.* Here comes the list of axioms that are satisfied by every *IC*-algebra, by **Theorem 5.2.3**.

(1) $(\vee, \wedge, \dot{+}, \div, \underline{0}, \underline{1})$ is a bounded commutative residuated lattice structure, as in (1).

(2) $2, \frac{1}{2}, j_*, j$ and $\alpha$ don't decrease.

(3) The adjunctions, as in (3).

(4) Defining axioms:

(4.f.2) and (4.f.2') $v \dot{+} v \leq 2v$, (4.b.1) and (4.b.2), (4.c.1) and (4.c.2), (4.d.1) and (4.d.2), (4.e.1) and (4.e.2), (4.f.1), (4.g) LÀ (et les règles de déduction)

(5) And the algebra of values is $[0, 1]$ to infinitesimals, as in (5).

We denote by $T_{\text{int}}$ the previous theory.
**Theorem 5.2.5.** *T*<sub>int</sub> and *T* ∪ {2*v* ≥ *v*÷*v*} are equivalent theories.

*Proof.* T<sub>int</sub> = (T \ {2(u÷v) ≤ 2u÷2v, 2u÷2v ≤ 2(u÷v)}) ∪ {2v = v÷v}, so T ∪ {2v ≥ v÷v} implies T<sub>int</sub>.

Moreover, (T \ {2(u÷v) ≤ 2u÷2v, 2u÷2v ≤ 2(u÷v)}) ⊢ 2v = v÷v ⇒ 2(u÷v) = 2u÷2v, so
T<sub>int</sub> ⊢ 2(u÷v) = 2u÷2v, so T<sub>int</sub> implies T.
□

**Corollary 5.2.6.** For all model *A* of *T*<sub>int</sub>, there exists a locale *L* such that the quotient of the Macneille completion of *A* by ≃ is isomorphic to USC(*L*).

For all model A of T<sub>int</sub>, there exists a locale L such that the quotient of A by ≃ embeds into USC(L).

*Proof.* Let *A* be a model of *T*<sub>int</sub>. *A* is a model of *T*, so, according to **Theorem C**, there exists a commutative residuated complete lattice *L* such that the quotient of the Macneille completion of *A* by ≃ is isomorphic to USC(*L*). Since, in *A*, ⊗ = ∨, in its Macneille completion, this identity is still true. Hence it is also true in the quotient and thus in USC(*L*). **Theorem 2.2.19** ensures that, for all *U* and *V* ∈ *L*, *U* ⊗ *V* = *U* ∧ *V*. Hence *L* is a locale.

This construction gives us a function $i$ from $A$ to $\mathcal{U}SC(\mathcal{L})$ such that, for all $a$ and $b \in A$, $i(a) = i(b) \Leftrightarrow a \simeq b$. Hence, the image of $i$ is the quotient of $A$ by $\simeq$, which proves that the quotient of $A$ by $\simeq$ embeds into $\mathcal{U}SC(\mathcal{L})$. $\square$

**Corollary 5.2.7.** For all *L*-terms *φ* and *ψ*, the following assertions are equivalent:

(1) For all locale $\mathcal{L}$, $\mathrm{USC}(\mathcal{L}) \models \varphi \le \psi$.

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

*Proof.* For all locale *L*, USC(*L*) is a model of **T** ∪ {2*v* ≥ *v*÷*v*}, which is equivalent to **T**<sub>int</sub>, so USC(*L*) is a model of **T**<sub>int</sub>. By Archimedeanity of every IC-algebra, we have that 2 implies 1.

Let $\varphi$ and $\psi$ be $\mathcal{L}$-terms both having $k$ free variables such that, for all locale $\mathcal{L}$, $\mathrm{USC}(\mathcal{L}) \models \varphi \le \psi$.

Let $n \in \mathbb{N}$. Let $A$ be a model of $\mathbf{T}$. According to **Corollary 5.2.6**, there exists a commutative residuated lattice $\mathcal{L}$ and a morphism $i: A \to \mathcal{U}SC(\mathcal{L})$ 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}$.

$$
\varphi(a) \le \psi(a) + \frac{1}{2^n}.
$$

The class of models of $\mathbf{T}$ being complete for $\mathbf{T}$, $\varphi \le \psi + \frac{1}{2^n}$ is consequence of $\mathbf{T}$.

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

**Corollary 5.2.8.** Let $\mathcal{L}' = \{\dot{+}, \dot{-}, \wedge, \vee, \dot{\frac{1}{2}}, \overline{1}, \underline{0}\}$ and write $2v$ for $v\dot{+}v$, $j(v)$ for $(v \div \frac{1}{2}) \dot{+} (v \div \frac{1}{2})$, $j_*(v)$ for $v\dot{+}\frac{1}{2}$ and $\alpha(v)$ for $\frac{v}{2} \vee ((v \div \frac{1}{2}) \dot{+} (v \div \frac{1}{2}))$. Let $\mathbf{T}'_{\text{int}}$ be the following theory in the language $\mathcal{L}'$.

(1) $(\forall, \wedge, \dot{+}, \dot{-}, \overline{0}, \underline{1})$ is a bounded commutative residuated lattice structure, as in (1).

(2) $\frac{1}{2}$ is non-decreasing.

(3) **The adjunctions:** (3) and (3.a.2') $\frac{v}{2} + \frac{v}{2} \le v$

(4) Defining axioms:

(4.d.1), (4.e.1)

(5) And the algebra of values is [0, 1] to infinitesimals, as in (5).

For all locale *L*, USC(*L*) is a model of *T*'<sub>*int*</sub>.

$a \preceq b \Leftrightarrow \forall n \in \mathbb{N} a \le b + \frac{1}{2^n}$ defines a preorder on every model of $\mathbf{T}'_{\text{int}}$.
For all model A of $T'_{int}$, there exists a locale $\mathcal{L}$ such that the quotient of the Macneille completion of A by the equivalence relation induced by the preorder $\leq$ is isomorphic to USC($\mathcal{L}$).

For all model A of $T'_{int}$, there exists a locale $\mathcal{L}$ such that the quotient of A by the equivalence relation induced by the preorder $\leq$ embeds into USC($\mathcal{L}$).

For all $\mathcal{L}$-terms $\varphi$ and $\psi$, if, for all locale $\mathcal{L}$, USC($\mathcal{L}$) $\models \varphi \leq \psi$, then for all $n \in \mathbb{N}$, $\varphi \leq \psi \dot{+} \frac{1}{2^n}$ is consequence of $T'_{int}$.

**Proof.** First, for all locale $\mathcal{L}$, by **Theorem 5.2.3**, USC($\mathcal{L}$) is a model of $T'_{int}$.

Second, let A be a model of $T'_{int}$.

**Claim:** By defining $2, j, j_*$ and $\alpha$ by $2v = v+v, j(v) = (v \div \frac{1}{2}) \div (v \div \frac{1}{2})$, $j_*(v) = v+\frac{1}{2}$ and $\alpha(v) = \frac{v}{2} \lor ((v \div \frac{1}{2}) \div (v \div \frac{1}{2}))$, A is a model of $T_{int}$.

Since every model of $T'_{int}$ is a model of $T_{int}$, according to **Corollary 5.2.6:**

For all model A of $T'_{int}$, there exists a locale $\mathcal{L}$ such that the quotient of the Macneille completion of A by the equivalence relation induced by the preorder $\leq$ is isomorphic to USC($\mathcal{L}$).

For all model A of $T'_{int}$, there exists a locale $\mathcal{L}$ such that the quotient of A by the equivalence relation induced by the preorder $\leq$ embeds into USC($\mathcal{L}$).

Since $T_{int}$ and $T'_{int}$ have same Archimedean models, from **Corollary 5.2.7**, we deduce that, for all $\mathcal{L}$-terms $\varphi$ and $\psi$, if, for all locale $\mathcal{L}$, USC($\mathcal{L}$) $\models \varphi \leq \psi$, then for all $n \in \mathbb{N}$, $\varphi \leq \psi \dot{+} \frac{1}{2^n}$ is consequence of $T'_{int}$.

**Proof of the claim:** The axioms of $T_{int}$ that aren't in $T'_{int}$ are the following ones:

(1) $2, j, j_*$ and $\alpha$ are non-decreasing. (2)

(2) (4.a), (4.c) and (4.f).

(3) (4.b), (4.d.2), (4.e.2) and (4.g).

The first two points are obviously satisfied by A. Let us prove the third one. Let $a$ and $b \in A$.

(4.b): Notice first that, for all $x$ and $y \in A$, since $2(\frac{x}{2}+\frac{y}{2}) = x+y$, $\frac{x+y}{2} \leq \frac{x}{2}+\frac{y}{2}$. Hence, $j_*(2a+b) = \frac{2a+b}{2}+\frac{1}{2} \leq \frac{2a}{2}+\frac{b}{2}+\frac{1}{2} \leq a+\frac{b}{2}+\frac{1}{2} = a+j_*(b)$.

Then, notice that, thanks to (3.b.1) and (3.b.2), $\forall x$ and $y \in A$ $j_*(2x+y) \geq x+j_*(y)$ is equivalent to $\forall x$ and $y \in A$ $2x+j(y) \geq j(x+y)$. We prove that $j(a+b) \leq 2a+j(b)$:

$$j(a \div b) = 2 \left( (a \div b) \div \frac{1}{2} \right) \leq 2 \left( \left( b \div \frac{1}{2} \right) \div a \right) = j(b) \div 2a.$$

(4.d.2): $\alpha(2a \land j_*(a)) = \frac{2a \land j_*(a)}{2} \lor j(2a \land j_*(a)) \leq \frac{2a}{2} \lor j \circ j_*(a) \leq a$.

(4.e.2): $2\alpha(a) \geq 2\frac{a}{2} \geq a$ and $j_* \circ \alpha(a) \leq j_* \circ j(a) \geq a$.

(4.g): First, let us notice that $j_*(\emptyset) = \frac{1}{2}$ and, for all $x \in A$ such that $x \leq \frac{1}{2}$, $\alpha(x) = \frac{x}{2} \lor 2(x \div \frac{1}{2}) = \frac{x}{2}$, so, for all $n \in \mathbb{N}$, $\alpha^n \circ j_*(\emptyset) = \frac{1}{2^n}$. Hence, for all $n \in \mathbb{N}^*$, using (3.a.2'), $\alpha^n \circ j_*(\emptyset) \div \alpha^n \circ j_*(\emptyset) = 2\frac{1}{2^n} \leq \frac{1}{2^{n-1}} = \alpha^{n-1} \circ j_*(\emptyset)$. $\square$

**5.3. Equivalence between IC-algebras and MC-algebras.** The aim of this section is to prove **Theorem 5.3.8** and its **Corollary 5.3.9**.

**Notation 5.3.1.** First of all, let's denote by $\mathcal{L}_M$ the language of [1, pp. 1404-1405], in which $\oplus$ is replace by $+$ and to which is added the symbol $\div$. Let us also denote by $T_M$ the theory of [1, pp.
1404-1405], to which are added the following two axioms:

$$a \leq (a \div b) \dot{+} b \text{ and } (a \dot{+} b) \div b \leq a.$$

Following [38], we give the following definitions.

**Definition 5.3.2.** Let $(X, \leq)$ be an ordered topological space. We recall that $X$ is Hausdorff if $\leq$ is closed (cf. **Definition 2.3.16**).

$X$ is intuitionistic if, for all open subset $U$ of $X$, $\uparrow U$ is open.

**Definition 5.3.3.** MC-algebras are defined in [1, pp. 1404-1405] and we define $d$ on any MC-algebra $A$, as in [1, Definition 6.1], by

$$\forall f \text{ and } g \in A \ d(f,g) = (\bigwedge \{q \in [0,1] | f \leq g \dot{+} q\}) \lor (\bigwedge \{q \in [0,1] | g \leq f \dot{+} q\}).$$

Let us recall the definition of Archimedeanity and Cauchy-completeness for MC-algebras ([1, Definitions 6.2 and 6.4]).

Let $A \in \mathbf{MC}$. We say that $A$ is Archimedean if, for all $f$ and $g \in A$, $d(f,g) = 0 \Rightarrow f = g$.

Let $(a_n)_n \in \mathbb{N}$ be a sequence in $A$, and let $a \in A$. The sequence $(a_n)_n \in \mathbb{N}$ is called a Cauchy sequence if, for every $\varepsilon > 0$, there exists $k \in \mathbb{N}$ such that for all $n, m \geq k$, $d(a_n, a_m) < \varepsilon$. The sequence $(a_n)_n \in \mathbb{N}$ is said to converge to $a \in A$, or that $a$ is a limit of $(a_n)_n \in \mathbb{N}$, if for every $\varepsilon > 0$, there exists $n_0 \in \mathbb{N}$ such that for all $m \geq n_0$, $d(a_m, a) < \varepsilon$. The sequence $(a_n)_n \in \mathbb{N}$ is said to converge if there exists $b \in A$ such that $(a_n)_n \in \mathbb{N}$ converges to $b$. The set $A$ is said to be Cauchy-complete if every Cauchy sequence in $A$ converges.

An MC-algebra $A$ is said intuitionistic when $\dot{+}$ admits a residual.

Intuitionistic ordered spaces and MC-algebras are linked by the following duality theorem.

**Theorem 5.3.4.** ([1, Theorem 8.5.]). The map that assigns to every ordered topological space $X$ the algebra $C_{\lambda}^{0}(X)$ gives rise to an equivalence of categories between the opposite of the category of compact Hausdorff ordered topological spaces with monotone continuous maps and the category of Cauchy-complete Archimedean MC-algebras.

We denote by $Sp(A)$ the compact Hausdorff ordered topological space thus associated to an MC-algebra $A$.

**Theorem 5.3.5.** ([38, Proposition 1.3.23.]). The category of intuitionistic Archimedean Cauchy-complete MC-algebras is equivalent to the opposite of the category of compact Hausdorff intuitionistic ordered spaces.

**Lemma 5.3.6.** Let $A$ be an MC-algebra.

$A$ is Archimedean if and only if, for all $f$ and $g \in A$ and $\forall n \in \mathbb{N} \ f \leq g \dot{+} \frac{1}{2^n} \Rightarrow f \leq g$.

*Proof.* Let $f$ and $g \in A$.

Assume that $A$ is Archimedean and, for all $n \in \mathbb{N}$, $f \leq g \dot{+} \frac{1}{2^n}$. Then, $\bigwedge \{q \in [0,1] | f \leq f \land g \dot{+} q\} = \bigwedge \{q \in [0,1] | f \land g \leq f \dot{+} q\} = 0$, so $d(f, f \land g) = 0$ and thus, since $A$ is Archimedean, $f = f \land g$, i.e. $f \leq g$.

Conversely, assume that, for all $h$ and $k \in A$, $\forall n \in \mathbb{N} \ h \leq k \dot{+} \frac{1}{2^n} \Rightarrow h \leq k$ and that $d(f, g) = 0$.

Then, for all $n \in \mathbb{N}$, $f \leq g \dot{+} \frac{1}{2^n}$ and $g \leq f \dot{+} \frac{1}{2^n}$, so $f \leq g$ and $g \leq f$, i.e. $f = g$. $\square$

**Definition 5.3.7.** For all locale $\mathcal{L}$, let's define $\odot$ by, for all $a$ and $b \in \mathrm{USC}(\mathcal{L})$, $a \odot b = j(\frac{a}{2} \dot{+} \frac{b}{2})$. We also define the theory $\mathbf{T}_{\mathrm{Mint}}$ as the theory $\mathbf{T}_{\mathrm{M}}$ in which all terms of the form $u \odot v$ have been replaced by $j(\frac{u}{2} \dot{+} \frac{v}{2})$.

**Theorem 5.3.8.**

(1) For all locale $\mathcal{L}$, $\mathrm{USC}(\mathcal{L})$ is an MC-algebra.
(2) Let $X$ be an ordered topological space. There exists a topological space $Y$ and an embedding of $C_{\nearrow}^0(X)$ in $USC(Y)$ for the language $\{\leq, \dot{+}, \odot, \wedge, \vee, (q)_q \in [0,1], \frac{1}{2}\}$.

Moreover, if $X$ is intuitionistic, then $C_{\nearrow}^0(X)$ is intuitionistic and this embedding also preserves $\dot{+}$.

**Proof.** (1) The theory of MC-algebras is satisfied by $[0,1]$ ([1, p. 1404]). Moreover, this theory is given in a language only having upper semi-continuous functions and every axiom is of the form $\varphi \leq \psi$ with $\varphi$ a term of $(USC([0,1]_u^n))_n \in \mathbb{N}$. Thus, by **Theorem 5.2.3**, every axiom of the theory of MC-algebras is also satisfied by every IC-algebra.

(2) Let $(X, \mathcal{T})$ be an ordered topological space.
We recall that, we denote by $X_u$ the set $X$ endowed with the topology $\{U \in \mathcal{T} | U$ is downward closed $\}$, and that $USC_{\nearrow}(X) = USC(X_u)$ (**Lemma 2.3.17**). Therefore, we prove that $C_{\nearrow}^0(X)$ embeds into $USC_{\nearrow}(X)$.

For all $f \in C_{\nearrow}^0(X)$, $f$ is non-decreasing and upper semi-continuous, so $f \in USC_{\nearrow}(X)$. That gives a natural order embedding of $C_{\nearrow}^0(X)$ into $USC_{\nearrow}(X)$, and this injection preserves all the punctual operations, namely $\dot{+}, \odot, \vee, \wedge, \frac{1}{2}, j_*$, $j$ and $\alpha$, and the constants.

Assume now that $X$ is intuitionistic and let $f$ and $g \in C_{\nearrow}^0(X)$.

Let $f \doteq g$: $X \to [0,1]$ and let's denote by $\ominus$ the residual of $\dot{+}$ in $USC_{\nearrow}(X)$.
$x \mapsto f(x) \doteq g(x)$

According to **Lemma 5.1.2 (4)** and (6 bis), $\uparrow (f \doteq g) \in C_{\nearrow}^0(X)$, and, for all $h \in C_{\nearrow}^0(X)$, $\uparrow (f \doteq g) \leq h \Leftrightarrow f \doteq g \leq h \Leftrightarrow f \leq g \dot{+} h$.

Hence $(f,g) \mapsto \uparrow (f \doteq g)$ is the residual of $\dot{+}$.

However, according to **Corollary 5.1.5**, $\uparrow (f \doteq g)$ is the smallest upper-semicontinuous non-decreasing function from $X$ to $[0,1]$ greater than $f \doteq g$, that-is-to-say, for all $h \in USC_{\nearrow}(X)$, $\uparrow (f \doteq g) \leq h \Leftrightarrow f \doteq g \leq h$ and $\uparrow (f \doteq g) \in USC_{\nearrow}(X)$. Hence $\uparrow (f \doteq g) \leq h \Leftrightarrow f \leq g \dot{+} h$ and $\uparrow (f \doteq g) \in USC_{\nearrow}(X)$. Hence $\uparrow (f \doteq g) = f \ominus g$. Thus, the embedding preserves the residuals.
$\square$

**Corollary 5.3.9.** The class of intuitionistic MC-algebras is stable under Macneille completion.

**Corollary 5.3.10.** $T_{int}$ is a conservative extension of $T_{Mint}$ in the following sense:
For all terms $\varphi$ and $\psi$ in the language $\mathcal{L}_M$, for all $n \in \mathbb{N} \varphi \leq \psi + \frac{1}{2^n}$ is a theorem of $T_{int}$, if and only if for all $n \in \mathbb{N} \varphi \leq \psi + \frac{1}{2^n}$ is a theorem of $T_{Mint}$.

**Proof.** Let $X$ be an ordered topological space. Let $X_u$ be the topological space of the **proof of Theorem 5.3.8**.

According to **Theorem 5.3.8 2**, $C_{\nearrow}^0(X) \to USC(Y)$ is an embedding for the language $f \mapsto f$
$\{\dot{+}, \odot, \wedge, \vee, (q)_q \in [0,1], \frac{1}{2}\}$. Hence, for all terms of arity $k \varphi[v]$ and $\psi[v]$ in the language $\mathcal{L}_M$, if for all $n \in \mathbb{N} \varphi \le \psi + \frac{1}{2^n}$ is a theorem of $T_{int}$, then, for all $f \in C_{\nearrow}^0(X)^k$, since $\varphi[f] \le \psi[f]$ in $USC(Y)$, $\varphi[f] \le \psi[f]$ in $C_{\nearrow}^0(X)$, so, for all $n \in \mathbb{N} \varphi \le \psi + \frac{1}{2^n}$ is a theorem of $T_{Mint}$.

Conversely, for all locale $\mathcal{L}$, for all terms of arity $k \varphi[v]$ and $\psi[v]$ in the language $\mathcal{L}_M$, if for all $n \in \mathbb{N} \varphi \le \psi + \frac{1}{2^n}$ is a theorem of $T_{Mint}$, then, since $USC(\mathcal{L}) \models T_{Mint}$, for all $f \in USC(\mathcal{L})^k$, $\varphi[f] \le \psi[f]$, so, for all $n \in \mathbb{N} \varphi \le \psi + \frac{1}{2^n}$ is a theorem of $T_{int}$.
$\square$

Hence we can finally conclude by stating the following theorem.
**Theorem 5.3.11.** Both the classes of intuitionistic MC-algebras and IC are sound for both theories $T_{int}$ and $T_M$.

Moreover, for all $\mathcal{L}$-terms $\varphi$ and $\psi$, the following assertions are equivalent:

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

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

(3) For all locale $\mathcal{L}$, $USC(\mathcal{L}) \models \varphi \le \psi$.

(4) For all topological space $X$, $C_{\lambda}^{0}(X) \models \varphi \le \psi$.

**5.4. Reduction of the axiomatisation of USC($\mathcal{L}$) to the axiomatisation of USC($X$).**
This subsection aims at proving that the class of IC-algebras and the class of all the $USC(X)$ for $X$ a topological space have same theory in the language $(USC([0, 1]^n))_{n \in \mathbb{N}}$ and that the class of IC-algebras and the class of Cauchy-complete Archimedean MC-algebra have same theory in the language $(C_{\lambda}^0([0, 1]))_{n \in \mathbb{N}}$. The first subsubsection is dedicated to defining the action of $(C_{\lambda}^0([0, 1]))_{n \in \mathbb{N}}$ on every Cauchy-complete Archimedean MC-algebra.

**5.4.1.** The action of all continuous functions from $[0, 1]$ to $[0, 1]$ on $USC(\mathcal{L})$. Before getting to the heart of the matter, we need some notations.

**Notation 5.4.1.** We recall here that the topology of $[0, 1]$ is denoted $\mathcal{T}_u$ and the topology of $[0, 1]^n$ is denoted $\mathcal{T}_{u,n}$, for all $n \in \mathbb{N}$ (2.1.1).

**Theorem 5.4.2.** (MC version of Theorem 2.3.26).

Let $A$ be a Cauchy-complete Archimedean MC-algebra.

There exists a unique family of continuous functions $(\cdot : C_{\lambda}^{0}([0, 1]^n) \to C^0(A^n, A))_{n \in \mathbb{N}}$ that is associative in the sense that, for all $a \in C_{\lambda}^0([0, 1]^n)$ and $(b_1, \dots, b_n) \in \prod_{i=1}^n C_{\lambda}^0([0, 1]^{k_i})$ and $(f_{i,1}, \dots, f_{i,k_i})_{i \in [1,n]} \in A^{\sum_{i=1}^n k_i}$,

$$ (a \circ (b_1, \dots, b_n)) \cdot (f_{1,1}, \dots, f_{n,k_n}) = a \cdot (b_1 \cdot (f_{1,1}, \dots, f_{1,k_1}), \dots, b_n \cdot (f_{n,1}, \dots, f_{n,k_n})) $$

and, for all $(f,g) \in A^2$:

(1) $\vee \cdot (f,g) = f \vee g$

(2) $\wedge \cdot (f,g) = f \wedge g$

(3) $\dot{\vee} \cdot (f,g) = f \dot{\vee} g$

(4) $\odot \cdot (f,g) = f \odot g$

Moreover, $\cdot$ are isometries, and, if there exists an ordered topological space $X$ such that $A = C_{\lambda}^0(X)$, then for every $n \in \mathbb{N}$, $a \in C_{\lambda}^0([0, 1]^n)$ and $f \in C_{\lambda}^0(X)^n$ $a \cdot f = a \circ f$.

**Remark 5.4.1.** The previous theorem means that there is a unique structure of module on any MC-algebra over the operad $(C_{\lambda}^0([0, 1]^n))_{n \in \mathbb{N}}$.

The uniqueness of such a family follows from a Stone-Weierstrass-type theorem, which can itself be seen as a corollary of **Theorem 2.3.23**.

**Theorem 5.4.3** (Stone-Weierstrass Theorem for MC-algebras, [1, Theorem 8.3]). Let $X$ be a preordered topological space, let $L$ be an MC-subalgebra of $C_{\lambda}^0(X)$, and suppose that, for every $x, y \in X$, if $x \not\ge y$ then there exists $\varphi \in L$ such that $\varphi(x) < \varphi(y)$.
If $X$ is compact, then, for every $\psi \in C_{\lambda}^{0}(X)$, there exists a sequence $(\psi_n)_n \in \mathbb{N}$ in $L$ uniformly converging to $\psi$.

**Corollary 5.4.4.** Let $n \in \mathbb{N}$.

$L_n = \{a \in C_{\lambda}^{0}([0, 1]^n) \mid a \text{ is a composition of } \vee, \wedge, \dot{+}, \odot, (d)_d \in [0,1] \text{ dyadic and the projections}\}$ is dense in $C_{\lambda}^{0}([0, 1]^n)$.

*Proof.* Let $n \in \mathbb{N}$. $L_n$ is stable by $\dot{+}, \vee, \wedge$, and $\odot$. Let $\overline{L}_n$ denote its uniforme closure. By continuity of $\dot{+}, \vee, \wedge$, and $\odot$, $\overline{L}_n$ is still stable by $\dot{+}, \vee, \wedge$, and $\odot$. Moreover, it contains all the constant functions. Therefore, $\overline{L}_n$ is an MC-algebra.

For all $x \preceq y \in [0, 1]^n$, there exists $i \in [1, n]$ such that $x_i < y_i$, and so the projection on the $i$-th coordinate, $\pi$ satisfies $\pi(x) < \pi(y)$. $\pi \in L_n$. Thanks to **Theorem 5.4.3**, $[0, 1]^n$ being compact, $\overline{L}_n$ is dense in $C_{\lambda}^{0}([0, 1]^n)$, i.e. $L_n$ is dense in $C_{\lambda}^{0}([0, 1]^n)$. $\square$

*Proof.* Proof of **Theorem 5.4.2**.

Let $A$ be a Cauchy-complete and Archimedean MC-algebra. **Theorem 5.3.4** allows to assume that there exists $X$ a compact Hausdorff ordered topological space such that $A = C_{\lambda}^{0}(X)$. Action of $(C_{\lambda}^{0}([0, 1]^n))_n \in \mathbb{N}$ on $C_{\lambda}^{0}(X)$ by composition satisfies points 1 to 4 of **Theorem 5.4.2**.

To prove the uniqueness part of **Theorem 5.4.2**, let $\cdot$ be a family of functions as in **Theorem 5.4.2**, $n \in \mathbb{N}$ and $a \in C_{\lambda}^{0}([0, 1]^n)$. There exists $(a_k)_k \in \mathbb{N} \in L_n^{\mathbb{N}}$ such that $a_k \to a$.

For all $k \in \mathbb{N}$, $a_k$ being a composition of elements of $\{\vee, \wedge, \dot{+}, \odot\}$ and of projections, since $\cdot$ preserves the composition, for all $f \in C_{\lambda}^{0}(X)^n$, $a_k \cdot f = a_k \circ f$. $\cdot$ being continuous, for all $f \in C_{\lambda}^{0}(X)^n$, $(a_k \cdot f) = \lim a_k \cdot f = \lim a_k \circ f = a \circ f$. $\square$

**5.4.2. The reduction.** The aim of this subsection is to prove the next theorem.

**Theorem 5.4.5.** For every $n \in \mathbb{N}$ and $a \in USC([0, 1]_u^n)$, if for all topological space $X$ and $f \in USC(X)^n$, $a \cdot f = \underline{0}$, then for all locale $\mathcal{L}$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = \underline{0}$.

An immediate corollary is the following one.

**Corollary 5.4.6.** For every $n \in \mathbb{N}$ and $a \in C_{\lambda}^{0}([0, 1]^n)$, if for all compact Hausdorff intuitionistic topological space $X$ and $f \in C_{\lambda}^{0}(X)^n$, $a \cdot f = \underline{0}$, then for all locale $\mathcal{L}$ and $f \in USC(\mathcal{L})^n$, $a \cdot f = \underline{0}$.

A tool lemma for this purpose is the following one.

**Lemma 5.4.7.** Any $\mathcal{L}$-morphism $F: USC(\mathcal{L}) \to USC(\mathcal{L}')$, where both $\mathcal{L}$ and $\mathcal{L}'$ are locales, is 1-Lipschitzian, and if $F$ is an embedding, $F$ is an isometry.

Thus, for all Cauchy-complete Archimedean MC-algebras $A$ and $B$ and all morphism of MC-algebras $F: A \to B$, $F$ is 1-Lipschitzian, and, if $F$ is an embedding, $F$ is an isometry.

*Proof.* For all $(f, g) \in USC(\mathcal{L})^2$ and $d \in [0, 1]$ dyadic, if $\|f \div g\| \le d$, then $f \div g \le \underline{d}$, and thus $F(f) \div F(g) = F(f \div g) \le F(\underline{d}) = \underline{d}$, which gives $\|F(f) \div F(g)\| \le d$. Thus, for all $(f, g) \in USC(\mathcal{L})^2$, $\|F(f) \div F(g)\| \le \|f \div g\|$, and then

$$d(F(f), F(g)) = \|F(f) \div F(g)\| \wedge \|F(g) \div F(f)\| \le \|f \div g\| \wedge \|g \div f\| = d(f, g).$$

If $F$ is an embedding, then, for all $(f, g) \in USC(\mathcal{L})^2$ and $d \in [0, 1]$ dyadic,

$$ \begin{align*} \|F(f) \div F(g)\| \le d &\Leftrightarrow F(f) \div F(g) \le \underline{d} \\ &\Leftrightarrow F(f \div g) \le F(d) \\ &\Leftrightarrow f \div g \le \underline{d} \\ &\Leftrightarrow \|f \div g\| \le d \end{align*} $$
which amounts to $\|F(f) \div F(g)\| = \|f \div g\|$.
Thus, for all $(f,g) \in USC(\mathscr{L})^2$,

$$d(F(f), F(g)) = \|F(f) \div F(g)\| \wedge \|F(g) \div F(f)\| = \|f \div g\| \wedge \|g \div f\| = d(f, g).$$

To prove the result for MC-algebras, thanks to **Theorem 5.3.4**, we just have to prove it for $C_{\div}^0(X)$ and $C_{\div}^0(Y)$, for $X$ and $Y$ compact ordered topological spaces. Let thus $F: C_{\div}^0(X) \to C_{\div}^0(Y)$ be a morphism of MC-algebras. By duality, it corresponds to a homeorphism from $Y$ to $\tilde{X}$ and thus extends to a morphism of AC-algebras $\tilde{F}: USC_{\div}(X) \to USC_{\div}(Y)$. It is thus 1-Lipschitzian. Moreover, if $F$ is an embedding, then so is $\tilde{F}$ and thus $\tilde{F}$ is an isometry and so is $F$.

□

**Corollary 5.4.8.** Let $A$ and $B$ be two Cauchy-complete Archimedean MC-algebras and $F: A \to B$ be a morphism of MC-algebras.

For all $a \in C_{\div}^0([0, 1]^n)$ and $f \in A$, $F(a \cdot f) = a \cdot F(f)$.

*Proof.* Let $a \in C_{\div}^0([0, 1]^n)$ and $f \in A$. There exists $(a_k)_{k \in \mathbb{N}} \in L_n^{\mathbb{N}}$ such that $a_k \to a$. For all $k \in \mathbb{N}$, $F(a_k \cdot f) = a_k \cdot F(f)$, so, since $F$ is continuous, $F(a \cdot f) = a \cdot F(f)$. □

*Proof.* Proof of **Theorem 5.4.5**.

Let $\mathscr{L}$ be a locale.

Since $USC(\mathscr{L})$ is a Cauchy-complete Archimedean MC-algebra, there exists a compact Hausdorff ordered topological space $X$ and an isomorphism of MC-algebras $i: USC(\mathscr{L}) \simeq C_{\div}^0(X)$ (**Theorem 5.3.4**). Moreover, there exists a topological space $Y$ and $i': C_{\div}^0(X) \to USC(Y)$ an embedding of $f \mapsto f$

MC-algebras. According to **Corollary 5.4.8**, $i$ and $i'$ preserves $b \cdot _-$, for all $b \in C^0([0, 1]^n, [0, 1])$. The lower bound of a family of continuous functions, if it exists, is the punctual lower bound. Hence, $i'$, as $i$, also preserves lower bounds. Thus, for all $a \in USC([0, 1]^n)$ and $f \in USC(\mathscr{L})^n$,

$$i' \circ i(a(f)) = i' \circ i \left( \bigwedge_{b \in C_{\div}^0(X) \atop b \ge a} b(f) \right) = \left( \bigwedge_{b \in C_{\div}^0(X) \atop b \ge a} b(i' \circ i(f)) \right) = a(i' \circ i(f)).$$

Thus, for all $a \in USC([0, 1]^n)$, if for all topological space $W$ and $f \in USC(W)$, $a \cdot f = \emptyset$, then, for all $f \in USC(\mathscr{L})^n$, $i' \circ i(a(f)) = a(i' \circ i(f)) = \emptyset$, which, by injectivity of $i' \circ i$, gives $a \cdot f = \emptyset$. □

**5.5. Cut Admissibility.** The language for sequent calculus in the intuitionistic case is the same as the one for **CFL<sub>ew</sub>**, recalled in the following table. We keep Notation 4.1.1.

<table><caption>FIGURE 4. Correspondence between structure symbols and $\mathscr{L}$</caption><thead><tr><th colspan="3">Positive symbols</th><th colspan="2">Negative correspondent</th></tr><tr><th>structures</th><th>formulas</th><th>algebraic correspondent</th><th>formulas</th><th>algebraic notation</th></tr></thead><tbody><tr><td>,</td><td>+</td><td>+</td><td>-</td><td>-</td></tr><tr><td>&epsilon;</td><td>0</td><td>0</td><td>1</td><td>1</td></tr><tr><td></td><td>&wedge;</td><td>&wedge;</td><td>&vee;</td><td>&vee;</td></tr><tr><td>&odot;<sub>2</sub></td><td>2</td><td>2</td><td>&ddot;<sub>2</sub></td><td>&ddot;<sub>2</sub></td></tr><tr><td>&bull;<sub>2</sub></td><td>j<sub>*</sub></td><td>j<sub>*</sub></td><td>j</td><td>j</td></tr><tr><td>&odot;<sub>&alpha;</sub></td><td>&alpha;</td><td>&alpha;</td><td>&#9633;<sub>&alpha;</sub></td><td>2v &wedge; j<sub>*</sub>(v)</td></tr></tbody></table>
<figure><img src="image_11.png" /><figcaption>FIGURE 5. LJK</figcaption></figure>

Here again, we use a system similar to **MGL** with several modalities. We need six modalities and three structural symbols $\circ_2$, $\bullet_2$ and $\circ_\alpha$. We thus obtain a system **MGL** ($\circ_2$, $\bullet_2$, $\circ_\alpha$) given by **GL** (from the **Appendix 8**) understood with contexts of the extended language and **Figure 2**. In addition to these rules, we add the structural rules given in **Figure 5** and call the total system **LJK**.

Since all the added rules are analytic (cf. **Definition 8.1.2**), according to **Theorems 8.1.12, 8.1.13, 5.2.5 and 5.3.11**, the **Theorems A and B** are true.

## 6. INVOLUTIVE CASE

In this section, we study the involutivity of the negation. We first prove that the negation of an AC-algebra is involutive if and only if this is the case for the negation of the underlying commutative residuated complete lattice (**Theorem 6.1.1**), which leads to an axiomatisation of these involutive AC-algebras. Finally, we give a sequent-style cut-free deductive system admitting the cut rule that describes involutive AC-algebras.

### 6.1. Involutive Continuous Algebras.

**Theorem 6.1.1.** Let $\mathcal{L}$ be a commutative residuated complete lattice. The negation of $\mathrm{USC}(\mathcal{L})$ is involutive if and only if so is the negation of $\mathcal{L}$.

*Proof.* If the negation on $\mathrm{USC}(\mathcal{L})$ is involutive, then, by **Lemma 2.2.19**, so is the negation on $\mathcal{L}$.
Assume now that the negation on $\mathcal{L}$ is involutive. For all $f \in USC(\mathcal{L})$,
$(1 \div f)(q) = \bigvee_{p<q1>r \ge p} (f(r-p) \leftrightarrow \perp) = \bigvee_{p<q} f(1-p) \leftrightarrow \perp$, so

$$
\begin{align*}
(1 \div (1 \div f))(q) &= \bigvee_{p<q} (1 \div f)(1-p) \leftrightarrow \perp \\
&= \bigvee_{p<q} \left( \bigvee_{r<1-p} f(1-r) \leftrightarrow \perp \right) \leftrightarrow \perp \\
&= \bigvee_{p<q} (f(p) \leftrightarrow \perp) \leftrightarrow \perp \\
&= \bigvee_{p<q} f(p) \\
&= f(q).
\end{align*}
$$

□

**Definition 6.1.2.** We denote by $T_{inv}$ the theory $T \cup \{v \le (1 \div (1 \div v))\}$.

We denote by InAC the class whose elements are the USC($\mathcal{L}$) for $\mathcal{L}$ an involutive commutative
residuated complete lattice and call these algebras Involutive Affine Continuous Algebras.

**Theorem 6.1.3.** For all model $A$ of $T_{inv}$, there exists an involutive commutative residuated complete lattice $\mathcal{L}$ such that the quotient of the Macneille completion of $A$ by $\simeq$ is isomorphic to $USC(\mathcal{L})$.

For all model $A$ of $T_{inv}$, there exists an involutive commutative residuated complete lattice $\mathcal{L}$ such
that the quotient of $A$ by $\simeq$ embeds into $USC(\mathcal{L})$.

Proof. Let $A$ be a model of $T_{inv}$. $A$ is a model of $T$, so, according to **Theorem C**, there exists a commutative residuated complete lattice $\mathcal{L}$ such that the quotient of the Macneille completion of $A$ by $\simeq$ is isomorphic to $USC(\mathcal{L})$. According to this same theorem, the quotient of $A$ by $\simeq$ also embeds into $USC(\mathcal{L})$.

Since, $A$ satisfies $v \le 1 \div (1 \div v)$ and the function $a \mapsto a$ preserves upper bounds, **Lemma 3.3.16** ensures that the Macneille completion of $A$, this identity is still true. Hence it is also true in the quotient and thus in $USC(\mathcal{L})$. **Theorem 6.1.1** then ensures that the negation on $\mathcal{L}$ is involutive.

□

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

(1) For all involutive commutative residuated complete lattice $\mathcal{L}$, $USC(\mathcal{L}) \models \varphi \le \psi$.

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

Proof. For all involutive commutative residuated complete lattice $\mathcal{L}$, $USC(\mathcal{L})$ is a model of $T_{inv}$.
By Archimedeanity of every InAC-algebra, we have that 2 implies 1.

Let $\varphi$ and $\psi$ be $\mathcal{L}$-terms both having $k$ free variables such that, for all locale $\mathcal{L}$, $USC(\mathcal{L}) \models \varphi \le \psi$.
Let $n \in \mathbb{N}$.

Let $A$ be a model of $T_{inv}$. According to **Corollary 6.1.3**, there exists an involutive commutative residuated lattice $\mathcal{L}$ and a morphism $i: A \to USC(\mathcal{L})$ 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 models of $\mathbf{T}$ being complete for $\mathbf{T}$, $\varphi \le \psi + \frac{1}{2^n}$ is consequence of $\mathbf{T}$.

□
6.2. **Cut Admissibility.** In the involutive case, since, contrary to **Appendix 8**, is commutative, there is only one negation symbol $\neg$. Moreover, since $\alpha$ is bijective, $\circ_{\alpha} = \bullet_{\alpha}$. Thus, we can forget $\bullet_{\alpha}$ and add the rule $\frac{\circ_{\alpha}\Gamma \vdash \Delta}{\Gamma \vdash \circ_{\alpha}\Delta}$. However, everything works as in **Appendix 8**. The language for the structures and formulas of sequent calculus in the involutive case, and its correspondence with the language $\mathcal{L}_{\text{inv}}$, are given in the table of Figure 6. We will also consider the language $\mathcal{L}'_{\text{inv}}$ which is $\mathcal{L}_{\text{inv}}$ with the symbols of the table of Figure 7. We keep Notation 4.1.1.

<table><caption>FIGURE 6. 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>j(1/2 + 1/2)</td></tr><tr><td>ε</td><td>0</td><td>0</td><td>1/2</td><td>1/2</td></tr><tr><td>○<sub>2</sub></td><td>2</td><td>2</td><td>1/2</td><td>1/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 7. 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>

The system **InMGL** for involutive modal full Lambek calculus can be applied with one or several modalities and one or two negations. Here, we also have only one negation, a difference that **Lemma 6.2.1** tacles. We thus obtain a system **InMGL** $(\circ_2, \bullet_2, \circ_{\alpha})$ in the language $\mathcal{L}_{\text{inv}}$ given by **InGL** (from the **Appendix 8**) and Figure 8 and a system **InMGL** $(\circ_2, \bullet_2, \circ_{\alpha}, \bullet_{\alpha})$ in the language $\mathcal{L}'_{\text{inv}}$ given by **InGL** and Figure 9. In addition to the rules of **InMGL** $(\circ_2, \bullet_2, \circ_{\alpha})$, we add the structural rules given in Figure 10 and call the total system **InCFL<sub>ew</sub>**. Define **InCFL<sub>ew</sub>**' as the system in the language $\mathcal{L}'_{\text{inv}}$ having for rules the ones of **InMGL** $(\circ_2, \bullet_2, \circ_{\alpha}, \bullet_{\alpha})$ and Figure 10.

<table><caption>FIGURE 8. Introduction Rules **InMGL** $(\circ_2, \bullet_2, \circ_{\alpha})$</caption><tr><td>$[L 2] \frac{\circ_2 A \vdash \Delta}{2A \vdash \Delta}$</td><td>$[L j_*] \frac{\bullet_2 A \vdash \Delta}{j_*(A) \vdash \Delta}$</td><td>$[R 2] \frac{\Gamma \vdash A}{\circ_2 \Gamma \vdash 2A}$</td><td>$[R j_*] \frac{\Gamma \vdash A}{\bullet_2 \Gamma \vdash j_*(A)}$</td></tr><tr><td>$[\circ_2 / \bullet_2] \frac{\circ_2 \Gamma \vdash \Delta}{\Gamma \vdash \bullet_2 \Delta}$</td><td>$[L \alpha] \frac{\circ_{\alpha} A \vdash \Delta}{\alpha(A) \vdash \Delta}$</td><td>$[R \alpha] \frac{\Gamma \vdash A}{\circ_{\alpha} \Gamma \vdash \alpha(A)}$</td><td>$[\circ_{\alpha} / \circ_{\alpha}] \frac{\circ_{\alpha} \Gamma \vdash \Delta}{\Gamma \vdash \circ_{\alpha} \Delta}$</td></tr><tr><td>$[\neg L] \frac{\gamma, \delta \vdash \beta}{\delta \vdash \gamma, \neg \beta}$</td><td>$[\neg R] \frac{\gamma, \delta \vdash \beta}{\gamma \vdash \beta, \neg \delta}$</td><td>$[L \neg] \frac{\neg a \vdash \delta}{\neg a \vdash \delta}$</td><td>$[R \neg] \frac{\gamma \vdash a \neg}{\gamma \vdash \neg a}$</td></tr></table>
<figure><img src="image_12.png" /><figcaption>FIGURE 9. Introduction Rules for *InMGL* (◦₂, •₂, ◦ₐ, •ₐ)</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>FIGURE 10. *InCFL*<sub>ew</sub></figcaption></figure>

Since ◦_α is self dual, we reduce *InCFL*<sub>ew</sub> to the setting of Appendix 8 thanks to the next lemma.

**Lemma 6.2.1.** The systems (1) *InMGL* (◦₂, •₂, ◦ₐ) ∪ {Γ, Δ ⊢ Θ / Δ, Γ ⊢ Θ} and (2) *InMGL* (◦₂, •₂, ◦ₐ, •ₐ) ∪ {Γ, Δ ⊢ Θ / Δ, Γ ⊢ Θ, ◦ₐ Γ ⊢ Δ / •ₐ Γ ⊢ Δ} are equivalent in the following sense:

For every deduction in (1) there exists a deduction in (2) with same premises and conclusion.
By letting, in (1), •_α = ◦_α and _≈_ = _¬_, every deduction in (2) is a deduction in (1).
Hence, in this sense, *InCFL*<sub>ew</sub> and *InCFL*<sub>ew</sub>' are equivalent.

Proof. We just have to prove that the rules of each system are deducible in the other one.
(1) → (2) : The two rules of (1) that are not rules of (2) are [◦_α/◦_α] and [¬L].
Here are the proof trees of Γ ⊢ ◦_αΔ / •_αΓ ⊢ Δ, [◦_α/◦_α] and [¬L] in (2). We recall the validity of the

deduction $\frac{\gamma \vdash \delta^-}{\delta \vdash \gamma^-} [\sim / \neg]$ and that $(\gamma, \delta)^- = \delta^-, \gamma^- [\text{neg}]$.
$$
\frac{
  \begin{array}{c}
    \begin{array}{c}
      \gamma \vdash \circ_{\alpha}\delta \\
      \overline{\gamma \vdash (\circ_{\alpha}\delta)^{\neg\sim}}
    \end{array} \\
    \begin{array}{c}
      (\circ_{\alpha}\delta)^{\neg} \vdash \gamma^{\neg} \\
      \overline{\circ_{\alpha}(\delta^{\neg}) \vdash \gamma^{\neg}}
    \end{array} \\
    \begin{array}{c}
      \delta^{\neg} \vdash \bullet_{\alpha}(\gamma^{\neg}) \\
      \overline{\delta^{\neg} \vdash (\bullet_{\alpha}\gamma)^{\neg}}
    \end{array} \\
    \begin{array}{c}
      \bullet_{\alpha}\gamma \vdash \delta^{\neg\sim} \\
      \overline{\bullet_{\alpha}\gamma \vdash \delta}
    \end{array}
  \end{array}
}{
  \begin{array}{c}
    \begin{array}{c}
      \circ_{\alpha}\gamma \vdash \delta \\
      \overline{\circ_{\alpha}\gamma \vdash \delta}
    \end{array} \\
    \begin{array}{c}
      \circ_{\alpha}/\bullet_{\alpha} \\
      \overline{\gamma \vdash \circ_{\alpha}\delta}
    \end{array}
  \end{array}
} \sim\neg \quad \begin{array}{l}
  \frac{\gamma, \delta \vdash \beta}{\delta, \gamma \vdash \beta} \quad (1.b) \\
  \frac{\delta \vdash \beta, \gamma^{\neg}}{\delta \vdash (\beta, \gamma^{\neg})^{\neg\sim}} \quad [\neg R] \\
  \frac{(\beta, \gamma^{\neg})^{\neg} \vdash \delta^{\neg}}{\gamma^{\neg\neg}, \beta^{\neg} \vdash \delta^{\neg}} \quad [\text{neg}] \\
  \frac{\beta^{\neg}, \gamma^{\neg\neg} \vdash \delta^{\neg}}{\gamma^{\neg}, \beta^{\neg}} \quad (1.b) \\
  \frac{(\gamma^{\neg}, \beta)^{\neg} \vdash \delta^{\neg}}{\delta \vdash (\gamma^{\neg}, \beta)^{\neg\sim}} \quad [\sim / \neg] \\
  \frac{\delta \vdash (\gamma^{\neg}, \beta)^{\neg\sim}}{\delta \vdash \gamma^{\neg}, \beta} \quad [\text{neg}]
\end{array}
\quad [\sim / \neg]
$$

(2) $\rightarrow$ (1): By letting $\bullet_{\alpha} = \circ_{\alpha}$ and $\sim = \neg$, every rule of (2) is a rule of (1), so every deduction in (2) becomes a deduction in (1). $\square$

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

**Lemma 6.2.2.** *Algebraic models of *InCFL*<sub>ew</sub> are the ones of the theory *T*<sub>inv</sub> satisfying property (6.b).*

*Proof.* According to **Theorem 8.1.12** and **Lemma 6.2.1**, the models of *InCFL*<sub>ew</sub> are the residuated lattices satisfying, for each previous structural rule *r*, the formula in the language *L'*<sub>inv</sub> where each structure variable has been replaced by a fresh new formula variable, — by $\Rightarrow$, $\vdash$ by $\geq$, $+$, by $\dagger$, $\circ_2$ by 2, $\bullet_2$ by $j_*$, $\circ_\alpha$ by $\alpha$ and each $\varepsilon_d$ by *d*.

Then, as in **Example 4.1.1** we can see that these axioms are equivalent to axioms of $\mathbf{T}_{\text{inv}}$ as refered to in the system $\mathbf{InCFL}_{\text{ew}}$. (2) can be treated the same way as (3.a) and (1.a), (4) and (5) can be treated the same way as (4.d). The only rule to which the previous methodology can't apply directly is (6.b) because it is infinitary. However, it is immediate that every model of this rule has equivalently the property $\forall n \in \mathbb{N}_{\frac{1}{2^n}} \ge v \Rightarrow \emptyset \ge v$, which is actually property (6.b).

Hence the models of $\mathbf{InCFL}_{\text{ew}}$ are exactly the models of $\mathbf{T}_{\text{inv}}$. $\square$

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

Since all the rules added to obtain $\mathbf{InCFL}_{\text{ew}}$ are analytic (cf. **Definition 8.1.2**), according to **Theorems 8.1.12** and 8.1.13, the following theorem is true.

**Theorem 6.2.3 (Completeness theorem).** *The class of USC($\mathcal{L}$), for $\mathcal{L}$ a complete commutative involutive residuated lattice, is sound and complete for $\mathbf{InCFL}_{\text{ew}}$.*

*Proof.* Since $\mathbf{InCFL}_{\text{ew}}'$ and $\mathbf{InCFL}_{\text{ew}}$ are equivalent (Lemma 6.2.1), according to **Theorem 8.1.12**, the class of $\text{USC}(\mathcal{L})$ for $\mathcal{L}$ a complete commutative involutive residuated lattice is sound and complete for $\mathbf{InCFL}_{\text{ew}}'$, this class is also sound and complete for $\mathbf{InCFL}_{\text{ew}}$. $\square$

**Theorem 6.2.4 (Cut Admissibility theorem).** *In the system $\mathbf{InCFL}_{\text{ew}}$, for all formulas $a_1, \dots, a_n$ and $b \{, \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.*

*Proof. Claim :* In the system $\mathbf{InCFL}_{\text{ew}}'$, for all formulas $a_1, \dots, a_n$ and $b$ and $\{, \circ_2, \bullet_2, \circ_\alpha, \bullet_\alpha, \varepsilon\}$-term $\underline{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.

The claim is a direct consequence of **Theorem 8.1.13**.

For each deduction *D* in *InCFL*<sub>ew</sub> ∪ {cut}, according to **Lemma 6.2.1** there exists a deduction in *InCFL*<sub>ew</sub>' ∪ {cut} having same premisses and conclusion. Since, according to **Theorem 4.1.4,**