# On the Logical and Algebraic Aspects of Reasoning with Formal Contexts

Prosenjit Howlader<EMAIL_ADDRESS>1234-5678-9012 and  Churn-
Jung Liau<EMAIL_ADDRESS>0000-0001-6842-9637 Institute of
Information Science,Academia SinicaTaipei115Taiwan

###### Abstract.

A formal context consists of objects, properties, and the incidence relation
between them. Various notions of concepts defined with respect to formal
contexts and their associated algebraic structures have been studied
extensively, including formal concepts in formal concept analysis (FCA), rough
concepts arising from rough set theory (RST), and semiconcepts and
protoconcepts for dealing with negation. While all these kinds of concepts are
associated with lattices, semiconcepts and protoconcepts additionally yield an
ordered algebraic structure, called double Boolean algebras. As the name
suggests, a double Boolean algebra contains two underlying Boolean algebras.

In this paper, we investigate logical and algebraic aspects of the
representation and reasoning about different concepts with respect to formal
contexts. We present two-sorted modal logic systems KB and KF for the
representation and reasoning of rough concepts and formal concepts
respectively. Then, in order to represent and reason about both formal and
rough concepts in a single framework, these two logics are unified into a two-
sorted Boolean modal logic BM, in which semiconcepts and protoconcepts are
also expressible. Based on the logical representation of semiconcepts and
protoconcepts, we prove the characterization of double Boolean algebras in
terms of their underlying Boolean algebras. Finally, we also discuss the
possibilities of extending our logical systems for the representation and
reasoning of more fine-grained information in formal contexts.

Modal logic, Boolean algebra, Double Boolean algbra, Formal concept analysis,
Rough set theory.

##  1\. Introduction

In lattice theory, a polarity (birkhoff1940lattice, ) is a triplet
$\mathbb{K}:=(G,M,I)$ where $G$ and $M$ are sets and $I\subseteq G\times M$ is
a binary relation between them. For $g\in G$ and $m\in M$, we usually use
$Igm$ or $gIm$ to denote $(g,m)\in I$. A given polarity induces two operators
$+:(\mathcal{P}(G),\subseteq)\rightarrow(\mathcal{P}(M),\supseteq)$ and
$-:(\mathcal{P}(M),\supseteq)\rightarrow(\mathcal{P}(G),\subseteq)$, where for
all $A\in\mathcal{P}(G)$ and $B\in\mathcal{P}(M)$:

$A^{+}=\\{m\in M\mid\mbox{ for all }g\in A\leavevmode\nobreak\
\leavevmode\nobreak\ gIm\\},$ $B^{-}=\\{g\in G\mid\mbox{ for all }m\in
B\leavevmode\nobreak\ \leavevmode\nobreak\ gIm\\}.$

In formal concept analysis (FCA) (FCA, ), a polarity is called a formal
context (or simply context). A (formal) concept is a pair of sets $(A,B)$ such
that $A^{+}=B$ and $A=B^{-}$, where $A$ and $B$ are called its extent  and
intent respectively. The set of all concepts is denoted by
$\mathbf{B}(\mathbb{K})$ and forms a complete lattice
$\underline{\mathbf{B}}(\mathbb{K})$. In addition, to deal with the negation
of concept, the notions of semiconcepts and protoconcepts are introduced in
(wille, ). Algebraic studies of these notions led to the definition of double
Boolean algebras (dBa) and pure double Boolean algebras (wille, ). These
structures have been studied extensively (wille, ; vormbrock2005semiconcept, ;
BALBIANI2012260, ; MR4566932, ; howlader2018algebras, ; howlader2020, ). A
Stone-type representation theorem for fully contextual and pure dBas is given
in (howlader2020, ). Representation theorems for arbitrary dBas, however,
remain open. In this article, we address this problem using Boolean algebras.

Düntsch et al. (duntsch2002modal, ) defined sufficiency, dual sufficiency,
possibility and necessity operators based on a context. For a context
$\mathbb{K}:=(G,M,I)$, $g\in G$, and $m\in M$
$I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}:=\\{m\in M\mid Igm\\}$
and $I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}:=\\{g\in G\mid
Igm\\}$ are the $I^{\rightarrow}$-neighborhood and
$I^{\leftarrow}$-neighbourhood of $g$ and $m$ respectively. For $A\subseteq
G$, and $B\subseteq M$, the pairs of dual approximation operators are defined
as:

$(\mbox{possibility})\leavevmode\nobreak\
B_{I}^{{\Diamond_{\mathfrak{m}}}}:=\\{g\in
G:I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}\cap
B\neq\emptyset\\},\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ (\mbox{necessity})\leavevmode\nobreak\
B_{I}^{{\Box_{\mathfrak{m}}}}:=\\{g\in
G:I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}\subseteq B\\}$.

$(\mbox{possibility})\leavevmode\nobreak\
A_{I}^{{\Diamond_{\mathfrak{g}}}}:=\\{m\in
M:I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}\cap
A\neq\emptyset\\},\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ (\mbox{necessity})\leavevmode\nobreak\
A_{I}^{{\Box_{\mathfrak{g}}}}:=\\{m\in
M:I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}\subseteq A\\}$.

If there is no confusion about the relation involved, we shall omit the
subscript and denote $B_{I}^{{\Diamond_{\mathfrak{m}}}}$ by
$B^{{\Diamond_{\mathfrak{m}}}}$, $B_{I}^{{\Box_{\mathfrak{m}}}}$ by
$B^{{\Box_{\mathfrak{m}}}}$ and similarly for the case of $A$.

The necessity and possibility operators correspond to approximation operators
in rough set theory (RST) (pawlak1982rough, ). Based on these operators,
Düntsch et al. (duntsch2002modal, ) and Yao (yao2004concept, ) introduced
property oriented concepts and object oriented concepts respectively. A pair
$(A,B)$ is a property oriented concept of $\mathbb{K}$ iff
$A^{{\Diamond_{\mathfrak{g}}}}=B$ and $B^{{\Box_{\mathfrak{m}}}}=A$, and it is
an object oriented concept of $\mathbb{K}$ iff $A^{{\Box_{\mathfrak{g}}}}=B$
and $B^{{\Diamond_{\mathfrak{m}}}}=A$. These two kinds of concepts are also
called rough concepts.

The operators used in formal and rough concepts correspond to modalities used
in modal logic (Gargov1987, ; blackburn2002moda, ). In particular, the
operator used in FCA is the window modality (sufficiency operator)
(Gargov1987, ) and those used in RST are box (necessity operator) and diamond
(possibility operator) modalities (blackburn2002moda, ). Furthermore, a
context is a two-sorted structure consisting of object and property sorts.

Considering these facts, a significant amount of work has been done on
relational semantics of logics interpreted in context-based models. In other
words, for these kinds of investigations, contexts are semantic frames of
logical formulas. Gehrke (Gehrke, ) presented a two-sorted relational
semantics for the implication-fusion fragment of several sub-structural
logics, where a reduced and separating frame is defined as a reduced and
separating context (Gehrke, ) with additional relations. The two-sorted
relational semantics for non-distributive modal logic was studied by Conradie
et al. (CWFSPAPMTAWN, ; Conradie2017167, ; CONRADIE2019923, ; CONRADIE2021371,
; nlsm, ), Greco et al. (Greco, ) and Hartonas (HCgame, ; CH, ) independently.
In (CWFSPAPMTAWN, ), an intuitive, epistemic interpretation of RS-frames for
modal logic, in terms of categorization systems and agents are proposed. A
sound and complete epistemic logic of categories and categorical perception of
agents is studied in (Conradie2017167, ). An LE-logic is proposed in (Greco, )
as a non-distributive modal logic for lattice expansion. In (nlsm, ), a two-
sorted relational semantics based on context for LE-logic is presented from
the perspective of FCA and RST. For FCA, modal operators are treated as window
modality and formulas are interpreted as formal concepts of a context. While
RST is taken into consideration, the modal operators are simply box and
diamond modalities.

All the logics studied in (CWFSPAPMTAWN, ; Conradie2017167, ; Greco, ; nlsm, )
are Gentzen-style sequent calculus. In this paper, we study Hilbert-style
axiomatic systems for formal contexts. Motivated from Boolean modal logic
(Gargov1987, ), we developed its two-sorted version that allows us to work
with box and window modalities within a single model.

To achieve the goal, we first introduce two-sorted modal logics KB and KF
interpreted in contexts. The logic KB deals with box modality while KF deals
with window modality. The two logics are integrated into a single two-sorted
Boolean modal logic BM which is interpreted in contexts with complements of
binary relations. We prove the soundness and completeness of the proposed
logics. We also show that these logics can represent both rough and formal
concepts.

More specifically, the language of BM consist of 2-indexed family
$\\{P_{s_{1}},P_{s_{2}}\\}$ of propositional variables, logical connectives
and modal connectives
${\Box_{\mathfrak{g}}},{\Box_{\mathfrak{m}}},{\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}$.
The compound $s$-sort formula build over atomic formulas in $P_{s}$ for
$s=s_{1},s_{2}$. The indexed family of formulas is denoted by
$Fm(\textbf{BM}):=\\{Fm(\textbf{BM})_{s_{1}},Fm(\textbf{BM})_{s_{2}}\\}$. We
characterize the pairs of formulas that represent concepts, semiconcepts, and
protoconcepts in a context. For instance, a pair of formulas $(\varphi,\psi)$
is a right semiconcept in a context-based model $\mathfrak{M}$ if
$\mathfrak{M}\models\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$ and
is a left semiconcept if
$\mathfrak{M}\models{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$. The
set of formula pairs representing left (resp. right) semiconcepts is denoted
by ${\tt SC}^{l}$ (resp. ${\tt SC}^{r}$). Two left (resp. right) semiconcepts
$(\varphi_{1},\psi_{1})$ and $(\varphi_{2},\psi_{2})$ are called equivalent if
$\varphi_{1}$ and $\varphi_{2}$ (resp. $\psi_{1}$ and $\psi_{2}$) are
equivalent. This defines an equivalence relation $\equiv^{l}_{\tt SC}$ (resp.
$\equiv^{r}_{\tt SC}$) over ${\tt SC}^{l}$ (resp. ${\tt SC}^{r}$). It is shown
that the corresponding equivalence classes ${\tt SC}^{l}/\equiv^{l}_{\tt SC}$
(resp. ${\tt SC}^{r}/\equiv^{r}_{\tt SC}$) forms Boolean algebras. For a
subset $\mathfrak{D}$ of $Fm(\textbf{BM})_{s_{1}}\times
Fm(\textbf{BM})_{s_{2}}$, we consider the maps $r:\mathfrak{D}\rightarrow{\tt
SC}^{l}/\equiv^{l}_{\tt SC}$ and $e:{\tt SC}^{l}/\equiv^{l}_{\tt
SC}\rightarrow\mathfrak{D}$; $r^{\prime}:\mathfrak{D}\rightarrow{\tt
SC}^{r}/\equiv^{r}_{\tt SC}$ and $e^{\prime}:{\tt SC}^{r}/\equiv^{r}_{\tt
SC}\rightarrow\mathfrak{D}$ such that $r\circ e=id_{{\tt
SC}^{l}/\equiv^{l}_{\tt SC}}$ and $r^{\prime}\circ e^{\prime}=id_{{\tt
SC}^{r}/\equiv^{r}_{\tt SC}}$. These maps induce an algebraic structure
$(\mathfrak{D},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top_{\mathfrak{D}},\bot_{\mathfrak{D}})$
where for all $x,y\in\mathfrak{D}$

$x\sqcap y:=e(r(x)\wedge r(y))$ $x\sqcup y:=e^{\prime}(r^{\prime}(x)\vee
r^{\prime}(y))$

$\bar{\neg}x:=e(\neg r(x))$ and $\lrcorner x:=e^{\prime}(\neg r^{\prime}(x))$

$\bot_{\mathfrak{D}}:=e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$
and
$\top_{\mathfrak{D}}:=e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])$

Then, it is shown that
$(\mathfrak{D},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top_{\mathfrak{D}},\bot_{\mathfrak{D}})$
is a pure dBa iff $r,r^{\prime},e,e^{\prime}$ satisfies certain conditions.
Moreover, we prove a more general result as follows:

:

Let $(B,\wedge,\neg,0,1)$ and
$(B^{\prime},\vee^{\prime},\neg^{\prime},0^{\prime},1^{\prime})$ be two
Boolean algebras and let $r:A\rightleftharpoons B:e$ and
$r^{\prime}:A\rightleftharpoons B^{\prime}:e^{\prime}$ be pairs of maps such
that $r\circ e=id_{B}$ and $r^{\prime}\circ e^{\prime}=id_{B^{\prime}}$. If
$\textbf{A}:=(A,\sqcap,\sqcup,\bar{\neg},\lrcorner,e^{\prime}(1^{\prime}),e(0))$
is an algebra where $\sqcap$, $\sqcup$, $\bar{\neg}$ and $\lrcorner$ are
defined as above, then A is a dBa iff $r,r^{\prime},e,e^{\prime}$ satisfy
certain conditions.

In a typical application of FCA to association rule mining, a formal context
can represent transaction data, where $G$ is the set of customers, $M$ is the
set of product items, and $(g,m)\in I$ means that $g$ has purchased $m$. In
such a scenario, the conditional probability that a group of customers will
purchase a product or not is a crucial piece of information. To facilitate
more expressive language for such kind of information, we also suggest
possible extensions of the above-mentioned logic to two-sorted graded and
weighted modal logics. To demonstrated the expressiveness of two-sorted graded
modal logic, we characterized a class of contexts with the properties such as
partial functions, functions, one-one and onto functions in terms of logical
formulas. We also discussed which two-sorted modal axiom can be extended to
the weighted case.

The remainder of the paper is organized as follows. We will first review basic
definitions and main results of general many-sorted modal logic and double
Boolean algebras in this introductory section. Then, in Section 2, we present
logics KB and KF for the representation and reasoning of rough and formal
concepts respectively. In Section 3, we investigate the concept lattices and
their relationships based on the logical representation. The two-sorted
Boolean modal logic BM is proposed in Section 4 as an uniform framework for
representing and reasoning about different notions of concepts. In Section 5,
we study logical representations of concepts, semiconcepts and protoconcepts
in BM and their relationships, and prove a characterization of dBas in terms
of Boolean algebras. The graded and weighted modal logics for expressing more
fine-grained information in formal contexts are discussed in Section 6.1 and
6.2 respectively. Finally, we summarize the paper and indicate directions of
future work in Section 7.

In this paper, we use the symbol $\implies$ to denote implication in the
metalanguage. The complement and power set of a set $X$ are denoted by
$\overline{X}$ and $\mathcal{P}(X)$ respectively.

###  1.1. Many-sorted modal logic

The many-sorted polyadic modal logic is introduced in (mspml, ). The alphabet
of the logic consists of a many-sorted signature $(S,\Sigma)$, where $S$ is
the collection of sorts and $\Sigma$ is the set of modalities, and an
$S$-indexed family $P:=\\{P_{s}\\}_{s\in S}$ of propositional variables, where
$P_{s}\neq\emptyset$ and $P_{s}\cap P_{t}=\emptyset$ for distinct $s,t\in S$.
Each modality $\sigma\in\Sigma$ is associated with an arity $s_{1}s_{2}\ldots
s_{n}\rightarrow s$. For any $n\in\mathbb{N}$, we denote
$\Sigma_{s_{1}s_{2}\ldots
s_{n}s}=\\{\sigma\in\Sigma\mid\sigma:s_{1}s_{2}\ldots s_{n}\rightarrow s\\}$.
For the purpose of the paper, we only need to consider unary modalities.
Hence, we will simply present many-sorted monadic modal logic below.

Let $(S,\Sigma)$ be a signature such that $\Sigma$ is a set of unary
modalities. Then, the set of formulas is an $S$-index family
$Fm_{S}:=\\{Fm_{s}\mid s\in S\\}$, defined inductively for each $s\in S$ by

$\varphi_{s}::=p_{s}\;\mid\;\neg\varphi_{s}\;\mid\;\varphi_{s}\wedge\varphi_{s}\;\mid\;\langle\sigma\rangle\varphi_{s^{\prime}}\;\mid\;[\sigma]\varphi_{s^{\prime}}$

where $p_{s}\in P_{s}$ and $\sigma\in\Sigma_{s^{\prime}s}$.

A many-sorted frame is a pair $\mathfrak{F}:=(\\{W_{s}\\}_{s\in
S},\\{R_{\sigma}\\}_{\sigma\in\Sigma})$ where $W_{s}\neq\emptyset$, $W_{s}\cap
W_{s^{\prime}}=\emptyset$ for $s\not=s^{\prime}\in S$ and $R_{\sigma}\subseteq
W_{s}\times W_{s^{\prime}}$ if $\sigma\in\Sigma_{s^{\prime}s}$ for
$s,s^{\prime}\in S$. The class of all many-sorted frames is denoted by
$\mathbb{MSF}$. A valuation $v$ is an $S$-indexed family of maps
$\\{v_{s}\\}_{s\in S}$, where $v_{s}:P_{s}\rightarrow\mathcal{P}(W_{s})$. A
many-sorted model $\mathfrak{M}:=(\mathfrak{F},v)$ consists of a many-sorted
frame $\mathfrak{F}$ and a valuation $v$. The satisfaction of a formula in a
model $\mathfrak{M}$ is defined inductively as follows.

###### Definition 1.1.

Let $\mathfrak{M}:=(\\{W_{s}\\}_{s\in
S},\\{R_{\sigma}\\}_{\sigma\in\Sigma},v)$ be a many-sorted model, $w\in W_{s}$
and $\varphi\in Fm_{s}$ for $s\in S$. We define
$\mathfrak{M},w\models_{s}\varphi$ by induction over $\varphi$ as follows:

  1. (1)

$\mathfrak{M},w\models_{s}p$ iff $w\in v_{s}(p)$

  2. (2)

$\mathfrak{M},w\models_{s}\neg\varphi$ iff
$\mathfrak{M},w\not\models_{s}\varphi$

  3. (3)

$\mathfrak{M},w\models_{s}\varphi_{1}\wedge\varphi_{2}$ iff
$\mathfrak{M},w\models_{s}\varphi_{1}$ and
$\mathfrak{M},w\models_{s}\varphi_{2}$

  4. (4)

If $\sigma\in\Sigma_{s^{\prime}s}$, then
$\mathfrak{M},w\models_{s}\langle\sigma\rangle\psi$ iff there is
$w^{\prime}\in W_{s^{\prime}}$ such that $(w,w^{\prime})\in R_{\sigma}$ and
$\mathfrak{M},w^{\prime}\models_{s^{\prime}}\psi$

  5. (5)

If $\sigma\in\Sigma_{s^{\prime}s}$, then
$\mathfrak{M},w\models_{s}[\sigma]\psi$ iff for all $w^{\prime}\in
W_{s^{\prime}}$, $(w,w^{\prime})\in R_{\sigma}$ implies that
$\mathfrak{M},w^{\prime}\models_{s^{\prime}}\psi$

Let $\mathfrak{M}$ be an $(S,\Sigma)$-model. Then, for a set $\Phi\subseteq
Fm_{s}$, $\mathfrak{M},w\models_{s}\Phi$ if $\mathfrak{M},w\models_{s}\varphi$
for all $\varphi\in\Phi$. Let $\mathcal{C}$ be a class of models. Then, for a
set $\Phi\cup\\{\varphi\\}\subseteq Fm_{s}$, $\varphi$ is a local semantic
consequence of $\Phi$ over $\mathcal{C}$, denoted by
$\Phi\models^{\mathcal{C}}_{s}\varphi$, if $\mathfrak{M},w\models_{s}\Phi$
implies $\mathfrak{M},w\models_{s}\varphi$ for all models
$\mathfrak{M}\in\mathcal{C}$ and $w$ in $\mathfrak{M}$. If $\mathcal{C}$ is
the class of all models, we omit the superscript and denote it as
$\Phi\models_{s}\varphi$. If $\Phi$ is empty, we say $\varphi$ is valid in
$\mathcal{C}$ and denoted it as $\mathcal{C}\models_{s}\varphi$. When
$\mathcal{C}$ is the class of all models based on a given frame
$\mathfrak{F}$, we also denote it by $\mathfrak{F}\models_{s}\varphi$.

To characterize the local semantic consequence, the modal system
$\mathbf{K}_{(S,\Sigma)}:=\\{\mathbf{K}_{s}\\}_{s\in S}$ is proposed in
(mspml, ), where $\mathbf{K}_{s}$ is the axiomatic system in Figure 1 in which
$\sigma\in\Sigma_{s^{\prime}s}$:

(1) Axioms (a) (PL): All propositional tautologies of sort $s$. (b) (Kσ):
$[\sigma](\varphi_{s^{\prime}}\rightarrow\psi_{s^{\prime}})\rightarrow([\sigma]\varphi_{s^{\prime}}\rightarrow[\sigma]\psi_{s^{\prime}})$
(c) (Dualσ):
$\langle\sigma\rangle\varphi_{s^{\prime}}\leftrightarrow\neg[\sigma]\neg\varphi_{s^{\prime}}$
(2) Inference rules: (a) (MP)s:
$\psi_{s}\varphi_{s},\varphi_{s}\rightarrow\psi_{s}$ (b) (UG${}_{\sigma})$:
$[\sigma]\varphi_{s^{\prime}}\varphi_{s^{\prime}}$

Figure 1. The axiomatic system $\mathbf{K}_{s}$

When the signature is clear from the context, the subscripts may be omitted
and we simply write the system as $\mathbf{K}$.

###### Definition 1.2.

Let $\Lambda=\\{\Lambda_{s}\subseteq Fm_{s}\\}_{s\in S}$ be an $S$-sorted set
of formulas. The normal modal logic defined by $\Lambda$ is
$\mathbf{K}\Lambda:=\\{\mathbf{K}_{s}\cup\Lambda_{s}\\}_{s\in S}$

###### Definition 1.3.

A sequence of formulas $\varphi_{1},\varphi_{2},\ldots\varphi_{n}$ is called a
$\mathbf{K}\Lambda$-proof for the formula $\varphi$ if $\varphi_{n}=\varphi$
and $\varphi_{i}$ is an instance of formulas in $\mathbf{K}\Lambda$ or
inferred from $\varphi_{1},\ldots,\varphi_{i-1}$ using modus ponens and
universal generalization. If $\varphi\in Fm_{s}$ has a proof in
$\mathbf{K}\Lambda$, we say that $\varphi$ is a theorem and write
$\vdash_{s}\varphi$. Let $\Phi\cup\\{\varphi\\}\subseteq Fm_{s}$ be a set of
formulas. Then, we say that $\varphi$ is provable form $\Phi$, denoted by
$\Phi\vdash_{s}\varphi$, if there exist
$\varphi_{1},\ldots,\varphi_{n}\in\Phi$ such that
$\vdash_{s}(\varphi_{1}\wedge\ldots\wedge\varphi_{n})\rightarrow\varphi$. In
addition, the set $\Phi$ is $\mathbf{K}\Lambda$-inconsistent if $\bot$ is
provable from it, otherwise it is $\mathbf{K}\Lambda$-consistent.

The completeness of $\mathbf{K}\Lambda$ is proved by using the standard
canonical model construction(mspml, ). First, we need the following
proposition.

###### Proposition 1.4.

$\mathbf{K}\Lambda$ is strongly complete with respect to a class of models
$\mathcal{C}$ iff any $\mathbf{K}\Lambda$-consistent set of formulas is
satisfied in some model from $\mathcal{C}$.

Then, the canonical model is defined as follows.

###### Definition 1.5.

The canonical model of $\mathbf{K}\Lambda$ is

$\mathfrak{M}^{\mathbf{K}\Lambda}:=(\\{W_{s}^{\mathbf{K}\Lambda}\\}_{s\in
S},\\{R_{\sigma}^{\mathbf{K}\Lambda}\\}_{\sigma\in\Sigma},V^{\mathbf{K}\Lambda})$

where

  * (a)

for any $s\in S$, $W_{s}^{\mathbf{K}\Lambda}=\\{\Phi\subseteq
Fm_{s}\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \Phi\leavevmode\nobreak\
\mbox{is maximally}\leavevmode\nobreak\
\mathbf{K}\Lambda\mbox{-consistent}\\}$,

  * (b)

for any $\sigma\in\Sigma_{s^{\prime}s}$, $w\in W_{s}^{\mathbf{K}\Lambda}$, and
$w^{\prime}\in W_{s^{\prime}}^{\mathbf{K}\Lambda}$,
$R_{\sigma}^{\mathbf{K}\Lambda}ww^{\prime}$ iff for any $\psi$, $\psi\in
w^{\prime}$ implies that $\langle\sigma\rangle\psi\in w$.

  * (c)

$V^{\mathbf{K}\Lambda}=\\{V^{\mathbf{K}\Lambda}_{s}\\}$ is the valuation
defined by $V_{s}^{\mathbf{K}\Lambda}(p)=\\{w\in
W_{s}^{\mathbf{K}\Lambda}\leavevmode\nobreak\ \mid\leavevmode\nobreak\ p\in
w\\}$ for any $s\in S$ and $p\in P_{s}$.

For simplicity, we will omit the superscript $\mathbf{K}\Lambda$ from the
canonical model from now on.

###### Lemma 1.6.

(Truth Lemma) If $s\in S$, $\varphi\in Fm_{s}$,
$\sigma\in\Sigma_{s^{\prime}s}$ and $w\in W_{s}$ then the following hold:

  * (a)

for any $w^{\prime}\in W_{s^{\prime}}$, $R_{\sigma}ww^{\prime}$ iff for any
formulas $\psi$, $[\sigma]\psi\in w$ implies $\psi\in w^{\prime}$.

  * (b)

If $\langle\sigma\rangle\psi\in w$ then there is $w^{\prime}\in
W_{s^{\prime}}$ such that $\psi\in w^{\prime}$ and $R_{\sigma}ww^{\prime}$.

  * (c)

$\mathfrak{M},w\models_{s}\varphi$ iff $\varphi\in w$.

###### Proposition 1.7.

If $\Phi_{s}$ is a $\mathbf{K}\Lambda$-consistent set of formulas then it is
satisfied in the canonical model.

These results lead to the soundness and completeness of $\mathbf{K}$ directly.

###### Theorem 1.8.

$\mathbf{K}$ is sound and strongly complete with respect to the class of all
$(S,\Sigma)$-models, i.e. for any $s\in S$ and $\Phi\cup\\{\varphi\\}\subseteq
Fm_{s}$, $\Phi\vdash_{s}\varphi$ iff $\Phi\models_{s}\varphi$.

###  1.2. Formal and rough concept analysis

In addition to formal concept lattices mentioned in Section 1, the set
$\mathbf{O}(\mathbb{K})$ of all object oriented concepts and the set
$\mathbf{P}(\mathbb{K})$ of all property oriented concepts also form complete
lattices, which are called object oriented concept lattices and property
oriented concept lattices respectively.

For concept lattices ${\mathcal{X}}=\mathbf{B}(\mathbb{K})$,
$\mathbf{O}(\mathbb{K})$, $\mathbf{P}(\mathbb{K})$, the set of all extents and
intents of $\mathcal{X}$ are denoted by $\mathcal{X}_{ext}$ and
$\mathcal{X}_{int}$, respectively.

###### Proposition 1.9.

For a context $\mathbb{K}:=(G,M,I)$, the following holds.

  * (a)

$\mathbf{B}(\mathbb{K})_{ext}=\\{A\subseteq G\mid A^{+-}=A\\}$ and
$\mathbf{B}(\mathbb{K})_{int}=\\{B\subseteq M\mid B^{-+}=B\\}$.

  * (b)

$\mathbf{P}(\mathbb{K})_{ext}=\\{A\subseteq G\mid
A^{{\Diamond_{\mathfrak{g}}}{\Box_{\mathfrak{m}}}}=A\\}$ and
$\mathbf{P}(\mathbb{K})_{int}=\\{B\subseteq M\mid
B^{{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}}=B\\}$.

  * (c)

$\mathbf{O}(\mathbb{K})_{ext}=\\{A\subseteq G\mid
A^{{\Box_{\mathfrak{g}}}{\Diamond_{\mathfrak{m}}}}=A\\}$ and
$\mathbf{O}(\mathbb{K})_{int}=\\{B\subseteq M\mid
B^{{\Diamond_{\mathfrak{m}}}{\Box_{\mathfrak{g}}}}=B\\}$.

It can be shown that the sets
$\mathbf{B}(\mathbb{K})_{ext},\mathbf{O}(\mathbb{K})_{ext}$ and
$\mathbf{P}(\mathbb{K})_{ext}$ form complete lattices and are isomorphic to
the corresponding concept lattices. Analogously, the sets
$\mathbf{B}(\mathbb{K})_{int},\mathbf{O}(\mathbb{K})_{int}$ and
$\mathbf{P}(\mathbb{K})_{int}$ form complete lattices and are dually
isomorphic to the corresponding concept lattices. Therefore, a concept can be
identified with its extent or intent. The relationship among the three kinds
of concept lattices are investigated in (yao2004comparative, ). In particular,
the following theorem is proved.

###### Theorem 1.10.

(yao2004comparative, ) For a context $\mathbb{K}=(G,M,I)$ and the complemented
context $\overline{\mathbb{K}}=(G,M,\overline{I})$, the following holds.

  * (a)

The concept lattice of $\mathbb{K}$ is isomorphic to the property oriented
concept lattice of $\overline{\mathbb{K}}$.

  * (b)

The property oriented concept lattice of $\mathbb{K}$ is dually isomorphic to
the object oriented concept lattice of $\mathbb{K}$.

  * (c)

The concept lattice of $\mathbb{K}$ is dually isomorphic to the object
oriented concept lattice of $\overline{\mathbb{K}}$.

To introduce negation in the study of formal concepts, Wille (wille, )
introduced semiconcepts and protoconcepts.

###### Definition 1.11.

A pair of sets $(A,B)$ is called protoconcept (resp. semiconcept) of a context
$\mathbb{K}$ if $A^{+-}=B^{-}$ (resp. $A^{+}=B$ or $B^{-}=A$).

To introduce negation in the study of the object oriented concepts, in the
line of the study by Wille, object oriented semiconcepts (resp. protoconcept)
were introduced (MR4566932, ).

###### Definition 1.12.

A pair of sets $(A,B)$ is called object oriented protoconcept (resp.
semiconcept) of a context $\mathbb{K}$ if
$A^{{\Box_{\mathfrak{g}}}{\Diamond_{\mathfrak{m}}}}=B^{{\Diamond_{\mathfrak{m}}}}$
(resp. $A^{{\Box_{\mathfrak{g}}}}=B$ or $B^{{\Diamond_{\mathfrak{m}}}}=A$).

As mentioned above, this leads to the study of dBa and pure dBa.

###### Definition 1.13.

(wille, ) An algebra
$\textbf{D}:=(D,\sqcup,\sqcap,\bar{\neg},\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)\bar{\neg}(x\sqcap x)=\bar{\neg}x&(3b)\lrcorner(x\sqcup x)=\lrcorner x\\\
(4a)x\sqcap(x\sqcup y)=x\sqcap x&(4b)x\sqcup(x\sqcap y)=x\sqcup x\\\
(5a)x\sqcap(y\bar{\vee}z)=(x\sqcap y)\bar{\vee}(x\sqcap
z)&(5b)x\sqcup(y\bar{\wedge}z)=(x\sqcup y)\bar{\wedge}(x\sqcup z)\\\
(6a)x\sqcap(x\bar{\vee}y)=x\sqcap x&(6b)x\sqcup(x\bar{\wedge}y)=x\sqcup x\\\
(7a)\bar{\neg}\bar{\neg}(x\sqcap y)=x\sqcap y&(7b)\lrcorner\lrcorner(x\sqcup
y)=x\sqcup y\\\ (8a)x\sqcap\bar{\neg}x=\bot&(8b)x\sqcup\lrcorner x=\top\\\
(9a)\bar{\neg}\top=\bot&(9b)\lrcorner\bot=\top\\\ (10a)x\sqcap(y\sqcap
z)=(x\sqcap y)\sqcap z&(10b)x\sqcup(y\sqcup z)=(x\sqcup y)\sqcup z\\\
(11a)\bar{\neg}\bot=\top\sqcap\top&(11b)\lrcorner\top=\bot\sqcup\bot\\\
(12)(x\sqcap x)\sqcup(x\sqcap x)=(x\sqcup x)\sqcap(x\sqcup x)&\end{array}$

where $x\bar{\vee}y:=\bar{\neg}(\bar{\neg}x\sqcap\bar{\neg}y)$ and
$x\bar{\wedge}y:=\lrcorner(\lrcorner x\sqcup\lrcorner y)$. If, in addition,
for any $x\in D$, $x\sqcap x=x$ or $x\sqcup x=x$ holds, then D is called a
pure dBa.

Each dBa D contains two underlying Boolean algebras.

###### Proposition 1.14.

(vormbrock, ) For a dBa $\textbf{
D}=(D,\sqcup,\sqcap,\bar{\neg},\lrcorner,\top,\bot)$, let $D_{\sqcap}=\\{x\in
D\mid x\sqcap x=x\\}$ and $D_{\sqcup}=\\{x\in D\mid x\sqcup x=x\\}$. Then,
$\textbf{D}_{\sqcap}:=(D_{\sqcap},\sqcap,\bar{\vee},\bar{\neg},\bot,\bar{\neg}\bot)$
and
$\textbf{D}_{\sqcup}:=(D_{\sqcup},\bar{\wedge},\sqcup,\lrcorner,\lrcorner\top,\top)$
are both Boolean algebras.

##  2\. Two-sorted modal logic for formal contexts

In this section, we present the logics KB and KF and discuss their
relationship with rough and formal concepts.

###  2.1. Two-sorted modal logic and concept lattices in rough set theory

To represent rough concept, we consider a particular two-sorted signature with
only two unary modalities
$(\\{s_{1},s_{2}\\},\\{{\Diamond_{\mathfrak{g}}},{\Diamond_{\mathfrak{m}}}\\})$
where the arity of ${\Diamond_{\mathfrak{g}}}$ and ${\Diamond_{\mathfrak{m}}}$
are $s_{1}s_{2}$ and $s_{2}s_{1}$ respectively. As usual, we denote dual
modalities of ${\Diamond_{\mathfrak{g}}}$ and ${\Diamond_{\mathfrak{m}}}$ by
${\Box_{\mathfrak{g}}}$ and ${\Box_{\mathfrak{m}}}$ respectively. We use
$Fm(\textbf{KB}):=\\{Fm(\textbf{KB})_{s_{1}},Fm(\textbf{KB})_{s_{2}}\\}$ to
denote the indexed family of formulas built over this signature111To simplify
the notation, we will directly write modal formulas as $\Diamond_{i}\varphi$
and $\Box_{i}\varphi$ instead of $\langle\Diamond_{i}\rangle\varphi$ and
$[\Diamond_{i}]\varphi$ for $i=\mathfrak{g,m}$..

This modal language is interpreted in context-based models. For a context
$\mathbb{K}=(G,M,I)$, a $\mathbb{K}$-based model is a quadruple
$\mathfrak{M}:=(G,M,I,v)$, where $v$ is the valuation. Then, we define the
satisfaction of modal formulas in the model by

  1. (1)

$\mathfrak{M},g\models_{s_{1}}{\Diamond_{\mathfrak{m}}}\varphi$ iff there is
$m\in M$ such that $(g,m)\in I$ and $\mathfrak{M},m\models_{s_{2}}\varphi$,

  2. (2)

$\mathfrak{M},m\models_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi$ iff there is
$g\in G$ such that $(g,m)\in I$ and $\mathfrak{M},g\models_{s_{1}}\varphi$.

Hence, in terms of the general framework of many-sorted modal logic, the model
is based on a special kind of two-sorted frames
$\mathfrak{F}=(W_{1},W_{2},R_{{\Diamond_{\mathfrak{g}}}},R_{{\Diamond_{\mathfrak{m}}}})$,
where $W_{1}=G,W_{2}=M,R_{{\Diamond_{\mathfrak{g}}}}=I^{-1}$, and
$R_{{\Diamond_{\mathfrak{m}}}}=I$. This kind of frame is called bidirectional
because the two binary relations are converse to each other. We also say that
$\mathfrak{F}$ is the corresponding frame of the context $(G,M,I)$ and any
models based on it. We use $\mathbb{CM}$ and $2\mathbb{SBF}$ to denote the
classes of all context-based models and their corresponding frames
respectively.

The logic system over the particular signature is $\mathbf{KB}$ consisting of
the system $\mathbf{K}$ (instantiated to the current signature) and the
additional axiom (B) as follows:

$\varphi_{s_{1}}\rightarrow{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\varphi_{s_{1}}$
$\varphi_{s_{2}}\rightarrow{\Box_{\mathfrak{g}}}{\Diamond_{\mathfrak{m}}}\varphi_{s_{2}}.$

We prove that $\mathbf{KB}$ is sound and complete with respect to
$2\mathbb{SBF}$ (and so $\mathbb{CM}$, too).

###### Theorem 2.1.

$\mathbf{KB}$ is sound with respect to $2\mathbb{SBF}$.

###### Proof.

The proof is straightforward. Here we give the proof for the axiom
$\varphi_{s_{1}}\rightarrow{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\varphi_{s_{1}}$.
Let $\mathfrak{M}$ be a model based on the frame
$(W_{1},W_{2},R_{{\Diamond_{\mathfrak{g}}}},R_{{\Diamond_{\mathfrak{m}}}})$
defined above and $\mathfrak{M},w_{1}\models_{s_{1}}\varphi_{s_{1}}$ for some
$w_{1}\in W_{1}$. Then, for any $w_{2}\in W_{2}$ such that
$R_{\Diamond_{\mathfrak{m}}}w_{1}w_{2}$, we have
$\mathfrak{M},w_{2}\models_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi_{s_{1}}$
because $R_{{\Diamond_{\mathfrak{g}}}}w_{2}w_{1}$ follows from the converse of
relation. This leads to
$\mathfrak{M},w_{1}\models_{s_{1}}{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\varphi_{s_{1}}$
immediately. ∎

The completeness theorem is proved using the canonical model of KB, which is
an instance of that constructed in Definition 1.5. Hence,

$\mathfrak{M}^{\textbf{KB}}:=(W_{s_{1}}^{\textbf{KB}},W_{s_{2}}^{\textbf{KB}},R_{\Diamond_{\mathfrak{g}}}^{\textbf{KB}},R_{{\Diamond_{\mathfrak{m}}}}^{\textbf{KB}},V^{\textbf{KB}})$

As above, we will omit the superscript KB for simplicity in the presentation
of the proof. It is easy to see that the model satisfies the following
properties for $x\in W_{s_{1}}$ and $y\in W_{s_{2}}$:

  * (a)

$R_{{\Diamond_{\mathfrak{g}}}}yx$ iff $\varphi\in x$ implies that
${\Diamond_{\mathfrak{g}}}\varphi\in y$ for any $\varphi\in
Fm(\mathbf{KB})_{s_{1}}$.

  * (b)

$R_{{\Diamond_{\mathfrak{m}}}}xy$ iff $\varphi\in y$ implies that
${\Diamond_{\mathfrak{m}}}\varphi\in x$ for any $\varphi\in
Fm(\mathbf{KB})_{s_{2}}$.

###### Theorem 2.2.

$\mathbf{KB}$ is strongly complete with respect to $2\mathbb{SBF}$, that is
for any $s\in\\{s_{1},s_{2}\\}$, $\varphi\in Fm(\mathbf{KB})_{s}$ and
$\Phi\subseteq Fm(\mathbf{KB})_{s}$, $\Phi\models^{2\mathbb{SBF}}_{s}\varphi$
implies that $\Phi\vdash_{s}^{\mathbf{KB}}\varphi$.

###### Proof.

It is sufficient to show that the canonical model is indeed bidirectional and
hence corresponds to a context-based one. Then, the result follows from
Propositions 1.4 and 1.7. Let $x\in W_{s_{1}}$ and $y\in W_{s_{2}}$ and assume
$R_{{\Diamond_{\mathfrak{g}}}}yx$. Then, for any $\varphi\in y$, we have
${\Box_{\mathfrak{g}}}{\Diamond_{\mathfrak{m}}}\varphi\in y$ by axiom (B),
which in turns implies ${\Diamond_{\mathfrak{m}}}\varphi\in x$ by Lemma 1.6.
Hence, $R_{{\Diamond_{\mathfrak{m}}}}xy$ by property (b) of the canonical
model. Analogously, we can show that $R_{{\Diamond_{\mathfrak{m}}}}xy$ implies
$R_{{\Diamond_{\mathfrak{g}}}}yx$. That is, $R_{{\Diamond_{\mathfrak{m}}}}$ is
indeed the converse of $R_{{\Diamond_{\mathfrak{g}}}}$. ∎

###### Example 2.3.

In a typical application of FCA to association rule mining, a formal context
$(G,M,I)$ can represent transaction data, where $G$ is the set of customers,
$M$ is the set of product items, and for $g\in G$, and $m\in M$, $gIm$ means
that the customer $g$ has bought the item $m$. Let $\mathfrak{M}=(G,M,I,v)$ be
a context-based model, and let $\varphi\in Fm(\textbf{KB})_{s_{1}}$ and
$\psi\in Fm(\textbf{KB})_{s_{2}}$ be formulas representing customers in the 30
to 50 age group and item set of electronic products respectively. Then, the
formulas ${\Box_{\mathfrak{g}}}\varphi$ and ${\Box_{\mathfrak{m}}}\psi$ in the
model $\mathfrak{M}$ may be interpreted as follows.

  * •

For $g\in G$, $\mathfrak{M},g\models_{s_{1}}{\Box_{\mathfrak{m}}}\psi$ means
that all items bought by $g$ are electronic products, or the customer $g$ only
buys electronic products.

  * •

For $m\in M$, $\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\varphi$
means that all customers buying $m$ are in the 30 to 50 age group.

$\Box$

Let us denote the truth set of a formula $\varphi\in
Fm(\textbf{KB})_{s_{i}}(i=1,2)$ in a model $\mathfrak{M}$ by
$[\\!\\![\varphi]\\!\\!]_{\mathfrak{M}}:=\\{w\in
W_{i}\mid\mathfrak{M},w\models_{s_{i}}\varphi\\}$. We usually omit the
subscript and simply write it as $[\\!\\![\varphi]\\!\\!]$.

###### Proposition 2.4.

Let $\mathfrak{M}:=(G,M,I,v)$ be a context-based model. Then, the relationship
between approximation operators and modal formulas is as follows:

  * (i)

$[\\!\\![\varphi]\\!\\!]^{{\Diamond_{\mathfrak{g}}}}=[\\!\\![{\Diamond_{\mathfrak{g}}}\varphi]\\!\\!]$
and
$[\\!\\![\varphi]\\!\\!]^{{\Box_{\mathfrak{g}}}}=[\\!\\![{\Box_{\mathfrak{g}}}\varphi]\\!\\!]$
for $\varphi\in Fm(\textbf{KB})_{s_{1}}$.

  * (ii)

$[\\!\\![\varphi]\\!\\!]^{{\Diamond_{\mathfrak{m}}}}=[\\!\\![{\Diamond_{\mathfrak{m}}}\varphi]\\!\\!]$
and
$[\\!\\![\varphi]\\!\\!]^{{\Box_{\mathfrak{m}}}}=[\\!\\![{\Box_{\mathfrak{m}}}\varphi]\\!\\!]$
for $\varphi\in Fm(\textbf{KB})_{s_{2}}$.

###### Definition 2.5.

Let $\mathfrak{C}$ be the bidirectional frame corresponding to the context
$\mathbb{K}=(G,M,I)$. Then, we define $Fm_{PC},Fm_{OC}\subseteq
Fm(\textbf{KB})_{s_{1}}\times Fm(\textbf{KB})_{s_{2}}$ by

  * (a)

$Fm_{PC}:=\\{(\varphi,\psi)\mid\models^{\mathfrak{C}}_{s_{1}}\varphi\leftrightarrow{\Box_{\mathfrak{m}}}\psi,\models^{\mathfrak{C}}_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow\psi\\}$

  * (b)

$Fm_{OC}:=\\{(\varphi,\psi)\mid\models^{\mathfrak{C}}_{s_{1}}\varphi\leftrightarrow{\Diamond_{\mathfrak{m}}}\psi,\models^{\mathfrak{C}}_{s_{2}}{\Box_{\mathfrak{g}}}\varphi\leftrightarrow\psi\\}$

  * (c)

$Fm_{PC_{ext}}:=\pi_{1}(Fm_{PC})$ and $Fm_{PC_{int}}:=\pi_{2}(Fm_{PC})$

  * (d)

$Fm_{OC_{ext}}:=\pi_{1}(Fm_{OC})$ and $Fm_{OC_{int}}:=\pi_{2}(Fm_{OC})$

where $\pi_{1}$ and $\pi_{2}$ are projection operators222That is, for a subset
$S\subseteq A\times B$, $\pi_{1}(S)=\\{a\in A\mid\exists b\in B,(a.b)\in S\\}$
and $\pi_{2}(S)=\\{b\in B\mid\exists a\in A,(a.b)\in S\\}$.

By the definition, we have $Fm_{PC_{ext}}:=\\{\varphi\in
Fm(\textbf{KB})_{s_{1}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{1}}{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow\varphi\\}$,
$Fm_{PC_{int}}:=\\{\varphi\in Fm(\textbf{KB})_{s_{2}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{2}}{\Diamond_{\mathfrak{g}}}{\Box_{\mathfrak{m}}}\varphi\leftrightarrow\varphi\\}$,
$Fm_{OC_{ext}}:=\\{\varphi\in Fm(\textbf{KB})_{s_{1}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{1}}{\Diamond_{\mathfrak{m}}}{\Box_{\mathfrak{g}}}\varphi\leftrightarrow\varphi\\}$,
and $Fm_{OC_{int}}:=\\{\varphi\in
Fm(\textbf{KB})_{s_{2}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{2}}{\Box_{\mathfrak{g}}}{\Diamond_{\mathfrak{m}}}\varphi\leftrightarrow\varphi\\}$.

Note that these sets are implicitly parameterized by the underlying context
and should be indexed with $\mathbb{K}$. However, for simplicity, we omit the
index. Obviously, when $(\varphi,\psi)\in Fm_{PC}$, we have
$([\\!\\![\varphi]\\!\\!],[\\!\\![\psi]\\!\\!])\in\mathbf{P}(\mathbb{K})$ for
any $\mathbb{K}$-based models. Hence, $Fm_{PC}$ consists of pairs of formulas
representing property oriented concepts. Analogously, $Fm_{OC}$ provides the
representation of object oriented concepts.

###  2.2. Two sorted modal logic and concept lattice in formal concept
analysis

To represent formal concepts, we consider another two-sorted signature
$(\\{s_{1},s_{2}\\},\\{{\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}\\}\\})$,
where $\Sigma_{s_{1}s_{2}}=\\{{\boxminus_{\mathfrak{g}}}\\}$ and
$\Sigma_{s_{2}s_{1}}=\\{{\boxminus_{\mathfrak{m}}}\\}$, and the logic KF based
on it. Syntactically, the signature is the same as that for $\mathbf{KB}$
except we use different symbols to denote the modalities. Hence, formation
rules of formulas remain unchanged and we denote the indexed family of
formulas by
$Fm(\textbf{KF})=\\{Fm(\textbf{KF})_{s_{1}},Fm(\textbf{KF})_{s_{2}}\\}$. In
addition, while both KF and $\mathbf{KB}$ are interpreted in context-based
models, the main difference between them is on the way of their modalities
being interpreted.

###### Definition 2.6.

Let $\mathfrak{M}:=(G,M,I,v)$ be a context-based model. Then,

  * (a)

For $\varphi\in Fm(\textbf{KF})_{s_{1}}$ and $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi$ iff for any
$g\in G$, $\mathfrak{M},g\models_{s_{1}}\varphi$ implies $Igm$

  * (b)

For $\varphi\in Fm(\textbf{KF})_{s_{2}}$ and $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\boxminus_{\mathfrak{m}}}\varphi$ iff for any
$m\in M$, $\mathfrak{M},m\models_{s_{2}}\varphi$ implies $Igm$

The logic system $\mathbf{KF}:=\\{\mathbf{KF}_{s_{1}},\mathbf{KF}_{s_{2}}\\}$
is shown in Figure 2.

(1) Axioms: (PL) Propositional tautologies of sort $s_{i}$ for $i=1,2$.
$(K_{{\boxminus_{\mathfrak{g}}}}^{1})$
${\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\neg\varphi_{2})\rightarrow({\boxminus_{\mathfrak{g}}}\neg\varphi_{1}\rightarrow{\boxminus_{\mathfrak{g}}}\neg\varphi_{2})$
for $\varphi_{1},\varphi_{2}\in Fm(\mathbf{KF})_{s_{1}}$ $(B^{1})$
$\varphi\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi$
for $\varphi\in Fm(\mathbf{KF})_{s_{1}}$
$(K_{{\boxminus_{\mathfrak{m}}}}^{2})$
${\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\neg\psi_{2})\rightarrow({\boxminus_{\mathfrak{m}}}\neg\psi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}\neg\psi_{2})$
for $\psi_{1},\psi_{2}\in Fm(\mathbf{KF})_{s_{2}}$ $(B^{2})$
$\psi\rightarrow{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi$ for
$\psi\in Fm(\mathbf{KF})_{s_{2}}$ (2) Inference rules: • $(MP)_{s}$: for
$s\in\\{s_{1},s_{2}\\}$ and $\varphi,\psi\in Fm_{s}$
$\psi\varphi,\varphi\rightarrow\psi$ •
$(UG^{1}_{{\boxminus_{\mathfrak{g}}}})$: for $\varphi\in
Fm(\textbf{KF})_{s_{1}}$, ${{\boxminus_{\mathfrak{g}}}}\varphi\neg\varphi$ •
$(UG^{2}_{{\boxminus_{\mathfrak{m}}}})$: for $\psi\in
Fm(\textbf{KF})_{s_{2}}$, ${\boxminus_{\mathfrak{m}}}\psi\neg\psi$

Figure 2. The axiomatic system KF

###### Example 2.7.

Continuing with Example 2.3, let $\varphi\in Fm(\textbf{KF})_{s_{1}}$ and
$\psi\in Fm(\textbf{KF})_{s_{2}}$ remain unchanged. Then, the intuitive
meanings of the formulas ${\boxminus_{\mathfrak{g}}}\varphi$ and
${\boxminus_{\mathfrak{m}}}\psi$ are as follows:

  * •

For $g\in G$, $\mathfrak{M},g\models_{s_{1}}{\boxminus_{\mathfrak{m}}}\psi$,
$g$ bought all electronic products.

  * •

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi$, all
customers in the 30 to 50 age group bought $m$. $\Box$

We define a translation $\rho:Fm(\textbf{KF})\rightarrow Fm(\mathbf{KB})$
where $\rho=\\{\rho_{1},\rho_{2}\\}$ as follows:

  1. (1)

$\rho_{i}(p):=p$ for all $p\in P_{s_{i}}$ ($i=1,2$).

  2. (2)

$\rho_{i}(\varphi\wedge\psi):=\rho_{i}(\varphi)\wedge\rho_{i}(\psi)$ for
$\varphi,\psi\in Fm(\textbf{KF})_{s_{i}}$ ($i=1,2$).

  3. (3)

$\rho_{i}(\neg\varphi):=\neg\rho_{i}(\varphi)$ for $\varphi\in
Fm(\textbf{KF})_{s_{i}}$ ($i=1,2$).

  4. (4)

$\rho_{2}({\boxminus_{\mathfrak{g}}}\varphi):={\Box_{\mathfrak{g}}}\neg\rho_{1}(\varphi)$
for $\varphi\in Fm(\textbf{KF})_{s_{1}}$.

  5. (5)

$\rho_{1}({\boxminus_{\mathfrak{m}}}\varphi):={\Box_{\mathfrak{m}}}\neg\rho_{2}(\varphi)$
for $\varphi\in Fm(\textbf{KF})_{s_{2}}$.

###### Theorem 2.8.

For any formula $\varphi\in Fm(\textbf{KF})_{s_{i}}(i=1,2)$ the following
hold.

  * (a)

$\Phi\vdash^{\textbf{KF}}\varphi$ iff
$\rho(\Phi)\vdash^{\mathbf{KB}}\rho(\varphi)$ for any $\Phi\subseteq
Fm(\textbf{KF})_{s_{i}}$.

  * (b)

Let $\mathfrak{M}:=(G,M,I,v)$ be a context-based model and let
$\overline{\mathfrak{M}}:=(G,M,\overline{I},v)$ be its complemented model.
Then, for any $g\in G,\mathfrak{M},g\models_{s_{1}}\varphi$ iff
$\overline{\mathfrak{M}},g\models_{s_{1}}\rho_{1}(\varphi)$, and for any $m\in
M,\mathfrak{M},m\models_{s_{2}}\varphi$ iff
$\overline{\mathfrak{M}},m\models_{s_{2}}\rho_{2}(\varphi)$

  * (c)

$\varphi$ is valid in the class $\mathbb{CM}$ iff $\rho(\varphi)$ is valid in
$\mathbb{CM}$.

###### Proof.

  * (a).

We can prove it by showing that $\varphi$ is an axiom in KF iff
$\rho(\varphi)$ is an axiom in $\mathbf{KB}$, and for each rule in KF, there
is a translation of it in $\mathbf{KB}$ and vice verse.

  * (b).

By induction on the complexity of formulas, as usual, the proof of basis and
Boolean cases are straightforward. For
$\varphi={\boxminus_{\mathfrak{g}}}\psi$, let us assume any $m\in M$. Then, by
Definition 2.6, $\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}}\psi$
iff for all $g\in G$, $\overline{I}gm$ implies that
$\mathfrak{M},g\models_{s_{1}}\neg\psi$. By induction hypothesis, this means
that for all $g\in G$, $\overline{I}gm$ implies that
$\overline{\mathfrak{M}},g\models_{s_{1}}\neg\rho_{1}(\psi)$. That is,
$\overline{\mathfrak{M}},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\neg\rho_{1}(\psi)$.
By the definition of $\rho$, this is exactly
$\overline{\mathfrak{M}},m\models_{s_{2}}\rho_{2}(\varphi)$. The case of
$\varphi={\boxminus_{\mathfrak{m}}}\psi$ is proved analogously.

  * (c).

This follows immediately from (b).

∎

###### Proposition 2.9.

  * (a).

For $\varphi_{1},\varphi_{2}\in Fm(\textbf{KF})_{s_{1}}$,
${\boxminus_{\mathfrak{g}}}\varphi_{2}\rightarrow{\boxminus_{\mathfrak{g}}}\varphi_{1}\varphi_{1}\rightarrow\varphi_{2}$

  * (b).

For $\varphi_{1},\varphi_{2}\in Fm(\textbf{KF})_{s_{2}}$,
${\boxminus_{\mathfrak{m}}}\varphi_{2}\rightarrow{\boxminus_{\mathfrak{m}}}\varphi_{1}\varphi_{1}\rightarrow\varphi_{2}$

###### Proof.

We only prove (a) and the proof of (b) is similar.

$\displaystyle\vdash^{\textbf{KF}}$
$\displaystyle\varphi_{1}\rightarrow\varphi_{2}$
$\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle\rho(\varphi_{1})\rightarrow\rho(\varphi_{2})(\mbox{\rm
Theorem\leavevmode\nobreak\ \ref{translation} (a)})$
$\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle(\rho(\varphi_{1})\rightarrow\rho(\varphi_{2}))\rightarrow(\neg\rho(\varphi_{2})\rightarrow\neg\rho(\varphi_{1}))(\mbox{\rm
PL})$ $\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle\neg\rho(\varphi_{2})\rightarrow\neg\rho(\varphi_{1})(\mbox{\rm
MP})$ $\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle{\Box_{\mathfrak{g}}}(\neg\rho(\varphi_{2})\rightarrow\neg\rho(\varphi_{1}))(\mbox{\rm
UG})$ $\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle{\Box_{\mathfrak{g}}}(\neg\rho(\varphi_{2})\rightarrow\neg\rho(\varphi_{1}))\rightarrow({\Box_{\mathfrak{g}}}\neg\rho(\varphi_{2})\rightarrow{\Box_{\mathfrak{g}}}\neg\rho(\varphi_{1}))(\mbox{\rm
K})$ $\displaystyle\vdash^{\mathbf{KB}}$
$\displaystyle{\Box_{\mathfrak{g}}}\neg\rho(\varphi_{2})\rightarrow{{\Box_{\mathfrak{g}}}}\neg\rho(\varphi_{1})(\mbox{\rm
MP})$ $\displaystyle\vdash^{\textbf{KF}}$
$\displaystyle{\boxminus_{\mathfrak{g}}}\varphi_{2}\rightarrow{\boxminus_{\mathfrak{g}}}\varphi_{1}(\mbox{\rm
Theorem \ref{translation}(a)})$

∎

###### Theorem 2.10.

KF is sound and strongly complete with respect to the class $\mathbb{CM}$.

###### Proof.

This follows from Theorem 2.8 and the fact that KB is sound and strongly
complete with respect to $\mathbb{CM}$. ∎

###### Proposition 2.11.

Recalling the definition of truth set, we have

  * (i)

$[\\!\\![{\boxminus_{\mathfrak{g}}}\varphi]\\!\\!]=[\\!\\![\varphi]\\!\\!]^{+}$
for $\varphi\in Fm(\textbf{KF})_{s_{1}}$

  * (ii)

$[\\!\\![{\boxminus_{\mathfrak{m}}}\varphi]\\!\\!]=[\\!\\![\varphi]\\!\\!]^{-}$
for $\varphi\in Fm(\textbf{KF})_{s_{2}}$.

###### Definition 2.12.

Let $\mathfrak{C}:=\\{(G,M,I^{-1},I)\\}$ be the corresponding frame of a
context. Then, we define $Fm_{FC}\subseteq Fm(\mathbf{KF})_{s_{1}}\times
Fm(\mathbf{KF})_{s_{2}}$ by

  * (a)

$Fm_{FC}:=\\{(\varphi,\psi)\mid\models^{\mathfrak{C}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi,\models^{\mathfrak{C}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi\\}$

  * (b)

$Fm_{FC_{ext}}:=\pi_{1}(Fm_{FC})$ and $Fm_{FC_{int}}:=\pi_{2}(Fm_{FC})$

From the definition, we can derive $Fm_{FC_{ext}}:=\\{\varphi\in
Fm(\mathbf{KF})_{s_{1}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\varphi\\}$
and $Fm_{FC_{int}}:=\\{\varphi\in
Fm(\mathbf{KF})_{s_{2}}\mid\leavevmode\nobreak\
\models^{\mathfrak{C}}_{s_{2}}{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\varphi\leftrightarrow\varphi\\}$.
Hence, the set $Fm_{FC}$ provides a logical representation of formal concepts
induced from the context $(G,M,I)$.

##  3\. Logical representation of three concept lattices

We have seen that a certain pairs of formulas in the logic KF and KB can
represent formal and rough concepts respectively. The observation suggests the
definition below.

###### Definition 3.1.

Let $\varphi\in Fm(\textbf{KB})_{s_{1}}$, $\psi\in Fm(\textbf{KB})_{s_{2}}$,
$\eta\in Fm(\textbf{KF})_{s_{1}}$, and $\gamma\in Fm(\textbf{KF})_{s_{2}}$.
Then, for a context $\mathbb{K}$, we say that

  * (a)

$(\varphi,\psi)$ is a (logical) property oriented concept of $\mathbb{K}$ if
$(\varphi,\psi)\in Fm_{PC}$.

  * (b)

$(\varphi,\psi)$ is a (logical) object oriented concept of $\mathbb{K}$ if
$(\varphi,\psi)\in Fm_{OC}$.

  * (c)

$(\eta,\gamma)$ is a (logical) formal concept of $\mathbb{K}$ if
$(\eta,\gamma)\in Fm_{FC}$.

We now explore the relationships between the three notions and their
properties. In what follows, for a context $\mathbb{K}=(G,M,I)$, we use
$\mathfrak{C}_{0}:=(G,M,I^{-1},I)$ and
$\mathfrak{C}_{1}:=(G,M,\overline{I^{-1}},\overline{I})$ to denote frames
corresponding to $\mathbb{K}$ and $\overline{\mathbb{K}}$ respectively.

Recall that we have defined the set $Fm_{X}$ for $X=PC,OC,FC$ with respect to
a context $\mathbb{K}$, but for simplicity, we do not explicitly attach it to
the notation. In what follows, we will use $Fm_{X}^{c}$ for $X=PC,OC,FC$ to
denote the corresponding set defined with respect to $\overline{\mathbb{K}}$.

###### Proposition 3.2.

Let $\mathbb{K}:=(G,M,I)$ be a context. Then,

  * (a)

$(\varphi,\psi)\in Fm_{PC}$ iff $(\neg\varphi,\neg\psi)\in Fm_{OC}$ for
$\varphi\in Fm(\textbf{KB})_{s_{1}}$ and $\psi\in Fm(\textbf{KB})_{s_{2}}$.

  * (b)

$(\varphi,\psi))\in Fm_{FC}$ iff $(\rho(\varphi),\neg\rho(\psi))\in
Fm^{c}_{PC}$ for $\varphi\in Fm(\textbf{KF})_{s_{1}}$ and $\psi\in
Fm(\textbf{KF})_{s_{2}}$.

  * (c)

$(\varphi,\psi)\in Fm_{FC}$ iff $(\neg\rho(\varphi),\rho(\psi))\in
Fm^{c}_{OC}$ for $\varphi\in Fm(\textbf{KF})_{s_{1}}$ and $\psi\in
Fm(\textbf{KF})_{s_{2}}$.

###### Proof.

  * (a)

By using (Dual) and propositional reasoning, we have $(\varphi,\psi)\in
Fm_{PC}$ iff
$\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi\leftrightarrow{\Box_{\mathfrak{m}}}\psi$
and
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow\psi$
iff
$\models^{\mathfrak{C}_{0}}_{s_{1}}\neg\varphi\leftrightarrow{\Diamond_{\mathfrak{m}}}\neg\psi$
and
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\Box_{\mathfrak{g}}}\neg\varphi\leftrightarrow\neg\psi$
iff $(\neg\varphi,\neg\psi)\in Fm_{OC}$.

  * (b)

Because $(\varphi,\psi)$ is a formal concept, we have
$\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
and
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$.
By Theorem 2.8 (b), we can derive
$\models^{\mathfrak{C}_{1}}_{s_{1}}\rho(\varphi)\leftrightarrow{\Box_{\mathfrak{m}}}\neg\rho(\psi)$
and
$\models^{\mathfrak{C}_{1}}_{s_{2}}{\Diamond_{\mathfrak{g}}}\rho(\varphi)\leftrightarrow\neg\rho(\psi)$.
Therefore, $(\rho(\varphi),\neg\rho(\psi))$ is a property oriented concept for
$\overline{\mathbb{K}}$. The proof for the converse direction is similar.

  * (c)

It follows from (a) and (b) immediately.

∎

Now, we can define a relation $\equiv_{1}$ on the set $Fm_{PC}$ as follows:
For $(\varphi,\psi),(\varphi^{\prime},\psi^{\prime})\in Fm_{PC}$,
$(\varphi,\psi)\equiv_{1}(\varphi^{\prime},\psi^{\prime})$ iff
$\models^{\mathfrak{C}_{0}}\varphi\leftrightarrow\varphi^{\prime}$. We will
denote the equivalence class of $\equiv_{1}$ by
$[(\varphi,\psi)]_{\equiv_{1}}$ and usually omit the subscript when the
equivalence relation is clear.

Analogously, we can define $\equiv_{2}$ and $\equiv_{3}$ on the set $Fm_{OC}$
and $Fm_{FC}$, respectively. Obviously, $\equiv_{1},\equiv_{2}$ and
$\equiv_{3}$ are all equivalence relations. Let
$Fm_{PC}/\equiv_{1},Fm_{OC}/\equiv_{2}$, and $Fm_{FC}/\equiv_{3}$ be the sets
of equivalence classes.

###### Proposition 3.3.

For $(\varphi,\psi),(\varphi^{\prime},\psi^{\prime})\in Fm_{X}$,
$(\varphi,\psi)\equiv_{i}(\varphi^{\prime},\psi^{\prime})$ iff
$\models^{\mathfrak{C}_{0}}\psi\leftrightarrow\psi^{\prime}$, where $i=1,2,3$
for $X=PC,OC,FC$ respectively.

###### Proof.

Let us prove the case of $FC$ as an example. Suppose
$(\varphi,\psi),(\varphi^{\prime},\psi^{\prime})\in Fm_{FC}$ and
$(\varphi,\psi)\equiv_{3}(\varphi^{\prime},\psi^{\prime})$. Then,
$\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi\leftrightarrow\varphi^{\prime}$,
which implies
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{g}}}\varphi^{\prime}$
according to the semantics of KF. In addition, by definition of $Fm_{FC}$,
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$,
and
$\models^{\mathfrak{C}_{0}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi^{\prime}\leftrightarrow\psi^{\prime}$.
Hence, $\models^{\mathfrak{C}_{0}}_{s_{2}}\psi\leftrightarrow\psi^{\prime}$.

Proofs for other two cases are similar. ∎

###### Proposition 3.4.

Let $X\in\\{PC_{ext},OC_{ext},FC_{ext}\\}$ and
$Y\in\\{PC_{int},OC_{int},FC_{int}\\}$. Then,

  * (a)

$Fm_{X}$ and $Fm_{Y}$ are closed under conjunction.

  * (b)

If $\varphi\in Fm_{X}$ and $\psi\in Fm_{Y}$, then
$\circ_{\mathfrak{g}}\varphi\in Fm_{Y}$ and $\circ_{\mathfrak{m}}\psi\in
Fm_{X}$, where $\circ\in\\{\boxminus,\Box,\Diamond\\}$ depending on $X$ and
$Y$ according to their respective definitions.

.

###### Proof.

  * (a).

We prove the case of $Fm_{FC_{ext}}$ as an example and other cases can be
proved in a similar way. Let $\varphi,\varphi^{\prime}\in Fm_{FC_{ext}}$.
Then,
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\varphi$
and
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi^{\prime}\leftrightarrow\varphi^{\prime}$.
By using the translation $\rho$ and Theorem 2.8, we have both
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime})\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi$
and
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime})\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi^{\prime}$.
Hence, we can derive
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime})\rightarrow(\varphi\wedge\varphi^{\prime})$.
Also, with the translation, we have
$\models^{\mathfrak{C}_{0}}_{s_{1}}(\varphi\wedge\varphi^{\prime})\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime})$
because the formula is mapped to an instance of axiom (B). Hence,
$\varphi\wedge\varphi^{\prime}\in Fm_{FC_{ext}}$.

  * (b).

Let us prove the case of $\varphi\in Fm_{FC_{ext}}$ as an example. Assume that
$\varphi\in Fm_{FC_{ext}}$ and $\circ=\boxminus$. Then, according to the
semantics of ${\boxminus_{\mathfrak{g}}}$,
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\varphi$
implies
$\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{g}}}\varphi$.
Hence ${\boxminus_{\mathfrak{g}}}\varphi\in Fm_{FC_{int}}$. Similarly, if
$\psi\in Fm_{FC_{int}}$, then ${\boxminus_{\mathfrak{m}}}\psi\in
Fm_{FC_{ext}}$.

∎

From the proposition, we can derive the following corollary immediately.

###### Corollary 3.5.

  * (a)

$(\varphi_{1},\psi_{1}),(\varphi_{2},\psi_{2})\in Fm_{PC}$ implies that
$(\varphi_{1}\wedge\varphi_{2},{\Diamond_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{2}))$
and $({\Box_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),\psi_{1}\wedge\psi_{2})\in
Fm_{PC}$.

  * (b)

$(\varphi_{1},\psi_{1}),(\varphi_{2},\psi_{2})\in Fm_{OC}$ implies that
$(\varphi_{1}\wedge\varphi_{2},{\Box_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{2}))$
and
$({\Diamond_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),\psi_{1}\wedge\psi_{2})\in
Fm_{OC}$.

  * (c)

$(\varphi_{1},\psi_{1}),(\varphi_{2},\psi_{2})\in Fm_{FC}$ implies that
$(\varphi_{1}\wedge\varphi_{2},{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{2}))$
and
$({\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),\psi_{1}\wedge\psi_{2})\in
Fm_{FC}$.

Now we can define the following structures:

  * •

$(Fm_{PC}/\equiv_{1},\vee_{1},\wedge_{1})$ where

    * –

$[(\varphi,\psi)]\vee_{1}[(\varphi^{\prime},\psi^{\prime})]:=[({\Box_{\mathfrak{m}}}(\psi\wedge\psi^{\prime}),(\psi\wedge\psi^{\prime}))]$

    * –

$[(\varphi,\psi)]\wedge_{1}[(\varphi^{\prime},\psi^{\prime})]:=[(\varphi\wedge\varphi^{\prime},{\Diamond_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime}))]$

  * •

$(Fm_{OC}/\equiv_{2},\vee_{2},\wedge_{2})$ where

    * –

$[(\varphi,\psi)]\vee_{2}[(\varphi^{\prime},\psi^{\prime})]:=[({\Diamond_{\mathfrak{m}}}(\psi\wedge\psi^{\prime}),(\psi\wedge\psi^{\prime}))]$

    * –

$[(\varphi,\psi)]\wedge_{2}[(\varphi^{\prime},\psi^{\prime})]:=[(\varphi\wedge\varphi^{\prime},{\Box_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime}))]$

  * •

$(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$ where

    * –

$[(\varphi,\psi)]\vee_{3}[(\varphi^{\prime},\psi^{\prime}]):=[({\boxminus_{\mathfrak{m}}}(\psi\wedge\psi^{\prime}),(\psi\wedge\psi^{\prime}))]$

    * –

$[(\varphi,\psi)]\wedge_{3}[(\varphi^{\prime},\psi^{\prime})]:=[(\varphi\wedge\varphi^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime}))]$

###### Theorem 3.6.

For a context $\mathbb{K}$, $(Fm_{PC}/\equiv_{1},\vee_{1},\wedge_{1})$,
$(Fm_{OC}/\equiv_{2},\vee_{2},\wedge_{2})$ and
$(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$, are lattices.

###### Proof.

We give proof for the structure $(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$ and
the proofs of other cases are similar. Let $(\varphi_{1},\psi_{1})$,
$(\varphi_{2},\psi_{2})$, $(\varphi_{1}^{\prime}$, $\psi_{1}^{\prime})$,
$(\varphi^{\prime}_{2},\psi^{\prime}_{2})\in Fm_{FC}$ such that
$(\varphi_{1},\psi_{1})\equiv_{3}(\varphi_{2},\psi_{2})$ and
$(\varphi_{1}^{\prime},\psi_{1}^{\prime})\equiv_{3}(\varphi^{\prime}_{2},\psi^{\prime}_{2})$.
By Corollary 3.5,
$(\varphi_{1}\wedge\varphi_{1}^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{1}^{\prime})),({\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{1}^{\prime}),\psi_{1}\wedge\psi_{1}^{\prime}),(\varphi_{2}\wedge\varphi_{2}^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi_{2}\wedge\varphi_{2}^{\prime}))$
and
$({\boxminus_{\mathfrak{m}}}(\psi_{2}\wedge\psi_{2}^{\prime}),\psi_{2}\wedge\psi_{2}^{\prime})\in
Fm_{FC}$. Now $(\varphi_{1},\psi_{1})\equiv_{3}(\varphi_{2},\psi_{2})$ and
$(\varphi_{1}^{\prime},\psi_{1}^{\prime})\equiv_{3}(\varphi^{\prime}_{2},\psi^{\prime}_{2})$
implies that $\models^{\mathfrak{C}_{0}}\varphi_{1}\leftrightarrow\varphi_{2}$
and
$\models^{\mathfrak{C}_{0}}\varphi_{1}^{\prime}\leftrightarrow\varphi_{2}^{\prime}$.
By Proposition 3.3, we have
$\models^{\mathfrak{C}_{0}}\psi_{1}\leftrightarrow\psi_{2}$ and
$\models^{\mathfrak{C}_{0}}\psi_{1}^{\prime}\leftrightarrow\psi_{2}^{\prime}$.
This leads to
$\models^{\mathfrak{C}_{0}}\varphi_{1}\wedge\varphi_{1}^{\prime}\leftrightarrow\varphi_{2}\wedge\varphi_{2}^{\prime}$
and
$\models^{\mathfrak{C}_{0}}\psi_{1}\wedge\psi_{1}^{\prime}\leftrightarrow\psi_{2}\wedge\psi_{2}^{\prime}$
which implies that
$(\varphi_{1}\wedge\varphi_{1}^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{1}^{\prime}))\equiv_{3}(\varphi_{2}\wedge\varphi_{2}^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi_{2}\wedge\varphi_{2}^{\prime}))$
and
$({\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{1}^{\prime}),\psi_{1}\wedge\psi_{1}^{\prime})\equiv_{3}({\boxminus_{\mathfrak{m}}}(\psi_{2}\wedge\psi_{2}^{\prime}),\psi_{2}\wedge\psi_{2}^{\prime})$.
Hence, $\wedge_{3}$ and $\vee_{3}$ are well-defined operations. Their
commutativity and associativity follow from the fact that
$\vdash^{\textbf{KF}}\varphi\wedge\psi\leftrightarrow\psi\wedge\varphi$ and
$\vdash^{\textbf{KF}}(\varphi\wedge\psi)\wedge\gamma\leftrightarrow\varphi\wedge(\psi\wedge\gamma)$.
Now we will show that for all
$[(\varphi_{1},\psi_{1})],[(\varphi_{2},\psi_{2})]\in Fm_{FC}/\equiv_{3}$,
$[(\varphi_{1},\psi_{1})]\wedge_{3}([\varphi_{1},\psi_{1}]\vee_{3}[(\varphi_{2},\psi_{2})])=[(\varphi_{1},\psi_{1})]$
which is equivalent to
$[(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{1})))]=[(\varphi_{1},\psi_{1})]$.
We know that
$\models^{\mathfrak{C}_{0}}\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})\rightarrow\varphi_{1}$.
In addition,

$\displaystyle\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi_{1}\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi_{1}\leavevmode\nobreak\
\mbox{as}\leavevmode\nobreak\ (\varphi_{1},\psi_{1})\in Fm_{FC}$
$\displaystyle\models^{\mathfrak{C}_{0}}_{s_{2}}\psi_{1}\wedge\psi_{2}\rightarrow\psi_{1}$
$\displaystyle\models^{\mathfrak{C}_{0}}_{s_{1}}{\boxminus_{\mathfrak{m}}}\psi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})\leavevmode\nobreak\
\mbox{by Proposition \ref{needproflattic}}$
$\displaystyle\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})$
$\displaystyle\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi_{1}\rightarrow\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})$

So
$\models^{\mathfrak{C}_{0}}_{s_{1}}\varphi_{1}\leftrightarrow\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})$
which implies that
$[(\varphi_{1},\psi_{1})]\wedge_{3}([\varphi_{1},\psi_{1}]\vee_{3}[(\varphi_{2},\psi_{2})])=[(\varphi_{1},{\boxminus_{\mathfrak{g}}}\varphi_{1})]=[(\varphi_{1},\psi_{1})]$
as the last term is in $Fm_{PC}/\equiv_{3}$. Analogously, we can show that
$[(\varphi_{1},\psi_{1})]\vee_{3}([\varphi_{1},\psi_{1}]\wedge_{3}[(\varphi_{2},\psi_{2})])=[(\varphi_{1},\psi_{1})]$.
Hence $(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$ is a lattice. ∎

###### Theorem 3.7.

Let us consider a context $\mathbb{K}$ and its complement
$\overline{\mathbb{K}}$. Then, for lattices defined above, we have

  * (a)

$(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$ and
$(Fm_{PC}^{c}/\equiv_{1},\vee_{1},\wedge_{1})$ are isomorphic.

  * (b)

$(Fm_{PC}/\equiv_{1},\vee_{1},\wedge_{1})$ and
$(Fm_{OC}/\equiv_{2},\vee_{2},\wedge_{2})$ are dually isomorphic.

  * (c)

$(Fm_{FC}/\equiv_{3},\vee_{3},\wedge_{3})$ and
$(Fm^{c}_{OC}/\equiv_{2},\vee_{2},\wedge_{2})$ are dually isomorphic.

###### Proof.

(a) By Proposition 3.2, the mapping $h:Fm_{FC}/\equiv_{3}\rightarrow
Fm_{PC}^{c}/\equiv_{1}$ defined by
$h([(\varphi,\psi)]):=[(\rho(\varphi),\rho(\neg\psi))]$ is well-defined and
surjective. Now $h([(\varphi_{1},\psi_{1})])=h([(\varphi_{2},\psi_{2})])$
implies
$[\rho((\varphi_{1}),\rho(\neg\psi_{1}))]=[(\rho(\varphi_{2}),\rho(\neg\psi_{2}))]$,
which in turn implies
$\models^{\mathfrak{C}_{1}}\rho(\varphi_{1})\leftrightarrow\rho(\varphi_{2})$,
and by Theorem 2.8,
$\models^{\mathfrak{C}_{0}}\varphi_{1}\leftrightarrow\varphi_{2}$. This means
that $[(\varphi_{1},\psi_{1})]=[(\varphi_{2},\psi_{2})]$. Thus, $h$ is
injective, and as a result, $h$ is a bijection. In addition,

$\displaystyle h([(\varphi_{1},\psi_{1})]\wedge_{3}[(\varphi_{2},\psi_{2})])$
$\displaystyle=h([(\varphi_{1}\wedge\varphi_{2},{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{2}))])$
$\displaystyle=[(\rho(\varphi_{1}\wedge\varphi_{2}),\rho(\neg{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge\varphi_{2})))]$
$\displaystyle=[(\rho(\varphi_{1}\wedge\varphi_{2}),{\Diamond_{\mathfrak{g}}}\rho(\varphi_{1}\wedge\varphi_{2}))]$
$\displaystyle=[(\rho(\varphi_{1})\wedge\rho(\varphi_{2}),{\Diamond_{\mathfrak{g}}}[\rho(\varphi_{1})\wedge\rho(\varphi_{2}))]$
$\displaystyle=h([(\varphi_{1},\psi_{1})])\wedge_{1}h([(\varphi_{2},\psi_{2})])$

Analogously, we also have
$h([(\varphi_{1},\psi_{1})]\vee_{3}[(\varphi_{2},\psi_{2})])=h([(\varphi_{1},\psi_{1})])\vee_{1}h([(\varphi_{2},\psi_{2})])$.
Therefore, $h$ is an isomorphism.

(b) In a similar way, we can show that $f:Fm_{PC}/\equiv_{1}\rightarrow
Fm_{OC}/\equiv_{1}$ defined by $f([(\varphi,\psi)]):=[(\neg\varphi,\neg\psi)]$
is a dual isomorphism.

(c) It follows from (a) and (b) immediately. ∎

##  4\. Two-sorted Boolean Modal logic

We have seen that KB and KF can respectively represent and reason about rough
and formal concepts in a context. However, we can only do that in two separate
logical systems. In this section, we develop a uniform framework that can deal
with both formal and rough concepts at the same time. By mixing possibility
and window modalities together, we can express combinations of both kinds of
concepts. Specifically, we consider two-sorted signature
$(\\{s_{1},s_{2}\\},\\{{\Box_{\mathfrak{g}}},{\Box_{\mathfrak{m}}},{\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}\\})$,
where
$\Sigma_{s_{1}s_{2}}=\\{{\Box_{\mathfrak{g}}},{\boxminus_{\mathfrak{g}}}\\}$
and
$\Sigma_{s_{2}s_{1}}=\\{{\Box_{\mathfrak{m}}},{\boxminus_{\mathfrak{m}}}\\}$.
The indexed family of formulas is denoted by
$Fm(\textbf{BM}):=\\{Fm(\textbf{BM})_{s_{i}}\mid i=1,2\\}$. The formulas are
interpreted in generalized context-based model defined below.

###### Definition 4.1.

A generalized context-based model (or simply generalized model) is a 5-tuple
$\mathfrak{M}:=(G,M,I,J,v)$, where both $(G,M,I)$ and $(G,M,J)$ are contexts,
$I\cup J=G\times M$, and $v$ is a two-sorted valuation.

We define the satisfaction of BM formulas in $\mathfrak{M}$ inductively as
above. For propositional connectives, and modal operators
${\Box_{\mathfrak{g}}},{\Box_{\mathfrak{m}}}$, the definition remains the same
as that for the satisfaction of KB formulas in the context-based model
$\mathfrak{M}:=(G,M,I,v)$. For modal operators
${\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}$, we have

  1. (1)

for $\varphi\in Fm(\textbf{BM})_{s_{1}}$ and $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi$ iff for all
$g\in G$, $\mathfrak{M},g\models_{s_{1}}\varphi$ implies that $\neg Jgm$;

  2. (2)

for $\psi\in Fm(\textbf{BM})_{s_{2}}$ and $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\boxminus_{\mathfrak{m}}}\psi$ iff for all
$m\in M$, $\mathfrak{M},m\models_{s_{2}}\psi$ implies that $\neg Jgm$.

As in the case of Boolean modal logic (Gargov1987, ), we define the following
operators: for $\varphi_{1},\varphi_{2}\in Fm(\textbf{BM})_{s_{1}}$,
$N_{\mathfrak{g}}(\varphi_{1},\varphi_{2}):={\Box_{\mathfrak{g}}}\varphi_{1}\wedge{\boxminus_{\mathfrak{g}}}\neg\varphi_{2}$
and
$[\mathsf{U}_{\mathfrak{g}}]\varphi_{1}:=N_{\mathfrak{g}}(\varphi_{1},\varphi_{1})$.
Similarly, for $\psi_{1},\psi_{2}\in Fm(\textbf{BM})_{s_{2}}$,
$N_{\mathfrak{m}}(\psi_{1},\psi_{2}):={\Box_{\mathfrak{m}}}\psi_{1}\wedge{\boxminus_{\mathfrak{m}}}\neg\psi_{2}$
and
$[\mathsf{U}_{\mathfrak{m}}]\psi_{1}:=N_{\mathfrak{m}}(\psi_{1},\psi_{1})$. We
also define the following operators:
${\overline{\Box}_{\mathfrak{g}}}\varphi:={\boxminus_{\mathfrak{g}}}\neg\varphi$,
${\overline{\Box}_{\mathfrak{m}}}\varphi:={\boxminus_{\mathfrak{m}}}\neg\varphi$,
${\overline{\boxminus}_{\mathfrak{g}}}\varphi:={\Box_{\mathfrak{g}}}\neg\varphi$
and
${\overline{\boxminus}_{\mathfrak{m}}}\varphi:={\Box_{\mathfrak{m}}}\neg\varphi$

The logic system $\mathbf{BM}:=\\{\mathbf{BM}_{s_{1}},\mathbf{BM}_{s_{2}}\\}$
consist of all axioms and inference rules of KF and KB as well as the axioms
given in Figure 3.

($N_{\mathfrak{g}}$) $N_{\mathfrak{g}}(\varphi_{1},\varphi_{2})\wedge
N_{\mathfrak{g}}(\varphi_{1}\rightarrow\psi_{1},\varphi_{2}\rightarrow\psi_{2})\rightarrow
N_{\mathfrak{g}}(\psi_{1},\psi_{2})$
for $\varphi_{1},\varphi_{2},\psi_{1},\psi_{2}\in Fm(\mathbf{BM})_{s_{1}}$
($N_{\mathfrak{m}}$) $N_{\mathfrak{m}}(\varphi_{1},\varphi_{2})\wedge
N_{\mathfrak{m}}(\varphi_{1}\rightarrow\psi_{1},\varphi_{2}\rightarrow\psi_{2})\rightarrow
N_{\mathfrak{m}}(\psi_{1},\psi_{2})$
for $\varphi_{1},\varphi_{2},\psi_{1},\psi_{2}\in Fm(\mathbf{BM})_{s_{2}}$
($\mathsf{U}_{\mathfrak{g}}$)
$[\mathsf{U}_{\mathfrak{g}}]\varphi\rightarrow[\mathsf{U}_{\mathfrak{g}}][\mathsf{U}_{\mathfrak{m}}][\mathsf{U}_{\mathfrak{g}}]\varphi$,
for $\varphi\in Fm(\mathbf{BM})_{s_{1}}$ ($\mathsf{U}_{\mathfrak{m}}$)
$[\mathsf{U}_{\mathfrak{m}}]\varphi\rightarrow[\mathsf{U}_{\mathfrak{m}}][\mathsf{U}_{\mathfrak{g}}][\mathsf{U}_{\mathfrak{m}}]\varphi$,
for $\varphi\in Fm(\mathbf{BM})_{s_{2}}$

Figure 3. The axiomatic system BM

###### Lemma 4.2.

Let $\mathfrak{M}=(G,M,I,J,v)$ be a generalized model, $\varphi\in
Fm(\textbf{BM})_{s_{1}}$ and $\psi\in Fm(\textbf{BM})_{s_{2}}$. The following
holds.

  * (a)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}[\mathsf{U}_{\mathfrak{g}}]\varphi$ iff for all
$g\in G(Igm\leavevmode\nobreak\ \mbox{or}\leavevmode\nobreak\
Jgm\implies\mathfrak{M},g\models_{s_{1}}\varphi)$.

  * (b)

For $g\in G$, $\mathfrak{M},g\models_{s_{1}}[\mathsf{U}_{\mathfrak{m}}]\psi$
iff for all $m\in M(Igm\leavevmode\nobreak\ \mbox{or}\leavevmode\nobreak\
Jgm\implies\mathfrak{M},m\models_{s_{2}}\psi)$.

  * (c)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\overline{\Box}_{\mathfrak{g}}}\varphi$ iff for
all $g\in G$, $(Jgm\implies\mathfrak{M},g\models_{s_{1}}\varphi)$.

  * (d)

For $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\overline{\Box}_{\mathfrak{m}}}\psi$ iff for
all $m\in M$, $(Jgm\implies\mathfrak{M},m\models_{s_{2}}\psi)$

  * (e)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\overline{\boxminus}_{\mathfrak{g}}}\varphi$
iff for all $g\in G$, $(\mathfrak{M},g\models_{s_{1}}\varphi\implies\neg
Igm)$.

  * (f)

For $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\overline{\boxminus}_{\mathfrak{m}}}\psi$ iff
for all $m\in M$, $(\mathfrak{M},m\models_{s_{2}}\psi\implies\neg Igm)$.

###### Proof.

Proof of (b) is similar to the proof of (a). Here we give proof for $(a)$. Let
$m\in M$. Then,
$\mathfrak{M},m\models_{s_{2}}[\mathsf{U}_{\mathfrak{g}}]\varphi$ is
equivalent to
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\varphi\wedge{\boxminus_{\mathfrak{g}}}\neg\varphi$,
which is equivalent to that for all $g\in G$, $Igm$ implies that
$\mathfrak{M},g\models_{s_{1}}\varphi$ and for all $g\in G$,
$\mathfrak{M},g\models_{s_{1}}\neg\varphi$ implies that $\neg Jgm$, which is
equivalent to that for all $g\in G$ ($Igm$ implies that
$\mathfrak{M},g\models_{s_{1}}\varphi$ and $Jgm$ implies that
$\mathfrak{M},g\models_{s_{1}}\varphi$), which is equivalent to that for all
$g\in G$ ($Igm$ or $Jgm$ implies that $\mathfrak{M},g\models_{s_{1}}\varphi$
).

Proofs of $(c),(d),(e)$ and $(f)$ follow from the definition. ∎

###### Theorem 4.3.

The logic BM is sound with respect to the class of all generalized context-
based models.

###### Proof.

To prove this theorem it is sufficient to show that all the axiom in Figure 3
are valid. Proofs for $(N_{\mathfrak{m}})$ and $(\mathsf{U}_{\mathfrak{m}})$
are similar to those for $(N_{\mathfrak{g}})$ and
$(\mathsf{U}_{\mathfrak{g}})$ respectively. Hence, we only present proofs for
$(N_{\mathfrak{g}})$ and $(\mathsf{U}_{\mathfrak{g}})$.

For the former, let $\mathfrak{M}=(G,M,I,J,v)$ be a generalized model. Then,
for any $m\in M$,
$\mathfrak{M},m\models_{s_{2}}N_{\mathfrak{g}}(\varphi_{1},\varphi_{2})\wedge
N_{\mathfrak{g}}(\varphi_{1}\rightarrow\psi_{1},\varphi_{2}\rightarrow\psi_{2})$
implies that
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\varphi_{1}\wedge{\boxminus_{\mathfrak{g}}}\neg\varphi_{2}$
and
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}(\varphi_{1}\rightarrow\psi_{1})\wedge{\boxminus_{\mathfrak{g}}}\neg(\varphi_{2}\rightarrow\psi_{2})$
by definition. This is equivalent to
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\varphi_{1}$,
$\mathfrak{M},m\models_{s_{2}}{\overline{\Box}_{\mathfrak{g}}}\varphi_{2}$,
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}(\varphi_{1}\rightarrow\psi_{1})$
and
$\mathfrak{M},m\models_{s_{2}}{\overline{\Box}_{\mathfrak{g}}}(\varphi_{2}\rightarrow\psi_{2})$.
By Lemma 4.2, we have
$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}}\psi_{1}\wedge{\overline{\Box}_{\mathfrak{g}}}\psi_{2}$,
which is equivalent to
$\mathfrak{M},m\models_{s_{2}}N_{\mathfrak{g}}(\varphi_{2},\psi_{2})$.

For the latter, assume
$\mathfrak{M},m_{0}\models_{s_{2}}[\mathsf{U}_{\mathfrak{g}}]\varphi$ for some
$m_{0}\in M$. Then, by Lemma 4.2, for all $g\in G$ ($Igm_{0}$ or
$Jgm_{0}\implies\mathfrak{M},g\models_{s_{1}}\varphi$), which implies that for
all $g\in G$, $\mathfrak{M},g\models_{s_{1}}\varphi$ as $I\cup J=G\times M$.
Hence, for all $m\in M$,
$\mathfrak{M},m\models_{s_{2}}[\mathsf{U}_{\mathfrak{g}}]\varphi$, which in
turn implies for all $g\in G$,
$\mathfrak{M},g\models_{s_{1}}[\mathsf{U}_{\mathfrak{m}}][\mathsf{U}_{\mathfrak{g}}]\varphi$
and for all $m\in M$ (and thus $m_{0}$),
$\mathfrak{M},m\models_{s_{2}}[\mathsf{U}_{\mathfrak{g}}][\mathsf{U}_{\mathfrak{m}}][\mathsf{U}_{\mathfrak{g}}]\varphi$.
∎

To prove completeness result, we construct a canonical model. Let $G$ and $M$
be the sets of all maximally consistent subsets of $Fm(\mathbf{BM})_{s_{1}}$
and $Fm(\mathbf{BM})_{s_{2}}$ respectively. Then, for all $X\in G$ and $Y\in
M$, we define the following sets of formulas.

${\Box_{\mathfrak{m}}}X:=\\{\varphi\mid{\Box_{\mathfrak{m}}}\varphi\in X\\}$,
${\boxminus_{\mathfrak{m}}}\neg
X:=\\{\varphi\mid{\boxminus_{\mathfrak{m}}}\neg\varphi\in X\\}$, and
$[\mathsf{U}_{\mathfrak{m}}]X:=\\{\varphi\mid[\mathsf{U}_{\mathfrak{m}}]\varphi\in
X\\}$.

${\Box_{\mathfrak{g}}}Y:=\\{\varphi\mid{\Box_{\mathfrak{g}}}\varphi\in Y\\}$,
${\boxminus_{\mathfrak{g}}}\neg
Y:=\\{\varphi\mid{\boxminus_{\mathfrak{g}}}\neg\varphi\in Y\\}$, and
$[\mathsf{U}_{\mathfrak{g}}]Y:=\\{\varphi\mid[\mathsf{U}_{\mathfrak{g}}]\varphi\in
Y\\}$.

###### Lemma 4.4.

For $X\in G$ and $Y\in M$,
$[\mathsf{U}_{\mathfrak{m}}]X={\Box_{\mathfrak{m}}}X\cap{\boxminus_{\mathfrak{m}}}\neg
X$ and
$[\mathsf{U}_{\mathfrak{g}}]Y={\Box_{\mathfrak{g}}}Y\cap{\boxminus_{\mathfrak{g}}}\neg
Y$.

###### Proof.

$\varphi\in[\mathsf{U}_{\mathfrak{m}}]X$ iff
$[\mathsf{U}_{\mathfrak{m}}]\varphi\in X$ iff
${\Box_{\mathfrak{m}}}\varphi\wedge{\boxminus_{\mathfrak{m}}}\neg\varphi\in X$
iff ${\Box_{\mathfrak{m}}}\varphi\in X$ and
${\boxminus_{\mathfrak{m}}}\neg\varphi\in X$, as $X$ is a maximally consistent
set. Hence, $\varphi\in[\mathsf{U}_{\mathfrak{m}}]X$ iff
$\varphi\in{\Box_{\mathfrak{m}}}X$ and
$\varphi\in{\boxminus_{\mathfrak{m}}}\neg X$, i.e.,
$\varphi\in{\Box_{\mathfrak{m}}}X\cap{\boxminus_{\mathfrak{m}}}\neg X$.
Therefore
$[\mathsf{U}_{\mathfrak{m}}]X={\Box_{\mathfrak{m}}}X\cap{\boxminus_{\mathfrak{m}}}\neg
X$. The proof of
$[\mathsf{U}_{\mathfrak{g}}]Y={\Box_{\mathfrak{g}}}Y\cap{\boxminus_{\mathfrak{g}}}\neg
Y$ is similar. ∎

###### Lemma 4.5.

For all $X\in G$ and $Y\in M$,

  * (a)

${\Box_{\mathfrak{m}}}X\subseteq Y$ iff ${\Box_{\mathfrak{g}}}Y\subseteq X$ ,

  * (b)

${\boxminus_{\mathfrak{m}}}\neg X\subseteq Y$ iff
${\boxminus_{\mathfrak{g}}}\neg Y\subseteq X$,

  * (c)

$[\mathsf{U}_{\mathfrak{m}}]X\subseteq Y$ iff ${\Box_{\mathfrak{m}}}X\subseteq
Y$ or ${\boxminus_{\mathfrak{m}}}\neg X\subseteq Y$

  * (d)

$[\mathsf{U}_{\mathfrak{g}}]Y\subseteq X$ iff ${\Box_{\mathfrak{g}}}Y\subseteq
X$ or ${\boxminus_{\mathfrak{g}}}\neg Y\subseteq X$

  * (e)

$[\mathsf{U}_{\mathfrak{m}}]X\subseteq Y$ iff
$[\mathsf{U}_{\mathfrak{g}}]Y\subseteq X$.

###### Proof.

  * (a)

Assume that ${\Box_{\mathfrak{m}}}X\subseteq Y$ but
${\Box_{\mathfrak{g}}}Y\not\subseteq X$. Then there exists $s_{1}$-sort
formula $\psi$ such that $\psi\in{\Box_{\mathfrak{g}}}Y$ and $\psi\notin X$.
$\psi\in{\Box_{\mathfrak{g}}}Y$ implies that ${\Box_{\mathfrak{g}}}\psi\in Y$
and $\psi\notin X$ implies that $\neg\psi\in X$, as $X$ is maximally
consistent. In addition, the maximal consistency of $X$ implies
$\neg\psi\rightarrow{\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\neg\psi\in
X$. Hence, we have ${\Box_{\mathfrak{m}}}{\Diamond_{\mathfrak{g}}}\neg\psi\in
X$ which implies that
${\Diamond_{\mathfrak{g}}}\neg\psi\in{\Box_{\mathfrak{m}}}X\subseteq Y$.
However, ${\Diamond_{\mathfrak{g}}}\neg\psi\in Y$ implies that
$\neg{\Box_{\mathfrak{g}}}\psi\in Y$ which is in contradiction with
${\Box_{\mathfrak{g}}}\psi\in Y$. Analogously, we can show that
${\Box_{\mathfrak{g}}}Y\subseteq X$ implies ${\Box_{\mathfrak{m}}}X\subseteq
Y$.

  * (b)

Assume that ${\boxminus_{\mathfrak{g}}}\neg Y\subseteq X$ but
${\boxminus_{\mathfrak{m}}}\neg X\not\subseteq Y$. Then there exists
$s_{2}$-sort formula $\psi$ such that $\psi\in{\boxminus_{\mathfrak{m}}}\neg
X$ and $\psi\notin Y$. $\psi\in{\boxminus_{\mathfrak{m}}}\neg X$ implies that
${\boxminus_{\mathfrak{m}}}\neg\psi\in X$ and $\psi\notin Y$ implies that
$\neg\psi\in Y$, as $Y$ is maximally consistent. In addition, as
$\neg\psi\rightarrow{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\neg\psi\in
Y$, we have ${\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\neg\psi\in
Y$. Now ${\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\neg\psi\in Y$
implies that
$\neg{\boxminus_{\mathfrak{m}}}\neg\psi\in{\boxminus_{\mathfrak{g}}}\neg
Y\subseteq X$ which is a contradiction as
$\psi\in{\boxminus_{\mathfrak{m}}}\neg X$ implies that
${\boxminus_{\mathfrak{m}}}\neg\psi\in X$. Hence,
${\boxminus_{\mathfrak{g}}}\neg Y\subseteq X$ implies
${\boxminus_{\mathfrak{m}}}\neg X\subseteq Y$. The proof of the converse is
similar.

  * (c)

If ${\Box_{\mathfrak{m}}}X\subseteq Y$ or ${\boxminus_{\mathfrak{m}}}\neg
X\subseteq Y$, then
$[\mathsf{U}_{\mathfrak{m}}]X={\Box_{\mathfrak{m}}}X\cap{\boxminus_{\mathfrak{m}}}\neg
X\subseteq Y$ by Lemma 4.4. On the other hand, assume that
$[\mathsf{U}_{\mathfrak{m}}]X\subseteq Y$ but
${\Box_{\mathfrak{m}}}X\not\subseteq Y$ and ${\boxminus_{\mathfrak{m}}}\neg
X\not\subseteq Y$. Then, there exists $\varphi\in{\Box_{\mathfrak{m}}}X$ and
$\varphi\notin Y$ and there exists $\psi\in{\boxminus_{\mathfrak{m}}}\neg X$
and $\psi\notin Y$. Hence, $\varphi\vee\psi\notin Y$ as $Y$ is maximally
consistent. In addition, $\varphi\in{\Box_{\mathfrak{m}}}X$ and
$\psi\in{\boxminus_{\mathfrak{m}}}\neg X$ implies that
${\Box_{\mathfrak{m}}}\varphi\in X$ and ${\boxminus_{\mathfrak{m}}}\neg\psi\in
X$. Then, by PL, MP, ${\rm UG}_{{\Box_{\mathfrak{m}}}}$, and
$K_{{\Box_{\mathfrak{m}}}}$, we can infer that
${\Box_{\mathfrak{m}}}(\varphi\vee\psi)\in X$. Analogously, by PL, MP, ${\rm
UG}_{{\boxminus_{\mathfrak{m}}}}^{2}$, and
$K_{{\boxminus_{\mathfrak{m}}}}^{2}$, we have
${\boxminus_{\mathfrak{m}}}\neg(\varphi\vee\psi)\in X$. Therefore,
$(\varphi\vee\psi)\in{\Box_{\mathfrak{m}}}X\cap{\boxminus_{\mathfrak{m}}}\neg
X=[\mathsf{U}_{\mathfrak{m}}]X\subseteq Y$, which leads to contradiction.

  * (d)

The proof is similar to that for (c).

  * (e)

It follows immediately from (a)-(d).

∎

###### Definition 4.6.

The canonical model $\mathfrak{M}_{c}:=(G,M,I,J,v)$ is a 5-tuple where,

  * (a)

$G$ and $M$ are the sets of all maximally consistent subsets of
$Fm(\mathbf{BM})_{s_{1}}$ and $Fm(\mathbf{BM})_{s_{2}}$ respectively,

  * (b)

$I\subseteq G\times M$ is defined by $IXY$ iff
${\Box_{\mathfrak{m}}}X\subseteq Y$ (or equivalently
${\Box_{\mathfrak{g}}}Y\subseteq X$),

  * (c)

$J\subseteq G\times M$ is defined by $JXY$ iff ${\boxminus_{\mathfrak{m}}}\neg
X\subseteq Y$ (or ${\boxminus_{\mathfrak{g}}}\neg Y\subseteq X$), and

  * (d)

$v$ is the two-sorted valuation defined by $v_{s_{1}}(p_{s_{1}})=\\{X\in G\mid
p_{s_{1}}\in X\\}$ and $v_{s_{2}}(p_{s_{2}})=\\{Y\in M\mid p_{s_{2}}\in Y\\}$.

We also use $R_{c}$ to denote $I\cup J$.

###### Lemma 4.7 (Truth Lemma).

Let $\mathfrak{M}_{c}:=(G,M,I,J,v)$ be the canonical model. Then, for any
$X\in G$, $Y\in M$, $\varphi\in Fm(\mathbf{BM})_{s_{1}}$, and $\psi\in
Fm(\mathbf{BM})_{s_{2}}$, we have $\varphi\in X$ iff
$\mathfrak{M}_{c},X\models\varphi$ and $\psi\in Y$ iff
$\mathfrak{M}_{c},Y\models\psi$

###### Proof.

By induction on the complexity of formulas, the basis case follows from the
definition of $v$ and the proof for propositional connectives is
straightforward. The only interesting cases are modal formulas, but their
proof is quite standard. Hence, as an example, we only show the case of
$\varphi={\boxminus_{\mathfrak{m}}}\psi$.

On one hand, ${\boxminus_{\mathfrak{m}}}\psi\in X$ iff
${\boxminus_{\mathfrak{m}}}\neg\neg\psi\in X$ iff
$\neg\psi\in{\boxminus_{\mathfrak{m}}}\neg X$. Hence, by the definition of
$J$, $\varphi\in X$ implies that for all $Y$ such that $JXY$, $\neg\psi\in Y$
which implies $\mathfrak{M}_{c},Y\not\models\psi$ by inductive hypothesis.
This results in $\mathfrak{M}_{c},X\models\varphi$ according to the semantics
of ${\boxminus_{\mathfrak{m}}}\psi$.

On the other hand, assume that $\varphi={\boxminus_{\mathfrak{m}}}\psi\not\in
X$. Then, we show that ${\boxminus_{\mathfrak{m}}}\neg X\cup\\{\psi\\}$ is
consistent. If not, then there exists
$\\{\psi_{1}\cdots,\psi_{k}\\}\in{\boxminus_{\mathfrak{m}}}\neg X$ such that
$\vdash\neg(\bigwedge_{i=1}^{k}\psi_{i}\wedge\psi)$. As
$\psi_{i}\in{\boxminus_{\mathfrak{m}}}\neg X$ means that
${\boxminus_{\mathfrak{m}}}\neg\psi_{i}\in X$ for all $1\leq i\leq k$, by
(PL), (MP), $(UG_{\boxminus_{\mathfrak{m}}}^{2})$, and
$(K_{\boxminus_{\mathfrak{m}}}^{2})$, we can infer that
${\boxminus_{\mathfrak{m}}}\psi\in X$, which is in contradiction with the
assumption. Hence, there exists a maximally consistent extension
$Y\supseteq{\boxminus_{\mathfrak{m}}}\neg X\cup\\{\psi\\}$ that by definition
satisfies $JXY$. In addition, $\mathfrak{M}_{c},Y\models\psi$ by inductive
hypothesis. Therefore, $\mathfrak{M}_{c},X\not\models\varphi$ by the semantics
of ${\boxminus_{\mathfrak{m}}}$. ∎

###### Lemma 4.8.

  * (a)

For all $X\in G$ and $Y\in M$, $R_{c}XY$ iff
$[\mathsf{U}_{\mathfrak{m}}]X\subseteq Y$ iff
$[\mathsf{U}_{\mathfrak{g}}]Y\subseteq X$.

  * (b)

For all $X_{1},X_{2}\in G$ and $Y_{1},Y_{2}\in M$, if $R_{c}X_{1}Y_{1}$,
$R_{c}X_{1}Y_{2}$, and $R_{c}X_{2}Y_{1}$, then $R_{c}X_{2}Y_{2}$.

###### Proof.

  * (a)

It follows immediately from Definition 4.6 and Lemma 4.5.

  * (b)

Let us consider any $\varphi\in[\mathsf{U}_{\mathfrak{m}}]X_{2}$. Then,
$[\mathsf{U}_{\mathfrak{m}}]\varphi\in X_{2}$ which implies that
$[\mathsf{U}_{\mathfrak{m}}][\mathsf{U}_{\mathfrak{g}}][\mathsf{U}_{\mathfrak{m}}]\varphi\in
X_{2}$. Now, $R_{c}X_{2}Y_{1}$ implies that
$[\mathsf{U}_{\mathfrak{m}}]X_{2}\subseteq Y_{1}$. Hence
$[\mathsf{U}_{\mathfrak{g}}][\mathsf{U}_{\mathfrak{m}}]\varphi\in Y_{1}$.
Also, $R_{c}X_{1}Y_{1}$ implies that
$[\mathsf{U}_{\mathfrak{g}}]Y_{1}\subseteq X_{1}$. Thus,
$[\mathsf{U}_{\mathfrak{m}}]\varphi\in X_{1}$. Finally, $R_{c}X_{1}Y_{2}$
implies $[\mathsf{U}_{\mathfrak{m}}]X_{1}\subseteq Y_{2}$ which leads to
$\varphi\in Y_{2}$. Therefore, we have
$[\mathsf{U}_{\mathfrak{m}}]X_{2}\subseteq Y_{2}$, which is equivalent to
$R_{c}X_{2}Y_{2}$.

∎

Note that $\mathfrak{M}_{c}$ is not necessarily a generalized model because it
is possible that $R_{c}=I\cup J\not=G\times M$. However, we can construct a
generalized model from $\mathfrak{M}_{c}$ using its generated sub-model from
any element of $G\cup M$. Without loss of generality, let us consider an $X\in
G$ and define

$M_{X}:=\\{Y\in M\mid\exists X_{i},Y_{i}(0\leq i\leq
n)(X_{0}=X,Y_{n}=Y,R_{c}X_{i}Y_{i}(\forall 0\leq i\leq
n),R_{c}X_{i}Y_{i-1}(\forall 1\leq i\leq n))\\},$ $G_{X}:=\\{Z\in G\mid\exists
Y\in M_{X},R_{c}ZY\\}.$

Then, we define $\mathfrak{M}_{c}^{X}:=(G_{X},M_{X},I_{X},J_{X},v_{X})$ where
$I_{X}=I\cap(G_{X}\times M_{X})$, $J_{X}=J\cap(G_{X}\times M_{X})$, and
$v_{X}$ is the two-sorted valuation defined by
$(v_{X})_{s_{1}}(p)=v_{s_{1}}(p)\cap G_{X}$,
$(v_{X})_{s_{2}}(p)=v_{s_{1}}(p)\cap M_{X}$, for all propositional symbols
$p$, respectively.

###### Lemma 4.9.

$\mathfrak{M}_{c}^{X}$ is a generalized context-based model.

###### Proof.

By construction, we have $I_{X}\cup J_{X}\subseteq G_{X}\times M_{X}$. To
prove the converse inclusion, we first show that $R_{c}XY$ for any $Y\in
M_{X}$. By definition, $Y\in M_{X}$ implies the existence of $X_{i},Y_{i}$ for
$0\leq i\leq n$ such that $X_{0}=X$, $Y_{n}=Y$, for all $0\leq i\leq n$,
$R_{c}X_{i}Y_{i}$, and for all $1\leq i\leq n$, $R_{c}X_{i}Y_{i-1}$. By
induction on $i$, we can prove that $R_{c}XY_{i}$ for all $0\leq i\leq n$, so
in particular, $R_{c}XY_{n}$, i.e., $R_{c}XY$. The induction base is simply
$R_{c}X_{0}Y_{0}$. Now, if $R_{c}XY_{i}$ holds, then we can derive
$R_{c}XY_{i+1}$ from $R_{c}X_{i+1}Y_{i}$ and $R_{c}X_{i+1}Y_{i+1}$ by using
Lemma 4.8. Next, for any $(Z,Y)\in G_{X}\times M_{X}$, we have $R_{c}XY$ as
$Y\in M_{X}$ and there exists $Y^{\prime}\in M_{X}$ such that
$R_{c}ZY^{\prime}$ as $Z\in G_{X}$. In addition, $R_{c}XY^{\prime}$ also holds
as $Y^{\prime}\in M_{X}$. Hence, we have $R_{c}ZY$ by Lemma 4.8. Therefore,
$G_{X}\times M_{X}\subseteq R_{c}=I\cup J$, which implies $(G_{X}\times
M_{X})\subseteq I_{X}\cup J_{X}$. ∎

###### Theorem 4.10.

The logic BM is complete with respect to the class of generalized models.

###### Proof.

Let $\Phi$ be a BM-consistent subset of $Fm(\mathbf{BM})_{s_{1}}$. Then, there
exists a maximally consistent extension $X\supseteq\Phi$. By Lemma 4.9, we can
construct the generalized model $\mathfrak{M}_{c}^{X}$, and by Truth Lemma,
$\mathfrak{M}_{c}^{X},X\models\varphi$ for all $\varphi\in\Phi$. Analogously,
when $\Phi$ is a BM-consistent subset of $Fm(\mathbf{BM})_{s_{2}}$, we can
prove its satisfiability by constructing the generalized model
$\mathfrak{M}_{c}^{Y}$ where $Y\in M$ is a maximally consistent extension of
$\Phi$. Therefore, the completeness follows from Proposition 1.4. ∎

###### Theorem 4.11.

Each generalized model $\mathfrak{M}:=(G,M,I,J,v)$ is modally equivalent to
some generalized model
$\underline{\mathfrak{M}}:=(\underline{G},\underline{M},\underline{I},\underline{J},\underline{v})$
such that $\underline{I}\cap\underline{J}=\emptyset$.

###### Proof.

Let us take an isomorphic but disjoint copy
$\mathfrak{M}^{\prime}:=(G^{\prime},M^{\prime},I^{\prime},J^{\prime},v^{\prime})$
of the given model $\mathfrak{M}$. For any $g\in G$ and $m\in M$, we use
$g^{\prime}$ and $m^{\prime}$ to denote their corresponding isomorphic images
in $G^{\prime}$ and $M^{\prime}$ respectively. Then, we construct a model
$\underline{\mathfrak{M}}:=(\underline{G},\underline{M},\underline{I},\underline{J},\underline{v})$
as follows. First, $\underline{G}=G\cup G^{\prime}$, $\underline{M}=M\cup
M^{\prime}$ and $\underline{v}_{s_{i}}(p)=v_{s_{i}}(p)\cup
v_{s_{i}}^{\prime}(p)$ for propositional variables $p$ and $i=1,2$. Second, we
define the relations $\underline{I}$ and $\underline{J}$ by the following
rules:

  * •

If $Igm$ and $Jgm$, then set $\underline{I}gm^{\prime}$,
$\underline{I}g^{\prime}m$, $\underline{J}gm$, and
$\underline{J}g^{\prime}m^{\prime}$.

  * •

If $Igm$ and $\neg Jgm$, then set $\underline{I}gm$,
$\underline{I}gm^{\prime}$, $\underline{I}g^{\prime}m$, and
$\underline{I}g^{\prime}m^{\prime}$.

  * •

If $\neg Igm$ and $Jgm$, then set $\underline{J}gm$,
$\underline{J}gm^{\prime}$, $\underline{J}g^{\prime}m$, and
$\underline{J}g^{\prime}m^{\prime}$.

As $I\cup J=G\times M$, there is no possibility of $\neg Igm$ and $\neg Jgm$.
Hence, the three rules are exhaustive. By the construction, it is easy to see
that $\underline{I}\cap\underline{J}=\emptyset$ and
$\underline{I}\cup\underline{J}=\underline{G}\times\underline{M}$.

Since $\mathfrak{M}^{\prime}$ is an isomorphic copy of $\mathfrak{M}$, they
are modally equivalent. That is for any $s_{1}$ formula $\varphi$ and $s_{2}$
formula $\psi$, $\mathfrak{M},g\models\varphi$ iff
$\mathfrak{M}^{\prime},g^{\prime}\models\varphi$ and
$\mathfrak{M},m\models\psi$ iff $\mathfrak{M}^{\prime},m^{\prime}\models\psi$.

Next, we define a two-sorted mapping $f$ as
$f_{s_{1}}:\underline{G}\rightarrow G$ and $f_{s_{2}}:\underline{M}\rightarrow
M$ such that $f_{s_{1}}(g)=f_{s_{1}}(g^{\prime})=g$ and
$f_{s_{2}}(m)=f_{s_{2}}(m^{\prime})=m$. Then, $f$ is a bounded morphism from
$\underline{\mathfrak{M}}$ to $\mathfrak{M}$. Hence,
$\underline{\mathfrak{M}}$ and $\mathfrak{M}$ are modally equivalent
(blackburn2002moda, ). ∎

It is easy to see that a generalized model $\mathfrak{M}:=(G,M,I,J,v)$
satisfying $I\cap J=\emptyset$ is actually a context-based model because in
this case, $J=\overline{I}$ and the modalities
$\\{{\Box_{\mathfrak{g}}},{\Box_{\mathfrak{m}}}\\}$ and
$\\{{\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}\\}$ are interpreted
in $\mathfrak{M}$ exactly as their interpretations with $(G,M,I,v)$ in KB and
KF respectively. Hence, we reach the following conclusion.

###### Theorem 4.12.

The logic BM is sound and complete with respect to the class of all context-
based models.

###### Proof.

It follows from Theorem 4.3, 4.10 and 4.11. ∎

###### Remark 1.

Let us consider two fragments of the logic $\bf{BM}$, $\mathcal{L}_{\Box}$ and
$\mathcal{L}_{\boxminus}$, generated by
$\\{{\Box_{\mathfrak{g}}},{\Box_{\mathfrak{m}}}\\}$ and
$\\{{\boxminus_{\mathfrak{g}}},{\boxminus_{\mathfrak{m}}}\\}$ respectively.
According to Section 2.1 and 2.2, $\mathcal{L}_{\Box}$ and
$\mathcal{L}_{\boxminus}$ can syntactically represent rough and formal
concepts in contexts. Hence, the logic BM provides a unified logical framework
for the representation and reasoning about both kinds of concepts.

##  5\. Boolean modal logic and Double Boolean Algebra

In Section 3, we show that certain pairs of formulas in KF and KB can
represent formal and rough concepts respectively. As BM contains all the
logical symbols of KF and KB, it provides a uniform framework to achieve the
full expressive power of both. In this section, by utilizing such expressive
power, we first reformulate all the notions of concepts in FCA and RST with
the single framework of BM. Then, using logical representation of semiconcept
and protoconcept, we proved a representation theorem for dBa in terms of
Boolean algebras.

For a context $\mathbb{K}=(G,M,I)$, we use $\mathfrak{C}_{\mathbb{K}}$ to
denote the class of all $\mathbb{K}$-based models. Then, the following
proposition easily follows from the semantics of BM.

###### Proposition 5.1.

Let $\varphi\in Fm(\textbf{BM})_{s_{1}}$ and $\psi\in
Fm(\textbf{BM})_{s_{2}}$.

  * (a)

$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}\psi\leftrightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi$.

  * (b)

$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\rightarrow{\boxminus_{\mathfrak{m}}}({\boxminus_{\mathfrak{g}}}\varphi\wedge\psi)$.

  * (c)

$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi$.

###### Definition 5.2.

Let $\varphi\in Fm(\textbf{BM})_{s_{1}}$ and $\psi\in
Fm(\textbf{BM})_{s_{2}}$. A pair of formula $(\varphi,\psi)$ is called,

  * (a)

(logical) formal concept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
and
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$,

  * (b)

(logical) property oriented concept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\Box_{\mathfrak{m}}}\psi$
and
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow\psi$,

  * (c)

(logical) object oriented concept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\Diamond_{\mathfrak{m}}}\psi$
and
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\Box_{\mathfrak{g}}}\varphi\leftrightarrow\psi$.

The above definition is a reformulation of Definition 3.1. The main difference
is that here we define them in a single language while Definition 3.1 is based
on two different languages. When we studied rough and formal concepts using
two different logics, we needed a translation between their languages and two
different models respectively based on a context and its complement. With the
uniform framework, we have the following result corresponding to Proposition
3.2.

###### Proposition 5.3.

Let $\varphi\in Fm(\textbf{BM})_{s_{1}}$ and $\psi\in
Fm(\textbf{BM})_{s_{2}}$. Then,

  * (a)

$(\varphi,\psi)$ is a property oriented concept iff $(\neg\varphi,\neg\psi)$
is a object oriented concept.

  * (b)

$(\varphi,\psi)$ is a formal concept iff $(\varphi,\neg\psi)$ is a property
oriented concept.

  * (c)

$(\varphi,\psi)$ is a formal concept iff $(\neg\varphi,\psi)$ is a object
oriented concept.

For a logical concept $(\varphi,\psi)$, we call $\varphi$ and $\psi$ its
extent formula and intent formula respectively. We denote the sets of all
logical formal concepts, logical property oriented concepts, and logical
object oriented concepts by FC, ${\tt PC}$, and ${\tt OC}$ respectively. As in
Section 3, we can define equivalence relation $\equiv_{\tt FC}$, $\equiv_{\tt
PC}$ and $\equiv_{\tt OC}$ on the sets ${\tt FC}$, ${\tt PC}$ and ${\tt OC}$
by identifying equivalent extent formulas of two concepts. It can be shown
that the sets of equivalence classless ${\tt FC}/\equiv_{\tt FC}$, ${\tt
PC}/\equiv_{\tt PC}$ and ${\tt OC}/\equiv_{\tt OC}$ form lattices just as in
Theorem 3.7.

In addition to rough and formal concepts, the logic can also represent more
general notions of concepts in FCA, such as semiconcepts and protoconcepts
(wille, ).

###### Definition 5.4.

A pair of formula $(\varphi,\psi)$ is called,

  * (a)

a (logical) semiconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$,

  * (b)

a (logical) property oriented semiconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\Box_{\mathfrak{m}}}\psi$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow\psi$,

  * (c)

a (logical) object oriented semiconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\Diamond_{\mathfrak{m}}}\psi$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\Box_{\mathfrak{g}}}\varphi\leftrightarrow\psi$.

We denote the sets of all logical semiconcepts, logical property oriented
smiconcepts, and logical object oriented semiconcepts by ${\tt SC}$, ${\tt
PS}$, and ${\tt OS}$ respectively.

A semiconcept $(\varphi,\psi)$ is called a left semiconcept if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$
and it is called a right semiconcept if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
. We denote the sets of all left and right semiconcepts by ${\tt SC}^{l}$ and
${\tt SC}^{r}$ respectively. We can also define equivalence relations over
${\tt SC}^{l}$ and ${\tt SC}^{r}$. We say two left semiconcepts
$(\varphi_{1},\psi_{1})$ and $(\varphi_{2},\psi_{2})$ are equivalent, denoted
by $(\varphi_{1},\psi_{1})\equiv^{l}_{sc}(\varphi_{2},\psi_{2})$, if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\leftrightarrow\varphi_{2}$.
Similarly, two right semiconcepts $(\varphi_{1},\psi_{1})$ and
$(\varphi_{2},\psi_{2})$ are equivalent if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}\psi_{1}\leftrightarrow\psi_{2}$
and denoted by $(\varphi_{1},\psi_{1})\equiv^{r}_{sc}(\varphi_{2},\psi_{2})$.
For simplification, we omit the subscript from the equivalence relations and
simply write them as $\equiv^{l}$ and $\equiv^{r}$. Let ${\tt
SC}^{l}/\equiv^{l}$ and ${\tt SC}^{r}/\equiv^{r}$ be the corresponding sets of
equivalence classes. Then, we define the following structures :

  * •

$({\tt
SC}^{l}/\equiv^{l},\wedge,\neg,[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$
where for any $[(\varphi,\psi)],[(\varphi^{\prime},\psi^{\prime})]\in{\tt
SC}^{l}/\equiv^{l}$,

    * –

$[(\varphi,\psi)]\wedge[(\varphi^{\prime},\psi^{\prime})]:=[(\varphi\wedge\varphi^{\prime},{\boxminus_{\mathfrak{g}}}(\varphi\wedge\varphi^{\prime}))]$

    * –

$\neg[(\varphi,\psi)]:=[(\neg\varphi,{\boxminus_{\mathfrak{g}}}\neg\varphi)]$

  * •

$({\tt
SC}^{r}/\equiv^{r},\vee,\neg,[({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])$
where for any $[(\varphi,\psi)],[(\varphi^{\prime},\psi^{\prime})]\in{\tt
SC}^{r}/\equiv^{r}$,

    * –

$[(\varphi,\psi)]\vee[(\varphi^{\prime},\psi^{\prime})]:=[({\boxminus_{\mathfrak{m}}}(\psi\wedge\psi^{\prime}),\psi\wedge\psi^{\prime})]$

    * –

$\neg[(\varphi,\psi)]:=[({\boxminus_{\mathfrak{m}}}\neg\psi,\neg\psi)]$

###### Theorem 5.5.

$({\tt
SC}^{l}/\equiv^{l},\wedge,\neg,[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$
and $({\tt
SC}^{r}/\equiv^{r},\vee,\neg,[({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])$
are both Boolean algebras.

###### Proof.

We only prove this for the structure $({\tt
SC}^{l}/\equiv^{l},\wedge,\neg,[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$.
The proof for the other one is similar. First, for
$[(\varphi,\psi)],[(\varphi^{\prime},\psi^{\prime})]\in{\tt
SC}^{l}/\equiv^{l}$, we define
$[(\varphi,\psi)]\vee[(\varphi^{\prime},\psi^{\prime})]=\neg(\neg[(\varphi,\psi)]\wedge\neg[(\varphi^{\prime},\psi^{\prime})])$.
Then, the result follows immediately from the fact that all operations over
the structure depend only on the first component of formula pairs and the
equivalence classes of formulas form an Boolean algebra already. ∎

Let $\mathfrak{D}\subseteq Fm(\textbf{BM})_{s_{1}}\times
Fm(\textbf{BM})_{s_{2}}$ be a subset of formula pairs such that there are maps
$r:\mathfrak{D}\rightarrow{\tt SC}^{l}/\equiv^{l}$, $e:{\tt
SC}^{l}/\equiv^{l}\rightarrow\mathfrak{D}$,
$r^{\prime}:\mathfrak{D}\rightarrow{\tt SC}^{r}/\equiv^{r}$, and
$e^{\prime}:{\tt SC}^{r}/\equiv^{r}\rightarrow\mathfrak{D}$ satisfying $r\circ
e=id_{{\tt SC}^{l}/\equiv^{l}}$ and $r^{\prime}\circ e^{\prime}=id_{{\tt
SC}^{r}/\equiv^{r}}$. Then, we define operations over $\mathfrak{D}$ as
follows: for all $x,y\in\mathfrak{D}$

$x\sqcap y:=e(r(x)\wedge r(y))$ $x\sqcup y:=e^{\prime}(r^{\prime}(x)\vee
r^{\prime}(y))$

$\bar{\neg}x:=e(\neg r(x))$ and $\lrcorner x:=e^{\prime}(\neg r^{\prime}(x))$

$\bot_{\mathfrak{D}}:=e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$
and
$\top_{\mathfrak{D}}:=e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])$

Next, we show that $\mathfrak{D}$ forms a pure dBa with respect to these
operations under some mild assumptions.

###### Theorem 5.6.

$(\mathfrak{D},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top_{\mathfrak{D}},\bot_{\mathfrak{D}})$
is a pure dBa iff the following holds.

  * (a)

$e\circ r\circ e^{\prime}\circ r^{\prime}=e^{\prime}\circ r^{\prime}\circ
e\circ r$

  * (b)

$e(r(x)\wedge r(e^{\prime}(r^{\prime}(x)\vee r^{\prime}(y))))=e(r(x))$ and
$e^{\prime}(r^{\prime}(x)\vee r^{\prime}(e(r(x)\wedge
r(y))))=e^{\prime}(r^{\prime}(x))$ for all $x,y\in A$.

  * (c)

$r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))=\neg[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})]$
and
$r^{\prime}(e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})]))=\neg[({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]$.

  * (d)

For $x\in\mathfrak{D}$, either $er(x)=x$ or $e^{\prime}r^{\prime}(x)=x$

###### Proof.

We first show that the structure satisfying these conditions also satisfies
axioms (1a)-(11a) and (12) for dBa. Let $x,y,z\in\mathfrak{D}$. Then,

:

(1a): $(x\sqcap x)\sqcap y=e(r(x\sqcap x)\wedge r(y))=e(re(r(x)\wedge
r(x))\wedge r(y))=e((r(x)\wedge r(x))\wedge r(y))=e(r(x)\wedge r(y))=x\sqcap
y$.

:

(2a): Commutativity follows from the definition of $\sqcap$ directly.

:

(3a): $\bar{\neg}(x\sqcap x)=e(\neg r(x\sqcap x))=e(\neg re(r(x)\wedge
r(x)))=e(\neg(r(x)\wedge r(x)))=e(\neg r(x))=\bar{\neg}x$.

:

(4a): it follows from the first part of assumption (ii).

:

(5a):
$x\sqcap(y\bar{\vee}z)=x\sqcap\bar{\neg}(\bar{\neg}y\sqcap\bar{\neg}z)=e(r(x)\wedge
r(\bar{\neg}(\bar{\neg}y\sqcap\bar{\neg}z)))=e(r(x)\wedge r(e(\neg
r(\bar{\neg}y\sqcap\bar{\neg}z))))=e(r(x)\wedge\neg
r(\bar{\neg}y\sqcap\bar{\neg}z))=e(r(x)\wedge\neg re(r(\bar{\neg}y)\wedge
r(\bar{\neg}z)))=e(r(x)\wedge\neg(re(\neg r(y))\wedge re(\neg
r(z))))=e(r(x)\wedge\neg(\neg r(y)\wedge\neg r(z)))=e(r(x)\wedge(r(y)\vee
r(z)))=e((r(x)\wedge r(y))\vee(r(x)\wedge r(z)))=(x\sqcap y)\bar{\vee}(x\sqcap
z)$. The last equality depends on the claim that for $u,v\in{\tt
SC}^{l}/\equiv^{l}$, $e(u\vee v)=e(u)\bar{\vee}e(v)$. The proof of the claim
is as follows:
$e(u)\bar{\vee}e(v)=\bar{\neg}(\bar{\neg}e(u)\sqcap\bar{\neg}e(v))=e(\neg
r(\bar{\neg}e(u)\sqcap\bar{\neg}e(v)))=e(\neg re(r(\bar{\neg}e(u))\wedge
r(\bar{\neg}e(v))))=e(\neg(r(\bar{\neg}e(u))\wedge
r(\bar{\neg}e(v))))=e(\neg(re(\neg re(u))\wedge re(\neg re(v))))=e(\neg(\neg
u\wedge\neg v))=e(u\vee v)$.

:

(6a): $x\sqcap(x\bar{\vee}y)=e(r(x)\wedge
r(x\bar{\vee}y))=e(r(x)\wedge(r(x)\vee r(y)))=e(r(x))=e(r(x)\wedge
r(x))=x\sqcap x$, where the second equality follows from the fact that
$r(x\bar{\vee}y)=r(x)\vee r(y)$ for any $x,y\in\mathfrak{D}$. We prove the
fact as follows:
$r(x\bar{\vee}y)=r(\bar{\neg}(\bar{\neg}x\sqcap\bar{\neg}y))=re(\neg
r(\bar{\neg}x\sqcap\bar{\neg}y))=\neg re(r(\bar{\neg}x)\wedge
r(\bar{\neg}y))=\neg(r(\bar{\neg}x)\wedge r(\bar{\neg}y))=\neg(re(\neg
r(x))\wedge re(\neg r(y)))=\neg(\neg r(x)\wedge\neg r(y))=r(x)\vee r(y)$.

:

(7a): $\bar{\neg}\bar{\neg}(x\sqcap y)=e(\neg re(\neg r(x\sqcap y))=e(\neg\neg
r(x\sqcap y))=e(r(x\sqcap y))=e(re(r(x)\wedge r(y)))=e(r(x)\wedge
r(y))=x\sqcap y$.

:

(8a): $x\sqcap\bar{\neg}x=e(r(x)\wedge re(\neg r(x)))=e(r(x)\wedge\neg
r(x))=e(r(x)\wedge\neg
r(x))=e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])=\bot_{\mathfrak{D}}$.

:

(9a): $\bar{\neg}\top_{\mathfrak{D}}=e(\neg r(\top_{\mathfrak{D}}))=e(\neg
r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])))=e(\neg\neg[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])=\\\
e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])=\bot_{\mathfrak{D}}$,
where the second equality follows from assumption (c).

:

(10a): the associativity follows from $r\circ e=id_{{\tt SC}^{l}/\equiv^{l}}$.

:

(11a):
$\top_{\mathfrak{D}}\sqcap\top_{\mathfrak{D}}=e(r(\top_{\mathfrak{D}})\wedge
r(\top_{\mathfrak{D}}))=e(re^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))=e(\neg[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])=e(\neg
re([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})]))=\bar{\neg}\bot_{\mathfrak{D}}$

:

(12): It follows from assumption (a).

Analogously, we can prove that the structure satisfies axioms (1b)-(11b) for
dBa. In addition, by assumption (d), it follows that for any
$x\in\mathfrak{D}$, either $x\sqcap x=x$ or $x\sqcup x=x$. Hence,
$(\mathfrak{D},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top_{\mathfrak{D}},\bot_{\mathfrak{D}})$
is a pure dBa.

Conversely, assume that
$(\mathfrak{D},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top_{\mathfrak{D}},\bot_{\mathfrak{D}})$
is a pure dBa. Then, axiom (12) of dBa, i.e. all $x,y\in D$, $(x\sqcap
x)\sqcup(x\sqcap x)=(x\sqcup x)\sqcap(x\sqcup x)$, implies assumption (a).
Translating axioms (4a): $x\sqcap(x\sqcup y)=x\sqcap x$ and (4b):
$x\sqcup(x\sqcap y)=x\sqcup x$ in terms of $e,r,e^{\prime},r^{\prime}$ we have
assumption (b). In addition, by axiom (9a):
$\bar{\neg}\top_{\mathfrak{D}}=\bot_{\mathfrak{D}}$, we have
$\bar{\neg}\top_{\mathfrak{D}}=e(\neg r(\top_{\mathfrak{D}}))=e(\neg
r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))$ and
$\bot_{\mathfrak{D}}=e([(\bot_{s_{1}},\boxminus\bot_{s_{1}})])$. Hence,
$e(\neg
r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))=e([(\bot_{s_{1}},\boxminus\bot_{s_{1}})])$
which implies that $\neg
r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])=[(\bot_{s_{1}},\boxminus\bot_{s_{1}})]$,
as $e$ is injective, from which the first part of assumption (c) follows
immediately. The second part of assumption (c) is proved in the same way.
Finally, because pure dBa satisfies that for all $x$, either $x\sqcap x=x$ or
$x\sqcup x=x$, we have assumption (d). ∎

Next, we show that a construction satisfying conditions in Theorem 5.6 is
always possible. Let us define an equivalence relation $\equiv_{\tt sc}$ over
SC by $(\varphi_{1},\psi_{1})\equiv_{\tt sc}(\varphi_{2},\psi_{2})$ iff
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\leftrightarrow\varphi_{2}$
and
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}\psi_{1}\leftrightarrow\psi_{2}$
and consider $\mathfrak{D}:=\texttt{SC}/\equiv_{\tt SC}$. Then, we can define
the following maps:

$r:\mathfrak{D}\rightarrow{\tt SC}^{l}/\equiv^{l}$,
$r([(\varphi,\psi)])=[(\varphi,{\boxminus_{\mathfrak{g}}}\varphi)]$ and
$e:{\tt SC}^{l}/\equiv^{l}\rightarrow\mathfrak{D}$,
$e([(\varphi,\psi)])=[(\varphi,\psi)]$

$r^{\prime}:\mathfrak{D}\rightarrow{\tt SC}^{r}/\equiv^{r}$,
$r^{\prime}([(\varphi,\psi)])=[({\boxminus_{\mathfrak{m}}}\psi,\psi)]$ and
$e^{\prime}:{\tt SC}^{r}/\equiv^{r}\rightarrow\mathfrak{D}$,
$e^{\prime}([(\varphi,\psi)])=[(\varphi,\psi)]$

###### Proposition 5.7.

The maps defined above satisfy $r\circ e=id_{{\tt SC}^{l}/\equiv^{l}}$ and
$r^{\prime}\circ e^{\prime}=id_{{\tt SC}^{r}/\equiv^{r}}$ and conditions
$(a)-(d)$ of Theorem 5.6.

###### Proof.

First, for $[(\varphi,\psi)]\in{\tt SC}^{l}/\equiv^{l}$, $r\circ
e([(\varphi,\psi)])=r([(\varphi,\psi)])=[(\varphi,{\boxminus_{\mathfrak{g}}}\varphi)]=[(\varphi,\psi)]$,
as
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}\psi\leftrightarrow{\boxminus_{\mathfrak{g}}}\varphi$.
Hence, $r\circ e=id_{{\tt SC}^{l}/\equiv^{l}}$. Similarly we can show that
$r^{\prime}\circ e^{\prime}=id_{{\tt SC}^{r}/\equiv^{r}}$.

Second, for $[(\varphi,\psi)]\in\mathfrak{D}$, $e\circ r\circ e^{\prime}\circ
r^{\prime}([(\varphi,\psi)])=[({\boxminus_{\mathfrak{m}}}\psi,{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi)]$
and $e^{\prime}\circ r^{\prime}\circ e\circ
r([(\varphi,\psi)])=[({\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi,{\boxminus_{\mathfrak{g}}}\varphi)]$.
As $(\varphi,\psi)$ is a semiconcept,
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$.
If
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$,
then
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi$
by Proposition 2.9, whence
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi$.
Thus
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$
by Proposition 5.1 (i). Hence, $e\circ r\circ e^{\prime}\circ
r^{\prime}([(\varphi,\psi)])=e^{\prime}\circ r^{\prime}\circ e\circ
r([(\varphi,\psi)])$. The proof for the case of
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$
is similar.

Third, for $[(\varphi_{1},\psi_{1})],[(\varphi_{2},\psi_{2})]\in\mathfrak{D}$,
$e(r([(\varphi_{1},\psi_{1})])\wedge
r(e^{\prime}(r^{\prime}([(\varphi_{1},\psi_{1})])\vee
r^{\prime}([(\varphi_{2},\psi_{2})]))))=[(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})))]$.
It is clear that
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})\rightarrow\varphi_{1}$.
As $(\varphi_{1},\psi_{1})$ is a semiconcept, we have
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi_{1}$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi_{1}\leftrightarrow\psi_{1}$.
Let us assume
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi_{1}\leftrightarrow\psi_{1}$
whence
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi_{1}\wedge\psi_{2}\leftrightarrow\psi_{1}\wedge\psi_{2}$.
Then, by Proposition 2.9,
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}({\boxminus_{\mathfrak{g}}}\varphi_{1}\wedge\psi_{2})\leftrightarrow{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})$
which implies that
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})$.
By Proposition 5.1 (iii),
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}{\boxminus_{\mathfrak{g}}}\varphi_{1}$.
Hence, we have
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\rightarrow{\boxminus_{\mathfrak{m}}}({\boxminus_{\mathfrak{g}}}\varphi_{1}\wedge\psi_{2})$
and
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\rightarrow\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}({\boxminus_{\mathfrak{g}}}\varphi_{1}\wedge\psi_{2})$.
Therefore, $e(r([(\varphi_{1},\psi_{1})])\wedge
r(e^{\prime}(r^{\prime}([(\varphi_{1},\psi_{1})])\vee
r^{\prime}([(\varphi_{2},\psi_{2})]))))=[(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2}),{\boxminus_{\mathfrak{g}}}(\varphi_{1}\wedge{\boxminus_{\mathfrak{m}}}(\psi_{1}\wedge\psi_{2})))]=[(\varphi_{1},{\boxminus_{\mathfrak{g}}}\varphi_{1})]=er([(\varphi_{1},\psi_{1})])$.
The proof for the case of
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi_{1}\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi_{1}$
is similar. Analogously, we can also show that
$e^{\prime}(r^{\prime}([(\varphi_{1},\psi_{1})])\vee
r^{\prime}(e(r([(\varphi_{1},\psi_{1})])\wedge
r([(\varphi_{2},\psi_{2})]))))=e^{\prime}(r^{\prime}([(\varphi_{2},\psi_{2})]))$.

Forth,
$r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))=[({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\bot_{s_{2}})]$.
To prove that
$r(e^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]))=\neg[(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})]$,
it is sufficient to show that
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}\bot_{s_{2}}\leftrightarrow\neg\bot_{s_{1}}$.
Now for all $\mathbb{K}$-based model $\mathfrak{M}$ and $g\in G$,
$\mathfrak{M},g\models\neg\bot_{s_{1}}$ and
$\mathfrak{M},g\models{\boxminus_{\mathfrak{m}}}\bot_{s_{2}}$. Hence
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{m}}}\top_{s_{2}}\leftrightarrow\neg\bot_{s_{1}}$.
Analogously, we can show that
$r^{\prime}(e([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})]))=\neg[({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})]$.

Finally, for any $[(\varphi,\psi)]\in\mathfrak{D}$, $(\varphi,\psi)$ is either
a left or a right semiconcept. Hence,
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow\psi$
or
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}\varphi\leftrightarrow{\boxminus_{\mathfrak{m}}}\psi$,
which implies $r\circ
e([(\varphi,\psi)])=[(\varphi,{\boxminus_{\mathfrak{g}}}\varphi)]=[(\varphi,\psi)]$
or $r^{\prime}\circ
e^{\prime}([(\varphi,\psi)])=[({\boxminus_{\mathfrak{m}}}\psi,\psi)]=[(\varphi,\psi)]$
respectively. ∎

Next, we define logical protoconcepts.

###### Definition 5.8.

A pair of formula $(\varphi,\psi)$ is called,

  * (a)

a logical protoconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\boxminus_{\mathfrak{g}}}\varphi\leftrightarrow{\boxminus_{\mathfrak{g}}}{\boxminus_{\mathfrak{m}}}\psi$,

  * (b)

a logical property oriented protoconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{1}}{\Diamond_{\mathfrak{g}}}\varphi\leftrightarrow{\Diamond_{\mathfrak{g}}}{\Box_{\mathfrak{m}}}\psi$,

  * (c)

a logical object oriented protoconcept of the context $\mathbb{K}$ if
$\models^{\mathfrak{C}_{\mathbb{K}}}_{s_{2}}{\Diamond_{\mathfrak{m}}}{\Box_{\mathfrak{g}}}\varphi\leftrightarrow{\Diamond_{\mathfrak{m}}}\psi$.

Note that a logical semiconcept is also a logical protoconcept. We denote the
set of all logical protoconcepts by ${\tt PR}$. Thus ${\tt SC}^{l}\cup{\tt
SC}^{r}\subseteq{\tt PR}$. As done with the set of logical semiconcept, we can
define an equivalence relation $\equiv_{\tt PR}$ over the set ${\tt PR}$. Let
$\mathfrak{D}_{1}={\tt PR}/\equiv_{\tt PR}$ be the set of its equivalence
classes. Then, with the definition of the following maps:

$r_{1}:\mathfrak{D}_{1}\rightarrow{\tt SC}^{l}/\equiv^{l}$,
$r_{1}([(\varphi,\psi)])=[(\varphi,{\boxminus_{\mathfrak{g}}}\varphi)]$ and
$e_{1}:{\tt SC}^{l}/\equiv^{l}\rightarrow\mathfrak{D}_{1}$,
$e_{1}([(\varphi,\psi)])=[(\varphi,\psi)]$

$r_{1}^{\prime}:\mathfrak{D}_{1}\rightarrow{\tt SC}^{r}/\equiv^{r}$,
$r_{1}^{\prime}([(\varphi,\psi)])=[({\boxminus_{\mathfrak{m}}}\psi,\psi)]$ and
$e_{1}^{\prime}:{\tt SC}^{r}/\equiv^{r}\rightarrow\mathfrak{D}_{1}$,
$e_{1}^{\prime}([(\varphi,\psi)])=[(\varphi,\psi)]$

we can show that $r_{1}\circ e_{1}=id_{{\tt SC}^{l}/\equiv^{l}}$,
$r_{1}^{\prime}\circ e_{1}^{\prime}=id_{{\tt SC}^{r}/\equiv^{r}}$, and
$r_{1},e_{1},r^{\prime}_{1}$ and $e^{\prime}_{1}$ satisfy (a)-(c) of Theorem
5.6.

Let us define operations on the set $\mathfrak{D}_{1}$ as follows: for all
$x,y\in\mathfrak{D}_{1}$

$x\sqcap y:=e_{1}(r_{1}(x)\wedge r_{1}(y))$ $x\sqcup
y:=e_{1}^{\prime}(r_{1}^{\prime}(x)\vee r_{1}^{\prime}(y))$

$\bar{\neg}x:=e_{1}(\neg r_{1}(x))$ and $\lrcorner x:=e_{1}^{\prime}(\neg
r_{1}^{\prime}(x))$

$\bot_{\mathfrak{D}}:=e_{1}([(\bot_{s_{1}},{\boxminus_{\mathfrak{g}}}\bot_{s_{1}})])$
and
$\top_{\mathfrak{D}}:=e_{1}^{\prime}([({\boxminus_{\mathfrak{m}}}\bot_{s_{2}},\bot_{s_{2}})])$

Then we can show that
$(\mathfrak{D}_{1},\sqcap,\sqcup,\bar{\neg},\lrcorner,\top,\bot)$ is a dBa.
Moreover, we can prove the following general theorem.

###### Theorem 5.9.

Let $(B,\wedge,-,0,1)$ and
$(B^{\prime},\vee^{\prime},-^{\prime},0^{\prime},1^{\prime})$ be two Boolean
algebras and let $r:A\rightleftharpoons B:e$ and
$r^{\prime}:A\rightleftharpoons B^{\prime}:e^{\prime}$ be pairs of maps such
that $r\circ e=id_{B}$ and $r^{\prime}\circ e^{\prime}=id_{B^{\prime}}$.
$\textbf{A}:=(A,\sqcap,\sqcup,\bar{\neg},\lrcorner,e^{\prime}(1^{\prime}),e(0))$
is a universal algebra where, $x\sqcap y:=e(r(x)\wedge r(y)),x\sqcup
y:=e^{\prime}(r^{\prime}(x)\vee^{\prime}r^{\prime}(y)),\neg x:=e(-r(x))$ and
$\lrcorner x:=e^{\prime}(-^{\prime}r^{\prime}(x))$. Then A is a dBa iff the
following holds

  * (a)

$e\circ r\circ e^{\prime}\circ r^{\prime}=e^{\prime}\circ r^{\prime}\circ
e\circ r$

  * (b)

$e(r(x)\wedge r(e^{\prime}(r^{\prime}(x)\vee^{\prime}r^{\prime}(y))))=e(r(x))$
and $e^{\prime}(r^{\prime}(x)\vee^{\prime}r^{\prime}(e(r(x)\wedge
r(y))))=e^{\prime}(r^{\prime}(x))$ for all $x,y\in A$.

  * (c)

$r(e^{\prime}(1^{\prime}))=1$ and $r^{\prime}(e(0))=0^{\prime}$.

Moreover every dBa can be obtained from such a construction.

###### Proof.

The first part of the proof is similar to that of Theorem 5.6.

To show that any dBa can be obtained from such a construction, let
$\textbf{D}:=(D,\sqcap,\sqcup,\bar{\neg},\lrcorner,\top,\bot)$ be a dBa. Then,
by Proposition 1.14, the two Boolean algebras in consideration are

$(B,\wedge,-,0,1)=\textbf{D}_{\sqcap}:=(D_{\sqcap},\sqcap,\bar{\neg},\bot,\bar{\neg}\bot)$
$(B^{\prime},\vee^{\prime},-^{\prime},0^{\prime},1^{\prime})=\textbf{D}_{\sqcup}:=(D_{\sqcup},\sqcup,\lrcorner,\lrcorner\top,\top).$

We thus define the following maps:

$r:D\rightarrow D_{\sqcap}$ by $r(x)=x\sqcap x$ for $x\in D$ and
$e:D_{\sqcap}\rightarrow D$, by $e(x)=x$ for $x\in D_{\sqcap}$.

$r^{\prime}:D\rightarrow D_{\sqcup}$ by $r^{\prime}(x)=x\sqcup x$ for $x\in D$
and $e^{\prime}:D_{\sqcup}\rightarrow D$, by $e^{\prime}(x)=x$ for $x\in
D_{\sqcup}$.

These maps are well-defined as $r(x)\sqcap r(x)=r(x)$ and $r^{\prime}(x)\sqcup
r^{\prime}(x)=r^{\prime}(x)$ follow from axioms (1a),(2a) and (1b),(2b) of dBa
respectively. Also, by the definition, it is clear that $r\circ
e=id_{D_{\sqcap}}$ and $r^{\prime}\circ e^{\prime}=id_{D_{\sqcup}}$.

We now show that they also satisfy conditions (a)-(c). For condition (a), let
$x\in D$. Then, $e\circ r\circ e^{\prime}\circ r^{\prime}(x)=e\circ r\circ
e^{\prime}(x\sqcup x)=e\circ r(x\sqcup x)=(x\sqcup x)\sqcap(x\sqcup
x)=(x\sqcap x)\sqcup(x\sqcap x)=e^{\prime}\circ r^{\prime}\circ e\circ r(x)$.
For condition (b), let $x,y\in D$. Then, $e(r(x)\sqcap
r(e^{\prime}(r^{\prime}(x)\sqcup r^{\prime}(y))))=e(x\sqcap x\sqcap r(x\sqcup
x\sqcup y\sqcup y))=e(x\sqcap r(x\sqcup y))=x\sqcap(x\sqcup y)\sqcap(x\sqcup
y)=x\sqcap x\sqcap(x\sqcup y)=x\sqcap x\sqcap x=x\sqcap x=e(r(x))$. Similarly,
we can show that $e^{\prime}(r^{\prime}(x)\sqcup r^{\prime}(e(r(x)\sqcap
r(y))))=e^{\prime}(r^{\prime}(x))$. For condition (c),
$r(e^{\prime}(1^{\prime}))=r(e^{\prime}(\top))=r(\top)=\top\sqcap\top=\bar{\neg}\bot=1$
and
$r^{\prime}(e(0))=r^{\prime}(e(\bot))=r^{\prime}(\bot)=\bot\sqcup\bot=\lrcorner\top=0^{\prime}$.

Hence, by the first part of the theorem,
$(D,\sqcap_{1},\sqcup_{1},\bar{\neg}_{1},\lrcorner_{1},\top,\bot)$ is a dBa
where $x\sqcap_{1}y=e(r(x)\sqcap r(y))=x\sqcap y$,
$x\sqcup_{1}y=e^{\prime}(r^{\prime}(x)\sqcup r^{\prime}(y))=x\sqcup y$,
$\neg_{1}x=e(\bar{\neg}r(x))=\bar{\neg}(x\sqcap x)=\bar{\neg}x$, and
$\lrcorner_{1}x=e^{\prime}(\lrcorner r^{\prime}(x))=\lrcorner(x\sqcup
x)=\lrcorner x$. Therefore, D is indeed constructed by the two underlying
Boolean algebras. ∎

Finally, we note that what has been done with (logical) semiconcepts and
protoconcepts here can carry over to object and property oriented ones.

##  6\. Possible extensions

In this section, we discuss two possible ways to extend two-sorted modal
logics considered so far. These extensions can express more fine-grained
information in context-based models.

###  6.1. Two-sorted graded modal logic

The first extension is two-sorted graded modal logic. Traditionally, graded
modalities have been applied to counting the number of accessible possible
worlds (BalestriniF99, ; Caro88, ; Cerrato90, ; Cerrato94, ; DeCaro, ;
Fattorosi-Barnaba88, ; Fattorosi-BarnabaG95, ). Hence, our extension is aimed
at the representation and reasoning about quantitative knowledge induced from
formal contexts.

The alphabet of the extended language consists of a two-sorted family
$P:=\\{P_{s_{1}},P_{s_{2}}\\}$ of propositional variables, the propositional
connectives $\vee$, $\wedge$ and $\neg$, and the modal operators
${\Box_{\mathfrak{g}}^{n}}$, ${\boxminus_{\mathfrak{g}}^{n}}$,
${\Box_{\mathfrak{m}}^{n}}$, ${\boxminus_{\mathfrak{m}}^{n}}$, for
$n\in\mathbb{N}$. The formula is the family
$Fm(\textbf{BM})^{gd}:=\\{Fm(\textbf{BM})^{gd}_{s_{1}},Fm(\textbf{BM})^{gd}_{s_{2}}\\}$
where,

$\varphi_{s_{1}}:=p_{s_{1}}\mid\varphi_{s_{1}}\wedge\varphi_{s_{1}}\mid\varphi_{s_{1}}\vee\varphi_{s_{1}}\mid\neg\varphi_{s_{1}}\mid{\Box_{\mathfrak{m}}^{n}}\varphi_{s_{2}}\mid{\boxminus_{\mathfrak{m}}^{n}}\varphi_{s_{2}}$
$\varphi_{s_{2}}:=p_{s_{2}}\mid\varphi_{s_{2}}\wedge\varphi_{s_{2}}\mid\varphi_{s_{2}}\vee\varphi_{s_{2}}\mid\neg\varphi_{s_{2}}\mid{\Box_{\mathfrak{g}}^{n}}\varphi_{s_{1}}\mid{\boxminus_{\mathfrak{g}}^{n}}\varphi_{s_{1}}.$

For a context-based model $\mathfrak{M}:=(G,M,I,v)$, and given $g\in G$ and
$m\in M$, recalling the definition of $I^{\rightarrow}$ and
$I^{\leftarrow}$-neighborhoods
$I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}:=\\{m\in M\mid Igm\\}$
and $I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}:=\\{g\in G\mid
Igm\\}$, we further define
$I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\psi):=\\{m\in
I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}\mid
m\models_{s_{2}}\psi\\}$ and
$I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\varphi):=\\{g\in
I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}\mid
g\models_{s_{1}}\varphi\\}$ for any formulas $\varphi\in
Fm(\textbf{BM})_{s_{1}}^{gd}$ and $\psi\in Fm(\textbf{BM})_{s_{2}}^{gd}$.
Also, we define the same notations for the complemented relation
$\overline{I}$. The satisfaction of a formula is then defined as follows

###### Definition 6.1.

Let $\mathfrak{M}:=(G,M,I,v)$ be a model, then for $m\in M$ and $g\in G$,

  * (a)

$\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}^{n}}\varphi$ iff
$|I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\neg\varphi)|\leq n$,

  * (b)

$\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}^{n}}\varphi$ iff
$|\overline{I}_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\varphi)|\leq
n$,

  * (c)

$\mathfrak{M},g\models_{s_{1}}{\Box_{\mathfrak{m}}^{n}}\psi$ iff
$|I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\neg\psi)|\leq n$,

  * (d)

$\mathfrak{M},g\models_{s_{1}}{\boxminus_{\mathfrak{m}}^{n}}\psi$ iff
$|\overline{I}_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\psi)|\leq
n$.

Intuitively, a property satisfies the formula
${\Box_{\mathfrak{g}}^{n}}\varphi$ if the number of objects with the property
but not satisfying $\varphi$ is at most $n$ and it satisfies the formula
${\boxminus_{\mathfrak{g}}^{n}}\varphi$ if the number of objects without the
property but satisfying $\varphi$ is at most $n$. The following example shows
a concrete interpretation of the graded modalities in the application context
of our running example.

###### Example 6.2.

Recalling the context of transaction data $(G,M,I)$ in Example 2.3, where $G$
and $M$ are sets of customers and product items respectively and for $g\in G$
and $m\in M$, $gIm$ means that the customer $g$ has bought the item $m$, let
$\mathfrak{M}=(G,M,I,v)$ be a model based on the context and let $\varphi\in
Fm(\textbf{BM})^{gd}_{s_{1}}$ and $\psi\in Fm(\textbf{BM})^{gd}_{s_{2}}$
remain the same as in Example 2.3. Then, the interpretation of some graded
modal formulas in $\mathfrak{M}$ are as follows.

  * (a)

For $g\in G$, $\mathfrak{M},g\models_{s_{1}}{\Box_{\mathfrak{m}}^{n}}\psi$
means that the number of non-electronic products bought by $g$ is no more than
$n$. When $n$ is a small number (e.g. $n=1$), this may mean that $g$ rarely
bought non-electronic products. However, the interpretation is sometimes
misleading. For example, if the customer $g$ has bought only one item in the
transaction data, then we can also say that he bought electronic products
only. The two readings of the formula ${\Box_{\mathfrak{m}}^{1}}\psi$ seem in
conflict with each other. To resolve this, we will need to use the weighted
modalities to be introduced in next subsection.

  * (b)

For $m\in M$, $\mathfrak{M},m\models_{s_{2}}{\Box_{\mathfrak{g}}^{n}}\varphi$
means that the number of customers buying $m$ and outside the 30-50 age group
is no more than $n$.

  * (c)

For $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\boxminus_{\mathfrak{m}}^{n}}\psi$ means that
the number of electronic products not bought by $g$ is no more than $n$.

  * (d)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\boxminus_{\mathfrak{g}}^{n}}\varphi$ means
that the number of customers in the 30-50 age group not buying $m$ is no more
than $n$. When $n$ is small, this may mean that $m$ is a popular product among
customers in this age group. Of course, the interpretation makes sense only
when the data set contains enough number of customers in the group.

We can also define several derived modalities
${\overline{\Box}_{\mathfrak{g}}^{n}}\varphi:={\boxminus_{\mathfrak{g}}^{n}}\neg\varphi$,
${\overline{\boxminus}_{\mathfrak{g}}^{n}}\varphi:={\Box_{\mathfrak{g}}^{n}}\neg\varphi$,
${\overline{\Box}_{\mathfrak{m}}^{n}}\psi:={\boxminus_{\mathfrak{m}}^{n}}\neg\psi$,
${\overline{\boxminus}_{\mathfrak{m}}^{n}}\psi:={\Box_{\mathfrak{m}}^{n}}\neg\psi$

###### Proposition 6.3.

For a model $\mathfrak{M}:=(G,M,I,v)$, $g\in G$ and $m\in M$, we have the
following.

  * (a)

$\mathfrak{M},m\models_{s_{2}}{\overline{\Box}_{\mathfrak{g}}^{n}}\varphi$ iff
$|\overline{I}_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\neg\varphi)|\leq
n$ and $\mathfrak{M},m\models{\overline{\boxminus}_{\mathfrak{g}}^{n}}\varphi$
iff $|I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\varphi)|\leq n$.

  * (b)

$\mathfrak{M},g\models_{s_{1}}{\overline{\Box}_{\mathfrak{m}}^{n}}\psi$ iff
$|\overline{I}_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\neg\psi)|\leq
n$ and $\mathfrak{M},g\models{\overline{\boxminus}_{\mathfrak{m}}^{n}}\psi$
iff $|I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\psi)|\leq n$.

###### Proof.

It follows from the definition immediately. ∎

###### Example 6.4.

Continuing with Example 6.2, let $\varphi\in Fm(\textbf{BM})^{gd}_{s_{1}}$ and
$\psi\in Fm(\textbf{BM})^{gd}_{s_{2}}$ remain unchanged. Then, the intuitive
meanings of the formulas ${\overline{\Box}_{\mathfrak{g}}^{n}}\varphi$,
${\overline{\boxminus}_{\mathfrak{g}}^{n}}\varphi$
${\overline{\Box}_{\mathfrak{m}}^{n}}\psi$,
${\overline{\boxminus}_{\mathfrak{m}}^{n}}\psi$ are as follows:

  * (a)

For $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\overline{\Box}_{\mathfrak{m}}^{n}}\psi$ means
that the number of non-electronic products not bought by $g$ is at most $n$.

  * (b)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\overline{\Box}_{\mathfrak{g}}^{n}}\varphi$,
the number of customers not in the 30 to 50 age group and not buy $m$ is less
than $n$.

  * (c)

For $g\in G$,
$\mathfrak{M},g\models_{s_{1}}{\overline{\boxminus}_{\mathfrak{m}}^{n}}\psi$,
$g$ the number of electronic products bought by $g$ is less than $n$.

  * (d)

For $m\in M$,
$\mathfrak{M},m\models_{s_{2}}{\overline{\boxminus}_{\mathfrak{g}}^{n}}\psi$,
the number of customers in the 30 to 50 age group and buy $m$ is less than
$n$.

Now we define modal operators that are dual to ${\Box_{\mathfrak{g}}^{n}}$,
${\boxminus_{\mathfrak{g}}^{n}}$, ${\Box_{\mathfrak{m}}^{n}}$,
${\boxminus_{\mathfrak{m}}^{n}}$.

${\Diamond_{\mathfrak{g}}^{n}}\varphi:=\neg{\Box_{\mathfrak{g}}^{n}}\neg\varphi$,
$\nabla_{\mathfrak{g}}^{n}\varphi:=\neg{\boxminus_{\mathfrak{g}}^{n}}\neg\varphi$,
${\Diamond_{\mathfrak{m}}^{n}}\psi:=\neg{\Box_{\mathfrak{m}}^{n}}\neg\psi$ and
$\nabla_{\mathfrak{m}}^{n}\psi:=\neg{\boxminus_{\mathfrak{m}}^{n}}\neg\psi$

###### Proposition 6.5.

For a model $\mathfrak{M}:=(G,M,I,v)$, $g\in G$ and $m\in M$, we have the
following results.

  * (a)

$\mathfrak{M},m\models_{s_{2}}{\Diamond_{\mathfrak{g}}^{n}}\varphi$ iff
$|I_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\varphi)|>n$ and
$\mathfrak{M},m\models_{s_{2}}\nabla_{\mathfrak{g}}^{n}\varphi$ iff
$|\overline{I}_{\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}m}(\neg\varphi)|>n$.

  * (b)

$\mathfrak{M},g\models_{s_{1}}{\Diamond_{\mathfrak{m}}^{n}}\psi$ iff
$|I_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\psi)|\textgreater n$
and $\mathfrak{M},g\models_{s_{1}}\nabla_{\mathfrak{m}}^{n}\psi$ iff
$|\overline{I}_{g\mathbin{\vbox{\hbox{\scalebox{0.3}{$\bullet$}}}}}(\neg\psi)|\textgreater
n$.

###### Proof.

The proof follows from the definition. ∎

We can also define dual modalities of ${\overline{\Box}_{\mathfrak{g}}^{n}}$,
${\overline{\boxminus}_{\mathfrak{g}}^{n}}$,
${\overline{\Box}_{\mathfrak{m}}^{n}}$,
${\overline{\boxminus}_{\mathfrak{m}}^{n}}$ in the same way. Furthermore, with
graded modalities, we can define modal operators that represent the exact
number of objects/properties satisfying a formula $\varphi$ as follows:
${\Diamond_{\mathfrak{g}}^{n}}!\varphi:={\Diamond_{\mathfrak{g}}^{n-1}}\varphi\wedge\neg{\Diamond_{\mathfrak{g}}^{n}}\varphi$,
${\Diamond_{\mathfrak{m}}^{n}}!\psi:={\Diamond_{\mathfrak{m}}^{n-1}}\psi\wedge\neg{\Diamond_{\mathfrak{m}}^{n}}\psi$,
$\overline{\Diamond}_{\mathfrak{g}}^{n}!\varphi:=\overline{\Diamond}_{\mathfrak{g}}^{n-1}\varphi\wedge\neg\overline{\Diamond}_{\mathfrak{g}}^{n}\varphi$
and
$\overline{\Diamond}_{\mathfrak{m}}^{n}!\psi:=\overline{\Diamond}_{\mathfrak{m}}^{n-1}\psi\wedge\neg\overline{\Diamond}_{\mathfrak{m}}^{n}\psi$

Next, we show that the language has the expressive power to specify properties
of the binary relation and its complement in a context.

###### Theorem 6.6.

Let $\mathfrak{M}:=(G,M,I,v)$ be a model. Then the following results hold.

  * (a)

$I$ and $\overline{I}$ are partial functions iff
$\mathfrak{M}\models_{s_{1}}\neg{\Diamond_{\mathfrak{m}}^{1}}\top_{s_{2}}$ and
$\mathfrak{M}\models_{s_{1}}\neg{\overline{\Diamond}_{\mathfrak{m}}^{1}}\top_{s_{2}}$
respectively.

  * (b)

$I$ and $\overline{I}$ are functions iff
$\mathfrak{M}\models_{s_{1}}{\Diamond_{\mathfrak{m}}^{1}}!\top_{s_{2}}$ and
$\mathfrak{M}\models_{s_{1}}{\overline{\Diamond}_{\mathfrak{m}}^{1}}!\top_{s_{2}}$
respectively.

  * (c)

$I$ is an injective function iff
$\mathfrak{M}\models_{s_{1}}{\Diamond_{\mathfrak{m}}^{1}}!\top_{s_{2}}$ and
$\mathfrak{M}\models_{s_{2}}\neg{\Diamond_{\mathfrak{g}}^{1}}\top_{s_{1}}$.

  * (d)

$\overline{I}$ is an injective function iff
$\mathfrak{M}\models_{s_{1}}{\overline{\Diamond}_{\mathfrak{m}}^{1}}!\top_{s_{2}}$
and