# Propositional Logics for the Lawvere Quantale

Giorgio Bacci  Radu Mardare  Prakash Panangaden  Gordon Plotkin  Department of
Computer Science, Aalborg University, Aalborg, Denmark  Computer and
Information Sciences, University of Strathclyde, Glasgow, Scotland  School of
Computer Science, McGill University and Mila, Montréal, Canada  LFCS, School
of Informatics, University of Edinburgh, Edinburgh, Scotland

###### Abstract

Lawvere showed that generalised metric spaces are categories enriched over
$[0,\infty]$, the quantale of the positive extended reals. The statement of
enrichment is a quantitative analogue of being a preorder. Towards seeking a
logic for quantitative metric reasoning, we investigate three
$[0,\infty]$-valued propositional logics over the Lawvere quantale. The basic
logical connectives shared by all three logics are those that can be
interpreted in any quantale, viz finite conjunctions and disjunctions, tensor
(addition for the Lawvere quantale) and linear implication (here a truncated
subtraction); to these we add, in turn, the constant $\mathbbm{1}$ to express
integer values, and scalar multiplication by a non-negative real to express
general affine combinations. Quantitative equational logic can be interpreted
in the third logic if we allow inference systems instead of axiomatic systems.

For each of these logics we develop a natural deduction system which we prove
to be decidably complete w.r.t. the quantale-valued semantics. The heart of
the completeness proof makes use of the Motzkin transposition theorem.
Consistency is also decidable; the proof makes use of Fourier-Motzkin
elimination of linear inequalities. Our logics are variants on $[0,1]$-logics,
via the exponential map $e^{-x}$: the first is equivalent to Goguen’s product
logic [9], the second is a version of product logic with a fixed choice of
constants, the third adds exponentiation. The first is known; the second and
third are apparently novel. The third is natural in the additive
$[0,\infty]$-context, but not the multiplicative $[0,1]$-context. Our proofs
are novel in all cases, making uses of linear algebraic results; these results
are commonly regarded informally as a kind of completeness result; here we put
that view to good use. Strong completeness does not hold in general, even (as
is known) for theories over finitely-many propositional variables; indeed even
an approximate form of strong completeness in the sense of Pavelka or Ben
Yaacov—provability up to arbitrary precision—does not hold. However, we can
show it for theories axiomatized by a (not necessarily finite) set of
judgements in _normal form_ over a finite set of propositional variables when
we restrict to models that do not map variables to $\infty$; the proof uses
Hurwicz’s general form of the Farkas’ Lemma.

###### keywords:

Quantitative reasoning, axiomatizations, quantitative algebras, metric spaces,
quantale-valued logics.

††journal: Electronic Notes in Theoretical Informatics and Computer
Science††volume: 3††thanks: Email<EMAIL_ADDRESS>Email:
<EMAIL_ADDRESS>Email<EMAIL_ADDRESS>Email:
<EMAIL_ADDRESS>
##  1 Introduction

Real-valued logics have been experiencing a recent resurgence of interest
because of probabilistic [15, 16, 1] and metric reasoning [24] and
applications such as neurosymbolic reasoning in machine learning [4, 5, 28].
They are generally fuzzy logics [11] often interpreted over $[0,1]$—for
example Łukasiewicz logic ([19, 33, 34]). In [18], Lawvere showed that
generalised metric spaces are categories enriched over $[0,\infty]$, the
quantale of the positive extended reals. The statement of enrichment is a
quantitative analogue of being a preorder. One can view Łukasiewicz logic as
the propositional logic of a quantale over $[0,1]$, see [23]. Also there are
interpretations of (variants of) linear logic in quantales [35].

In this paper, we propose studying logic over Lawvere’s quantale, and we begin
such a study with propositional logic. An argument that points towards this
quantale comes also from the literature on quantitative algebras [20], where
the development of quantitative equational logic is based on a family of
binary predicates ”$=_{\varepsilon}$” for every $\varepsilon\geq 0$. These are
used in quantitative equations, such as $s=_{\varepsilon}t$, to encode the
fact that the distance between the interpretation of the terms $s$ and $t$ in
a metric space is at most $\varepsilon$. Once this quantitative information is
embedded in the predicate ”$=_{\varepsilon}$”, quantitative equations become
Boolean statements, i.e., true or false in a model. An alternative way to
tackle this issue is to consider only one ”$=$” predicate that is valued in
the Lawvere quantale. This requires exchanging the classical “Boolean core” of
quantitative equational logic with a many-valued logic interpreted over
Lawvere’s quantale.

In this paper, we investigate basic concepts and proof systems for such
propositional logics. We consider three closely related logics, built up in
stages. The basic logical connectives, shared by all three logics, are those
that can be interpreted in any quantale, viz finite conjunctions and
disjunctions, tensor (addition for the Lawvere quantale) and linear
implication (here a truncated subtraction). To these we add, in turn, the
constant $\mathbbm{1}$ to express integer values, and scalar multiplication by
a non-negative real to express general non-negative affine combinations.
Quantitative equational logic can be interpreted in the third logic once we
extend the provability principles and instead of only looking to theories
defined by axiomatic systems, we also consider theories closed under systems
of inferences.

Our logics are variants of $[0,1]$-valued logics, via the exponential map
$e^{-x}$: the first is equivalent to product logic [13, 12], the second is a
version of product logic with a fixed choice of constants [26, 10], the third
adds exponentiation. The first is known; the second and third are apparently
novel. The third is natural in the additive $[0,\infty]$-context, but not the
multiplicative $[0,1]$-context, where multiplication by a constant becomes
exponentiation. Multiplication by a constant can be viewed as a graded
modality; however the literature on product logic modalities seems to consider
only Kripke models [31].

Our proofs are novel in all cases. The proofs used in the fuzzy logic
literature, e.g., in [13, 26], employ the methods of algebraic logic, and for
product logic in particular, use results of ordered Abelian group theory. Our
proofs are arguably simpler. They consist of a syntactic reduction to a normal
form using only affine combinations of propositional variables, followed by a
novel application of theorems from linear algebra, such as the Farkas’ Lemma.
It has been long noted in the literature [8] that the Farkas’ Lemma, and
related results, can be thought of as completeness theorems. Here they are
literally seen as such, and used to prove general completeness for our
propositional logics.

For each of these logics we develop a natural deduction system, and prove it
complete relative to interpretations in the Lawvere quantale. The proof of
completeness uses a normalisation technique which replaces a sequent
$\varphi\vdash\psi$ that is not in normal form, with a finite set of sequents
in normal form. The main normal form is a sequent where the formulas
$\varphi$, $\psi$ are tensors $r_{1}*p_{1}\otimes\ldots\otimes
r_{n}*p_{n}\otimes r$ of propositional variables multiplied by positive reals,
and a scalar. Semantically, these are exactly affine linear combinations of
the variables. Leaving aside the details, this reduces the problem of proving
that a given sequent follows from a given finite set of sequents, to the
problem of proving that a given affine inequality is a consequence of a given
finite set of affine inequalities. This is exactly the province of (variants
of) the Farkas’ Lemma [6] and the Motzkin transposition theorem [22]. These
show that when such a consequence holds for all values of the variables, then
the given affine inequality is a linear combination of the given set of
inequalities (an integer variant of Motzkin [30] is used when the reals are
integers). It is in this way that the Farkas’ Lemma and its relatives can be
viewed as completeness results (rather than, as in another–very similar–view,
as a dichotomy result that either there is a linear combination or there is a
counterexample).

As reduction to sets of normal forms and the Farkas’ Lemma (and related) are
effective, it follows that satisfiability is decidable. We can also decide
consistency via the reduction to normal form, now making use of Fourier-
Motzkin elimination [7, 32]. By making these reductions efficient one can
further show that consequence is co-NP complete and that consistency is NP-
complete.

Strong completeness does not hold in general, even for theories over finitely-
many propositional variables; indeed even an approximate form of strong
completeness in the sense of Pavelka or Ben Yaacov [3, 25, 33, 34]—provability
up to arbitrary precision—does not hold. However, we can show it does hold for
such theories that admit a, not necessarily finite, set of axioms in _normal
form_ over a _finite_ set of propositional variables when we restrict to
models that do not map variables to $\infty$; the proof uses Hurwicz’s general
form [14] of the Farkas’ Lemma.

#### Synopsis

In Section 2, we present some preliminaries and basic notation. In Section 3,
we introduce the three quantale-valued logics with their syntax and semantics.
Section 4 is dedicated to natural deduction systems, one for each of the three
logics. It contains soundness statements and a series of results regarding
provability in these logics. A subsection here is dedicated to deduction
theorems, with a detailed discussion about the failure of the classic
deduction theorem. In Section 5, we collect a series of model-theoretic
results and we introduce the concept of a diagrammatic theory that is central
in the model theory of these logics. Section 6 is dedicated to normalization;
it contains a brief description of an algorithm that computes the normal form
of a sequent. Due to space restrictions, the algorithm is only explained for a
couple of key cases. Section 7 is dedicated to completeness and incompleteness
results for all these logics. In Section 8, we show how we can encode
quantitative equational logic in our logic. Quantitative equational reasoning
requires more than just an axiomatic system; it needs a system of inferences
that does not produce one axiomatic theory, but a set of axiomatic theories.

##  2 Preliminaries and Notation

A _quantale_ is a complete lattice with a binary, associative operation
$\otimes$ (the _tensor_) preserving all joins (and so with both $a\otimes-$
and $-\otimes a$ having adjoints). A quantale is called _commutative_ whenever
its tensor is; it is called _unital_ if there is an element $1$, the unit,
such that $1\otimes a=a=a\otimes 1$, for all $a$; and it is called _integral_
if the unit is the top element. For commutative quantales, where the adjoints
coincide, we denote the adjoint to $a\otimes-$ by $a\multimap-$, which is
characterised by

$a\otimes b\leq c\Longleftrightarrow b\leq a\multimap c\,.$

The complete lattice $[0,\infty]$ ordered by the “greater or equal” relation
$\geq$ with extended sum as tensor, is known as the _Lawvere quantale_ (or
metric quantale). In this paper, we mainly work with the Lawvere quantale, so
it is convenient to have an explicit characterisation of its basic operations.
Join and meet are $\inf$ and $\sup$, respectively, $\infty$ is the bottom
element and $0$ the top. For $r,s\in[0,\infty]$, we define truncated
subtraction as

$r\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}s=\begin{cases}0&\text{if $r\leq s$}\\\
r-s&\text{if $r>s$ and $r\neq\infty$}\\\ \infty&\text{if $r=\infty$ and
$s\neq\infty$}\,.\end{cases}$

Then, the right adjoint $s\multimap r$ is just
$r\mathbin{\text{\ooalign{\raise 4.30554pt\hbox{.}\cr$-$\cr}}}s$ (note that
the order of terms is inverted). We remark that the continuous t-norms of
fuzzy logic are exactly the integral commutative quantales over $[0,1]$,
except that the condition of preserving all sups is replaced by the stronger
condition of monotonicity plus continuity (in the usual sense) [11].

##  3 Logics for the Lawvere Quantale

In this section, we present three propositional logics interpreted over the
Lawvere quantale which we will collectively refer to as _logics for the
Lawvere quantale_ (LLQ).

Syntax of logical formulas. Formulas are freely generated from a set
$\mathbb{P}=\\{p_{1},p_{2},\dots\\}$ of atomic propositions over logical
connectives that can be interpreted in the Lawvere quantale:

$\displaystyle\bot\mid\top\mid\phi\land\psi\mid\phi\lor\psi\mid\phi\otimes\psi\mid\phi\multimap\psi$
(quantale connect.) $\displaystyle\mathbbm{1}$ (constant) $\displaystyle
r*\phi\quad\text{(for $r\in[0,\infty)$)}$ (scalar multiplication)

The first logic, $\mathbb{L}$, uses only the basic logical connectives that
can be interpreted in any commutative quantale, viz, the constants bottom
($\bot$) and top ($\top$), binary conjunction ($\land$) and disjunction
($\lor$), tensor ($\otimes$), and linear implication ($\multimap$).

The second logic, $\mathbb{L}_{\mathbbm{1}}$, additionally allows the use of
the constant $\mathbbm{1}$.

The third logic, $\mathbb{L}_{\mathbbm{1}}^{*}$, extends the syntax further
with scalar multiplication by a non-negative real ($r*-$).

It will be useful to define, in all LLQ, the following derived connectives:

$\displaystyle\lnot\phi$
$\displaystyle\mathrel{\mathop{:}}=\phi\multimap\bot\,,$ (Negation)
$\displaystyle\phi\multimapboth\psi$
$\displaystyle\mathrel{\mathop{:}}=(\phi\multimap\psi)\land(\psi\multimap\phi)\,.$
(Double implication)

Moreover, for any $n\in\mathbb{N}$, the derived connective $n\phi$ is
inductively defined as follows

$\displaystyle 0\phi\mathrel{\mathop{:}}=\top$ and
$\displaystyle(n+1)\phi\mathrel{\mathop{:}}=\phi\otimes n\phi\,.$

Thus $\mathbb{L}_{\mathbbm{1}}$ effectively has all natural numbers as
constants via the formulas $r*\mathbbm{1}$. (In fact
$\mathbb{L}_{\mathbbm{1}}$ is equivalent to the logic obtained from
$\mathbb{L}$ by adding all rationals as constants.) Similarly, for any
$r\in[0,\infty)$, we write simply $r$ to denote the formula $r*\mathbbm{1}$.

###### Notation

To simplify the presentation, we assume an operator precedence rule so that
$*$ binds most strongly, followed by $\otimes$, next are $\land$ and $\lor$,
and the weakest are $\multimap$, $\multimapboth$ and $\lnot$. Thus, the
formula $r*\phi\otimes\psi\land s*\psi\multimap\theta$ is interpreted as
$(((r*\phi)\otimes\psi)\land(s*\psi))\multimap\theta$.

Semantics of logical formulas. The models of LLQ are maps
$m\colon\mathbb{P}\to[0,\infty]$ interpreting the propositional symbols in the
Lawvere quantale, which can be extended uniquely to formulas by setting

$\displaystyle\begin{aligned} m(\bot)&\mathrel{\mathop{:}}=\infty\,,\\\
m(\top)&\mathrel{\mathop{:}}=0\,,\\\
m(\mathbbm{1})&\mathrel{\mathop{:}}=1\,,\\\
m(r*\phi)&\mathrel{\mathop{:}}=rm(\phi)\,,\end{aligned}$
$\displaystyle\begin{aligned}
m(\phi\land\psi)&\mathrel{\mathop{:}}=\max\\{m(\psi),m(\phi)\\}\,,\\\
m(\phi\lor\psi)&\mathrel{\mathop{:}}=\min\\{m(\psi),m(\phi)\\}\,,\\\
m(\phi\otimes\psi)&\mathrel{\mathop{:}}=m(\phi)+m(\psi)\,,\\\
m(\phi\multimap\psi)&\mathrel{\mathop{:}}=m(\psi)\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}m(\phi)\,,\end{aligned}$

with derived connectives $\lnot$ and $\multimapboth$ interpreted as

$\displaystyle m(\lnot\phi)=\infty\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}m(\phi)\,,$ $\displaystyle
m(\phi\multimapboth\psi)=|m(\psi)-m(\phi)|\,.$

##  4 Natural Deduction Systems

We present natural deduction systems for the thee logics
$\mathbb{L}\subseteq\mathbb{L}_{\mathbbm{1}}\subseteq\mathbb{L}_{\mathbbm{1}}^{*}$.
As each logic is intended to be a conservative extension of its sub-logics, we
present their deduction systems incrementally.

Let
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}},\mathbb{L}_{\mathbbm{1}}^{*}\\}$.
A _judgement_ in $\mathcal{L}$ is a syntactic construct of the form

$\phi_{1},\dots,\phi_{n}\vdash\psi\,,$ (Judgement)

where the $\phi_{i}$ and $\psi$ are logical formulas of $\mathcal{L}$, called
respectively the _antecedents_ and the _consequent_ of the judgement. Note
that the antecedents $\Gamma=(\phi_{1},\dots,\phi_{n})$ of a judgement form a
finite ordered list, possibly, with repetitions. As is customary, for $\Gamma$
and $\Delta$ lists of formulas, their comma-separated juxtaposition
$\Gamma,\Delta$ denotes concatenation; and $\vdash\psi$ is the notation for a
judgement with empty list of antecedents.

A judgement $\gamma=(\Gamma\vdash\psi)$ in $\mathcal{L}$ _is satisfied by_ a
model $m$, in symbols $m\models_{\mathcal{L}}\gamma$, whenever

$\textstyle\sum_{\phi\in\Gamma}m(\phi)\geq m(\psi)\,.$ (Semantics of
judgements)

When the logic $\mathcal{L}$ is clear from the context or the satisfiability
holds in all LLQ, we simply write $m\models\gamma$.

A judgement is _satisfiable_ if it is satisfied by a model; _unsatisfiable_ if
it is not satisfiable; and a _tautology_ if it is satisfied by all models.
Note that, for any model $m$ in LLQ

$\displaystyle\begin{aligned} m\models(\vdash\phi)&&\text{iff}&&m(\phi)&=0\\\
m\models(\vdash\lnot\phi)&&\text{iff}&&m(\phi)&=\infty\quad\text{({i.e.},
$\phi$ is infinite)}\\\
m\models(\vdash\lnot\lnot\phi)&&\text{iff}&&m(\phi)&<\infty\quad\text{({i.e.},
$\phi$ is finite)}\\\ m\models(\phi\vdash\psi)&&\text{iff}&&m(\phi)&\geq
m(\psi)\,.\end{aligned}$

In particular, $\vdash\phi\multimap\phi$, $\vdash\top$, and $\vdash\lnot\bot$
are examples of tautologies, while $\vdash\phi\multimapboth(\lnot\lnot\phi)$
is not. Moreover, by using negation we can express whether the interpretation
of a formula is either finite or infinite.

An inference (rule) is a syntactic construct of the form $~{}\gamma~{}S$, for
$S$ a set of judgements and $\gamma$ a judgement. The judgements in $S$ are
the _hypotheses of the inference_ and $\gamma$ is the _conclusion of the
inference_. When $S=\\{\gamma^{\prime}\\}$ is a singleton, we write

$\begin{aligned} ~{}\gamma~{}\gamma^{\prime}\end{aligned}\quad\text{to denote
that both}\quad\begin{aligned}
~{}\gamma~{}\gamma^{\prime}\end{aligned}\;\text{and }\;\begin{aligned}
~{}\gamma^{\prime}~{}\gamma\end{aligned}\;\text{hold.}$

A judgement $\gamma$ is a _semantic consequence_ of a set $S$ of judgements,
in symbols $S\models\gamma$, if every model that satisfies all the judgements
in $S$ satisfies also $\gamma$. Thus, $\emptyset\models\gamma$ (or more simply
$\models\gamma$) means that $\gamma$ is a tautology. For a model $m$, we will
also use the notation $S\models_{m}\gamma$, to mean that, whenever $m$
satisfies all the judgements of $S$, then it satisfies also $\gamma$.

#### The natural deduction system of $\mathbb{L}$

It consists of the inference rules in Figure LABEL:fig:LL. Figure 4 contains
the basic rules of logical deduction (id) and (cut), and the structural rules
of weakening (weak) and permutation (perm). Note that, there is no
cancellation rule. Figure LABEL:tab:latticeRules provides the rules for the
lattice operations of the Lawvere quantale111Recall that the order on
$[0,\infty]$ is reversed!. Figure LABEL:tab:lawvereRules collects the rules
that are specific to the Lawvere quantale. (wem) is the weak excluded middle;
(tot) states that the quantale is totally ordered; the other rules explain the
actions of $\otimes$ and its adjoint in the Lawvere quantale.

#### The natural deduction system of $\mathbb{L}_{\mathbbm{1}}$

It includes all the rules in Figure LABEL:fig:LL and, in addition,

$\vdash\bot\vdash\mathbbm{1}\lor\lnot\mathbbm{1}$

expressing that $0\geq 1$ and $1\geq\infty$ are inconsistencies. Thus, with
$\mathbb{L}_{\mathbbm{1}}$ we exit the universe of classical logic, as
$\mathbbm{1}$ cannot be provably equivalent either to $\top$, or to $\bot$.

#### The natural deduction system of $\mathbb{L}_{\mathbbm{1}}^{*}$

It extends the deduction system of $\mathbb{L}_{\mathbbm{1}}$ with the rules
for scalar multiplication in Figure LABEL:tab:scalarRules. In ($S_{4}$),
${\bowtie}$ can be either of $\land,\lor,\otimes,\multimap$, meaning that we
have one version of ($S_{4}$) for each of these operators.

=∞ . $-$ n=∞. Fact LABEL:fact:wdt shows that $\mathbb{L}_{\mathbbm{1}}$ is not
equivalent to any of the extensions of product logic with truth-constants
proposed in [3], for which such a weak deduction theorem does hold.

(a) Logical deduction and Structural rules

###  4.2 Totality Lemma

We call pairs of judgements of the following form

$\displaystyle(\vdash\phi\multimap\psi\;,\;\vdash\psi\multimap\phi)$ or
$\displaystyle(\vdash\lnot\phi\;,\;\vdash\lnot\lnot\phi)$

_supplementary judgements_. These judgements, when used as a pair as above,
explore different alternatives for the interpretations of LLQ-formulas. The
first pair of judgements explores different ordering alternatives; the second
is choosing either a finite or infinite interpretation for a formula.

Supplementary judgements play a special rôle in reasoning, as clearly stated
in the following lemma.

######  Lemma 4.3 (Totality Lemma).

The following statements are provable in all LLQ.

  1. (1)

$\text{If
}\Big{[}\dfrac{\vdash\rho~{}~{}~{}~{}\phi\vdash\psi}{\vdash\theta}\text{ and
}\dfrac{\vdash\rho~{}~{}~{}~{}\psi\vdash\phi}{\vdash\theta}\Big{]}\text{ then
}\dfrac{\vdash\rho}{\vdash\theta}$.

  2. (2)

$\text{If
}\Big{[}\dfrac{\vdash\rho~{}~{}~{}~{}\vdash\lnot\phi}{\vdash\theta}\text{ and
}\dfrac{\vdash\rho~{}~{}~{}~{}\vdash\lnot\lnot\phi}{\vdash\theta}\Big{]}\text{
then }\dfrac{\vdash\rho}{\vdash\theta}$.

The totality lemma, along with others, allows us to prove the distributivity
of the tensor product with respect to $\land$ and $\lor$, respectively.

##  5 Theories and Models

In what follows, we use $\mathcal{L}$ to range over
$\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}},\mathbb{L}_{\mathbbm{1}}^{*}\\}$, as
the following definitions are uniform for all LLQ.

A _theory_ $\mathbb{T}$ in $\mathcal{L}$ is a set of judgements that is
deductively closed (in symbols, $\mathbb{T}\Vdash_{\mathcal{L}}\gamma$ implies
$\gamma\in\mathbb{T}$). An _axiomatic theory_ in $\mathcal{L}$ is a theory for
which there exists a set of judgements, called _axioms_ , such that all the
judgements in the theory can be proven in $\mathcal{L}$ from the axioms; it is
_finitely axiomatized_ if it admits a finite set of axioms.

If $\mathbb{T}$ and $\mathbb{T}^{\prime}$ are two theories in $\mathcal{L}$
such that $\mathbb{T}\subseteq\mathbb{T}^{\prime}$, we say that
$\mathbb{T}^{\prime}$ is a _extension_ of $\mathbb{T}$; it is a _proper
extension_ if $\mathbb{T}\subsetneq\mathbb{T}^{\prime}$.

A theory $\mathbb{T}$ in $\mathcal{L}$ is _disjunctive_ , if for any formulas
$\phi,\psi\in\mathcal{L}$, $\vdash\phi\lor\psi\in\mathbb{T}$ implies that
either $\vdash\phi\in\mathbb{T}$ or $\vdash\psi\in\mathbb{T}$. It is immediate
that if $\mathbb{T}$ is a disjunctive theory, because of (tot) and (wem), we
have that for any set of supplementary judgements in $\mathcal{L}$, at least
one of the judgements belongs to $\mathbb{T}$.

A theory in $\mathcal{L}$ is _inconsistent_ if it contains $\top\vdash\bot$,
otherwise it is _consistent_ ; it is _maximal consistent_ if it is consistent
and all its proper extensions are inconsistent.

A _model of a theory $\mathbb{T}$_ is a model $m$ that satisfies all the
judgements of the theory. If the theory is axiomatized, $m$ is a model for all
the axioms iff it is a model of the theory.

Note that an assignment of values to all the propositional atoms defines a
unique model since the values of all formulas are given inductively and are
determined by the values of the atomic propositions.

######  Lemma 5.1.

In all LLQ the following statements are true.

  1. (1)

If a theory has a model, then it is consistent.

  2. (2)

Any model satisfies a disjunctive consistent theory.

In the case of $\mathbb{L}_{\mathbbm{1}}^{*}$ we can identify a special class
of disjunctive consistent theories.

######  Definition 5.2.

A _diagrammatic theory_ is a consistent theory $\mathbb{T}$ of
$\mathbb{L}_{\mathbbm{1}}^{*}$ such that for any $p\in\mathbb{P}$,

  * •

either $p\vdash\bot\in\mathbb{T}$,

  * •

or there exists $\varepsilon\in[0,\infty)$ such that $\varepsilon\vdash
p\in\mathbb{T}$ and $p\vdash\varepsilon\in\mathbb{T}$.

It is not difficult to observe that in a diagrammatic theory, for any
$\phi\in\mathbb{L}_{\mathbbm{1}}^{*}$, either $\phi\vdash\bot\in\mathbb{T}$,
or there exists $\varepsilon\in[0,\infty)$ such that $\varepsilon\vdash\phi$,
$\phi\vdash\varepsilon\in\mathbb{T}$.

######  Lemma 5.3.

In $\mathbb{L}_{\mathbbm{1}}^{*}$ we have that

  1. (1)

Every diagrammatic theory has a unique model.

  2. (2)

Every model satisfies a unique diagrammatic theory.

  3. (3)

A theory is diagrammatic iff it is maximal consistent.

  4. (4)

Every disjunctive consistent theory has a unique diagrammatic extension; and a
unique model.

##  6 Normal Forms

In this section, we prove that any finitely axiomatized theory can be
presented in a normal form, where all the axioms have a specific syntactic
format.

There are some important classes of judgements that play a crucial role in our
development:

$\displaystyle\bot\vdash\phi\;\mid\;\phi\vdash\top$ (tautological)
$\displaystyle\top\vdash\bot\;\mid\;\top\vdash\mathbbm{1}\;\mid\;\mathbbm{1}\vdash\bot$
(inconsistent) $\displaystyle\underbrace{\top\vdash
p\;\mid\;p\vdash\bot}_{\text{alethic}}\;\mid\;\underbrace{\vdash\lnot\lnot
p}_{\text{finitist}}$ (assertive) $\displaystyle\textstyle(\bigotimes_{i\leq
n}r_{i}*p_{i})\otimes r*\mathbbm{1}\vdash(\bigotimes_{j\leq
m}s_{i}*q_{i})\otimes s*\mathbbm{1}$ (affine)

where $p,p_{i},q_{j}\in\mathbb{P}$ are atomic propositions. In the case of
$\mathbb{L}$ and $\mathbb{L}_{\mathbbm{1}}$ the coefficient in an affine
judgement are positive integers, and for $\mathbb{L}$ the term involving
$\mathbbm{1}$ is not present.

######  Definition 6.1 (Normal form).

A judgement is in _normal form_ if it is either tautological, inconsistent,
assertive (finitist or alethic), or affine.

###### Notation 4

Since in $\mathbb{L}_{\mathbbm{1}}^{*}$ $\otimes$ commutes with all the other
logical connectives, we assume hereafter that in all the formulas the scalar
products guard the atomic propositions or the constants, and no other scalar
products appear in a formula.

######  Definition 6.2.

A theory in LLQ is _normal_ , or it has a _normal axiomatization_ , if it
admits a finite axiomatization such that

  * •

every axiom is in normal form;

  * •

no atomic proposition that occurs in an alethic axiom appears in any other
axiom;

  * •

there is an assertive judgement for each atomic proposition that appears in
the axioms.

For LLQ it is not possible, in general, to convert a judgement into a model-
theoretic equivalent judgement in normal form. It is however possible to
associate with any judgement $\gamma$, a finite (possibly empty) set of normal
theories $\mathbb{T}_{1},\dots,\mathbb{T}_{n}$, such that:

$\displaystyle m\models\gamma$ iff $\displaystyle\text{for some $i\leq n$,
}\,m\models\mathbb{T}_{i}\,\,.$

In such a case, we call the set $\\{\mathbb{T}_{1},\dots,\mathbb{T}_{n}\\}$ of
theories a _normal representation of the judgement_ $\gamma$. Similarly, a
_normal representation of a finite set of judgements $V$_ (or of a finitely
axiomatized theory) is a finite (possibly empty) set of normal theories
$\mathbb{T}_{1},\dots,\mathbb{T}_{n}$, such that, $m$ is a model of $V$ iff it
is a model for at least one of the theories
$\mathbb{T}_{1},\dots,\mathbb{T}_{n}$.

###  6.1 Normalization Algorithm

There exists a simple algorithm that allows us to compute, for any given
finite set of judgements $V$, its normal representation $\mathcal{N}(V)$. The
details of this algorithm are in the appendix. In what follows, we sketch how
this algorithm works on a couple of examples that illustrate the main
subtleties of the algorithm.

Suppose we have a finite set $V$ of judgements. If $V$ is not already in
normal form, we can use the theorems of LLQ to simplify the judgements and
eventually convert them to a normal form. In doing this, in some cases, we
will have to use pairs $(\gamma_{1},\gamma_{2})$ of supplementary judgements
(see Section 4.2) that will be treated as new axioms. This is done when the
conversion cannot progress without extra assumptions. One can think of it as
“a proof by cases” resulting in two new separate set of judgements $V_{1}$ and
$V_{2}$, each containing one of the supplementary judgements. The invariant
preserved in each reduction step is that, for $i\in\\{1,2\\}$

  * •

all the judgements in $V_{i}$ are provable from $V\cup\\{\gamma_{i}\\}$;

  * •

all the judgements in $V$ are provable from $V_{i}$.

######  Example 6.3.

Let $\gamma=\theta\vdash(\phi\lor\psi)\otimes\rho$ be the judgement we would
like to reduce to normal form. The disjunction occurring in $\gamma$ is
problematic as it prevents $\gamma$ to be provably equivalent to another
(single) judgement in normal form. However, by using the supplementary
hypotheses $\psi\vdash\phi$ and $\phi\vdash\psi$, we can split the reduction
by cases and obtain $V_{1}=\\{\phi\vdash\psi,\theta\vdash\psi\otimes\rho\\}$
and $V_{2}=\\{\psi\vdash\phi,\theta\vdash\phi\otimes\rho\\}$, two sets of
judgements on which each element is (at least) one step closer to be in normal
form (Fig. 1(f)). Note that the invariant described above is preserved.

pt$\theta\vdash(\phi\lor\psi)\otimes\rho$pt$\phi\vdash\psi$$\theta\vdash\psi\otimes\rho$$V_{2}$pt$\psi\vdash\phi$$\theta\vdash\phi\otimes\rho$$V_{1}$
(f)

pt$\theta\vdash(\phi\multimap\psi)\otimes\rho$pt$\phi\vdash\psi$$\theta\vdash\rho$$W_{1}$pt$\psi\vdash\phi$$\theta\vdash(\phi\multimap\psi)\otimes\rho$pt$\vdash\lnot\psi$$\psi\vdash\phi$$\theta\vdash(\phi\multimap\psi)\otimes\rho$pt$\vdash\lnot\phi$$\vdash\lnot\psi$$\theta\vdash\rho$$W_{4}$pt$\vdash\lnot\lnot\phi$$\vdash\lnot\psi$$\vdash\lnot\theta$$W_{3}$pt$\vdash\lnot\lnot\psi$$\psi\vdash\phi$$\theta\otimes\phi\vdash\psi\otimes\rho$$W_{2}$pt
(g)

Figure 1: Conversion into normal representation: (a) Rule 3 and (b) Rule 5 of
the normalization algorithm

######  Example 6.4.

Let $\gamma=\theta\vdash(\phi\multimap\psi)\otimes\rho$ be the judgement to be
converted into normal form. In this specific case, the problematic connective
is $\multimap$. By adding appropriate pairs of supplementary judgements, in
sequence, we split the reduction in four cases and obtain $W_{1},\dots,W_{4}$
as new sets of judgements (Fig 1(g)).

Of interest in this particular case, is that in order to guarantee that the
new sets of judgements have strictly reduced complexity —interpreted as number
of sub-formulas not in normal form— we need to take several reduction steps.

Starting from a finite set of judgements $V$, the normalization algorithm
works essentiality by repeatedly applying conversion rules to the judgements
that are not in normal form by inspecting the structure of the formulas in the
judgements. Note that, Examples 6.3 and 6.4 describe actual conversion rules
in the algorithm (for the other rules see the full version of the paper on
ArXiV). As each conversion rule guarantees that the number of sub-formulas not
in normal form is strictly reduced, the algorithms eventually terminates.

The output $\mathcal{N}(V)$ of the algorithm is a set of theories
(technically, only their axioms). The next theorem states the correctness of
this conversion.

######  Theorem 6.5 (Normal representation).

Given a finite set $V$ of judgements in
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}},\mathbb{L}_{\mathbbm{1}}^{*}\\}$,
the set of the theories axiomatized by the elements in $\mathcal{N}(V)$ is a
normal representation of the theory axiomatized by $V$. Consequently, any
model of $V$ is a model for at least one of the elements in $\mathcal{N}(V)$;
and any model of an element in $\mathcal{N}(V)$ is a model of $V$.

The normalization algorithm also allows us to prove the decidability of
satisfiability in LLQ.

######  Theorem 6.6 (Decidability of satisfiability in LLQ).

Given a finite set $V$ of judgements in
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}},\mathbb{L}_{\mathbbm{1}}^{*}\\}$,
$V$ is satisfiable iff there exists $S\in\mathcal{N}(V)$ s.t.
$\vdash\bot\not\in S$. Consequently, the satisfiability of judgements in LLQ
is decidable.

##  7 Completeness and Incompleteness

In this section, we demonstrate first that all the logics for the Lawvere
quantale are incomplete in general, even for theories over finitely many
propositional symbols. Secondly, we prove that all LLQ are complete if
consider finitely-axiomatised theories only. Finally, we prove an approximate
form of strong completeness over a well behaved class of theories, not
necessarily finitely-axiomatizable.

######  Theorem 7.1 (Incompleteness).

LLQ are incomplete: for any
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}}\mathbb{L}_{\mathbbm{1}}^{*}\\}$,
there exist theories $\mathbb{T}$ and judgements $\gamma$ in $\mathbb{L}$ so
that all the models of $\mathbb{T}$ are models of $\gamma$ but $\gamma$ is not
provable from $\mathbb{T}$ in $\mathcal{L}$. Moreover, the result is
independent of the particular proof systems that are chosen for LLQ, in the
sense that any finite set of finitary proof rules that can be proposed (as an
alternative to the rules presented in this paper) still produces an incomplete
theory for each $\mathcal{L}$.

######  Proof 7.2.

Consider
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}}\mathbb{L}_{\mathbbm{1}}^{*}\\}$
with their proof systems presented in Section 4, or any alternative finite set
of _finitary_ rules that can describe $\mathcal{L}$. Let $p,q\in\mathbb{P}$ be
two atomic propositions and $\mathbb{T}$ a theory in $\mathcal{L}$ axiomatized
by all the judgements of the form $(n+1)p\vdash nq\quad\text{for all
}n\in\mathbb{N}\,.$

Note that in all the models $m$ of $\mathbb{T}$ we must have $m(p)\geq m(q)$,
hence all the models of $\mathbb{T}$ are also models of $p\vdash q$. Assume
there exists a finite proof of $p\vdash q$ in $\mathcal{L}$ from the set
$\\{(n+1)p\vdash q\mid n\geq 0\\}$ of axioms of $\mathbb{T}$. Since this proof
is finite and uses a finite set of finitary rules, there must exist $k\geq 0$
so that the only judgements used in the proof of $p\vdash q$ are from the set
$V=\\{(n+1)p\vdash q\mid 0\leq n\leq k\\}$. If that is the case, then any
model of $V$ is a model for $p\vdash q$ (from soundness). But this is false:
consider the model $m$ such that $m(p)=\frac{k}{k+1}$ and $m(q)=1$. This is a
model of $V$, but not a model of $p\vdash q$.

A consequence of Theorem 7.1 is that not all consistent theories have models.
For instance in $\mathbb{L}_{\mathbbm{1}}$, the theory axiomatized by the set
$\\{p\vdash n\mid n\in\mathbb{N}\\}\cup\\{\vdash\lnot\lnot p\\}$ of axioms for
$p\in\mathbb{P}$, is consistent: any proof will use a finite subset of axioms
from the first set and possibly $\vdash\lnot\lnot p$, and these are not
sufficient to prove $\vdash\bot$. However, this theory has no model, because
in any model $m$ the axioms in the first set guarantee that $m(p)\geq n$, for
all $n\in\mathbb{N}$, while the last axiom require that $m(p)$ is finite.

######  Theorem 7.3 (Completeness for finitely-axiomatized theories).

Let
$\mathcal{L}\in\\{\mathbb{L},\mathbb{L}_{\mathbbm{1}}\mathbb{L}_{\mathbbm{1}}^{*}\\}$
and $\mathbb{T}$ a finitely-axiomatized theory in $\mathcal{L}$. If a
judgement $\gamma$ is a semantic consequence of $\mathbb{T}$ in $\mathcal{L}$,
then $\gamma$ is provable from $\mathbb{T}$ in $\mathcal{L}$ (in symbols,
$\mathbb{T}\models_{\mathcal{L}}\gamma$ implies
$\mathbb{T}\Vdash_{\mathcal{L}}\gamma$).

######  Proof 7.4.

The proof is similar for all LLQ, by adapting only the arguments to the
appropriate context. Hereafter, we sketch the proof for
$\mathbb{L}_{\mathbbm{1}}^{*}$, as it is the most complex of all. We only
sketch this for the case both $\gamma$ and $\mathbb{T}$ are in normal form.
The other cases can all be reduced to this one.

Assume that $\gamma$ is a normal judgement and $\mathbb{T}$ a normal theory.
The cases when $\gamma$ is an alethic or a finitist judgement are relatively
simple. We detail here the case when $\gamma$ is affine:

$(\bigotimes_{i\leq n}r_{i}*p_{i})\otimes
r*\mathbbm{1}\vdash(\bigotimes_{j\leq m}s_{j}*q_{j})\otimes s*\mathbbm{1}$

with $m,n$ possibly $0$. We need to show that the judgement above is provable
from the axioms of $\mathbb{T}$. We have a couple of cases regarding the
possibility that some of atomic propositions $p_{i}$, $q_{j}$ appear in
alethic axioms in $\mathbb{T}$, but we can easily deal with these propositions
and eventually reduce the problem to the case when none of the atomic
propositions $p_{i}$, $q_{j}$ appear in the alethic axioms of $\mathbb{T}$.

Consequently, all these atomic propositions appear in finitist axioms of
$\mathbb{T}$. Using commutativity and associativity of $\otimes$, we will
reorganise both our judgement and the non-assertive axioms of $\mathbb{T}$ so
that we put together different copies of the same atomic proposition in a
tensorial product and use the facts that $0p=\top$ and
$r*\top\otimes\phi\dashv\vdash\phi$. So, without losing generality, we can
assume that our judgement $\gamma$ is

$(\bigotimes_{i\leq k}a_{i}*x_{i})\otimes
r*\mathbbm{1}\vdash(\bigotimes_{i\leq k}b_{i}*x_{i})\otimes s*\mathbbm{1}$

and the non-assertive axioms of $\mathbb{T}$ are

$\left\\{\begin{aligned} (\bigotimes_{i\leq k}a^{1}_{i}*x_{i})\otimes
r^{1}*\mathbbm{1}&\vdash(\bigotimes_{i\leq k}b^{1}_{i}*x_{i})\otimes
s^{1}*\mathbbm{1}\\\ &\dots\\\ (\bigotimes_{i\leq k}a^{l}_{i}*x_{i})\otimes
r^{l}*\mathbbm{1}&\vdash(\bigotimes_{i\leq k}b^{l}_{i}*x_{i})\otimes
s^{l}*\mathbbm{1}\end{aligned}\right.$

for some positive reals $a_{i},b_{i},a_{i}^{j},b_{i}^{j},r,s,r^{j},s^{j}$ and
atomic propositions $x_{1},\dots,x_{k}$. Consider the matrices
$A\in\mathbb{R}^{l\times k}$, $C\in\mathbb{R}^{k\times 1}$ and vector
$\beta\in\mathbb{R}^{k}$.

$\displaystyle
A=\begin{pmatrix}a^{1}_{1}-b^{1}_{1}&\dots&a^{1}_{k}-b^{1}_{k}\\\
\dots&\dots&\dots\\\
a^{l}_{1}-b^{l}_{1}&\dots&a^{l}_{k}-b^{l}_{k}\end{pmatrix}$ $\displaystyle
C=(b_{1}-a_{1},\dots,b_{k}-a_{k})\,$
$\displaystyle\beta=\begin{pmatrix}r^{1}-s^{1}\\\ \dots\\\
r^{l}-s^{l}\end{pmatrix}$

and let $\delta=r-s$. According to our hypothesis, any model of $\mathbb{T}$
is a model of $\gamma$, it follows that there exists no
$x=(x_{1},\dots,x_{k})\in\mathbb{R}^{k}$ such that

$\displaystyle Ax+\beta\geq 0\,,\quad Cx+\delta>0\,.$

By Mozkin transposition theorem [22]222Motzkin [22] contains an unfortunate
typo. For a correct form of the statement see [2]. Here we use an adapted form
for affine transformations obtained by using the Fundamental Theorem of Linear
Inequalities (see [27, Corollary 7.1h]), there exist $t_{0}\in\mathbb{R}$ and
$t=(t_{1},\dots,t_{l})\in\mathbb{R}^{l\times 1}$, such that

$\displaystyle Cx+\delta=t(Ax+\beta)+t_{0}\,,\quad t\geq 0\,,\quad t_{0}\geq
0\,.$

In $\mathbb{L}_{\mathbbm{1}}^{*}$ we can repeatedly apply the derived rule
following the pattern from $t$, $t_{0}$

$r*\phi_{1}\otimes s*\phi_{2}\vdash r*\psi_{1}\otimes
s*\psi_{2}\lx@proof@logical@and\phi_{1}\vdash\psi_{1}\phi_{2}\vdash\psi_{2}$

we obtain a proof from $\mathbb{T}$ for $\big{(}(\bigotimes_{i\leq
k}a_{i}*x_{i})\otimes r*\mathbbm{1}\big{)}\vdash\big{(}(\bigotimes_{i\leq
k}b_{i}*x_{i})\otimes s*\mathbbm{1}\big{)}$.

A consequence of this completeness result is the following.

######  Corollary 7.5.

For any finitely axiomatized theory of $\mathbb{L}_{\mathbbm{1}}^{*}$, the set
of its diagrammatic extensions coincide with the set of the diagrammatic
theories of its models.

Incompleteness over general theories (Theorem 7.1) is a common trait of
several many-valued logics [21, 33, 34], especially, if interpreted over the
reals. A weaker form of completeness result, first proposed by Ben Yaacov
[34], is _approximate completeness_. Rather than compromise on the theories,
one asks instead whether a judgement can be “proven up to arbitrary
precision”.

In $\mathbb{L}_{\mathbbm{1}}^{*}$, approximate completeness can be formally
stated as follows: whenever all the models of a set of judgements $S$ are also
models of $\vdash\psi$, the judgement $\epsilon\vdash\psi$ is provable from
$S$ in $\mathbb{L}_{\mathbbm{1}}^{*}$, for any $\varepsilon>0$.

It is not difficult to see that the above statement is still too strong to
hold in $\mathbb{L}_{\mathbbm{1}}^{*}$ for general sets of judgements $S$.
Actually, already theories using only finitely-many atomic propositions (one
is enough) can falsify the statement.

######  Fact 5 (Failure of approximate completeness).

Consider the set $S=\\{p\vdash n\mid n\in\mathbb{N}\\}$ of judgements in
$\mathbb{L}_{\mathbbm{1}}^{*}$, for $p\in\mathbb{P}$ a fixed atomic
proposition, and take $\psi=\lnot p$.

The only model $m$ of $S$ is such that $m(p)=\infty$, because satisfying all
the judgements of the form $p\vdash n$, for $n\in\mathbb{N}$, is equivalent to
say that the interpretation of $p$ is $\infty$. Thus, it is also a model for
$\vdash\lnot p$.

Assume that approximate completeness holds in $\mathbb{L}_{\mathbbm{1}}^{*}$
and let $\varepsilon<\infty$. Then, $\lnot p$ is provable from $S$. As any
proof is finite, there must exists a finite subset $S^{\prime}\subseteq S$
such that $\varepsilon\vdash\lnot p$ is provable from $S^{\prime}$.

Define $N\mathrel{\mathop{:}}=\max\\{n\mid p\vdash n\in S^{\prime}\\}$. Then,
$m^{\prime}(p)\mathrel{\mathop{:}}=N$ is a model for $S^{\prime}$ and, by
Theorem LABEL:soundness, $m\models(\varepsilon\vdash\lnot p)$. That is,
$\varepsilon=m^{\prime}(e)\geq m^{\prime}(\lnot\phi)$. However,
$m^{\prime}(\lnot\phi)=\infty$, thus, $m^{\prime}(\lnot\phi)>\varepsilon$
—contradiction.

Despite the fact that we cannot hope for a general form of approximate strong
completeness, we can still recover a mildly restricted version of it by
focusing on a suitable well-behaved class of judgements and theories over
finitely-many atomic propositions.

Let $\mathbb{P}_{n}=\\{p_{1},\dots,p_{n}\\}$ be a finite set of atomic
propositions, and denote by $\mathbb{L}_{\mathbbm{1}}^{*}(n)$ the logic
$\mathbb{L}_{\mathbbm{1}}^{*}$ restricted over $\mathbb{P}_{n}$. Then, using
the Hurwicz’s general form of Farkas’ Lemma [14], and following a similar
proof structure as in Theorem 7.3, we can prove the following approximate
completeness result.

######  Theorem 7.6 (Restricted approximate completeness).

Let $S$ be a set of normal judgements in $\mathbb{L}_{\mathbbm{1}}^{*}(n)$
such that it has only models valued over $[0,\infty)$. If a normal
judgement333By an abuse of notation, here we actually mean that $\vdash\phi$
is provably equivalent to a judgement in normal form. $\vdash\psi$ is a
semantic consequence of $S$ in $\mathbb{L}_{\mathbbm{1}}^{*}(n)$, then for any
$\varepsilon>0$, $\varepsilon\vdash\psi$ is provable from $S$.

######  Proof 7.7.

We assume that $S$ is not finite (the finite case is covered by Theorem 7.3)
and in normal form. We further assume that the constant $\mathbbm{1}$ is never
used neither in $S$ nor in $\psi$. This will guarantee us to work on linear
maps, rather than affine ones. The generalisation to the case of affine maps
can be done by invoking the Fundamental Theorem of Linear Inequalities (for
details see e.g. [27, Corollary 7.1h]). Without loss of generality, as in
Theorem 7.3, we can assume that $\vdash\psi$ is provably equivalent to

$(\bigotimes_{i\leq n}a_{i}*p_{i})\vdash(\bigotimes_{i\leq n}b_{i}*p_{i})$

and the non-assertive judgements in $S$ are

$\left\\{\begin{aligned} (\bigotimes_{i\leq
n}a^{1}_{i}*p_{i})&\vdash(\bigotimes_{i\leq n}b^{1}_{i}*p_{i})\\\
(\bigotimes_{i\leq n}a^{2}_{i}*p_{i})&\vdash(\bigotimes_{i\leq
n}b^{2}_{i}*p_{i})\\\ &\dots\end{aligned}\right.$

Let $\mathcal{X}=\mathbb{R}^{n}$ and $\mathcal{Y}=\mathbb{R}^{\mathbb{N}}$,
and denote by $\mathcal{X}^{*}$, $\mathcal{Y}^{*}$ their dual spaces,
respectively (i.e., $\mathcal{X}^{*}$ is the set of all continuous linear
functionals $\mathcal{X}\to\mathbb{R}$). Define the maps
$T_{S}\colon\mathcal{X}\to\mathcal{Y}$ and
$t_{\psi}\colon\mathcal{X}\to\mathbb{R}$, for $x_{i}\in\mathbb{R}$,
$j\in\mathbb{N}$ as follows

$\displaystyle T_{S}(x_{1},\dots,x_{n})(j)$
$\displaystyle\mathrel{\mathop{:}}=\sum_{i\leq n}(a_{i}^{j}-b_{i}^{j})x_{i}$
$\displaystyle t_{\psi}(x_{1},\dots,x_{n})\mathrel{\mathop{:}}=\sum_{i\leq
n}(a_{i}-b_{i})x_{i}$

In abstract terms, the set of judgements in $S$ can be thought of as the
inequality $T_{S}(x_{1},\dots,x_{n})\geq 0$ and, similarly, $\psi$ as the
inequality $t_{\psi}(x_{1},\dots,x_{n})\geq 0$. Define the sets

$\displaystyle V_{S}$ $\displaystyle=\\{x^{*}\in\mathcal{X}^{*}\mid\forall
x\in\mathcal{X}.\;T_{S}(x)\geq 0\text{ implies }x^{*}(x)\geq 0\\}\,,$
$\displaystyle Z_{S}$ $\displaystyle=\\{x^{*}\in\mathcal{X}^{*}\mid\exists
y^{*}\in\mathcal{Y}^{*}.\;x^{*}=T^{*}_{S}(y^{*})\text{ and }y^{*}\geq 0\\}\,.$

where $T^{*}_{S}\colon\mathcal{Y}^{*}\to\mathcal{X}^{*}$ is the adjoint of
$T_{S}$ uniquely defined by the adjoint property as
$T^{*}_{S}(y^{*})\mathrel{\mathop{:}}=y^{*}\circ T_{S}$.

By Hurwicz’s general form of Farkas’ Lemma [14], we know that $V_{S}$ is the
_regularly convex envelope_ of $Z_{S}$, which corresponds to the topological
closure $\overline{Z_{S}}$ of $Z_{S}$ for finite-dimensional vector spaces as
$\mathcal{X}^{*}$ is. Let $\pi_{k}\colon\mathcal{Y}\to\mathbb{R}$ denote the
$k^{\text{th}}$-projection function defined as
$\pi_{k}((x_{i})_{i\in\mathbb{N}})=x_{k}$. Clearly
$\pi_{k}\in\mathcal{Y}^{*}$. Moreover, the finite positive linear combinations
of these projections, forms a dense subset $P$ of
$\mathcal{Y}^{*}_{+}=\\{y^{*}\mid y^{*}\geq 0\\}$. Notice that
$Z_{S}=T^{*}_{S}(\mathcal{Y}^{*}_{+})$. Since $T^{*}_{S}$ is a continuous
function, $\overline{Z_{S}}=\overline{T^{*}_{S}(P)}$. As we have established
that $V_{S}=\overline{Z_{S}}$, any element of $V_{S}$ can be approached
arbitrary close by a map of the form $T^{*}_{S}(p)$, for $p\in P$. In simpler
terms, as $T^{*}_{S}(p)=p\circ T_{S}$, any element of $V_{S}$ is arbitrary
close to a finite positive linear combination of judgements in $S$.

By hypothesis, $\psi$ is a semantic consequence of $S$, meaning that,
$t_{\psi}\in V_{S}$. From this, to prove $\vdash\psi$ from $S$ in
$\mathbb{L}_{\mathbbm{1}}^{*}$ we just need to pick an appropriate $p\in P$
(which exists) and replicate the finite positive linear combination it
represents by using the derived rule

$r*\phi_{1}\otimes s*\phi_{2}\vdash r*\psi_{1}\otimes
s*\psi_{2}\lx@proof@logical@and\phi_{1}\vdash\psi_{1}\phi_{2}\vdash\psi_{2}$

to obtain a judgement $\vdash\psi^{\prime}$ that is $\varepsilon$-close to
$\vdash\psi$. As we assumed $\psi$ to be provably equivalent to $\vdash\psi$,
by chaining the two proofs together, we are done.

##  8 Inference Systems for the Lawvere Quantale

In this section, we extend further the concept of proof systems in LLQ and
discuss _inference systems_. These are obtained by requiring that a theory in
$\mathbb{L}_{\mathbbm{1}}^{*}$ obeys extra inferences (proof rules), in
addition to its axioms and to the inferences of
$\mathbb{L}_{\mathbbm{1}}^{*}$. Because in LLQ inferences cannot be
internalized as judgements (see Fact LABEL:fact:wdt), the effect of closing a
theory by a rule does not always produce another theory, as happens in
classical logics, but often a set of theories.

Note that, all the inferences of LLQ have finite sets of hypotheses and so,
when one works with theories of LLQ, will only have derived rules that
contains a finite set of hypotheses. But if we now allow ourselves to work
with inferences that might not be derived from the proof rules, we might have
to handle inferences with a countable set of hypotheses. In fact, for our
purpose, we are interested in only one type of such inferences that we shall
call _inductive inferences_.

######  Definition 8.1 (Inductive inferences).

An _inductive inference_ in LLQ is an inference of type

$\vdash\psi\\{\vdash\phi_{i}\mid i\in\mathbb{N}\\}$

such that for any $i,j\in\mathbb{N}$ with $i<j$, $\phi_{j}\vdash\phi_{i}$.

Observe that the inferences with a finite number of hypotheses are all
particular cases of inductive inferences, since they all can be equivalently
represented firstly as inferences with only one hypothesis (the conjunction of
all the hypotheses); and secondly, this hypothesis can be seen as a constant
sequence of hypotheses. Hence, all the proof rules of LLQ and all the
inferences that can be derived from them are inductive inferences. Last but
not least, observe that any axiom $\vdash\psi$ can be seen as an inductive
inference with an empty set of hypotheses.

######  Definition 8.2.

A theory $\mathbb{T}$ of $\mathbb{L}_{\mathbbm{1}}^{*}$ is _closed under the
inductive inference_

$\vdash\psi\\{\vdash\phi_{i}\mid i\in\mathbb{N}\\}$

if for any diagrammatic extension $\mathbb{T}^{+}$ of $\mathbb{T}$ we have
that

  * •

either $\vdash\psi\in\mathbb{T}^{+}$,

  * •

or there exists $\varepsilon\in[0,\infty)$, $\varepsilon>0$ and
$i\in\mathbb{N}$ such that $\phi_{i}\vdash\varepsilon\in\mathbb{T}^{+}$.

When a model $m$ is such that $\\{\vdash\phi_{i}\mid i\in
I\\}\models_{m}\vdash\psi$, we say that it is a model of the inference $I$.

Observe that the previous definition makes sense semantically, since it
implies that a theory $\mathbb{T}$ of $\mathbb{L}_{\mathbbm{1}}^{*}$ is closed
under the inference $I$ iff any model $m$ of $\mathbb{T}$ is a model of $I$.

######  Definition 8.3 (Inference System).

An _inference system in $\mathbb{L}_{\mathbbm{1}}^{*}$_ is a set $\mathcal{R}$
of inductive inferences in $\mathbb{L}_{\mathbbm{1}}^{*}$.

We say that a model satisfies an inference system if it is a model for each
inference in the system.

A theory is closed with respect to an inference system, if it is closed under
each inference in the system.

Since we can see any axiom of a theory as a particular inference with an empty
set of hypotheses, we see that any finite axiomatic system of LLQ is, in fact,
a particular case of an inference system. There exists, however, interesting
mathematical theories, such as the quantitative equational logic, that cannot
be presented by using an axiomatic system in LLQ, but only by using an
inference system.

Because the finite axiomatic systems in LLQ are particular type of inference
systems, we can read the completeness theorem for finitely-axiomatized
theories proven before, as a particular case of completeness for inference
systems. In what follows, we will enforce these results and prove completeness
results directly for inference systems.

######  Theorem 8.4 (Completeness for inference systems).

Let $\mathcal{R}$ be an inference system of $\mathbb{L}_{\mathbbm{1}}^{*}$ and

$\vdash\psi\\{\vdash\phi_{i}\mid i\in\mathbb{N}\\}$

an inductive inference. If $I$ is satisfied by all the models of
$\mathcal{R}$, then all the finitely axiomatized theories closed under
$\mathcal{R}$ are also closed under $I$.

######  Proof 8.5.

Let $\mathbb{T}$ be a finitely axiomatized theory closed under $\mathcal{R}$.
Then any model $m$ of $\mathbb{T}$ satisfies $I$, hence

  * •

either $m\models(\vdash\psi)$

  * •

or there exist $i\in\mathbb{N}$ and $\varepsilon>0$ such that
$m\models(\phi_{i}\vdash\varepsilon)$.

Applying Corollary 7.5, to $m$ corresponds a diagrammatic theory
$\mathbb{T}_{m}$ such that $m\models(\phi\vdash\phi^{\prime})$ implies
$\phi\vdash\phi^{\prime}\in\mathbb{T}_{m}$; and to each diagrammatic extension
$\mathbb{T}^{+}$ of $\mathbb{T}$ corresponds a model $m_{\mathbb{T}^{+}}$ such
that $m_{\mathbb{T}^{+}}\models(\phi\vdash\phi^{\prime})$ implies
$\phi\vdash\phi^{\prime}\in\mathbb{T}^{+}$.

Consider now an arbitrary diagrammatic extension $\mathbb{T}^{+}$ of
$\mathbb{T}$. Since $m_{\mathbb{T}^{+}}$ is a model of $\mathbb{T}$, we have
that

  * •

either $m_{\mathbb{T}^{+}}\models(\vdash\psi)$, implying
$\vdash\psi\in\mathbb{T}^{+}$,

  * •

or there exist $i\in\mathbb{N}$ and $\varepsilon>0$ such that
$m_{\mathbb{T}^{+}}\models(\phi_{i}\vdash\varepsilon)$, implying
$\phi_{i}\vdash\varepsilon\in\mathbb{T}^{+}$.

Hence, $\mathbb{T}$ is closed under $I$.

###  8.1 The inference system of Quantitative Algebra

In this section, we show how we can use LLQ as a support for quantitative
equational reasoning [20]. Quantitative algebras [20] have been introduced, as
a generalization of universal algebras, meant to axiomatize not only
congruences, but algebraic structures over extended metric spaces. Given an
algebraic similarity type $\Omega$, a quantitative algebra is an
$\Omega$-algebra supported by an extended metric space, so that all the
algebraic operators are nonexpansive. Such a structure can be axiomatized
using an extension of equational logics that uses, instead of equations of
type $s=t$ for some terms $s,t$, quantitative equations of type
$s=_{\varepsilon}t$ for some $\varepsilon\in[0,\infty)$. This quantitative
equation is interpreted as ”the distance between the interpretation of $s$ and
$t$ is less or equal to $\varepsilon$”.

In the theory of quantitative algebras, $=_{\varepsilon}$ are treated as
classic Boolean predicates, so in any model, $s=_{\varepsilon}t$ is either
true or false. However, a different way to look to this, is to actually think
that we only have one equality predicate and $s=t$ is interpreted in the
Lawvere quantale, thus allowing us to reason about the distance between $s$
and $t$. For instance, instead of $s=_{\varepsilon}t$, we could could use the
syntax of $\mathbb{L}_{\mathbbm{1}}^{*}$, treate $s=t$ as an atomic
proposition, and write $\varepsilon\vdash s=t$. This allows us to properly
reason about extended metric spaces and encode, in our logic, the entire
theory of quantitative equational reasoning.

In this section, we show how such an encoding is defined.
$\mathbb{L}_{\mathbbm{1}}^{*}$ has already all the necessary ingredients to do
this work. However, since $\mathbb{L}_{\mathbbm{1}}^{*}$ is only
propositional, the way to do this is to treat all the equations as atomic
propositions. This is exactly how we encode the classic equational logic into
Boolean propositional logic. And, as in the classic case, while this is
sufficient, it unfortunately requires an infinite set of axioms.

As we have already anticipated, the theory of quantitative equational logic
requires an inference system in $\mathbb{L}_{\mathbbm{1}}^{*}$, and it cannot
be only encoded using an axiomatic system. This is because a judgement of type
$s=_{\varepsilon}t\vdash s^{\prime}=_{\delta}t^{\prime}$ in quantitative
reasoning corresponds to the inference $\dfrac{\varepsilon\vdash
s=t}{\delta\vdash s^{\prime}=t^{\prime}}$ which cannot be internalized due to
the fact that in $\mathbb{L}_{\mathbbm{1}}^{*}$ the deduction theorem fails.

Concretely, assuming an algebraic similarity type $\Omega$ and a set $X$ of
variables, we construct all the possible algebraic terms. Let $\Omega X$ be
the set of these terms. We define $\mathbb{L}_{\mathbbm{1}}^{*}$ for
$\mathbb{P}=\\{s=t\mid s,t\in\Omega X\\}$. This gives us the syntax we need.

The original axioms of quantitative equational logic are presented in Table 1,
where they are stated for arbitrary terms
$s,t,u,s_{1},\dots,s_{n},t_{1},\dots,t_{n}\in\Omega X$, for arbitrary $n$-ary
operator $f:n\in\Omega$, arbitrary positive reals
$\varepsilon,\varepsilon^{\prime}\in[0,\infty)$ and arbitrary decreasing
convergent sequence $(\varepsilon_{i})_{i\in\mathbb{N}}$ of positive reals
with limit $\varepsilon$. These axioms, together with the standard
substitution, cut and assumption rules, provide the proof system of
quantitative equational logics.

(Refl) $\displaystyle\vdash t=_{0}t\quad\,$ (Symm) $\displaystyle
s=_{\varepsilon}t\vdash t=_{\varepsilon}s\,$ (Triang) $\displaystyle
t=_{\varepsilon}u,u=_{\varepsilon^{\prime}}s\vdash
t=_{\varepsilon+\varepsilon^{\prime}}s\,$ (Max) $\displaystyle
s=_{\varepsilon}t\vdash s=_{\varepsilon+\varepsilon^{\prime}}t\,$ (Nexp)
$\displaystyle\\{s_{i}=_{\varepsilon}t_{i}\mid i\leq n\\}\vdash
f(s_{1},\dots,s_{n})=_{\varepsilon}f(t_{1},\dots,t_{n})\quad\,$ (Cont)
$\displaystyle\\{s=_{\varepsilon_{i}}t\mid i\in\mathbb{N}\\}\vdash
s=_{\varepsilon}t\,$ Table 1: Quantitative algebras

When translated into LLQ, the substitution, cut, and assumption rules are
embedded in the way a proof operates. And the axioms of quantitative
equational logic can be translated into the corresponding inferences in Table
8.1.

Table 2: Quantitative algebras

However, in this translation, the set of axioms is actually infinite, because
the terms equalities are names for atomic propositions and, as such, we will
have, for instance, a (refl) inference rule for each term $t$, a (symm)
inference rule for each tuple of terms $s$ and $t$, etc. This is not
surprising, as the same situation happens when we encode the classic
equational logic developed for universal algebras in propositional logic.

Observe also that the axiom (cont) of quantitative equational logic, which is
an infinitery axiom, is translated into $\mathbb{L}_{\mathbbm{1}}^{*}$ as an
inductive inference rule. Indeed, first of all, we can convert each hypothesis
of type $\varepsilon_{i}\vdash s=t$ into the equivalent one,
$\vdash\varepsilon_{i}\multimap(s=t)$. And secondly, because for $i\geq j$ we
have $\varepsilon_{i}\leq\varepsilon_{j}$, and this implies that
$\varepsilon_{j}\multimap(s=t)\vdash\varepsilon_{i}\multimap(s=t)$ is a
theorem in $\mathbb{L}_{\mathbbm{1}}^{*}$.

A limitation of this encoding comes from the fact that we need an infinite set
of inductive inferences to rule the quantitative equational reasoning. But
this is similar with what is happening in the classical logic, when one
encodes the classic equational logic into propositional logic. And as in the
classic case, this can be avoided by extending $\mathbb{L}_{\mathbbm{1}}^{*}$
with predicates. This would allow us to present a more compact and finitary
inference system. We leave this extension for future work.

##  9 Conclusions

In this paper, we developed three propositional logics interpreted in the
Lawvere quantale. We develop natural deduction systems for them, which collect
rules similar to rules well-known from other logics. We show that despite
their natural arithmetic interpretation, these logics manifest important
metatheoretical original features that differentiate them from other related
logics. We prove that the logics are incomplete in general, but complete if we
restrict to finitely-axiomatized theories. We present a normalization
algorithm that proves the consequence is decidable and, when made efficient,
establishes complexity bounds. Although one of our logics and results for it
are known in the context of product logics, our proofs are novel in all cases.

We also show that quantitative equational logic can all be encoded in our new
settings. Moreover, we demonstrate that for this class of logics one can
either use axiomatic systems or systems of inferences, the second providing a
higher expressivity from the point of view of mathematical theories that can
be developed.

It would be interesting to extend our logic to allow products as well as sums.
In that case we would be interested in systems of polynomial inequalities,
when the Krivine–Stengle Positivstellensatz would surely come into play [17,
29] in place of the Farkas’ Lemma.

## Acknowledgements

Prakash Panangaden’s visits to the University of Edinburgh have been supported
by a Strategic Talent Grant from the School of Informatics, University of
Edinburgh under a scheme funded by Huawei. His research has also been
supported by research grants from NSERC.

## References

  * [1] Baier, C. and J. Katoen, “Principles of model checking,” MIT Press, 2008\.
URL https://mitpress.mit.edu/9780262026499/principles-of-model-checking/

  * [2] Border, K. C., _Alternative linear inequalities_ , Cal Tech Lecture Notes (2013).
URL https://kcborder.caltech.edu/Notes/Alternative.pdf

  * [3] Esteva, F., L. Godo, P. Hájek and M. Navara, _Residuated fuzzy logics with an involutive negation_ , Arch. Math. Log. 39 (2000), pp. 103–124.
URL https://doi.org/10.1007/s001530050006

  * [4] Fagin, R. and J. Y. Halpern, _Reasoning about knowledge and probability_ , J. ACM 41 (1994), pp. 340–367.
URL https://doi.org/10.1145/174652.174658

  * [5] Fagin, R., R. Riegel and A. G. Gray, _Foundations of reasoning with uncertainty via real-valued logics_ , CoRR abs/2008.02429 (2020).
URL https://arxiv.org/abs/2008.02429

  * [6] Farkas, J., _Theorie der einfachen ungleichungen._ , Journal für die reine und angewandte Mathematik (Crelles Journal) 1902 (1902), pp. 1–27.
URL https://doi.org/10.1515/crll.1902.124.1

  * [7] Fourier, J. B. J., _Solution d’une question particuliere du calcul des inégalités_ , Nouveau Bulletin des Sciences par la Société philomatique de Paris 99 (1826), p. 100.
  * [8] Gärtner, B. and J. Matousek, “Understanding and using linear programming,” Universitext, Springer, 2007.
URL https://doi.org/10.1007/978-3-540-30717-4

  * [9] Goguen, J. A., _Concept representation in natural and artificial languages: Axioms, extensions and applications for fuzzy sets_ , Int. J. Man Mach. Stud. 6 (1974), pp. 513–561.
URL https://doi.org/10.1016/S0020-7373(74)80017-9

  * [10] Hájek, P., _Fuzzy logic and arithmetical hierarchy_ , Fuzzy sets and Systems 73 (1995), pp. 359–363.
URL https://doi.org/10.1016/0165-0114(94)00299-M

  * [11] Hájek, P., “Metamathematics of Fuzzy Logic,” Trends in Logic 4, Kluwer, 1998.
URL https://doi.org/10.1007/978-94-011-5300-3

  * [12] Hájek, P., _What is mathematical fuzzy logic_ , Fuzzy Sets Systems 157 (2006), pp. 597–603.
URL https://doi.org/10.1016/j.fss.2005.10.004

  * [13] Hájek, P., L. Godo and F. Esteva, _A complete many-valued logic with product-conjunction_ , Arch. Math. Log. 35 (1996), pp. 191–208.
URL https://doi.org/10.1007/BF01268618

  * [14] Hurwicz, L., _Programming in linear spaces_ , in: _Traces and Emergence of Nonlinear Programming_ , Springer, 2014 pp. 131–195.
URL https://doi.org/10.1007/978-3-0348-0439-4_8

  * [15] Kozen, D., _Semantics of probabilistic programs_ , Journal of Computer and Systems Sciences 22 (1981), pp. 328–350.
URL https://doi.org/10.1016/0022-0000(81)90036-2

  * [16] Kozen, D., _A probabilistic PDL_ , Journal of Computer and Systems Sciences 30 (1985), pp. 162–178.
URL https://doi.org/10.1016/0022-0000(85)90012-1

  * [17] Krivine, J.-L., _Anneaux préordonnés_ , Journal d’analyse mathématique 12 (1964), pp. p–307.
URL https://hal.science/hal-00165658

  * [18] Lawvere, F. W., _Metric spaces, generalized logic, and closed categories_ , Rendiconti del seminario matématico e fisico di Milano 43 (1973), pp. 135–166.
URL https://doi.org/10.1007/BF02924844

  * [19] Lukasiewicz, J., _Untersuchungen uber den aussagenkalkul_ , CR des seances de la Societe des Sciences et des Letters de Varsovie, cl. III 23 (1930).
  * [20] Mardare, R., P. Panangaden and G. D. Plotkin, _Quantitative algebraic reasoning_ , in: M. Grohe, E. Koskinen and N. Shankar, editors, _Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16_ (2016), pp. 700–709.
URL https://doi.org/10.1145/2933575.2934518

  * [21] Marra, V., _Łukasiewicz logic: An introduction_ , in: G. Bezhanishvili, S. Löbner, V. Marra and F. Richter, editors, _Logic, Language, and Computation - 9th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2011, Revised Selected Papers_ , Lecture Notes in Computer Science 7758 (2011), pp. 12–16.
URL https://doi.org/10.1007/978-3-642-36976-6_3

  * [22] Motzkin, T. S., _Two consequences of the transposition theorem on linear inequalities_ , Econometrica (pre-1986) 19 (1951), p. 184.
  * [23] Nola, A. D. and C. Russo, _The semiring-theoretic approach to MV-algebras: A survey_ , Fuzzy Sets Syst. 281 (2015), pp. 134–154.
URL https://doi.org/10.1016/j.fss.2015.08.026

  * [24] Panangaden, P., “Labelled Markov Processes,” Imperial College Press, 2009\.
URL https://doi.org/10.1142/p595

  * [25] Pavelka, J., _On fuzzy logic III_ , Zeit. Math. Logik u. Grundl. Math. 25 (1979), pp. 447–464.
URL https://doi.org/10.1002/malq.19790250706

  * [26] Savický, P., R. Cignoli, F. Esteva, L. Godo and C. Noguera, _On product logic with truth-constants_ , J. Log. Comput. 16 (2006), pp. 205–225.
URL https://doi.org/10.1093/logcom/exi075

  * [27] Schrijver, A., “Theory of linear and integer programming,” Wiley-Interscience series in discrete mathematics and optimization, Wiley, 1998\.
  * [28] Sen, P., B. W. S. R. de Carvalho, R. Riegel and A. G. Gray, _Neuro-symbolic inductive logic programming with logical neural networks_ , in: _Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022_ (2022), pp. 8212–8219.
URL https://doi.org/10.1609/aaai.v36i8.20795

  * [29] Stengle, G., _A nullstellensatz and a positivstellensatz in semialgebraic geometry_ , Mathematische Annalen 207 (1974), pp. 87–97.
URL https://doi.org/10.1007/BF01362149

  * [30] Stoer, J. and C. Witzgall, “Convexity and optimization in finite dimensions I,” Springer Science & Business Media, 2012.
URL https://doi.org/10.1007/978-3-642-46216-0

  * [31] Vidal, A., F. Esteva and L. Godo, _On modal extensions of product fuzzy logic_ , J. Log. Comput. 27 (2017), pp. 299–336.
URL https://doi.org/10.1093/logcom/exv046

  * [32] Williams, H. P., _Fourier’s method of linear programming and its dual_ , The American mathematical monthly 93 (1986), pp. 681–695.
URL https://doi.org/10.2307/2322281

  * [33] Yaacov, I. B., _On theories of random variables_ , Israel Journal of Mathematics 194 (2013), pp. 957–1012.
URL https://doi.org/10.1007/s11856-012-0155-4

  * [34] Yaacov, I. B. and A. P. Pedersen, _A proof of completeness for continuous first-order logic_ , The Journal of Symbolic Logic 75 (2010), pp. 168–190.
URL https://doi.org/10.2178/jsl/1264433914

  * [35] Yetter, D. N., _Quantales and (noncommutative) linear logic_ , J. Symb. Log. 55 (1990), pp. 41–64.
URL https://doi.org/10.2307/2274953


Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

CAMLIS’23: Conference on Applied Machine Learning for Information Security,
October 19–20, 2023, Arlington, VA

<EMAIL_ADDRESS>orcid=0009-0003-9181-9766, ]

<EMAIL_ADDRESS>orcid=0009-0003-9646-196X, ]

[orcid=0000-0001-9002-1187, ]

[]

[orcid=0009-0004-7611-6947, ]

[]

[]

# Multi-Agent Reinforcement Learning for Maritime Operational Technology Cyber
Security

Alec Wilson  BMT, London, UK  Ryan Menzies  Neela Morarji  David Foster  ADSP,
London, UK  Marco Casassa Mont  Esin Turkbeyler  Lisa Gralewski

(2023)

###### Abstract

This paper demonstrates the potential for autonomous cyber defence to be
applied on industrial control systems and provides a baseline environment to
further explore Multi-Agent Reinforcement Learning’s (MARL) application to
this problem domain. It introduces a simulation environment, IPMSRL, of a
generic Integrated Platform Management System (IPMS) and explores the use of
MARL for autonomous cyber defence decision-making on generic maritime based
IPMS Operational Technology (OT).

OT cyber defensive actions are less mature than they are for Enterprise IT.
This is due to the relatively ‘brittle’ nature of OT infrastructure
originating from the use of legacy systems, design-time engineering
assumptions, and lack of full-scale modern security controls. There are many
obstacles to be tackled across the cyber landscape due to continually
increasing cyber-attack sophistication and the limitations of traditional IT-
centric cyber defence solutions. Traditional IT controls are rarely deployed
on OT infrastructure, and where they are, some threats aren’t fully addressed.

In our experiments, a shared critic implementation of Multi Agent Proximal
Policy Optimisation (MAPPO) outperformed Independent Proximal Policy
Optimisation (IPPO). MAPPO reached an optimal policy (episode outcome mean of
1) after 800K timesteps, whereas IPPO was only able to reach an episode
outcome mean of 0.966 after one million timesteps. Hyperparameter tuning
greatly improved training performance. Across one million timesteps the tuned
hyperparameters reached an optimal policy whereas the default hyperparameters
only managed to win sporadically, with most simulations resulting in a draw.
We tested a real-world constraint, attack detection alert success, and found
that when alert success probability is reduced to 0.75 or 0.9, the MARL
defenders were still able to win in over 97.5% or 99.5% of episodes,
respectively.

###### keywords:

Multi-Agent Reinforcement Learning Cyber Security Operational Technology

##  1 Introduction

Operational Technology (OT) cyber defensive actions are less mature than they
are for Enterprise IT. This is due to the relative ‘brittle’ nature of OT
infrastructure originating from the use of legacy systems, design-time
engineering assumptions, and lack of full-scale modern security controls.
Traditional IT controls are rarely deployed on OT infrastructure, and where
they are, some threats aren’t fully addressed. Additionally, there may be a
lack of trained cyber personnel available in deployed operational OT
environments e.g., at-sea vessels, hence the opportunity to develop autonomous
defensive systems. Reinforcement learning (RL) [1] [2] is a subset of machine
learning that allows an AI-driven system (sometimes referred to as an agent)
to learn through trial and error using feedback signals (through rewards) from
its actions. An agent executes autonomous actions and is given a reward (or
punishment) contingent with the consequences of these actions in an
environment. The agent adapts its strategy, referred to as a policy, to
maximize cumulative reward.

RL has seen key recent developments in various domains such as game
environments e.g., Go [3] and real world problems e.g., video compression [4].
Many domains, including cyber-security, are now using RL to train within
simulated environments. There are a few examples of cyber focused RL
environments in the literature, notably: Yawning Titan [5], CyberBattleSim
[6], and the CybORG environment [7]. These environments are focused on IT
networks and currently lack the ability to train multiple defenders. The
existing environments do not reflect the challenges of cyber defence on an OT
Industrial Control System (ICS). IPMSRL aims to reflect the nuances of OT more
accurately in an abstract simulator and provide a platform for defensive
agents to be trained to recover an IPMS from a cyber-attack.

We applied Multi-agent Reinforcement Learning (MARL) to the cyber defence of
ICSs because of the collaborative nature of the problem. Agents working
together distributed across a network taking coordinated remedial actions is
likely to be more successful than a single, or multiple uncoordinated,
agent(s) working independently.

##  2 Operational Technology Scenario

This paper focused on a generic IPMS, a form of Industrial Control System used
onboard ships and submarines.

An IPMS provides the capability for remote monitoring, control and management
of the ship’s machinery systems and damage control from key components. This
real-time monitoring and control facilitates continuous situational awareness
of the machinery state and damage condition of the ship.

IPMS controls and monitors many ship systems across Propulsion, Power,
Steering, Stability, Auxiliary and Ancillary systems as well as those
providing Damage Control and Fire Fighting (DCFF). To achieve this, IPMS
utilises a distributed control system architecture that facilitates interfaces
with sensors, equipment, plants, software-based control systems and network-
based data.

An IPMS produces alerts in event of failures, anomalies, or issues. These
alerts are not necessarily cyber security alerts; however, they are likely to
be instrumental in the context of cyber-attack detection and response. These
alerts were assumed to be fed into additional Cyber Threat Detection and
Security Information and Event Management (SIEM) tools, leveraging IPMS inputs
to detect and generate relevant attack alerts. The IPMS architecture is based
upon traditional Industrial Control System (ICS) design, inclusive of Remote
Terminal Units (RTUs), Programmable Logic Controllers (PLCs) and multifunction
control consoles providing Human Machine Interfaces (HMIs) combined by a dual
redundant network backbone. Specifically, HMI refers to IPMS consoles as well
as panels on the equipment. The architecture work has been deliberately
abstracted and generalised using open-source information.

##  3 IPMSRL - Simulation Environment

In this paper we introduce IPMSRL, a highly configurable network based multi-
agent RL environment. IPMSRL simulates an abstracted generic maritime IPMS
where defensive agents attempt to restore an infected network. Meanwhile an
attacker attempts to propagate through the network and disrupt IPMS and
controlled systems to negatively impact operations.

The IPMSRL network comprises two types of node: critical nodes and non-
critical infectable nodes. Critical nodes represent components of core-
controlled systems critical to effective operation of the vessel. Two
controlled systems are modelled, Chilled Water Plants (CWPs) and the
Propulsion System. This selection represents a diverse subset of available
controlled systems. Infectable nodes represent HMIs, RTUs, Local Operating
Panels (LOPs), PLCs, and network switches.

The properties of the links between nodes, shown in Figure 1, differ depending
on their type. In Figure 1, the star representation of the network is for
visualisation purposes only. Any HMI/RTU/LOP node which is connected to a
network switch is adjacent to any other node directly connected to a network
switch, i.e., they are interconnected. The network holds redundancy in its
structure through its dual ring network backbone.

Figure 1: Example of an IPMSRL Network Topology.

###  3.1 MITRE ATT&CK® Framework

MITRE ATT&CK111© 2023 The MITRE Corporation. This work is reproduced and
distributed with the permission of The MITRE Corporation.® ICS [8], provides
detailed analysis of typical Tactics, Techniques, and Procedures (TTPs)
adopted by cyber attackers, which is relevant to industrial control systems.

Fine-grained attack steps, based on MITRE ATT&CK® ICS, were implemented to
enable more realism, context and complexity to the cyber defensive remedial
actions. At different MITRE ATT&CK® ICS stages the attacker will have
different capabilities e.g., lateral movement by leveraging an HMI’s network
card and connections. Different defensive remedial actions are required
depending on the MITRE ATT&CK® ICS stage that the attacker has exploited.

The twelve attack stages, represented in IPMSRL, correspond to the associated
MITRE ATT&CK® ICS Tactics are shown in Figure 2:

Figure 2: MITRE ATT&CK® ICS Tactics with the number of techniques for each
tactic [8].

###  3.2 Attacker

The goal of the attacker is to compromise the vessel’s operational capacity,
for example, by disrupting IPMS systems and controlled systems (CWPs,
Propulsion System) which negatively impacts the vessel. An attacker propagates
through the network by initially infecting a non-critical infectable node,
increasing the node’s infection level using an abstraction of the MITRE
ATT&CK® ICS [8], framework, and then infecting an adjacent node. Any given
node after infection acts independently. It is therefore possible that if
multiple nodes are infected then each infected node can progress the infection
or laterally move in the same timestep. This makes it very difficult for the
defender(s) to recover the network to a clean state once an infection has
spread.

Attackers can be created on a sliding scale from fully targeted to fully
viral. Fully targeted attackers move directly towards critical nodes
displaying ‘knowledge’ of the network. Fully viral attackers move randomly to
any adjacent node. Partially viral attackers move towards critical nodes but
may also move randomly with a given configured probability.

Attackers also have other configurable attributes such as the probability an
infection will progress through the MITRE ATT&CK® ICS stages or the
probability of a successful lateral move.

###  3.3 Alerts

Each of the infectable nodes has an alert system which can be triggered when
an infection is present or when an attacker initially tries to infect a non-
infected node. The probability that an alert is successfully parsed to the
defender(s) allows the user to configure the scale of asymmetric information
within the environment. In the context of this paper, an assumption was made
that IPMS-generated alerts were fed into a SIEM for further processing and
cyber threat detection. The alert success probability, therefore, directly
impacts the partial observability of the defender’s observation space.

It is worth noting that the alerts are static in nature. This means that if an
alert is set off at a certain timestep, the defender will receive information
about the progress of the node infection at a given timestep. No further
information about the progression of the infection will be given to the
defender unless another alert is set off or the defender takes a remedial
action on a node.

###  3.4 NIST SP-800-61

NIST SP-800-61 [9], describes a standard process to handle cyber incidents and
responses. The three key cyber defensive steps relevant to the problem space
are Contain, Eradicate, and Recover, shown in Figure 3. Each of these types of
action need to be taken in a logical order based on cyber defensive best
practice. In general, this will be to contain an attack to avoid it spreading
across systems, eradicate the attack to remove it from the infected system and
recover a node to return the system back to an operational state. The order of
these actions is important and other factors such as the severity of infection
impact the effectiveness and ease of taking these actions.

Figure 3: Summary of NIST SP-800-61 Remedial Actions, adapted to targeted
Maritime / OT scenario.

###  3.5 Defensive Remedial Actions

Each defensive agent can take four types of action: Contain, Eradicate,
Recover and Wait. These are aligned with the real-world cyber incident
response process indicated in NIST SP-800-61 discussed above.

Containing makes a given node un-operational but prevents the infection from
propagating from that node. Eradicating cleans a node of infection. Recovering
returns the node to an operational state. For critical nodes, only the recover
and wait actions are available whereas, for all other nodes, all actions are
available. At each timestep, each defender in succession takes an action. Each
of these actions have a configurable delay where a timestep lag is applied
depending on the infection state of the node and type of action. This delay
tries to reflect the real-world differences between taking simple actions
against early infections e.g., modifying credentials, and taking more extreme
actions to prevent unrecoverable damage e.g., quarantining systems. Additional
dialogue on valuing the costs of remedial actions is considered in later
discussion about the reward function.

IPMSRL supports partial observability in which each defensive agent has its
own view of the network state. In addition to the alerts, defensive agents can
investigate a node’s true infection information by interacting with that node.
This knowledge is not shared amongst other defensive agents.

###  3.6 Reward Function

IPMSRL features a highly customisable reward function for both global and
intrinsic rewards. Global rewards are awarded to the agents at the end of the
episode, whereas intrinsic rewards are awarded within an episode222The global
and intrinsic rewards are divided and shared equally between each agent..
Global rewards have been subdivided into mission objective and state rewards.
The implemented reward function aims to tackle the problem of sparse global
rewards, where agents struggle to train since they only receive a small number
of reward signals, often at the end of an episode. This is a known problem
within RL, and specifically within applied control problems such as robotics
[10]. The reward function used in IPMSRL uses a combination of intrinsic
rewards and reward shaping [11] [12] to allow for further experimentation into
how these additions positively/negatively affect training. The mission
objective is defined as follows for win/loss/draw. For episode step $t$ and
max steps in an episode $T$, a win, draw or loss is defined as:

  * •

Win (+1) – There are no infected nodes or contained nodes, and $t<T$.

  * •

Loss (-1) – Any of the critical infrastructure has been infected, and $t<T$.

  * •

Draw (+0) – $t=T$ and neither the win nor loss criteria has been met for t
steps.

For our experiments, $T=50$.

The state reward reflects the impact to non-critical and critical nodes during
the episode and is graded as low, medium or high. Critical nodes, such as
PLCs, RTUs and PCSs that directly control machinery or switches, are more
strongly penalised than other nodes, such as HMIs. The weighting of penalties
was informed by the failure effects and impact analysis of a generic IPMS.
State reward is produced by a 50/50 split of ‘state generic’ and ‘state
specific’ rewards:

State Generic – this refers to penalties that are provided when nodes within
the environment meet certain conditions e.g., a node is contained but not
infected or a node is uninfected and contained without being recovered.

State Specific – this is defined, in levels of severity, as the number of
different types of nodes which had been infected in an episode. For example,
if two HMIs were infected then the smallest negative reward value (defined in
the config) is applied.

IPMSRL has the ability for agents to receive intrinsic rewards called action
score rewards. The defender(s) receive a negative reward depending on the
action chosen and the status of the node that is being interacted with (graded
as low, medium or high). Nodes with a more severe infection status receive a
higher penalty. The agents are therefore incentivised to deal with infections
early when they are first alerted. The weighting of the reward function
components are user configurable and will be discussed in further detail
within the experimental results section.

##  4 Multi-Agent Reinforcement Learning (MARL)

In this paper, two MARL algorithms, IPPO [13], and MAPPO [14], were
tested333Multi-Agent Deep Deterministic Policy Gradient (MADDPG) and Q-MIX
were also explored but the implementations within Ray and RLlib were found to
be unstable during training on IPMSRL.. Our implementation of IPPO is
equivalent to the IPPO algorithm referenced in the original paper [13]. In
IPPO, each agent has an actor and critic network with the actor network
representing the policy, and the critic network representing the value
function. These actor and critic networks are independent to each agent. Our
MAPPO implementation is slightly different to the MAPPO algorithm used in the
original paper [14]. The original paper states that their MAPPO algorithm uses
shared parameters for both the policy and critic networks. The MAPPO
implementation used in this paper uses independent policy networks for each
agent, but uses a shared centralised critic also referred to as a centralised
value function. An important note is that in other papers, some MAPPO
implementations use shared information between agents by using the joint
observations and action spaces444This is the same as the implementation within
MARLlib [15], using the global state within training.. Both Proximal Policy
Optimisation (PPO) based algorithms were stable during training and
demonstrated the ability to recover an infected network within IPMSRL. Two
defensive agents were used for all the experiments in this paper. The hardware
used for training was a 6 core CPU, 56GB RAM and a NVIDIA Tesla K80 with 12GBs
of vRAM. Ray Tune [16] and RLlib were utilised for training. Training the PPO
based algorithms for one million timesteps took approximately one hour. The
performance metrics used for the experiments were mean episode reward, mean
episode length and mean episode outcome which is the mean of the episode
outcomes (win (+1)/draw (+0.5)/loss (0)).

###  4.1 Hyperparameter Tuning with MAPPO

An Initial hyperparameter tuning stage to create a baseline for the
environment parameter experiments was completed. A brief grid-search over
commonly successful hyperparameters was used for eleven PPO specific and
general machine learning hyperparameters. In Figure 4, a clear difference
between the training performance between the tuned and default hyperparameters
can be seen. The hyperparameters which were most influential in the improved
performance were the Learning Rate, Gamma, Lambda and the Clip Parameter. When
MAPPO was trained using the default hyperparameters, it converged to an
optimal policy more slowly than the tuned model, but it was still able to
reach an optimal policy. MAPPO was also used during the Experimental Results
section. Throughout the experiments, it was found that in general, PPO based
algorithms were still able to improve their performances during training with
most configurations of hyperparameters.

Figure 4: Comparison between default and tuned hyperparameters on MAPPO with
90% CI.

###  4.2 IPPO vs MAPPO

MAPPO outperformed IPPO, converging to the optimal policy quicker. This
statement is based on the higher win rate, higher reward total and the ability
to win an episode in fewer episode steps, suggesting a more efficient strategy
has developed. The point at which the two algorithms diverge in Figure 5
underpins some of the differences in performance. At 200K timesteps IPPO and
MAPPO have similar performance and are drawing most episodes. After this
point, both IPPO and MAPPO start to develop a winning policy but with MAPPO
optimising its policy at a faster rate. In our experimentation, MAPPO clearly
gains an advantage using the same critic network. The centralised critic
allows for the agents to find a better policy where agents are collaborative
faster than without the shared critic network. This is the converse to what
has been found elsewhere in the literature, where the addition of a shared
value function reduced the performance significantly [13].

MAPPO’s confidence interval (90%) bands were much narrower than IPPO. The
narrower area of the confidence interval suggests that the individual trials
of MAPPO algorithm were more stable than IPPO, implying the training is more
consistent. This experiment demonstrates that the centralised critic can help
improve the policy updates at each training epoch.

Figure 5: IPPO vs MAPPO Experiment with a CI of 90%

##  5 Experimental Results

###  5.1 Alert Success Probability

A configurable attacker parameter is the alert success probability: this is
the probability of an alert being set off on any infected node after an
infection on a node progresses successfully laterally to another node.

Figure 6: Alert Success Probability Experiment.

Figure 6.1 shows that the episode outcome mean for probabilities 0.00 (blue
plot) and 0.1 (orange plot) converges to 0.5. This suggests that almost every
episode is ending in a draw. Figure 6.3 shows they all converge to episode
length mean of 50. This implies the defender is not receiving enough
information to win but is managing to draw nearly all episodes.

In Table 1, the impact of the defenders receiving more accurate information
about the environment is clear. The more accurate the information they
receive, the better they can perform. Without an alert success probability of
1, within the training time set, none of the parameters were able to produce
an optimal strategy. However, an agent with an alert probability of 0.75 or
0.9 was still able to win in over 97.5% or 99.5% of episodes, respectively.
These results suggest that the agents can learn effective strategies in
partially observable environments, but that the SIEMs alert detection and
processing is important to the success of autonomous cyber defence.

Table 1: Alert Success Probability Experiment Results. Parameter | Episode Outcome Mean | Episode Reward Mean | Episode Length Mean |
---|---|---|---|---
0 | 0.4963 | -4.8858 | 49.9803 |
0.1 | 0.4927 | -4.0741 | 49.7891 |
0.25 | 0.5463 | -1.5508 | 43.5021 |
0.5 | 0.7913 | 0.0672 | 22.9676 |
0.75 | 0.9772 | 0.845 | 5.8354 |
0.9 | 0.9962 | 0.9454 | 3.9113 |
1 | 0.9995 | 0.9801 | 3.2588 |

###  5.2 Reward Experiments

In Figure 7, an investigation into the difference in training performance
between state-based rewards and balanced rewards was conducted. State based
reward refers to a reward function solely made up of the state rewards
discussed in the reward function section. Whereas balanced reward also
includes intrinsic rewards, given to the agents during an episode based on
their actions, and an overall score based on the episode outcome. Using solely
state rewards, convergence towards a winning strategy was faster than for
balanced rewards, but performed less optimally overall than balanced rewards.
Figure 7 shows the two parameter sets plotted with 90% confidence intervals,
validating their significant differences in behaviour.

Figure 7: Reward Shaping Experiment - State Reward vs Balanced Reward with 90%
CI.

Figure 7.1 shows that once the state-based reward parameter reaches an episode
outcome mean of almost 1, indicating it has won almost every episode, the
episode length mean, shown in Figure 7.3 reaches a value around 10 steps per
episode. It then plateaus for the duration of the training. This is a far
higher mean steps per episode than the balanced reward agents. A lower episode
length mean suggests that the defender(s), if the win rate is near 100%, find
a more efficient defensive strategy. The balanced reward approach, which
initially converges toward a winning strategy more slowly, reaches an episode
length mean of 3.18. This is a dramatic improvement and represents a far more
effective and performant strategy. The state reward agents have no incentive
to improve or fine-tune their behaviour further than the condition required to
reliably win. The agents trained with just state reward are therefore ’lazy’
with their action choices, taking more actions than is necessary to win an
episode. This experiment shows the value of reward shaping and how important
the dynamics of agent incentives are to a performant outcome.

##  6 Conclusion and Future Work

This paper introduced IPMSRL, a highly configurable network based multi-agent
RL environment and demonstrated the capabilities of MARL agents to
successfully recover an abstract IPMS to an operational state following a
cyber-attack. Findings demonstrate that hyperparameter tuning, reward shaping
and the quality of alerts are all important aspects in developing performant
agents.

A key issue with using a simulator to train an RL agent is the sim-to-real-
gap. This describes the differences present between real systems and the
simulated environments that are used to replicate them and the problems that
even small differences can cause. The issues are compounded further when
environments are intentionally abstracted away from the real system for
reasons of dimensionality, security or complexity. RL simulators such as
IPMSRL are important for developing the core concepts needed to build
confidence and understanding in the techniques being employed, such as MARL.
But more realistic simulators or emulators will be required to facilitate
movement towards applying these concepts on real systems, which should be the
eventual goal.

Another avenue of future research is the generalisability of the agents.
Agents will need to be able to adapt to different types of attack, scenario
(where components may be valued differently) and network topology. Without
demonstrating this flexibility, agents are unlikely to be stable enough to be
trusted in real world control systems.

###### Acknowledgements.

Research funded by Frazer-Nash Consultancy Ltd. on behalf of the Defence
Science and Technology Laboratory (Dstl) which is an executive agency of the
UK Ministry of Defence providing world class expertise and delivering cutting-
edge science and technology for the benefit of the nation and allies. The
research supports the Autonomous Resilient Cyber Defence (ARCD) project within
the Dstl Cyber Defence Enhancement programme. The authors would also like to
thank Clare Jubb, Andy Pollard, Christos Giachritsis, Jake Rigby, Ben Golding,
Julie Kimbrey and Brian Bassil for their wider contribution to the project and
paper.

## References

  * Barto et al. [1995] A. Barto, S. Bradtke, S. Singh, Learning to Act using Real-Time Dynamic Programming’, 1995.
  * Sutton and Barto [2018] R. Sutton, A. Barto,  Reinforcement learning: an introduction, Second edition,  in: Adaptive computation and machine learning series, The MIT Press, Cambridge, Massachusetts, 2018.
  * Silver et al. [2016] D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbrenner, I. Sutskever, T. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, D. Hassabis,  Mastering the game of Go with deep neural networks and tree search,  Nature 529 (2016) 484–489. URL: https://doi.org/10.1038/nature16961. doi:10.1038/nature16961.
  * Mandhane et al. [2022] A. Mandhane, A. Zhernov, M. Rauh, C. Gu, M. Wang, F. Xue, W. Shang, D. Pang, R. Claus, C.-H. Chiang, C. Chen, J. Han, A. Chen, D. J. Mankowitz, J. Broshear, J. Schrittwieser, T. Hubert, O. Vinyals, T. Mann, MuZero with Self-competition for Rate Control in VP9 Video Compression, 2022. URL: http://arxiv.org/abs/2202.06626, arXiv:2202.06626 [cs, eess].
  * Andrew et al. [2022] A. Andrew, S. Spillard, J. Collyer, N. Dhir, Developing Optimal Causal Cyber-Defence Agents via Cyber Security Simulation’, 2022. URL: http://arxiv.org/abs/2207.12355, volume: 26.
  * Research [2021] M. D. Research, CyberBattleSim’, 2021\. URL: https://github.com/microsoft/cyberbattlesim.
  * Standen et al. [2021] M. Standen, M. Lucas, D. Bowman, T. Richer, J. Kim, D. Marriott,  CybORG: A Gym for the Development of Autonomous Cyber Agents’,  arXiv 26 (2021) 2023\. URL: http://arxiv.org/abs/2108.09118.
  * noa [2023] The MITRE Corporation, ‘MITRE ATT&CK ICS MATRIX’, 2023. URL: https://attack.mitre.org/matrices/ics/.
  * Cichonski et al. [2012] P. Cichonski, T. Millar, T. Grance, K. Scarfone, Computer Security Incident Handling Guide : Recommendations of the National Institute of Standards and Technology, Technical Report NIST SP 800-61r2, National Institute of Standards and Technology, 2012\. URL: https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-61r2.pdf. doi:10.6028/NIST.SP.800-61r2.
  * Qureshi et al. [2018] A. Qureshi, Y. Nakamura, Y. Yoshikawa, H. Ishiguro,  Intrinsically motivated reinforcement learning for human-robot interaction in the real-world’,  Neural Netw 107 (2018) 23–33,. doi:10.1016/j.neunet.2018.03.014.
  * Popov et al. [2017] I. Popov, N. Heess, T. Lillicrap, R. Hafner, G. Barth-Maron, M. Vecerik, T. Lampe, Y. Tassa, T. Erez, M. Riedmiller,  Data-efficient Deep Reinforcement Learning for Dexterous Manipulation (2017).
  * Mguni et al. [2022] D. H. Mguni, T. Jafferjee, J. Wang, O. Slumbers, N. Perez-Nieves, F. Tong, L. Yang, J. Zhu, Y. Yang, J. Wang, LIGS: Learnable Intrinsic-Reward Generation Selection for Multi-Agent Learning, 2022. URL: http://arxiv.org/abs/2112.02618, arXiv:2112.02618 [cs].
  * de Witt et al. [2020] C. S. de Witt, T. Gupta, D. Makoviichuk, V. Makoviychuk, P. H. S. Torr, M. Sun, S. Whiteson, Is Independent Learning All You Need in the StarCraft Multi-Agent Challenge?, 2020\. URL: http://arxiv.org/abs/2011.09533, arXiv:2011.09533 [cs].
  * Yu et al. [2022] C. Yu, A. Velu, E. Vinitsky, J. Gao, Y. Wang, A. Bayen, Y. Wu, The Surprising Effectiveness of PPO in Cooperative, Multi-Agent Games, 2022. URL: http://arxiv.org/abs/2103.01955, arXiv:2103.01955 [cs].
  * Hu et al. [2023] S. Hu, Y. Zhong, M. Gao, W. Wang, H. Dong, Z. Li, X. Liang, X. Chang, Y. Yang, MARLlib: A Scalable Multi-agent Reinforcement Learning Library, 2023. URL: http://arxiv.org/abs/2210.13708, arXiv:2210.13708 [cs].
  * Liaw et al. [2018] R. Liaw, E. Liang, R. Nishihara, P. Moritz, J. E. Gonzalez, I. Stoica,  Tune: A research platform for distributed model selection and training,  arXiv preprint arXiv:1807.05118 (2018).