Kripke Contexts, Double Boolean Algebras with Operators and Corresponding Modal Systems

Abstract

The notion of a context in formal concept analysis and that of an approximation space in rough set theory are unified in this study to define a Kripke context. For any context (G,M,I), a relation on the set G of objects and a relation on the set M of properties are included, giving a structure of the form ((G,R), (M,S), I). A Kripke context gives rise to complex algebras based on the collections of protoconcepts and semiconcepts of the underlying context. On abstraction, double Boolean algebras (dBas) with operators and topological dBas are defined. Representation results for these algebras are established in terms of the complex algebras of an appropriate Kripke context. As a natural next step, logics corresponding to classes of these algebras are formulated. A sequent calculus is proposed for contextual dBas, modal extensions of which give logics for contextual dBas with operators and topological contextual dBas. The representation theorems for the algebras result in a protoconcept-based semantics for these logics.

1 Introduction

Formal concept analysis (FCA) (Wille, 1982) and rough set theory (Pawlak, 1982) are both well-established areas of study with applications in several domains including knowledge representation and data analysis. There has also been a lot of study connecting and comparing the two areas, e.g. in Yao (2004), Meschke (2010), Hu et al. (2001), Ganter and Meschke (2011), Yao and Chen (2006), Kent (1994), Howlader and Banerjee (2018), Howlader and Banerjee (2020a), Saquer and Deogun (2001), and the work presented here is motivated by such studies from the perspective of algebra and logic.

The central objects of FCA are contexts and concepts of a context (Ganter & Wille, 1999). A context is a triple $\mathbb {K}:=(G, M, I)$, where G is the set of objects, and M is the set of attributes and $I\subseteq G\times M$. For any $A\subseteq G, B\subseteq M$, the following sets are defined: $A^{\prime }:=\{m \in M:\text{ for } \text{ all } ~g\in G(g\in A\implies gRm)\}$, and $B^{\prime }:=\{g\in G:\text{ for } \text{ all } ~m\in M(m\in M\implies gRm)\}$. A pair (A, B) is called a concept of $\mathbb {K}$, if $A^{\prime }=B$ and $B^{\prime }=A$. For a concept (A, B), A is its extent and B its intent. $\mathcal {B}(\mathbb {K})$ denotes the set of all concepts of $\mathbb {K}$. An order relation $\le$ is obtained on $\mathcal {B}(\mathbb {K})$ as follows: $\text{ for }~(A_{1},B_{1}),(A_{2},B_{2})\in \mathcal {B}(\mathbb {K}), (A_{1},B_{1}) \le (A_{2},B_{2})~\text{ if } \text{ and } \text{ only } \text{ if }~ A_{1}\subseteq A_{2}~(\text{ equivalent } \text{ to }~ B_{2}\subseteq B_{1})$.

The notion of a concept was generalized to that of semiconcepts and protoconcepts in Luksch and Wille (1991), Wille (2000). A pair (A, B) is called a semiconcept of $\mathbb {K}$, if $A^{\prime }=B$ or $B^{\prime }=A$. (A, B) is called a protoconcept of $\mathbb {K}$, if $A^{\prime \prime }=B^{\prime }$ (equivalently $A^{\prime }=B^{\prime \prime }$). $\mathfrak {H}(\mathbb {K})$ and $\mathfrak {P}(\mathbb {K})$ denote the sets of all semiconcepts and protoconcepts of $\mathbb {K}$ respectively. It is observed that $\mathcal {B}(\mathbb {K})\subseteq \mathfrak {H}(\mathbb {K})\subseteq \mathfrak {P}(\mathbb {K})$. The partial order $\le$ on $\mathcal {B}(\mathbb {K})$ is extended to the set $\mathfrak {P}(\mathbb {K})$ as: for any $(A,B),(C,D)\in \mathfrak {P}(\mathbb {K})$, $(A,B)\sqsubseteq (C,D)$ if and only if $A\subseteq C$ and $D\subseteq B$.

The following operations are defined on $\mathfrak {P}(\mathbb {K})$. For $(A_{1},B_{1}),(A_{2},B_{2})$ in $\mathfrak {P}(\mathbb {K})$,

$$\begin{aligned} (A_{1},B_{1})\sqcap (A_{2},B_{2})&:=(A_{1}\cap A_{2}, (A_{1}\cap A_{2})^{'}),\\ (A_{1},B_{1})\sqcup (A_{2},B_{2})&:=((B_{1}\cap B_{2})^{'}, B_{1}\cap B_{2}),\\ \lnot (A,B)&:=(G{\setminus }A,(G{\setminus }A)^{'}),\\ \lrcorner (A,B)&:=((M{\setminus }B)^{'}, M{\setminus }B),\\ \top&:=(G,\emptyset ),\\ \bot&:=(\emptyset ,M).\\ \end{aligned}$$

With these operations, the protoconcepts of any context form an algebraic structure called double Boolean algebra (dBa) (Wille, 2000). The structure of a dBa is such that there are two negation operators in it, which result in two Boolean algebras being derived from it—justifying the name. The set of semiconcepts, with the same operations as above, forms a subalgebra of the algebra of protoconcepts. In this work, our interest lies in contextual and pure dBas (Vormbrock & Wille, 2005; Wille, 2000), the structures formed by protoconcepts and semiconcepts respectively.

There may be circumstances in which the objects and properties defining a context are indistinguishable with respect to certain attributes. For example, two diseases may be indistinguishable by the symptoms available. Indistinguishability of objects and properties have motivated authors (Kent, 1994, 1996; Saquer & Deogun, 2001; Hu et al., 2001) to study “indiscernibility” relations on the set of objects and the set of properties. Rough set-theoretic notions of approximation spaces and approximation operators (Pawlak, 1982, 1991) are then introduced in FCA.

A Pawlakian approximation space is a pair (W, E), where W is a set and E is an equivalence relation on W. This is generalised to a pair (W, E) with E any binary relation on W, and called a generalised approximation space (Yao & Lin, 1996). For $x\in W$, $E(x):=\{y\in W~:~ xRy\}$. The lower and upper approximations of any $A (\subseteq W)$ are defined respectively as $\underline{A}_{E}:=\{x\in W~:~E(x)\subseteq A\}$, and $\overline{A}^{E}:=\{x\in W~:~E(x)\cap A\ne \emptyset \}$. Kent introduced the notion of approximation space into FCA (Kent, 1994, 1996), and defined lower and upper approximations of contexts and concepts. The work of Saquer and Deogun (2001) differs from that of Kent in choosing the “indiscernibility” relations. Kent considers an indiscernibility relation on the set G of objects which is externally given by some agent, whereas Saquer and Deogun consider a relation that is determined by the given context. For a given context $\mathbb {K}:= (G, M, I)$, relations $E_{1}, E_{2}$ are defined on the set G of objects and the set M of properties respectively, as follows.

• (a) For $g_{1},g_{2}\in G$, $g_{1}E_{1} g_{2}$ if and only if $I(g_{1})=I(g_{2})$.

• (b) For $m_{1}, m_{2}\in M$, $m_{1}E_{2}m_{2}$ if and only if $I^{-1}(m_{1})= I^{-1}(m_{2})$.

Furthermore, for $A\subseteq G, B\subseteq M$, lower and upper approximations are defined in terms of concepts of $\mathbb {K}$, and using these, approximations of any pair (A, B) that is not a concept, are given. Apart from Hu et al. (2001) introduce approximation spaces on the sets of objects and properties. In Hu et al. (2001), for a given context $\mathbb {K}:= (G, M, I)$, relations $J_{1}, J_{2}$ are defined on G and M respectively, as follows.

• (a) For $g_{1},g_{2}\in G$, $g_{1}J_{1} g_{2}$ if and only if $I(g_{1})\subseteq I(g_{2})$.

• (b) For $m_{1}, m_{2}\in M$, $m_{1}J_{2}m_{2}$ if and only if $I^{-1}(m_{1})\subseteq I^{-1}(m_{2})$.

The relations $E_{1}, E_{2}$ are equivalence relations (Saquer & Deogun, 2001), while the relations $J_{1}, J_{2}$ are partial order relations (Hu et al., 2001). These observations have motivated us to define the Kripke context, which unifies within a single framework, the notions of a context of FCA and approximation space of rough set theory.

Definition 1

A Kripke context based on a context $\mathbb {K}:=(G,M,I)$ is a triple ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$, where R, S are relations on G and M respectively.

So a Kripke context consists of a context of FCA and two Kripke frames, which in the terminology of rough set theory, are generalised approximation spaces. Note that for a context $\mathbb {K}:=(G, M, I)$, we get a Kripke context ${\mathbb {K}}{\mathbb {C}}_{DS}:=((G, E_{1}), (M, E_{2}), I)$. Moreover, ${\mathbb {K}}{\mathbb {C}}_{DS}$ is an example such that the relations $E_{1}$ and $E_{2}$ are reflexive, symmetric and transitive. This observation has led us to define reflexive, symmetric or transitive Kripke contexts, where the relations R and S are reflexive, symmetric or transitive.

It is shown that, using the lower and upper approximation operators induced by the approximation space (G, R), (M, S) in a Kripke context ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$, one can define unary operators $f_{R}$ and $f_{S}$ on the set $\mathfrak {P}(\mathbb {K})$ of protoconcepts of the underlying context $\mathbb {K}:=(G,M,I)$ such that $f_{R}$ is an interior-type operator, while $f_{S}$ is a closure-type operator. The Kripke context thus leads to complex algebras. The algebra of protoconcepts with the operators $f_{R}$ and $f_{S}$, is called the full complex algebra of ${\mathbb {K}}{\mathbb {C}}$. Any subalgebra of the full complex algebra of ${\mathbb {K}}{\mathbb {C}}$ is called a complex algebra. For a Kripke context ${\mathbb {K}}{\mathbb {C}}$, the algebra of semiconcepts $\mathfrak {H}(\mathbb {K})$ with operators $f_{R}{\restriction }{\mathfrak {H}(\mathbb {K})}$ and $f_{S}{\restriction }{\mathfrak {H}(\mathbb {K})}$ is an instance of a complex algebra of ${\mathbb {K}}{\mathbb {C}}$. We show how, in terms of approximation spaces and operators $f_{E_{1}}$ and $f_{E_{2}}$, the full complex algebra of the Kripke context ${\mathbb {K}}{\mathbb {C}}_{DS}$ can be utilised to compute all the approximation operators defined in the work of Saquer and Deogun (2001).

To understand the equational theory of the full complex algebra of protoconcepts and the complex algebra of semiconcepts, abstractions of these structures are defined: these are the double Boolean algebras with operators (dBao) and topological dBas respectively. An immediate example of a dBao is a Boolean algebra with operators (Blackburn et al., 2001); a topological Boolean algebra (Jonsson & Tarski, 1951) gives an instance of a topological dBa. It is shown that the full complex algebra of ${\mathbb {K}}{\mathbb {C}}$ forms a contextual dBao, while the complex algebra of semiconcepts forms a pure dBao. For a reflexive and transitive Kripke context, the full complex algebra forms a topological contextual dBa and the complex algebra of semiconcepts forms a topological pure dBa. Representation theorems for these classes of algebras are then proved, in terms of the complex algebras of protoconcepts and semiconcepts of an appropriate Kripke context. The results are based on the representations obtained for dBas by Wille (2000) and Balbiani (2012).

As a natural next step, logics corresponding to dBaos are formulated. A sequent calculus, denoted CDBL, is proposed for contextual dBas. CDBL is extended to MCDBL and MCDBL4 for the contextual dBaos and topological contextual dBas respectively. Due to the representation theorems for the algebras, one is able to get another semantics for these logics, based on protoconcepts of contexts.

Section 2 gives the preliminaries required for this work. Kripke contexts, their examples and the related complex algebras are studied in Sect. 3. In particular, we indicate in Sect. 3.1 how the various approximations defined in Saquer and Deogun (2001) can be expressed using terms of the full complex algebra of ${\mathbb {K}}{\mathbb {C}}_{DS}$. The dBaos and the topological dBa along with the representation results are presented in Sect. 4. In Sect. 5, the logics corresponding to the algebras are studied. CDBL for the class of contextual dBas is discussed in Sect. 5.1; in Sect. 5.2, CDBL is extended to MCDBL and MCDBL4. In Sect. 5.3, the protoconcept-based semantics for the logics is given. Section 6 concludes the article.

In our presentation, the symbols $\Rightarrow$, $\Leftrightarrow$, and, or and not will be used with the usual meanings in the metalanguage. Throughout, for a map f on X, $f\restriction {A}$ denotes the restriction of the map f on $A\subseteq X$, $\mathcal {P}(X)$ denotes the power set of any set X, and the complement of $A\subseteq X$ in a set X is denoted $A^{c}$. For basic notions on universal algebra and lattices, we refer to Burris and Sankappanavar (1981), Davey and Priestley (2002).

2 Preliminaries

In the following subsections, we present basic notions and results related to dBas, Boolean algebras with operators and approximation operators. Our primary references are Ganter and Wille (1999), Wille (2000), Balbiani (2012), Blackburn et al. (2001), Jonsson and Tarski (1951), Saquer and Deogun (2001).

2.1 Double Boolean Algebra

A double Boolean algebra is defined as follows.

Definition 2

(Wille, 2000) An algebra ${\textbf {D}}:= (D,\sqcup ,\sqcap , \lnot ,\lrcorner ,\top ,\bot )$, satisfying the following properties is called a double Boolean algebra (dBa). For any $x,y,z \in D$, $\begin{array}{ll} (1a)~ (x \sqcap x ) \sqcap y = x \sqcap y &{} (1b)~ (x \sqcup x)\sqcup y = x \sqcup y \\ (2a)~ x\sqcap y = y\sqcap x &{} (2b)~ x \sqcup y = y\sqcup x \\ (3a)~ x \sqcap ( y \sqcap z) = (x \sqcap y) \sqcap z &{} (3b)~ x \sqcup (y \sqcup z) = (x \sqcup y)\sqcup z \\ (4a)~ \lnot (x \sqcap x) = \lnot x &{} (4b)~ \lrcorner (x \sqcup x )= \lrcorner x \\ (5a)~ x \sqcap (x \sqcup y)=x \sqcap x &{} (5b)~ x \sqcup (x \sqcap y) = x \sqcup x \\ (6a)~ x \sqcap (y \vee z ) = (x\sqcap y)\vee (x \sqcap z) &{} (6b)~ x \sqcup (y \wedge z) = (x \sqcup y) \wedge (x \sqcup z) \\ (7a)~ x \sqcap (x\vee y)= x \sqcap x &{} (7b)~ x\sqcup (x \wedge y) =x \sqcup x \\ (8a)~ \lnot \lnot (x \sqcap y)= x \sqcap y &{} (8b)~ \lrcorner \lrcorner (x \sqcup y) = x\sqcup y \\ (9a)~ x \sqcap \lnot x= \bot &{} (9b)~ x \sqcup \lrcorner x = \top \\ (10a)~ \lnot \bot = \top \sqcap \top &{} (10b)~ \lrcorner \top =\bot \sqcup \bot \\ (11a)~ \lnot \top = \bot &{} (11b)~ \lrcorner \bot =\top \\ (12)~ (x \sqcap x) \sqcup (x \sqcap x) = (x \sqcup x) \sqcap (x \sqcup x), &{} \end{array}$

where $x\vee y := \lnot (\lnot x \sqcap \lnot y)$, and $x \wedge y :=\lrcorner (\lrcorner x \sqcup \lrcorner y)$. A quasi-order relation $\sqsubseteq$ on ${\textbf {D}}$ is defined as follows: $x\sqsubseteq y ~\text{ if } \text{ and } \text{ only } \text{ if }~ x\sqcap y=x\sqcap x~\text{ and }~x\sqcup y=y\sqcup y,$ for any $x,y \in D$.

A dBa ${\textbf {D}}$ is called contextual if $\sqsubseteq$ is a partial order. A contextual dBa is also known as a regular dBa (Breckner & Săcărea, 2019). ${\textbf {D}}$ is pure if for all $x\in D$, either $x\sqcap x=x$ or $x\sqcup x=x$. In the following, let ${{\varvec{D}}}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ be a dBa. Let us give some notations that shall be used:

$D_{\sqcap }:=\{x\in D~:~x\sqcap x=x\}$, $D_{\sqcup }:=\{x\in D~:~x\sqcup x=x\}$, $D_{p}:=D_{\sqcap }\cup D_{\sqcup }$.

For $x\in D$, $x_{\sqcap }:=x\sqcap x$ and $x_{\sqcup }:=x\sqcup x$.

Proposition 1

(Wille, 2000) ${\textbf {D}}_{p}:=(D_{p},\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ is the largest pure subalgebra of ${\textbf {D}}$. Moreover, if ${\textbf {D}}$ is pure, ${\textbf {D}}_{p}={\textbf {D}}$.

Proposition 2

(Balbiani, 2012) Every pure dBa ${\textbf {D}}$ is contextual.

Proposition 3

(Vormbrock, 2007)

• 1. ${\textbf {D}}_{\sqcap }:=(D_{\sqcap },\sqcap ,\vee ,\lnot ,\bot ,\lnot \bot )$ is a Boolean algebra whose order relation is the restriction of $\sqsubseteq$ to $D_{\sqcap }$ and is denoted by $\sqsubseteq _{\sqcap }$.

• 2. ${\textbf {D}}_{\sqcup }:=(D_{\sqcup },\sqcup ,\wedge ,\lrcorner ,\top ,\lrcorner \top )$ is a Boolean algebra whose order relation is the restriction of $\sqsubseteq$ to $D_{\sqcup }$ and it is denoted by $\sqsubseteq _{\sqcup }$.

• 3. $x\sqsubseteq y$ if and only if $x\sqcap x\sqsubseteq y\sqcap y$ and $x\sqcup x\sqsubseteq y\sqcup y$ for $x,y\in D$, that is, $x_{\sqcap }\sqsubseteq _{\sqcap } y_{\sqcap }$ and $x_{\sqcup }\sqsubseteq y_{\sqcup }$.

Proposition 4

(Kwuida, 2007) Let $x,y,a\in D$. Then the following hold.

• 1. $x\sqcap \bot =\bot$ and $x\sqcup \bot =x\sqcup x$ that is $\bot \sqsubseteq x$.

• 2. $x\sqcup \top =\top$ and $x\sqcap \top =x\sqcap x$ that is $x\sqsubseteq \top$.

• 3. $x=y$ implies that $x\sqsubseteq y$ and $y\sqsubseteq x$.

• 4. $x\sqsubseteq y$ and $y \sqsubseteq x$ if and only if $x\sqcap x=y\sqcap y$ and $x\sqcup x = y\sqcup y$.

• 5. $x\sqcap y\sqsubseteq x,y\sqsubseteq x\sqcup y, x\sqcap y\sqsubseteq y,x\sqsubseteq x\sqcup y$.

• 6. $x\sqsubseteq y$ implies $x\sqcap a\sqsubseteq y\sqcap a$ and $x\sqcup a\sqsubseteq y\sqcup a$.

Proposition 5

(Howlader & Banerjee, 2020b) For any $x,y\in D$, the following hold.

• 1. $\lnot x\sqcap \lnot x=\lnot x$ and $\lrcorner x\sqcup \lrcorner x=\lrcorner x$, that is, $\lnot x=(\lnot x)_{\sqcap }\in D_{\sqcap }$, $\lrcorner x=(\lrcorner x)_{\sqcup }\in D_{\sqcup }$.

• 2. $x\sqsubseteq y$ if and only if $\lnot y\sqsubseteq \lnot x$ and $\lrcorner y\sqsubseteq \lrcorner x$.

• 3. $\lnot \lnot x=x\sqcap x$ and $\lrcorner \lrcorner x=x\sqcup x$.

• 4. $x\vee y\in D_{\sqcap }, x\wedge y\in D_{\sqcup }$.

• 5. $\lnot \lnot \bot =\bot$, and $\lrcorner \lrcorner \top =\top$.

• 6. $\lnot (x\sqcap y)=\lnot x\vee \lnot y$ and $\lrcorner (x\sqcup y)=\lrcorner x\wedge \lrcorner y$.

Definition 3

A subset F of D is a filter in ${\textbf {D}}$ if and only if $x\sqcap y\in F$ for all $x,y \in F$, and for all $z\in D$ and $x \in F, x\sqsubseteq z$ implies that $z\in F$. An ideal in a dBa is defined dually.

A filter F (ideal I) is proper if and only if $F\ne D$ ($I\ne D$). A proper filter F (ideal I) is called primary if and only if $x\in F~ \text{ or } ~\lnot x \in F ~(x\in I ~\text{ or }~ \lrcorner x\in I)$, for all $x\in D$.

The set of primary filters is denoted by $\mathcal {F}_{pr}({\textbf {D}})$; the set of all primary ideals is denoted by $\mathcal {I}_{pr}({\textbf {D}})$.

A base $F_{0}$ for a filter F is a subset of D such that $F=\{x\in D~:~ z\sqsubseteq x~\text{ for } \text{ some }~ z\in F_{0}\}$. A base for an ideal is defined similarly.

For a subset X of D, F(X) and I(X) denote the filter and ideal generated by X respectively.

Lemma 1

(Kwuida, 2007) Let F be a filter and I an ideal of ${\textbf {D}}$. Then for any element $x\in D$,

• 1. $F(F\cup \{x\})=\{a\in D~:~ x\sqcap w\sqsubseteq a~\text{ for } \text{ some }~ w\in F\}$.

• 2. $I(I\cup \{x\})=\{a\in D~:~a\sqsubseteq x\sqcup w~\text{ for } \text{ some }~ w\in I\}$.

The following are introduced in Wille (2000) to prove representation theorems for dBas.

$\mathcal {F}_{p}({\textbf {D}}):=\{F \subseteq D : F ~\text{ is } \text{ a } \text{ filter } \text{ of }~{\textbf {D}}~\text{ and }~F\cap D_{\sqcap } ~\text{ is } \text{ a } \text{ prime } \text{ filter } \text{ in }~ {\textbf {D}}_{\sqcap }\}$.

$\mathcal {I}_{p}({\textbf {D}}):=\{I \subseteq D : I ~\text{ is } \text{ an } \text{ ideal } \text{ of }~{\textbf {D}}~\text{ and }~I\cap D_{\sqcup }~ \text{ is } \text{ a } \text{ prime } \text{ ideal } \text{ in }~ {\textbf {D}}_{\sqcup }\}$.

Proposition 6

(Howlader & Banerjee, 2020b) $\mathcal {F}_{p}({\textbf {D}})=\mathcal {F}_{pr}({\textbf {D}})$ and $\mathcal {I}_{p}({\textbf {D}})=\mathcal {I}_{pr}({\textbf {D}})$.

Lemma 2

(Wille, 2000)

• 1. For any filter F of ${\textbf {D}}$, $F\cap D_{\sqcap }$ and $F\cap D_{\sqcup }$ are filters of the Boolean algebras ${\textbf {D}}_{\sqcap }$, ${\textbf {D}}_{\sqcup }$ respectively.

• 2. Each filter $F_{0}$ of the Boolean algebra ${\textbf {D}}_{\sqcap }$ is the base of some filter F of ${\textbf {D}}$ such that $F_{0}=F\cap D_{\sqcap }$. Moreover if $F_{0}$ is prime, $F\in \mathcal {F}_{p}({\textbf {D}})$.

It is straightforward to show that similar results hold for ideals of dBas.

For a context $\mathbb {K}:=(G, M, I)$ and sets $A \subseteq G,B,\subseteq M$, recall the sets $A^\prime , B^\prime$ and the operations on protoconcepts of $\mathbb {K}$ defined in Sect. 1.

Lemma 3

(Davey & Priestley, 2002)

• 1. $A\subseteq A^{\prime \prime }$ and $B\subseteq B^{\prime \prime }$.

• 2. $A\subseteq X$ implies that $X^{\prime }\subseteq A^{\prime }$, $B\subseteq Y$ implies that $Y^{\prime }\subseteq B^{\prime }$, for any $X\subseteq G$ and $Y\subseteq M$.

Theorem 7

(Wille, 2000)

• 1. $\underline{\mathfrak {P}}(\mathbb {K}):= (\mathfrak {P}(\mathbb {K}), \sqcap ,\sqcup ,\lnot ,\lrcorner ,\top ,\bot )$ is a contextual dBa.

• 2. $\underline{\mathfrak {H}}(\mathbb {K}):=(\mathfrak {H}(\mathbb {K}), \sqcap ,\sqcup ,\lnot ,\lrcorner ,\top ,\bot )$ is a pure dBa. Moreover, $\underline{\mathfrak {H}}(\mathbb {K})=\underline{\mathfrak {P}}(\mathbb {K})_{p}$.

Theorem 8

(Wille, 2000)

• 1. The power set Boolean algebra $(\mathcal {P}(G), \cap , \cup ,^{c}, G, \emptyset )$ is isomorphic to the Boolean algebra $\underline{\mathfrak {P}}(\mathbb {K})_{\sqcap }:= (\mathfrak {P}(\mathbb {K})_{\sqcap }, \sqcap ,\vee ,\lnot ,\bot ,\lnot \bot )$, where any $A (\subseteq G)$ is mapped to $(A,A^{\prime }) \in \mathfrak {P}(\mathbb {K})_{\sqcap }$.

• 2. The power set Boolean algebra $(\mathcal {P}(M), \cup , \cap , ^{c}, M, \emptyset )$ is anti-isomorphic to the Boolean algebra $\underline{\mathfrak {P}}(\mathbb {K})_{\sqcup }:= (\mathfrak {P}(\mathbb {K})_{\sqcup }, \sqcup ,\wedge , \lrcorner ,\top ,\lrcorner \top )$, where any $B (\subseteq M)$ is mapped to $(B^{\prime },B) \in \mathfrak {P}(\mathbb {K})_{\sqcup }$.

Let us now move to representation theorems for dBas. The following notations and results are needed. Let ${\textbf {D}}$ be a dBa. For any $x \in D$,

$F_{x}:=\{F\in \mathcal {F}_{p}({\textbf {D}})~:~x\in F\}$ and $I_{x}:=\{I\in \mathcal {I}_{p}({\textbf {D}})~:~x\in I\}$.

Lemma 4

(Wille, 2000; Howlader & Banerjee, 2020a) Let $x\in D$. Then the following hold.

• 1. $(F_{x})^{c}=F_{\lnot x}$ and $(I_{x})^{c}=I_{\lrcorner x}$.

• 2. $F_{x\sqcap y}=F_{x}\cap F_{y}$ and $I_{x\sqcup y}=I_{x}\cap I_{y}$.

To prove the representation theorem, Wille uses the standard context corresponding to the dBa ${\textbf {D}}$, defined as $\mathbb {K}({\textbf {D}}):=(\mathcal {F}_{p}({\textbf {D}}),\mathcal {I}_{p}({\textbf {D}}),\Delta )$, where for all $F\in \mathcal {F}_{p}({\textbf {D}})$ and $I\in \mathcal {I}_{p}({\textbf {D}})$, $F\Delta I$ if and only if $F\cap I=\emptyset$. Then we have

Lemma 5

(Wille, 2000) For all $x\in {\textbf {D}}$, $F_{x}^{\prime }=I_{x_{\sqcap \sqcup }}$ and $I_{x}^{\prime }=F_{x_{\sqcup \sqcap }}$.

Theorem 9

(Wille, 2000) The map $h:{\textbf {D}}\rightarrow \underline{\mathfrak {P}}(\mathbb {K}({\textbf {D}}))$ defined by $h(x):=(F_{x},I_{x})$ for all $x\in {\textbf {D}}$ is a quasi-embedding.

As a consequence of the above theorem, we have

Corollary 1

For a contextual dBa ${\textbf {D}}$, the map $h:{\textbf {D}}\rightarrow \underline{\mathfrak {P}}(\mathbb {K}({\textbf {D}}))$ defined by $h(x):=(F_{x},I_{x})$ for all $x\in {\textbf {D}}$ is an embedding.

Theorem 10

(Balbiani, 2012) Let ${\textbf {D}}$ be a pure dBa. The map $h:{\textbf {D}}\rightarrow \underline{\mathfrak {H}}(\mathbb {K}({\textbf {D}}))$ defined by $h(x):=(F_{x},I_{x})$ for all $x\in {\textbf {D}}$ is an embedding.

2.2 Boolean Algebras with Operators

In the literature, there are several definitions of Boolean algebras with additional operators. In this section, we mention the ones to be used in this work.

Definition 4

(Blackburn et al., 2001) A Boolean algebra with operators (Bao) is an algebra $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, f)$ such that $(B, \vee , \wedge , \lnot , 0)$ is a Boolean algebra and $f:B \rightarrow B$ satisfies the following.

$\begin{array}{ll} {{ Normality}:}~ f(0)=0,&{{ Additivity}:}~ f(x\vee y)= f(x)\vee f(y). \end{array}$

Note that Blackburn et al. (2001) gives a general definition of Baos with more than one operator. In Jonsson and Tarski (1951), a Boolean algebra $(B, \vee , \wedge , \lnot , 0)$ with only an additive operator f is taken as the definition of Bao.

Definition 5

(Jonsson & Tarski, 1951) An algebra $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, f )$ is called a closure algebra if $(B, \vee , \wedge , \lnot , 0)$ is a Boolean algebra and for all $x, y\in B$, $f:B \rightarrow B$ satisfies the following conditions.

$\begin{array}{ll} 1.~ f(0)=0.&{} 2.~ f(x\vee y)= f(x)\vee f(y).\\ 3.~ ff(x)=f(x).&{} 4.~ x\le f(x). \end{array}$

Note that for a closure algebra $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, f )$, one can define an operator g on B as: $g(x):=\lnot f(\lnot x)$, for all $x\in B$. Then for all $x, y\in B$,

$\begin{array}{ll} 1^{\prime }.~ g(1)=1.&{} 2^{\prime }.~ g(x\wedge y)= g(x)\wedge g(y).\\ 3^{\prime }.~ gg(x)=g(x).&{} 4^{\prime }.~g(x) \le x. \end{array}$

An algebra $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, g )$, where $(B, \vee , \wedge , \lnot , 0)$ is a Boolean algebra and g satisfies $1^{\prime },2^{\prime }, 3^{\prime },4^{\prime }$ is called a topological Boolean algebra in Rasiowa (1974). Moreover, for a topological Boolean algebra $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, g )$, one can define an operator $g^{\delta }(x):=\lnot g(\lnot x)$, for all $x\in D$ such that $\mathfrak {A}:=(B, \vee , \wedge , \lnot , 0, g^{\delta })$ is a closure algebra. In other words, a closure algebra and a topological Boolean algebra of Rasiowa (1974) are dual to each other and one can be obtained from the other. In this work, by a topological Boolean algebra, we shall mean a closure algebra.

2.3 Approximation Operators

Recall the definitions of lower and upper approximation operators in an approximation space given in Sect. 1. If the relation is clear from the context, we shall omit the subscript and denote $\underline{A}_{E}$ by $\underline{A}$, $\overline{A}^{E}$ by $\overline{A}$.

Proposition 11

(Yao & Lin, 1996)

• I. For an approximation space (W, E), the following hold.

• (i) $\overline{A}=(\underline{(A^{c})})^{c}, \underline{A}=(\overline{(A^{c})})^{c}$.

• (ii) $\underline{W}= W$.

• (iii) $\underline{A\cap B}=\underline{A}\cap \underline{B}, \overline{A\cup B}=\overline{A}\cup \overline{B}$.

• (iv) $A\subseteq B$ implies that $\underline{A} \subseteq \underline{B}, \overline{A} \subseteq \overline{B}$.

• II. Moreover if E is a reflexive and transitive relation then the following hold.

• (i) $\underline{A}\subseteq A$ and $A\subseteq \overline{A}$.

• (ii) $\underline{(\underline{A})}=\underline{A}$ and $\overline{(\overline{A})}=\overline{A}$.

Let $\mathbb {K}:=(G,M, I)$ be a context and recall the approximation spaces $(G, E_{1})$ and $(M, E_{2})$ mentioned in Sect. 1. In Saquer and Deogun (2001), $A\subseteq G$ and $B\subseteq M$ are called feasible if $A^{\prime \prime }=A$ and $B^{\prime \prime }=B$. Then the concept approximation(s) of A are defined as follows.

• If A is feasible, the concept approximation of A is $(A, A^{\prime })$.

• If A is not feasible, A is considered as s rough set of the approximation space $(G, E_{1})$, and its concept approximations are defined with the help of its lower approximation $\underline{A}_{E_{1}}$ and upper approximation $\overline{A}^{E_{1}}$. The lower concept approximation of A is the pair $((\underline{A}_{E_{1}})^{\prime \prime }, (\underline{A}_{E_{1}})^{\prime })$, while its upper concept approximation is $((\overline{A}^{E_{1}})^{\prime \prime }, (\overline{A}^{E_{1}})^{\prime })$.

For $B\subseteq M$:

• if B is feasible, the concept approximation of B is $(B^{\prime }, B)$;

• if B is non-feasible, the lower and upper concept approximations of B are defined by $((\overline{B}^{E_{2}})^{\prime }, (\overline{B}^{E_{2}})^{\prime \prime })$ and $((\underline{B}_{E_{2}})^{\prime }, (\underline{B}_{E_{2}})^{\prime \prime })$ respectively.

A pair (A, B) is called a non-definable concept, if it is not a concept of the context $\mathbb {K}$. A concept is said to approximate such a pair (A, B), if its extent approximates A and intent approximates B. The four possible cases for A, B are considered: (i) both A and B are feasible, (ii) A is feasible and B is not, (iii) B is feasible and A is not, and (iv) both A and B are not feasible. In case both A and B are feasible and $A^{\prime }=B$ then the pair (A, B) itself constitutes a concept and no approximations are needed. For the other cases, the lower approximation of (A, B) is obtained in terms of the meet of the lower concept approximations of its individual components, while the upper approximation of (A, B) is obtained in terms of the join of the upper concept approximations of its individual components. For example, consider case (iv), when both A and B are not feasible.

The lower approximation of (A, B) is defined by $\underline{(A, B)}:=((\underline{A}_{E_{1}})^{\prime \prime }, (\underline{A}_{E_{1}})^{\prime })\sqcap ((\overline{B}^{E_{2}})^{\prime }, (\overline{B}^{E_{2}})^{\prime \prime }) =((\underline{A}_{E_{1}})^{\prime \prime }\cap (\overline{B}^{E_{2}})^{\prime }, ((\underline{A}_{E_{1}})^{\prime \prime }\cap (\overline{B}^{E_{2}})^{\prime })^{\prime } )$.

The upper approximation of (A, B) is defined by $\overline{(A, B)}:=((\overline{A}^{E_{1}})^{\prime \prime }, (\overline{A}^{E_{1}})^{\prime })\sqcup ((\underline{B}_{E_{2}})^{\prime }, (\underline{B}_{E_{2}})^{\prime \prime }) =(((\overline{A}^{E_{1}})^{\prime }\cap (\underline{B}_{E_{2}})^{\prime \prime })^{\prime }, (\overline{A}^{E_{1}})^{\prime }\cap (\underline{B}_{E_{2}})^{\prime \prime } )$.

Let us illustrate these notions by an example. The following context (G, M, I) is a subcontext of a context given by Ganter and Wille (1999) with some modifications. $G:=\{Leech, Bream,Frog,Dog, Cat\}$ and $M:=\{a,b,c,g\}$, where a:= needs water to live, b:= lives in water, c:= lives on land, g:=can move around. I is given by Table 1, where * as an entry corresponding to object x and property y means xIy holds.

Table 1 Context $\mathbb {K}$

Observe that the properties a and g are indiscernible by objects, while Leech and Bream as well as Dog and Cat are indiscernible by properties. The induced approximation spaces are $(G, \{\{Leech, Bream\},\{Frog\}, \{Dog, Cat\}\})$ and $(M, \{\{a,\text{ g }\}, \{b\},\{c\}\})$.

Let $A:=\{Leech, Bream , Dog\}$ and $B:=\{a,c\}$. A is not feasible, as $A^{\prime \prime }\ne A$. B is also non-feasible. The upper and lower concept approximations of A are $(G,\{a, g\})$ and $(\{ Leech, Bream, Frog\}, \{a,b,\text{ g }\})$, respectively. The upper and lower concept approximations of B are both given by $(\{Frog,Dog,Cat\}, \{a,\text{ g },c\})$. Moreover, (A, B) is a non-definable concept. The lower approximation of (A, B) is $(\{Frog\}, M)$ and the upper approximation is $(G,\{a, g\})$.

3 Kripke Context

As given by Definition 1 in Sect. 1, a Kripke context based on a context $\mathbb {K}:=(G,M,I)$ is a triple ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$, where R, S are binary relations on G and M respectively. Let us give a couple of examples of Kripke contexts. The first example is based on Pawlakian approximation spaces.

Example 1

${\mathbb {K}}{\mathbb {C}}:=((G, R), (M, S), I)$, where $G:=\{D_1,D_2,D_3,D_4\}$ represents a collection of diseases and $M:=\{S_1,S_2,S_3,S_4,S_5\}$ a collection of symptoms. $D_iIS_j$ holds if disease $D_i$ has symptom $S_j$, and I is given by Table 2. Equivalence relations R on G and S on M are then induced as follows, relating respectively, the diseases that have the same set of symptoms, and the symptoms that apply to the same set of diseases:

$D_i R D_j$, if and only if $I(D_i)= I(D_j)$, $i,j \in \{1,2,3,4\}$ and $S_i R S_j$, if and only if $I^{-1}(S_i)= I^{-1}(S_j)$, $i,j \in \{1,2,3,4,5\}$.

One thus gets the approximation spaces (G, R) and (M, S).

Table 2 Context $\mathbb {K}$

Our next example is motivated by the notion of bisimulation between Kripke frames (Blackburn et al., 2001). It gives a Kripke context ${\mathbb {K}}{\mathbb {C}}:=((G, R), (M, S), I)$ such that the relation I is in fact, a bisimulation between the Kripke frames (G, R) and (M, S), that is, it satisfies the back and forth conditions: for all $g\in G$ and $m\in M$,

for all $g_{1}\in G$ $(gRg_{1}$ and $gIm\implies \text{ there } \text{ exists }~ m_{1}\in M(mSm_{1}~\text{ and }~g_{1}Im_{1}))$;

for all $m_{1}\in M$ $(mSm_{1}$ and $gIm \implies \text{ there } \text{ exists }~ g_{1}\in M(gRg_{1}~\text{ and }~g_{1}Im_{1}))$.

Example 2

${\mathbb {K}}{\mathbb {C}}:=((G, R), (M, S), I)$, where $G:=\{c, d, e\}$, $M:=\{a, b\}$, $R:=\{ (d, e), ( c, d)\}$ and $S:=\{(a, b), (b, a)\}$. I is given by Table 3. Figure 1 depicts the objects, properties and the three relations R, S, I. Each circular node represents an object and each rectangular node a property. Two circular nodes are connected by an arrow if they are related by R. Similarly for the rectangular nodes. The dotted arrow represents the relation I. From the figure it is clear that I satisfies the back and forth conditions.

Table 3 Context $\mathbb {K}$

Fig. 1

Kripke Context ${\mathbb {K}}{\mathbb {C}}$

In a Kripke context ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$, if (G, R) is a Pawlakian approximation space, one gets an interior operator $-_{R}:\mathcal {P}(G)\rightarrow \mathcal {P}(G)$ defined as $-_{R}(A):=\underline{A}_{R}$ for all $A\in \mathcal {P}(G)$ (Proposition 11). Similarly, one has the interior operator $-_{S}:\mathcal {P}(M)\rightarrow \mathcal {P}(M)$ defined by $-_{M}(B):=\underline{B}_{S}$ for all $B\in \mathcal {P}(M)$, if (M, S) is a Pawlakian approximation space. Now from Theorem 8, we get the isomorphism $f:\mathcal {P}(G)\rightarrow \mathfrak {P}(\mathbb {K})_{\sqcap }$ given by $f(A):=(A, A^{\prime })$ for all $A\in \mathcal {P}(G)$ and the anti-isomorphism $g:\mathcal {P}(M)\rightarrow \mathfrak {P}(\mathbb {K})_{\sqcup }$ given by $g(B):=(B^{\prime }, B)$ for all $B\in \mathcal {P}(M)$. Taking a cue from the compositions of $f,-_{R}$ and $g,-_{S}$, we can define two unary operators $f_R$ and $f_S$ on $\mathfrak {P}(\mathbb {K})$ as given below. It will be seen in Theorem 12 that $f_R$ is an interior-type operator on $\mathfrak {P}(\mathbb {K})$, while $g_S$ is a closure-type operator on $\mathfrak {P}(\mathbb {K})$. For any $(A,B)\in \mathfrak {P}(\mathbb {K})$,

• $f_{R}((A,B)):=(\underline{A}_{R},(\underline{A}_{R})^{\prime })$,

• $f_{S}((A,B)):=((\underline{B}_{S})^{\prime },\underline{B}_{S})$.

$f_{R}, f_{S}$ are well-defined, as $(\underline{A}_{R}, (\underline{A}_{R})^{\prime })$ and $((\underline{B}_{S})^{\prime },\underline{B}_{S})$ are both semiconcepts and hence protoconcepts of $\mathbb {K}$. This implies that the set $\mathfrak {P}(\mathbb {K})$ of protoconcepts is closed under the operators $f_{R}, f_{S}$. We have

Definition 6

Let ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$ be a Kripke context. The full complex algebra of ${\mathbb {K}}{\mathbb {C}}$, $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}):=(\mathfrak {P}(\mathbb {K}),\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,f_{R},f_{S})$, is the expansion of the algebra $\underline{\mathfrak {P}}(\mathbb {K})$ of protoconcepts with the operators $f_{R}$ and $f_{S}$.

Any subalgebra of $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$ is called a complex algebra of ${\mathbb {K}}{\mathbb {C}}$.

Let $f_{R}^{\delta }, f_{S}^{\delta }$ denote the operators on $\mathfrak {P}(\mathbb {K})$ that are dual to $f_{R}, f_{S}$ respectively. In other words, for each $x:=(A,B)\in \mathfrak {P}(\mathbb {K})$,

$f_{R}^{\delta }(x):=\lnot f_{R}(\lnot x)=\lnot f_{R}((A^{c}, A^{c\prime }))=\lnot (\underline{A}^{c}_{R},(\underline{A}^{c}_{R})^{\prime })=((\underline{A}^{c}_{R})^{c},(\underline{A}^{c}_{R})^{c\prime })=(\overline{A}^{R},(\overline{A}^{R})^{\prime })$, by Proposition 11(i).

Similarly $f_{S}^{\delta }(x):=\lrcorner f_{S}(\lrcorner x)=((\overline{B}^{S})^{\prime }, \overline{B}^{S})$.

Again, note that $f_{R}^{\delta }(x) = (\overline{A}^{R}, (\overline{A}^{R})^{\prime })$ and $f_{S}^{\delta }(x) = ((\overline{B}^{S})^{\prime },\overline{B}^{S})$ are semiconcepts of $\mathbb {K}$. Let us now list some properties of $f_{R}$ and $f_{S}$.

Theorem 12

For all $x, y\in \mathfrak {P}(\mathbb {K})$, the following hold.

• 1. $f_{R}(x\sqcap y)=f_{R}(x)\sqcap f_{R}(y)$ and $f_{S}(x\sqcup y)=f_{S}(x)\sqcup f_{S}(y)$.

• 2. $f_{R}(x\sqcap x)=f_{R}(x)$ and $f_{S}(x\sqcup x)=f_{S}(x)$.

• 3. $f_{R}(\lnot \bot )=\lnot \bot$ and $f_{S}(\lrcorner \top )=\lrcorner \top$.

• 4. $f_{R}(\lnot x)=\lnot f_{R}^{\delta }(x)$ and $f_{S}(\lrcorner x)=\lrcorner f_{S}^{\delta }(x)$.

Proof

Let $x:=(A,B)$ and $y:=(C,D)$.

1. We use Proposition 11(iii) in the following equations. $f_{R}((A,B)\sqcap (C,D))=f_{R}(A\cap C, (A\cap C)^{\prime })=(\underline{A\cap C}_{R},(\underline{A\cap C}_{R})^{\prime } )=(\underline{A}_{R}\cap \underline{C}_{R},(\underline{A}_{R}\cap \underline{C}_{R})^{\prime })=(\underline{A}_{R},(\underline{A}_{R})^{\prime })\sqcap (\underline{C}_{R}, (\underline{C}_{R})^{\prime })=f_{R}((A,B))\sqcap f_{R}((C,D))$.

$f_{S}((A,B)\sqcup (C,D))=f_{S}((B\cap D)^{\prime },B\cap D)=((\underline{B\cap D}_{S})^{\prime },\underline{B\cap D}_{S})=f_{S}((A,B))\sqcup f_{S}((C,D))$.

2. $f_{R}((A,B)\sqcap (A,B))=f_{R}((A, A^{\prime }))=(\underline{A}_{R},(\underline{A}_{R})^{\prime })= f_{R}((A,B))$. Similarly, one can show that $f_{S}((A,B)\sqcup (A,B))=((\underline{B}_{S})^{\prime }, \underline{B}_{S})$.

3. $f_{R}(\lnot \bot )=f_{R}((G,G^{\prime }))=(\underline{G}_{R},(\underline{G}_{R})^{\prime })=(G,G^{\prime })=\lnot \bot$, by Proposition 11(ii). Similarly, one gets $f_{S}(\lrcorner \top )=\lrcorner \top$.

4. $f_{R}(\lnot (A,B))=f_{R}(A^{c}, A^{c\prime })=(\underline{A^{c}}_{R}, (\underline{A^{c}}_{R})^{\prime })=((\overline{A}^{R})^{c}, (\overline{A}^{R})^{c\prime })$ by Proposition 11(i). So $f_{R}(\lnot (A, B))=\lnot (\overline{A}^{R}, (\overline{A}^{R})^{\prime } )=\lnot f_{R}^{\delta }((A, B))$. Similarly, one can show that $f_{S}(\lrcorner (A, B))=\lrcorner f_{S}^{\delta }((A, B))$. $\square$

Using Theorem 12(1,3,4), one obtains

Corollary 2

For all $x, y\in \mathfrak {P}(\mathbb {K})$,

• 1. $f_{R}^{\delta }(x\vee y)=f_{R}^{\delta }(x)\vee f_{R}^{\delta }(y)$ and $f_{S}^{\delta }(x\wedge y)=f_{S}^{\delta }(x)\wedge f_{S}^{\delta }(y)$.

• 2. $f_{R}^{\delta }(\bot )=\bot$ and $f_{S}^{\delta }(\top )=\top$.

Consider the restriction maps $f_{R}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcap }}$ and $f_{S}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcup }}$. From Theorem 12(2), it follows that $\mathfrak {P}(\mathbb {K})_{\sqcap }$ and $\mathfrak {P}(\mathbb {K})_{\sqcup }$ are closed under $f_{R}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcap }}$ and $f_{S}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcup }}$ respectively. Using Theorem 12(1,3) and Corollary 2, we get

Corollary 3

$\underline{\mathfrak {P}}({\mathbb {K}}{\mathbb {C}})^{+}_{\sqcap }:=(\mathfrak {P}(\mathbb {K})_{\sqcap }, \sqcap , \vee , \lnot , \bot , f_{R}^{\delta }\restriction {\mathfrak {P}(\mathbb {K})_{\sqcap }})$ and $\underline{\mathfrak {P}}({\mathbb {K}}{\mathbb {C}})^{+}_{\sqcup }:=(\mathfrak {P}(\mathbb {K})_{\sqcup }, \sqcup , \wedge , \lrcorner , \top , f_{S}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcup }})$ are Baos.

We next consider a Kripke context ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$ where the relations R, S satisfy certain properties that are of particular relevance here.

Definition 7

• 1. ${\mathbb {K}}{\mathbb {C}}$ is reflexive from the left, if R is reflexive.

• 2. ${\mathbb {K}}{\mathbb {C}}$ is reflexive from the right, if S is reflexive.

• 3. ${\mathbb {K}}{\mathbb {C}}$ is reflexive, if it is reflexive from both left and right.

The cases for symmetry and transitivity of ${\mathbb {K}}{\mathbb {C}}$ are similarly defined.

Observe that the Kripke context in Example 2 is symmetric from the right.

Theorem 13

Let ${\mathbb {K}}{\mathbb {C}}:= ((G,R), (M,S), I)$ be a reflexive and transitive Kripke context. Then for all $x\in \mathfrak {P}(\mathbb {K})$, the following hold.

• 1. $f_{R}(x)\sqsubseteq x$ and $x\sqsubseteq f_{S}(x)$.

• 2. $f_{R}f_{R}(x)=f_{R}(x)$ and $f_{S}f_{S}(x)=f_{S}(x)$.

Proof

1. Let $(A, B)\in \mathfrak {P}(\mathbb {K})$. By Proposition 11(v) $\underline{A}_{R}\subseteq A$ and $\underline{B}_{S}\subseteq B$, which implies that $A^{\prime }\subseteq (\underline{A}_{R})^{\prime }$ and $B^{\prime }\subseteq (\underline{B}_{S})^{\prime }$. Now $B^{\prime \prime }=A^{\prime }$ and $A^{\prime \prime }=B^{\prime }$, as $(A, B)\in \mathfrak {P}(\mathbb {K})$. By Lemma 3, $A\subseteq A^{\prime \prime }$ and $B\subseteq B^{\prime \prime }$. So $A\subseteq B^{\prime }$ and $B\subseteq A^{\prime }$, which implies that $B\subseteq (\underline{A}_{R})^{\prime }$ and $A\subseteq (\underline{B}_{S})^{\prime }$. Therefore $f_{R}((A,B))=(\underline{A}_{R},(\underline{A}_{R})^{\prime })\sqsubseteq (A,B)$ and $(A,B)\sqsubseteq f_{S}((A,B))=((\underline{B}_{S})^{\prime }, \underline{B}_{S})$.

2. $f_{R}f_{R}((A,B))=f_{R}((\underline{A}_{R},(\underline{A}_{R})^{\prime }))=(\underline{(\underline{A}_{R})}_{R}, (\underline{(\underline{A}_{R})}_{R})^{\prime })=(\underline{A}_{R},(\underline{A}_{R})^{\prime })= f_{R}((A,B))$, by Proposition 11(vi). Similarly, one can show that $f_{S}f_{S}((A,B))=f_{S}((A,B))$. $\square$

Theorems 13 and 12(4) give

Corollary 4

For all $x\in \mathfrak {P}(\mathbb {K})$, $x\sqsubseteq f_{R}^{\delta }(x)$ and $f_{R}^{\delta }f_{R}^{\delta }(x)=f_{R}^{\delta }(x)$.

Further, using Theorems 12, 13 and Corollaries 2, 4, we get

Corollary 5

$\underline{\mathfrak {P}}({\mathbb {K}}{\mathbb {C}})^{+}_{\sqcap }:=(\mathfrak {P}(\mathbb {K})_{\sqcap }, \sqcap , \vee , \lnot , \bot , f_{R}^{\delta }\restriction {\mathfrak {P}(\mathbb {K})_{\sqcap }})$ and $\underline{\mathfrak {P}}({\mathbb {K}}{\mathbb {C}})^{+}_{\sqcup }:= (\mathfrak {P}(\mathbb {K})_{\sqcup }, \sqcup , \wedge , \lrcorner , \top , f_{S}\restriction {\mathfrak {P}(\mathbb {K})_{\sqcup }})$ are topological Boolean algebras.

3.1 Complex Algebra to Concept Approximation

Recall the Kripke context ${\mathbb {K}}{\mathbb {C}}_{DS}:=((G, E_{1}), (M, E_{2}), I)$ defined in Sect. 1, where $(G, E_{1}), (M, E_{2})$ are Pawlakian approximation spaces. We observe that terms of the full complex algebra $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}_{DS})$ are able to express the various notions of concept approximations mentioned in Sect. 2.3. Indeed, for ${\mathbb {K}}{\mathbb {C}}_{DS}$, we get the operators $f_{E_{1}},f_{E_{2}}:\mathfrak {P}(\mathbb {K}) \rightarrow \mathfrak {P}(\mathbb {K})$ as above, that is, $f_{E_{1}}((A,B)):=(\underline{A}_{E_{1}},(\underline{A}_{E_{1}})^{\prime })$, and $f_{E_{2}}((A,B)):=((\underline{B}_{E_{2}})^{\prime },\underline{B}_{E_{2}})$ for any $(A,B)\in \mathfrak {P}(\mathbb {K})$. Moreover, $f_{E_{1}}^{\delta }((A,B)) = (\overline{A}^{E_{1}}, (\overline{A}^{E_{1}})^{\prime })$ and $f_{E_{2}}^{\delta }((A,B)) = ((\overline{B}^{E_{2}})^{\prime },\overline{B}^{E_{2}})$. Let $A\subseteq G$ and $B\subseteq M$.

If A and B are feasible then the concept approximations of A and B are $(A, A^{\prime })$ and $(B^{\prime }, B)$ respectively and these are elements of $\mathfrak {P}(\mathbb {K})$.

Suppose A and B are both non-feasible sets. Let $x, y\in \mathfrak {P}(\mathbb {K})$ be such that the extent of x is A and intent of y is B. Then we have the following.

The lower concept approximation of A, $((\underline{A}_{E_{1}})^{\prime \prime }, (\underline{A}_{E_{1}})^{\prime })=(\underline{A}_{E_{1}}, (\underline{A}_{E_{1}})^{\prime })\sqcup (\underline{A}_{E_{1}}, (\underline{A}_{E_{1}})^{\prime })=f_{E_{1}}(x)\sqcup f_{E_{1}}(x)$.

The upper concept approximation of A, $((\overline{A}^{E_{1}})^{\prime \prime }, (\overline{A}^{E_{1}})^{\prime })= (\overline{A}^{E_{1}}, (\overline{A}^{E_{1}})^{\prime })\sqcup (\overline{A}^{E_{1}}, (\overline{A}^{E_{1}})^{\prime })=f_{E_{1}}^{\delta }(x)\sqcup f_{E_{1}}^{\delta }(x)$.

The lower concept approximation of B, $((\overline{B}^{E_{2}})^{\prime }, (\overline{B}^{E_{2}})^{\prime \prime })=((\overline{B}^{E_{2}})^{\prime },\overline{B}^{E_{2}})\sqcap ((\overline{B}^{E_{2}})^{\prime },\overline{B}^{E_{2}})=f^{\delta }_{E_{2}}(y)\sqcap f^{\delta }_{E_{2}}(y)$.

The upper concept approximation of B, $((\underline{B}_{E_{2}})^{\prime }, (\underline{B}_{E_{2}})^{\prime \prime } )=((\underline{B}_{E_{2}})^{\prime },\underline{B}_{E_{2}})\sqcap ((\underline{B}_{E_{2}})^{\prime },\underline{B}_{E_{2}}) =f_{E_{2}}(y)\sqcap f_{E_{2}}(y)$.

Now by definition, approximations of any pair (A, B) are obtained using the concept approximations of A and B. As shown above, the latter are all expressible by the terms of the full complex algebra, and hence we have the observation. For instance, suppose, (A, B) is a non-definable concept of $\mathbb {K}$ with A and B non-feasible.

The lower approximation of (A, B), $((\underline{A}_{E_{1}})^{\prime \prime }\cap (\overline{B}^{E_{2}})^{\prime }, ((\underline{A}_{E_{1}})^{\prime \prime }\cap (\overline{B}^{E_{2}})^{\prime })^{\prime })=(f_{E_{1}}(x)\sqcup f_{E_{1}}(x))\sqcap (f^{\delta }_{E_{2}}(y)\sqcap f^{\delta }_{E_{2}}(y))=(f_{E_{1}}(x)\sqcup f_{E_{1}}(x))\sqcap f^{\delta }_{E_{2}}(y)$.

The upper approximation of (A, B), $(((\overline{A}^{E_{1}})^{\prime }\cap (\underline{B}_{E_{2}})^{\prime \prime })^{\prime }, (\overline{A}^{E_{1}})^{\prime }\cap (\underline{B}_{E_{2}})^{\prime \prime } ) =(f^{\delta }_{E_{1}}(x)\sqcup f^{\delta }_{E_{1}}(x))\sqcup (f_{E_{2}}(y)\sqcap f_{E_{2}}(y))=(f_{E_{2}}(y)\sqcap f_{E_{2}}(y))\sqcup f^{\delta }_{E_{1}}(x)$.

4 The Algebras

In this section, we study abstractions of the algebraic structure $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$ obtained in Sect. 3. These are dBas with operators (Definition 8), and topological dBas (Definition 9).

4.1 Double Boolean Algebras with Operators

Definition 8

A structure $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}},{\textbf {C}})$ is a dBa with operators (dBao) provided

1. $(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ is a dBa and

2. ${\textbf {I}},{\textbf {C}}$ are monotonic operators on D satisfying the following for any $x,y\in D$.

$\begin{array}{ll} 1a~ {\textbf {I}}(x \sqcap y) = {\textbf {I}}(x) \sqcap {\textbf {I}}(y) &{} 1b~ {\textbf {C}}(x \sqcup y) = {\textbf {C}}(x)\sqcup {\textbf {C}}(y)\\ 2a~ {\textbf {I}}(\lnot \bot )= \lnot \bot &{} 2b~{\textbf {C}}(\lrcorner \top )=\lrcorner \top \\ 3a~ {\textbf {I}}(x\sqcap x)={\textbf {I}}(x) &{} 3b~ {\textbf {C}}(x\sqcup x)={\textbf {C}}(x) \end{array}$

A contextual dBao is a dBao in which the underlying dBa is contextual. If the underlying dBa is pure, the dBao is called a pure dBao.

The duals of ${\textbf {I}}$ and ${\textbf {C}}$ with respect to $\lnot ,\lrcorner$ are defined as ${\textbf {I}}^{\delta }(a):=\lnot {\textbf {I}}(\lnot a)$ and ${\textbf {C}}^{\delta }(a):=\lrcorner {\textbf {C}}(\lrcorner a)$ for all $a\in D$.

Any Bao provides a trivial example of a contextual and pure dBao. Indeed, in a Bao $(B,\sqcap ,\sqcup ,\lnot ,\top ,\bot ,f)$, setting $\lrcorner =\lnot$, ${\textbf {C}}:=f$ and ${\textbf {I}}:=f^\delta$, one obtains the dBao $(B,\sqcap ,\sqcup ,\lnot ,\lrcorner ,\top ,\bot ,{\textbf {I}},{\textbf {C}})$. Due to the idempotence of the operators $\sqcap ,\sqcup$ in the Boolean algebra $(B,\sqcap ,\sqcup ,\lnot ,\top ,\bot )$, the dBa $(B,\sqcap ,\sqcup ,\lnot ,\lrcorner ,\top ,\bot )$ is pure; as $B_\sqcap = B_\sqcup = B$, the dBa is contextual as well.

An immediate consequence is the following.

Theorem 14

Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,{\textbf {I}},{\textbf {C}})$ be a dBao. Then

• 1. $\mathfrak {O}_{p}:=(D_{p}, \sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}}\restriction {D_{p}},{\textbf {C}}\restriction {D_{p}} )$ is the largest pure subalgebra of $\mathfrak {O}$.

• 2. If $\mathfrak {O}$ is pure, it is contextual and moreover, $\mathfrak {O}=\mathfrak {O}_{p}$.

Proof

1. From Proposition 1 it follows that $(D_{p}, \sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ is the largest pure subalgebra of ${\textbf {D}}$. To complete the proof it is sufficient to show that $D_{p}$ is closed under ${\textbf {I}}$ and ${\textbf {C}}$, which follows from Definition 8(1a, 3a, 1b, 3b).

2. Proposition 2 gives the first part. For any pure dBa, $D=D_{p}$. $\square$

As intended, the sets of protoconcepts and semiconcepts of a context provide examples of dBaos:

Theorem 15

Let ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$ be a Kripke context based on the context $\mathbb {K}:=(G,M,I)$. Then the following hold.

• 1. $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}):=(\mathfrak {P}(\mathbb {K}),\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,f_{R},f_{S})$ is a contextual dBao.

• 2. $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}):=(\mathfrak {H}(\mathbb {K}),\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,f_{R}\restriction {\mathfrak {H}(\mathbb {K})},f_{S}\restriction {\mathfrak {H}(\mathbb {K})})$ is a pure dBao. It is the largest pure subalgebra of $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$, that is, $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})_{p}=\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}})$.

Proof

1. From Theorem 7 it follows that $(\mathfrak {P}(\mathbb {K}),\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ is a dBa. To show monotonicity of $f_{R},f_{S}$, let $(A, B), (C, D)\in \mathfrak {P}(\mathbb {K})$ and $(A,B)\sqsubseteq (C,D)$. Then, by definition of $\sqsubseteq$, $A\subseteq C$ and $D\subseteq B$, and by using Proposition 11(iv), $\underline{A}_{R}\subseteq \underline{C}_{R}$, which implies $(\underline{C}_{R})^{\prime }\subseteq (\underline{A}_{R})^{\prime }$. Hence $f_{R}((A,B))\sqsubseteq f_{R}((C,D))$. Similar to the above, we can show the monotonicity of $f_{S}$. Rest of the proof follows from Theorem 12.

2. From Theorem 7, it follows that $\underline{\mathfrak {P}}(\mathbb {K})_{p}=\underline{\mathfrak {H}}(\mathbb {K})$. By Theorem 14(2), $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})_{p}=\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}})$ is the largest pure subalgebra of $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$. $\square$

The following lists some basic properties of the operators ${\textbf {I}},{\textbf {C}}$ and their duals in a dBao.

Lemma 6

Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}},{\textbf {C}})$ be a dBao. Then the following hold for any $a,x,y\in D$.

• 1. $\lnot {\textbf {I}}^{\delta }(\lnot a)= {\textbf {I}}a$ and $\lrcorner {\textbf {C}}^{\delta }(\lrcorner a)={\textbf {C}}(a)$.

• 2. ${\textbf {I}}(\lnot a)=\lnot {\textbf {I}}^{\delta }(a)$ and ${\textbf {I}}^{\delta }(\lnot a)=\lnot {\textbf {I}}(a)$.

• 3. ${\textbf {C}}(\lrcorner a)=\lrcorner {\textbf {C}}^{\delta }(a)$ and ${\textbf {C}}^{\delta }(\lrcorner a)=\lrcorner {\textbf {C}}(a)$.

• 4. ${\textbf {I}}^{\delta }$ and ${\textbf {C}}^{\delta }$ both are monotonic.

• 5. ${\textbf {I}}^{\delta }(a\sqcap a)={\textbf {I}}^{\delta }(a)$ and ${\textbf {C}}^{\delta }(a\sqcup a)={\textbf {C}}^{\delta }(a)$.

• 6. ${\textbf {I}}^{\delta }(x\vee y)={\textbf {I}}^{\delta }(x)\vee {\textbf {I}}^{\delta }(y)$ and ${\textbf {C}}^{\delta }(x\wedge y)={\textbf {C}}^{\delta }(x)\wedge {\textbf {C}}^{\delta }(y)$.

• 7. ${\textbf {I}}^{\delta }(\bot )=\bot$ and ${\textbf {C}}^{\delta }(\top )=\top$.

• 8. ${\textbf {I}}^{\delta }(x)\sqcap {\textbf {I}}^{\delta }(x)={\textbf {I}}^{\delta }(x)$ and ${\textbf {C}}^{\delta }(x)\sqcup {\textbf {C}}^{\delta }(x)={\textbf {C}}^{\delta }(x)$.

Proof

The proof is obtained in a straightforward manner. We use 1, 2, 3 and 5 of Proposition 5, (8a), (8b) of Definition 2 and 3a, 3b of Definition 8. $\square$

We noted earlier that a Bao provides an example of a dBao. The converse question is addressed in Theorems 16 and 17 below.

Theorem 16

Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,{\textbf {I}},{\textbf {C}})$ be a dBao such that for all $a\in D$ $\lnot a=\lrcorner a$, $\lnot \lnot a=a$. Then $(D,\sqcup ,\sqcap ,\lnot ,\top ,\bot ,{\textbf {C}})$ and $(D,\sqcup ,\sqcap ,\lnot ,\top ,\bot ,{\textbf {I}}^{\delta })$ are Baos.

Proof

That $(D,\sqcup ,\sqcap ,\lnot ,\top ,\bot )$ forms a Boolean algebra is not difficult to prove, and the proof is given in the “Appendix”. In particular, one can show that $y\sqcup z=y\vee z$ and $y\sqcap z=y\wedge z$ for any $y,z \in D$. It is then easy to verify that ${\textbf {C}}$ and ${\textbf {I}}^{\delta }$ are additive and normal. Indeed, Definition 8(1b) implies that ${\textbf {C}}$ is additive. As $\lrcorner \top = \bot$, by Definition 8(3b), it is normal. On the other hand, as $y\sqcup z=y\vee z$ for all $y,z \in D$, from Lemma 6(6) it follows that ${\textbf {I}}^{\delta }(x\sqcup y)={\textbf {I}}^{\delta }(x\vee y)={\textbf {I}}^{\delta }(x)\vee {\textbf {I}}^{\delta }(y)={\textbf {I}}^{\delta }(x)\sqcup {\textbf {I}}^{\delta }(y)$. ${\textbf {I}}^{\delta }(\bot )=\bot$ by Lemma 6(7). $\square$

Theorem 17

Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}},{\textbf {C}})$ be a dBao. Then $\mathfrak {O}_{\sqcap }:=(D_{\sqcap },\sqcap ,\vee ,\lnot ,\bot , {\textbf {I}}^{\delta }\restriction {D_{\sqcap }})$ and $\mathfrak {O}_{\sqcup }:=(D_{\sqcup },\sqcup ,\wedge ,\lrcorner ,\top , {\textbf {C}}\restriction {D_{\sqcup }})$ are Baos.

Proof

By Proposition 3, ${\textbf {D}}_{\sqcap }$ and ${\textbf {D}}_{\sqcup }$ are Boolean algebras. Let $x\in D_{\sqcap }$. Then ${\textbf {I}}^{\delta }\restriction {D_{\sqcap }}(x)\sqcap {\textbf {I}}^{\delta }\restriction {D_{\sqcap }}(x)={\textbf {I}}^{\delta }(x)\sqcap {\textbf {I}}^{\delta }(x)={\textbf {I}}^{\delta }(x)={\textbf {I}}^{\delta }\restriction {D_{\sqcap }}(x)$, by Lemma 6(8). So $D_{\sqcap }$ is closed under ${\textbf {I}}^{\delta }\restriction {D_{\sqcap }}$. Similarly, $D_{\sqcup }$ is closed under ${\textbf {C}}\restriction {D_{\sqcup }}$. That both ${\textbf {I}}^{\delta }\restriction {D_{\sqcap }}$ and ${\textbf {C}}\restriction {D_{\sqcup }}$ are additive and normal follows from Lemma 6(6,7) and Definition 8. $\square$

The following result addresses the converse of Theorem 17.

Theorem 18

Let ${\textbf {D}}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot ,)$ be a dBa such that $\mathfrak {O}_{\sqcap }:=(D_{\sqcap },\sqcap ,\vee ,\lnot ,\bot , \overline{{\textbf {I}}})$ and $\mathfrak {O}_{\sqcup }:=(D_{\sqcup },\sqcup ,\wedge ,\lrcorner ,\top , \overline{{\textbf {C}}})$ are Baos. Then $\mathfrak {O}:= (D,\sqcup ,\sqcap , \lnot ,\lrcorner ,\top ,\bot , {\textbf {I}},{\textbf {C}})$ is a dBao, where ${\textbf {I}}(x):=\lnot \overline{{\textbf {I}}}(\lnot x)$ and ${\textbf {C}}(x):= \overline{{\textbf {C}}}(x\sqcup x)$ for all $x\in D$.

Proof

Let $x,y\in D$. Using Proposition 5(6), ${\textbf {I}}(x\sqcap y)=\lnot \overline{{\textbf {I}}}(\lnot (x\sqcap y))=\lnot \overline{{\textbf {I}}}(\lnot x \vee \lnot y)=\lnot (\overline{{\textbf {I}}}(\lnot x)\vee \overline{{\textbf {I}}}(\lnot y))$, as $\lnot x,\lnot y\in D_{\sqcap }$ by Proposition 5(1). As $\overline{{\textbf {I}}}(\lnot x), \overline{{\textbf {I}}}(\lnot y) \in D_{\sqcap }$, using definition of $\vee$ we have ${\textbf {I}}(x\sqcap y)=\lnot \overline{{\textbf {I}}}(\lnot x)\sqcap \lnot \overline{{\textbf {I}}}(\lnot y)={\textbf {I}}(x)\sqcap {\textbf {I}}(y)$. Using Proposition 5(5), ${\textbf {I}}(\lnot \bot )=\lnot \overline{{\textbf {I}}} (\lnot \lnot \bot )=\lnot \overline{{\textbf {I}}}(\bot )=\lnot \bot$. By Definition 2(4a), ${\textbf {I}}(x\sqcap x)=\lnot \overline{{\textbf {I}}}(\lnot (x\sqcap x))=\lnot \overline{{\textbf {I}}}(\lnot x)={\textbf {I}}(x)$.

${\textbf {C}}(\lrcorner \top )=\overline{{\textbf {C}}}(\lrcorner \top \sqcup \lrcorner \top )=\overline{{\textbf {C}}}(\lrcorner \top )=\lrcorner \top$, as $\top \in D_{\sqcup }$. That ${\textbf {C}}(x\sqcup x)= {\textbf {C}}(x)$ is immediate from Definition 2. Finally, one shows that ${\textbf {C}}(x\sqcup y)={\textbf {C}}(x)\sqcup {\textbf {C}}(y)$ for all $x, y\in D$. Let $x, y\in D$. Using commutativity and associativity of $\sqcup$ and Definition 2(1b), additivity of $\overline{{\textbf {C}}}$ and the fact that $x\sqcup x, y \sqcup y \in D_{\sqcup }$, we have the following equalities. ${\textbf {C}}(x\sqcup y)=\overline{{\textbf {C}}}((x\sqcup y)\sqcup (x\sqcup y))=\overline{{\textbf {C}}}((x\sqcup x)\sqcup (y\sqcup y))=\overline{{\textbf {C}}}(x\sqcup x)\sqcup \overline{{\textbf {C}}}(y\sqcup y)={\textbf {C}}(x)\sqcup {\textbf {C}}(y)$. So $\mathfrak {O}$ is a dBao. $\square$

We end this part by noting a close connection between the full complex algebra of a Kripke frame and that of a corresponding Kripke context. Let (W, R) be a Kripke frame and $\mathfrak {F}^{+}:=(\mathcal {P}(W),\cap ,\cup ,^c,W,\emptyset ,m_{R})$ be the full complex algebra (Blackburn et al., 2001), where for all $A\in \mathcal {P}(W)$, $m_{R}(A):=\{w\in W:R(w)\cap A\ne \emptyset \}=\overline{A}^{R}$. This is a Bao, and as observed earlier, yields the dBao $(\mathcal {P}(W),\cap ,\cup ,^c,W,\emptyset ,m^{\delta }_{R}, m_{R} )$. For the Kripke frame (W, R), let us define the Kripke context ${\mathbb {K}}{\mathbb {C}}_{0}:=((W,R),(W,R),\ne )$. By Definition 6, we have the full complex algebra of ${\mathbb {K}}{\mathbb {C}}_{0}$ as $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}_{0}):=(\mathfrak {P}(\mathbb {K}), \sqcup ,\sqcap , \lnot , \lrcorner , \top ,\bot , f_{1}, f_{2})$, where $f_{1}((A, B)):=(\underline{A}_{R}, (\underline{A}_{R})^{\prime })$, $f_{2}((A, B)):=((\underline{B}_{R})^{\prime }, \underline{B}_{R})$ for all $(A,B)\in \mathfrak {P}(\mathbb {K})$. Then we get

Theorem 19

For the full complex algebra $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}_{0})$, the following hold.

• 1. $\lnot x=\lrcorner x$, $\lnot \lnot x=x$ and $f_{1}(x)=\lnot f_{2}(\lnot x)$ for all $x\in \mathfrak {P}(\mathbb {K})$.

• 2. $(\mathfrak {P}(\mathbb {K}), \sqcup ,\sqcap , \lnot , \top ,\bot , f_{2})$ is a Bao, which is isomorphic to $\mathfrak {F}^{+}$.

Proof

1. Let $A\subseteq W$ and $x\in A^{c}$. Then for all $a\in A$, $x\ne a$, which implies that $x\in A^{\prime }$. Now let $x\in A^{\prime }$. Then $x\ne a$, for all $a\in A$, which implies that $x\in A^{c}$. So $A^{\prime }=A^{c}$, and $A^{\prime \prime }=A^{c\prime }=A^{cc}=A$. Therefore $(A,B)\in \mathfrak {P}(\mathbb {K})$ if and only if $A=B^{c}$, which is equivalent to $A^{c}=B$.

Let $(A,A^{c})\in \mathfrak {P}(\mathbb {K})$. Then $\lnot (A,A^{c})=(A^{c},A)=\lrcorner (A,A^{c})$ and $\lnot \lnot (A,A^{c})=(A,A^{c})$. $f_{2}((A,A^{c})):=(\underline{(A^{c})}_{R}^{\prime },\underline{(A^{c})}_{R})$, giving

$\lnot f_{2}(\lnot (A,A^{c}))= \lnot f_{2}((A^{c},A))=\lnot ((\underline{A}_{R})^{\prime },\underline{A}_{R})= ((\underline{A}_{R})^{\prime c}, (\underline{A}_{R})^{\prime c \prime })=(\underline{A}_{R}, (\underline{A}_{R})^{\prime })$.

So $f_{1}((A,A^{c}))=(\underline{A}_{R},(\underline{A}_{R})^{\prime })=\lnot f_{2}(\lnot (A,A^{c}))$.

2. By Theorem 16 it follows that $(\mathfrak {P}(\mathbb {K}), \sqcup ,\sqcap , \lnot , \top ,\bot , f_{2})$ is a Bao.

Let us define a map f from $\mathcal {P}(W)$ to $\mathfrak {P}(\mathbb {K})$ by $f(A):=(A,A^{c})$ for all $A\subseteq W$. It is clear that f is well-defined. To show f is a homomorphism, let $A,B\subseteq W$. $f(A\cap B)=(A\cap B, (A\cap B)^{c})=(A,A^{c})\sqcap (B,B^{c})=f(A)\sqcap f(B)$ and $f(A\cup B)=(A\cup B, (A\cup B)^{c})=(A,A^{c})\sqcup (B,B^{c})=f(A)\sqcup f(B)$. $f(A^{c})=(A^{c}, A)=\lnot f(A)=\lrcorner f(A)$ and $f(W)=(W,\emptyset )=\top$ $f(\emptyset )=(\emptyset , W)=\bot$. $f(m_{R}(A))=(\overline{A}^{R}, (\overline{A}^{R})^{c})=((\underline{A^{c}}_{_{R}})^{c},\underline{A^{c}}_{_{R}})=f_{2}((A,A^{c}))=f_{2}(f(A))$.

Injectivity and surjectivity of f follow trivially. $\square$

From Theorem 19, we may conclude that the dBao $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}_{0})$ is identifiable with the Bao $\mathfrak {F}^{+}$.

4.1.1 Representation Theorems for dBaos

For every dBao $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}}, {\textbf {C}})$, we construct a Kripke context based on the standard context $\mathbb {K}({\textbf {D}}):=(\mathcal {F}_{p}({\textbf {D}}),\mathcal {I}_{p}({\textbf {D}}), \Delta )$ corresponding to the underlying dBa D. For that, relations R and S are defined on $\mathcal {F}_{p}({\textbf {D}})$ and $\mathcal {I}_{p}({\textbf {D}})$ respectively as follows.

For all $u,u_{1}\in \mathcal {F}_{p}({\textbf {D}})$, $uRu_{1}$ if and only if ${\textbf {I}}^{\delta }(a)\in u$ for all $a\in u_{1}$.

For all $v,v_{1}\in \mathcal {I}_{p}({\textbf {D}})$, $vSv_{1}$ if and only if ${\textbf {C}}^{\delta }(a)\in v$ for all $a\in v_{1}$.

The following results are required to get (Representation) Theorem 20.

Lemma 7

If F is a primary filter (ideal) of a dBa D, then for any $x\in D$, exactly one of the elements x and $\lnot x$ belongs to F.

Proof

Proof follows from the definition of a primary filter (ideal).

Lemma 8

Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}}, {\textbf {C}})$ be a dBao. The following hold.

• 1. For all $u,u_{1}\in \mathcal {F}_{p}({\textbf {D}})$, $uRu_{1}$ if and only if for all $a\in D$, ${\textbf {I}}a\in u$ implies that $a\in u_{1}$.

• 2. For all $v,v_{1}\in \mathcal {I}_{p}({\textbf {D}})$, $vSv_{1}$ if and only if for all $a\in D$, ${\textbf {C}}a\in v$ implies that $a\in v_{1}$.

Proof

1. For all $a\in D$, suppose ${\textbf {I}}a\in u$ implies that $a\in u_{1}$. If possible, assume . Then there exists $a_{1}\in u_{1}$ such that ${\textbf {I}}^{\delta }(a_{1})\notin u$. So $\lnot {\textbf {I}}^{\delta }(a_{1})\in u$, which implies that ${\textbf {I}}(\lnot a_{1})\in u$ by Lemma 6(2). As $a_{1}\in u_{1}$, $\lnot a_{1}\notin u_{1}$, which contradicts that ${\textbf {I}}(\lnot a_{1})\in u$. Hence $uRu_{1}$.

Now, we assume that $uRu_{1}$ and let $a_{1}\in D$ such that ${\textbf {I}}a_{1}\in u$. If possible, suppose $a_{1}\notin u_{1}$. Then $\lnot a_{1}\in u_{1}$. So ${\textbf {I}}^{\delta }(\lnot a_{1})\in u$ as $uRu_{1}$. Therefore by Lemma 6, ${\textbf {I}}^{\delta }(\lnot a_{1})=\lnot {\textbf {I}}(a_{1})\in u$, which is a contradiction by Lemma 7. Hence $a_{1}\in u_{1}$.

Proof of 2 is similar to the above. $\square$

Lemma 9

Let ${\textbf {D}}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ be a dBa. For all $a,b\in D$, the following hold.

• 1. If $a\sqcap b=\bot$ then $a\sqcap a\sqsubseteq \lnot b$.

• 2. If $a\sqcap a\sqsubseteq \lnot b$ then $a\sqcap b\sqsubseteq \bot$.

• 3. If $a\sqcup b=\top$ then $\lrcorner b\sqsubseteq a\sqcup a$.

• 4. If $\lrcorner b\sqsubseteq a\sqcup a$ then $\top \sqsubseteq a\sqcup b$.

In particular, if ${\textbf {D}}$ is a contextual dBa then $a\sqcap b=\bot$ if and only if $a\sqcap a\sqsubseteq \lnot b$, and $a\sqcup b=\top$ if and only if $\lrcorner b\sqsubseteq a\sqcup a$.

Proof

1. Let $a,b\in D$ and $a\sqcap b=\bot$. Then by Definition 2(1a) and the associative law, $\bot = (a\sqcap a)\sqcap (b\sqcap b)$. So $\bot \vee \lnot (b\sqcap b)=((a\sqcap a)\sqcap (b\sqcap b))\vee \lnot (b\sqcap b)$. By Definition 2(6a), $\bot \vee \lnot (b\sqcap b)=((a\sqcap a)\vee \lnot (b\sqcap b))\sqcap ((b\sqcap b)\vee \lnot (b\sqcap b))$. Now $(a\sqcap a)\vee \lnot (b\sqcap b)=\lnot (\lnot (a\sqcap a)\sqcap \lnot \lnot (b\sqcap b))=\lnot (\lnot a\sqcap (b\sqcap b))$ by Definition 2(4a) and Proposition 5(3). So $(a\sqcap a)\vee \lnot (b\sqcap b)=\lnot (\lnot a\sqcap b)$ by Definition 2(1a). Similarly, we can show that $\bot \vee \lnot (b\sqcap b )=\lnot (b\sqcap \lnot \bot )$. Therefore $\bot \vee \lnot (b\sqcap b )=\lnot (b\sqcap \lnot \bot )=\lnot (b\sqcap (\top \sqcap \top ))$ by Definition 2(10a). Using Definition 2(1a) and Proposition 4(2), $\bot \vee \lnot (b\sqcap b )=\lnot (b\sqcap \top )=\lnot (b\sqcap b)=\lnot b$, where the last equality follows from Definition 2(4a). This implies that $\lnot b=\lnot (\lnot a\sqcap b)\sqcap \lnot \bot =\lnot (\lnot a\sqcap b)$, as $\lnot (\lnot a\sqcap b),b\sqcap b, \lnot \bot \in D_{\sqcap }$. $\lnot \lnot a\sqsubseteq \lnot (\lnot a\sqcap b)$, as $\lnot a\sqcap b\sqsubseteq \lnot a$. So $a\sqcap a\sqsubseteq \lnot (\lnot a\sqcap b)=\lnot b$.

2. Let $a\sqcap a\sqsubseteq \lnot b$. Then $a\sqcap a\sqcap b\sqsubseteq \lnot b\sqcap b$ by Proposition 4(6) and by Definition 2(1a), $a\sqcap b\sqsubseteq \bot$.

Now if ${\textbf {D}}$ is a contextual dBa then $\sqsubseteq$ becomes a partial order. Therefore from the above it follows that $a\sqcap b=\bot$ if and only if $a\sqcap a\sqsubseteq \lnot b$.

The other parts can be proved dually. $\square$

Lemma 10

Let $\mathfrak {O}$ be a dBao and ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O}):=((\mathcal {F}_{p}({\textbf {D}}),R), (\mathcal {I}_{p}({\textbf {D}}),S),\Delta )$. Then for all $a\in D$ the following hold.

• 1. $\overline{F_{a}}^{R}=F_{{\textbf {I}}^{\delta }(a)}$ and $\underline{F_{a}}_{R}=F_{{\textbf {I}}(a)}$.

• 2. $\overline{I_{a}}^{S}=I_{{\textbf {C}}^{\delta }(a)}$ and $\underline{I_{a}}_{S}=I_{{\textbf {C}}(a)}$.

Proof

1. Let $F\in \overline{F_{a}}^{R}$. Then there exists $F_{1}\in F_{a}$ such that $FRF_{1}$, which implies that ${\textbf {I}}^{\delta }(a)\in F$, as $a\in F_{1}$. So $\overline{F_{a}}^{R}\subseteq F_{{\textbf {I}}^{\delta }(a)}$.

Let $F\in F_{{\textbf {I}}^{\delta }(a)}$ and we show that $F\in \overline{F_{a}}^{R}$. We must then find a primary filter $F_{1}\in F_{a}$ such that $FRF_{1}$. Let $F_{0}:=\{x\in D: {\textbf {I}}x\in F\}$ and $F_{01}:=\{x\sqcap a: x\in F_{0}\}$. Then $F_{01}$ is closed under $\sqcap$ and $F_{01}\subseteq D_{\sqcap }$. Next we show that $\bot \notin F_{01}$. If possible, suppose $\bot \in F_{01}$. Then there exists $x_{1}\in F_{0}$ such that $x_{1}\sqcap a=\bot$, which implies that $a\sqcap a\sqsubseteq \lnot x_{1}$ by Lemma 9(1). So ${\textbf {I}}^{\delta }(a\sqcap a)\sqsubseteq {\textbf {I}}^{\delta }(\lnot x_{1})$, whence ${\textbf {I}}^{\delta }(a)\sqsubseteq {\textbf {I}}^{\delta }(\lnot x_{1})$ by Lemma 6(4,5). ${\textbf {I}}^{\delta }(\lnot x_{1})\in F$, as ${\textbf {I}}^{\delta }(a)\in F$ and F is a filter, which implies that $\lnot {\textbf {I}}( x_{1})\in F$. So ${\textbf {I}}(x_{1})\notin F$ which contradicts that $x_{1}\in F_{0}$. Therefore $\bot \notin F_{01}$. Since ${\textbf {D}}_{\sqcap }$ is a Boolean algebra and $F_{01}\subseteq D_{\sqcap }$, there exists a prime filter $F_{2}$ containing $F_{01}$. So $F_{3}:=\{x\in D: y\sqsubseteq x~\text{ for } \text{ some }~ y\in F_{2}\}$ is a primary filter containing $F_{2}$ by Lemma 2 and Proposition 6. For all $x\in F_{0}$, $x\sqcap a\in F_{01}\subseteq F_{2}$ and $x\sqcap a\sqsubseteq x, x\sqcap a\sqsubseteq a$, which implies that $F_{0}\subseteq F_{3}$ and $a\in F_{3}$. By Lemma 8(1) it follows that $FRF_{3}$. Therefore $F\in \overline{F_{a}}^{R}$.

Using Proposition 11(i), Lemmas 4 and 6(1), we get

$\underline{F_{a}}_{R}=(\overline{(F_{a}^{c})}^{R})^{c}=(\overline{(F_{\lnot a})}^{R})^{c}=F_{{\textbf {I}}^{\delta }(\lnot a)}^{c}=F_{\lnot {\textbf {I}}^{\delta }(\lnot a) }= F_{{\textbf {I}}(a)}$.

2 can be proved dually. $\square$

The Kripke context ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$ of Lemma 10 is used to obtain the representation theorem.

Theorem 20

(Representation theorem) Let $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot , {\textbf {I}}, {\textbf {C}})$ be a dBao. The following hold.

• 1. $\mathfrak {O}$ is quasi-embeddable into the full complex algebra $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of the Kripke context ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$. $h:D\rightarrow \mathfrak {P}(\mathbb {K}({\textbf {D}}))$ defined by $h(x):=(F_{x},I_{x})$ for all $x \in D$, is the required quasi-embedding.

• 2. If $\mathfrak {O}$ is a contextual dBao then the quasi-embedding h is an embedding.

• 3. $\mathfrak {O}_{p}$ is embeddable into the largest pure subalgebra $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$.

Proof

1. Let ${\textbf {D}}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top ,\bot )$ be the underlying dBa. By Theorem 9, we know that the map $h:D\rightarrow \mathfrak {P}(\mathbb {K}({\textbf {D}}))$ defined by $h(x):=(F_{x},I_{x})$ for all $x \in D$ is a quasi-embedding. To show h is a dBao homomorphism, we prove that for any $x \in D$, $h({\textbf {I}}x)=f_{R}(h(x))$ and $h({\textbf {C}}x)=f_{S}(h(x))$, that is, $(F_{{\textbf {I}}x}, I_{{\textbf {I}}x})=(\underline{F_{x}}_{R},(\underline{F_{x}}_{R})^{\prime })$ and $(F_{{\textbf {C}}x}, I_{{\textbf {C}}x})=((\underline{I_{x}}_{S})^{\prime }, \underline{I_{x}}_{S})$. By Lemma 10(1), $\underline{F_{x}}_{R}=F_{{\textbf {I}}x}$. By Lemma 5, $F_{{\textbf {I}}x}^{\prime }=I_{{\textbf {I}}x_{\sqcap \sqcup }}=I_{({\textbf {I}}x\sqcap {\textbf {I}}x)\sqcup ({\textbf {I}}x\sqcap {\textbf {I}}x)}=I_{{\textbf {I}}x\sqcup {\textbf {I}}x}=I_{{\textbf {I}}x}$, the last two equalities hold, as ${\textbf {I}}x\sqcap {\textbf {I}}x={\textbf {I}}(x\sqcap x)={\textbf {I}}x$ and by Lemma 4(1). So $(\underline{F_{x}}_{R})^{\prime }=I_{{\textbf {I}}x}$.

Similar to the above, using Lemma 10(2) and Lemma 5, we can show that $(F_{{\textbf {C}}x}, I_{{\textbf {C}}x})=((\underline{I_{x}}_{S})^{\prime }, \underline{I_{x}}_{S})$. Hence h is the required quasi-embedding from the dBao $\mathfrak {O}$ into $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ .

2. Since $\mathfrak {O}$ is contextual, the quasi-order is a partial order. As a result, h becomes injective.

3. Let $x\in D_{p}$. Then either $x\sqcap x=x$ or $x\sqcup x=x$. If $x\sqcap x=x$, $h(x)=(F_{x}, I_{x})= (F_{x}, F_{x}^{\prime })$, by Lemmas 4 and 5. Now if $x\sqcup x=x$, $h(x)=(F_{x}, I_{x})= (I_{x}^{\prime }, I_{x})$, by Lemmas 4 and 5. So $h\restriction {D_{p}}$ is an injective dBao homomorphism from $\mathfrak {O}_{p}$ to $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$, as $\mathfrak {O}_{p}$ is pure and by Proposition 2. $\square$

Corollary 6

Let $\mathfrak {O}$ be a pure dBao. Then $\mathfrak {O}$ is embeddable into the complex algebra $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of the Kripke context ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$.

Proof

Proof follows from Theorems 14(2) and 20(3). $\square$

4.2 Topological Double Boolean Algebras

Definition 9

A dBao $\mathfrak {O}:=(D,\sqcap ,\sqcup ,\lnot ,\lrcorner ,\top ,\bot ,{\textbf {I}},{\textbf {C}})$ is called a topological dBa if the following hold.

$\begin{array}{ll} 4a~ {\textbf {I}}(x) \sqsubseteq x &{} 4b~ x\sqsubseteq {\textbf {C}}(x ) \\ 5a~ {\textbf {I}}{} {\textbf {I}}(x)= {\textbf {I}}(x)&{} 5b~ {\textbf {C}}{} {\textbf {C}}(x)={\textbf {C}}(x) \end{array}$

A topological contextual dBa is a topological dBa in which the underlying dBa is contextual. If the underlying dBa is pure, the topological dBa is called a topological pure dBa.

Again, as intended, we obtain a class of examples of topological dBas from the sets of protoconcepts and semiconcepts of contexts.

Theorem 21

Let ${\mathbb {K}}{\mathbb {C}}:=((G,R),(M,S),I)$ be a reflexive and transitive Kripke context. Then the following hold.

• 1. $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$ is a topological contextual dBa.

• 2. $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})_{p}=\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}})$ is a topological pure dBa.

Proof

1. Proof follows from Theorems 15 and 13.

2. Proof is similar to the proof of Theorem 15(2). $\square$

Now, we will show that for a topological dBa $\mathfrak {O}$, ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$ is a reflexive and transitive Kripke context. For that, we first prove the following lemma.

Lemma 11

Let $\mathfrak {D}$ be a topological dBa. Then for all $a\in D$, ${\textbf {I}}^{\delta }{} {\textbf {I}}^{\delta }(a)={\textbf {I}}^{\delta }(a)$ and ${\textbf {C}}^{\delta }{} {\textbf {C}}^{\delta }(a)={\textbf {C}}^{\delta }(a)$.

Proof

Let $a\in D$. By Definition 9(5a), ${\textbf {I}}{} {\textbf {I}}(\lnot a)={\textbf {I}}(\lnot a)$, which implies that $\lnot {\textbf {I}}{} {\textbf {I}}(\lnot a)=\lnot {\textbf {I}}(\lnot a)$. By Lemma 6(2), ${\textbf {I}}^{\delta }(\lnot {\textbf {I}}\lnot a)={\textbf {I}}^{\delta }(a)$, whence ${\textbf {I}}^{\delta }{} {\textbf {I}}^{\delta }(a)={\textbf {I}}^{\delta }(a)$. Similarly, we can show that ${\textbf {C}}^{\delta }{} {\textbf {C}}^{\delta }(a)={\textbf {C}}^{\delta }(a)$. $\square$

We now have

Theorem 22

${\mathbb {K}}{\mathbb {C}}(\mathfrak {O}):=((\mathcal {F}_{p}({\textbf {D}}), R), (\mathcal {I}_{p}({\textbf {D}}), S), \Delta )$ is a reflexive and transitive Kripke context.

Proof

To show R is reflexive, let $F\in \mathcal {F}_{p}({\textbf {D}})$ and ${\textbf {I}}a\in F$ for some $a\in D$. By Definition 9(4a), ${\textbf {I}}a\sqsubseteq a$, which implies that $a\in F$, as F is a filter. So FRF by Lemma 8.

To show R is transitive, let $F,F_{1}, F_{2}\in \mathcal {F}_{p}(\mathfrak {O})$ such that $FRF_{1}$ and $F_{1}RF_{2}$. We show that $FRF_{2}$. Let $a\in F_{2}$. Then ${\textbf {I}}^{\delta }(a)\in F_{1}$, as $F_{1}RF_{2}$, which implies that ${\textbf {I}}^{\delta }{} {\textbf {I}}^{\delta }(a)\in F$, as $FRF_{1}$. So ${\textbf {I}}^{\delta }(a)={\textbf {I}}^{\delta }{} {\textbf {I}}^{\delta }(a)\in F$, using Lemma 11. Thus $FRF_{2}$.

Similarly, one can show that S is reflexive and transitive. $\square$

Combining Theorem 20, Corollary 6 and Theorem 22, we get the representation results for topological dBas in terms of reflexive and transitive Kripke contexts.

Theorem 23

A topological dBa $\mathfrak {O}$ is quasi-embeddable into the full complex algebra $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of the reflexive and transitive Kripke context ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$.

$\mathfrak {O}_{p}$ is embeddable into the complex algebra $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$. Moreover,

• 1. If $\mathfrak {O}$ is a topological contextual dBa then $\mathfrak {O}$ is embeddable into $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$.

• 2. If $\mathfrak {O}$ is a topological pure dBa then $\mathfrak {O}$ is embeddable into the complex algebra $\underline{\mathfrak {H}}^{+}({\mathbb {K}}{\mathbb {C}}(\mathfrak {O}))$ of ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$.

5 Logics Corresponding to the Algebras

We next formulate the logic CDBL for contextual dBas. The logic MCDBL for the class of contextual dBaos, and its extension MCDBL4 for topological contextual dBas are both defined with CDBL as their base. In Sect. 5.3, it is shown that, apart from the algebraic semantics, the logics can be imparted a protoconcept-based semantics, due to the representation theorems for the respective classes of algebras obtained in Sects. 4.

5.1 CDBL

The language $\mathfrak {L}$ of CDBL consists of a countably infinite set PV of propositional variables, propositional constants $\bot ,\top$, and logical connectives $\sqcup ,\sqcap ,\lnot ,\lrcorner$. The set $\mathfrak {F}$ of formulae is given by the following scheme:

$$\begin{aligned} \top \mid \bot \mid p \mid \alpha \sqcup \beta \mid \alpha \sqcap \beta \mid \lnot \alpha \mid \lrcorner \alpha , \end{aligned}$$

where $p\in {\textbf {PV}}$. $\vee$ and $\wedge$ are definable connectives: $\alpha \vee \beta :=\lnot (\lnot \alpha \sqcap \lnot \beta )$ and $\alpha \wedge \beta :=\lrcorner (\lrcorner \alpha \sqcup \lrcorner \beta )$ for all $\alpha ,\beta \in \mathfrak {F}$. A sequent in CDBL is a pair of formulae denoted by $\alpha \vdash \beta$ for $\alpha ,\beta \in \mathfrak {F}$. If $\alpha \vdash \beta$ and $\beta \vdash \alpha$, we use the abbreviation $\alpha \dashv \vdash \beta$.

The axioms of ${\textbf {CDBL}}$ are given by the following schema.

1 $\alpha \vdash \alpha$.

Axioms for $\sqcap$ and $\sqcup$:

$\begin{array}{ll} 2a~ \alpha \sqcap \beta \vdash \alpha &{} 2b~ \alpha \vdash \alpha \sqcup \beta \\ 3a~ \alpha \sqcap \beta \vdash \beta &{} 3b~ \beta \vdash \alpha \sqcup \beta \\ 4a~ \alpha \sqcap \beta \vdash (\alpha \sqcap \beta )\sqcap (\alpha \sqcap \beta ) &{} 4b~ (\alpha \sqcup \beta )\sqcup (\alpha \sqcup \beta )\vdash \alpha \sqcup \beta \end{array}$

Axioms for $\lnot$ and $\lrcorner$:

$\begin{array}{ll} 5a~\lnot (\alpha \sqcap \alpha )\vdash \lnot \alpha &{} 5b~\lrcorner \alpha \vdash \lrcorner (\alpha \sqcup \alpha )\\ 6a~\alpha \sqcap \lnot \alpha \vdash \bot &{} 6b~\top \vdash \alpha \sqcup \lrcorner \alpha \\ 7a~\lnot \lnot (\alpha \sqcap \beta )\dashv \vdash (\alpha \sqcap \beta )&{} 7b~\lrcorner \lrcorner (\alpha \sqcup \beta )\dashv \vdash (\alpha \sqcup \beta ) \end{array}$

Generalization of the law of absorption:

$\begin{array}{ll} 8a~\alpha \sqcap \alpha \vdash \alpha \sqcap (\alpha \sqcup \beta )&{} 8b~\alpha \sqcup (\alpha \sqcap \beta )\vdash \alpha \sqcup \alpha \\ 9a~\alpha \sqcap \alpha \vdash \alpha \sqcap (\alpha \vee \beta )&{} 9b~\alpha \sqcup (\alpha \wedge \beta )\vdash \alpha \sqcup \alpha \\ \end{array}$

Laws of distribution:

$\begin{array}{ll} 10a~\alpha \sqcap (\beta \vee \gamma )\dashv \vdash (\alpha \sqcap \beta )\vee (\alpha \sqcap \gamma ) &{} 10b~\alpha \sqcup (\beta \wedge \gamma )\dashv \vdash (\alpha \sqcup \beta )\wedge (\alpha \sqcup \gamma )\\ \end{array}$

Axioms for $\bot ,\top$:

$\begin{array}{ll} 11a~ \bot \vdash \alpha &{} 11b~ \alpha \vdash \top \\ 12a~\lnot \top \vdash \bot &{} 12b~\top \vdash \lrcorner \bot \\ 13a~\lnot \bot \dashv \vdash \top \sqcap \top &{} 13b~\lrcorner \top \dashv \vdash \bot \sqcup \bot \\ \end{array}$

The compatibility axiom:

14 $(\alpha \sqcup \alpha )\sqcap (\alpha \sqcup \alpha )\dashv \vdash (\alpha \sqcap \alpha )\sqcup (\alpha \sqcap \alpha )$

Rules of inference of CDBL are as follows.

For $\sqcap$ and $\sqcup$:

For $\lnot , \lrcorner$:

Transitivity:

Order:

(R5) captures the order relation of the contextual dBas.

Derivability is defined in the standard manner: a sequent S is derivable (or provable) in CDBL, if there exists a finite sequence of sequents $S_{1},\ldots , S_{m}$ such that $S_{m}$ is the sequent S and for all $k \in \{1,\ldots ,m\}$ either $S_{k}$ is an axiom or $S_{k}$ is obtained by applying rules of CDBL to elements from $\{S_{1} ,\ldots , S_{k-1}\}$. Let us give a few examples of derived rules and sequents.

Proposition 24

The following rules are derivable in CDBL.

Proof

(R6) is derived using $(R1), (R1)^{\prime }$ and (R4), while for (R7) one uses $(R2), (R2)^{\prime }$ and (R4). $\square$

Theorem 25

For $\alpha ,\beta ,\gamma \in \mathfrak {F}$, the following are provable in CDBL.

$\begin{array}{ll} 1a~ (\alpha \sqcap \beta )\dashv \vdash (\beta \sqcap \alpha ).&{} 1b~ \alpha \sqcup \beta \dashv \vdash \beta \sqcup \alpha .\\ 2a~ \alpha \sqcap (\beta \sqcap \gamma )\dashv \vdash (\alpha \sqcap \beta )\sqcap \gamma .&{} 2b~ \alpha \sqcup (\beta \sqcup \gamma )\dashv \vdash (\alpha \sqcup \beta )\sqcup \gamma .\\ 3a~ (\alpha \sqcap \alpha )\sqcap \beta \dashv \vdash (\alpha \sqcap \beta ).&{} 3b~ (\alpha \sqcup \alpha )\sqcup \beta \dashv \vdash \alpha \sqcup \beta .\\ 4a~ \lnot \alpha \vdash \lnot (\alpha \sqcap \alpha ).&{} 4b~ \lrcorner (\alpha \sqcup \alpha )\vdash \lrcorner \alpha .\\ 5a~ \alpha \sqcap (\alpha \sqcup \beta )\vdash (\alpha \sqcap \alpha ).&{} 5b~ \alpha \sqcup \alpha \vdash \alpha \sqcup (\alpha \sqcap \beta ).\\ 6a~ \alpha \sqcap (\alpha \vee \beta )\vdash \alpha \sqcap \alpha .&{} 6b~ \alpha \sqcup \alpha \vdash \alpha \sqcup (\alpha \wedge \beta ).\\ 7a~ \bot \vdash \alpha \sqcap \lnot \alpha .&{} 7b~ \alpha \sqcup \lrcorner \alpha \vdash \top .\\ 8a~ \bot \vdash \lnot \top . &{} 8b~ \lrcorner \bot \vdash \top .\\ \end{array}$

Proof

The proofs are straightforward and one makes use of axioms 2a, 3a, 4a, Proposition 24 and the rule (R4) in most cases. For instance, here is a proof for 1a:

Interchanging $\alpha$ and $\beta$ in the above, we get $(\beta \sqcap \alpha )\vdash (\alpha \sqcap \beta )$.

(4a) follows from axiom 2a and (R3). (7a), (8a) follow from axiom 11a. The remaining proofs are given in the “Appendix”. Note that the proofs of $(ib), i=1,2,3,4,5,6,7,8,$ are obtained using the axioms and rules dual to those used to derive (ia). $\square$

Definitions of valuations on the algebras and satisfaction of sequents are as follows.

Definition 10

Let ${\textbf {D}}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top _{D},\bot _{D})$ be a contextual dBa. A valuation $v:\mathfrak {F}\rightarrow D$ on ${\textbf {D}}$ is a map such that for all $\alpha ,\beta \in \mathfrak {F}$ the following hold.

$$\begin{aligned} \begin{array}{ll} 1.~v(\alpha \sqcup \beta ):=v(\alpha )\sqcup v(\beta ).&{} 4.~ v(\alpha \sqcap \beta ):=v(\alpha )\sqcap v(\beta ).\\ 2.~v(\lrcorner \alpha ):=\lrcorner v(\alpha ).&{} 5.~ v(\lnot \alpha ):=\lnot v(\alpha ). \\ 3.~v(\top ):=\top _{D}.&{} 6.~v(\bot ):=\bot _{D}. \end{array} \end{aligned}$$

Definition 11

A sequent $\alpha \vdash \beta$ is said to be satisfied by a valuation v on a contextual dBa ${\textbf {D}}$ if and only if $v(\alpha )\sqsubseteq v(\beta )$. $\alpha \vdash \beta$ is true in ${\textbf {D}}$ if and only if for all valuations v on ${\textbf {D}}$, v satisfies $\alpha \vdash \beta$. $\alpha \vdash \beta$ is valid in the class of all contextual dBas if and only if it is true in every contextual dBa.

Theorem 26

(Soundness) If a sequent $\alpha \vdash \beta$ is provable in CDBL then it is valid in the class of all contextual dBas.

Proof

The proof that all the axioms of CDBL are valid in the class of all contextual dBas is straightforward and can be obtained using Proposition 4 and Definition 2. One then needs to verify that the rules of inference preserve validity. Using Proposition 4, one can show that $(R1), (R2),(R1)^{\prime }$ and $(R2)^{\prime }$ preserve validity. The cases for (R3) and $(R3)^{\prime }$ follow from Proposition 5.

To show (R5) preserves validity, let the sequents $\alpha \sqcap \beta \vdash \alpha \sqcap \alpha , \alpha \sqcap \alpha \vdash \alpha \sqcap \beta , \alpha \sqcup \beta \vdash \beta \sqcup \beta$, and $\beta \sqcup \beta \vdash \alpha \sqcup \beta$ be valid in the class of all contextual dBas. Let ${\textbf {D}}$ be a contextual dBa and v a valuation in ${\textbf {D}}$. Then v satisfies each sequent, which implies that $v(\alpha \sqcap \beta )\sqsubseteq v(\alpha \sqcap \alpha ), v(\alpha \sqcap \alpha )\sqsubseteq v(\beta \sqcap \alpha ), v(\alpha \sqcup \beta )\sqsubseteq v(\beta \sqcap \beta )$ and $v(\beta \sqcup \beta )\sqsubseteq v(\alpha \sqcup \beta )$. So $v(\alpha \sqcap \beta )= v(\alpha \sqcap \alpha )$ and $v(\alpha \sqcup \beta )=v(\beta \sqcup \beta )$, as ${\textbf {D}}$ is contextual. This gives $v(\alpha )\sqcap v(\beta )=v(\alpha )\sqcap v(\alpha )$ and $v(\alpha )\sqcup v(\beta )=v(\beta )\sqcup v(\beta )$. Thus $v(\alpha )\sqsubseteq v(\beta )$, whence $\alpha \vdash \beta$ is satisfied by v. $\square$

As usual, the completeness theorem is proved using the Lindenbaum-Tarski algebra of CDBL, and the algebra is constructed in the standard way as follows. A relation $\equiv _{\vdash }$ is defined on $\mathfrak {F}$ by: $\alpha \equiv _{\vdash }\beta$ if and only if $\alpha \dashv \vdash \beta$, for $\alpha ,\beta \in \mathfrak {F}$. $\equiv _{\vdash }$ is a congruence relation on $\mathfrak {F}$ with respect to $\sqcup$, $\sqcap$, $\lnot$, $\lrcorner$. The quotient set $\mathfrak {F}/\equiv _{\vdash }$ with operations induced by the logical connectives, give the Lindenbaum-Tarski algebra $\mathcal {L}(\mathfrak {F}):= (\mathfrak {F}/\equiv _{\vdash },\sqcup ,\sqcap ,\lnot ,\lrcorner ,[\top ],[\bot ])$. The axioms in CDBL and Theorem 25 ensure that $\mathcal {L}(\mathfrak {F})$ is a dBa. One then has

Proposition 27

For any formula $\alpha$ and $\beta$ the following are equivalent.

• 1. $\alpha \vdash \beta$ is provable in CDBL.

• 2. $[\alpha ]\sqsubseteq [\beta ]$ in $\mathcal {L}(\mathfrak {F})$ of CDBL.

Proof

For $1\implies 2$, we make use of $(R1)^{\prime }$, (R4), axiom 2a and Theorem 25(2a, 3a).

So $\alpha \sqcap \alpha \dashv \vdash \alpha \sqcap \beta$, which implies that $[\alpha ]\sqcap [\alpha ]=[\alpha \sqcap \alpha ]=[\alpha \sqcap \beta ]=[\alpha ]\sqcap [\beta ]$. Dually we can show that $[\alpha ]\sqcup [\beta ]=[\beta ]\sqcup [\beta ]$. Therefore $[\alpha ]\sqsubseteq [\beta ]$.

For $2\implies 1$, suppose $[\alpha ]\sqsubseteq [\beta ]$. Then $[\alpha ]\sqcap [\beta ]=[\alpha ]\sqcap [\alpha ]$. So $[\alpha \sqcap \beta ]=[\alpha \sqcap \alpha ]$. Similarly we can show that $[\alpha \sqcup \beta ]=[\beta \sqcup \beta ]$. Therefore $\alpha \sqcap \beta \dashv \vdash \alpha \sqcap \alpha$ and $\alpha \sqcup \beta \dashv \vdash \beta \sqcup \beta$. Now using (R5), $\alpha \vdash \beta$. $\square$

It is worth noting that the axioms of CDBL are obtained by converting the dBa axioms into sequents. Nonetheless, the system is complete with respect to the class of contextual dBas, because the relation $\equiv _{\vdash }$ provides a partial order on the set $\mathfrak {F}/\equiv _{\vdash }$, which forces the Lindenbaum algebra $\mathcal {L}(\mathfrak {F})$ to become a contextual dBa.

Theorem 28

$\mathcal {L}(\mathfrak {F})$ is a contextual dBa.

Proof

Follows directly by axiom 1, (R4) and Proposition 27. $\square$

The canonical map $v_{0}:\mathfrak {F}\rightarrow \mathfrak {F}/\equiv _{\vdash }$ defined by $v_{0}(\gamma ):=[\gamma ]$ for all $\gamma \in \mathfrak {F}$, can be shown to be a valuation on $\mathcal {L}(\mathfrak {F})$.

Theorem 29

(Completeness) If a sequent $\alpha \vdash \beta$ is valid in the class of all contextual dBas then it is provable in CDBL.

Proof

If $\alpha \vdash \beta$ be valid in the class of all contextual dBas, it is true in $\mathcal {L}(\mathfrak {F})$. Consider the canonical valuation $v_{0}$. Then $v_{0}(\alpha )\sqsubseteq v_{0}(\beta )$ and so $[\alpha ]\sqsubseteq [\beta ]$. By Proposition 27, it follows that $\alpha \vdash \beta$ is provable in CDBL. $\square$

5.2 MCDBL and ${\textbf {MCDBL4}}$

The language $\mathfrak {L}_{1}$ of MCDBL adds two unary modal connectives $\square$ and $\blacksquare$ to the language $\mathfrak {L}$ of CDBL. The formulae are given by the following scheme.

$$\begin{aligned} \top \mid \bot \mid p\mid \alpha \sqcup \beta \mid \alpha \sqcap \beta \mid \lnot \alpha \mid \lrcorner \alpha \mid \square \alpha \mid \blacksquare \alpha , \end{aligned}$$

where $p\in {\textbf {PV}}$. The set of formulae is denoted by $\mathfrak {F}_{1}$. The axiom schema for MCDBL consists of all the axioms of CDBL and the following.

$\begin{array}{ll} 15a~\square \alpha \sqcap \square \beta \dashv \vdash \square (\alpha \sqcap \beta )&{} 15b~ \blacksquare \alpha \sqcup \blacksquare \beta \dashv \vdash \blacksquare (\alpha \sqcup \beta )\\ 16a~ \square (\lnot \bot )\dashv \vdash \lnot \bot &{} 16b~\blacksquare (\lrcorner \top )\dashv \vdash \lrcorner \top \\ 17a~\square (\alpha \sqcap \alpha )\dashv \vdash \square (\alpha )&{} 17b~ \blacksquare (\alpha \sqcup \alpha )\dashv \vdash \blacksquare (\alpha ) \end{array}$

Rules of inference: All the rules of CDBL and the following.

   

Definable modal operators are $\lozenge , \blacklozenge$, given by $\lozenge \alpha :=\lnot \square \lnot \alpha$ and $\blacklozenge \alpha :=\lrcorner \blacksquare \lrcorner \alpha$. It is immediate that

Theorem 30

If a sequent $\alpha \vdash \beta$ is provable in ${\textbf {CDBL}}$ then it is provable in ${\textbf {MCDBL}}$.

A valuation v on a contextual dBao $\mathfrak {O}:=(D,\sqcup ,\sqcap ,\lnot ,\lrcorner ,\top _{D},\bot _{D},{\textbf {I}},{\textbf {C}})$, is a map from $\mathfrak {F}_{1}$ to D that satisfies the conditions in Definition 10 and the following for the modal operators:

Definition 12

$v(\square \alpha ):={\textbf {I}}(v(\alpha ))$ and $v(\blacksquare \alpha ):={\textbf {C}}(v(\alpha ))$.

Definitions of satisfaction, truth and validity of sequents are given in a similar manner as before.

5.2.1 ${\textbf {MCDBL}}\Sigma$

${\textbf {MCDBL4}}$ is obtained as a special case of the logic ${\textbf {MCDBL}}\Sigma$ that is defined as follows.

Definition 13

Let $\Sigma$ be any set of sequents in MCDBL. ${\textbf {MCDBL}}\Sigma$ is the logic obtained from MCDBL by adding all the sequents in $\Sigma$ as axioms.

Note that if $\Sigma =\emptyset$ then ${\textbf {MCDBL}}\Sigma$ is the same as ${\textbf {MCDBL}}$. The set $\Sigma$ required to define ${\textbf {MCDBL4}}$ will be given at the end of this section. Let us briefly discuss some features of ${\textbf {MCDBL}}\Sigma$ for any $\Sigma$—these would then apply to both ${\textbf {MCDBL}}$ and ${\textbf {MCDBL4}}$.

Let $V_{\Sigma }$ denote the class of those contextual dBaos in which the sequents of $\Sigma$ are valid. As a consequence of axioms 15a, 16a, 17a, 15a, 16b, 17b and rules (R8), (R9), one can conclude that if a sequent $\alpha \vdash \beta$ is provable in ${\textbf {MCDBL}}\Sigma$ then it is valid in the class $V_{\Sigma }$.

As before, one has the Lindenbaum-Tarski algebra $\mathcal {L}_{\Sigma }(\mathfrak {F}_{1})$ for ${\textbf {MCDBL}}\Sigma$; it has additional unary operators induced by the modal operators in $\mathfrak {L}_{1}$. More precisely, $\mathcal {L}_{\Sigma }(\mathfrak {F}_{1}):=(\mathfrak {F}_{1}/{\equiv _{\vdash }}, \sqcup ,\sqcap ,\lnot ,\lrcorner ,[\top ],[\bot ],f_{\square },f_{\blacksquare })$, where $f_{\square },f_{\blacksquare }$ are defined as: $f_{\square }([\alpha ]):=[\square \alpha ]$, $f_{\blacksquare }([\alpha ]):=[\blacksquare \alpha ]$.

Proposition 27 extends to this case. Using this proposition and rules (R8), (R9), one shows that the operators $f_{\square }, f_{\blacksquare }$ are monotonic:

Lemma 12

For $\alpha ,\beta \in \mathfrak {F}_{1}$, $[\alpha ]\sqsubseteq [\beta ]$ in $\mathcal {L}_{\Sigma }( \mathfrak {F}_{1})$ implies that $f_{\square }([\alpha ])\sqsubseteq f_{\square }([\beta ])$ and $f_{\blacksquare }([\alpha ])\sqsubseteq f_{\blacksquare }([\beta ])$.

$(\mathfrak {F}_{1}/{\equiv _{\vdash }}, \sqcup ,\sqcap ,\lnot ,\lrcorner ,[\top ],[\bot ])$ is a contextual dBa; Lemma 12 along with axioms 16a, 16b, 17a, 17b and the result corresponding to Proposition 27 give

Theorem 31

$\mathcal {L}_{\Sigma }(\mathfrak {F}_{1}) \in V_\Sigma$.

One then gets in the standard manner,

Theorem 32

(Completeness) If a sequent $\alpha \vdash \beta$ is valid in the class $V_{\Sigma }$ then it is provable in ${\textbf {MCDBL}}\Sigma$.

MCDBL4 is defined as the logic ${\textbf {MCDBL}}\Sigma$ where $\Sigma$ contains the following:

$$\begin{aligned} \begin{array}{l l} 18a~ \square \alpha \vdash \alpha &{} 18b~ \alpha \vdash \blacksquare \alpha \\ 19a~ \square \square \alpha \dashv \vdash \square \alpha &{} 19b~ \blacksquare \blacksquare \alpha \dashv \vdash \blacksquare \alpha \end{array} \end{aligned}$$

We have thus obtained

Theorem 33

(Soundness and completeness)

• 1. $\alpha \vdash \beta$ is provable in MCDBL if and only if $\alpha \vdash \beta$ is valid in the class of all contextual dBaos.

• 2. $\alpha \vdash \beta$ is provable in MCDBL4 if and only if $\alpha \vdash \beta$ is valid in the class of all topological contextual dBas.

5.3 Protoconcept-Based Semantics for the Logics

As a consequence of the representation result for contextual dBas (Corollary 1), we get another semantics for CDBL based on the sets of protoconcepts of contexts. The required basic definitions are derivable from those given in Sect. 5. However, for the sake of completeness, these are mentioned here. We first define valuations, models and satisfaction for a context $\mathbb {K}:=(G,M,I)$.

Valuations associate formulae with protoconcepts of $\mathbb {K}$:

A valuation is a map $v:\mathfrak {F}\rightarrow \mathfrak {P}(\mathbb {K})$ such that

$\begin{array}{ll} v(\alpha \sqcup \beta ):=v(\alpha )\sqcup v(\beta ).&{} v(\alpha \sqcap \beta ):=v(\alpha )\sqcap v(\beta ).\\ v(\lnot \alpha ):=\lnot v(\alpha ).&{} v(\lrcorner \alpha ):=\lrcorner v(\alpha ).\\ v(\top ):= (G, \emptyset ).&{} v(\bot ):=(\emptyset , M). \end{array}$

A model for CDBL based on the context $\mathbb {K}$ is a pair $\mathbb {M}:=(\mathfrak {P}(\mathbb {K}), v)$, where v is a valuation.

Let $\mathcal {K}$ denote the collection of all contexts.

Definition 14

A sequent $\alpha \vdash \beta$ is said to be satisfied in a model $\mathbb {M}$ based on $\mathbb {K}$ if $v(\alpha )\sqsubseteq v(\beta )$. $\alpha \vdash \beta$ is true in $\mathbb {K}$ if it is satisfied in every model based on $\mathbb {K}$. $\alpha \vdash \beta$ is valid in the class $\mathcal {K}$ if it is true in every context $\mathbb {K}\in \mathcal {K}$.

As for any context $\mathbb {K}$ the set $\mathfrak {P}(\mathbb {K})$ of protoconcepts of $\mathbb {K}$ forms a contextual dBa (Theorem 7(1)), and for any model $\mathbb {M}:=(\mathfrak {P}(\mathbb {K}),v)$, v is a valuation according to Definition 10, Theorem 26 gives us the soundness of CDBL with respect to the above semantics. In other words, if a sequent is provable in CDBL then it is valid in the class $\mathcal {K}$.

For the completeness result, we make use of the (Representation) Corollary 1 for contextual dBas and the fact that the Lindenbaum-Tarski algebra $\mathcal {L}(\mathfrak {F})$ is a contextual dBa (Theorem 28). From these it follows that $h:\mathfrak {F}/\equiv _{\vdash } \rightarrow \mathfrak {P}(\mathbb {K}(\mathcal {L}(\mathfrak {F})))$ defined as $h([\alpha ]):= (F_{[\alpha ]}, I_{[\alpha ]})$ for all $[\alpha ]\in \mathfrak {F}/\equiv _{\vdash }$, is an embedding. Recall the canonical map $v_0: \mathfrak {F}\rightarrow \mathfrak {F}/\equiv _{\vdash }$ defined in Sect. 5. The composition $v_{1}:=h\circ v_{0}$ is then a valuation, which implies that $\mathbb {M}(\mathcal {L}(\mathfrak {F})):=( \mathfrak {P}(\mathbb {K}(\mathcal {L}(\mathfrak {F}))), v_{1})$ is a model for CDBL.

Theorem 34

(Completeness) If a sequent $\alpha \vdash \beta$ is valid in $\mathcal {K}$ then $\alpha \vdash \beta$ is provable in CDBL.

Proof

If possible, suppose $\alpha \vdash \beta$ is not provable in CDBL. By Proposition 27, $[\alpha ]\not \sqsubseteq [\beta ]$. By Proposition 3(3), either $[\alpha ]\sqcap [\alpha ]\not \sqsubseteq _{\sqcap } [\beta ]\sqcap [\beta ]$ or $[\alpha ]\sqcup [\alpha ]\not \sqsubseteq _{\sqcup } [\beta ]\sqcup [\beta ]$. Then there exists a prime filter $F_{0}$ in $\mathcal {L}(\mathfrak {F})_{\sqcap }$ (a Boolean algebra by Proposition 3) such that $[\alpha ]\sqcap [\alpha ]\in F_{0}$ and $[\beta ]\sqcap [\beta ]\notin F_{0}$. By Lemma 2, there exists a filter F in $\mathcal {L}(\mathfrak {F})$ such that $F\cap \mathcal {L}(\mathfrak {F})_{\sqcap }=F_{0}$ and as $F_{0}$ is prime, $F\in \mathcal {F}_{p}(\mathcal {L}(\mathfrak {F}))$. As $[\alpha ]\sqcap [\alpha ]\in F_{0}$, $[\alpha ]\sqcap [\alpha ]\in F$ and $[\beta ]\sqcap [\beta ]\notin F$, because $[\beta ]\sqcap [\beta ]\notin F_{0}$ and $[\beta ]\sqcap [\beta ]\in \mathcal {L}(\mathfrak {F})_{\sqcap }$. So $[\alpha ]\in F$, as $[\alpha ]\sqcap [\alpha ]\sqsubseteq [\alpha ]$, and $[\beta ]\notin F$, otherwise $[\beta ]\sqcap [\beta ]\in F$. This gives $F\in F_{[\alpha ]}$ and $F\notin F_{[\beta ]}$, whence .

In case $[\alpha ]\sqcup [\alpha ]\not \sqsubseteq _{\sqcap }[\beta ]\sqcup [\beta ]$, we can dually show that there exists $I\in \mathcal {I}_{p}(\mathcal {L}(\mathfrak {F}))$ such that $[\alpha ]\notin I$ and $[\beta ]\in I$ giving .

So , which implies that $\alpha \vdash \beta$ is not true in the model $\mathbb {M}(\mathcal {L}(\mathfrak {F}))$—a contradiction. $\square$

In case of MCDBL and MCDBL4, instead of a context $\mathbb {K}:=(G, M, I)$, we consider a Kripke context ${\mathbb {K}}{\mathbb {C}}:=((G, R), (M, S), I)$ based on $\mathbb {K}:=(G, M, I)$. A valuation $v: \mathfrak {F}_{1}\rightarrow \mathfrak {P}(\mathbb {K})$ extends the one for CDBL with the following definitions for the modal operators: $v(\square \alpha ):= f_{R}(v(\alpha ))$ and $v(\blacksquare \alpha ):=f_{S}(v(\alpha ))$. Let us denote the class of all Kripke contexts by ${\mathcal{KC}\mathcal{}}$ and that of all reflexive and transitive Kripke contexts by ${\mathcal{KC}\mathcal{}}_{RT}$. Models, satisfaction of sequents is as for CDBL. Then it is straightforward to show that MCDBL and MCDBL4 are sound with respect to the classes ${\mathcal{KC}\mathcal{}}$ and ${\mathcal{KC}\mathcal{}}_{RT}$ respectively.

Note that by Theorem 31, for MCDBL the Lindenbaum-Tarski algebra $\mathcal {L}_{\Sigma }(\mathfrak {F}_{1})$ is a contextual dBao, while for MCDBL4, it is a topological contextual dBa. The completeness of MCDBL with respect to the class ${\mathcal{KC}\mathcal{}}$ is then proved in a similar manner as Theorem 34, the representation result given by Theorem 20(2) being used. In case of MCDBL4, as a consequence of Theorem 22, ${\mathbb {K}}{\mathbb {C}}(\mathcal {L}_{\Sigma }(\mathfrak {F}_{1}))$ is a reflexive and transitive Kripke context. Using the (Representation) Theorem 23(1), one gets completeness of MCDBL4 with respect to the class ${\mathcal{KC}\mathcal{}}_{RT}$.

6 Conclusions

In a pioneering work unifying FCA and rough set theory, Düntsch and Gediga (2002), Yao (2004) proposed object oriented and property oriented concepts of a context. For a context $\mathbb {K}:=(G, M, I)$, its complement is the context $\mathbb {K}^{c}:=(G, M, -R)$, where $-R:=G\times M{\setminus }R$. It has been shown that the lattice of concepts of $\mathbb {K}$ is dually isomorphic (isomorphic) to that of object oriented (property oriented) concepts of $\mathbb {K}^{c}$. In the line of Wille’s work, negation was introduced into the study and object oriented semiconcepts and protoconcepts of a context were proposed in Howlader and Banerjee (2018), Howlader and Banerjee (2020a). It was observed that (A, B) is a protoconcept of $\mathbb {K}$, if and only if $(A^{c}, B)$ is an object oriented protoconcept of $\mathbb {K}^{c}$. The same holds for semiconcepts of a context. For a context $\mathbb {K}$, object oriented protoconcepts form a dBa, while object oriented semiconcepts form a pure dBa. The entire study presented here may also be done in terms of object oriented semiconcepts and protoconcepts. In particular, one may derive representation results for the algebras introduced here, with the help of corresponding algebras of object oriented semiconcepts and protoconcepts.

A complete Vormbrock and Wille (2005) dBa ${\textbf {D}}$ is one for which the Boolean algebras ${\textbf {D}}_{\sqcap }$ and ${\textbf {D}}_{\sqcup }$ are complete. Vormbrock and Wille (2005) have shown that any complete fully contextual (pure) dBa ${\textbf {D}}$ for which ${\textbf {D}}_{\sqcap }$ and ${\textbf {D}}_{\sqcup }$ are atomic, is isomorphic to the algebra of protoconcepts (semiconcepts) of some context. This result gives rise to the question of such a characterisation in case of a complete fully contextual dBao ${\textbf {D}}$ for which ${\textbf {D}}_{\sqcap }$ and ${\textbf {D}}_{\sqcup }$ are atomic. It appears that, using Vormbrock and Wille’s results and the representation results obtained here for dBaos in terms of the full complex algebra of protoconcepts, one should be able to obtain the desired characterisation.

Another direction of investigation one may pursue, is the duality between the class of all Kripke contexts and that of all dBaos. We have shown in this work that a dBao $\mathfrak {O}$ induces a Kripke context ${\mathbb {K}}{\mathbb {C}}(\mathfrak {O})$, and on the other hand, a Kripke context ${\mathbb {K}}{\mathbb {C}}$ induces a dBao $\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}})$. A natural question then would be: is ${\mathbb {K}}{\mathbb {C}}(\underline{\mathfrak {P}}^{+}({\mathbb {K}}{\mathbb {C}}))$ isomorphic to ${\mathbb {K}}{\mathbb {C}}$?

Topological representation results for algebras are well-studied in literature. This would serve as yet another immediate point of investigation for the algebras discussed in this work.

Logics corresponding to dBas, pure dBas and their extensions with operators as defined here, remain an open question. The logic MCDBL4 for topological contextual dBas is obtained as a special case of ${\textbf {MCDBL}}\Sigma$, where $\Sigma$ is any set of sequents in ${\textbf {MCDBL}}$. This gives a scheme of obtaining several other logics that may express properties of dBaos and corresponding classes of Kripke contexts besides the ones considered here. For topological contextual dBas and correspondingly, reflexive and transitive Kripke contexts, MCDBL4 with $\Sigma$ containing the modal axioms for reflexivity and transitivity, serves the purpose. One may well include other axioms (such as symmetry) in $\Sigma$, and investigate the resulting modal systems.

Appendix A: Proofs

Proof in Theorem 16, that $(D,\sqcap ,\sqcup ,\lnot ,\top ,\bot )$ is a Boolean algebra: Let $\mathfrak {O}$ be a dBao such that for all $a\in D$, $\lnot a=\lrcorner a$ and $\lnot \lnot a=a$. Let $x,y\in D$ such that $x\sqsubseteq y$ and $y\sqsubseteq x$. By Proposition 4(4), $x\sqcap x=y\sqcap y$ and $x\sqcup x=y\sqcup y$. Using Proposition 5(3), $\lnot \lnot x=\lnot \lnot y$ and so $x=y$. Therefore $(D,\sqsubseteq )$ is a partially ordered set. From Definition 2(2a and 2b) it follows that $\sqcap ,\sqcup$ is commutative, while Definition 2(3a and 3b) gives that $\sqcap ,\sqcup$ is associative. Using Definition 2(5a) and Proposition 5(3), $x\sqcap (x\sqcup y)=x\sqcap x=\lnot \lnot x$. So $x\sqcap (x\sqcup y)= x$. Again using Definition 2(5b) and Proposition 5(3), $x\sqcup (x\sqcap y)= x$. Therefore $(D,\sqcap ,\sqcup ,\lnot ,\top ,\bot )$ is a bounded complemented lattice. To show it is a distributive lattice, we show that for all $x,y, \in D$ $x\sqcap y= x\wedge y$ and $x\vee y= x\sqcup y$. Rest of the proof follows from Definition 2(6a and 6b).

Let $x,y\in D$. Then $x,y\sqsubseteq x\sqcup y$. Proposition 5(2) gives $\lnot (x\sqcup y)\sqsubseteq \lnot x,\lnot y$. Therefore by Proposition 4(6), $\lnot (x\sqcup y)\sqcap \lnot y\sqsubseteq \lnot x\sqcap \lnot y$ and $\lnot (x\sqcup y)\sqcap \lnot (x\sqcup y)\sqsubseteq \lnot (x\sqcup y)\sqcap \lnot y$. So $\lnot (x\sqcup y)\sqcap \lnot (x\sqcup y)\sqsubseteq \lnot x\sqcap \lnot y$. By Proposition 5(1), $\lnot (x\sqcup y)\sqsubseteq \lnot x\sqcap \lnot y,$ and by Proposition 5(2), $\lnot (\lnot x\sqcap \lnot y)\sqsubseteq \lnot \lnot (x\sqcup y)=(x\sqcup y)\sqcap (x\sqcup y)\sqsubseteq x\sqcup y$. Hence $x\vee y\sqsubseteq x\sqcup y$. Using Proposition 4(5) and Proposition 5(2), $\lnot x\sqcap \lnot y\sqsubseteq \lnot x,\lnot y$. So $\lnot \lnot x\sqsubseteq \lnot (\lnot x\sqcap \lnot y)$ and $\lnot \lnot y\sqsubseteq \lnot (\lnot x\sqcap \lnot y)$. Therefore $x\sqsubseteq \lnot (\lnot x\sqcap \lnot y)=x\vee y$ and $y\sqsubseteq \lnot (\lnot x\sqcap \lnot y)=x\vee y$. Proposition 4(6) gives $x\sqcup y \sqsubseteq x\vee y$, as $(x\vee y)\sqcup (x\vee y)=\lrcorner \lrcorner (x\vee y)=\lnot \lnot (x\vee y)=x\vee y$. So $x\sqcup y=x\vee y$. Dually we can show that $x\sqcap y=x\wedge y$.

Proof of Theorem 25

      2a.

Now,

Similarly we can show that $\alpha \sqcap (\beta \sqcap \gamma )\vdash (\alpha \sqcap \beta )\sqcap \gamma$.

3a.

5a.

6a. Proof is identical to that of 5a. $\square$