11institutetext: School of Mathematics, University of the Witwatersrand,
Johannesburg 22institutetext: Vrije Universiteit, Amsterdam, The Netherlands
33institutetext: Department of Mathematics and Applied Mathematics, University
of Johannesburg, South Africa 44institutetext: KPMG, Amstelveen, The
Netherlands 55institutetext: National Institute for Theoretical and
Computational Sciences (NITheCS), South Africa

# Modal reduction principles: a parametric shift to graphs

Willem Conradie 1155 0000-0001-9906-4132 Krishna Manoorkar 2244
0000-0003-3664-7757 Alessandra Palmigiano 2233 0000-0001-9656-7527 Mattia
Panettiere 2244 0000-0002-9218-5449

###### Abstract

Graph-based frames have been introduced as a logical framework which
internalizes an inherent boundary to knowability (referred to as
‘informational entropy’), due, e.g., to perceptual, evidential or linguistic
limits. They also support the interpretation of lattice-based (modal) logics
as hyper-constructive logics of evidential reasoning. Conceptually, the
present paper proposes graph-based frames as a formal framework suitable for
generalizing Pawlak’s rough set theory to a setting in which inherent limits
to knowability exist and need to be considered. Technically, the present paper
establishes systematic connections between the first-order correspondents of
Sahlqvist modal reduction principles on Kripke frames, and on the more general
relational environments of graph-based and polarity-based frames. This work is
part of a research line aiming at: (a) comparing and inter-relating the
various (first-order) conditions corresponding to a given (modal) axiom in
different relational semantics; (b) recognizing when first-order sentences in
the frame-correspondence languages of different relational structures encode
the same “modal content”; (c) meaningfully transferring relational properties
across different semantic contexts. The present paper develops these results
for the graph-based semantics, polarity-based semantics, and all Sahlqvist
modal reduction principles.

As an application, we study well known modal axioms in rough set theory (such
as those corresponding to seriality, reflexivity, and transitivity) on graph-
based frames and show that, although these axioms correspond to different
first-order conditions on graph-based frames, their intuitive meaning is
retained. This allows us to introduce the notion of hyperconstructivist
approximation spaces as the subclass of graph-based frames defined by the
first-order conditions corresponding to the same modal axioms defining
classical generalized approximation spaces, and to transfer the properties and
the intuitive understanding of different approximation spaces to the more
general framework of graph-based frames. The approach presented in this paper
provides a base for systematically comparing and connecting various formal
frameworks in rough set theory, and for the transfer of insights across
different frameworks.

###### Keywords:

Graph-based frames Rough set theory Modal logic Modal reduction principles
Correspondence theory

##  1 Introduction

##### Generalizations of Rough Set Theory.

The contributions of the present paper lie within, and are motivated by,
several research lines in Rough Set Theory [60, 61, 58] aimed at generalizing
Pawlak’s original setting both for extending its scope, and for making the
theory more modular and systematic. Instrumental to these generalizations were
several cross-fertilizations with other research lines such as (two-valued [8]
and many-valued [39, 40, 9, 46]) modal logic, and Formal Concept Analysis
[42]. Since Orlowska’s work identifying the modal logic S5 as the logic of
information spaces [57], and building on the insight that formalizing the
indiscernibility relation as an equivalence relation might be too restrictive
[90, 66], Vakarelov [75, 74] introduces a framework in which lower and upper
approximations are associated with different indiscernibility relations; Yao
and Lin [89] account systematically for various notions of generalized
approximation spaces, each defined in terms of certain first-order properties
(e.g. reflexivity, symmetry, transitivity, seriality, Euclideanness)
corresponding (via the well known Sahlqvist theory in modal logic [70, 77]) to
various well known modal axioms (which are, more specifically, modal reduction
principles [76], cf. Definition 2.5); moreover, in the same paper, this
approach is systematically extended to the setting of graded and probabilistic
approximation spaces, via graded [38] and probabilistic modal logic [37];
using duality-theoretic and correspondence-theoretic techniques, Balbiani and
Vakarelov [1] introduce a sound and complete decidable poly-modal logic of
weak and strong indiscernibility and complementarity for information systems.
Also building on insights and results stemming from duality and representation
theory for modal logic, Banerjee and Chakraborty [2, 4, 3] study the
mathematical framework of rough set theory from a more abstract viewpoint
grounded on the notion of rough algebras, i.e. modal algebras the non-modal
reducts of which are more general than Boolean algebras, and hence allow
access to a base logic which, being paraconsistent, is strictly more general
than classical propositional logic. Based on this algebraic perspective,
proof-theoretic frameworks have also been developed for the logics of rough
algebras [68, 69, 54, 48, 47, 6, 7].

##### Unifying RST and FCA.

Closely related to these developments are proposals of unifying frameworks for
rough set theory and formal concept analysis [50, 82, 87, 11, 88, 84, 41, 85],
both in the two-valued and in the many-valued setting. This unification is
particularly sought after for modelling classification problems characterized
by partial or incomplete information.

Drawing on insights developed in the research lines discussed above, in [21],
a framework unifying rough set theory and formal concept analysis is proposed,
based on duality-theoretic and algebraic insights stemming from the
mathematical theory of modal logic [24, 23, 29]. The main tool exploited in
[21] is an embedding, defined as in [56], from the class of sets to the class
of formal contexts (cf. [21, Definition 3.3]) which preserves the Boolean
(powerset) algebra associated with each set, in the sense that the concept
lattice of any formal context in the image of the embedding is order-
isomorphic to the powerset algebra of its pre-image (cf. [21, Proposition
3.4]). This embedding can be extended (cf. [21, Proposition 3.7]) to a
complex-algebra-preserving embedding from the class of Kripke frames to the
class of enriched formal contexts, or polarity-based frames.111A polarity (or
formal context) is a triple $\mathbb{P}=(A,X,I)$ where $A$ and $X$ are two
sets, and $I\subseteq A\times X$. For the modal signature
$\tau=\\{\Box,\Diamond\\}$, a polarity-based frame is a structure
$\mathbb{F}=(\mathbb{P},R_{\Box},R_{\Diamond})$, where $\mathbb{P}$ is
polarity, and $R_{\Box}\subseteq A\times I,R_{\Diamond}\subseteq X\times I$
are relations that satisfy certain compatibility conditions (cf. [16,
Definition 2]).  These structures have been defined in [22, 16] in the context
of a research program aimed at developing the logical foundations of
categorization theory, and consist of formal contexts enriched with additional
relations, each defined on the basis of duality-theoretic considerations
(discussed in [28]), and supporting the interpretation of a normal modal
operator. In [21], the study of the preservation properties of the embedding
mentioned above leads to the understanding that a connection can be
established (cf. [21, Sections 3.4 and 4]) between the first-order conditions
on Kripke frames and those on enriched formal contexts corresponding to the
modal axioms considered in the literature in rough set theory for generalizing
approximation spaces.

##### Rough concepts and beyond: towards parametric correspondence.

Besides motivating the identification of conceptual approximation spaces (cf.
[21, Section 5]) as the subclass of enriched formal contexts serving as a
unifying environment for rough set theory and formal concept analysis, these
developments naturally elicit the questions of whether the connection found
and exploited in [21], between the first-order conditions corresponding to a
finite number of well known modal axioms in different semantic settings, can
be systematically extended to significantly large classes of modal axioms, and
also to different semantic settings. Concrete examples pointing to the
existence of such systematic connections cropped up, not only in relation with
the semantics of enriched formal contexts (aka polarity-based frames) for
lattice-based modal logics (sometimes referred to as ‘non-distributive’ modal
logics), but also for an alternative relational semantic setting for the same
logics (namely, graph-based frames), and have been discussed in [16, 19, 21,
22, 78]. In [20], both questions are answered positively: the above-mentioned
connection is generalized from a finite set of modal axioms to the class of
Sahlqvist modal reduction principles [5, 76] (cf. Section 2.5) and is also
extended to two-valued and many-valued Kripke frames, and two-valued and many-
valued enriched formal contexts. These results initiate a line of research
which aims at making correspondence theory not just (methodologically) unified
[23], but also (effectively) parametric [20].

##### Extending parametric correspondence: the case of graph-based frames.

The contributions of the present paper include positive answers to these same
questions for Sahlqvist modal reduction principles, relative to Kripke frames,
graph-based frames, and polarity-based frames, pivoting on graph-based frames.
Graph-based frames [15, 19, 28, 31] (cf. Definition 10) are relational
structures based on graphs $(Z,E)$, where $Z$ is a nonempty set and
$E\subseteq Z\times Z$ is a reflexive relation. Graph-based frames provide
complete semantics to non-distributive modal logic [19], which fact, as also
discussed in [28], supports the interpretation of this logic as the logic of
informational entropy, i.e. an inherent boundary to knowability due e.g. to
perceptual, theoretical, evidential or linguistic limits. In graphs $(Z,E)$ on
which these relational structures are based, the reflexive relation $E$ is
interpreted as the inherent indiscernibility relation induced by informational
entropy, much in the same style as Pawlak’s approximation spaces in rough set
theory. However, $E$ is only required to be reflexive but, in general, neither
transitive nor symmetric, which is in line with proposals in rough set theory
[81, 89, 75], also discussed above, that indiscernibility does not need to be
modelled by equivalence relations. Another key difference is that, rather than
generating modal operators which associate any subset of $Z$ with its
definable $E$-approximations, $E$ generates a complete lattice (i.e. the
lattice of formal $E^{c}$-concepts, as shown in the picture below). Hence, the
role played by $E$ in generating the complex algebras of graph-based frames is
analogous to the role played by the order relation of intuitionistic Kripke
frames in generating the Heyting algebra structure of their associated complex
algebras: both $E$ and the order ultimately support the interpretation of the
propositional (i.e. non-modal) connectives. The resulting propositional
fragment of non-distributive modal logic is sound (and complete) w.r.t.
general lattices, and is hence much weaker than both classical and
intuitionistic logic. Rather than being a flaw, this is a feature of this
framework, which precisely captures and internalizes the correct reasoning
patterns under informational entropy into the propositional fragment of the
language.

$(\varnothing,uvw)$$(w,uv)$$(vw,u)$$V(p)$$(uvw,\varnothing)$$V(p\vee
q)=$$(u,w)$$V(q)$$\leftrightsquigarrow$$Z$$E^{c}$$Z$$u$$v$$w$$u$$v$$w$$\leftrightsquigarrow$$u$$q$$p$$v$$p\vee
q$$p\vee q$$p$$w$$p$$q$$p\vee q$

Figure 1: From left to right, a reflexive graph, its associated formal
context, and its concept lattice. Valuations of atomic propositions and
formulas to elements of the concept lattice dually correspond to
satisfaction/refutation relations between states of the graph and formulas. In
the picture, formulas above (resp. below) a state of the reflexive graph are
satisfied (resp. refuted) at that state.

##### Inherent vs. epistemic indiscernibility.

The environment of graph-based frames makes it possible to differentiate
between inherent indiscernibility (modelled by $E$) and other (possibly more
contingent, e.g. subjective, or epistemic) types of indiscernibility (modelled
by the additional relations which support the interpretation of the modal
operators). The conceptual difference between inherent and other types of
indiscernibility is reflected into the different roles taken by these
relations w.r.t. the interpretation of the logical language: the elements of
the concept lattice represented on the right-hand side of the picture do not
represent definable approximations of predicates, but rather, they represent
‘all there is to know’ about predicates, i.e. the theoretical horizon to
knowability, given the inherent boundary encoded into $E$. In their turn, the
elements of the concept lattices are approximated by the modal operators
induced by the additional relations of the graph-based relational structures,
and this approximation reflects the epistemic (subjective) indiscernibility of
agents.

##### Methodology for the shift from Kripke frames to graph-based frames.

The relation $E$ is intended as the generalization of the identity relation
$\Delta$ on sets, and the embedding from sets to reflexive graphs
corresponding to this generalization, which is defined by the assignment
$S\mapsto(S,\Delta_{S})$, plays the same role in the present context as the
role played by the embedding from sets to formal contexts discussed above, and
displays properties analogous to those of that embedding (namely, it can be
extended to a complex algebra-preserving embedding from Kripke frames to
graph-based frames). Thus, conceptually, the environment of classical Kripke
frames can be understood as the limit case of the present environment in which
any two states are inherently indistinguishable only if they are identical.

##### Graph-based frames and non-distributive logics as hyper-constructivist
logics.

In [28], it is argued that graph-based frames support a view of non-
distributive (modal) logics as hyper-constructivist logics, i.e. logics in
which the principle of excluded middle fails at the meta-linguistic level.
Indeed, as illustrated by the picture above in the case of the proposition
variable $q$, the satisfaction and refutation set of a formula $\varphi$ on
graph-based models are not necessarily set-theoretic complements of one other;
therefore, it is possible for a formula to be neither satisfied nor refuted at
a state. The progressive generalizations, from classical propositional logic
to intuitionistic logic, and from intuitionistic logic to the propositional
fragment of non-distributive (modal) logic (hereafter: non-distributive logic)
is reflected in two ways: concerning relational models, the move from
classical to intuitionistic logic is captured as the move from sets to
preorders (i.e. sets equipped with reflexive and transitive relations), and
the move from intuitionistic to non-distributive logic is captured as the move
from preorders to reflexive graphs (i.e. transitivity is dropped); concerning
the notion of truth, classical truth is replaced in intuitionistic logic with
a finer-grained notion of provable truth, which makes the law of excluded
middle fail at the level of the logical language, since at a given state there
might be neither a proof of $\varphi$ nor a proof of $\neg\varphi$; however,
at the metalogical level of satisfaction and refutation, if a formula is not
satisfied at a given state of an intuitionistic model, then it is refuted at
that state.

##### Hyper-constructivist logics and evidential truth.

As discussed in [28], the failure of the law of excluded middle at the
metalogical level supported by the graph-based semantics suggests that the
notion of truth supported by non-distributive (modal) logics is even more
refined than intuitionistic truth, and can be intuitively construed as an
evidence-based truth: that is, to refute a formula at a given state, the lack
of positive evidence is not enough, but rather, there needs to be evidence
against.

##### Many-valued graph-based frames.

In [18], the many-valued version is introduced of the graph-based semantics of
[19] for two axiomatic extensions of the basic normal non-distributive modal
logic, and in particular their potential is explored for modelling situations
in which informational entropy derives from the theoretical frameworks under
which empirical studies are conducted. This has been proposed as a suitable
framework for modelling competing theories in the empirical sciences. In a
similar vein, in [27], the many-valued graph-based semantic setting for non-
distributive modal logics has been further extended to a multi-type setting,
and has been proposed as a suitable formal framework for modelling socio-
political competition.

For the readers’ convenience, the relevant developments in graph-based and
polarity-based semantics for modal logic and of their applications are
summarised in Table 1.

.  Date Development Reference 2015 Graph-based semantics for (non-
distributive) modal logics [15] 2016 Introduction of enriched RS-polarities as
semantic framework for an epistemic logic of categories and (formal) concepts.
[22] 2017 Approach in [22] generalized to arbitrary (hence not necessarily RS)
polarities, adding a ‘common knowledge’-type construction and formalizing key
concepts in categorization theory. [16] 2019 Complete axiomatization of modal
logic of graph-based frames. Examples of correspondents of some well-known
MRPs on graph-based frames; suggestive similarities noted, but no systematic
theory of connection with classical Kripke frames. Introduction of the notion
of parameterized composition ($E$-composition) in the context of graph-based
frames. Interpretation of graph-based models for reasoning about informational
entropy. [19] 2019 General correspondence theory for the class of logics
algebraically captured by varieties of normal lattice expansions(LE-logics),
with graph-based semantics as a particular example of associated relational
semantics. Correspondents as pure quasi-inequalities to with standard
translations can be applied. No general theory establishing systematic
connections between first-order correspondents of the same modal axioms across
relational semantics, yet. [17] 2020 Systematic study of interconnections
between polarity-based and graph based-semantics. Methodology for extending
both to accommodate arbitrary additional, normal connectives. Study of
possible interpretations of these semantic structures and arguable
preservation of intuition/meaning of well-know epistemic axioms across these
semantics and interpretations. [28] 2021 Novel unification of Rough Set Theory
and Formal Concept Analysis generalizing Pawlak’s original approximation with
polarity-based frames. [21] 2021 Many-valued graph-based semantics extended to
a multi-type setting; proposed as formal framework for modelling socio-
political competition. [26] 2022 Introduction of many-valued graph-based
frames and models and application to reasoning about competing theories. [18]
2022 General theorems expressing the first-order frame correspondents of all
Sahlqvist MRPs as inclusions of (parameterized) relational compositions, both
over Kripke frames and polarity based frames in both crisp and many-valued
cases together with systematic, effective, parametric translations between all
of these. (The present paper does the same but for graph-based frames rather
than polarity-based frames.) [20]

Table 1:  Summary of relevant related work on graph and and polarity based
semantics.

##### Main contributions.

Besides extending the network of systematic connections, established in [20],
among various relational semantics for modal logic so as to include graph-
based frames, the results of the present paper, which we summarise in Table 2,
lay the foundations of a systematic generalization of Rough Set Theory to
settings which require forms of reasoning whose associated notion of truth is
evidence-based in the sense indicated above. Mathematically, these settings
can be formalized by environments whose naturally associated logics are hyper-
constructive.

##### Comparison with results on polarity-based frames.

As observed in [28], although the polarity-based semantics and the graph-based
semantics arise from the same duality-based methodology and they both provide
complete semantics to non-distributive (modal) logics, they support very
different interpretations of what these logics are about, and the first-order
languages canonically associated with these two classes of relational
structures are also very different. This difference can be appreciated e.g.
when comparing the first-order correspondents on polarity-based frames and on
graph-based frames of a simple and well known Sahlqvist modal reduction
principle, as reported in the following table.222In any frame based on a
polarity $(A,X,I)$, variables $x,y,z,\ldots$ range over $X$, and variables
$a,b,c,\ldots$ range over $A$.

Axiom | Correspondents |
---|---|---
| Kripke frames: | $\forall x\forall y\forall z\>((xRy\ \&\ yRz)\Rightarrow xRz)$
$\Box p\vdash\Box\Box p$ | Polarity-based frames: | $\forall a\forall x(aIx\Rightarrow\forall y(\forall b(bR_{\Box}x\Rightarrow bIy)\Rightarrow aIy))$
| Graph-based frames: | $\forall z_{1}\forall z_{2}\forall z_{3}((\forall z_{4}(z_{3}Ez_{4}\Rightarrow z_{4}R_{\Box}z_{1})\ \&\ z_{2}R_{\Box}z_{3})\Rightarrow z_{2}R_{\Box}z_{1})$

In order to be able to systematically connect the first-order correspondents
of any Sahlqvist modal reduction principle across these relational semantics,
we need to establish a common ground between their associated first-order
languages. Establishing this common ground is precisely what the core
technical contribution of the present paper is about. Although, as indicated
earlier, the methodology followed in the present paper is analogous to the one
adopted in [20], transferring it to graph-based frames requires specific
steps, which are presented in Sections 5 and 6.

Hyper-constructivist approximation spaces |  Introduction of hyper-constructivist approximation spaces (see Definition 13), i.e., approximation spaces based on graph based frames, where the law of excluded middle fails at the frame level.
---|---
$E$-mediated and non $E$-mediated compositions |  Introduction and study of the fundamental properties of three notions of relational compositions (cf. Definition 14) which reflect the semantics of the compositions of connectives in graph-based frames (see Lemma 8), and which coincide with the usual composition of relations in the special case in which a graph-based frame is a Kripke frame (see Lemma 7).
Relational languages $\mathsf{GRel}_{\mathcal{L}}$ and $\mathsf{KRel}_{\mathcal{L}}$ |  Introduction of suitable relational languages for Kripke frames and graph-based frames, which serve as the natural environment for the bridge between the first-order correspondents of modal reduction principles in the two semantics. Indeed, we show that such first-order correspondents can always be written as ‘inclusions of relations’, i.e. term inequalities in these relational languages (see Lemmas 10 and 11, and the discussions following the lemmas). These definitions hinge on the notions of composition discussed above.
Shifting of term inequalities in $\mathsf{KRel}_{\mathcal{L}}$ |  Introduction of the notion of shifting between $\mathsf{KRel}_{\mathcal{L}}$-inequalities and $\mathsf{GRel}_{\mathcal{L}}$-inequalities (cf. Definition 19). This notion is exemplified in Table 3 for the best known mrps considered in Rough Set Theory.
Parametric correspondence across Kripke frames and graph-based frames |  Systematic connection between the correspondents of Sahlqvist mrps in Kripke frames and graph-based frames formulated and established in terms of the notion of shifting (see Theorem 6.1).
Lifting of term inequalities in $\mathsf{GRel}_{\mathcal{L}}$ |  Introduction of the notion of lifting of $\mathsf{GRel}_{\mathcal{L}}$-inequalities to $\mathsf{PRel}_{\mathcal{L}}$-inequalities (cf. Definition 20), a relational language for polarity-based frames.
Parametric correspondence across graph-based and polarity-based frames |  Systematic connection between the correspondents of Sahlqvist mrps in graph-based frames and polarity-based frames formulated and established in terms of the notion of lifting (see Theorem 6.2). This extends the results in [20].
Table 2: Main contributions of the present paper

##### Structure of the paper.

In Section 2, after introducing notation used throughout the paper (cf.
Section 2.1), we collect preliminaries on the various (set-based and
algebraic) generalizations of Rough Set Theory (cf. Sections 2.2 and 2.3), on
graph-based frames as semantic structures for general lattice-based modal
logic (cf. Section 2.4), and on modal reduction principles (cf. Section 2.5).
In Section 3, we discuss two case studies in which informational entropy plays
a relevant role and is accounted for in the setting of graph-based frames; in
Section 4, we introduce the notion of hyperconstructivist approximation spaces
and discuss the methodology underlying this definition as an instance of the
general transfer results presented in the following sections. In Section 5, we
introduce and study the properties of several notions of compositions of
relations in the settings of Kripke frames and of graph-based frames. Thanks
to these definitions, suitable propositional languages
$\mathsf{GRel}_{\mathcal{L}}$ and $\mathsf{KRel}_{\mathcal{L}}$ can be
introduced (cf. Section 5.2) in which first-order conditions on Kripke frames
and on polarity-based frames can be represented. In Section 6, we show that
the correspondents of all Sahlqvist modal reduction principles on Kripke
frames and on graph-based frames can be represented as term-inequalities of
the languages $\mathsf{GRel}_{\mathcal{L}}$ and $\mathsf{KRel}_{\mathcal{L}}$.
Represented in this way, a systematic connection can be established between
them (cf. Section 6.3), and with polarity-based frames (cf. Section 6.4). In
Section 7, we apply the main result of the previous section to describe the
relationship between the first-order correspondents of well known modal axioms
in Rough Set Theory in graph-based frames and in Kripke frames. We show that,
based on this mathematical relationship, also the intuitive meaning of these
axioms can be systematically transferred across these different semantics.
Finally, we conclude in Section 8.

##  2 Preliminaries

The present section collects basic definitions and facts about the various
intersecting topics and results on which the contributions of the present
paper build. In Section 2.1, we introduce the notation used throughout the
paper. In Section 2.2, we collect the basic definitions on approximation
spaces and their modal logic. In Section 2.3, we review the literature on
various algebraic approaches to rough set theory. In Section 2.4, we collect
basic definitions and facts on non-distributive modal logics and their graph-
based frames. In Section 2.5, we collect preliminaries on inductive modal
reduction principles and discuss a general and compact representation of their
associated output when running the algorithm ALBA [17] on them.

###  2.1 Notational conventions and basic constructions

We let $\Delta_{U}$ denote the identity relation on a set $U$, and we will
drop the subscript when it causes no ambiguity. The superscript $(\cdot)^{c}$
denotes the relative complement of a subset of a given set. Hence, for any
binary relation $R\subseteq U\times V$, we let $R^{c}\subseteq U\times V$ be
defined by $(u,v)\in R^{c}$ iff $(u,v)\notin R$. For any such $R$ and any
$U^{\prime}\subseteq U$ and $V^{\prime}\subseteq V$, we let
$R[U^{\prime}]:=\\{v\in V\mid(u,v)\in R\mbox{ for some }u\in U^{\prime}\\}$
and $R^{-1}[V^{\prime}]:=\\{u\in U\mid(u,v)\in R\mbox{ for some }v\in
V^{\prime}\\}$, and write $R[u]$ and $R^{-1}[v]$ for $R[\\{u\\}]$ and
$R^{-1}[\\{v\\}]$, respectively. Any such $R$ gives rise to the semantic modal
operators $\langle R\rangle,[R]:\mathcal{P}(V)\to\mathcal{P}(U)$ s.t. $\langle
R\rangle W:=R^{-1}[W]$ and $[R]W:=(R^{-1}[W^{c}])^{c}$ for any $W\subseteq V$.
For any $T\subseteq U\times V$, and any $U^{\prime}\subseteq U$ and
$V^{\prime}\subseteq V$, let

$\small\begin{array}[]{ll}T^{(1)}[U^{\prime}]:=\\{v\mid\forall u(u\in
U^{\prime}\Rightarrow uTv)\\}&T^{(0)}[V^{\prime}]:=\\{u\mid\forall v(v\in
V^{\prime}\Rightarrow uTv)\\}\\\ T^{[1]}[U^{\prime}]:=\\{v\mid\forall u(u\in
U^{\prime}\Rightarrow uT^{c}v)\\}&T^{[0]}[V^{\prime}]:=\\{u\mid\forall v(v\in
V^{\prime}\Rightarrow uT^{c}v)\\}\end{array}$ (1)

Well known properties of these constructions (cf. [[34], Sections 7.22-7.29])
are stated in the following lemma.

###### Lemma 1

For any relation $T\subseteq U\times V$, and all $V^{\prime}\subseteq V$,
$U^{\prime}\subseteq U$, $\mathcal{U}\subseteq\mathcal{P}(U)$, and
$\mathcal{V}\subseteq\mathcal{P}(V)$,

  1. 1.

$X_{1}\subseteq X_{2}\subseteq U$ implies $T^{(1)}[X_{2}]\subseteq
T^{(1)}[X_{1}]$, and $Y_{1}\subseteq Y_{2}\subseteq V$ implies
$T^{(0)}[Y_{2}]\subseteq T^{(0)}[Y_{1}]$.

  2. 2.

$U^{\prime}\subseteq T^{(0)}[V^{\prime}]$ iff $V^{\prime}\subseteq
T^{(1)}[U^{\prime}]$.

  3. 3.

$U^{\prime}\subseteq T^{(0)}[T^{(1)}[U^{\prime}]]$ and $V^{\prime}\subseteq
T^{(1)}[T^{(0)}[V^{\prime}]]$.

  4. 4.

$T^{(1)}[U^{\prime}]=T^{(1)}[T^{(0)}[T^{(1)}[U^{\prime}]]]$ and
$T^{(0)}[V^{\prime}]=T^{(0)}[T^{(1)}[T^{(0)}[V^{\prime}]]]$.

  5. 5.

$T^{(0)}[\bigcup\mathcal{V}]=\bigcap_{V^{\prime}\in\mathcal{V}}T^{(0)}[V^{\prime}]$
and
$T^{(1)}[\bigcup\mathcal{U}]=\bigcap_{U^{\prime}\in\mathcal{U}}T^{(1)}[U^{\prime}]$.

All properties listed in Lemma 1 hold with $(\cdot)^{[0]}$ and $(\cdot)^{[1]}$
replacing $(\cdot)^{(0)}$ and $(\cdot)^{(1)}$ respectively, by instantiating
$T:=T^{c}$, so we will refer to this lemma also when invoking these
properties.

######  Lemma 2 ([20], Lemma 3.10)

For any relation $T\subseteq U\times V$, and any $W\subseteq V$,

$T^{[0]}[W^{c}]=(T^{-1}[W^{c}])^{c}=[T]W$ and
$(T^{[0]}[W])^{c}=T^{-1}[W]=\langle T\rangle W$.

###  2.2 Approximation spaces and their modal logic

Approximation spaces have been introduced by Pawlak [59] as the basic formal
environment for Rough Set Theory. These are structures $\mathbb{X}=(S,R)$ such
that $S$ is a nonempty set, and $R\subseteq S\times S$ is an equivalence
relation. For any such $\mathbb{X}$ and any $Z\subseteq S$, the upper and
lower approximations of $Z$ are respectively defined as follows:

$\overline{Z}:=\bigcup\\{R[z]\mid z\in Z\\}\quad\mbox{ and
}\quad\underline{Z}:=\bigcup\\{R[z]\mid z\in Z\mbox{ and }R[z]\subseteq Z\\}.$

A rough set of $\mathbb{X}$ is a pair $(\underline{Z},\overline{Z})$ for any
$Z\subseteq S$ (cf. [4]). Since $R$ is an equivalence relation,

$\overline{Z}=\langle R\rangle Z\quad\mbox{ and }\quad\underline{Z}=[R]Z,$

with $\langle R\rangle$ and $[R]$ validating the axioms of the classical
normal modal logic S5 (cf. [57]).

As approximation spaces are exactly the Kripke frames for the normal modal
logic S5 [57], this logic completely axiomatizes Pawlak’s rough set theory.
Given a language for classical modal logic over a set $\mathsf{Prop}$ of
proposition variables and a valuation $V:\mathsf{Prop}\to\mathcal{P}(S)$ on
$\mathbb{X}$, the satisfiability on models $M=(\mathbb{X},V)$ is defined as
usual in modal logic. The extension $[\\![{\varphi}]\\!]\subseteq S$ of any
formula $\varphi$ is defined recursively as follows:

$M,w\Vdash p$ | iff | $w\in V(p)$ | $[\\![{p}]\\!]=V(p)$
---|---|---|---
$M,w\Vdash\varphi\lor\psi$ | iff |  $w\in[\\![{\varphi}]\\!]$ or $w\in[\\![{\psi}]\\!]$ | $[\\![{\varphi\lor\psi}]\\!]=[\\![{\varphi}]\\!]\cup[\\![{\psi}]\\!]$
$M,w\Vdash\varphi\land\psi$ | iff |  $w\in[\\![{\varphi}]\\!]$ and $w\in[\\![{\psi}]\\!]$ | $[\\![{\varphi\land\psi}]\\!]=[\\![{\varphi}]\\!]\cap[\\![{\psi}]\\!]$
$M,w\Vdash\neg\varphi$ | iff | $w\notin[\\![{\varphi}]\\!]$ | $[\\![{\neg\varphi}]\\!]=[\\![{\varphi}]\\!]^{c}$
$M,w\Vdash\Box\varphi$ | iff |  $wRu$ implies $u\in[\\![{\varphi}]\\!]$ | $[\\![{\Box\varphi}]\\!]=[R][\\![{\varphi}]\\!]$
$M,w\Vdash\Diamond\varphi$ | iff |  $wRu$ for some $u\in[\\![{\varphi}]\\!]$ | $[\\![{\Diamond\varphi}]\\!]=\langle R\rangle[\\![{\varphi}]\\!]$

As is well known [57], the modal logic S5 is the axiomatic extension of the
basic normal modal logic $K$ with the following axioms, respectively
corresponding to the reflexivity, transitivity and symmetry of the
indiscernibility relation $R$.

$\Box\varphi\rightarrow\varphi\quad\quad\Box\varphi\rightarrow\Box\Box\varphi\quad\quad\varphi\rightarrow\Box\Diamond\varphi.$

Motivated by the idea that the indiscernibility relation does not need to be
an equivalence relation, the following definition provides the environment for
a generalized and more modular definition of approximation space.

######  Definition 1 ([86], Section 2)

A generalized approximation space is a tuple $\mathbb{X}=(S,R)$ such that $S$
is a non-empty set, and $R\subseteq S\times S$ is any relation. For any such
$\mathbb{X}$ and any $Z\subseteq S$, the upper and lower approximations of $Z$
are respectively

$\overline{Z}:=\langle R\rangle Z=\bigcup\\{R^{-1}[z]\mid z\in Z\\}\quad\mbox{
and }\quad\underline{Z}:=[R]Z=\\{s\in S\mid R[s]\subseteq Z\\}.$

The following table lists the names of subclasses of generalized approximation
spaces in terms of their defining first-order condition.

Class | first-order condition
---|---
serial | $\forall s\exists t(R(s,t))$
reflexive | $\forall s(R(s,s))$
symmetric | $\forall s\forall t(R(s,t)\Rightarrow R(t,s))$
transitive | $\forall s\forall t(\exists u(R(s,u)\ \&\ R(u,t))\Rightarrow R(s,t))$
Euclidean | $\forall u\forall v\forall w(R(u,v)\ \&\ R(u,w)\Rightarrow R(v,w))$

The following proposition directly derives from well known results in the
Sahlqvist theory of classical normal modal logic, and has made it possible to
completely characterize various subclasses of generalized approximation spaces
in terms of well known modal axioms.

######  Proposition 1 ([86], Section 2)

For any generalized approximation space $\mathbb{X}=(S,R)$,

  1. 1.

$\mathbb{X}\Vdash\Box p\rightarrow\Diamond p\,$ iff $\,\mathbb{X}$ is serial.

  2. 2.

$\mathbb{X}\Vdash\Box p\rightarrow p\,$ iff $\,\mathbb{X}$ is reflexive.

  3. 3.

$\mathbb{X}\Vdash p\rightarrow\Box\Diamond p\,$ iff $\,\mathbb{X}$ is
symmetric.

  4. 4.

$\mathbb{X}\Vdash\Box p\rightarrow\Box\Box p\,$ iff $\,\mathbb{X}$ is
transitive.

  5. 5.

$\mathbb{X}\Vdash\Diamond p\rightarrow\Box\Diamond p\,$ iff $\,\mathbb{X}$ is
Euclidian.

###  2.3 The algebraic approach to Rough Set Theory

Several logical frameworks motivated by Rough Set Theory have been introduced
based on classes of generalized Boolean algebras with operators. Their
associated logics typically have a propositional base that is strictly weaker
than classical propositional logic.

##### Rough algebras and their generalizations.

Chakraborty and Banerjee [4] introduced topological quasi-Boolean algebras
(tqBas) as a generalization of S5 Boolean algebras with operators (BAOs).

######  Definition 2 ([4])

A topological quasi-Boolean algebra (tqBa) is an algebra
$\mathbb{T}=(\mathbb{L},I)$ such that
$\mathbb{L}=(\mathrm{L},\vee,\wedge,\neg,\top,\bot)$ is a De Morgan algebra
and for all $a,b\in\mathbb{L}$,

$T1.\,I(a\wedge b)=Ia\wedge Ib\quad T2.\,IIa=Ia\quad T3.\,Ia\leq a\quad
T4.\,I\top=\top.$

For any $a\in A$, let $Ca:=\neg I\neg a$. Subclasses of tqBas have been
defined as in the following table.

Algebras | Acronyms | Axioms
---|---|---
topological quasi Boolean algebra 5 | tqBa5 | T5: $CIa=Ia$
intermediate algebra of type 1 | IA1 | T5, T6: $Ia\vee\neg Ia=\top$
intermediate algebra of type 2 | IA2 | T5, T7: $I(a\vee b)=Ia\vee Ib$
intermediate algebra of type 3 | IA3 | T5, T8: $Ia\leq Ib$ and $Ca\leq Cb$ imply $a\leq b$
pre-rough algebra | pra | T5, T6, T7, T8.

A rough algebra is a complete and completely distributive pre-rough algebra.
Different sub-classes of tqBas have been studied extensively in the literature
on rough set theory [4, 3]. Notice that the lower and upper approximation
operators $I$ and $C$ are finitely meet-preserving and join-preserving
operators on $\mathbb{L}$ respectively. Thus, these operators can serve as
algebraic interpretations of normal modal operators $\Box$ and $\Diamond$ on
$\mathbb{L}$. Thus, tqBa5s and their sub-classes can be seen as normal modal
expansions of De Morgan algebras.

##### Rough algebras based on distributive lattices.

In [52], Kumar and Banerjee define rough lattices as an algebraic abstraction
of algebras obtained from quasi order-generated covering-based approximation
spaces (QOCAS). These approximation spaces can be seen as the approximation
spaces arising from granules seen as open neighborhoods in a topological
space.

######  Definition 3 ([52], Definition 4.4)

An algebra $\mathbb{L}=(\mathrm{L},\vee,\wedge,I,C,0,1)$ is a rough lattice if
$(\mathrm{L},\vee,\wedge,0,1)$ is a completely distributive lattice join-
generated by its completely join-irreducible elements and
$I,C:\mathrm{L}\to\mathrm{L}$ satisfy the following conditions for all
$a,b\in\mathrm{L}$ and any $A\subseteq\mathrm{L}$:

  1. 1.

$I(\bigwedge A)=\bigwedge\\{I(a)\mid a\in A\\}$ and $C(\bigvee
A)=\bigvee\\{C(a)\mid a\in A\\}$.

  2. 2.

$C(\bigwedge A)=\bigwedge\\{C(a)\mid a\in A\\}$ and $I(\bigvee
A)=\bigvee\\{I(a)\mid a\in A\\}$.

  3. 3.

$Ia\leq a$ and $a\leq Ca$.

  4. 4.

$I1=1$ and $C0=0$.

  5. 5.

$IIa=Ia$ and $CCa=Ca$.

  6. 6.

$ICa=Ca$ and $CIa=Ia$.

  7. 7.

$Ia\leq Ib$ and $Ca\leq Cb$ imply $a\leq b$.

Again, note that, as lower and upper approximation operators are completely
join-preserving and meet-preserving respectively, these algebras are perfect
distributive modal algebras [44], and hence they are naturally endowed with a
(bi)Heyting algebra structure. Kumar [51] also introduced rough Heyting
algebras to describe the interaction between the approximation operators $I$
and $C$ and Heyting implication.

######  Definition 4 ([51], Definition 40)

An algebra $\mathbb{L}=(L,\vee,\wedge,\rightarrow,I,C,0,1)$ is a rough Heyting
algebra iff its $\\{\rightarrow\\}$-free reduct is a rough lattice, its
$\\{I,C\\}$-free reduct is a Heyting algebra, and the following identities are
valid:

  1. 1.

$I(a\rightarrow b)=(Ia\rightarrow Ib)\wedge(Ca\rightarrow Cb)$.

  2. 2.

$C(a\rightarrow b)=Ca\rightarrow Cb$.

##### Rough algebras based on concept lattices.

In [21], several classes of algebras are defined as varieties of modal
expansions of general (i.e. possibly non-distributive) lattices. Since,
following the approach of formal concept analysis [42], general lattices can
be studied as hierarchies of formal concepts arising from relational
databases, the role of modal operators can be seen as approximating categories
or concepts under incomplete or uncertain information [21].

######  Definition 5 (cf. [21], Section 6)

An abstract conceptual rough algebra (resp. conceptual rough algebra) (acra
(resp. cra)) is an algebra $\mathbb{A}=(\mathbb{L},\Box,\Diamond)$ such that
$\mathbb{L}$ is a bounded lattice (resp. complete lattice) and $\Box$ and
$\Diamond$ are unary operations on $\mathbb{L}$ such that $\Diamond$ is
finitely join-preserving (resp. completely join-preserving) and $\Box$ is
finitely meet-preserving (resp. completely meet-preserving), and for any
$a\in\mathbb{L}$,

$\Box a\leq\Diamond a.$

Subclasses of abstract conceptual rough algebras (resp. conceptual rough
algebras) have been considered, which are reported in the following table.

Class | Axioms
---|---
reflexive |  $\Box a\leq a$ and $a\leq\Diamond a$
transitive |  $\Box a\leq\Box\Box a$ and $\Diamond\Diamond a\leq\Diamond a$
symmetric |  $a\leq\Box\Diamond a$ and $\Diamond\Box a\leq a$
dense |  $\Box\Box a\leq\Box a$ and $\Diamond a\leq\Diamond\Diamond a$

In particular, a conceptual tqBa is a reflexive and transitive acra.
Subclasses of tqBas have been defined as reported in the following table.

Class | Axioms
---|---
Conceptual tqBa5 |  $\Diamond\Box a\leq\Box a$ and $\Diamond a\leq\Box\Diamond a$
conceptual IA1 |  $\Box(a\vee b)\leq\Box a\vee\Box b$ and $\Diamond a\wedge\Diamond b\leq\Diamond(a\wedge b)$
conceptual IA2 | $(\Box a\leq\Box b\ \&\ \Diamond a\leq\Diamond b)\Rightarrow a\leq b$

A conceptual pre-rough algebra is a conceptual tqBA5 which is both conceptual
IA1 and IA2.

##### Rough algebras based on posets.

Cattaneo [12] further generalizes rough set theory by defining the notion of
abstract approximation spaces on posets.

######  Definition 6 ([12], Section 1)

An abstract approximation space is a structure
$\mathcal{U}=(\Sigma,\mathbb{O}(\Sigma),\mathbb{C}(\Sigma))$ such that
$(\Sigma,\leq,0,1)$ is a bounded poset, $\mathbb{O}(\Sigma)$ and
$\mathbb{C}(\Sigma)$ are subposets of $\Sigma$ containing $0$ and $1$ such
that inner and outer approximation maps $i:\Sigma\to\mathbb{O}(\Sigma)$ and
$c:\Sigma\to\mathbb{C}(\Sigma)$ exist such that, for any $x\in\Sigma$, any
$\alpha\in\mathbb{O}(\Sigma)$, and any $\gamma\in\mathbb{C}(\Sigma)$,

  1. 1.

$i(x)\leq x$ and $x\leq c(x)$.

  2. 2.

$\alpha\leq x\Rightarrow\alpha\leq i(x)$.

  3. 3.

$x\leq\gamma\Rightarrow c(x)\leq\gamma$.

Algebraic structures arising from rough operators defined on various classes
of lattice-based algebras such as orthomodular lattices [33], quasi-Brouwer-
Zadeh distributive lattices [13], MV-algebras [67], cylindric algebras have
been studied in literature.

##### Fuzzy and probabilistic rough algebras.

Several fuzzy and probabilistic generalizations of rough set theory have been
studied extensively in the literature [83, 53, 36]. Yao [83] introduces a
framework for probabilistic rough set approximations using the notion of rough
membership.

######  Definition 7 ([83], Section 3.1)

A probabilistic approximation space is a structure $\mathbb{X}=(U,E,P)$ such
that $E\subseteq U\times U$ is an equivalence relation and $P:2^{U}\to[0,1]$
is a probability function. The rough membership in any $A\subseteq U$ is given
by the map $\mu_{A}:U\to[0,1]$ defined by the assignment $x\mapsto
P(A\mid[x])$, where $[x]\coloneqq\\{y\in U\mid xEy\\}$.

######  Definition 8 ([83], Section 4.3)

For all parameters $\alpha,\beta\in[0,1]$, and any probabilistic approximation
space $\mathbb{X}=(U,E,P)$, the generalized probabilistic approximation
operators
$\underline{appr_{\alpha}},\overline{appr_{\beta}}:\mathcal{P}(U)\to\mathcal{P}(U)$
are defined as follows. If $0\leq\beta<\alpha\leq 1$, then for any $A\subseteq
U$,

$\underline{appr_{\alpha}}(A)=\\{x\in U\mid
P(A\mid[x])\geq\alpha\\}\quad\text{and}\quad\overline{appr_{\beta}}(A)=\\{x\in
U\mid P(A\mid[x])<\beta\\}.$

If $\alpha=\beta\neq 0$, then

$\underline{appr_{\alpha}}(A)=\\{x\in U\mid
P(A\mid[x])>\alpha\\}\quad\text{and}\quad\overline{appr_{\alpha}}(A)=\\{x\in
U\mid P(A\mid[x])\leq\alpha\\}.$

Given the properties they were shown to satisfy (e.g. monotonicity,
distributivity over union and intersection), the approximation operators
$\underline{appr_{\alpha}}$ and $\overline{appr_{\beta}}$ can be regarded as
paramentric fuzzy regular modal operators $\Box_{\alpha}$ and
$\Diamond_{\beta}$ on the powerset algebra $\mathcal{P}(U)$, respectively.

Using both constructive and algebraic methods, Wu and Zhang [80] introduce a
generalization of rough set theory to a fuzzy framework.

######  Definition 9 ([80], Definition 4)

A generalized fuzzy approximation space is a structure $\mathbb{X}=(W,U,R)$
such that $U$ and $W$ are non-empty finite sets, and $R:U\times W\to[0,1]$ is
a fuzzy relation. For any fuzzy subset $A$ of $W$, the lower and upper
approximations of $A$, $\underline{R}(A)$ and $\overline{R}(A)$, are defined
as follows: For any $x\in U$,

$\overline{R}(A)(x)=\bigvee_{y\in W}(R(x,y)\wedge
A(y))\quad\text{and}\quad\underline{R}(A)(x)=\bigwedge_{y\in W}((1-R(x,y))\vee
A(y)).$

A generalized fuzzy approximation space $\mathbb{X}=(W,U,R)$ with $U=W$ is:

  1. 1.

reflexive if $R(x,x)=1$ for all $x\in U$.

  2. 2.

symmetric if $R(x,y)=R(y,z)$ for all $x,y\in U$.

  3. 3.

transitive if $R(x,z)\geq\bigvee_{y\in U}(R(x,y)\wedge R(y,x))$ for all
$x,z\in U$.

  4. 4.

serial if $\exists y(R(x,y)=1)$ for all $x\in U$.

Let $\mathcal{F}(W)$ denote the set of all fuzzy subsets of $W$. The fuzzy
approximation operators $\underline{R}$ and $\overline{R}$ defined above
satisfy the following properties [80]: for all $A,B\in\mathcal{F}(W)$, and any
$\alpha\in[0,1]$,

1.$\underline{R}(A)=\neg\overline{R}(\neg A)$ |  | 2.$\overline{R}(A)=\neg\underline{R}(\neg A)$
---|---|---
3.$\underline{R}(A\vee\hat{\alpha})=\underline{R}(A)\vee\hat{\alpha}$ |  | 4.$\overline{R}(A\wedge\hat{\alpha})=\overline{R}(A)\wedge\hat{\alpha}$
5.$\underline{R}(A\wedge B)=\underline{R}(A)\wedge\underline{R}(B)$ |  | 6.$\overline{R}(A\vee B)=\overline{R}(A)\vee\overline{R}(B)$,

where $\hat{\alpha}$ is the constant fuzzy set $\hat{\alpha}(x)=\alpha$ for
all $x\in U\cup W$. As lower and upper approximation operators $\underline{R}$
and $\overline{R}$ are completely meet-preserving and join-preserving, these
operators are semantic modal operators $\Box$ and $\Diamond$ on
$\mathcal{F}(W)$.

The following proposition generalizes Proposition 1 to the fuzzy setting. The
inclusion symbol between fuzzy sets in the proposition denotes as usual that
the function on the left-hand side of the inclusion is pointwise dominated by
the one on the right-hand side. We let $A$ denote an element of
$\mathcal{F}(W)$, $x,y$ denote elements of $W$, and $\alpha$ denote a constant
in $[0,1]$. For any $Y\subseteq W$, we let $1_{Y}$ denote the fuzzy set which
assigns membership value $1$ to all the elements of $Y$ and $0$ to all the
elements not in $Y$.

######  Proposition 2 ([80], Section 3.3)

A generalized fuzzy approximation space $\mathbb{X}=(W,W,R)$ is:

  1. 1.

reflexive iff $A\subseteq\overline{R}(A)$ or equivalently iff
$\underline{R}(A)\subseteq A$ for every $A\in\mathcal{F}(W)$.

  2. 2.

symmetric iff for all $x,y\in W$

$\underline{R}(1_{U-\\{x\\}})(y)=\underline{R}(1_{U-\\{y\\}})(x)\text{ or
equivalently iff }\overline{R}(1_{x})(y)=\overline{R}(1_{y})(x).$

  3. 3.

transitive iff $\underline{R}(A)\subseteq\underline{R}(\underline{R}(A))$ or
equivalently iff $\overline{R}(\overline{R}(A))\subseteq\overline{R}(A)$ for
every $A\in\mathcal{F}(W)$.

  4. 4.

serial iff $\underline{R}(\varnothing)=\varnothing$ iff $\overline{R}(W)=W$
iff $\forall\alpha(\overline{R}(\hat{\alpha})=\hat{\alpha})$ iff
$\forall\alpha(\underline{R}(\hat{\alpha})=\hat{\alpha})$ iff $\forall
A(\underline{R}(A)\subseteq\overline{R}(A))$.

Several types of many-valued algebras generalizing the interval $[0,1]$ have
been studied in the literature as an environment for fuzzy rough set theory
[80, 21, 72, 64, 14].

###  2.4 Basic normal non-distributive modal logic and its graph-based
semantics

The present section collects basic definitions and facts from [43, 17, 28].
Let $\mathsf{Prop}$ be a (countable or finite) set of atomic propositions. The
language $\mathcal{L}$ of the basic normal non-distributive modal logic is
defined as follows:

$\varphi:=\bot\mid\top\mid
p\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\Box\varphi\mid\Diamond\varphi$,

where $p\in\mathsf{Prop}$. The basic, or minimal normal $\mathcal{L}$-logic is
a set $\mathbf{L}$ of sequents $\varphi\vdash\psi$ with
$\varphi,\psi\in\mathcal{L}$, containing the following axioms:

$p\vdash p$ |  | $\bot\vdash p$ |  | $p\vdash p\vee q$ |  | $p\wedge q\vdash p$ |  | $\top\vdash\Box\top$ |  | $\Box p\wedge\Box q\vdash\Box(p\wedge q)$
---|---|---|---|---|---|---|---|---|---|---
|  | $p\vdash\top$ |  | $q\vdash p\vee q$ |  | $p\wedge q\vdash q$ |  | $\Diamond\bot\vdash\bot$ |  | $\Diamond(p\vee q)\vdash\Diamond p\vee\Diamond q$

and closed under the following inference rules:

$\frac{\varphi\vdash\chi\quad\chi\vdash\psi}{\varphi\vdash\psi}\quad\frac{\varphi\vdash\psi}{\varphi\left(\chi/p\right)\vdash\psi\left(\chi/p\right)}\quad\frac{\chi\vdash\varphi\quad\chi\vdash\psi}{\chi\vdash\varphi\wedge\psi}\quad\frac{\varphi\vdash\chi\quad\psi\vdash\chi}{\varphi\vee\psi\vdash\chi}\quad\frac{\varphi\vdash\psi}{\Box\varphi\vdash\Box\psi}\quad\frac{\varphi\vdash\psi}{\Diamond\varphi\vdash\Diamond\psi}$

By an $\mathcal{L}$-logic we understand any extension of $\mathbf{L}$ with
$\mathcal{L}$-axioms $\varphi\vdash\psi$.

Graph-based models for non-distributive logics arise in close connection with
the topological structures dual to general lattices in Ploščica’s
representation [62] (see also [32, 31]).

A reflexive graph is a structure $\mathbb{G}=(Z,E)$ such that $Z$ is a
nonempty set, and $E\subseteq Z\times Z$ is a reflexive relation.333In the
context of the generalization of rough set theory pursued in the present paper
(cf. Section 4), the intuitive reading of $zEz^{\prime}$ is ‘$z$ is inherently
indiscernible from $z^{\prime}$’ for all $z,z^{\prime}\in Z$. We let
$D\subseteq Z\times Z$ be defined as $xDa$ iff $aEx$. For every set $S$, we
let $\mathbb{G}_{S}=(S,\Delta)$. From now on, we assume that all graphs we
consider are reflexive even when we drop the adjective. Any graph
$\mathbb{G}=(Z,E)$ defines the polarity444 A formal context [42], or polarity,
is a structure $\mathbb{P}=(A,X,I)$ such that $A$ and $X$ are sets, and
$I\subseteq A\times X$ is a binary relation. Every such $\mathbb{P}$ induces
maps $(\cdot)^{\uparrow}:\mathcal{P}(A)\to\mathcal{P}(X)$ and
$(\cdot)^{\downarrow}:\mathcal{P}(X)\to\mathcal{P}(A)$, respectively defined
by the assignments $B^{\uparrow}:=I^{(1)}[B]$ and
$Y^{\downarrow}:=I^{(0)}[Y]$. A formal concept of $\mathbb{P}$ is a pair
$c=(B,Y)$ such that $B\subseteq A$, $Y\subseteq X$, and $B^{\uparrow}=Y$ and
$Y^{\downarrow}=B$. Given a formal concept $c=(B,Y)$ we often write
$[\\![{c}]\\!]$ for $B$ and $(\\![{c}]\\!)$ for $Y$ and, consequently,
$c=([\\![{c}]\\!],(\\![{c}]\\!))$. The set $L(\mathbb{P})$ of the formal
concepts of $\mathbb{P}$ can be partially ordered as follows: for any $c,d\in
L(\mathbb{P})$,  $c\leq d\quad\mbox{ iff
}\quad[\\![{c}]\\!]\subseteq[\\![{d}]\\!]\quad\mbox{ iff
}\quad(\\![{d}]\\!)\subseteq(\\![{c}]\\!).$ With this order, $L(\mathbb{P})$
is a complete lattice, the concept lattice $\mathbb{P}^{+}$ of $\mathbb{P}$.
Any complete lattice $\mathbb{L}$ is isomorphic to the concept lattice
$\mathbb{P}^{+}$ of some polarity $\mathbb{P}$.
$\mathbb{P_{G}}=(Z_{A},Z_{X},I_{E^{c}})$ where $Z_{A}=Z=Z_{X}$ and
$I_{E^{c}}\subseteq Z_{A}\times Z_{X}$ is defined as $aI_{E^{c}}x$ iff
$aE^{c}x$. More generally, any relation $R\subseteq Z\times Z$ ‘lifts’ to
relations $I_{R^{c}}\subseteq Z_{A}\times Z_{X}$ and $J_{R^{c}}\subseteq
Z_{X}\times Z_{A}$ defined as $aI_{R^{c}}x$ iff $aR^{c}x$ and $xJ_{R^{c}}a$
iff $xR^{c}a$. In what follows, for any $W\subseteq Z$, we will write
$(W)_{A}\subseteq Z_{A}$ and $(W)_{X}\subseteq Z_{X}$ as its corresponding
‘lifted’ copies. The next lemma follows directly from the definitions above:

###### Lemma 3

For any relation $R\subseteq Z\times Z$ and any $Y,B\subseteq Z$,

$I^{(0)}_{R^{c}}[Y]=(R^{[0]}[Y])_{A}\quad
I^{(1)}_{R^{c}}[B]=(R^{[1]}[B])_{X}\quad
J^{(0)}_{R^{c}}[B]=(R^{[0]}[B])_{X}\quad J^{(1)}_{R^{c}}[Y]=(R^{[1]}[Y])_{A}.$

The complete lattice $\mathbb{G}^{+}$ associated with a graph $\mathbb{G}$ is
the concept lattice of $\mathbb{P_{G}}$. By specializing [28, Proposition 3.1]
to $\mathbb{P_{G}}$ we get the following.

###### Proposition 3

For every graph $\mathbb{G}=(Z,E)$, the lattice $\mathbb{G}^{+}$ is completely
join-generated by the set $\\{\mathbf{z}_{A}=(z^{[10]},z^{[1]})\mid z\in Z\\}$
and completely meet-generated by the set
$\\{\mathbf{z}_{X}=(z^{[0]},z^{[01]})\mid z\in Z\\}$.

###### Definition 10

A graph-based $\mathcal{L}$-frame is a structure
$\mathbb{F}=(\mathbb{G},R_{\Diamond},R_{\Box})$ where $\mathbb{G}=(Z,E)$ is a
reflexive graph,555 Applying notation (1) to a graph-based $\mathcal{L}$-frame
$\mathbb{F}$, we sometimes abbreviate $E^{[0]}[Y]$ and $E^{[1]}[B]$ as
$Y^{[0]}$ and $B^{[1]}$, respectively, for all $Y,B\subseteq Z$. If
$Y=\\{y\\}$ and $B=\\{b\\}$, we write $y^{[0]}$ and $b^{[1]}$ for
$\\{y\\}^{[0]}$ and $\\{b\\}^{[1]}$, and write $Y^{[01]}$ and $B^{[10]}$ for
$(Y^{[0]})^{[1]}$ and $(B^{[1]})^{[0]}$, respectively. Lemma 3 implies that
$Y^{[0]}=I_{E^{c}}^{(0)}[Y]=Y^{\downarrow}$ and
$B^{[1]}=I_{E^{c}}^{(1)}[B]=B^{\uparrow}$, where $(\cdot)^{\downarrow}$ and
$(\cdot)^{\uparrow}$ are the maps associated with $\mathbb{P_{G}}$. and
$R_{\Diamond}$ and $R_{\Box}$ are binary relations on $Z$ satisfying the
following $E$-compatibility conditions (notation defined in (1)): for all
$b,y\in Z$,

$\displaystyle(R_{\Box}^{[0]}[y])^{[10]}$ $\displaystyle\subseteq
R_{\Box}^{[0]}[y]\qquad$ $\displaystyle(R_{\Box}^{[1]}[b])^{[01]}\subseteq
R_{\Box}^{[1]}[b]$ $\displaystyle(R_{\Diamond}^{[0]}[b])^{[01]}$
$\displaystyle\subseteq R_{\Diamond}^{[0]}[b]\qquad$
$\displaystyle(R_{\Diamond}^{[1]}[y])^{[10]}\subseteq R_{\Diamond}^{[1]}[y].$

The complex algebra of a graph-based $\mathcal{L}$-frame
$\mathbb{F}=(\mathbb{G},R_{\Diamond},R_{\Box})$ is the complete
$\mathcal{L}$-algebra $\mathbb{F}^{+}=(\mathbb{G}^{+},[R_{\Box}],\langle
R_{\Diamond}\rangle),$ where $\mathbb{G}^{+}$ is the concept lattice of
$\mathbb{P}_{\mathbb{G}}$, and $[R_{\Box}]$ and $\langle R_{\Diamond}\rangle$
are unary operations on $\mathbb{P}_{\mathbb{G}}^{+}$ defined as follows: for
every $c=([\\![{c}]\\!],(\\![{c}]\\!))\in\mathbb{P}_{\mathbb{G}}^{+}$,

$[R_{\Box}]c:=(R_{\Box}^{[0]}[(\\![{c}]\\!)],(R_{\Box}^{[0]}[(\\![{c}]\\!)])^{[1]})\quad\mbox{
and }\quad\langle R_{\Diamond}\rangle
c:=((R_{\Diamond}^{[0]}[[\\![{c}]\\!]])^{[0]},R_{\Diamond}^{[0]}[[\\![{c}]\\!]]).$

###### Lemma 4

([21], Lemma 2.6) For every graph $(Z,E)$ and every relation $R\subseteq
Z\times Z$,

  1. 1.

the following are equivalent:

    1. (i)

$(R^{[0]}[y])^{[10]}\subseteq R^{[0]}[y]$ for every $y\in Z$;

    2. (ii)

$(R^{[0]}[Y])^{[10]}\subseteq R^{[0]}[Y]$ for every $Y\subseteq Z$;

    3. (iii)

$R^{[1]}[B]=R^{[1]}[B^{[10]}]$ for every $B\subseteq Z$;

  2. 2.

the following are equivalent:

    1. (i)

$(R^{[1]}[b])^{[01]}\subseteq R^{[1]}[b]$ for every $b\in Z$;

    2. (ii)

$(R^{[1]}[B])^{[01]}\subseteq R^{[1]}[B]$ for every $B\subseteq Z$;

    3. (iii)

$R^{[0]}[Y]=R^{[0]}[Y^{[01]}]$ for every $Y\subseteq Z$.

For any graph-based $\mathcal{L}$-frame $\mathbb{F}$, we let
$R_{\Diamondblack}\subseteq Z\times Z$ be defined by $xR_{\Diamondblack}a$ iff
$aR_{\Box}x$, and $R_{\blacksquare}\subseteq Z\times Z$ by
$aR_{\blacksquare}x$ iff $xR_{\Diamond}a$. Hence, for every $B,Y\subseteq Z$,

$R_{\Diamondblack}^{[0]}[B]=R_{\Box}^{[1]}[B]\quad
R_{\Diamondblack}^{[1]}[Y]=R_{\Box}^{[0]}[Y]\quad
R_{\blacksquare}^{[0]}[Y]=R_{\Diamond}^{[1]}[Y]\quad
R_{\blacksquare}^{[1]}[B]=R_{\Diamond}^{[0]}[B].$ (2)

By Lemma 4, the $E$-compatibility of $R_{\Box}$ and $R_{\Diamond}$ guarantees
that the operations $[R_{\Box}],\langle R_{\Diamond}\rangle$ (as well as
$[R_{\blacksquare}],\langle R_{\Diamondblack}\rangle$) are well defined on
$\mathbb{G}^{+}$.

######  Lemma 5 ([19], Lemma 5)

Let $\mathbb{F}=(\mathbb{G},R_{\Box},R_{\Diamond})$ be a graph-based
$\mathcal{L}$-frame. Then the algebra
$\mathbb{F}^{+}=(\mathbb{G}^{+},[R_{\Box}],\langle R_{\Diamond}\rangle)$ is a
complete lattice expansion such that $\langle R_{\Diamondblack}\rangle$ and
$[R_{\Box}]$ (resp. $\langle R_{\Diamond}\rangle$ and $[R_{\blacksquare}]$)
form an adjoint pair.666For any posets $A$ and $B$, the maps $f:A\to B$ and
$g:B\to A$ form an adjoint pair (notation: $f\dashv g$) if for every $a\in A$,
and every $b\in B$, $f(a)\leq b\mbox{ iff }a\leq g(b)$. The map $f$ (resp.
$g$) is the unique left (resp. right) adjoint of $g$ (resp. $f$). It is well
known (cf. [34]) that in a complete lattice a map is completely join
preserving (resp. meet preserving) iff it is a left (resp. right) adjoint of
some map.  Therefore, $[R_{\Box}]$ (resp. $\langle R_{\Diamond}\rangle$) is
completely meet-preserving (resp. completely join-preserving).

###### Definition 11

For every Kripke frame $\mathbb{X}=(S,R)$, the relational structure
$\mathbb{F_{\mathbb{X}}}\coloneqq(\mathbb{G}_{S},R_{\Diamond},R_{\Box})$,
where $R_{\Box}=R_{\Diamond}=R$, is a graph-based frame, since any relation
$R$ on $S$ is clearly $\Delta$-compatible (cf. Definition 10). Conversely, for
any graph-based frame $\mathbb{F}=((Z,E),R_{\Diamond},R_{\Box})$ such that
$E=\Delta$, and $R_{\Diamond}=R_{\Box}$, let
$\mathbb{X_{F}}\coloneqq(Z,R_{\Box})$ be its associated Kripke frame.

For any Kripke frame $\mathbb{X}$, let $\mathbb{X^{+}}$ be its associated
complex algebra.

######  Proposition 4 ([21], Proposition 3.7)

If $\mathbb{X}$ is a Kripke frame, then
$\mathbb{F}_{\mathbb{X}}^{+}\cong\mathbb{X}^{+}$.

###### Proposition 5

For any graph-based frame $\mathbb{F}$, and any Kripke frame $\mathbb{X}$,

$\mathbb{F_{X_{F}}}\cong\mathbb{F}$ and $\mathbb{X_{F_{X}}}\cong\mathbb{X}$.

######  Definition 12 ([19], Definition 4)

A graph-based $\mathcal{L}$-model is a tuple $\mathbb{M}=(\mathbb{F},V)$ where
$\mathbb{F}=(\mathbb{G},R_{\Diamond},R_{\Box})$ is a graph-based
$\mathcal{L}$-frame and $V:\mathsf{Prop}\to\mathbb{F}^{+}$. Since $V(p)$ is a
formal concept (cf. Section 2.4) of $\mathbb{P}_{\mathbb{G}}$, we write
$V(p)=([\\![{p}]\\!],(\\![{p}]\\!))$. For every such $\mathbb{M}$, the
valuation $V$ can be extended compositionally to all $\mathcal{L}$-formulas as
follows:

$V(p)$ | $=$ | $([\\![{p}]\\!],(\\![{p}]\\!))$ |  |  |  |
---|---|---|---|---|---|---
$V(\top)$ | $=$ | $(Z,\varnothing)$ |  | $V(\bot)$ | $=$ | $(\varnothing,Z)$
$V(\varphi\wedge\psi)$ | $=$ | $([\\![{\varphi}]\\!]\cap[\\![{\psi}]\\!],([\\![{\varphi}]\\!]\cap[\\![{\psi}]\\!])^{[1]})$ |  | $V(\varphi\vee\psi)$ | $=$ | $(((\\![{\varphi}]\\!)\cap(\\![{\psi}]\\!))^{[0]},(\\![{\varphi}]\\!)\cap(\\![{\psi}]\\!))$
$V(\Box\varphi)$ | $=$ | $(R_{\Box}^{[0]}[(\\![{\varphi}]\\!)],(R_{\Box}^{[0]}[(\\![{\varphi}]\\!)])^{[1]})$ |  | $V(\Diamond\varphi)$ | $=$ | $((R_{\Diamond}^{[0]}[[\\![{\varphi}]\\!]])^{[0]},R_{\Diamond}^{[0]}[[\\![{\varphi}]\\!]]).$

Moreover, the existence of the adjoints of $[R_{\Box}]$ and $\langle
R_{\Diamond}\rangle$ (cf. Lemma 5) supports the interpretation of the language
$\mathcal{L}^{*}$, which is an expansion of $\mathcal{L}$ with the connectives
$\blacksquare$ and $\Diamondblack$ interpreted as follows:

$V(\blacksquare\varphi)$ | $=$ | $(R_{\blacksquare}^{[0]}[(\\![{\varphi}]\\!)],(R_{\blacksquare}^{[0]}[(\\![{\varphi}]\\!)])^{[1]})$ |  | $V(\Diamondblack\varphi)$ | $=$ | $((R_{\Diamondblack}^{[0]}[[\\![{\varphi}]\\!]])^{[0]},R_{\Diamondblack}^{[0]}[[\\![{\varphi}]\\!]])$
---|---|---|---|---|---|---

Spelling out the definition above as is done in [15], we can define the
satisfaction and refutation relations $\mathbb{M},\mathbf{z}\Vdash\varphi$ and
$\mathbb{M},\mathbf{z}\succ\varphi$ for every graph-based $\mathcal{L}$-model
$\mathbb{M}=(\mathbb{F},V)$, $\mathbf{z}\in Z$, and any $\mathcal{L}$-formula
$\varphi$, by the following simultaneous recursion:

$\mathbb{M},\mathbf{z}\Vdash\bot$ |  | never |  | $\mathbb{M},\mathbf{z}\succ\bot$ |  | always
---|---|---|---|---|---|---
$\mathbb{M},\mathbf{z}\Vdash\top$ |  | always |  | $\mathbb{M},\mathbf{z}\succ\top$ |  | never
$\mathbb{M},\mathbf{z}\Vdash p$ | iff | $\mathbf{z}\in[\\![{p}]\\!]$ |  | $\mathbb{M},\mathbf{z}\succ p$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}^{\prime}E\mathbf{z}\Rightarrow\mathbf{z}^{\prime}\not\Vdash p]$
$\mathbb{M},\mathbf{z}\succ\varphi\vee\psi$ | iff | $\mathbb{M},\mathbf{z}\succ\varphi\text{ and }\mathbb{M},\mathbf{z}\succ\psi$ |  | $\mathbb{M},\mathbf{z}\Vdash\varphi\vee\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}E\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\succ\varphi\vee\psi]$
$\mathbb{M},\mathbf{z}\Vdash\varphi\wedge\psi$ | iff | $\mathbb{M},\mathbf{z}\Vdash\varphi\text{ and }\mathbb{M},\mathbf{z}\Vdash\psi$ |  | $\mathbb{M},\mathbf{z}\succ\varphi\wedge\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}^{\prime}E\mathbf{z}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\Vdash\varphi\wedge\psi]$
$\mathbb{M},\mathbf{z}\succ\Diamond\varphi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}R_{\Diamond}\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\Vdash\varphi]$ |  | $\mathbb{M},\mathbf{z}\Vdash\Diamond\varphi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}E\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\succ\Diamond\varphi]$
$\mathbb{M},\mathbf{z}\Vdash\Box\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}R_{\Box}\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\succ\psi]$ |  | $\mathbb{M},\mathbf{z}\succ\Box\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}^{\prime}E\mathbf{z}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\Vdash\Box\psi]$
$\mathbb{M},\mathbf{z}\succ\Diamondblack\varphi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}R_{\Diamondblack}\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\Vdash\varphi]$ |  | $\mathbb{M},\mathbf{z}\Vdash\Diamondblack\varphi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}E\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\succ\Diamondblack\varphi]$
$\mathbb{M},\mathbf{z}\Vdash\blacksquare\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}R_{\blacksquare}\mathbf{z}^{\prime}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\succ\psi]$ |  | $\mathbb{M},\mathbf{z}\succ\blacksquare\psi$ | iff | $\forall\mathbf{z}^{\prime}[\mathbf{z}^{\prime}E\mathbf{z}\Rightarrow\mathbb{M},\mathbf{z}^{\prime}\not\Vdash\blacksquare\psi]$

Note that the satisfaction of disjuction formulas at a state is defined as the
non-refutation of the disjuncts at all its $E$-successors, which is different
from the satisfaction clause in distributive logics. Also, unlike distributive
modal logic, the satisfiability clauses for all modal operators including the
diamonds are given by universal quantifiers.

An $\mathcal{L}$-sequent $\varphi\vdash\psi$ is true in $\mathbb{M}$, denoted
$\mathbb{M}\models\varphi\vdash\psi$, if for all
$\mathbf{z},\mathbf{z}^{\prime}\in Z$, if $\mathbb{M},\mathbf{z}\Vdash\varphi$
and $\mathbb{M},\mathbf{z}^{\prime}\succ\psi$ then
$\mathbf{z}E^{c}\mathbf{z}^{\prime}$. An $\mathcal{L}$-sequent
$\varphi\vdash\psi$ is valid in $\mathbb{F}$, denoted
$\mathbb{F}\models\varphi\vdash\psi$, if it is true in every model based on
$\mathbb{F}$.

The next lemma follows immediately from the definition of an
$\mathcal{L}$-sequent being true in a graph-based $\mathcal{L}$-model.

######  Lemma 6 ([19], Lemma 7)

For any graph-based $\mathcal{L}$-frame $\mathbb{F}$ and any
$\mathcal{L}$-sequent $\varphi\vdash\psi$,

$\mathbb{F}\models\varphi\vdash\psi$ iff
$\mathbb{F}^{+}\models\varphi\vdash\psi$.

###  2.5 Inductive modal reduction principles and their ALBA-outputs

A modal reduction principle (mrp) of the basic language of non-distributive
modal logic $\mathcal{L}$ is an inequality $s(p)\leq t(p)$ such that both $s$
and $t$ are built up using only $\Box$ and $\Diamond$. The term $s(p)$ (resp.
$t(p)$) is good if it is a (possibly empty) sequence of diamonds (resp. boxes)
followed by a (possibly empty) sequence of boxes (resp. diamonds). A modal
reduction principle is inductive iff it is Sahlqvist iff either $s(p)$ or
$t(p)$ is good, and is analytic inductive if both are good. So, inductive
modal reduction principles are of one of the following types:

$\text{(a)}\ \ \
\varphi[\alpha(p)/!y]\leq\psi[\chi(p)/!x]\quad\quad\quad\text{(b)}\ \ \
\varphi[\zeta(p)/!y]\leq\psi[\delta(p)/!x],$

where $\Box$ (resp. $\Diamond$) is the only connective allowed in $\alpha(p)$
and $\psi(!x)$ (resp. $\varphi(!y)$ and $\delta(p)$), and $\chi$ (resp.
$\zeta$) has $\Diamond$ (resp. $\Box$) as principal connective whenever
$\chi(p)\neq p$ (resp. $\zeta(p)\neq p$). Analytic inductive mrps are of the
form $\varphi[\alpha(p)/!y]\leq\psi[\delta(p)/!x]$, where $\psi(!x)$,
$\varphi(!y)$, $\delta(p)$ and $\alpha(p)$ are as above, and thus they are of
both types (a) and (b). Prime examples of analytic inductive mrps feature
prominently in several proposed modal axiomatizations of generalized
approximation spaces (cf. Sections 2.2 and 2.3). The ALBA outputs of inductive
mrps are the following inequalities in the expanded language $\mathcal{L}^{+}$
(cf. [17]):777 The language $\mathcal{L}^{+}$ expands $\mathcal{L}^{*}$ with
two denumerable sets of sorted variables
$\mathsf{NOM}\ni\mathbf{i},\mathbf{j}$ and
$\mathsf{CONOM}\ni\mathbf{m},\mathbf{n}$. The reader is referred to [25, 17]
for a general presentation of ALBA.

type (a) |  $\quad\forall\mathbf{j}[\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]\leq\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]]$,
---|---
type (b) |  $\quad\forall\mathbf{m}[\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]\leq\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]$,

where, when $\theta$ is a sequence of $\Box$ (resp. $\Diamond$) connectives of
length $n$, $\mathsf{LA}(\theta)(!u)$ (resp. $\mathsf{RA}(\theta)(!u)$) is a
sequence of $\Diamondblack$ (resp. $\blacksquare$) connectives of length $n$
ending with a (single) occurrence of the variable $u$.

###### Example 1

The mrp $\Diamond\Diamond\Box\Box p\leq\Box\Diamond\Box p$ is inductive of
type (a), but not analytic, since it instantiates type (a) above as follows:
$\varphi(y)\coloneqq\Diamond\Diamond y$, $\alpha(p)\coloneqq\Box\Box p$,
$\psi(x)\coloneqq\Box x$, $\chi(p)\coloneqq\Diamond\Box p$. Thus,
$\mathsf{LA}(\psi)(u)=\Diamondblack u$,
$\mathsf{LA}(\alpha)(u)=\Diamondblack\Diamondblack u$; therefore, its ALBA
output is

|  $\forall\mathbf{j}\;[(\Diamondblack u)[(\Diamond\Diamond
y)[\mathbf{j}/y]/u]\leq(\Diamond\Box p)[(\Diamondblack\Diamondblack
u)[\mathbf{j}/u]/p]]$,
---|---
i.e. |  $\forall\mathbf{j}\;[(\Diamondblack u)[(\Diamond\Diamond\mathbf{j})/u]\leq(\Diamond\Box p)[(\Diamondblack\Diamondblack\mathbf{j})/p]]$,
i.e. |  $\forall\mathbf{j}\;[\Diamondblack\Diamond\Diamond\mathbf{j}\leq\Diamond\Box\Diamondblack\Diamondblack\mathbf{j}]$.

The mrp $\Diamond\Box\Box p\leq\Box\Box\Box\Diamond\Diamond\Diamond\Diamond p$
is analytic inductive, as it instantiates the analytic shape above as follows:
$\varphi(y)\coloneqq\Diamond y$, $\alpha(p)\coloneqq\Box\Box p$,
$\psi(y)\coloneqq\Box\Box\Box y$,
$\delta(p)\coloneqq\Diamond\Diamond\Diamond\Diamond p$. Thus,
$\mathsf{RA}(\delta)(u)=\blacksquare\blacksquare\blacksquare\blacksquare u$,
and $\mathsf{RA}(\varphi)(u)\coloneqq\blacksquare u$. Since this mrp is
analytic, it can be solved both as a type (a) and as a type (b); solving it as
type (b) yields

|  $\forall\mathbf{m}\;[(\Box\Box
y)[(\blacksquare\blacksquare\blacksquare\blacksquare
u)[\mathbf{m}/u]/p]\leq(\blacksquare u)[(\Box\Box\Box y)[\mathbf{m}/y]/u]]$,
---|---
i.e. |  $\forall\mathbf{m}\;[(\Box\Box y)[(\blacksquare\blacksquare\blacksquare\blacksquare\mathbf{m})/p]\leq(\blacksquare u)[(\Box\Box\Box\mathbf{m})/u]]$,
i.e. |  $\forall\mathbf{m}\;[\Box\Box\blacksquare\blacksquare\blacksquare\blacksquare\mathbf{m}\leq\blacksquare\Box\Box\Box\mathbf{m}]$.

##  3  Two case studies on informational entropy

In the present section, we discuss two examples in which informational entropy
is relevant to the analysis, and is explicitly accounted for in the
environment of graph-based frames.

###  3.1 Social media news network

Let the reflexive graph $(Z,E)$ represent a social media news network, where
$Z$ is a set of accounts, and $zEz^{\prime}$ iff account $z$ is a source of
news for account $z^{\prime}$, that is, $z^{\prime}$ follows the news posted
by $z$. Under this interpretation, the reflexivity of $E$ says that every
account is a source of information for itself. For any news (fact) $p$, an
account $z$ refutes $p$ iff none of its $E$-predecessors post (i.e. support)
$p$. That is, $z$ refutes $p$ iff none of its information sources support $p$.
We interpret $z\succ p$ as account ‘$z$ refutes news $p$’ (that is, $z$ makes
a post denying $p$) and $z\Vdash p$ as account ‘$z$ confirms (posts) news
$p$’. Formally, for any $z\in Z$, and any proposition $p$,

$z\succ p\quad\text{iff}\quad\text{for all }z^{\prime},\text{ if
}z^{\prime}Ez\,\text{ then }\,z^{\prime}\not\Vdash p.$

On the other hand, an account $z$ posts news $p$ iff none of the followers of
$z$ refutes $p$.888Recall that, since $E$ is reflexive, $z$ is among its
followers, and hence not refuting $p$ is a (clearly) necessary, but in general
not sufficient condition for $z$ to post (support) $p$. Formally, for any
$z\in Z$, and any proposition $p$,

$z\Vdash p\quad\text{iff}\quad\text{for all $z^{\prime}$},\text{ if
}zEz^{\prime}\,\text{ then }\,z^{\prime}\not\succ p.$

This clause reflects the common practice, in the management of social media
accounts, of not posting any news item which one’s own audience would find
controversial, on pain of loss of followers, conflicts, backlashes or
embarrassments [63, 73, 79]. Seen from the followers’ perspective, if one of
the accounts they follow (confirm) post a news item $p$, then they either
decide to no longer refute it or they stop following this account (such
behaviour is especially common in more politically active users[35, 65]).
Thus, the satisfaction clause above reflects the equilibrium to which these
dynamics converge.

Note that, as $E$ is reflexive, if it is the case that $zEz^{\prime}\implies
z^{\prime}\not\succ p$, for all $z^{\prime}$, then $z\not\succ p$. By the
defining condition of refutation, the latter implies an account
$z^{\prime\prime}\in Z$ exists such that $z^{\prime\prime}Ez$ and
$z^{\prime\prime}\Vdash p$. Thus, the compatibility conditions between
relations $\Vdash$ and $\succ$ in graph-based modal logic is naturally
justified in this interpretation. Notice that, in general, accounts followed
by an account $z$ need not see news posted by $z$. That is, accounts which are
sources of news for $z$ need not follow $z$ for the news. Thus, in general, it
is possible that there exist accounts $z,z^{\prime}\in Z$ such that
$zEz^{\prime}$, $z\succ p$ and $z^{\prime}\Vdash p$. Note that relation $E$
encodes inherent indiscernibility of the model in the sense that the accounts
which have the same sources of information (accounts they follows) will refute
exactly same set of news items, while accounts with the same set of followers
will post the same set of news items. Thus, they are indiscernible from each
other with regards to their behaviour on social media. This phenomenon is
often observed on social media in the formation on communities which are so-
called echo-chambers. Thus, we can see a concept
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))$ as an echo-chamber (community)
with news sources $[\\![{\varphi}]\\!]$ and followers $(\\![{\varphi}]\\!)$.

Let $R_{\Diamond}\supseteq E^{-1}$ be a relation such that for any
$z,z^{\prime}\in Z$, $zR_{\Diamond}z^{\prime}$ iff $z$ can possibly hear news
from $z^{\prime}$. Recall that the refutation clause for $\Diamond$ (see
Section 2.4) is

$z\succ\Diamond p\quad\text{iff}\quad\text{for all $z^{\prime}$,
}\;zR_{\Diamond}z^{\prime}\;\text{implies}\;z^{\prime}\not\Vdash p.$

This can be interpreted as follows. In some circumstances for some news $p$, a
social media account may want to be very sure before refuting it. In this case
$z$ may check the posts from all the news sources they can possibly access,
and not only the accounts they follow, and only refute if none of the possible
sources confirm (post about) $p$. That is, $z\succ\Diamond p$, iff none of the
possible news sources for $z$ confirm (post) $p$.

Let $R_{\Box}\supseteq E$ be a relation such that for any $z,z^{\prime}\in Z$,
$zR_{\Box}z^{\prime}$ iff $z^{\prime}$ can possibly get the news posted by
$z$. By the definition of refutation clause for $\Box$ (See Section 2.4), is
given by

$z\Vdash\Box p\quad\text{iff}\quad\text{for all
$z^{\prime}$}\,zR_{\Box}z^{\prime}\,\text{implies}\,z^{\prime}\not\succ p.$

This can be interpreted as follows. In some circumstances for some news $p$, a
social media account may want to be sure that none of the accounts who are
possibly reached by them refute it. In this case $z$ may confirm (post) news
$p$ if none of the accounts who can possibly be reached by a post from $z$
refute $p$. That is, $z\Vdash\Box p$, iff none of the possible recipients of
news from $z$ refute $p$. The relations $R_{\Diamond}$ and $R_{\Box}$ can be
seen as the upper approximations of relations $E^{-1}$ and $E$. Thus, the
accounts which have the same sets of accounts related to them by
$R_{\Diamond}$, that is accounts who see posts from same set of accounts (even
for important news) can be seen as a core set of followers of these sources
(core of an echo-chamber), on the other hand, the set of news sources with the
same follower accounts related by $R_{\Box}$ are the accounts whose posts are
always seen by the same set of accounts. These can be seen as the core news
sources of an echo-chamber. Thus, for an echo-chamber (community) described by
concept $([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))$, the sets
$[\\![{\Box{\varphi}}]\\!]$ and $(\\![{\Diamond{\varphi}}]\\!)$ can be
interpreted as the core followers and core news sources of this echo-chamber
respectively. The conditions $E\subseteq R_{\Box}$ and $E^{-1}\subseteq
R_{\Diamond}$, imply that
$[\\![{\Box{\varphi}}]\\!]\subseteq[\\![{\varphi}]\\!]$ and
$(\\![{\Diamond{\varphi}}]\\!)\subseteq(\\![{\varphi}]\\!)$ (and hence that
$(\\![{\varphi}]\\!)\subseteq(\\![{\Box{\varphi}}]\\!)$ and
$[\\![{\varphi}]\\!]\subseteq[\\![{\Diamond{\varphi}}]\\!]$) which can be
interpreted as saying the set of core followers and core news sources of an
echo-chamber are subsets of the sets of all followers and news sources in this
echo-chamber respectively.

###  3.2 Rashomon

Akira Kurosawa’s acclaimed 1950 film Rashomon is set in medieval Japan and
depicts the death by cutlass of a samurai through the widely differing and
mutually conflicting accounts of the characters mainly involved: the bandit
($b$), the samurai’s wife ($\ell$), and the samurai himself ($s$) speaking
through a medium, as well as the account of a witness, the woodcutter ($w$).
Both in popular culture and in academic literature, Rashomon’s story has been
regarded as the paradigmatic illustration of the subjectivity of truth and the
impossibility of reaching factual accuracy, and the expression Rashomon effect
has been coined to refer to the effect of observers’ subjective perception on
their recollection of an event causing them to produce widely divergent but
equally plausible accounts of it.

Each main character testifies to be the one who killed $s$, and rather than
self-exculpation, the main intent of the characters testimony (including $w$’s
testimony) is to portray an image of themselves which is aligned with their
own social role, and which embodies its virtues. Hence, in each testimony, the
witnesses arrange their facts (highlighting some of them, ignoring or
excluding or misrepresenting others) according to their own ‘moral agenda’,
and it is precisely the compatibility between their various ‘moral agendas’
that we represent in the reflexive graph below (where all reflexive arrows are
omitted), rather than the factual compatibility among the various testimonies:

$z_{b}$$z_{\ell}$$z_{w}$$z_{s}$

In the graph $(Z,E)$ represented in the picture above, each state in the
domain $Z:=\\{z_{b},z_{\ell},z_{s},z_{w}\\}$ represents one testimony, and the
intended interpretation of edges in $E\subseteq Z\times Z$ is the following:

$z_{x}Ez_{y}$ iff $y$’s portrayal of $x$’s moral agenda does not clash with
$x$’s own portrayal.

As represented in the graph above, the moral agendas of $\ell,s$ and $b$ are
undermined by all the other testimonies: indeed, $b$’s portrayal of himself as
a competent, powerful, resourceful, and sexually irresistible bandit with his
own code of honour is undermined by $\ell$’s and $s$’s portrayal of him as a
rapist, and by $w$’s portrayal of him as clumsy, incompetent, and gullible;
$\ell$’s portrayal of herself as a passive victim (not only of rape by the
bandit, but also of her husband’s cynicism and cold lack of interest in her
honour and her fate) is undermined both by $b$’s portrayal of her as a fierce
woman, and by $s$’s and $w$’s portrayals of her as being cold, manipulative,
and capable of turning situations to her own advantage; $s$’s portrayal of
himself as a honourable man who has suffered the basest betrayal by his lawful
wife is undermined by $b$’s description of $\ell$’s legitimate interest in
protecting her own honour, and by $\ell$’s and $w$’s portrayal of $s$ as a
cowardly and dishonorable man. Finally, since the presence of $w$ at the scene
is not registered in any other testimony, $w$’s portrayal of himself as a pure
witness and a law-abiding citizen is compatible with all testimonies
(including his own). The concept lattice arising from this graph is
represented in the following picture, 999Notice that the resulting concept
lattice is distributive; this is unsurprising, since the graph originating it
is not only reflexive but also transitive (cf. [28, Proposition 4.1]) where
e.g. $(\ell s,bw)$ is the shorthand for the formal concept of $(Z,E)$ having
$\\{z_{\ell},z_{s}\\}$ as its extension and $\\{z_{b},z_{w}\\}$ as its
intension.

$(b\ell s,w)$$(\varnothing,b\ell sw)$ $(b\ell sw,\varnothing)$ $(b,\ell
sw)$$(b\ell,sw)$$(\ell,bsw)$$(bs,\ell w)$$(s,b\ell w)$$(\ell s,bw)$

Additional “epistemic” relations, besides the basic relation $E$, can be
considered, each of which encoding e.g. how each of the main characters might
argue (for instance, for the purpose of persuading a jury of their moral
stance) that some of the other testimonies do not actually invalidate their
own portrayal of themselves. For instance, $s$ might argue that the overall
portrayal $b$ makes of him is not incompatible with his own portrayal of
himself as a dignified man, who adheres to his social role; likewise, $b$
might argue that, through $s$’s testimony, his outlaw code of honour emerges
with sufficient clarity; finally, $\ell$ might argue that, while in the
beginning $b$ might have mistaken her character as fierce, later on he
recognized this as a misunderstanding, and hence, overall, $b$’s portrayal of
$\ell$ is compatible with $\ell$’s own. Thus, the additional relations
$R_{b}$, $R_{\ell}$ and $R_{s}$ are represented as follows (in the following
pictures, $E$ is understood to be properly included in each of the three
additional relations):

$z_{b}$$z_{\ell}$$z_{w}$$z_{s}$$R_{b}$$z_{b}$$z_{\ell}$$z_{w}$$z_{s}$$R_{\ell}$$z_{b}$$z_{s}$$z_{w}$$z_{\ell}$$R_{s}$

That is, the intended interpretation of edges in $R_{u}\subseteq Z\times Z$,
for any $u\in\\{b,\ell,s\\}$, is the following: for all
$x,y\in\\{b,\ell,s,w\\}$,

$z_{x}R_{u}z_{y}$ iff $y$’s portrayal of $x$’s moral agenda does not clash
with $x$’s own portrayal, according to $u$.

These additional relations are all $E$-compatible, and each of them induces a
pair of adjoint modal operators $\Diamond_{u}\dashv\Box_{u}$ for any
$u\in\\{b,\ell,s\\}$, represented as follows:101010In the pictures, the red
descending arrows represent the non-identity assignments of the $\Box$-type
operators and the blue ascending ones those of their left adjoints; for the
sake of readability, the identity assignments of all operations are omitted.

$(b\ell s,w)$$(\varnothing,b\ell sw)$ $(b\ell sw,\varnothing)$ $(b,\ell sw)$$(b\ell,sw)$$(\ell,bsw)$$(bs,\ell w)$$(s,b\ell w)$$(\ell s,bw)$$\Diamond_{b}\dashv\Box_{b}$ | $(b\ell s,w)$$(\varnothing,b\ell sw)$ $(b\ell sw,\varnothing)$ $(b,\ell sw)$$(b\ell,sw)$$(\ell,bsw)$$(bs,\ell w)$$(s,b\ell w)$$(\ell s,bw)$$\Diamond_{\ell}\dashv\Box_{\ell}$ | $(b\ell s,w)$$(\varnothing,b\ell sw)$ $(b\ell sw,\varnothing)$ $(b,\ell sw)$$(b\ell,sw)$$(\ell,bsw)$$(bs,\ell w)$$(s,b\ell w)$$(\ell s,bw)$$\Diamond_{s}\dashv\Box_{s}$ $\Diamond_{s}\dashv\Box_{s}$
---|---|---

As it can be easily verified by inspection, the operations represented above
validate the following axioms for any $u\in\\{b,\ell,s\\}$ and any
$c\in\mathbb{L}$:

$\Box_{u}c\vdash c\quad c\vdash\Diamond_{u}c\quad
c\vdash\Box_{u}\Diamond_{u}c\quad\Diamond_{u}\Box_{u}c\vdash
c\quad\Box_{u}c\vdash\Box_{u}\Box_{u}c\quad\Diamond_{u}\Diamond_{u}c\vdash\Diamond_{u}c,$

which implies (cf. Table 3) that the relations $R_{b}$, $R_{\ell}$ and $R_{s}$
are $E$-reflexive and $E$-transitive (see Remark 1 below). Hence, each of the
pairs of adjoint operations induced by the additional relation can be
understood to represent the lower and upper approximations of ‘knowable truth’
from the subjective viewpoint of the main characters of the story. Finally,
notice that the ‘knowable truth’ can be exactly captured via the collective
upper and lower approximations respectively defined by the assignments
$c\mapsto\Box_{b}c\vee\Box_{\ell}c\vee\Box_{s}c$ and
$c\mapsto\Diamond_{b}c\wedge\Diamond_{\ell}c\wedge\Diamond_{s}c$.

###### Remark 1

In Section 6.3, we show how the first-order correspondents of modal reduction
principles in Kripke frames can be shifted (see Definition 19 and Theorem 6.1)
to properties on graph-based frames which are parametric on the relation $E$;
hence we use the convention that the shifting (parametric on $E$) of some
property prop is called $E$-prop. For instance, the shifting of denseness is
called $E$-denseness, and the shifting of reflexivity is $E$-reflexivity.

In both examples considered above, the reflexive relations $E$ is used to
model the inherent indiscernibility or limits of knowability in a given
situation, while additional relations ($R_{\Diamond}$, $R_{\Box}$, $R_{s}$,
$R_{\ell}$ etc.) are used to model agent-specific indiscernibility. The
inherent indiscernibility relation $E$ gives rise to a complete lattice,
representing the space of conceptual possibilities and their ordering (in the
first example above this becomes the space of so-called echo chambers while,
in the second, the moral compatibility space of testimonies). This is
analogous to the equivalence relation in an approximation space giving rise to
a Boolean algebra of rough sets. Unlike in the modal logic approach to rough
set theory (see, e.g., [57]), however, $E$ is not used to interpret
modalities. Rather, $E$ is used to generate a lattice of stable sets on which
the propositional connectives are algebraically interpreted, thereby
‘internalizing $E$’ into the propositional fragment of the logic, which causes
it to be non-classical and, in fact, non-distributive. This is similar to the
situation in intuitionistic (modal) logic where the partial orders in
intuitionistic Kripke frame generate Heyting algebras of upwards closed sets.

The relations associated with an agent captures the peculiarities of their
specific epistemic access or lens through which they view the space of
conceptual possibilities (in the first example above, this takes the form of
epistemic access between agents beyond the “source/follower” relation and, in
the second, the agents’ notions of compatibility as viewed from their personal
moral standpoints). As one would expect, such views remain inherently
conditioned and mediated by the space of conceptual possibilities (i.e. by the
inherent bounds on knowability), and this fact is mathematically captured by
the requirement that the agents’ relations be compatible with $E$.
Accordingly, a modal expression $\Diamond p$ represents the proposition $p$
reflected through a particular agent-specific lens. Thus, the modeling of the
scenarios above using graph-based frames maintains a neat separation between
the inherent and the epistemic indiscernibility. Such a clear division of
labour would not be possible had we used $E$ to interpret an additional set of
modal operators.

##  4 Hyper-constructivist approximation spaces

In the previous section, we showed how graph-based frames and their associated
modal languages can formalize reasoning under epistemic uncertainty (modelled
by additional relations $R_{\Box}$, $R_{\Diamond}$ etc.) in a framework with
inherent indiscernibility (modeled by relation $E$). In a similar way, such
models have served to represent other scenarios in which inherent limits to
knowability play a relevant role [19, 27, 18]. These examples motivate the
introduction of hyper-constructivist (or evidentialist) approximation spaces,
based on graph-based frames, as a generalization of approximation spaces to a
framework with inherent informational entropy. The strategy we follow for
introducing this generalization is similar to the one adopted in [21] for
introducing the notion of conceptual approximation space. Namely, we identify
the defining properties of hyper-constructivist approximation spaces (cf.
Definition 13) in terms of the first-order conditions corresponding, on graph-
based frames, to the Sahlqvist mrps corresponding, on Kripke frames, to the
first-order conditions expressing the seriality, reflexivity, transitivity,
and symmetry of the accessibility relations associated with the modal
operators.

###### Definition 13

A hyper-constructivist (or evidentialist) approximation space is a graph-based
$\mathcal{L}$-frame $\mathbb{F}=(Z,E,R_{\Box},R_{\Diamond})$ such that
$E\subseteq
R_{\Box}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}\,R_{\blacksquare}$, where
${\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}$ is defined as in Definition 14. A
hyperconstructivist approximation space
$\mathbb{F}=(Z,E,R_{\Box},R_{\Diamond})$ is:

  1. 1.

$E$-reflexive if $E\subseteq R_{\Box}$ and $D\subseteq R_{\Diamond}$.

  2. 2.

$E$-symmetric if $R_{\blacksquare}\subseteq R_{\Box}$ and
$R_{\Diamondblack}\subseteq R_{\Diamond}$.

  3. 3.

$E$-transitive if
$R_{\Box}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\Box}\subseteq R_{\Box}$
and
$R_{\Diamond}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\Diamond}\subseteq
R_{\Diamond}$.

  4. 4.

Pawlak if it is $E$-reflexive, $E$-symmetric and $E$-transitive.

In what follows, we motivate the definition above. As discussed in Section
2.2, one of the most basic requirements in the notion of generalized
approximation spaces is that the indiscernibility relation be serial, since
this condition is the first-order correspondent of the mrp $\Box a\leq\Diamond
a$, which guarantees that the lower approximation is smaller than or equal to
the upper approximation. The ALBA outputs of $\Box a\leq\Diamond a$ (which is
an analytic inductive mrp) are
$\forall\mathbf{j}(\mathbf{j}\leq\Diamond\Diamondblack\mathbf{j})$ and
$\forall\mathbf{m}(\Box\blacksquare\mathbf{m}\leq\mathbf{m})$ (cf. Section
2.5), which, when translated in the first-order language of Kripke frames,
yield the first-order correspondents $\forall w(\\{w\\}\subseteq
R_{\Diamond}^{-1}[R^{-1}_{\Diamondblack}[w]])$ and $\forall
w((R_{\Box}^{-1}[(R_{\blacksquare}^{-1}[\\{w\\}^{cc}])^{cc}])^{c}\subseteq\\{w\\}^{c})$,
which can be respectively unravelled as $\forall w\exists
v(wR_{\Diamond}v\,\&\,vR_{\Diamondblack}w)$ and $\forall w\exists
v(wR_{\Box}v\,\&\,vR_{\blacksquare}w)$. These first-order sentences can
equivalently be rewritten as the relational inclusions $\Delta\subseteq
R_{\Diamond}\circ R_{\Diamondblack}$ and $\Delta\subseteq R_{\Box}\circ
R_{\blacksquare}$, respectively. Translating the ALBA outputs above in the
first-order language of graph-based frames yields

$\forall
z(R_{\Diamond}^{[0]}[E^{[0]}[R_{\Diamondblack}^{[0]}[z^{[10]}]]]\subseteq
z^{[1]})\quad$ and $\quad\forall
z(R_{\Box}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[z^{[01]}]]]\subseteq
z^{[0]})$.

By the $E$-compatibility of $R_{\Box}$ and $R_{\Diamond}$ (cf. Lemma 4) these
inclusions can be simplified as follows:

$\forall z(R_{\Diamond}^{[0]}[E^{[0]}[R_{\Diamondblack}^{[0]}[z]]]\subseteq
z^{[1]})\quad$ and $\quad\forall
z(R_{\Box}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[z]]]\subseteq z^{[0]})$,

and then be partially unravelled as the following implications (recall that
$D\coloneqq E^{-1})$:

$\forall x\forall z(x\in
R_{\Diamond}^{[0]}[E^{[0]}[R_{\Diamondblack}^{[0]}[z]]]\Rightarrow
xD^{c}z)\quad$ and $\forall a\forall z(a\in
R_{\Box}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[z]]]\Rightarrow aE^{c}z)$,

which, on application of contraposition yields

$\forall x\forall z(xDz\Rightarrow x\notin
R_{\Diamond}^{[0]}[E^{[0]}[R_{\Diamondblack}^{[0]}[z]]])\quad$ and
$\quad\forall a\forall z(aEz\Rightarrow a\notin
R_{\Box}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[z]]])$,

and then as follows:

$\forall x\forall z(xDz\Rightarrow
x(R_{\Diamond}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\Diamondblack})z)\quad$
and $\quad\forall a\forall z(aEz\Rightarrow
a(R_{\Box}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\blacksquare})z)$,

by letting
$x(R_{\Diamond}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\Diamondblack})z$
iff $x\notin R_{\Diamond}^{[0]}[E^{[0]}[R_{\Diamondblack}^{[0]}[z]]]$, and
$a(R_{\Box}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\blacksquare})z$ iff
$a\notin R_{\Box}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[z]]]$. These
‘abbreviations’, which are in fact instances of the notion of $E$-mediated
composition (cf. Definition 14 in Section 5.1, below), allow us to
equivalently rewrite these first-order sentences as relational inclusions
$D\subseteq
R_{\Diamond}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\Diamondblack}$
and $E\subseteq
R_{\Box}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\blacksquare}$,
respectively.

What is more, when rewritten in this way, it is possible to recognize the
similarity between the first-order correspondents on graph-based frames and
those on Kripke frames. Specifically, it is not difficult to verify that,
instantiating $E\coloneqq\Delta$ in $D\subseteq
R_{\Diamond}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\Diamondblack}$,
one obtains a condition which is equivalent to $\Delta\subseteq
R_{\Diamond}\circ R_{\Diamondblack}$, and similarly with the second pair of
inclusions. This hints at the existence of a transfer of relational
constructions and properties along the natural embedding of sets into
reflexive graphs. Such transfer hinges on a ‘parametric shift’ from $\Delta$
to $E$.

In Section 6.3, we show that this transfer of properties and constructions,
formalized in terms of the notion of shifting (cf. Definition 19), extends to
all first-order correspondents of inductive mrps. In Section 7, we apply this
result to the principled definition of various hyper-constructivist
counterparts of generalized approximation spaces, and discuss how this
transfer works not only technically but also conceptually, given that the
intuitive meaning of modal axioms transfers from Kripke frames to the graph-
based frames (cf. Examples 10, 11, 12).

##  5 Relational compositions, and the algebras of relations on graph-based
and Kripke frames

In this section we partly recall, partly introduce several notions of
relational compositions on graph-based frames [19, 20]. We also introduce the
relational languages $\mathsf{KRel}_{\mathcal{L}}$ and
$\mathsf{GRel}_{\mathcal{L}}$ associated with Kripke frames and graph-based
frames respectively and used to express first-order conditions in these
contexts. We define a translation from $\mathsf{GRel}$ to $\mathsf{KRel}$
which is compatible with the natural relationship between these classes. The
definitions and notation we introduce here will be key to a meaningful
comparison of the correspondents of inductive mrps in different semantic
settings.

###  5.1 Composing relations on graph-based frames

The following definition expands those given in [21, Section 3.4]. As will be
clear from Lemma 7, the $E$-compositions can be understood as the counterparts
of the usual composition of relations in the setting of graph-based frames.

###### Definition 14

For any graph $\mathbb{G}=(Z,E)$, and any $R,T\subseteq Z\times Z$, the
$E$-mediated compositions $R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T$
and $R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T$ and the composition
$R\,\ast T\subseteq Z\times Z$ are defined as follows: for all $a,x\in Z$,

$x(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)a$ | iff | $x\in(R^{[0]}[E^{[0]}[T^{[0]}[a]]])^{c}$ | i.e. | $(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[a]={R}^{[0]}[E^{[0]}[T^{[0]}[a]]]$
---|---|---|---|---
$a(R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T)x$ | iff | $a\in(R^{[0]}[E^{[1]}[T^{[0]}[x]]])^{c}$ | i.e. | $(R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T)^{[0]}[x]=R^{[0]}[E^{[1]}[T^{[0]}[x]]]$
$a(R\,\ast T)x$ | iff | $a\in(R^{[0]}[T^{[0]}[x]])^{c}$ | i.e. |  $(R\,\ast T)^{[0]}[x]=R^{[0]}[T^{[0]}[x]]$.

The following lemma, which readily follows from the definition, shows that the
two notions of $E$-mediated composition collapse to the usual notion when
$E\coloneqq\Delta$.

###### Lemma 7

For all sets $S$, all relations $R,T\subseteq S\times S$ on the graph
$\mathbb{G}_{S}=(S,\Delta)$,

$R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{\Delta}T=R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{\Delta}T=R\,\circ
T.$

The following lemma shows that the $E$-mediated compositions
${\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}$ and
${\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}$ are well defined,
associative, and have unit $E$ and $D$, respectively; hence they endow the set
of $E$-compatible relations over a reflexive graph with a monoidal structure.

###### Lemma 8

For any graph $\mathbb{G}=(Z,E)$, all $R,T,U\subseteq Z\times Z$, and any
$Y\subseteq Z$,

  1. 1.

if $R$ is $E$-compatible, then
$R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}D=R=D\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R\quad\text{and}\quad
R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}E=R=E\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R$;

  2. 2.

if $R$ is $E$-compatible, then so are
$R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T$,
$R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T$, and $R\,\ast T$;

  3. 3.

if $R$ and $T$ are $E$-compatible, then
$(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[Y]=R^{[0]}[E^{[0]}[T^{[0]}[Y]]]$
and
$(R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T)^{[0]}[Y]=R^{[0]}[E^{[1]}[T^{[0]}[Y]]]$;

  4. 4.

if $R$, $T$, and $U$ are $E$-compatible, then
$R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}(T\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}U)=(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}U$
and
$R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}(T\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}U)=(R\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}T)\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}U$.

###### Proof

1\. For any $a\in Z$,
$(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}D)^{[0]}[a]=R^{[0]}[E^{[0]}[D^{[0]}[a]]]=R^{[0]}[E^{[0]}[E^{[1]}[a]]]=R^{[0]}[a]$,
the last identity holding by the $E$-compatibility of $R$. The remaining
identities are omitted.
2\. For any $a\in Z$,

$((R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[a])^{[10]}$ | = | $({R}^{[0]}[E^{[0]}[T^{[0]}[a]]])^{[10]}$ | Definition 14 (i)
---|---|---|---
| = | ${R}^{[0]}[E^{[0]}[T^{[0]}[a]]]$ | Lemma 4
| = |  $(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[a]$. | Definition 14 (i)

The remaining identities are proven similarly.
3\. We only prove the first statement.

$R^{[0]}[E^{[0]}[T^{[0]}[Y]]]$ | = | $R^{[0]}[E^{[0]}[T^{[0]}[\bigcup_{y\in Y}y]]]$ | $Y=\bigcup_{y\in Y}y$
---|---|---|---
| = | $R^{[0]}[E^{[0]}[\bigcap_{y\in Y}T^{[0]}[y]]]$ | Lemma 1 (v)
| = | $R^{[0]}[E^{[0]}[\bigcap_{y\in Y}E^{[1]}[E^{[0]}[T^{[0]}[y]]]]]$ |  $E$-compatibilty of $T$
| = | $R^{[0]}[E^{[0]}[E^{[1]}[\bigcup_{y\in Y}E^{[0]}[T^{[0]}[y]]]]]$ | Lemma 1 (v)
| = | $R^{[0]}[\bigcup_{y\in Y}E^{[0]}[T^{[0]}[y]]]$ |  $E$-compatibilty of $R$
| = | $\bigcap_{y\in Y}R^{[0]}[E^{[0]}[T^{[0]}[y]]]$ | Lemma 1 (v)
| = | $\bigcap_{y\in Y}(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[y]$ | Definition 14 (i)
| = |  $(R\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}T)^{[0]}[Y]$. | Lemma 1(v)

4\. Immediate consequence of item 3.

###### Remark 2

In general, $\ast$-composition is not associative; let us build a
counterexample to $R\ast(T\ast U)=(R\ast T)\ast U$. Let
$\mathbb{G}=(Z,\Delta)$, such that $Z=\\{z_{1},z_{2}\\}$. let $R,U,T\subseteq
Z\times Z$ such that $R=Z\times Z$, $U=\varnothing$, and $T=\Delta$,
respectively. Since $E=\Delta$, every set is Galois-stable, hence all three
relations are $E$-compatible. For any $x\in Z$,

$R^{[0]}[(T\,\ast U)^{[0]}[x]]$ | = | $R^{[0]}[T^{[0]}[U^{[0]}[x]]]$ | Definition
---|---|---|---
| = | $R^{[0]}[T^{[0]}[Z]]$ | $U=\varnothing$
| = | $R^{[0]}[\\{b\in Z\mid\forall w(w\in Z\Rightarrow b\Delta^{c}w)\\}]$ | $T=\Delta$
| = | $R^{[0]}[\varnothing]$ |
| = | $\\{b\in Z\mid\forall w(w\in\varnothing\Rightarrow bR^{c}w)\\}$ |
| = | $Z$ |

$(R\,\ast T)^{[0]}[U^{[0]}[x]]$ | = | $(R\,\ast T)^{[0]}[Z]$ | $U=\varnothing$
---|---|---|---
| = | $\\{b\in Z\mid\forall w(w\in Z\Rightarrow b(R\,\ast T)^{c}w)\\}$ | Definition of $(-)^{[0]}$
| = | $\\{b\in Z\mid\forall w(w\in Z\Rightarrow b\in R^{[0]}[T^{[0]}[w]])\\}$ | Definition of $\ast$
| = | $\bigcap_{w\in Z}R^{[0]}[T^{[0]}[w]]$ |
| = | $\bigcap_{w\in Z}R^{[0]}[Z\setminus\\{w\\}]$ | $T=\Delta$
| = | $R^{[0]}[\bigcup_{w\in Z}Z\setminus\\{w\\}]$ | Lemma 1
| = | $R^{[0]}[Z]$ |
| = | $\\{b\in Z\mid\forall w(w\in Z\Rightarrow bR^{c}w)\\}$ |
| = | $\varnothing$ | $R=Z\times Z$

###### Remark 3

In general, $\ast$-composition is not associative. It is easy to show a
counterexample analogous to the one in Remark 2 which its natural counterpart
in Kripke frames. To simplify notation, we will write e.g. $R\ast T\ast U$
which should be read as $(R\ast(T\ast U))$.

###  5.2 (Heterogeneous) relation algebras and their propositional languages

In this section, we introduce algebraic structures in the context of which the
notions of composition introduced above can be studied systematically from a
universal-algebraic or category-theoretic perspective. Besides being of
potential independent interest, these structures can be naturally associated
with propositional languages which are key tools to build a common ground
where the first-order correspondents of modal axioms in various semantic
contexts can be compared and systematically related.

###### Definition 15

The relation algebras associated with any graph-based frame
$\mathbb{F}=(Z,E,R_{\Diamond},R_{\Box})$, and any Kripke frame
$\mathbb{X}=(W,R_{\Diamond},R_{\Box})$ are respectively defined as follows:

$\mathbb{F}^{\ast}:=(\mathcal{P}(Z\times
Z),E,D,R_{\Diamond},R_{\Diamondblack},R_{\Box},R_{\blacksquare},{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E},{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E},\ast)$,
$\quad\mathbb{X}^{\ast}:=(\mathcal{P}(W\times
W),\Delta,R_{\Diamond},R_{\Diamondblack},R_{\Box},R_{\blacksquare},\circ,\star),$

where $R_{\Diamondblack}$ and $R_{\blacksquare}$ denote the converse relations
of $R_{\Box}$ and $R_{\Diamond}$ respectively, the binary operations
${\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E},{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}$
and $\ast$ are defined as in Definition 14, the binary operation $\circ$ is
the standard relational composition, and $\star$ is defined by the same
assignment as $\ast$.

Consider the set
$\mathsf{Rel}_{\mathcal{L}}:=\\{\Delta,E,D,R_{\Diamond},R_{\Diamondblack},R_{\Box},R_{\blacksquare}\\}$
of constant symbols. The propositional languages $\mathsf{KRel}_{\mathcal{L}}$
and $\mathsf{GRel}_{\mathcal{L}}$ associated with Kripke frames (resp. graph-
based frames) are defined by the following recursions:

$\displaystyle\mathsf{KRel}_{\mathcal{L}}\ni\xi::=$ $\displaystyle\,\Delta\mid
R_{\Diamond}\mid R_{\Diamondblack}\mid R_{\Box}\mid
R_{\blacksquare}\mid\xi\circ\xi\mid\xi\star\xi,$
$\displaystyle\mathsf{GRel}_{\mathcal{L}}\ni\alpha::=$ $\displaystyle\,D\mid
E\mid R_{\Diamond}\mid R_{\Diamondblack}\mid R_{\Box}\mid
R_{\blacksquare}\mid\alpha\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}\alpha\mid\alpha\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}\alpha\mid\alpha\,\ast\alpha,$

where the intended interpretation of the constant symbols on graph-based
frames and on Kripke frames is the obvious one. Term inequalities of
$\mathsf{KRel}_{\mathcal{L}}$ (resp. $\mathsf{GRel}_{\mathcal{L}}$ ) are
written as $\xi_{1}\subseteq\xi_{2}$ (resp. $\alpha_{1}\subseteq\alpha_{2})$
and are interpreted on Kripke frames (resp. graph-based frames) in the obvious
way. In particular,

$\mathbb{X}\models\xi_{1}\subseteq\xi_{2}\quad\text{ iff
}\quad\mathbb{X}^{\ast}\models\xi_{1}\subseteq\xi_{2}\quad\text{and}\quad\mathbb{F}\models\alpha_{1}\subseteq\alpha_{2}\quad\text{
iff }\quad\mathbb{F}^{\ast}\models\alpha_{1}\subseteq\alpha_{2}.$

A natural translation exists between $\mathsf{GRel}_{\mathcal{L}}$-terms and
$\mathsf{KRel}_{\mathcal{L}}$-terms which is defined as follows.

###### Definition 16

Let $\tau:\mathsf{GRel}_{\mathcal{L}}\to\mathsf{KRel}_{\mathcal{L}}$ be
defined as follows:

$\tau(E)$ | $=$ | $\Delta$ |  | $\tau(D)$ | $=$ | $\Delta$
---|---|---|---|---|---|---
$\tau(R_{\Diamond})$ | $=$ | $R_{\Diamond}$ |  | $\tau(R_{\Diamondblack})$ | $=$ | $R_{\Diamondblack}$
$\tau(R_{\Box})$ | $=$ | $R_{\Box}$ |  | $\tau(R_{\blacksquare})$ | $=$ | $R_{\blacksquare}$
$\tau(\alpha_{1}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}\alpha_{2})$ | $=$ | $\tau(\alpha_{1})\circ\tau(\alpha_{2})$ |  | $\tau(\alpha_{1}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}\alpha_{2})$ | $=$ | $\tau(\alpha_{1})\circ\tau(\alpha_{2})$
$\tau(\alpha_{1}\ast\alpha_{2})$ | $=$ | $\tau(\alpha_{1})\star\tau(\alpha_{2})$ |  | $\tau(\alpha_{1}\ast\alpha_{2})$ | $=$ |  $\tau(\alpha_{1})\star\tau(\alpha_{2})$.

###### Lemma 9

For any Kripke frame $\mathbb{X}$, any
$\mathsf{GRel}_{\mathcal{L}}$-inequality $\alpha_{1}\subseteq\alpha_{2}$, and
any $\alpha\in\mathsf{GRel}_{\mathcal{L}}$

  1. 1.

$\alpha^{\mathbb{F_{X}}}=\tau(\alpha)^{\mathbb{X}}$,

  2. 2.

$\mathbb{F_{X}}\models\alpha_{1}\subseteq\alpha_{2}\quad\quad\mbox{iff}\quad\quad\mathbb{X}\models\tau(\alpha_{1})\subseteq\tau(\alpha_{2}).$

###### Proof

Item 1 is proved by straightforward induction on the complexity of $\alpha$.
Item 2 directly follows from 1.

In the next section we represent the first-order correspondents of inductive
mrps as term inequalities of $\mathsf{GRel}_{\mathcal{L}}$ and
$\mathsf{KRel}_{\mathcal{L}}$. Intuitively, the various compositions
considered above are used as “abbreviations” to achieve a more compact
representation of the correspondents which is also more amenable to
computation.

##  6 Correspondents of inductive modal reduction principles

With the definitions of the previous section in place, we are now in a
position to give a concrete representation of the first-order correspondents
of inductive mrps on graph-based $\mathcal{L}$-frames and on Kripke
$\mathcal{L}$-frames as term-inequalities in the languages
$\mathsf{GRel}_{\mathcal{L}}$ and $\mathsf{KRel}_{\mathcal{L}}$. This
representation also puts us in a position to show that these two
representations are naturally connected in the same way in which Kripke frames
are connected to graph-based frames. Specifically, in the following two
subsections, we show that

###### Proposition 6

The first-order correspondent of any inductive mrp on graph-based (resp.
Kripke) frames can be represented as a term inequality in
$\mathsf{GRel}_{\mathcal{L}}$ (resp. $\mathsf{KRel}_{\mathcal{L}}$).

In Section 6.3, we also show that the first-order correspondent on graph-based
$\mathcal{L}$-frames of any inductive mrp is the “shifted” version of its
first-order correspondent on Kripke $\mathcal{L}$-frames.

###  6.1 Correspondents on graph-based frames

###### Definition 17

Let us associate terms in $\mathsf{GRel}_{\mathcal{L}}$ with
${\mathcal{L}^{*}}$-terms of certain syntactic shapes as follows:

  1. 1.

if $\varphi(!w)$ (resp. $\psi(!w)$) is a finite (possibly empty) concatenation
of diamond (resp. box) connectives, let us define
$R_{\varphi}\in\mathsf{GRel}_{\mathcal{L}}$ (resp.
$R_{\psi}\in\mathsf{GRel}_{\mathcal{L}}$) by induction on $\varphi$ (resp.
$\psi$) as follows:
if $\varphi:=y$, then $R_{\varphi}:=D$; if $\varphi:=f\varphi^{\prime}$ with
$f\in\\{\Diamond,\Diamondblack\\}$, then
$R_{\varphi}:=R_{f}{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi^{\prime}}$;
if $\psi:=y$, then $R_{\psi}:=E$; if $\psi:=g\psi^{\prime}$ with
$g\in\\{\Box,\blacksquare\\}$, then
$R_{\psi}:=R_{g}{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi^{\prime}}$;

  2. 2.

if $\chi(!w)=\varphi_{1}\psi_{1}\ldots\varphi_{n_{\chi}}\psi_{n_{\chi}}(!w)$
such that each $\varphi_{i}$ (resp. $\psi_{i}$) is a finite concatenation of
diamond (resp. box) connectives of which only $\psi_{n_{\chi}}$ is possibly
empty, then $R_{\chi}\in\mathsf{GRel}_{\mathcal{L}}$ is defined as follows:
if $\psi_{n_{\chi}}$ is empty, $R_{\chi}\coloneqq R_{\varphi_{1}}\ast
R_{\psi_{1}}\ast\cdots\ast R_{\varphi_{n_{\chi}}};\\\ $ if $\psi_{n_{\chi}}$
is nonempty, $R_{\chi}\coloneqq R_{\varphi_{1}}\ast R_{\psi_{1}}\ast\cdots\ast
R_{\varphi_{n_{\chi}}}\ast R_{\psi_{n_{\chi}}}\ast D;$

  3. 3.

if
$\zeta(!w)=\psi_{1}\varphi_{1}\ldots\psi_{n_{\zeta}}\varphi_{n_{\zeta}}(!w)$
such that each $\varphi_{i}$ (resp. $\psi_{i}$) is a finite concatenation of
diamond (resp. box) connectives, of which only $\varphi_{n_{\zeta}}$ is
possibly empty, then $R_{\zeta}\in\mathsf{GRel}_{\mathcal{L}}$ is defined as
follows:
if $\varphi_{n_{\zeta}}$ is empty, $R_{\zeta}\coloneqq R_{\psi_{1}}\ast
R_{\varphi_{1}}\ast\cdots\ast R_{\psi_{n_{\zeta}}};$
if $\varphi_{n_{\zeta}}$ is nonempty, $R_{\zeta}\coloneqq R_{\psi_{1}}\ast
R_{\varphi_{1}}\ast\cdots\ast R_{\psi_{n_{\zeta}}}\ast
R_{\varphi_{n_{\zeta}}}\ast E.$

The first item of the following lemma shows that the semantic operations
induced by the relations introduced in Definition 17 coincide with the term
functions induced by their associated formulas. As is to be expected, this
strong property does not fully extend to formulas of a more general shape such
as $\chi$ and $\zeta$; however, a more limited version applies for singleton
subsets. ††margin:  MP: expand proof

###### Lemma 10

For any graph-based frame $\mathbb{F}$ based on $(Z,E)$, all terms
$\varphi(!t)$, $\psi(!t)$, $\chi(!t)$, $\zeta(!t)$ as in Definition 17, all
$B,Y\subseteq Z$, and all $a,x\in Z$,

  1. 1.

$(\\![{\varphi(!t)}]\\!)(t\coloneqq(B^{[10]},B^{[1]})=R^{[0]}_{\varphi}[B]$
and $[\\![{\psi(!t)}]\\!](t\coloneqq Y=(Y^{[0]},Y^{[01]}))=R^{[0]}_{\psi}[Y]$;

  2. 2.

$(\\![{\chi[\mathbf{j}/!t]}]\\!)(\mathbf{j}\coloneqq(a^{[10]},a^{[1]}))=R^{[0]}_{\chi}[a^{[10]}]=R^{[0]}_{\chi}[a];$

  3. 3.

$[\\![{\zeta[\mathbf{m}/!t]}]\\!](\mathbf{m}\coloneqq(x^{[0]},x^{[01]})=R^{[0]}_{\zeta}[x^{[01]}]=R^{[0]}_{\zeta}[x].$

###### Proof

Item (1) can be shown straightforwardly by induction on $\varphi$ and $\psi$,
using Lemma 8 (2 and 3). Items (2) and (3) can be shown by induction on the
number of alternations of box and diamond connectives, using item (1), and
Definition 14.

As discussed in Section 2.5, the ALBA output of mrps of type (a) is

$\forall\mathbf{j}\left(\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]\leq\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]\right).$

When interpreted on graph-based frames, the condition above translates as
follows:

$\forall
a\left((\\![{\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]}]\\!)(\mathbf{j}:=(a^{[10]},a^{[1]}))\subseteq(\\![{\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]}]\\!)(\mathbf{j}:=(a^{[10]},a^{[1]})\right).$
(3)

Since $\mathsf{LA}(\psi)[\varphi(!y)/!u]$ and $\chi[\mathsf{LA}(\alpha)/p]$
are of the shape required by by items (1) and (2) of Lemma 10 respectively,
the following identities hold:

$(\\![{\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]}]\\!)(\mathbf{j}:=(a^{[10]},a^{[1]})$ | $=$ | $R_{\mathsf{LA}(\psi)[\varphi/!u]}^{[0]}[a^{[10]}]$ | $=$ |  $(R_{\mathsf{LA}(\psi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi})^{[0]}[a]$.
---|---|---|---|---
$(\\![{\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]}]\\!)(\mathbf{j}:=(a^{[10]},a^{[1]}))$ | $=$ | $R_{\chi[\mathsf{LA}(\alpha)/p]}^{[0]}[a^{[10]}]$ | $=$ |  $R_{\chi[\mathsf{LA}(\alpha)/p]}^{[0]}[a]$.

Hence, (3) can be rewritten as follows:

$\forall
a\left(R_{\chi[\mathsf{LA}(\alpha)/p]}^{[0]}[a]\subseteq(R_{\mathsf{LA}(\psi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi})^{[0]}[a]\right)\quad\text{i.e.}\quad
R_{\mathsf{LA}(\psi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi}\subseteq
R_{\chi[\mathsf{LA}(\alpha)/p]}$ (4)

Similarly, the ALBA output of mrps of type (b) can be represented as follows:

$\forall\mathbf{m}\left(\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]\leq\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]\right),$

and, when interpreted on graph-based frames, the condition translates as
follows:

$\forall
x\left([\\![{\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]}]\\!](\mathbf{m}:=(x^{[0]},x^{[01]}))\subseteq[\\![{\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]}]\\!](\mathbf{m}:=(x^{[0]},x^{[01]}))\right).$
(5)

By items (3) and (1) of Lemma 10,

$[\\![{\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]}]\\!](\mathbf{m}:=(x^{[0]},x^{[01]}))$ | $=$ | $R_{\mathsf{RA}(\varphi)[\psi/!u]}^{[0]}[x^{[01]}]$ | $=$ |  $(R_{\mathsf{RA}(\varphi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi})^{[0]}[x]$.
---|---|---|---|---
$[\\![{\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]}]\\!](\mathbf{m}:=(x^{[0]},x^{[01]}))$ | $=$ | $R_{\zeta[\mathsf{RA}(\delta)/p]}^{[0]}[x^{[01]}]$ | $=$ |  $R_{\zeta[\mathsf{RA}(\delta)/p]}^{[0]}[x]$.

Therefore, we can rewrite (5) as follows:

$\forall
x\left(R_{\zeta[\mathsf{RA}(\delta)/p]}^{[0]}[x]\subseteq(R_{\mathsf{RA}(\varphi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi})^{[0]}[x]\right)\quad\text{i.e.}\quad
R_{\mathsf{RA}(\varphi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi}\subseteq
R_{\zeta[\mathsf{RA}(\delta)/p]}.$ (6)

Finally, notice that, if the mrp is also analytic, the shape of $\chi(p)$
(resp. $\zeta(p)$) simplifies to
$\chi(p)=\varphi_{n_{\chi}}\psi_{n_{\chi}}(p)$ with $n_{\chi}=1$ and
$\psi_{n_{\chi}}$ empty (resp.
$\zeta(p)=\psi_{n_{\zeta}}\varphi_{n_{\zeta}}(p)$ with $n_{\zeta}=1$ and
$\varphi_{n_{\zeta}}$ empty). Hence, (4) and (6) simplify to the following
inclusions:

$R_{\mathsf{LA}(\psi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi}\subseteq
R_{\varphi_{n_{\chi}}}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\mathsf{LA}(\alpha)}\quad\quad
R_{\mathsf{RA}(\varphi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi}\subseteq
R_{\psi_{n_{\zeta}}}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\mathsf{RA}(\delta)}.$
(7)

###### Example 2

The mrp $p\leq\Diamond\Box p$ is inductive of type (a), where $\varphi(y):=y$,
and $\alpha(p):=p$, hence $\mathsf{LA}(\alpha)(u):=u$, and $\psi(x):=x$, hence
$\mathsf{LA}(\psi)(v):=v$, and $\chi(p):=\Diamond\Box p$. Then the ALBA output
of this inequality is

| $\forall\mathbf{j}\left([[\mathbf{j}/y]/v]\leq\Diamond\Box[[\mathbf{j}/u]/p]\right),$ |
---|---|---
iff | $\forall\mathbf{j}\left(\mathbf{j}\leq\Diamond\Box\mathbf{j}\right)$ |
iff | $\forall\mathbf{j}\left((\\![{\Diamond\Box\mathbf{j}}]\\!)\subseteq(\\![{\mathbf{j}}]\\!)\right)$ | (definition of order on polarities)
iff | $\forall a\left(R_{\Diamond}^{[0]}[R_{\Box}^{[0]}[E^{[1]}[a]]]\subseteq E^{[1]}[a]\right)$ | (standard translation)
iff | $\forall a\left((R_{\Diamond}\,\ast R_{\Box}\,\ast D)^{[0]}[a]\subseteq({D})^{[0]}[a]\right)$ |  (Definition 14)
iff | $D\subseteq R_{\Diamond}\,\ast R_{\Box}\,\ast D.$ |  (Lemma 1)

###### Example 3

The mrp $\Box\Diamond p\leq\Box\Diamond\Diamond p$ is inductive of shape (b)
with $\varphi(y):=y$, hence $\mathsf{RA}(\varphi)(v):=v$ and $\psi(x):=\Box
x$, and $\delta(p):=\Diamond\Diamond p$, hence
$\mathsf{RA}(\delta)(u):=\blacksquare\blacksquare u$, and
$\chi(p):=\Box\Diamond p$.

| $\forall p[\Box\Diamond p\leq\Box\Diamond\Diamond p]$ |
---|---|---
iff | $\forall\mathbf{m}[\Box\Diamond\blacksquare\blacksquare\mathbf{m}\leq\Box\mathbf{m}]$ | ALBA output
i.e. | $\forall x\left(R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[x^{\downarrow\uparrow}]]]]\subseteq R_{\Box}^{[0]}[x^{\downarrow\uparrow}]\right)$ |
iff | $\forall x\left(R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[x]]]]]\subseteq R_{\Box}^{[0]}[x]\right)$ |  ($R_{\Box}$ and $R_{\Diamond}$ $E$-compatible)
iff | $\forall x\forall a\left(a\in R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[E^{[1]}[R_{\blacksquare}^{[0]}[x]]]]]\Rightarrow a\in R_{\Box}^{[0]}[x]\right)$ |
iff | $\forall x\forall a\left(a(R_{\Box}\,\ast R_{\Diamond}\,\ast(R_{\blacksquare}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\blacksquare}))^{c}x\Rightarrow aR_{\Box}^{c}x\right)$ |
iff |  $R_{\Box}\subseteq R_{\Box}\,\ast R_{\Diamond}\,\ast(R_{\blacksquare}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\blacksquare})$. |

###  6.2 Correspondents on Kripke frames

In the present subsection, which is an adaptation of [20, Section 4.2], we
specialize the discussion of the previous subsection to the environment of
Kripke frames, so as to obtain a specific representation of the first-order
correspondents of inductive mrps on Kripke frames as pure inclusions of binary
relations on Kripke frames.

###### Definition 18

Let us associate terms in $\mathsf{KRel}_{\mathcal{L}}$ with
${\mathcal{L}}^{*}$-terms of certain syntactic shapes as follows:

  1. 1.

if $\varphi(!w)$ (resp. $\psi(!w)$) is a finite (possibly empty) concatenation
of diamond (resp. box) connectives, let us define
$R_{\varphi}\in\mathsf{KRel}_{\mathcal{L}}$ (resp.
$R_{\psi}\in\mathsf{KRel}_{\mathcal{L}}$) by induction on $\varphi$ (resp.
$\psi$) as follows:
if $\varphi:=y$, then $R_{\varphi}:=\Delta$; if $\varphi:=f\varphi^{\prime}$
with $f\in\\{\Diamond,\Diamondblack\\}$, then $R_{\varphi}:=R_{f}\circ
R_{\varphi^{\prime}}$.
if $\psi:=y$, then $R_{\psi}:=\Delta$; if $\psi:=g\psi^{\prime}$ with
$g\in\\{\Box,\blacksquare\\}$, then $R_{\psi}:=R_{g}\circ R_{\psi^{\prime}}$.

  2. 2.

if $\chi(!w)=\varphi_{1}\psi_{1}\ldots\varphi_{n_{\chi}}\psi_{n_{\chi}}(!w)$
such that each $\varphi_{i}$ (resp. $\psi_{i}$) is a finite concatenation of
diamond (resp. box) connectives, of which only $\psi_{n_{\chi}}$ is possibly
empty. Let us define $R_{\chi}\in\mathsf{KRel}_{\mathcal{L}}$ by induction on
$n_{\chi}$ as follows:
if $\psi_{n_{\chi}}$ is empty, $R_{\chi}\coloneqq R_{\varphi_{1}}\star
R_{\psi_{1}}\star\cdots\star R_{\varphi_{n_{\chi}}};$
if $\psi_{n_{\chi}}$ is nonempty, $R_{\chi}\coloneqq R_{\varphi_{1}}\star
R_{\psi_{1}}\star\cdots\star R_{\varphi_{n_{\chi}}}\star
R_{\psi_{n_{\chi}}}\star\Delta$ .

  3. 3.

if
$\zeta(!w)=\psi_{1}\varphi_{1}\ldots\psi_{n_{\zeta}}\varphi_{n_{\zeta}}(!w)$
such that each $\varphi_{i}$ (resp. $\psi_{i}$) is a finite concatenation of
diamond (resp. box) connectives, of which only $\varphi_{n_{\zeta}}$ is
possibly empty. Let us define $R_{\zeta}\in\mathsf{KRel}_{\mathcal{L}}$ by
induction on $n_{\zeta}$ as follows:
if $\varphi_{n_{\zeta}}$ is empty, $R_{\zeta}\coloneqq R_{\psi_{1}}\star
R_{\varphi_{1}}\star\cdots\star R_{\psi_{n_{\zeta}}};$
if $\varphi_{n_{\zeta}}$ is nonempty, $R_{\zeta}\coloneqq R_{\psi_{1}}\star
R_{\varphi_{1}}\star\cdots\star R_{\psi_{n_{\zeta}}}\star
R_{\varphi_{n_{\zeta}}}\star\Delta$ .

The next lemma is a Kripke-frame analogue of Lemma 10.

###### Lemma 11

For any Kripke frame $\mathbb{X}$ based on $W$, all terms $\varphi(!w)$,
$\psi(!w)$, $\chi(!w)$, and $\zeta(!w)$ as in Definition 18, any $S\subseteq
W$, and any $a,x\in W$,

  1. 1.

$[\\![{\varphi(!w)}]\\!](w\coloneqq S)=\langle R_{\varphi}\rangle
S\quad\text{and}\quad[\\![{\psi(!w)}]\\!](w\coloneqq S)=[R_{\psi}]S.$

  2. 2.

$[\\![{\chi[\mathbf{j}/!w]}]\\!](\mathbf{j}\coloneqq\\{a\\})=\langle
R_{\chi}\rangle\\{a\\}.$

  3. 3.

$[\\![{\zeta[\mathbf{m}/!w]}]\\!](\mathbf{m}\coloneqq\\{x\\}^{c})=[R_{\zeta}]\\{x\\}^{c}.$

###### Proof

Item (1) is proved by induction on the complexity of $\varphi$ and $\psi$
respectively. As to item (2), we proceed by induction on the number of
alternations of boxes and diamonds in $\chi$. If $\chi=w$, $R_{\chi}=\Delta$,
so the statement follows trivially. For the inductive case, $\chi\neq x$, and
then $\chi=\varphi_{1}\psi_{1}\cdots\varphi_{n}\psi_{n}(!x)$ such that $n\geq
1$, and the $\varphi_{i}$ (resp. $\psi_{i}$) are finite, nonempty,
concatenations of diamond (resp. box) operators, except for $\psi_{n}$ which
is possibly empty. If $n=1$ and $\psi_{1}$ empty, then
$R_{\chi}=R_{\varphi_{1}}$, hence the statement follows from item (1). If
$n=1$ and $\psi_{1}(!z)$ is not empty, then, $R_{\chi}=R_{\varphi_{1}}\star
R_{\psi_{1}}\star\Delta$, so:

| $[\\![{\chi[\mathbf{j}/x]}]\\!](\mathbf{j}\coloneqq\\{a\\})$ |
---|---|---
$=$ | $[\\![{\varphi_{1}(!y)}]\\!](y\coloneqq[\\![{\psi_{1}[\mathbf{j}/z]}]\\!](\mathbf{j}\coloneqq\\{a\\}))$ |
$=$ | $\langle R_{\varphi_{1}}\rangle[\\![{\psi_{1}[\mathbf{j}/z]}]\\!](\mathbf{j}\coloneqq\\{a\\})$ | item (1)
$=$ | $\langle R_{\varphi_{1}}\rangle[R_{\psi_{1}}]\\{a\\}$ | item (1)
$=$ | $\langle R_{\varphi_{1}}\rangle R^{[0]}_{\psi_{1}}[\\{a\\}^{c}]$ |  Lemma 2
$=$ | $(R^{[0]}_{\varphi_{1}}[R^{[0]}_{\psi_{1}}[\\{a\\}^{c}]])^{c}$ |  Lemma 2
$=$ | $(R^{[0]}_{\varphi_{1}}[R^{[0]}_{\psi_{1}}[\Delta^{[0]}[a]]])^{c}$ | $\Delta^{[0]}[a]=\\{a\\}^{c}$
$=$ | $((R_{\varphi_{1}}\star R_{\psi_{1}}\star\Delta)^{[0]}[a])^{c}$ |  Definition 14
$=$ | $(R_{\chi}^{[0]}[a])^{c}$ | $\chi=\varphi_{1}\psi_{1}$
$=$ | $\langle R_{\chi}\rangle\\{a\\}$ |  Lemma 2

The proof of the inductive step and of item (3) is similar, and is omitted.

As discussed in Section 2.5, the ALBA output of mrps of type (a) is

$\forall\mathbf{j}\left(\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]\leq\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]\right).$

When interpreted on Kripke frames, the condition above translates as follows:

$\forall
a\left([\\![{\mathsf{LA}(\psi)[\varphi[\mathbf{j}/!y]/!u]}]\\!](\mathbf{j}:=\\{a\\})\subseteq[\\![{\chi[\mathsf{LA}(\alpha)[\mathbf{j}/!u]/p]}]\\!](\mathbf{j}:=\\{a\\})\right).$
(8)

Since $\mathsf{LA}(\psi)[\varphi(!y)/!u]$ and $\chi[\mathsf{LA}(\alpha)/p]$
are of the shape required by by items (i) and (ii) of Lemma 11 respectively,
(8) can be rewritten as follows

$\forall a\left((R_{\mathsf{LA}(\psi)}\,\circ R_{\varphi})^{-1}[a]\subseteq
R_{\chi[\mathsf{LA}(\alpha)/p]}^{-1)}[a]\right)\quad\text{i.e.}\quad
R_{\mathsf{LA}(\psi)}\,\circ R_{\varphi}\subseteq
R_{\chi[\mathsf{LA}(\alpha)/p]}.$ (9)

Similarly, the ALBA output of mrps of type (b) is

$\forall\mathbf{m}\left(\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]\leq\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]\right),$

and, when interpreted on Kripke frames, the condition translates as follows:

$\forall
x\left([\\![{\zeta[\mathsf{RA}(\delta)[\mathbf{m}/!u]/p]}]\\!](\mathbf{m}:=\\{x\\}^{c})\subseteq[\\![{\mathsf{RA}(\varphi)[\psi[\mathbf{m}/!y]/!u]}]\\!](\mathbf{m}:=\\{x\\}^{c})\right).$
(10)

By items (3) and (1) of Lemma 11, Lemma 2, and contraposition, we can rewrite
(10) as follows:

$\forall x\left((R_{\mathsf{RA}(\varphi)}\,\circ R_{\psi})^{-1}[x]\subseteq
R_{\zeta[\mathsf{RA}(\delta)/p]}^{-1}[x]\right)\quad\text{i.e.}\quad
R_{\mathsf{RA}(\varphi)}\,\circ R_{\psi}\subseteq
R_{\zeta[\mathsf{RA}(\delta)/p]}.$ (11)

Finally, notice that, if the mrp is also analytic, the shape of $\chi(p)$
(resp. $\zeta(p)$) simplifies to
$\chi(p)=\varphi_{n_{\chi}}\psi_{n_{\chi}}(p)$ with $n_{\chi}=1$ and
$\psi_{n_{\chi}}$ empty (resp.
$\zeta(p)=\psi_{n_{\zeta}}\varphi_{n_{\zeta}}(p)$ with $n_{\zeta}=1$ and
$\varphi_{n_{\zeta}}$ empty). Hence, (9) and (11) simplify to the following
inclusions:

$R_{\mathsf{LA}(\psi)}\,\circ R_{\varphi}\subseteq
R_{\varphi_{n_{\chi}}}\,\circ R_{\mathsf{LA}(\alpha)}\quad\quad
R_{\mathsf{RA}(\varphi)}\,\circ R_{\psi}\subseteq R_{\psi_{n_{\zeta}}}\,\circ
R_{\mathsf{RA}(\delta)}.$ (12)

###### Example 4

The mrp $p\leq\Diamond\Box p$ is inductive of type (a), where $\varphi(y):=y$,
and $\alpha(p):=p$, hence $\mathsf{LA}(\alpha)(u):=u$, and $\psi(x):=x$, hence
$\mathsf{LA}(\psi)(v):=v$, and $\chi(p):=\Diamond\Box p$. Then the ALBA output
of this inequality is

| $\forall\mathbf{j}\left([[\mathbf{j}/y]/v]\leq\Diamond\Box[[\mathbf{j}/u]/p]\right)$ |
---|---|---
iff | $\forall\mathbf{j}\left(\mathbf{j}\leq\Diamond\Box\mathbf{j}\right)$ |
iff | $\forall\mathbf{j}\left((\\![{\Diamond\Box\mathbf{j}}]\\!)\subseteq(\\![{\mathbf{j}}]\\!)\right)$ | (Definition of order on polarities)
iff | $\forall a\left(R_{\Diamond}^{[0]}[R_{\Box}^{[0]}[a^{c}]]\subseteq a^{c}\right)$ | (Standard translation)
iff | $\forall a\left(R_{\Diamond}^{[0]}[R_{\Box}^{[0]}[\Delta^{[0]}[a]]]\subseteq\Delta^{[0]}[a]\right)$ |  (Definition of $\Delta$)
iff | $\forall a\left((R_{\Diamond}\,\star R_{\Box}\,\star\Delta)^{[0]}[a]\subseteq\Delta^{[0]}[a]\right)$ |  (Definition 14)
iff | $\forall x\forall a\left(x(R_{\Diamond}\,\star R_{\Box}\,\star\Delta)^{c}a\subseteq x\Delta^{c}[a]\right)$ |  (Definition of $(\cdot)^{[0]}$)
iff | $\Delta\subseteq R_{\Diamond}\,\star R_{\Box}\,\star\Delta$ |  (Lemma 1)

###### Example 5

The mrp $\Box\Diamond p\leq\Box\Diamond\Diamond p$ is inductive of shape (b)
with $\varphi(y):=y$, hence $\mathsf{RA}(\varphi)(v):=v$ and $\psi(x):=\Box
x$, and $\delta(p):=\Diamond\Diamond p$, hence
$\mathsf{RA}(\delta)(u):=\blacksquare\blacksquare u$, and
$\chi(p):=\Box\Diamond p$.

| $\forall p[\Box\Diamond p\leq\Box\Diamond\Diamond p]$ |
---|---|---
iff | $\forall\mathbf{m}[\Box\Diamond\blacksquare\blacksquare\mathbf{m}\leq\Box\mathbf{m}]$ | ALBA output
i.e. | $\forall x\left(R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[\Delta^{[1]}[R_{\blacksquare}^{[0]}[x^{[01]]}]]]]\subseteq R_{\Box}^{[0]}[x^{[01]}]\right)$ |
iff | $\forall x\left(R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[\Delta^{[1]}[R_{\blacksquare}^{[0]}[x]]]]]\subseteq R_{\Box}^{[0]}[x]\right)$ |  ($R_{\Box}$ and $R_{\Diamond}$ $\Delta$-compatible)
iff | $\forall x\forall a\left(a\in R^{[0]}_{\Box}[R^{[0]}_{\Diamond}[R_{\blacksquare}^{[0]}[\Delta^{[1]}[R_{\blacksquare}^{[0]}[x]]]]]\Rightarrow a\in R_{\Box}^{[0]}[x]\right)$ |
iff | $\forall x\forall a\left(a(R_{\Box}\,\star R_{\Diamond}\,\star(R_{\blacksquare}\,\circ R_{\blacksquare}))^{c}x\Rightarrow aR_{\Box}^{c}x\right)$ |
iff |  $R_{\Box}\subseteq R_{\Box}\,\star R_{\Diamond}\,\star(R_{\blacksquare}\,\circ R_{\blacksquare})$. |

###  6.3 Shifting Kripke frames to graph-based frames

In the two previous subsections, we have shown that, both in the setting of
graph-based frames and in that of Kripke frames, the first-order
correspondents of inductive mrps can be expressed as pure inclusions of
(compositions, pseudo compositions, $E$-mediated compositions of) binary
relations associated with certain terms. Besides providing a more compact way
to represent first-order sentences, this relational representation has also
specific correspondence-theoretic consequences: it allows us to formulate and
establish a systematic connection between the first-order correspondents, in
the two semantic settings, of any inductive mrp. Establishing this connection
is the focus of the present subsection. Specifically, we show that, for any
inductive mrp $s(p)\leq t(p)$, its first-order correspondent on graph-based
frames is the “shifted version" (in a sense that will be made precise below)
of its first-order correspondent on Kripke frames. That is, thanks to the
relational representation, the interesting phenomenon observed in [21,
Proposition 5] in the context of polarity-based frames and in [19, Proposition
4] in the context of graph-based frames can be generalized (and made much more
explicit in the process) to all inductive mrps.

For any $\xi\in\mathsf{KRel}_{\mathcal{L}}$ (resp.
$\gamma\in\mathsf{GRel}_{\mathcal{L}}$), let $\xi^{\mathbb{X}}$ (resp.
$\gamma^{\mathbb{F}}$) denote the interpretation of $\xi$ (resp. $\gamma$) in
$\mathbb{X}$ (resp. $\mathbb{F}$).

###### Definition 19

The $\mathsf{GRel}_{\mathcal{L}}$-inequality $\gamma_{1}\subseteq\gamma_{2}$
is the shifting of the $\mathsf{KRel}_{\mathcal{L}}$-inequality
$\xi_{1}\subseteq\xi_{2}$ if, for any Kripke frame $\mathbb{X}$,

$\xi_{1}^{\mathbb{X}}=\gamma_{1}^{\mathbb{F_{X}}}\quad\text{ and
}\quad\xi_{2}^{\mathbb{X}}=\gamma_{2}^{\mathbb{F_{X}}}.$

###### Example 6

The $\mathsf{GRel}_{\mathcal{L}}$-inequality $E\subseteq R_{\Box}$ is the
shifting of the $\mathsf{KRel}_{\mathcal{L}}$-inequality $\Delta\subseteq
R_{\Box}$ (encoding the reflexivity of $R_{\Box}$). Indeed, $\Delta\subseteq
R_{\Box}$ instantiates $E\subseteq R_{\Box}$ on all graph-based frames with
$E\coloneqq\Delta$, which are exactly the shifted Kripke frames.

The $\mathsf{GRel}_{\mathcal{L}}$-inequality
$R_{\Box}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\Box}\subseteq
R_{\Box}$ is the shifting of the $\mathsf{KRel}_{\mathcal{L}}$-inequality
$R_{\Box}\circ R_{\Box}\subseteq R_{\Box}$ (encoding the transitivity of
$R_{\Box}$) on Kripke frames. Indeed, by Lemma 7, $R_{\Box}\circ
R_{\Box}\subseteq R_{\Box}$ is the instantiation of
$R_{\Box}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\Box}\subseteq
R_{\Box}$ when $E\coloneqq\Delta$.

###### Proposition 7

Every $\mathsf{GRel}_{\mathcal{L}}$-inequality $\gamma_{1}\subseteq\gamma_{2}$
is the shifting of the $\mathsf{KRel}_{\mathcal{L}}$-inequality
$\tau(\gamma_{1})\subseteq\tau(\gamma_{2})$ (see Definition 16).

###### Proof

Immediate by item 1 of Lemma 9.

###### Theorem 6.1

For any inductive mrp $s(p)\leq t(p)$, the
$\mathsf{GRel}_{\mathcal{L}}$-inequality encoding its first-order
correspondent on graph-based frames is the shifting of the
$\mathsf{KRel}_{\mathcal{L}}$-inequality encoding its first-order
correspondent on Kripke frames.

###### Proof

By Proposition 7, it is enough to show that the
$\mathsf{KRel}_{\mathcal{L}}$-inequality equivalent to the first order
correspondent of $s(p)\leq t(p)$ on Kripke frames is the translation of the
$\mathsf{GRel}_{\mathcal{L}}$-inequality equivalent to the first order
correspondent of $s(p)\leq t(p)$ on graph-based frames. Such correspondents
are (depending on the type of $s(p)\leq t(p)$):

Type |  $\mathsf{KRel}_{\mathcal{L}}$-inequalities |  $\mathsf{GRel}_{\mathcal{L}}$-inequalities
---|---|---
(a) | $R_{\mathsf{LA}(\psi)}\circ R_{\varphi}\subseteq R_{\chi[\mathsf{LA}(\alpha)/p]}$ | $R_{\mathsf{LA}(\psi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Diamond$}}}}_{E}R_{\varphi}\subseteq R_{\chi[\mathsf{LA}(\alpha)/p]}$
(b) | $R_{\mathsf{RA}(\varphi)}\,\circ R_{\psi}\subseteq R_{\zeta[\mathsf{RA}(\delta)/p]}$ | $R_{\mathsf{RA}(\varphi)}\,{\vbox{\hbox{\scalebox{0.6}{$\Box$}}}}_{E}R_{\psi}\subseteq R_{\zeta[\mathsf{RA}(\delta)/p]}$

where the notation $R_{\varphi},R_{\psi},R_{\chi},R_{\zeta}$ refers to
Definition 17 in the graph-based context, and Definition 18 in the Kripke one.
Therefore, it is sufficient to prove that the
$\mathsf{KRel}_{\mathcal{L}}$-terms associated to formulas in Definition 18
coincide with the translations of the terms associated with the same formulas