1–LABEL:LastPageJun. 12, 2017Jan. 23, 2018

A precursor to this paper, reporting preliminary results, appeared in the
proceedings of AiML 2016 [12].

# A Real-Valued Modal Logic

Denisa Diaconescua  ,  George Metcalfeb  and  Laura Schnürigerc  aFaculty of
Mathematics and Computer Science, University of Bucharest, Romania
<EMAIL_ADDRESS>b,cMathematical Institute, University of Bern,
Switzerland<EMAIL_ADDRESS>
###### Abstract.

A many-valued modal logic is introduced that combines the usual Kripke frame
semantics of the modal logic K with connectives interpreted locally at worlds
by lattice and group operations over the real numbers. A labelled tableau
system is provided and a coNEXPTIME upper bound obtained for checking validity
in the logic. Focussing on the modal-multiplicative fragment, the labelled
tableau system is then used to establish completeness for a sequent calculus
that admits cut-elimination and an axiom system that extends the
multiplicative fragment of Abelian logic.

###### Key words and phrases:

Many-Valued Logic, Modal Logic, Abelian Logic, Łukasiewicz Logic, Proof
Theory, Tableau Calculus, Sequent Calculus

###### 1991 Mathematics Subject Classification:

F.4.1, I.2.3

The research of the first author was supported by Sciex grant 13.192 and
Romanian National Authority for Scientific Research and Innovation grant,
CNCS-UEFISCDI, project number PN-II-RU-TE-2014-4-0730.

The second and third authors acknowledge support from Swiss National Science
Foundation grant 200021_146748 and the EU Horizon 2020 research and innovation
programme under the Marie Skłodowska-Curie grant agreement No 689176.

##  1\. Introduction

Many-valued modal logics combine the frame semantics of classical modal logics
with a many-valued semantics at each world. As in the classical case, they may
be understood as a compromise between the good computational properties
(decidability and lower complexity) of propositional logics and the
expressivity of their first-order counterparts, some of which are not even
recursively axiomatizable. Such logics have been used to model modal notions
such as necessity, belief, and spatio-temporal relations in the presence of
multiple degrees of truth, certainty, and possibility, and span fuzzy belief
[19, 15], fuzzy similarity measures [16], many-valued tense logics [20, 11],
and spatial reasoning with vague predicates [33]. They also provide a basis
for studying fuzzy description logics, which, analogously to the classical
case, may be understood as many-valued multi-modal logics (see, e.g., [34, 18,
23, 1]).

Uniform approaches to many-valued modal logics defined over algebras with a
complete lattice reduct are described in [5, 32], extending previous work on
modal logics based on finite Heyting algebras [13, 14]. In an infinite-valued
setting, two core families emerge: “order-based” modal logics, including modal
extensions of Gödel logics [7, 28, 8, 6], where only the order type of the
truth values matters, and “continuous” modal logics, such as those based on
Łukasiewicz logic [17, 5, 21, 25, 26, 3], where propositional connectives are
interpreted by continuous functions over sets of real numbers (see also [24,
23, 27] for related systems). Such logics are easy to define semantically —
just decide on a suitable set of values and operations — but not so easy to
study. For example, an axiomatization for the Gödel modal logic over many-
valued frames is provided in [8], but no axiomatization is yet known for the
Gödel modal logic over standard (Boolean-valued or “crisp”) frames. Moreover,
decidability and complexity problems for these and other order-based modal
logics, which typically lack the finite model property, have been solved only
recently (see [6]).

In this paper we focus on continuous modal logics. Axiomatizations for finite-
valued Łukasiewicz modal logics have been provided in [21], but the axiom
system presented for the infinite-valued Łukasiewicz modal logic
${\mathrm{K(\mathrmL)}}$ includes a rule with infinitely many premises.
Similarly, only an approximate completeness result (corresponding to including
an infinitary rule) is established for the closely related continuous
propositional modal logic considered in [3]. Studying logics that lack a
finitary axiom system, and therefore also a suitable algebraic semantics, may
be difficult, as may be seen by considering classical modal logic deprived of
the theory of Boolean algebras with operators. Note also that, although
validity in finite-valued Łukasiewicz modal logics is PSPACE-complete [4],
only a coNEXPTIME upper bound is known for the infinite-valued case, as may be
deduced from complexity results for Łukasiewicz description logics (see [23]).

We address some of these issues here by defining and investigating a many-
valued modal logic ${\mathrm{K(A)}}$ with propositional connectives
interpreted as the usual lattice and group operations over the real numbers.
According to this semantics, the logic may be viewed as a minimal modal
extension of Abelian logic, the logic of lattice-ordered abelian groups,
introduced independently by Meyer and Slaney as a relevant logic [31] and
Casari as a comparative logic [9]. Some refinements to the usual definition of
many-valued modal logics (see, e.g., [5]) are needed to deal with the fact
that the real numbers do not form a complete lattice. However, since
${\mathrm{K(A)}}$ enjoys a finite model property, these non-standard features
can be safely ignored for practical purposes. Indeed, the logic
${\mathrm{K(A)}}$ provides a rather simple formalism for reasoning about state
transition systems where linear combinations of real-valued variables are
compared among worlds using modal operators. Since the connectives are
interpreted by common arithmetical operations $\min$, $\max$, $+$, and $-$,
further connectives interpreted by combinations of these operations (e.g., for
many-valued modal or description logics that reason about degrees of truth,
certainty, and possibility) can also be defined in this setting. In
particular, we show here that the Łukasiewicz modal logic
${\mathrm{K(\mathrmL)}}$ can be interpreted in the logic ${\mathrm{K(A)}}$
extended with a constant.

As our first main technical contribution, we present a sound and complete
labelled tableau calculus for ${\mathrm{K(A)}}$ and obtain a coNEXPTIME upper
bound for checking validity in this logic. The calculus is quite closely
related to a labelled tableau calculus for a Łukasiewicz description logic
presented in [23], and indeed provides the same upper bound for checking
validity. However, an important advantage of defining a logic over lattice-
ordered abelian groups is that we are able to explicitly identify and study
the modal-multiplicative fragment, solving problems for this fragment that
seem at the moment to be quite difficult for the full logic. In particular, we
show that the modal-multiplicative fragment of ${\mathrm{K(A)}}$ has an
EXPTIME upper bound for checking validity and provide a sequent calculus for
the fragment that admits cut-elimination. More significantly, we use the
labelled tableau calculus to establish the completeness of an axiom system
extending the multiplicative fragment of Abelian logic that, unlike other
known axiomatizations for continuous modal logics, contains only finitary
rules.

##  2\. A Modal Extension of Abelian Logic

In this section we define the real-valued modal logic ${\mathrm{K(A)}}$
semantically as a minimal modal extension of Abelian logic ${\mathrm{A}}$, the
logic of lattice-ordered abelian groups. We then show that validity in this
logic remains unchanged when the semantics is restricted to the class of
finite serial models. Finally, we provide a syntactic embedding of the minimal
modal extension ${\mathrm{K(\mathrmL)}}$ of infinite-valued Łukasiewicz logic
into ${\mathrm{K(A)}}$ with an additional constant.

Since we will consider several propositional languages in this paper, let us
begin with some quite general definitions. Given a propositional language
$\mathcal{L}$ (also known as an algebraic signature or type) consisting of
connectives with fixed arities, let ${\rm Fm}(\mathcal{L})$ denote the set of
$\mathcal{L}$-formulas $\varphi,\psi,\chi,\dots$, defined inductively in the
usual way over a countably infinite set ${\rm Var}$ of (propositional)
variables $p,q,r,\dots$. The complexity of $\varphi\in{\rm Fm}(\mathcal{L})$
is the number of occurrences of connectives in $\varphi$, and if $\mathcal{L}$
contains a unary operation $\Box$, then the modal depth of $\varphi$ is the
deepest nesting of the modal connective $\Box$ in $\varphi$.

###  2.1. Abelian Logic

Let us begin with a brief summary of Abelian logic ${\mathrm{A}}$, introduced
independently by Meyer and Slaney in [31] as a relevant logic, and Casari in
[9] as a comparative logic. In both settings, ${\mathrm{A}}$ was defined via
axiom systems that are complete with respect to validity in the variety of
lattice-ordered abelian groups. However, since this variety is generated by a
single algebra defined over the real numbers, we may also use this algebra to
introduce Abelian logic semantically as a many-valued logic.

Consider a language $\mathcal{L}_{\mathrm{A}}$ with binary connectives
$\land$, $\lor$, $\&$, and $\to$, and a constant $\overline{0}$, fixing also
$\lnot\varphi:=\varphi\to\overline{0}$. We define Abelian logic ${\mathrm{A}}$
via the logical matrix $\langle\mathbf{R},\mathbb{R}^{+}_{0}\rangle$
consisting of the algebra
$\mathbf{R}=\langle\mathbb{R},\min,\max,+,-,0\rangle$ and the set of
designated truth values $\mathbb{R}^{+}_{0}=\\{r\in\mathbb{R}:r\geq 0\\}$.
That is, an ${\mathrm{A}}$-valuation is a map $e\colon{\rm Var}\to\mathbb{R}$
extended to all $\mathcal{L}_{\mathrm{A}}$-formulas by

$\begin{array}[]{rcl}e(\varphi\land\psi)&=&\min(e(\varphi),e(\psi))\\\\[1.8063pt]
e(\varphi\lor\psi)&=&\max(e(\varphi),e(\psi))\\\\[1.8063pt]
e(\varphi\&\psi)&=&e(\varphi)+e(\psi)\\\\[1.8063pt]
e(\varphi\to\psi)&=&e(\psi)-e(\varphi)\\\\[1.8063pt]
e(\overline{0})&=&0,\end{array}$

and $\varphi\in{\rm Fm}(\mathcal{L}_{\mathrm{A}})$ is _${\mathrm{A}}$ -valid_
if $e(\varphi)\geq 0$ for each ${\mathrm{A}}$-valuation $e$.

$\begin{array}[t]{rl}{\rm(B)}&(\varphi\to\psi)\to((\psi\to\chi)\to(\varphi\to\chi))\\\
{\rm(C)}&(\varphi\to(\psi\to\chi))\to(\psi\to(\varphi\to\chi))\\\
{\rm(\,I\,)}&\varphi\to\varphi\\\
{\rm(A)}&((\varphi\to\psi)\to\psi)\to\varphi\\\
(\&1)&\varphi\to(\psi\to(\varphi\&\psi))\\\
(\&2)&(\varphi\to(\psi\to\chi))\to((\varphi\&\psi)\to\chi)\\\
(\overline{0}\,1)&\overline{0}\\\
(\overline{0}\,2)&\varphi\to(\overline{0}\to\varphi)\\\ (\land
1)&(\varphi\land\psi)\to\varphi\\\ (\land 2)&(\varphi\land\psi)\to\psi\\\
(\land
3)&((\varphi\to\psi)\land(\varphi\to\chi))\to(\varphi\to(\psi\land\chi))\\\
(\lor 1)&\varphi\to(\varphi\lor\psi)\\\ (\lor 2)&\psi\to(\varphi\lor\psi)\\\
(\lor 3)&((\varphi\to\chi)\land(\psi\to\chi))\to((\varphi\lor\psi)\to\chi)\\\
\end{array}$
$\psi\lx@proof@logical@and\varphi\varphi\to\psi\qquad\varphi\land\psi\lx@proof@logical@and\varphi\psi$
Figure 1. The Axiom System ${\mathrm{HA}}$

As mentioned above, $\mathbf{R}$ generates the variety of lattice-ordered
abelian groups. But also, using methods of abstract algebraic logic, it is
easily proved that this variety provides an algebraic semantics for the axiom
system ${\mathrm{HA}}$ displayed in Figure 1: an axiomatization of
multiplicative additive intuitionistic linear logic with just one constant
$\overline{0}$ extended with the axiom schema ${\rm(A)}\
((\varphi\to\psi)\to\psi)\to\varphi$. It follows then that $\varphi\in{\rm
Fm}(\mathcal{L}_{\mathrm{A}})$ is derivable in ${\mathrm{HA}}$ if and only if
$\varphi$ is ${\mathrm{A}}$-valid.

The choice of Abelian logic as the basis for the many-valued modal logics
studied in this paper is motivated both by its expressivity and the central
role of its semantics in ordinary mathematics. The connectives of
${\mathrm{A}}$ are interpreted by the basic arithmetical operations $\min$,
$\max$, $+$, $-$, and $0$, from which connectives for other many-valued
logics, interpreted via combinations of these operations, can be defined. In
particular, there exist syntactic embeddings of infinite-valued Łukasiewicz
logic into ${\mathrm{A}}$ that allow results for the latter to be transferred
to results about the former. The use of basic arithmetical operations on the
real numbers means also that a huge array of results and methods from linear
algebra are available for investigating ${\mathrm{A}}$ and its modal
expansions. For example, such methods have been used to obtain analytic
sequent and hypersequent calculi and co-NP completeness results for Abelian
logic and infinite-valued Łukasiewicz logic in [29] (see also [2, 30]).

###  2.2. Kripke Semantics

We define a minimal (crisp) modal extension ${\mathrm{K(A)}}$ of Abelian logic
by interpreting formulas locally in the algebra $\mathbf{R}$ over standard
Kripke frames. That is, a (crisp) frame is a pair $\mathfrak{F}=\langle
W,R\rangle$, where $W$ is a non-empty set of _worlds_ and $R\subseteq W\times
W$ is an (crisp) accessibility relation. As usual, we write $Rxy$ or $Rxy=1$
to denote $\langle x,y\rangle\in R$ and $Rxy=0$ to denote $\langle
x,y\rangle\not\in R$. For any $x\in W$, we let $R[x]=\\{y\in W:Rxy\\}$. Modal
formulas are defined over the language $\mathcal{L}_{{\mathrm{A}}}^{\Box}$
extending $\mathcal{L}_{\mathrm{A}}$ with an additional unary “box” connective
$\Box$, where the dual “diamond” connective is defined as
$\Diamond\varphi:=\lnot\Box\lnot\varphi$.

There exists a very general method for defining crisp modal logics over
algebras with a complete lattice reduct (see in particular [5]), where the
$\Box$ and $\Diamond$ connectives are interpreted as infima and suprema of
values of formulas at accessible worlds. However, since the real numbers do
not form a complete lattice — they lack a top and bottom element — we make
here a couple of minor adjustments to this method. First, we adopt the useful
convention that
$\bigwedge_{\mathbb{R}}\emptyset=\bigvee_{\mathbb{R}}\emptyset=0$, and second,
we restrict valuations of variables in a particular model to a fixed interval.
Both these choices will be justified to some extent by Lemma 1 below.

A _${\mathrm{K(A)}}$ -model_ $\mathfrak{M}=\langle W,R,V\rangle$ consists of a
frame $\langle W,R\rangle$ together with a valuation map $V\colon{\rm
Var}\times W\to[-r,r]$ for some $r\in\mathbb{R}^{+}_{0}$ that is extended to
$V\colon{\rm Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})\times W\to\mathbb{R}$ by

$\begin{array}[]{rcl}V(\varphi\land\psi,x)&=&\min(V(\varphi,x),V(\psi,x))\\\\[1.8063pt]
V(\varphi\lor\psi,x)&=&\max(V(\varphi,x),V(\psi,x))\\\\[1.8063pt]
V(\varphi\&\psi,x)&=&V(\varphi,x)+V(\psi,x)\\\\[1.8063pt]
V(\varphi\to\psi,x)&=&V(\psi,x)-V(\varphi,x)\\\\[1.8063pt]
V(\overline{0},x)&=&0\\\\[1.8063pt]
V(\Box\varphi,x)&=&\bigwedge_{\mathbb{R}}\\{V(\varphi,y):Rxy\\}.\end{array}$

By calculation, we obtain also

$\begin{array}[]{rcl}V(\lnot\varphi,x)&=&-V(\varphi,x)\\\\[1.8063pt]
V(\Diamond\varphi,x)&=&\bigvee_{\mathbb{R}}\\{V(\varphi,y):Rxy\\}.\end{array}$

An $\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula $\varphi$ is _valid_ in a
${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle W,R,V\rangle$ if
$V(\varphi,x)\geq 0$ for all $x\in W$. If $\varphi$ is valid in all
${\mathrm{K(A)}}$-models, then $\varphi$ is _${\mathrm{K(A)}}$ -valid_,
written $\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

The convention that
$\bigwedge_{\mathbb{R}}\emptyset=\bigvee_{\mathbb{R}}\emptyset=0$ is rather
counter-intuitive. This can be avoided, however, by restricting to serial
frames: that is, frames $\mathfrak{F}=\langle W,R\rangle$ such that for all
$x\in W$, there exists $y\in W$ such that $Rxy$. With this restriction,
$\bigwedge_{\mathbb{R}}\emptyset$ and $\bigvee_{\mathbb{R}}\emptyset$ may
simply be left undefined. Similarly, restricting the codomain of a valuation
to a bounded subset of $\mathbb{R}$ can be avoided by considering only finite
models. Surprisingly perhaps, considering only finite serial models does not
affect the valid formulas of the logic.

######  Lemma 1.

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$ if and only if $\varphi$ is
valid in all finite serial ${\mathrm{K(A)}}$-models.

######  Proof 2.1.

The left-to-right direction is immediate. For the opposite direction, we note
first that if $\varphi$ is not valid in a ${\mathrm{K(A)}}$-model
$\mathfrak{M}=\langle W,R,V\rangle$, then it will not be valid in the serial
${\mathrm{K(A)}}$-model $\mathfrak{M}^{\prime}=\langle W\cup W^{\prime},R\cup
R^{\prime},V^{\prime}\rangle$ where $W^{\prime}$ is a set of new distinct
worlds $x^{\prime}$ for each $x\in W$ satisfying $R[x]=\emptyset$,
$R^{\prime}=\\{\langle x,x^{\prime}\rangle,\langle
x^{\prime},x^{\prime}\rangle:x\in W\text{ and }R[x]=\emptyset\\}$, and
$V^{\prime}$ extends $V$ with $V(p,x^{\prime})=0$ for all $p\in{\rm Var}$ and
$x^{\prime}\in W^{\prime}$. Clearly, if $\mathfrak{M}$ is finite, then
$\mathfrak{M}^{\prime}$ is also finite.

It now suffices to prove the following: for any ${\mathrm{K(A)}}$-model
$\mathfrak{M}=\langle W,R,V\rangle$, $x\in W$, finite set of formulas $S$, and
$\varepsilon>0$, there exists a finite ${\mathrm{K(A)}}$-model
$\mathfrak{M}^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ with
$x\in W^{\prime}$ such that $|V(\varphi,x)-V^{\prime}(\varphi,x)|<\varepsilon$
for all $\varphi\in S$. We proceed by induction on the sum of the complexities
of the formulas in $S$.

For the base case, $S$ contains only variables and $\overline{0}$, and we let
$\mathfrak{M}^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ with
$W^{\prime}=\\{x\\}$, $R^{\prime}=\emptyset$, and $V^{\prime}(p,x)=V(p,x)$ for
each $p\in{\rm Var}$. For the inductive step, suppose first that
$S=S^{\prime}\cup\\{\psi_{1}\to\psi_{2}\\}$. Then we can apply the induction
hypothesis with $\mathfrak{M}$, $x\in W$,
$S^{\prime\prime}=S^{\prime}\cup\\{\psi_{1},\psi_{2}\\}$, and
$\frac{\varepsilon}{2}>0$ to obtain a finite ${\mathrm{K(A)}}$-model
$\mathfrak{M}^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ with
$x\in W^{\prime}$ such that
$|V(\varphi,x)-V^{\prime}(\varphi,x)|<\frac{\varepsilon}{2}$ for all
$\varphi\in S^{\prime\prime}$. It suffices then to observe that
$|V(\psi_{1}\to\psi_{2},x)-V^{\prime}(\psi_{1}\to\psi_{2},x)|=|V(\psi_{2},x)-V(\psi_{1},x)-V^{\prime}(\psi_{2},x)+V^{\prime}(\psi_{1},x)|\leq|V(\psi_{2},x)-V^{\prime}(\psi_{2},x)|+|V(\psi_{1},x)-V^{\prime}(\psi_{1},x)|<\frac{\varepsilon}{2}+\frac{\varepsilon}{2}=\varepsilon$.
The cases where $S$ contains $\psi_{1}\&\psi_{2}$, $\psi_{1}\land\psi_{2}$, or
$\psi_{1}\lor\psi_{2}$ are very similar.

Finally, suppose that $S$ consists of variables and boxed formulas
$\Box\psi_{1},\ldots,\Box\psi_{n}$ ($n\geq 1$). Then for
$i\in\\{1,\ldots,n\\}$, there exists $y_{i}\in W$ such that $Rxy_{i}$ and
$|V(\Box\psi_{i},x)-V(\psi_{i},y_{i})|<\frac{\varepsilon}{2}$. We apply the
induction hypothesis to each submodel $\mathfrak{M}_{i}$ of $\mathfrak{M}$
generated by $y_{i}$ (i.e., the restriction of $\mathfrak{M}$ to the smallest
subset of $W$ containing $y_{i}$ and closed under $R$) with
$S^{\prime}=(S\setminus\\{\Box\psi_{1},\ldots,\Box\psi_{n}\\})\cup\\{\psi_{1},\ldots,\psi_{n}\\}$,
$y_{i}\in W_{i}$, and $\frac{\varepsilon}{2}>0$ to obtain a finite
${\mathrm{K(A)}}$-model $\mathfrak{M}^{\prime}_{i}=\langle
W^{\prime}_{i},R^{\prime}_{i},V^{\prime}_{i}\rangle$ and $y_{i}\in
W^{\prime}_{i}$ such that
$|V(\varphi,y_{i})-V^{\prime}(\varphi,y_{i})|<\frac{\varepsilon}{2}$ for all
$\varphi\in S^{\prime}$. By renaming worlds, we may assume that these models
are disjoint and do not include $x$. Now let $\mathfrak{M}^{\prime}=\langle
W^{\prime},R^{\prime},V^{\prime}\rangle$ be the finite ${\mathrm{K(A)}}$-model
with $W^{\prime}=\\{x\\}\cup W^{\prime}_{1}\cup\ldots\cup W^{\prime}_{n}$ such
that for $u,v\in W^{\prime}$ and $p\in{\rm Var}$,

$\begin{array}[]{rclcrcl}R^{\prime}uv&=&\begin{cases}R^{\prime}_{i}uv&\text{if
}u,v\in W^{\prime}_{i}\\\ 1&\text{if }u=x,\ v\in\\{y_{1},\ldots,y_{n}\\}\\\
0&\text{otherwise}\end{cases}&\quad\text{and}&V^{\prime}(p,u)&=&\begin{cases}V^{\prime}_{i}(p,u)&\text{if
}u\in W^{\prime}_{i}\\\ V(p,x)&\text{if }u=x.\end{cases}\end{array}$

Clearly $V^{\prime}(p,x)=V(p,x)$ for each variable $p\in S$. Moreover,
$|V(\Box\psi_{i},x)-V(\psi_{i},y_{i})|<\frac{\varepsilon}{2}$ and
$|V(\psi_{i},y_{j})-V^{\prime}(\psi_{i},y_{j})|<\frac{\varepsilon}{2}$ for
$i,j\in\\{1,\ldots,n\\}$, so
$|V(\Box\psi_{i},x)-V^{\prime}(\Box\psi_{i},x)|<\varepsilon$.

As remarked above, the preceding lemma provides some justification both for
assuming in the definition of the semantics of ${\mathrm{K(A)}}$ that
$\bigwedge_{\mathbb{R}}\emptyset=\bigvee_{\mathbb{R}}\emptyset=0$, and for
restricting valuations of variables in a particular ${\mathrm{K(A)}}$-model to
a fixed interval. It shows that for determining the valid formulas of
${\mathrm{K(A)}}$, we need only consider finite serial
${\mathrm{K(A)}}$-models. For such frames we can leave
$\bigwedge_{\mathbb{R}}\emptyset$ and $\bigvee_{\mathbb{R}}\emptyset$
undefined; we can also make use of a standard (unrestricted) valuation map
$V\colon{\rm Var}\times W\to\mathbb{R}$, since only finite infima and suprema
are needed for calculating values of formulas. In principle then, we could
define the logic ${\mathrm{K(A)}}$ without extra assumptions by considering
only finite serial ${\mathrm{K(A)}}$-models. We prefer here, however, to give
a more general semantics and to discover this finite model property as a fact
about the logic rather than building it into the definition.

Any ${\mathrm{K(A)}}$-model can be viewed as a state transition system, where
each state is labelled with a vector of real numbers that represents the
values of the variables in ${\rm Var}$ at that state. Such a transition system
may be used to represent choices for various players in a game together with
points (or other resources) accumulated by the players during that game.
Consider for example the ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle
W,R,V\rangle$ depicted below, where the vectors $\begin{pmatrix}p\\\
q\end{pmatrix}$ represent the values of $p$ and $q$, respectively, at each
state.

$\begin{pmatrix}0\\\ 0\end{pmatrix}$$\begin{pmatrix}1\\\
0\end{pmatrix}$$\begin{pmatrix}0\\\ 1\end{pmatrix}$$\begin{pmatrix}2\\\
0\end{pmatrix}$$\begin{pmatrix}4\\\ 1\end{pmatrix}$$\begin{pmatrix}1\\\
1\end{pmatrix}$$\begin{pmatrix}1\\\ 3\end{pmatrix}$

We can use the model $\mathfrak{M}$ to define various two-player games, where
in the first round, starting at the root, Player $P$ chooses one of several
(in this case, two) options, and in the second round, Player $Q$ also chooses
one of several (in this case, also two) options. The points assigned to Player
$P$ and Player $Q$ at each state are the values of $p$ and $q$, respectively.
Let also call the values of $p-q$ and $q-p$ at a state, the scores for $P$ and
$Q$, respectively. We assume in all these games that the players have complete
knowledge of both $\mathfrak{M}$ and their opponent’s goals.

Let us consider some different ways of concluding games based on
$\mathfrak{M}$. Suppose that in Game 1 each player’s goal is to maximize her
final score. Player $P$’s maximal payoff is then the value at the root of the
formula $\Diamond\Box(q\to p)$, which is $2$. If Player $P$’s goal in Game 2
is to maximize her final number of points, and Player $Q$ aims to minimize
this number, then the required formula is $\Diamond\Box p$, which at the root
also takes value $2$. Reversing the roles for Game $3$, we obtain the formula
$\Box\Diamond q$, which takes value $1$ at the root. More complicated goals
can also be modelled. For example, if both players aim to maximize the sum of
their scores accumulated during the two rounds, then Player $P$’s maximal
payoff is the value of the formula $\Diamond((q\to p)\&\Box(q\to p))$ at the
root, namely $3$.

Formulas can also be used to express general relationships between games. For
example, the model $\mathfrak{M}$ shows that

$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\Diamond\Box(q\to p)\to(\Box\Diamond
q\to\Diamond\Box p).$

That is, Player $P$’s maximal payoff in Game 1 exceeds her maximal payoff in
Game 2 minus her maximal payoff in Game 3. On the other hand, it can be shown
(e.g., using one of the calculi introduced below) that

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Diamond\Box(q\to p)\to(\Box\Box
q\to\Diamond\Box p).$

This means that if the goals of Games 1 and 2 are adopted with respect to an
arbitrary ${\mathrm{K(A)}}$-model $\mathfrak{M}^{\prime}$ based on a finite
rooted tree with branches of length $2$, then Player $P$’s maximal payoff in
Game 1 for $\mathfrak{M}^{\prime}$ is always less than or equal to her maximal
payoff in Game 2 for $\mathfrak{M}^{\prime}$ minus the minimum number of
points for Player $Q$ in all final states of $\mathfrak{M}^{\prime}$.

###  2.3. Łukasiewicz Modal Logic

Let us briefly recall the semantics of the Łukasiewicz modal logic
${\mathrm{K(\mathrmL)}}$ studied by Hansoul and Teheux in [21]. For
convenience, we make use of a language $\mathcal{L}_{\mathrmL}^{\Box}$ with
the binary connective $\supset$ and unary connectives ${\sim}$ and $\Box$,
where further connectives are defined as
$\varphi\oplus\psi:={\sim}\varphi\supset\psi$,
$\varphi\odot\psi:={\sim}({\sim}\varphi\oplus{\sim}\psi)$,
$\varphi\lor\psi:=(\varphi\supset\psi)\supset\psi$,
$\varphi\land\psi:={\sim}({\sim}\varphi\lor{\sim}\psi)$, and
$\Diamond\varphi:={\sim}\Box{\sim}\varphi$.

A _${\mathrm{K(\mathrmL)}}$ -model_ $\mathfrak{M}=\langle W,R,V\rangle$
consists of a frame $\langle W,R\rangle$ and a valuation map $V\colon{\rm
Var}\times W\to[0,1]$ that is extended to $V\colon{\rm
Fm}(\mathcal{L}_{\mathrmL}^{\Box})\times W\to[0,1]$ by

$\begin{array}[]{rcl}V({\sim}\varphi,x)&=&1-V(\varphi,x)\\\\[1.8063pt]
V(\varphi\supset\psi,x)&=&\min(1,1-V(\varphi,x)+V(\psi,x))\\\\[1.8063pt]
V(\Box\varphi,x)&=&\bigwedge_{[0,1]}\\{V(\varphi,y):Rxy\\}.\end{array}$

An $\mathcal{L}_{\mathrmL}^{\Box}$-formula $\varphi$ is _valid_ in a
${\mathrm{K(\mathrmL)}}$-model $\mathfrak{M}=\langle W,R,V\rangle$ if
$V(\varphi,x)=1$ for all $x\in W$. If $\varphi$ is valid in all
${\mathrm{K(\mathrmL)}}$-models, then $\varphi$ is _${\mathrm{K(\mathrmL)}}$
-valid_, written $\models_{{\mathrm{{\mathrm{K(\mathrmL)}}}}}\varphi$.

An axiom system for ${\mathrm{K(\mathrmL)}}$ is presented in [21] as an
extension of an axiomatization of infinite-valued Łukasiewicz logic with the
modal axioms and rules

$\begin{array}[]{c}\Box(\varphi\supset\psi)\supset(\Box\varphi\supset\Box\psi)\\\\[1.8063pt]
\Box(\varphi\oplus\varphi)\supset(\Box\varphi\oplus\Box\varphi)\\\\[1.8063pt]
\Box(\varphi\odot\varphi)\supset(\Box\varphi\odot\Box\varphi)\\\\[5.42003pt]
\Box\varphi\varphi\end{array}$

and the following rule with infinitely many premises

$\varphi\lx@proof@logical@and\varphi\oplus\varphi\varphi\oplus(\varphi\odot\varphi)\varphi\oplus(\varphi\odot\varphi\odot\varphi)\ldots$

It is proved that an $\mathcal{L}_{\mathrmL}^{\Box}$-formula $\varphi$ is
derivable in this system if and only if
$\models_{{\mathrm{{\mathrm{K(\mathrmL)}}}}}\varphi$.111In fact, the authors
of [21] prove a more general strong completeness result: an
$\mathcal{L}_{\mathrmL}^{\Box}$-formula $\varphi$ is derivable from a
(possibly infinite) set of $\mathcal{L}_{\mathrmL}^{\Box}$-formulas
$\mathrm{\Sigma}$ in the system if and only if for every
${\mathrm{K(\mathrmL)}}$-model $\langle W,R,V\rangle$ and $x\in W$, whenever
$V(\psi,x)=1$ for all $\psi\in\mathrm{\Sigma}$, also $V(\varphi,x)=1$. Note
that an infinitary rule is needed to obtain a strong completeness theorem even
for propositional Łukasiewicz logic and Abelian logic. However, in this paper
we establish only (weak) completeness results.

This raises an intriguing question. Is there an elegant axiomatization
containing only finitary rules, obtained perhaps by removing the infinitary
rule above? Our first step towards addressing this issue will be to view
Łukasiewicz modal logic ${\mathrm{K(\mathrmL)}}$ as a fragment of a modest
extension of the Abelian modal logic ${\mathrm{K(A)}}$. Let
$\mathcal{L}_{{\mathrm{A^{c}}}}^{\Box}$ be the language
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$ extended with an extra constant $c$. A
${\mathrm{K(A^{c})}}$-model $\mathfrak{M}=\langle
W,R,V,c^{\mathfrak{M}}\rangle$ consists of a ${\mathrm{K(A)}}$-model $\langle
W,R,V\rangle$ and an element $c^{\mathfrak{M}}\in\mathbb{R}$, where valuations
are extended as before, using the additional clause $V(c,x)=c^{\mathfrak{M}}$
for each $x\in W$.

Let us fix $\bot:=c\land\lnot c$ and define the following mapping from ${\rm
Fm}(\mathcal{L}_{\mathrmL}^{\Box})$ to ${\rm
Fm}(\mathcal{L}_{{\mathrm{A^{c}}}}^{\Box})$:

$\begin{array}[]{rcl}p^{*}&=&(p\land\overline{0})\lor\bot\ \text{ for each}\
p\in{\rm Var}\\\\[1.8063pt]
({\sim}\varphi)^{*}&=&\varphi^{*}\to\bot\\\\[1.8063pt]
(\varphi\supset\psi)^{*}&=&(\varphi^{*}\to\psi^{*})\land\overline{0}\\\\[1.8063pt]
(\Box\varphi)^{*}&=&\Box\varphi^{*}.\end{array}$

We show that this mapping preserves validity between ${\mathrm{K(\mathrmL)}}$
and ${\mathrm{K(A^{c})}}$ by identifying the value taken by an
$\mathcal{L}_{\mathrmL}^{\Box}$-formula in $[0,1]$ with the value taken by the
corresponding $\mathcal{L}_{{\mathrm{A^{c}}}}^{\Box}$-formula in the interval
$[-|c|,0]$.

######  Proposition 2.

Let $\varphi\in{\rm Fm}(\mathcal{L}_{\mathrmL}^{\Box})$. Then
$\models_{{\mathrm{{\mathrm{K(\mathrmL)}}}}}\varphi$ if and only if
$\models_{{\mathrm{{\mathrm{K(A^{c})}}}}}\varphi^{*}$.

######  Proof 2.2.

Suppose first that $\varphi$ is not valid in a ${\mathrm{K(\mathrmL)}}$-model
$\mathfrak{M}=\langle W,R,V\rangle$. So $V(\varphi,x)<1$ for some $x\in W$. We
consider the ${\mathrm{K(A^{c})}}$-model $\mathfrak{M}^{\prime}=\langle
W,R,V^{\prime},c^{\mathfrak{M}}\rangle$ where $V^{\prime}(p,x)=V(p,x)-1$ for
any $p\in{\rm Var}$ and $x\in W$, and $c^{\mathfrak{M}}=-1$. It suffices to
prove that $V^{\prime}(\psi^{*},x)=V(\psi,x)-1$ for any $\psi\in{\rm
Fm}(\mathcal{L}_{\mathrmL}^{\Box})$, since then
$V^{\prime}(\varphi^{*},x)=V(\varphi,x)-1<0$ and
$\not\models_{{\mathrm{{\mathrm{K(A^{c})}}}}}\varphi^{*}$. We proceed by
induction on the complexity of $\psi$. The base case follows by definition and
for the inductive step for the propositional connectives, we just notice that,
using the induction hypothesis,

$\begin{array}[]{rcl}V^{\prime}((\psi_{1}\supset\psi_{2})^{*},x)&=&V^{\prime}((\psi_{1}^{*}\to\psi_{2}^{*})\land\overline{0},x)\\\\[1.8063pt]
&=&\min(V^{\prime}(\psi_{2}^{*},x)-V^{\prime}(\psi_{1}^{*},x),0)\\\\[1.8063pt]
&=&\min((V(\psi_{2},x)-1)-(V(\psi_{1},x)-1),0)\\\\[1.8063pt]
&=&\min(V(\psi_{2},x)-V(\psi_{1},x),0)\\\\[1.8063pt]
&=&\min(1-V(\psi_{1},x)+V(\psi_{2},x),1)-1\\\\[1.8063pt]
&=&V(\psi_{1}\supset\psi_{2},x)-1,\end{array}$

the case where $\psi$ is ${\sim}\psi_{1}$ being very similar. For the modal
case, we obtain

$\begin{array}[]{rcl}V^{\prime}((\Box\psi_{1})^{*},x)&=&V^{\prime}(\Box\psi_{1}^{*},x)\\\\[1.8063pt]
&=&\bigwedge_{\mathbb{R}}\\{V^{\prime}(\psi_{1}^{*},y):Rxy\\}\\\\[1.8063pt]
&=&\bigwedge_{\mathbb{R}}\\{V(\psi_{1},y)-1:Rxy\\}\\\\[1.8063pt]
&=&\bigwedge_{[0,1]}\\{V(\psi_{1},y):Rxy\\}-1\\\\[1.8063pt]
&=&V(\Box\psi_{1},x)-1,\end{array}$

noting that in the case where $R[x]=\emptyset$, we obtain
$\bigwedge_{\mathbb{R}}\\{V^{\prime}(\psi_{1}^{*},y):Rxy\\}=0=1-1=\bigwedge_{[0,1]}\\{V(\psi_{1},y):Rxy\\}-1$
as required.

Suppose now conversely that $\varphi^{*}$ is not valid in a
${\mathrm{K(A^{c})}}$-model $\mathfrak{M}=\langle
W,R,V,c^{\mathfrak{M}}\rangle$. That is, $V(\varphi^{*},x)<0$ for some $x\in
W$. Observe first that if $c^{\mathfrak{M}}=0$, then, by a simple induction on
the complexity of $\varphi$, we obtain $V(\varphi^{*},x)=0$ for all $x\in W$,
a contradiction. Hence $c^{\mathfrak{M}}\neq 0$. Moreover, by scaling
(dividing $V(p,x)$ by $c^{\mathfrak{M}}$ for each $p\in{\rm Var}$ and $x\in
W$), we may assume that $V(\bot,x)=-1$ for all $x\in W$. We consider the
${\mathrm{K(\mathrmL)}}$-model $\mathfrak{M}^{\prime}=\langle
W,R,V^{\prime}\rangle$ where $V^{\prime}(p,x)=\max(\min(V(p,x)+1,1),0)$. It
then suffices to prove that $V^{\prime}(\psi,x)=V(\psi^{*},x)+1$ for any
$\psi\in{\rm Fm}(\mathcal{L}_{\mathrmL}^{\Box})$, proceeding by induction on
the complexity of $\psi$.

Note that the addition of a constant $c$ to ${\mathrm{K(A)}}$ does not affect
the fact that validity in the logic is equivalent to validity in finite
models. It does, however, introduce a difference between the logic
${\mathrm{K(A^{c})}}$ and the same logic restricted to serial models. Clearly,
the formula $c\to\Box c$ is valid in all serial models, but not in all models.

##  3\. A Labelled Tableau Calculus

In this section we introduce a labelled tableau calculus for checking
${\mathrm{K(A)}}$-validity that is based very closely on the Kripke semantics
described above. We use the calculus here to show that the problem of checking
${\mathrm{K(A)}}$-validity is in the complexity class coNEXPTIME. In Section
4, we will also use (a fragment of) the calculus to establish the completeness
of an axiom system and a sequent calculus admitting cut-elimination for the
modal-multiplicative fragment of ${\mathrm{K(A)}}$.

###  3.1. The Calculus

Our labelled tableau calculus ${\mathrm{LK(A)}}$ proves that an
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula $\varphi$ is valid by showing that
the assumption that $\varphi$ takes a value less than $0$ in some world
$w_{1}$ leads to a contradiction. Informally, we build a tableau for $\varphi$
as follows. First we decompose the propositional structure of $\varphi$ to
obtain inequations between sums of formulas labelled with the world $w_{1}$.
We then use box formulas occurring on the right of these inequations to
generate new worlds accessible to $w_{1}$ and further inequations between sums
of formulas labelled with $w_{1}$ and these accessible worlds. Box formulas on
the left are decomposed by considering accessible worlds to $w_{1}$ and
generating new inequations for those worlds. The process is then repeated with
the new inequations and worlds appearing on the tableau. The formula $\varphi$
will be valid if the generated set of inequations (suitably interpreted) on
each branch of the tableau is unsatisfiable over the real numbers.

By a labelled formula we mean an ordered pair consisting of an
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula $\varphi$ and a natural number
$k$, written $(\varphi)^{k}$. Given a multiset of
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formulas
$\mathrm{\Gamma}=[\varphi_{1},\ldots,\varphi_{n}]$ (denoting the empty
multiset by $[]$) and $k_{1},\ldots,k_{n}\in\mathbb{N}$, we let
$(\mathrm{\Gamma})^{\mathbf{k}}$ denote the multiset of labelled formulas
$[(\varphi_{1})^{k_{1}},\ldots,(\varphi_{n})^{k_{n}}]$.

Tableaux are constructed from (tableau) nodes of two types:

  1. (1)

labelled inequations of the form
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
where $\triangleright\in\\{>,\geq\\}$ and
$(\mathrm{\Gamma})^{\mathbf{k}},(\mathrm{\Delta})^{\mathbf{l}}$ are finite
multisets of labelled formulas;

  2. (2)

relations of the form $rij$ where $i,j\in\mathbb{N}$.

An ${\mathrm{LK(A)}}$-tableau is a finite tree of nodes generated according to
the inference rules of the system presented in Figure 2. That is, if nodes
above the line in an instance of a rule occur on the same branch $B$, then $B$
can be extended with the nodes below the line. For convenience, we often write
branches as (numbered) lists, noting for future reference that tableaux for
formulas in the modal-multiplicative fragment (i.e., not containing $\land$ or
$\lor$) consist of just one branch.

$\begin{array}[]{cc}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}},(\overline{0})^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}&(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\overline{0})^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\\[14.45377pt]
(\mathrm{\Gamma})^{\mathbf{k}},(\varphi)^{i},(\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}},(\varphi\&\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}&(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi)^{i},(\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\&\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\\[14.45377pt]
(\mathrm{\Gamma})^{\mathbf{k}},(\psi)^{i}\triangleright(\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}},(\varphi\to\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}&(\mathrm{\Gamma})^{\mathbf{k}},(\varphi)^{i}\triangleright(\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\to\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\\[14.45377pt]
\begin{array}[]{c}(\mathrm{\Gamma})^{\mathbf{k}},(\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}\\\
(\mathrm{\Gamma})^{\mathbf{k}},(\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}\end{array}(\mathrm{\Gamma})^{\mathbf{k}},(\varphi\land\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}&(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\quad(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\land\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\\[21.68121pt]
(\mathrm{\Gamma})^{\mathbf{k}},(\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}\quad(\mathrm{\Gamma})^{\mathbf{k}},(\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}(\mathrm{\Gamma})^{\mathbf{k}},(\varphi\lor\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}&\begin{array}[]{c}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\
(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\end{array}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\lor\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}\\\\[14.45377pt]
\begin{array}[]{c}(\varphi)^{j}\geq(\Box\varphi)^{i}\\\
\end{array}\begin{array}[]{c}rij\\\
(\mathrm{\Gamma})^{\mathbf{k}},(\Box\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}\end{array}&\begin{array}[]{c}(\Box\varphi)^{i}\geq(\varphi)^{j}\\\
rij\end{array}(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\Box\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}j\in\mathbb{N}\text{
new}\end{array}$ $rkjrik\ j\in\mathbb{N}\text{ new}$ Figure 2. The labelled
tableau calculus ${\mathrm{LK(A)}}$

Observe that the rules for $\overline{0}$, $\&$, $\to$, $\land$, and $\lor$
decompose formulas on the left and right of inequations, using the same label
for added subformulas, while the rules for $\Box$ introduce inequations
between a boxed formula $\Box\varphi$ labelled with $i$, and $\varphi$
labelled with a different $j$. Let us note also that the premises
$(\mathrm{\Gamma})^{\mathbf{k}},(\Box\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
and
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\Box\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}$
of $(\Box\,\triangleright)$ and $(\triangleright\,\Box)$, respectively, are
not, strictly speaking, necessary for either the soundness or the completeness
of the calculus. However, they restrict the decomposition of boxed formulas to
those occurring as subformulas of the initial formula, thereby ensuring a
subformula property for the calculus.

Let ${\rm LVar}$ be the set of all formulas of the form $(p)^{i}$ and
$(\Box\varphi)^{i}$ for $p\in{\rm Var}$, $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$, and $i\in\mathbb{N}$, considered as a
set of variables. Given an ${\mathrm{LK(A)}}$-tableau $T$ and a branch $B$ of
$T$, the system of inequations $S$ associated to $B$ consists of all labelled
inequations occurring on $B$ that contain only formulas from ${\rm LVar}$.
Each labelled inequation in $S$ is interpreted here as an inequation between
formal sums (where addition is over the multisets occurring in the labelled
inequation and the empty multiset is $0$) of variables from ${\rm LVar}$. We
call the branch $B$ open if the set of inequations $S$ associated to $B$ is
consistent over $\mathbb{R}$, and closed otherwise. The tableau $T$ is called
closed if all of its branches are closed, and open if it has at least one open
branch.

A tableau for an $\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula $\varphi$ is an
${\mathrm{LK(A)}}$-tableau with root node $[]>[(\varphi)^{1}]$ and covering
node $r12$. We say that $\varphi$ is ${\mathrm{LK(A)}}$-derivable, written
$\vdash_{{\mathrm{{\mathrm{LK(A)}}}}}\varphi$, if there exists a closed
tableau for $\varphi$.

The seriality axiom $\Box p\to\Diamond p$ is ${\mathrm{LK(A)}}$-derivable
using the tableau

$1:$ | $[]>(\Box p\to(\Box(p\to\overline{0})\to\overline{0}))^{1}$
---|---
$2:$ | $r12$
$3:$ | $(\Box p)^{1}>(\Box(p\to\overline{0})\to\overline{0})^{1}$
$4:$ | $(\Box p)^{1},(\Box(p\to\overline{0}))^{1}>(\overline{0})^{1}$
$5:$ | $(\Box p)^{1},(\Box(p\to\overline{0}))^{1}>[]$
$6:$ | $(p)^{2}\geq(\Box p)^{1}$
$7:$ | $(p\to\overline{0})^{2}\geq(\Box(p\to\overline{0}))^{1}$
$8:$ | $(\overline{0})^{2}\geq(p)^{2},(\Box(p\to\overline{0}))^{1}$
$9:$ | $[]\geq(p)^{2},(\Box(p\to\overline{0}))^{1}$

which generates a (single) inconsistent system of inequations over
$\mathbb{R}$

$\\{x+y>0,\ z\geq x,\ 0\geq z+y\\}$

where $x$, $y$, and $z$ stand for $(\Box p)^{1}$,
$(\Box(p\to\overline{0}))^{1}$, and $(p)^{2}$, respectively.

The calculus ${\mathrm{LK(A)}}$ can also be used to prove that an
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula is not ${\mathrm{K(A)}}$-valid;
indeed a concrete counter-model for such a formula can be constructed from an
open branch of a tableau where, taking care to avoid loops, the rules have
been applied exhaustively.

Consider a tableau for the formula $\Box(p\lor q)\to(\Box p\lor\Box q)$ that
begins with

$1:$ | $[]>(\Box(p\lor q)\to(\Box p\lor\Box q))^{1}$
---|---
$2:$ | $r12$
$3:$ | $(\Box(p\lor q))^{1}>(\Box p\lor\Box q)^{1}$
$4:$ | $(\Box(p\lor q))^{1}>(\Box p)^{1}$
$5:$ | $(\Box(p\lor q))^{1}>(\Box q)^{1}$
$6:$ | $(\Box p)^{1}\geq(p)^{3}$
$7:$ | $r13$
$8:$ | $(\Box q)^{1}\geq(q)^{4}$
$9:$ | $r14$
$10:$ | $(p\lor q)^{2}\geq(\Box(p\lor q))^{1}$
$11:$ | $(p\lor q)^{3}\geq(\Box(p\lor q))^{1}$
$12:$ | $(p\lor q)^{4}\geq(\Box(p\lor q))^{1}$

then continues by splitting into two subtrees, namely

$(p)^{2}\geq(\Box(p\lor q))^{1}$ $(p)^{3}\geq(\Box(p\lor q))^{1}$
$(p)^{4}\geq(\Box(p\lor q))^{1}$ $(q)^{4}\geq(\Box(p\lor q))^{1}$
$(q)^{3}\geq(\Box(p\lor q))^{1}$ $(p)^{4}\geq(\Box(p\lor q))^{1}$
$(q)^{4}\geq(\Box(p\lor q))^{1}$

and a second that is exactly the same except that the root is
$(q)^{2}\geq(\Box(p\lor q))^{1}$.

Observe now that the systems of inequations for the two leftmost branches of
the subtree above are both inconsistent, since, combining inequations, we
obtain

$(p)^{3}\geq(\Box(p\lor q))^{1}>(\Box p)^{1}\geq(p)^{3}.$

Similarly, the system of inequations for the rightmost branch is inconsistent,
since we obtain

$(q)^{4}\geq(\Box(p\lor q))^{1}>(\Box q)^{1}\geq(q)^{4}.$

The system of inequations for the remaining branch is consistent, however. Let
us denote each $(p)^{i}$ and $(q)^{i}$ by $x_{i}$ and $y_{i}$, respectively,
for $i=2,3,4$, $(\Box p)^{1}$ and $(\Box q)^{1}$ by $x^{\prime}_{1}$ and
$y^{\prime}_{1}$, respectively, and $(\Box(p\lor q))^{1}$ by $z$. Then for
this branch, we obtain the set of inequations

$\\{z>x^{\prime}_{1},\,z>y^{\prime}_{1},\,x^{\prime}_{1}\geq
x_{3},\,y^{\prime}_{1}\geq y_{4},\,x_{2}\geq z,\,y_{3}\geq z,\,x_{4}\geq z\\}$

which can be satisfied over $\mathbb{R}$ by taking, e.g.,

$x_{2}=3,\,x_{3}=0,\,x_{4}=3,\,y_{3}=3,\,y_{4}=0,\,x^{\prime}_{1}=1,\,y^{\prime}_{1}=1,\,z=2.$

We obtain a ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle W,R,V\rangle$ by
identifying $w_{i}$ in $W$ with each $i\in\mathbb{N}$ occurring on the branch
and including $\langle w_{i},w_{j}\rangle$ in $R$ whenever $rij$ appears; that
is, $W=\\{w_{1},w_{2},w_{3},w_{4}\\}$ and $R=\\{\langle
w_{1},w_{2}\rangle,\langle w_{1},w_{3}\rangle,\langle w_{1},w_{4}\rangle\\}$.
We also use the assignment satisfying the set of inequations to define (the
other values are unimportant)

$V(p,w_{2})=V(p,w_{4})=V(q,w_{3})=3\quad\text{and}\quad
V(q,w_{2})=V(p,w_{3})=V(q,w_{4})=0.$

Then $V(\Box(p\lor q),w_{1})=3$ and $V(\Box p\lor\Box q,w_{1})=0$, so
$V(\Box(p\lor q)\to(\Box p\lor\Box q),w_{1})=-3$.

###  3.2. Soundness

Let $T$ be an ${\mathrm{LK(A)}}$-tableau and let $B$ be a branch of $T$. We
call a serial ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle W,R,V\rangle$
faithful to $B$ if there is a map $f\colon\mathbb{N}\to W$ (said to show that
$\mathfrak{M}$ is faithful to $B$) such that if $rij$ occurs on $B$, then
$Rf(i)f(j)$, and for every inequation
$(\varphi_{1})^{i_{1}},\ldots,(\varphi_{n})^{i_{n}}\triangleright(\psi_{1})^{j_{1}},\ldots,(\psi_{m})^{j_{m}}$
occurring on $B$,

$V(\varphi_{1},f(i_{1}))+\ldots+V(\varphi_{n},f(i_{n}))\,\triangleright\,V(\psi_{1},f(j_{1}))+\ldots+V(\psi_{m},f(j_{m})).$

We say that $\mathfrak{M}$ is faithful to $T$ if $\mathfrak{M}$ is faithful to
a branch $B$ of $T$. Observe that in this case, the map defined by
$e((p)^{i})=V(p,i)$ and $e((\Box\varphi)^{i})=V(\Box\varphi,i)$ satisfies the
system of inequations associated to $B$, and hence $T$ is open.

The following lemma establishes the soundness of the rules of
${\mathrm{LK(A)}}$.

######  Lemma 3.

Let $\mathfrak{M}=\langle W,R,V\rangle$ be a finite serial
${\mathrm{K(A)}}$-model faithful to a branch $B$ of an
${\mathrm{LK(A)}}$-tableau $T$. If a rule of ${\mathrm{LK(A)}}$ is applied to
$B$, giving a tableau $T^{\prime}$ extending $T$, then $\mathfrak{M}$ is
faithful to $T^{\prime}$.

######  Proof 3.1.

Let $f$ be a map showing that the finite serial ${\mathrm{K(A)}}$-model
$\mathfrak{M}=\langle W,R,V\rangle$ is faithful to the branch $B$ of the
tableau $T$. The cases of $(\overline{0}\,\triangleright)$,
$(\triangleright\,\overline{0})$, $({\to}\,\triangleright)$,
$(\triangleright\,{\to})$, $(\&\,\triangleright)$, $(\triangleright\,\&)$,
$(\triangleright\,\lor)$, and $(\land\,\triangleright)$ follow easily. For
$(\lor\,\triangleright)$, suppose that
$(\mathrm{\Gamma})^{\mathbf{k}},(\varphi\lor\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
appears on $B$, and that we obtain an extension $T^{\prime}$ of $T$ by two
branches: one branch $B^{\prime}$ extending $B$ with
$(\mathrm{\Gamma})^{\mathbf{k}},(\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$,
and another branch $B^{\prime\prime}$ extending $B$ with
$(\mathrm{\Gamma})^{\mathbf{k}},(\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$.
Let
$(\mathrm{\Gamma})^{\mathbf{k}}=[(\varphi_{1})^{k_{1}},\ldots,(\varphi_{n})^{k_{n}}]$
and
$(\mathrm{\Delta})^{\mathbf{l}}=[(\psi_{1})^{l_{1}},\ldots,(\psi_{m})^{l_{m}}]$
and denote $V(\varphi_{1},f(k_{1}))+\ldots+V(\varphi_{n},f(k_{n}))$ by
$V(\mathrm{\Gamma},f(\mathbf{k}))$ and
$V(\psi_{1},f(l_{1}))+\ldots+V(\psi_{m},f(l_{m}))$ by
$V(\mathrm{\Delta},f(\mathbf{l}))$. Since $\mathfrak{M}$ is faithful to $B$,
we have
$V(\mathrm{\Gamma},f(\mathbf{k}))+V(\varphi\lor\psi,f(i))\triangleright
V(\mathrm{\Delta},f(\mathbf{l}))$. Hence

$V(\mathrm{\Gamma},f(\mathbf{k}))+\max(V(\varphi,f(i)),V(\psi,f(i)))\,\triangleright\,V(\mathrm{\Delta},f(\mathbf{l})).$

If $\max(V(\varphi,f(i)),V(\psi,f(i)))=V(\varphi,f(i))$ then $\mathfrak{M}$ is
faithful to the branch $B^{\prime}$, otherwise $\mathfrak{M}$ is faithful to
the branch $B^{\prime\prime}$. Hence $\mathfrak{M}$ is faithful to
$T^{\prime}$. The case of $(\triangleright\,\land)$ follows similarly.

For $(\Box\,\triangleright)$, suppose that
$(\mathrm{\Gamma})^{\mathbf{k}},(\Box\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
and $rij$ appear on $B$ and we obtain an extension $T^{\prime}$ of $T$ by a
branch $B^{\prime}$ which extends $B$ with
$(\varphi)^{j}\geq(\Box\varphi)^{i}$. Since $\mathfrak{M}$ is faithful to $B$,
we have $Rf(i)f(j)$. But then $V(\varphi,f(j))\geq V(\Box\varphi,f(i))$, so
$\mathfrak{M}$ is faithful to $B^{\prime}$ and $T^{\prime}$.

For $(\triangleright\,\Box)$ suppose that
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\Box\varphi)^{i},(\mathrm{\Delta})^{\mathbf{l}}$
appears on $B$ and we obtain an extension $T^{\prime}$ of $T$ by a branch
$B^{\prime}$ that extends $B$ with $rij$ ($j\in\mathbb{N}$ new) and
$(\Box\varphi)^{i}\geq(\varphi)^{j}$. Since $\mathfrak{M}$ is finite and
serial, there exists $v\in W$ such that $Rf(i)v$ and
$V(\Box\varphi,f(i))=V(\varphi,v)$. Hence the map $f^{\prime}$ defined to
coincide with $f$ except that $f^{\prime}(j)=v$ together with the branch
$B^{\prime}$ show that $\mathfrak{M}$ is faithful to $T^{\prime}$.

Finally, for $(\rm ex)$, suppose that $rik$ appears on $B$ and we obtain an
extension $T^{\prime}$ of $T$ by a branch $B^{\prime}$ that extends $B$ with
$rkj$ ($j\in\mathbb{N}$ new). Since $rik$ is in $B$, we have $Rf(i)f(k)$.
Because $\mathfrak{M}$ is serial, there exists $v\in W$ such that $Rf(k)v$.
The map $f^{\prime}$ defined to coincide with $f$ except that
$f^{\prime}(j)=v$ shows that $\mathfrak{M}$ is faithful to $B^{\prime}$ and,
hence, to $T^{\prime}$.

######  Proposition 4.

If $\vdash_{{\mathrm{{\mathrm{LK(A)}}}}}\varphi$, then
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

######  Proof 3.2.

Suppose that $\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$. By Lemma 1,
there exist a finite serial ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle
W,R,V\rangle$ and $w_{1}\in W$ such that $0>V(\varphi,w_{1})$. Let
$f\colon\mathbb{N}\to W$ be any function such that $f(1)=w_{1}$ and
$f(2)=w_{2}$, where $Rw_{1}w_{2}$. This function shows that $\mathfrak{M}$ is
faithful to the only branch of the tableau consisting just of the root
$[]>[(\varphi)^{1}]$ and covering node $r12$. Suppose that by applying the
decomposition rules to this tableau, we obtain a tableau $T$. Applying Lemma 3
inductively, $\mathfrak{M}$ is faithful to $T$ by some branch $B$. But then
the system of inequations associated with $B$ is consistent over $\mathbb{R}$,
and $T$ is open. Hence $\not\vdash_{{\mathrm{{\mathrm{LK(A)}}}}}\varphi$.

###  3.3. Completeness

We establish the completeness of ${\mathrm{LK(A)}}$ by showing that an open
branch of a tableau for a formula where the rules have been applied
exhaustively generates a ${\mathrm{K(A)}}$-model where the formula is not
valid. In order to avoid repetitions occurring when a rule is applied more
than once to a labelled inequation with the same conclusions (or with a new
label in the case of $(\triangleright\,\Box)$), we distinguish between active
and inactive inequations and use new variables to denote modal formulas that
have already been decomposed. To make this precise, we introduce the notation
$\lceil\Box\varphi\rceil$ to denote a variable corresponding to the modal
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formula $\Box\varphi$, and define ${\rm
Var}^{*}={\rm Var}\cup\\{\lceil\Box\varphi\rceil:\Box\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})\\}$. We let ${\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})^{*}$ denote the set of
$\mathcal{L}_{{\mathrm{A}}}^{\Box}$-formulas over ${\rm Var}^{*}$, noting that
of course ${\rm Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})\subseteq{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})^{*}$. The complexity of a labelled
inequation
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
over ${\rm Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})^{*}$ is defined as the sum
of the complexities of the formula occurrences in $\mathrm{\Gamma}$ and
$\mathrm{\Delta}$.

We now consider a slight variant ${\mathrm{LK^{\prime}(A)}}$ of
${\mathrm{LK(A)}}$, replacing the rules for $\Box$ with the following rules
that decompose several occurrences of a labelled formula simultaneously:

$\begin{array}[]{ccc}\begin{array}[]{c}(\varphi)^{j_{1}}\geq(\lceil\Box\varphi\rceil)^{i}\\\
\vdots\\\ (\varphi)^{j_{s}}\geq(\lceil\Box\varphi\rceil)^{i}\\\
(\mathrm{\Gamma}_{1})^{\mathbf{k_{1}}},n_{1}(\lceil\Box\varphi\rceil)^{i}\triangleright(\mathrm{\Delta}_{1})^{\mathbf{l_{1}}}\\\
\vdots\\\
(\mathrm{\Gamma}_{m})^{\mathbf{k_{m}}},n_{m}(\lceil\Box\varphi\rceil)^{i}\triangleright(\mathrm{\Delta}_{m})^{\mathbf{l_{m}}}\\\
\end{array}\begin{array}[]{c}rij_{1}\\\ \vdots\\\ rij_{s}\\\
(\mathrm{\Gamma}_{1})^{\mathbf{k_{1}}},n_{1}(\Box\varphi)^{i}\triangleright(\mathrm{\Delta}_{1})^{\mathbf{l_{1}}}\\\
\vdots\\\
(\mathrm{\Gamma}_{m})^{\mathbf{k_{m}}},n_{m}(\Box\varphi)^{i}\triangleright(\mathrm{\Delta}_{m})^{\mathbf{l_{m}}}\\\
\end{array}&&\begin{array}[]{c}(\lceil\Box\varphi\rceil)^{i}\geq(\varphi)^{j}\\\
rij\\\ (\mathrm{\Gamma}_{1})^{\mathbf{k_{1}}}\triangleright
n_{1}(\lceil\Box\varphi\rceil)^{i},(\mathrm{\Delta}_{1})^{\mathbf{l_{1}}}\\\
\vdots\\\ (\mathrm{\Gamma}_{m})^{\mathbf{k_{m}}}\triangleright
n_{m}(\lceil\Box\varphi\rceil)^{i},(\mathrm{\Delta}_{m})^{\mathbf{l_{m}}}\\\
\end{array}\begin{array}[]{c}(\mathrm{\Gamma}_{1})^{\mathbf{k_{1}}}\triangleright
n_{1}(\Box\varphi)^{i},(\mathrm{\Delta}_{1})^{\mathbf{l_{1}}}\\\ \vdots\\\
(\mathrm{\Gamma}_{m})^{\mathbf{k_{m}}}\triangleright
n_{m}(\Box\varphi)^{i},(\mathrm{\Delta}_{m})^{\mathbf{l_{m}}}\\\
\end{array}j\in\mathbb{N}\text{ new}\end{array}$

Closed and open ${\mathrm{LK^{\prime}(A)}}$-tableaux are defined as for
${\mathrm{LK(A)}}$, except that the system associated to a branch of a tableau
consists of all inequations on the branch that contain only variables from
$\\{(q)^{i}:q\in{\rm Var}^{*},i\in\mathbb{N}\\}$. We call an
${\mathrm{LK^{\prime}(A)}}$-tableau for $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$ complete if it is constructed as
follows, making use of the notions of active and inactive inequations of the
tableau to control applications of the rules:

  1. (1)

Begin the tableau with the active labelled inequation $[]>[(\varphi)^{1}]$ and
relation $r12$.

  2. (2)

If all active labelled inequations have complexity $0$, then stop.

  3. (3)

Apply the rules for $\overline{0},\&,\to,\land,\lor$ exhaustively to active
labelled inequations, changing the premise to inactive and the conclusions to
active after each application.

  4. (4)

Fix $i$ such that $(\Box\psi)^{i}$ occurs in an active labelled inequation,
and apply $(\rm ex)$ to every branch $B$ containing $(\Box\chi)^{i}$ for some
$\Box\chi$ in an active inequation to obtain relations $rik_{B}$ for some new
$k_{B}\in\mathbb{N}$.

  5. (5)

For each $(\Box\psi)^{i}$ occurring on the right in an active labelled
inequation, apply $(\triangleright\,\Box^{\prime})$ to the collection of all
active labelled inequations
$(\mathrm{\Gamma}_{t})^{\mathbf{k_{t}}}\triangleright
n_{t}(\Box\psi)^{i},(\mathrm{\Delta}_{t})^{\mathbf{l_{t}}}$ (where
$(\Box\psi)^{i}$ does not occur in $(\mathrm{\Delta}_{t})^{\mathbf{l_{t}}}$)
on a branch, changing the premise to inactive and the conclusions to active
after each application.

  6. (6)

For each $(\Box\psi)^{i}$ occurring on the left in an active labelled
inequation, apply $(\Box\,\triangleright^{\prime})$ to the collection of all
active labelled inequations
$(\mathrm{\Gamma}_{t})^{\mathbf{k_{t}}},n_{t}(\Box\psi)^{i}\triangleright(\mathrm{\Delta}_{t})^{\mathbf{l_{t}}}$
(where $(\Box\psi)^{i}$ does not occur in
$(\mathrm{\Gamma}_{t})^{\mathbf{k_{t}}}$) and all relations
$rij_{1},\ldots,rij_{s}$ on a branch, changing the premises to inactive and
the conclusions to active after each application.

  7. (7)

Repeat from (2).

Observe that steps (3), (5), and (6) above decrease the multiset of
complexities of the active labelled inequations, according to the standard
multiset well-ordering (see [10]). Hence the procedure terminates with a
complete ${\mathrm{LK^{\prime}(A)}}$-tableau $T$ for any $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$. Suppose now that we change each
$(\lceil\Box\psi\rceil)^{i}$ to $(\Box\psi)^{i}$ in $T$. Replacing
applications of the rules $(\Box\,\triangleright^{\prime})$ and
$(\triangleright\,\Box^{\prime})$ with appropriate repeated applications of
the rules $(\Box\,\triangleright)$ and $(\triangleright\,\Box)$, we obtain an
${\mathrm{LK(A)}}$-tableau $T^{\prime}$ for $\varphi$ such that each branch of
$T^{\prime}$ contains all the inequations (modulo renaming of variables)
occurring on the corresponding branch of $T$. Hence we obtain:

######  Lemma 5.

If there exists a closed complete ${\mathrm{LK^{\prime}(A)}}$-tableau for
$\varphi\in{\rm Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$, then
$\vdash_{{\mathrm{{\mathrm{LK(A)}}}}}~{}\varphi$.

Let $T$ be an open complete ${\mathrm{LK^{\prime}(A)}}$-tableau for
$\varphi\in{\rm Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$ and let $e$ be a map
satisfying the system of inequations associated to an open branch $B$ of $T$.
We say that $\mathfrak{M}=\langle W,R,V\rangle$ is the $e$-induced model of
$T$ by $B$ if

  * •

$W=\\{w_{i}:i\in\mathbb{N}\text{ is a label occurring on }B\\}$;

  * •

$Rw_{i}w_{j}$ if and only if $rij$ occurs on $B$;

  * •

the valuation map $V\colon{\rm Var}^{*}\times W\to[-r,r]$ is defined by

$\begin{array}[]{rcl}V(p,w_{i})&=&\begin{cases}e((p)^{i})&\text{ if
}(p)^{i}\text{ occurs on }B\\\ 0&\text{ otherwise}\end{cases}\end{array}$

where $r=\max\\{|e((p)^{i})|:(p)^{i}\mbox{ occurs on }B\\}$.

######  Lemma 6.

Let $\mathfrak{M}=\langle W,R,V\rangle$ be the $e$-induced model of an open
complete ${\mathrm{LK^{\prime}(A)}}$-tableau $T$ by a branch $B$. Extend the
map $e$ by fixing $e((\varphi)^{i})=V(\varphi,w_{i})$ for each $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})^{*}$ and $w_{i}\in W$, and denote
$e((\varphi_{1})^{k_{1}})+\ldots+e((\varphi_{n})^{k_{n}})$ by
$e((\mathrm{\Gamma})^{\mathbf{k}})$ for
$(\mathrm{\Gamma})^{\mathbf{k}}=[(\varphi_{1})^{k_{1}},\ldots,(\varphi_{n})^{k_{n}}]$.
Then $e((\mathrm{\Gamma})^{\mathbf{k}})\triangleright
e((\mathrm{\Delta})^{\mathbf{l}})$ for each labelled inequation
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
that appears on $B$.

######  Proof 3.3.

We prove the claim by induction on the complexity of
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$.
The base case follows using the definition of $\mathfrak{M}$ and the fact that
$e$ satisfies the system of inequations associated to $B$. Moreover, the cases
where
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
appears as a premise of an application of a rule for $\overline{0}$, $\&$, or
$\to$ follow directly using the induction hypothesis.

Suppose that the inequation is
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},(\varphi\lor\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
and
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},(\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
appears on $B$. (The case where
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},(\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
appears on $B$ is symmetrical.) By the induction hypothesis,
$e((\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}})+e((\varphi)^{i})\triangleright
e((\mathrm{\Delta})^{\mathbf{l}})$. Since
$e((\varphi\lor\psi)^{i})=\max(e((\varphi)^{i}),e((\psi)^{i}))$ we obtain the
desired inequality. The case when the inequation is
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\land\psi)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$
follows similarly.

Suppose that the inequation is
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi\lor\psi)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$
and
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\varphi)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$
and
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\psi)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$
appear on $B$. The desired inequality follows by applying the induction
hypothesis to these two inequations and noticing that
$e((\varphi\lor\psi)^{i})=\max(e((\varphi)^{i}),e((\psi)^{i}))$. The case when
the inequation is
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},(\varphi\land\psi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
follows similarly.

Suppose that the inequation is
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},n(\Box\varphi)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
and
$(\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}},n(\lceil\Box\varphi\rceil)^{i}\triangleright(\mathrm{\Delta})^{\mathbf{l}}$
occurs on $B$. Since $\mathfrak{M}$ is finite and serial, there is a $j$ such
that $rij$ occurs on $B$ and $V(\Box\varphi,w_{i})=V(\varphi,w_{j})$. But then
also $(\varphi)^{j}\geq(\lceil\Box\varphi\rceil)^{i}$ occurs on $B$. By the
induction hypothesis twice,
$e((\mathrm{\Gamma}^{\prime})^{\mathbf{k^{\prime}}})+ne((\lceil\Box\varphi\rceil)^{i})\triangleright
e((\mathrm{\Delta})^{\mathbf{l}})$ and $e((\varphi)^{j})\geq
e((\lceil\Box\varphi\rceil)^{i})$, and the desired inequality follows since
also
$e((\Box\varphi)^{i})=V(\Box\varphi,w_{i})=V(\varphi,w_{j})=e((\varphi)^{j})$.

Finally, suppose that the inequation is
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright
n(\Box\varphi)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$ and
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright
n(\lceil\Box\varphi\rceil)^{i},(\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}}$
and $(\lceil\Box\varphi\rceil)^{i}\geq(\varphi)^{j}$ appear on $B$ together
with the relation $rij$. By the induction hypothesis twice,
$e((\mathrm{\Gamma})^{\mathbf{k}})\triangleright
ne((\lceil\Box\varphi\rceil)^{i})+e((\mathrm{\Delta}^{\prime})^{\mathbf{l^{\prime}}})$
and $e((\lceil\Box\varphi\rceil)^{i})\geq e((\varphi)^{j})$, and the desired
inequality follows since also $e((\varphi)^{j})=V(\varphi,w_{j})\geq
V(\Box\varphi,w_{i})=e((\Box\varphi)^{i})$.

######  Theorem 7.

The following are equivalent for any $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A}}}^{\Box})$:

  1. (1)

There exists a closed complete ${\mathrm{LK^{\prime}(A)}}$-tableau for
$\varphi$.

  2. (2)

$\vdash_{{\mathrm{{\mathrm{LK(A)}}}}}\varphi$.

  3. (3)

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

######  Proof 3.4.

(1) $\Rightarrow$ (2) $\Rightarrow$ (3) is just the combination of Lemma 5 and
Proposition 4. We prove (3) $\Rightarrow$ (1) by contraposition. If (1) fails,
then there is an open complete ${\mathrm{LK^{\prime}(A)}}$-tableau $T$
beginning with $[]>[(\varphi)^{1}],\ r12$. Let $e$ be a map satisfying the
system of inequations associated to a branch $B$ of $T$ and consider the
$e$-induced model $\mathfrak{M}=\langle W,R,V\rangle$ of $T$ by $B$. By Lemma
6, we obtain $0>e((\varphi)^{1})=V(\varphi,w_{1})$. Hence
$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

Let us remark here that there exist significant similarities between
${\mathrm{LK(A)}}$ and the tableau calculus given in [23] for the fuzzy
description logic “Łukasiewicz fuzzy $\mathcal{ALC}$”. Both calculi reduce the
validity of a formula to the satisfiability of linear programming problems,
using labels to record values of formulas at different worlds. Superficial
differences arise as a result of the restriction of values for Łukasiewicz
fuzzy $\mathcal{ALC}$ to the real unit interval $[0,1]$ and the use of several
modal operators (corresponding to roles in the description logic). More
significantly, roles in Łukasiewicz fuzzy $\mathcal{ALC}$ are interpreted by
fuzzy rather than crisp relations and appear also in inequations, whereas
${\mathrm{LK(A)}}$ proceeds by directly generating a crisp frame suitable for
constructing a potential countermodel.

###  3.4. Complexity

It follows directly from the completeness proof above that checking the
${\mathrm{K(A)}}$-validity of an $\mathcal{L}_{\mathrm{A}}^{\Box}$-formula
$\varphi$ is decidable. We simply apply the procedure for building a complete
${\mathrm{LK^{\prime}(A)}}$-tableau for $\varphi$ to generate finitely many
linear programming problems which can then be checked for satisfiability.
Considering this procedure in more detail, we obtain an upper bound for the
complexity of checking ${\mathrm{K(A)}}$-validity.

######  Theorem 8.

The problem of checking if $\varphi\in{\rm
Fm}(\mathcal{L}_{\mathrm{A}}^{\Box})$ is ${\mathrm{K(A)}}$-valid is in
coNEXPTIME.

######  Proof 3.5.

By Theorem 7, we may consider a complete ${\mathrm{LK^{\prime}(A)}}$-tableau
$T$ for an $\mathcal{L}_{\mathrm{A}}^{\Box}$-formula $\varphi$ obtained by
following steps (1)-(7) in the procedure above. We may also assume that no
labelled inequation appears twice on the same branch of $T$. Suppose that
$\varphi$ has complexity $n$. A new label $j$ is introduced by applying the
rule $(\triangleright\,\Box^{\prime})$ to a labelled inequation
$(\mathrm{\Gamma})^{\mathbf{k}}\triangleright(\Box\psi)^{i},(\mathrm{\Delta})^{\mathbf{l}}$,
and by step (4), producing a new labelled inequation
$(\lceil\Box\psi\rceil)^{i}\geq(\psi)^{j}$, where $\Box\psi$ is a subformula
of $\varphi$, and $\psi$ has smaller modal depth than $\Box\psi$. Note that
the number of subformulas $\Box\psi$ of $\varphi$ is bounded by $n$; also the
modal depth of $\varphi$ is bounded by $n$. Hence the number of labels
appearing on a branch of $T$ is at most exponential in $n$. Observe next that
the complexity of any labelled inequation that occurs in $T$ is bounded by
$n$, and that there are at most $n$ new variables of the form
$\lceil\Box\psi\rceil$ appearing in $T$. Hence the number of different
labelled inequations that can appear in $T$, and so also the length of any
branch of $T$, is at most exponential in $n$.

To show that $\varphi$ is not ${\mathrm{K(A)}}$-valid, we choose a branch $B$
of $T$ non-deterministically, noting that (binary) branching occurs only when
applying the rules $\lor$ and $\land$. By the above reasoning, the length of
$B$ and the complexity of the labelled inequations appearing on $B$ are at
most exponential in $n$. The result then follows from the fact that the linear
programming problem is in P [22].

It is no surprise that the upper bound provided here for checking
${\mathrm{K(A)}}$-validity matches the known upper bound for checking validity
in fuzzy description logics based on infinite-valued Łukasiewicz logic (see
[23]) and indeed also the Łukasiewicz modal logic described in Section 2. In
all these cases, unpacking the semantics leads to a non-deterministic guessing
of linear programming problems of exponential size in the complexity of the
original formula. Validity in modal or description logics based on finite
Łukasiewicz logics is known to be PSPACE-complete [4], and the same holds for
many-valued modal logics based on Gödel logics [6]; however, these arguments
do not seem to generalize to the current setting.

##  4\. The Modal-Multiplicative Fragment

In this section, we provide an axiom system (without infinitary rules) and
analytic sequent calculus for the modal-multiplicative fragment of
${\mathrm{K(A)}}$, and in doing so, take a first step towards obtaining such
systems for the full logic.

###  4.1. An Axiom System

$\begin{array}[]{rll}{\rm(B)}&&(\varphi\to\psi)\to((\psi\to\chi)\to(\varphi\to\chi))\\\\[1.8063pt]
{\rm(C)}&&(\varphi\to(\psi\to\chi))\to(\psi\to(\varphi\to\chi))\\\\[1.8063pt]
{\rm(I)}&&\varphi\to\varphi\\\\[1.8063pt]
{\rm(A)}&&((\varphi\to\psi)\to\psi)\to\varphi\\\\[1.8063pt]
{\rm(K)}&&\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi)\\\\[1.8063pt]
\textrm{(D${}_{n}$)}&&\Box(n\varphi)\to n\Box\varphi\qquad(n\geq
2)\\\\[1.8063pt] \end{array}$
$\psi\lx@proof@logical@and\varphi\varphi\to\psi\qquad\Box\varphi\varphi\qquad\varphi
n\varphi\quad(n\geq 2)$ Figure 3. The axiom system ${\mathrm{K(A_{m})}}$

For convenience (in particular, to reduce the number of cases in proofs), we
define the modal-multiplicative fragment here over a language
$\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$ consisting of the binary connective
$\to$ and unary connective $\Box$. To define further connectives, we fix
$p_{0}\in{\rm Var}$ and let

$\overline{0}:=p_{0}\to
p_{0},\quad\lnot\varphi:=\varphi\to\overline{0},\quad\varphi\&\psi:=\lnot\varphi\to\psi,\quad\text{and}\quad\Diamond\varphi:=\lnot\Box\lnot\varphi.$

We also define $0\varphi:=\overline{0}$ and
$(n+1)\varphi:=\varphi\&(n\varphi)$ for each $n\in\mathbb{N}$.

Our axiom system ${\mathrm{K(A_{m})}}$ for the modal-multiplicative fragment
of ${\mathrm{K(A)}}$ is presented in Figure 3. For a formula $\varphi\in{\rm
Fm}(\mathcal{L}_{\mathrm{A_{m}}}^{\Box})$, we write
$\vdash_{{\mathrm{K(A_{m})}}}\varphi$ if there exists a
${\mathrm{K(A_{m})}}$-derivation of $\varphi$, defined as usual as a finite
sequence of $\mathcal{L}_{\mathrm{A_{m}}}^{\Box}$-formulas that ends with
$\varphi$ and is constructed inductively using the axioms and rules of
${\mathrm{K(A_{m})}}$.

Establishing soundness for this system is straightforward. It is easily
checked that the axioms (B), (C), (I), (A), and (K) are valid in all
${\mathrm{K(A)}}$-models. For the less standard axioms (Dn) ($n\geq 2$), it
suffices to consider a ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle
W,R,V\rangle$ and $x\in W$, and observe that for all $\varphi\in{\rm
Fm}(\mathcal{L}_{\mathrm{A_{m}}}^{\Box})$,

$\begin{array}[]{rcl}V(\Box(n\varphi),x)&=&\bigwedge_{\mathbb{R}}\\{V(n\varphi,y):Rxy\\}\\\\[3.61371pt]
&=&\bigwedge_{\mathbb{R}}\\{nV(\varphi,y):Rxy\\}\\\\[3.61371pt]
&=&n\bigwedge_{\mathbb{R}}\\{V(\varphi,y):Rxy\\}\\\\[3.61371pt]
&=&V(n\Box\varphi,x).\end{array}$

It is clear that (mp) and (nec) preserve validity in ${\mathrm{K(A)}}$-models.
For (conn) ($n\geq 2$), we just note that if $V(n\varphi,x)\geq 0$ for a
${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle W,R,V\rangle$ and $x\in W$, then
$V(\varphi,x)\geq 0$. Hence a simple induction on the length of a
${\mathrm{K(A_{m})}}$-derivation gives the following result.

######  Proposition 9.

Let $\varphi\in{\rm Fm}(\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box})$. If
$\vdash_{{\mathrm{K(A_{m})}}}\varphi$, then
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

The proof of the converse direction is much harder. Before arriving finally at
this result in Theorem 19, we make a detour via a sequent calculus and exploit
the completeness result for our labelled tableau calculus provided by Theorem
7.

###  4.2. A Sequent Calculus

For the purposes of this paper, a sequent is an ordered pair of finite
multisets of $\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formulas
$\mathrm{\Gamma}$ and $\mathrm{\Delta}$, written
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$. A sequent rule is a set of
instances, each consisting of a finite set of sequents called premises and a
sequent called the conclusion. Such rules are typically written schematically,
using $\varphi,\psi,\chi$ and
$\mathrm{\Gamma},\mathrm{\Delta},\Pi,\mathrm{\Sigma}$ to denote arbitrary
formulas and finite multisets of formulas, respectively. We also often write
$\mathrm{\Gamma},\mathrm{\Delta}$ to denote the multiset union
$\mathrm{\Gamma}\uplus\mathrm{\Delta}$, $n\mathrm{\Gamma}$ for
$\mathrm{\Gamma},\ldots,\mathrm{\Gamma}$ ($n$ times), and
$\Box\mathrm{\Gamma}$ for $[\Box\varphi:\varphi\in\mathrm{\Gamma}]$.

We make use of a formula translation (assuming
$\varphi_{1}\&\ldots\&\varphi_{n}=\overline{0}$ for $n=0$),

$\begin{array}[]{rcl}\mathcal{I}(\varphi_{1},\ldots,\varphi_{n}\Rightarrow\psi_{1},\ldots,\psi_{m})&:=&(\varphi_{1}\&\ldots\&\varphi_{n})\to(\psi_{1}\&\ldots\&\psi_{m}),\end{array}$

and say that a sequent $\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ is
_${\mathrm{K(A)}}$ -valid_, written
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$,
if
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})$.

A sequent calculus ${\mathrm{GL}}$ consists of a set of sequent rules, and a
${\mathrm{GL}}$-derivation of a sequent $S$ from a set of sequents $Y$ is a
finite tree of sequents with root $S$ such that each node is either (i) a leaf
node and in $Y$, or (ii) together with its parent nodes forms an instance of a
rule of ${\mathrm{GL}}$. In this case, we write
$Y\vdash_{{\mathrm{{\mathrm{GL}}}}}S$ or just
$\vdash_{{\mathrm{{\mathrm{GL}}}}}S$ if $Y=\emptyset$. A sequent rule is
${\mathrm{GL}}$-derivable if there is a ${\mathrm{GL}}$-derivation of the
conclusion of any instance of the rule from its premises;
${\mathrm{GL}}$-admissible if whenever the premises of an instance of the rule
are ${\mathrm{GL}}$-derivable, the conclusion is ${\mathrm{GL}}$-derivable;
and ${\mathrm{GL}}$-invertible if whenever the conclusion of an instance of
the rule is ${\mathrm{GL}}$-derivable, the premises are
${\mathrm{GL}}$-derivable.

$\begin{array}[]{c}\begin{array}[]{ccc}\mathrm{\Delta}\Rightarrow\mathrm{\Delta}&&\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma},\varphi\Rightarrow\mathrm{\Delta}\Pi\Rightarrow\varphi,\mathrm{\Sigma}\\\\[10.84006pt]
\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}\Pi\Rightarrow\mathrm{\Sigma}&&\qquad\qquad\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}n\mathrm{\Gamma}\Rightarrow
n\mathrm{\Delta}\quad(n\geq 2)\\\\[10.84006pt]
\mathrm{\Gamma},\varphi\to\psi\Rightarrow\mathrm{\Delta}\mathrm{\Gamma},\psi\Rightarrow\varphi,\mathrm{\Delta}&&\mathrm{\Gamma}\Rightarrow\varphi\to\psi,\mathrm{\Delta}\mathrm{\Gamma},\varphi\Rightarrow\psi,\mathrm{\Delta}\\\\[10.84006pt]
\end{array}\\\ \Box\mathrm{\Gamma}\Rightarrow
n[\Box\varphi]\mathrm{\Gamma}\Rightarrow n[\varphi]\quad(n\geq 0)\end{array}$
Figure 4. The sequent calculus ${\mathrm{GK(A_{m})}}$

A sequent calculus ${\mathrm{GK(A_{m})}}$ for the modal-multiplicative
fragment of ${\mathrm{K(A)}}$, an extension of a calculus for the
multiplicative fragment of Abelian logic given in [29], is presented in Figure
4. Although only rules for $\to$ and $\Box$ appear in this system, the
following rules for other connectives are ${\mathrm{GK(A_{m})}}$-derivable:

$\begin{array}[]{ccc}\mathrm{\Gamma},\varphi\&\psi\Rightarrow\mathrm{\Delta}\mathrm{\Gamma},\varphi,\psi\Rightarrow\mathrm{\Delta}&&\mathrm{\Gamma}\Rightarrow\varphi\&\psi,\mathrm{\Delta}\mathrm{\Gamma}\Rightarrow\varphi,\psi,\mathrm{\Delta}\\\\[7.22743pt]
\mathrm{\Gamma},\lnot\varphi\Rightarrow\mathrm{\Delta}\mathrm{\Gamma}\Rightarrow\varphi,\mathrm{\Delta}&&\mathrm{\Gamma}\Rightarrow\lnot\varphi,\mathrm{\Delta}\mathrm{\Gamma},\varphi\Rightarrow\mathrm{\Delta}\\\\[7.22743pt]
\mathrm{\Gamma},\overline{0}\Rightarrow\mathrm{\Delta}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}&&\mathrm{\Gamma}\Rightarrow\overline{0},\mathrm{\Delta}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}\end{array}$

Below we provide a simple example of a ${\mathrm{GK(A_{m})}}$-derivation,
making use of the derived rules for $\&$ given above.

$\Rightarrow\Box(\varphi\&\varphi)\to(\Box\varphi\&\Box\varphi)\Box(\varphi\&\varphi)\Rightarrow\Box\varphi\&\Box\varphi\Box(\varphi\&\varphi)\Rightarrow\Box\varphi,\Box\varphi\varphi\&\varphi\Rightarrow\varphi,\varphi\varphi,\varphi\Rightarrow\varphi,\varphi$

Sequents of the form $\Rightarrow\Box(n\varphi)\to n\Box\varphi$ can be proved
similarly using the rule $(\Box_{n})$.

It is straightforward to establish an equivalence between derivability of a
sequent in ${\mathrm{GK(A_{m})}}$ and derivability of its formula
interpretation in the axiom system ${\mathrm{K(A_{m})}}$.

######  Proposition 10.

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$
if and only if
$\vdash_{{\mathrm{{\mathrm{K(A_{m})}}}}}\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})$.

######  Proof 4.1.

It suffices for the left-to-right direction to show that for any rule of
${\mathrm{GK(A_{m})}}$ with premises $S_{1},\ldots,S_{m}$ and conclusion $S$,
whenever $\vdash_{{\mathrm{{\mathrm{K(A_{m})}}}}}\mathcal{I}(S_{i})$ for each
$i\in\\{1,\ldots,m\\}$, also
$\vdash_{{\mathrm{{\mathrm{K(A_{m})}}}}}\mathcal{I}(S)$. For example, consider
the rule $(\Box_{n})$ and assume that
$\vdash_{{\mathrm{{\mathrm{K(A)}}}}}\mathcal{I}(\mathrm{\Gamma}\Rightarrow
n[\varphi])$. Suppose that $\mathrm{\Gamma}=[\psi_{1},\ldots,\psi_{m}]$ and
let $\psi=\psi_{1}\&\ldots\&\psi_{m}$. We continue the
${\mathrm{K(A_{m})}}$-derivation of $\mathcal{I}(\mathrm{\Gamma}\Rightarrow
n[\varphi])=\psi\to n\varphi$ to obtain a ${\mathrm{K(A_{m})}}$-derivation of
$\Box\psi\to n\Box\varphi$:

$\begin{array}[]{rll}1.&\psi\to n\varphi\\\ 2.&\Box(\psi\to
n\varphi)&(\text{nec})\\\ 3.&\Box(\psi\to n\varphi)\to(\Box\psi\to\Box
n\varphi)&\rm{(K)}\\\ 4.&\Box\psi\to\Box n\varphi&(\text{mp})\text{ with
2,3}\\\ 5.&\Box n\varphi\to n\Box\varphi&\textrm{(D${}_{n}$)}\\\
6.&(\Box\psi\to\Box n\varphi)\to((\Box n\varphi\to
n\Box\varphi)\to(\Box\psi\to n\Box\varphi))&\rm{(B)}\\\ 7.&(\Box n\varphi\to
n\Box\varphi)\to(\Box\psi\to n\Box\varphi)&(\text{mp})\text{ with 4,6}\\\
8.&\Box\psi\to n\Box\varphi&(\text{mp})\text{ with 5,7}.\end{array}$

$(\Box\psi_{1}\&\ldots\&\Box\psi_{m})\to\Box\psi$ is derivable using (B), (C),
(I), and (K), so, using (B) and (mp), we obtain a
${\mathrm{K(A_{m})}}$-derivation of
$\mathcal{I}(\Box\mathrm{\Gamma}\Rightarrow
n[\Box\varphi])=(\Box\psi_{1}\&\ldots\&\Box\psi_{m})\to n\Box\varphi$.

For the right-to-left direction, it is easy to show that every axiom of
${\mathrm{K(A_{m})}}$ is ${\mathrm{GK(A_{m})}}$-derivable; see, e.g., Example
4.2 for ${\mathrm{GK(A_{m})}}$-derivations of instances of (Dn). Also, the
rules of ${\mathrm{K(A_{m})}}$ are ${\mathrm{GK(A_{m})}}$-derivable. For
example, for $(\text{con}_{n})$, starting with $\Rightarrow n\varphi$, we
apply (cut) with the ${\mathrm{GK(A_{m})}}$-derivable sequent
$n\varphi\Rightarrow n[\varphi]$ to obtain $\Rightarrow n[\varphi]$ and then,
applying (scn), also $\Rightarrow\varphi$. Hence, if
$\vdash_{{\mathrm{{\mathrm{K(A_{m})}}}}}\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})$,
then
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\Rightarrow\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})$
and, applying (cut) with the ${\mathrm{GK(A_{m})}}$-derivable sequent
$\mathrm{\Gamma},\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})\Rightarrow\mathrm{\Delta}$,
also
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$.

We now consider a more complicated family of rules, indexed by
$k\in\mathbb{N}\setminus\\!\\{0\\}$ and $n\in\mathbb{N}$, that will be very
useful in subsequent cut-elimination and completeness proofs:

$\begin{array}[]{c}\mathrm{\Delta},\Box\mathrm{\Gamma}\Rightarrow\Box\varphi_{1},\ldots,\Box\varphi_{n},\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma}_{0}\Rightarrow\mathrm{\Gamma}_{1}\Rightarrow
k[\varphi_{1}]\ldots\mathrm{\Gamma}_{n}\Rightarrow
k[\varphi_{n}]\quad\text{where
}k\mathrm{\Gamma}=\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{n}.\end{array}$

Critically for our later considerations, $(\Box_{k,n})$ is
${\mathrm{GK(A_{m})}}$-derivable for all $k\in\mathbb{N}\setminus\\!\\{0\\}$,
$n\in\mathbb{N}$ (for $k=1$, omitting the application of (sck)):

$\mathrm{\Delta},\Box\mathrm{\Gamma}\Rightarrow\Box\varphi_{1},\ldots,\Box\varphi_{n},\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Delta}\Rightarrow\mathrm{\Delta}\Box\mathrm{\Gamma}\Rightarrow\Box\varphi_{1},\ldots,\Box\varphi_{n}\Box(\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{n})\Rightarrow
k[\Box\varphi_{1}],\ldots,k[\Box\varphi_{n}]\lx@proof@logical@and\Box\mathrm{\Gamma}_{0}\Rightarrow\mathrm{\Gamma}_{0}\Rightarrow\Box(\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{n})\Rightarrow
k[\Box\varphi_{1}],\ldots,k[\Box\varphi_{n}]\lx@proof@logical@and\Box\mathrm{\Gamma}_{1}\Rightarrow
k[\Box\varphi_{1}]\mathrm{\Gamma}_{1}\Rightarrow
k[\varphi_{1}]\vdots\Box\mathrm{\Gamma}_{n}\Rightarrow
k[\Box\varphi_{n}]\mathrm{\Gamma}_{n}\Rightarrow k[\varphi_{n}]$

We devote the remainder of this subsection to showing that the calculus
${\mathrm{GK(A_{m})}}$ admits cut-elimination. That is, we provide an
algorithm for constructively eliminating applications of the rule (cut) from
${\mathrm{GK(A_{m})}}$-derivations. Observe first that the “cancellation” rule

$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}\mathrm{\Gamma},\varphi\Rightarrow\varphi,\mathrm{\Delta}$

is both ${\mathrm{GK(A_{m})}}$-derivable and can be used, with (mix), to
derive (cut):

$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}\lx@proof@logical@and\varphi\to\varphi\Rightarrow\varphi\Rightarrow\varphi\mathrm{\Gamma}\Rightarrow\varphi\to\varphi,\mathrm{\Delta}\mathrm{\Gamma},\varphi\Rightarrow\varphi,\mathrm{\Delta}\qquad\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}\mathrm{\Gamma},\Pi,\varphi\Rightarrow\varphi,\mathrm{\Sigma},\mathrm{\Delta}\lx@proof@logical@and\mathrm{\Gamma},\varphi\Rightarrow\mathrm{\Delta}\Pi\Rightarrow\varphi,\mathrm{\Sigma}$

Hence, to prove cut-elimination, it will be enough to show constructively that
(can) is admissible in ${\mathrm{GK(A_{m})}}$ without (cut).

We begin by showing that every cut-free ${\mathrm{GK(A_{m})}}$-derivation can
be transformed into a derivation in a restricted calculus
${\mathrm{GK(A_{m})^{r}}}$ consisting only of the rules $(\textsc{id})$,
$(\to\Rightarrow)$, $(\Rightarrow\to)$, and $(\Box_{k,n})$
($k\in\mathbb{N}\setminus\\!\\{0\\}$, $n\in\mathbb{N}$).

######  Lemma 11.

The rules $(\to\Rightarrow)$ and $(\Rightarrow\to)$ are
${\mathrm{GK(A_{m})^{r}}}$-invertible.

######  Proof 4.2.

To show that $(\to\Rightarrow)$ is ${\mathrm{GK(A_{m})^{r}}}$-invertible, we
prove, more generally, that
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma},m[\varphi\to\psi]\Rightarrow\mathrm{\Delta}$
implies
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma},m\psi\Rightarrow
m\varphi,\mathrm{\Delta}$ for all $m\in\mathbb{N}$, proceeding by induction on
the height of a ${\mathrm{GK(A_{m})^{r}}}$-derivation of
$\mathrm{\Gamma},m[\varphi\to\psi]\Rightarrow\mathrm{\Delta}$. For the base
case, $\mathrm{\Delta}=\mathrm{\Gamma}\uplus m[\varphi\to\psi]$ and it
suffices to observe that
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma},m\psi\Rightarrow
m\varphi,m[\varphi\to\psi],\mathrm{\Gamma}$. For the inductive step, we
observe that when the last rule applied is $(\to\Rightarrow)$ or
$(\Rightarrow\to)$, the claim follows immediately by applying the induction
hypothesis and, where necessary, the relevant rule. If the last rule applied
is $(\Box_{k,n})$, then $m[\varphi\to\psi]$ must occur also on the right of
the sequent and the claim follows by first applying the rule $(\Box_{k,n})$
and then $(\Rightarrow\to)$ $m$ times. The proof that $(\Rightarrow\to)$ is
${\mathrm{GK(A_{m})^{r}}}$-invertible is very similar.

######  Lemma 12.

The rules (mix) and (scn) are ${\mathrm{GK(A_{m})^{r}}}$-admissible.

######  Proof 4.3.

To show the ${\mathrm{GK(A_{m})^{r}}}$-admissibility of (mix), we prove that

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}\
\text{ and }\
\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\Pi\Rightarrow\mathrm{\Sigma}\quad\Longrightarrow\quad\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}r\mathrm{\Gamma},s\Pi\Rightarrow
s\mathrm{\Sigma},r\mathrm{\Delta}\ \text{ for all }r,s\in\mathbb{N},$

proceeding by induction on the sum of the heights of
${\mathrm{GK(A_{m})^{r}}}$-derivations $d_{1}$ and $d_{2}$ of
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ and
$\Pi\Rightarrow\mathrm{\Sigma}$, respectively.

For the base case, if $d_{1}$ and $d_{2}$ have height $0$, then
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ and
$\Pi\Rightarrow\mathrm{\Sigma}$ are instances of $(\textsc{id})$, i.e.,
$\mathrm{\Gamma}=\mathrm{\Delta}$ and $\Pi=\mathrm{\Sigma}$. So
$r\mathrm{\Gamma}\uplus s\Pi=r\mathrm{\Delta}\uplus s\mathrm{\Sigma}$ and
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}r\mathrm{\Gamma},s\Pi\Rightarrow
s\mathrm{\Sigma},r\mathrm{\Delta}$ by $(\textsc{id})$. If the last application
of a rule in $d_{1}$ or $d_{2}$ is $(\to\Rightarrow)$ or $(\Rightarrow\to)$,
then the result follows easily by an application of the induction hypothesis
and further applications of the rule.

Suppose now that $d_{1}$ ends with

$\begin{array}[]{c}\Omega,\Box\mathrm{\Gamma}^{\prime}\Rightarrow\Box\varphi_{1},\ldots,\Box\varphi_{n},\Omega\lx@proof@logical@and\mathrm{\Gamma}_{0}\Rightarrow\mathrm{\Gamma}_{1}\Rightarrow
k[\varphi_{1}]\ldots\mathrm{\Gamma}_{n}\Rightarrow
k[\varphi_{n}]\quad\text{where
}k\mathrm{\Gamma}^{\prime}=\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{n}.\end{array}$

If $d_{2}$ has height $0$, then $\Pi=\mathrm{\Sigma}$. An application of the
induction hypothesis to the ${\mathrm{GK(A_{m})^{r}}}$-derivation of the
premise $\mathrm{\Gamma}_{0}\Rightarrow$ together with a
${\mathrm{GK(A_{m})^{r}}}$-derivation of the empty sequent $\Rightarrow$ of
height $0$ yields
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}r\mathrm{\Gamma}_{0}\Rightarrow$.
It follows then that the sequent
$r\Omega,r\Box\mathrm{\Gamma}^{\prime},s\Pi\Rightarrow
s\Pi,r\Box\varphi_{1},\ldots,r\Box\varphi_{n},r\Omega$ is
${\mathrm{GK(A_{m})^{r}}}$-derivable using an application of the rule
$(\Box_{k,rn})$. The case where $d_{1}$ has height $0$ and $d_{2}$ ends with
$(\Box_{k,n})$ is symmetrical.

If $d_{2}$ ends with

$\begin{array}[]{c}\Theta,\Box\Pi^{\prime}\Rightarrow\Box\psi_{1},\ldots,\Box\psi_{m},\Theta\lx@proof@logical@and\Pi_{0}\Rightarrow\Pi_{1}\Rightarrow
l[\psi_{1}]\ldots\Pi_{m}\Rightarrow l[\psi_{m}]\quad\text{where
}l\Pi^{\prime}=\Pi_{0}\uplus\Pi_{1}\uplus\ldots\uplus\Pi_{m},\end{array}$

then we obtain the required ${\mathrm{GK(A_{m})^{r}}}$-derivation

$r\Omega,s\Theta,r\Box\mathrm{\Gamma}^{\prime},s\Box\Pi^{\prime}\Rightarrow
r\Box\varphi_{1},\ldots,r\Box\varphi_{n},s\Box\psi_{1},\ldots,s\Box\psi_{m},r\Omega,s\Theta\lx@proof@logical@and
rl\mathrm{\Gamma}_{0},sk\Pi_{0}\Rightarrow\\{l\mathrm{\Gamma}_{i}\Rightarrow
kl[\varphi_{i}]\\}_{i\in\\{1,\ldots,n\\}}\\{k\Pi_{j}\Rightarrow
kl[\psi_{j}]\\}_{1\leq j\leq m}$

where the premises are all ${\mathrm{GK(A_{m})^{r}}}$-derivable using the
induction hypothesis.

We establish the ${\mathrm{GK(A_{m})^{r}}}$-admissibility of (scn) by proving
that

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}n\mathrm{\Gamma}\Rightarrow
n\mathrm{\Delta}\quad\Longrightarrow\quad\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta},$

proceeding by induction on the sum of the complexities of the formulas in
$\mathrm{\Gamma},\mathrm{\Delta}$. For the base case, if
$n\mathrm{\Gamma}=n\mathrm{\Delta}$ (in particular if $\mathrm{\Gamma}$ and
$\mathrm{\Delta}$ contain only variables), then
$\mathrm{\Gamma}=\mathrm{\Delta}$ and
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$
by $(\textsc{id})$. If $\mathrm{\Gamma}$ contains a formula $\varphi\to\psi$,
then by the invertibility of the rule $(\to\Rightarrow)$ established in Lemma
11,
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}n(\mathrm{\Gamma}-[\varphi\to\psi]),n\psi\Rightarrow
n\varphi,n\mathrm{\Delta}$. The induction hypothesis and an application of
$(\to\Rightarrow)$ gives
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$.
The case where $\mathrm{\Delta}$ contains a formula $\varphi\to\psi$ is
symmetrical. In the final case, the ${\mathrm{GK(A_{m})^{r}}}$-derivation of
$n\mathrm{\Gamma}\Rightarrow n\mathrm{\Delta}$ must end with an application of
$(\Box_{k,nl})$ where $\mathrm{\Gamma}=\Pi\uplus[\Box\mathrm{\Sigma}]$ and
$\mathrm{\Delta}=\Pi\uplus[\Box\varphi_{1},\ldots,\Box\varphi_{l}]$. Hence
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$
using $(\Box_{kn,l})$ and the ${\mathrm{GK(A_{m})^{r}}}$-admissibility of
(mix).

We now have all the necessary tools to prove the promised cut-elimination
theorem.

######  Theorem 13.

${\mathrm{GK(A_{m})}}$ admits cut-elimination.

######  Proof 4.4.

To establish cut-elimination for ${\mathrm{GK(A_{m})}}$, it suffices to prove
that an uppermost application of (cut) in a ${\mathrm{GK(A_{m})}}$-derivation
can be eliminated; that is, we show that cut-free
${\mathrm{GK(A_{m})}}$-derivations of the premises of an instance of (cut) can
be transformed into a cut-free ${\mathrm{GK(A_{m})}}$-derivation of the
conclusion. Observe first that the rule $(\Box_{n})$ is
${\mathrm{GK(A_{m})^{r}}}$-derivable using $(\Box_{k,n})$ with $k=n$,
$\varphi_{1}=\ldots=\varphi_{n}=\varphi$, and
$\mathrm{\Gamma}_{1}=\ldots=\mathrm{\Gamma}_{n}=\mathrm{\Gamma}$. Hence, the
proof of Lemma 12 shows that any cut-free ${\mathrm{GK(A_{m})}}$-derivation
can be transformed algorithmically into a
${\mathrm{GK(A_{m})^{r}}}$-derivation. We prove (constructively) that

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma},\varphi\Rightarrow\varphi,\mathrm{\Delta}\quad\Longrightarrow\quad\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}.\qquad(\star)$

Suppose then that there are cut-free ${\mathrm{GK(A_{m})}}$-derivations of the
premises $\mathrm{\Gamma},\varphi\Rightarrow\mathrm{\Delta}$ and
$\Pi\Rightarrow\varphi,\mathrm{\Sigma}$ of an uppermost application of (cut).
By (mix), we obtain a cut-free ${\mathrm{GK(A_{m})}}$-derivation of
$\mathrm{\Gamma},\Pi,\varphi\Rightarrow\varphi,\mathrm{\Sigma},\mathrm{\Delta}$
and hence a ${\mathrm{GK(A_{m})^{r}}}$-derivation of this sequent. By
$(\star)$, we obtain a ${\mathrm{GK(A_{m})^{r}}}$-derivation of
$\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}$, which also
gives the desired cut-free ${\mathrm{GK(A_{m})}}$-derivation.

We prove $(\star)$ by induction on the lexicographically ordered pair
consisting of the modal depth of $\varphi$ and the sum of the complexities of
the formulas in $\mathrm{\Gamma},\varphi\Rightarrow\varphi,\mathrm{\Delta}$.
If $\mathrm{\Gamma}\uplus[\varphi]=[\varphi]\uplus\mathrm{\Delta}$, then
$\mathrm{\Gamma}=\mathrm{\Delta}$ and
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ is derivable using
$(\textsc{id})$. If $\varphi$ has the form $\psi\to\chi$, then we use the
${\mathrm{GK(A_{m})^{r}}}$-invertibility of $(\to\Rightarrow)$ and
$(\Rightarrow\to)$ and apply the induction hypothesis twice. The cases where
$\mathrm{\Gamma}$ or $\mathrm{\Delta}$ includes a formula $\psi\to\chi$ are
very similar. Lastly, suppose that
$\mathrm{\Gamma},\varphi\Rightarrow\varphi,\mathrm{\Delta}$ contains only
variables and box formulas. Then there is a ${\mathrm{GK(A_{m})}}$-derivation
of the sequent ending with an application of $(\Box_{k,n})$. The case where
$\varphi$ is a variable is trivial, so let us just consider the case where
$\varphi=\Box\chi$ and the derivation ends with an application of
$(\Box_{k,n})$. The case where $\varphi$ occurs in the context appearing on
both sides of the conclusion follows immediately, so suppose that the
derivation ends with

$\mathrm{\Sigma},\Box\Pi,\Box\chi\Rightarrow\Box\chi,\Box\psi_{2},\ldots,\Box\psi_{n},\mathrm{\Sigma}\lx@proof@logical@and\Pi_{0},k_{0}[\chi]\Rightarrow\Pi_{1},k_{1}[\chi]\Rightarrow
k[\chi]\\{\Pi_{i},k_{i}[\chi]\Rightarrow k[\psi_{i}]\\}_{i=2}^{n}$

where $k\Pi=\Pi_{0}\uplus\Pi_{1}\uplus\ldots\uplus\Pi_{n}$ and
$k=k_{0}+k_{1}+\ldots+k_{n}$. By the induction hypothesis,

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})^{r}}}}}}\Pi_{1}\Rightarrow(k-k_{1})[\chi].$

By Lemma 12 (the ${\mathrm{GK(A_{m})^{r}}}$-admissibility of (mix)), we have
${\mathrm{GK(A_{m})^{r}}}$-derivations of

$\begin{array}[]{l}k_{0}\Pi_{1},(k-k_{1})\Pi_{0},(k-k_{1})k_{0}[\chi]\Rightarrow(k-k_{1})k_{0}[\chi]\\\\[1.8063pt]
k_{i}\Pi_{1},(k-k_{1})\Pi_{i},(k-k_{1})k_{i}[\chi]\Rightarrow(k-k_{1})k_{i}[\chi],(k-k_{1})k[\psi_{i}]\quad\text{for
}i\in\\{2,\ldots,n\\}.\end{array}$

So, by the induction hypothesis, we have
${\mathrm{GK(A_{m})^{r}}}$-derivations of

$\begin{array}[]{l}k_{0}\Pi_{1},(k-k_{1})\Pi_{0}\Rightarrow\\\\[1.8063pt]
k_{i}\Pi_{1},(k-k_{1})\Pi_{i}\Rightarrow(k-k_{1})k[\psi_{i}]\quad\text{for
}i\in\\{2,\ldots,n\\}.\end{array}$

Now by an application of $(\Box_{(k-k_{1})k,n-1})$, we have a
${\mathrm{GK(A_{m})^{r}}}$-derivation ending with

$\mathrm{\Sigma},\Box\Pi\Rightarrow\Box\psi_{2},\ldots,\Box\psi_{n},\mathrm{\Sigma}\lx@proof@logical@and
k_{0}\Pi_{1},(k-k_{1})\Pi_{0}\Rightarrow\\{k_{i}\Pi_{1},(k-k_{1})\Pi_{i}\Rightarrow(k-k_{1})k[\psi_{i}]\\}_{i=2}^{n}$

where
$(k-k_{1})k\Pi=(k_{0}+k_{2}+\ldots+k_{n})(\Pi_{0}\uplus\Pi_{1}\uplus\ldots\uplus\Pi_{n})$.

###  4.3. Completeness

In this section we establish the completeness of both the axiom system
${\mathrm{K(A_{m})}}$ and the sequent calculus ${\mathrm{GK(A_{m})}}$ for the
modal-multiplicative fragment of ${\mathrm{K(A)}}$. The crucial ingredient of
our proof will be the fact that an ${\mathrm{LK^{\prime}(A)}}$-tableau for an
$\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formula always consists of just one
branch, and hence a single inconsistent system of linear inequations can be
associated with each valid $\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formula.

We begin by proving two lemmas for ${\mathrm{K(A)}}$-valid sequents of a
certain form, recalling that sequents contain only
$\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formulas by definition.

######  Lemma 14.

Let $\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}$ be a
${\mathrm{K(A)}}$-valid sequent such that no variable occurs in both
$\mathrm{\Gamma}\uplus\mathrm{\Delta}$ and $\Pi\uplus\mathrm{\Sigma}$. Then
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ and
$\Pi\Rightarrow\mathrm{\Sigma}$ are both ${\mathrm{K(A)}}$-valid.

######  Proof 4.5.

Suppose contrapositively that
$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$.
Then there exists a ${\mathrm{K(A)}}$-model $\mathfrak{M}=\langle
W,R,V\rangle$ and $x\in W$ such that
$V(\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}),x)<0$. Since
$\mathrm{\Gamma}\uplus\mathrm{\Delta}$ and $\Pi\uplus\mathrm{\Sigma}$ have
disjoint sets of variables, we may assume without loss of generality that
$V(p,y)=0$ for all $p\in{\rm Var}$ occurring in $\Pi\uplus\mathrm{\Sigma}$ and
$y\in W$. A simple induction yields also that $V(\varphi,y)=0$ for all
$\varphi\in\Pi\uplus\mathrm{\Sigma}$ and $y\in W$. But then
$V(\mathcal{I}(\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}),x)<0$.
So
$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\mathrm{\Delta}$.
The case where
$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\Pi\Rightarrow\mathrm{\Sigma}$
follows by symmetry.

######  Lemma 15.

Let $\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\mathrm{\Delta}$ be
a ${\mathrm{K(A)}}$-valid sequent such that $\Pi$ and $\mathrm{\Sigma}$
contain only variables. Then $\Pi=\mathrm{\Sigma}$ and
$\Box\mathrm{\Gamma}\Rightarrow\Box\mathrm{\Delta}$ is
${\mathrm{K(A)}}$-valid.

######  Proof 4.6.

Suppose that
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\mathrm{\Delta}$.
It suffices to show that $\Pi=\mathrm{\Sigma}$, since then clearly also
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\mathrm{\Gamma}\Rightarrow\Box\mathrm{\Delta}$.
Suppose for a contradiction that $\Pi\not=\mathrm{\Sigma}$. Without loss of
generality, some $p\in{\rm Var}$ occurs strictly more times in $\Pi$ than
$\mathrm{\Sigma}$. Consider a ${\mathrm{K(A)}}$-model
$\mathfrak{M}=\langle\\{x\\},\emptyset,V\rangle$ with one irreflexive world
$x$ satisfying $V(p,x)=1$ and $V(q,x)=0$ for all $q\in{\rm
Var}\setminus\\{p\\}$. Then
$V(\mathcal{I}(\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\mathrm{\Delta}),x)<0$
and so
$\not\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\mathrm{\Delta}$,
a contradiction.

To deal with ${\mathrm{K(A)}}$-valid sequents in general, we use the fact that
for such a sequent, there must exist a corresponding closed complete
${\mathrm{LK^{\prime}(A)}}$-tableau with one branch and an associated
inconsistent set of inequations. We use this set of inequations to show that
the rule $(\Box_{k,m})$ for suitable $k,m$ can be applied backwards to the
sequent to obtain ${\mathrm{K(A)}}$-valid sequents containing formulas of
strictly smaller modal depth. To this end, it will be helpful to extend some
of the notions for the labelled tableau calculus ${\mathrm{LK^{\prime}(A)}}$
to sequents. We define a complete ${\mathrm{LK^{\prime}(A)}}$-tableau for a
sequent $\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ to be a tableau beginning
with the active inequation $(\mathrm{\Gamma})^{1}>(\mathrm{\Delta})^{1}$ and
relation $r12$, constructed according to steps (2)–(7). Consulting the proof
of Theorem 7, we obtain the following result.

######  Corollary 16.

There exists a closed complete ${\mathrm{LK^{\prime}(A)}}$-tableau for a
sequent $\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ if and only if
$\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ is ${\mathrm{K(A)}}$-valid.

To argue about the inconsistency of a system of inequations associated to a
tableau, we recall some basic notions from linear programming. Let $S$ be a
system of inequations of the form $I_{i}=(f_{i}(\bar{x})>g_{i}(\bar{x}))$
($i\in\\{1,\ldots,n\\}$) and $J_{j}=(h_{j}(\bar{x})\geq k_{j}(\bar{x}))$
($j\in\\{1,\ldots,m\\}$) where each $f_{i},g_{i},h_{j},k_{j}$ is a positive
linear sum of variables in $\bar{x}$. Then $S$ is inconsistent over
$\mathbb{R}$ if and only if there exists an inequation given by a linear
combination of these inequations

$\begin{array}[]{rcl}L_{S}&=&\sum_{i=1}^{n}\lambda_{i}I_{i}+\sum_{j=1}^{m}\mu_{j}J_{j}\end{array}$

where $\lambda_{1},\ldots,\lambda_{n}\in\mathbb{N}$ (not all zero) and
$\mu_{1},\ldots,\mu_{m}\in\mathbb{N}$ such that

$\begin{array}[]{rcl}\lambda_{1}f_{1}+\ldots+\lambda_{n}f_{n}+\mu_{1}h_{1}+\ldots+\mu_{m}h_{m}&=&\lambda_{1}g_{1}+\ldots+\lambda_{n}g_{n}+\mu_{1}k_{1}+\ldots+\mu_{m}k_{m}.\end{array}$

We say that $L_{S}$ is inconsistent and that each inequation
$f_{i}(\bar{x})>g_{i}(\bar{x})$ or $h_{j}(\bar{x})\geq k_{j}(\bar{x})$ is used
$\lambda_{i}$ or $\mu_{j}$ times, respectively, in $L_{S}$.

Given a labelled inequation
$I=(\mathrm{\Gamma}_{1})^{\mathbf{k_{1}}}\triangleright(\mathrm{\Delta}_{1})^{\mathbf{l_{1}}}$,
let
$I^{E}=(\mathrm{\Gamma}_{2})^{\mathbf{k_{2}}}\triangleright(\mathrm{\Delta}_{2})^{\mathbf{l_{2}}}$
be the inequation obtained by applying the rules for $\to$ in
${\mathrm{LK^{\prime}(A)}}$ to $I$ exhaustively. By further replacing each
boxed formula $\Box\varphi$ with $\lceil\Box\varphi\rceil$, we obtain the
_reduced form_ $I^{R}$ of $I$, saying that $I$ is _in reduced form_ if
$I=I^{R}$. We now have all the required tools to prove our main lemma.

######  Lemma 17.

Let $\Box\mathrm{\Gamma}\Rightarrow\Box\psi_{1},\ldots,\Box\psi_{m}$ be a
${\mathrm{K(A)}}$-valid sequent. Then there exist
$k\in\mathbb{N}\setminus\\!\\{0\\}$ and multisets of
$\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formulas
$\mathrm{\Gamma}_{0},\mathrm{\Gamma}_{1},\ldots,\mathrm{\Gamma}_{m}$ such that

  1. (i)

$k\mathrm{\Gamma}=\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{m}$

  2. (ii)

$\mathrm{\Gamma}_{0}\Rightarrow$ and $\mathrm{\Gamma}_{i}\Rightarrow
k[\psi_{i}]$ for $i\in\\{1,\ldots,m\\}$ are all ${\mathrm{K(A)}}$-valid.

######  Proof 4.7.

Let $\mathrm{\Gamma}=[\varphi_{1},\ldots,\varphi_{n}]$. By assumption,
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\varphi_{1},\ldots,\Box\varphi_{n}\Rightarrow\Box\psi_{1},\ldots,\Box\psi_{m}$,
and, by Corollary 16, we obtain a complete closed tableau $T$ in
${\mathrm{LK^{\prime}(A)}}$ that begins with

$({\Box\varphi_{1}})^{1},\ldots,({\Box\varphi_{n}})^{1}>({\Box\psi_{1}})^{1},\ldots,({\Box\psi_{m}})^{1}\quad\text{and}\quad
r12.$

This tableau will contain the inequation

$\begin{array}[]{rcl}I&=&(\lceil\Box\varphi_{1}\rceil)^{1},\ldots,(\lceil\Box\varphi_{n}\rceil)^{1}>(\lceil\Box\psi_{1}\rceil)^{1},\ldots,(\lceil\Box\psi_{m}\rceil)^{1}\end{array}$

and for new labels $y_{1},\ldots,y_{m}\in\mathbb{N}$, the inequations

$\begin{array}[]{rclcrcl}I_{1}&=&(\lceil\Box\psi_{1}\rceil)^{1}\geq(\psi_{1})^{y_{1}}&\quad\ldots&I_{m}&=&(\lceil\Box\psi_{m}\rceil)^{1}\geq(\psi_{m})^{y_{m}}.\end{array}$

Let us fix $y_{0}=2$. Then $T$ contains for each $i\in\\{1,\ldots,n\\}$ and
$j\in\\{0,\ldots,m\\}$, an inequation

$\begin{array}[]{rcl}I_{i,j}&=&(\varphi_{i})^{y_{j}}\geq(\lceil\Box\varphi_{i}\rceil)^{1}.\end{array}$

Consider now the set of inequations associated to $T$

$\begin{array}[]{rcl}S&=&\\{I\\}\cup\\{I_{j}^{R}:1\leq j\leq
m\\}\cup\\{I_{ij}^{R}:1\leq i\leq n,\,0\leq j\leq m\\}\cup
S^{\prime},\end{array}$

noting that the inequations in $S^{\prime}$ are obtained by applying rules of
${\mathrm{LK^{\prime}(A)}}$ to inequations in $\\{I_{j}^{E}:1\leq j\leq
m\\}\cup\\{I_{ij}^{E}:1\leq i\leq n,\,0\leq j\leq m\\}$. Since $T$ is closed,
$S$ is inconsistent over $\mathbb{R}$. Hence there is an inconsistent linear
combination $L_{S}$ of the inequations in $S$. The following observations can
be confirmed by simple inductions on the height of $T$:

  1. (i)

The (reduced form) inequation $I$ is the only strict inequation occurring in
$S$, and hence must be used $k$ times in $L_{S}$ for some
$k\in\mathbb{N}\setminus\\!\\{0\\}$.

  2. (ii)

For each $j\in\\{1,\ldots,m\\}$, $(\lceil\Box\psi_{j}\rceil)^{1}$ occurs in
$S$ only in $I$ and in the reduced form $I_{j}^{R}$ of $I_{j}$; hence, by (i),
$I_{j}^{R}$ must also be used $k$ times in $L_{S}$.

  3. (iii)

For each $i\in\\{1,\ldots,n\\}$, $(\lceil\Box\varphi_{i}\rceil)^{1}$ occurs in
$S$ only in $I$ and in the reduced forms $I_{i,j}^{R}$ of $I_{i,j}$ for
$j\in\\{0,\ldots,m\\}$; hence, given that $I_{i,j}^{R}$ is used in the linear
combination $\lambda_{i,j}$ times, we obtain
$\lambda_{i,0}+\lambda_{i,1}+\ldots+\lambda_{i,m}=k$; in particular, not all
$\lambda_{i,j}$ are zero.

The inconsistent linear combination of the inequations in $S$ is therefore

$\begin{array}[]{rcl}L_{S}&=&kI+\sum_{j=1}^{m}kI^{R}_{j}+\sum_{i=1}^{n}\sum_{j=0}^{m}\lambda_{i,j}I^{R}_{i,j}+L_{S^{\prime}}.\end{array}$

We define multisets of formulas

$\begin{array}[]{rcl}\mathrm{\Gamma}_{j}&=&\lambda_{1,j}[\varphi_{1}],\ldots,\lambda_{n,j}[\varphi_{n}]\
\text{ for $j\in\\{0,\ldots,m\\}$}\\\\[3.61371pt]
\mathrm{\Delta}&=&k[\lceil\Box\varphi_{1}\rceil],\ldots,k[\lceil\Box\varphi_{n}\rceil],k[\lceil\Box\psi_{1}\rceil],\ldots,k[\lceil\Box\psi_{m}\rceil].\end{array}$

Note that, as required,
$k\mathrm{\Gamma}=\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{m}$.
Consider now the inequation

$\begin{array}[]{rcl}J&=&kI+\sum_{j=1}^{m}kI_{j}+\sum_{i=1}^{n}\sum_{j=0}^{m}\lambda_{i,j}I_{i,j}\\\\[3.61371pt]
&=&(\mathrm{\Gamma}_{0})^{y_{0}},(\mathrm{\Gamma}_{1})^{y_{1}},\ldots,(\mathrm{\Gamma}_{m})^{y_{m}},(\mathrm{\Delta})^{1}>(\mathrm{\Delta})^{1},k[(\psi_{1})^{y_{1}}],\ldots,k[(\psi_{m})^{y_{m}}].\end{array}$

Then $L_{S}=J^{R}+L_{S^{\prime}}$ and the set of inequations
$S^{*}=\\{J^{R}\\}\cup S^{\prime}$ is inconsistent over $\mathbb{R}$.

Recall that each (reduced form) inequation in $S^{\prime}$ is obtained by
applying rules of ${\mathrm{LK^{\prime}(A)}}$ to the inequations
$\\{I_{j}^{E}:1\leq j\leq m\\}\cup\\{I_{ij}^{E}:1\leq i\leq n,\,0\leq j\leq
m\\}$. But following the procedure for building a complete
${\mathrm{LK^{\prime}(A)}}$-tableau, the inequations in $S^{\prime}$ are
obtained by first applying the rules $(\Box\,\triangleright^{\prime})$ and
$(\triangleright\,\Box^{\prime})$. Hence these inequations in $S^{\prime}$ and
$J^{R}$ are also obtained by first applying the rules
$(\Box\,\triangleright^{\prime})$ and $(\triangleright\,\Box^{\prime})$ to
$J^{E}$ and then continuing as before.

Now for each $j\in\\{0,\ldots,m\\}$, let ${\rm Var}_{j}\subseteq{\rm Var}$ be
a countably infinite set such that ${\rm Var}_{0}\cap{\rm
Var}_{1}\cap\ldots\cap{\rm Var}_{m}=\emptyset$, and let $h_{j}\colon{\rm
Var}\to{\rm Var}_{j}$ be a bijective map that extends in the obvious way to
all formulas and multisets of formulas. Consider the inequation

$\begin{array}[]{rcl}J^{\prime}&=&(h_{0}(\mathrm{\Gamma}_{0}))^{1},(h_{1}(\mathrm{\Gamma}_{1}))^{1},\ldots,(h_{m}(\mathrm{\Gamma}_{m}))^{1},(\mathrm{\Delta})^{1}>(\mathrm{\Delta})^{1},k[(h_{1}(\psi_{1}))^{1}],\ldots,k[(h_{m}(\psi_{m}))^{1}].\end{array}$

An easy induction on the height of a tableau shows that applying the rules of
${\mathrm{LK^{\prime}(A)}}$ to $J^{\prime}$ and relation $r12$ also produces a
set of inequations that is inconsistent over $\mathbb{R}$. But then by
Corollary 16,

$\models_{{\mathrm{{\mathrm{K(A)}}}}}h_{0}(\mathrm{\Gamma}_{0}),h_{1}(\mathrm{\Gamma}_{1}),\ldots,h_{m}(\mathrm{\Gamma}_{m}),\mathrm{\Delta}\Rightarrow\mathrm{\Delta},k[h_{1}(\psi_{1})],\ldots,k[h_{m}(\psi_{m})].$

Applying Lemma 14 repeatedly, we obtain

$\models_{{\mathrm{{\mathrm{K(A)}}}}}h_{0}(\mathrm{\Gamma}_{0})\Rightarrow\quad\text{
and
}\quad\models_{{\mathrm{{\mathrm{K(A)}}}}}h_{i}(\mathrm{\Gamma}_{i})\Rightarrow
k[h_{i}(\psi_{i})]\,\text{ for }i\in\\{1,\ldots,m\\},$

and hence, renaming variables,

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}_{0}\Rightarrow\quad\text{
and }\quad\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}_{i}\Rightarrow
k[\psi_{i}]\,\text{ for }i\in\\{1,\ldots,m\\}$

as required.

######  Proposition 18.

Let $\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$ be a ${\mathrm{K(A)}}$-valid
sequent. Then
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$.

######  Proof 4.8.

We prove the claim by induction on the lexicographically ordered pair
consisting of the modal depth of
$\mathcal{I}(\mathrm{\Gamma}\Rightarrow\mathrm{\Delta})$ and the sum of the
complexities of the formulas in $\mathrm{\Gamma}\uplus\mathrm{\Delta}$.

For the base case, suppose that
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$
and that both $\mathrm{\Gamma}$ and $\mathrm{\Delta}$ contain only variables.
Then, by Lemma 15, we obtain $\mathrm{\Gamma}=\mathrm{\Delta}$. Hence, by
$(\textsc{id})$, we get
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}\Rightarrow\mathrm{\Delta}$.

For the inductive step, suppose first that
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma},\varphi\to\psi\Rightarrow\mathrm{\Delta}$.
Then also
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma},\psi\Rightarrow\varphi,\mathrm{\Delta}$.
So by the induction hypothesis,
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma},\psi\Rightarrow\varphi,\mathrm{\Delta}$.
Hence, by $(\to\Rightarrow)$, we get
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma},\varphi\to\psi\Rightarrow\mathrm{\Delta}$.
The case where $\varphi\to\psi$ occurs on the right is very similar.

Now suppose that
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\psi_{1},\ldots,\Box\psi_{m}$
where $\Pi$ and $\mathrm{\Sigma}$ contain only variables. By Lemma 15, we
obtain $\Pi=\mathrm{\Sigma}$ and
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\Box\mathrm{\Gamma}\Rightarrow\Box\psi_{1},\ldots,\Box\psi_{m}$.
By $(\textsc{id})$, we get
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\Pi\Rightarrow\mathrm{\Sigma}$.
Moreover, by Lemma 17, there exist $k\in\mathbb{N}\setminus\\!\\{0\\}$ and
multisets of $\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formulas
$\mathrm{\Gamma}_{0},\mathrm{\Gamma}_{1},\ldots,\mathrm{\Gamma}_{m}$ such that

  1. (i)

$k\mathrm{\Gamma}=\mathrm{\Gamma}_{0}\uplus\mathrm{\Gamma}_{1}\uplus\ldots\uplus\mathrm{\Gamma}_{m}$

  2. (ii)

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}_{0}\Rightarrow$ and
$\models_{{\mathrm{{\mathrm{K(A)}}}}}\mathrm{\Gamma}_{i}\Rightarrow
k[\psi_{i}]$ for $i\in\\{1,\ldots,m\\}$.

But then by the induction hypothesis also

  1. (iii)

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}_{0}\Rightarrow$ and
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\mathrm{\Gamma}_{i}\Rightarrow
k[\psi_{i}]$ for $i\in\\{1,\ldots,m\\}$.

Hence, using the ${\mathrm{GK(A_{m})}}$-derivable rule $(\Box_{k,m})$, we
obtain
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\Box\mathrm{\Gamma}\Rightarrow\Box\psi_{1},\ldots,\Box\psi_{m}$.
Finally, using (mix), we obtain
$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\Box\mathrm{\Gamma},\Pi\Rightarrow\mathrm{\Sigma},\Box\psi_{1},\ldots,\Box\psi_{m}$
as required.

Our main theorem now follows as a direct combination of Propositions 9, 10,
and 18.

######  Theorem 19.

The following are equivalent for any $\varphi\in{\rm
Fm}(\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box})$:

  1. (1)

$\models_{{\mathrm{{\mathrm{K(A)}}}}}\varphi$.

  2. (2)

$\vdash_{{\mathrm{K(A_{m})}}}\varphi$.

  3. (3)

$\vdash_{{\mathrm{{\mathrm{GK(A_{m})}}}}}\,\Rightarrow\\!\varphi$.

Let us remark finally that, since any ${\mathrm{LK^{\prime}(A)}}$-tableau for
an $\mathcal{L}_{{\mathrm{A_{m}}}}^{\Box}$-formula has just one branch, we
obtain (consulting the proof of Theorem 8) a smaller upper bound for the
complexity of checking ${\mathrm{K(A)}}$-validity in this fragment.

######  Theorem 20.

The problem of checking if $\varphi\in{\rm
Fm}(\mathcal{L}_{\mathrm{A_{m}}}^{\Box})$ is ${\mathrm{K(A)}}$-valid is in
EXPTIME.

##  5\. Concluding Remarks

This paper takes a significant step towards a proof-theoretic account of
continuous modal logics: many-valued modal logics with connectives interpreted
locally by continuous functions over sets of real numbers. We have introduced
here a minimal modal extension ${\mathrm{K(A)}}$ of Abelian logic (see [31, 9,
29]), where propositional connectives are interpreted using lattice-ordered
group operations over the real numbers, and shown that the modal Łukasiewicz
logic ${\mathrm{K(\mathrmL)}}$ studied in [21] is a fragment of this logic
with an additional constant. We have provided a labelled tableau calculus for
${\mathrm{K(A)}}$ and established a coNEXPTIME upper bound for checking
validity. More significantly, for the modal-multiplicative fragment of
${\mathrm{K(A)}}$, we have obtained both a sequent calculus that admits cut-
elimination and an axiomatization without infinitary rules. Notably, this
latter result was established using the completeness of the labelled tableau
calculus to derive a corresponding proof in the sequent calculus. The more
standard algebraic approach to proving completeness of many-valued modal
logics, employed, e.g., for finite-valued Łukasiewicz modal logics in [21],
proceeds by constructing a canonical model as the set of maximal filters of
the Lindenbaum-Tarski algebra of the logic. For finite-valued Łukasiewicz
modal logics, completeness is proved using the fact that the appropriate
reduct of this algebra is semi-simple, which is not applicable in the
infinite-valued case or for the modal-multiplicative fragment of
${\mathrm{K(A)}}$.

Clearly, there are many open questions still to be addressed. The most
pressing issue is to find an axiomatization and algebraic semantics for the
full logic ${\mathrm{K(A)}}$. We conjecture that such an axiomatization can be
obtained by extending the axiom system ${\mathrm{HA}}$ for Abelian logic with
the axiom schema (K), (Dn) ($n\geq 2$) and rules (mp), (nec) from Figure 3,
and the axiom schema $(\Box\varphi\land\Box\psi)\to\Box(\varphi\land\psi)$. It
can be shown using methods of abstract algebraic logic that this axiom system
is sound and complete with respect to a corresponding variety of algebras with
a lattice-ordered abelian group reduct; the difficulty of course is to prove
that the axiomatization is complete with respect to the frame semantics of
${\mathrm{K(A)}}$, perhaps by extending the proof for the modal-multiplicative
fragment (using the labelled tableau calculus and a Gentzen-style calculus),
or via an alternative representation of the algebras. Such a proof would
provide the basis for an axiomatization and algebraic semantics for
${\mathrm{K(\mathrmL)}}$, and, more generally, a starting point for a Jónsson-
Tarski-style account of the relationship between relational and algebraic
semantics for these logics. Note that we can already develop such a
relationship for the modal-multiplicative fragment axiomatized in this paper,
but the algebras corresponding to the axiom system ${\mathrm{K(A_{m})}}$ will
not form a variety.

We have focussed in this work only on the minimal modal extension of Abelian
logic. However, adapting the Kripke semantics and labelled tableau calculi to
other (e.g., reflexive, symmetric, transitive) classes of frames is a
straightforward exercise. More challenging is the problem of adapting the
completeness proofs for the modal-multiplicative fragment to suitably extended
axiom systems and sequent calculi. For the reflexive case, completeness
proofs, similar to those given here, can be obtained for the extension of the
axiom system ${\mathrm{K(A_{m})}}$ with the axiom schema
$\Box\varphi\to\varphi$ and the sequent calculus ${\mathrm{GK(A_{m})}}$ with
the rule

$\mathrm{\Gamma},\Box\varphi\Rightarrow\mathrm{\Delta}\mathrm{\Gamma},\varphi\Rightarrow\mathrm{\Delta}$

However, a general approach for tackling different classes of frames is still
lacking.

Finally, it remains to determine whether the upper bounds given here for the
complexity of checking ${\mathrm{K(A)}}$-validity are optimal. Let us just
note that it makes sense to first investigate the EXPTIME upper bound for the
modal-multiplicative fragment, before considering the coNEXPTIME upper bound
for the full logic ${\mathrm{K(A)}}$ and indeed also ${\mathrm{K(\mathrmL)}}$.

## References

  * [1] F. Baader, S. Borgwardt, and R. Peñaloza.  Decidability and complexity of fuzzy description logics.  KI, 31(1):85–90, 2017.
  * [2] M. Baaz and G. Metcalfe.  Herbrand’s theorem, skolemization and proof systems for first-order Łukasiewicz logic.  Journal of Logic and Computation, 20(1):35–54, 2008.
  * [3] S. Baratella.  Continuous propositional modal logic.  Submitted (available at http://www.science.unitn.it/~baratell/CPropML.pdf).
  * [4] F. Bou, M. Cerami, and F. Esteva.  Finite-valued Łukasiewicz modal logic is PSPACE-complete.  In Proceedings of IJCAI 2011, pages 774–779, 2011.
  * [5] F. Bou, F. Esteva, L. Godo, and R. Rodríguez.  On the minimum many-valued logic over a finite residuated lattice.  Journal of Logic and Computation, 21(5):739–790, 2011.
  * [6] X. Caicedo, G. Metcalfe, R. Rodríguez, and J. Rogger.  Decidability in order-based modal logics.  Journal of Computer System Sciences, 88:53–74, 2017.
  * [7] X. Caicedo and R. Rodríguez.  Standard Gödel modal logics.  Studia Logica, 94(2):189–214, 2010.
  * [8] X. Caicedo and R. Rodríguez.  Bi-modal Gödel logic over [0,1]-valued Kripke frames.  Journal of Logic and Computation, 25(1):37–55, 2015.
  * [9] E. Casari.  Comparative logics and abelian $\ell$-groups.  In C. Bonotto, R. Ferro, S. Valentini, and A. Zanardo, editors, Logic Colloquium ’88, pages 161–190. Elsevier, 1989.
  * [10] N. Dershowitz and Z. Manna.  Proving termination with multiset orderings.  Communications of the Association for Computing Machinery, 22:465–476, 1979.
  * [11] D. Diaconescu and G. Georgescu.  Tense operators on MV-algebras and Łukasiewicz-Moisil algebras.  Fundamenta Informaticae, 81(4):379–408, 2007.
  * [12] D. Diaconescu, G. Metcalfe, and L. Schnüriger.  Axiomatizing a real-valued modal logic.  In Proceedings of AiML 2016, pages 236–251, 2016.
  * [13] M. C. Fitting.  Many-valued modal logics.  Fundamenta Informaticae, 15(3–4):235–254, 1991.
  * [14] M. C. Fitting.  Many-valued modal logics II.  Fundamenta Informaticae, 17:55–73, 1992.
  * [15] L. Godo, P. Hájek, and F. Esteva.  A fuzzy modal logic for belief functions.  Fundamenta Informaticae, 57(2–4):127–146, 2003.
  * [16] L. Godo and R. Rodríguez.  A fuzzy modal logic for similarity reasoning.  In Fuzzy Logic and Soft Computing, pages 33–48. Kluwer, 1999.
  * [17] P. Hájek.  Metamathematics of Fuzzy Logic.  Kluwer, Dordrecht, 1998.
  * [18] P. Hájek.  Making fuzzy description logic more general.  Fuzzy Sets and Systems, 154(1):1–15, 2005.
  * [19] P. Hájek, D. Harmancová, F. Esteva, P. Garcia, and L. Godo.  On modal logics for qualitative possibility in a fuzzy setting.  In Proceedings of UAI 1994, pages 278–285, 1994.
  * [20] P. Hájek, D. Harmancová, and R. Verbrugge.  A qualitative fuzzy possibilistic logic.  International Journal of Approximate Reasoning, 12:1–19, 1995.
  * [21] G. Hansoul and B. Teheux.  Extending Łukasiewicz logics with a modality: Algebraic approach to relational semantics.  Studia Logica, 101(3):505–545, 2013.
  * [22] L. G. Khachiyan.  A polynomial algorithm in linear programming.  Soviet Mathematics Doklady, 20:191–194, 1979.
  * [23] A. Kulacka, D. Pattinson, and L. Schröder.  Syntactic labelled tableaux for Łukasiewicz fuzzy ALC.  In Proceedings of IJCAI 2013, pages 962–968, 2013.
  * [24] C. Kupke and D. Pattinson.  On modal logics of linear inequalities.  In Proceedings of AiML 2010, pages 235–255. King’s College Publications, 2010.
  * [25] M. Marti and G. Metcalfe.  Hennessy-Milner properties for many-valued modal logics.  In Proceedings of AiML 2014, pages 407–420. King’s College Publications, 2014.
  * [26] M. Marti and G. Metcalfe.  Expressivity of chain-based modal logics.  Archive for Mathematical Logic. To appear.
  * [27] M. Mio and A. Simpson.  Łukasiewicz mu-calculus.  In Proceedings Workshop on Fixed Points in Computer Science, volume 126 of EPCTS, pages 87–104. Open Publishing Association, 2013.
  * [28] G. Metcalfe and N. Olivetti.  Towards a proof theory of Gödel modal logics.  Logical Methods in Computer Science, 7(2):1–27, 2011.
  * [29] G. Metcalfe, N. Olivetti, and D. Gabbay.  Sequent and hypersequent calculi for abelian and Łukasiewicz logics.  ACM Transactions on Computational Logic, 6(3):578–613, 2005.
  * [30] G. Metcalfe, N. Olivetti, and D. Gabbay.  Proof Theory for Fuzzy Logics, volume 36 of Applied Logic.  Springer, 2008.
  * [31] R. K. Meyer and J. K. Slaney.  Abelian logic from A to Z.  In Paraconsistent Logic: Essays on the Inconsistent, pages 245–288. Philosophia Verlag, 1989.
  * [32] G. Priest.  Many-valued modal logics: a simple approach.  Review of Symbolic Logic, 1:190–203, 2008.
  * [33] S. Schockaert, M. De Cock, and E. Kerre.  Spatial reasoning in a fuzzy region connection calculus.  Artificial Intelligence, 173(2):258–298, 2009.
  * [34] U. Straccia.  Reasoning within fuzzy description logics.  Journal of Artificial Intelligence Research, 14:137–166, 2001.