# Modal Translation
of Substructural Logics

Chrysafis Hartonas
Department of Computer Science and Engineering,
University of Applied Sciences of Thessaly (TEI of Thessaly), Greece
${\tt<EMAIL_ADDRESS>
###### Abstract

In an article dating back in 1992, Kosta Došen initiated a project of modal
translations in substructural logics, aiming at generalizing the well-known
Gödel-McKinsey-Tarski translation of intuitionistic logic into S4. Došen’s
translation worked well for (variants of) BCI and stronger systems (BCW, BCK),
but not for systems below BCI. Dropping structural rules results in logic
systems without distribution. In this article, we show, via translation, that
every substructural (indeed, every non-distributive) logic is a fragment of a
corresponding sorted, residuated (multi) modal logic. At the conceptual and
philosophical level, the translation provides a classical interpretation of
the meaning of the logical operators of various non-distributive propositional
calculi. Technically, it allows for an effortless transfer of results, such as
compactness, Löwenheim-Skolem property and decidability.
Keywords: Gödel translation, Substructural Logics, Resource Conscious Logics,
Non-Distributive Logics, Representation of Lattice Expansions, Sorted Modal
Logic

##  1 Introduction

In 1933, Kurt Gödel published a paper [28] he had presented the year before in
the Mathematics Colloqium in Vienna, chaired by his former teacher, Karl
Menger. In his presentation and paper Gödel proposed his well-known
interpretation of Intuitionistic Logic (IL) into a certain modal extension of
Classical Propositional Logic (CPL), now widely known as Lewis’s system S4.
Gödel proposed to translate every IL formula $\varphi$ to an S4-formula
$\varphi^{\Box}$ by prefixing a $\Box$ to every subformula of $\varphi$. He
proved that if IL$\;\vdash\varphi$, then S4$\;\vdash\varphi^{\Box}$ and he
advanced the conjecture, later proven by McKinsey and Tarski [51], that the
converse also holds. Grigori Mints [52] complemented the result by providing a
characterization of modal formulas equivalent in S4 to GMT-translations of
intuitionistic formulas. Grzegorczyk [32] showed that adding to S4 the axiom
(G) $\Box(\Box(p\mbox{$\rightarrow$}\Box
p)\mbox{$\rightarrow$}p)\mbox{$\rightarrow$}p$, the (now known as) Grzegorczyk
system Grz = S4+G is strictly stronger than S4, it is not contained in S5 and
the same result about the GMT-translation of IL into Grz is provable. This was
also shown to be true for McKinsey’s system S4.1 =
S4+($\Box\Diamond\varphi\rightarrow\Diamond\Box\varphi$). This quickly led to
the investigation of logics, variably called super-intuitionistic, or
intermediate logics between IL and CPL and their modal companions, i.e. modal
logics containing S4, cf. [47, 48, 12, 21, 5], in some cases logics between S4
and S5 [16], which culminated in the Blok-Esakia theorem, independently proven
by Blok [8] and Esakia [21]. The topological interpretation of S4 [49, 50,
51], interpreting the box operator as an interior operator, provided
furthermore the background for investigating dualities between modal
companions of superintuitionistic logics and topological spaces [5]. In all of
the above cases distribution is assumed and topological dualities investigated
are based on the Priestley [59] duality for distributive lattices, or on the
Esakia [21, 20, 22] duality for Heyting algebras.

For logics without distribution, Goldblatt [29] provided a translation of
Orthologic O into the B system of modal logic. This quickly led to modal
approaches to quantum logic [58, 4], as an immediate application. Goldblatt’s
result is specific to Orthologic and it was Kosta Došen [15] who embarked in a
project of extending the GMT translation to the case of substructural logics.
Došen’s main result is an embedding of BCI (to which he refers as BC), BCK,
BCW with intuitionistic negation into S4-type modal extensions of versions of
BCI, BCK, BCW, respectively, all equipped with a classical-type negation
(satisfying double negation and De Morgan laws). The result is established by
proof-theoretic means, but the approach does not apply uniformly to
substructural logics at large. Indeed, Došen points out that difficulties
arise when dealing with weak systems such as the non-commutative and/or non-
associative full Lambek Calculus (N)FL (see [15], Introduction, as well as end
of Section 4).

A parallel investigation into subintuitionistic logics has also developed,
initiated by Corsi [14] in 1987 and then by Restall [60] in 1994, followed up
by Celani and Jansana [11] and others. Unlike substructural logics which are
proof-theoretically specified, subintuitionistic logics are typically
specified in a model-theoretic way, as the logics of Kripke frames for
intuitionistic logic with some frame conditions weakened, or dropped. Proof-
theoretically, this is reflected as a weakening of the axiomatization of
intuitionistic logic. In all cases, however, and as it is typical in
mainstream relevance logic [1, 2], distribution is explicitly forced in the
axiomatization and we therefore leave these outside the scope of our
investigation. Our focus, instead, is with modal translations of non-
distributive logics, arising as the logics of normal lattice expansions.

Normality for a lattice operator means that it is an additive operator [42,
43]
$f:\mathcal{L}^{i_{1}}\times\cdots\times\mathcal{L}^{i_{n}}\longrightarrow\mathcal{L}^{i_{n+1}}$
(distributing over binary joins in each argument place), where for each $j$,
$i_{j}\in\\{1,\partial\\}$ and $\mathcal{L}^{\partial}$ designates the
opposite lattice of $\mathcal{L}$ (usually designated by $\mathcal{L}^{op}$).
The tuple $\delta=(i_{1},\ldots,i_{n};i_{n+1})$ will be referred to as its
distribution type. For example, boxes and diamonds are normal operators
$\Diamond:\mathcal{L}\longrightarrow\mathcal{L}$,
$\Box:\mathcal{L}^{\partial}\longrightarrow\mathcal{L}^{\partial}$.
Implication is a normal operator with distribution type
$(1,\partial;\partial)$, in other words it is an additive operator
$\mbox{$\rightarrow$}:\mathcal{L}\times\mathcal{L}^{\partial}\longrightarrow\mathcal{L}^{\partial}$.

In this article, we restrict attention to the hierarchy of substructural logic
systems displayed in Figure 1

Figure 1: Hierarchy of Substructural Systems $\textstyle{\bf
BCK}$$\textstyle{{\bf
NFL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\bf
FL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\bf
BCI}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\bf
BCW}}$

and we present a uniform translation of the logics, proven here to be full and
faithful. The target system of the translation is a corresponding sorted,
residuated (multi) modal logic. Though we do not treat here Grishin’s dual
operators [31], it will be obvious that our approach is easily extendible to
the Full Lambek-Grishin (FLG) system.

The main structure of the argument is the following. We insist that a
substructural logic SUB and its modal companion logic sub.ML2 are interpreted
over the same class $\mathbb{F}$ of frames $\mathfrak{F}$. For modal
definability (of the frames for substructural logics) reasons, we remove
restrictions typically assumed to hold, such as frames being separated and
reduced (RS-frames [26]). Models $(\mathfrak{F},\Vdash)$,
$(\mathfrak{F},\models)$ are defined for SUB and sub.ML2, respectively, and a
translation $\varphi^{\bullet}$ and co-translation $\varphi^{\circ}$ of
sentences of the language of SUB into the sorted language of sub.ML2 are
defined. We then prove that $\varphi\Vdash\psi$ in SUB iff
$\varphi^{\bullet}\models\psi^{\bullet}$ iff
$\psi^{\circ}\models\varphi^{\circ}$ in sub.ML2. To transfer the result on the
provability relation, completeness theorems for each of SUB and sub.ML2 need
to be proven, hence obtaining that $\varphi\vdash\psi$ in the proof system for
SUB iff $\varphi^{\bullet}\vdash\psi^{\bullet}$ iff
$\psi^{\circ}\mbox{$\medvert\\!\\!\\!\\!\sim$}\hskip 1.5pt\varphi^{\circ}$ in
the sorted proof system for sub.ML2, thereby establishing that the translation
is full and faithful.

Lacking distribution, substructural logics are interpreted [63, 26, 13] in
sorted frames $\mathfrak{F}=(X,\upVdash,Y)$ with additional structure (to
account for the residuated operators). As we detail in Section 2.1, the dual
complex algebra of the frame can be taken to be either the formal concept
lattice of the frame (equivalently, its complete lattice $\mathcal{G}(X)$ of
Galois-stable sets), or the sorted, residuated modal algebra
$\largediamond:\powerset(X)\leftrightarrows\powerset(Y):\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt$ associated to the frame, where the residuated operators are generated
by the complement $I$ of the Galois relation $\upVdash$ of the frame.
Additional frame relations generate operators both on powerset algebras and on
sets of Galois stable sets where, roughly, the latter are the Galois closures
of the former (see [39, 36, 37]) and exploiting this connection leads to the
possibility for a modal translation of substructural (non-distributive, more
generally) logics.

Logically, the sorted, residuated modal logics we consider in this article
arise as a synthesis in the sense of [10] of classical propositional logic and
the logic of residuated Boolean algebras, combined together by means of a
logical adjunction (a pair of sorted, residuated operators).

From an algebraic point of view, we consider the logics of sorted, residuated
modal algebras $\Diamond:\mathcal{A}\leftrightarrows\mathcal{B}:\blacksquare$,
$a\leq\blacksquare b$ iff $\Diamond a\leq b$, where both $\mathcal{A,B}$ are
Boolean algebras and where $\mathcal{A}$ is moreover a residuated Boolean
algebra [44] with operators $\leftfilledspoon,\odot,\rightfilledspoon$, i.e.
$a_{1}\leq c\leftfilledspoon a_{2}$ iff $a_{1}\odot a_{2}\leq c$ iff
$a_{2}\leq a_{1}\rightfilledspoon c$. If the full Lambek-Grishin calculus is
to be considered, then both $\mathcal{A,B}$ are residuated Boolean algebras.
These structures serve as algebraic models to the sorted, residuated modal
logics we consider in this article. Note that the set
$\mathcal{A}_{\bullet}=\\{\blacksquare b\;|\;b\in\mathcal{B}\\}$ is a meet
sub-semilattice of $\mathcal{A}$ which has a full lattice structure (non-
distributive, in general) when defining joins in $\mathcal{A}_{\bullet}$ by
setting $a\veebar a^{\prime}=\blacksquare(\Diamond a\vee\Diamond a^{\prime})$.
Similarly for the set $\mathcal{B}_{\circ}=\\{\Box a\;|\;a\in\mathcal{A}\\}$
and they are dually isomorphic
$\mathcal{A}_{\bullet}\backsimeq\mathcal{B}^{\partial}_{\circ}$. In the case
of interest in this article, the closure operator $\blacksquare\Diamond$
carries over the residuation structure of $\mathcal{A}$ to
$\mathcal{A}_{\bullet}$. More precisely, our representation results [39, 37]
have established the following:

######  Theorem 1.1 ([39, 37]).

Every residuated lattice
$\mathcal{L}=(L,\wedge,\vee,0,1,\mbox{$\leftarrow$},\circ,\mbox{$\rightarrow$})$
is a sublattice of the lattice $\mathcal{A}_{\bullet}$ of a sorted, residuated
modal algebra $\Diamond:\mathcal{A}\leftrightarrows\mathcal{B}:\blacksquare$
where, moreover, $(\mathcal{A},\leftfilledspoon,\odot,\rightfilledspoon)$ is a
residuated Boolean algebra and where the lattice operator $\circ$ is the
closure of the restriction of $\odot$ on $\mathcal{A}_{\bullet}$, while its
residuals $\mbox{$\leftarrow$},\mbox{$\rightarrow$}$ are simply the
restrictions of the residuals $\leftfilledspoon,\rightfilledspoon$ of $\odot$
on $\mathcal{A}_{\bullet}$. $\leftVdash$

The target system of the translation can be therefore taken to be a
corresponding sorted, residuated (multi) modal logic. Options exist as to the
specification of the signature of the target companion modal logic and, in
accordance with the previous discussion, we opt for the following sorted modal
language

$\displaystyle\alpha$ $\displaystyle:=$ $\displaystyle
P_{i}\;(i\in\mathbb{N})\;|\;\neg\alpha\;|\;\alpha\wedge\alpha\;|\;\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta\;|\;\alpha\odot\alpha\;|\;\alpha\leftfilledspoon\alpha\;|\;\alpha\rightfilledspoon\alpha$
$\displaystyle\beta$ $\displaystyle:=$ $\displaystyle
Q_{i}\;(i\in\mathbb{N})\;|\;\neg\beta\;|\;\beta\wedge\beta\;|\;\largesquare\alpha\;|\;\beta\ostar\beta\;|\;\beta\leftspoon\beta\;|\;\beta\rightspoon\beta$

for the full Lambek-Grishin (FLG) calculus, where $\odot,\ostar$ are
residuated binary diamonds, with residuals
$\leftfilledspoon,\rightfilledspoon$ and $\leftspoon,\rightspoon$,
respectively. However, for the purposes of this article, focusing on the
systems of Figure 1, we restrict to the sublanguage without the
$\leftspoon,\ostar,\rightspoon$ logical operators.

As an application for the usefulness of the result, we extend the standard
translation of modal logic into first-order logic to the two-sorted case.
Using established results [19, 53, 30, 9] for sorted first-order logic and for
its two-variable fragment we obtain compactness, finite model property and
decidability, as well as the Löwenheim-Skolem property for just about any
substructural logic. A complexity bound for the satisfiability problem of the
two-variable fragment of first-order logic is also known [9], which can be
probably improved for the particular fragments at hand.

The structure of this article is as follows.

Section 2 briefly goes through some necessary preliminaries, presenting the
basics of sorted frames, running through a quick presentation of substructural
logics and reminding the reader of the basics on canonical extensions of
lattice expansions.

Section 3 studies sorted frames with relations and their associated complex
algebra (in fact, algebras (plural), as both a sorted algebra and an algebra
of Galois stable sets are of significance) and it draws on recent work by this
author on representation and duality for normal lattice expansions [39, 41,
36, 37].

Section 4 specifies the proposed modal translation and the argument that the
translation is full and faithful is detailed. The main structure of the
argument is that given a substructural logic SUB and its sorted modal
companion logic sub.ML2 a translation $\varphi^{\bullet},\psi^{\bullet}$ of
SUB-sentences $\varphi,\psi$ is defined and it is shown that
$\varphi^{\bullet}\models\psi^{\bullet}$ in some sub.ML2-model $\mathfrak{M}$
iff $\varphi\Vdash\psi$ in an associated SUB-model $\mathfrak{N}$ (produced by
just tampering with the interpretation function of $\mathfrak{M}$ and allowing
only Galois stable sets to be in its range). To conclude from this that the
sequent $\varphi\vdash\psi$ is provable in SUB iff its translation
$\varphi^{\bullet}\vdash\psi^{\bullet}$ is provable in the companion logic
sub.ML2, we establish soundness and completeness theorems of both SUB and
sub.ML2 over the same class of frames.

Some consequences regarding properties of the logics we consider are then
presented in Sections 5 and 6. Pointers for generalization of the results to
just about any non-distributive logic are suggested in the Conclusions section
7.

##  2 Review and Technical Preliminaries

###  2.1 Sorted Frames

Single-sorted modal systems cannot express a fact such as that the set $W$ of
worlds (states, points) is partitioned in a number of subsets, which is
typical of domains populated by distinct types of individuals. Sorted modal
logic arises precisely when taking into consideration the typing of the domain
of the frame. Many-sorted modal logic has so far received little attention.
Yde Venema’s [64], preceded by Balbiani’s modal multi-logic of geometry [3],
employs a two-sorted system whose intended application domain is the
projective plane, the two sorts being points and lines. Steven Kuhn’s PhD
dissertation [46], supervised by Kit Fine, is perhaps the only source where a
comprehensive study of many-sorted modal logics is carried out, dating back in
1976 and with a lot having changed in the meantime, as far as the theory of
modal logic is concerned. Venema and Balbiani’s work is developed in the
context of spatial logics, where individuals of distinct sorts populate the
application domain of interest. Two-sorted frames have been the focus of
attention in other contexts, as well, such as Wille’s formal concept analysis
(FCA) [65] and Hardegree’s logic of natural kinds [33], but they were not
accompanied by an interest in the two-sorted modal logic of the frames, though
the approach seems to suit the needs of FCA extensions such as temporal FCA
[66], or rough FCA [45]. Explicitly related to modal logics are also the
sorted frames of [6, 7], called step-frames, which are structures $(X,Y,f,R)$
where $f:X\longrightarrow Y$ and $R\subseteq X\times\powerset(Y)$, with a
sorted diamond operator
$\lozenge_{{}_{R}}:\powerset(Y)\longrightarrow\powerset(X)$, used in defining
approximations of free algebras of modal logics.

The class of two-sorted frames we consider consists of triples
$(X,\upVdash,Y)$, where $X,Y$ are non-empty sets and $\upVdash\;\subseteq
X\times Y$ is a binary relation (to be called the Galois relation of the
frame). Two-sorted frames may be concretely regarded as information systems,
or object-attribute systems, where $X$ is the set of formal objects, $Y$ is
the set of formal attributes of objects and $\upVdash$ is the attribute
assignment map. In general, a frame will have additional relations $R_{i},i\in
I$, of various sorting (contained in some product with factors $X$, $Y$).

Sorted frames generalize plain Kripke frames. Indeed, if $X=Y$ and $\upVdash$
is the non-identity relation $\neq$, then both maps of the Galois connection
(1) are the set-complementation operator
${}\mbox{${}^{\upVdash}$}U=-U=U\mbox{${}^{\upVdash}$}$.

The Galois relation of the frame generates a Galois connection (hence its
naming)

$\displaystyle U\mbox{${}^{\upVdash}$}$ $\displaystyle=\\{y\in Y\;|\;\forall
x\in U\;x\upVdash y\\}$ $\displaystyle{}\mbox{${}^{\upVdash}$}V\;=\\{x\in
X\;|\;\forall y\in V\;x\upVdash y\\}$ (1)

and, by composition of the Galois maps, a closure operator on each of
$\powerset(X)$ and $\powerset(Y)$. The relation $x\preceq z$ iff
$\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$ iff
$\forall y\in Y\;(x\upVdash y\longrightarrow z\upVdash y)$ is easily seen to
be a preorder on $X$. Similarly for $Y$. A frame is separated (clarified) [25]
if the preorder $\preceq$ is a partial order. Separation turns out to be
necessary in order to prove discrete, or Stone dualities for various classes
of lattices with operators [36, 37], but it will not be assumed for frames in
this article. The reason for this is that our argument is mostly semantically
based in that it requires that we interpret both the substructural and the
sorted modal logic systems over the same class of frames and we wish to ensure
modal definability of the frames (by the modal companion logics of the
substructural systems we examine).

The closure operators can be equivalently regarded as obtained by composition
of the residuated pair of maps generated by the complement $I$ of the
attribute assignment map $\upVdash$, i.e.
${}\mbox{${}^{\upVdash}$}(U\mbox{${}^{\upVdash}$})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond U$ and
$({}\mbox{${}^{\upVdash}$}V)\mbox{${}^{\upVdash}$}=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}V$,
where
${}\mbox{${}^{\upVdash}$}V=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt(-V),U\mbox{${}^{\upVdash}$}=\largesquare(-U)$ and
$\largesquare=-\largediamond-,\;\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}=-\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt-$,

$\displaystyle\largediamond U$ $\displaystyle=$ $\displaystyle\\{y\in
Y\;|\;\exists x\in X\;(xIy\wedge x\in U)\\}$
$\displaystyle\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0ptV$ $\displaystyle=$ $\displaystyle\\{x\in X\;|\;\forall y\in
Y\;(xIy\longrightarrow y\in V)\\}$ (2)

Where $I$ is the complement of $\upVdash$, the following conditions are
assumed.

$\forall x\in X\exists y\in Y\;xIy\hskip 42.67912pt\forall y\in Y\exists x\in
X\;xIy$ (3)

The frame conditions (3) correspond to the inclusions
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0ptB\subseteq\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}B$ and
$\largesquare A\subseteq\largediamond A$. This implies that
$\largesquare\emptyset=\largesquare(-X)=X\mbox{${}^{\upVdash}$}=\emptyset$
and, similarly,
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\emptyset=\emptyset$.

A subset $A$ of $X$ is Galois stable, or just stable, if
${}\mbox{${}^{\upVdash}$}(A\mbox{${}^{\upVdash}$})=A$ (equivalently, if
$A=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond A$). Dually, a subset $B$ of $Y$ is co-stable if
$({}\mbox{${}^{\upVdash}$}B)\mbox{${}^{\upVdash}$}=B$ (equivalently,
$B=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}B$). Stable
and co-stable sets are $\preceq$-increasing. Indeed, if $x\in A$ and $x\preceq
z$, i.e.
$\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$, then
from $\\{x\\}\subseteq A$ we obtain
$A\mbox{${}^{\upVdash}$}\subseteq\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$,
hence $z\in{}\mbox{${}^{\upVdash}$}(\\{z\\}\mbox{${}^{\upVdash}$})\subseteq
A$, by stability of $A$. Similarly for co-stable sets.

A formal concept [25] is a pair consisting of a stable and a co-stable set
$(A,B)$ such that $B=A\mbox{${}^{\upVdash}$}$ (and then also
$A={}\mbox{${}^{\upVdash}$}B$). The formal concept lattice of the frame is the
complete lattice of formal concepts, with operations defined by

$\bigwedge_{i\in I}(A_{i},B_{i})=(\bigwedge_{i\in I}A_{i},\bigvee_{i\in
I}B_{i})\hskip 56.9055pt\bigvee_{i\in I}(A_{i},B_{i})=(\bigvee_{i\in
I}A_{i},\bigwedge_{i\in I}B_{i})$

where meets and joins on the right hand side of the equations are taken in the
complete lattice of (co)stable sets, where meets are set intersections and
joins are closures of unions. Clearly, the formal concept lattice is
isomorphic to the lattice of concept extents (the complete lattice
${\mathcal{G}}(X)$ of Galois stable subsets of $X$) and dually isomorphic to
the lattice of concept intents (the complete lattice ${\mathcal{G}}(Y)$ of the
co-stable subsets of $Y$).

For a frame $\mathfrak{F}=(X,\upVdash,Y)$, let $\mathfrak{Con}(\mathfrak{F})$
be its formal concept lattice and $\mathfrak{Res}(\mathfrak{F})$ be its
associated sorted, residuated modal algebra. It is evidently only a matter of
focus which algebraic structure we decide to consider as the complex algebra
$\mathfrak{F}^{+}$ of the frame $\mathfrak{F}$. The two algebraic structures
are not unrelated and, in fact, $\mathfrak{Con}(\mathfrak{F})$ is isomorphic
to $\mathcal{A}_{\bullet}$ and it therefore sits inside
$\mathfrak{Res}(\mathfrak{F})$ as a meet sub-semilattice of
$\mathfrak{Res}(\mathfrak{F})$.

######  Remark 2.1 (Notational Conventions).

For a sorted frame $(X,\upVdash,Y,\ldots)$, perhaps with additional structure,
$\upVdash\;\subseteq X\times Y$ always designates the Galois relation.
$(\;)\mbox{${}^{\upVdash}$},{}\mbox{${}^{\upVdash}$}(\;)$ designate the maps
of the induced Galois connection (1). The complement of $\upVdash$ will be
consistently designated by $I$ and it generates a pair of residuated set-
operators
$\largediamond:\powerset(X)\leftrightarrows\powerset(Y):\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt$.

$\preceq$ is the preorder on each of $X,Y$ defined by
$\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$, for
$x,z\in X$ and, similarly, $v\preceq y$ iff
${}\mbox{${}^{\upVdash}$}\\{v\\}\subseteq{}\mbox{${}^{\upVdash}$}\\{y\\}$, for
$y,v\in Y$.

We typically and consistently use $x,z$ to range over $X$ and $y,v$ to range
over $Y$.

For $u$ in $X$, or in $Y$, we let $\Gamma u$ be the $\preceq$-upset, $\Gamma
u=\\{w\;|\;u\preceq w\\}$. Without separation in the frame, $\Gamma u=\Gamma
u^{\prime}$ only implies that $u\preceq u^{\prime}\preceq u$, without forcing
that $u=u^{\prime}$.

Given a (two-sorted) frame $(X,\upVdash,Y)$, a sorted frame relation $R$ is
any relation $R\subseteq\prod_{i=1}^{n+1}Z_{i}$, where for each $i$,
$Z_{i}\in\\{X,Y\\}$. To keep track of the various relations and their sorting
we make the convention to indicate the sorting by an upper index, a string of
$1$’s and $\partial$’s, with 1 pointing to $X$ and $\partial$ pointing to $Y$.
Thus, for example, $R^{11\partial}$ is a relation contained in the cartesian
product $X\times(X\times Y)$. An $(n+1)$-ary relation $R\subseteq
Z\times\prod_{i=1}^{n}Z_{i}$ will be always written in the form $zRz_{1}\cdots
z_{n}$.

The sets obtained by not filling one argument place will be written in the
form $zRz_{1}\cdots z_{i-1}(\;)z_{i+1}\cdots z_{n}=\\{z_{i}\;|\;zRz_{1}\cdots
z_{i}\cdots z_{n}\\}$. For a two place relation we write $xR$ and $Rz$, rather
than $xR(\;)$ and $(\;)Rz$, respectively. Similarly, for a 3-place relation we
write $Rzu,xRz$, rather than $(\;)Rzu$ and $xRz(\;)$, respectively, but we use
$xR(\;)u$ when the second argument place is not filled.

###  2.2 A Substructural Review

Substructural logics arise from the Gentzen system LJ for intuitionistic logic
by dropping a combination of the structural rules of exchange, contraction and
weakening and expanding the logical signature of the language to include the
operator symbols $\circ$ (fusion, cotenability), $\leftarrow$ (reverse
implication) and, often, a constant $\mathfrak{t}$.

We let NFL be the system with all structural rules dropped (including the
association rule), which is precisely the non-associative Full Lambek
calculus. We write FL for the associative Lambek calculus. For
$r\subseteq\\{c,e,w\\}$ we designate by ${\bf(N)FL}_{r}$ the system resulting
by adding to (N)FL the structural rules in $r$ (where $c$ abbreviates
‘contraction’, $e$ abbreviates ‘exchange’ and similarly for $w$ and
‘weakening’). With the exception of ${\bf FL}_{ecw}$, which is precisely LJ,
distribution of conjunctions over disjunctions and conversely does not hold,
unless explicitly added to the axiomatization (an option typically taken by
mainstream relevance logicians [1, 2]).

The algebraic semantics of these systems has been investigated by Hiroakira
Ono, Nick Galatos [23, 57, 54, 55, 56] and several others.

An FL-algebra is a structure $\langle
L,\leq,\wedge,\vee,0,1,\mbox{$\leftarrow$},\circ,\mbox{$\rightarrow$},\mathfrak{t}\rangle$
where

  1. 1.

$\langle L,\leq,\wedge,\vee,0,1\rangle$ is a bounded lattice

  2. 2.

$\langle L,\leq,\circ,\mathfrak{t}\rangle$ is a partially-ordered monoid
($\circ$ is monotone and associative and $\mathfrak{t}$ is a two-sided
identity element $a\circ\mathfrak{t}=a=\mathfrak{t}\circ a$)

  3. 3.

$\mbox{$\leftarrow$},\circ,\mbox{$\rightarrow$}$ are residuated, i.e. $a\circ
b\leq c$ iff $b\leq a\mbox{$\rightarrow$}c$ iff $a\leq c\mbox{$\leftarrow$}b$

  4. 4.

for any $a\in L$, $\;a\circ 0=0=0\circ a$

An FL-algebra is commonly referred to as a residuated lattice [24]. FL-
algebras (residuated lattices) are precisely the algebraic models of the
associative full Lambek calculus. By residuation, the distribution types of
the operators are
$\delta(\circ)=(1,1;1),\delta(\mbox{$\rightarrow$})=(1,\partial;\partial)$ and
$\delta(\mbox{$\leftarrow$})=(\partial,1;\partial)$.

An FLe-algebra adds to the axiomatization the exchange (commutativity) axiom
$a\circ b=b\circ a$ for the cotenability operator (in which case $\leftarrow$
and $\rightarrow$ coincide). It corresponds to the system BCI studied by Došen
[15].

An FLew-algebra adds the weakening axiom $b\circ a\leq a$, as well, in which
case combining with commutativity $a\circ b\leq a\wedge b$ follows. In
addition, by $1\circ\mathfrak{t}\leq\mathfrak{t}$, the identity
$\mathfrak{t}=1$ holds in FLew-algebras. FLew-algebras are also referred to in
the literature as full BCK-algebras, corresponding to full BCK-logic,
resulting from BCK whose purely implicational signature is expanded to include
conjunction and disjunction connectives, alongside the cotenability logical
operator and the constants $0,1$. Algebraically, they constitute the class of
commutative integral residuated lattices [24].

Similarly, an FLec-algebra, adds the contraction axiom $a\wedge b\leq a\circ
b$ (a distinguished case of which is square increasingness $a\leq a\circ a$).
FLec-algebras are also known as BCW-algebras.

The language of the Lambek Calculus (associative, or not) that we consider is
displayed below,

$L\ni\varphi\;:=\;p_{i}\;(i\in\mathbb{N})\;|\;\top\;|\;\bot\;|\;\varphi\wedge\varphi\;|\;\varphi\vee\varphi\;|\;\varphi\mbox{$\leftarrow$}\varphi\;|\;\varphi\circ\varphi\;|\;\varphi\mbox{$\rightarrow$}\varphi$

where we omit the constant $\mathfrak{t}$, avoiding matters of secondary
interest. The use of the names BCI, BCW and BCK is more widespread than the
use of the names FLe, FLec, FLew due to their connection with type theory and
the Curry-Howard isomorphism, where BCI, BCK, BCW designate restricted
families of $\lambda$-terms and the combinators B,C,I,K,W correspond to the
following Hilbert-style axiomatization of their pure implicational fragment.

(B) |  $(\varphi\mbox{$\rightarrow$}\psi)\mbox{$\rightarrow$}((\vartheta\mbox{$\rightarrow$}\varphi)\mbox{$\rightarrow$}(\vartheta\mbox{$\rightarrow$}\psi))$
---|---
(C) |  $(\varphi\mbox{$\rightarrow$}(\psi\mbox{$\rightarrow$}\vartheta))\mbox{$\rightarrow$}(\psi\mbox{$\rightarrow$}(\varphi\mbox{$\rightarrow$}\vartheta))$
(I) | $\varphi\mbox{$\rightarrow$}\varphi$
(K) |  $\varphi\mbox{$\rightarrow$}(\psi\mbox{$\rightarrow$}\varphi)$
(W) |  $(\varphi\mbox{$\rightarrow$}(\varphi\mbox{$\rightarrow$}\psi))\mbox{$\rightarrow$}(\varphi\mbox{$\rightarrow$}\psi)$

Proof systems for substructural logics can be found in the literature and we
do not take the space to restate them here. The reader may wish to consult
[63], for a Gentzen System, or [15] for a Hilbert-style axiomatization. In
fact, for the purposes of this article we will be content with a proof system
as a symmetric consequence system, with sequents of the form
$\varphi\vdash\psi$, directly encoding the corresponding algebraic
specification.

Fragments of these systems are also of independent interest, corresponding for
example to the logics of implicative
$(L,\leq,0,1,\wedge,\vee,\mbox{$\rightarrow$})$, or bi-implicative lattices
$(L,\leq,0,1,\wedge,\vee,\mbox{$\leftarrow$},\mbox{$\rightarrow$})$. Going in
the other direction, extensions of these systems for example by various
negation and/or modal operators are also of interest, but we shall not treat
such extensions in the present article.

Contrasting to relational semantics, algebraic semantics and soundness and
completeness for the systems are well established results in the substructural
logics community, see for example [56, 24].

Lacking distribution, substructural logics are interpreted in sorted frames
$(X,\upVdash,Y,R^{111})$, where $R^{111}$ is a ternary relation with the
indicated sorting type and $\upVdash\;\subseteq X\times Y$ is the Galois
relation of the frame. Fusion and implication have been modeled in sorted
frames by Gehrke [26] and then also by Dunn, Gehrke and Palmigiano [17], using
RS-frames (separated (clarified) and reduced frames, in Wille’s sense [25]).
For our argument of a full and faithful modal translation to go through we
need to ensure that the class of frames we use is modally definable, since
both the substructural systems and their companion modal logics are to be
interpreted in the same class of frames, with respect to which completeness
theorems should be derivable. For this reason we drop both restrictions of
being separated and being reduced for frames.

Given a frame $\mathfrak{F}=(X,\upVdash,Y,R^{111})$ a model
$\mathfrak{N}=(\mathfrak{F},V)$ for the interpretation of the language of a
substructural logic is equipped with a map
$V:\\{p_{i}\;|\;i\in\mathbb{N}\\}\longrightarrow{\mathcal{G}}(X)$, assigning a
stable set (a concept extent) to propositional variables. An interpretation
$\overline{V}$ of sentences $\varphi$ as formal concepts
$\overline{V}(\varphi)=(\mbox{$[\\![\varphi]\\!]$},\mbox{$(\\!|\varphi|\\!)$})$
with extent $[\\![\varphi]\\!]$ and intent
$\mbox{$(\\!|\varphi|\\!)$}=\mbox{$[\\![\varphi]\\!]$}\mbox{${}^{\upVdash}$}$
is then recursively defined. The satisfaction $\Vdash$ and co-satisfaction
$\Vdash^{\\!\\!\partial}$ relations are defined by setting, for $x\in X$ and
$y\in Y$, $x\Vdash\varphi$ iff $x\in\mbox{$[\\![\varphi]\\!]$}$ and
$y\Vdash^{\\!\\!\partial}\varphi$ iff $y\in\mbox{$(\\!|\varphi|\\!)$}$. The
recursive definition of the interpretation $\overline{V}$ is specified by the
appropriate clauses for $\Vdash$ and $\Vdash^{\\!\\!\partial}$, shown in Table
1. The relation $R^{\partial 11}$ involved in the semantic clauses is defined
by setting $R^{\partial
11}zz^{\prime}=(R^{111}zz^{\prime})\mbox{${}^{\upVdash}$}$.

Table 1: (Co)Satisfaction relations for Substructural Logics $x\Vdash p_{i}$ | iff | $x\in V(p_{i})$
---|---|---
$x\Vdash\top$ | iff | $x=x$
$y\Vdash^{\\!\\!\partial}\bot$ | iff | $y=y$
$x\Vdash\varphi\wedge\psi$ | iff |  $x\Vdash\varphi$ and $x\Vdash\psi$
$y\Vdash^{\\!\\!\partial}\varphi\vee\psi$ | iff |  $y\Vdash^{\\!\\!\partial}\varphi$ and $y\Vdash^{\\!\\!\partial}\psi$
$x\Vdash\varphi\mbox{$\rightarrow$}\psi$ | iff | $\forall z\in X\;\forall y\in Y\;(z\Vdash\varphi\;\wedge\;y\Vdash^{\\!\\!\partial}\psi\;\longrightarrow\;yR^{\partial 11}zx)$
$y\Vdash^{\\!\\!\partial}\varphi\circ\psi$ | iff | $\forall x,z\in X\;(z\Vdash\varphi\;\wedge\;x\Vdash\psi\;\longrightarrow\;yR^{\partial 11}zx)$
$x\Vdash\psi\mbox{$\leftarrow$}\varphi$ | iff |  $\forall y\in Y\;\forall z\in X\;(y\Vdash^{\\!\\!\partial}\psi\;\wedge\;z\Vdash\varphi\;\longrightarrow\;yR^{\partial 11}xz)$

For a sentence $\varphi$ it suffices to specify either a satisfaction, or a
co-satisfaction clause, since in the interpretation
$\overline{V}(\varphi)=(\mbox{$[\\![\varphi]\\!]$},\mbox{$(\\!|\varphi|\\!)$})$
we have
$\mbox{$[\\![\varphi]\\!]$}={}\mbox{${}^{\upVdash}$}\mbox{$(\\!|\varphi|\\!)$}$
and
$\mbox{$(\\!|\varphi|\\!)$}=\mbox{$[\\![\varphi]\\!]$}\mbox{${}^{\upVdash}$}$.
Hence both $x\Vdash\varphi$ iff $\forall y\in
Y\;(y\Vdash^{\\!\\!\partial}\varphi\;\longrightarrow\;x\upVdash y)$, as well
as $y\Vdash^{\\!\\!\partial}\varphi$ iff $\forall x\in
X\;(x\Vdash\varphi\;\longrightarrow\;x\upVdash y)$ always obtain.

Table 2 displays relational constraints on frames, to be considered in the
sequel.

Table 2: Relational Constraints on Frames

  1. (C1)

For all points $w,z,u,v\in X$, statements (1) and (2) below are equivalent

     * (1)

$\exists x\;(xR^{111}uv\;\wedge\;zR^{111}xw)$

     * (2)

$\exists x\;(xR^{111}vw\;\wedge\;zR^{111}ux)$

  2. (C2)

$\forall x,z,z^{\prime}\in
X\;(xR^{111}zz^{\prime}\;\longleftrightarrow\;xR^{111}z^{\prime}z)$

  3. (C3)

$\forall x,z,z^{\prime}\in
X\;(xR^{111}zz^{\prime}\;\longrightarrow\;z^{\prime}\preceq x)$

  4. (C4)

$\forall x\in X\;xR^{111}xx$

The reader familiar with the literature on relevance logic will recognize them
as the standard frame conditions relevance logicians consider on frames [1, 2,
18] and some of our related proof obligations come across the same type of
difficulties as encountered in proving completeness theorems for relevance
logic in relational semantics. An exception is the relational constraint (C3),
corresponding to Weakening being assumed. In a Boolean setting (for the logics
of residuated Boolean algebras) (C3) can be replaced by the condition $\forall
x,z,z^{\prime}\in X\;(xR^{111}zz^{\prime}\;\longrightarrow\;z^{\prime}=x)$,
but this is too strong a requirement for the semantics of substructural
logics.

######  Definition 2.2.

Taking the frame constraints of Table 2 in consideration, we distinguish the
frame classes $\mathbb{NFL,FL,BCI,BCW,BCK}$ by the obvious criteria, detailed
below:

  * $\mathbb{NFL}$) Unrestricted class of frames $\mathfrak{F}=(X,\upVdash,Y,R^{111})$

  * $\mathbb{FL}$) Frames where the constraint (C1) holds

  * $\mathbb{BCI}$) Frames where the constraints (C1) and (C2) hold

  * $\mathbb{BCK}$) Frames where the constraints (C1), (C2) and (C3) hold

  * $\mathbb{BCW}$) Frames where the constraints (C1), (C2) and (C4) hold

###  2.3 Canonical Extensions

Canonical extensions for bounded lattices were introduced by Gehrke and
Harding [27], extending to the non-distributive case the notion of a canonical
extension of Jónsson and Tarski [42, 43]. A canonical lattice extension is
defined as a pair $(\alpha,C)$ where $C$ is a complete lattice and $\alpha$ is
an embedding of a lattice $\mathcal{L}$ into $C$ such that the following
density and compactness requirements are satisfied

> $\bullet$ (density) $\alpha[{\mathcal{L}}]$ is dense in $C$, where the
> latter means that every element of $C$ can be expressed both as a meet of
> joins and as a join of meets of elements in $\alpha[{\mathcal{L}}]$
>  $\bullet$ (compactness) for any set $A$ of closed elements and any set $B$
> of open elements of $C$, $\bigwedge A\leq\bigvee B$ iff there exist finite
> subcollections $A^{\prime}\subseteq A,B^{\prime}\subseteq B$ such that
> $\bigwedge A^{\prime}\leq\bigvee B^{\prime}$

where the closed elements of $C$ are defined in [27] as the elements in the
meet-closure of the representation map $\alpha$ and the open elements of $C$
are defined dually as the join-closure of the image of $\alpha$. Existence of
canonical extensions for bounded lattices is proven in [27] by demonstrating
that the compactness and density requirements are satisfied in the
representation due to Hartonas and Dunn [40] (though it is to be noted that
the lattice representation argument of [40] is merely reproduced in [27],
without attributing it to [40]).

The canonical extension construction is functorial. Indeed, recall from [27]
that if $(\alpha,C)$ is a canonical extension of a bounded lattice $L$, and
${\tt K,O}$ are its sets of closed and open elements, the $\sigma$ and
$\pi$-extensions
$f_{\sigma},f_{\pi}:{\mathcal{L}}_{\sigma}\longrightarrow{\mathcal{L}}_{\sigma}$
(where, following the notation of [27], ${\mathcal{L}}_{\sigma}$ designates
the canonical extension of $\mathcal{L}$) of a unary monotone map
$f:L\longrightarrow L$ are defined in [27], taking also into consideration
Lemma 4.3 of [27], by setting, for $k\in{\tt K}$, $o\in{\tt O}$ and $u\in C$

$\displaystyle f_{\sigma}(k)=\bigwedge\\{f(a)\;|\;k\leq a\in L\\}$
$\displaystyle f_{\sigma}(u)=\bigvee\\{f_{\sigma}(k)\;|\;{\tt K}\ni k\leq
u\\}$ (4) $\displaystyle f_{\pi}(o)=\bigvee\\{f(a)\;|\;L\ni a\leq o\\}$
$\displaystyle f_{\pi}(u)=\bigwedge\\{f_{\pi}(o)\;|\;u\leq o\in{\tt O}\\}$ (5)

where in these definitions $\mathcal{L}$ is identified with its isomorphic
image in $C$ and $a\in{\mathcal{L}}$ is then identified with its
representation image. Working concretely with the canonical extension of [40],
the $\sigma$ extension
$f_{\sigma}:{\mathcal{L}}_{\sigma}\longrightarrow{\mathcal{L}}_{\sigma}$ of a
monotone map $f$ as in equation (4) and the dual $\sigma$-extension
$f_{\sigma}^{\partial}:{\mathcal{L}}^{\partial}_{\sigma}\longrightarrow{\mathcal{L}}^{\partial}_{\sigma}$
(not used in [27]) are defined by instantiating equation (4) in the concrete
canonical extension of [40] considered here by setting, for $x\in X$ and $y\in
Y$ and where $x_{e}$ is a principal filter, $y_{e}$ a principal ideal and the
closed elements are precisely the principal upper sets $\Gamma u$ (for each of
$X$, $Y$).

$f_{\sigma}(\Gamma x)$ | = |  $\bigwedge\\{\alpha_{X}(fa)\;|\;a\in{\mathcal{L}},\Gamma x\leq\alpha_{X}(a)\\}$ | = | $\bigwedge\\{\Gamma x_{fa}\;|\;\Gamma x\subseteq\Gamma x_{a}\\}$
---|---|---|---|---
| = | $\bigwedge\\{\Gamma x_{fa}\;|\;a\in x\\}$ | = | $\Gamma(\bigvee\\{x_{fa}\;|\;a\in x\\})$
$f_{\sigma}^{\partial}(\Gamma y)$ | = | $\bigwedge\\{\alpha_{Y}(fa)\;|\;a\in{\mathcal{L}},\Gamma y\leq\alpha_{Y}(a)\\}$ | = | $\bigwedge\\{\Gamma y_{fa}\;|\;\Gamma y\subseteq\Gamma y_{a}\\}$
| = | $\bigwedge\\{\Gamma y_{fa}\;|\;a\in y\\}$ | = |  $\Gamma(\bigvee\\{y_{fa}\;|\;a\in y\\})$

From [34] recall that if $f$ is an $n$-ary normal operator of distribution
type $\delta=(i_{1},\ldots,i_{n};i_{n+1})$, where $i_{j}\in\\{1,\partial\\}$
(in other words
$f:\mathcal{L}^{i_{1}}\times\cdots\times\mathcal{L}^{i_{n}}\longrightarrow\mathcal{L}^{i_{n+1}}$
is an additive operator), then we defined filter/ideal operators
$f^{\sharp},f^{\flat}$ which, in the unary case are precisely the maps
$f^{\sharp}(x)=\bigvee\\{x_{fa}\;|\;a\in x\\}$ and
$f^{\flat}(y)=\bigvee\\{y_{fa}\;|\;a\in y\\}$ (for a filter $x$ and ideal
$y$). It can be then immediately observed that $f_{\sigma}(\Gamma
x)=\Gamma(f^{\sharp}x)$, if $f$ distributes over joins, and that
$f^{\partial}_{\sigma}(\Gamma y)=\Gamma(f^{\flat}y)$ if it distributes over
meets (the cases of co-distribution being reducible to these two by
considering $f$ as a map from $\mathcal{L}$ to its opposite lattice
$\mathcal{L}^{\partial}$, or the other way around). The $\pi$-extension
$f_{\pi}$ is obtained from the dual $\sigma$ extension
$f^{\partial}_{\sigma}$, by composition with the Galois maps,
$f_{\pi}({}\mbox{${}^{\upVdash}$}\\{y\\})={}\mbox{${}^{\upVdash}$}(f^{\partial}_{\sigma}({}\mbox{${}^{\upVdash}$}\\{y\\})\mbox{${}^{\upVdash}$})={}\mbox{${}^{\upVdash}$}(f^{\partial}_{\sigma}(\Gamma
y))$, where the set $\\{{}\mbox{${}^{\upVdash}$}\\{y\\}\;|\;y\in Y\\}$ is the
set of open elements of $\mathcal{L}_{\sigma}$ and
${}\mbox{${}^{\upVdash}$}(\;),(\;)\mbox{${}^{\upVdash}$}$ designates the
Galois connection generated by $\upVdash$.

Besides serving as a means to construct the $\sigma$-extension of maps, as
shown in [39, 41], point operators are used in [34] and in each of [39, 41] to
construct relational structures dual to lattice expansions. Roughly, for each
normal lattice operator
$f:\mathcal{L}^{i_{1}}\times\cdots\times\mathcal{L}^{i_{n}}\longrightarrow\mathcal{L}^{i_{n+1}}$,
where $i_{j}\in\\{1,\partial\\}$, a canonical relation $R_{f}$ is defined by
setting $uR_{f}u_{1}\cdots u_{n}$ iff $f^{\sharp}(u_{1},\ldots,u_{n})\leq u$
and a dual relation $R^{\partial}_{f}$ is then appropriately derived. The
relations $R_{f},R^{\partial}_{f}$ are then used to define operators $F$ on
stable sets and $F^{\partial}$ on co-stable sets that are shown in [39, 41] to
be the canonical (dual) extension $f_{\sigma},f^{\partial}_{\sigma}$ of $f$.

We conclude this section with considering the case where the represented
lattice (expansion) is distributive, or a Boolean algebra. For the approach
based on and extending the Hartonas-Dunn lattice duality [40], the canonical
frames for distributive and Boolean algebras are the obvious subframes of the
canonical lattice frame. Indeed, let $\mathcal{L}$ be a lattice and assume it
is a Boolean algebra. Let ${\mathcal{G}}(\mbox{\rm Filt}(\mathcal{L}))$ be the
set of Galois-stable subsets of the Hartonas-Dunn dual canonical frame
$(\mbox{\rm Filt}(\mathcal{L}),\upVdash,\mbox{\rm Idl}(\mathcal{L}))$ (the
canonical extension of $\mathcal{L}$) and let $\mbox{\rm
Ult}(\mathcal{L})\subseteq\mbox{\rm Filt}(\mathcal{L})$ be its set of
ultrafilters. It is not hard to see that the map $\eta:{\mathcal{G}}(\mbox{\rm
Filt}(\mathcal{L}))\longrightarrow\powerset(\mbox{\rm Ult}(\mathcal{L}))$
defined by $\eta(A)=A\cap\mbox{\rm Ult}(\mathcal{L})$ is an isomorphism of
canonical extensions. Indeed, by uniqueness of canonical extensions [27],
there is an isomorphism $\eta:{\mathcal{G}}(\mbox{\rm
Filt}(\mathcal{L}))\backsimeq\powerset(\mbox{\rm Ult}(\mathcal{L}))$,
commuting with the embeddings $\alpha_{A}(a)=\\{x\in\mbox{\rm
Filt}(\mathcal{L})\;|\;a\in x\\}$, $h_{A}(a)=\\{u\in\mbox{\rm
Ult}(\mathcal{L})\;|\;a\in u\\}$, i.e. $\eta(\alpha_{A}(a))=h_{A}(a)$, for all
$a\in\mathcal{L}$. Given that by join density of principal filters any filter
$x$ is $x=\bigvee_{a\in x}x_{a}$, where we let $x_{a}=a\\!\uparrow$ designate
a principal filter and that, letting $\Gamma x=x\\!\Uparrow$, $\Gamma
x=\Gamma(\bigvee_{a\in x}x_{a})=\bigwedge_{a\in x}\Gamma x_{a}=\bigwedge_{a\in
x}\alpha_{A}(a)$ and since $\eta$ preserves both meets and joins, being an
isomorphism, we obtain

$\eta(\Gamma x)$ | = | $\eta(\bigwedge_{a\in x}\alpha_{A}(a))=\bigcap_{a\in x}\eta(\alpha_{A}(a))=\bigcap_{a\in x}h_{A}(a)$
---|---|---
| = | $\bigcap_{a\in x}\\{u\in\mbox{\rm Ult}(\mathcal{L})\;|\;a\in u\\}=\\{u\in\mbox{\rm Ult}(\mathcal{L})\;|\;x\leq u\\}$
| = |  $\\{u\in\mbox{\rm Ult}(\mathcal{L})\;|\;u\in\Gamma x\\}=\Gamma x\cap\mbox{\rm Ult}(\mathcal{L})$

where $\leq$ in ‘$x\leq u$’ designates filter inclusion. Given also join-
density of the set of closed elements of ${\mathcal{G}}(\mbox{\rm
Filt}(\mathcal{L}))$ (see Lemma 3.1, [36]) we obtain that for any stable set
$A\in{\mathcal{G}}(\mbox{\rm Filt}(\mathcal{L}))$,

$\displaystyle\eta(A)$ $\displaystyle=$ $\displaystyle\eta(\bigvee_{x\in
A}\Gamma x)=\bigcup_{x\in A}\eta(\Gamma x)=\bigcup_{x\in A}\bigcap_{a\in
x}\\{u\in\mbox{\rm Ult}(\mathcal{L})\;|\;a\in u\\}$ $\displaystyle=$
$\displaystyle\bigcup_{x\in A}\\{u\in\mbox{\rm Ult}(\mathcal{L})\;|\;x\leq
u\\}$

Stable sets are increasing, i.e. $x\in A$ implies $\Gamma x\subseteq A$ (see
Lemma 3.1, [36]), hence $\eta(A)=A\cap\mbox{\rm Ult}(\mathcal{L})$.

The following lemma will be useful in the sequel.

######  Lemma 2.3.

Let $\mathcal{A}$ be a Boolean algebra with a unary monotone operator
$f:\mathcal{A}\longrightarrow\mathcal{A}$. Let also $\mathcal{A}_{\sigma}$ be
the Hartonas-Dunn canonical extension
$\mathcal{A}_{\sigma}=\mathcal{G}(\mbox{\rm Filt}(\mathcal{A}))$ of
$\mathcal{A}$ considered merely as a lattice and let
$\mathcal{A}_{\delta}=\powerset(\mbox{\rm Ult}(\mathcal{A}))$ be the standard
construction of the canonical (ultrafilter) extension of the Boolean algebra
$\mathcal{A}$, after Stone [62]. Designate the canonical extension
($\sigma$-extension) of the map $f$ respectively by $f_{\sigma}$ and
$f_{\delta}$. Then, the isomorphism $\eta:\mathcal{G}(\mbox{\rm
Filt}(\mathcal{A}))\backsimeq\powerset(\mbox{\rm Ult}(\mathcal{A}))$ is a
homomorphism of lattice expansions, i.e. it commutes with the
$\sigma$-extensions of $f$, $\eta f_{\sigma}=f_{\delta}\eta$.

###### Proof.

For the purposes of this proof, let $X=\mbox{\rm Filt}(\mathcal{A})$,
$X^{u}=\mbox{\rm Ult}(\mathcal{A})$, $\Gamma x=\\{z\in X\;|\;x\leq z\\}$, for
a filter $x$ and where $\leq$ designates filter inclusion, and
$\Gamma^{u}x=\\{u\in X^{u}\;|\;x\leq u\\}$ and recall that it was argued above
that $\eta(\Gamma x)=\Gamma^{u}x$. Letting
$\alpha:\mathcal{A}\hookrightarrow\mathcal{A}_{\sigma}$ and
$h:\mathcal{A}\hookrightarrow\mathcal{A}_{\delta}$ be the canonical embeddings
of $\mathcal{A}$ it is not hard to see that the intersection closure of
$\alpha[\mathcal{A}]$ is the collection of $\Gamma x$, with $x\in X$ and,
similarly, the intersection closure of $h[\mathcal{A}]$ is the collection of
the sets $\Gamma^{u}x$, with $x\in X$. In other words, the sets of the form
$\Gamma x,\Gamma^{u}x$ are the closed (filter) elements of
$\mathcal{A}_{\sigma}$ and $\mathcal{A}_{\delta}$, respectively. By
$\eta(\Gamma x)=\Gamma^{u}x$, the isomorphism of canonical extensions
preserves closed elements (and similarly for open elements). Given the
definition of the $\sigma$-extension of a monotone map in
$\mathcal{A}_{\sigma}$ we obtain

$\eta f_{\sigma}(\Gamma x)=\\{u\in X^{u}\;|\;\forall a\in\mathcal{A}\;(a\in
x\;\longrightarrow\;f(a)\in u)\\}$ (6)

Similarly, considering the $\sigma$-extension of $f$ in
$\mathcal{A}_{\delta}=\powerset(X^{u})$ we obtain by definition

$f_{\delta}(\eta(\Gamma x))=f_{\delta}(\Gamma^{u}x)=\\{u\in X^{u}\;|\;\forall
a\in\mathcal{A}\;(\Gamma^{u}x\subseteq h(a)\;\longrightarrow\;f(a)\in u)\\}$
(7)

where $\Gamma^{u}x\subseteq h(a)$ iff $\eta(\Gamma x)\subseteq\eta\alpha(a)$
iff $\Gamma x\subseteq\alpha(a)$ iff $a\in x$. Hence we obtain that $\eta
f_{\sigma}(\Gamma x)=f_{\delta}(\eta(\Gamma x))$, as claimed. ∎

Using the fact pointed out in [27] that
$(\mathcal{L}\times\mathcal{M})_{\sigma}\backsimeq\mathcal{L}_{\sigma}\times\mathcal{M}_{\sigma}$
and
$(\mathcal{L}^{\partial})_{\sigma}\backsimeq(\mathcal{L}_{\sigma})^{\partial}$,
Lemma 2.3 extends readily to $n$-ary maps that are either monotone, or
antitone in their argument places.

##  3 Sorted Frames with Relations and their Logics

The extensions of ML2 that we consider arise as the logics of sorted frames
with additional relations. Cases of interest include temporal formal contexts
$((X,\prec),\upVdash,Y)$, where $\prec\;\subseteq X\times X$ is a relation of
temporal succession of (instances of) formal objects, of use in Temporal FCA
[66], or contexts with an indiscernibility relation $\approx$ on formal
objects, $((X,\approx),\upVdash,Y)$, arising in Rough FCA [45]. Frames of this
type correspond to extensions of substructural logics with unary modal
operators, which we do not discuss in this article.

We focus here on structures $(X,\upVdash,Y,R^{111})$, where $R$ has the
sorting type indicated by the superscript (with $1$ pointing to $X$ and
$\partial$ to $Y$), i.e. $R\subseteq X\times(X\times X)$. With a spatial
intuition, as in [64], $R$ can be understood, for example, as a colinearity
relation for points in $X$, $xRx^{\prime}x^{\prime\prime}$ iff $\exists y\in
Y\;\\{x,x^{\prime},x^{\prime\prime}\\}\upVdash y$, where $\upVdash$ is the
incidence relation of the frame. We make no further assumptions about the
accessibility relation $R^{111}$, such as the ‘compatibility’ assumption made
in [26, 13], because we wish to ensure modal definability of our frame
classes. It is for the same reason that we do not assume that frames are
separated and/or reduced.

###  3.1 Sorted, Residuated Modal Logics

Given a frame $(X,\upVdash,Y,R^{111})$, the relation $R^{111}$ generates a
classical binary additive operator on $\powerset(X)$, defined in the standard
way by

$\displaystyle U\mbox{$\bigodot$}U^{\prime}$ $\displaystyle=$
$\displaystyle\\{x\in X\;|\;\exists u,u^{\prime}\in
X\;(xR^{111}uu^{\prime}\;\wedge\;u\in U\;\wedge\;u^{\prime}\in U^{\prime})\\}$
$\displaystyle=$ $\displaystyle\bigcup_{u\in U,u^{\prime}\in
U^{\prime}}R^{111}uu^{\prime}$

It follows from the definition that $\bigodot$ distributes over arbitrary
unions in each argument place and we let
$\tilde{\Leftarrow},\tilde{\Rightarrow}$ be its residuals in the algebra of
subsets of $X$, i.e. $U\subseteq W\tilde{\Leftarrow}U^{\prime}$ iff $U\bigodot
U^{\prime}\subseteq W$ iff $U^{\prime}\subseteq U\tilde{\Rightarrow}W$. Hence
$(\powerset(X),\tilde{\Leftarrow},\bigodot,\tilde{\Rightarrow})$ is a
residuated Boolean algebra.

######  Lemma 3.1.

The residuals $\tilde{\Leftarrow},\tilde{\Rightarrow}$ are defined by

  * •

$U\tilde{\Rightarrow}W=\\{x\in X\;|\;\forall z,z^{\prime}\in X\;(z\in
U\;\wedge\;z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in W)\\}$

  * •

$W\tilde{\Leftarrow}U=\\{x\in X\;|\;\forall z,z^{\prime}\in X\;(z\in
U\;\wedge\;z^{\prime}R^{111}xz\;\longrightarrow\;z^{\prime}\in W)\\}$

###### Proof.

The proof is by the following calculation

$U\bigodot U^{\prime}\subseteq W$ | iff | $\forall z^{\prime}\in X\;(\exists z,x\in X\;(z^{\prime}R^{111}zx\;\wedge\;z\in U\;\wedge\;x\in U^{\prime})\longrightarrow z^{\prime}\in W)$
---|---|---
| iff | $\forall x,z,z^{\prime}\in X\;(x\in U^{\prime}\;\longrightarrow\;(z\in U\;\wedge\;z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in W))$
| iff |  $U^{\prime}\subseteq\\{x\in X\;|\;\forall z,z^{\prime}\in X\;(z\in U\;\wedge\;z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in W)))\\}$

and since $U\bigodot U^{\prime}\subseteq W$ iff $U^{\prime}\subseteq
U\tilde{\Rightarrow}W$ the claim for $\tilde{\Rightarrow}$ is true. Similarly,
$U\bigodot U^{\prime}\subseteq W$ iff $U\subseteq\\{z\in X\;|\;\forall
x,z^{\prime}\in X\;(x\in
U^{\prime}\;\wedge\;z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in
W)\\}$, then just change bound variables. ∎

Properties of the operator $\bigodot$ correspond to the relational constraints
of Table 2.

######  Lemma 3.2.

The following hold

  1. 1.

(C1) holds iff $\bigodot$ is associative

  2. 2.

(C2) holds iff $\bigodot$ is commutative (in which case $\tilde{\Leftarrow}$
coincides with $\tilde{\Rightarrow}$)

  3. 3.

If (C3) holds then $\bigodot$ is thinning on the family of
$\preceq$-increasing sets, i.e. the inclusion $U\bigodot W\subseteq W$ holds
for any $\preceq$-increasing $U,W\subseteq X$

  4. 4.

(C4) holds iff $\bigodot$ is contractive, i.e. the inclusion $U\cap W\subseteq
U\bigodot W$ holds for any $U,W\subseteq X$

  5. 5.

If both (C2) and (C3) hold, then $U\bigodot W\subseteq U\cap W$ for any
$U,W\subseteq X$

  6. 6.

If (C2)-(C4) all hold, then (C1) also holds since $\bigodot$ is trivialized to
the set intersection operation

###### Proof.

Assuming (C1), let $z\in(U\bigodot V)\bigodot W$, $x\in U\bigodot V$ and $u\in
U,v\in V,w\in W$ so that $xR^{111}uv$ and $zR^{111}xw$, so that $\exists
x(xR^{111}uv\;\wedge\;zR^{111}xw)$ holds. By (C1), let $x^{\prime}$ be such
that $x^{\prime}R^{111}vw$ and $zR^{111}ux^{\prime}$, so that $x^{\prime}\in
V\bigodot W$ and $z\in U\bigodot(V\bigodot W)$, hence $(U\bigodot V)\bigodot
W\subseteq U\bigodot(V\bigodot W)$. The other direction of the inclusion is
obtained similarly, going from (2) to (1). Conversely, if $\bigodot$ is
associative, then from the identity $(U\bigodot V)\bigodot
W=U\bigodot(V\bigodot W)$ the equivalence of conditions (1) and (2) is
obtained in a straightforward manner, as it is merely a restatement of the
special case of association
$(\\{u\\}\bigodot\\{v\\})\bigodot\\{w\\}=\\{u\\}\bigodot(\\{v\\}\bigodot\\{w\\})$,
for any $u,v,w\in X$.

The case of (C2) and commutativity is immediate.

Assuming (C3), let $x\in U\bigodot V$, where $U,V$ are $\preceq$-increasing.
Let $u\in U,v\in V$ so that $xR^{111}uv$. By (C3), $v\preceq x$ and since
$v\in V$, we obtain $x\in V$ by $\preceq$-increasingness of $V$.

If $x\in U\cap V$ and (C4) holds, then by $xR^{111}xx$ it follows $x\in
U\bigodot V$. Conversely, if $\bigodot$ is contractive, choose $U=\\{x\\}=V$
to get $\\{x\\}\subseteq\\{x\\}\bigodot\\{x\\}$ from which $xR^{111}xx$
follows. ∎

The sorted modal language of a frame $\mathfrak{F}=(X,\upVdash,Y,R^{111})$,
where we let $I$ be the complement of $\upVdash$, is the language

$\displaystyle\alpha$ $\displaystyle:=$ $\displaystyle
P_{i}\;(i\in\mathbb{N})\;|\;\neg\alpha\;|\;\alpha\wedge\alpha\;|\;\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta\;|\;\alpha\odot\alpha\;|\;\alpha\leftfilledspoon\alpha\;|\;\alpha\rightfilledspoon\alpha$
$\displaystyle\beta$ $\displaystyle:=$ $\displaystyle
Q_{i}\;(i\in\mathbb{N})\;|\;\neg\beta\;|\;\beta\wedge\beta\;|\;\largesquare\alpha$

The language contains a copy of the language of CPL (in the second sort), a
copy of the language of residuated Boolean algebras (in the first sort),
synthesized by the sorted modalities on which a residuation axiom will be
imposed.

The language is interpreted in models $\mathfrak{M}=(\mathfrak{F},\imath)$,
where $\imath(P_{i})\subseteq X$, $\imath(Q_{i})\subseteq Y$ and the
interpretation is extended to all sentences by adding to the clauses for CPL
(for each sort) satisfaction clauses for the additional constructs, as shown
in Table 3.

Table 3: Satisfaction clauses for sub.ML2 $x\models\alpha\odot\alpha^{\prime}$ | iff | $\exists z,z^{\prime}\in X\;(xR^{111}zz^{\prime}\;\wedge\;z\models\alpha\;\wedge\;z^{\prime}\models\alpha^{\prime})$
---|---|---
$x\models\alpha\rightfilledspoon\alpha^{\prime}$ | iff |  $\forall z,z^{\prime}\in X\;(z\models\alpha\;\wedge\;z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\models\alpha^{\prime})$
$x\models\alpha^{\prime}\leftfilledspoon\alpha$ | iff | $\forall z,z^{\prime}\in X\;(z\models\alpha\;\wedge\;z^{\prime}R^{111}xz\;\longrightarrow\;z^{\prime}\models\alpha^{\prime})$
$x\models\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta$ | iff | $\forall y\in Y\;(xIy\;\longrightarrow\;y\models\beta)$
$y\models\largesquare\alpha$ | iff |  $\forall x\in X\;(xIy\;\longrightarrow\;x\models\alpha)$

It follows directly from definitions that
$\mbox{$[\\![\alpha\odot\alpha^{\prime}]\\!]$}=\\{x\in
X\;|\;x\models\alpha\circ\alpha^{\prime}\\}=\mbox{$[\\![\alpha]\\!]$}\bigodot\mbox{$[\\![\alpha^{\prime}]\\!]$}$
and similarly
$\mbox{$[\\![\alpha\rightfilledspoon\alpha^{\prime}]\\!]$}=\mbox{$[\\![\alpha]\\!]$}\tilde{\Rightarrow}\mbox{$[\\![\alpha^{\prime}]\\!]$}$,
$\mbox{$[\\![\alpha^{\prime}\leftfilledspoon\alpha]\\!]$}=\mbox{$[\\![\alpha^{\prime}]\\!]$}\tilde{\Leftarrow}\mbox{$[\\![\alpha]\\!]$}$.

The two-sorted logic $\Lambda_{2}(\mathbb{F})$ of a class $\mathbb{F}$ of
frames $\mathfrak{F}=(X,\upVdash,Y,R^{111})$ is a pair of sets of sentences
$\Lambda_{2}(\mathbb{F})=({\tt A},{\tt B})$ such that for every $\alpha\in{\tt
A}$ and any model $\mathfrak{M}=(\mathfrak{F},\imath)$ over any frame
$\mathfrak{F}=(X,\upVdash,Y,R^{111})$ in the frame class $\mathbb{F}$,
$\mbox{$[\\![\alpha]\\!]$}_{\imath}=X$ and similarly for $\beta\in{\tt B}$,
$\mbox{$(\\!|\beta|\\!)$}_{\imath}=Y$. The hierarchy of the corresponding
sorted, residuated modal logics is displayed in Figure 2, where the modal
companion logic of a substructural logic SUB is designated by sub.ML2.

Figure 2: Hierarchy of Modal Companion Logics $\textstyle{{\bf
bck.ML}_{2}\mbox{ (C1)(C2)(C3)-frames}}$$\textstyle{{\bf bcw.ML}_{2}\mbox{
(C1)(C2)(C4)-frames}}$$\textstyle{{\bf
bci.ML}_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mbox{
(C1)(C2)-frames}}$$\textstyle{{\bf
fl.ML}_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mbox{
(C1)-frames}}$$\textstyle{{\bf
nfl.ML}_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Note that for the systems including and above bci.ML2, the signature of the
language may be restricted by dropping the (superfluous) $\leftfilledspoon$.

#### Sorted Modal Logic: The Basic System ML2

The language of the minimal two-sorted, residuated modal logic (ML2) is
generated by the following scheme

$\displaystyle\alpha$ $\displaystyle:=$ $\displaystyle
P_{i}\;(i\in\mathbb{N})\;|\;\neg\alpha\;|\;\alpha\wedge\alpha\;|\;\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta$ $\displaystyle\beta$ $\displaystyle:=$ $\displaystyle
Q_{i}\;(i\in\mathbb{N})\;|\;\neg\beta\;|\;\beta\wedge\beta\;|\;\largesquare\alpha$

Further logical connectives and constants are defined as usual in classical
normal modal logic, i.e.
$\alpha\vee\alpha^{\prime}=\neg(\neg\alpha\wedge\neg\alpha^{\prime})$,
$\top=P_{0}\vee\neg P_{0}$, $\bot=P_{0}\wedge\neg P_{0}$,
$\alpha\mbox{$\rightarrow$}\alpha^{\prime}=\neg\alpha\vee\alpha^{\prime}$ and
similarly for sentences of the second sort. In addition, diamond operators are
defined by $\largediamond\alpha=\neg\largesquare\neg\alpha$ and
$\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\beta=\neg\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\neg\beta$, where the two occurrences of negation are of different sort.
Note that there are distinct constants $\top_{1},\top_{2}$ (and similarly for
$\bot_{1},\bot_{2}$), corresponding to each sort. We avoid subscripts by
letting $\top_{{}_{1}}=\top,\bot_{{}_{1}}=\bot$ and $\top_{{}_{2}}={\tt
t},\bot_{{}_{2}}={\tt f}$.

Models $\mathfrak{M}=(\mathfrak{F},\imath)$ for ML2 on two-sorted frames
$\mathfrak{F}=(X,I,Y),I\subseteq X\times Y,$ (always assumed to satisfy
condition (3)) are defined as detailed for the general case of sub.ML2.

Let ML${}^{\bullet}_{2}$ designate the set of sentences of the first sort of
the form
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta$, for some sentence $\beta$ of the second sort. Similarly, let
ML${}^{\circ}_{2}$ designate the set of sentences of second sort of the form
$\largesquare\alpha$, for some sentence $\alpha$ of the first sort. If $A$ is
an ML${}^{\bullet}_{2}$ sentence and $B$ is an ML${}^{\circ}_{2}$ one, then
clearly,
$\mbox{$[\\![A]\\!]$}=\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond
A]\\!]$}=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\mbox{$[\\![A]\\!]$}$ and
$\mbox{$(\\!|B|\\!)$}=\mbox{$(\\!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}B|\\!)$}=\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\mbox{$(\\!|B|\\!)$}$.

In accordance with our decision for the substructural logics proof systems we
adopt a symmetric consequence system, directly encoding the algebraic
specification of the logic. Thus, sequents for the logic ML2 are of the form
$\alpha\vdash\alpha^{\prime}$, where $\alpha,\alpha^{\prime}$ are sentences of
the first sort, as well as of the form
$\beta\mbox{$\medvert\\!\\!\\!\\!\sim$}\beta^{\prime}$, where
$\beta,\beta^{\prime}$ are sentences of the second sort. The proof system
consists of axioms and rules for sequents of the first type and of the second
type, which are copies of the rules for classical propositional logic and can
be found in any standard reference. Furthermore, bridge rules are included,
shown in Table 4, to relate the two subsystems.

Table 4: Residuation Axioms, D-Axioms and Bridge Rules $\alpha\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\alpha$ |  $\largediamond\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\mbox{$\medvert\\!\\!\\!\\!\sim$}\beta$ |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\vdash\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\beta$ |  $\largesquare\alpha\mbox{$\medvert\\!\\!\\!\\!\sim$}\largediamond\alpha$ |  $\top\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\top$ | ${\tt t}\vdash\largesquare{\tt t}$
---|---|---|---|---|---
$\frac{\mbox{\rm$\alpha\vdash\alpha^{\prime}$}}{\mbox{\rm$\largesquare\alpha\mbox{$\medvert\\!\\!\\!\\!\sim$}\largesquare\alpha^{\prime}$}}$ |  $\frac{\mbox{\rm$\beta\mbox{$\medvert\\!\\!\\!\\!\sim$}\beta^{\prime}$}}{\mbox{\rm$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime}$}}$ |  $\largesquare\alpha\wedge\largesquare\alpha^{\prime}\mbox{$\medvert\\!\\!\\!\\!\sim$}\largesquare(\alpha\wedge\alpha^{\prime})$ |  |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta\wedge\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta^{\prime}\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt(\beta\wedge\beta^{\prime})$

For semantic entailment we write $\alpha\models\alpha^{\prime}$ and
$\beta\models\beta^{\prime}$ (we do not change notation between the two
sorts), with a standard, classical understanding. As usual, we write
$\vdash\alpha$ stand for $\top\vdash\alpha$, as well as $\models\alpha$ for
$\top\models\alpha$ and similarly for $\vdash\beta$ and $\models\beta$. It is
immediate that ML2 is sound in the class of two-sorted frames satisfying
condition (3).

The Lindenbaum-Tarski algebra of the logic is naturally a two-sorted algebra
$(\mathcal{A},\mathcal{B},\Diamond,\blacksquare)$ where both ${\mathcal{A},B}$
are Boolean algebras,
$\Diamond:\mathcal{A}\rightleftarrows\mathcal{B}:\blacksquare$ are normal
modal operators satisfying the D-axiom $\blacksquare
b\leq\raisebox{-1.5pt}{\mbox{\LARGE{$\filleddiamond$}}}b$ and $\Box
a\leq\Diamond a$ and, in addition, for any $a\in\mathcal{A},b\in\mathcal{B}$,
$\Diamond a\leq b$ iff $a\leq\blacksquare b$ and then also
$\raisebox{-1.5pt}{\mbox{\LARGE{$\filleddiamond$}}}b\leq a$ iff $b\leq\Box a$
where boxes and diamonds are interdefinable using classical complementation,
as usual.

Soundness is immediate and completeness of ML2 is proven along the lines of
the completeness proof for normal modal logics, except that we consider both
the set $X=\mbox{\rm Ult}(\mathcal{A})$ of ultrafilters of $\mathcal{A}$
(consisting of equivalence classes of sentences of the first sort), as well as
the set $Y=\mbox{\rm Ult}(\mathcal{B})$ of ultrafilters of $\mathcal{B}$
(consisting of equivalence classes of sentences of the second sort). The
canonical relation $I\subseteq X\times Y$ is defined along the standard lines:
$uIv$ iff for all $b\in\mathcal{B}$, if $\blacksquare b\in u$, then $b\in v$.
This can be shown to be equivalent to the definition $\forall a\;(a\in
u\;\longrightarrow\;\raisebox{-1.5pt}{\mbox{\LARGE{$\filleddiamond$}}}a\in
v)$, as usual. Furthermore, by residuation, the defining condition for the
accessibility relation $I$ can be stated analogously and equivalently using
$\Box$ (or $\Diamond$). We state the completeness result below; details are
left to the interested reader.

######  Proposition 3.3.

ML2 is sound and complete in two-sorted frames satisfying conditions (3).
$\leftVdash$

The proof systems of the modal companion logics sub.ML2, extending ML2, are
specified as follows.

#### nfl.ML2

Monotonicity and residuation axioms for
$\leftfilledspoon,\odot,\rightfilledspoon$ are added

$\frac{\mbox{\rm$\alpha\vdash\alpha_{1}\hskip 14.22636pt\alpha^{\prime}\vdash\alpha^{\prime}_{1}$}}{\mbox{\rm$\alpha\odot\alpha^{\prime}\vdash\alpha_{1}\odot\alpha^{\prime}_{1}$}}$ |  |
---|---|---
$\alpha\odot(\alpha\rightfilledspoon\alpha^{\prime})\vdash\alpha^{\prime}$ | $\alpha^{\prime}\vdash\alpha\rightfilledspoon(\alpha\odot\alpha^{\prime})$ | $\frac{\mbox{\rm$\alpha\vdash\alpha_{1}\hskip 14.22636pt\alpha^{\prime}_{1}\vdash\alpha^{\prime}$}}{\mbox{\rm$\alpha_{1}\rightfilledspoon\alpha^{\prime}_{1}\vdash\alpha\rightfilledspoon\alpha^{\prime}$}}$
$\alpha^{\prime}\vdash(\alpha\odot\alpha^{\prime})\leftfilledspoon\alpha$ | $(\alpha^{\prime}\leftfilledspoon\alpha)\odot\alpha\vdash\alpha^{\prime}$ | $\frac{\mbox{\rm$\alpha_{1}\vdash\alpha\hskip 14.22636pt\alpha^{\prime}\vdash\alpha_{1}^{\prime}$}}{\mbox{\rm$\alpha\leftfilledspoon\alpha^{\prime}\vdash\alpha_{1}\leftfilledspoon\alpha_{1}^{\prime}$}}$

#### fl.ML2 = nfl.ML2 \+ Associativity axioms

$\alpha_{1}\odot(\alpha_{2}\odot\alpha_{3})\vdash(\alpha_{1}\odot\alpha_{2})\odot\alpha_{3}$
and
$(\alpha_{1}\odot\alpha_{2})\odot\alpha_{3}\vdash\alpha_{1}\odot(\alpha_{2}\odot\alpha_{3})$

#### bci.ML2 = fl.ML2 \+ Commutativity axiom

$\alpha\odot\alpha^{\prime}\vdash\alpha^{\prime}\odot\alpha$

#### bcw.ML2 = bci.ML2 \+ Contraction axiom

$\alpha\wedge\alpha^{\prime}\vdash\alpha\odot\alpha^{\prime}$

#### bck.ML2 = bci.ML2 \+ Controlled weakening axiom

$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta\odot\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta^{\prime}\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta^{\prime}$

It follows from the axiomatization that the Lindenbaum algebra of nfl.ML2 is a
sorted, residuated modal algebra
$\Diamond:\mathcal{A}\leftrightarrows\mathcal{B}:\blacksquare$, where in
addition $(\mathcal{A},\leftfilledspoon,\circ,\rightfilledspoon)$ is a
residuated Boolean algebra. Adding associativity, commutativity and
contraction axioms, the operator $\circ$ of the algebra
$(\mathcal{A},\leftfilledspoon,\circ,\rightfilledspoon)$ is associative,
commutative, contractive, respectively, and, with commutativity,
$\leftfilledspoon=\rightfilledspoon$. Note that contractiveness of $\odot$ can
be assumed, yielding bcw.ML2, but not weakening, which can only be introduced
in a controlled way (reminiscent of Linear Logic’s ! operator). Recall that
satisfaction clauses (on top of the usual clauses for CPL, for each sort of
sentences) have been specified in Table 3.

######  Theorem 3.4 (sub.ML2 Soundness).

sub.ML2 is sound in $\mathbb{SUB}$-frames.

###### Proof.

The proof was essentially given in Lemma 3.2. For soundness of the bck.ML2
axiom
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta\odot\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta^{\prime}\vdash\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta^{\prime}$ it only needs to be observed that, given a frame
$(X,\upVdash,Y,R^{111})$, for any subset $V\subseteq Y$, the set
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0ptV\subseteq X$ is $\preceq$-increasing, since it is a Galois stable set
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0ptV=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0ptV$ (by residuation). ∎

###  3.2 Formal Concept Lattice Logics

Let $\mathfrak{F}=(X,\upVdash,Y,R^{111})$ be a frame and let $\bigovert$ be
the closure of the restriction of $\bigodot$ on the set ${\mathcal{G}}(X)$ of
Galois stable subsets of $X$, i.e. $A\bigovert
C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)$. The Galois dual operator
$\bigovert^{\\!\partial}$ is defined on co-stable sets
$B=A\mbox{${}^{\upVdash}$},D=C\mbox{${}^{\upVdash}$}$ by

$B\bigovert^{\\!\partial}D=({}\mbox{${}^{\upVdash}$}B\bigovert{}\mbox{${}^{\upVdash}$}D)\mbox{${}^{\upVdash}$}=(A\bigovert
C)\mbox{${}^{\upVdash}$}=\bigcap_{u\in A,u^{\prime}\in C}R^{\partial
11}uu^{\prime}$ (9)

where we let $R^{\partial 11}$ be defined by $R^{\partial
11}uu^{\prime}=(R^{111}uu^{\prime})\mbox{${}^{\upVdash}$}$, i.e. for any $y\in
Y$ it holds that $yR^{\partial 11}uu^{\prime}$ iff $\forall x\in
X\;(xR^{111}uu^{\prime}\longrightarrow x\upVdash y)$. Hence we have
$B\bigovert^{\\!\partial}D=\bigcap_{u\in A,u^{\prime}\in C}R^{\partial
11}uu^{\prime}$ and it then follows that $\bigovert^{\partial}$ distributes
over arbitrary intersections of co-stable sets in each argument place.
Therefore, by duality, $\bigovert$ distributes over arbitrary joins of Galois
stable sets and hence it is residuated in ${\mathcal{G}}(X)$, with residuals
$\Leftarrow,\Rightarrow$, i.e. $C\subseteq F\Leftarrow A$ iff $A\bigovert
C\subseteq F$ iff $F\subseteq A\Rightarrow C$.

######  Lemma 3.5.

The residuals $\Leftarrow,\Rightarrow$ of $\bigovert$ are the restrictions of
the residuals $\tilde{\Leftarrow},\tilde{\Rightarrow}$ of $\bigodot$ on stable
sets. They are equivalently defined by

$A\Rightarrow C$ | = | $\\{x\in X\;|\;\forall z\in X\;\forall v\in Y\;(z\in A\;\wedge\;C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))\\}$
---|---|---
$C\Leftarrow A$ | = |  $\\{x\in X\;|\;\forall z\in X\;\forall v\in Y\;(z\in A\;\wedge\;C\upVdash v\;\longrightarrow\;vR^{\partial 11}xz))\\}$

###### Proof.

Note that for a stable set
$A=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond A$ and any set $U$ the inclusion
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond U\subseteq A$ obtains iff the inclusion $U\subseteq A$
does. In particular, $A\bigovert C\subseteq F$ iff $A\bigodot C\subseteq F$,
from which the first claim of the corollary follows. For the second claim we
do only the case for $\Rightarrow$ (repeating the computation from [37]).

|  $A\bigovert F\subseteq C$
---|---
iff |  $A\bigodot F\subseteq C$
iff | $\forall z^{\prime}\in X\;(z^{\prime}\in A\bigodot F\;\longrightarrow\;z^{\prime}\in C)$
iff | $\forall z^{\prime}\;(\exists x\in X\;\exists z\in X\;(z^{\prime}R^{111}zx\;\wedge\;z\in A\;\wedge\;x\in F)\;\longrightarrow\;z^{\prime}\in C)$
iff | $\forall x,z,z^{\prime}\in X\;((z^{\prime}R^{111}zx\;\wedge\;z\in A\;\wedge\;x\in F)\;\longrightarrow\;z^{\prime}\in C)$
iff | $\forall x,z,z^{\prime}\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;(z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in C))$
iff | $\forall x,z\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;\forall z^{\prime}\in X\;(z^{\prime}R^{111}zx\;\longrightarrow\;z^{\prime}\in C))$
iff | $\forall x,z\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;(R^{111}zx\;\subseteq\;C))$
iff | $\forall x,z\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;(C\mbox{${}^{\upVdash}$}\subseteq(R^{111}zx)\mbox{${}^{\upVdash}$}))$
iff |  $\forall x,z\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;(C\mbox{${}^{\upVdash}$}\subseteq R^{\partial 11}zx))$
iff | $\forall x,z\in X\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;\forall v\in Y\;(C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))$
iff | $\forall x,z\in X\;\forall v\in Y\;((z\in A\;\wedge\;x\in F)\;\longrightarrow\;(C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))$
iff | $\forall x,z\in X\;\forall v\in Y\;(x\in F\;\longrightarrow\;(z\in A\longrightarrow(C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx)))$
iff | $\forall x,z\in X\;\forall v\in Y\;(x\in F\;\longrightarrow\;(z\in A\;\wedge\;C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))$
iff | $\forall x\in X\;(x\in F\;\longrightarrow\;\forall z\in X\;\forall v\in Y\;(z\in A\;\wedge\;C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))$
iff | $F\subseteq\\{x\in X\;|\;\forall z\in X\;\forall v\in Y\;(z\in A\;\wedge\;C\upVdash v\;\longrightarrow\;vR^{\partial 11}zx))\\}$
iff |  $F\subseteq A\Rightarrow C$

The case for $\Leftarrow$ can be obtained from the above by appropriately
modifying the last few lines, then changing bound variables to obtain the
definition of $\Leftarrow$ as stated in the lemma. ∎

######  Lemma 3.6.

If $\bigodot$ is associative, commutative, thinning, or contractive, then so
is $\bigovert$. Consequently, the obvious correlation obtains between the
frame constraints of Table 2 and properties of the $\bigovert$ operator on the
complete lattice ${\mathcal{G}}(X)$ of Galois stable subsets of $X$ (which is
isomorphic to the formal concept lattice of the frame).

###### Proof.

We first verify that associativity of $\bigodot$ implies associativity of
$\bigovert$. Recall first that if $A$ is a stable set, then
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond U\subseteq A$ iff $U\subseteq A$, for any set $U$. This
implies in particular that $F\subseteq A\Rightarrow C$ (iff $A\bigovert
F\subseteq C$) iff $A\bigodot F\subseteq C$, for stable sets $A,F,C$. We then
obtain

$A\bigovert(C\bigovert E)\subseteq(A\bigovert C)\bigovert E$ | iff | $A\bigodot(C\bigovert E)\subseteq(A\bigovert C)\bigovert E$
---|---|---
| iff | $C\bigovert E\subseteq A\Rightarrow((A\bigovert C)\bigovert E)$
| iff | $C\bigodot E\subseteq A\Rightarrow((A\bigovert C)\bigovert E)$
| iff | $A\bigodot(C\bigodot E)\subseteq(A\bigovert C)\bigovert E$
Similarly,
$(A\bigovert C)\bigovert E\subseteq A\bigovert(C\bigovert E)$ | iff |  $(A\bigodot C)\bigodot E\subseteq A\bigovert(C\bigovert E)$

Hence, given associativity of $\bigodot$ and given that we have, by
monotonicity, $A\bigodot(C\bigodot E)\subseteq A\bigovert(C\bigovert E)$ and,
similarly, $(A\bigodot C)\bigodot E\subseteq(A\bigovert C)\bigovert E$, it
follows that $\bigovert$ is associative. By duality,
$B\bigovert^{\\!\partial}D=({}\mbox{${}^{\upVdash}$}B\bigovert{}\mbox{${}^{\upVdash}$}D)\mbox{${}^{\upVdash}$}$
and $A\bigovert
C={}\mbox{${}^{\upVdash}$}(A\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}C\mbox{${}^{\upVdash}$})$,
this implies associativity of $\bigovert^{\\!\partial}$. For the reader’s
reassurance we display the calculation, given formal concepts
$(A,B),(C,D),(E,F)$ (i.e.
$B=A\mbox{${}^{\upVdash}$},D=C\mbox{${}^{\upVdash}$},F=E\mbox{${}^{\upVdash}$}$).

$(B\bigovert^{\\!\partial}D)\bigovert^{\\!\partial}F$ | = |  $(A\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}C\mbox{${}^{\upVdash}$})\bigovert^{\\!\partial}E\mbox{${}^{\upVdash}$}$ | = | $(A\bigovert C)\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}E\mbox{${}^{\upVdash}$}$
---|---|---|---|---
| = |  $((A\bigovert C)\bigovert E)\mbox{${}^{\upVdash}$}$ | = | $(A\bigovert(C\bigovert E))\mbox{${}^{\upVdash}$}$
| = |  $A\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}(C\bigovert E)\mbox{${}^{\upVdash}$}$ | = | $A\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}(C\mbox{${}^{\upVdash}$}\bigovert^{\\!\partial}E\mbox{${}^{\upVdash}$})$
| = |  $B\bigovert^{\\!\partial}(D\bigovert^{\\!\partial}F)$

It is clear that $\bigovert$ is commutative iff $\bigodot$ is.

For the thinning property, assuming $\bigodot$ is thinning on
$\preceq$-increasing sets then in particular for stable sets $A,C$ we have
$A\bigodot C\subseteq C$, hence
$\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)\subseteq C$, given stability of $C$, which
means by definition that $A\bigovert C\subseteq C$.

For contractiveness, assume $U\cap U^{\prime}\subseteq U\bigodot U^{\prime}$
for any sets $U,U^{\prime}\subseteq X$. In particular for stable sets $A\cap
C\subseteq A\bigodot C$ and, taking closure, $A\cap C\subseteq A\bigovert C$.
∎

Language and semantics for formal concept logics are those for substructural
logics, presented in Section 2.2. As noted in Section 2.2, it is sufficient
for the purposes of this article to consider proof systems as symmetric
consequence systems $\varphi\vdash\psi$, directly encoding the algebraic
specification of the logic. The relational semantics of the substructural
systems has been specified in Table 1. Algebraic soundness and completeness
are well-established in the literature on substructural logics and, thereby,
completeness in relational semantics can be established by a representation
argument. For soundness, we verify that the algebra of stable subsets of the
set $X$ of a frame $\mathfrak{F}=(X,\upVdash,Y,R^{111})$ is in the equational
class of the Lindenbaum-Tarski algebra of the logic.

######  Theorem 3.7 (Soundness for SUB).

Every substructural system SUB of Figure 1 is sound in the corresponding frame
class $\mathbb{SUB}$, as defined in Definition 2.2.

###### Proof.

Let $\mathfrak{F}=(X,\upVdash,Y,R^{111})$ be a frame and ${\mathcal{G}}(X)$
its complete lattice of stable sets. In Sections 3.1 and 3.2 we have shown
that ${\mathcal{G}}(X)$ is equipped with an operator $\bigovert$, residuated
with implication operators $\Leftarrow,\Rightarrow$. This suffices for
soundness of NFL in the class $\mathbb{NFL}$.

For the associative Lambek Calculus FL, the corresponding frame class
$\mathbb{FL}$ assumes the constraint (C1) of Table 2. In Lemma 3.2 it was
shown that (C1) is equivalent to associativity of $\bigodot$ and in Lemma 3.6
we verified that associativity of $\bigodot$ implies associativity of
$\bigovert$, which was defined on stable sets by setting $A\bigovert
C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)$. Furthermore, it was shown in Section 3.2
that $\bigovert$ is residuated in ${\mathcal{G}}(X)$ (and we in fact verified
in Lemma 3.5 that its residuals $\Leftarrow,\Rightarrow$ are the respective
restrictions of the residuals $\tilde{\Leftarrow},\tilde{\Rightarrow}$ of
$\bigodot$ in the algebra of all subsets of $X$). This establishes soundness
of FL in its homonym frame class $\mathbb{FL}$.

For BCI, Lemma 3.2 verified the equivalence between the constraint (C2) and
commutativity of $\bigodot$, from which commutativity of $\bigovert$
immediately follows, as observed in Lemma 3.6. Therefore, BCI is sound in its
corresponding frame class $\mathbb{BCI}$.

For BCW, assuming contraction, it was verified in Lemma 3.2 that the
relational constraint (C4) in the frame class $\mathbb{BCW}$ is equivalent to
contractiveness of $\bigodot$, which immediately implies contractiveness of
$\bigovert$, as observed in Lemma 3.6, i.e. the inequation $a\wedge b\leq
a\circ b$ holds in ${\mathcal{G}}(X)$. In other words, BCW is sound in the
class $\mathbb{BCW}$.

For BCK, assuming weakening, it was verified in Lemma 3.2 that if the
relational constraint (C3) (i.e. $\forall x,z,z^{\prime}\in
X\;(xR^{111}zz^{\prime}\longrightarrow z^{\prime}\preceq x)$) holds, then the
inclusion $U\bigodot V\subseteq V$ holds for $\preceq$-increasing sets, and
since every stable set is $\preceq$-increasing it follows that $A\bigodot
C\subseteq C$, from which we obtain $A\bigovert
C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)\subseteq C$, given that we assume $C$ to be
stable. Therefore, BCK is sound in the $\mathbb{BCK}$ frame class and this
concludes the proof. ∎

##  4 Modal Translation of Substructural Logics

In [38] we proved, via translation, that PLL (Positive Lattice Logic) is a
fragment of ML2. We defined a translation $\varphi^{\bullet}$ and a co-
translation $\varphi^{\circ}$ of a sentence $\varphi$ of the language of PLL
into the two-sorted modal language ML2, by recursion, and we proved that the
translation is full and faithful. This section extends the result to any
substructural logic.

In Table 5, the translation of PLL into ML2 defined in [38] is extended to
include the case of substructural logics.

Table 5: Translation and co-translation of SUB into sub.ML2 $p_{i}^{\bullet}$ | = |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond P_{i}$ |  $p_{i}^{\circ}$ | = | $\largesquare\neg P_{i}$
---|---|---|---|---|---
$\top^{\bullet}$ | = |  $\top$ |  $\top^{\circ}$ | = | ${\tt f}$
$\bot^{\bullet}$ | = |  $\bot$ |  $\bot^{\circ}$ | = | ${\tt t}$
$(\varphi\wedge\psi)^{\bullet}$ | = |  $\varphi^{\bullet}\wedge\psi^{\bullet}$ | $(\varphi\wedge\psi)^{\circ}$ | = | $\largesquare(\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\varphi^{\circ}\vee\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\psi^{\circ})$
$(\varphi\vee\psi)^{\bullet}$ | = |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt(\largediamond\varphi^{\bullet}\vee\largediamond\psi^{\bullet})$ |  $(\varphi\vee\psi)^{\circ}$ | = | $\varphi^{\circ}\wedge\psi^{\circ}$
$(\varphi\circ\psi)^{\bullet}$ | = |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(\varphi^{\bullet}\odot\psi^{\bullet})$ | $(\varphi\circ\psi)^{\circ}$ | = | $\largesquare\neg(\varphi^{\bullet}\odot\psi^{\bullet})$
$(\varphi\mbox{$\rightarrow$}\psi)^{\bullet}$ | = |  $\varphi^{\bullet}\rightfilledspoon\psi^{\bullet}$ |  $(\varphi\mbox{$\rightarrow$}\psi)^{\circ}$ | = | $\largesquare\neg(\varphi\mbox{$\rightarrow$}\psi)^{\bullet}$
$(\psi\mbox{$\leftarrow$}\varphi)^{\bullet}$ | = |  $\psi^{\bullet}\leftfilledspoon\varphi^{\bullet}$ |  $(\psi\mbox{$\leftarrow$}\varphi)^{\circ}$ | = |  $\largesquare\neg(\psi\mbox{$\leftarrow$}\varphi)^{\bullet}$

######  Theorem 4.1.

Let $\mathfrak{F}$ be a $\mathbb{SUB}$-frame and
$\mathfrak{M}=(\mathfrak{F},\imath)$ a sub.ML2-model. Define a SUB-model
$\mathfrak{N}$ on $\mathfrak{F}$ by setting
$V(p_{i})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\imath(P_{i})$. Then for any SUB-sentences $\varphi,\psi$

  1. 1.

$\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}=\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}=\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\neg\varphi^{\circ}]\\!]$}_{\mathfrak{M}}=\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}$

  2. 2.

$\mbox{$(\\!|\varphi|\\!)$}_{\mathfrak{N}}=\mbox{$(\\!|\varphi^{\circ}|\\!)$}_{\mathfrak{M}}=\mbox{$(\\!|\largesquare\neg\varphi^{\bullet}|\\!)$}_{\mathfrak{M}}=\mbox{$(\\!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\varphi^{\circ}|\\!)$}_{\mathfrak{M}}$

  3. 3.

$\varphi\Vdash\psi$ iff $\varphi^{\bullet}\models\psi^{\bullet}$ iff
$\psi^{\circ}\models\varphi^{\circ}$

###### Proof.

Claim 3) is an immediate consequence of the first two, which we prove
simultaneously by structural induction. Note that, for 2), the identities
$\mbox{$(\\!|\varphi|\\!)$}_{\mathfrak{N}}=\mbox{$(\\!|\largesquare\neg\varphi^{\bullet}|\\!)$}_{\mathfrak{M}}=\mbox{$(\\!|\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\varphi^{\circ}|\\!)$}_{\mathfrak{M}}$
are easily seen to hold for any $\varphi$, given the proof of claim 1), since

$\mbox{$(\\!|\varphi|\\!)$}_{\mathfrak{N}}=\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}^{\upVdash}=\largesquare(-\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}})=\mbox{$[\\![\largesquare\neg\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}$
$\mbox{$(\\!|\varphi|\\!)$}_{\mathfrak{N}}=\largesquare(-\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}})=\largesquare(-\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\varphi^{\bullet}]\\!]$}_{\mathfrak{M}})=\mbox{$[\\![\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\largesquare\neg\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}=\mbox{$[\\![\largesquare\raisebox{-3.5pt}{\mbox{\Huge{$\filleddiamond$}}}\varphi^{\circ}]\\!]$}_{\mathfrak{M}}$

For the induction proof, the cases for PLL have been covered in [38],
Proposition 4.1, to which we refer the reader for details.

  1. (Case $\bigovert$)

The following calculation proves the claim.

$\mbox{$[\\![\varphi\circ\psi]\\!]$}_{\mathfrak{N}}$ | = |  $\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}\bigovert\mbox{$[\\![\psi]\\!]$}_{\mathfrak{N}}$ |
---|---|---|---
| = |  $\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}\bigovert\mbox{$[\\![\psi^{\bullet}]\\!]$}_{\mathfrak{M}}$ | By induction
| = | $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}\bigodot(\mbox{$[\\![\psi^{\bullet}]\\!]$}_{\mathfrak{M}})$ |
| = |  $\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond\mbox{$[\\![\varphi^{\bullet}\bigodot\psi^{\bullet}]\\!]$}_{\mathfrak{M}}$ |
| = |  $\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\largediamond(\varphi^{\bullet}\bigodot\psi^{\bullet})]\\!]$}_{\mathfrak{M}}$ |
| = |  $\mbox{$[\\![(\varphi\circ\psi)^{\bullet}]\\!]$}_{\mathfrak{M}}$ | By defn of modal translation

The other two identities for claim 1) are straightforward, given definitions.
For 2), observe that
$\mbox{$(\\!|\varphi\circ\psi|\\!)$}_{\mathfrak{N}}=\mbox{$(\\!|\varphi|\\!)$}_{\mathfrak{N}}\bigovert^{\\!\partial}\mbox{$(\\!|\psi|\\!)$}_{\mathfrak{N}}=\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}^{\upVdash}\bigovert^{\\!\partial}\mbox{$[\\![\psi]\\!]$}_{\mathfrak{N}}^{\upVdash}$
$=(\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}\bigovert\mbox{$[\\![\psi]\\!]$}_{\mathfrak{N}})^{\upVdash}=\largesquare(-\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(\varphi^{\bullet}\bigodot\psi^{\bullet})]\\!]$}_{\mathfrak{M}})=\mbox{$(\\!|\largesquare\neg(\varphi^{\bullet}\bigodot\psi^{\bullet})|\\!)$}_{\mathfrak{M}}$
but the latter is precisely
$\mbox{$(\\!|(\varphi\circ\psi)^{\circ}|\\!)$}_{\mathfrak{M}}$.

  2. (Case $\Rightarrow$)

By definition of semantics and by the fact that $\Rightarrow$ is the
restriction of $\tilde{\Rightarrow}$ on stable sets, see Lemma 3.5, we obtain

$\mbox{$[\\![\varphi\mbox{$\rightarrow$}\psi]\\!]$}_{\mathfrak{N}}$ | = | $\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}\Rightarrow\mbox{$[\\![\psi]\\!]$}_{\mathfrak{N}}$
---|---|---
| = |  $\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}\tilde{\Rightarrow}\mbox{$[\\![\psi^{\bullet}]\\!]$}_{\mathfrak{M}}$ By induction and Lemma 3.5
| = | $\mbox{$[\\![\varphi^{\bullet}\rightfilledspoon\psi^{\bullet}]\\!]$}_{\mathfrak{M}}$
| = |  $\mbox{$[\\![(\varphi\mbox{$\rightarrow$}\psi)^{\bullet}]\\!]$}_{\mathfrak{M}}$

  3. (Case $\Leftarrow$)

Similar to the case for $\Rightarrow$.

Hence for any $\varphi$ we obtained that
$\mbox{$[\\![\varphi]\\!]$}_{\mathfrak{N}}=\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}$
and the identities
$\mbox{$[\\![\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}=\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\neg\varphi^{\circ}]\\!]$}_{\mathfrak{M}}=\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\varphi^{\bullet}]\\!]$}_{\mathfrak{M}}$ have been verified
for the PLL fragment in [38] and are immediate for
$\circ,\mbox{$\leftarrow$},\mbox{$\rightarrow$}$ by the way the co-translation
was defined. ∎

To transfer the result to the provability relation, completeness results need
to be established, for each system SUB and its companion modal logic sub.ML2.

######  Theorem 4.2 (Completeness for SUB).

Every substructural system SUB of Figure 1 is (sound, by Theorem 3.7, and)
complete in the corresponding frame class $\mathbb{SUB}$, as defined in
Definition 2.2.

###### Proof.

For completeness, let $\mathcal{L}$ be the Lindenbaum-Tarski algebra of the
logic and let $\mathfrak{F}=(\mbox{\rm Filt}(\mathcal{L}),\upVdash,\mbox{\rm
Idl}(\mathcal{L}))$ be the canonical lattice frame [40], where $\mbox{\rm
Filt}(\mathcal{L})$ is the complete lattice of (proper) lattice-filters,
$\mbox{\rm Idl}(\mathcal{L})$ is the complete lattice of (proper) lattice-
ideals and $x\upVdash y$ iff $x\cap y\neq\emptyset$. Note that the canonical
frame is separated i.e. the pre-order induced by setting $x\preceq z$ iff
$\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$ is a
partial order on $X$ and similarly for $Y$. This is because if
$\\{x\\}\mbox{${}^{\upVdash}$}\subseteq\\{z\\}\mbox{${}^{\upVdash}$}$, then
for any $a\in x$, $x\upVdash y_{a}$, hence $z\upVdash y_{a}$ which implies
that $a\in z$. Furthermore, it follows from the definition of $\upVdash$ that
it is increasing in each argument place.

Following [34] and as detailed in [39, 37], define the canonical relation
$R^{111}$ by first defining a point operator
$x\widehat{\circ}z=\bigvee\\{x_{a\circ b}\;|\;a\in x,b\in z\\}$ on filters,
where $x,z,z^{\prime}\in X$ and $x_{e}=e\\!\uparrow$ designates a principal
filter and then letting $xR^{111}zz^{\prime}\mbox{ iff
}z\widehat{\circ}z^{\prime}\leq x$, where $\leq$ designates filter inclusion.
Note that for any $x,z,z^{\prime}$ we easily obtain from the definition that

$xR^{111}zz^{\prime}\;\mbox{ iff }\;\forall a,b\;(a\in z\;\wedge\;b\in
z^{\prime}\;\longrightarrow\;a\circ b\in x)$

It remains to show (a) that the canonical frame for a substructural logic SUB
is a $\mathbb{SUB}$-frame and that (b) the canonical (co)interpretation,
defined by $\mbox{$[\\![\varphi]\\!]$}=\\{x\in\mbox{\rm
Filt}(\mathcal{L})\;|\;[\varphi]\in x\\}$ and
$\mbox{$(\\!|\varphi|\\!)$}=\\{y\in\mbox{\rm
Idl}(\mathcal{L})\;|\;[\varphi]\in y\\}$ respects the recursive satisfaction
conditions of Table 1. We do this next in two lemmas, the canonical frame and
canonical interpretation lemmas. ∎

######  Lemma 4.3 (Canonical SUB-Frame Lemma).

The canonical frame for a substructural logic SUB is a $\mathbb{SUB}$-frame.

###### Proof.

There is nothing to prove for NFL. We argue separately each case of a logic
above NFL (see Figure 1).

#### FL

To show that for all points $w,z,u,v\in X$, statements (1) and (2) below are
equivalent in the canonical frame

> (1) $\exists x\;(xR^{111}uv\;\wedge\;zR^{111}xw)$ (2) $\exists
> x\;(xR^{111}vw\;\wedge\;zR^{111}ux)$

note first that equivalence of (1), (2) is an immediate consequence of
associativity of the point operator $\widehat{\circ}$. Indeed, assuming (1)
holds, i.e. for some $x\in X$ both $u\widehat{\circ}v\leq x$ and
$x\widehat{\circ}w\leq z$ hold, then $(u\widehat{\circ}v)\widehat{\circ}w\leq
x\widehat{\circ}w\leq z$ and we may take $x^{\prime}=v\widehat{\circ}w$.
Similarly for the converse.

To prove associativity of the point operator $\widehat{\circ}$ note that it
follows from [34] (Theorem 6.6) where point operators were first introduced
that $\widehat{\circ}$ distributes over arbitrary joins in each argument
place, given that the lattice operator $\circ$ distributes over binary joins
and that ([34], Lemma 6.7) it preserves principal filters, i.e.
$x_{a}\widehat{\circ}x_{b}=x_{a\circ b}$. It is then obtained that

$u\widehat{\circ}(v\widehat{\circ}w)$ | = |  $(\bigvee_{a\in u}x_{a})\widehat{\circ}((\bigvee_{b\in v}x_{b})\widehat{\circ}(\bigvee_{c\in w}x_{c}))$ | = | $\bigvee_{a\in u,b\in v,c\in w}(x_{a}\widehat{\circ}(x_{b}\widehat{\circ}x_{c}))$
---|---|---|---|---
| = |  $\bigvee_{a\in u,b\in v,c\in w}x_{a\circ(b\circ c)}$ | = | $\bigvee_{a\in u,b\in v,c\in w}x_{(a\circ b)\circ c}$
| = | $\cdots$ | = |  $(u\widehat{\circ}v)\widehat{\circ}w$

and this establishes associativity of $\widehat{\circ}$. This implies,
incidentally, that the associativity equation is canonical. Indeed, recall
that the operator $\bigovert$, defined on stable sets by $A\bigovert
C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)$, was shown in [39, 37] to be the
$\sigma$-extension $\circ^{\sigma}$ of the lattice cotenability operator
$\circ$. From [27], recall that $\circ^{\sigma}$ is first defined on closed
elements of ${\mathcal{G}}(X)$ (sets of the form $\Gamma x=\\{z\in X\;|\;x\leq
z\\}$) by setting

$\Gamma z\circ^{\sigma}\Gamma z^{\prime}=\bigwedge\\{\Gamma x_{a\circ
b}\;|\;a\in z,b\in z^{\prime}\\}$

then extended to all stable sets using join-density of closed elements by
setting $A\circ^{\sigma}C=\bigvee_{z\in A,z^{\prime}\in C}(\Gamma
z\circ^{\sigma}\Gamma z^{\prime})$. As pointed out in [39, 35, 37, 36], this
delivers the same map on stable sets as the map defined on closed elements by
setting $\Gamma z\medcircle\Gamma
z^{\prime}=\Gamma(z\widehat{\circ}z^{\prime})$, then again extending to all
stable sets by using join-density of closed elements. This is immediate since
$\bigwedge\\{\Gamma x_{a\circ b}\;|\;a\in z,b\in
z^{\prime}\\}=\Gamma\left(\bigvee\\{x_{a\circ b}\;|\;a\in z,b\in
z^{\prime}\\}\right)$, where by the definition of point operators in [34] we
have $\bigvee\\{x_{a\circ b}\;|\;a\in z,b\in
z^{\prime}\\}=z\widehat{\circ}z^{\prime}$. Thereby, the identity
$A\bigovert(C\bigovert F)=(A\bigovert C)\bigovert F$ obtains on stable sets
iff the identity $\Gamma u\bigovert(\Gamma v\bigovert\Gamma w)=(\Gamma
u\bigovert\Gamma v)\bigovert\Gamma w$ on closed elements holds. Given the fact
pointed out above that $\Gamma z\bigovert\Gamma z^{\prime}=\Gamma
z\medcircle\Gamma z^{\prime}=\Gamma(z\widehat{\circ}z^{\prime})$,
associativity of the filter operator $\widehat{\circ}$ implies canonicity of
the associativity equation since $\Gamma u\mbox{$\bigovert$}(\Gamma
v\mbox{$\bigovert$}\Gamma w)=(\Gamma u\mbox{$\bigovert$}\Gamma
v)\mbox{$\bigovert$}\Gamma w\mbox{ iff
}\Gamma(u\widehat{\circ}(v\widehat{\circ}w))=\Gamma((u\widehat{\circ}v)\widehat{\circ}w)$,
which is equivalent to the identity
$u\widehat{\circ}(v\widehat{\circ}w)=(u\widehat{\circ}v)\widehat{\circ}w$,
given that the canonical lattice frame is separated.

#### BCI

The case is straightforward, since by definition of $\;\widehat{\circ}$, if
$\circ$ is commutative, then so is the operator $\widehat{\circ}$:
$z\widehat{\circ}z^{\prime}=\bigvee\\{x_{a\circ b}\;|\;a\in z,b\in
z^{\prime}\\}=\bigvee\\{x_{b\circ a}\;|\;a\in z,b\in
z^{\prime}\\}=z^{\prime}\widehat{\circ}z$. Hence $xR^{111}zz^{\prime}$ holds
iff $xR^{111}z^{\prime}z$ holds, i.e. the constraint (C2) holds in the
canonical frame.

#### BCK

Given $a\circ b\leq b$, we obtain $x_{b}\leq x_{a\circ b}$ for any $a$. Hence

$z^{\prime}=\bigvee_{b\in z^{\prime}}x_{b}\leq\bigvee_{b\in
z^{\prime}}x_{a\circ b}\leq\bigvee_{a\in z,b\in z^{\prime}}x_{a\circ
b}=z\widehat{\circ}z^{\prime}$

Therefore, if $xR^{111}zz^{\prime}$, i.e. $z\widehat{\circ}z^{\prime}\leq x$,
it follows that $z^{\prime}\leq z\widehat{\circ}z^{\prime}\leq x$ and thereby
the constraint (C3) holds in the canonical frame.

#### BCW

We now have $a\wedge b\leq a\circ b$, i.e. $x_{a\circ b}\leq x_{a\wedge b}$.
Then

$z\widehat{\circ}z^{\prime}=\bigvee_{a\in z,b\in z^{\prime}}x_{a\circ
b}\leq\bigvee_{a\in z,b\in z^{\prime}}x_{a\wedge b}=\bigvee_{a\in z,b\in
z^{\prime}}(x_{a}\vee x_{b})=\left(\bigvee_{a\in
z}x_{a}\right)\vee\left(\bigvee_{b\in z^{\prime}}x_{b}\right)=z\vee
z^{\prime}$

In particular, $x\widehat{\circ}x\leq x\vee x=x$, i.e. $xR^{111}xx$ holds.
Hence the constraint (C4) holds in the canonical frame of BCW. ∎

######  Lemma 4.4 (Canonical SUB-Interpretation Lemma).

The canonical interpretation, assigning to a sentence $\varphi$ the formal
concept $(\mbox{$[\\![\varphi]\\!]$},\mbox{$(\\!|\varphi|\\!)$})$ with extent
$\mbox{$[\\![\varphi]\\!]$}=\\{x\in X\;|\;[\varphi]\in x\\}$ and intent
$\mbox{$(\\!|\varphi|\\!)$}=\\{y\in Y\;|\;[\varphi]\in y\\}$, where
$[\varphi]$ is the equivalence class of $\varphi$ under provability, satisfies
the recursive conditions of Table 1.

###### Proof.

The proof is by induction, the cases for $\top,\bot,\wedge,\vee$ are
straightforward and we turn to the cases for the residuated operators.

The canonical accessibility relation $R^{111}$ has been defined by setting,
for filters $x,u,v$, $xR^{111}uv$ iff $u\widehat{\circ}v\leq x$ (where we
consistently use $\leq$ for filter inclusion). Hence
$R^{111}uv=\\{x\;|\;u\widehat{\circ}v\leq x\\}=\Gamma(u\widehat{\circ}v)$ is a
Galois stable set, in fact a closed element of ${\mathcal{G}}(X)$. The
canonical Galois relation $\upVdash$ is increasing in each argument place from
which it follows that $yR^{\partial 11}uv$ iff $u\widehat{\circ}v\upVdash y$.
It needs to be verified, given the co-satisfaction clause for $\circ$, that
$y\in\mbox{$(\\!|\varphi\circ\psi|\\!)$}$ iff for any $u,v\in X$, if
$u\in\mbox{$[\\![\varphi]\\!]$}$ and $v\in\mbox{$[\\![\psi]\\!]$}$, then
$yR^{\partial 11}uv$. By definition of the canonical interpretation we have
$y\in\mbox{$(\\!|\varphi\circ\psi|\\!)$}$ iff $[\varphi\circ\psi]\in y$ iff
$[\varphi]\circ[\psi]\in y$. For lattice elements $a,b$, given monotonicity of
$\widehat{\circ}$ and increasingness of $\upVdash$ we obtain

$a\circ b\in y$ | iff |  $x_{a\circ b}\upVdash y$ | iff |  $x_{a}\widehat{\circ}x_{b}\upVdash y$ | iff | $\forall u,v\in X\;(x_{a}\leq u\;\wedge\;x_{b}\leq v\;\longrightarrow\;u\widehat{\circ}v\upVdash y)$
---|---|---|---|---|---|---
| iff |  $\forall u,v\in X\;(a\in u\;\wedge\;b\in v\;\longrightarrow\;yR^{\partial 11}uv)$

In particular, for $a=[\varphi],b=[\psi]$ the above yields precisely the co-
satisfaction clause for cotenability:
$y\Vdash^{\\!\\!\partial}\varphi\circ\psi\mbox{ iff }\forall u,v\in
X\;(u\Vdash\varphi\;\wedge\;v\Vdash\psi\;\longrightarrow\;yR^{\partial
11}uv)$.

For the satisfaction clause for implication, it suffices to show that
$a\mbox{$\rightarrow$}b\in z$ iff $\forall x\in X\;\forall y\in Y\;(a\in
x\;\wedge\;b\in y\;\longrightarrow\;yR^{\partial 11}zx)$.

Define first a point operator
$x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y$ as in [34], given a
filter $x$ and an ideal $y$, to be the ideal generated by all implications
$a\mbox{$\rightarrow$}b$ with $a\in x,b\in y$, i.e.
$x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y=\bigvee\\{y_{a\mbox{$\rightarrow$}b}\;|\;a\in
x,b\in y\\}$.

Note that, it follows from the results of [39] that for the particular case of
the normal lattice operator
$\circ:\mathcal{L}\times\mathcal{L}\longrightarrow\mathcal{L}$, of
distribution type $(1,1;1)$, the operator $\bigovert$ on ${\mathcal{G}}(X)$
defined by $A\bigovert C=\bigvee_{x\in A,z\in C}(\Gamma x\bigovert\Gamma
z)=\bigvee_{x\in A,z\in C}\Gamma(x\widehat{\circ}z)$ is its $\sigma$-extension
and that $A\bigovert
C=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond(A\bigodot C)$.

In [39] and more specifically in [35] we have also constructed the
$\sigma$-extension $\Rightarrow_{1}=\mbox{$\rightarrow$}^{\sigma}$ of the
lattice implication operator $\rightarrow$ in our canonical lattice frame.
This was done by first defining
$\Rightarrow_{0}:{\mathcal{G}}(X)\times{\mathcal{G}}(Y)\longrightarrow{\mathcal{G}}(Y)$
by $\Gamma x\Rightarrow_{0}\Gamma
y=\Gamma(x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y)$. This is a
monotone operator, completely distributing over arbitrary joins of closed
elements in each argument place, hence it is extended to all of
${\mathcal{G}}(X)\times{\mathcal{G}}(Y)$ by setting
$A\Rightarrow_{0}B=(\bigvee_{x\in A}\Gamma x)\Rightarrow_{0}(\bigvee_{y\in
B}\Gamma y)$ $=\bigvee_{x\in A,y\in B}(\Gamma x\Rightarrow_{0}\Gamma y)$. Then
$\Rightarrow_{1}:{\mathcal{G}}(X)\times{\mathcal{G}}(X)^{\partial}\longrightarrow{\mathcal{G}}(X)^{\partial}$
was defined in [35] by setting
$A\Rightarrow_{1}C={}\mbox{${}^{\upVdash}$}(A\Rightarrow_{0}C\mbox{${}^{\upVdash}$})$.
In particular, $\Gamma
x\Rightarrow_{1}{}\mbox{${}^{\upVdash}$}\\{y\\}={}\mbox{${}^{\upVdash}$}(\Gamma
x\Rightarrow_{0}\Gamma
y)={}\mbox{${}^{\upVdash}$}\\{x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y\\}$.

By results of [27], Proposition 6.6, it follows that residuation is preserved
by canonical extensions, hence for stable sets $A,C,F$ it holds that
$A\bigovert F\subseteq C$ iff $C\subseteq A\Rightarrow_{1}C$. In particular
then, $\Gamma x\bigovert\Gamma z\subseteq{}\mbox{${}^{\upVdash}$}\\{y\\}$ iff
$\Gamma z\subseteq\Gamma x\Rightarrow_{1}{}\mbox{${}^{\upVdash}$}\\{y\\}$.
This is equivalent, given the definitions of the stable set operators, to
$x\widehat{\circ}z\upVdash y$ iff $z\upVdash
x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y$. Given the definition of
$R^{\partial 11}$, we obtain

$yR^{\partial 11}xz\;\mbox{ iff }\;x\widehat{\circ}z\upVdash y\;\mbox{ iff
}\;z\upVdash x\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y$ (10)

Furthermore, using the above we obtain

$a\mbox{$\rightarrow$}b\in x$ | iff |  $x\upVdash y_{a\mbox{$\rightarrow$}b}$ iff $x\upVdash(x_{a}\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y_{b})$
---|---|---
| iff | $\forall z\in X\;\forall y\in Y\;(x_{a}\leq z\;\wedge\;y_{b}\leq y\;\longrightarrow\;x\upVdash(z\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y))$
| iff | $\forall z\in X\;\forall y\in Y\;(a\in z\;\wedge\;b\in y\;\longrightarrow\;x\upVdash(z\stackrel{{\scriptstyle\flat}}{{\longrightarrow}}y))$
| iff |  $\forall z\in X\;\forall y\in Y\;(a\in z\;\wedge\;b\in y\;\longrightarrow\;z\widehat{\circ}x\upVdash y)$ using (10)
| iff |  $\forall z\in X\;\forall y\in Y\;(a\in z\;\wedge\;b\in y\;\longrightarrow\;yR^{\partial 11}zx)$

By a completely symmetric argument and with
$y\stackrel{{\scriptstyle\flat}}{{\longleftarrow}}z$ defined as the join
$\bigvee\\{y_{a\circ b}\;|\;a\in z,b\in y\\}$ we similarly obtain that
$x\widehat{\circ}z\upVdash y$ iff $x\upVdash
y\stackrel{{\scriptstyle\flat}}{{\longleftarrow}}z$, from which it follows by
the same argument as above that $b\mbox{$\leftarrow$}a\in x$ iff $\forall z\in
x$ $\forall y\in Y\;(a\in z\;\wedge\;b\in y\;\longrightarrow\;yR^{\partial
11}xz)$ and this completes the proof of the canonical interpretation lemma. ∎

We may then conclude.

######  Theorem 4.5 (SUB Soundness and Completeness).

Each substructural logic SUB of Figure 1 is sound and complete in the
respective $\mathbb{SUB}$ frame-class. $\leftVdash$

For completeness of the modal companion logics, recall that to show that if
$\alpha$ (resp. $\beta$) is logically valid, i.e. $\models\alpha$ (resp.
$\models\beta$), then $\alpha$ is a theorem, i.e. $\vdash\alpha$ (resp.
$\mbox{$\medvert\\!\\!\\!\\!\sim$}\beta$), one proceeds contrapositively
arguing that for every non-theorem $\alpha$ (resp. $\beta$) a model can be
found such that $\alpha$ (resp. $\beta$) is not valid in that model. The well
established completeness argument proceeds by demonstrating that there is in
fact a single model that invalidates all non-theorems of the logic, the so-
called canonical model
$\mathfrak{M}_{c}=(\mathfrak{F}_{c},\mbox{$[\\![\;]\\!]$}_{c})$ of the logic,
where $\mathfrak{F}_{c}=(W,\upVdash_{w},W^{\prime})$ is the canonical (sorted,
in our case) frame and $\mbox{$[\\![\zeta]\\!]$}_{c}=\\{w\in W\;|\;[\zeta]\in
w\\}$, while
$\mbox{$(\\!|\eta|\\!)$}=\largesquare(W\setminus\mbox{$[\\![\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\neg\eta]\\!]$}_{c})$ and where $[\zeta]$ is the equivalence class, under
provability, of $\zeta$.

Algebraically, the canonical frame construction is a realization of a
canonical extension of the Lindenbaum-Tarski algebra of the logic. The
standard (ultrafilter) canonical frame of a modal companion logic sub.ML2 is
constructed from ultrafilters, as detailed for ML2. The canonical
accessibility relation $R^{111}$ is defined on utrafilters by the condition
$xR^{111}zz^{\prime}$ iff for all $a\in z$ and $a^{\prime}\in z^{\prime}$ we
have $a\circ a^{\prime}\in x$. We will however have use, for proof purposes,
of an alternative canonical extension which regards the Boolean algebra merely
as a lattice. By the results of Section 2.3 the two canonical extension
constructions are isomorphic, a fact that we use in the proofs of the
canonical frame and interpretation lemmas.

######  Lemma 4.6 (Canonical sub.ML2-Frame Lemma).

The canonical frame of sub.ML2 is a $\mathbb{SUB}$-frame.

###### Proof.

There is nothing to prove for the system nfl.ML2 (the canonical relation
$R^{111}$ generates residuated operators as detailed in Section 3.1) and we
discuss each other system separately.

#### fl.ML2

This case (associativity relational constraint) has been identified as a non-
elementary case and resolved by logicians working on Relevance Logic [1, 2]
and we could simply refer to the related results (see, for example, a detailed
proof in [18]). However, a simple solution can be now given using the notion
of a canonical extension and related results and we report it below. Note
first that, algebraically, the canonical frame is a realization of the
construction of a canonical extension of the Lindenbaum-Tarski algebra of the
logic (a residuated Boolean algebra, considering only the first sort, where
the associative operation $\circ$ is defined). For distributive lattices the
extension is based on the set of prime filters (as is the case for relevance
logic) and for the Boolean case ultrafilters are considered, as it is well
known. For arbitrary lattices all filters are used [40]. We already mentioned
(and proved) in Section 4.2 that the associativity equation $a\circ(b\circ
c)=(a\circ b)\circ c$ is canonical (it is preserved by canonical extensions).
Furthermore, the set operator (on sets of ultrafilters) defined by

$U_{1}\mbox{$\bigodot$}U_{2}=\\{u\in\mbox{\rm Ult}(\mathcal{A})\;|\;\exists
u_{1},u_{2}\in\mbox{\rm Ult}(\mathcal{A})\;(u_{1}\in U_{1}\;\wedge\;u_{2}\in
U_{2}\;\wedge\;uRu_{1}u_{2})\\}$

is the $\sigma$-extension of $\circ$ (by the results of Jónsson and Tarski on
Boolean algebras with operators [42, 43]), hence associative, where the
canonical accessibility relation $R$ is defined (as for relevance logic) by

$uRu_{1}u_{2}\;\mbox{ iff }\;\forall a,b\;(a\in u_{1}\;\wedge\;b\in
u_{2}\;\longrightarrow\;a\circ b\in u)$

It is furthermore elementary to see that the associativity relational
constraint (C1) is equivalent to the identity
$\\{u\\}\bigodot(\\{v\\}\bigodot\\{w\\})=(\\{u\\}\bigodot\\{v\\})\bigodot\\{w\\}$,
for any $u,v,w\in\mbox{\rm Ult}(\mathcal{A})$. Hence (C1) holds in the
canonical fl.ML2 frame.

#### bci.ML2

Straightforward, since assuming $xR^{111}zz^{\prime}$, if $a\in z,b\in
z^{\prime}$, then $a\circ b\in x$, hence since commutativity is assumed in
this case we also get $b\circ a\in x$ from which $xR^{111}z^{\prime}z$
follows, by definition of the relation.

#### bck.ML2

Let $x,z,z^{\prime}$ be ultrafilters such that $xR^{111}zz^{\prime}$ holds.
Fix $a\in z$, arbitrary. For any $b\in z^{\prime}$, $a\circ b\in x$ and since
$a\circ b\leq b$ holds in the Lindenbaum-Traksi algebra of the logic and $x$
is a filter, we obtain that $b\in x$. It follows that $z^{\prime}\subseteq x$,
which implies that $z^{\prime}=x$, since they are both maximal filters. Since
$\preceq$ is a preorder, hence reflexive, it follows from $x\preceq x$ that
$z^{\prime}\preceq x$. Hence the relational constraint (C3) holds in the
canonical frame.

#### bcw.ML2

The case is straightforward since, given any ultrafilter $x$, for any lattice
elements $a,b$, if both $a,b\in x$, then $a\wedge b\in x$ and since
contraction is assumed in bcw.ML2 we get $a\circ b\in x$ from $a\wedge b\leq
a\circ b$. Hence (C4) holds in the canonical frame. ∎

######  Lemma 4.7 (Canonical sub.ML2-Interpretation Lemma).

The canonical interpretation of sub.ML2 satisfies the recursive clauses of
Table 3.

###### Proof.

For each sort of sentences, the canonical interpretation
$\mbox{$[\\![\;]\\!]$}_{c},\mbox{$(\\!|\;|\\!)$}_{c}$ assigns to a sentence
the set of respective ultrafilters containing its equivalence class, as usual.
The proof is by induction and we skip the familiar cases corresponding to the
Boolean operators $\neg,\wedge$ (for each sort). For the needs of the proof we
let $a=[\alpha]$, primed or with subscripts, and $b=[\beta]$, again possibly
with subscripts or primed.

#### Case
$\largesquare\alpha,\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\beta$

Both cases are immediate by the way the canonical frame relation $I$ is
defined.

#### Case $\odot$

The current proof obligation is known in the relevance logic literature and it
has been handled by Routley and Meyer [61] (see also [2, 18]) with a
maximalization argument using Zorn’s lemma (delivering prime filters, which
are maximal filters in our Boolean algebra case) and we could simply direct
the reader to that proof argument. Instead, we provide a proof that makes use
of the uniqueness, up to isomorphism, of canonical extensions of lattice
expansions, see Lemma 2.3.

Recall from the results of Jónsson and Tarski [42, 43] that the additive,
binary operator $\circ$ on the Boolean algebra $\mathcal{A}$ is represented
(in the ultrafilter canonical extension) relationally as the operator

$U\medcircle U^{\prime}=\\{u\in\mbox{\rm Ult}(\mathcal{A})\;|\;\exists
w,w^{\prime}\in\mbox{\rm Ult}(\mathcal{A})\;(uRww^{\prime}\wedge w\in U\wedge
w^{\prime}\in U^{\prime})\\}$

where $R$ is defined by

$uRww^{\prime}\;\mbox{ iff }\;\forall a,a^{\prime}\in\mathcal{A}\;(a\in
w\;\wedge\;a^{\prime}\in w^{\prime}\;\longrightarrow\;a\circ a^{\prime}\in u)$

Furthermore, $\medcircle=\circ^{\sigma}_{u}$ is the $\sigma$-extension (in the
terminology of [27]) of the cotenability operator $\circ$ and it is a
completely additive operator, i.e.
$U\circ^{\sigma}_{u}U^{\prime}=\bigcup_{w\in U,w^{\prime}\in
U^{\prime}}\\{w\\}\circ^{\sigma}_{u}\\{w^{\prime}\\}$. Note also that
$uRww^{\prime}$ iff $u\in\\{w\\}\circ^{\sigma}_{u}\\{w^{\prime}\\}$.

Now regard the Boolean algebra merely as a lattice and take its canonical
extension as the complete lattice of Galois stable sets ${\mathcal{G}}(X)$,
where $X=\mbox{\rm Filt}(\mathcal{A})$. Let $X\supseteq X^{u}=\mbox{\rm
Ult}(\mathcal{A})$. As shown in Section 2.3, the isomorphism (by uniqueness of
canonical extensions of lattices) between ${\mathcal{G}}(X)$ and
$\powerset(X^{u})$ sends a stable set $A\in{\mathcal{G}}(X)$ to $A^{u}=A\cap
X^{u}$. The cotenability operator $\circ$ is now represented as an operator on
Galois stable sets as in the proof of Lemma 4.3, by first defining a point
operator $\widehat{\circ}$ (on filters), setting
$z\widehat{\circ}z^{\prime}=\bigvee\\{x_{a\circ a^{\prime}}\;|\;a\in
z,a^{\prime}\in z^{\prime}\\}$, then defining $R^{111}\subseteq X^{3}$ by
$xR^{111}zz^{\prime}$ iff $z\widehat{\circ}z^{\prime}\leq x$, which is
equivalent to the definition $xR^{111}zz^{\prime}$ iff $\forall
a,a^{\prime}\in\mathcal{A}\;(a\in z\;\wedge\;a^{\prime}\in
z^{\prime}\;\longrightarrow\;a\circ a^{\prime}\in x)$. Note that the
restriction $R=R^{111}\cap(X^{u})^{3}$ on the set of ultrafilters is precisely
the canonical accessibility relation $R$ in the standard canonical
(ultrafilter) extension of the Boolean algebra with an additive operator
$\circ$. By the analysis in Section 2.3, $\eta(\Gamma x\circ^{\sigma}\Gamma
z)=\eta(\Gamma(x\widehat{\circ}z))=\\{u\in X^{u}\;|\;x\widehat{\circ}z\leq
u\\}$ which is precisely the set $\\{u\in X^{u}\;|\;uR^{111}xz\\}$. By Lemma
2.3, $\eta(\Gamma x\circ^{\sigma}\Gamma z)=\eta(\Gamma
x)\circ^{\sigma}_{u}\eta(\Gamma
z)=(\Gamma^{u}x)\circ^{\sigma}_{u}(\Gamma^{u}z)$, using the notation
introduced in the above mentioned lemma. By complete additivity of
$\circ^{\sigma}_{u}$ the latter is the union $\bigcup_{x\leq w,z\leq
w^{\prime}}(\\{w\\}\circ^{\sigma}_{u}\\{w^{\prime}\\})$. Hence we have
obtained that, for an ultrafilter $u$ and any filters $x,z$,

$uR^{111}xz$ | iff | $\exists w,w^{\prime}\in X^{u}\;(x\leq w\;\wedge\;z\leq w^{\prime}\;\wedge\;u\in(\\{w\\}\circ^{\sigma}_{u}\\{w^{\prime}\\})$
---|---|---
| iff |  $\exists w,w^{\prime}\in X^{u}\;(x\leq w\;\wedge\;z\leq w^{\prime}\;\wedge\;uRww^{\prime})$

In particular, given elements $a,a^{\prime}$ of the Boolean algebra,

$uR^{111}x_{a}x_{a^{\prime}}\;\mbox{ iff }\;\exists w,w^{\prime}\in
X^{u}\;(a\in w\;\wedge\;a^{\prime}\in w^{\prime}\;\wedge\;uRww^{\prime})$ (11)

Now let $a=[\alpha],a^{\prime}=[\alpha^{\prime}]$ be the respective
equivalence classes of $\alpha,\alpha^{\prime}$. The canonical interpretation
$\mbox{$[\\![\alpha\odot\alpha^{\prime}]\\!]$}_{c}$ is the representation of
the equivalence class
$[\alpha\odot\alpha^{\prime}]=[\alpha]\circ[\alpha^{\prime}]$, i.e.
$\mbox{$[\\![\alpha\odot\alpha^{\prime}]\\!]$}_{c}=h(a\circ a^{\prime})$,
where $h$ is the Stone representation map $h(e)=\\{u\in X^{u}=\mbox{\rm
Ult}(\mathcal{A})\;|\;e\in u\\}$. Assume for an ultrafilter $u$ that
$u\in\mbox{$[\\![\alpha\odot\alpha^{\prime}]\\!]$}_{c}$, so that $a\circ
a^{\prime}\in u$. It needs to be shown that there exist ultrfilters
$w,w^{\prime}$ such that $a\in w,a^{\prime}\in w^{\prime}$ and
$uRww^{\prime}$. But $a\in x_{a},a^{\prime}\in x_{a^{\prime}}$ and if $a\circ
a^{\prime}\in u$, then $x_{a}\widehat{\circ}x_{a^{\prime}}=x_{a\circ
a^{\prime}}\leq u$, i.e. $uR^{111}x_{a}x_{a^{\prime}}$ holds. This is
equivalent, by (11), to the assertion that ultrafilters $w,w^{\prime}$ exist
with $a\in w,a^{\prime}\in w^{\prime}$ and where $uRww^{\prime}$. This shows
that for an ultrafilter $u$,

$a\circ a^{\prime}\in u\;\mbox{ iff }\;\exists w,w^{\prime}\in X^{u}\;(a\in
w\;\wedge\;a^{\prime}\in w^{\prime}\;\wedge\;uRww^{\prime})$

hence the canonical interpretation conforms to the relevant clause in the
definition of the satisfaction relation of Table 3.

#### Case $\rightfilledspoon$, $\leftfilledspoon$

The cases of $\leftfilledspoon,\rightfilledspoon$ follow from the case for
$\odot$, given Lemma 3.1 and hence the proof is complete. ∎

Hence we may conclude

######  Theorem 4.8 (Completeness for sub.ML2).

Each modal companion logic sub.ML2 is (sound, by Theorem 3.4) and complete in
the respective $\mathbb{SUB}$ frame-class. $\leftVdash$

By Theorem 4.1 and by the soundness and completeness results proven above for
each substructural logic SUB and its companion modal logic sub.ML2, we obtain
that

######  Corollary 4.9.

$\varphi\vdash\psi$ in SUB iff $\varphi^{\bullet}\vdash\psi^{\bullet}$ iff
$\psi^{\circ}\mbox{$\medvert\\!\\!\\!\\!\sim$}\varphi^{\circ}$ in sub.ML2.
$\leftVdash$

##  5 Translation into Sorted First-Order Logic

Assume $V_{x},V_{y}$ are countable, non-empty and disjoint sets and let

${\mathcal{L}}^{1}(V_{x},V_{y},{\bf P}^{x}_{i},{\bf Q}^{y}_{i},{\bf
I}^{xy},{\bf R}^{xxx},=_{x},=_{y})$

be the two-sorted, first-order language with equality whose sorted variables
are in $V_{x}$ (ranged over by $x,z$ etc),$V_{y}$ (ranged over by $y,v$ etc)
and it includes sorted quantifiers $\forall^{x},\forall^{y}$, a binary
predicate Ixy, unary predicates P${}^{x}_{i}$, Q${}^{y}_{i}$ (where sorting is
indicated by the superscript) corresponding to the propositional variables of
sub.ML2 and a three-place predicate ${\bf R}^{xxx}$. Superscripts indicating
sorting type will be dropped in the sequel, for simplicity of notation. A two-
sorted first-order structure for ${\mathcal{L}}^{1}$ is a structure $\langle
X,Y,{\bf I}^{I},{\bf P}^{I}_{i},{\bf Q}^{I}_{i},{\bf R}^{I})$ where $X,Y$ are
disjoint sets and ${\bf P}^{I}_{i}\subseteq X$, ${\bf R}^{I}\subseteq X^{3}$,
${\bf Q}^{I}_{i}\subseteq Y$, for each $i$, and ${\bf I}^{I}\subseteq X\times
Y$, while $=^{I}_{x},=^{I}_{y}$ are the identity relations for each sort.

The standard translation of sub.ML2 into FOL (First-Order Logic) is exactly as
in the single-sorted case, except for the relativization to two sorts,
displayed in Table 6.

Table 6: Standard Translation of sub.ML2 into 2-Sorted FOL ST${}_{x}(P_{i})$ | = |  ${\bf P}_{i}(x)$
---|---|---
ST${}_{x}(\neg\alpha)$ | = |  $\neg\mbox{ST${}_{x}(\alpha)$}$
ST${}_{x}(\alpha\wedge\alpha^{\prime})$ | = |  $\mbox{ST${}_{x}(\alpha)$}\wedge\mbox{ST${}_{x}(\alpha^{\prime})$}$
ST${}_{x}(\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta)$ | = |  $\forall y\;({\bf I}(x,y)\;\longrightarrow\;\mbox{ST${}_{y}(\beta)$})$
ST${}_{x}(\alpha\odot\alpha^{\prime})$ | = | $\exists z,z^{\prime}\;({\bf R}(x,z,z^{\prime})\;\wedge\;\mbox{ST${}_{z}(\alpha)$}\;\wedge\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}_{x}(\alpha\rightfilledspoon\alpha^{\prime})$ | = | $\forall z,z^{\prime}\;(\mbox{ST${}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},z,x)\;\longrightarrow\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}_{x}(\alpha^{\prime}\leftfilledspoon\alpha)$ | = |  $\forall z,z^{\prime}\;(\mbox{ST${}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},x,z)\;\longrightarrow\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}_{y}(Q_{i})$ | = | ${\bf Q}_{i}(y)$
ST${}_{y}(\neg\beta)$ | = | $\neg\mbox{ST${}_{y}(\beta)$}$
ST${}_{y}(\beta\wedge\beta^{\prime})$ | = | $\mbox{ST${}_{y}(\beta)$}\wedge\mbox{ST${}_{y}(\beta^{\prime})$}$
ST${}_{y}(\largesquare\alpha)$ | = |  $\forall x\;({\bf I}(x,y)\;\longrightarrow\;\mbox{ST${}_{x}(\alpha)$})$

Note that a sub.ML2-model $\mathfrak{M}=((X,I,Y,R^{111}),V)$ is also an
${\mathcal{L}}^{1}$-structure, setting ${\bf I}^{I}=I,{\bf R}^{I}=R^{111},{\bf
P}^{I}_{i}=V(P_{i}),{\bf Q}^{I}_{i}=V(Q_{i})$, so that the following is
immediate.

######  Proposition 5.1.

For any sub.ML2 formulae $\alpha,\beta$ (of sort 1, 2, respectively),
sub.ML2-model $\mathfrak{M}=((X,I,Y,R^{111}),V)$ and $x\in X,y\in Y$,
$x\models_{\mathfrak{M}}\alpha$ iff
$\mathfrak{M}\models\mbox{ST${}_{z}(\alpha)$}[z:=x]$ and
$y\models_{\mathfrak{M}}\beta$ iff
$\mathfrak{M}\models\mbox{ST${}_{v}(\beta)$}[v:=y]$. $\leftVdash$

Composing with the translation and co-translation of SUB into sub.ML2,
respective translations of SUB into ${\mathcal{L}}^{1}$ are obtained,
displayed in Table 7.

Table 7: Standard (2-Sorted) First-Order Translation and Co-Translation of SUB ST${}^{\bullet}_{x}(p_{i})$ | = | $\forall y\;({\bf I}(x,y)\longrightarrow\;\exists z\;({\bf I}(z,y)\;\wedge\;{\bf P}_{i}(z)))$
---|---|---
ST${}^{\circ}_{y}(p_{i})$ | = | $\forall x\;({\bf I}(x,y)\;\longrightarrow\;\neg{\bf P}_{i}(x))$
ST${}^{\bullet}_{x}(\top)$ | = | $x=x$
ST${}^{\circ}_{y}(\top)$ | = | $\forall x\;({\bf I}(x,y)\;\longrightarrow\;x\neq x)$
ST${}^{\bullet}_{x}(\bot)$ | = | $\forall y\;({\bf I}(x,y)\;\longrightarrow\;y\neq y)$
ST${}^{\circ}_{y}(\bot)$ | = | $y=y$
ST${}^{\bullet}_{x}(\varphi\wedge\psi)$ | = | $\mbox{ST${}^{\bullet}_{x}(\varphi)$}\wedge\mbox{ST${}^{\bullet}_{x}(\psi)$}$
ST${}^{\circ}_{y}(\varphi\wedge\psi)$ | = | $\forall x\;({\bf I}(x,y)\;\longrightarrow\;\exists v\;({\bf I}(x,v)\;\wedge\;(\mbox{ST${}^{\circ}_{v}(\varphi)$}\vee\mbox{ST${}^{\circ}_{v}(\psi)$})))$
ST${}^{\bullet}_{x}(\varphi\vee\psi)$ | = |  $\forall y\;({\bf I}(x,y)\;\longrightarrow\;\exists z\;({\bf I}(z,y)\;\wedge\;(\mbox{ST${}^{\bullet}_{z}(\varphi)$}\vee\mbox{ST${}^{\bullet}_{z}(\psi)$})))$
ST${}^{\circ}_{y}(\varphi\vee\psi)$ | = |  $\mbox{ST${}^{\circ}_{y}(\varphi)$}\wedge\mbox{ST${}^{\circ}_{y}(\psi)$}$
ST${}^{\bullet}_{x}(\varphi\mbox{$\rightarrow$}\psi)$ | = | $\forall z,z^{\prime}\;(\mbox{ST${}^{\bullet}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},z,x)\;\longrightarrow\;\mbox{ST${}^{\bullet}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}^{\circ}_{y}(\varphi\mbox{$\rightarrow$}\psi)$ | = |  $\forall x\;({\bf I}(x,y)\longrightarrow\neg\mbox{ST${}^{\bullet}_{x}(\varphi\mbox{$\rightarrow$}\psi)$})$
ST${}^{\bullet}_{x}(\varphi\circ\psi)$ | = | $\forall y\;({\bf I}(x,y)\;\longrightarrow\;\exists x^{\prime}\;({\bf I}(x^{\prime},y)\;\wedge\;\exists z,z^{\prime}\;({\bf R}(x^{\prime},z,z^{\prime})\;\wedge$
|  |  $\wedge\;\mbox{ST${}^{\bullet}_{z}(\alpha)$}\;\wedge\;\mbox{ST${}^{\bullet}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}^{\circ}_{y}(\varphi\circ\psi)$ | = |  $\forall x\;({\bf I}(x,y)\longrightarrow\neg\exists z,z^{\prime}({\bf R}(x,z,z^{\prime})\wedge\mbox{ST${}^{\bullet}_{z}(\varphi)$}\wedge\mbox{ST${}^{\bullet}_{z^{\prime}}(\psi)$}))$
ST${}^{\bullet}_{x}(\psi\mbox{$\leftarrow$}\varphi)$ | = |  $\forall z,z^{\prime}\;(\mbox{ST${}^{\bullet}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},x,z)\;\longrightarrow\;\mbox{ST${}^{\bullet}_{z^{\prime}}(\alpha^{\prime})$})$
ST${}^{\circ}_{y}(\psi\mbox{$\leftarrow$}\varphi)$ | = |  $\forall x\;({\bf I}(x,y)\longrightarrow\neg\mbox{ST${}^{\bullet}_{x}(\psi\mbox{$\leftarrow$}\varphi)$})$

######  Corollary 5.2.

For any SUB-sentences $\varphi,\psi$, any sub.ML2-model
(${\mathcal{L}}^{1}$-structure) $\mathfrak{M}=((X,I,Y,R^{111}),V)$ and
corresponding SUB-model $\mathfrak{N}$, any $x\in X,y\in Y$,

  1. 1.

$x\Vdash_{\mathfrak{N}}\varphi$ iff $x\models_{\mathfrak{M}}\varphi^{\bullet}$
iff $\mathfrak{M}\models\mbox{ST${}^{\bullet}_{z}(\varphi)$}[z:=x]$

  2. 2.

$\varphi\Vdash_{\mathfrak{N}}\psi$ iff
$\varphi^{\bullet}\models_{\mathfrak{M}}\psi^{\bullet}$ iff for any $x\in X$,
if $\mathfrak{M}\models\mbox{ST${}^{\bullet}_{z}(\varphi)$}[z:=x]$, then
$\mathfrak{M}\models\mbox{ST${}^{\bullet}_{z}(\psi)$}[z:=x]$

  3. 3.

$\Vdash_{\mathfrak{N}}\varphi$ iff $\models_{\mathfrak{M}}\varphi^{\bullet}$
iff $\mathfrak{M}\models\forall x\;\mbox{ST${}^{\bullet}_{x}(\varphi)$}$

  4. 4.

$\mathfrak{M}\models\mbox{ST${}^{\bullet}_{z}(\varphi)$}[z:=x]$ iff
$\mathfrak{M}\models(\forall y\;({\bf I}(z,y)\;\longrightarrow\;\exists
z^{\prime}\;({\bf I}(z^{\prime},y)\;\wedge$
$\wedge\;\mbox{ST${}^{\bullet}_{z^{\prime}}(\varphi)$})[z:=x]$
and similarly for ST${}^{\circ}_{v}(\varphi)$. $\leftVdash$

Compactness and the Löwenheim-Skolem properties for any substructural logic
SUB follow immediately from the reduction presented in this article.

######  Theorem 5.3.

The following hold.

  1. 1.

(Compactness) A set of SUB-sentences has a model iff every finite subset of it
has a model

  2. 2.

(Upward Löwenheim-Skolem) If a set of SUB-sentences has a countable model,
then it has a model of cardinality $\kappa$, for any $\kappa>\aleph_{0}$

  3. 3.

(Downward Löwenheim-Skolem) If a set of SUB-sentences has an infinite model,
then it has a model of cardinality $\aleph_{0}$

###### Proof.

If $\Gamma$ is a set of SUB-sentences and $\mathfrak{M}=((X,R,Y,R^{111}),V)$
is a SUB-model of $\Gamma$, then clearly every finite subset of $\Gamma$ has a
model, to wit $\mathfrak{M}$. For the converse, if every finite subset $F$ of
a set $\Gamma$ of SUB-sentences has a model $\mathfrak{M}_{F}$, then every
finite subset of $\Gamma^{\bullet}$ thereby has a model (the same model
$\mathfrak{M}_{F}$), hence $\Gamma^{\bullet}$ has a model
$\mathfrak{M}=(\mathfrak{F},\imath)$ by compactness of sorted FOL (cf [19])
and then $\mathfrak{N}$, on the same frame $\mathfrak{F}$ and with
interpretation $V$ defined by
$V(p_{i})=\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip
1.0pt\largediamond\imath(P_{i})$, is a model of $\Gamma$.

The Löwenheim-Skolem properties follow by the same back and forth argument
from SUB-models to first-order structures, using Corollary 5.2 and the
Löwenheim-Skolem theorem for sorted first-order logic. ∎

##  6 Sort Reduction and Decidability

Decidability can be deduced from the finite model property (FMP) of the two-
variable fragment of FOL, yet to the best of this author’s knowledge the FMP
property has only been proven for unsorted FOL, hence sort-reduction needs to
be performed (cf Enderton [19]), extending ${\mathcal{L}}^{1}$ with two unary
predicates ${\bf T}_{1},{\bf T}_{2}$, redefining first-order structures for
${\mathcal{L}}^{1}$ so that ${\bf T}^{I}_{1}=X,{\bf T}^{I}_{2}=Y$ and
relativising the translation of Table 6

$\mbox{ST}^{\prime}_{x}(P_{i})$ | = |  ${\bf T}_{1}(x)\wedge{\bf P}_{i}(x)$
---|---|---
$\mbox{ST}^{\prime}_{y}(Q_{i})$ | = |  ${\bf T}_{2}(y)\wedge{\bf Q}_{i}(y)$
$\mbox{ST}^{\prime}_{x}(\raisebox{-1.2pt}[0.0pt][0.0pt]{{\color[rgb]{0,0,0}\rule{7.68236pt}{7.68236pt}}}\hskip 1.0pt\beta)$ | = | $\forall y\;({\bf T}_{2}(y)\;\longrightarrow\;({\bf I}(x,y)\longrightarrow\mbox{ST}^{\prime}_{y}(\beta)))$
$\mbox{ST}^{\prime}_{y}(\largesquare\alpha)$ | = | $\forall x\;({\bf T}_{1}(x)\;\longrightarrow\;({\bf I}(x,y)\longrightarrow\mbox{ST}^{\prime}_{x}(\alpha)))$
$\mbox{ST}^{\prime}_{x}(\alpha\odot\alpha^{\prime})$ | = |  $\exists z,z^{\prime}\;({\bf T}_{1}(z)\wedge{\bf T}_{1}(z^{\prime})\wedge{\bf R}(x,z,z^{\prime})\;\wedge\;\mbox{ST${}_{z}(\alpha)$}\;\wedge\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$})$
$\mbox{ST}^{\prime}_{x}(\alpha\rightfilledspoon\alpha^{\prime})$ | = |  $\forall z,z^{\prime}\;({\bf T}_{1}(z)\wedge{\bf T}_{1}(z^{\prime})\longrightarrow(\mbox{ST${}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},z,x)\;\longrightarrow\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$}))$
$\mbox{ST}^{\prime}_{x}(\alpha^{\prime}\leftfilledspoon\alpha)$ | = |  $\forall z,z^{\prime}\;({\bf T}_{1}(z)\wedge{\bf T}_{1}(z^{\prime})\longrightarrow(\mbox{ST${}_{z}(\alpha)$}\;\wedge\;{\bf R}(z^{\prime},x,z)\;\longrightarrow\;\mbox{ST${}_{z^{\prime}}(\alpha^{\prime})$}))$

with the obvious clauses for negation and conjunction. For a two-sorted first-
order model $\mathfrak{M}$, let $\mathfrak{M}^{\prime}$ be its corresponding
single-sorted model, whose universe is the union of the universes of each sort
of $\mathfrak{M}$. The translation by sort reduction is known to be full and
faithful (cf Enderton [19]).

######  Theorem 6.1 (Decidability and Complexity).

A substructural logic SUB has the finite model property and its satisfiability
problem is decidable in nondeterministic exponential time.