# The Distributive Full Lambek Calculus with Modal Operators

Daniel Rogozin  Lomonosov Moscow State University
Moscow, Russia
Serokell OÜ
Tallinn, Estonia

###### Abstract

In this paper, we study logics of bounded distributive residuated lattices
with modal operators considering $\Box$ and $\Diamond$ in a noncommutative
setting. We introduce relational semantics for such substructural modal
logics. We prove that any canonical logic is Kripke complete via discrete
duality and canonical extensions. That is, we show that a modal extension of
the distributive full Lambek calculus is the logic of its frames if its
variety is closed under canonical extensions. After that, we establish a
Priestley-style duality between residuated distributive modal algebras and
topological Kripke structures based on Priestley spaces.

###### keywords:

The Lambek calculus, canonical extensions, bounded distributive lattice
expansions, Priestley-style duality, residuated lattices

111The research is supported by the Presidential Council, research grant
MK-430.2019.1.

##  1 Introduction

Substructural logic is logic lacking some of the well-known structural rules
such as contraction, weakening, or exchange. Algebraically, substructural
logics represent ordered residuated algebras [16]. One may examine modalities
in substructural logics at least in two perspectives. Modalities in those
logics are pretty helpful is such philosophical issues such as a relevant
necessity. The second perspective is more applied and related to such issues
as resource management. Here, linear logic proved its efficiency in computer
science and linguistics.

The computer science applications are more related to resource-sensitive
computation and related applications in type theory [1] [25].

The noncommutative version of linear logic, the Lambek calculus [35], has
plenty of applications in linguistics, for instances, proof-theoretical
characterisation of inference in Lambek grammars, the equivalent version of
context-free grammars [39]. The Lambek calculus characterises inference in
categorial grammars. There are several approaches to consider categorial
grammars from a broader modal point of view as well, see the paper by van
Benthem [50], for example. Modalities in such logics (the $!$-modality, to be
more precise) introduce lacking structural rules in a restricted way:

$\Gamma,\Delta\Rightarrow B$ $\Gamma,!A,\Delta\Rightarrow B$

$\Gamma,!A,B,\Delta\Rightarrow C$ $\Gamma,B,!A,\Delta\Rightarrow C$

$\Gamma,!A,B,!A,\Delta\Rightarrow C$ $\Gamma,!A,B,\Delta\Rightarrow C$

$\Gamma,!A,!A,\Delta\Rightarrow B$ $\Gamma,!A,\Delta\Rightarrow B$

$\Gamma,!A,B,!A,\Delta\Rightarrow C$ $\Gamma,B,!A,\Delta\Rightarrow C$

Modal extensions of linear logic have an interpretation within the context of
resource management based on the phase semantics proposed by Girard [24].
Algebraically, exponential modalities were studied by Ono as additional
exponential operators on FL algebras [36]. The Lambek calculus and its modal
extensions also have the cover semantics proposed by Goldblatt [28] [29]. The
abstract polymodal case of such an extension of the full Lambek calculus was
recently studied by Kanovich, Kuznetsov, Scedrov, and Nigam [32]. In this
paper, (sub)exponential modalities are considered from proof-theoretical and
complexity perspectives.

The basic Lambek calculus is complete with respect to so-called language
models, residuated semigroups on subsets of free semigroup [40]. The Lambek
calculus is complete with respect to subsets of a transitive relation as well,
see [2]. Dunn, Gehrke, Palmigiano, and other authors considered relational
semantics for the Lambek calculus using canonical extensions [7] [12].
Alternatively, one may consider bi-approximation semantics for substructural
logic studied by Suzuki [47].

In this paper, we study the distributive version of the full Lambek calculus
extended with normal modal operators $\Box$ and $\Diamond$ to consider a
broader class of noncommutative modalities as an abstraction of storage
operators in noncommutative linear logic in a distributive setting. We
introduce noncommutative Kripke frames, relational structures for the
distributive Lambek calculus extended with binary modal relations. We
establish a discrete duality between such Kripke frames and perfect
distributive residuated modal algebras developing an approach proposed in
[22]. After that, we overview canonical extensions of related modal algebras
applying techniques provided in [12] [17] [21] to show that any canonical
residuated distributive modal logic is Kripke complete. We also prove that the
subexponential modality axioms are canonical ones. Thus, we show that the
corresponding logics enriched with subexponentials are Kripke complete.
Finally, we extend the obtained duality to topological duality between
residuated distributive modal algebras and special topological Kripke spaces
based on bDRL-spaces, Priestley spaces with a ternary relation dual algebras
of which are bounded distributive residuated lattices [15]. We also use some
ideas from positive modal and intuitionistic modal logics [5] [38].

The text contains a short appendix with the brief survey on canonical
extensions and duality for bounded distributive lattices to keep the paper
self-contained.

##  2 The distributive Lambek calculus with modal operators

In this section, we formulate the distributive full Lambek calculus enriched
with modal operators. We represent such logics with pairs of formulas that
have the form $\varphi\vdash\psi$. One needs to read that as “$\psi$ is
derivable from $\varphi$”.

The language extends the language of the full Lambek calculus with modal
operators $\Box$ and $\Diamond$ as follows:

$\varphi,\psi::=\bot\>|\>\top\>|\>p\>|\>(\varphi\bullet\psi)\>|\>(\varphi\setminus\psi)\>|\>(\varphi/\psi)\>|\>(\varphi\lor\psi)\>|\>(\varphi\land\psi)\>|\>\Box\varphi\>|\>\Diamond\varphi$.

By a _substructural distributive normal modal logic_ , we mean some set of
pairs $\vartheta\vdash\psi$, where $\vartheta$, $\psi$ are formulas, according
to the following definition:

######  Definition 2.1.

A substructural normal distributive modal logic is a set of sequents $\Lambda$
that contains the axioms below and closed under the following inference rules:

$p\vdash p$

  * •

$\bot\vdash p$

  * •

$p\vdash\top$

  * •

$p_{i}\vdash p_{1}\lor p_{2},i=1,2$

  * •

$p_{1}\land p_{2}\vdash p_{i},i=1,2$

  * •

$p\land(q\lor r)\vdash(p\land q)\lor(p\land r)$

  * •

$(p\bullet q)\bullet r\dashv\vdash p\bullet(q\bullet r)$

  * •

$p\bullet{\bf 1}\dashv\vdash{\bf 1}\bullet p\dashv\vdash p$

  * •

$\Diamond(p\lor q)\vdash\Diamond p\lor\Diamond q$

  * •

$\Diamond\bot\vdash\bot$

  * •

$\Box p\land\Box q\vdash\Box(p\land q)$

  * •

$\top\vdash\Box\top$

  * •

$\Box p\bullet\Box q\vdash\Box(p\bullet q)$

$\varphi\vdash\psi$ $\psi\vdash\theta$ $\varphi\vdash\theta$

$\varphi\vdash\psi$ $\theta\vdash\psi$ $\varphi\lor\theta\vdash\psi$

$\varphi\bullet\theta\vdash\psi$ $\theta\vdash\varphi\setminus\psi$

$\varphi\vdash\psi$ $\Box\varphi\vdash\Box\psi$

$\varphi(p)\vdash\psi(p)$ $\varphi[p:=\gamma]\vdash\psi[p:=\gamma]$

$\varphi\vdash\psi$ $\varphi\vdash\theta$ $\varphi\vdash\psi\land\theta$

$\theta\vdash\varphi\setminus\psi$ $\varphi\bullet\theta\vdash\psi$

$\varphi\vdash\psi$ $\Diamond\varphi\vdash\Diamond\psi$

Substructural normal distributive modal logic extends distributive normal
modal logic with residuals, product, and the axiom connecting $\Box$ and
$\bullet$. See this paper [22] to examine in-depth logics of bounded
distributive lattices with modal operators that we extend.

We introduce ternary Kripke frames with the additional binary modal relations.
Such a ternary frame might be considered as a noncommutative generalisation of
a relevant Kripke, see, e.g., here [46]. As it is usual in the relational
semantics of substructural logic, product and residuals have the ternary
semantics as in, e.g., [2] [11] [43].

######  Definition 2.2.

A Kripke frame is a structure $\mathcal{F}=\langle
W,\leq,R,R_{\Box},R_{\Diamond},\mathcal{O}\rangle$, where $\langle
W,\leq,\rangle$ is a partial order, $R$ is a ternary relation on $W$,
$R_{\Box},R_{\Diamond}$ are binary relations on $W$, and $\mathcal{O}\subseteq
W$ such that for all $\forall u,v,w,u^{\prime},v^{\prime},w^{\prime}\in W$

  1. (1)

$Ruvw\>\&\>wR_{\Box}w^{\prime}\Rightarrow\exists x,y\in
W\>\>Rxyw^{\prime}\>\&\>uR_{\Box}x\>\&\>vR_{\Box}y$

  2. (2)

$\exists x\in W(Ruwx\>\&\>Rxu^{\prime}v^{\prime})\Leftrightarrow\exists y\in
W(Rwu^{\prime}y\>\&\>Ruyv^{\prime})$

  3. (3)

$Ruvw\>\&\>u^{\prime}\leq u\Rightarrow Ru^{\prime}vw$,
$Ruvw\>\&\>v^{\prime}\leq v\Rightarrow Ruv^{\prime}w$, $Ruvw\>\&\>w\leq
w^{\prime}\Rightarrow Ruvw^{\prime}$

  4. (4)

$\forall o\in\mathcal{O}\>\>Rvow\Leftrightarrow Rovw$

  5. (5)

$v\leq w\Leftrightarrow\exists o\in\mathcal{O}Rvow$

  6. (6)

$\mathcal{O}$ is upwardly closed

  7. (7)

$u\leq v\>\&\>vR_{\Box}w\Rightarrow uR_{\Box}w$ and $u\leq
v\>\&\>uR_{\Diamond}w\Rightarrow vR_{\Diamond}w$

A Kripke model is a Kripke frame equipped with a valuation function that maps
each propositional variable to $\leq$-upwardly closed subset of worlds.

######  Definition 2.3.

Let $\mathcal{F}=\langle W,\leq,R,R_{\Box},R_{\Diamond},\mathcal{O}\rangle$ be
a Kripke frame, a Kripke model is a pair
$\mathcal{M}=\langle\mathcal{F},\vartheta\rangle$, where
$\vartheta:\operatorname{PV}\to\operatorname{Up}(W,\leq)$. Here,
$\operatorname{Up}(W,\leq)$ is the collection of all upwardly closed sets. The
connectives have the following semantics:

  1. (1)

$\mathcal{M},w\models p\Leftrightarrow w\in\vartheta(p)$

  2. (2)

$\mathcal{M},w\models\top$, $\mathcal{M},w\not\models\bot$,
$\mathcal{M},w\models{\bf 1}\Leftrightarrow w\in\mathcal{O}$

  3. (3)

$\mathcal{M},w\models\varphi\bullet\psi\Leftrightarrow\exists u,v\in
W\>Ruvw\>\&\>\mathcal{M},u\models\varphi\>\&\>\mathcal{M},v\models\psi$

  4. (4)

$\mathcal{M},w\models\varphi\setminus\psi\Leftrightarrow\forall u,v\in
W\>Ruwv\>\&\>\mathcal{M},u\models\varphi\text{ implies
}\mathcal{M},v\models\psi$

  5. (5)

$\mathcal{M},w\models\psi/\varphi\Leftrightarrow\forall u,v\in
W\>Ruwv\>\&\>\mathcal{M},u\models\varphi\text{ implies
}\mathcal{M},v\models\psi$

  6. (6)

$\mathcal{M},w\models\varphi\land\psi\Leftrightarrow\mathcal{M},w\models\varphi\>\&\>\mathcal{M},w\models\psi$

  7. (7)

$\mathcal{M},w\models\varphi\lor\psi\Leftrightarrow\mathcal{M},w\models\varphi\>\text{or}\>\mathcal{M},w\models\psi$

  8. (8)

$\mathcal{M},w\models\Box\varphi\Leftrightarrow\forall v\in
R_{\Box}(w)\>\>\mathcal{M},v\models\varphi$

  9. (9)

$\mathcal{M},w\models\Diamond\varphi\Leftrightarrow\exists v\in
R_{\Diamond}(w)\>\>\mathcal{M},v\models\varphi$

  10. (10)

$\mathcal{M},w\models\varphi\vdash\psi\Leftrightarrow\mathcal{M},w\models\varphi\Rightarrow\mathcal{M},w\models\psi$

  11. (11)

$\mathcal{M}\models\varphi\vdash\psi\Leftrightarrow\forall w\in
W\>\mathcal{M},w\models\varphi\vdash\psi$

The following definitions are also standard ones.

######  Definition 2.4.

Let $\mathcal{F}$ be a Kripke frame

  1. (1)

Let $\varphi\vdash\psi$ be a sequent, then
$\mathcal{F}\models\varphi\vdash\psi$ iff for all valuations $\vartheta$
$\langle\mathcal{F},\vartheta\rangle\models\varphi\vdash\psi$.

  2. (2)

$\operatorname{Log}(\mathcal{F})=\\{\varphi\vdash\psi\>|\>\mathcal{F}\models\varphi\vdash\psi\\}$.

  3. (3)

Let $\mathbb{F}$ be a class of Kripke frames, then
$\operatorname{Log}(\mathbb{F})=\bigcap\limits_{\mathcal{F}\in\mathbb{F}}\operatorname{Log}(\mathcal{F})$.

  4. (4)

Let $\Lambda$ be a substructural normal modal logic, then
$\operatorname{Frames}(\mathcal{L})=\\{\mathcal{F}\>|\>\mathcal{F}\models\mathcal{L}\\}$
and $\mathcal{L}$ is _complete_ iff
$\mathcal{L}=\operatorname{Log}(\operatorname{Frames}(\mathcal{L}))$.

By ${\bf L}_{\bf K}$, we mean the minimal substructural distributive normal
modal logic, the minimal set of sequents containing the axioms above and
closed under the required inference rules.

The soundness theorem is the standard one.

######  Theorem 2.5.

Let $\mathbb{F}$ be a class of Kripke frames, then
$\operatorname{Log}(\mathbb{F})$ is a substructural distributive normal modal
logic.

######  Proof 2.6.

Let us show that $\mathcal{F}\models\Box p\bullet\Box
q\Rightarrow\Box(p\bullet q)$, where $\mathcal{F}=\langle
W,R,R_{\Box},R_{\Diamond},\mathcal{O}\rangle$ is an arbitrary frame. Let
$\vartheta$ be a valuation and
$\mathcal{M}=\langle\mathcal{F},\vartheta\rangle$ a model such that
$\mathcal{M},w\models\Box p\bullet\Box q$, and $w\in W$. Then there exists
$u,v$ such that $Ruvw$, $\mathcal{M},u\models\Box p$,
$\mathcal{M},v\models\Box q$. On the other hand, let $w^{\prime}\in
R_{\Box}(w)$. $Ruvw\>\&\>wR_{\Box}w^{\prime}$ implies $\exists x,y\in
W\>\>Rxyw^{\prime}\>\&\>uR_{\Box}x\>\&\>vR_{\Box}y$. $\mathcal{M},u\models\Box
p$, $\mathcal{M},v\models\Box q$ implies that for each $x\in
R_{\Box}(u)\>\mathcal{M},x\models p$ and for each $y\in R_{\Box}(v)$.
$Rxyw^{\prime}$ implies $\mathcal{M},w^{\prime}\models p\bullet q$. Thus,
$\mathcal{M},w\models\Box(p\bullet q)$

One may extend the notion of a bounded morphism for the relevant case to have
homomorphisms between Kripke frames and models that preserve truth.

######  Definition 2.7.

Let $\mathcal{F}_{1},\mathcal{F}_{2}$ be Kripke frames, a map
$f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ is a bounded morphism, if:

  1. (1)

$R_{1}uvw\Rightarrow R_{2}f(u)f(v)f(w)$

  2. (2)

$R_{2}f(u)v^{\prime}w^{\prime}\Rightarrow\exists v,w\>v^{\prime}\leq
f(v)\>\&\>f(w)\leq w^{\prime}\>\&\>Ruvw$

  3. (3)

$R_{2}u^{\prime}f(v)w^{\prime}\Rightarrow\exists u,w\>u^{\prime}\leq
f(u)\>\&\>f(w)\leq w^{\prime}\>\&\>Ruvw$

  4. (4)

$R_{2}u^{\prime}v^{\prime}f(w)\Rightarrow\exists u,v\>u^{\prime}\leq
f(u)\>\&\>v^{\prime}\leq f(v)\>\&\>Ruvw$

  5. (5)

$f[(R_{\nabla})_{1}(x)]=(R_{\nabla})_{2}(f(x))$, $\nabla=\Box,\Diamond$

  6. (6)

$f^{-1}[\mathcal{O}_{2}]=\mathcal{O}_{1}$

By the notation $\mathcal{F}_{1}\twoheadrightarrow\mathcal{F}_{2}$ we mean
that there exists a surjective bounded morphism
$f:\mathcal{F}_{1}\twoheadrightarrow\mathcal{F}_{2}$ and we call such a map
_$p$ -morphism_. Let $\mathcal{F}_{1}$, $\mathcal{F}_{2}$ be Kripke frames,
$\vartheta_{1}$, $\vartheta_{2}$ valuations on $\mathcal{F}_{1}$ and
$\mathcal{F}_{2}$ correspondingly, and $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ a
bounded morphism. Then $f:\mathcal{M}_{1}\to\mathcal{M}_{2}$ is a bounded
morphism of models, if

$\mathcal{M}_{1},w\models p_{i}\Leftrightarrow\mathcal{M}_{2},f(w)\models
p_{i}$ for each propositional variable $p_{i}$.

The following lemma has the standard proof given in [4] [6].

######  Lemma 2.8.

  1. (1)

$\mathcal{M}_{1},w\models\varphi\Leftrightarrow\mathcal{M}_{2},f(w)\models\varphi$.

  2. (2)

$\mathcal{F}_{1}\twoheadrightarrow\mathcal{F}_{2}$ implies
$\operatorname{Log}(\mathcal{F}_{1})\subseteq\operatorname{Log}(\mathcal{F}_{2})$.

  3. (3)

$\mathcal{F}_{1}\cong\mathcal{F}_{2}$ implies
$\operatorname{Log}(\mathcal{F}_{1})=\operatorname{Log}(\mathcal{F}_{2})$.

##  3 Residuated distributive modal algerbas

In this section, we study algebraic semantics and canonical extensions for
substructural distributive modal logic. The required lattice-theoretic and
canonical extensions definitions and notations are explained in the appendix.
Let us define a residuated lattice [30].

######  Definition 3.1.

A residuated lattice is an algebra
$\mathcal{R}=\langle\mathcal{L},\cdot,\setminus,/,\varepsilon\rangle$, where
$\mathcal{L}$ is a bounded lattice, $\cdot$ is a binary associative monotone
operation, $\varepsilon$ is a multiplicative identity, $\setminus$ and $/$ are
residuals, that is, the following equivalence holds for all
$a,b,c\in\mathcal{L}$:

$b\leq a\setminus c\Leftrightarrow a\cdot b\leq c\Leftrightarrow a\leq c/b$

Note that the class of all residuated lattices forms a variety since the
quasi-identities above might be equivalently reformulated as identities, see
[30, Lemma 2.3].

A residuated lattice is called bounded distributive if its lattice reduct is a
bounded distributive lattice. A residuated lattice morphism is a map
$f:\mathcal{L}_{1}\to\mathcal{L}_{2}$ that commutes with all operations in a
usual way.

Let us recall the essential facts about (prime) filters on bounded
distributive residuated lattices, see [15] [49]. As a matter of fact, these
statements hold for an arbitrary distributive lattice ordered semigroup since
those properties of filters and their products do not depend on residuals.

######  Lemma 3.2.

Let $\mathcal{L}$ be a bounded distributive residuated lattice. Let
$X,Y\subseteq\mathcal{L}$ and $X\cdot Y=\\{x\cdot y\>|\>x\in X,y\in Y\\}$. Let
us define $X\bullet Y=\uparrow X\cdot Y$, then

  1. (1)

If $Z\subseteq\mathcal{L}$ is a filter, then $X\cdot Y\subseteq Z$ iff
$X\bullet Y\subseteq Z$.

  2. (2)

If $X,Y\subseteq\mathcal{L}$ are filters, then $X\bullet Y$ is a filter.

  3. (3)

Let $X,Y,Z$ be filters in $\mathcal{L}$ and $Z$ is prime such that
$XY\subseteq Z$, then there exist prime filters $X^{\prime},Y^{\prime}$ such
that $X\subseteq X^{\prime}$, $Y\subseteq Y^{\prime}$, and
$X^{\prime}Y^{\prime}\subseteq Z$.

A residuated distributive modal algebra is a bounded distributive residuated
lattice extended with the operators $\Box$ and $\Diamond$ that distribute over
finite infima and suprema respectively. One may also consider such algebras as
full Lambek algebras [36] [37] reducts of which are bounded distributive
lattices. Here, modalities are merely the ${\bf K}$-like operators without any
additional requirements except the connection between $\Box$ and $\cdot$. We
require that $\Box$ is also “weakly normal” with respect to the product. Such
a “weak normality” corresponds to the promotion principle which is widespread
in linear logic. This principle often has the ${\bf K}4$ form, where formulas
in the premise are boxed from the left. This version of the promotion rule is
rather the ${\bf K}$-rule than the ${\bf K}4$ one:

$\varphi_{1}\bullet\dots\bullet\varphi_{n}\vdash\psi$
$\Box\varphi_{1}\bullet\dots\bullet\Box\varphi_{n}\vdash\Box\psi$

The inference rule also allows one to obtain the Kripke axioms formulated in
terms of residuals as, e.g.,
$\Box(\varphi\setminus\psi)\Rightarrow\Box\varphi\setminus\Box\psi$ and
$\Box(\psi/\varphi)\Rightarrow\Box\psi/\Box\varphi$.

This “weak normality” requirement is introduced as the additional inequation,
more precisely:

######  Definition 3.3.

A residuated distributive modal algebra (RDMA) is an algebra
$\mathcal{M}=\langle\mathcal{R},\Box,\Diamond\rangle$ with the following
conditions for each $a,b\in\mathcal{R}$:

  1. (1)

$\Box(a\land b)=\Box a\land\Box b$, $\Box\top=\top$

  2. (2)

$\Diamond(a\lor b)=\Diamond a\lor\Diamond b$, $\Diamond\bot=\bot$

  3. (3)

$\Box a\cdot\Box b\leq\Box(a\cdot b)$

An RDMA homomorphism is a bounded distributive residuated lattice homomorphism
$f:\mathcal{M}_{1}\to\mathcal{M}_{2}$ such that $f(\Box a)=\Box(f(a))$ and
$f(\Diamond a)=\Diamond(f(a))$.

One may associate with an arbitrary substructural normal modal logic its
variety of RDMAs as follows:

######  Definition 3.4.

Let $\Lambda$ be a substructural normal modal logic, $\mathcal{V}_{\Lambda}$
is a variety defined by the set of inequations
$\\{\varphi\leq\psi\>|\>\Lambda\vdash\varphi\vdash\psi\\}$.

Note that $\varphi$, $\psi$ are terms of the signature
$\langle\wedge,\vee,\bot,\top,\cdot,\setminus,/,\varepsilon,\Box,\Diamond\rangle$
in such inequations as $\varphi\leq\psi$. One has an algebraic completeness
for each substructural distributive normal modal logic as usual.

######  Theorem 3.5.

Let $\Lambda$ be a substructural normal modal logic, then there exists an RDMA
$\mathcal{R}_{\Lambda}$ such that $\varphi\vdash\psi\in\Lambda$ iff
$\mathcal{R}_{\Lambda}\models\varphi\leq\psi$.

One such RDMA is the free countably generated algebra in the variety
$\mathcal{V}_{\Lambda}$, the Lindenbaum-Tarski algebra up to isomorphism.

The following statement also holds according to the general technique, see
[26]:

######  Lemma 3.6.

Let $\mathcal{\Lambda}$ be a residuated distributive normal modal logic, then
the map $\Lambda\mapsto\mathcal{V}_{\Lambda}$ is the isomorphism between the
lattice of residuated distributive normal modal logics and the lattice of
varieties of RDMAs.

We define a completely distributive residuated perfect lattice as a
distributive version of a residuated perfect one defined in [12].

######  Definition 3.7.

A distributive residuated lattice $\mathcal{L}=\langle
L,\bigvee,\bigwedge,\cdot,\setminus,/,\varepsilon\rangle$ is called perfect
distributive residuated lattice, if:

  * •

Its lattice reduct is perfect distributive, see Definition .3.

  * •

$\cdot$, $\setminus$, and $/$ are binary operations on $L$ such that $/$ and
$\setminus$ right and left residuals of $\cdot$, repsectively; $\cdot$ is a
complete operator on $\mathcal{L}$, and
$/:\mathcal{L}\times\mathcal{L}^{\delta}\to\mathcal{L}$,
$\setminus:\mathcal{L}^{\delta}\times\mathcal{L}\to\mathcal{L}$ are complete
dual operators, where $\mathcal{L}^{\delta}$ is the dual of $\mathcal{L}$.

Here we formulate canonical extensions for bounded distributive lattices with
a residuated family in the fashion of [18], where the author introduces
canonical extensions for Heyting algebras. Here we take a generalised version
of that construction formulated for residuated lattices, see [17].

######  Lemma 3.8.

Let $\mathcal{L}=\langle L,\cdot,\setminus,/,\varepsilon\rangle$ be a bounded
distributive residuated lattice, then $\mathcal{L}^{\sigma}=\langle
L^{\sigma},\cdot^{\sigma},\setminus^{\pi},/^{\pi},\varepsilon\rangle$ is a
perfect distributive residuated lattice.

Instead of proof that repeats this one [17], we just define $\cdot^{\sigma}$,
$\setminus^{\pi}$, and $/^{\pi}$ explicitly. Here we note that the canonical
extension of a lattice reduct is a perfect distributive lattice [20].

Let $a,a^{\prime}\in\mathcal{F}(\mathcal{L}^{\sigma})$ and
$b\in\mathcal{F}(\mathcal{L}^{\sigma})$, then

  1. (1)

$a\setminus^{\pi}b=\bigvee\\{x\setminus y\>|\>a\leq x\in\mathcal{L}\ni y\leq
b\\}$ and similarly for the right residual

  2. (2)

$a\cdot^{\sigma}a^{\prime}=\bigwedge\\{x\cdot x^{\prime}\>|\>a\leq
x\in\mathcal{L}\>\&\>a\leq x^{\prime}\in\mathcal{L}\\}$

Let $a,b\in\mathcal{L}^{\sigma}$, then.

  1. (1)

$a\cdot^{\sigma}b=\bigvee\\{x\cdot^{\sigma}y\>|\>a\geq
x\in\mathcal{F}(\mathcal{L}^{\sigma})\>\&\>b\geq
y\in\mathcal{F}(\mathcal{L}^{\sigma})\\}$

  2. (2)

$a\setminus^{\pi}b=\bigwedge\\{x\setminus^{\pi}y\>|\>a\geq
x\in\mathcal{F}(\mathcal{L}^{\sigma})\>\&\>b\leq
y\in\mathcal{I}(\mathcal{L}^{\sigma})\\}$ and $b/^{\pi}a$ is defined similarly

The residuation property follows from the meet-density of
$\mathcal{F}(\mathcal{L}^{\sigma})$ and join-density of
$\mathcal{I}(\mathcal{L}^{\sigma})$ in $\mathcal{L}^{\sigma}$. Hence
$\mathcal{L}^{\sigma}$ is a perfect distributive residuated lattice.

Let us describe the discrete duality for perfect distributive residuated
lattices. Here we concretise the construction that establishes the discrete
duality between perfect residuated lattices and perfect posets with ternary
relation in [12] within a distributive setting. We piggyback the Raney
representation of perfect distributive lattices as algebras of downsets of
completely join-irreducible elements [42] that generalise Birkhoff
representation for finite lattices [3]. We just recall that any perfect
distributive lattice $\mathcal{L}$ is isomorphic to the lattice
$\operatorname{Down}(\mathcal{J}^{\infty}(\mathcal{L}))$ mapping
$a\in\mathcal{L}$ to $\mathcal{J}^{\infty}(\mathcal{L})\cap\downarrow a$.

This representation might be extended to the duality between the categories of
perfect distributive lattices and posets.

Let $\mathcal{L}$ be a perfect distributive residuated lattice. We define the
relation
$R\subseteq\mathcal{J}^{\infty}(\mathcal{L})\times\mathcal{J}^{\infty}(\mathcal{L})\times\mathcal{J}^{\infty}(\mathcal{L})$
as $Rabc\Leftrightarrow a\cdot b\leq c$. Let us put
$\mathcal{O}=\uparrow\varepsilon$, where $\varepsilon$ is a multiplicative
identity. The structure
$\mathcal{L}_{+}=\langle\mathcal{J}^{\infty}(\mathcal{L}),\leq,R,\mathcal{O}\rangle$
is the _dual frame_ of a perfect distributive residuated lattice
$\mathcal{L}$.

Let $\langle W,\leq\rangle$ be a poset and $R\subseteq W^{3}$, $\mathcal{O}$
with the conditions (ii)-(vi) from Definition 2.4. Let us define the following
operations on $\operatorname{Up}(W,\leq)$:

  * •

$A\setminus B=\\{w\in W\>|\>\forall u,v\in W\>Ruwv\>\&\>u\in A\Rightarrow v\in
B\\}$

  * •

$B/A=\\{w\in W\>|\>\forall u,v\in W\>Rwuv\>v\in A\Rightarrow v\in B\\}$

  * •

$A\cdot B=\\{w\in W\>|\>\exists u,v\in W\>Ruvw\>\&\>u\in A\>\&\>v\in B\\}$

These operations are clearly well defined. Let us check $A\setminus
B\in\operatorname{Up}(W,\leq)$, if $A,B\in\operatorname{Up}(W,\leq)$. Let
$x\in A\setminus B$ and $x\leq y$, then $A\cdot\\{x\\}\subseteq B$. Let
$w\in\\{y\\}\cdot A$, then there exists $a\in A$ such that $Ryaw$, then $Rxaw$
by the item (iii), Definition 2.4. Thus, $\\{y\\}\cdot A\subseteq B$.
Similarly, $B/A\in\operatorname{Up}(W,\leq)$. The residuation property for
these operations holds immediately.

The following theorem establishes the discrete duality between perfect
distributive residuated algebras and posets with a ternary relation that
encodes the product. Let us call such a poset with the relation as above a
_ternary Kripke frame_.

######  Theorem 3.9.

  1. (1)

Let $\mathcal{R}$ be a perfect distributive residuated lattice, then
$\mathcal{R}\cong(\mathcal{R}_{+})^{+}$.

  2. (2)

Let $\mathcal{F}$ be a ternary Kripke frame, then
$\mathcal{F}\cong(\mathcal{F}^{+})_{+}$.

######  Proof 3.10.

  1. (1)

Let $R$ be a lattice reduct of $\mathcal{R}$. Accoding to the Raney
representation,
$\eta:R\cong\operatorname{Up}(\mathcal{J}^{\infty}(R),\leq_{\delta})$ such
that $\eta:a\mapsto\\{b\in\mathcal{J}^{\infty}(R)\>|\>a\leq_{\delta}b\\}$,
where $\leq_{\delta}$ is a dual order on $\mathcal{J}^{\infty}(R)$. Let us
ensure that this isomorphism also preserves products and residuals.

Let $z\in\eta(a)\cdot\eta(b)$, then there exists $x\in\eta(a)$ and
$y\in\eta(b)$ such that $x\cdot y\leq_{\delta}z$. That is, $a\leq_{\delta}x$
and $b\leq_{\delta}y$, so $a\cdot b\leq_{\delta}z$, then $z\in\eta(a\cdot b)$.

Let $z\in\eta(a\cdot b)$, then $z$ is a join-irreducible element such that
$a\cdot b\leq_{\delta}z$. Then $\uparrow z$ is a prime filter since $R$ is
perfect distributive. It is clear that $\uparrow a\cdot\uparrow
b\subseteq\uparrow b$. By Lemma 3.2, there exists prime filters $A$ and $B$
such that $\uparrow a\subseteq A$, $\uparrow b\subseteq B$, $A\cdot\uparrow
b\subseteq\uparrow z$ and $\uparrow a\cdot B\subseteq\uparrow z$. $R$ is
completely distributive, so there exists
$a^{\prime},b^{\prime}\in\mathcal{J}^{\infty}(R)$ such that $\uparrow
a^{\prime}=A$ and $\uparrow b^{\prime}=B$. Moreover, $\uparrow
a\subseteq\uparrow a^{\prime}$ and $\uparrow b\subseteq\uparrow b^{\prime}$
implies $a\leq_{\delta}a^{\prime}$ and $b\leq_{\delta}b^{\prime}$, so
$a^{\prime}\in\eta(a^{\prime})$ and $b^{\prime}\in\eta(b)$. So
$a^{\prime}\cdot b^{\prime}\leq_{\delta}z$, and, thus,
$z\in\eta(a)\cdot\eta(b)$.

$\eta$ preserves left and right residuals similarly to [15, Lemma 6.10]. That
was shown for arbitrary bounded residuated residuated lattices and the
extended Priestley embedding.

  2. (2)

$\varepsilon:\langle
W,\leq\rangle\to\langle\mathcal{J}^{\infty}(W,\leq),\leq_{\delta}\rangle$ is a
poset isomorphism such that $\varepsilon:a\mapsto\uparrow a$. This isomorphism
might be extended to the frame isomorphism via the frame conditions that
connect a ternary relation with the partial order.

##  4 Discrete duality and completeness

In this section, we establish a discrete duality between the categories of all
Kripke frames and the category of all perfect residuated distributive modal
algebras. We show that the Thomason theorem [48] holds for normal residuated
distributive modal logics.

######  Definition 4.1.

Let $\mathcal{L}$ be a perfect distributive residuated lattice and
$\Box,\Diamond$ unary operators on $\mathcal{L}$, then
$\mathcal{M}=\langle\mathcal{L},\Box,\Diamond\rangle$ is called a perfect
distributive residuated modal algebra, if for each where
$A\subseteq\mathcal{L}$ and $a,b\in\mathcal{L}$

  * •

$\Box\bigwedge A=\bigwedge\\{\Box a\>|\>a\in A\\}$

  * •

$\Diamond\bigvee A=\bigvee\\{\Diamond a\>|\>a\in A\\}$

  * •

$\Box a\cdot\Box b\leq\Box(a\cdot b)$

Given $\mathcal{M}$, $\mathcal{N}$ perfect residuated distributive modal
algebras, a map $\mathcal{M}\to\mathcal{N}$ is a homomorphism if $f$ is a
complete lattice homomorphism that preserves product, residuals, modal
operators, and the multiplicative identity.

Let us show that the variety of all RDMAs is closed under canonical
extensions.

######  Lemma 4.2.

Let $\mathcal{R}$ be a istributive residuated lattice and
$\mathcal{M}=\langle\mathcal{R},\Box,\Diamond\rangle$ an RDMA, then
$\mathcal{M}^{\sigma}=\langle\mathcal{R}^{\sigma},\Box^{\pi},\Diamond^{\pi}\rangle=\langle\mathcal{R}^{\sigma},\Box^{\sigma},\Diamond^{\sigma}\rangle$
is a perfect DRMA.

######  Proof 4.3.

The lattice reduct of $\mathcal{R}^{\sigma}$ is a perfect distributive
lattice, [20]. In fact, one needs to show that the inequation $\Box a\cdot\Box
b\leq\Box(a\cdot b)$ is canonical. Firstly, let us suppose that
$a,b\in\mathcal{C}(\mathcal{M}^{\sigma})$. Note that
$\Box^{\sigma}a\cdot^{\sigma}\Box^{\sigma}b=\bigwedge\\{\Box x\cdot\Box
y\>|\>a\leq x\in\mathcal{M},b\leq y\in\mathcal{M}\\}$ that follows from the
definition of a filter element, the fact that $\Box^{\sigma}$ preserves all
infina and $\cdot^{\sigma}$ is an order-preserving operation. Then:

$\begin{array}[]{lll}&\Box^{\sigma}a\cdot^{\sigma}\Box^{\sigma}b=&\\\
&\bigwedge\\{\Box x\cdot\Box y\>|\>a\leq x\in\mathcal{L},\leq
x\in\mathcal{L}\\}\leq\bigwedge\\{\Box(x\cdot y)\>|\>a\leq
x\in\mathcal{L}\>\&\>b\leq x\in\mathcal{L}\\}=&\\\
&\bigwedge\Box^{\sigma}\\{(x\cdot y)\>|\>a\leq x\in\mathcal{L}\>\&\>b\leq
x\in\mathcal{L}\\}=&\\\ &\Box^{\sigma}\bigwedge\\{(x\cdot y)\>|\>a\leq
x\in\mathcal{L}\>\&\>b\leq
x\in\mathcal{L}\\}=\Box^{\sigma}(a\cdot^{\sigma}b)&\end{array}$

Let $a,b\in\mathcal{L}^{\sigma}$, then

$\begin{array}[]{lll}&\Box^{\sigma}a\cdot^{\sigma}\Box
b=\bigvee\\{\Box^{\sigma}x\cdot^{\sigma}\Box^{\sigma}y\>|\>a\geq
x\in\mathcal{C}(\mathcal{L}^{\sigma})\>\&\>b\geq
y\in\mathcal{C}(\mathcal{L}^{\sigma})\\}\leq&\\\
&\bigvee\\{\Box^{\sigma}(x\cdot^{\sigma}y)\>|\>a\geq
x\in\mathcal{C}(\mathcal{L}^{\sigma})\>\&\>b\geq
y\in\mathcal{C}(\mathcal{L}^{\sigma})\\}\leq&\\\
&\Box^{\sigma}\bigvee\\{x\cdot^{\sigma}y\>|\>a\geq
x\in\mathcal{C}(\mathcal{L}^{\sigma})\>\&\>b\geq
y\in\mathcal{C}(\mathcal{L}^{\sigma})\\}=\Box^{\sigma}(a\cdot b)&\end{array}$

######  Definition 4.4.

A substructural normal modal logic $\mathcal{L}$ is called canonical, if
$\mathcal{V}_{\mathcal{L}}$ is closed under canonical extensions

The complex algebra of a Kripke frame $\mathcal{F}=\langle
W,\leq,R,R_{\Box},R_{\Diamond},\mathcal{O}\rangle$ is the complex algebra of
the underlying residuated frame $\mathcal{F}^{+}$ with the modal operators
defined as $[R_{\Box}]A=\\{u\in W\>|\>\forall w\>(uR_{\Box}w\Rightarrow w\in
A)\\}$ and $\langle R_{\Diamond}\rangle=\\{u\in W\>|\>\exists w\>(uR_{\Diamond
w}\>\&\>w\in A)\\}$. Here $A$ is upwardly closed subset. These operations are
well-defined. The dual frame of a perfect RDMA $\mathcal{M}=\langle
M,\bigvee,\bigwedge,\Box,\Diamond,\cdot,\setminus,/,\varepsilon\rangle$ is the
dual frame $\mathcal{M}_{+}$ of an underlying perfect distributive residuated
lattice with binary relations on completely join irreducible elements
introduced as $aR_{\Box}b\Leftrightarrow\Box\kappa(a)\leq\kappa(b)$ and
$aR_{\Diamond}b\Leftrightarrow a\leq\Diamond b$. Here, $\kappa$ is an order
isomorphism between between $\mathcal{J}^{\infty}(\mathcal{M})$ and
$\mathcal{M}^{\infty}(\mathcal{M})$.

Logically, Kripke frames and their complex algebras are connected with each
other as follows:

######  Proposition 4.5.

Let $\mathcal{F}$ be a Kripke frame, then
$\operatorname{Log}(\mathcal{F})=\operatorname{Log}(\mathcal{F}^{+})=\\{\varphi\vdash\psi\>|\>\mathcal{F}^{+}\models\varphi\leq\psi\\}$

The following discrete duality theorem is merely a combination of Theorem 3.9
and the similar fact proved for distributive modal algebras and frames for
distributive modal logics [22].

######  Theorem 4.6.

  1. (1)

Let $\mathcal{F}$ be a Kripke frame, then
$\mathcal{F}\cong(\mathcal{F}^{+})_{+}$

  2. (2)

Let $\mathcal{M}$ be a perfect DRMA, then
$\mathcal{M}\cong(\mathcal{M}_{+})^{+}$

  3. (3)

Functors
$(.)_{+}:\operatorname{pDRMA}\rightleftarrows\operatorname{KF}:(.)^{+}$
establish a dual equivalence between the categories of all Kripke frames and
all perfect RDMAs.

######  Proof 4.7.

It is easy to check that if $f:\mathcal{F}_{1}\to\mathcal{F}_{2}$ is a bounded
morphism of Kripke frames, then
$f^{+}:{\mathcal{F}_{2}}^{+}\to{\mathcal{F}_{1}}^{+}$ such that
$f^{+}:A\mapsto f^{-1}[A]$ is a perfect DRMA morphism. It is immediate that
$h_{+}:{\mathcal{M}_{2}}_{+}\to{\mathcal{M}_{1}}_{+}$ is a bounded morphism,
where $h:\mathcal{M}_{1}\to\mathcal{M}_{2}$ is a perfect DRMA morphism. Thus,
the dual equivalence follows from the previous two items and the lemma that
claims that $(.)_{+}$ and $(.)^{+}$ are contravariant functors.

The discrete duality established above together with canonical extensions of
residuated distributive modal algebras provides the following consequence:

######  Theorem 4.8.

Let $\mathcal{L}$ be a canonical substructural distributive modal logic, then
$\mathcal{L}$ is Kripke complete.

######  Proof 4.9.

The proof is similar to the analogous fact proved in [22], but we reproduce a
sketch.

Let $\varphi\vdash\psi\in\mathcal{L}$. Then
$\mathcal{M}_{\mathcal{L}}\models\varphi\leq\psi$ by Theorem 3.5. But
$\mathcal{M}_{\mathcal{L}}\models\varphi\leq\psi$ iff and only
$(\mathcal{M}_{\mathcal{L}})^{\sigma}\models\varphi\leq\psi$ since
$\mathcal{M}_{\mathcal{L}}$ is a subalgebra of
$(\mathcal{M}_{\mathcal{L}})^{\sigma}$ by Lemma 4.2 and the condition
according to which $\mathcal{V}_{\mathcal{L}}$ is a canonical variety. By
discrete duality, Theorem 4.6,
$({(\mathcal{M}_{\mathcal{L}})^{\sigma}}_{+})^{+}\models\varphi\leq\psi$. By
Proposition 4.5,
${(\mathcal{M}_{\mathcal{L}})^{\sigma}}_{+}\models\varphi\vdash\psi$. In fact,
${(\mathcal{M}_{\mathcal{L}})^{\sigma}}_{+}$ is a canonical frame of a given
logic $\mathcal{L}$ and we showed that
${(\mathcal{M}_{\mathcal{L}})^{\sigma}}_{+}\models\mathcal{L}$.

As a consequence, the minimal normal substructural distributive modal logic is
complete with respect to the class of all Kripke frames.

######  Corollary 4.10.

${\bf L}_{\bf K}$ is Kripke-complete.

Now we show that the following sequents that describe modalities as storage
operators are canonical ones. This lemma partially repeats here [12,
Propositions 6.7 – 6.10].

######  Lemma 4.11.

The following sequents are canonical:

  1. (1)

$\Box p\bullet q\dashv\vdash q\bullet\Box p$

  2. (2)

$\Box p\vdash\Box p\bullet\Box p$

  3. (3)

$\Box p\bullet q\vdash\Box p\bullet q\bullet\Box p$, $q\bullet\Box p\vdash\Box
p\bullet q\bullet\Box p$

  4. (4)

$\Box p\vdash\varepsilon$

  5. (5)

$\Box(p\land q)\dashv\vdash\Box p\bullet\Box q$

  6. (6)

$\Box(p\setminus q)\vdash\Diamond p\setminus\Diamond q$ and
$\Box(p/q)\vdash\Diamond p/\Diamond q$

######  Proof 4.12.

Let us check only the third sequent. The rest sequents might be checked
similarly.

Let ${\bf K}_{nc}$ be ${\bf L}_{{\bf K}}\oplus\Box a\bullet b\vdash\Box
a\bullet b\bullet\Box a$ and $\mathcal{V}_{{\bf K}_{nc}}$ its variety. Let us
show that $\mathcal{V}_{{\bf K}_{nc}}$ is closed under canonical extensions.

Let $\mathcal{M}\in\mathcal{V}_{{\bf K}_{nc}}$, one needs to check that
$\mathcal{M}^{\sigma}\in\mathcal{V}_{{\bf K}_{nc}}$. Let
$a,b\in\mathcal{C}(\mathcal{M}^{\sigma})$.

$\begin{array}[]{lll}&\Box^{\sigma}a\cdot^{\sigma}b=\bigwedge\\{\Box
x\>|\>a\leq x\in\mathcal{M}\\}\cdot^{\sigma}\bigwedge\\{y\>|\>b\leq
y\in\mathcal{M}\\}=&\\\ &\bigwedge\\{\Box x\cdot y\>|\>a\leq
x\in\mathcal{M}\>\&\>b\leq y\in\mathcal{M}\\}\leq&\\\ &\bigwedge\\{\Box x\cdot
y\cdot\Box x\>|\>a\leq x\in\mathcal{M}\>\&\>b\leq
y\in\mathcal{M}\\}=\Box^{\sigma}a\cdot^{\sigma}b\cdot^{\sigma}\Box^{\sigma}a&\end{array}$

Let $a,b\in\mathcal{M}^{\sigma}$, then

$\begin{array}[]{lll}&\Box^{\sigma}a\cdot^{\sigma}b=\bigvee\\{\Box^{\sigma}x\cdot^{\sigma}y\>|\>a\geq
x\in\mathcal{C}(\mathcal{M}^{\sigma})\>\&\>b\geq
y\in\mathcal{C}(\mathcal{M}^{\sigma})\\}\leq&\\\
&\bigvee\\{\Box^{\sigma}x\cdot^{\sigma}y\cdot^{\sigma}\Box^{\sigma}x\>|\>a\geq
x\in\mathcal{C}(\mathcal{M}^{\sigma})\>\&\>b\geq
y\in\mathcal{C}(\mathcal{M}^{\sigma})\\}=\Box^{\sigma}a\cdot^{\sigma}b\cdot^{\sigma}\Box^{\sigma}a&\end{array}$

The following completeness theorems follows from Theorem 4.8, Corollary 4.10,
and Lemma 4.11.

######  Corollary 4.13.

Let $\Gamma$ be the set of all sequents from the lemma above and
$\Delta\subseteq\Gamma$. Then $\mathcal{L}={\bf L}_{{\bf K}}\oplus\Delta$ is
Kripke complete.

One may also consider the subexponential polymodal case introduced in [32].
Let us define a subexponential signature:

######  Definition 4.14.

A subexponential signature is an ordered quintuple:
$\Sigma=\langle\mathcal{I},\preceq,\mathcal{W},\mathcal{C},\mathcal{E}\rangle$,
where $\langle\mathcal{I},\preceq\rangle$ is a preorder.
$\mathcal{W},\mathcal{C},\mathcal{E}$ are upwardly closed subsets of
$\mathcal{I}$ and $\mathcal{W}\cap\mathcal{C}\subseteq\mathcal{E}$.

Let us define the following axioms:

  * •

$\Box_{s_{1}}p\bullet\Box_{s_{2}}q\vdash\Box_{s}(p\bullet q)$, $s\preceq
s_{1},s_{2}$

  * •

$\Box_{s}p\vdash p$

  * •

$\Box_{s}p\vdash\Box_{s}\Box_{s}p$

  * •

$\Box_{s}p\bullet q\vdash\Box_{s}p\bullet q\bullet\Box_{s}p$,
$q\bullet\Box_{s}p\vdash\Box_{s}p\bullet q\bullet\Box_{s}p$, where
$s\in\mathcal{C}$

  * •

$\Box_{s}p\bullet q\dashv\vdash p\bullet\Box_{s}q$, $s\in\mathcal{E}$

  * •

$\Box_{s}p\vdash{\bf 1}$, where $s\in\mathcal{W}$

The system $\operatorname{DSMALC}_{\Sigma}$ is a substructural distributive
polymodal logic with modal axioms as above plus $\Box_{s}(p\land
q)\dashv\vdash\Box_{s}p\land\Box_{s}q$ and $\Box_{s}\top\dashv\vdash\top$ for
each $s\in\mathcal{\Sigma}$. For simplicity, let us put the diamond axioms
$\Diamond_{s}(p\lor q)\Leftrightarrow\Diamond_{s}p\lor\Diamond_{s}q$ and
$\Diamond_{s}\bot\dashv\vdash\bot$ with the ${\bf S}4$ axioms for $\Diamond$
$p\vdash\Diamond_{s}p$ and $\Diamond_{s}\Diamond_{s}p\vdash\Diamond_{s}p$ for
each $s\in\mathcal{\Sigma}$ axioms without any additional postulates. The
modal inference rules have the form: from $\varphi\vdash\psi$ infer
$\nabla_{s_{2}}\varphi\vdash\nabla_{s_{1}}\psi$ for $s_{1}\preceq s_{2}$,
where $nabla=\Box,\Diamond$.

######  Theorem 4.15.

$\operatorname{DSMALC}_{\Sigma}$ is canonical and, thus, Kripke complete.

######  Proof 4.16.

One may show that the variety $\mathcal{V}_{\operatorname{DSMALC}_{\Sigma}}$
is canonical showing that $\Box_{s_{1}}p\cdot\Box_{s_{2}}q\leq\Box_{s}(p\cdot
q)$ for $s\preceq s_{1},s_{2}$ is a canonical inequation similarly to Lemma
4.2. The whole statement follows from the observation above and Theorem 4.8,
Lemma 4.11, and Corollary 4.13.

##  5 Topological duality

In this section, we characterise a topological duality for residuated
distributive modal algebras in the same fashion as in [14] [44]. We consider
topological Kripke frames, ternary Kripke frames defined on Priestley spaces
with binary modal relations, the category of which is dually equivalent to the
category of all RDMAs. Alternatively, one may characterise such a duality in
terms of general descriptive frames following the Goldblatt’s approach [27].
See the Appendix to have an explanation of the Priestley duality related
definitions, terms, and notations.

Firstly, we consider a Priestley-style duality for residuated distributive
bounded lattices. We piggyback the construction obtained by Galatos in his PhD
thesis [15]. This construction is a noncommutative generalisation of relevant
spaces, the dual spaces of relevant algebras studied by Urquhart [49]. In
fact, those spaces and their extensions with modal relations are the instances
of relational Priestley spaces [26].

######  Definition 5.1.

Let $\mathcal{X}=\langle X,\tau,\leq\rangle$ be a Priestley space, $R\subseteq
X^{3}$ and $E\subseteq X$. A bDRL-space is a tuple $\mathcal{X}=\langle
X,\tau,\leq,R,E\rangle$ such that:

  1. (1)

For all $x,y,z,w\in X$ there exists $u\in X$ such that $R(x,y,u)$ and
$R(u,z,w)$ iff there exists $v\in X$ such that $R(y,z,v)$ and $R(x,v,w)$.

  2. (2)

For all $x,y,z,w\in X$ if $x\leq y$ then $R(y,u,v)$ implies $R(x,u,v)$,
$R(u,y,v)$ implies $R(u,x,v)$, and $R(u,v,y)$ implies $R(u,v,x))$.

  3. (3)

Let $A,B\subseteq X$ be upwardly closed clopens then
$R[A,B,\rule{7.11317pt}{0.42677pt}]$, $\\{z\in
X\>|\>R[z,B,\rule{7.11317pt}{0.42677pt}]\subseteq A\\}$, and $\\{z\in
X\>|\>R[B,z,\rule{7.11317pt}{0.42677pt}]\\}$ are also clopens.

  4. (4)

For all $x,y,z\in X$ $\neg R(x,y,z)$ iff there exists upwardly closed clopens
$A,B\subseteq X$ such that that there exist $x\in A$ and $y\in B$ such that
$z\notin R[A,B,\rule{7.11317pt}{0.42677pt}])$.

  5. (5)

$E$ is upwardly closed cloped such that if $A$ is clopen then
$R[E,A,\rule{7.11317pt}{0.42677pt}]=R[A,E,\rule{7.11317pt}{0.42677pt}]=A$.

Here $R[A,B,\rule{7.11317pt}{0.42677pt}]$ denotes $\\{c\in X\>|\>\exists a\in
A\>\exists b\in B\>\>Rabc\\}$.

We note that such a space is totally disconnected concerning a ternary
relation according to the fourth condition. We introduce topological Kripke
frames as bDRL-spaces with modal relations as follows.

######  Definition 5.2.

A _modal bDRL-space_ is a structure $\mathcal{X}=\langle
X,\tau,\leq,R,R_{\Box},R_{\Diamond},E\rangle$, where $\langle
X,\tau,\leq,R,E\rangle$ is a bDRL space and the following conditions hold:

  1. (1)

If $A$ is upwardly closed clopen, then $R_{\Box}(A),R_{\Diamond}(A)$ are
upwardly closed clopens.

  2. (2)

For each $x\in X$, $R_{\Box}(x)$ and $R_{\Diamond}(x)$ are closed.

  3. (3)

$Ruvw\>\&\>wR_{\Box}w^{\prime}\Rightarrow\exists x,y\in
W\>\>Rxyw^{\prime}\>\&\>uR_{\Box}x\>\&\>vR_{\Box}y$.

  4. (4)

$u\leq v\>\&\>vR_{\Box}w\Rightarrow uR_{\Box}w$.

  5. (5)

$u\leq v\>\&\>uR_{\Diamond}w\Rightarrow vR_{\Diamond}w$.

Given a residuated distributive modal algebra
$\mathcal{M}=\langle\mathcal{R},\Diamond,\Box\rangle$ on a bounded
distributive lattice $\mathcal{R}$, we define the set of all prime filters
$\operatorname{PF}(\mathcal{L})$ and a map $\phi$ similarly to the bounded
distributive lattice case described in the paper appendix. Let us define a
ternary relation
$R\subseteq\operatorname{PF}(\mathcal{L})\times\operatorname{PF}(\mathcal{L})\times\operatorname{PF}(\mathcal{L})$
as $R(A,B,C)\Leftrightarrow A\bullet B\subseteq C$ and $E=\phi(\varepsilon)$.
We also define binary relations $R_{\Box}$ and $R_{\Diamond}$ on
$\operatorname{PF}(\mathcal{L})$ as $AR_{\Diamond}B\Leftrightarrow b\in
B\Rightarrow\Diamond b\in A$ and $AR_{\Box}B\Leftrightarrow\Box a\in
A\Rightarrow a\in B$.

Standardly, the subbasis of the topology $\tau$ is defined with by the sets
$\phi(a)$ and $-\phi(a)$, $a\in\mathcal{M}$. Then the structure
$\langle\operatorname{PF}(\mathcal{M}),\tau,E,R,R_{\Box},R_{\Diamond}\rangle$
is the _dual space_ of a residuated distributive modal algebra $\mathcal{M}$.

Let $\mathcal{X}=\langle X,\tau,\leq,R,R_{\Box},R_{\Diamond},E\rangle$ be a
modal bDRL-space and $\operatorname{ClUp}(\mathcal{X})$ the set of all
upwardly closed clopens of $\mathcal{X}$. We define product as a binary
operation on $\operatorname{ClUp}(\mathcal{X})$ as $A\circ
B=R[A,B,\rule{7.11317pt}{0.42677pt}]$. Residuals are $A\setminus B=\\{c\in
X\>|\>A\circ c\subseteq B\\}$ and $B/A=\\{c\in X\>|\>c\circ A\subseteq B\\}$.
Modal operators $[R_{\Box}]$, $R_{\Diamond}$ are defined as
$[R_{\Box}]A=\\{a\in X\>|\>\forall b\in X(aR_{\Box}b\Rightarrow b\in A)\\}$
and $\langle R_{\Diamond}\rangle A=\\{a\in X\>|\>\exists b\in
X(aR_{\Diamond}b\>\&\>b\in A)\\}$. The structure
$\langle\operatorname{ClUp}(\mathcal{X}),\cup,\cap,\emptyset,X,\circ,\setminus,/,E,[R_{\Box}],\langle
R_{\Diamond}\rangle\rangle$ is the _dual algebra_ of a modal bDRL-space
$\mathcal{X}$. One may show that $\phi$ commutes with products and residuals
[15], that is:

$\phi$ commutes with modal operators as $\phi(\Diamond a)=\langle
R_{\Diamond}\rangle[\phi(a)]$ and $\phi(\Box a)=[R_{\Box}][\phi(a)]$ that also
may be shown similarly to Proposition 5.2.1 here [38].

The key theorem is the following one:

######  Theorem 5.3.

  1. (1)

The dual algebra of a modal bDRL-space $\mathcal{X}$ is an RDMA.

  2. (2)

The dual space of a residuated distributive modal algebra $\mathcal{M}$ is a
modal bDRL-space.

######  Proof 5.4.

  1. (1)

Let $A,B$ be upwardly closed clopens, let us show that
$[R_{\Box}]A\bullet[R_{\Box}]B\subseteq[R_{\Box}](A\bullet B)$. Let
$c\in[R_{\Box}]A\bullet[R_{\Box}]B$, then $c\in
R[R_{\Box}A,[R_{\Box}]B,\rule{7.11317pt}{0.42677pt}]$. This denotes that
$R(a,b,c)$ for some $a\in R_{\Box}A$ and $b\in R_{\Box}B$. Let $c^{\prime}\in
X$ such that $cR_{\Box}c^{\prime}$, let us show that $c^{\prime}\in A\bullet
B$. $R(a,b,c)$ and $cR_{\Box}c^{\prime}$ implies that
$R(a^{\prime},b^{\prime},c^{\prime})$ for some $a^{\prime}\in R_{\Box}(a)$ and
$b^{\prime}\in R_{\Box}(b)$ by the definition of a modal bDRL-space. Thus,
$a^{\prime}\in A$ and $b^{\prime}\in B$, so $c^{\prime}\in A\bullet B$.

  2. (2)

We check the condition that connect the ternary relation with the
$\Box$-relation. Let $A,B$ be prime filters. Let us suppose that $RABC$ and
$CR_{\Box}C^{\prime}$, where $A,B,C,C^{\prime}$ are prime filters. Let us show
that $RA^{\prime}B^{\prime}C^{\prime}$ for some prime filters
$A^{\prime},B^{\prime}$. Let us put $A_{1}:=\\{a\in X\>|\>\Box a\in A\\}$ and
$B_{1}:=\\{b\in X\>|\>\Box b\in B\\}$. $A_{1}$ and $B_{1}$ are clearly
filters. Now let us show that $A_{1}\cdot B_{1}\subseteq C^{\prime}$. Let
$a\cdot b\in A_{1}\cdot B_{1}$, then $\Box a\in A$ and $\Box b\in B$. So $\Box
a\cdot\Box b\in A\bullet B$, so $\Box(a\cdot b)\in A\bullet B$. Hence
$\Box(a\cdot b)\in C$ and $a\cdot b\in C^{\prime}$. By Lemma 3.2, there exist
prime filters $A^{\prime}\supseteq A_{1}$ and $B^{\prime}\supseteq B_{1}$ such
that $A^{\prime\prime}B^{\prime\prime}\subseteq C^{\prime}$.

Let $A$ be a prime filter, then $R_{\Box}(A)$ and $R_{\Diamond}(A)$ are closed
that might be shown as the well-known Esakia’s lemma [13]. Let $A$ be an
upwardly closed clopen, $R_{\Box}(A)$ and $R_{\Diamond}(A)$ are upwardly
closed clopens. The last two facts might be proved similarly to the
intutionistic modal logic case [38].

######  Definition 5.5.

Given modal bDRL spaces $\mathcal{X}$, $\mathcal{Y}$, a contnuous bounded
morphism is a map $f:\mathcal{X}\to\mathcal{Y}$ such that $f$ is a Priestley
map that preserves ternary and binary relations as a bounded morphism.

As usual, the previous lemma allows one to claim that $\operatorname{PF}$ and
$\operatorname{ClUp}$ are contravariant functors. The following theorem
establish a desired topological duality itself.

######  Theorem 5.6.

  1. (1)

Let $\mathcal{M}$ be a residuated distributive modal algebra, then
$\operatorname{ClUp}(\operatorname{PF}(\mathcal{M}))\cong\mathcal{M}$

  2. (2)

Let $\mathcal{X}$ be a modal dBRL-space, then
$\operatorname{PF}(\operatorname{ClUp}(\mathcal{X}))\cong\mathcal{X}$

  3. (3)

Contravariant functors
$\operatorname{PF}:\operatorname{RDMA}\rightleftarrows\operatorname{TKF}:\operatorname{ClUp}$
constitute a dual equivalence between the category of all substructural
distributive modal algebras and the category of all modal dBRL-spaces.

######  Proof 5.7.

(i) The isomorphism is map $a\mapsto\phi(a)$ that commutes with products,
residuals and modal operators as discussed above.

(ii) A homeomorphism is a map $g:x\mapsto\\{A\in\operatorname{ClUp}\>|\>x\in
A\\}$. As it is shown by Galatos, $R_{\mathcal{X}}(x,y,z)\Leftrightarrow
R_{\operatorname{PF}(\operatorname{ClUp}(\mathcal{X}))}(g(x),g(y),g(x))$. One
may immediately extend this homeomorphism and show that this map commutes with
binary modal relations.

(iii) Follows from the previous two items and the previous theorem. Let us
ensure briefly that these functors behave as expected with morphisms. Let
$h:\mathcal{M}_{1}\to\mathcal{M}_{2}$ be an RDMA homomorphism, then a map
$\operatorname{PF}(h):\operatorname{PF}(\mathcal{M}_{2})\to\operatorname{PF}(\mathcal{M}_{1})$
such that $\operatorname{PF}(h):F\mapsto h^{-1}[F]$ is a Priestley map, where
$F$ is a prime filter. This map also satisfies the monotonicity and lifting
properties for a ternary relation, see [15]. One may show that
$\operatorname{PF}(h)$ has the monotonicity and lifting properties for
$[R_{\Box}]$ and $\langle R_{\Diamond}\rangle$ similarly to the intutionistic
modal logic case. On the other hand,
$\operatorname{ClUp}(f):\operatorname{ClUp}(Y)\to\operatorname{ClUp}(X)$ such
that $\operatorname{ClUp}(f):A\mapsto f^{-1}[A],A\in\operatorname{ClUp}(Y)$ is
a lattice homomorphism. $\operatorname{ClUp}(f)$ also preserves product and
residuals. $\operatorname{ClUp}(f)$ preserves $[R_{\Box}]$ and $\langle
R_{\Diamond}\rangle$ similarly to the intuitionistic modal logic case.

Hence, we obtained the Priestley-style duality for the category of residuated
distributive modal algebras and the category of all topological Kripke frames
introduced by us.

##  6 Further work

In this paper, we examined canonicity for the distributive full Lambek
calculus and its modal extensions within a “usual” Kripkean semantics. The
further questions that should be solved are Sahlqvist and Goldblatt-Thomason
theorems for such semantics and its non-distributive generalisation to study
canonicity and modal definability for noncommutative modal logic with
residuals in depth. One may consider for these purposes the frameworks
described in [9] and [8].

One may also consider a Kleene star as a modal operator [34], but such a
modality is neither $\Box$ nor $\Diamond$. The (non)canonicity of the variety
of residuated Kleene lattices also should be studied and explored considering
a Kleene residuated lattice as a sort of bounded lattice with operators.

We took the Lambek calculus with additive connections as the underlying logic
requiring the lacking distributivity principle which is unprovable in the full
Lambek calculus. A Priestley-style topological duality provided in this paper
might be extended considering dual spaces for non-distributive residuated
modal algebras using the canonical extensions technique studied by Gehrke and
van Gool, e.g., here [23].

The distributive Lambek calculus also has a sort of Gentzen cut-free calculus
and FMP [33], but the same issues for the modal extensions are not
investigated yet.

## Appendix

In this section, we recall the required background related to bounded
distributive lattice canonical extensions and topological duality. Such
notions as lattice, distributive lattice, filter, and prime filters are
supposed to be known. We refer the reader to these textbooks [10] [45].

Let us recall Priestley duality, the dual equivalence between the caterory of
bounded distributive lattices and the category of Priestley spaces [41]. First
of all, we define a Priestley space.

######  Definition .1.

  1. (1)

A Priestley space is a triple $\mathcal{X}=\langle X,\tau,\leq\rangle$, where
$\langle X,\tau\rangle$ is a compact topological space, $\langle
X,\leq\rangle$ is a bounded partial order with the additional Priestley
separation axiom:

$x\not\leq y\Rightarrow$ there exists a clopen $U\subseteq X$ such that $x\in
U$ and $y\not\in U$

  2. (2)

Let $\mathcal{X}_{1},\mathcal{X}_{2}$ be Priestley spaces and
$f:\mathcal{X}_{1}\to\mathcal{X}_{2}$, then $f$ is a Priestley map, if $f$ is
continuous, order-preserving and preserves bounds.

Let $\mathcal{L}$ be a bounded distributive lattice and $\operatorname{PF}$
the set of prime filters in $\mathcal{L}$. Let us define a map
$\phi:\mathcal{L}\to\mathcal{P}(\operatorname{PF}(\mathcal{L}))$ such that
$\phi:a\mapsto\\{F\in\operatorname{PF}(\mathcal{L})\>|\>a\in F\\}$. The sets
$\phi(a)$ and $-\phi(a)$ form a subbasis of topology on
$\operatorname{PF}(\mathcal{L})$, where $a\in\mathcal{L}$. The structure
$\langle\operatorname{PF}(\mathcal{L}),\tau,\subseteq\rangle$ is a Priestley
space, where $\tau$ is generated by the subbasis above.

Let $\mathcal{X}=\langle X,\tau,\leq\rangle$ be a Priestley space and
$\operatorname{ClUp}(\mathcal{X})$ the set of all clopen upwardly closed
subsets of $\mathcal{X}$. The dual algebra of a Priestley space is an algebra
$\langle\operatorname{ClUp}(\mathcal{X}),\cap,\cup,\emptyset,X\rangle$, which
is a bounded distribute lattice.

Let $\mathcal{L}$ be a bounded distributive lattice, then
$\eta_{\mathcal{L}}:\mathcal{L}\to\operatorname{ClUp}(\operatorname{PF}(\mathcal{L}))$
is a lattice isomorphism. Given a Priestley space $\mathcal{X}$, then
$\varepsilon_{\mathcal{X}}:\mathcal{X}\to\operatorname{PF}(\operatorname{ClUp}(\mathcal{X}))$
is a Priestley homeomorphism. Moreover, if
$h:\mathcal{L}_{1}\to\mathcal{L}_{2}$ is a bounded lattice homomorphism, then
$\operatorname{PF}(h):\operatorname{PF}(\mathcal{L}_{2})\to\operatorname{PF}(\mathcal{L}_{1})$
is a Priestley map, where $\operatorname{PF}(h):A\mapsto h^{-1}(A)$. If
$f:\mathcal{X}_{1}\to\mathcal{X}_{2}$ is a Priestley map, then
$\operatorname{ClUp}(f):\operatorname{ClUp}(\mathcal{X}_{2})\to\operatorname{CU}(\mathcal{X}_{1})$
is a bounded lattice homomorphism, where $\operatorname{ClUp}(f):A\mapsto
f^{-1}(A)$. The facts mentioned above establish Priestley duality:

######  Theorem .2.

The functors $\operatorname{PF}:{\bf BDistr}\rightleftarrows{\bf
Priest}:\operatorname{ClUp}$ constitute a dual equivalence between the
category of all bounded distributive lattices and the category of all
Priestley spaces.

Canonical extensions were introduced by Jonsson and Tarski to extend a Stone
representation to Boolean algebras with operators [31]. Let us overview
canonical extensions of distributive lattice expansions. We refer the reader
to these paper [20] [21] to have a more detailed picture of bounded
distributive lattice expansions and canonical extensions for them.

Given a complete lattice $\mathcal{L}$, $a\in\mathcal{L}$ is called
_completely join irreducible_ , if $a=\bigvee\limits_{i\in I}a_{i}$ implies
that $a=a_{i}$ for some $i\in I$. Completely meet irreducible elements are
defined dually. By $J^{\infty}(\mathcal{L})$ ($M^{\infty}(\mathcal{L})$ we
denote the set of all completely join (meet) irreducible elements. There is an
order isomorphism $\kappa:J^{\infty}(\mathcal{L})\to M^{\infty}(\mathcal{L})$
such that $\kappa:u\mapsto\bigvee(-\uparrow u)$ [20].

A complete lattice $\mathcal{L}$ is _completely distributive_ [10], if for
each doubly indexed subset $\\{x_{ij}\\}_{i\in I,j\in J}$ of $\mathcal{L}$ one
has

$\bigwedge_{i\in I}(\bigvee_{j\in J}x_{ij})=\bigvee_{\alpha:I\to
J}(\bigwedge_{i\in I}x_{i\alpha(i)})$

A perfect distributive lattice is a doubly algebraic completely distributive
lattice, that is:

######  Definition .3.

Let $\mathcal{L}$ be a bounded distributive lattice, then $\mathcal{L}$ is
called perfect distributive lattice, if it is completely distributive and
every $x\in\mathcal{L}$ has the form $x=\bigvee\\{j\in
J^{\infty}(\mathcal{L})\>|\>j\leq x\\}$ and $x=\bigwedge\\{m\in
M^{\infty}(\mathcal{L})\>|\>x\leq m\\}$. That is, $J^{\infty}(\mathcal{L})$
and $M^{\infty}(\mathcal{L})$ are join-dense and meet-dense in $\mathcal{L}$
correspondingly.

Given a lattice $\mathcal{L}$, by the completion of $\mathcal{L}$ we mean an
embedding $\mathcal{L}\hookrightarrow\mathcal{L}^{\prime}$, where
$\mathcal{L}^{\prime}$ is a complete lattice. For simplicity, we assume that
$\mathcal{L}^{\prime}$ contains $\mathcal{L}$ as a sublattice. The definition
of a canonical extension is the standard one:

######  Definition .4.

Let $\mathcal{L}$ be a bounded distributive lattice, a canonical extension of
$\mathcal{L}$ is a completion
$\mathcal{L}\hookrightarrow\mathcal{L}^{\sigma}$, where $\mathcal{L}^{\sigma}$
is a complete lattice and the following conditions hold:

  1. (1)

(Density) Every element of $\mathcal{L}^{\sigma}$ is both a join of meets and
meets of joins of elements from $\mathcal{L}$

  2. (2)

(Compactness) Let $S,T\subseteq\mathcal{L}$ such that $\bigwedge S\leq\bigvee
T$ in $\mathcal{L}^{\sigma}$, then there exist finite subsets
$S^{\prime}\subseteq S$ and $T^{\prime}\subseteq T$ such that $\bigwedge
S^{\prime}\leq\bigvee T^{\prime}$.

Now we define filter and ideal elements, or, closed and open elements,
according to the alternative terminology.

######  Definition .5.

Let $\mathcal{L}$ be a bounded distributive lattice and $\mathcal{L}^{\sigma}$
a canonical extension of $\mathcal{L}$. Let us define the following sets:

  1. (1)

$\mathcal{F}(\mathcal{L}^{\sigma})=\\{x\in\mathcal{L}^{\sigma}\>|\>\text{$x$
is a meet of elements from $\mathcal{L}$}\\}$, the set of filter elements

  2. (2)

$\mathcal{I}(\mathcal{L}^{\sigma})=\\{x\in\mathcal{L}^{\sigma}\>|\>\text{$x$
is a join of elements from $\mathcal{L}$}\\}$, the set of ideal elements

It is known that the poset $F(\mathcal{L}^{\delta})$ is isomorphic to the
poset $\operatorname{Filt}(\mathcal{L})$, the set of all filters of
$\mathcal{L}$ and the similar statement holds for
$\mathcal{I}(\mathcal{L}^{\sigma})$ and the of all ideals of $\mathcal{L}$. We
recall that a canonical extension of a bounded lattice $\mathcal{L}$ is unique
up to isomoprphism that fixes $\mathcal{L}$, see, e. g., [19]. For each
canonical extension $\mathcal{L}\hookrightarrow\mathcal{L}^{\sigma}$, the
poset $\mathcal{F}(\mathcal{L}^{\sigma})\cup\mathcal{I}(\mathcal{L}^{\sigma})$
is uniquely defined by $\mathcal{L}$. The uniqueness of a canonical extension
of $\mathcal{L}$ up to an isomorphism fixing $\mathcal{L}$ follows from this
observation.

In the case of bounded distributive lattices, one has the following fact [20]:

######  Proposition 1.

Let $\mathcal{L}$ be a bounded distributive lattice, then
$\mathcal{L}^{\sigma}$ is a perfect distributive lattice.

We also note that canonical extensions commute with dual order and Cartesian
product. That is,
$(\mathcal{L}^{op})^{\sigma}\cong(\mathcal{L}^{\sigma})^{op}$ and
$(\mathcal{L}^{n})^{\sigma}\cong(\mathcal{L}^{\sigma})^{n}$. Now we overview
bounded distributive lattices expansions, that is, bounded distributive
lattices enriched with the additional family of operators, and their canonical
extensions [19].

Let $\mathcal{K}$, $\mathcal{L}$ be bounded distributive lattices and
$f:\mathcal{K}\to\mathcal{L}$. Let us define maps $f^{\sigma}$,
$f^{\pi}:\mathcal{K}^{\sigma}\to\mathcal{L}^{\sigma}$ as follows:

  1. (1)

$f^{\pi}(u)=\bigwedge\\{\bigvee\\{f(a)\>|\>a\in\mathcal{K},x\leq a\leq
y\\}\>|\>\mathcal{F}(\mathcal{K}^{\sigma})\ni x\leq u\leq
y\in\mathcal{I}(\mathcal{K}^{\sigma})\\}$

  2. (2)

$f^{\sigma}(u)=\bigvee\\{\bigwedge\\{f(a)\>|\>a\in\mathcal{K},x\leq a\leq
y\\}\>|\>\mathcal{F}(\mathcal{K}^{\sigma})\ni x\leq u\leq
y\in\mathcal{I}(\mathcal{K}^{\sigma})\\}$

Every element of $\mathcal{K}$ is a filter element and an ideal element of
$\mathcal{L}^{\sigma}$, then $f^{\sigma}$ and $f^{\pi}$ both extend $f$. It is
clear that $f^{\sigma}\leq f^{\pi}$ in a pointwise order. We formulate the
following fact about extensions of maps on bounded distributive lattices that
we are going to use further. If the original map $f$ is order preserving, then
one may simplify the definitions of $f^{\sigma}$ and $f^{\pi}$ as follows,
e.g. [22] [19]:

######  Proposition 2.

Let $\mathcal{K}$, $\mathcal{L}$ be bounded distributive lattices and
$f:\mathcal{K}\to\mathcal{L}$. Then:

  1. (1)

$f^{\pi}(u)=\bigwedge\\{\bigvee\\{f(a)\>|\>a\in\mathcal{K},a\leq
y\\}\>|\>u\leq y\in\mathcal{I}(\mathcal{K}^{\sigma})\\}$, where
$u\in\mathcal{K}^{\sigma}$

  2. (2)

$f^{\sigma}(u)=\bigvee\\{\bigwedge\\{f(a)\>|\>a\in\mathcal{K},x\leq
a\\}\>|\>u\geq x\in\mathcal{F}(\mathcal{K}^{\sigma})\\}$, where
$u\in\mathcal{K}^{\sigma}$

  3. (3)

$f^{\sigma}(x)=f^{\pi}(x)=\bigwedge\\{f(a)\>|\>x\leq a\in\mathcal{K}\\}$,
where $x\in\mathcal{F}(\mathcal{K}^{\sigma})$

  4. (4)

$f^{\sigma}(y)=f^{\pi}(y)=\bigvee\\{f(a)\>|\>a\in\mathcal{K},a\leq y\\}$,
where $y\in\mathcal{I}(\mathcal{K}^{\sigma})$

As a consequence, for each $u\in\mathcal{K}^{\sigma}$ one has
$f^{\sigma}(u)=\bigvee\\{f^{\sigma}(x)\>|\>u\geq
x\in\mathcal{F}(\mathcal{K}^{\sigma})\\}$. The third and fourth items denote
that $f^{\sigma}$ and $f^{\pi}$ send filter (ideal) elements to filter (ideal)
ones. A map $f:\mathcal{K}\to\mathcal{L}$ is called _smooth_ , if
$f^{\pi}(u)=f^{\sigma}(u)$ for each $u\in\mathcal{K}^{\sigma}$. In particular,
a map is smooth if it preserves or reverses finite joins or meets. For
instance, modal operators $\Box$ and $\Diamond$ are smooth and their
smoothness since $\Box$ and $\Diamond$ are meet and join hemimorphisms
correspondingly. Thus, $\Box^{\sigma}=\Box^{\pi}$ and
$\Diamond^{\sigma}=\Diamond^{\pi}$.

## References

  * [1] Abramsky, S., _Computational interpretations of linear logic_ , Theoretical computer science 111 (1993), pp. 3–57.
  * [2] Andréka, H. and S. Mikulás, _Lambek calculus and its relational semantics: Completeness and incompleteness_ , Journal of Logic, Language and Information 3 (1994), pp. 1–37.
URL https://doi.org/10.1007/BF01066355

  * [3] Birkhoff, G. et al., _Rings of sets_ , Duke Mathematical Journal 3 (1937), pp. 443–454.
  * [4] Blackburn, P., M. d. Rijke and Y. Venema, “Modal Logic,” Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001.
  * [5] Celani, S. and R. Jansana, _Priestley duality, a sahlqvist theorem and a goldblatt-thomason theorem for positive modal logic_ , Logic Journal of IGPL 7 (1999), pp. 683–715.
  * [6] Chagrov, Z., A. Chagrov and M. Zakharyaschev, “Modal Logic,” Oxford logic guides, Clarendon Press, 1997.
URL https://books.google.ru/books?id=dhgi5NF4RtcC

  * [7] Chernilovskaya, A., M. Gehrke and L. Van Rooijen, _Generalized kripke semantics for the lambek–grishin calculus_ , Logic Journal of the IGPL 20 (2012), pp. 1110–1132.
  * [8] Conradie, W. and A. Palmigiano, _Algorithmic correspondence and canonicity for non-distributive logics_ , Ann. Pure Appl. Log. 170 (2019), pp. 923–974.
URL https://doi.org/10.1016/j.apal.2019.04.003

  * [9] Conradie, W., A. Palmigiano and A. Tzimoulis, _Goldblatt-thomason for le-logics_ , arXiv preprint arXiv:1809.08225 (2018).
  * [10] Davey, B. A. and H. A. Priestley, “Introduction to lattices and order,” Cambridge university press, 2002.
  * [11] Došen, K., _A brief survey of frames for the lambek calculus_ , Mathematical Logic Quarterly 38 (1992), pp. 179–187.
URL https://onlinelibrary.wiley.com/doi/abs/10.1002/malq.19920380113

  * [12] Dunn, J. M., M. Gehrke and A. Palmigiano, _Canonical extensions and relational completeness of some substructural logics_ , J. Symbolic Logic 70 (2005), pp. 713–740.
URL https://doi.org/10.2178/jsl/1122038911

  * [13] Esakia, L., _Topological kripke models_ , , 214, Russian Academy of Sciences, 1974, pp. 298–301.
  * [14] Esakia, L., “Duality Theory: Hybrids,” Springer International Publishing, Cham, 2019 pp. 41–75.
URL https://doi.org/10.1007/978-3-030-12096-2_3

  * [15] Galatos, N., “Varieties of residuated lattices,” Ph.D. thesis (2003).
  * [16] Galatos, N., P. Jipsen, T. Kowalski and H. Ono, 151, Elsevier, 2007.
  * [17] Gehrke, M., _Topological duality and algebraic completions_ .
  * [18] Gehrke, M., “Canonical Extensions, Esakia Spaces, and Universal Models,” Springer Netherlands, Dordrecht, 2014 pp. 9–41.
URL https://doi.org/10.1007/978-94-017-8860-1_2

  * [19] Gehrke, M. and J. Harding, _Bounded lattice expansions_ , Journal of Algebra 238 (2001), pp. 345 – 371.
URL http://www.sciencedirect.com/science/article/pii/S0021869300986228

  * [20] Gehrke, M. and B. Jónsson, _Bounded distributive lattices with operators_ , Math. Japonica 40 (1994), pp. 207–215.
  * [21] Gehrke, M. and B. Jónsson, _Bounded distributive lattice expansions_ , Mathematica Scandinavica 94 (2004), pp. 13–45.
URL https://www.mscand.dk/article/view/14428

  * [22] Gehrke, M., H. Nagahashi and Y. Venema, _A sahlqvist theorem for distributive modal logic_ , Annals of Pure and Applied Logic 131 (2005), pp. 65 – 102.
URL http://www.sciencedirect.com/science/article/pii/S0168007204000880

  * [23] Gehrke, M. and S. J. Van Gool, _Distributive envelopes and topological duality for lattices via canonical extensions_ , Order 31 (2014), pp. 435–461.
  * [24] Girard, J.-Y., _Linear logic: its syntax and semantics_ , London Mathematical Society Lecture Note Series (1995), pp. 1–42.
  * [25] Girard, J.-Y. and Y. Lafont, _Linear logic and lazy computation_ , in: _International Joint Conference on Theory and Practice of Software Development_ , Springer, 1987, pp. 52–66.
  * [26] Goldblatt, R., _Varieties of complex algebras_ , Annals of Pure and Applied Logic 44 (1989), pp. 173 – 242.
URL http://www.sciencedirect.com/science/article/pii/0168007289900328

  * [27] Goldblatt, R., “Mathematics of modality,” 43, Center for the Study of Language (CSLI), 1993.
  * [28] Goldblatt, R., _Grishin algebras and cover systems for classical bilinear logic_ , Studia Logica 99 (2011), p. 203.
  * [29] Goldblatt, R., _Cover systems for the modalities of linear logic_ , arXiv preprint arXiv:1610.09117 (2016).
  * [30] Jipsen, P. and C. Tsinakis, _A survey of residuated lattices_ , in: _Ordered algebraic structures_ , Springer, 2002 pp. 19–56.
  * [31] Jonsson, B. and A. Tarski, _Boolean algebras with operators. part i_ , American Journal of Mathematics 73 (1951), pp. 891–939.
URL http://www.jstor.org/stable/2372123

  * [32] Kanovich, M., S. Kuznetsov, V. Nigam and A. Scedrov, _Subexponentials in non-commutative linear logic_ , Mathematical Structures in Computer Science 29 (2019), pp. 1217–1249.
  * [33] Kozak, M., _Distributive full lambek calculus has the finite model property_ , Studia Logica 91 (2009), pp. 201–216.
  * [34] Kuznetsov, S., _*-continuity vs. induction: Divide and conquer._ , in: _Advances in Modal Logic_ , 2018, pp. 493–510.
  * [35] Lambek, J., _The mathematics of sentence structure_ , The American Mathematical Monthly 65 (1958), pp. 154–170.
  * [36] Ono, H., _Semantics for substructural logics_ , Substructural logics (1993).
  * [37] Ono, H., “Modal and Substructural Logics,” Springer Singapore, Singapore, 2019 pp. 47–60.
URL https://doi.org/10.1007/978-981-13-7997-0_4

  * [38] Palmigiano, A., _Dualities for some intuitionistic modal logics_ (2004).
  * [39] Pentus, M., _Lambek grammars are context free_ , in: _[1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science_ , IEEE, 1993, pp. 429–433.
  * [40] Pentus, M., _Models for the lambek calculus_ , Annals of Pure and Applied Logic 75 (1995), pp. 179 – 213, invited papers presented at the Conference on Proof Theory, Provability Logic, and Computation.
URL http://www.sciencedirect.com/science/article/pii/0168007294000639

  * [41] Priestley, H. A., _Ordered topological spaces and the representation of distributive lattices_ , Proceedings of the London Mathematical Society 3 (1972), pp. 507–530.
  * [42] Raney, G. N., _Completely distributive complete lattices_ , Proceedings of the American Mathematical Society 3 (1952), pp. 677–680.
  * [43] Routley, R. and R. Meyer, _The semantics of entailment_ , , 68, Elsevier, 1973 pp. 199–243.
  * [44] Sambin, G. and V. Vaccaro, _Topology and duality in modal logic_ , Annals of Pure and Applied Logic 37 (1988), pp. 249–296.
  * [45] Sankappanavar, H. P. and S. Burris, _A course in universal algebra_ , Graduate Texts Math 78 (1981).
  * [46] Seki, T., _A sahlqvist theorem for relevant modal logics_ , Studia Logica 73 (2003), pp. 383–411.
URL https://doi.org/10.1023/A:1023335229747

  * [47] Suzuki, T., _Bi-approximation semantics for substructural logic at work_ , in: M. Kracht, M. de Rijke, H. Wansing and M. Zakharyaschev, editors, _Advances in Modal Logic_ , CSLI Publications, 2010 pp. 411–433.
  * [48] Thomason, S. K., _Categories of frames for modal logic 1_ , The journal of symbolic logic 40 (1975), pp. 439–442.
  * [49] Urquhart, A., _Duality for algebras of relevant logics_ , Studia Logica: An International Journal for Symbolic Logic 56 (1996), pp. 263–276.
URL http://www.jstor.org/stable/20015846

  * [50] van Benthem, J., _Categorial grammar at a cross-roads_ , in: _Resource-Sensitivity, Binding and Anaphora_ , Springer, 2003 pp. 3–21.