# Obligations and permissions, algebraically

Andrea De Domenico  Ali Farjami  Krishna Manoorkar  Alessandra Palmigiano
Mattia Panettiere  Xiaolong Wang

###### Abstract

We further develop the algebraic approach to input/output logic initiated in
[1], where subordination algebras and a family of their generalizations were
proposed as a semantic environment of various input/output logics. In
particular, we consider precontact algebras as a suitable algebraic
environment for negative permission, and we characterize properties of several
types of permission (negative, static, dynamic), as well as their interactions
with normative systems, by means of suitable modal languages encoding outputs.

###### keywords:

input/output logic, subordination algebras, precontact algebras,
selfextensional logics, slanted algebras, algorithmic correspondence theory.

###### MSC:

03G25 , 03G10

††journal: Annals of Pure and Applied Logic

[inst1]organization=School of Business and Economics, Vrije Universiteit
Amsterdam,addressline=The Netherlands

[inst2]organization=School of Computer Engineering, Iran University of Science
and Technology,addressline=Tehran, country=Iran

[inst3]organization=Department of Mathematics and Applied Mathematics,
University of Johannesburg,addressline=South Africa

[inst4]organization=School of Philosophy and Social Development, Shandong
University,addressline=Jinan, country=China

##  1 Introduction

The present paper continues a line of investigation, recently initiated in
[1], which pursues the study of input/output logic from the viewpoint of
algebraic logic [2], by establishing systematic connections between
input/output logic and subordination algebras, two areas of research in non-
classical logics which have been pursued independently of one another by
different research communities, with different motivations and methods.

The framework of input/output logic [3] is designed for modelling the
interaction between logical inferences and other agency-related notions such
as conditional obligations, goals, ideals, preferences, actions, and beliefs,
in the context of the formalization of normative systems in philosophical
logic and AI. Recently, the original framework of input/output logic, based on
classical propositional logic, has been generalized to incorporate various
forms of nonclassical reasoning [4, 5], and these generalizations have
contextually motivated the introduction of algebraic and proof-theoretic
methods in the study of input/output logic [6, 7].

Subordination algebras [8] are tuples $(A,\prec)$ consisting of a Boolean
algebra $A$ and a binary relation $\prec$ on $A$ such that the direct (resp.
inverse) image of each element $a\in A$ is a filter (resp. an ideal) of $A$.
These structures have been introduced for connecting and systematising several
notions (including pre-contact algebras [9] and quasi-modal algebras [10, 11],
of which subordination algebras are equivalent presentations, and proximity
lattices [12]) cropping up in the context of generalizations of Stone duality,
within a research program which brings together constructive and point-free
mathematics, non-classical logics, and their applications to the
(denotational) semantics of programming languages. For instance, in the
context of proximity lattices, the proximity relation $\prec$ relates (the
algebraic interpretation of) two logical propositions $\varphi$ and $\psi$ if,
whenever $\varphi$ is observed, $\psi$ is actually true. In [1], subordination
algebras and generalizations thereof are proposed as an algebraic semantic
framework for several input/output logics. Moreover, via the recently
established link between subordination algebras and slanted algebras [13],
well-known properties of normative systems and their associated output
operators have been equivalently characterized in terms of modal axioms, using
results from the general theory of unified correspondence [14, 15, 16]. In the
present paper, we systematically study the algebraic counterparts of
normative, permission, and dual permission systems based on the algebras of
the classes canonically associated with (fully) selfextensional logics [17,
18]; normative, permission, and dual permission systems on selfextensional
logics have been introduced and studied in the companion paper [19]. In
particular, in the present paper, we refine and streamline the proof of the
main characterization result [1, Proposition 3.7], and further extend it to
characterize properties of various notions of permission systems also in
relation to normative systems, by means of modal axioms in an expanded
signature which includes negative modal operators (intuitively representing
prohibitions). Moreover, we apply these characterization results to resolve
different issues: we obtain logical characterizations of output operators for
both normative and permission systems; we obtain dual characterizations of
conditions on subordination algebras (resp. precontact algebras) and on their
associated spaces; we algebraize positive static permissions, and modally
characterize the notion of cross-coherence; we clarify the relation between
certain conditions on positive bi-subordination lattices and Dunn’s axioms for
positive modal logic.

#### Structure of the paper

In Section 2, we collect basic definitions and facts about the abstract
logical framework of selfextensional logics in which we are going to develop
our results, and recall the definition of normative systems, introduced in
[1], pertaining to this framework. We also introduce, discuss and study the
properties of negative permission systems in the context of selfextensional
logics. In Section 3, we partly recall, partly introduce, semantic structures
generalizing subordination algebras and precontact algebras, which we take as
the algebraic semantic environment of input/output logics based on
selfextensional logics and their associated permission systems, and study the
basic properties of these algebraic models. In Section 4, we partly recall,
partly define, how these algebraic structures can be associated with certain
classes of slanted algebras [20] (cf. Definition 2.8), which form an algebraic
environment in which output operators from input/output logic can be
systematically represented as modal operators endowed with order-theoretic,
algebraic, and topological properties. In Section 5, we characterize
conditions on (the algebraic counterparts of) normative systems and permission
systems in terms of the validity of modal inequalities on their associated
slanted algebras. In Section 6, we use the results of the previous section to
characterize the output operators of both normative and permission systems in
terms of properties of their associated modal operators (cf. Propositions 6.1,
6.3, and 6.4), to define the algebraic counterparts of the static positive
permission systems and modally characterize the notion of cross coherence (cf.
Section 6.2), to extend Celani’s dual characterization results for
subordination lattices, and obtain both these results and similar results as
consequences of standard modal correspondence (cf. Propositions 6.11, 6.12,
and 6.13), and to clarify the relation between certain conditions on positive
bi-subordination lattices and Dunn’s axioms for positive modal logic (cf.
Section 6.4). We conclude in Section 7. In the appendix, we adapt some of
Jansana’s results on selfextensional logics with conjunction [18] to the
setting of selfextensional logics with disjunction.

##  2 Preliminaries

The present section collects preliminaries on selfextensional logics (cf.
Section 2.1), on normative and permission systems based on these (cf. Section
2.2), on subordination algebras and related structures (cf. Section 2.3), on
canonical extensions and slanted algebras (cf. Section 2.4).

###  2.1 Selfextensional logics

In what follows, we align to the literature in abstract algebraic logic [2],
and understand a logic to be a tuple $\mathcal{L}=(\mathrm{Fm},\vdash)$, such
that $\mathrm{Fm}$ is the term algebra (in a given algebraic signature which,
abusing notation, we will also denote by $\mathcal{L}$) over a set
$\mathsf{Prop}$ of atomic propositions, and $\vdash$ is a consequence relation
on $\mathrm{Fm}$, i.e. $\vdash$ is a relation between sets of formulas and
formulas such that, for all $\Gamma,\Delta\subseteq\mathrm{Fm}$ and all
$\varphi\in\mathrm{Fm}$, (a) if $\varphi\in\Gamma$ then $\Gamma\vdash\varphi$;
(b) if $\Gamma\vdash\varphi$ and $\Gamma\subseteq\Delta$, then
$\Delta\vdash\varphi$; (c) if $\Delta\vdash\varphi$ and $\Gamma\vdash\psi$ for
every $\psi\in\Delta$, then $\Gamma\vdash\varphi$; (d) if
$\Gamma\vdash\varphi$, then $\sigma[\Gamma]\vdash\sigma(\varphi)$ for every
homomorphism (i.e. variable-substitution) $\sigma:\mathrm{Fm}\to\mathrm{Fm}$.
Clearly, any such $\vdash$ induces a preorder on $\mathrm{Fm}$, which we still
denote $\vdash$, by restricting to singletons. A logic $\mathcal{L}$ is
selfextensional (cf. [17]) if the relation
${\equiv}\subseteq\,\mathrm{Fm}\times\mathrm{Fm}$, defined by
$\varphi\equiv\psi$ iff $\varphi\vdash\psi$ and $\psi\vdash\varphi$, is a
congruence of $\mathrm{Fm}$. In this case, the Lindenbaum-Tarski algebra of
$\mathcal{L}$ is the partially ordered algebra
$Fm=(\mathrm{Fm}/{\equiv},\vdash)$ where, abusing notation, $\vdash$ also
denotes the order on $\mathrm{Fm}/{\equiv}$ defined as
$[\varphi]_{\equiv}\vdash[\psi]_{\equiv}$ iff $\varphi\vdash\psi$. For any
algebra $\mathbb{A}$ of the same signature of $\mathcal{L}$, a subset $F$ of
the domain $A$ of $\mathbb{A}$ is an $\mathcal{L}$-filter of $\mathbb{A}$ if
for every $\Gamma\cup\\{\varphi\\}\subseteq\mathrm{Fm}$ and every homomorphism
$h:\mathrm{Fm}\to\mathbb{A}$, if $\Gamma\vdash\varphi$ and $h[\Gamma]\subseteq
F$, then $h(\varphi)\in F$. Let $\mathrm{Fi}_{\mathcal{L}}\mathbb{A}$ denote
the set of $\mathcal{L}$-filters of $\mathbb{A}$. It is easy to see that
$\mathrm{Fi}_{\mathcal{L}}\mathbb{A}$ is a closure system over $\mathbb{A}$,
where a closure system over $\mathbb{A}$ is a collection of subsets of
$\mathbb{A}$ which is closed under arbitrary intersection. A g-model of
$\mathcal{L}$ is a tuple $(\mathbb{A},\mathcal{G})$ s.t. $\mathbb{A}$ is an
$\mathcal{L}$-algebra and
$\mathcal{G}\subseteq\mathrm{Fi}_{\mathcal{L}}\mathbb{A}$ is a closure system
over $\mathbb{A}$. Any such $\mathcal{G}$ induces a consequence relation
$\models_{\mathcal{G}}$ on $\mathrm{Fm}$ defined by
$\Gamma\models_{\mathcal{G}}\varphi$ iff for all $h\in
Hom(\mathrm{Fm},\mathbb{A})$ and all $F\in\mathcal{G}$, if $h[\Gamma]\subseteq
F$ then $h(\varphi)\in F$. It follows straightforwardly from the definitions
that $\vdash\ =\ \models_{\mathrm{Fi}_{\mathcal{L}}\mathbb{A}}\ \subseteq\
\models_{\mathcal{G}}$. A g-model is full whenever $\vdash\ =\
\models_{\mathcal{G}}$. Any g-model $(\mathbb{A},\mathcal{G})$ induces an
equivalence relation $\equiv_{\mathcal{G}}$ on $\mathbb{A}$, referred to as
the Frege relation of $(\mathbb{A},\mathcal{G})$, defined as follows:
$a\equiv_{\mathcal{G}}b$ whenever $a\in F$ iff $b\in F$ for any
$F\in\mathcal{G}$. Clearly,
$\mathcal{G}\subseteq\mathrm{Fi}_{\mathcal{L}}\mathbb{A}$ implies that
$\equiv_{\mathrm{Fi}_{\mathcal{L}}\mathbb{A}}\ \subseteq\
\equiv_{\mathcal{G}}$. Then the logic $\mathcal{L}$ is fully selfextensional
if $\equiv_{\mathcal{G}}$ is a congruence of (the algebra of) any full g-model
$(\mathbb{A},\mathcal{G})$ of $\mathcal{L}$. The class
$\mathsf{Alg}(\mathcal{L})$ canonically associated with a fully
selfextensional logic $\mathcal{L}$ is the class of those
$\mathcal{L}$-algebras $\mathbb{A}$ such that some full g-model
$(\mathbb{A},\mathcal{G})$ exists s.t. $\equiv_{\mathcal{G}}$ is the identity
$\Delta_{\mathbb{A}}$. Thus, $\mathsf{Alg}(\mathcal{L})=\\{\mathbb{A}\mid\
\equiv_{\mathrm{Fi}_{\mathcal{L}}\mathbb{A}}\ =\ \Delta_{\mathbb{A}}\\}$, and
so, on any $\mathbb{A}\in\mathsf{Alg}(\mathcal{L})$, the specialization
preorder induced by $\mathrm{Fi}_{\mathcal{L}}\mathbb{A}$ is a partial order.

For any selfextensional logic $\mathcal{L}$, the intrinsic variety of
$\mathcal{L}$ is the variety $\mathsf{K}_{\mathcal{L}}$ generated by the
Lindenbaum-Tarski algebra $Fm$. Hence,
$\mathsf{K}_{\mathcal{L}}\models\varphi=\psi$ iff $\varphi\dashv\vdash\psi$
for all $\varphi,\psi\in\mathrm{Fm}$. It is well known that
$\mathsf{Alg}(\mathcal{L})\subseteq\mathsf{K}_{\mathcal{L}}$ (cf. [18, Lemma
3.10]).

The environment described above takes the notion of consequence relation as
primary in defining a logical system, and in particular, it abstracts away
from any concrete logical signature. However, the familiar logical connectives
such as conjunction and disjunction can be reintroduced in terms of of their
behaviour w.r.t. the consequence relation of the given logic. Indeed, for any
$\Gamma\subseteq\mathrm{Fm}$, let
$Cn(\Gamma):=\\{\psi\mid\Gamma\vdash\psi\\}$.111In what follows, we write e.g.
$Cn(\varphi)$ for $Cn(\\{\varphi\\})$, and $Cn(\Gamma,\varphi)$ for
$Cn(\Gamma\cup\\{\varphi\\})$. The conjunction property $(\wedge_{P})$ holds
for $\mathcal{L}$ if a term $t(x,y)$ (which we denote $x\wedge y$) exists in
the language of $\mathcal{L}$ such that
$Cn(\varphi\wedge\psi)=Cn(\\{\varphi,\psi\\})$ for all
$\varphi,\psi\in\mathrm{Fm}$. The disjunction property $(\vee_{P})$ holds for
$\mathcal{L}$ if a term $t(x,y)$ (which we denote $x\vee y$) exists in the
language of $\mathcal{L}$ such that $Cn(\varphi\vee\psi)=Cn(\varphi)\cap
Cn(\psi)$ for all $\varphi,\psi\in\mathrm{Fm}$. The strong disjunction
property $(\vee_{S})$ holds for $\mathcal{L}$ if a term $t(x,y)$ (which we
denote $x\vee y$) exists in the language of $\mathcal{L}$ such that
$Cn(\Gamma,\varphi\vee\psi)=Cn(\Gamma,\varphi)\cap Cn(\Gamma,\psi)$ for all
$\varphi,\psi\in\mathrm{Fm}$ and every $\Gamma\subseteq\mathrm{Fm}$.

The weak negation property ($\neg_{W}$) holds for $\mathcal{L}$ if a term
$t(x)$ (which we denote $\neg x$) exists in the language of $\mathcal{L}$ such
that $\psi\in Cn(\varphi)$ implies $\neg\varphi\in Cn(\neg\psi)$ for any
$\varphi,\psi\in\mathrm{Fm}$. For any logic $\mathcal{L}$ with $\neg_{W}$,

  1. 1.

The right-involutive negation property ($\neg_{Ir}$) holds for $\mathcal{L}$
if $Cn(\neg\neg\varphi)\subseteq Cn(\varphi)$ for any $\varphi\in\mathrm{Fm}$.

  2. 2.

The left-involutive negation property ($\neg_{Il}$) holds for $\mathcal{L}$ if
$Cn(\varphi)\subseteq Cn(\neg\neg\varphi)$ for any $\varphi\in\mathrm{Fm}$.

  3. 3.

The involutive negation property ($\neg_{I}$) holds for $\mathcal{L}$ if both
$\neg_{Il}$ and $\neg_{Ir}$ hold for $\mathcal{L}$.

  4. 4.

The absurd negation property ($\neg_{A}$) holds for $\mathcal{L}$ if
$Cn(\varphi,\neg\varphi)=\mathrm{Fm}$ for any $\varphi\in\mathrm{Fm}$.

  5. 5.

The pseudo negation property ($\neg_{P}$) holds for $\mathcal{L}$ if
$\wedge_{P}$ holds for $\mathcal{L}$, and moreover, $\neg\psi\in
Cn(\varphi,\neg(\varphi\wedge\psi))$ for any $\varphi,\psi\in\mathrm{Fm}$.

  6. 6.

The excluded middle property ($\sim_{A}$) holds for $\mathcal{L}$ if
$Cn(\varphi)\cap Cn(\neg\varphi)=Cn(\varnothing)$ for any
$\varphi\in\mathrm{Fm}$.

  7. 7.

The pseudo co-negation property ($\sim_{P}$) holds for $\mathcal{L}$ if
$\vee_{P}$ holds for $\mathcal{L}$, and moreover,
$\varphi\vee\neg(\varphi\vee\psi)\in Cn(\neg\psi)$ for all
$\varphi,\psi\in\mathrm{Fm}$.

  8. 8.

The strong negation property ($\neg_{S}$) holds for $\mathcal{L}$ if
$Cn(\varphi,\psi)=\mathrm{Fm}$ implies $\neg\psi\in Cn(\varphi)$.

The (weak)222We refer to this property as weak, because in the literature the
property referred to as deduction-detachment property is $\psi\in
Cn(\Gamma,\varphi)$ iff $\varphi\rightarrow\psi\in Cn(\Gamma)$ for all
$\varphi,\psi\in\mathrm{Fm}$ and $\Gamma\subseteq\mathrm{Fm}$. deduction-
detachment property ($\rightarrow_{P}$) holds for $\mathcal{L}$ if a term
$t(x,y)$ (which we denote $x\rightarrow y$) exists in the language of
$\mathcal{L}$ such that $\psi\in Cn(\chi,\varphi)$ iff
$\varphi\rightarrow\psi\in Cn(\chi)$ for all $\varphi,\psi\in\mathrm{Fm}$.

The co-implication property
($\mbox{\rotatebox[origin={c}]{180.0}{$\,>\mkern-8.0mu\raisebox{-0.27986pt}{\rule[2.5252pt]{5.94167pt}{0.43057pt}}\,$}}_{P}$)
holds for $\mathcal{L}$ if a term $t(x,y)$ (which we denote
$x\mbox{\rotatebox[origin={c}]{180.0}{$\,>\mkern-8.0mu\raisebox{-0.27986pt}{\rule[2.5252pt]{5.94167pt}{0.43057pt}}\,$}}y$,
to be read as “$x$ excludes $y$”) exists in the language of $\mathcal{L}$ such
that $\chi\in
Cn(\varphi\mbox{\rotatebox[origin={c}]{180.0}{$\,>\mkern-8.0mu\raisebox{-0.27986pt}{\rule[2.5252pt]{5.94167pt}{0.43057pt}}\,$}}\psi)$
iff $Cn(\chi)\cap Cn(\psi)\subseteq Cn(\varphi)$ for all
$\varphi,\psi,\chi\in\mathrm{Fm}$.

Every selfextensional logic with $\wedge_{P}$ is fully selfextensional [21,
Theorems 4.31 and 4.46]. Moreover, in [18], selfextensional logics with
$\wedge_{P}$ are characterized as those such that the equations that define a
semilattice hold for each element $A$ in the class $\mathsf{Alg}(\mathcal{L})$
of algebras canonically associated with $\mathcal{L}$, and the following
condition is satisfied for all
$\varphi_{1},\ldots,\varphi_{n},\varphi\in\mathrm{Fm}$:

$\varphi_{1},...,\varphi_{n}\vdash\varphi\quad\text{iff}\quad
h(\varphi_{1})\wedge\cdots\wedge h(\varphi_{n})\leq h(\varphi)\,\text{ for all
}A\in\mathsf{Alg}(\mathcal{L})\text{ and any }h\in Hom(\mathrm{Fm},A).$

Hence, for every selfextensional logic with $\wedge_{P}$ and all
$\varphi,\psi\in\mathrm{Fm}$, $\varphi\vdash\psi$ iff $h(\varphi)\leq h(\psi)$
for every $A\in\mathsf{Alg}(\mathcal{L})$ and every homomorphism
$h:\mathrm{Fm}\to A$. Similar properties hold for super-compact
selfextensional logics with $\vee_{P}$ (cf. Section A). Therefore, for any
selfextensional logic $\mathcal{L}$, property $\wedge_{P}$ (resp. $\vee_{P}$
if $\mathcal{L}$ is also super-compact) guarantees that the relation of
logical entailment of $\mathcal{L}$ is completely captured by the order of the
algebras in $\mathsf{Alg}(\mathcal{L})$, and that each such algebra is a meet
(resp. join) semilattice w.r.t. the (possibly defined) operation interpreting
the term $\wedge$ (resp. $\vee$). This is the main reason why the theory
developed from Section 3 on will take ordered algebras (and distinguished
subclasses thereof, such as semilattices, lattices and distributive lattices)
as its basic environment. In what follows, for the sake of readability, in
defining and considering conditions on these algebras corresponding to e.g.
different metalogical properties of selfextensional logics, in relation with
different closure properties of input/output logics based on them (see next
subsection), we will sometimes omit reference to the minimal assumptions
presupposed by the satisfaction of those conditions.

######  Lemma 2.1.

(cf. [19, Lemma 2.1 and Proposition 2.2]) For any logic
$\mathcal{L}=(\mathrm{Fm},\vdash)$,

  1. 1.

If properties $\wedge_{P}$, $\vee_{P}$, and $\neg_{W}$ hold for $\mathcal{L}$,
then $\neg\varphi\vee\neg\psi\vdash\neg(\varphi\wedge\psi)$ for all
$\varphi,\psi\in\mathrm{Fm}$.

  2. 2.

If in addition property $\neg_{Il}$ holds for $\mathcal{L}$, then
$\neg(\varphi\wedge\psi)\vdash\neg\varphi\vee\neg\psi$ for all
$\varphi,\psi\in\mathrm{Fm}$.

  3. 3.

if $\wedge_{P}$ and $\vee_{S}$ hold for $\mathcal{L}$, then
$\alpha\wedge(\beta\vee\gamma)\vdash(\alpha\wedge\beta)\vee(\alpha\wedge\gamma)$
for all $\alpha,\beta,\gamma\in\mathrm{Fm}$.

###  2.2 Input/output logics on selfextensional logics

Input/output logic [3] is a framework modelling the interaction between the
relation of logical entailment between states of affair (being represented by
formulas) and other binary relations on states of affair, representing e.g.
systems of norms, strategies, preferences, and so on. Although the original
framework of input/output logic takes $\mathcal{L}$ to be classical
propositional logic, in the present section we collect basic definitions and
facts, introduced in [19], about input/output logic in the more general
framework of selfextensional logics.

#### Normative systems.

Let $\mathcal{L}=(\mathrm{Fm},\vdash)$ be a logic in the sense specified in
Section 2.1. A normative system on $\mathcal{L}$ is a relation
$N\subseteq\mathrm{Fm}\times\mathrm{Fm}$, the elements $(\alpha,\varphi)$ of
which are called conditional norms (or obligations).

A normative system $N\subseteq\mathrm{Fm}\times\mathrm{Fm}$ is internally
incoherent if $(\alpha,\varphi)$ and $(\alpha,\psi)\in N$ for some
$\alpha,\varphi,\psi\in\mathrm{Fm}$ such that $Cn(\alpha)\neq\mathrm{Fm}$ and
$Cn(\varphi,\psi)=\mathrm{Fm}$; a normative system $N$ is internally coherent
if it is not internally incoherent. If
$N,N^{\prime}\subseteq\mathrm{Fm}\times\mathrm{Fm}$ are normative systems, $N$
is almost included in $N^{\prime}$ (in symbols: $N\subseteq_{c}N^{\prime}$) if
$(\alpha,\varphi)\in N$ and $Cn(\alpha)\neq\mathrm{Fm}$ imply
$(\alpha,\varphi)\in N^{\prime}$.

Each norm $(\alpha,\varphi)\in N$ can be intuitively read as “given $\alpha$,
it should be the case that $\varphi$”. This interpretation can be further
specified according to the context: for instance, if $N$ formally represents a
system of (real-life) rules/norms, then we can read $(\alpha,\varphi)\in N$ as
“$\varphi$ is obligatory whenever $\alpha$ is the case”; if $N$ formally
represents a scientific theory, then we can read $(\alpha,\varphi)\in N$ as
“under conditions $\alpha$, one should observe $\varphi$”, in the sense that
the scientific theory predicts $\varphi$ whenever $\alpha$; finally, if $N$
formally represents (the execution of) a program, then we can read
$(\alpha,\varphi)\in N$ as “in every state of computation in which $\alpha$
holds, the program will move to a state in which $\varphi$ holds”. For any
$\Gamma\subseteq\mathrm{Fm}$, let
$N(\Gamma):=\\{\psi\mid\exists\alpha(\alpha\in\Gamma\ \&\ (\alpha,\psi)\in
N)\\}$.

An input/output logic is a tuple $\mathbb{L}=(\mathcal{L},N)$ s.t.
$\mathcal{L}=(\mathrm{Fm},\vdash)$ is a selfextensional logic, and $N$ is a
normative system on $\mathcal{L}$.

For any input/output logic $\mathbb{L}=(\mathcal{L},N)$, and each $1\leq i\leq
4$, the output operation $out_{i}^{N}$ is defined as follows: for any
$\Gamma\subseteq\mathrm{Fm}$,

$out_{i}^{N}(\Gamma):=N_{i}(\Gamma)=\\{\psi\in\mathrm{Fm}\mid\exists\alpha(\alpha\in\Gamma\
\&\ (\alpha,\psi)\in N_{i})\\}$

where $N_{i}\subseteq\mathrm{Fm}\times\mathrm{Fm}$ is the closure of $N$ under
(i.e. the smallest extension of $N$ satisfying) the inference rules below, as
specified in the table.

$(\top,\top)$ $(\bot,\bot)$ | $(\beta,\varphi)\lx@proof@logical@and(\alpha,\varphi)\beta\vdash\alpha$ | $(\alpha,\psi)\lx@proof@logical@and(\alpha,\varphi)\varphi\vdash\psi$
---|---|---
$(\alpha,\varphi\land\psi)\lx@proof@logical@and(\alpha,\varphi)(\alpha,\psi)$ | $(\alpha\lor\beta,\varphi)\lx@proof@logical@and(\alpha,\varphi)(\beta,\varphi)$ | $(\alpha,\psi)\lx@proof@logical@and(\alpha,\varphi)(\alpha\land\varphi,\psi)$

$N_{i}$ | Rules
---|---
$N_{1}$ | $\mathrm{(\top),(SI),(WO),(AND)}$
$N_{2}$ | $\mathrm{(\top),(SI),(WO),(AND),(OR)}$
$N_{3}$ | $\mathrm{(\top),(SI),(WO),(AND),(CT)}$
$N_{4}$ | $\mathrm{(\top),(SI),(WO),(AND),(OR),(CT)}$
Table 1: closures of normative systems

Clearly, with the exception of $\mathrm{(SI)}$ and $\mathrm{(WO)}$, all the
rules above (as well as the rules below) apply only to those input/output
logics based on selfextensional logics with the (minimal) metalogical
properties guaranteeing the existence of the corresponding term-connectives.
So, for instance, rules $\mathrm{(AND)}$ and $\mathrm{(CT)}$ only apply in the
context of logics for which $\wedge_{P}$ holds, and so on. For the sake of a
better readability, in the remainder of the paper we will implicitly assume
these basic properties, and only mention the additional properties when it is
required.

#### Negative permission systems.

The following definition (cf. [19, Section 4.1]) generalizes the usual notion
of negative permission (cf. [22, Section 2]) while being formulated purely in
terms of the consequence relation of the given selfextensional logic, and it
informally says that any $\varphi$ is permitted under a given $\alpha$ iff
$\varphi$ is not logically inconsistent with any obligation $\psi$ under
$\alpha$.

For any input/output logic $\mathbb{L}=(\mathcal{L},N)$,

$P_{N}:=\\{(\alpha,\varphi)\mid\forall\psi((\alpha,\psi)\in N\Rightarrow
Cn(\varphi,\psi)\neq\mathrm{Fm})\\}$.

As discussed in [19, Section 4.1], If $N$ is internally coherent, then
$N\subseteq_{c}P_{N}$. Moreover,

For any $N,N^{\prime}\subseteq\mathrm{Fm}$, if $N\subseteq N^{\prime}$ then
$P_{N^{\prime}}\subseteq P_{N}$.

The following closure rules on
$P_{N}^{c}:=(\mathrm{Fm}\times\mathrm{Fm})\setminus P_{N}$:333That is, the
reading of the rule
$(\alpha,\varphi)\lx@proof@logical@and(\beta,\psi)\alpha\vdash\beta$ is as
follows: if $(\alpha,\psi)\notin P_{N}$ and $\alpha\vdash\beta$ then
$(\beta,\varphi)\notin P_{N}$. have been introduced and discussed in [19,
Section 4.1].

$(\top,\bot)$ | $(\bot,\top)$ | $(\alpha,\varphi)\lx@proof@logical@and(\beta,\varphi)\alpha\vdash\beta$
---|---|---
$(\alpha,\varphi)\lx@proof@logical@and(\alpha,\psi)\varphi\vdash\psi$ | $(\alpha,\varphi\vee\psi)\lx@proof@logical@and(\alpha,\varphi)(\alpha,\psi)$ | $(\alpha\vee\beta,\varphi)\lx@proof@logical@and(\alpha,\varphi)(\beta,\varphi)$
$(\alpha,\psi)\lx@proof@logical@and(\alpha,\varphi)\in N(\alpha\wedge\varphi,\psi)$ |  |

For any input/output logic $\mathbb{L}=(\mathcal{L},N)$ and any $1\leq i\leq
4$, we let $P_{i}:=P_{N_{i}}$.

######  Proposition 2.2.

(cf. [19, Corollary 4.6]) For any input/output logic
$\mathbb{L}=(\mathcal{L},N)$, if $\wedge_{P}$, $\vee_{S}$, $\bot_{P}$, and
$\top_{W}$ hold for $\mathcal{L}$, then $P_{i}^{c}$ for $1\leq i\leq 4$ is
closed under the rules indicated in the following table.

$P_{i}^{c}$ | Rules
---|---
$P_{1}^{c}$ | $\mathrm{(\top)^{\rhd},(SI)^{\rhd},(WO)^{\rhd},(AND)^{\rhd}}$
$P_{2}^{c}$ | $\mathrm{(\top)^{\rhd},(SI)^{\rhd},(WO)^{\rhd},(AND)^{\rhd},(OR)^{\rhd}}$
$P_{3}^{c}$ | $\mathrm{(\top)^{\rhd},(SI)^{\rhd},(WO)^{\rhd},(AND)^{\rhd},(CT)^{\rhd}}$
$P_{4}^{c}$ | $\mathrm{(\top)^{\rhd},(SI)^{\rhd},(WO)^{\rhd},(AND)^{\rhd},(OR)^{\rhd},(CT)^{\rhd}}$

In Section 3.2 we will systematically connect the closure rules of (the
relative complements of) permission systems with the environment of
(proto-)precontact algebras.

In [19], it is discussed how the perspective afforded by the general setting
of selfextensional logics makes it possible to consider a notion of dual
conditional permission system which, in the setting of classical propositional
logic, is absorbed by the usual notion of negative permission, namely the
following:

$(\alpha,\varphi)\in D_{N}\text{ iff }(\neg\alpha,\varphi)\notin N\text{ iff
}(\neg\alpha,\neg\varphi)\in P_{N}.$

However, in the same paper it was discussed that a more general version of
$D_{N}$ can be introduced, similarly to the generalized definition of $P_{N}$
reported above, namely:

$D_{N}:=\\{(\alpha,\varphi)\mid\exists\beta((\beta,\varphi)\notin N\ \&\
Cn(\alpha,\beta)=\mathrm{Fm})\\},$

which cannot be subsumed by the definition of $P_{N}$. While the notion of
negative permission $P_{N}$ intuitively characterizes those states of affair
$\alpha$ and $\varphi$ which can both be the case without generating a
violation of the normative system $N$, the dual negative permission system
$D_{N}$ characterizes those states of affair $\alpha$ and $\varphi$ which can
both fail to be the case without generating a violation of the normative
system $N$. The following closure rules on
$D_{N}^{c}:=(\mathrm{Fm}\times\mathrm{Fm})\setminus D_{N}$ have been
introduced and discussed in [19, Section 4.2]:

$(\bot,\top)$ | $(\top,\bot)$ | $(\beta,\varphi)\lx@proof@logical@and(\alpha,\varphi)\alpha\vdash\beta$
---|---|---
$(\alpha,\psi)\lx@proof@logical@and(\alpha,\varphi)\varphi\vdash\psi$ | $(\alpha,\varphi\wedge\psi)\lx@proof@logical@and(\alpha,\varphi)(\alpha,\psi)$ | $(\alpha\wedge\beta,\varphi)\lx@proof@logical@and(\alpha,\varphi)(\beta,\varphi)$
$(\alpha,\psi)\lx@proof@logical@and(\alpha,\varphi)(\varphi\mbox{\rotatebox[origin={c}]{180.0}{$\,>\mkern-8.0mu\raisebox{-0.27986pt}{\rule[2.5252pt]{5.94167pt}{0.43057pt}}\,$}}\alpha,\psi)\in N$ |  |

For any input/output logic $\mathbb{L}=(\mathcal{L},N)$ and any $1\leq i\leq
4$, we let $D_{i}:=D_{N_{i}}$.

######  Proposition 2.3.

(cf. [19, Corollary 4.9]) For any input/output logic
$\mathbb{L}=(\mathcal{L},N)$, if $\wedge_{P}$, $\vee_{S}$, $\top_{P}$,
$\bot_{P}$, and $\neg_{W}$ hold for $\mathcal{L}$, then $D_{i}^{c}$ for $1\leq
i\leq 4$ is closed under the rules indicated in the following table.

$D_{i}^{c}$ | Rules
---|---
$D_{1}^{c}$ | $\mathrm{(\top)^{\lhd},(SI)^{\lhd},(WO)^{\lhd},(AND)^{\lhd}}$
$D_{2}^{c}$ | $\mathrm{(\top)^{\lhd},(SI)^{\lhd},(WO)^{\lhd},(AND)^{\lhd},(OR)^{\lhd}}$
$D_{3}^{c}$ | $\mathrm{(\top)^{\lhd},(SI)^{\lhd},(WO)^{\lhd},(AND)^{\lhd},(CT)^{\lhd}}$
$D_{4}^{c}$ | $\mathrm{(\top)^{\lhd},(SI)^{\lhd},(WO)^{\lhd},(AND)^{\lhd},(OR)^{\lhd},(CT)^{\lhd}}$

###  2.3 Subordination algebras and related structures

In the present section, we collect the definitions of a family of inter-
related structures originally introduced and studied in the context of a
point-free approach to the region-based theories of discrete spaces. These
structures, suitably generalized, serve in the present paper as the main
semantic environment for normative and permission systems on selfextensional
logics.

#### Precontact algebras and related structures.

A precontact algebra [9, 23] is a tuple $\mathbb{C}=(\mathbb{A},\mathcal{C})$
such that $\mathbb{A}$ is a Boolean algebra, and $\mathcal{C}$ is a binary
relation on the domain of $\mathbb{A}$ such that, for all
$a,b,c\in\mathbb{A}$,

  1. (C1)

$a\mathcal{C}b$ implies $a,b\neq\bot$;

  2. (C2)

$a\mathcal{C}(b\vee c)$ iff $a\mathcal{C}b$ or $a\mathcal{C}c$;

  3. (C3)

$(a\vee b)\mathcal{C}c$ iff $a\mathcal{C}c$ or $b\mathcal{C}c$.

Additional conditions on precontact algebras considered in the literature (cf.
[9, 23]) are:

  1. (C4)

If $a\neq\bot$ then $a\mathcal{C}a$;

  2. (C5)

If $a\mathcal{C}b$ then $b\mathcal{C}a$;

  3. (C6)

If $a\prec_{\mathcal{C}}c$ then $\exists
b(a\prec_{\mathcal{C}}b\prec_{\mathcal{C}}c)$, where $a\prec_{\mathcal{C}}b$
iff $a\cancel{\mathcal{C}}\neg b$;

  4. (C7)

If $a\notin\\{\bot,\top\\}$ then $a\mathcal{C}\neg a$ or $\neg a\mathcal{C}a$;

  5. (C8)

if $a\wedge b\neq\bot$, then $a\mathcal{C}b$.

A contact algebra is a precontact algebra satisfying (C4) and (C5). A
precontact algebra is connected if it satisfies (C7).

#### Subordination algebras and related structures.

A strong proximity lattice [12] is a tuple $\mathbb{P}=(\mathbb{L},\prec)$
such that $\mathbb{L}$ is a bounded distributive lattice and $\prec$ is a
binary relation on the domain of $\mathbb{L}$ such that, for every
$a,x,y\in\mathbb{L}$,

  1. (P0)

$\bot\prec a$ and $a\prec\top$;

  2. (P1)

${\prec}\circ{\prec}={\prec}$;

  3. (P2)

$x\prec a$ and $y\prec a$ iff $x\vee y\prec a$;

  4. (P3)

$a\prec x$ and $a\prec y$ iff $a\prec x\wedge y$;

  5. (P4)

$a\prec x\vee y\Rightarrow\exists x^{\prime}\exists y^{\prime}(x^{\prime}\prec
x\ \&\ y^{\prime}\prec y\ \&\ a\prec x^{\prime}\vee y^{\prime})$;

  6. (P5)

$x\wedge y\prec a\Rightarrow\exists x^{\prime}\exists y^{\prime}(x\prec
x^{\prime}\ \&\ y\prec y^{\prime}\ \&\ x^{\prime}\wedge y^{\prime}\prec a)$.

A subordination algebra [24, Definition 7.2.1] is a tuple
$\mathbb{S}=(\mathbb{A},\prec)$ such that $\mathbb{A}$ is a Boolean algebra,
and $\prec$ is a binary relation on the domain of $\mathbb{A}$ such that, for
all $a,b,c,d\in\mathbb{A}$,

  1. (S1)

$\bot\prec\bot$ and $\top\prec\top$;

  2. (S2)

if $a\prec b$ and $a\prec c$ then $a\prec b\wedge c$;

  3. (S3)

if $a\prec c$ and $b\prec c$ then $a\vee b\prec c$;

  4. (S4)

if $a\leq b\prec c\leq d$ then $a\prec d$.

Clearly, $\bot\prec a\prec\top$ for any $a\in\mathbb{A}$. A compingent algebra
[25] is a subordination algebra such that, for all $a,b\in\mathbb{A}$,

  1. (S5)

if $a\prec b$ then $a\leq b$;

  2. (S6)

if $a\prec b$ then $\neg b\prec\neg a$;

  3. (S7)

if $a\prec b$ then $a\prec c\prec b$ for some $c\in\mathbb{A}$;

  4. (S8)

$a\neq\bot$ implies $b\prec a$ for some $b\neq\bot$.

Subordination algebras are equivalent representations of precontact algebras:
for any subordination algebra $\mathbb{S}=(A,\prec)$, the tuple
$\mathbb{S}_{{\rhd}}:=(A,\mathcal{C}_{\prec})$, where $a\mathcal{C}_{\prec}b$
iff $a\not\prec\neg b$, is a precontact algebra. Conversely, for any
precontact algebra $\mathbb{C}=(A,\mathcal{C})$, the tuple
$\mathbb{C}^{\rhd}:=(A,\prec_{\mathcal{C}})$, where $a\prec_{\mathcal{C}}b$
iff $a\cancel{\mathcal{C}}\neg b$, is a subordination algebra. Finally,
$\mathbb{S}=(\mathbb{S}_{\rhd})^{\rhd}$ and
$\mathbb{C}=(\mathbb{C}^{\rhd})_{\rhd}$.

#### Dual precontact algebras and related structures.

To our knowledge, the following structures have not independently emerged in
the literature: a dual precontact algebra is a tuple
$\mathbb{D}=(\mathbb{A},\mathcal{D})$ such that $\mathbb{A}$ is a Boolean
algebra, and $\mathcal{D}$ is a binary relation on the domain of $\mathbb{A}$
such that, for all $a,b,c\in\mathbb{A}$,

  1. (D1)

$a\mathcal{D}b$ implies $a,b\neq\top$;

  2. (D2)

$a\mathcal{D}(b\wedge c)$ iff $a\mathcal{D}b$ or $a\mathcal{D}c$;

  3. (D3)

$(a\wedge b)\mathcal{D}c$ iff $a\mathcal{D}c$ or $b\mathcal{D}c$.

Additional properties:

  1. (D4)

If $a\neq\top$ then $a\mathcal{D}a$;

  2. (D5)

If $a\mathcal{D}b$ then $b\mathcal{D}a$;

  3. (D6)

If $a\prec_{\mathcal{D}}c$ then $\exists
b(a\prec_{\mathcal{D}}b\prec_{\mathcal{D}}c)$; , where $a\prec_{\mathcal{D}}b$
iff $a\cancel{\mathcal{D}}\neg b$;

  4. (D7)

If $a\notin\\{\bot,\top\\}$ then $a\mathcal{D}\neg a$ or $\neg a\mathcal{D}a$;

  5. (D8)

if $a\vee b\neq\top$, then $a\mathcal{D}b$.

Dual precontact algebras are equivalent representations of subordination
algebras: for any subordination algebra $\mathbb{S}=(A,\prec)$, the tuple
$\mathbb{S}_{{\lhd}}:=(A,\mathcal{D}_{\prec})$, where $a\mathcal{D}_{\prec}b$
iff $\neg a\not\prec b$, is a dual precontact algebra. Conversely, for any
dual precontact algebra $\mathbb{D}=(A,\mathcal{D})$, the tuple
$\mathbb{D}^{\lhd}:=(A,\prec_{\mathcal{D}})$, where $a\prec_{\mathcal{D}}b$
iff $\neg a\cancel{\mathcal{D}}b$, is a subordination algebra. Finally,
$\mathbb{S}=(\mathbb{S}_{\lhd})^{\lhd}$ and
$\mathbb{D}=(\mathbb{D}^{\lhd})_{\lhd}$. Hence, precontact algebras and dual
precontact algebras are mutually equivalent presentations, via the assignments
$\mathbb{D}\mapsto(\mathbb{D}^{\lhd})_{{\rhd}}$ and
$\mathbb{C}\mapsto(\mathbb{C}^{\rhd})_{{\lhd}}$.

#### Examples.

As mentioned at the beginning of this section, the structures discussed above
arise in the literature as abstract (e.g. qualitative, point-free) models of
spatial reasoning; the basic tenet of this generalization is that regions,
rather than points, are taken as the basic spatial notion. Prime examples of
subordination, precontact, and dual precontact algebras arise as follows: for
any topological space444A topological space is a tuple $\mathbb{X}=(X,\tau)$
s.t. $X$ is a set and $\tau$ is a family of subsets of $X$ which is closed
under arbitrary unions (hence $\varnothing=\bigcup\varnothing\in\tau$) and
finite intersections (hence $X=\bigcap\varnothing\in\tau$). Elements of $\tau$
are referred to as open sets, while complements of open sets are referred to
as closed sets. We let $K(\mathbb{X})$ denote the set of the closed sets of
$\mathbb{X}$. By definition, $K(\mathbb{X})$ is closed under finite unions and
arbitrary intersections, hence $\varnothing$ and $X$ are both closed and open
sets. For any $y\subseteq X$, let $cl(y)$ (resp. $int(y)$) denote the smallest
closed set which includes $y$, i.e. the intersection of the closed sets which
include $y$ (resp. the largest open set included in $y$, i.e. the union of the
open sets included in $y$). By definition, the assignments $y\mapsto int(y)$
and $y\mapsto cl(y)$ define monotone operations on $\mathcal{P}(X)$, and
moreover, $int(y)\subseteq y\subseteq cl(y)$ for any $y\subseteq X$. Notice
that $int(y)\cap int(z)=int(y\cap z)$: the right-to-left inclusion immediately
follows from the monotonicity of $int(-)$; the converse inclusion follows from
$int(y)\cap int(z)$ being an open subset of $y\cap z$. Likewise, $cl(y)\cup
cl(z)=cl(y\cup z)$. Finally, $(cl(y^{c}))^{c}=int(y)$: the left-to-right
inclusion holds since $(cl(y^{c}))^{c}$ is an open set included in $y$; to
show that $int(y)\subseteq(cl(y^{c}))^{c}$, notice that every element of
$int(y)$ has a neighbourhood (i.e. an open set to which the given element
belongs) included in $y$ and hence disjoint from $y^{c}$, while every element
in $cl(y^{c})$ has no neighbourhood disjoint from $y^{c}$. Dually,
$cl(y)=(int(y^{c}))^{c}$, i.e. $int(y^{c})=(cl(y))^{c}$.
$\mathbb{X}=(X,\tau)$,

  1. 1.

$\mathbb{S_{X}}:=(\mathcal{P}(X),\prec_{\tau})$, where $y\prec_{\tau}z$ iff
$cl(y)\subseteq z$, is a subordination algebra555The relation $\prec_{\tau}$
is known as the ‘well inside’ or ‘well below’ relation (cf. [26]). satisfying
(S5) and (S7). If $\mathbb{X}$ is T1,666A topological space $\mathbb{X}$ is
$\mathrm{T_{1}}$ if, for any two distinct points, each is contained in an open
set not containing the other point. then $\mathbb{S_{X}}$ satisfies (S8) as
well;

  2. 2.

$\mathbb{C_{X}}:=(\mathcal{P}(X),\mathcal{C}_{\tau})$, where
$y\mathcal{C}_{\tau}z$ iff $cl(y)\cap cl(z)\neq\varnothing$, is a precontact
algebra (cf. [27]) satisfying (C4), (C5), and (C8). If $\mathbb{X}$ is
connected777A topological space $\mathbb{X}$ is _connected_ if it is not the
union of two or more disjoint non-empty open subsets., then $\mathbb{C_{X}}$
satisfies (C7) as well;

  3. 3.

$\mathbb{D_{X}}:=(\mathcal{P}(X),\mathcal{D}_{\tau})$, where
$y\mathcal{D}_{\tau}z$ iff $int(y)\cup int(x)\neq X$, is a dual precontact
algebra satisfying (D4), (D5), and (D8). If $\mathbb{X}$ is connected, then
$\mathbb{D_{X}}$ satisfies (D7) as well.

Item 2 (resp. item 3) above follows from $cl(-)$ (resp. $int(-)$) preserving
finite, hence empty unions (resp. intersections), as discussed in Footnote 4.
Item 1 can be verified straightforwardly (for (S3), one uses that $cl(-)$
preserves finite unions; for (S4), $b\subseteq cl(b)$).

######  Lemma 2.4.

For all $y,z\subseteq X$,

  1. 1.

$y\prec_{\mathcal{C}_{\tau}}z$ implies $y\prec_{\tau}z$, and
$y\prec_{\mathcal{D}_{\tau}}z$ implies $y\prec_{\tau}z$;

  2. 2.

$y\mathcal{C}_{\prec_{\tau}}z$ implies $y\mathcal{C}_{\tau}z$, and
$y\mathcal{D}_{\prec_{\tau}}z$ implies $y\mathcal{D}_{\tau}z$;

  3. 3.

$y\mathcal{C}_{\tau}z$ iff $y\mathcal{C}_{\mathcal{D}_{\tau}}z$, and
$y\mathcal{D}_{\tau}z$ iff $y\mathcal{D}_{\mathcal{C}_{\tau}}z$.

###### Proof.

1\. By definition, $y\prec_{\mathcal{C}_{\tau}}z$ iff $cl(y)\cap
cl(z^{c})=\varnothing$, hence (cf. Footnote 4)
$cl(y)\subseteq(cl(z^{c}))^{c}\subseteq int(z)\subseteq z$, as required. For
the second part, $y\prec_{\mathcal{D}_{\tau}}z$ iff $int(y^{c})\cup int(z)=X$,
hence (cf. Footnote 4)
$cl(y)\cap(int(z))^{c}\subseteq(int(y^{c}))^{c}\cap(int(z))^{c}=(int(y^{c})\cup
int(z))^{c}=\varnothing$ implies $cl(y)\subseteq int(z)\subseteq z$, i.e.
$y\prec_{\tau}z$, as required.

2\. By definition, $y\mathcal{C}_{\prec_{\tau}}z$ iff $cl(y)\not\subseteq
z^{c}$, i.e. $cl(y)\cap z\neq\varnothing$ which implies $cl(y)\cap
cl(z)\neq\varnothing$ i.e. $y\mathcal{C}_{\tau}z$, as required. For the second
part, by definition, $y\mathcal{D}_{\prec_{\tau}}z$ iff
$cl(y^{c})\not\subseteq z$, i.e. $cl(y^{c})\cap z^{c}\neq\varnothing$, hence
(cf. Footnote 4) $int(y)\cup int(z)\subseteq(cl(y^{c}))^{c}\cup
z=(cl(y^{c})\cap z^{c})^{c}\neq X$ implies that $int(y)\cup int(z)\neq X$,
i.e. $y\mathcal{D}_{\tau}z$, as required.

3\. By definition, $y\mathcal{C}_{\tau}z$ iff $cl(y)\cap
cl(z)\neq\varnothing$, iff (cf. Footnote 4) $int(y^{c})\cup
int(z^{c})=(cl(y))^{c}\cup(cl(z))^{c}=(cl(y)\cap cl(z))^{c}\neq X$, i.e.
$y\mathcal{C}_{\mathcal{D}_{\tau}}z$, as required. For the second part, by
definition, $y\mathcal{D}_{\tau}z$ iff $int(y)\cup int(z)\neq X$, iff (cf.
Footnote 4) $(cl(y^{c})\cap
cl(z^{c}))^{c}=(cl(y^{c}))^{c}\cup(cl(z^{c}))^{c}=int(y)\cup int(z)\neq X$,
i.e. $y\mathcal{D}_{\mathcal{C}_{\tau}}z$, as required. ∎

The inclusions of items 1 and 2 of the previous lemma are all proper in
general.

Besides serving as abstract models of qualitative spatial reasoning, the
structures discussed above also serve as models of information theory,
particularly in the context of the (denotational) semantics of programming
languages. For instance, as observed in [28], the argument was made in [29]
that the proximity relation $\prec$ can be interpreted as a stronger relation
between (the algebraic interpretation of) two logical propositions $\varphi$
and $\psi$ than the logical entailment; namely, $\varphi\prec\psi$ if,
whenever $\varphi$ is observed, $\psi$ is actually true. However, this
interpretation is by no means the only one; for instance, taking $\prec$ to
represent a scientific theory, encoded as a set of predictions (i.e. $a\prec
b$ reads as “$a$ predicts $b$”, in the sense that, whenever $a$ is the case,
$b$ should be empirically observed), then $a\mathcal{C}_{\prec}b$ can be
interpreted as “$b$ is compatible with $a$”, in the sense that the
simultaneous observation of $a$ and $b$ does not lead to the rejection of the
‘scientific theory’ $\prec$. Similarly, the dual precontact relation
$\mathcal{D}_{\prec}$ can be understood as encoding a form of negative
compatibility, in the sense that $a\mathcal{D}_{\prec}b$ iff $a$ and $b$ can
be simultaneously refuted without this leading to a violation of $\prec$.

An analogous interpretation allows us to take (generalizations of)
subordination algebras, precontact algebras, and dual precontact algebras as
models of normative, permission, and dual permission systems respectively. We
will do so in Section 3, where we will also systematically connect these
structures with the slanted algebras we discuss in the next subsection.

###  2.4 Canonical extensions and slanted algebras

In the present subsection, we adapt material from [13, Sections 2.2 and
3.1],[30, Section 2]. For any poset $A$, a subset $B\subseteq A$ is upward
closed, or an up-set (resp. downward closed, or a down-set) if $\lfloor
B\rfloor:=\\{c\in A\mid\exists b(b\in B\ \&\ b\leq c)\\}\subseteq B$ (resp.
$\lceil B\rceil:=\\{c\in A\mid\exists b(b\in B\ \&\ c\leq b)\\}\subseteq B$);
a subset $B\subseteq A$ is down-directed (resp. up-directed) if, for all
$a,b\in B$, some $x\in B$ exists s.t. $x\leq a$ and $x\leq b$ (resp. $a\leq x$
and $b\leq x$). It is straightforward to verify that when $A$ is a lattice,
down-directed upsets and up-directed down-sets coincide with lattice filters
and ideals, respectively.

######  Definition 2.5.

Let $A$ be a subposet of a complete lattice $A^{\prime}$.

  1. 1.

An element $k\in A^{\prime}$ is closed if $k=\bigwedge F$ for some non-empty
and down-directed $F\subseteq A$; an element $o\in A^{\prime}$ is open if
$o=\bigvee I$ for some non-empty and up-directed $I\subseteq A$;

  2. 2.

$A$ is dense in $A^{\prime}$ if every element of $A^{\prime}$ can be expressed
both as the join of closed elements and as the meet of open elements of $A$.

  3. 3.

$A$ is compact in $A^{\prime}$ if, for all $F,I\subseteq A$ s.t. $F$ is non-
empty and down-directed, $I$ is non-empty and up-directed, if $\bigwedge
F\leq\bigvee I$ then $a\leq b$ for some $a\in F$ and $b\in I$.888When the
poset $A$ is a lattice, the compactness can be equivalently reformulated by
dropping the requirements that $F$ be down-directed and $I$ be up-directed.

  4. 4.

The canonical extension of a poset $A$ is a complete lattice $A^{\delta}$
containing $A$ as a dense and compact subposet.

The canonical extension $A^{\delta}$ of any poset $A$ always exists999For
instance, the canonical extension of a Boolean algebra $A$ is (isomorphic to)
the powerset algebra $\mathcal{P}(Ult(A))$, where $Ult(A)$ is the set of the
ultrafilters of $A$. and is unique up to an isomorphism fixing $A$ (cf. [30,
Propositions 2.6 and 2.7]). The set of the closed (resp. open) elements of
$A^{\delta}$ is denoted $K(A^{\delta})$ (resp. $O(A^{\delta})$). The following
proposition collects well known facts which we will use in the remainder of
the paper. In particular, items 1(iii) and (iv) are variants of [31, Lemma
3.2].

######  Proposition 2.6.

For every poset $A$,

  1. 1.

for all $k_{1},k_{2}\in K(A^{\delta})$ all $o_{1},o_{2}\in O(A^{\delta})$ and
all $u_{1},u_{2}\in A^{\delta}$,

    1. (i)

$k_{1}\leq k_{2}$ iff $k_{2}\leq b$ implies $k_{1}\leq b$ for all $b\in A$.

    2. (ii)

$o_{1}\leq o_{2}$ iff $b\leq o_{1}$ implies $b\leq o_{2}$ for all $b\in A$.

    3. (iii)

$u_{1}\leq u_{2}$ iff $k\leq u_{1}$ implies $k\leq u_{2}$ for all $k\in
K(A^{\delta})$, iff $u_{2}\leq o$ implies $u_{1}\leq o$ for all $o\in
O(A^{\delta})$.

    4. (iv)

If $A$ is a $\vee$-SL, then $k_{1}\vee k_{2}\in K(A^{\delta})$.

    5. (v)

If $A$ is a $\wedge$-SL, then $o_{1}\wedge o_{2}\in O(A^{\delta})$.

  2. 2.

if $\neg:A\to A$ is antitone and s.t. $(A,\neg)\models\forall a\forall b(\neg
a\leq b\Leftrightarrow\neg b\leq a)$, then $\neg^{\sigma}:A^{\delta}\to
A^{\delta}$ defined as $\neg^{\sigma}o:=\bigwedge\\{\neg a\mid a\leq o\\}$ for
any $o\in O(A^{\delta})$ and $\neg^{\sigma}u:=\bigvee\\{\neg^{\sigma}o\mid
u\leq o\\}$ for any $u\in A^{\delta}$ is antitone and s.t.
$(A^{\delta},\neg^{\sigma})\models\forall u\forall v(\neg u\leq
v\Leftrightarrow\neg v\leq u)$. If in addition, $(A,\neg)\models a\leq\neg\neg
a$, then $(A^{\delta},\neg^{\sigma})\models u\leq\neg\neg u$. Hence, if
$(A,\neg)\models a=\neg\neg a$ (i.e. $\neg$ is involutive), then
$(A^{\delta},\neg^{\sigma})\models u=\neg\neg u$.

  3. 3.

if $\neg:A\to A$ is antitone and s.t. $(A,\neg)\models\forall a\forall
b(a\leq\neg b\Leftrightarrow b\leq\neg a)$, then $\neg^{\pi}:A^{\delta}\to
A^{\delta}$ defined as $\neg^{\pi}k:=\bigvee\\{\neg a\mid k\leq a\\}$ for any
$k\in K(A^{\delta})$ and $\neg^{\pi}u:=\bigwedge\\{\neg^{\pi}k\mid k\leq u\\}$
for any $u\in A^{\delta}$ is antitone and s.t.
$(A^{\delta},\neg^{\pi})\models\forall u\forall v(u\leq\neg v\Leftrightarrow
v\leq\neg u)$. If in addition, $(A,\neg)\models\neg\neg a\leq a$, then
$(A^{\delta},\neg^{\pi})\models\neg\neg u\leq u$. Hence, if $\neg$ is
involutive, then so is $\neg^{\pi}$.

###### Proof.

1\. (i) The left-to-right direction immediately follows from the transitivity
of the order. Conversely, if $k_{1}$ and $k_{2}\in K(A^{\delta})$, then
$k_{i}=\bigwedge F_{i}$ for some (nonempty down-directed) $F_{i}\subseteq A$.
Hence in particular, $k_{2}\leq b$ for all $b\in F_{2}$. Then the assumption
implies that $k_{1}\leq b$ for all $b\in F_{2}$, i.e. $k_{1}\leq\bigwedge
F_{2}=k_{2}$, as required. The proofs of (ii) and (iii) are similar, using
denseness for the latter item.
(iv) If $k_{1}$ and $k_{2}$ are as in the proof of item (i), let us show that
$k_{1}\vee k_{2}=\bigwedge F_{1}\vee\bigwedge F_{2}=\bigwedge\\{c_{1}\vee
c_{2}\mid c_{i}\in F_{i}\\}$. For the left-to-right inequality, let us show
that $k_{i}\leq c_{1}\vee c_{2}$ for any $1\leq i,j\leq 2$ and any $c_{j}\in
F_{j}$. Indeed, $k_{i}=\bigwedge F_{i}\leq c_{i}\leq c_{1}\vee c_{2}$.
Therefore, $k_{1}\vee k_{2}\leq\bigwedge\\{c_{1}\vee c_{2}\mid c_{i}\in
F_{i}\\}$. For the converse inequality, by item (iii), it is enough to show
that if $o\in O(A^{\delta})$ and $k_{1}\vee k_{2}\leq o$ (i.e. $k_{i}\leq o$)
then $\bigwedge\\{c_{1}\vee c_{2}\mid c_{i}\in F_{i}\\}\leq o$. By
compactness, $k_{i}\leq o$ implies that some $d_{i}\in F_{i}$ exists such that
$k_{i}\leq d_{i}\leq o$. Hence, $\bigwedge\\{c_{1}\vee c_{2}\mid c_{i}\in
F_{i}\\}\leq d_{1}\vee d_{2}\leq o$, as required. To finish the proof that
$k_{1}\vee k_{2}\in K(A^{\delta})$, it is enough to show that the set
$\\{c_{1}\vee c_{2}\mid c_{i}\in F_{i}\\}$, which is a subset of $A$ since $A$
is a $\vee$-SL, is also nonempty and down-directed. Clearly, this set is
nonempty since $F_{1}$ and $F_{2}$ are; if $c_{i},d_{i}\in F_{i}$, then
$e_{i}\leq c_{i}$ and $e_{i}\leq d_{i}$ for some $e_{i}\in F_{i}$. Hence,
$e_{1}\vee e_{2}\leq c_{1}\vee c_{2}$ and $e_{1}\vee e_{2}\leq d_{1}\vee
d_{2}$, as required. The proof of (v) is order-dual.

2\. For the first part of the statement, see [30, Proposition 3.6]. Let us
assume that $(A,\neg)\models a\leq\neg\neg a$, and show that
$(A^{\delta},\neg^{\sigma})\models u\leq\neg\neg u$. The following chain of
equivalences holds in $(A^{\delta},\neg^{\sigma})$, where $k$ ranges in
$K(A^{\delta})$ and $o$ in $O(A^{\delta})$:

| $\forall u(u\leq\neg\neg u)$ |
---|---|---
iff | $\forall u\forall k\forall o((k\leq u\ \&\ \neg\neg u\leq o)\Rightarrow k\leq o)$ | denseness
iff | $\forall k\forall o(\exists u(k\leq u\ \&\ \neg\neg u\leq o)\Rightarrow k\leq o)$ |
iff | $\forall k\forall o(\neg\neg k\leq o\Rightarrow k\leq o)$ | Ackermann’s lemma (cf. [14, Lemma 1])
iff |  $\forall k(k\leq\neg\neg k)$. | denseness

Hence, to complete the proof, it is enough to show that, if $k\in
K(A^{\delta})$, then $k\leq\neg\neg k$. By definition, $k=\bigwedge D$ for
some down-directed $D\subseteq A$. Since $\neg^{\sigma}$ is a (contravariant)
left adjoint, $\neg^{\sigma}$ is completely meet-reversing. Hence, $\neg
k=\neg(\bigwedge D)=\bigvee\\{\neg d\mid d\in D\\}$, and since $D$ being down-
directed implies that $\\{\neg d\mid d\in D\\}\subseteq A$ is up-directed, we
deduce that $\neg k\in O(A^{\delta})$. Hence,

$\neg\neg k$ | $=$ | $\bigwedge\\{\neg a\mid a\leq\neg k\\}$ | $\neg k\in O(A^{\delta})$
---|---|---|---
| $=$ | $\bigwedge\\{\neg a\mid a\leq\bigvee\\{\neg d\mid d\in D\\}\\}$ |
| $=$ |  $\bigwedge\\{\neg a\mid\exists d(d\in D\ \&\ a\leq\neg d)\\}$. | compactness

Hence, to show that $\bigwedge\lfloor D\rfloor=\bigwedge D=k\leq\neg\neg k$,
it is enough to show that if $a\in A$ is s.t. $\exists d(d\in D\ \&\ a\leq\neg
d)$, then $d^{\prime}\leq\neg a$ for some $d^{\prime}\in D$. From $a\leq\neg
d$, by the antitonicity of $\neg$, it follows $\neg\neg d\leq\neg a$;
combining this inequality with $d\leq\neg\neg d$ which holds by assumption for
all $d\in A$, we get $d^{\prime}:=d\leq\neg a$, as required. Finally, notice
that by instantiating the left-hand inequality in the equivalence
$(A^{\delta},\neg^{\sigma})\models\forall u\forall v(\neg u\leq
v\Leftrightarrow\neg v\leq u)$ with $v:=\neg u$, one immediately gets
$(A^{\delta},\neg^{\sigma})\models\forall u(\neg\neg u\leq u)$. The proof of 3
is dual to that of 2. ∎

######  Proposition 2.7.

For any poset $A$, for all $a,b\in A$, $k,k_{1},k_{2}\in K(A^{\delta})$, and
$o,o_{1},o_{2}\in O(A^{\delta})$, and all $D_{i}\subseteq A$ nonempty and
down-directed, and $U_{i}\subseteq A$ nonempty and up-directed for $1\leq
i\leq 2$,

  1. 1.

if $A$ is a $\wedge$-semilattice, then

    1. (i)

$D_{1}\wedge D_{2}\coloneqq\\{c_{1}\wedge c_{2}\ |\ c_{1}\in D_{1}\ \&\
c_{2}\in D_{2}\\}$ is nonempty and down-directed;

    2. (ii)

if $k_{i}=\bigwedge D_{i}$, then $k_{1}\wedge k_{2}=\bigwedge(D_{1}\wedge
D_{2})\in K(A^{\delta})$;

    3. (iii)

$k_{1}\wedge k_{2}\leq b$ implies $a_{1}\wedge a_{2}\leq b$ for some
$a_{1},a_{2}\in A$ s.t. $k_{i}\leq a_{i}$;

    4. (iv)

$k_{1}\wedge k_{2}\leq o$ implies $a_{1}\wedge a_{2}\leq b$ for some
$a_{1},a_{2},b\in A$ s.t. $k_{i}\leq a_{i}$ and $b\leq o$.

  2. 2.

if $A$ is a $\vee$-semilattice, then

    1. (i)

$U_{1}\vee U_{2}\coloneqq\\{c_{1}\vee c_{2}\ |\ c_{1}\in U_{1}\ \&\ c_{2}\in
U_{2}\\}$ is nonempty and up-directed;

    2. (ii)

if $o_{i}=\bigvee U_{i}$, then $o_{1}\vee o_{2}=\bigvee(U_{1}\vee U_{2})\in
O(A^{\delta})$;

    3. (iii)

$a\leq o_{1}\vee o_{2}$ implies $a\leq b_{1}\vee b_{2}$ for some
$b_{1},b_{2}\in A$ s.t. $b_{i}\leq o_{i}$;

    4. (iv)

$k\leq o_{1}\vee o_{2}$ implies $a\leq b_{1}\vee b_{2}$ for some
$a,b_{1},b_{2}\in A$ s.t. $b_{i}\leq o_{i}$ and $k\leq a$.

  3. 3.

If $A$ is a $\wedge$-semilattice with top, then $\bigwedge K\in K(A^{\delta})$
for every $K\subseteq K(A^{\delta})$.

  4. 4.

If $A$ is a $\vee$-semilattice with bottom, then $\bigvee O\in O(A^{\delta})$
for every $O\subseteq O(A^{\delta})$.

###### Proof.

We only prove items 1 and 3, the proofs of items 2 and 4 being dual to 1 and
3, respectively.
1 (i) By assumption, some $c_{i}\in D_{i}$ exists for any $1\leq i\leq 2$.
Hence, $c_{1}\wedge c_{2}\in D_{1}\wedge D_{2}\neq\varnothing$. To show that
$D_{1}\wedge D_{2}$ is down-directed, let $c_{i},d_{i}\in D_{i}$ for any
$1\leq i\leq 2$ s.t. $c_{1}\wedge c_{2},d_{1}\wedge d_{2}\in D_{1}\wedge
D_{2}$. Since $D_{i}$ is down-directed, some $e_{i}\in D_{i}$ exists s.t.
$e_{i}\leq c_{i}$ and $e_{i}\leq d_{i}$ for any $1\leq i\leq 2$. then
$e_{1}\wedge e_{2}\in D_{1}\wedge D_{2}$ and $e_{1}\wedge e_{2}\leq
c_{1}\wedge c_{2}$ and $e_{1}\wedge e_{2}\leq d_{1}\wedge d_{2}$, as required.
(ii) By assumption, $k_{i}=\bigwedge D_{i}\leq d_{i}$ for all $d_{i}\in
D_{i}$, hence $k_{1}\wedge k_{2}\leq d_{1}\wedge d_{2}$, i.e. $k_{1}\wedge
k_{2}$ is a lower bound of $D_{1}\wedge D_{2}$. To show that $k_{1}\wedge
k_{2}$ is the greatest lower bound, let $c$ be a lower bound of $D_{1}\wedge
D_{2}$. Then $c\leq d_{1}\wedge d_{2}\leq d_{i}$ for any $d_{i}\in D_{i}$,
hence $c$ is a lower bound of $D_{i}$, and thus $c\leq\bigwedge D_{i}=k_{i}$.
This shows that $c\leq k_{1}\wedge k_{2}$, as required. Finally, together with
item (i), the identity just proved implies that $k_{1}\wedge k_{2}\in
K(A^{\delta})$.
(iii) By the previous item, $k_{1}\wedge k_{2}\in K(A^{\delta})$. Hence, by
compactness, $k_{1}\wedge k_{2}=\bigwedge(D_{1}\wedge D_{2})\leq b$ implies
that $a_{1}\wedge a_{2}\leq b$ for some $a_{i}\in D_{i}$. Moreover,
$k_{i}=\bigwedge D_{i}$ implies that $k_{i}\leq a_{i}$, as required.
(iv) By assumption, $o=\bigvee U$ for some nonempty up-directed subset
$U\subseteq A$. Then by compactness, the assumption implies that $a_{1}\wedge
a_{2}\leq b$ for some $a_{i}\in D_{i}$ and some $b\in U$. Hence
$k_{i}=\bigwedge D_{i}\leq a_{i}$ and $b\leq\bigvee U=o$, as required.

3\. If $A$ is a semilattice with top, then $\bigwedge S\in K(A^{\delta})$ for
every $S\subseteq A$; indeed, $\bigwedge S=\bigwedge\lfloor S\rfloor$, where
$\lfloor S\rfloor$ is the meet-semilattice filter generated by $S$, which is
nonempty (since $\top\in\lfloor S\rfloor$) and down-directed. Then, to prove
the statement, it is enough to show that $\bigwedge K=\bigwedge S$ where
$S:=\\{a\in A\mid\exists k_{a}(k_{a}\in K\ \&\ k_{a}\leq a)\\}$. By
definition, $\bigwedge K\leq k_{a}\leq a$ for every $a\in S$, hence $\bigwedge
K\leq\bigwedge S$. Conversely, if $k\in K$ and $a\in A$ s.t. $k\leq a$, then
$a\in S$. This shows that, for every $k\in K$, the inclusion $\\{a\in A\mid
k\leq a\\}\subseteq S$ holds, and hence $\bigwedge S\leq\bigwedge\\{a\in A\mid
k\leq A\\}=k$ is a lower bound of $K$. Thus, $\bigwedge S\leq\bigwedge K$, as
required. ∎

The following definition introduces the algebraic environment for interpreting
the output operators associated with normative and permission systems.

######  Definition 2.8.

Consider the modal signatures
$\tau_{\Diamond,\blacksquare}:=\\{\Diamond,\blacksquare\\}$,
$\tau_{{\rhd},{\blacktriangleright}}:=\\{{\rhd},{\blacktriangleright}\\}$ and
$\tau_{{\lhd},{\blacktriangleleft}}:=\\{{\lhd},{\blacktriangleleft}\\}$.

  1. 1.

A slanted $\tau_{\Diamond,\blacksquare}$-algebra is a triple
$\mathbb{A}=(A,\Diamond,\blacksquare)$ s.t. $A$ is an ordered algebra, and
$\Diamond,\blacksquare:A\to A^{\delta}$ s.t. $\Diamond a\in K(A^{\delta})$ and
$\blacksquare a\in O(A^{\delta})$ for every $a\in A$. Such a slanted algebra
is:

    1. (a)

monotone if $\Diamond$ and $\blacksquare$ are monotone, i.e. $a\leq b$ implies
$\Diamond a\leq\Diamond b$ and $\blacksquare a\leq\blacksquare b$ for all
$a,b\in A$;

    2. (b)

regular101010Of course, in order for a slanted algebra $\mathbb{A}$ to be
regular, the poset $A$ needs to be a lattice, and in order for $\mathbb{A}$ to
be normal, $A$ needs to be a bounded lattice. As mentioned earlier on, for the
sake of readability, we will sometimes omit to mention assumptions which can
be inferred from the context.  if $\Diamond$ and $\blacksquare$ are regular,
i.e. $\Diamond(a\vee b)=\Diamond a\vee\Diamond b$, and $\blacksquare(a\wedge
b)=\blacksquare a\wedge\blacksquare b$ for all $a,b\in A$;

    3. (c)

normal if $\Diamond$ and $\blacksquare$ are normal, i.e. they are regular and
$\Diamond\bot=\bot$ and $\blacksquare\top=\top$;

    4. (d)

tense if $\Diamond a\leq b$ iff $a\leq\blacksquare b$ for all $a,b\in A$.

  2. 2.

A slanted $\tau_{{\rhd},{\blacktriangleright}}$-algebra is a triple
$\mathbb{A}=(A,{\rhd},{\blacktriangleright})$ s.t. $A$ is an ordered algebra,
and ${\rhd},{\blacktriangleright}:A\to A^{\delta}$ s.t.
${\rhd}a,{\blacktriangleright}a\in O(A^{\delta})$ for every $a\in A$. Such a
slanted algebra is:

    1. (a)

antitone if ${\rhd}$ and ${\blacktriangleright}$ are antitone, i.e. $a\leq b$
implies ${\rhd}b\leq{\rhd}a$ and
${\blacktriangleright}b\leq{\blacktriangleright}a$ for all $a,b\in A$;

    2. (b)

regular if ${\rhd}$ and ${\blacktriangleright}$ are regular, i.e.
${\rhd}(a\vee b)={\rhd}a\wedge{\rhd}b$, and ${\blacktriangleright}(a\vee
b)={\blacktriangleright}a\wedge{\blacktriangleright}b$ for all $a,b\in A$;

    3. (c)

normal if ${\rhd}$ and ${\blacktriangleright}$ are normal, i.e. they are
regular and ${\rhd}\bot=\top={\blacktriangleright}\bot$;

    4. (d)

tense if $a\leq{\rhd}b$ iff $b\leq{\blacktriangleright}a$ for all $a,b\in A$.

  3. 3.

A slanted $\tau_{{\lhd},{\blacktriangleleft}}$-algebra is a triple
$(A,{\lhd},{\blacktriangleleft})$ such that $A$ is an ordered algebra, and
${\lhd},{\blacktriangleleft}:A\to A^{\delta}$ s.t.
${\lhd}a,{\blacktriangleleft}a\in K(A^{\delta})$ for every $a\in A$. Such a
slanted algebra is:

    1. (a)

antitone if ${\lhd}$ and ${\blacktriangleleft}$ are antitone, i.e. $a\leq b$
implies ${\lhd}b\leq{\lhd}a$ and
${\blacktriangleleft}b\leq{\blacktriangleleft}a$ for all $a,b\in A$;

    2. (b)

regular if ${\lhd}$ and ${\blacktriangleleft}$ are regular, i.e.
${\rhd}(a\wedge b)={\rhd}a\vee{\rhd}b$, and ${\blacktriangleright}(a\wedge
b)={\blacktriangleright}a\vee{\blacktriangleright}b$ for all $a,b\in A$;

    3. (c)

normal if ${\lhd}$ and ${\blacktriangleleft}$ are normal, i.e. they are
regular and ${\lhd}\top=\bot={\blacktriangleleft}\top$;

    4. (d)

tense if ${\lhd}a\leq b$ iff ${\blacktriangleleft}b\leq a$ for all $a,b\in A$.

Each operation mapping every $a\in A$ to $K(A^{\delta})$ (resp. to
$O(A^{\delta})$) is referred to as c-slanted (resp. o-slanted). In what
follows, we will typically omit reference to the modal signature of the given
slanted algebra, and rely on the context for the disambiguation, whenever
necessary. Also, while the slanted algebras of the three modal signatures
considered above will be the focus of most of the paper, from Proposition 5.5
on, we will also consider slanted algebras of different modal signatures,
which we omit to explicitly define, since their definition will be clear from
the context.

The antitone modal operators ${\lhd}$ and ${\rhd}$ mentioned above are the
‘slanted’ versions of the operations in classical logic defined as
${\rhd}\varphi:=\neg\Diamond\varphi$ and ${\lhd}\varphi:=\neg\Box\varphi$.
Hence, under the alethic (temporal) interpretation of $\Box$ and $\Diamond$,
the operators ${\rhd}$ and ${\lhd}$ express the impossibility of and
skepticism about $\varphi$ being the case (in the future), respectively, while
${\blacktriangleright}$ and ${\blacktriangleleft}$ encode analogous meanings
but oriented towards “the past”. In Section 4, we discuss how slanted algebras
arise from algebraic models of normative and permission systems on
selfextensional logics.

The following definition is framed in the context of monotone (resp. antitone)
slanted algebras, but can be given for arbitrary slanted algebras, albeit at
the price of complicating the definition of $\Diamond^{\sigma}$,
$\blacksquare^{\pi}$, ${\rhd}^{\pi}$, ${\blacktriangleright}^{\pi}$,
${\lhd}^{\sigma}$, and ${\blacktriangleleft}^{\sigma}$. Because we are mostly
going to apply it in the monotone (resp. antitone) setting, we present the
simplified version here.

######  Definition 2.9.

For any monotone slanted algebra $\mathbb{A}=(A,\Diamond,\blacksquare)$,
antitone slanted algebra $\mathbb{A}=(A,{\rhd},{\blacktriangleright})$ and
$\mathbb{A}=(A,{\lhd},{\blacktriangleleft})$, the canonical extension of
$\mathbb{A}$ is the (standard!) modal algebra
$\mathbb{A}^{\delta}:=(A^{\delta},\Diamond^{\sigma},\blacksquare^{\pi})$
(resp.
$\mathbb{A}^{\delta}:=(A^{\delta},{\rhd}^{\pi},{\blacktriangleright}^{\pi})$,
$\mathbb{A}^{\delta}:=(A^{\delta},{\lhd}^{\sigma},{\blacktriangleleft}^{\sigma})$)
such that
$\Diamond^{\sigma},\blacksquare^{\pi},{\rhd}^{\pi},{\blacktriangleright}^{\pi},{\lhd}^{\sigma},{\blacktriangleleft}^{\sigma}:A^{\delta}\to
A^{\delta}$ are defined as follows: for every $k\in K(A^{\delta})$, $o\in
O(A^{\delta})$ and $u\in A^{\delta}$,

$\Diamond^{\sigma}k:=\bigwedge\\{\Diamond a\mid a\in A\mbox{ and }k\leq
a\\}\quad\Diamond^{\sigma}u:=\bigvee\\{\Diamond^{\sigma}k\mid k\in
K(A^{\delta})\mbox{ and }k\leq u\\}$
$\blacksquare^{\pi}o:=\bigvee\\{\blacksquare a\mid a\in A\mbox{ and }a\leq
o\\},\quad\blacksquare^{\pi}u:=\bigwedge\\{\blacksquare^{\pi}o\mid o\in
O(A^{\delta})\mbox{ and }u\leq o\\}$ ${\rhd}^{\pi}k:=\bigvee\\{{\rhd}a\mid
a\in A\mbox{ and }k\leq a\\},\quad{\rhd}^{\pi}u:=\bigwedge\\{{\rhd}^{\pi}k\mid
k\in K(A^{\delta})\mbox{ and }k\leq u\\}$
${\blacktriangleright}^{\pi}k:=\bigvee\\{{\blacktriangleright}a\mid a\in
A\mbox{ and }k\leq
a\\},\quad{\blacktriangleright}^{\pi}u:=\bigwedge\\{{\blacktriangleright}^{\pi}k\mid
k\in K(A^{\delta})\mbox{ and }k\leq u\\}.$
${\lhd}^{\sigma}o:=\bigwedge\\{{\lhd}a\mid a\in A\mbox{ and }a\leq
o\\},\quad{\lhd}^{\sigma}u:=\bigvee\\{{\lhd}^{\sigma}o\mid o\in
O(A^{\delta})\mbox{ and }u\leq o\\}$
${\blacktriangleleft}^{\sigma}o:=\bigwedge\\{{\blacktriangleleft}a\mid a\in
A\mbox{ and }a\leq
o\\},\quad{\blacktriangleleft}^{\sigma}u:=\bigvee\\{{\blacktriangleleft}^{\sigma}o\mid
o\in O(A^{\delta})\mbox{ and }u\leq o\\}.$

The equivalences in the conclusions of the items in the lemma below say that
the maps $\Diamond^{\sigma}$ and $\blacksquare^{\pi}$ (resp. ${\rhd}^{\pi}$
and ${\blacktriangleright}^{\pi}$, and also ${\lhd}^{\sigma}$ and
${\blacktriangleleft}^{\sigma}$) form adjoint pairs.

######  Lemma 2.10.

For any tense slanted algebra $\mathbb{A}$ which is based on a bounded
lattice,

  1. 1.

if $\mathbb{A}=(A,\Diamond,\blacksquare)$, then $\Diamond^{\sigma}u\leq v$ iff
$u\leq\blacksquare^{\pi}v$ for all $u,v\in A^{\delta}$.

  2. 2.

if $\mathbb{A}=(A,{\rhd},{\blacktriangleright})$, then $u\leq{\rhd}^{\pi}v$
iff $v\leq{\blacktriangleright}^{\pi}u$ for all $u,v\in A^{\delta}$.

  3. 3.

if $\mathbb{A}=(A,{\lhd},{\blacktriangleleft})$, then ${\lhd}^{\sigma}u\leq v$
iff ${\blacktriangleleft}^{\sigma}v\leq u$ for all $u,v\in A^{\delta}$.

###### Proof.

1\. Let $u,v\in A^{\delta}$. In what follows, $k\in K(A^{\delta})$, $o\in
O(A^{\delta})$, and $a,b\in A$.

$\Diamond^{\sigma}u\leq v$ | iff | $\bigvee\\{\Diamond^{\sigma}k\mid k\leq u\\}\leq\bigwedge\\{o\mid v\leq o\\}$ | denseness + def $\Diamond^{\sigma}u$
---|---|---|---
| iff | $\bigvee\\{\Diamond^{\sigma}k\mid k\leq u\\}\leq\bigwedge\\{o\mid v\leq o\\}$ |
| iff | $\forall k\forall o(k\leq u\ \&\ v\leq o\Rightarrow\Diamond^{\sigma}k\leq o)$ |
| iff | $\forall k\forall o(k\leq u\ \&\ v\leq o\Rightarrow k\leq\blacksquare^{\pi}o)$ | $(\ast)$
| iff | $\bigvee\\{k\mid k\leq u\\}\leq\bigwedge\\{\blacksquare^{\pi}o\mid v\leq o\\}$ |
| iff | $u\leq\blacksquare^{\pi}v$ | denseness + def $\blacksquare^{\pi}v$.

To justify the equivalence marked with $(\ast)$, let us show that
$\Diamond^{\sigma}k\leq o$ iff $k\leq\blacksquare^{\pi}o$ for all $k$ and $o$.

$\Diamond^{\sigma}k\leq o$ | iff | $\bigwedge\\{\Diamond a\mid k\leq a\\}\leq\bigvee\\{b\mid b\leq o\\}$ | def $\Diamond^{\sigma}k$ and open element
---|---|---|---
| iff | $\exists a\exists b(k\leq a\ \&\ b\leq o\ \&\ \Diamond a\leq b)$ | compactness
| iff | $\exists a\exists b(k\leq a\ \&\ b\leq o\ \&\ a\leq\blacksquare b)$ |  $\mathbb{A}$ is tense
| iff | $\bigwedge\\{a\mid k\leq a\\}\leq\bigvee\\{\blacksquare b\mid b\leq o\\}$ | compactness
| iff |  $k\leq\blacksquare o$. | def $\blacksquare^{\pi}o$ and closed element.

Compactness can be applied in the argument above since, thanks to $A$ being a
bounded lattice and by items 3 and 4 of Proposition 2.7, $\bigwedge\\{\Diamond
a\mid k\leq a\\}\in K(A^{\delta})$ and $\bigvee\\{\blacksquare b\mid b\leq
o\\}\in O(A^{\delta})$. The proof of the remaining items is similar and is
omitted. ∎

By well known order-theoretic facts about adjoint pairs of maps (cf. [32]),
the lemma above immediately implies the following

######  Corollary 2.11.

Any tense and lattice-based slanted algebra $\mathbb{A}$ is normal.

In what follows, slanted algebras will be considered in the context of some
input/output logic based on some (fully) selfextensional logic $\mathcal{L}$.
Therefore, for any algebraic signature $\mathcal{L}$ and any modal signature
$\tau$ disjoint from $\mathcal{L}$, a slanted $\mathcal{L}_{\tau}$-algebra is
a structure $\mathbb{A}=(A,\tau^{\mathbb{A}})$, such that $A$ is an
$\mathcal{L}$-algebra, and $\tau^{\mathbb{A}}$ is a $\tau$-indexed set of
operations $A\to A^{\delta}$ each of which is either c-slanted or o-slanted.
For any slanted $\mathcal{L}_{\tau}$-algebra $\mathbb{A}$, any assignment
$v:\mathsf{Prop}\to\mathbb{A}$ uniquely extends to a homomorphism
$v:\mathcal{L}_{\tau}\to\mathbb{A}^{\delta}$ (abusing notation, the same
symbol denotes both the assignment and its homomorphic extension). Hence,

######  Definition 2.12.

For any algebraic signature $\mathcal{L}$ and any modal signature $\tau$, an
$\mathcal{L}_{\tau}$-inequality $\phi\leq\psi$ is satisfied in a slanted
$\mathcal{L}_{\tau}$-algebra $\mathbb{A}$ under the assignment $v$ (notation:
$(\mathbb{A},v)\models\phi\leq\psi$) if $(\mathbb{A}^{\delta},e\cdot
v)\models\phi\leq\psi$ in the usual sense, where $e\cdot v$ is the assignment
on $\mathbb{A}^{\delta}$ obtained by composing the assignment
$v:\mathsf{Prop}\to\mathbb{A}$ and the canonical embedding
$e:\mathbb{A}\to\mathbb{A}^{\delta}$.

Moreover, $\phi\leq\psi$ is valid in $\mathbb{A}$ (notation:
$\mathbb{A}\models\phi\leq\psi$) if $(\mathbb{A}^{\delta},e\cdot
v)\models\phi\leq\psi$ for every assignment $v$ into $\mathbb{A}$ (notation:
$\mathbb{A}^{\delta}\models_{\mathbb{A}}\phi\leq\psi$).

##  3 Algebraic models of normative and permission systems on selfextensional
logics

In the present section, we discuss the three main types of algebras with
relations which generalize the structures discussed in Section 2.3, and which
form the basic semantic environment for normative and permission systems on
selfextensional logics.

###  3.1 (Proto-)subordination algebras

######  Definition 3.1 ((Proto-)subordination algebra).

A proto-subordination algebra is a tuple $\mathbb{S}=(A,\prec)$ such that $A$
is a (possibly bounded) poset (with bottom denoted $\bot$ and top denoted
$\top$ when they exist), and $\prec\ \subseteq A\times A$. A proto-
subordination algebra is named as indicated in the left-hand column in the
table below when $\prec$ satisfies the properties indicated in the right-hand
column. In what follows, we will refer to a proto-subordination algebra
$\mathbb{S}=(A,\prec)$ as e.g. join- or meet-semilattice based (abbreviated as
$\vee$-SL based and $\wedge$-SL based, respectively), (distributive) lattice-
based ((D)L-based), or Boolean-based (B-based) if $A$ is a (distributive)
lattice, a Boolean algebra, and so on. More in general, for any fully
selfextensional logic $\mathcal{L}$, we say that $\mathbb{S}=(A,\prec)$ is
$\mathsf{Alg}(\mathcal{L})$-based if $A\in\mathsf{Alg}(\mathcal{L})$.

$\mathrm{(\bot)}$ | $\bot\prec\bot$ | $\mathrm{(\top)}$ | $\top\prec\top$
---|---|---|---
$\mathrm{(SB)}$ | $\exists b(b\prec a)$ | $\mathrm{(SF)}$ | $\exists b(a\prec b)$
$\mathrm{(SI)}$ | $a\leq b\prec x\Rightarrow a\prec x$ | $\mathrm{(WO)}$ | $b\prec x\leq y\Rightarrow b\prec y$
$\mathrm{(AND)}$ | $a\prec x\ \&\ a\prec y\Rightarrow a\prec x\wedge y$ | $\mathrm{(OR)}$ | $a\prec x\ \&\ b\prec x\Rightarrow a\vee b\prec x$
$\mathrm{(DD)}$ | $a\prec x_{1}\ \&\ a\prec x_{2}\Rightarrow\exists x(a\prec x\ \&\ x\leq x_{1}\ \&\ x\leq x_{2})$
$\mathrm{(UD)}$ | $a_{1}\prec x\ \&\ a_{2}\prec x\Rightarrow\exists a(a\prec x\ \&\ a_{1}\leq a\ \&\ a_{2}\leq a)$

Name | Properties
---|---
$\Diamond$-defined | (DD) (SF)
$\blacksquare$-defined | (UD) (SB)
defined |  $\Diamond$-defined + $\blacksquare$-defined
$\Diamond$-premonotone |  $\Diamond$-defined + (SI)
$\blacksquare$-premonotone |  $\blacksquare$-defined + (WO)
$\Diamond$-monotone |  $\Diamond$-premonotone + (WO)
$\blacksquare$-monotone |  $\blacksquare$-premonotone + (SI)
monotone |  $\Diamond$-monotone + $\blacksquare$-monotone
$\Diamond$-regular |  $\Diamond$-monotone + (OR)
$\blacksquare$-regular |  $\blacksquare$-monotone + (AND)
regular |  $\Diamond$-regular + $\blacksquare$-regular
$\Diamond$-normal |  $\Diamond$-regular + ($\bot$)
$\blacksquare$-normal |  $\blacksquare$-regular + ($\top$)
subordination algebra |  $\Diamond$-normal + $\blacksquare$-normal

In what follows, we will also consider the properties listed below. Some of
them are the algebraic counterparts of well known closure rules of normative
systems in input/output logic [3, 22], and others have been considered in the
context of subordination algebras and related structures [11].

(D) | $a\prec c\Rightarrow\exists b(a\prec b\ \&\ b\prec c)$ | (S6) | $a\prec b\Rightarrow\neg b\prec\neg a$
---|---|---|---
(CT) | $a\prec b\ \&\ a\wedge b\prec c\Rightarrow a\prec c$ | (T) | $a\prec b\ \&\ b\prec c\Rightarrow a\prec c$
(DCT) | $c\prec a\vee b\ \&\ b\prec a\Rightarrow c\prec a$ |  |
(S9) | $\exists c(c\prec b\ \&\ x\prec a\vee c)\Leftrightarrow\exists a^{\prime}\exists b^{\prime}(a^{\prime}\prec a\ \&\ b^{\prime}\prec b\ \&\ x\leq a^{\prime}\vee b^{\prime})$
(SL1) | $a\prec b\vee c\Rightarrow\exists b^{\prime}\exists c^{\prime}(b^{\prime}\prec b\ \&\ c^{\prime}\prec c\ \&\ a\prec b^{\prime}\vee c^{\prime})$
(SL2) | $b\wedge c\prec a\Rightarrow\exists b^{\prime}\exists c^{\prime}(b^{\prime}\prec b\ \&\ c^{\prime}\prec c\ \&\ b^{\prime}\wedge c^{\prime}\prec a)$

######  Lemma 3.2.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$,

  1. 1.

if $\mathbb{S}$ is $\vee$-semilattice based, then

    1. (i)

$\mathbb{S}\models\mathrm{(OR)}$ implies $\mathbb{S}\models\mathrm{(UD)}$;

    2. (ii)

if $\mathbb{S}\models\mathrm{(SI)}$, then $\mathbb{S}\models\mathrm{(UD)}$ iff
$\mathbb{S}\models\mathrm{(OR)}$;

  2. 2.

if $\mathbb{S}$ is $\wedge$-semilattice based, then

    1. (i)

$\mathbb{S}\models\mathrm{(AND)}$ implies $\mathbb{S}\models\mathrm{(DD)}$;

    2. (ii)

if $\mathbb{S}\models\mathrm{(WO)}$, then $\mathbb{S}\models\mathrm{(DD)}$ iff
$\mathbb{S}\models\mathrm{(AND)}$.

###### Proof.

1(i) and 2(i) are straightforward. As for 1(ii), by 1(i), to complete the
proof we need to show the ‘only if’ direction. Let $a,b,x\in A$ s.t. $a\prec
x$ and $b\prec x$. By (UD), this implies that $c\prec x$ for some $c\in A$
such that $a\leq c$ and $b\leq c$. Since $A$ is a $\vee$-semilattice, this
implies that $a\vee b\leq c\prec x$, and by (SI), this implies that $a\vee
b\prec x$, as required. 2(ii) is proven similarly. ∎

######  Lemma 3.3.

For any bounded proto-subordination algebra $\mathbb{S}=(A,\prec)$,

  1. 1.

If $\mathbb{S}\models\mathrm{(SI)}$, then

    1. (i)

$\mathbb{S}\models\mathrm{(\top)}$ implies $\mathbb{S}\models\mathrm{(SF)}$;

    2. (ii)

$\mathbb{S}\models\mathrm{(SB)}$ implies $\mathbb{S}\models\mathrm{(\bot)}$.

  2. 2.

If $\mathbb{S}\models\mathrm{(WO)}$, then

    1. (i)

$\mathbb{S}\models\mathrm{(\bot)}$ implies $\mathbb{S}\models\mathrm{(SB)}$ ;

    2. (ii)

$\mathbb{S}\models\mathrm{(SF)}$ implies $\mathbb{S}\models\mathrm{(\top)}$.

###### Proof.

1\. (i) Let $a\in A$. Then by assumption, $a\leq\top\prec\top$, which by (SI)
implies $a\prec\top$, as required.

(ii) (SB) implies that $\bot\leq b\prec\bot$ for some $b\in A$. Hence,
$\bot\prec\bot$ follows from (SI), as required. The proof of 2. is similar. ∎

Normative systems can be interpreted in proto-subordination algebras as
follows:

######  Definition 3.4.

A model for an input/output logic $\mathbb{L}=(\mathcal{L},N)$ is a tuple
$\mathbb{M}=(\mathbb{S},h)$ s.t. $\mathbb{S}=(A,\prec)$ is an
$\mathsf{Alg}(\mathcal{L})$-based proto-subordination algebra, and
$h:\mathrm{Fm}\to A$ is a homomorphism s.t. for all
$\varphi,\psi\in\mathrm{Fm}$, if $(\varphi,\psi)\in N$, then $h(\varphi)\prec
h(\psi)$.

###  3.2 (Proto-)precontact algebras

######  Definition 3.5 ((Proto-)precontact algebra).

A proto-precontact algebra is a tuple $\mathbb{C}=(A,\mathcal{C})$ such that
$A$ is a (possibly bounded) poset (with bottom denoted $\bot$ and top denoted
$\top$ when they exist), and $\mathcal{C}\ \subseteq A\times A$. A proto-
precontact algebra is named as indicated in the left-hand column in the table
below when $\mathcal{C}$ satisfies the properties indicated in the right-hand
column.111111In the tables below, most properties are stated contrapositively
and mention $\cancel{\mathcal{C}}$ rather than $\mathcal{C}$, since this is
the form in which they will be used in the subsequent sections. In what
follows, we will refer to a proto-precontact algebra
$\mathbb{C}=(A,\mathcal{C})$ as e.g. (distributive) lattice-based
((D)L-based), or Boolean-based (B-based) if $A$ is a (distributive) lattice, a
Boolean algebra, and so on. More in general, for any fully selfextensional
logic $\mathcal{L}$, we say that $\mathbb{C}=(A,\mathcal{C})$ is
$\mathsf{Alg}(\mathcal{L})$-based if $A\in\mathsf{Alg}(\mathcal{L})$.

$\mathrm{(\bot)}^{\rhd}$ | $\bot\cancel{\mathcal{C}}\top$ | $\mathrm{(\top)}^{\rhd}$ | $\top\cancel{\mathcal{C}}\bot$
---|---|---|---
$\mathrm{(SB)}^{\rhd}$ | $\exists b(b\cancel{\mathcal{C}}a)$ | $\mathrm{(SF)}^{\rhd}$ | $\exists b(a\cancel{\mathcal{C}}b)$
$\mathrm{(SI)}^{\rhd}$ | $b\cancel{\mathcal{C}}c\ \&\ a\leq b\Rightarrow a\cancel{\mathcal{C}}c$ | $\mathrm{(WO)}^{\rhd}$ | $a\cancel{\mathcal{C}}c\ \&\ b\leq c\Rightarrow a\cancel{\mathcal{C}}b$
$\mathrm{(AND)}^{\rhd}$ | $a\cancel{\mathcal{C}}b\ \&\ a\cancel{\mathcal{C}}c\Rightarrow a\cancel{\mathcal{C}}(b\vee c)$ | $\mathrm{(OR)}^{\rhd}$ | $a\cancel{\mathcal{C}}c\ \&\ b\cancel{\mathcal{C}}c\Rightarrow(a\vee b)\cancel{\mathcal{C}}c$

Name | Properties
---|---
${\rhd}$-defined | (DD)⊳ (SF)⊳
${\blacktriangleright}$-defined | (UD)⊳ (SB)⊳
defined |  ${\rhd}$-defined + ${\blacktriangleright}$-defined
${\rhd}$-preantitone |  ${\rhd}$-defined + (SI)⊳
${\blacktriangleright}$-preantitone |  ${\blacktriangleright}$-defined + (WO)⊳
preantitone |  ${\rhd}$-preantitone + ${\blacktriangleright}$-preantitone
${\rhd}$-antitone |  ${\rhd}$-preantitone + (WO)⊳
${\blacktriangleright}$-antitone |  ${\blacktriangleright}$-preantitone + (SI)⊳
antitone |  ${\rhd}$-antitone + ${\blacktriangleright}$-antitone
${\rhd}$-regular |  ${\rhd}$-antitone + (OR)⊳
${\blacktriangleright}$-regular |  ${\blacktriangleright}$-antitone + (AND)⊳
regular |  ${\rhd}$-regular + ${\blacktriangleright}$-regular
${\rhd}$-normal |  ${\rhd}$-regular + ($\bot$)⊳
${\blacktriangleright}$-normal |  ${\blacktriangleright}$-regular + ($\top$)⊳
precontact algebra |  ${\rhd}$-normal + ${\blacktriangleright}$-normal

In what follows, we will also consider the properties listed below:121212See
also Section 5.5, above Proposition 5.6, for more conditions also involving
$\prec$.

(NS) | $a\cancel{\mathcal{C}}a\Rightarrow a\leq\bot$ |
---|---|---
(SFN) | $\exists b(a\cancel{\mathcal{C}}b\ \&\ \top\leq a\vee b)$ |
(ALT)⊳ | $a\cancel{\mathcal{C}}b\Rightarrow\exists c\exists d(\top\leq c\vee d\ \&\ a\cancel{\mathcal{C}}c\ \&\ b\cancel{\mathcal{C}}d)$
(ALT)▶ | $b\cancel{\mathcal{C}}a\Rightarrow\exists c\exists d(\top\leq c\vee d\ \&\ c\cancel{\mathcal{C}}a\ \&\ d\cancel{\mathcal{C}}b)$
$\mathrm{(CMO)}$ | $a\cancel{\mathcal{C}}b\ \&\ a\cancel{\mathcal{C}}c\Rightarrow(a\wedge c)\cancel{\mathcal{C}}b$ |
$\mathrm{(\vee\wedge)}$ | $(a\vee y)\cancel{\mathcal{C}}x\ \&\ a\cancel{\mathcal{C}}(x\wedge y)\Rightarrow(a\wedge x)\cancel{\mathcal{C}}y$ |

######  Lemma 3.6.

For any $\vee$-semilattice-based proto-precontact algebra
$\mathbb{C}=(A,\mathcal{C})$,

  1. (i)

$\mathbb{C}\models\mathrm{(OR)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(UD)^{\rhd}}$;

  2. (ii)

$\mathbb{C}\models\mathrm{(AND)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(DD)^{\rhd}}$;

  3. (iii)

if $\mathbb{C}\models\mathrm{(SI)^{\rhd}}$, then
$\mathbb{C}\models\mathrm{(UD)^{\rhd}}$ iff
$\mathbb{C}\models\mathrm{(OR)^{\rhd}}$;

  4. (iv)

if $\mathbb{C}\models\mathrm{(WO)^{\rhd}}$, then
$\mathbb{C}\models\mathrm{(DD)^{\rhd}}$ iff
$\mathbb{C}\models\mathrm{(AND)^{\rhd}}$.

###### Proof.

As to (i), let $a,b\in A$ s.t. $\forall d(a\leq d\ \&\ b\leq d\Rightarrow
d\mathcal{C}c)$; then $(a\vee b)\mathcal{C}c$, which implies, by (OR)⊳, that
either $a\mathcal{C}c$ or $b\mathcal{C}c$, as required. The proof of (ii) is
similar. As to (iii), by (i), to complete the proof we need to show the ‘only
if’ direction. Let $a,b,c\in A$ s.t. $(a\vee b)\mathcal{C}c$. Then, by (SI)⊳,
the left-hand side of (UD)⊳ is satisfied with $a_{1}:=a$, $a_{2}:=b$, and
$x:=c$. Therefore, $a\mathcal{C}c$ or $b\mathcal{C}c$, as required. The proof
of (iv) is similar. ∎

######  Lemma 3.7.

For any bounded proto-precontact algebra $\mathbb{C}=(A,\mathcal{C})$,

  1. 1.

If $\mathbb{C}\models\mathrm{(SI)^{\rhd}}$, then

    1. (i)

$\mathbb{C}\models\mathrm{(\top)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(SF)^{\rhd}}$;

    2. (ii)

$\mathbb{C}\models\mathrm{(SB)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(\bot)^{\rhd}}$.

  2. 2.

If $\mathbb{C}\models\mathrm{(WO)^{\rhd}}$, then

    1. (i)

$\mathbb{C}\models\mathrm{(\bot)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(SB)^{\rhd}}$;

    2. (ii)

$\mathbb{C}\models\mathrm{(SF)^{\rhd}}$ implies
$\mathbb{C}\models\mathrm{(\top)^{\rhd}}$.

###### Proof.

(i) Let $a\in A$. Then by assumption, $a\leq\top\cancel{\mathcal{C}}\bot$,
which by (SI)⊳ implies $a\cancel{\mathcal{C}}\bot$, as required.

(ii) (SB)⊳ implies that $\bot\leq b\cancel{\mathcal{C}}\top$ for some $b\in
A$. Hence, $\bot\cancel{\mathcal{C}}\top$ follows from (SI)⊳, as required. The
proof of 2. is similar. ∎

###  3.3 Dual (proto-)precontact algebras

######  Definition 3.8 (Dual (proto-)precontact algebra).

A dual proto-precontact algebra is a tuple $\mathbb{D}=(A,\mathcal{D})$ such
that $A$ is a (possibly bounded) poset (with bottom denoted $\bot$ and top
denoted $\top$ when they exist), and $\mathcal{D}\ \subseteq A\times A$. A
dual proto-precontact algebra is named as indicated in the left-hand column in
the table below when $\mathcal{D}$ satisfies the properties indicated in the
right-hand column.131313In the tables below, most properties are stated
contrapositively and mention $\cancel{\mathcal{D}}$ rather than $\mathcal{D}$,
since this is the form in which they will be used in the subsequent sections.
In what follows, we will refer to a dual proto-precontact algebra
$\mathbb{D}=(A,\mathcal{D})$ as e.g. (distributive) lattice-based
((D)L-based), or Boolean-based (B-based) if $A$ is a (distributive) lattice, a
Boolean algebra, and so on. More in general, for any fully selfextensional
logic $\mathcal{L}$, we say that $\mathbb{D}=(A,\mathcal{D})$ is
$\mathsf{Alg}(\mathcal{L})$-based if $A\in\mathsf{Alg}(\mathcal{L})$.

$\mathrm{(\bot)}^{\lhd}$ | $\top\cancel{\mathcal{D}}\bot$ | $\mathrm{(\top)}^{\lhd}$ | $\bot\cancel{\mathcal{D}}\top$
---|---|---|---
$\mathrm{(SB)}^{\lhd}$ | $\exists b(b\cancel{\mathcal{D}}a)$ | $\mathrm{(SF)}^{\lhd}$ | $\exists b(a\cancel{\mathcal{D}}b)$
$\mathrm{(SI)}^{\lhd}$ | $a\leq b\ \&\ a\cancel{\mathcal{D}}c\Rightarrow b\cancel{\mathcal{D}}c$ | $\mathrm{(WO)}^{\lhd}$ | $a\cancel{\mathcal{D}}c\ \&\ c\leq b\Rightarrow a\cancel{\mathcal{D}}b$
$\mathrm{(AND)}^{\lhd}$ | $a\cancel{\mathcal{D}}\ \&\ a\cancel{\mathcal{D}}c\Rightarrow a\cancel{\mathcal{D}}(b\wedge c)$ | $\mathrm{(OR)}^{\lhd}$ | $a\cancel{\mathcal{D}}c\ \&\ b\cancel{\mathcal{D}}c\Rightarrow(a\wedge b)\cancel{\mathcal{D}}c$
$\mathrm{(DD)}^{\lhd}$ | $(a\cancel{\mathcal{D}}x_{1}\ \&\ a\cancel{\mathcal{D}}x_{2})\Rightarrow\exists x[x\leq x_{1}\ \&\ x\leq x_{2}\ \&\ a\cancel{\mathcal{D}}x]$
$\mathrm{(UD)}^{\lhd}$ | $(a_{1}\cancel{\mathcal{D}}x\ \&\ a_{2}\cancel{\mathcal{D}}x)\Rightarrow\exists a[a\leq a_{1}\ \&\ a\leq a_{2}\ \&\ a\cancel{\mathcal{D}}x]$

Name | Properties
---|---
${\lhd}$-defined | (DD)⊲ (SF)⊲
${\blacktriangleleft}$-defined | (UD)⊲ (SB)⊲
defined |  ${\lhd}$-defined + ${\blacktriangleleft}$-defined
${\lhd}$-preantitone |  ${\lhd}$-defined + (SI)⊲
${\blacktriangleleft}$-preantitone |  ${\blacktriangleleft}$-defined + (WO)⊲
preantitone |  ${\lhd}$-preantitone + ${\blacktriangleleft}$-preantitone
${\lhd}$-antitone |  ${\lhd}$-preantitone + (WO)⊲
${\blacktriangleleft}$-antitone |  ${\blacktriangleleft}$-preantitone + (SI)⊲
antitone |  ${\lhd}$-antitone + ${\blacktriangleleft}$-antitone
${\lhd}$-regular |  ${\lhd}$-antitone + (OR)⊲
${\blacktriangleleft}$-regular |  ${\blacktriangleleft}$-antitone + (AND)⊲
regular |  ${\lhd}$-regular + ${\blacktriangleleft}$-regular
${\lhd}$-normal |  ${\lhd}$-regular + ($\bot$)⊲
${\blacktriangleleft}$-normal |  ${\blacktriangleleft}$-regular + ($\top$)⊲
dual precontact algebra |  ${\lhd}$-normal + ${\blacktriangleleft}$-normal

In what follows, we will also consider the properties listed
below:141414Unlike the other conditions in the list, $\mathrm{(CT)}^{\lhd}$
also involves $\prec$, and will be treated separately in Proposition 5.6.5.

(SR) | $a\cancel{\mathcal{D}}a\Rightarrow\top\leq a$ | $\mathrm{(CMO)}^{\lhd}$ | $a\cancel{\mathcal{D}}b\ \&\ a\cancel{\mathcal{D}}c\Rightarrow(a\vee b)\cancel{\mathcal{D}}c$
---|---|---|---
(SFN)⊲ | $\exists b(a\cancel{\mathcal{D}}b\ \&\ a\wedge b\leq\bot)$ | $\mathrm{(CT)}^{\lhd}$ | $a\cancel{\mathcal{D}}b\ \&\ b\mbox{\rotatebox[origin={c}]{180.0}{$\,>\mkern-8.0mu\raisebox{-0.27986pt}{\rule[2.5252pt]{5.94167pt}{0.43057pt}}\,$}}a\prec c\Rightarrow a\cancel{\mathcal{D}}c$

######  Lemma 3.9.

For any $\wedge$-semilattice based dual proto-precontact algebra
$\mathbb{D}=(A,\mathcal{D})$,

  1. (i)

$\mathbb{D}\models\mathrm{(OR)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(UD)^{\lhd}}$;

  2. (ii)

$\mathbb{D}\models\mathrm{(AND)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(DD)^{\lhd}}$;

  3. (iii)

if $\mathbb{D}\models\mathrm{(SI)^{\lhd}}$, then
$\mathbb{D}\models\mathrm{(UD)^{\lhd}}$ iff
$\mathbb{D}\models\mathrm{(OR)^{\lhd}}$;

  4. (iv)

if $\mathbb{D}\models\mathrm{(WO)^{\lhd}}$, then
$\mathbb{D}\models\mathrm{(DD)^{\lhd}}$ iff
$\mathbb{D}\models\mathrm{(AND)^{\lhd}}$.

###### Proof.

As to (i), let $a,b\in A$ s.t. $\forall d(d\leq a\ \&\ d\leq b\Rightarrow
d\mathcal{D}c)$; then $(a\wedge b)\mathcal{D}c$, which implies, by (OR)⊲, that
either $a\mathcal{D}c$ or $b\mathcal{D}c$, as required. The proof of (ii) is
similar. As to (iii), by (i), to complete the proof we need to show the ‘only
if’ direction. Let $a,b,c\in A$ s.t. $(a\wedge b)\mathcal{D}c$. Then, by
(SI)⊲, the left-hand side of (UD)⊲ is satisfied with $a_{1}:=a$, $a_{2}:=b$,
and $x:=c$. Therefore, $a\mathcal{C}c$ or $b\mathcal{C}c$, as required. The
proof of (iv) is similar. ∎

######  Lemma 3.10.

For any bounded dual proto-precontact algebra $\mathbb{D}=(A,\mathcal{D})$,

  1. 1.

If $\mathbb{D}\models\mathrm{(SI)^{\lhd}}$, then

    1. (i)

$\mathbb{D}\models\mathrm{(\top)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(SF)^{\lhd}}$;

    2. (ii)

$\mathbb{D}\models\mathrm{(SB)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(\bot)^{\lhd}}$.

  2. 2.

If $\mathbb{D}\models\mathrm{(WO)^{\lhd}}$, then

    1. (i)

$\mathbb{D}\models\mathrm{(\bot)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(SB)^{\lhd}}$;

    2. (ii)

$\mathbb{D}\models\mathrm{(SF)^{\lhd}}$ implies
$\mathbb{D}\models\mathrm{(\top)^{\lhd}}$.

###### Proof.

(i) Let $a\in A$. Then by assumption, $\bot\cancel{\mathcal{D}}\top\ \&\
\bot\leq a$, which by (SI)⊲ implies $a\cancel{\mathcal{D}}\top$, as required.

(ii) (SB)⊲ implies that $b\cancel{\mathcal{D}}\bot\ \&\ b\leq\top$ for some
$b\in A$. Hence, $\top\cancel{\mathcal{D}}\bot$ follows from (SI)⊲, as
required. The proof of 2. is similar. ∎

###  3.4 Algebraizing negative and dual negative permission systems

We finish the present section by introducing the algebraic counterparts of the
negative and dual negative permission systems associated with a given
normative system in the literature on input/output logic. Originally
introduced in the context of normative systems on classical propositional
logic [3], these notions have been generalized in [19, Sections 4.1 and 4.2]
to normative systems based on arbitrary selfextensional logics. In what
follows, we extend these notions to the algebraic counterparts of input/output
logics on fully selfextensional logics. For any such logic $\mathcal{L}$, any
$A\in\mathsf{Alg}(\mathcal{L})$, and any subset $X\subseteq A$, we let $F(X)$
denote the $\mathcal{L}$-filter generated by $X$. We will write e.g. $F(a,b)$
for $F(\\{a,b\\})$.

######  Definition 3.11.

Let $\mathcal{L}$ be a fully selfextensional logic. For any
$\mathsf{Alg}(\mathcal{L})$-based proto-subordination algebra
$\mathbb{S}=(A,\prec)$, we let

$\mathcal{C}_{\prec}:=\\{(a,b)\mid\forall c(a\prec c\Rightarrow F(b,c)\neq
A)\\}\quad$ $\quad\quad\mathcal{D}_{\prec}:=\\{(a,b)\mid\exists c(c\not\prec
b\ \&\ F(a,c)=A)\\}$.

The following proposition is the algebraic counterpart of [19, Propositions
4.2 and 4.7].

######  Proposition 3.12.

Let $\mathcal{L}$ be a selfextensional logic with $\wedge_{P}$, $\bot_{P}$,
$\neg_{A}$ and $\neg_{S}$. For any $\mathsf{Alg}(\mathcal{L})$-based proto-
subordination algebra $\mathbb{S}=(A,\prec)$,

  1. 1.

if $\mathbb{S}\models\mathrm{(WO)}$, then $\mathcal{C}_{\prec}=\\{(a,b)\mid
a\not\prec\neg b\\}$;

  2. 2.

if $\mathbb{S}\models\mathrm{(SI)}$, then
$\mathcal{D}_{\prec}=\\{(a,b)\mid\neg a\not\prec b\\}$.

###### Proof.

The assumptions imply that $F(a,\neg a)=A$ for every $a\in A$ and
$A\models\forall a\forall b(F(a,b)=A\Rightarrow b\leq\neg a)$, where $F(a,b)$
is the $\mathcal{L}$-filter of $A$ generated by $\\{a,b\\}$.
1\. For the left-to-right inclusion, let $c:=\neg b$; hence $F(b,\neg b)=A$,
which implies, by the definition of $\mathcal{C}_{\prec}$, $a\not\prec\neg b$,
as required. Conversely, let $a,b\in A$ s.t. $a\not\prec\neg b$ and let $c\in
A$ s.t. $F(b,c)=A$. By the preliminary observations on $A$, this implies that
$c\leq\neg b$. Hence, $a\not\prec c$, for otherwise, by $\mathrm{(WO)}$,
$a\prec c$ and $c\leq\neg b$ would imply that $a\prec\neg b$, against the
assumption.
2\. For the right-to-left inclusion, take $c:=\neg a$ as the witness; as
discussed above, $F(a,\neg a)=A$, as required. Conversely, let $a,b\in A$ s.t.
$c\not\prec b$ for some $c\in A$ s.t. $F(a,c)=A$. As discussed above, this
implies that $c\leq\neg a$. Hence, $\neg a\not\prec b$, for otherwise, by
$\mathrm{(SI)}$, $c\prec b$, against the assumption. ∎

######  Definition 3.13.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$,

  1. 1.

the proto-precontact algebra associated with $\mathbb{S}$ is
$\mathbb{S}_{{\rhd}}:=(A,\mathcal{C}_{\prec})$;

  2. 2.

the dual proto-precontact algebra associated with $\mathbb{S}$ is
$\mathbb{S}_{{\lhd}}:=(A,\mathcal{D}_{\prec})$.

The following is a straightforward consequence of Proposition 3.12.

######  Corollary 3.14.

Let $\mathbb{S}=(A,\prec)$ be a proto-subordination algebra as in Proposition
3.12. For any $\mathrm{(X)\ \in\\{(\top),(\bot),}$
$\mathrm{(SB),(SF),(SI),(WO),(DD),(UD),(AND),(OR)}\\}$,

  1. 1.

$\mathbb{S}\models\mathrm{(X)}\,$ iff
$\,\mathbb{S}_{\rhd}\models\mathrm{(X)^{{\rhd}}}$.

  2. 2.

$\mathbb{S}\models\mathrm{(X)}\,$ iff
$\,\mathbb{S}_{\lhd}\models\mathrm{(X)}^{\lhd}$.

The corollary above can be further refined to various more general classes of
proto-subordination algebras, so as to extend [19, Propositions 4.5 and 4.8]
to an algebraic setting.

An $\mathsf{Alg}(\mathcal{L})$ proto-subordination algebra
$\mathbb{S}=(A,\prec)$ is internally incoherent if $a\prec b$ and $a\prec c$
for some $a,b,c\in A$ such that $F(a)\neq A$ and $F(b,c)=A$; $\mathbb{S}$ is
internally coherent if it is not internally incoherent.

##  4 Slanted algebras arising from defined relational algebras

######  Definition 4.1.

Let $\mathbb{S}=(A,\prec)$, $\mathbb{C}=(A,\mathcal{C})$, and
$\mathbb{D}=(A,\mathcal{D})$ be a proto-subordination algebra, a proto-
precontact algebra, and a dual proto-precontact algebra, respectively.

  1. 1.

if $\mathbb{S}\models\mathrm{(DD)+(UD)+(SB)+(SF)}$, then the slanted algebra
associated with $\mathbb{S}$ is $\mathbb{S}^{*}=(A,\Diamond,\blacksquare)$
s.t. $\Diamond a\coloneqq\bigwedge{\prec}[a]$ and $\blacksquare
a\coloneqq\bigvee{\prec^{-1}}[a]$ for any $a$.

  2. 2.

if
$\mathbb{C}\models\mathrm{(DD)^{\rhd}+(UD)^{\rhd}+(SB)^{\rhd}+(SF)^{\rhd}}$,
then the slanted algebra associated with $\mathbb{C}$ is
$\mathbb{C}^{*}=(A,{\rhd},{\blacktriangleright})$ s.t.
${\rhd}a\coloneqq\bigvee(\mathcal{C}[a])^{c}$ and
${\blacktriangleright}a\coloneqq\bigvee({\mathcal{C}^{-1}}[a])^{c}$ for any
$a$.

  3. 3.

$\mathbb{D}\models\mathrm{(DD)^{\lhd}+(UD)^{\lhd}+(SB)^{\lhd}+(SF)^{\lhd}}$,
then the slanted algebra associated with $\mathbb{D}$ is
$\mathbb{D}^{*}=(A,{\lhd},{\blacktriangleleft})$ s.t.
${\lhd}a\coloneqq\bigwedge(\mathcal{D}[a])^{c}$ and
${\blacktriangleleft}a\coloneqq\bigwedge({\mathcal{D}^{-1}}[a])^{c}$ for any
$a$.

The assumption $\mathbb{S}\models\mathrm{(DD)}$ implies that ${\prec}[a]$ is
down-directed for every $a\in A$, and $\mathbb{S}\models\mathrm{(SF)}$ implies
that ${\prec}[a]\neq\varnothing$. Hence, $\Diamond a\in K(A^{\delta})$.
Likewise, $\mathbb{S}\models\mathrm{(UD)+(SB)}$ guarantees that $\blacksquare
a\in O(A^{\delta})$, and $\mathbb{C}\models\mathrm{(DD)^{\rhd}+(SF)^{\rhd}}$
(resp. $\mathbb{D}\models\mathrm{(DD)^{\lhd}+(SF)^{\lhd}}$) guarantees that
${\rhd}a\in O(A^{\delta})$ (resp. ${\lhd}a\in K(A^{\delta})$) and
$\mathbb{C}\models\mathrm{(UD)^{\rhd}+(SB)^{\rhd}}$ (resp.
$\mathbb{D}\models\mathrm{(UD)^{\lhd}+(SB)^{\lhd}}$) guarantees that
${\blacktriangleright}a\in O(A^{\delta})$ (resp. ${\blacktriangleleft}a\in
K(A^{\delta})$) for all $a\in A$.

######  Lemma 4.2.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$, any proto-
precontact algebra $\mathbb{C}=(A,\mathcal{C})$, any dual proto-precontact
algebra $\mathbb{D}=(A,\mathcal{D})$ and all $a,b\in A$,

  1. 1.

if $\mathbb{S}$ is defined (i.e.
$\mathbb{S}\models\mathrm{(DD)+(SF)+(UD)+(SB)}$), then

    1. (i)

$a\prec b$ implies $\Diamond a\leq b$ and $a\leq\blacksquare b$.

    2. (ii)

if $\mathbb{S}\models\mathrm{(WO)}$, then $\Diamond a\leq b$ iff $a\prec b$.

    3. (iii)

if $\mathbb{S}\models\mathrm{(SI)}$, then $a\leq\blacksquare b$ iff $a\prec
b$.

  2. 2.

if $\mathbb{C}$ is defined (i.e.
$\mathbb{C}\models\mathrm{(DD)^{\rhd}+(SF)^{\rhd}+(UD)^{\rhd}+(SB)^{\rhd}}$),
then

    1. (i)

$a\cancel{\mathcal{C}}b$ implies $b\leq{\rhd}a$ and
$a\leq{\blacktriangleright}b$.

    2. (ii)

if $\mathbb{C}\models\mathrm{(WO)^{\rhd}}$, then $b\leq{\rhd}a$ iff
$a\cancel{\mathcal{C}}b$.

    3. (iii)

if $\mathbb{C}\models\mathrm{(SI)^{\rhd}}$, then $a\leq{\blacktriangleright}b$
iff $a\cancel{\mathcal{C}}b$.

  3. 3.

if $\mathbb{D}$ is defined (i.e.
$\mathbb{D}\models\mathrm{(DD)^{\lhd}+(SF)^{\lhd}+(UD)^{\lhd}+(SB)^{\lhd}}$),
then

    1. (i)

$a\cancel{\mathcal{D}}b$ implies ${\lhd}a\leq b$ and
${\blacktriangleleft}b\leq a$.

    2. (ii)

if $\mathbb{D}\models\mathrm{(WO)^{\lhd}}$, then ${\lhd}a\leq b$ iff
$a\cancel{\mathcal{D}}b$.

    3. (iii)

if $\mathbb{D}\models\mathrm{(SI)^{\lhd}}$, then ${\blacktriangleleft}b\leq a$
iff $a\cancel{\mathcal{D}}b$.

###### Proof.

Below, we group together the proofs of sub-items (i) of each item, and
likewise for sub-items (ii) and (iii).

(i) $a\prec b$ iff $b\in{\prec}[a]$ iff $a\in{\prec}^{-1}[b]$, hence $a\prec
b$ implies $b\geq\bigwedge{\prec}[a]=\Diamond a$ and
$a\leq\bigvee{\prec}^{-1}[b]=\blacksquare b$.

Likewise, $a\cancel{\mathcal{C}}b$ iff $b\notin{\mathcal{C}}[a]$ (i.e.
$b\in({\mathcal{C}}[a])^{c}$) iff $a\notin{\mathcal{C}}^{-1}[b]$ (i.e.
$a\in({\mathcal{C}}^{-1}[b])^{c}$). Hence, $a\cancel{\mathcal{C}}b$ implies
$b\leq\bigvee({\mathcal{C}}[a])^{c}={\rhd}a$ and
$a\leq\bigvee({\mathcal{C}}^{-1}[b])^{c}={\blacktriangleright}b$. Finally,
$a\cancel{\mathcal{D}}b$ iff $b\notin{\mathcal{D}}[a]$ (i.e.
$b\in({\mathcal{D}}[a])^{c}$) iff $a\notin{\mathcal{D}}^{-1}[b]$ (i.e.
$a\in({\mathcal{D}}^{-1}[b])^{c}$). Hence, $a\cancel{\mathcal{D}}b$ implies
$b\geq\bigwedge({\mathcal{D}}[a])^{c}={\lhd}a$ and
$a\geq\bigwedge({\mathcal{D}}^{-1}[b])^{c}={\blacktriangleleft}b$.

(ii) By (i), to complete the proof, we need to show the ‘only if’ direction.
The assumption $\mathbb{S}\models\mathrm{(DD)+(SF)}$ implies that ${\prec}[a]$
is non-empty and down-directed for any $a\in A$. Hence, by compactness,
$\bigwedge{\prec}[a]=\Diamond a\leq b$ implies that $c\leq b$ for some
$c\in{\prec}[a]$, i.e. $a\prec c\leq b$ for some $c\in A$, and by (WO), this
implies that $a\prec b$, as required.

Likewise, the assumption $\mathbb{C}\models\mathrm{(DD)^{\rhd}+(SF)^{\rhd}}$
implies that $({\mathcal{C}}[a])^{c}$ is non-empty and up-directed for any
$a\in A$. Hence, by compactness, $b\leq{\rhd}a=\bigvee({\mathcal{C}}[a])^{c}$
implies that $b\leq c$ for some $c\in({\mathcal{C}}[a])^{c}$ (i.e.
$a\cancel{\mathcal{C}}c$), i.e. $a\cancel{\mathcal{C}}c$ and $b\leq c$ for
some $c\in A$, i.e. $a\cancel{\mathcal{C}}c$ and $b\geq c$ for some $c\in A$.
By $\mathrm{(WO)}^{\rhd}$, this implies that $a\cancel{\mathcal{C}}b$, as
required.

Finally, $\mathbb{D}\models\mathrm{(DD)^{\lhd}+(SF)^{\lhd}}$ implies that
$({\mathcal{D}}[a])^{c}$ is non-empty and down-directed for any $a\in A$.
Hence, by compactness, $\bigwedge({\mathcal{D}}[a])^{c}={\lhd}a\leq b$ implies
that $c\leq b$ for some $c\in({\mathcal{D}}[a])^{c}$ (i.e.
$a\cancel{\mathcal{D}}c$), i.e. $a\cancel{\mathcal{D}}c$ and $c\leq b$ for
some $c\in A$. By $\mathrm{(WO)}^{\lhd}$, this implies that
$a\cancel{\mathcal{D}}b$, as required.

(iii) is proven similarly to (ii), by observing that
$\mathbb{S}\models\mathrm{(UD)+(SB)}$ implies that ${\prec}^{-1}[a]$ is non-
empty and up-directed for every $a\in A$, that
$\mathbb{C}\models\mathrm{(UD)^{\rhd}+(SB)^{\rhd}}$ implies that
$(\mathcal{C}^{-1}[a])^{c}$ is nonempty and up-directed for every $a\in A$,
and that $\mathbb{D}\models\mathrm{(UD)^{\lhd}+(SB)^{\lhd}}$ implies that
$({\mathcal{D}}^{-1}[a])^{c}$ is non-empty and down-directed for every $a\in
A$. ∎

An immediate consequence of the lemma above and Corollary 2.11 is the
following

######  Corollary 4.3.

For any defined proto-subordination algebra $\mathbb{S}=(A,\prec)$, any
defined proto-precontact algebra $\mathbb{C}=(A,\mathcal{C})$, and any defined
dual proto-precontact algebra $\mathbb{D}=(A,\mathcal{D})$, if $A$ is a
bounded lattice, then

  1. 1.

if $\mathbb{S}\models\mathrm{(SI)+(WO)}$, then $\mathbb{S}^{\ast}$ is tense,
hence is normal.

  2. 2.

if $\mathbb{C}\models\mathrm{(SI)^{\rhd}+(WO)^{\rhd}}$, then
$\mathbb{C}^{\ast}$ is tense, hence is normal.

  3. 3.

if $\mathbb{D}\models\mathrm{(SI)^{\lhd}+(WO)^{\lhd}}$, then
$\mathbb{D}^{\ast}$ is tense, hence is normal.

######  Lemma 4.4.

For any defined proto-subordination algebra $\mathbb{S}=(A,\prec)$, any
defined proto-precontact algebra $\mathbb{C}=(A,\mathcal{C})$, and any defined
dual proto-precontact algebra $\mathbb{D}=(A,\mathcal{D})$,

  1. 1.

If $\mathbb{S}$ is bounded and $\mathbb{S}\models\mathrm{(\bot)}$, then
$\mathbb{S}^{\ast}\models\Diamond\bot\leq\bot$.

  2. 2.

If $\mathbb{S}$ is bounded and $\mathbb{S}\models\mathrm{(\top)}$, then
$\mathbb{S}^{\ast}\models\top\leq\blacksquare\top$.

  3. 3.

If $\mathbb{C}$ is bounded and $\mathbb{C}\models\mathrm{(\bot)^{\rhd}}$, then
$\mathbb{C}^{\ast}\models\top\leq{\rhd}\bot$.

  4. 4.

If $\mathbb{C}$ is bounded and $\mathbb{C}\models\mathrm{(\top)^{\rhd}}$, then
$\mathbb{C}^{\ast}\models\top\leq{\blacktriangleright}\bot$.

  5. 5.

If $\mathbb{D}$ is bounded and $\mathbb{D}\models\mathrm{(\bot)^{\lhd}}$, then
$\mathbb{D}^{\ast}\models{\lhd}\top\leq\bot$.

  6. 6.

If $\mathbb{D}$ is bounded and $\mathbb{D}\models\mathrm{(\top)^{\lhd}}$, then
$\mathbb{D}^{\ast}\models{\blacktriangleleft}\top\leq\bot$.

  7. 7.

If $\mathbb{S}\models\mathrm{(SI)}$, then $\Diamond$ on $\mathbb{S}^{*}$ is
monotone;

  8. 8.

if $\mathbb{S}\models\mathrm{(WO)}$, then $\blacksquare$ on $\mathbb{S}^{*}$
is monotone.

  9. 9.

If $\mathbb{C}\models\mathrm{(SI)^{\rhd}}$, then ${\rhd}$ on $\mathbb{C}^{*}$
is antitone.

  10. 10.

If $\mathbb{C}\models\mathrm{(WO)^{\rhd}}$, then ${\blacktriangleright}$ on
$\mathbb{C}^{*}$ is antitone.

  11. 11.

If $\mathbb{D}\models\mathrm{(SI)^{\lhd}}$, then ${\lhd}$ on $\mathbb{D}^{*}$
is antitone.

  12. 12.

If $\mathbb{D}\models\mathrm{(WO)^{\lhd}}$, then ${\blacktriangleleft}$ on
$\mathbb{D}^{*}$ is antitone.

###### Proof.

1\. By assumption, $\bot\in{\prec}[\bot]$; hence,
$\Diamond\bot=\bigwedge{\prec}[\bot]\leq\bot$, as required. The proofs of 2-6
are similar. 7\. Let $a,b\in A$ s.t. $a\leq b$. To show that $\Diamond
a=\bigwedge{\prec}[a]\leq\bigwedge{\prec}[b]=\Diamond b$, it is enough to show
that ${\prec}[b]\subseteq{\prec}[a]$, i.e. that if $x\in A$ and $b\prec x$,
then $a\prec x$. Indeed, by (SI), $a\leq b\prec x$ implies $a\prec x$, as
required. Item 8 is shown similarly. Likewise, as to 9, to show that
${\rhd}b=\bigvee({\mathcal{C}}[b])^{c}\leq\bigvee({\mathcal{C}}[a])^{c}={\rhd}a$
whenever $a\leq b$, it is enough to show that
$({\mathcal{C}}[b])^{c}\subseteq({\mathcal{C}}[a])^{c}$, i.e. that
${\mathcal{C}}[a]\subseteq{\mathcal{C}}[b]$, i.e. that if $c\in A$ and
$a\mathcal{C}c$, then $b\mathcal{C}c$, which is exactly what is guaranteed by
(SI)⊳ under $a\leq b$. The proofs of 10-12 are similar. ∎

The following lemma shows that the converse conditions of Lemma 4.4 hold under
additional assumptions.

######  Lemma 4.5.

For any defined proto-subordination algebra $\mathbb{S}=(A,\prec)$, any
defined proto-precontact algebra $\mathbb{C}=(A,\mathcal{C})$, and any defined
dual proto-precontact algebra $\mathbb{D}=(A,\mathcal{D})$,

  1. 1.

If $\mathbb{S}\models\mathrm{(WO)}$, then

    1. (i)

$\mathbb{S}\models\mathrm{(SI)}\quad$ iff $\quad\Diamond$ on
$\mathbb{S}^{\ast}$ is monotone.

    2. (ii)

if $\mathbb{S}$ is $\vee$-SL based, then $\mathbb{S}\models\mathrm{(OR)}\quad$
iff $\quad\mathbb{S}^{\ast}\models\Diamond(a\vee b)\leq\Diamond a\vee\Diamond
b$.

    3. (iii)

if $\mathbb{S}$ is bounded, then $\mathbb{S}\models(\bot)\quad$ iff
$\quad\mathbb{S}^{\ast}\models\Diamond\bot\leq\bot$.

  2. 2.

If $\mathbb{S}\models\mathrm{(SI)}$, then

    1. (i)

$\mathbb{S}\models\mathrm{(WO)}\quad$ iff $\quad\blacksquare$ on
$\mathbb{S}^{\ast}$ is monotone.

    2. (ii)

if $\mathbb{S}$ is $\wedge$-SL based, then
$\mathbb{S}\models\mathrm{(AND)}\quad$ iff
$\quad\mathbb{S}^{\ast}\models\blacksquare a\wedge\blacksquare
b\leq\blacksquare(a\wedge b)$.

    3. (iii)

if $\mathbb{S}$ is bounded, then $\mathbb{S}\models(\top)\quad$ iff
$\quad\mathbb{S}^{\ast}\models\top\leq\blacksquare\top$.

  3. 3.

If $\mathbb{C}\models\mathrm{(WO)^{\rhd}}$, then

    1. (i)

$\mathbb{C}\models\mathrm{(SI)^{\rhd}}\quad$ iff $\quad{\rhd}$ on
$\mathbb{C}^{\ast}$ is antitone.

    2. (ii)

if $\mathbb{C}$ is $\vee$-SL based, then
$\mathbb{C}\models\mathrm{(OR)^{\rhd}}\quad$ iff
$\quad\mathbb{C}^{\ast}\models{\rhd}a\wedge{\rhd}b\leq{\rhd}(a\vee b)$.

    3. (iii)

if $\mathbb{C}$ is bounded, then $\mathbb{C}\models(\bot)^{\rhd}\quad$ iff
$\quad\mathbb{C}^{\ast}\models\top\leq{\rhd}\bot$.

  4. 4.

If $\mathbb{C}\models\mathrm{(SI)^{\rhd}}$, then

    1. (i)

$\mathbb{C}\models\mathrm{(WO)^{\rhd}}\quad$ iff $\quad{\blacktriangleright}$
on $\mathbb{C}^{\ast}$ is antitone.

    2. (ii)

if $\mathbb{C}$ is $\vee$-SL based, then
$\mathbb{C}\models\mathrm{(AND)^{\rhd}}\;$ iff
$\;\mathbb{C}^{\ast}\models{\blacktriangleright}a\wedge{\blacktriangleright}b\leq{\blacktriangleright}(a\vee
b)$.

    3. (iii)

if $\mathbb{C}$ is bounded, then $\mathbb{C}\models(\top)^{\rhd}\quad$ iff
$\quad\mathbb{C}^{\ast}\models\top\leq{\blacktriangleright}\bot$.

  5. 5.

If $\mathbb{D}\models\mathrm{(WO)^{\lhd}}$, then

    1. (i)

$\mathbb{D}\models\mathrm{(SI)^{\lhd}}\quad$ iff $\quad{\lhd}$ on
$\mathbb{D}^{\ast}$ is antitone.

    2. (ii)

if $\mathbb{D}$ is $\vee$-SL based, then
$\mathbb{D}\models\mathrm{(OR)^{\lhd}}\quad$ iff
$\quad\mathbb{D}^{\ast}\models{\lhd}(a\wedge b)\leq{\lhd}a\vee{\lhd}b$.

    3. (iii)

if $\mathbb{D}$ is bounded, then $\mathbb{D}\models(\bot)^{\lhd}\quad$ iff
$\quad\mathbb{D}^{\ast}\models{\lhd}\top\leq\bot$.

  6. 6.

If $\mathbb{D}\models\mathrm{(SI)^{\lhd}}$, then

    1. (i)

$\mathbb{D}\models\mathrm{(WO)^{\lhd}}\quad$ iff $\quad{\blacktriangleleft}$
on $\mathbb{D}^{\ast}$ is antitone.

    2. (ii)

if $\mathbb{D}$ is $\vee$-SL based, then
$\mathbb{D}\models\mathrm{(AND)^{\lhd}}\;$ iff
$\;\mathbb{D}^{\ast}\models{\blacktriangleleft}(a\wedge
b)\leq{\blacktriangleleft}a\vee{\blacktriangleleft}b$.

    3. (iii)

if $\mathbb{D}$ is bounded, then $\mathbb{D}\models(\top)^{\lhd}\quad$ iff
$\quad\mathbb{D}^{\ast}\models{\blacktriangleleft}\top\leq\bot$.

###### Proof.

1\. (i) By Lemma 4.4 7, the proof is complete if we show the ‘if’ direction.
Let $a,b,x\in A$ s.t. $a\leq b\prec x$. By Lemma 4.2 1(ii), to show that
$a\prec x$, it is enough to show that $\Diamond a\leq x$. Since $\Diamond$ is
monotone, $a\leq b$ implies $\Diamond a\leq\Diamond b$, and, by Lemma 4.2
1(i), $b\prec x$ implies that $\Diamond b\leq x$. Hence, $\Diamond a\leq x$,
as required.

(ii) From left to right, let $a,b\in A$. Since both $\Diamond(a\vee b)$ and
$\Diamond a\vee\Diamond b$ are closed elements of $A^{\delta}$ (cf.
Proposition 2.6 1(iv)), by Proposition 2.6 1(i), to show that $\Diamond(a\vee
b)\leq\Diamond a\vee\Diamond b$, it is enough to show that for any $x\in A$,
if $\Diamond a\vee\Diamond b\leq x$, then $\Diamond(a\vee b)\leq x$.

$\Diamond a\vee\Diamond b\leq x$ | iff |  $\Diamond a\leq x$ and $\Diamond b\leq x$ |
---|---|---|---
| iff |  $a\prec x$ and $b\prec x$ | Lemma 4.2.1(ii) (WO)
| implies | $a\vee b\prec x$ | (OR)
| implies | $\Diamond(a\vee b)\leq x$ | Lemma 4.2.1(i)

Conversely, let $a,b,x\in A$ s.t. $a\prec x$ and $b\prec x$. By Lemma 4.2
(ii), to show that $a\vee b\prec x$, it is enough to show that $\Diamond(a\vee
b)\leq x$, and since $\mathbb{S}^{\ast}\models\Diamond(a\vee b)\leq\Diamond
a\vee\Diamond b$, it is enough to show that $\Diamond a\vee\Diamond b\leq x$,
i.e. that $\Diamond a\leq x$ and $\Diamond b\leq x$. These two inequalities
hold by Lemma 4.2 1(i), and the assumptions on $a,b$ and $x$.

(iii) By Lemma 4.2 (ii), $\bot\prec\bot$ is equivalent to
$\Diamond\bot\leq\bot$, as required. 2\. is proven similarly.

3\. (i) By Lemma 4.4 9, the proof is complete if we show the ‘if’ direction.
Let $a,b,x\in A$ s.t. $a\leq b\cancel{\mathcal{C}}x$. By Lemma 4.2 2(ii), to
show that $a\cancel{\mathcal{C}}x$, it is enough to show that $x\leq{\rhd}a$.
Since ${\rhd}$ is antitone, $a\leq b$ implies ${\rhd}b\leq{\rhd}a$, and, by
Lemma 4.2 2(i), $b\cancel{\mathcal{C}}x$ implies that $x\leq{\rhd}b$. Hence,
$x\leq{\rhd}a$, as required.

(ii) From left to right, let $a,b\in A$. Since both ${\rhd}(a\vee b)$ and
${\rhd}a\wedge{\rhd}b$ are open elements of $A^{\delta}$ (cf. Proposition 2.6
1(v)), by Proposition 2.6 1(ii), to show that
${\rhd}a\wedge{\rhd}b\leq{\rhd}(a\vee b)$, it is enough to show that for any
$x\in A$, if $x\leq{\rhd}a\wedge{\rhd}b$, then $x\leq{\rhd}(a\vee b)$.

$x\leq{\rhd}a\wedge{\rhd}b$ | iff |  $x\leq{\rhd}a$ and $x\leq{\rhd}b$ |
---|---|---|---
| iff |  $x\cancel{\mathcal{C}}a$ and $x\cancel{\mathcal{C}}b$ | Lemma 4.2.2(ii) (WO)⊳
| implies | $(a\vee b)\cancel{\mathcal{C}}x$ | (OR)⊳
| implies | $x\leq{\rhd}(a\vee b)$ | Lemma 4.2.2(i)

Conversely, let $a,b,x\in A$ s.t. $a\cancel{\mathcal{C}}x$ and
$b\cancel{\mathcal{C}}x$. By Lemma 4.2.2(ii), to show that $(a\vee
b)\cancel{\mathcal{C}}x$, it is enough to show that $x\leq{\rhd}(a\vee b)$,
and since $\mathbb{S}^{\ast}\models{\rhd}a\wedge{\rhd}b\leq{\rhd}(a\vee b)$,
it is enough to show that $x\leq{\rhd}a\wedge{\rhd}b$, i.e. that
$x\leq{\rhd}a$ and $x\leq{\rhd}b$. These two inequalities hold by Lemma
4.2.2(i), and the assumptions on $a,b$ and $x$.

(iii) By Lemma 4.2.2(ii), $\bot\cancel{\mathcal{C}}\top$ is equivalent to
$\top\leq{\rhd}\bot$, as required. 4\. is proven similarly.

5\. (i) By Lemma 4.4.11, the proof is complete if we show the ‘if’ direction.
For contraposition, let $a,b,x\in A$ s.t. $a\leq b\ \&\
a\cancel{\mathcal{D}}x$. By Lemma 4.2.3(ii), to show that
$b\cancel{\mathcal{D}}x$, it is enough to show that ${\lhd}b\leq x$. Since
${\lhd}$ is antitone, $a\leq b$ implies ${\lhd}b\leq{\lhd}a$, and, by Lemma
4.2.3(i), $a\cancel{\mathcal{D}}x$ implies that ${\lhd}a\leq x$. Hence,
${\lhd}b\leq x$, as required.

(ii) From left to right, let $a,b\in A$. Since both ${\lhd}(a\wedge b)$ and
${\lhd}a\vee{\lhd}b$ are closed elements of $A^{\delta}$ (cf. Proposition
2.6.1(iv)), by Proposition 2.6.1(i), to show that ${\lhd}(a\wedge
b)\leq{\lhd}a\vee{\lhd}b$, it is enough to show that for any $x\in A$, if
${\lhd}a\vee{\lhd}b\leq x$, then${\lhd}(a\wedge b)\leq x$.

${\lhd}a\vee{\lhd}b\leq x$ | iff | ${\lhd}a\leq x\ \&\ {\lhd}b\leq x$ |
---|---|---|---
| iff |  $a\cancel{\mathcal{D}}x$ and $b\cancel{\mathcal{D}}b$ | Lemma 4.2.3(ii) (WO)⊲
| implies | $(a\wedge b)\cancel{\mathcal{D}}x$ | (OR)⊲
| implies | ${\lhd}(a\wedge b)\leq x$ | Lemma 4.2.3(i)

Conversely, for contraposition, let $a,b,x\in A$ s.t. $a\cancel{\mathcal{D}}x$
and $b\cancel{\mathcal{D}}x$. By Lemma 4.2.3(ii), to show that $(a\wedge
b)\cancel{\mathcal{D}}x$, it is enough to show that ${\lhd}(a\wedge b)\leq x$,
and since $\mathbb{S}^{\ast}\models{\lhd}(a\wedge b)\leq{\lhd}a\vee{\lhd}b$,
it is enough to show that ${\lhd}a\vee{\lhd}b\leq x$, i.e. that ${\lhd}a\leq
x$ and ${\lhd}b\leq x$. These two inequalities hold by Lemma 4.2.3(i), and the
assumptions on $a,b$ and $x$.

(iii) By Lemma 4.2.3(ii), $\top\cancel{\mathcal{D}}\bot$ is equivalent to
${\lhd}\top\leq\bot$, as required. 6\. is proven similarly. ∎

######  Corollary 4.6.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$, any proto-
precontact algebra $\mathbb{C}=(A,\mathcal{C})$, and any dual proto-precontact
algebra $\mathbb{D}=(A,\mathcal{D})$,

  1. 1.

if $\mathbb{S}$ is defined, then

    1. (i)

$\mathbb{S}$ is monotone iff $\mathbb{S}^{*}$ is monotone;

    2. (ii)

$\mathbb{S}$ is regular iff $\mathbb{S}^{*}$ is regular;

    3. (iii)

$\mathbb{S}$ is a subordination algebra iff $\mathbb{S}^{*}$ is normal.

  2. 2.

if $\mathbb{C}$ is defined, then

    1. (i)

$\mathbb{C}$ is antitone iff $\mathbb{C}^{*}$ is antitone;

    2. (ii)

$\mathbb{C}$ is regular iff $\mathbb{C}^{*}$ is regular;

    3. (iii)

$\mathbb{C}$ is a precontact algebra iff $\mathbb{C}^{*}$ is normal.

  3. 3.

if $\mathbb{D}$ is defined, then

    1. (i)

$\mathbb{D}$ is antitone iff $\mathbb{D}^{*}$ is antitone;

    2. (ii)

$\mathbb{D}$ is regular iff $\mathbb{D}^{*}$ is regular;

    3. (iii)

$\mathbb{D}$ is a dual precontact algebra iff $\mathbb{D}^{*}$ is normal.

######  Lemma 4.7.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$, any proto-
precontact algebra $\mathbb{C}=(A,\mathcal{C})$ and any dual proto-precontact
algebra $\mathbb{D}=(A,\mathcal{D})$, for all $a,b\in A$, $k,h\in
K(A^{\delta})$, and $o,p\in O(A^{\delta})$, and all $D\subseteq A$ nonempty
and down-directed, and $U\subseteq A$ nonempty and up-directed,

  1. 1.

if $\mathbb{S}$ is $\Diamond$-monotone (i.e.
$\mathbb{S}\models\mathrm{(SF)+(DD)+(WO)+(SI)}$), then

    1. (i)

${\prec}[D]\coloneqq\\{c\ |\ \exists a(a\in D\ \&\ a\prec c)\\}$ is nonempty
and down-directed;

    2. (ii)

if $k=\bigwedge D$, then $\Diamond k=\bigwedge{\prec}[D]\in K(A^{\delta})$;

    3. (iii)

$\Diamond k\leq b$ implies $a\prec b$ for some $a\in A$ s.t. $k\leq a$;

    4. (iv)

$\Diamond k\leq o$ implies $a\prec b$ for some $a,b\in A$ s.t. $k\leq a$ and
$b\leq o$.

  2. 2.

if $\mathbb{S}$ is $\blacksquare$-monotone (i.e.
$\mathbb{S}\models\mathrm{(SB)+(UD)+(WO)+(SI)}$), then

    1. (i)

${\prec}^{-1}[U]\coloneqq\\{c\ |\ \exists a(a\in U\ \&\ c\prec a)\\}$ is
nonempty and up-directed;

    2. (ii)

if $o=\bigvee U$, then $\blacksquare o=\bigvee{\prec}^{-1}[U]\in
O(A^{\delta})$;

    3. (iii)

$a\leq\blacksquare o$ implies $a\prec b$ for some $b\in A$ s.t. $b\leq o$.

    4. (iv)

$k\leq\blacksquare o$ implies $a\prec b$ for some $a,b\in A$ s.t. $k\leq a$
and $b\leq o$.

  3. 3.

if $\mathbb{C}$ is ${\rhd}$-antitone (i.e.
$\mathbb{C}\models\mathrm{(SF)^{\rhd}+(DD)^{\rhd}+(WO)^{\rhd}+(SI)^{\rhd}}$),
then

    1. (i)

${\cancel{\mathcal{C}}}[D]\coloneqq\\{c\ |\ \exists a(a\in D\ \&\
a\cancel{\mathcal{C}}c)\\}$ is nonempty and up-directed;

    2. (ii)

if $k=\bigwedge D$, then ${\rhd}k=\bigvee{\cancel{\mathcal{C}}}[D]\in
O(A^{\delta})$;

    3. (iii)

$a\leq{\rhd}k$ implies $c\cancel{\mathcal{C}}a$ for some $c\in A$ s.t. $k\leq
c$;

    4. (iv)

$h\leq{\rhd}k$ implies $c\cancel{\mathcal{C}}b$ for some $b,c\in A$ s.t.
$h\leq b$ and $k\leq c$.

  4. 4.

if $\mathbb{C}$ is ${\blacktriangleright}$-antitone (i.e.
$\mathbb{C}\models\mathrm{(SB)^{\rhd}+(UD)^{\rhd}+(WO)^{\rhd}+(SI)^{\rhd}}$),
then

    1. (i)

${\cancel{\mathcal{C}}}^{-1}[D]\coloneqq\\{c\ |\ \exists a(a\in D\ \&\
c\cancel{\mathcal{C}}a)\\}$ is nonempty and up-directed;

    2. (ii)

if $k=\bigwedge D$, then
${\blacktriangleright}k=\bigvee{\cancel{\mathcal{C}}}^{-1}[D]\in
O(A^{\delta})$;

    3. (iii)

$a\leq{\blacktriangleright}k$ implies $a\cancel{\mathcal{C}}c$ for some $c\in
A$ s.t. $k\leq c$;

    4. (iv)

$h\leq{\blacktriangleright}k$ implies $b\cancel{\mathcal{C}}c$ for some
$b,c\in A$ s.t. $h\leq b$ and $k\leq c$.

  5. 5.

if $\mathbb{D}$ is ${\lhd}$-antitone (i.e.
$\mathbb{D}\models\mathrm{(SF)^{\lhd}+(DD)^{\lhd}+(WO)^{\lhd}+(SI)^{\lhd}}$),
then

    1. (i)

$\cancel{\mathcal{D}}[U]\coloneqq\\{c\ |\ \exists a(a\in U\ \&\
a\cancel{\mathcal{D}}c)\\}$ is nonempty and down-directed;

    2. (ii)

if $o=\bigvee U$, then ${\lhd}o=\bigwedge\cancel{\mathcal{D}}[U]\in
K(A^{\delta})$;

    3. (iii)

${\lhd}o\leq a$ implies $c\cancel{\mathcal{D}}a$ for some $c\in A$ s.t. $c\leq
o$;

    4. (iv)

${\lhd}o\leq p$ implies $c\cancel{\mathcal{D}}a$ for some $a,c\in A$ s.t.
$c\leq o$ and $a\leq p$.

  6. 6.

if $\mathbb{D}$ is ${\blacktriangleleft}$-antitone (i.e.
$\mathbb{D}\models\mathrm{(SB)^{\lhd}+(UD)^{\lhd}+(WO)^{\lhd}+(SI)^{\lhd}}$),
then

    1. (i)

${\cancel{\mathcal{C}}}^{-1}[U]\coloneqq\\{c\ |\ \exists a(a\in U\ \&\
c\cancel{\mathcal{D}}a)\\}$ is nonempty and down-directed;

    2. (ii)

if $o=\bigvee U$, then
${\blacktriangleleft}o=\bigwedge{\cancel{\mathcal{D}}}^{-1}[U]\in
K(A^{\delta})$;

    3. (iii)

${\blacktriangleleft}o\leq a$ implies $a\cancel{\mathcal{D}}c$ for some $c\in
A$ s.t. $c\leq o$;

    4. (iv)

${\blacktriangleleft}o\leq p$ implies $a\cancel{\mathcal{D}}c$ for some
$a,c\in A$ s.t. $a\leq p$ and $c\leq o$.

###### Proof.

1\. (i) By (SF), $D$ nonempty implies that so is ${\prec}[D]$. If
$c_{i}\in{\prec}[D]$ for $1\leq i\leq 2$, then $a_{i}\prec c_{i}$ for some
$a_{i}\in D$. Since $D$ is down-directed, some $a\in D$ exists s.t. $a\leq
a_{i}$ for each $i$. Thus, $\mathrm{(SI)}$ implies that $a\prec c_{i}$, from
which the claim follows by $\mathrm{(DD)}$.

(ii) By definition, $\Diamond k\coloneqq\bigwedge\\{\Diamond a\ |\ a\in
A,k\leq a\\}=\bigwedge\\{c\ |\ \exists a(a\prec c\ \&\ k\leq a)\\}$. Since
$k=\bigwedge D$, by compactness, $k\leq a$ iff $d\leq a$ for some $d\in D$.
Thus, $\Diamond k=\bigwedge\\{c\ |\ \exists a(a\prec c\ \&\ k\leq
a)\\}=\bigwedge\\{c\ |\ \exists a(a\in\lfloor D\rfloor\ \&\ a\prec
c)\\}=\bigwedge{\prec}[D]\in K(A^{\delta})$, the last membership holding by
(i).

(iii) Let $k=\bigwedge D$ for some $D\subseteq A$ nonempty and down-directed.
By (ii), $K(A^{\delta})\ni\Diamond k=\bigwedge{\prec}[D]$. Hence, $\Diamond
k\leq b$ implies by compactness that $c\leq b$ for some $c\in A$ s.t. $a\prec
c$ for some $a\in D$ (hence $k=\bigwedge D\leq a$). By $\mathrm{(WO)}$, this
implies that $a\prec b$ for some $a\in A$ s.t. $k\leq a$, as required.

(iv) By (ii), $\Diamond k\in K(A^{\delta})$. Moreover, $o\in O(A^{\delta})$
implies that $o=\bigvee U$ for some nonempty and up-directed $U\subseteq A$.
Hence, by compactness and (iii), $\Diamond k\leq o$ implies that $a\prec b$
for some $a\in A$ s.t. $k\leq a$ and some $b\in U$ (for which $b\leq o$). The
proof of 2 is similar.

3\. (i) By (SF)⊳, $D$ is nonempty implies that so is
$\cancel{\mathcal{C}}[D]$. If $c_{i}\in\cancel{\mathcal{C}}[D]$ for $1\leq
i\leq 2$, then $a_{i}\cancel{\mathcal{C}}c_{i}$ for some $a_{i}\in D$. Since
$D$ is down-directed, some $a\in D$ exists s.t. $a\leq a_{i}$ for each $i$.
Thus, $\mathrm{(SI)^{\rhd}}$ implies that $a\cancel{\mathcal{C}}c_{i}$, from
which the claim follows by $\mathrm{(DD)^{\rhd}}$.

(ii) By definition, ${\rhd}k\coloneqq\bigvee\\{{\rhd}a\ |\ a\in A,k\leq
a\\}=\bigvee\\{c\ |\ \exists a(a\cancel{\mathcal{C}}c\ \&\ k\leq a)\\}$. Since
$k=\bigwedge D$, by compactness, $k\leq a$ iff $d\leq a$ for some $d\in D$.
Thus, ${\rhd}k=\bigvee\\{c\ |\ \exists a(a\cancel{\mathcal{C}}c\ \&\ k\leq
a)\\}=\bigvee\\{c\ |\ \exists a(a\in\lfloor D\rfloor\ \&\
a\cancel{\mathcal{C}}c)\\}=\bigvee\cancel{\mathcal{C}}[D]\in O(A^{\delta})$,
the last membership holding by (i).

(iii) Let $k=\bigwedge D$ for some $D\subseteq A$ nonempty and down-directed.
By (ii), $O(A^{\delta})\ni{\rhd}k=\bigvee\cancel{\mathcal{C}}[D]$. Hence,
$a\leq{\rhd}k$ implies by compactness that $a\leq b$ for some $b\in A$ s.t.
$c\cancel{\mathcal{C}}b$ for some $c\in D$ (hence $k=\bigwedge D\leq c$). By
$\mathrm{(WO)}^{\rhd}$, this implies that $c\cancel{\mathcal{C}}a$ for some
$c\in A$ s.t. $k\leq c$, as required.

(iv) By (ii), ${\rhd}k\in O(A^{\delta})$. Moreover, $h\in K(A^{\delta})$
implies that $h=\bigwedge E$ for some nonempty and down-directed $E\subseteq
A$. Hence, by compactness and (iii), $h\leq{\rhd}k$ implies that $h\leq b$ for
some $b\in\cancel{\mathcal{C}}[D]$, i.e. $c\cancel{\mathcal{C}}b$ for some
$c\in D$ (for which $k\leq c$). The proof of 4 is similar.

5\. (i) By (SF)⊲, $D$ is nonempty implies that so is
$\cancel{\mathcal{D}}[U]$. If $c_{i}\in\cancel{\mathcal{D}}[U]$ for $1\leq
i\leq 2$, then $a_{i}\cancel{\mathcal{D}}c_{i}$ for some $a_{i}\in U$. Since
$U$ is up-directed, some $a\in U$ exists s.t. $a_{i}\leq a$ for each $i$.
Thus, $\mathrm{(SI)^{\lhd}}$ implies that $a\cancel{\mathcal{D}}c_{i}$, from
which the claim follows by $\mathrm{(DD)^{\lhd}}$.

(ii) By definition, ${\lhd}o\coloneqq\bigwedge\\{{\lhd}a\ |\ a\in A,a\leq
o\\}=\bigwedge\\{c\ |\ \exists a(a\cancel{\mathcal{D}}c\ \&\ a\leq o)\\}$.
Since $o=\bigvee U$, by compactness, $a\leq o$ iff $a\leq d$ for some $d\in
U$. Thus, ${\lhd}o=\bigwedge\\{c\ |\ \exists a(a\cancel{\mathcal{D}}c\ \&\
a\leq o)\\}=\bigwedge\\{c\ |\ \exists a(a\in\lceil U\rceil\ \&\
a\cancel{\mathcal{D}}c)\\}=\bigwedge\cancel{\mathcal{D}}[U]\in K(A^{\delta})$,
the last membership holding by (i).

(iii) Let $o=\bigvee U$ for some $U\subseteq A$ nonempty and down-directed. By
(ii), $K(A^{\delta})\ni{\lhd}o=\bigwedge\cancel{\mathcal{D}}[U]$. Hence,
${\lhd}o\leq a$ implies by compactness that $b\leq a$ for some $b\in A$ s.t.
$c\cancel{\mathcal{D}}b$ for some $c\in U$ (hence $o=\bigvee U\geq c$). By
$\mathrm{(WO)}^{\lhd}$, this implies that $c\cancel{\mathcal{D}}a$ for some
$c\in A$ s.t. $c\leq o$, as required.

(iv) By (ii), ${\lhd}o\in K(A^{\delta})$. Moreover, $p\in O(A^{\delta})$
implies that $p=\bigvee V$ for some nonempty and up-directed $V\subseteq A$.
Hence, by compactness and (iii), ${\lhd}o\leq p$ implies that $b\leq p$ for
some $b\in\cancel{\mathcal{D}}[U]$, i.e. $c\cancel{\mathcal{D}}b$ for some
$c\in U$ (for which $c\leq o$). The proof of 4 is similar. ∎

##  5 Modal characterization of classes of relational algebras

######  Proposition 5.1.

For any proto-subordination algebra $\mathbb{S}=(A,\prec)$,

  1. 1.

If $\mathbb{S}$ is monotone, then

    1. (i)

$\mathbb{S}\models\;\prec\ \subseteq\ \leq\ $ iff $\ \mathbb{S}^{*}\models
a\leq\Diamond a\ $ iff $\ \mathbb{S}^{*}\models\blacksquare a\leq a$.

    2. (ii)

$\mathbb{S}\models\;\leq\ \subseteq\ \prec\ $ iff $\
\mathbb{S}^{*}\models\Diamond a\leq a\ $ iff $\ \mathbb{S}^{*}\models
a\leq\blacksquare a$.

    3. (iii)

$\mathbb{S}\models\mathrm{(T)}\quad$ iff $\quad\mathbb{S}^{*}\models\Diamond
a\leq\Diamond\Diamond a$.

    4. (iv)

$\mathbb{S}\models\mathrm{(D)}\quad$ iff
$\quad\mathbb{S}^{*}\models\Diamond\Diamond a\leq\Diamond a$.

  2. 2.

If $\mathbb{S}$ is monotone and $\wedge$-SL based, then

    1. (i)

$\mathbb{S}\models\mathrm{(CT)}\ $ iff $\ \mathbb{S}^{*}\models\Diamond
a\leq\Diamond(a\wedge\Diamond a)$.

    2. (ii)

$\mathbb{S}\models\mathrm{(SL2)}\ $ iff $\
\mathbb{S}^{*}\models\Diamond(\Diamond a\wedge\Diamond b)\leq\Diamond(a\wedge
b)$.

  3. 3.

If $\mathbb{S}$ is monotone and $\vee$-SL based, then

    1. (i)

$\mathbb{S}\models\mathrm{(SL1)}\ $ iff $\
\mathbb{S}^{*}\models\blacksquare(a\vee b)\leq\blacksquare(\blacksquare
a\vee\blacksquare b)$.

    2. (ii)

$\mathbb{S}\models\mathrm{(S9\Leftarrow)}\ $ iff $\
\mathbb{S^{*}}\models\blacksquare a\vee\blacksquare
b\leq\blacksquare(a\vee\blacksquare b)$.

    3. (iii)

$\mathbb{S}\models\mathrm{(S9\Rightarrow)}\ $ iff $\
\mathbb{S^{*}}\models\blacksquare(a\vee\blacksquare b)\leq\blacksquare
a\vee\blacksquare b$.

    4. (iv)

$\mathbb{S}\models\mathrm{(DCT)}$ iff $\
\mathbb{S^{*}}\models\blacksquare(a\vee\blacksquare a)\leq\blacksquare a$.

  4. 4.

if $\mathbb{S}$ is monotone and based on $(A,\neg)$ with $A\models\forall
a\forall b(\neg a\leq b\Leftrightarrow\neg b\leq a)$,

    1. (i)

$\mathbb{S}\models\mathrm{(S6)}\ $ iff $\ \mathbb{S^{*}}\models\neg\Diamond
a=\blacksquare\neg a$. Thus, if $A\models\neg\neg a=a$, then $\blacksquare
a\coloneqq\neg\Diamond\neg a$.

  5. 5.

if $\mathbb{S}$ is monotone and based on $(A,\neg)$ with $A\models\forall
a\forall b(a\leq\neg b\Leftrightarrow b\leq\neg a)$,

    1. (i)

$\mathbb{S}\models\mathrm{(S6)}\ $ iff $\ \mathbb{S^{*}}\models\Diamond\neg
a=\neg\blacksquare a$. Thus, if $A\models\neg\neg a=a$, then $\Diamond
a\coloneqq\neg\blacksquare\neg a$.

###### Proof.

In what follows, variables $a,b,c\ldots$ range in $A$. Also, for the sake of a
more concise and readable presentation, we will write conjunctions of
relational atoms as chains; for instance, $a\leq b\ \&\ b\prec c$ will be
written as $a\leq b\prec c$.

1 (i)

$\forall a(a\leq\Diamond a)$ | iff | $\forall a\forall b(\Diamond a\leq b\Rightarrow a\leq b)$ | Proposition 2.6.1(i)
---|---|---|---
| iff | $\forall a\forall b(a\prec b\Rightarrow a\leq b)$ |
| iff | $\prec\ \subseteq\ \leq$ |

(ii)

$\forall a(\Diamond a\leq a)$ | iff | $\forall a\forall b(a\leq b\Rightarrow\Diamond a\leq b)$ | Proposition 2.6.1(i)
---|---|---|---
| iff | $\forall a\forall b(a\leq b\Rightarrow a\prec b)$ |
| iff | $\leq\ \subseteq\ \prec$ |

(iii)

| $\forall a(\Diamond a\leq\Diamond\Diamond a)$ |
---|---|---
iff | $\forall a\forall c(\Diamond\Diamond a\leq c\Rightarrow\Diamond a\leq c)$ | Proposition 2.6.1(i)
iff | $\forall a\forall c(\exists b(a\prec b\ \&\ \Diamond b\leq c)\Rightarrow\Diamond a\leq c)$ | Lemma 4.7.1(iii)
iff | $\forall a\forall b\forall c(a\prec b\prec c\Rightarrow a\prec c)$ | Lemma 4.2.1(ii)

(iv)

| $\forall a(\Diamond\Diamond a\leq\Diamond a)$ |
---|---|---
iff | $\forall a\forall c(\Diamond a\leq c\Rightarrow\Diamond\Diamond a\leq c)$ | Proposition 2.6.1(i)
iff | $\forall a\forall c(\Diamond a\leq c\Rightarrow\exists b(b\prec c\ \&\ \Diamond a\leq b)$ | Lemma 4.7.1(iii)
iff | $\forall a\forall c(a\prec c\Rightarrow\exists b(a\prec b\ \&\ b\prec c))$ | Lemma 4.2.1(ii)

2(i)

| $\forall a(\Diamond a\leq\Diamond(a\wedge\Diamond a))$ |
---|---|---
iff | $\forall a\forall c(\Diamond(a\wedge\Diamond a)\leq c\Rightarrow\Diamond a\leq c)$ | Proposition 2.6.1(i)
iff | $\forall a\forall c(\exists d(a\wedge\Diamond a\leq d\prec c)\Rightarrow\Diamond a\leq c)$ | Lemma 4.7.1(iii)
iff | $\forall a\forall c\forall d(a\wedge\Diamond a\leq d\prec c\Rightarrow\Diamond a\leq c)$ |
iff | $\forall a\forall c\forall d(\exists b(\Diamond a\leq b\ \&\ a\wedge b\leq d\prec c)\Rightarrow\Diamond a\leq c)$ | Proposition 2.7.1(iii)
iff | $\forall a\forall b\forall c\forall d(a\prec b\ \&\ a\wedge b\leq d\prec c\Rightarrow a\prec c)$ |
iff | $\forall a\forall b\forall c(a\prec b\ \&\ a\wedge b\prec c\Rightarrow a\prec c)$ | $(\ast\ast)$

Let us show the equivalence marked with $(\ast\ast)$. The top-to-bottom
direction immediately obtains by letting $d:=a\wedge b\in A$, since $A$ is a
$\wedge$-SL. Conversely, let $a,b,c,d\in A$ s.t. $a\prec b$ and $a\wedge b\leq
d\prec c$; by (SI), the latter chain implies $a\wedge b\prec c$, hence by
assumption we conclude $a\prec c$, as required.

(ii)

| $\forall a\forall b(\Diamond(\Diamond a\wedge\Diamond b)\leq\Diamond(a\wedge b))$ |
---|---|---
iff | $\forall a\forall b\forall c(\Diamond(a\wedge b)\leq c\Rightarrow\Diamond(\Diamond a\wedge\Diamond b)\leq c)$ | Proposition 2.6.1(i)
iff | $\forall a\forall b\forall c(a\wedge b\prec c\Rightarrow\exists d(d\prec c\ \&\ \Diamond a\wedge\Diamond b\leq d)$ | Lemma 4.7.1(iii)
iff | $\forall a\forall b\forall c(a\wedge b\prec c\Rightarrow\exists d(d\prec c\ \&\ \exists e\exists f(a\prec e\ \&\ b\prec f\ \&\ e\wedge f\leq d)))$ | Proposition 2.7.1(iii)
iff | $\forall a\forall b\forall c(a\wedge b\prec c\Rightarrow\exists d\exists e\exists f(a\prec e\ \&\ b\prec f\ \&\ e\wedge f\leq d\prec c))$ |
iff | $\forall a\forall b\forall c(a\wedge b\prec c\Rightarrow\exists e\exists f((a\prec e\ \&\ b\prec f\ \&\ e\wedge f\prec c))$ | $(\ast\ast)$

For the equivalence marked with $(\ast\ast)$, the bottom-to-top direction
immediately obtains by letting $d:=e\wedge f\in A$. The converse direction
follows from (SI).

3 (i)

| $\forall a\forall b(\blacksquare(a\vee b)\leq\blacksquare(\blacksquare a\vee\blacksquare b))$ |
---|---|---
iff | $\forall a\forall b\forall c(c\leq\blacksquare(a\vee b)\Rightarrow c\leq\blacksquare(\blacksquare a\vee\blacksquare b))$ | Proposition 2.6.1(ii)
iff | $\forall a\forall b\forall c(c\prec a\vee b\Rightarrow c\leq\blacksquare(\blacksquare a\vee\blacksquare b))$ | Lemma 4.2.1(iii)
iff | $\forall a\forall b\forall c(c\prec a\vee b\Rightarrow\exists d(c\prec d\leq\blacksquare a\vee\blacksquare b))$ | Lemma 4.7.2(iii)
iff | $\forall a\forall b\forall c(c\prec a\vee b\Rightarrow\exists d\exists e\exists f(c\prec d\leq e\vee f\ \&\ e\leq\blacksquare a\ \&\ f\leq\blacksquare b))$ | Proposition 2.7.2(iii)
iff | $\forall a\forall b\forall c(c\prec a\vee b\Rightarrow\exists e\exists f(c\prec e\vee f\ \&\ e\leq\blacksquare a\ \&\ f\leq\blacksquare b))$ | $(\ast)$
iff | $\forall a\forall b\forall c(c\prec a\vee b\Rightarrow\exists e\exists f(c\prec e\vee f\ \&\ e\prec a\ \&\ f\prec b))$ | Lemma 4.2.1(iii)

As to the equivalence marked with $(\ast)$, the bottom-to-top direction
obtains by instantiating $d:=e\vee f\in A$, the converse direction follows
from (WO).

(iii)

| $\forall a\forall b(\blacksquare(a\vee\blacksquare b)\leq\blacksquare a\vee\blacksquare b)$ |
---|---|---
iff | $\forall a\forall b\forall c(c\leq\blacksquare(a\vee\blacksquare b)\Rightarrow c\leq\blacksquare a\vee\blacksquare b)$ | Proposition 2.6.1(ii)
iff | $\forall a\forall b\forall c\forall d(c\prec d\leq a\vee\blacksquare b\Rightarrow c\leq\blacksquare a\vee\blacksquare b)$ | Lemma 4.7.2(iv)
iff | $\forall a\forall b\forall c\forall d\forall e(c\prec d\leq a\vee e\ \&\ e\prec b$ | Proposition 2.7.2(iii)
| $\Rightarrow\exists f\exists g(c\leq f\vee g\ \&\ f\prec a\ \&\ g\prec b))$ |
iff | $\forall a\forall b\forall c\forall e(c\prec a\vee e\ \&\ e\prec b\Rightarrow\exists f\exists g(c\leq f\vee g\ \&\ f\prec a\ \&\ g\prec b))$ | $(\ast\ast)$

Let us show the equivalence marked with $(\ast\ast)$. The top-to-bottom
direction obtains by instantiating $d:=a\vee e\in A$. The converse direction
follows from (WO). The proof of (ii) is similar.

(iv)

| $\forall a(\blacksquare(a\vee\blacksquare a)\leq\blacksquare a)$ |
---|---|---
iff | $\forall a\forall b(b\leq\blacksquare(a\vee\blacksquare a)\Rightarrow b\leq\blacksquare a)$ | Proposition 2.6.1(ii)
iff | $\forall a\forall b\forall c(b\prec c\leq a\vee\blacksquare a\Rightarrow b\prec a)$ | Lemma 4.2.1(iii)
iff | $\forall a\forall b\forall c(\exists d(b\prec c\leq a\vee d\ \&\ d\leq\blacksquare a)\Rightarrow b\prec a)$ | Proposition 2.7.2(iii)
iff | $\forall a\forall b\forall c(\exists d(b\prec c\leq a\vee d\ \&\ d\prec a)\Rightarrow b\prec a)$ | Lemma 4.2.1(iii)
iff | $\forall a\forall b\forall d(b\prec a\vee d\ \&\ d\prec a\Rightarrow b\prec a)$ | ($\ast\ast$)

As to the equivalence marked with $(\ast\ast)$, the top-to-bottom direction
obtains by instantiating $c:=a\vee d\in A$. The converse direction follows
from (WO).

4 (i) The proof of this item will make use of the fact that the assumption on
$(A,\neg)$ implies, by Proposition 2.6.2, and basic properties of adjoint maps
between complete lattices (cf. [32]), that $\neg^{\sigma}$ is completely meet-
reversing. Hence, using this latter property in combination with denseness (in
what follows, we will flag this out as ‘denseness +’), a term such as $\neg
k$, for any $k\in K(A^{\delta})$, can be equivalently rewritten as follows:

$\neg k=\neg\bigwedge\\{o\in O(A^{\delta})\mid k\leq o\\}=\bigvee\\{\neg o\mid
o\in O(A^{\delta})\ \&\ k\leq o\\}.$

| $\forall a(\neg\Diamond a\leq\blacksquare\neg a)$ |
---|---|---
iff | $\forall a\forall o(\Diamond a\leq o\Rightarrow\neg o\leq\blacksquare\neg a)$ | denseness +
iff | $\forall a\forall b\forall o(a\prec b\leq o\Rightarrow\neg o\leq\blacksquare\neg a)$ | Lemma 4.7.1(iv)
iff | $\forall a\forall b(a\prec b\Rightarrow\neg b\leq\blacksquare\neg a)$ | $(\ast)$
iff | $\forall a\forall b(a\prec b\Rightarrow\neg b\prec\neg a)$ | Lemma 4.2.1(iii)

For the equivalence marked with $(\ast)$, the top-to-bottom direction obtains
by instantiating $o:=b\in A\subseteq O(A^{\delta})$, and the converse follows
by the antitonicity of $\neg$. The proofs of 5(i) is similar, using the fact
that the assumption on $(A,\neg)$ implies, by Proposition 2.6.3, that
$\neg^{\sigma}$ is completely join-reversing. ∎

######  Remark 5.2.

By Proposition 5.1 1(i) and 2(i), for any monotone proto-subordination algebra
$\mathbb{S}$ which is $\wedge$-SL based, $\mathbb{S}\models\prec\ \subseteq\
\leq$ iff $\mathbb{S}^{\ast}\models a\leq\Diamond a$, which implies
$\mathbb{S}^{\ast}\models\Diamond a\leq\Diamond(a\wedge\Diamond a)$, i.e.
$\mathbb{S}\models\mathrm{(CT)}$. This observation generalizes [3, Observation
15].

######  Proposition 5.3.

For any proto-precontact algebra $\mathbb{C}=(A,\mathcal{C})$,

  1. 1.

if $\mathbb{C}$ is antitone, then

    1. (i)