Modal reduction principles: a parametric shift to graphs

Abstract

Graph-based frames have been introduced as a logical framework which internalises 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 generalising 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) recognising 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 generalised 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 (Pawlak, 1984, 1998; Pawlak & Skowron, 2007) aimed at generalising Pawlak's original setting both for extending its scope, and for making the theory more modular and systematic. Instrumental to these generalisations were several cross-fertilizations with other research lines such as (two-valued (Blackburn et al., 2002) and many-valued (Bou et al., 2011; Fitting, 1991, 1992; Godo et al., 2003)) modal logic, and Formal Concept Analysis (Ganter & Wille, 2012). Since Orlowska's work identifying the modal logic S5 as the logic of information spaces (Orlowska, 1994), and building on the insight that formalising the indiscernibility relation as an equivalence relation might be too restrictive (Rasiowa & Skowron, 1984; Zakowski, 1983), Vakarelov (1991, 2005) introduces a framework in which lower and upper approximations are associated with different indiscernibility relations; Yao and Lin (1996) account systematically for various notions of generalised 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 van Benthem, 1984; Sahlqvist, 1975) to various well known modal axioms (which are, more specifically, modal reduction principles (van Benthem, 1976), 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 (Fine, 1972) and probabilistic modal logic (Fagin et al., 1990); using duality-theoretic and correspondence-theoretic techniques, Balbiani and Vakarelov (2001) 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 (1994, 1996, 2004) 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 (van der Berg et al., 2023a, 2023b; Greco et al., 2019; Greco, Liang et al., 2019; Ma et al., 2018; Saha et al., 2014, 2016).

Unifying RST and FCA. Closely related to these developments are proposals of unifying frameworks for rough set theory and formal concept analysis (Cattaneo et al., 2016; Formica, 2018; Kent, 1996; Yao, 2004a, 2004b, 2006, 2016, 2020), both in the two-valued and in the many-valued setting. This unification is particularly sought after for modelling classification problems characterised by partial or incomplete information.

Drawing on insights developed in the research lines discussed above, in Conradie et al. (2021), 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 (Conradie et al., 2014; Conradie & Palmigiano, 2012; Conradie et al., 2017). The main tool exploited in Conradie et al. (2021) is an embedding, defined as in Moshier (2016), from the class of sets to the class of formal contexts (cf. Conradie et al. (2021, 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. Conradie et al. (2021, Proposition 3.4)). This embedding can be extended (cf. Conradie et al. (2021, 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¹. These structures have been defined in (Conradie et al., 2016, 2017) in the context of a research program aimed at developing the logical foundations of categorisation theory, and consist of formal contexts enriched with additional relations, each defined on the basis of duality-theoretic considerations (discussed in Conradie et al., 2020), and supporting the interpretation of a normal modal operator. In Conradie et al. (2021), the study of the preservation properties of the embedding mentioned above leads to the understanding that a connection can be established (cf. Conradie et al. (2021, 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 generalising approximation spaces.

Rough concepts and beyond: towards parametric correspondence. Besides motivating the identification of conceptual approximation spaces (cf. Conradie et al. (2021, 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 Conradie et al. (2021), 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 (van Benthem, 2001; Conradie et al., 2019b, 2021, 2016, 2017). In Conradie et al. (2022), both questions are answered positively: the above-mentioned connection is generalised from a finite set of modal axioms to the class of Sahlqvist modal reduction principles (van Benthem, 1976) (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 (Conradie et al., 2014), but also (effectively) parametric (Conradie et al., 2022).

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 (Conradie & Craig, 2015; Conradie et al., 2019b, 2020; Craig et al., 2015) (cf. Definition 2.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 (Conradie et al., 2019b), which fact, as also discussed in Conradie et al. (2020), 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 (Vakarelov, 2005; Wybraniec-Skardowska, 1989; Yao & Lin, 1996), 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 internalises the correct reasoning patterns under informational entropy into the propositional fragment of the language. (Figure 1.)

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 generalisation of the identity relation Δ on sets, and the embedding from sets to reflexive graphs corresponding to this generalisation, which is defined by the assignment $S\mapsto (S,{\mathrm{\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 Conradie et al. (2020), 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 φ 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 generalisations, 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 φ nor a proof of $\mathrm{\neg \phi }$; 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 (Conradie et al., 2020), 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 Conradie et al. (2019a), the many-valued version is introduced of the graph-based semantics of Conradie et al. (2019b) 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 Conradie et al. (2021), 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.

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

Date	Development	Reference
2015	Graph-based semantics for (non-distributive) modal logics	(Conradie & Craig, 2015)
2016	Introduction of enriched RS-polarities as semantic framework for an epistemic logic of categories and (formal) concepts.	(Conradie et al., 2016)
2017	Approach in Conradie et al. (2016) generalised to arbitrary (hence not necessarily RS) polarities, adding a ‘common knowledge’-type construction and formalising key concepts in categorisation theory.	(Conradie et al., 2017)
2019	Complete axiomatization of modal logic of graph-based frames.	(Conradie et al., 2019b)
	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 parameterised composition (E-composition) in the context of graph-based frames.
	Interpretation of graph-based models for reasoning about informational entropy.
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.	(Conradie & Palmigiano, 2019)
	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.
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.	(Conradie et al., 2020)
2021	Novel unification of Rough Set Theory and Formal Concept Analysis generalising Pawlak's original approximation with polarity-based frames.	(Conradie et al., 2021)
2021	Many-valued graph-based semantics extended to a multi-type setting; proposed as formal framework for modelling socio-political competition.	(Conradie et al., 2019)
2022	Introduction of many-valued graph-based frames and models and application to reasoning about competing theories.	(Conradie et al., 2019a)
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.)	(Conradie et al., 2022)

Main contributions. Besides extending the network of systematic connections, established in Conradie et al. (2022), 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 generalisation 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 formalised by environments whose naturally associated logics are hyper-constructive.

Table 2. Main contributions of the present paper.

Hyper-constructivist approximation spaces	Introduction of hyper-constructivist approximation spaces (see Definition 4.1), 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 5.1) which reflect the semantics of the compositions of connectives in graph-based frames (see Lemma 5.2), 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 5.1).
Relational languages ${\mathsf{\text{GRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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 6.1 and 6.2, and the discussions following the lemmas). These definitions hinge on the notions of composition discussed above.
Shifting of term inequalities in ${\mathsf{\text{KRel}}}_{\mathcal{L}}$	Introduction of the notion of shifting between ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequalities and ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities (cf. Definition 6.3). 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{\text{GRel}}}_{\mathcal{L}}$	Introduction of the notion of lifting of ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities to ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequalities (cf. Definition 6.4), 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 Conradie et al. (2022).

Comparison with results on polarity-based frames. As observed in Conradie et al. (2020), 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².

Table

Axiom	Correspondents
$\mathrm{◻p}⊢\mathrm{◻◻p}$	Kripke frames: $\mathrm{\forall x}\mathrm{\forall y}\mathrm{\forall z}\left(\mathrm{xRy}\mathrm{\&}\mathrm{yRz}\right)\Rightarrow \mathrm{xRz})$
	Polarity-based frames: $\mathrm{\forall a}\mathrm{\forall x}\left(\right(\mathrm{aIx}\Rightarrow \mathrm{\forall y}\left(\mathrm{\forall b}\right(b{R}_{◻}x\Rightarrow \mathrm{bIy})\Rightarrow \mathrm{aIy}))$
	Graph-based frames: $\mathrm{\forall }{z}_1\mathrm{\forall }{z}_2\mathrm{\forall }{z}_3\left(\right(\mathrm{\forall }{z}_4(z_{3}E{z}_4\Rightarrow z_4{R}_{◻}{z}_1)\mathrm{\&}{z}_2{R}_{◻}{z}_3)\Rightarrow z_2{R}_{◻}{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 Conradie et al. (2022), transferring it to graph-based frames requires specific steps, which are presented in Sections 5 and 6.

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) generalisations 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{\text{GRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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{\text{GRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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 (Conradie & Palmigiano, 2019) on them.

2.1. Notational conventions and basic constructions

We let ${\mathrm{\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\left[U^{\prime }\right]:=\{v\in V|(u,v)\in R\text{ for some }u\in U^{\prime }\}$ and $R^{-1}\left[V^{\prime }\right]:=\{u\in U|(u,v)\in R\text{ for some }v\in V^{\prime }\}$, and write $R\left[u\right]$ and $R^{-1}\left[v\right]$ for $R\left[\right\{u\left\}\right]$ and $R^{-1}\left[\right\{v\left\}\right]$, respectively. Any such R gives rise to the semantic modal operators $〈R〉,\left[R\right]:\mathcal{P}\left(V\right)\to \mathcal{P}\left(U\right)$ s.t.  $〈R〉W:=R^{-1}\left[W\right]$ and $\left[R\right]W:=\left(R^{-1}\right[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 (1) $\begin{array}{r}\begin{array}{ll}{T}^{\left(1\right)}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}& T^{\left(0\right)}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}\\ T^{\left[1\right]}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow u{T}^{c}v\left)\right\}& T^{\left[0\right]}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow u{T}^{c}v\left)\right\}\end{array}\end{array}$(1) Well known properties of these constructions (cf. Davey and Priestley (2002, Sections 7.22-7.29)) are stated in the following lemma.

Lemma 2.1

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

(1)	$X_1\subseteq X_2\subseteq U$ implies $T^{\left(1\right)}\left[X_2\right]\subseteq T^{\left(1\right)}\left[X_1\right]$, and $Y_1\subseteq Y_2\subseteq V$ implies $T^{\left(0\right)}\left[Y_2\right]\subseteq T^{\left(0\right)}\left[Y_1\right]$.
(2)	$U^{\prime }\subseteq T^{\left(0\right)}\left[V^{\prime }\right]$ iff $V^{\prime }\subseteq T^{\left(1\right)}\left[U^{\prime }\right]$.
(3)	$U^{\prime }\subseteq T^{\left(0\right)}\left[T^{\left(1\right)}\right[U^{\prime }\left]\right]$ and $V^{\prime }\subseteq T^{\left(1\right)}\left[T^{\left(0\right)}\right[V^{\prime }\left]\right]$.
(4)	$T^{\left(1\right)}\left[U^{\prime }\right]=T^{\left(1\right)}\left[T^{\left(0\right)}\right[T^{\left(1\right)}\left[U^{\prime }\right]\left]\right]$ and $T^{\left(0\right)}\left[V^{\prime }\right]=T^{\left(0\right)}\left[T^{\left(1\right)}\right[T^{\left(0\right)}\left[V^{\prime }\right]\left]\right]$.
(5)	$T^{\left(0\right)}[\bigcup \mathcal{V}]=\bigcap _{V^{\prime }\in \mathcal{V}}{T}^{\left(0\right)}\left[V^{\prime }\right]$ and $T^{\left(1\right)}[\bigcup \mathcal{U}]=\bigcap _{U^{\prime }\in \mathcal{U}}{T}^{\left(1\right)}\left[U^{\prime }\right]$.

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

Lemma 2.2

Conradie et al. (2022, Lemma 3.10)

For any relation $T\subseteq U\times V$, and any $W\subseteq V$, $\begin{array}{r}{T}^{\left[0\right]}\left[W^c\right]=\left(T^{-1}\right[W^c]{)}^c=[T\left]W\mathrm{and}\right({\mathrm{T}}^{\left[0\right]}\left[\mathrm{W}\right]{)}^{\mathrm{c}}={\mathrm{T}}^{-1}\left[\mathrm{W}\right]=〈\mathrm{T}〉\mathrm{W}.\end{array}$

2.2. Approximation spaces and their modal logic

Approximation spaces have been introduced by Pawlak (1982) 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: $\begin{array}{r}\overline{Z}:=\bigcup \left\{R\right[z]|z\in Z\}\text{ and }\underset{\_}{Z}:=\bigcup \left\{R\right[z]|z\in Z\text{and}R[z]\subseteq Z\}.\end{array}$A rough set of $\mathbb{X}$ is a pair $(\underset{\_}{Z},\overline{Z})$ for any $Z\subseteq S$ (cf. Banerjee and Chakraborty (1996)). Since R is an equivalence relation, $\begin{array}{r}\overline{Z}=〈R〉Z\text{and}\underset{\_}{Z}=\left[R\right]Z,\end{array}$with $〈R〉$ and $\left[R\right]$ validating the axioms of the classical normal modal logic S5 (cf. Orlowska (1994)).

As approximation spaces are exactly the Kripke frames for the normal modal logic S5 (Orlowska, 1994), this logic completely axiomatizes Pawlak's rough set theory. Given a language for classical modal logic over a set $\mathsf{\text{Prop}}$ of proposition variables and a valuation $V:\mathsf{\text{Prop}}\to \mathcal{P}\left(S\right)$ on $\mathbb{X}$, the satisfiability on models $M=(\mathbb{X},V)$ is defined as usual in modal logic. The extension $\left[\right[\varphi \left]\right]\subseteq S$ of any formula ϕ is defined recursively as follows: $\begin{array}{r}\begin{array}{llll}M,w⊩p& \mathrm{iff}& w\in V\left(p\right)& \left[\right[p\left]\right]=V\left(p\right)\\ M,w⊩\varphi \vee \psi & \mathrm{iff}& w\in \left[\right[\varphi \left]\right]\mathrm{or}\mathrm{w}\in \left[\right[\psi \left]\right]& \left[\right[\varphi \vee \psi \left]\right]=\left[\right[\varphi \left]\right]\cup \left[\right[\psi \left]\right]\\ M,w⊩\varphi \wedge \psi & \mathrm{iff}& w\in \left[\right[\varphi \left]\right]\mathrm{and}\mathrm{w}\in \left[\right[\psi \left]\right]& \left[\right[\varphi \wedge \psi \left]\right]=\left[\right[\varphi \left]\right]\cap \left[\right[\psi \left]\right]\\ M,w⊩\mathrm{\neg \varphi }& \mathrm{iff}& w\notin \left[\right[\varphi \left]\right]& \left[\right[\mathrm{\neg \varphi }\left]\right]=\left[\right[\varphi ]{]}^c\\ M,w⊩\mathrm{◻\varphi }& \mathrm{iff}& \mathrm{wRu}\mathrm{implies}\mathrm{u}\in \left[\right[\varphi \left]\right]& \left[\right[\mathrm{◻\varphi }\left]\right]=\left[R\right]\left[\right[\varphi \left]\right]\\ M,w⊩\mathrm{◊\varphi }& \mathrm{iff}& \mathrm{wRu}\mathrm{for}\mathrm{some}\mathrm{u}\in \left[\right[\varphi \left]\right]& \left[\right[\mathrm{◊\varphi }\left]\right]=〈R〉\left[\right[\varphi \left]\right]\end{array}\end{array}$

As is well known (Orlowska, 1994), 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. $\begin{array}{r}\mathrm{◻\varphi }\to \varphi \mathrm{◻\varphi }\to \mathrm{◻◻\varphi }\varphi \to \mathrm{◻◊\varphi }.\end{array}$Motivated by the idea that the indiscernibility relation does not need to be an equivalence relation, the following definition provides the environment for a generalised and more modular definition of approximation space.

Definition 2.1

Yao (1998, Section 2)

A generalised 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 $\begin{array}{r}\overline{Z}:=〈R〉Z=\bigcup \left\{R^{-1}\right[z]|z\in Z\}\text{and}\underset{\_}{Z}:=\left[R\right]Z=\{s\in S|R[s]\subseteq Z\}.\end{array}$The following table lists the names of subclasses of generalised approximation spaces in terms of their defining first-order condition.

Table

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

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 characterise various subclasses of generalised approximation spaces in terms of well known modal axioms.

Proposition 2.1

Yao (1998, Section 2)

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

(1)	$\mathbb{X}⊩\mathrm{◻p}\to \mathrm{◊p}$ iff $\mathbb{X}$ is serial.
(2)	$\mathbb{X}⊩\mathrm{◻p}\to p$ iff $\mathbb{X}$ is reflexive.
(3)	$\mathbb{X}⊩p\to \mathrm{◻◊p}$ iff $\mathbb{X}$ is symmetric.
(4)	$\mathbb{X}⊩\mathrm{◻p}\to \mathrm{◻◻p}$ iff $\mathbb{X}$ is transitive.
(5)	$\mathbb{X}⊩\mathrm{◊p}\to \mathrm{◻◊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 generalised Boolean algebras with operators. Their associated logics typically have a propositional base that is strictly weaker than classical propositional logic.

Rough algebras and their generalisations. Banerjee and Chakraborty (1996) introduced topological quasi-Boolean algebras (tqBas) as a generalisation of S5 Boolean algebras with operators (BAOs).

Definition 2.2

Banerjee and Chakraborty (1996)

A topological quasi-Boolean algebra (tqBa) is an algebra $\mathbb{T}=(\mathbb{L},I)$ such that $\mathbb{L}=(\mathrm{L},\vee ,\wedge ,\mathrm{\neg },\mathrm{\top },\mathrm{\perp })$ is a De Morgan algebra and for all $a,b\in \mathbb{L}$, $\begin{array}{r}T1.I(a\wedge b)=\mathrm{Ia}\wedge \mathrm{Ib}T2.\mathrm{IIa}=\mathrm{Ia}T3.\mathrm{Ia}\le aT4.I\mathrm{\top }=\mathrm{\top }.\end{array}$

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

Table

Algebras	Acronyms	Axioms
topological quasi Boolean algebra 5	tqBa5	T5: CIa = Ia
intermediate algebra of type 1	IA1	T5, T6: $\mathrm{Ia}\vee \mathrm{\neg Ia}=\mathrm{\top }$
intermediate algebra of type 2	IA2	T5, T7: $I(a\vee b)=\mathrm{Ia}\vee \mathrm{Ib}$
intermediate algebra of type 3	IA3	T5, T8: $\mathrm{Ia}\le \mathrm{Ib}$ and $\mathrm{Ca}\le \mathrm{Cb}$ imply $a\le 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 (Banerjee & Chakraborty, 1996, 2004). 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 $◻$ and $◊$ 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 Kumar and Banerjee (2015), 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 neighbourhoods in a topological space.

Definition 2.3

Kumar and Banerjee (2015, 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. $I(\bigwedge A)=\bigwedge \left\{I\right(a)|a\in A\}$ and $C(\bigvee A)=\bigvee \left\{C\right(a)|a\in A\}$.

2. $C(\bigwedge A)=\bigwedge \left\{C\right(a)|a\in A\}$ and $I(\bigvee A)=\bigvee \left\{I\right(a)|a\in A\}$.

3. $\mathrm{Ia}\le a$ and $a\le \mathrm{Ca}$.

4. I1 = 1 and C0 = 0.

5. IIa = Ia and CCa = Ca.

6. ICa = Ca and CIa = Ia.

7. $\mathrm{Ia}\le \mathrm{Ib}$ and $\mathrm{Ca}\le \mathrm{Cb}$ imply $a\le 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 (Gehrke et al., 2005), and hence they are naturally endowed with a (bi)Heyting algebra structure. Kumar (2020) also introduced rough Heyting algebras to describe the interaction between the approximation operators I and C and Heyting implication.

Definition 2.4

(Kumar, 2020, Definition 40)

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

1. $I(a\to b)=(\mathrm{Ia}\to \mathrm{Ib})\wedge (\mathrm{Ca}\to \mathrm{Cb})$.

2. $C(a\to b)=\mathrm{Ca}\to \mathrm{Cb}$.

Rough algebras based on concept lattices. In Conradie et al. (2021), 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 (Ganter & Wille, 2012), 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 (Conradie et al., 2021).

Definition 2.5

cf. (Conradie et al., 2021, Section 6)

An abstract conceptual rough algebra (resp. conceptual rough algebra) (acra (resp. cra)) is an algebra $\mathbb{A}=(\mathbb{L},◻,◊)$ such that $\mathbb{L}$ is a bounded lattice (resp. complete lattice) and $◻$ and $◊$ are unary operations on $\mathbb{L}$ such that $◊$ is finitely join-preserving (resp. completely join-preserving) and $◻$ is finitely meet-preserving (resp. completely meet-preserving), and for any $a\in \mathbb{L}$, $\begin{array}{r}\mathrm{◻a}\le \mathrm{◊a}.\end{array}$Subclasses of abstract conceptual rough algebras (resp. conceptual rough algebras) have been considered, which are reported in the following table.

Table

Class	Axioms
reflexive	$\mathrm{◻a}\le a$ and $a\le \mathrm{◊a}$
transitive	$\mathrm{◻a}\le \mathrm{◻◻a}$ and $\mathrm{◊◊a}\le \mathrm{◊a}$
symmetric	$a\le \mathrm{◻◊a}$ and $\mathrm{◊◻a}\le a$
dense	$\mathrm{◻◻a}\le \mathrm{◻a}$ and $\mathrm{◊a}\le \mathrm{◊◊a}$

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

Table

Class	Axioms
Conceptual tqBa5	$\mathrm{◊◻a}\le \mathrm{◻a}$ and $\mathrm{◊a}\le \mathrm{◻◊a}$
conceptual IA1	$◻(a\vee b)\le \mathrm{◻a}\vee \mathrm{◻b}$ and $\mathrm{◊a}\wedge \mathrm{◊b}\le ◊(a\wedge b)$
conceptual IA2	$(\mathrm{◻a}\le \mathrm{◻b}\mathrm{\&}\mathrm{◊a}\le \mathrm{◊b})\Rightarrow a\le b$

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

Rough algebras based on posets. Cattaneo (1996) further generalises rough set theory by defining the notion of abstract approximation spaces on posets.

Definition 2.6

Cattaneo (1996, Section 1)

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

1. $i\left(x\right)\le x$ and $x\le c\left(x\right)$.

2. $\alpha \le x\Rightarrow \alpha \le i\left(x\right)$.

3. $x\le \gamma \Rightarrow c\left(x\right)\le \gamma$.

Algebraic structures arising from rough operators defined on various classes of lattice-based algebras such as orthomodular lattices (Dai, 2021), quasi-Brouwer-Zadeh distributive lattices (Cattaneo & Ciucci, 2004), MV-algebras (Rasouli & Davvaz, 2010), cylindric algebras have been studied in literature.

Fuzzy and probabilistic rough algebras. Several fuzzy and probabilistic generalisations of rough set theory have been studied extensively in the literature (Dubois & Prade, 1990; Liu, 2008; Yao, 2008). Yao (Yao, 2008) introduces a framework for probabilistic rough set approximations using the notion of rough membership.

Definition 2.7

Yao (2008, 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\left(A|\right[x\left]\right)$, where $\left[x\right]:=\{y\in U|\mathrm{xEy}\}$.

Definition 2.8

Yao (2008, Section 4.3)

For all parameters $\alpha ,\text{β}\in [0,1]$, and any probabilistic approximation space $\mathbb{X}=(U,E,P)$, the generalised probabilistic approximation operators $\underset{\_}{\mathrm{app}{r}_{\alpha }},\overline{\mathrm{app}{r}_{\text{β}}}:\mathcal{P}\left(U\right)\to \mathcal{P}\left(U\right)$ are defined as follows. If $0\le \text{β}<\alpha \le 1$, then for any $A\subseteq U$, $\begin{array}{r}\underset{\_}{\mathrm{app}{r}_{\alpha }}\left(A\right)=\{x\in U|P(A|\left[x\right])\ge \alpha \}\mathrm{and}\overline{\mathrm{app}{\mathrm{r}}_{\text{β}}}\left(\mathrm{A}\right)=\{\mathrm{x}\in \mathrm{U}|\mathrm{P}(\mathrm{A}|\left[\mathrm{x}\right])<\text{β}\}.\end{array}$If $\alpha =\text{β}\ne 0$, then $\begin{array}{r}\underset{\_}{\mathrm{app}{r}_{\alpha }}\left(A\right)=\{x\in U|P(A|\left[x\right])>\alpha \}\mathrm{and}\overline{\mathrm{app}{\mathrm{r}}_{\alpha }}\left(\mathrm{A}\right)=\{\mathrm{x}\in \mathrm{U}|\mathrm{P}(\mathrm{A}|\left[\mathrm{x}\right])\le \alpha \}.\end{array}$

Given the properties they were shown to satisfy (e.g. monotonicity, distributivity over union and intersection), the approximation operators $\underset{\_}{\mathrm{app}{r}_{\alpha }}$ and $\overline{\mathrm{app}{r}_{\text{β}}}$ can be regarded as paramentric fuzzy regular modal operators ${◻}_{\alpha }$ and ${◊}_{\text{β}}$ on the powerset algebra $\mathcal{P}\left(U\right)$, respectively.

Using both constructive and algebraic methods, Wu and Zhang (2004) introduce a generalisation of rough set theory to a fuzzy framework.

Definition 2.9

Wu and Zhang (2004, Definition 4)

A generalised 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, $\underset{\_}{R}\left(A\right)$ and $\overline{R}\left(A\right)$, are defined as follows: For any $x\in U$, $\begin{array}{r}\overline{R}\left(A\right)\left(x\right)=\underset{y\in W}{\bigvee }\left(R\right(x,y)\wedge A(y\left)\right)\mathrm{and}\underset{\_}{\mathrm{R}}\left(\mathrm{A}\right)\left(\mathrm{x}\right)=\underset{\mathrm{y}\in \mathrm{W}}{\bigwedge }\left(\right(1-\mathrm{R}(\mathrm{x},\mathrm{y}))\vee \mathrm{A}(\mathrm{y}\left)\right).\end{array}$A generalised fuzzy approximation space $\mathbb{X}=(W,U,R)$ with U = W is:

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

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

3. transitive if $R(x,z)\ge \underset{y\in U}{\bigvee }\left(R\right(x,y)\wedge R(y,x\left)\right)$ for all $x,z\in U$.

4. serial if $\mathrm{\exists y}\left(R\right(x,y)=1)$ for all $x\in U$.

Let $\mathcal{F}\left(W\right)$ denote the set of all fuzzy subsets of W. The fuzzy approximation operators $\underset{\_}{R}$ and $\overline{R}$ defined above satisfy the following properties (Wu & Zhang, 2004): for all $A,B\in \mathcal{F}\left(W\right)$, and any $\alpha \in [0,1]$, $\begin{array}{r}\begin{array}{ll}1.\underset{\_}{R}\left(A\right)=\mathrm{\neg }\overline{R}\left(\mathrm{\neg A}\right)& 2.\overline{R}\left(A\right)=\mathrm{\neg }\underset{\_}{R}\left(\mathrm{\neg A}\right)\\ 3.\underset{\_}{R}(A\vee \hat{\alpha })=\underset{\_}{R}\left(A\right)\vee \hat{\alpha }& 4.\overline{R}(A\wedge \hat{\alpha })=\overline{R}\left(A\right)\wedge \hat{\alpha }\\ 5.\underset{\_}{R}(A\wedge B)=\underset{\_}{R}\left(A\right)\wedge \underset{\_}{R}\left(B\right)& 6.\overline{R}(A\vee B)=\overline{R}\left(A\right)\vee \overline{R}\left(B\right),\end{array}\end{array}$where $\hat{\alpha }$ is the constant fuzzy set $\hat{\alpha }\left(x\right)=\alpha$ for all $x\in U\cup W$. As lower and upper approximation operators $\underset{\_}{R}$ and $\overline{R}$ are completely meet-preserving and join-preserving, these operators are semantic modal operators $◻$ and $◊$ on $\mathcal{F}\left(W\right)$.

The following proposition generalises Proposition 2.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}\left(W\right)$, x, y denote elements of W, and α 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.2

Wu and Zhang (2004, Section 3.3)

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

(1)	reflexive iff $A\subseteq \overline{R}\left(A\right)$ or equivalently iff $\underset{\_}{R}\left(A\right)\subseteq A$ for every $A\in \mathcal{F}\left(W\right)$.
(2)	symmetric iff for all $x,y\in W$ $\begin{array}{r}\underset{\_}{R}\left(1_{U-\left\{x\right\}}\right)\left(y\right)=\underset{\_}{R}\left(1_{U-\left\{y\right\}}\right)\left(x\right)\text{or equivalently iff }\overline{R}\left(1_x\right)\left(y\right)=\overline{R}\left(1_y\right)\left(x\right).\end{array}$
(3)	transitive iff $\underset{\_}{R}\left(A\right)\subseteq \underset{\_}{R}\left(\underset{\_}{R}\right(A\left)\right)$ or equivalently iff $\overline{R}\left(\overline{R}\right(A\left)\right)\subseteq \overline{R}\left(A\right)$ for every $A\in \mathcal{F}\left(W\right)$.
(4)	serial iff $\underset{\_}{R}\left(\varnothing \right)=\varnothing$ iff $\overline{R}\left(W\right)=W$ iff $\mathrm{\forall \alpha }\left(\overline{R}\right(\hat{\alpha })=\hat{\alpha })$ iff $\mathrm{\forall \alpha }\left(\underset{\_}{R}\right(\hat{\alpha })=\hat{\alpha })$ iff $\mathrm{\forall A}\left(\underset{\_}{R}\right(A)\subseteq \overline{R}(A\left)\right)$.

Several types of many-valued algebras generalising the interval $[0,1]$ have been studied in the literature as an environment for fuzzy rough set theory (Chakraborty, 2011; Conradie et al., 2021; Radzikowska & Kerre, 2004; Sun et al., 2008; Wu & Zhang, 2004).

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

The present section collects basic definitions and facts from Conradie and Palmigiano (2019), Conradie et al. (2020), and Gehrke and Harding (2001). Let $\mathsf{\text{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: $\begin{array}{r}\phi :=\mathrm{\perp }|\mathrm{\top }|p|\phi \wedge \phi |\phi \vee \phi |\mathrm{◻\phi }|\mathrm{◊\phi },\end{array}$where $p\in \mathsf{\text{Prop}}$. The basic, or minimal normal $\mathcal{L}$-logic is a set $\mathbf{\text{L}}$ of sequents $\varphi ⊢\psi$ with $\varphi ,\psi \in \mathcal{L}$, containing the following axioms: $\begin{array}{r}\begin{array}{cccccc}p⊢p& \mathrm{\perp }⊢p& p⊢p\vee q& p\wedge q⊢p& \mathrm{\top }⊢◻\mathrm{\top }& \mathrm{◻p}\wedge \mathrm{◻q}⊢◻(p\wedge q)\\ & p⊢\mathrm{\top }& q⊢p\vee q& p\wedge q⊢q& ◊\mathrm{\perp }⊢\mathrm{\perp }& ◊(p\vee q)⊢\mathrm{◊p}\vee \mathrm{◊q}\end{array}\end{array}$and closed under the following inference rules: $\begin{array}{rl}& \frac{\varphi ⊢\chi \chi ⊢\psi }{\varphi ⊢\psi }\frac{\varphi ⊢\psi }{\varphi \left(\chi /p\right)⊢\psi \left(\chi /p\right)}\frac{\chi ⊢\varphi \chi ⊢\psi }{\chi ⊢\varphi \wedge \psi }\frac{\varphi ⊢\chi \psi ⊢\chi }{\varphi \vee \psi ⊢\chi }\\ & \frac{\varphi ⊢\psi }{\mathrm{◻\varphi }⊢\mathrm{◻\psi }}\frac{\varphi ⊢\psi }{\mathrm{◊\varphi }⊢\mathrm{◊\psi }}\end{array}$By an $\mathcal{L}$-logic we understand any extension of $\mathbf{\text{L}}$ with $\mathcal{L}$-axioms $\varphi ⊢\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 (Ploščica, 1994) (see also Craig et al., 2015, 2013).

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³. We let $D\subseteq Z\times Z$ be defined as xDa iff aEx. For every set S, we let ${\mathbb{G}}_S=(S,\mathrm{\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 polarity⁴ ${\mathbb{P}}_{\mathbb{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 $a{I}_{E^c}x$ iff $a{E}^{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 $a{I}_{R^c}x$ iff $a{R}^{c}x$ and $x{J}_{R^c}a$ iff $x{R}^{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 2.3

For any relation $R\subseteq Z\times Z$ and any $Y,B\subseteq Z$, $\begin{array}{r}{I}_{R^c}^{\left(0\right)}\left[Y\right]=\left(R^{\left[0\right]}\right[Y\left]{)}_A{I}_{R^c}^{\left(1\right)}\right[B]=(R^{\left[1\right]}\left[B\right]{)}_X{J}_{R^c}^{\left(0\right)}\left[B\right]=\left(R^{\left[0\right]}\right[B\left]{)}_X{J}_{R^c}^{\left(1\right)}\right[Y]=(R^{\left[1\right]}\left[Y\right]{)}_A.\end{array}$

The complete lattice ${\mathbb{G}}^{+}$ associated with a graph $\mathbb{G}$ is the concept lattice of ${\mathbb{P}}_{\mathbb{G}}$. By specialising (Conradie et al., 2020, Proposition 3.1) to ${\mathbb{P}}_{\mathbb{G}}$ we get the following.

Proposition 2.3

For every graph $\mathbb{G}=(Z,E)$, the lattice ${\mathbb{G}}^{+}$ is completely join-generated by the set $\{{\mathbf{\text{z}}}_A=(z^{\left[10\right]},z^{\left[1\right]})|z\in Z\}$ and completely meet-generated by the set $\{{\mathbf{\text{z}}}_X=(z^{\left[0\right]},z^{\left[01\right]})|z\in Z\}$.

Definition 2.10

A graph-based $\mathcal{L}$-frame is a structure $\mathbb{F}=(\mathbb{G},R_{◊},R_{◻})$ where $\mathbb{G}=(Z,E)$ is a reflexive graph⁵, and $R_{◊}$ and $R_{◻}$ are binary relations on Z satisfying the following E-compatibility conditions (notation defined in (1(1) $\begin{array}{r}\begin{array}{ll}{T}^{\left(1\right)}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}& T^{\left(0\right)}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}\\ T^{\left[1\right]}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow u{T}^{c}v\left)\right\}& T^{\left[0\right]}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow u{T}^{c}v\left)\right\}\end{array}\end{array}$(1) )): for all $b,y\in Z$, $\begin{array}{rl}\left(R_{◻}^{\left[0\right]}\right[y]{)}^{\left[10\right]}& \subseteq R_{◻}^{\left[0\right]}\left[y\right]\left(R_{◻}^{\left[1\right]}\right[b]{)}^{\left[01\right]}\subseteq R_{◻}^{\left[1\right]}[b]\\ \left(R_{◊}^{\left[0\right]}\right[b]{)}^{\left[01\right]}& \subseteq R_{◊}^{\left[0\right]}\left[b\right]\left(R_{◊}^{\left[1\right]}\right[y]{)}^{\left[10\right]}\subseteq R_{◊}^{\left[1\right]}[y].\end{array}$The complex algebra of a graph-based $\mathcal{L}$-frame $\mathbb{F}=(\mathbb{G},R_{◊},R_{◻})$ is the complete $\mathcal{L}$-algebra ${\mathbb{F}}^{+}=({\mathbb{G}}^{+},[R_{◻}],〈R_{◊}〉),$ where ${\mathbb{G}}^{+}$ is the concept lattice of ${\mathbb{P}}_{\mathbb{G}}$, and $\left[R_{◻}\right]$ and $〈R_{◊}〉$ are unary operations on ${\mathbb{P}}_{\mathbb{G}}^{+}$ defined as follows: for every $c=\left(\right[\left[c\right]],(\left[c\right]\left)\right)\in {\mathbb{P}}_{\mathbb{G}}^{+}$, $\begin{array}{r}\left[R_{◻}\right]c:=\left(R_{◻}^{\left[0\right]}\right[\left(\right[c\left]\right)],(R_{◻}^{\left[0\right]}\left[\right(\left[c\right]\left)\right]{)}^{\left[1\right]})\text{ and }〈R_{◊}〉c:=(\left(R_{◊}^{\left[0\right]}\right[\left[\right[c\left]\right]]{)}^{\left[0\right]},R_{◊}^{\left[0\right]}[\left[\right[c\left]\right]\left]\right).\end{array}$

Lemma 2.4

Conradie et al. (2021, Lemma 2.6)

For every graph $(Z,E)$ and every relation $R\subseteq Z\times Z$,

(1)	the following are equivalent: (i) $\left(R^{\left[0\right]}\right[y]{)}^{\left[10\right]}\subseteq R^{\left[0\right]}[y]$ for every $y\in Z$; (ii) $\left(R^{\left[0\right]}\right[Y]{)}^{\left[10\right]}\subseteq R^{\left[0\right]}[Y]$ for every $Y\subseteq Z$; (iii) $R^{\left[1\right]}\left[B\right]=R^{\left[1\right]}\left[B^{\left[10\right]}\right]$ for every $B\subseteq Z$;
(2)	the following are equivalent: (i) $\left(R^{\left[1\right]}\right[b]{)}^{\left[01\right]}\subseteq R^{\left[1\right]}[b]$ for every $b\in Z$; (ii) $\left(R^{\left[1\right]}\right[B]{)}^{\left[01\right]}\subseteq R^{\left[1\right]}[B]$ for every $B\subseteq Z$; (iii) $R^{\left[0\right]}\left[Y\right]=R^{\left[0\right]}\left[Y^{\left[01\right]}\right]$ for every $Y\subseteq Z$.

For any graph-based $⧫\mathcal{L}$-frame $\mathbb{F}$, we let $R_{⧫}\subseteq Z\times Z$ be defined by $x{R}_{⧫}a$ iff $a{R}_{◻}x$, and $R_{◼}\subseteq Z\times Z$ by $a{R}_{◼}x$ iff $x{R}_{◊}a$. Hence, for every $B,Y\subseteq Z$, (2) $\begin{array}{r}{R}_{⧫}^{\left[0\right]}\left[B\right]=R_{◻}^{\left[1\right]}\left[B\right]R_{⧫}^{\left[1\right]}\left[Y\right]=R_{◻}^{\left[0\right]}\left[Y\right]R_{◼}^{\left[0\right]}\left[Y\right]=R_{◊}^{\left[1\right]}\left[Y\right]R_{◼}^{\left[1\right]}\left[B\right]=R_{◊}^{\left[0\right]}\left[B\right].\end{array}$(2) By Lemma 2.4, the E-compatibility of $R_{◻}$ and $R_{◊}$ guarantees that the operations $\left[R_{◻}\right],〈R_{◊}〉$ (as well as $\left[R_{◼}\right],〈R_{⧫}〉$) are well defined on ${\mathbb{G}}^{+}$.

Lemma 2.5

Conradie et al. (2019b, Lemma 5)

Let $\mathbb{F}=(\mathbb{G},R_{◻},R_{◊})$ be a graph-based $\mathcal{L}$-frame. Then the algebra  ${\mathbb{F}}^{+}=({\mathbb{G}}^{+},[R_{◻}],〈R_{◊}〉)$ is a complete lattice expansion such that $〈R_{⧫}〉$ and $\left[R_{◻}\right]$ (resp. $〈R_{◊}〉$ and $\left[R_{◼}\right]$) form an adjoint pair⁶. Therefore, $\left[R_{◻}\right]$ (resp. $〈R_{◊}〉$) is completely meet-preserving (resp. completely join-preserving).

Definition 2.11

For every Kripke frame $\mathbb{X}=(S,R)$, the relational structure ${\mathbb{F}}_{\mathbb{X}}:=({\mathbb{G}}_S,R_{◊},R_{◻})$, where $R_{◻}=R_{◊}=R$, is a graph-based frame, since any relation R on S is clearly Δ-compatible (cf. Definition 2.10). Conversely, for any graph-based frame $\mathbb{F}=\left(\right(Z,E),R_{◊},R_{◻})$ such that $E=\mathrm{\Delta }$, and $R_{◊}=R_{◻}$, let ${\mathbb{X}}_{\mathbb{F}}:=(Z,R_{◻})$ be its associated Kripke frame.

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

Proposition 2.4

Conradie et al. (2021, Proposition 3.7)

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

Proposition 2.5

For any graph-based frame $\mathbb{F}$, and any Kripke frame $\mathbb{X}$, $\begin{array}{r}{\mathbb{F}}_{{\mathbb{X}}_{\mathbb{F}}}\cong \mathbb{F}\mathrm{and}{\mathbb{X}}_{{\mathbb{F}}_{\mathbb{X}}}\cong \mathbb{X}.\end{array}$

Definition 2.12

Conradie et al. (2019b, Definition 4)

A graph-based $\mathcal{L}$-model is a tuple $\mathbb{M}=(\mathbb{F},V)$ where $\mathbb{F}=(\mathbb{G},R_{◊},R_{◻})$ is a graph-based $\mathcal{L}$-frame and $V:\mathsf{\text{Prop}}\to {\mathbb{F}}^{+}$. Since $V\left(p\right)$ is a formal concept (cf. Section 2.4) of ${\mathbb{P}}_{\mathbb{G}}$, we write $V\left(p\right)=\left(\right[\left[p\right]],(\left[p\right]\left)\right)$. For every such $\mathbb{M}$, the valuation V can be extended compositionally to all $\mathcal{L}$-formulas as follows: $\begin{array}{r}\begin{array}{ll}V\left(p\right)=\left(\right[\left[p\right]],(\left[p\right]\left)\right)& \\ V\left(\mathrm{\top }\right)=(Z,\varnothing )& V\left(\mathrm{\perp }\right)=(\varnothing ,Z)\\ V(\varphi \wedge \psi )=\left(\right[\left[\varphi \right]]\cap [\left[\psi \right]],(\left[\right[\varphi \left]\right]\cap \left[\right[\psi \left]\right]{)}^{\left[1\right]})& V(\varphi \vee \psi )=\left(\right(\left(\right[\varphi \left]\right)\cap \left(\right[\psi \left]\right){)}^{\left[0\right]},\left(\right[\varphi \left]\right)\cap \left(\right[\psi \left]\right))\\ V\left(\mathrm{◻\varphi }\right)=\left(R_{◻}^{\left[0\right]}\right[\left(\right[\varphi \left]\right)],(R_{◻}^{\left[0\right]}\left[\right(\left[\varphi \right]\left)\right]{)}^{\left[1\right]})& V\left(\mathrm{◊\varphi }\right)=\left(\right(R_{◊}^{\left[0\right]}\left[\right[\left[\varphi \right]\left]\right]{)}^{\left[0\right]},R_{◊}^{\left[0\right]}\left[\right[\left[\varphi \right]\left]\right]).\end{array}\end{array}$Moreover, the existence of the adjoints of $\left[R_{◻}\right]$ and $〈R_{◊}〉$ (cf. Lemma 2.5) supports the interpretation of the language ${\mathcal{L}}^{\ast }$, which is an expansion of $\mathcal{L}$ with the connectives $◼$ and interpreted as follows: $\begin{array}{r}V\left(\mathrm{◼\varphi }\right)=\left(R_{◼}^{\left[0\right]}\right[\left(\right[\varphi \left]\right)],(R_{◼}^{\left[0\right]}\left[\right(\left[\varphi \right]\left)\right]{)}^{\left[1\right]}\left)V\right(\mathrm{⧫\varphi })=(\left(R_{⧫}^{\left[0\right]}\right[\left[\right[\varphi \left]\right]]{)}^{\left[0\right]},R_{⧫}^{\left[0\right]}[\left[\right[\varphi \left]\right]\left]\right)\end{array}$

Spelling out the definition above as is done in Conradie and Craig (2015), we can define the satisfaction and refutation relations $\mathbb{M},\mathbf{\text{z}}⊩\varphi$ and $\mathbb{M},\mathbf{\text{z}}\succ \varphi$ for every graph-based $\mathcal{L}$-model $\mathbb{M}=(\mathbb{F},V)$, $\mathbf{\text{z}}\in Z$, and any $\mathcal{L}$-formula ϕ, by the following simultaneous recursion: $\begin{array}{r}\begin{array}{llll}\mathbb{M},\mathbf{\text{z}}⊩\mathrm{\perp }& \mathrm{never}& \mathbb{M},\mathbf{\text{z}}\succ \mathrm{\perp }& \mathrm{always}\\ \mathbb{M},\mathbf{\text{z}}⊩\mathrm{\top }& \mathrm{always}& \mathbb{M},\mathbf{\text{z}}\succ \mathrm{\top }& \mathrm{never}\\ \mathbb{M},\mathbf{\text{z}}⊩p& \mathrm{iff}\mathbf{\text{z}}\in \left[\right[\mathrm{p}\left]\right]& \mathbb{M},\mathbf{\text{z}}\succ p& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[{\mathbf{\text{z}}}^{\prime }\mathrm{E}\mathbf{\text{z}}\Rightarrow {\mathbf{\text{z}}}^{\prime }⊮\mathrm{p}]\\ \mathbb{M},\mathbf{\text{z}}\succ \varphi \vee \psi & \mathrm{iff}\mathbb{M},\mathbf{\text{z}}\succ \varphi \mathrm{and}\mathbb{M},\mathbf{\text{z}}\succ \psi & \mathbb{M},\mathbf{\text{z}}⊩\varphi \vee \psi & \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}\mathrm{E}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }\nsucc \varphi \vee \psi ]\\ \mathbb{M},\mathbf{\text{z}}⊩\varphi \wedge \psi & \mathrm{iff}\mathbb{M},\mathbf{\text{z}}⊩\varphi \mathrm{and}\mathbb{M},\mathbf{\text{z}}⊩\psi & \mathbb{M},\mathbf{\text{z}}\succ \varphi \wedge \psi & \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[{\mathbf{\text{z}}}^{\prime }\mathrm{E}\mathbf{\text{z}}\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }⊮\varphi \wedge \psi ]\\ \mathbb{M},\mathbf{\text{z}}\succ \mathrm{◊\varphi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}{\mathrm{R}}_{◊}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }⊮\varphi ]& \mathbb{M},\mathbf{\text{z}}⊩\mathrm{◊\varphi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}\mathrm{E}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }\nsucc \mathrm{◊\varphi }]\\ \mathbb{M},\mathbf{\text{z}}⊩\mathrm{◻\psi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}{\mathrm{R}}_{◻}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }\nsucc \psi ]& \mathbb{M},\mathbf{\text{z}}\succ \mathrm{◻\psi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[{\mathbf{\text{z}}}^{\prime }\mathrm{E}\mathbf{\text{z}}\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }⊮\mathrm{◻\psi }]\\ \mathbb{M},\mathbf{\text{z}}\succ \mathrm{⧫\varphi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}{\mathrm{R}}_{⧫}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }⊮\varphi ]& \mathbb{M},\mathbf{\text{z}}⊩\mathrm{⧫\varphi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}\mathrm{E}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }\nsucc \mathrm{⧫\varphi }]\\ \mathbb{M},\mathbf{\text{z}}⊩\mathrm{◼\psi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[\mathbf{\text{z}}{\mathrm{R}}_{◼}{\mathbf{\text{z}}}^{\prime }\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }\nsucc \psi ]& \mathbb{M},\mathbf{\text{z}}\succ \mathrm{◼\psi }& \mathrm{iff}\mathrm{\forall }{\mathbf{\text{z}}}^{\prime }[{\mathbf{\text{z}}}^{\prime }\mathrm{E}\mathbf{\text{z}}\Rightarrow \mathbb{M},{\mathbf{\text{z}}}^{\prime }⊮\mathrm{◼\psi }]\end{array}\end{array}$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 ⊢\psi$ is true in $\mathbb{M}$, denoted $\mathbb{M}\models \varphi ⊢\psi$, if for all $\mathbf{\text{z}},{\mathbf{\text{z}}}^{\prime }\in Z$, if $\mathbb{M},\mathbf{\text{z}}⊩\varphi$ and $\mathbb{M},{\mathbf{\text{z}}}^{\prime }\succ \psi$ then $\mathbf{\text{z}}{E}^c{\mathbf{\text{z}}}^{\prime }$. An $\mathcal{L}$-sequent $\varphi ⊢\psi$ is valid in $\mathbb{F}$, denoted $\mathbb{F}\models \varphi ⊢\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 2.6

Conradie et al. (2019b, Lemma 7)

For any graph-based $\mathcal{L}$-frame $\mathbb{F}$ and any $\mathcal{L}$-sequent $\varphi ⊢\psi$, $\begin{array}{r}\mathbb{F}\models \varphi ⊢\psi \mathrm{iff}{\mathbb{F}}^{+}\models \varphi ⊢\psi .\end{array}$

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\left(p\right)\le t\left(p\right)$ such that both s and t are built up using only $◻$ and $◊$. The term $s\left(p\right)$ (resp. $t\left(p\right)$) 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\left(p\right)$ or $t\left(p\right)$ is good, and is analytic inductive if both are good. So, inductive modal reduction principles are of one of the following types: $\begin{array}{r}\left(\mathrm{a}\right)\varphi \left[\alpha \right(\mathrm{p})/!\mathrm{y}]\le \psi \left[\chi \right(\mathrm{p})/!\mathrm{x}]\left(\mathrm{b}\right)\varphi \left[\zeta \right(\mathrm{p})/!\mathrm{y}]\le \psi \left[\delta \right(\mathrm{p})/!\mathrm{x}],\end{array}$where $◻$ (resp. $◊$) is the only connective allowed in $\alpha \left(p\right)$ and $\psi (!x)$ (resp. $\phi (!y)$ and $\delta \left(p\right)$), and χ (resp. ζ) has $◊$ (resp. $◻$) as principal connective whenever $\chi \left(p\right)\ne p$ (resp. $\zeta \left(p\right)\ne p$). Analytic inductive mrps are of the form $\varphi \left[\alpha \right(p)/!y]\le \psi \left[\delta \right(p)/!x]$, where $\psi (!x)$, $\varphi (!y)$, $\delta \left(p\right)$ and $\alpha \left(p\right)$ 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 generalised 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. Conradie & Palmigiano, 2019)⁷: $\begin{array}{r}\begin{array}{ll}& \mathrm{type}\left(\mathrm{a}\right)\mathrm{\forall }\mathbf{\text{j}}\left[\mathsf{LA}\right(\psi \left)\right[\varphi [\mathbf{\text{j}}/!\mathrm{y}]/!\mathrm{u}]\le \chi [\mathsf{LA}\left(\alpha \right)[\mathbf{\text{j}}/!\mathrm{u}]/\mathrm{p}\left]\right],\\ & \mathrm{type}\left(\mathrm{b}\right)\mathrm{\forall }\mathbf{\text{m}}\left[\zeta \right[\mathsf{RA}\left(\delta \right)[\mathbf{\text{m}}/!\mathrm{u}]/\mathrm{p}]\le \mathsf{RA}(\varphi \left)\right[\psi [\mathbf{\text{m}}/!\mathrm{y}]/!\mathrm{u}],\end{array}\end{array}$where, when θ is a sequence of $◻$ (resp. $◊$) connectives of length n, $\mathsf{\text{LA}}\left(\theta \right)(!u)$ (resp. $\mathsf{\text{RA}}\left(\theta \right)(!u)$) is a sequence of (resp. $◼$) connectives of length n ending with a (single) occurrence of the variable u.

Example 2.1

The mrp $\mathrm{◊◊◻◻p}\le \mathrm{◻◊◻p}$ is inductive of type (a), but not analytic, since it instantiates type (a) above as follows: $\phi \left(y\right):=\mathrm{◊◊y}$, $\alpha \left(p\right):=\mathrm{◻◻p}$, $\psi \left(x\right):=\mathrm{◻x}$, $\chi \left(p\right):=\mathrm{◊◻p}$. Thus, $\mathsf{\text{LA}}\left(\psi \right)\left(u\right)=\mathrm{⧫u}$, $\mathsf{\text{LA}}\left(\alpha \right)\left(u\right)=\mathrm{⧫⧫u}$; therefore, its ALBA output is $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{j}}\left[\right(\mathrm{⧫u}\left)\right[\left(\mathrm{◊◊y}\right)\left[\mathbf{\text{j}}/y\right]/u]\le (\mathrm{◊◻p}\left)\right[\left(\mathrm{⧫⧫u}\right)\left[\mathbf{\text{j}}/u\right]/p\left]\right],\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall }\mathbf{\text{j}}\left[\right(\mathrm{⧫u}\left)\right[\left(\mathrm{◊◊}\mathbf{\text{j}}\right)/u]\le (\mathrm{◊◻p}\left)\right[\left(\mathrm{⧫⧫}\mathbf{\text{j}}\right)/p\left]\right],\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall }\mathbf{\text{j}}[\mathrm{⧫◊◊}\mathbf{\text{j}}\le \mathrm{◊◻⧫⧫}\mathbf{\text{j}}].\end{array}$The mrp $\mathrm{◊◻◻p}\le \mathrm{◻◻◻◊◊◊◊p}$ is analytic inductive, as it instantiates the analytic shape above as follows: $\phi \left(y\right):=\mathrm{◊y}$, $\alpha \left(p\right):=\mathrm{◻◻p}$, $\psi \left(y\right):=\mathrm{◻◻◻y}$, $\delta \left(p\right):=\mathrm{◊◊◊◊p}$. Thus, $\mathsf{\text{RA}}\left(\delta \right)\left(u\right)=\mathrm{◼◼◼◼u}$, and $\mathsf{\text{RA}}\left(\phi \right)\left(u\right):=\mathrm{◼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 $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{m}}\left[\right(\mathrm{◻◻y}\left)\right[\left(\mathrm{◼◼◼◼u}\right)\left[\mathbf{\text{m}}/u\right]/p]\le (\mathrm{◼u}\left)\right[\left(\mathrm{◻◻◻y}\right)\left[\mathbf{\text{m}}/y\right]/u\left]\right],\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall }\mathbf{\text{m}}\left[\right(\mathrm{◻◻y}\left)\right[\left(\mathrm{◼◼◼◼}\mathbf{\text{m}}\right)/p]\le (\mathrm{◼u}\left)\right[\left(\mathrm{◻◻◻}\mathbf{\text{m}}\right)/u\left]\right],\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall }\mathbf{\text{m}}[\mathrm{◻◻◼◼◼◼}\mathbf{\text{m}}\le \mathrm{◼◻◻◻}\mathbf{\text{m}}].\end{array}$

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 $\mathrm{zE}{z}^{\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⊩p$ as account ‘z confirms (posts) news p’. Formally, for any $z\in Z$, and any proposition p, $\begin{array}{r}z\succ p\mathrm{iff}\text{for all}{\mathrm{z}}^{\prime },\mathrm{if}{\mathrm{z}}^{\prime }\mathrm{Ez}\mathrm{then}{\mathrm{z}}^{\prime }⊮\mathrm{p}.\end{array}$On the other hand, an account z posts news p iff none of the followers of z refutes p⁸. Formally, for any $z\in Z$, and any proposition p, $\begin{array}{r}z⊩p\mathrm{iff}\text{for all}{\mathrm{z}}^{\prime },\mathrm{if}\mathrm{zE}{\mathrm{z}}^{\prime }\mathrm{then}{\mathrm{z}}^{\prime }\nsucc \mathrm{p}.\end{array}$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 (Powers et al., 2019; Thorson, 2014; Vraga et al., 2015). 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 Du & Gregory, 2017; Rainie & Smith, 2012). 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 $\mathrm{zE}{z}^{\prime }⟹z^{\prime }\nsucc p$, for all $z^{\prime }$, then $z\nsucc p$. By the defining condition of refutation, the latter implies an account $z^{″}\in Z$ exists such that $z^{″}\mathrm{Ez}$ and $z^{″}⊩p$. Thus, the compatibility conditions between relations $⊩$ and ≻ 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 $\mathrm{zE}{z}^{\prime }$, $z\succ p$ and $z^{\prime }⊩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 $\left(\right[\left[\varphi \right]],(\left[\varphi \right]\left)\right)$ as an echo-chamber (community) with news sources $\left[\right[\varphi \left]\right]$ and followers $\left(\right[\varphi \left]\right)$.

Let $R_{◊}\supseteq E^{-1}$ be a relation such that for any $z,z^{\prime }\in Z$, $z{R}_{◊}{z}^{\prime }$ iff z can possibly hear news from $z^{\prime }$. Recall that the refutation clause for $◊$ (see Section 2.4) is $\begin{array}{r}z\succ \mathrm{◊p}\mathrm{iff}\text{for all}{\mathrm{z}}^{\prime },\mathrm{z}{\mathrm{R}}_{◊}{\mathrm{z}}^{\prime }\mathrm{implies}{\mathrm{z}}^{\prime }⊮\mathrm{p}.\end{array}$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 \mathrm{◊p}$, iff none of the possible news sources for z confirm (post) p.

Let $R_{◻}\supseteq E$ be a relation such that for any $z,z^{\prime }\in Z$, $z{R}_{◻}{z}^{\prime }$ iff $z^{\prime }$ can possibly get the news posted by z. By the definition of refutation clause for $◻$ (See Section 2.4), is given by $\begin{array}{r}z⊩\mathrm{◻p}\mathrm{iff}\text{for all}{\mathrm{z}}^{\prime }\mathrm{z}{\mathrm{R}}_{◻}{\mathrm{z}}^{\prime }\mathrm{implies}{\mathrm{z}}^{\prime }\nsucc \mathrm{p}.\end{array}$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⊩\mathrm{◻p}$, iff none of the possible recipients of news from z refute p. The relations $R_{◊}$ and $R_{◻}$ 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_{◊}$, 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_{◻}$ 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 $\left(\right[\left[\varphi \right]],(\left[\varphi \right]\left)\right)$, the sets $\left[\right[◻\varphi \left]\right]$ and $\left(\right[◊\varphi \left]\right)$ can be interpreted as the core followers and core news sources of this echo-chamber respectively. The conditions $E\subseteq R_{◻}$ and $E^{-1}\subseteq R_{◊}$, imply that $\left[\right[◻\varphi \left]\right]\subseteq \left[\right[\varphi \left]\right]$ and $\left(\right[◊\varphi \left]\right)\subseteq \left(\right[\varphi \left]\right)$ (and hence that $\left(\right[\varphi \left]\right)\subseteq \left(\right[◻\varphi \left]\right)$ and $\left[\right[\varphi \left]\right]\subseteq \left[\right[◊\varphi \left]\right]$) 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 (ℓ), 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:

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: $\begin{array}{r}{z}_{x}E{z}_y\mathrm{iff}\mathrm{y}{}^{\prime }\mathrm{s}\mathrm{portrayal}\mathrm{of}\mathrm{x}{}^{\prime }\mathrm{s}\text{moral agenda does not clash with}\mathrm{x}{}^{\prime }\mathrm{s}\mathrm{own}\mathrm{portrayal}.\end{array}$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 ℓ's and s's portrayal of him as a rapist, and by w's portrayal of him as clumsy, incompetent, and gullible; ℓ'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 ℓ's legitimate interest in protecting her own honour, and by ℓ's and w's portrayal of s as a cowardly and dishonourable 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⁹, where e.g. $(\mathrm{\ell s},\mathrm{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.

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, ℓ might argue that, while in the beginning b might have mistaken her character as fierce, later on he recognised this as a misunderstanding, and hence, overall, b's portrayal of ℓ is compatible with ℓ'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):

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\}$, $\begin{array}{rl}& z_x{R}_u{z}_y\mathrm{iff}\mathrm{y}{}^{\prime }\mathrm{s}\mathrm{portrayal}\mathrm{of}\mathrm{x}{}^{\prime }\mathrm{s}\mathrm{moral}\mathrm{agenda}\mathrm{does}\mathrm{not}\mathrm{clash}\mathrm{with}\mathrm{x}{}^{\prime }\mathrm{sown}\mathrm{portrayal},\\ & \mathrm{according}\mathrm{to}\mathrm{u}.\end{array}$These additional relations are all E-compatible, and each of them induces a pair of adjoint modal operators ${◊}_u⊣{◻}_u$ for any $u\in \{b,\ell ,s\}$, represented as follows¹⁰:

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}$: $\begin{array}{r}{◻}_{u}c⊢cc⊢{◊}_{u}cc⊢{◻}_u{◊}_{u}c{◊}_u{◻}_{u}c⊢c{◻}_{u}c⊢{◻}_u{◻}_{u}c{◊}_u{◊}_{u}c⊢{◊}_{u}c,\end{array}$which implies (cf. Table 3) that the relations $R_b$, $R_{\ell }$ and $R_s$ are E-reflexive and E-transitive (see Remark 3.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 {◻}_{b}c\vee {◻}_{\ell }c\vee {◻}_{s}c$ and $c\mapsto {◊}_{b}c\wedge {◊}_{\ell }c\wedge {◊}_{s}c$.

Remark 3.1

In Section 6.3, we show how the first-order correspondents of modal reduction principles in Kripke frames can be shifted (see Definition 6.3 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_{◊}$, $R_{◻}$, $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. Orlowska, 1994), 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 ‘internalising 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 $\mathrm{◊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 formalise reasoning under epistemic uncertainty (modelled by additional relations $R_{◻}$, $R_{◊}$ 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 (Conradie et al., 2019a, 2019b, 2021). These examples motivate the introduction of hyper-constructivist (or evidentialist) approximation spaces, based on graph-based frames, as a generalisation of approximation spaces to a framework with inherent informational entropy. The strategy we follow for introducing this generalisation is similar to the one adopted in Conradie et al. (2021) for introducing the notion of conceptual approximation space. Namely, we identify the defining properties of hyper-constructivist approximation spaces (cf. Definition 4.1) 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 4.1

A hyper-constructivist (or evidentialist) approximation space is a graph-based $\mathcal{L}$-frame $\mathbb{F}=(Z,E,R_{◻},R_{◊})$ such that $E\subseteq R_{◻}{◻\text{}}}_E{R}_{◼}$, where is defined as in Definition 5.1. A hyperconstructivist approximation space $\mathbb{F}=(Z,E,R_{◻},R_{◊})$ is:

1. E-reflexive if $E\subseteq R_{◻}$ and $D\subseteq R_{◊}$.

2. E-symmetric if $R_{◼}\subseteq R_{◻}$ and $R_{⧫}\subseteq R_{◊}$.

3. E-transitive if $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$ and $R_{◊}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}$.

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 generalised approximation spaces is that the indiscernibility relation be serial, since this condition is the first-order correspondent of the mrp $\mathrm{◻a}\le \mathrm{◊a}$, which guarantees that the lower approximation is smaller than or equal to the upper approximation. The ALBA outputs of $\mathrm{◻a}\le \mathrm{◊a}$ (which is an analytic inductive mrp) are $\mathrm{\forall }\mathbf{\text{j}}(\mathbf{\text{j}}\le \mathrm{◊⧫}\mathbf{\text{j}})$ and $\mathrm{\forall }\mathbf{\text{m}}(\mathrm{◻◼}\mathbf{\text{m}}\le \mathbf{\text{m}})$ (cf. Section 2.5), which, when translated in the first-order language of Kripke frames, yield the first-order correspondents $\mathrm{\forall w}\left(\right\{w\}\subseteq R_{◊}^{-1}[R_{⧫}^{-1}\left[w\right]\left]\right)$ and $\mathrm{\forall w}\left(\right(R_{◻}^{-1}\left[\right(R_{◼}^{-1}\left[\right\{w{\}}^{\mathrm{cc}}\left]{)}^{\mathrm{cc}}\right]{)}^c\subseteq \left\{w{\}}^c\right)$, which can be respectively unravelled as $\mathrm{\forall w}\mathrm{\exists v}\left(w{R}_{◊}v\mathrm{\&}v{R}_{⧫}w\right)$ and $\mathrm{\forall w}\mathrm{\exists v}\left(w{R}_{◻}v\mathrm{\&}v{R}_{◼}w\right)$. These first-order sentences can equivalently be rewritten as the relational inclusions $\mathrm{\Delta }\subseteq R_{◊}\circ R_{⧫}$ and $\mathrm{\Delta }\subseteq R_{◻}\circ R_{◼}$, respectively. Translating the ALBA outputs above in the first-order language of graph-based frames yields $\begin{array}{r}\mathrm{\forall }z\left(R_{◊}^{\left[0\right]}\right[E^{\left[0\right]}\left[R_{⧫}^{\left[0\right]}\right[z^{\left[10\right]}\left]\right]]\subseteq z^{\left[1\right]})\mathrm{and}\mathrm{\forall z}\left({\mathrm{R}}_{◻}^{\left[0\right]}\right[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{R}}_{◼}^{\left[0\right]}\right[{\mathrm{z}}^{\left[01\right]}\left]\right]]\subseteq {\mathrm{z}}^{\left[0\right]}).\end{array}$By the E-compatibility of $R_{◻}$ and $R_{◊}$ (cf. Lemma 2.4) these inclusions can be simplified as follows: $\begin{array}{r}\mathrm{\forall }z\left(R_{◊}^{\left[0\right]}\right[E^{\left[0\right]}\left[R_{⧫}^{\left[0\right]}\right[z\left]\right]]\subseteq z^{\left[1\right]})\mathrm{and}\mathrm{\forall }\mathrm{z}\left({\mathrm{R}}_{◻}^{\left[0\right]}\right[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{R}}_{◼}^{\left[0\right]}\right[\mathrm{z}\left]\right]]\subseteq {\mathrm{z}}^{\left[0\right]}),\end{array}$and then be partially unravelled as the following implications (recall that $D:=E^{-1})$: $\begin{array}{r}\mathrm{\forall }x\mathrm{\forall z}(x\in R_{◊}^{\left[0\right]}[E^{\left[0\right]}\left[R_{⧫}^{\left[0\right]}\right[z\left]\right]]\Rightarrow x{D}^{c}z)\mathrm{and}\mathrm{\forall }\mathrm{a\forall z}(\mathrm{a}\in {\mathrm{R}}_{◻}^{\left[0\right]}[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{R}}_{◼}^{\left[0\right]}\right[\mathrm{z}\left]\right]]\Rightarrow \mathrm{a}{\mathrm{E}}^{\mathrm{c}}\mathrm{z}),\end{array}$which, on application of contraposition yields $\begin{array}{r}\mathrm{\forall }x\mathrm{\forall z}(\mathrm{xDz}\Rightarrow x\notin R_{◊}^{\left[0\right]}[E^{\left[0\right]}\left[R_{⧫}^{\left[0\right]}\right[z\left]\right]\left]\right)\mathrm{and}\mathrm{\forall }\mathrm{a\forall z}(\mathrm{aEz}\Rightarrow \mathrm{a}\notin {\mathrm{R}}_{◻}^{\left[0\right]}[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{R}}_{◼}^{\left[0\right]}\right[\mathrm{z}\left]\right]\left]\right),\end{array}$and then as follows: $\begin{array}{r}\mathrm{\forall }x\mathrm{\forall z}(\mathrm{xDz}\Rightarrow x(R_{◊}{◊\text{}}}_E{R}_{⧫}\left)z\right)\mathrm{and}\mathrm{\forall }\mathrm{a\forall z}(\mathrm{aEz}\Rightarrow \mathrm{a}({\mathrm{R}}_{◻}{◻\text{}}}_{\mathrm{E}}{\mathrm{R}}_{◼}\left)\mathrm{z}\right),\end{array}$by letting $x\left(R_{◊}{◊\text{}}}_E{R}_{⧫}\right)z$ iff $x\notin R_{◊}^{\left[0\right]}\left[E^{\left[0\right]}\right[R_{⧫}^{\left[0\right]}\left[z\right]\left]\right]$, and $a\left(R_{◻}{◻\text{}}}_E{R}_{◼}\right)z$ iff $a\notin R_{◻}^{\left[0\right]}\left[E^{\left[1\right]}\right[R_{◼}^{\left[0\right]}\left[z\right]\left]\right]$. These ‘abbreviations’, which are in fact instances of the notion of E-mediated composition (cf. Definition 5.1 in Section 5.1, below), allow us to equivalently rewrite these first-order sentences as relational inclusions $D\subseteq R_{◊}{◊\text{}}}_E{R}_{⧫}$ and $E\subseteq R_{◻}{◻\text{}}}_E{R}_{◼}$, respectively.

What is more, when rewritten in this way, it is possible to recognise 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:=\mathrm{\Delta }$ in $D\subseteq R_{◊}{◊\text{}}}_E{R}_{⧫}$, one obtains a condition which is equivalent to $\mathrm{\Delta }\subseteq R_{◊}\circ R_{⧫}$, 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 Δ to E.

In Section 6.3, we show that this transfer of properties and constructions, formalised in terms of the notion of shifting (cf. Definition 6.3), 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 generalised 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 7.1, 7.2, 7.3).

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 (Conradie et al., 2019b, 2022). We also introduce the relational languages ${\mathsf{\text{KRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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{\text{GRel}}$ to $\mathsf{\text{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 Conradie et al. (2021, Section 3.4). As will be clear from Lemma 5.1, the E-compositions can be understood as the counterparts of the usual composition of relations in the setting of graph-based frames.

Definition 5.1

For any graph $\mathbb{G}=(Z,E)$, and any $R,T\subseteq Z\times Z$, the E-mediated compositions $R{◊\text{}}}_{E}T$ and $R{◻\text{}}}_{E}T$ and the composition $R\ast T\subseteq Z\times Z$ are defined as follows: for all $a,x\in Z$, $\begin{array}{r}\begin{array}{lll}x\left(R{◊\text{}}}_{E}T\right)a& \mathrm{iff}\mathrm{x}\in \left({\mathrm{R}}^{\left[0\right]}\right[{\mathrm{E}}^{\left[0\right]}\left[{\mathrm{T}}^{\left[0\right]}\right[\mathrm{a}\left]\right]]{)}^{\mathrm{c}}& \mathrm{i}.\mathrm{e}.\left(\mathrm{R}{◊\text{}}}_{\mathrm{E}}\mathrm{T}{)}^{\left[0\right]}\right[\mathrm{a}]={\mathrm{R}}^{\left[0\right]}[{\mathrm{E}}^{\left[0\right]}\left[{\mathrm{T}}^{\left[0\right]}\right[\mathrm{a}\left]\right]]\\ a\left(R{◻\text{}}}_{E}T\right)x& \mathrm{iff}\mathrm{a}\in \left({\mathrm{R}}^{\left[0\right]}\right[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{T}}^{\left[0\right]}\right[\mathrm{x}\left]\right]]{)}^{\mathrm{c}}& \mathrm{i}.\mathrm{e}.\left(\mathrm{R}{◻\text{}}}_{\mathrm{E}}\mathrm{T}{)}^{\left[0\right]}\right[\mathrm{x}]={\mathrm{R}}^{\left[0\right]}[{\mathrm{E}}^{\left[1\right]}\left[{\mathrm{T}}^{\left[0\right]}\right[\mathrm{x}\left]\right]]\\ a(R\ast T)x& \mathrm{iff}\mathrm{a}\in \left({\mathrm{R}}^{\left[0\right]}\right[{\mathrm{T}}^{\left[0\right]}\left[\mathrm{x}\right]]{)}^{\mathrm{c}}& \mathrm{i}.\mathrm{e}.(\mathrm{R}\ast \mathrm{T}{)}^{\left[0\right]}[\mathrm{x}]={\mathrm{R}}^{\left[0\right]}[{\mathrm{T}}^{\left[0\right]}\left[\mathrm{x}\right]].\end{array}\end{array}$

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:=\mathrm{\Delta }$.

Lemma 5.1

For all sets S, all relations $R,T\subseteq S\times S$ on the graph ${\mathbb{G}}_S=(S,\mathrm{\Delta })$, $\begin{array}{r}R{◊\text{}}}_{\mathrm{\Delta }}T=R{◻\text{}}}_{\mathrm{\Delta }}T=R\circ T.\end{array}$

The following lemma shows that the E-mediated compositions and 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 5.2

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

(1)	if R is E-compatible, then $R{◊\text{}}}_{E}D=R=D{◊\text{}}}_{E}R\mathrm{and}\mathrm{R}{◻\text{}}}_{\mathrm{E}}\mathrm{E}=\mathrm{R}=\mathrm{E}{◻\text{}}}_{\mathrm{E}}\mathrm{R}$;
(2)	if R is E-compatible, then so are $R{◊\text{}}}_{E}T$, $R{◻\text{}}}_{E}T$, and $R\ast T$;
(3)	if R and T are E-compatible, then $\left(R{◊\text{}}}_{E}T{)}^{\left[0\right]}\right[Y]=R^{\left[0\right]}[E^{\left[0\right]}\left[T^{\left[0\right]}\right[Y\left]\right]]$  and  $\left(R{◻\text{}}}_{E}T{)}^{\left[0\right]}\right[Y]=R^{\left[0\right]}[E^{\left[1\right]}\left[T^{\left[0\right]}\right[Y\left]\right]]$;
(4)	if R, T, and U are E-compatible, then $R{◊\text{}}}_E\left(T{◊\text{}}}_{E}U\right)=\left(R{◊\text{}}}_{E}T\right){◊\text{}}}_{E}U$  and  $R{◻\text{}}}_E\left(T{◻\text{}}}_{E}U\right)=\left(R{◻\text{}}}_{E}T\right){◻\text{}}}_{E}U$.

Proof.

(1) For any $a\in Z$, $\left(R{◊\text{}}}_{E}D{)}^{\left[0\right]}\right[a]=R^{\left[0\right]}[E^{\left[0\right]}\left[D^{\left[0\right]}\right[a\left]\right]]=R^{\left[0\right]}[E^{\left[0\right]}\left[E^{\left[1\right]}\right[a\left]\right]]=R^{\left[0\right]}[a]$, the last identity holding by the E-compatibility of R. The remaining identities are omitted.

(2) For any $a\in Z$, $\begin{array}{rl}\left(\right(R{◊\text{}}}_{E}T{)}^{\left[0\right]}\left[a\right]{)}^{\left[10\right]}& =\left(R^{\left[0\right]}\right[E^{\left[0\right]}\left[T^{\left[0\right]}\right[a\left]\right]]{)}^{\left[10\right]}\text{Definition 5.1 (i)}\\ & =R^{\left[0\right]}\left[E^{\left[0\right]}\right[T^{\left[0\right]}\left[a\right]\left]\right]\text{Lemma 2.4}\\ & =\left(R{◊\text{}}}_{E}T{)}^{\left[0\right]}\right[a].\text{Definition 5.1 (i)}\end{array}$The remaining identities are proven similarly.

(3) We only prove the first statement. $\begin{array}{rl}{R}^{\left[0\right]}\left[E^{\left[0\right]}\right[T^{\left[0\right]}\left[Y\right]\left]\right]& =R^{\left[0\right]}\left[E^{\left[0\right]}\left[T^{\left[0\right]}\left[\bigcup _{y\in Y}y\right]\right]\right]Y=\bigcup _{y\in Y}y\\ & =R^{\left[0\right]}\left[E^{\left[0\right]}\left[\bigcap _{y\in Y}{T}^{\left[0\right]}\right[y\left]\right]\right]\text{Lemma 2.1 (v)}\\ & =R^{\left[0\right]}\left[E^{\left[0\right]}\left[\bigcap _{y\in Y}{E}^{\left[1\right]}\right[E^{\left[0\right]}\left[T^{\left[0\right]}\right[y\left]\right]\left]\right]\right]E\text{-compatibilty of}T\\ & =R^{\left[0\right]}\left[E^{\left[0\right]}\left[E^{\left[1\right]}\left[\bigcup _{y\in Y}{E}^{\left[0\right]}\right[T^{\left[0\right]}\left[y\right]\left]\right]\right]\right]\text{Lemma 2.1 (v)}\\ & =R^{\left[0\right]}\left[\bigcup _{y\in Y}{E}^{\left[0\right]}\right[T^{\left[0\right]}\left[y\right]\left]\right]E\text{-compatibilty of}R\\ & =\bigcap _{y\in Y}{R}^{\left[0\right]}\left[E^{\left[0\right]}\right[T^{\left[0\right]}\left[y\right]\left]\right]\text{Lemma 2.1 (v)}\\ & =\bigcap _{y\in Y}\left(R{◊\text{}}}_{E}T{)}^{\left[0\right]}\right[y]\text{Definition 5.1 (i)}\\ & =\left(R{◊\text{}}}_{E}T{)}^{\left[0\right]}\right[Y].\text{Lemma 2.1 (v)}\end{array}$(4) Immediate consequence of item 3.

Remark 5.1

In general, *-composition is not associative; let us build a counterexample to $R\ast (T\ast U)=(R\ast T)\ast U$. Let $\mathbb{G}=(Z,\mathrm{\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=\mathrm{\Delta }$, respectively. Since $E=\mathrm{\Delta }$, every set is Galois-stable, hence all three relations are E-compatible. For any $x\in Z$, $\begin{array}{rl}{R}^{\left[0\right]}\left[\right(T\ast U{)}^{\left[0\right]}\left[x\right]]& =R^{\left[0\right]}\left[T^{\left[0\right]}\right[U^{\left[0\right]}\left[x\right]\left]\right]\mathrm{Definition}\\ & =R^{\left[0\right]}\left[T^{\left[0\right]}\right[Z\left]\right]U=\varnothing \\ & =R^{\left[0\right]}\left[\right\{b\in Z|\mathrm{\forall w}(w\in Z\Rightarrow b{\mathrm{\Delta }}^{c}w)\left\}\right]T=\mathrm{\Delta }\\ & =R^{\left[0\right]}\left[\varnothing \right]\\ & =\{b\in Z|\mathrm{\forall w}(w\in \varnothing \Rightarrow b{R}^{c}w\left)\right\}\\ & =Z\\ (R\ast T{)}^{\left[0\right]}[U^{\left[0\right]}\left[x\right]]& =(R\ast T{)}^{\left[0\right]}[Z]U=\varnothing \\ & =\{b\in Z|\mathrm{\forall w}(w\in Z\Rightarrow b(R\ast T{)}^{c}w)\left\}\mathrm{Definition}\mathrm{of}\right(-{)}^{\left[0\right]}\\ & =\{b\in Z|\mathrm{\forall w}(w\in Z\Rightarrow b\in R^{\left[0\right]}\left[T^{\left[0\right]}\right[w\left]\right]\left)\right\}\mathrm{Definition}\mathrm{of}\ast \\ & =\bigcap _{w\in Z}{R}^{\left[0\right]}\left[T^{\left[0\right]}\right[w\left]\right]\\ & =\bigcap _{w\in Z}{R}^{\left[0\right]}[Z\setminus \{w\left\}\right]T=\mathrm{\Delta }\\ & =R^{\left[0\right]}[\bigcup _{w\in Z}Z\setminus \{w\left\}\right]\text{Lemma 2.1}\\ & =R^{\left[0\right]}\left[Z\right]\\ & =\{b\in Z|\mathrm{\forall w}(w\in Z\Rightarrow b{R}^{c}w\left)\right\}\\ & =\varnothing R=Z\times Z\end{array}$

Remark 5.2

In general, *-composition is not associative. It is easy to show a counterexample analogous to the one in Remark 5.1 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\left)\right)$.

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 5.2

The relation algebras associated with any graph-based frame $\mathbb{F}=(Z,E,R_{◊},R_{◻})$, and any Kripke frame $\mathbb{X}=(W,R_{◊},R_{◻})$ are respectively defined as follows: $\begin{array}{r}{\mathbb{F}}^{\ast }:=\left(\mathcal{P}\right(Z\times Z),E,D,R_{◊},R_{⧫},R_{◻},R_{◼},{◊\text{}}}_E,{◻\text{}}}_E,\ast ),{\mathbb{X}}^{\ast }:=\left(\mathcal{P}\right(W\times W),\mathrm{\Delta },R_{◊},R_{⧫},R_{◻},R_{◼},\circ ,\star ),\end{array}$where $R_{⧫}$ and $R_{◼}$ denote the converse relations of $R_{◻}$ and $R_{◊}$ respectively, the binary operations ${◊\text{}}}_E,{◻\text{}}}_E$ and * are defined as in Definition 5.1, the binary operation ° is the standard relational composition, and ★ is defined by the same assignment as *.

Consider the set ${\mathsf{\text{Rel}}}_{\mathcal{L}}:=\{\mathrm{\Delta },E,D,R_{◊},R_{⧫},R_{◻},R_{◼}\}$ of constant symbols. The propositional languages ${\mathsf{\text{KRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{GRel}}}_{\mathcal{L}}$ associated with Kripke frames (resp. graph-based frames) are defined by the following recursions: $\begin{array}{rl}& {\mathsf{KRel}}_{\mathcal{L}}\ni \xi ::=\mathrm{\Delta }|R_{◊}|R_{⧫}|R_{◻}|R_{◼}|\xi \circ \xi |\xi \star \xi ,\\ & {\mathsf{GRel}}_{\mathcal{L}}\ni \alpha ::=D|E|R_{◊}|R_{⧫}|R_{◻}|R_{◼}|\alpha {◊\text{}}}_E\alpha |\alpha {◻\text{}}}_E\alpha |\alpha \ast \alpha ,\end{array}$where the intended interpretation of the constant symbols on graph-based frames and on Kripke frames is the obvious one. Term inequalities of ${\mathsf{\text{KRel}}}_{\mathcal{L}}$ (resp. ${\mathsf{\text{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, $\begin{array}{r}\mathbb{X}\models {\xi }_1\subseteq {\xi }_2\mathrm{iff}{\mathbb{X}}^{\ast }\models {\xi }_1\subseteq {\xi }_2\mathrm{and}\mathbb{F}\models {\alpha }_1\subseteq {\alpha }_2\mathrm{iff}{\mathbb{F}}^{\ast }\models {\alpha }_1\subseteq {\alpha }_2.\end{array}$A natural translation exists between ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-terms and ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-terms which is defined as follows.

Definition 5.3

Let $\tau :{\mathsf{\text{GRel}}}_{\mathcal{L}}\to {\mathsf{\text{KRel}}}_{\mathcal{L}}$ be defined as follows: $\begin{array}{r}\begin{array}{ll}\tau \left(E\right)=\mathrm{\Delta }& \tau \left(D\right)=\mathrm{\Delta }\\ \tau \left(R_{◊}\right)=R_{◊}& \tau \left(R_{⧫}\right)=R_{⧫}\\ \tau \left(R_{◻}\right)=R_{◻}& \tau \left(R_{◼}\right)=R_{◼}\\ \tau \left({\alpha }_1{◊\text{}}}_E{\alpha }_2\right)=\tau \left({\alpha }_1\right)\circ \tau \left({\alpha }_2\right)& \tau \left({\alpha }_1{◻\text{}}}_E{\alpha }_2\right)=\tau \left({\alpha }_1\right)\circ \tau \left({\alpha }_2\right)\\ \tau ({\alpha }_1\ast {\alpha }_2)=\tau \left({\alpha }_1\right)\star \tau \left({\alpha }_2\right)& \tau ({\alpha }_1\ast {\alpha }_2)=\tau \left({\alpha }_1\right)\star \tau \left({\alpha }_2\right).\end{array}\end{array}$

Lemma 5.3

For any Kripke frame $\mathbb{X}$, any ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality ${\alpha }_1\subseteq {\alpha }_2$, and any $\alpha \in {\mathsf{\text{GRel}}}_{\mathcal{L}}$

(1)	${\alpha }^{{\mathbb{F}}_{\mathbb{X}}}=\tau (\alpha {)}^{\mathbb{X}}$,
(2)	${\mathbb{F}}_{\mathbb{X}}\models {\alpha }_1\subseteq {\alpha }_2\text{iff}\mathbb{X}\models \tau \left({\alpha }_1\right)\subseteq \tau \left({\alpha }_2\right).$

Proof.

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

In the next section we represent the first-order correspondents of inductive mrps as term inequalities of ${\mathsf{\text{GRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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{\text{GRel}}}_{\mathcal{L}}$ and ${\mathsf{\text{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.1

The first-order correspondent of any inductive mrp on graph-based (resp. Kripke) frames can be represented as a term inequality in ${\mathsf{\text{GRel}}}_{\mathcal{L}}$ (resp. ${\mathsf{\text{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 6.1

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

1. if $\phi (!w)$ (resp. $\psi (!w)$) is a finite (possibly empty) concatenation of diamond (resp. box) connectives, let us define $R_{\varphi }\in {\mathsf{\text{GRel}}}_{\mathcal{L}}$ (resp. $R_{\psi }\in {\mathsf{\text{GRel}}}_{\mathcal{L}}$) by induction on ϕ (resp.  ψ) as follows:

   if $\varphi :=y$, then $R_{\varphi }:=D$;  if $\varphi :=f{\varphi }^{\prime }$ with $f\in \{◊,⧫\}$, then $R_{\varphi }:=R_f{◊\text{}}}_E{R}_{{\varphi }^{\prime }}$;

   if $\psi :=y$, then $R_{\psi }:=E$;  if $\psi :=g{\psi }^{\prime }$ with $g\in \{◻,◼\}$, then $R_{\psi }:=R_g{◻\text{}}}_E{R}_{{\psi }^{\prime }}$;

2. if $\chi (!w)={\varphi }_1{\psi }_1\dots {\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{\text{GRel}}}_{\mathcal{L}}$ is defined as follows:

   if ${\psi }_{n_{\chi }}$ is empty, $R_{\chi }:=R_{{\phi }_1}\ast R_{{\psi }_1}\ast \cdots \ast R_{{\phi }_{n_{\chi }}}$;

   if ${\psi }_{n_{\chi }}$ is nonempty, $R_{\chi }:=R_{{\phi }_1}\ast R_{{\psi }_1}\ast \cdots \ast R_{{\phi }_{n_{\chi }}}\ast R_{{\psi }_{n_{\chi }}}\ast D;$

3. if $\zeta (!w)={\psi }_1{\varphi }_1\dots {\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{\text{GRel}}}_{\mathcal{L}}$ is defined as follows:

   if ${\varphi }_{n_{\zeta }}$ is empty, $R_{\zeta }:=R_{{\psi }_1}\ast R_{{\varphi }_1}\ast \cdots \ast R_{{\psi }_{n_{\zeta }}};$

   if ${\varphi }_{n_{\zeta }}$ is nonempty, $R_{\zeta }:=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 6.1 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 χ and ζ; however, a more limited version applies for singleton subsets.

Lemma 6.1

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

(1)	$\left(\right[\phi (!t)\left]\right)(t:=(B^{\left[10\right]},B^{\left[1\right]})=R_{\phi }^{\left[0\right]}[B]$  and  $\left[\right[\psi (!t)\left]\right](t:=Y=(Y^{\left[0\right]},Y^{\left[01\right]}\left)\right)=R_{\psi }^{\left[0\right]}\left[Y\right]$;
(2)	$\left(\right[\chi [\mathbf{\text{j}}/!t]\left]\right)(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]}\left)\right)=R_{\chi }^{\left[0\right]}\left[a^{\left[10\right]}\right]=R_{\chi }^{\left[0\right]}\left[a\right]$;
(3)	$\left[\right[\zeta [\mathbf{\text{m}}/!t]\left]\right](\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]})=R_{\zeta }^{\left[0\right]}[x^{\left[01\right]}]=R_{\zeta }^{\left[0\right]}[x]$.

Proof.

Item (1) can be shown straightforwardly by induction on φ and ψ, using Lemma 5.2 (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 5.1.

As discussed in Section 2.5, the ALBA output of mrps of type (a) is $\begin{array}{r}\mathrm{\forall }\mathbf{\text{j}}\left(\mathsf{LA}\right(\psi \left)\right[\varphi [\mathbf{\text{j}}/!y]/!u]\le \chi [\mathsf{LA}\left(\alpha \right)[\mathbf{\text{j}}/!u]/p\left]\right).\end{array}$When interpreted on graph-based frames, the condition above translates as follows: (3) $\begin{array}{r}\mathrm{\forall a}\left(\right(\left[\chi \left[\mathsf{LA}\right(\alpha \left)\right[\mathbf{\text{j}}/!u\left]/p\right]\right]\left)\right(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]}))\subseteq (\left[\mathsf{LA}\left(\psi \right)\left[\varphi \right[\mathbf{\text{j}}/!y]/!u]\right]\left)\right(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]})).\end{array}$(3) Since $\mathsf{\text{LA}}\left(\psi \right)\left[\varphi \right(!y)/!u]$ and $\chi \left[\mathsf{\text{LA}}\right(\alpha \left)/p\right]$ are of the shape required by by items (1) and (2) of Lemma 6.1 respectively, the following identities hold: $\begin{array}{r}\begin{array}{l}\left(\right[\mathsf{LA}\left(\psi \right)\left[\varphi \right[\mathbf{\text{j}}/!y]/!u]\left]\right)(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]})=R_{\mathsf{LA}\left(\psi \right)[\varphi /!u]}^{\left[0\right]}[a^{\left[10\right]}]=(R_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_E{R}_{\varphi }{)}^{\left[0\right]}\left[a\right].\\ \left(\right[\chi \left[\mathsf{LA}\right(\alpha \left)\right[\mathbf{\text{j}}/!u\left]/p\right]\left]\right)(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]}\left)\right)=R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{\left[0\right]}\left[a^{\left[10\right]}\right]=R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{\left[0\right]}\left[a\right].\end{array}\end{array}$Hence, (3(3) $\begin{array}{r}\mathrm{\forall a}\left(\right(\left[\chi \left[\mathsf{LA}\right(\alpha \left)\right[\mathbf{\text{j}}/!u\left]/p\right]\right]\left)\right(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]}))\subseteq (\left[\mathsf{LA}\left(\psi \right)\left[\varphi \right[\mathbf{\text{j}}/!y]/!u]\right]\left)\right(\mathbf{\text{j}}:=(a^{\left[10\right]},a^{\left[1\right]})).\end{array}$(3) ) can be rewritten as follows: (4) $\begin{array}{r}\mathrm{\forall a}\left(R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{\left[0\right]}\right[a]\subseteq (R_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_E{R}_{\varphi }{)}^{\left[0\right]}\left[a\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_{\mathrm{E}}{\mathrm{R}}_{\varphi }\subseteq {\mathrm{R}}_{\chi \left[\mathsf{LA}\right(\alpha \left)/\mathrm{p}\right]}\end{array}$(4) Similarly, the ALBA output of mrps of type (b) can be represented as follows: $\begin{array}{r}\mathrm{\forall }\mathbf{\text{m}}\left(\zeta \right[\mathsf{RA}\left(\delta \right)[\mathbf{\text{m}}/!u]/p]\le \mathsf{RA}(\varphi \left)\right[\psi [\mathbf{\text{m}}/!y]/!u\left]\right),\end{array}$and, when interpreted on graph-based frames, the condition translates as follows: (5) $\begin{array}{r}\mathrm{\forall x}\left(\right[\left[\zeta \left[\mathsf{RA}\right(\delta \left)\right[\mathbf{\text{m}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]}))\subseteq [\left[\mathsf{RA}\left(\varphi \right)\left[\psi \right[\mathbf{\text{m}}/!y]/!u]\right]\left]\right(\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]})\left)\right).\end{array}$(5) By items (3) and (1) of Lemma 6.1, $\begin{array}{r}\begin{array}{l}\left[\right[\mathsf{RA}\left(\varphi \right)\left[\psi \right[\mathbf{\text{m}}/!y\left]/!u\right]\left]\right](\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]}\left)\right)=R_{\mathsf{RA}\left(\varphi \right)\left[\psi /!u\right]}^{\left[0\right]}\left[x^{\left[01\right]}\right]=\left(R_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_E{R}_{\psi }{)}^{\left[0\right]}\right[x].\\ [\left[\zeta \left[\mathsf{RA}\right(\delta \left)\right[\mathbf{\text{m}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]}))=R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{\left[0\right]}[x^{\left[01\right]}]=R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{\left[0\right]}[x].\end{array}\end{array}$Therefore, we can rewrite (5(5) $\begin{array}{r}\mathrm{\forall x}\left(\right[\left[\zeta \left[\mathsf{RA}\right(\delta \left)\right[\mathbf{\text{m}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]}))\subseteq [\left[\mathsf{RA}\left(\varphi \right)\left[\psi \right[\mathbf{\text{m}}/!y]/!u]\right]\left]\right(\mathbf{\text{m}}:=(x^{\left[0\right]},x^{\left[01\right]})\left)\right).\end{array}$(5) ) as follows: (6) $\begin{array}{r}\mathrm{\forall x}\left(R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{\left[0\right]}\right[x]\subseteq (R_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_E{R}_{\psi }{)}^{\left[0\right]}\left[x\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_{\mathrm{E}}{\mathrm{R}}_{\psi }\subseteq {\mathrm{R}}_{\zeta \left[\mathsf{RA}\right(\delta \left)/\mathrm{p}\right]}.\end{array}$(6) Finally, notice that, if the mrp is also analytic, the shape of $\chi \left(p\right)$ (resp. $\zeta \left(p\right)$) simplifies to $\chi \left(p\right)={\varphi }_{n_{\chi }}{\psi }_{n_{\chi }}\left(p\right)$ with $n_{\chi }=1$ and ${\psi }_{n_{\chi }}$ empty (resp. $\zeta \left(p\right)={\psi }_{n_{\zeta }}{\varphi }_{n_{\zeta }}\left(p\right)$ with $n_{\zeta }=1$ and ${\varphi }_{n_{\zeta }}$ empty). Hence, (4(4) $\begin{array}{r}\mathrm{\forall a}\left(R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{\left[0\right]}\right[a]\subseteq (R_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_E{R}_{\varphi }{)}^{\left[0\right]}\left[a\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_{\mathrm{E}}{\mathrm{R}}_{\varphi }\subseteq {\mathrm{R}}_{\chi \left[\mathsf{LA}\right(\alpha \left)/\mathrm{p}\right]}\end{array}$(4) ) and (6(6) $\begin{array}{r}\mathrm{\forall x}\left(R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{\left[0\right]}\right[x]\subseteq (R_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_E{R}_{\psi }{)}^{\left[0\right]}\left[x\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_{\mathrm{E}}{\mathrm{R}}_{\psi }\subseteq {\mathrm{R}}_{\zeta \left[\mathsf{RA}\right(\delta \left)/\mathrm{p}\right]}.\end{array}$(6) ) simplify to the following inclusions: (7) $\begin{array}{r}{R}_{\mathsf{LA}\left(\psi \right)}{◊\text{}}}_E{R}_{\varphi }\subseteq R_{{\varphi }_{n_{\chi }}}{◊\text{}}}_E{R}_{\mathsf{LA}\left(\alpha \right)}{R}_{\mathsf{RA}\left(\varphi \right)}{◻\text{}}}_E{R}_{\psi }\subseteq R_{{\psi }_{n_{\zeta }}}{◻\text{}}}_E{R}_{\mathsf{RA}\left(\delta \right)}.\end{array}$(7)

Example 6.1

The mrp $p\le \mathrm{◊◻p}$ is inductive of type (a), where $\varphi \left(y\right):=y$, and $\alpha \left(p\right):=p$, hence $\mathsf{\text{LA}}\left(\alpha \right)\left(u\right):=u$, and $\psi \left(x\right):=x$, hence $\mathsf{\text{LA}}\left(\psi \right)\left(v\right):=v$, and $\chi \left(p\right):=\mathrm{◊◻p}$. Then the ALBA output of this inequality is $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{j}}\left(\right[\left[\mathbf{\text{j}}/y\right]/v]\le \mathrm{◊◻}[\left[\mathbf{\text{j}}/u\right]/p\left]\right),\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}(\mathbf{\text{j}}\le \mathrm{◊◻}\mathbf{\text{j}})\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}\left(\right(\left[\mathrm{◊◻}\mathbf{\text{j}}\right])\subseteq (\left[\mathbf{\text{j}}\right]\left)\right)\left(\mathrm{definition}\mathrm{of}\mathrm{order}\mathrm{on}\mathrm{polarities}\right)\\ \mathrm{iff}& \mathrm{\forall a}\left(R_{◊}^{\left[0\right]}\right[R_{◻}^{\left[0\right]}\left[E^{\left[1\right]}\right[a\left]\right]]\subseteq E^{\left[1\right]}[a\left]\right)\left(\mathrm{standard}\mathrm{translation}\right)\\ \mathrm{iff}& \mathrm{\forall }a\left(\right(R_{◊}\ast R_{◻}\ast D{)}^{\left[0\right]}\left[a\right]\subseteq \left(D{)}^{\left[0\right]}\right[a\left]\right)\text{(Definition 5.1)}\\ \mathrm{iff}& D\subseteq R_{◊}\ast R_{◻}\ast D.\text{(Lemma 2.1)}\end{array}$

Example 6.2

The mrp $\mathrm{◻◊p}\le \mathrm{◻◊◊p}$ is inductive of shape (b) with $\varphi \left(y\right):=y$, hence $\mathsf{\text{RA}}\left(\varphi \right)\left(v\right):=v$ and $\psi \left(x\right):=\mathrm{◻x}$, and $\delta \left(p\right):=\mathrm{◊◊p}$, hence $\mathsf{\text{RA}}\left(\delta \right)\left(u\right):=\mathrm{◼◼u}$, and $\chi \left(p\right):=\mathrm{◻◊p}$. $\begin{array}{rl}& \mathrm{\forall p}[\mathrm{◻◊p}\le \mathrm{◻◊◊p}]\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{m}}[\mathrm{◻◊◼◼}\mathbf{\text{m}}\le ◻\mathbf{\text{m}}]\mathrm{ALBA}\mathrm{output}\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall x}\left(R_{◻}^{\left[0\right]}\right[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[E^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x^{\downarrow \uparrow }\left]\right]\left]\right]\subseteq R_{◻}^{\left[0\right]}\left[x^{\downarrow \uparrow }\right])\\ \mathrm{iff}& \mathrm{\forall x}\left(R_{◻}^{\left[0\right]}\right[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[E^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x\left]\right]\left]\right]]\subseteq R_{◻}^{\left[0\right]}[x\left]\right)\left(R_{◻}\mathrm{and}{\mathrm{R}}_{◊}\mathrm{E}-\mathrm{compatible}\right)\\ \mathrm{iff}& \mathrm{\forall x}\mathrm{\forall a}(a\in R_{◻}^{\left[0\right]}[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[E^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x\left]\right]\left]\right]]\Rightarrow a\in R_{◻}^{\left[0\right]}[x\left]\right)\\ \mathrm{iff}& \mathrm{\forall x}\mathrm{\forall a}\left(a\right(R_{◻}\ast R_{◊}\ast \left(R_{◼}{◻\text{}}}_E{R}_{◼}\right){)}^{c}x\Rightarrow a{R}_{◻}^{c}x)\\ \mathrm{iff}& R_{◻}\subseteq R_{◻}\ast R_{◊}\ast \left(R_{◼}{◻\text{}}}_E{R}_{◼}\right).\end{array}$

6.2. Correspondents on Kripke frames

In the present subsection, which is an adaptation of Conradie et al. (2022, Section 4.2), we specialise 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 6.2

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

1. if $\phi (!w)$ (resp. $\psi (!w)$) is a finite (possibly empty) concatenation of diamond (resp. box) connectives, let us define $R_{\varphi }\in {\mathsf{\text{KRel}}}_{\mathcal{L}}$ (resp. $R_{\psi }\in {\mathsf{\text{KRel}}}_{\mathcal{L}}$) by induction on ϕ (resp. ψ) as follows:

   if $\varphi :=y$, then $R_{\varphi }:=\mathrm{\Delta }$;  if $\varphi :=f{\varphi }^{\prime }$ with $f\in \{◊,⧫\}$, then $R_{\varphi }:=R_f\circ R_{{\varphi }^{\prime }}$.

   if $\psi :=y$, then $R_{\psi }:=\mathrm{\Delta }$;  if $\psi :=g{\psi }^{\prime }$ with $g\in \{◻,◼\}$, then $R_{\psi }:=R_g\circ R_{{\psi }^{\prime }}$.

2. if $\chi (!w)={\varphi }_1{\psi }_1\dots {\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{\text{KRel}}}_{\mathcal{L}}$ by induction on $n_{\chi }$ as follows:

   if ${\psi }_{n_{\chi }}$ is empty, $R_{\chi }:=R_{{\phi }_1}\star R_{{\psi }_1}\star \cdots \star R_{{\phi }_{n_{\chi }}}$;

   if ${\psi }_{n_{\chi }}$ is nonempty, $R_{\chi }:=R_{{\phi }_1}\star R_{{\psi }_1}\star \cdots \star R_{{\phi }_{n_{\chi }}}\star R_{{\psi }_{n_{\chi }}}\star \mathrm{\Delta }$.

3. if $\zeta (!w)={\psi }_1{\varphi }_1\dots {\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{\text{KRel}}}_{\mathcal{L}}$ by induction on $n_{\zeta }$ as follows:

   if ${\varphi }_{n_{\zeta }}$ is empty, $R_{\zeta }:=R_{{\psi }_1}\star R_{{\varphi }_1}\star \cdots \star R_{{\psi }_{n_{\zeta }}};$

   if ${\varphi }_{n_{\zeta }}$ is nonempty, $R_{\zeta }:=R_{{\psi }_1}\star R_{{\varphi }_1}\star \cdots \star R_{{\psi }_{n_{\zeta }}}\star R_{{\varphi }_{n_{\zeta }}}\star \mathrm{\Delta }$.

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

Lemma 6.2

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

(1)	$\left[\right[\phi (!w)\left]\right](w:=S)=〈R_{\phi }〉S\mathrm{and}\left[\right[\psi (!\mathrm{w})\left]\right](\mathrm{w}:=\mathrm{S})=\left[{\mathrm{R}}_{\psi }\right]\mathrm{S}.$
(2)	$\left[\right[\chi [\mathbf{\text{j}}/!w]\left]\right](\mathbf{\text{j}}:=\{a\left\}\right)=〈R_{\chi }〉\left\{a\right\}.$
(3)	$\left[\right[\zeta [\mathbf{\text{m}}/!w]\left]\right](\mathbf{\text{m}}:=\{x{\}}^c)=[R_{\zeta }\left]\right\{x{\}}^c.$

Proof.

Item (1) is proved by induction on the complexity of φ and ψ respectively. As to item (2), we proceed by induction on the number of alternations of boxes and diamonds in χ. If $\chi =w$, $R_{\chi }=\mathrm{\Delta }$, so the statement follows trivially. For the inductive case, $\chi \ne x$, and then $\chi ={\phi }_1{\psi }_1\cdots {\phi }_n{\psi }_n(!x)$ such that $n\ge 1$, and the ${\phi }_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_{{\phi }_1}$, hence the statement follows from item (1). If n = 1 and ${\psi }_1(!z)$ is not empty, then, $R_{\chi }=R_{{\phi }_1}\star R_{{\psi }_1}\star \mathrm{\Delta }$, so: $\begin{array}{rl}& \left[\right[\chi \left[\mathbf{\text{j}}/x\right]\left]\right](\mathbf{\text{j}}:=\{a\left\}\right)\\ & =\left[\right[{\phi }_1(!y)\left]\right](y:=[\left[{\psi }_1\left[\mathbf{\text{j}}/z\right]\right]\left]\right(\mathbf{\text{j}}:=\left\{a\right\}\left)\right)\\ & =〈R_{{\phi }_1}〉\left[\right[{\psi }_1\left[\mathbf{\text{j}}/z\right]\left]\right](\mathbf{\text{j}}:=\{a\left\}\right)\mathrm{item}\left(1\right)\\ & =〈R_{{\phi }_1}〉\left[R_{{\psi }_1}\right]\left\{a\right\}\mathrm{item}\left(1\right)\\ & =〈R_{{\phi }_1}〉R_{{\psi }_1}^{\left[0\right]}\left[\right\{a{\}}^c]\text{Lemma 2.2}\\ & =\left(R_{{\phi }_1}^{\left[0\right]}\right[R_{{\psi }_1}^{\left[0\right]}\left[\right\{a{\}}^c\left]\right]{)}^c\text{Lemma 2.2}\\ & =\left(R_{{\phi }_1}^{\left[0\right]}\right[R_{{\psi }_1}^{\left[0\right]}\left[{\mathrm{\Delta }}^{\left[0\right]}\right[a\left]\right]\left]{)}^c{\mathrm{\Delta }}^{\left[0\right]}\right[a]=\{a{\}}^c\\ & =\left(\right(R_{{\phi }_1}\star R_{{\psi }_1}\star \mathrm{\Delta }{)}^{\left[0\right]}\left[a\right]{)}^c\text{Definition 5.1}\\ & =\left(R_{\chi }^{\left[0\right]}\right[a]{)}^c\chi ={\phi }_1{\psi }_1\\ & =〈R_{\chi }〉\left\{a\right\}\text{Lemma 2.2}\end{array}$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 $\begin{array}{r}\mathrm{\forall }\mathbf{\text{j}}\left(\mathsf{LA}\right(\psi \left)\right[\varphi [\mathbf{\text{j}}/!y]/!u]\le \chi [\mathsf{LA}\left(\alpha \right)[\mathbf{\text{j}}/!u]/p\left]\right).\end{array}$When interpreted on Kripke frames, the condition above translates as follows: (8) $\begin{array}{r}\mathrm{\forall a}\left(\right[\left[\mathsf{LA}\left(\psi \right)\left[\varphi \right[\mathbf{\text{j}}/!y]/!u]\right]\left]\right(\mathbf{\text{j}}:=\left\{a\right\})\subseteq [\left[\chi \left[\mathsf{LA}\right(\alpha \left)\right[\mathbf{\text{j}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{j}}:=\left\{a\right\}\left)\right).\end{array}$(8) Since $\mathsf{\text{LA}}\left(\psi \right)\left[\varphi \right(!y)/!u]$ and $\chi \left[\mathsf{\text{LA}}\right(\alpha \left)/p\right]$ are of the shape required by by items (i) and (ii) of Lemma 6.2 respectively, (8(8) $\begin{array}{r}\mathrm{\forall a}\left(\right[\left[\mathsf{LA}\left(\psi \right)\left[\varphi \right[\mathbf{\text{j}}/!y]/!u]\right]\left]\right(\mathbf{\text{j}}:=\left\{a\right\})\subseteq [\left[\chi \left[\mathsf{LA}\right(\alpha \left)\right[\mathbf{\text{j}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{j}}:=\left\{a\right\}\left)\right).\end{array}$(8) ) can be rewritten as follows (9) $\begin{array}{r}\mathrm{\forall a}\left(\right(R_{\mathsf{LA}\left(\psi \right)}\circ R_{\varphi }{)}^{-1}\left[a\right]\subseteq R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{-1)}\left[a\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{LA}\left(\psi \right)}\circ {\mathrm{R}}_{\varphi }\subseteq {\mathrm{R}}_{\chi \left[\mathsf{LA}\right(\alpha \left)/\mathrm{p}\right]}.\end{array}$(9) Similarly, the ALBA output of mrps of type (b) is $\begin{array}{r}\mathrm{\forall }\mathbf{\text{m}}\left(\zeta \right[\mathsf{RA}\left(\delta \right)[\mathbf{\text{m}}/!u]/p]\le \mathsf{RA}(\varphi \left)\right[\psi [\mathbf{\text{m}}/!y]/!u\left]\right),\end{array}$and, when interpreted on Kripke frames, the condition translates as follows: (10) $\begin{array}{r}\mathrm{\forall x}\left(\right[\left[\zeta \left[\mathsf{RA}\right(\delta \left)\right[\mathbf{\text{m}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{m}}:=\left\{x{\}}^c\right)\subseteq \left[\right[\mathsf{RA}\left(\varphi \right)\left[\psi \right[\mathbf{\text{m}}/!y]/!u]\left]\right](\mathbf{\text{m}}:=\{x{\}}^c\left)\right).\end{array}$(10) By items (3) and (1) of Lemmas 6.2 and 2.2, and contraposition, we can rewrite (10(10) $\begin{array}{r}\mathrm{\forall x}\left(\right[\left[\zeta \left[\mathsf{RA}\right(\delta \left)\right[\mathbf{\text{m}}/!u\left]/p\right]\right]\left]\right(\mathbf{\text{m}}:=\left\{x{\}}^c\right)\subseteq \left[\right[\mathsf{RA}\left(\varphi \right)\left[\psi \right[\mathbf{\text{m}}/!y]/!u]\left]\right](\mathbf{\text{m}}:=\{x{\}}^c\left)\right).\end{array}$(10) ) as follows: (11) $\begin{array}{r}\mathrm{\forall x}\left(\right(R_{\mathsf{RA}\left(\varphi \right)}\circ R_{\psi }{)}^{-1}\left[x\right]\subseteq R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{-1}\left[x\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{RA}\left(\varphi \right)}\circ {\mathrm{R}}_{\psi }\subseteq {\mathrm{R}}_{\zeta \left[\mathsf{RA}\right(\delta \left)/\mathrm{p}\right]}.\end{array}$(11) Finally, notice that, if the mrp is also analytic, the shape of $\chi \left(p\right)$ (resp. $\zeta \left(p\right)$) simplifies to $\chi \left(p\right)={\varphi }_{n_{\chi }}{\psi }_{n_{\chi }}\left(p\right)$ with $n_{\chi }=1$ and ${\psi }_{n_{\chi }}$ empty (resp. $\zeta \left(p\right)={\psi }_{n_{\zeta }}{\varphi }_{n_{\zeta }}\left(p\right)$ with $n_{\zeta }=1$ and ${\varphi }_{n_{\zeta }}$ empty). Hence, (9(9) $\begin{array}{r}\mathrm{\forall a}\left(\right(R_{\mathsf{LA}\left(\psi \right)}\circ R_{\varphi }{)}^{-1}\left[a\right]\subseteq R_{\chi \left[\mathsf{LA}\right(\alpha \left)/p\right]}^{-1)}\left[a\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{LA}\left(\psi \right)}\circ {\mathrm{R}}_{\varphi }\subseteq {\mathrm{R}}_{\chi \left[\mathsf{LA}\right(\alpha \left)/\mathrm{p}\right]}.\end{array}$(9) ) and (11(11) $\begin{array}{r}\mathrm{\forall x}\left(\right(R_{\mathsf{RA}\left(\varphi \right)}\circ R_{\psi }{)}^{-1}\left[x\right]\subseteq R_{\zeta \left[\mathsf{RA}\right(\delta \left)/p\right]}^{-1}\left[x\right])\mathrm{i}.\mathrm{e}.{\mathrm{R}}_{\mathsf{RA}\left(\varphi \right)}\circ {\mathrm{R}}_{\psi }\subseteq {\mathrm{R}}_{\zeta \left[\mathsf{RA}\right(\delta \left)/\mathrm{p}\right]}.\end{array}$(11) ) simplify to the following inclusions: (12) $\begin{array}{r}{R}_{\mathsf{LA}\left(\psi \right)}\circ R_{\varphi }\subseteq R_{{\varphi }_{n_{\chi }}}\circ R_{\mathsf{LA}\left(\alpha \right)}{R}_{\mathsf{RA}\left(\varphi \right)}\circ R_{\psi }\subseteq R_{{\psi }_{n_{\zeta }}}\circ R_{\mathsf{RA}\left(\delta \right)}.\end{array}$(12)

Example 6.3

The mrp $p\le \mathrm{◊◻p}$ is inductive of type (a), where $\varphi \left(y\right):=y$, and $\alpha \left(p\right):=p$, hence $\mathsf{\text{LA}}\left(\alpha \right)\left(u\right):=u$, and $\psi \left(x\right):=x$, hence $\mathsf{\text{LA}}\left(\psi \right)\left(v\right):=v$, and $\chi \left(p\right):=\mathrm{◊◻p}$. Then the ALBA output of this inequality is $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{j}}\left(\right[\left[\mathbf{\text{j}}/y\right]/v]\le \mathrm{◊◻}[\left[\mathbf{\text{j}}/u\right]/p\left]\right)\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}(\mathbf{\text{j}}\le \mathrm{◊◻}\mathbf{\text{j}})\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}\left(\right(\left[\mathrm{◊◻}\mathbf{\text{j}}\right])\subseteq (\left[\mathbf{\text{j}}\right]\left)\right)\left(\mathrm{Definition}\mathrm{of}\mathrm{order}\mathrm{on}\mathrm{polarities}\right)\\ \mathrm{iff}& \mathrm{\forall a}\left(R_{◊}^{\left[0\right]}\right[R_{◻}^{\left[0\right]}\left[a^c\right]]\subseteq a^c)\left(\mathrm{Standard}\mathrm{translation}\right)\\ \mathrm{iff}& \mathrm{\forall a}\left(R_{◊}^{\left[0\right]}\right[R_{◻}^{\left[0\right]}\left[{\mathrm{\Delta }}^{\left[0\right]}\right[a\left]\right]]\subseteq {\mathrm{\Delta }}^{\left[0\right]}[a\left]\right)(\mathrm{Definition}\mathrm{of}\mathrm{\Delta })\\ \mathrm{iff}& \mathrm{\forall a}\left(\right(R_{◊}\star R_{◻}\star \mathrm{\Delta }{)}^{\left[0\right]}\left[a\right]\subseteq {\mathrm{\Delta }}^{\left[0\right]}\left[a\right])\text{(Definition 5.1)}\\ \mathrm{iff}& \mathrm{\forall x}\mathrm{\forall a}\left(x\right(R_{◊}\star R_{◻}\star \mathrm{\Delta }{)}^{c}a\subseteq x{\mathrm{\Delta }}^c\left[a\right]\left)(\mathrm{Definition}\mathrm{of}\right(\cdot {)}^{\left[0\right]})\\ \mathrm{iff}& \mathrm{\Delta }\subseteq R_{◊}\star R_{◻}\star \mathrm{\Delta }\text{(Lemma 2.1)}\end{array}$

Example 6.4

The mrp $\mathrm{◻◊p}\le \mathrm{◻◊◊p}$ is inductive of shape (b) with $\varphi \left(y\right):=y$, hence $\mathsf{\text{RA}}\left(\varphi \right)\left(v\right):=v$ and $\psi \left(x\right):=\mathrm{◻x}$, and $\delta \left(p\right):=\mathrm{◊◊p}$, hence $\mathsf{\text{RA}}\left(\delta \right)\left(u\right):=\mathrm{◼◼u}$, and $\chi \left(p\right):=\mathrm{◻◊p}$. $\begin{array}{rl}& \mathrm{\forall p}[\mathrm{◻◊p}\le \mathrm{◻◊◊p}]\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{m}}[\mathrm{◻◊◼◼}\mathbf{\text{m}}\le ◻\mathbf{\text{m}}]\mathrm{ALBA}\mathrm{output}\\ \mathrm{i}.\mathrm{e}.& \mathrm{\forall x}\left(R_{◻}^{\left[0\right]}\right[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[{\mathrm{\Delta }}^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x^{\left[01\right]]}\left]\right]\left]\right]\subseteq R_{◻}^{\left[0\right]}\left[x^{\left[01\right]}\right])\\ \mathrm{iff}& \mathrm{\forall x}\left(R_{◻}^{\left[0\right]}\right[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[{\mathrm{\Delta }}^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x\left]\right]\left]\right]]\subseteq R_{◻}^{\left[0\right]}[x\left]\right)(R_{◻}\mathrm{and}{\mathrm{R}}_{◊}\mathrm{\Delta }-\mathrm{compatible})\\ \mathrm{iff}& \mathrm{\forall x}\mathrm{\forall a}(a\in R_{◻}^{\left[0\right]}[R_{◊}^{\left[0\right]}\left[R_{◼}^{\left[0\right]}\right[{\mathrm{\Delta }}^{\left[1\right]}\left[R_{◼}^{\left[0\right]}\right[x\left]\right]\left]\right]]\Rightarrow a\in R_{◻}^{\left[0\right]}[x\left]\right)\\ \mathrm{iff}& \mathrm{\forall x}\mathrm{\forall a}\left(a\right(R_{◻}\star R_{◊}\star (R_{◼}\circ R_{◼}){)}^{c}x\Rightarrow a{R}_{◻}^{c}x)\\ \mathrm{iff}& R_{◻}\subseteq R_{◻}\star R_{◊}\star (R_{◼}\circ R_{◼}).\end{array}$

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\left(p\right)\le t\left(p\right)$, 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 Conradie et al. (2021, Proposition 5) in the context of polarity-based frames and in Conradie et al. (2019b, Proposition 4) in the context of graph-based frames can be generalised (and made much more explicit in the process) to all inductive mrps.

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

Definition 6.3

The ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality ${\gamma }_1\subseteq {\gamma }_2$ is the shifting of the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality ${\xi }_1\subseteq {\xi }_2$ if, for any Kripke frame $\mathbb{X}$, $\begin{array}{r}{\xi }_1^{\mathbb{X}}={\gamma }_1^{{\mathbb{F}}_{\mathbb{X}}}\mathrm{and}{\xi }_2^{\mathbb{X}}={\gamma }_2^{{\mathbb{F}}_{\mathbb{X}}}.\end{array}$

Example 6.5

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

The ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$ is the shifting of the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality $R_{◻}\circ R_{◻}\subseteq R_{◻}$ (encoding the transitivity of $R_{◻}$) on Kripke frames. Indeed, by Lemma 5.1, $R_{◻}\circ R_{◻}\subseteq R_{◻}$ is the instantiation of $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$ when $E:=\mathrm{\Delta }$.

Proposition 6.2

Every ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality ${\gamma }_1\subseteq {\gamma }_2$ is the shifting of the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality $\tau \left({\gamma }_1\right)\subseteq \tau \left({\gamma }_2\right)$ (see Definition 5.3).

Proof.

Immediate by item 1 of Lemma 5.3.

Theorem 6.1

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

Proof.

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

Table

Type	${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequalities	${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities
(a)	$R_{\mathsf{\text{LA}}\left(\psi \right)}\circ R_{\varphi }\subseteq R_{\chi \left[\mathsf{\text{LA}}\right(\alpha \left)/p\right]}$	$R_{\mathsf{\text{LA}}\left(\psi \right)}{◊\text{}}}_E{R}_{\varphi }\subseteq R_{\chi \left[\mathsf{\text{LA}}\right(\alpha \left)/p\right]}$
(b)	$R_{\mathsf{\text{RA}}\left(\varphi \right)}\circ R_{\psi }\subseteq R_{\zeta \left[\mathsf{\text{RA}}\right(\delta \left)/p\right]}$	$R_{\mathsf{\text{RA}}\left(\varphi \right)}{◻\text{}}}_E{R}_{\psi }\subseteq R_{\zeta \left[\mathsf{\text{RA}}\right(\delta \left)/p\right]}$

where the notation $R_{\phi },R_{\psi },R_{\chi },R_{\zeta }$ refers to Definition 6.1 in the graph-based context, and Definition 6.2 in the Kripke one. Therefore, it is sufficient to prove that the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-terms associated to formulas in Definition 6.2 coincide with the translations of the terms associated with the same formulas in Definition 6.1. This follows straightforwardly by induction and by the definition of the translation (cf. Definition 5.3).

In what follows, we will sometimes refer to the shiftings of ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequalities corresponding to Sahlqvist mrps of type (a) (resp. (b)) as D-shiftings (resp. E-shiftings).

Example 6.6

The mrp $p\le \mathrm{◊◻p}$ is inductive of type (a), where $\varphi \left(y\right):=y$, and $\alpha \left(p\right):=p$, hence $\mathsf{\text{LA}}\left(\alpha \right)\left(u\right):=u$, and $\psi \left(x\right):=x$, hence $\mathsf{\text{LA}}\left(\psi \right)\left(v\right):=v$, and $\chi \left(p\right):=\mathrm{◊◻p}$, and, as discussed in Example 6.3, its first-order correspondent on classical Kripke frames can be represented as the following $\mathsf{\text{KRel}}$-inequality: $\mathrm{\Delta }\subseteq R_{◊}\star R_{◻}\star \mathrm{\Delta }$, while as discussed in Example 6.1, its first-order correspondent on graph-based frames can be represented as the following $\mathsf{\text{GRel}}$-inequality: $D\subseteq R_{◊}\ast R_{◻}\ast D$. Since $\tau \left(D\right)=\mathrm{\Delta }$ and $\tau (R_{◊}\ast R_{◻}\ast D)=R_{◊}\star R_{◻}\star \mathrm{\Delta }$, By Proposition 6.2, $D\subseteq R_{◊}\ast R_{◻}\ast D$ is a shifting (particularly D-shifting) of $\mathrm{\Delta }\subseteq R_{◊}\star R_{◻}\star \mathrm{\Delta }$.

We conclude the present subsection with the following example in which all the steps from the ALBA output and the generation of the inequalities are presented.

Example 6.7

The mrp $\mathrm{◊p}\le \mathrm{◻◊◻p}$ is inductive of type (a), where $\varphi \left(y\right):=\mathrm{◊y}$, and $\alpha \left(p\right):=p$, hence $\mathsf{\text{LA}}\left(\alpha \right)\left(u\right):=u$, and $\psi \left(x\right):=\mathrm{◻x}$, hence $\mathsf{\text{LA}}\left(\psi \right)\left(v\right):=\mathrm{⧫v}$, and $\chi \left(p\right):=\mathrm{◊◻p}$. Let us compute the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality representing the first order correspondent of this mrp on graph-based frames: $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{j}}\left(⧫\right[◊\left[\mathbf{\text{j}}/y\right]/v]\le \mathrm{◊◻}[\left[\mathbf{\text{j}}/u\right]/p\left]\right)\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}(\mathrm{⧫◊}\mathbf{\text{j}}\le \mathrm{◊◻}\mathbf{\text{j}})\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}\left(\right(\left[\mathrm{◊◻}\mathbf{\text{j}}\right])\subseteq (\left[\mathrm{⧫◊}\mathbf{\text{j}}\right]\left)\right)\text{(Definition of order on polarities)}\\ \mathrm{iff}& \mathrm{\forall a}\left(R_{◊}^{\left[0\right]}\right[R_{◻}^{\left[0\right]}\left[E^{\left[1\right]}\right[a\left]\right]]\subseteq R_{⧫}^{\left[0\right]}[E^{\left[1\right]}\left[R_{◊}^{\left[0\right]}\right[a\left]\right]\left]\right)\left(\mathrm{Standard}\mathrm{translation}\right)\\ \mathrm{iff}& \mathrm{\forall a}\left(\right(R_{◊}\ast R_{◻}\ast D{)}^{\left[0\right]}\left[a\right]\subseteq \left(R_{⧫}{◊\text{}}}_E{R}_{◊}{)}^{\left[0\right]}\right[a\left]\right)\text{(Definition 5.1)}\\ \mathrm{iff}& R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}\ast R_{◻}\ast D.\text{(Lemma 2.1)}\end{array}$Let us now compute the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality equivalent to the first order correspondent of the mrp on Kripke frames: $\begin{array}{rl}& \mathrm{\forall }\mathbf{\text{j}}\left(⧫\right[◊\left[\mathbf{\text{j}}/y\right]/v]\le \mathrm{◊◻}[\left[\mathbf{\text{j}}/u\right]/p\left]\right)\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}(\mathrm{⧫◊}\mathbf{\text{j}}\le \mathrm{◊◻}\mathbf{\text{j}})\\ \mathrm{iff}& \mathrm{\forall }\mathbf{\text{j}}\left(\right(\left[\mathrm{◊◻}\mathbf{\text{j}}\right])\subseteq (\left[\mathrm{⧫◊}\mathbf{\text{j}}\right]\left)\right)\text{(Definition of order on polarities)}\\ \mathrm{iff}& \mathrm{\forall a}\left(R_{◊}^{\left[0\right]}\right[R_{◻}^{\left[0\right]}\left[{\mathrm{\Delta }}^{\left[0\right]}\right[a\left]\right]]\subseteq R_{⧫}^{\left[0\right]}[{\mathrm{\Delta }}^{\left[1\right]}\left[R_{◊}^{\left[0\right]}\right[a\left]\right]\left]\right)\left(\mathrm{Standard}\mathrm{translation}\right)\\ \mathrm{iff}& \mathrm{\forall a}\left(\right(R_{◊}\star R_{◻}\star \mathrm{\Delta }{)}^{\left[0\right]}\left[a\right]\subseteq (R_{⧫}\circ R_{◊}{)}^{\left[0\right]}[a\left]\right)\text{(Definition 5.1)}\\ \mathrm{iff}& R_{⧫}\circ R_{◊}\subseteq R_{◊}\star R_{◻}\star \mathrm{\Delta }.\text{(Lemma 2.1)}\end{array}$The $\mathsf{\text{GRel}}$-inequality $R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}\ast R_{◻}\ast D$ is the translation (and D-shifting) of $R_{⧫}\circ R_{◊}\subseteq R_{◊}\star R_{◻}\star \mathrm{\Delta }$.

6.4. Lifting graph-based frames to polarity-based frames

Having established a systematic connection between the first-order correspondents of inductive mrps on Kripke frames and on graph-based frames in the previous subsection, in the present subsection we establish analogous results along the following lifting construction of graph-based frames to polarity-based frames.

Definition 6.4

Lifting of graph-based frames

For any reflexive graph $\mathbb{G}=(Z,E)$ and any graph-based frame $\mathbb{F}=(\mathbb{G},R_{◊},R_{◻})$, let the lifting of $\mathbb{F}$ be the polarity-based frame ${\mathbb{P}}_{\mathbb{F}}:=({\mathbb{P}}_{\mathbb{G}},J_{R_{◊}^c},I_{R_{◻}^c})$, where ${\mathbb{P}}_{\mathbb{G}}:=(Z_A,Z_X,I_{E^c})$, $J_{R_{◊}^c}$, and $I_{R_{◻}^c}$ are defined as in Section 2.4.

Lemma 6.3

For any reflexive graph $\mathbb{G}=(Z,E)$ and any E-compatible relation R, the lifted relations $I_{R^c}$ and $J_{R^c}$ are $I_{E^c}$-compatible.

Proof.

We show just one of the two properties of $I_{E^c}$-compatibility, as the other is proved similarly. $\begin{array}{rl}& I_{E^c}^{\left(0\right)}\left[I_{E^c}^{\left(1\right)}\right[\left(I_{R^c}^{\left(0\right)}\right[x\left]\right)\left]\right]\\ & =I_E^{\left[0\right]}\left[I_E^{\left[1\right]}\right[\left(I_R^{\left[0\right]}\right[x\left]\right)\left]\right]\text{Definition of}(\cdot {)}^{\left[0\right]}\mathrm{and}(\cdot {)}^{\left[1\right]}\\ & =\left(E^{\left[0\right]}\right[E^{\left[1\right]}\left[\right(R^{\left[0\right]}\left[x\right]\left)\right]]{)}_A\text{Definition of}{I}_E\mathrm{and}{\mathrm{I}}_{\mathrm{R}}\\ & =\left(\right(R^{\left[0\right]}\left[x\right]{)}^{\left[10\right]}{)}_A\mathrm{notational}\mathrm{convention}\\ & \subseteq \left(R^{\left[0\right]}\right[x]{)}_{A}E-\mathrm{compatibility}\mathrm{of}\mathrm{R}\\ & ={I_R}^{\left[0\right]}\left[x\right]\text{Definition of}{I}_R\\ & ={I_{R^c}}^{\left(0\right)}\left[x\right]\text{Definition of}(\cdot {)}^{\left[0\right]}\end{array}$

By the lemma above, ${\mathbb{P}}_{\mathbb{F}}$ is a well defined polarity-based frame, and, by definition, the complex algebras ${{\mathbb{F}}_{\mathbb{P}}}^{+}$ and ${\mathbb{F}}^{+}$ coincide. Notice that the lifting of Kripke frames to polarity-based frames defined in Conradie et al. (2022, Definition 4.17) is the composition of the shifting defined in Section 6.3 and the lifting defined above. In Conradie et al. (2022, Section 4.1), the relational language ${\mathsf{\text{PRel}}}_{\mathcal{L}}$ (see Conradie et al. (2022, Definition 3.20)) has been introduced, which contains terms of types ${\mathsf{\text{T}}}_{A\times X}$, ${\mathsf{\text{T}}}_{X\times A}$, ${\mathsf{\text{T}}}_{A\times A}$ and ${\mathsf{\text{T}}}_{X\times X}$, and is defined by the following simultaneous recursions: $\begin{array}{r}\begin{array}{ll}{\mathsf{T}}_{A\times X}\ni \text{β}::=I|R_{◻}|\text{β}{;}_I\text{β}|\rho ;\text{β}|\text{β};\lambda & {\mathsf{T}}_{A\times A}\ni \rho ::=\delta ;\text{β}\\ {\mathsf{T}}_{X\times A}\ni \delta ::=J|R_{◊}|\delta {;}_I\delta |\lambda ;\delta |\delta ;\rho & {\mathsf{T}}_{X\times X}\ni \lambda ::=\text{β};\delta ,\end{array}\end{array}$where $I,J,R_{◊},$ and $R_{◻}$ are naturally interpreted as the $I,J,R_{◊},$ and $R_{◻}$ of a polarity-based frame, while ; and ${;}_I$ are interpreted as the composition operations in Conradie et al. (2022, Definition 3.2). Moreover, relational ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-terms $R_{\phi },R_{\psi },R_{\chi },R_{\zeta }$ are associated with formulas $\phi ,\psi ,\chi ,\zeta$ as in Definition 6.1.

In Conradie et al. (2022, Section 4.1), the first-order correspondents of inductive mrps on polarity-based frames are shown to be representable as term inequalities in ${\mathsf{\text{PRel}}}_{\mathcal{L}}$ as indicated below: $\begin{array}{r}\begin{array}{l}\mathrm{type}\left(\mathrm{a}\right){\mathrm{R}}_{\chi \left[\mathsf{LA}\right(\alpha \left)/\mathrm{p}\right]}\subseteq {\mathrm{R}}_{\mathsf{LA}\left(\psi \right)}{;}_{\mathrm{I}}{\mathrm{R}}_{\varphi }\mathrm{of}\mathrm{type}{\mathsf{T}}_{\mathsf{X}\times \mathsf{A}},\\ \mathrm{type}\left(\mathrm{b}\right){\mathrm{R}}_{\zeta \left[\mathsf{RA}\right(\delta \left)/\mathrm{p}\right]}\subseteq {\mathrm{R}}_{\mathsf{RA}\left(\varphi \right)}{;}_{\mathrm{I}}{\mathrm{R}}_{\psi }\mathrm{of}\mathrm{type}{\mathsf{T}}_{\mathsf{A}\times \mathsf{X}}.\end{array}\end{array}$The following definition extends the definition of lifting in Conradie et al. (2022, Definition 4.17) to graph-based frames.

Definition 6.5

Let ${\xi }_1\subseteq {\xi }_2$ be a ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality, and ${\text{β}}_1\subseteq {\text{β}}_2$ (resp. ${\delta }_1\subseteq {\delta }_2$) be a ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequality of type ${\mathsf{\text{T}}}_{A\times X}$ (resp. ${\mathsf{\text{T}}}_{X\times A}$).

1. The inequality ${\text{β}}_1\subseteq {\text{β}}_2$ is the I-lifting of ${\xi }_1\subseteq {\xi }_2$ if for any graph-based frame $\mathbb{F}$, ${\text{β}}_1^{{\mathbb{P}}_{\mathbb{F}}}=I_{({\xi }_2^{\mathbb{F}}{)}^c}$ and ${\text{β}}_2^{{\mathbb{P}}_{\mathbb{F}}}=I_{({\xi }_1^{\mathbb{F}}{)}^c}$.

2. The inequality ${\delta }_1\subseteq {\delta }_2$ is the J-lifting of ${\xi }_1\subseteq {\xi }_2$ if for any graph-based frame $\mathbb{F}$, ${\delta }_1^{{\mathbb{P}}_{\mathbb{F}}}=J_{({\xi }_2^{\mathbb{F}}{)}^c}$ and ${\delta }_2^{{\mathbb{P}}_{\mathbb{F}}}=J_{({\xi }_1^{\mathbb{F}}{)}^c}$.

The following theorem extends (Conradie et al., 2022, Theorem 4.20) to graph-based frames.

Theorem 6.2

For any inductive modal reduction principle $s\left(p\right)\le t\left(p\right)$ of $\mathcal{L}$,

(1)	if $s\left(p\right)\le t\left(p\right)$ is of type (a), then the ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequality of type ${\mathsf{\text{T}}}_{X\times A}$ encoding its first-order correspondent on polarity-based frames is the J-lifting of the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality encoding its first-order correspondent on graph-based frames;
(2)	if $s\left(p\right)\le t\left(p\right)$ is of type (b), then the ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequality of type ${\mathsf{\text{T}}}_{A\times X}$ encoding its first-order correspondent on polarity-based frames is the I-lifting of the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality encoding its first-order correspondent on graph-based frames.

Proof.

Analogous to that of Conradie et al. (2022, Theorem 4.20).

Example 6.8

The ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequality $R_{◻}\subseteq I$ is the I-lifting of the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality $E\subseteq R_{◻}$. Indeed, $\mathbb{F}\models E\subseteq R_{◻}$ iff $I_{R_{◻}^c}\subseteq I_{E^c}$ iff ${\mathbb{P}}_{\mathbb{F}}\models R_{◻}\subseteq I$ for every graph-based frame $\mathbb{F}$. These inequalities encode first-order conditions corresponding to the inductive mrp $\mathrm{◻p}\le p$ on polarity-based frames and on graph-based frames, respectively.

Similarly, the ${\mathsf{\text{PRel}}}_{\mathcal{L}}$-inequality $R_{◻}\subseteq R_{◻}{;}_I{R}_{◻}$ is the I-lifting of $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$, Indeed, $\mathbb{F}\models R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$ iff $I_{R_{◻}^c}\subseteq I_{(R_{◻}{◻\text{}}}_E{R}_{◻}{)}^c}$ iff $I_{R_{◻}^c}\subseteq I_{R_{◻}^c}{;}_I{I}_{R_{◻}^c}$ iff ${\mathbb{P}}_{\mathbb{F}}\models R_{◻}\subseteq R_{◻}{;}_I{R}_{◻}$ for every graph-based frame $\mathbb{F}$. The second equivalence hinges on the identity $I_{(S{◻\text{}}}_{E}T{)}^c}=I_{S^c}{;}_I{I}_{T^c}$ for all $S,T\subseteq Z\times Z$, which is proved similarly to Conradie et al. (2022, Lemma 3.12). These inequalities encode first-order conditions corresponding to the inductive mrp $\mathrm{◻p}\le \mathrm{◻◻p}$.

7. Applications to rough set theory

In the present section, we take stock of the technical results presented in the previous sections by further elucidating the relationship between hyperconstructive approximation spaces (cf. Definition 4.1) and generalised approximation spaces (seen as Kripke frames with $R_{◊}=R_{◻}$, cf. Definition 2.1). Firstly, as is expected, the definition of hyperconstructivist approximation spaces collapses to that of generalised approximation spaces when instantiating $E:=\mathrm{\Delta }$ (cf. Proposition 2.5). Thus, generalised approximation spaces form the proper subclass of hyperconstructivist approximation spaces capturing the limit case in which there is no inherent entropy and $R_{◻}=R_{◼}=R$. On this subclass, all ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities collapse to ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequalities, since the relational compositions on graph-based frames (cf. Definition 5.1) reduce to the relational compositions on Kripke frames (cf. Lemma 5.3). Hence, in particular, and as is expected, the correspondents of Sahlqvist mrps on graph-based frames, represented as discussed in Section 6.1, collapse, in the sense specified in Lemma 5.3, to the correspondents of the same mrps on Kripke frames, represented as discussed in Section 6.2.

More interesting is the relationship in the converse direction, which hinges on the notion of shifting (cf. Definition 6.3): every Sahlqvist mrp $s\left(p\right)\le t\left(p\right)$ (cf. Section 2.5) defines an elementary (i.e. first-order definable) class $\mathbf{\text{K}}\left(s\right(p)\le t(p\left)\right)$ of Kripke frames and an elementary class $\mathbf{\text{G}}\left(s\right(p)\le t(p\left)\right)$ of graph-based frames. By Theorem 6.1, when represented as a ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequality, the first-order condition defining $\mathbf{\text{G}}\left(s\right(p)\le t(p\left)\right)$ is the shifting of the first-order condition defining $\mathbf{\text{K}}\left(s\right(p)\le t(p\left)\right)$, represented as a ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality. The notion of shifting allows for a systematic relationship to be established between $\mathbf{\text{K}}\left(s\right(p)\le t(p\left)\right)$ and $\mathbf{\text{G}}\left(s\right(p)\le t(p\left)\right)$ which is formulated in terms of their own first-order languages, and hence independently from their correspondence-theoretic link, in the sense that this relationship can be established purely on the basis of the syntax of $\mathbf{\text{K}}\left(s\right(p)\le t(p\left)\right)$ and $\mathbf{\text{G}}\left(s\right(p)\le t(p\left)\right)$. A similarly systematic relationship between the two correspondents of any Sahlqvist mrps on graph-based frames and on polarity-based frames, respectively, is established in Theorem 6.2 by hinging on the notion of lifting (cf. Definition 6.5). This relationship is again independent from the correspondence-theoretic link of the two first-order conditions.

It is easy to check that the well known modal axioms listed in Table 3 are all Sahlqvist mrps, and hence Theorems 6.1 and 6.2 apply to these axioms. Table 3 also reports the relational correspondents of these mrps on Kripke frames, graph-based frames, and polarity-based frames. It is easy to verify that, for each mrp in the table (they are all analytic inductive, and hence of both types (a) and (b)), its relational correspondent on graph-based frames when considering it as type (a) (resp. (b)) is the D-shifting (resp. E-shifting) of its relational correspondent on Kripke frames, and its relational correspondent on polarity-based frames when considering it as type (a) (resp. (b)) is the J-lifting (resp. I-lifting) of its relational correspondent on graph-based frames.

Table 3. Well-known modal reduction principles and their correspondents as relational inequalities.

Property	Axiom	${\mathsf{\text{KRel}}}_{\mathcal{L}}$ correspondent	${\mathsf{\text{GRel}}}_{\mathcal{L}}$ correspondent	${\mathsf{\text{PRel}}}_{\mathcal{L}}$ correspondent
Reflexivity	$p\le \mathrm{◊p}$	$\mathrm{\Delta }\subseteq R_{◊}$	$D\subseteq R_{◊}$	$R_{◊}\subseteq J$
		$\mathrm{\Delta }\subseteq R_{◼}$	$E\subseteq R_{◼}$	$R_{◼}\subseteq I$
	$\mathrm{◻p}\le p$	$\mathrm{\Delta }\subseteq R_{⧫}$	$D\subseteq R_{⧫}$	$R_{⧫}\subseteq J$
		$\mathrm{\Delta }\subseteq R_{◻}$	$E\subseteq R_{◻}$	$R_{◻}\subseteq I$
Transitivity	$\mathrm{◊◊p}\le \mathrm{◊p}$	$R_{◊}\circ R_{◊}\subseteq R_{◊}$	$R_{◊}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}$	$R_{◊}\subseteq R_{◊}{;}_I{R}_{◊}$
		$R_{◼}\circ R_{◼}\subseteq R_{◼}$	$R_{◼}{◻\text{}}}_E{R}_{◼}\subseteq R_{◼}$	$R_{◼}\subseteq R_{◼}{;}_I{R}_{◼}$
	$\mathrm{◻p}\le \mathrm{◻◻p}$	$R_{⧫}\circ R_{⧫}\subseteq R_{⧫}$	$R_{⧫}{◊\text{}}}_E{R}_{⧫}\subseteq R_{⧫}$	$R_{⧫}\subseteq R_{⧫}{;}_I{R}_{⧫}$
		$R_{◻}\circ R_{◻}\subseteq R_{◻}$	$R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$	$R_{◻}\subseteq R_{◻}{;}_I{R}_{◻}$
Symmetry	$p\le \mathrm{◻◊p}$	$R_{⧫}\subseteq R_{◊}$	$R_{⧫}\subseteq R_{◊}$	$R_{◊}\subseteq R_{⧫}$
		$R_{◻}\subseteq R_{◼}$	$R_{◻}\subseteq R_{◼}$	$R_{◼}\subseteq R_{◻}$
	$\mathrm{◊◻p}\le p$	$R_{◊}\subseteq R_{⧫}$	$R_{◊}\subseteq R_{⧫}$	$R_{⧫}\subseteq R_{◊}$
		$R_{◼}\subseteq R_{◻}$	$R_{◼}\subseteq R_{◻}$	$R_{◻}\subseteq R_{◼}$
Seriality	$\mathrm{◻p}\le \mathrm{◊p}$	$\mathrm{\Delta }\subseteq R_{◊}\circ R_{⧫}$	$D\subseteq R_{◊}{◊\text{}}}_E{R}_{⧫}$	$R_{◊}{;}_I{R}_{⧫}\subseteq J$
		$\mathrm{\Delta }\subseteq R_{◻}\circ R_{◼}$	$E\subseteq R_{◻}{◻\text{}}}_E{R}_{◼}$	$R_{◻}{;}_I{R}_{◼}\subseteq I$
Partial functionality	$\mathrm{◊p}\le \mathrm{◻p}$	$R_{⧫}\circ R_{◊}\subseteq \mathrm{\Delta }$	$R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq D$	$J\subseteq R_{⧫}{;}_I{R}_{◊}$
		$R_{◼}\circ R_{◻}\subseteq \mathrm{\Delta }$	$R_{◼}{◻\text{}}}_E{R}_{◻}\subseteq E$	$I\subseteq R_{◼}{;}_I{R}_{◻}$
Euclideanness	$\mathrm{◊p}\le \mathrm{◻◊p}$	$R_{⧫}\circ R_{◊}\subseteq R_{◊}$	$R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}$	$R_{◊}\subseteq R_{⧫}{;}_I{R}_{◊}$
		$R_{◼}\circ R_{◻}\subseteq R_{◼}$	$R_{◼}{◻\text{}}}_E{R}_{◻}\subseteq R_{◼}$	$R_{◼}\subseteq R_{◼}{;}_I{R}_{◻}$
	$\mathrm{◊◻p}\le \mathrm{◻p}$	$R_{⧫}\circ R_{◊}\subseteq R_{⧫}$	$R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq R_{⧫}$	$R_{⧫}\subseteq R_{⧫}{;}_I{R}_{◊}$
		$R_{◼}\circ R_{◻}\subseteq R_{◻}$	$R_{◼}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$	$R_{◻}\subseteq R_{◼}{;}_I{R}_{◻}$
Confluence	$\mathrm{◊◻p}\le \mathrm{◻◊p}$	$R_{⧫}\circ R_{◊}\subseteq R_{◊}\circ R_{⧫}$	$R_{⧫}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}{◊\text{}}}_E{R}_{⧫}$	$R_{◊}{;}_I{R}_{⧫}\subseteq R_{⧫}{;}_I{R}_{◊}$
		$R_{◼}\circ R_{◻}\subseteq R_{◻}\circ R_{◼}$	$R_{◼}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}{◻\text{}}}_E{R}_{◼}$	$R_{◻}{;}_I{R}_{◼}\subseteq R_{◼}{;}_I{R}_{◻}$
Denseness	$\mathrm{◊p}\le \mathrm{◊◊p}$	$R_{◊}\subseteq R_{◊}\circ R_{◊}$	$R_{◊}\subseteq R_{◊}{◊\text{}}}_E{R}_{◊}$	$R_{◊}{;}_I{R}_{◊}\subseteq R_{◊}$
		$R_{◼}\subseteq R_{◼}\circ R_{◼}$	$R_{◼}\subseteq R_{◼}{◻\text{}}}_E{R}_{◼}$	$R_{◼}{;}_I{R}_{◼}\subseteq R_{◼}$
	$\mathrm{◻◻p}\le \mathrm{◻p}$	$R_{⧫}\subseteq R_{⧫}\circ R_{⧫}$	$R_{⧫}\subseteq R_{⧫}{◊\text{}}}_E{R}_{⧫}$	$R_{⧫}{;}_I{R}_{⧫}\subseteq R_{⧫}$
		$R_{◻}\subseteq R_{◻}\circ R_{◻}$	$R_{◻}\subseteq R_{◻}{◻\text{}}}_E{R}_{◻}$	$R_{◻}{;}_I{R}_{◻}\subseteq R_{◻}$

The mathematically grounded relationships just discussed reflect also on the ‘preservation’ of the intuitive meaning of Sahlqvist mrps across these different semantics, as we argue in the following examples.

Example 7.1

The Sahlqvist mrps $p\le \mathrm{◊p}$ and $\mathrm{◻p}\le p$ correspond to the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality $\mathrm{\Delta }\subseteq R$ on generalised approximation spaces. When interpreting the accessibility relation R as epistemic indiscernibility (e.g. that of an agent), the informal interpretation of $\mathrm{\Delta }\subseteq R$ is that if the agent can tell two states apart, then these states are distinct, and since in generalised approximation spaces two states are inherently indistinguishable iff they are identical, then this condition is equivalent to the condition that, if the agent can tell two states apart, then these states must not be inherently indistinguishable, which is by and large what the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities $E\subseteq R_{◻}$, and $D\subseteq R_{◊}$ (i.e. the correspondents of the same mrps on graph-based frames) express, except for a subtle refinement. Namely, the information encoded in E about any state z of a graph-based frame presents itself from two perspectives: the set $E^{\left[1\right]}\left[z\right]$ of the states which are discernible from z, and the set $E^{\left[0\right]}\left[z\right]$ of the states from which z is discernible. Since E is not symmetric, these two perspectives are not equivalent in general, and become equivalent when E is symmetric. In general, inequality $E\subseteq R_{◻}$ encodes the condition that, for any two states x and y, if x is inherently indiscernible from y, then x is indistinguishable from y according to the agent. Inequality $D\subseteq R_{◊}$ says that if x is inherently indiscernible from y, then y is indistinguishable from x also according to the agent.

Example 7.2

The Sahlqvist mrps $p\le \mathrm{◻◊p}$ and $\mathrm{◊◻p}\le p$ correspond to the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequalities $R^{-1}\subseteq R$ and $R\subseteq R^{-1}$ on Kripke frames. Under the same interpretation of the accessibility relation as in the example above, this condition encodes the symmetry of the indiscernibility relation. The same mrps correspond to the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities $R_{⧫}\subseteq R_{◊}$ and $R_{◻}\subseteq R_{◼}$ on graph-based frames, which express the symmetry of the indiscernibility relations. Hence, the meaning of these conditions across the two semantics is both formally and intuitively verbatim the same.

Example 7.3

The Sahlqvist mrps $\mathrm{◊◊p}\le \mathrm{◊p}$ and $\mathrm{◻p}\le \mathrm{◻◻p}$ correspond to the ${\mathsf{\text{KRel}}}_{\mathcal{L}}$-inequality $R\circ R\subseteq R$ on generalised approximation spaces. When interpreting the accessibility relation R as epistemic indiscernibility (e.g. that of an agent), the informal interpretation of $R\circ R\subseteq R$ is that for any two states x and y, if the agent can distinguish y from x, then the agent can distinguish y from every element in $R^{-1}\left[x\right]$, which is the set of all states which the agent cannot tell apart from x.

The same mrps correspond to the ${\mathsf{\text{GRel}}}_{\mathcal{L}}$-inequalities $R_{◊}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}$, and $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$ on graph-based frames. Unravelling $R_{◊}{◊\text{}}}_E{R}_{◊}\subseteq R_{◊}$, we get that $R_{◊}^{\left[0\right]}\left[x\right]\subseteq R_{◊}^{\left[0\right]}\left[E^{\left[0\right]}\right[R_{◊}^{\left[0\right]}\left[x\right]\left]\right]$ for every x. That is, if the agent can distinguish y from x, then the agent can distinguish y from any element of $E^{\left[0\right]}\left[R_{◊}^{\left[0\right]}\right[x\left]\right]$, which is the set of all states which can be (inherently) distinguished from every state which the agent can distinguish from x, that is, the set of all the states that the informational entropy allows to distinguish from all the states which the agent can distinguish from x. Hence, $E^{\left[0\right]}\left[R_{◊}^{\left[0\right]}\right[x\left]\right]$ is ‘as close as it gets’, in a scenario characterised by informational entropy, to the set of states that the agent cannot distinguish from x in a scenario with no informational entropy. Similar considerations, from the other perspective, apply to the meaning of $R_{◻}{◻\text{}}}_E{R}_{◻}\subseteq R_{◻}$.

The above examples show that transferring the modal axioms defining approximation spaces to the hyperconstructive (graph-based) setting preserves their intuitive meaning. In some cases, axioms which have the same first-order correspondent on approximation spaces correspond to non-equivalent first-order conditions on graph-based frames, which hints at the comparatively greater richness of the hyperconstructivist setting.

We can now refer to classes of hyperconstructivist approximation spaces defined by Sahlqvist mrps using the same name we use for the classes of generalised approximation spaces of which they are the shiftings. For example, reflexive graph-based frames are defined as graph-based frames satisfying the reflexivity axioms $D\subseteq R_{◊}$ and $E\subseteq R_{◻}$, while the class of symmetric graph-based frames are defined as graph-based frames satisfying the symmetry axioms $R_{◻}\subseteq R_{◼}$ and $R_{⧫}\subseteq R_{◊}$. As discussed in Section 4, this motivates us to define different sub-classes of hyperconstructivist approximation spaces like reflexive, symmetric, transitive and Pawlak approximation spaces (cf.  Definition 4.1) as analogues of these classes of frames in classical approximation spaces to the graph-based frames. The following propositions follows immediately from the general results discussed in the previous section.

Proposition 7.1

For any Pawlak's hyperconstructivist approximation space $\mathbb{F}=(Z,E,R_{◊},R_{◻})$, and any $a,b\in {\mathbb{F}}^{+}$, $\begin{array}{r}\begin{array}{lll}1.◊(a\vee b)=\mathrm{◊a}\vee \mathrm{◊b}& 2.◻(a\wedge b)=\mathrm{◻a}\wedge \mathrm{◻b}& 3.a\le \mathrm{◻b}\Rightarrow \mathrm{◊a}\le b\\ 4.\mathrm{◊a}\le b\Rightarrow a\le \mathrm{◻b}& 5.\mathrm{◻a}\le a& 6.a\le \mathrm{◊a}\\ 7.a\le \mathrm{◻◊a}& 8.\mathrm{◊◻a}\le a& 9.\mathrm{◊◊a}\le \mathrm{◊a}\\ 10.\mathrm{◻a}\le \mathrm{◻◻a}.\end{array}\end{array}$

All the conditions of the proposition above are satisfied by the lower and upper approximation operators of Pawlak's approximation spaces.

Different axiomatic classes of approximation spaces are used in rough set theory as models of approximate reasoning in different situations. The systematic relationship established in the present paper among generalised, hyperconstructivist, and conceptual approximation spaces makes it possible to capture a wider range of situations and reasoning modes while still taking advantage of the basic intuitions developed about the original setting.

On the algebraic side, the present results pave the way to systematically extending rough set theory to algebras based on general (i.e. not necessarily distributive) lattices. Different classes of general lattices with approximation operators can be defined which as lattice-based counterparts of classes of Boolean algebras with operators. Algebraic models of rough set theory based on various classes of lattices such as Boolean algebras, completely distributive lattices, ortholattices, De Morgan lattices (cf. Section 2.3) can then be encompassed and studied uniformly as subclasses of lattice-based ‘rough algebras’, which will then serve as a suitable common ground for comparing and transferring insights and results concerning formal frameworks of rough set theory defined on (or dual to) different classes of lattices.

8. Conclusions

The present paper provides a systematic theory to explain and generalise some observations about similarities in the shape of first-order correspondents of the common rough set theory axioms like reflexivity, symmetry and transitivity in Kripke and graph-based frames. The precise nature of these similarities is made explicit via the notion of shifting. This notion makes it possible to define the shifted counterparts of first-order conditions which are well known and widely used in modal logic and rough set theory; thus, we are now in a position to provide counterparts of rough theory axioms and different classes of approximation spaces in graph-based frames.

Parametric correspondence. Together with (Conradie et al., 2022), Theorems 6.1 and 6.2 suggest that the various correspondence theories for different logics and semantic contexts can be not only methodologically unified by the same algebraic and algorithmic mechanisms; they can also be parametrically related to each other in terms of their outputs. Furthermore, this parametric relation hinges on the natural connections between different semantic settings. In the present case, Kripke frames can be naturally embedded into graph-based frames, and graph-based frames into polarity-based frames. The present contribution can be understood as a preservation result of the first-order correspondents of inductive mrps under these natural embeddings, as shown in Figure 2.

Figure 2. A commutative diagram of semantic contexts.

Notation. A crucial step in achieving these results is the ability to express the first-order correspondents of modal axioms in various semantic contexts in a more algebraic language, specifically in the languages of (heterogeneous) relation algebras. As we illustrated with the example of the modal transitivity axiom, the mathematical and meaning-based connections are near impossible to detect when the correspondents are expressed in the standard first-order frame correspondence languages of Kripke, polarity and graph based frames, respectively, yet become transparently clear when written in a suitable relational algebraic language as inclusions of relational compositions. The use of these languages to express correspondents is essential in the formulations and proofs of the general results given in Theorems 6.1 and 6.2.

Future work. The present work can be further pursued in several directions. Firstly, the perfect modularity of the graph-based setting allows to systematically study natural subclasses of hyperconstructivist approximation spaces. One example of such a class would be the hyperconstructivist counterparts of tolerance spaces (Skowron & Stepaniuk, 1996), obtained by assuming the symmetry of the indiscernibility relation. Secondly, similar shifting/lifting results may be sought for other logics, including polyadic modal logics and many-valued modal logics (i.e. a similar correspondence may be shown between many-valued Kripke frames and many-valued graph-based frames). For instance, a natural extension of the present work concerns investigating the remaining connections between the semantics presently investigated and their many-valued versions, as represented by the three un-annotated edges in Figure 2. Thirdly, the class of formulas covered by the shifting/lifting could possibly be expanded to more than inductive modal reduction principles. However, we do not expect this to be possible for all formulas with first-order frame correspondents, not even for all inductive formulas. Indeed, there exist inductive formulas whose corespondents over polarity-based frames are not liftings of their correspondents over Kripke frames (see the concluding section of Conradie et al., 2022), and we expect similar examples to exist in the case of shiftings to graph-based frames. Fourthly, the literature contains instances of correspondence theory for modal logics on non-classical base obtained via Gödel-McKinsey-Tarski (GMT) translation (Gödel, 1933; McKinsey & Tarski, 1948) to the multi-modal classical context (see e.g. Gehrke et al., 2005 for an instance in the context of distributive modal logic and Conradie et al., 2019 for one in the context of bi-intuitionistic modal logic). In the context of graph-based frames, a similar approach suggests itself, whereby one would translate formulas over graph-based frames into formulas over Kripke frames, prefixing propositional variables with modalities interpreted with the relation E to simulate the closure of valuations. However, this approach involves several challenges, especially on the proof-theoretic front, not least of which is the fact that conditions such as the E-compatibility of the additional relations can not be represented by (analytic) inductive inequalities, and thus, the general methods for developing analytic display calculi for modal logics developed in Greco et al. (2016) would not be available, while they are straightforwardly applicable to the present setting. Future work will investigate such a GMT-translation based approach but, at present, it remains to be seen whether the parametric connection between correspondents on Kripke and graph-based frames can also be obtained in this way. Finally, parametric connections between the correspondents of modal formulas remain to be investigated between other semantics environments.

Acknowledgments

The research of Krishna Manoorkar is supported by the NWO grant KIVI.2019.001 awarded to Alessandra Palmigiano. The authors confirm that there are no relevant financial or non-financial competing interests to report.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Additional information

Funding

This work was supported by the KPMG (grant number KIVI.2019.001).

Notes

1 A 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 =\{◻,◊\}$, a polarity-based frame is a structure $\mathbb{F}=(\mathbb{P},R_{◻},R_{◊})$, where $\mathbb{P}$ is polarity, and $R_{◻}\subseteq A\times I,R_{◊}\subseteq X\times I$ are relations that satisfy certain compatibility conditions (cf. Conradie et al. (2017, Definition 2)).

2 In any frame based on a polarity $(A,X,I)$, variables $x,y,z,\dots$ range over X, and variables $a,b,c,\dots$ range over A.

3 In the context of the generalisation of rough set theory pursued in the present paper (cf. Section 4), the intuitive reading of $\mathrm{zE}{z}^{\prime }$ is ‘z is inherently indiscernible from $z^{\prime }$’ for all $z,z^{\prime }\in Z$.

4 A formal context (Ganter & Wille, 2012), 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^{\left(1\right)}\left[B\right]$ and $Y^{\downarrow }:=I^{\left(0\right)}\left[Y\right]$. 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 $\left[\right[c\left]\right]$ for B and $\left(\right[c\left]\right)$ for Y and, consequently, $c=\left(\right[\left[c\right]],(\left[c\right]\left)\right)$. The set $L\left(\mathbb{P}\right)$ of the formal concepts of $\mathbb{P}$ can be partially ordered as follows: for any $c,d\in L\left(\mathbb{P}\right)$, $\begin{array}{r}c\le d\text{ iff }\left[\right[c\left]\right]\subseteq \left[\right[d\left]\right]\text{ iff }\left(\right[d\left]\right)\subseteq \left(\right[c\left]\right).\end{array}$With this order, $L\left(\mathbb{P}\right)$ 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}$.

5 Applying notation (1(1) $\begin{array}{r}\begin{array}{ll}{T}^{\left(1\right)}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}& T^{\left(0\right)}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow \mathrm{uTv}\left)\right\}\\ T^{\left[1\right]}\left[U^{\prime }\right]:=\left\{v|\mathrm{\forall u}\right(u\in U^{\prime }\Rightarrow u{T}^{c}v\left)\right\}& T^{\left[0\right]}\left[V^{\prime }\right]:=\left\{u|\mathrm{\forall v}\right(v\in V^{\prime }\Rightarrow u{T}^{c}v\left)\right\}\end{array}\end{array}$(1) ) to a graph-based $\mathcal{L}$-frame $\mathbb{F}$, we sometimes abbreviate $E^{\left[0\right]}\left[Y\right]$ and $E^{\left[1\right]}\left[B\right]$ as $Y^{\left[0\right]}$ and $B^{\left[1\right]}$, respectively, for all $Y,B\subseteq Z$. If $Y=\left\{y\right\}$ and $B=\left\{b\right\}$, we write $y^{\left[0\right]}$ and $b^{\left[1\right]}$ for $\{y{\}}^{\left[0\right]}$ and $\{b{\}}^{\left[1\right]}$, and write $Y^{\left[01\right]}$ and $B^{\left[10\right]}$ for $(Y^{\left[0\right]}{)}^{\left[1\right]}$ and $(B^{\left[1\right]}{)}^{\left[0\right]}$, respectively. Lemma 2.3 implies that $Y^{\left[0\right]}=I_{E^c}^{\left(0\right)}\left[Y\right]=Y^{\downarrow }$ and $B^{\left[1\right]}=I_{E^c}^{\left(1\right)}\left[B\right]=B^{\uparrow }$, where $(\cdot {)}^{\downarrow }$ and $(\cdot {)}^{\uparrow }$ are the maps associated with ${\mathbb{P}}_{\mathbb{G}}$.

6 For any posets A and B, the maps $f:A\to B$ and $g:B\to A$ form an adjoint pair (notation: $f⊣g$) if for every $a\in A$, and every $b\in B$, $f\left(a\right)\le b\text{ iff }a\le g\left(b\right)$. The map f (resp. g) is the unique left (resp. right) adjoint of g (resp. f). It is well known (cf. (Davey & Priestley, 2002)) 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.

7 The language ${\mathcal{L}}^{+}$ expands ${\mathcal{L}}^{\ast }$ with two denumerable sets of sorted variables $\mathsf{\text{NOM}}\ni \mathbf{\text{i}},\mathbf{\text{j}}$ and $\mathsf{\text{CONOM}}\ni \mathbf{\text{m}},\mathbf{\text{n}}$. The reader is referred to Conradie and Palmigiano (2019, 2020) for a general presentation of ALBA.

8 Recall 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.

9 Notice that the resulting concept lattice is distributive; this is unsurprising, since the graph originating it is not only reflexive but also transitive (cf. Conradie et al. (2020, Proposition 4.1))

10 In the pictures, the red descending arrows represent the non-identity assignments of the $◻$-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.