2 Preliminaries

First of all, we recall the definitions of sup-lattice, quantale, quantale module, and quantale module nucleus.

Right modules and bimodules are defined in a completely analogous way. We refer the reader to [Reference Kruml, Paseka and Hazewinkel8, Reference Rosenthal11, Reference Russo13, Reference Russo16, Reference Solovyov19] for further information on quantales and their modules.

The next result is part of Lemma 6.1 of [Reference Russo14], and is crucial for the definition of the category $\mathcal {QM}$ .

Lemma 2.3. Let Q and R be quantales and $h: Q \to R$ a quantale homomorphism. Then h induces a structure of Q-module on every R-module N, with the following operation:

(1) $$ \begin{align} \cdot_h: (a, x) \in Q \times N \longmapsto h(a) \cdot x \in N. \end{align} $$

The process described in the previous lemma is known as the restriction of scalars along h. In fact, it defines a functor $(\ )_h: R\textrm {-}\mathcal {M}\!\!\:{od} \to Q\textrm {-}\mathcal {M}\!\!\:{od}$ between the categories of R-modules and Q-modules. Such a functor is both adjoint and coadjoint [Reference Russo14, Theorem 6.7]. The left adjoint is of particular interest for us, as it involves the tensor product of modules, whose construction we recall hereafter.

Theorem 2.4 (Theorem 6.3 of [Reference Russo15]).

Let $M_1$ be a right Q-module and $M_2$ a left Q-module. Then the tensor product $M_1 \otimes _Q M_2$ of the Q-modules $M_1$ and $M_2$ exists. It is, up to isomorphisms, the quotient $\wp (M_1 \times M_2)/\vartheta _\rho $ of the free sup-lattice generated by $M_1 \times M_2$ by the (sup-lattice) congruence $\vartheta _\rho $ generated by the set

(2) $$ \begin{align} \rho = \left\{ \begin{array}{@{}l} \left(\left\{\left(\bigvee X, y\right)\right\}, \bigcup_{x \in X}\{(x,y)\}\right) \\ \left(\left\{\left(x, \bigvee Y\right)\right\}, \bigcup_{y \in Y}\{(x,y)\}\right) \\ \left(\{(x \cdot_1 a, y)\}, \{(x,a \cdot_2 y)\}\right) \\ \end{array} \right\vert \left. \begin{array}{l} X \subseteq M_1, y \in M_2 \\ Y \subseteq M_2, x \in M_1 \\ a \in Q \\ \end{array} \!\!\!\right\}. \end{align} $$

Last, we recall that, given a quantale Q, a Q-module M, and $\vartheta \subseteq M^2$ , an element s of M is called $\vartheta $ -saturated if, for all $(v,w) \in \vartheta $ and $a \in Q$ , the following condition holds:

(3) $$ \begin{align} av \leq s \iff aw \leq s; \end{align} $$

the quotient of M over the congruence generated by $\vartheta $ is isomorphic to the set of the $\vartheta $ -saturated elements of M with suitable operations (see [Reference Russo16]).

We conclude this section by defining the category of quantales and their modules.

3 Coproducts and pushouts in $\mathcal {QM}$

The category $\mathcal {QM}$ can also be seen as a non-full subcategory of the product category $\mathcal Q \times \mathcal {SL}$ , of the category of quantales with the one of sup-lattices. However, due to the strong condition imposed on morphisms, it is not surprising that $\mathcal {QM}$ has a quite different behaviour with respect to $\mathcal Q \times \mathcal {SL}$ . In this paper, we introduced this category as a (not too) broader abstract framework for the category of deductive systems. For this reason, in this paper we will concentrate our attention to amalgamation and coproduct, which are particularly relevant to logic. The coproduct of unital quantales has been described in [Reference Liang9]. It is the quotient of the powerset of the coproduct of the monoid reducts of the given quantales, over the smallest congruence that identifies subsets of the factors with their join in the respective quantales. The product of quantales is given simply by the Cartesian product with coordinatewise operations. Regarding sup-lattices and quantale modules, they have analogous products, while coproducts have exactly the same objects as products [Reference Galatos and Tsinakis6, Lemma 5.1].

The coproduct in the category $\mathcal {QM}$ is strongly connected to the tensor product of quantale modules discussed in [Reference Russo14, Reference Russo15], as we can see from the following characterization.

Theorem 3.1. Let $F = \{(Q_i,M_i)\}_{i \in I}$ be a family of objects of $\kern1.2pt\mathcal {QM}$ and let $R = \coprod _{i \in I} Q_i$ be the coproduct of the $Q_i$ ’s in the category of unital quantales (see also [Reference Liang9]). Then the coproduct of F in $\mathcal {QM}$ is the object

$$ \begin{align*}\left(R, \coprod_{i \in I} R \otimes_{Q_i} M_i\right),\end{align*} $$

with associated family of morphisms $\{(\nu _i,\mu _i (1 \otimes \iota _{M_i}))\}$ where, for each $i \in I$ , $\nu _i$ is the embedding of $Q_i$ in R, $1 \otimes \iota _{M_i}$ is the $Q_i$ -module morphism defined by $x \in M_i \mapsto 1 \otimes x \in R \otimes _{Q_i} M_i$ as in [Reference Russo14, Section 6], and $\mu _i$ is the R-module embedding of $R \otimes _{Q_i} M_i$ in the R-module coproduct of the family $\{R \otimes _{Q_i} M_i\}_{i \in I}$ as in [Reference Russo13, Proposition 4.13].

Proof. Let $(S,N) \in \mathcal {QM}$ and $\{(h_i,f_i): (Q_i, M_i) \to (S,N)\}$ be a family of morphisms. Since R is the quantale coproduct of the $Q_i$ ’s, there exists a quantale morphism $h: R \to S$ such that $h\nu _i=h_i$ for all $i \in I$ .

By [Reference Russo14, Lemma 6.6], the sup-lattices $\hom _R(R,N_h)$ and N are isomorphic; moreover, such an isomorphism becomes a $Q_i$ -module isomorphism between the structure of $Q_i$ -module on $\hom _R(R,N_h)$ defined in [Reference Russo14, Lemma 6.4] (here R is to be thought of as an R- $Q_i$ -bimodule) and $(N_h)_{\nu _i} = N_{h_i}$ . Consequently, we have $\hom _{Q_i}(M_i,N_{h_i}) \cong _{\mathcal {SL}} \hom _{Q_i}(M_i, \hom _R(R,N_h))$ . The latter, in turn, is isomorphic to $\hom _R(R \otimes _{Q_i} M_i, N_h)$ by [Reference Russo14, Lemma 6.5]. Therefore we have $\hom _{Q_i}(M_i,N_{h_i}) \cong _{\mathcal {SL}} \hom _R(R \otimes _{Q_i} M_i, N_h)$ .

Then we have an R-module morphism $f_i': R \otimes _{Q_i} M_i \to N_h$ canonically associated with each $Q_i$ -module morphism $f_i: M_i \to N_{h_i}$ . The R-module $M = \coprod _{i \in I} R \otimes _{Q_i} M_i$ is the coproduct of the family $\{R \otimes _{Q_i} M_i\}_{i \in I}$ in $R\textrm {-}\mathcal {M}\!\!\:{od}$ , hence there exists an R-module morphism $f: M \to N_h$ such that $f'\mu _i = f_i'$ for all i.

Taking a closer look at all those isomorphisms (the proof of [Reference Russo14, Lemma 6.5] was actually presented in [Reference Russo12, Theorem 4.7.6]), it is not hard to see that, for all $i \in I$ , $r \in R$ , and $x \in M_i$ , $f_i'(r \otimes x) = r \cdot f_i(x)$ , whence

$$ \begin{align*}(f\mu_i(1 \otimes \iota_{M_i}))(x) = f_i'(1 \otimes x) = f_i(x),\end{align*} $$

which completes the proof.

Proposition 3.2. Let $h: Q \to R$ be a quantale morphism and $M \in Q\textrm {-}\mathcal {M}\!\!\:{od}$ . If there exists an embedding $f: M \to N_h$ for some $N \in R\textrm {-}\mathcal {M}\!\!\:{od}$ , then the Q-module homomorphism

$$ \begin{align*}\mu: x \in M \mapsto 1 \otimes x \in R \otimes_Q M\end{align*} $$

is an embedding.

Proof. Let us use the following notations: $M' = f[M]$ and $\top ' = \bigvee M'$ .

Let, for all $x \in M$ , $\overline x$ be the following element of $\wp (R \times M)$ :

(4) $$ \begin{align} \overline x = \{(r, y) \in R \times M \mid r \cdot f(y) \leq f(x)\}. \end{align} $$

Recalling that sup-lattices can also be seen as modules over the two-element quantale $\{\bot ,1\}$ , we shall prove that, for each $x \in M$ , $\overline x$ is a saturated element of the relation defined as in (2) by proving that condition (3) is verified for all the pair types in (2). The scalar a in (3) shall be dropped because it is actually $1$ , while the case of $a = \bot $ is trivial.

Let us check (3) for the first type of pairs in (2). Let $A \subseteq R$ and $y \in M$ ; then

$$ \begin{align*}\begin{array}{l} \{(\bigvee A, y)\} \subseteq \overline x \\ \iff \bigvee A \cdot f(y) \leq f(x) \\ \iff r \cdot f(y) \leq f(x) \\ \iff \bigcup_{r \in A}\{(r, y)\} \subseteq \overline x. \end{array}\end{align*} $$

As for the second type, let $r \in R$ and $Y \subseteq M$ . Then we have

$$ \begin{align*}\begin{array}{l} \{(r,\bigvee Y)\} \subseteq \overline x \\ \iff r \cdot f(\bigvee Y) = \bigvee\limits_{y \in Y} r \cdot f(y) \leq f(x) \\ \iff \forall y \in Y \ (r \cdot f(y) \leq f(x))\\ \iff \forall y \in Y \ (\{(r, y)\} \subseteq \overline x)\\ \iff \bigcup_{y \in Y}\{(r, y)\} \subseteq \overline x. \end{array}\end{align*} $$

Last, let us consider $r {\kern-1pt}\in{\kern-1pt} R$ , $q {\kern-1pt}\in{\kern-1pt} Q$ , and $y {\kern-1pt}\in{\kern-1pt} M$ . The equality $r {\kern-1pt}\cdot{\kern-1pt} f(q {\kern-1pt}\cdot{\kern-1pt} y) {\kern-1pt}={\kern-1pt} (r {\kern-1pt}\cdot{\kern-1pt} h(q)){\kern-1pt}\cdot{\kern-1pt} f(y)$ implies that $r \cdot f(q \cdot y) \leq f(x)$ if and only if $(r \cdot h(q))\cdot f(y) \leq f(x)$ , and therefore $\{r, q \cdot y)\} \subseteq \overline x$ if and only if $\{(r \cdot h(q), y)\} \subseteq \overline x$ . This finally proves that $\overline x$ is saturated in $R \times M$ with respect to the relation which determines the tensor product.

As a final step, let us show that the mapping $x \mapsto \overline x$ is injective. For all $x \in M$ , $(1,x) \in \overline x$ and, for any $y \in M$ , if $\overline x = \overline y$ then $(1,x) \in \overline y$ and $(1,y) \in \overline x$ , which implies that $1 \cdot f(x) = f(x) \leq f(y)$ and $1 \cdot f(y) = f(y) \leq f(x)$ , i.e., $f(x) = f(y)$ . Then, by the injectivity of f, $x = y$ and the thesis follows.

Theorem 3.3. Let $\mathbf A = (Q_1, M_1) \stackrel {(h_1,f_1)}{\longleftarrow } (Q,M) \stackrel {(h_2,f_2)}{\longrightarrow } (Q_2,M_2)$ be a span in $\mathcal {QM}$ and R a quantale such that

is a pushout square in the category of quantales. If, for $i=1,2$ , $M_i$ embeds in $(P_i)_{k_i}$ as a $Q_i$ -module, for some R-module $P_i$ , then the pushout of $\mathbf A$ exists in $\mathcal {QM}$ and it is, up to isomorphism, $(R,R \otimes _Q N)$ , where N is the pushout of the Q-module span $(M_1)_{h_1} \stackrel {f_1}{\longleftarrow } M \stackrel {f_2}{\longrightarrow } (M_2)_{h_2}$ .

Moreover, if $\mathbf P$ is the diagram of an amalgamated coproduct (i.e., the morphisms in $\mathbf P$ are embeddings), and $f_1$ and $f_2$ are embeddings, then $(R,R \otimes _Q N)$ is the amalgamated coproduct of $\mathbf A$ in $\mathcal {QM}$ .

Proof. First of all, let us observe that, for $i = 1, 2$ , the following sup-lattice isomorphisms hold:

$$ \begin{align*}\begin{array}{ll} \hom_R(R \otimes_Q M, R \otimes_{Q_i} M_i) & \\ \cong \hom_Q(M, \hom_R(R, R \otimes_{Q_i} M_i)) & \text{(by [12, Theorem 4.7.6])} \\ \cong \hom_Q(M, R \otimes_{Q_i} M_i) & \text{(by [12, Theorem 4.7.8])} \\ \cong \hom_Q(M, \hom_{Q_i}(Q_i, R \otimes_{Q_i} M_i)) & \text{(by [12, Theorem 4.7.8])} \\ \cong \hom_{Q_i}(Q_i \otimes_Q M, R \otimes_{Q_i} M_i) & \text{(by [12, Theorem 4.7.6])} \\ \cong \hom_{Q_i}(Q_i \otimes_Q M, \hom_R(R, R \otimes_{Q_i} M_i)) & \text{(by [12, Theorem 4.7.8])} \\ \cong \hom_R(R \otimes_{Q_i}(Q_i \otimes_Q M), R \otimes_{Q_i} M_i) & \text{(by [12, Theorem 4.7.6]).} \end{array}\end{align*} $$

Let N be the pushout of the Q-module span

$$ \begin{align*}(M_1)_{h_1} \stackrel{f_1}{\longleftarrow} M \stackrel{f_2}{\longrightarrow} (M_2)_{h_2},\end{align*} $$

with associated morphisms $n_i: (M_i)_{h_i} \to N$ , $i=1,2$ , and let $f_i': R \otimes _Q M \to R \otimes _{Q_i} M_i$ , $i = 1,2$ , be the morphisms obtained via the above correspondence from the image of the morphism $f_i$ under the functor $R \otimes _{Q_i} (Q_i \otimes _Q {}_{\text {--}})$ or, which is the same, the image of $f_i$ under the left adjoint to the functor $( \ )_{k_ih_i} = ( \ )_{h_i} \circ ( \ )_{k_i}$ .

Since R is the pushout of $h_1$ and $h_2$ , whenever we have a pair of quantale morphisms $l_i: Q_i \to S$ such that $l_1h_1 = l_2h_2$ , there exists a quantale morphism $k: R \to S$ such that $kk_i=l_i$ , $i = 1,2$ , as in the following diagram:

(5)

Now, referring ourselves to the next diagram, if we have an S-module L and morphisms $g_i: M_i \to L_{l_i}$ , $i = 1,2$ , such that $g_1f_1 = g_2f_2$ , then the tensor functors will give us two R-module morphisms $g_i': R \otimes _{Q_i} M_i \to L_k$ , $i=1,2$ , such that $g_1'f_1' = g_2'f_2'$ . Since N is a Q-module pushout, there exists a Q-module morphism $g: N \to L_{l_ih_i}$ such that $gn_i = g_i$ , for $i = 1,2$ . Applying the tensor functor again, we get then an R-module morphism $g': R \otimes _Q N \to L_k$ such that $g'n_i' = g_i'$ , for $i = 1,2$ . Now, since the $M_i$ ’s embed in some R-modules by hypothesis, by Proposition 3.2, the diagram (6) commutes and, therefore, $(R,R \otimes _Q N)$ is the desired pushout. This proves the first assertion.

(6)

With the given additional hypotheses, $f_1$ , $f_2$ , $n_1$ , $n_2$ , $1 \otimes \iota _M$ , and $1 \otimes \iota _N$ are embeddings too, therefore $(R,R \otimes _Q N)$ is the amalgamation of the span $\mathbf A$ .

4 The subcategory of deductive systems

In this section, we shall define the category $\mathcal {DS}_0$ as a subcategory of $\mathcal {QM}$ , and review some results from [Reference Russo14, Reference Russo17] in the light of the ones above. First, we shall recall some very basic definitions.

As usual, by a propositional language we mean a pair $\mathcal {L} = \left \langle L, \nu \right \rangle $ consisting of a set L and a map $\nu : L \to \omega $ . The elements of L are called connectives, and the image of a connective under $\nu $ is called its arity; nullary connectives are most often called constant symbols or simply constants.

Given a propositional language $\mathcal {L}$ and a denumerable set $\operatorname {Var} = \{x_n \mid n < \omega \}$ of propositional variables, the set ${Fm}_{\mathcal {L}}$ of $\mathcal {L}$ -formulas is defined recursively in the usual manner:

1. (F1) every propositional variable and every constant symbol is an $\mathcal {L}$ -formula;

2. (F2) if f is a connective of arity $\nu (f)> 0$ and $\varphi _1, \ldots , \varphi _{\nu (f)}$ are $\mathcal {L}$ -formulas, then $f\varphi _1\ldots \varphi _{\nu (f)}$ —usually denoted by $f(\varphi _1, \ldots , \varphi _{\nu (f)})$ —is an $\mathcal {L}$ -formula;

3. (F3) all $\mathcal {L}$ -formulas are built by finitely many iterative applications of (F1) and (F2).

From a universal algebraic viewpoint, ${Fm}_{\mathcal {L}}$ can also be defined as the absolutely free algebra over the signature $\mathcal {L}$ . The substitution monoid $\Sigma _{\mathcal L}$ over $\mathcal {L}$ is the monoid of $\mathcal {L}$ -endomorphisms of ${Fm}_{\mathcal {L}}$ . We remark that, since ${Fm}_{\mathcal {L}}$ is a term algebra, each substitution is completely determined by its values on the variables.

Starting from formulas, it is possible to define

• • the set ${Eq}$ of $\mathcal {L}$ -equations as ${Fm}_{\mathcal {L}}^2$ , and

• • for all $T \subseteq \omega ^2$ , the set ${Seq}_T$ of sequents closed under the types in T as $\bigcup \limits _{(m,n) \in T} {Fm}_{\mathcal {L}}^m \times {Fm}_{\mathcal {L}}^n$ .

An inference rule over $\mathcal {L}$ is a pair $(\Phi ,\psi )$ where $\Phi $ is a set of formulas, equations, or sequents of a fixed type, and $\psi $ is a single formula, equation, or sequent of the same type. Then we say that $\varphi $ is directly derivable from $\Psi $ by the rule $(\Phi ,\psi )$ if there is a substitution $\sigma $ such that $\sigma \psi = \varphi $ and $\sigma [\Phi ] \subseteq \Psi $ . An inference rule $(\Phi ,\psi )$ is usually denoted by $\frac {\Phi }{\psi }$ .

An axiom in the language $\mathcal {L}$ is simply a formula (or an equation, or a sequent) in $\mathcal {L}$ .

Now we recall the representation of propositional logics as quantale modules. If D is ${Fm}_{\mathcal {L}}$ , ${Eq}$ , or any ${Seq}_T$ , we have a left monoid action from $\Sigma _{\mathcal L}$ to D. By applying the left adjoints to the forgetful functors from quantales to monoids and from sup-lattices to sets, respectively, we obtain a quantale $\wp \Sigma _{\mathcal L}$ and a left $\wp \Sigma _{\mathcal L}$ -module $\wp D$ . Thanks to this change of perspective, one can see a consequence relation $\vdash $ as a $\wp \Sigma _{\mathcal L}$ -module nucleus on $\wp D$ , as the following result shows.

Proposition 4.2 (Lemma 3.5 of [Reference Galatos and Tsinakis6]).

For any consequence relation $\vdash $ on $\wp D$ , the mapping

$$ \begin{align*}\gamma_\vdash: \Phi \in \wp D \mapsto \bigcup_{\Phi \vdash \Psi} \Psi \in \wp D\end{align*} $$

is a $\wp \Sigma _{\mathcal L}$ -module nucleus. Reciprocally, for any $\wp \Sigma _{\mathcal L}$ -module nucleus $\gamma $ on $\wp D$ , the relation

$$ \begin{align*}\Phi \vdash_\gamma \Psi \iff \Psi \subseteq \gamma(\Phi)\end{align*} $$

is a consequence relation on $\wp D$ .

Moreover, $\vdash _{\gamma _\vdash } = \ \vdash $ and $\gamma _{\vdash _\gamma } = \gamma $ , for any consequence relation $\vdash $ and for any nucleus $\gamma $ .

Given a consequence relation $\vdash $ with associated nucleus $\gamma $ , the $\gamma $ -closed system $\wp D_\gamma $ coincides with the lattice of theories ${Th}_\vdash $ of $\vdash $ . Thanks to the previous result, we can think of a consequence relation either as a binary relation or as a $\wp \Sigma _{\mathcal L}$ -module nucleus, and we shall use either one of the notations depending on convenience. Similarly, we shall indifferently denote the lattice of theories by $\wp D_\gamma $ , ${Th}_\vdash $ or ${Th}_\gamma $ , and we will rather call it the module of theories.

Such a representation was introduced by Galatos and Tsinakis in [Reference Galatos and Tsinakis6] with the aim of algebraically characterizing interpretations between logical systems over the same language, such as Glivenko interpretation of classical into intuitionistic logic [Reference Glivenko7], and some cases of algebraizability [Reference Blok and Pigozzi3]. Eventually, the present author extended that result to the case of systems with different underlying languages. Such an extension obviously required the addition of a translation of the connectives of one language into the other. So we shall now recall the definition of language translation and two results about it from [Reference Russo14]. They are crucial for the definition of the category $\mathcal {DS}_0$ .

Now recall that, for any language $\mathcal {L}$ , the set $V=\{\sigma \in \Sigma _{\mathcal L} \mid \sigma [\operatorname {Var}] \subseteq \operatorname {Var}\}$ is the universe of a submonoid $\mathbf {V}$ of $\Sigma _{\mathcal L}$ . Furthermore, if $\mathbf {V}$ and $\mathbf {V}'$ are two such submonoids corresponding to the languages $\mathcal {L}$ and $\mathcal {L}'$ , then $\mathbf {V}\cong \mathbf {V}'$ . In the sequel, we identify all these monoids and denote all of them by $\mathbf {V}$ .

The first part of the following result is an immediate consequence of the previous lemma, while the second part is Corollary 6.9 of [Reference Russo14].

We refer to a quantale homomorphism $h: \wp \Sigma _{\mathcal L} \to \wp \Sigma _{\mathcal {L'}}$ induced by a language translation as a quantale translation.

As an instance of [Reference Russo14, Definition 3.7], we get the following definition.

Definition 4.6. Let $\mathcal {L}$ and $\mathcal {L}'$ be languages, $\tau : \mathcal {L} \to \mathcal {L}'$ a language translation with associated monoid homomorphism $h: \Sigma _{\mathcal L} \to \Sigma _{\mathcal {L'}}$ , and $S = \left \langle D, \vdash \right \rangle $ and $T = \left \langle D', \vdash '\right \rangle $ be deductive systems over $\mathcal {L}$ and $\mathcal {L}'$ , respectively.

A map $\iota : D \longrightarrow \wp D'$ is said to be h-action-invariant if $\iota (\sigma (\varphi )) = h(\sigma ) \cdot \iota (\varphi )$ for all $\sigma \in \Sigma _{\mathcal L}$ and $\varphi \in D$ .

An h-action-invariant map $\iota : D \to \wp D'$ is called an interpretation via h of $\vdash $ in $\vdash '$ if, for all $\Phi \cup \{\psi \} \subseteq D$ ,

$$ \begin{align*} \Phi \vdash \psi \quad \textrm{implies} \quad \iota[\Phi] \vdash' \iota(\psi). \end{align*} $$

An interpretation is called a conservative interpretation, or a representation, if

$$ \begin{align*} \Phi \vdash \psi \quad \textrm{if and only if} \quad \iota[\Phi] \vdash' \iota(\psi). \end{align*} $$

Given another translation $\tau ': \mathcal {L}' \to \mathcal {L}$ , with associated monoid homomorphism ${k: \Sigma _{\mathcal {L'}} \to \Sigma _{\mathcal L}}$ , two representations $\iota : D \to \wp D'$ , via h, and $\iota ': D' \to \wp (D)$ , via k, are said to form an equivalence if, for all $\varphi \in D'$ ,

$$ \begin{align*} \varphi \dashv'\vdash' \iota[\iota'(\varphi)]. \end{align*} $$

We can now set the following definition.

Although quite obvious, it is worth observing explicitly that $\mathcal {DS}_0$ is not a full subcategory of $\mathcal {QM}$ .

By Theorem 7.1 and Corollary 7.2 of [Reference Russo14], the category whose objects are propositional logics and whose morphisms are pairs translation–interpretation between them is equivalent to $\mathcal {DS}_0$ . More precisely, we have the following immediate result.

5 Coproduct, pushout and amalgamation in $\mathcal {DS}_0$

In [Reference Russo17, Section 5], the author constructed the so-called “logical coproduct” of deductive systems and proved that the given systems are conservatively interpretable in it [Reference Russo17, Theorem 5.3]. As clearly stated in that paper, the name logical coproduct was suggested by the relationship between the new logic and its components, but it was not clear whether that construction really corresponded to a coproduct in some category. The main result of this section shows that the answer is positive: $\mathcal {DS}_0$ is the right categorical setting and the logical coproduct of propositional logics is indeed a coproduct in the narrow categorical sense.

For the sake of readability, the original construction had been given for a pair of systems and languages, but it was also observed that everything holds for arbitrary families of systems and languages. So, let us briefly recall it in such a more general setting.

Given a family of propositional languages $\{\mathcal {L}_i\}_{i \in I}$ , the quantale of substitutions $\wp \Sigma _{\mathcal L}$ of their disjoint union $\mathcal {L}$ is the coproduct of the family of quantales $\{{\wp \Sigma _{\mathcal L}}_i\}_{i \in I}$ . Now, for each $i \in I$ , let $(D_i, \vdash _i)$ be a deductive system, of the same fixed type, over $\mathcal {L}_i$ , with associated nucleus $\gamma _i$ and module of theories ${Th}_i = (\wp D_i)_{\gamma _i}$ . The logical coproduct of the given systems $(E, \vdash )$ is the system defined over the $\mathcal {L}$ -domain E of the same type of the $D_i$ ’s, and whose consequence relation $\vdash $ is defined by means of the union of the axioms and rules of the family $\{\vdash _i\}_{i \in I}$ .

With the above notations, let also ${Th}$ be the $\wp \Sigma _{\mathcal L}$ -module of theories of $(E,\vdash )$ . Then, combining Theorem 3.1 with the results of [Reference Russo17, Section 5], we can see that the logical coproduct is indeed the coproduct in $\mathcal {DS}_0$ while it is not necessarily isomorphic to the one in $\mathcal {QM}$ , as the following result and counterexample show.

Proof. Let $\mathcal {L}'$ be a propositional language and $(D',\vdash ')$ be an $\mathcal {L}'$ -system (of any type) with $\gamma '$ and ${Th}'$ being, respectively, the associated module nucleus on $\wp D'$ and the module of theories. Suppose that, for each $i \in I$ , there exists a language translation $t_i: \mathcal {L}_i \to \mathcal {L}'$ and an interpretation $f_i: {Th}_i \to {Th}'$ with respect to $t_i$ (we shall denote by $t_i$ also the quantale morphisms induced by the given translations). Since $\wp \Sigma _{\mathcal L}$ is the quantale coproduct of the ${\wp \Sigma _{\mathcal L}}_i$ ’s and all the associated embeddings are induced by language translations, it is easy to see that the morphism $t: \wp \Sigma _{\mathcal L} \to \wp \Sigma _{\mathcal {L'}}$ extending the $t_i$ ’s to $\wp \Sigma _{\mathcal L}$ is also induced by a language translation. Moreover, by [Reference Russo14, Theorem 7.1], given such a translation, any $\wp \Sigma _{\mathcal L}$ -module morphism from ${Th}$ to ${Th}_t'$ is indeed induced by an interpretation, so we just need to show that there exists a morphism $f: {Th} \to {Th}_t'$ such that $fe_i = f_i$ for all $i \in I$ , where $e_i: {Th}_i \to {Th}$ is the embedding of [Reference Russo17, Theorem 5.3].

Let us denote by $(\wp \Sigma _{\mathcal {L'}}, M)$ the coproduct of $\{({\wp \Sigma _{\mathcal L}}_i,{Th}_i)\}_{i \in I}$ in $\mathcal {QM}$ . By Theorem 3.1, $M = \coprod _{i \in I} \wp \Sigma _{\mathcal L} \otimes _{Q_i} {Th}_i$ and, for each $i \in I$ , there exists a ${\wp \Sigma _{\mathcal L}}_i$ -module embedding of ${Th}_i$ into $M_{t_i}$ . Now let us consider the following commutative diagram:

(7)

where all the i-indexed morphisms are ${\wp \Sigma _{\mathcal L}}_i$ -module morphisms, while g and $g'$ are the $\wp \Sigma _{\mathcal L}$ -module morphisms extending, respectively, the $e_i$ ’s and the $f_i$ ’s to M. We want to prove that the $\wp \Sigma _{\mathcal L}$ -module morphism f exists. In order to do that, let us prove that $\ker g \subseteq \ker g'$ , so let us consider a pair $((m_i)_{i \in I}, (n_i)_{i \in I}) \in \ker g$ . Each $m_i$ and each $n_i$ are joins of tensors, say

$$ \begin{align*}m_i = \bigvee_{j_i \in J_i} \Sigma_{j_i} \otimes_{{\wp\Sigma_{\mathcal L}}_i} \Phi_{j_i} \quad \text{ and } \quad n_i = \bigvee_{k_i \in K_i} \Xi_{k_i} \otimes_{{\wp\Sigma_{\mathcal L}}_i} \Psi_{k_i},\end{align*} $$

with the $\Phi _{j_i}$ ’s and $\Psi _{k_i}$ ’s in ${Th}_i$ for all $i \in I$ , and $\Sigma _{j_i}, \Xi _{k_i} \in \wp \Sigma _{\mathcal {L'}}$ for all indexes. We have the following:

$$ \begin{align*}\begin{array}{l} g\left(\left(m_i\right)_{i\in I}\right) = g\left(\left(n_i\right)_{i \in I}\right) \iff \\ g\left(\left(\bigvee_{j_i \in J_i} \Sigma_{j_i} \otimes_{{\wp\Sigma_{\mathcal L}}_i} \Phi_{j_i}\right)_{i\in I}\right) = g\left(\left(\bigvee_{k_i \in K_i} \Xi_{k_i} \otimes_{{\wp\Sigma_{\mathcal L}}_i} \Psi_{k_i}\right)_{i \in I}\right) \iff \\ \bigvee_{i \in I} \left(\bigvee_{j_i \in J_i} \Sigma_{j_i} \cdot e_i\left(\Phi_{j_i}\right)\right) = \bigvee_{i \in I} \left(\bigvee_{k_i \in K_i} \Xi_{k_i} \cdot e_i\left(\Psi_{k_i}\right)\right) \iff \\ \bigvee_{i \in I} \left(\bigvee_{j_i \in J_i} \Sigma_{j_i} \cdot \Phi_{j_i}\right) = \bigvee_{i \in I} \left(\bigvee_{k_i \in K_i} \Xi_{k_i} \cdot \Psi_{k_i}\right) \iff \\ \bigvee_{i \in I} \left(\bigvee_{j_i \in J_i} \Sigma_{j_i} \cdot \Phi_{j_i}\right) \dashv\vdash \bigvee_{i \in I} \left(\bigvee_{k_i \in K_i} \Xi_{k_i} \cdot \Psi_{k_i}\right). \end{array}\end{align*} $$

Now, let $\Gamma = \bigvee _{i \in I} \left (\bigvee _{j_i \in J_i} \Sigma _{j_i} \cdot \Phi _{j_i}\right )$ , $\Delta = \bigvee _{i \in I} \left (\bigvee _{k_i \in K_i} \Xi _{k_i} \cdot \Psi _{k_i}\right )$ , and recall that, by [Reference Russo17, Section 5], $\vdash $ is the smallest $\Sigma _{\mathcal L}$ -invariant consequence relation on E verifying all the axioms and rules of all the $\vdash _i$ ’s. Therefore, there exists a $\vdash $ -proof, i.e., a finite sequence of entailments, of each element of $\Delta $ from $\Gamma $ and vice-versa. For the transitivity of the consequence relations, given $\Gamma _0 = \operatorname {Ax} \cup \bigcup _{i \in I} \left (\bigcup _{j_i \in J_i} \Sigma _{j_i} \Phi _{j_i}\right )$ , there exists also a $\vdash $ -proof of $\Delta $ from $\Gamma _0$ . Let $\delta \in \Delta $ and $\Gamma _0 \vdash \Gamma _1 \vdash \dots \vdash \Gamma _n \supseteq \{\delta \}$ be a proof of $\delta $ from $\Gamma _0$ — so, each element of $\Gamma _{a+1}$ is directly derivable from $\Gamma _a$ — such that, for all $a \in \{0, \ldots , n-1\}$ , $\Gamma _a \subseteq \Gamma _{a+1}$ .Footnote ² We shall now show by induction that such a proof can be interpreted in $\vdash '$ via the translation t.

• • Induction basis: For every element $\alpha $ of $\Gamma _0$ , there exist $i \in I$ , $\varphi \in D_i$ , and $\sigma \in \Sigma _{\mathcal L}$ such that $\alpha = \sigma (\varphi )$ and $t(\sigma )(f_i(\varphi ))$ is directly derivable from $g'((m_i)_{i \in I})$ in $\vdash '$ .

  Indeed, for all $\alpha \in \Gamma _0$ , there exists $i \in I$ such that either $\alpha = \varphi \in \operatorname {Ax}_i$ or $\alpha = \sigma (\varphi )$ with $\sigma \in \Sigma _{j_i}$ and $\varphi \in \Phi _{j_i} \subseteq D_i$ for some $j_i \in J_i$ . In the former case, $\vdash ' f_i(\alpha )=t(\sigma )(f_i(\varphi ))$ , where $\sigma = \operatorname {id}$ , while in the latter $t(\sigma )(f_i(\varphi )) \in g'((m_i)_{i \in I}$ . In both cases, $t(\sigma )(f_i(\varphi ))$ is directly derivable from $g'((m_i)_{i \in I})$ .

• • Induction step: For all $a \in \{0, \ldots , n-1\}$ and $\alpha \in \Gamma _{a+1}$ , there exists $i \in I$ , $\Sigma \in \wp \Sigma _{\mathcal L}$ , $\Theta \subseteq \operatorname {Ax}_i \cup (\Gamma _a \cap \wp D_i)$ and $\varphi \in D_i$ such that $\alpha \in \Sigma \cdot \{\varphi \}$ and $t(\Sigma )\cdot f_i(\Theta ) \vdash ' t(\Sigma ) \cdot f_i(\varphi )$ .s

  In other words, we will now prove that every “global” deduction, that is, every deduction in $\vdash $ , can be traced back to a “local” one in some $\vdash _i$ , and therefore interpreted in $\vdash '$ by means of t and $f_i$ .

  Each element $\alpha $ of $\Gamma _{a+1}$ is a consequence of $\Gamma _a$ . Therefore, there exists $i \in I$ such that either $\alpha = \varphi $ is an axiom of $\vdash _i$ or there exist $\Theta \subseteq \Gamma _a \cap \wp D_i$ , $\Lambda \subseteq D_i$ , and $\Sigma \in \wp \Sigma _{\mathcal L}$ such that $\frac {\Theta }{\Lambda }$ is an inference rule of $\vdash _i$ and $\alpha = \sigma (\varphi ) \in \Sigma \cdot \Lambda $ . In both cases, $t(\Sigma ) \cdot f_i(\Theta ) \vdash ' t(\sigma )(f_i(\varphi ))$ .

Since

$$ \begin{align*}\begin{array}{l} g'((m_i)_{i \in I}) = \bigvee_{i \in I} \left(\bigvee_{j_i \in J_i} t(\Sigma_{j_i}) \cdot f_i(\Phi_{j_i})\right), \text{ and} \\ g'((n_i)_{i \in I}) = \bigvee_{i \in I} \left(\bigvee_{k_i \in K_i} t(\Xi_{k_i}) \cdot f_i(\Psi_{j_i})\right), \end{array}\end{align*} $$

from the steps above it follows $g'((n_i)_{i \in I}) \subseteq g'((m_i)_{i \in I})$ . The converse inclusion is completely analogous, hence we have $g'((m_i)_{i \in I}) = g'((n_i)_{i \in I})$ and, therefore, $((m_i)_{i \in I},(n_i)_{i \in I}) \in \ker g'$ .

Last, from $\ker g \subseteq \ker g'$ , we get that there exists a $\wp \Sigma _{\mathcal L}$ -module morphism ${f: {Th} \to {Th}_t'}$ which makes the whole diagram in (7) commutative. This completes the proof.

In Theorems 3.1 and 5.1 we described the coproducts in $\mathcal {QM}$ and $\mathcal {DS}_0$ , respectively. In the next example, we will show that the coproduct of a family of objects of $\mathcal {DS}_0$ in $\mathcal {QM}$ need not be isomorphic to the coproduct of the same family in $\mathcal {DS}_0$ .

Example 5.2. Let us consider the language $\mathcal {L} = (\{\to ,\neg \},(2,1))$ and let us consider the deductive system of Classical Propositional Logic on $\mathcal {L}$ . Now consider the coproducts in $\mathcal {QM}$ and $\mathcal {DS}_0$ of two copies of such a system. In order to make the disjoint union of two copies of the language and, therefore, the coproduct of two copies of the quantale of substitutions, let us denote them by $\mathcal {L}_1 = (\{\to _1,\neg _1\},(2,1))$ and $\mathcal {L}_2 = (\{\to _2,\neg _2\},(2,1))$ . Consequently, the two systems shall be denoted by $({\wp \Sigma _{\mathcal L}}_i,{Th}_i)$ , $i =1,2$ .

Theorem 3.1 guarantees that the coproduct of the given pair of systems in $\mathcal {QM}$ is $(\wp \Sigma _{\mathcal L},M)$ , where $M = \coprod _{i=1}^2 \wp \Sigma _{\mathcal L} \otimes _{{\wp \Sigma _{\mathcal L}}_i} {Th}_i$ , and let us denote by $(\wp \Sigma _{\mathcal L}, {Th})$ the coproduct of the two systems in $\mathcal {DS}_0$ , and by $\gamma $ the nucleus associated with its consequence relation. By [Reference Russo17, Theorem 5.3] and Theorem 3.1, There exist ${\wp \Sigma _{\mathcal L}}_i$ -module embeddings $e_i: {Th}_i \to {Th}$ and $g_i: {Th}_i \to M$ , and a unique $\wp \Sigma _{\mathcal L}$ -module morphism $g: M \to {Th}$ such that $g\circ g_i = e_i$ , for $i =1, 2$ , as in the diagram (7). We will show that such a morphism g is surjective but not injective. Surjectivity is actually an immediate consequence of [Reference Russo17, Theorem 5.4] (see also diagram (7) of the same paper).

By [Reference Russo17, Theorem 5.4], for all $i \in I$ , $\wp \Sigma _{\mathcal L} \otimes _{{\wp \Sigma _{\mathcal L}}_i} {Th}_i$ is isomorphic to the lattice of theories ${Th}_i'$ of the deductive system defined on E by means of the axioms and rules of  $\vdash _i$ . Let us denote by $\delta _i$ the nuclei such that ${Th}_i' = \wp E_{\delta _i}$ , for $i =1,2$ , and refer to the following commutative diagram, where $\alpha $ is the isomorphism as in [Reference Russo17, Theorem 5.4], and $g'\circ \alpha = g$ .

For $j \neq i$ , and for any variable x, the formula $x \to _j x$ is a tautology of the j-th system and not one of the i-th system, therefore, $x \to _j x \in \delta _j(\varnothing )$ and $x \to _j x \notin \delta _i(\varnothing )$ . It follows that $(\delta _1(\varnothing ),\delta _2(\varnothing )) \neq (\delta _1(\{x \to _2 x\}), \delta _2(\varnothing ))$ . On the other hand, $x \to _1 x$ and $x \to _2 x$ are both tautologies in ${Th}$ , hence $g'(\delta _1(\varnothing ),\delta _2(\varnothing )) = g'(\delta _1(\{x \to _2 x\}),\delta _2(\varnothing )) = \gamma (\varnothing )$ . It follows that $g(\delta _1(\varnothing ),\delta _2(\varnothing )) = g(\delta _1(\{x \to _2 x\}),\delta _2(\varnothing )) = \gamma (\varnothing )$ and, therefore, g is not injective.

Regarding the so-called “logical amalgamation” presented in [Reference Russo17, Section 6], the situation is slightly different. In order to discuss this point in detail, let us first introduce the pertinent notations.

Let $\{\mathcal {L}_i\}_{i=1}^2$ be propositional languages, and $S_i = (D_i, \vdash _i)$ be deductive systems, of the same fixed type, over $\mathcal {L}_i$ , with associated nuclei $\gamma _i$ and modules of theories ${{Th}_i = (\wp D_i)_{\gamma _i}}$ , for $i=1,2$ . Let $\mathcal M$ also be a common fragment of the $\mathcal {L}_i$ ’s and ${S = (C, \vdash _\beta )}$ a deductive system on $\mathcal M$ whose domain is, again, of the same type of $D_1$ and $D_2$ , with associated nucleus $\beta $ and module of theories ${Th}' = \wp C_\beta $ , and such that there exist conservative interpretations $r_i: {Th}' \to {Th}_i$ , $i=1,2$ .

Last, with an abuse of notation, namely, identifying the languages with their sets of connectives, let

$$ \begin{align*}\mathcal{L} = ((\mathcal{L}_1 \setminus \mathcal M) \sqcup (\mathcal{L}_2 \setminus \mathcal M)) \cup \mathcal M,\end{align*} $$

$\sqcup $ denoting the disjoint union, so that $\mathcal M$ is now a fragment of $\mathcal {L}$ too, and $\mathcal {L}$ has no further overlapping with (the copies of) $\mathcal {L}_1$ and $\mathcal {L}_2$ .

From [Reference Russo17, Corollary 4.3] we know that $\wp \Sigma _{\mathcal L}$ is the amalgamated coproduct of $\wp \Sigma _{\mathcal {L}_1}$ and $\wp \Sigma _{\mathcal {L}_2}$ with respect to the common subquantale $\wp \Sigma _{\mathcal M}$ . In a more general setting, as the one considered in [Reference Russo17, Section 6], in which $\mathcal M$ is not exactly a common fragment of the $\mathcal {L}_i$ ’s but has a translation to each of them, we cannot guarantee that the V-formation of quantales of substitutions can be amalgamated, because the category of quantales does not have the amalgamation property. In fact, we cannot even guarantee the existence of all pushouts in $\mathcal {DS}_0$ . Therefore, the construction of [Reference Russo17, Section 6] is useful in such a general setting and in any concrete situation in which one may not want to identify connectives of the initial languages.

Corollary 4.3 of [Reference Russo17] and Theorem 3.3 provide the correct way to obtain the amalgamated coproduct in $\mathcal {QM}$ of the V-formation

$$ \begin{align*}(\wp\Sigma_{\mathcal{L}_1},{Th}_1) \stackrel{(\iota_1,r_1)}{\longleftarrow} (\wp\Sigma_{\mathcal M},{Th}') \stackrel{(\iota_2,r_2)}{\longrightarrow} (\wp\Sigma_{\mathcal{L}_2},{Th}_2),\end{align*} $$

where $\iota _1$ and $\iota _2$ are the quantale embeddings induced by the inclusions of $\mathcal M$ in the other two languages.

On the other hand, thanks to Theorem 5.1, in this specific case we shall be able to obtain an even more elegant amalgamation in $\mathcal {DS}_0$ than the one presented in [Reference Russo17]. Indeed, with the given notations, let us also denote by $e_i$ , $i = 1,2$ , the inclusion maps of $\wp \Sigma _{\mathcal {L}_1}$ and $\wp \Sigma _{\mathcal {L}_2}$ in $\wp \Sigma _{\mathcal L}$ , and by $\iota _i$ , $i=1,2$ , the inclusion maps of $\wp \Sigma _{\mathcal M}$ in $\wp \Sigma _{\mathcal {L}_1}$ and  $\wp \Sigma _{\mathcal {L}_2}$ . Then we have the following theorem.

Theorem 5.3. The amalgamated coproduct of the V-formation

$$ \begin{align*}(\wp\Sigma_{\mathcal{L}_1},{Th}_1) \stackrel{(\iota_1,r_1)}{\longleftarrow} (\wp\Sigma_{\mathcal M},{Th}') \stackrel{(\iota_2,r_2)}{\longrightarrow} (\wp\Sigma_{\mathcal{L}_2},{Th}_2)\end{align*} $$

in $\mathcal {DS}_0$ is $(\wp \Sigma _{\mathcal L}, {Th})$ , where ${Th}$ is the module of theories of the $\mathcal {L}$ -system whose consequence relation is determined by the union of the axioms and rules of $S_1$ , $S_2$ , and the set of rules

$$ \begin{align*}\Theta = \left\{\frac{e_ir_i(\{\varphi\})}{e_kr_k(\{\varphi\})} \bigg| \varphi \in C, i \neq k \in \{1,2\}\right\}\!.\end{align*} $$

Proof. By [Reference Russo17, Corollary 4.3],

is the diagram of an amalgamated coproduct of quantales. Then the assertion follows readily from Theorem 3.3 and [Reference Russo17, Theorems 6.4, 6.5, and 6.6].