<figure><img src="image_1.png" /></figure>

HAL
open science

# The Word Problem in Semiconcept Algebras (CLA 2011)

Philippe Balbiani

► To cite this version:

Philippe Balbiani. The Word Problem in Semiconcept Algebras (CLA 2011). 8th International Conference on Concept Lattices and Their Applications (CLA 2011), Oct 2011, Nancy, France. pp.279-294. hal-03997006

HAL Id: hal-03997006

https://hal.science/hal-03997006

Submitted on 20 Feb 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Word Problem in Semiconcept Algebras

Philippe Balbiani

CNRS — Université de Toulouse

Institut de recherche en informatique de Toulouse

118 ROUTE DE NARBONNE, 31062 TOULOUSE CEDEX 9, France

Philippe.Balbiani@irit.fr

**Abstract.** The aim of this article is to prove that the word problem in semiconcept algebras is **PSPACE**-complete.

**Keywords:** Formal concept analysis, semiconcept algebras, word problem, decidability/complexity.

## 1 Introduction

In formal concept analysis [2, 3], the properties of formal contexts are reflected by the properties of the concept lattices they give rise to [10, 12]. Extending concept lattices to protoconcept algebras and semiconcept algebras, Herrmann et al. [5] and Wille [11] introduced negations in conceptual structures based on formal contexts such as double Boolean algebras and pure double Boolean algebras. These algebras have attracted interest for their theoretical merits — basic representations have been obtained — and for their practical relevance — applications in the field of knowledge representation and reasoning have been developed [5–7, 9, 11].

The basic representations of protoconcept algebras and semiconcept algebras evoked above have been obtained by means of equational axioms. Hence, the problem naturally arises of whether there is an algorithm which given terms $s, t$, decides whether they represent the same element in all models of these equational axioms. Such a problem is called the word problem (WP) in protoconcept algebras or in semiconcept algebras. In Mathematics and Computer Science, word problems are of the utmost importance.

Within the context of protoconcept algebras, Vormbrock [8] demonstrates that given terms $s, t$, if $s = t$ is not valid in all protoconcept algebras then there exists a finite protoconcept algebra in which $s = t$ is not valid. Nevertheless, the upper bound on the size of the finite protoconcept algebra given in [8, Page 258] is not elementary. Therefore, it does not allow us to conclude — as wrongly stated in [8, Page 240] — that the WP in protoconcept algebras is **NP**-complete. Switching over to semiconcept algebras, the aim of this article is to prove that the WP in semiconcept algebras is **PSPACE**-complete.

Sections 2 and 3 show some of the basic properties of formal contexts and semiconcept algebras that have been discussed in [5–7, 9, 11]. In Section 4, we present
the WP in semiconcept algebras. Section 5 introduces a basic 2-sorted modal logic that will be used in Sections 6 and 7 to prove that the WP in semiconcept algebras is **PSPACE**-complete. The proofs of Lemmas 10, 11, 12 and 13 can be found in the annex.

# 2 From Formal Contexts to Semiconcept Algebras

In formal concept analysis, the properties of semiconcepts are reflected by the properties of the algebras they give rise to.

## 2.1 Formal Contexts

Formal contexts are structures of the form $\mathbb{K} = (G, M, \Delta)$ where $G$ is a nonempty set (with typical member denoted $g$), $M$ is a nonempty set (with typical member denoted $m$) and $\Delta$ is a binary relation between $G$ and $M$. The elements of $G$ are called “objects”, the elements of $M$ are called “attributes” and the intended meaning of $g \Delta m$ is “object $g$ possesses attribute $m$”.

<table><caption>Tab. 1.</caption><thead><tr><th>Δ</th><th>a<sub>1</sub></th><th>a<sub>2</sub></th></tr></thead><tbody><tr><td>o<sub>1</sub></td><td>×</td><td>×</td></tr><tr><td>o<sub>2</sub></td><td>×</td><td></td></tr></tbody></table>

*Example 1.* In Tab. 1 is an example of a formal context $\mathbb{K}^{2,2}$ with 2 objects — $o_1$ and $o_2$ — and 2 attributes — $a_1$ and $a_2$.

For all $X \subseteq G$ and for all $Y \subseteq M$, let

$$X^{\triangleright} = \{m \in M: \text{ for all } g \in G, \text{ if } g \in X \text{ then } g \Delta m\}$$

$$Y^{\triangleleft} = \{g \in G: \text{ for all } m \in M, \text{ if } m \in Y \text{ then } g \Delta m\}$$

That is to say, $X^{\triangleright}$ is the set of all attributes possessed by all objects in $X$ and $Y^{\triangleleft}$ is the set of all objects possessing all attributes in $Y$.

*Example 2.* In the formal context $\mathbb{K}^{2,2}$ of Tab. 1, $\{o_1\}^{\triangleright} = \{a_1, a_2\}$ and $\{a_2\}^{\triangleleft} = \{o_1\}$.

To carry out our plan, we need to learn a little more about the pair $(\triangleright, \triangleleft)$ of maps $\triangleright$: $2^G \mapsto 2^M$ and $\triangleleft$: $2^M \mapsto 2^G$. Obviously, for all $X \subseteq G$ and for all $Y \subseteq M$,

$$- X \subseteq Y^{\triangleleft} \text{ iff } X^{\triangleright} \supseteq Y.$$

Hence, the pair $(\triangleright, \triangleleft)$ of maps $\triangleright$: $2^G \mapsto 2^M$ and $\triangleleft$: $2^M \mapsto 2^G$ is a Galois connection between $(2^G, \subseteq)$ and $(2^M, \supseteq)$. Thus, for all $X, X_1, X_2 \subseteq G$ and for all $Y, Y_1, Y_2 \subseteq M$,

- if $X_1 \subseteq X_2$ then $X_1^{\triangleright} \supseteq X_2^{\triangleright}$,

- if $Y_1 \supseteq Y_2$ then $Y_1^{\triangleleft} \subseteq Y_2^{\triangleleft}$,

- $X \subseteq X^{\triangleright\triangleleft}$ and $X^{\triangleright} = X^{\triangleright\triangleleft\triangleright}$,

- $Y^{\triangleleft} \supseteq Y$ and $Y^{\triangleleft} = Y^{\triangleleft\triangleleft}$.
## 2.2 Semiconcept Algebras

Let $\mathbb{K} = (G, M, \Delta)$ be a formal context. Given $X \subseteq G$, the pair $(X, X^{\Delta})$ is called “left semiconcept of $\mathbb{K}$”. Remark that $(\emptyset, M)$ is a left semiconcept of $\mathbb{K}$. Let

$$ \mathcal{H}_l(\mathbb{K}) = (\mathcal{H}_l(\mathbb{K}), \perp_l, \top_l, \neg_l, \vee_l, \wedge_l) $$

be the algebraic structure of type $(0, 0, 1, 2, 2)$ where $\mathcal{H}_l(\mathbb{K})$ is the set of all left semiconcepts of $\mathbb{K}$, $\perp_l = (\emptyset, M)$, $\top_l = (G, G^{\Delta})$, $\neg_l(X, X^{\Delta}) = (G \setminus X, (G \setminus X)^{\Delta})$, $(X_1, X_1^{\Delta}) \vee_l (X_2, X_2^{\Delta}) = (X_1 \cup X_2, (X_1 \cup X_2)^{\Delta})$ and $(X_1, X_1^{\Delta}) \wedge_l (X_2, X_2^{\Delta}) = (X_1 \cap X_2, (X_1 \cap X_2)^{\Delta})$. Remark that if $G$ is finite then $\mathcal{H}_l(\mathbb{K})$ is finite too and moreover, $|\mathcal{H}_l(\mathbb{K})| = 2^{|G|}$. It is a simple exercise to check that the above operations $\perp_l, \top_l, \neg_l, \cdot, \vee_l, \wedge_l$ on $\mathcal{H}_l(\mathbb{K})$ are isomorphic to the Boolean operations $\emptyset, G, G \setminus, \cdot, \cup, \cap$ and $\wedge, \vee$ on $2^G$. Hence, $\mathcal{H}_l(\mathbb{K})$ satisfies the conditions of nondegenerate Boolean algebras. Given $Y \subseteq M$, the pair $(Y^{\Delta}, Y)$ is called “right semiconcept of $\mathbb{K}$”. Remark that $(G, \emptyset)$ is a right semiconcept of $\mathbb{K}$. Let

$$ \mathcal{H}_r(\mathbb{K}) = (\mathcal{H}_r(\mathbb{K}), \perp_r, \top_r, \neg_r, \vee_r, \wedge_r) $$

be the algebraic structure of type $(0, 0, 1, 2, 2)$ where $\mathcal{H}_r(\mathbb{K})$ is the set of all right semiconcepts of $\mathbb{K}$, $\perp_r = (M^{\Delta}, M)$, $\top_r = (G, \emptyset)$, $\neg_r(Y^{\Delta}, Y) = ((M \setminus Y)^{\Delta}, M \setminus Y)$, $(Y_1^{\Delta}, Y_1) \vee_r (Y_2^{\Delta}, Y_2) = ((Y_1 \cap Y_2)^{\Delta}, Y_1 \cap Y_2)$ and $(Y_1^{\Delta}, Y_1) \wedge_r (Y_2^{\Delta}, Y_2) = ((Y_1 \cup Y_2)^{\Delta}, Y_1 \cup Y_2)$. Remark that if $M$ is finite then $\mathcal{H}_r(\mathbb{K})$ is finite too and moreover, $|\mathcal{H}_r(\mathbb{K})| = 2^{|M|}$. It is a simple exercise to check that the above operations $\perp_r, \top_r, \neg_r, \cdot, \vee_r, \wedge_r$ on $\mathcal{H}_r(\mathbb{K})$ are anti-isomorphic to the Boolean operations $\emptyset, M, M \setminus, \cdot, \cup, \cap$ and $\wedge, \vee$ on $2^M$. Hence, $\mathcal{H}_r(\mathbb{K})$ satisfies the conditions of nondegenerate Boolean algebras. Now, for the concept underlying most of our work in this article. Given $X \subseteq G$ and $Y \subseteq M$, the pair $(X, Y)$ is called “semiconcept of $\mathbb{K}$” iff $Y = X^{\Delta}$ or $X = Y^{\Delta}$. Remark that $(\emptyset, M)$ and $(G, \emptyset)$ are semiconcepts of $\mathbb{K}$.

**Example 3.** In the formal context $\mathbb{K}^{2,2}$ of Tab. 1, the semiconcepts are $(\emptyset, \{a_1, a_2\})$, $(\{o_1\}, \{a_1, a_2\})$, $(\{o_2\}, \{a_1\})$, $(\{o_1\}, \{a_2\})$, $(\{o_1, o_2\}, \{a_1\})$ and $(\{o_1, o_2\}, \emptyset)$. Let

$$ \mathcal{H}(\mathbb{K}) = (\mathcal{H}(\mathbb{K}), \perp_l, \top_l, \neg_l, \vee_l, \wedge_l, \top_r, \neg_r, \vee_r, \wedge_r) $$

be the algebraic structure of type $(0, 0, 0, 0, 1, 1, 2, 2, 2, 2)$ where $\mathcal{H}(\mathbb{K})$ is the set of all semiconcepts of $\mathbb{K}$, $\perp_l = (\emptyset, M)$, $\top_l = (M^{\Delta}, M)$, $\neg_l(X, Y) = (G \setminus X, (G \setminus X)^{\Delta})$, $\top_r = (G, \emptyset)$, $\neg_r(X, Y) = ((M \setminus Y)^{\Delta}, M \setminus Y)$, $(X_1, Y_1) \vee_l (X_2, Y_2) = (X_1 \cup X_2, (X_1 \cup X_2)^{\Delta})$, $(X_1, Y_1) \vee_r (X_2, Y_2) = ((Y_1 \cap Y_2)^{\Delta}, Y_1 \cap Y_2)$, $(X_1, Y_1) \wedge_l (X_2, Y_2) = (X_1 \cap X_2, (X_1 \cap X_2)^{\Delta})$ and $(X_1, Y_1) \wedge_r (X_2, Y_2) = ((Y_1 \cup Y_2)^{\Delta}, Y_1 \cup Y_2)$.

**Example 4.** In the formal context $\mathbb{K}^{2,2}$ of Tab. 1, $\perp_l = (\emptyset, \{a_1, a_2\})$, $\top_l = (\{o_1, o_2\}, \{a_1\})$, $\top_r = (\{o_1, o_2\}, \emptyset)$, $\neg_l = (\{o_1\}, \{a_1, a_2\})$ and $\neg_r = (\{o_1, o_2\}, \emptyset)$.

Remark that if $G, M$ are finite then $\mathcal{H}(\mathbb{K})$ is finite too and moreover, $|\mathcal{H}(\mathbb{K})| \le 2^{|G|} + 2^{|M|}$. Obviously, the operations $\perp_l, \top_l, \neg_l, \cdot, \vee_l, \wedge_l$ and $\wedge, \vee$ on $\mathcal{H}(\mathbb{K})$ when restricted to the set of all left semiconcepts of $\mathbb{K}$, are isomorphic to the Boolean operations
Ø, G, G \-, . ∪ . and . ∩ . on 2<sup>G</sup> whereas the operations ⊥<sub>r</sub>, ⊤<sub>r</sub>, ¬<sub>r</sub>, . ∨<sub>r</sub> . and . ∧<sub>r</sub> ., when restricted to the set of all right semiconcepts of IK, are anti-isomorphic to the Boolean operations Ø, M, M \-, . ∪ . and . ∩ . on 2<sup>M</sup>. In other respects, it is a simple matter to check that ℋ(IK) satisfies the following conditions for every x, y, z ∈ ℋ(IK):

$$
- x \wedge_l (y \wedge_l z) = (x \wedge_l y) \wedge_l z \text{ and } x \vee_r (y \vee_r z) = (x \vee_r y) \vee_r z,
$$

$$
- x \wedge_l y = y \wedge_l x \text{ and } x \vee_r y = y \vee_r x,
$$

$$
- \neg_l (x \wedge_l x) = \neg_l x \text{ and } \neg_r (x \vee_r x) = \neg_r x,
$$

$$
- x \wedge_l (y \wedge_l y) = x \wedge_l y \text{ and } x \vee_r (y \vee_r y) = x \vee_r y,
$$

$$
- x \wedge_l (y \vee_l z) = (x \wedge_l y) \vee_l (x \wedge_l z) \text{ and } x \vee_r (y \wedge_r z) = (x \vee_r y) \wedge_r (x \vee_r z),
$$

$$
- x \wedge_l (x \vee_l y) = x \wedge_l x \text{ and } x \vee_r (x \wedge_r y) = x \vee_r x,
$$

$$
- x \wedge_l (x \vee_r y) = x \wedge_l x \text{ and } x \vee_r (x \wedge_l y) = x \vee_r x,
$$

$$
- \neg_l (\neg_l x \wedge_l \neg_l y) = x \vee_l y \text{ and } \neg_r (\neg_r x \vee_r \neg_r y) = x \wedge_r y,
$$

$$
- \neg_l \bot_l = \top_l \text{ and } \neg_r \top_r = \bot_r,
$$

$$
- \neg_l \top_r = \bot_l \text{ and } \neg_r \bot_l = \top_r,
$$

$$
- \top_r \wedge_l \top_r = \top_l \text{ and } \bot_l \vee_r \bot_l = \bot_r,
$$

$$
- x \wedge_l \neg_l x = \bot_l \text{ and } x \vee_r \neg_r x = \top_r,
$$

$$
- \neg_l \neg_l (x \wedge_l y) = x \wedge_l y \text{ and } \neg_r \neg_r (x \vee_r y) = x \vee_r y,
$$

$$
- (x \wedge_l x) \vee_r (x \wedge_l x) = (x \vee_r x) \wedge_l (x \vee_r x),
$$

$$
- x \wedge_l x = x \text{ or } x \vee_r x = x.
$$

Let us remark that the first 13 above conditions come in pairs of mirror images
obtained by interchanging $⊥_l$ with $⊤_r$, $⊤_l$ with $⊥_r$, $¬_l$ with $¬_r$, $∇_l$ with $∧_r$
and $∧_l$ with $∇_r$ whereas the last 2 above conditions are equivalent to their own
mirror images. This leads us to the principle of duality stating that from any
condition provable from the 15 above conditions, another such condition results
immediately by interchanging $⊥_l$ with $⊤_r$, $⊤_l$ with $⊥_r$, $¬_l$ with $¬_r$, $∇_l$ with $∧_r$
and $∧_l$ with $∇_r$. The set $\mathcal{H}(\mathbb{K})$ can be ordered by the binary relation $⊆$ defined
by

$$
(X_1, Y_1) \subseteq (X_2, Y_2) \text{ iff } X_1 \subseteq X_2 \text{ and } Y_1 \supseteq Y_2
$$

for every (X₁, Y₁), (X₂, Y₂) ∈ ℋ(IK). Obviously, for all (X₁, Y₁), (X₂, Y₂) ∈ ℋ(IK),

$$
- (X_1, Y_1) \subseteq (X_2, Y_2) \text{ iff } (X_1, Y_1) \wedge_l (X_2, Y_2) = (X_1, Y_1) \wedge_l (X_1, Y_1) \text{ and } (X_1, Y_1) \vee_r (X_2, Y_2) = (X_2, Y_2) \vee_r (X_2, Y_2),
$$

$$
- \text{ if } (X_1, Y_1) \in \mathcal{H}_l(\mathbb{K}) \text{ then } (X_1, Y_1) \subseteq (X_2, Y_2) \text{ iff } (X_1, Y_1) \wedge_l (X_2, Y_2) = (X_1, Y_1),
$$

$$
- \text{ if } (X_2, Y_2) \in \mathcal{H}_r(\mathbb{K}) \text{ then } (X_1, Y_1) \sqsubseteq (X_2, Y_2) \text{ iff } (X_1, Y_1) \vee_r (X_2, Y_2) = (X_2, Y_2).
$$

Moreover, the binary relation ⊑ is reflexive, antisymmetric and transitive on ℋ(IK). In order to give an abstract characterization of the operations ⊥<sub>l</sub>, ⊥<sub>r</sub>, ⊤<sub>l</sub>, ⊤<sub>r</sub>, ¬<sub>l</sub>, ¬<sub>r</sub>, ∨<sub>l</sub>, ∨<sub>r</sub>, ∧<sub>l</sub> and ∧<sub>r</sub>, we shall say that an algebraic structure 𝒩 = (D, ⊥<sub>l</sub>, ⊥<sub>r</sub>, ⊤<sub>l</sub>, ⊤<sub>r</sub>, ¬<sub>l</sub>, ¬<sub>r</sub>, ∨<sub>l</sub>, ∨<sub>r</sub>, ∧<sub>l</sub>, ∧<sub>r</sub>) of type (0, 0, 0, 0, 1, 1, 2, 2, 2, 2) is a pure double Boolean algebra iff the operations ⊥<sub>l</sub>, ⊥<sub>r</sub>, ⊤<sub>l</sub>, ⊤<sub>r</sub>, ¬<sub>l</sub>, ¬<sub>r</sub>, ∨<sub>l</sub>, ∨<sub>r</sub>, ∧<sub>l</sub> and ∧<sub>r</sub> satisfy the 15 above conditions.
# 3 From Semiconcept Algebras to Formal Contexts

The aim of this section is to give an abstract characterization of the operations $⊥_l, ⊥_r, ⊤_l, ⊤_r, ¬_l, ¬_r, ∨_l, ∨_r, ∧_l, ∧_r$ and $∧_r$.

## 3.1 Filters and Ideals

Let $\mathcal{D} = (D, ⊥_l, ⊥_r, ⊤_l, ⊤_r, ¬_l, ¬_r, ∨_l, ∨_r, ∧_l, ∧_r)$ be a pure double Boolean algebra. We define

$$D_l = \{x \wedge_l x : x \in D\} \\ D_r = \{x \vee_r x : x \in D\}$$

Intuitively, elements of $D_l$ can be considered as sets of objects and elements of $D_r$ can be considered as sets of attributes.

**Example 5.** In the semiconcept algebra associated to the formal context $\mathbb{K}^{2,2}$ of Tab. 1, $D^{2,2} = \{(\emptyset, \{a_1, a_2\}), (\{o_1\}, \{a_1, a_2\}), (\{o_2\}, \{a_1\}), (\{o_1\}, \{a_2\}), (\{o_1, o_2\}, \{a_1\}), (\{o_1, o_2\}, \emptyset)\}$, $D_l^{2,2} = \{(\emptyset, \{a_1, a_2\}), (\{o_1\}, \{a_1, a_2\}), (\{o_2\}, \{a_1\}), (\{o_1, o_2\}, \{a_1\})\}$ and $D_r^{2,2} = \{(\{o_1\}, \{a_1, a_2\}), (\{o_1, o_2\}, \{a_1\}), (\{o_1\}, \{a_2\}), (\{o_1, o_2\}, \emptyset)\}$.

Obviously, the operations $⊥_l, ⊤_l, ¬_l, ∨_l$ and $∧_l$ are stable on $D_l$ and the operations $⊥_r, ⊤_r, ¬_r, ∨_r$ and $∧_r$ are stable on $D_r$. Hence, the algebraic structures $D_l = (D_l, ⊥_l, ⊤_l, ¬_l, ∨_l, ∧_l)$ and $D_r = (D_r, ⊤_r, ⊥_r, ¬_r, ∨_r, ∧_r)$ are algebraic structures of type $(0, 0, 1, 2, 2)$. More precisely, they are Boolean algebras. Moreover, the set $D$ can be ordered by the binary relation $≤$ defined by

$$x \leq y \text{ iff } x \wedge_l y = x \wedge_l x \text{ and } x \vee_r y = y \vee_r y$$

for every $x, y \in D$. Obviously, for all $x, y \in D$,

- if $x \in D_l$ then $x \leq y$ iff $x \wedge_l y = x$,

- if $y \in D_r$ then $x \leq y$ iff $x \vee_r y = y$.

Moreover, the binary relation $≤$ is reflexive, antisymmetric and transitive on $D$.

<figure><img src="image_3.png" /><figcaption>Fig. 1.</figcaption></figure>
*Example 6.* In Fig. 1 is represented the binary relation $\leq^{2,2}$ ordering the set $D^{2,2}$ of the semiconcept algebra associated to the formal context $\mathbb{K}^{2,2}$ of Tab. 1.

A nonempty subset $F$ of $D$ is called a filter iff for all $x, y \in D$,

$$-x, y \in F \text{ implies } x \wedge_l y \in F,$$

$$-x \in F \text{ and } x \leq y \text{ imply } y \in F.$$

A nonempty subset $I$ of $D$ is called an ideal iff for all $x, y \in D$,

$$-x, y \in I \text{ implies } x \vee_r y \in I,$$

$$-x \in I \text{ and } y \leq x \text{ imply } y \in I.$$

The following lemma explains how filters and ideals can be transformed into filters and ideals of the Boolean algebras $\mathcal{D}_l$ and $\mathcal{D}_r$.

**Lemma 1.** Let $F, I$ be nonempty subsets of $D$. If $F$ is a filter then $F \cap D_l$ is a filter of the Boolean algebra $\mathcal{D}_l$ and $F \cap D_r$ is a filter of the Boolean algebra $\mathcal{D}_r$ and if $I$ is an ideal then $I \cap D_l$ is an ideal of the Boolean algebra $\mathcal{D}_l$ and $I \cap D_r$ is an ideal of the Boolean algebra $\mathcal{D}_r$.

Let $F$ be a nonempty subset of $D_l$ and $I$ be a nonempty subset of $D_r$. We define

$$[F] = \{x \in D: \text{there exists } y \in F \text{ such that } y \leq x\}$$

$$(I] = \{x \in D: \text{there exists } y \in I \text{ such that } x \leq y\}$$

The following lemma explains how filters of the Boolean algebra $\mathcal{D}_l$ and ideals of the Boolean algebra $\mathcal{D}_r$ can be transformed into filters and ideals.

**Lemma 2.** Let $F$ be a nonempty subset of $D_l$, $I$ be a nonempty subset of $D_r$. If $F$ is a filter of the Boolean algebra $\mathcal{D}_l$ then $[F)$ is a filter and $[F) \cap D_l = F$ and if $I$ is an ideal of the Boolean algebra $\mathcal{D}_r$ then $(I]$ is an ideal and $(I] \cap D_r = I$.

As a result,

**Lemma 3.** There exists filters $F$ such that $F \cap D_l$ is a prime filter of the Boolean algebra $\mathcal{D}_l$ and there exists ideals $I$ such that $I \cap D_r$ is a prime ideal of the Boolean algebra $\mathcal{D}_r$.

We shall say that $\mathcal{D}$ is concrete iff there exists a formal context $\mathbb{K}$ and a function $h$ assigning to each element of $D$ an element of $\mathcal{H}(\mathbb{K})$ such that $h$ is injective and $h$ is a homomorphism from $\mathcal{D}$ to $\mathcal{H}(\mathbb{K})$.

## 3.2 Representation

Now, the main question is to prove that every pure double Boolean algebra is concrete. Let $\mathcal{D} = (D, \perp_l, \perp_r, \top_l, \top_r, \neg_l, \neg_r, \vee_l, \vee_r, \wedge_l, \wedge_r)$ be a pure double Boolean algebra and consider the formal context

$$\mathbb{K}(D) = (\mathcal{F}_p(D), \mathcal{I}_p(D), \Delta)$$
where $\mathcal{F}_p(D)$ is the set of all filters $F$ for which $F \cap D_l$ is a prime filter of the Boolean algebra $\mathcal{D}_l$, $\mathcal{I}_p(D)$ is the set of all ideals $I$ for which $I \cap D_r$ is a prime ideal of the Boolean algebra $\mathcal{D}_r$ and $F \Delta I$ iff $F \cap I$ is nonempty. Let

$$ \mathcal{H}(\mathcal{K}(D)) = (\mathcal{H}(\mathcal{K}(D)), \perp'_l, \perp'_r, \top'_l, \top'_r, \neg'_l, \neg'_r, \vee'_l, \vee'_r, \wedge'_l, \wedge'_r) $$

For all elements $x$ of $D$, let

$$ \mathcal{F}_x = \{F \in \mathcal{F}_p(D) : x \in F\} $$

$$ \mathcal{I}_x = \{I \in \mathcal{I}_p(D) : x \in I\} $$

Here, the first results are

**Lemma 4.** Let $x \in D$. $\mathcal{F}_{x \wedge l x} = \mathcal{F}_x$ and $\mathcal{I}_{x \vee r x} = \mathcal{I}_x$.

**Lemma 5.** Let $x \in D$. If $x \in D_l$ then $\mathcal{F}_x^\Delta = \mathcal{I}_x$ and if $x \in D_r$ then $\mathcal{I}_x^\Delta = \mathcal{F}_x$.

**Lemma 6.** Let $x \in D$. $\mathcal{F}_{\neg_l \neg_l x}^\Delta = \mathcal{I}_{\neg_l \neg_l x}$ and $\mathcal{I}_{\neg_r \neg_r x}^\Delta = \mathcal{F}_{\neg_r \neg_r x}$.

The next lemmas point the way to the strategy followed in our approach to the proof that every pure double Boolean algebra is concrete.

**Lemma 7.** Let $x \in D$. The pair $(\mathcal{F}_x, \mathcal{I}_x)$ is a semiconcept of $\mathcal{K}(D)$.

**Lemma 8.** Let $x, y \in D$. If $x \neq y$ then $(\mathcal{F}_x, \mathcal{I}_x) \neq (\mathcal{F}_y, \mathcal{I}_y)$.

For all $x \in D$, let

$$ h(x) = (\mathcal{F}_x, \mathcal{I}_x) $$

The next lemma is central for proving that the function $h$ is a homomorphism from $\mathcal{D}$ to $\mathcal{H}(\mathcal{K})$.

**Lemma 9.** Let $x, y \in D$.

$$ - \mathcal{F}_{\perp l} = \emptyset \text{ and } \mathcal{I}_{\perp l} = \mathcal{I}_p(D), $$

$$ - \mathcal{F}_{\perp r} = \mathcal{I}_p(D)^{\Delta} \text{ and } \mathcal{I}_{\perp r} = \mathcal{I}_p(D), $$

$$ - \mathcal{F}_{\top l} = \mathcal{F}_p(D) \text{ and } \mathcal{I}_{\top l} = \mathcal{F}_p(D)^{\Delta}, $$

$$ - \mathcal{F}_{\top r} = \mathcal{F}_p(D) \text{ and } \mathcal{I}_{\top r} = \emptyset, $$

$$ - \mathcal{F}_{\neg_l x} = \mathcal{F}_p(D) \setminus \mathcal{F}_x \text{ and } \mathcal{I}_{\neg_l x} = (\mathcal{F}_p(D) \setminus \mathcal{F}_x)^{\Delta}, $$

$$ - \mathcal{F}_{\neg_r x} = (\mathcal{I}_p(D) \setminus \mathcal{I}_x)^{\Delta} \text{ and } \mathcal{I}_{\neg_r x} = \mathcal{I}_p(D) \setminus \mathcal{I}_x, $$

$$ - \mathcal{F}_{x \vee l y} = \mathcal{F}_x \cup \mathcal{F}_y \text{ and } \mathcal{I}_{x \vee l y} = (\mathcal{F}_x \cup \mathcal{F}_y)^{\Delta}, $$

$$ - \mathcal{F}_{x \vee r y} = (\mathcal{I}_x \cap \mathcal{I}_y)^{\Delta} \text{ and } \mathcal{I}_{x \vee r y} = \mathcal{I}_x \cap \mathcal{I}_y, $$

$$ - \mathcal{F}_{x \wedge l y} = \mathcal{F}_x \cap \mathcal{F}_y \text{ and } \mathcal{I}_{x \wedge l y} = (\mathcal{F}_x \cap \mathcal{F}_y)^{\Delta}, $$

$$ - \mathcal{F}_{x \wedge r y} = (\mathcal{I}_x \cup \mathcal{I}_y)^{\Delta} \text{ and } \mathcal{I}_{x \wedge r y} = \mathcal{I}_x \cup \mathcal{I}_y. $$

As a result,

**Theorem 1.** The function $h$ is a homomorphism from $\mathcal{D}$ to $\mathcal{H}(\mathcal{K})$.

In other words: every pure double Boolean algebra is concrete.
# 4 The Word Problem in Pure Double Boolean Algebras

Let us introduce the word problem in pure double Boolean algebras.

## 4.1 Syntax

Let $Var$ denote a countable set of individual variables (with typical instances denoted $x$, $y$, etc). The set $t(Var)$ of all terms (with typical instances denoted $s$, $t$, etc) is given by the rule

$$s ::= x \mid 0_l \mid 0_r \mid 1_l \mid 1_r \mid -l s \mid -r s \mid (s \sqcup_l t) \mid (s \sqcup_r t) \mid (s \sqcap_l t) \mid (s \sqcap_r t)$$

Let us adopt the standard rules for omission of the parentheses.

*Example 7.* For instance, $x \sqcap_l (x \sqcup_r y)$ is a term.

## 4.2 Semantics

Let $\mathcal{D} = (D, \perp_l, \perp_r, \top_l, \top_r, \neg_l, \neg_r, \vee_l, \vee_r, \wedge_l, \wedge_r)$ be a pure double Boolean algebra. A valuation based on $\mathcal{D}$ is a function $m$ assigning to each individual variable $x$ an element $m(x)$ of $D$.

*Example 8.* The function $m^{2,2}$ defined below is a valuation based on the pure double Boolean algebra $\mathcal{D}^{2,2}$ defined in Example 5: $m^{2,2}(x) = (\{o_2\}, \{a_1\})$, $m^{2,2}(y) = (\{o_1\}, \{a_2\})$ and for all individual variables $z$, if $z \neq x, y$ then $m^{2,2}(z) = (\{o_1, o_2\}, \{a_1\})$.

$m$ induces a function $(\cdot)^m$ assigning to each term $s$ an element $(s)^m$ of $D$ such that $(x)^m = m(x)$, $(0_l)^m = \perp_l$, $(0_r)^m = \perp_r$, $(1_l)^m = \top_l$, $(1_r)^m = \top_r$, $(-l s)^m = \neg_l(s)^m$, $(-r s)^m = \neg_r(s)^m$, $(s \sqcup_l t)^m = (s)^m \vee_l (t)^m$, $(s \sqcup_r t)^m = (s)^m \vee_r (t)^m$, $(s \sqcap_l t)^m = (s)^m \wedge_l (t)^m$ and $(s \sqcap_r t)^m = (s)^m \wedge_r (t)^m$.

*Example 9.* Concerning the valuation $m^{2,2}$ defined in Example 8, we have $(x \sqcup_r y)^{m^{2,2}} = (\{o_1, o_2\}, \emptyset)$ and $(-l x)^{m^{2,2}} = (\{o_1\}, \{a_1, a_2\})$.

## 4.3 The Word Problem

Now, for the WP in pure double Boolean algebras:

**input:** terms $s, t$,

**output:** determine whether there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \neq (t)^m$.

A general strategy for proving a decision problem to be **PSPACE**-complete is first, to reduce to it a decision problem easily proved to be **PSPACE**-hard and second, to reduce it to a decision problem easily proved to be in **PSPACE**. **PSPACE** is the key complexity class of the satisfiability problem of numerous modal logics [1, Chapter 6]. Therefore, we introduce in Section 5 a **PSPACE**-complete modal logic and we show in Sections 6 and 7 how to reduce one into the other its satisfiability problem and the WP in pure double Boolean algebras.
# 5 A Basic 2-Sorted Modal Logic

In Section 3, we gave the proof that every pure double Boolean algebra can be homomorphically embedded into the pure double Boolean algebra over some formal context. Formal contexts are 2-sorted structures. Hence, the modal logic that will be used in Sections 6 and 7 for proving the WP in pure double Boolean algebras to be PSPACE-complete is a 2-sorted one.

## 5.1 Syntax

The language of $K_2$ is based on a countable set $OVar$ of object variables (with typical instances denoted $P$, $Q$, etc) and a countable set $AVar$ of attribute variables (with typical instances denoted $p$, $q$, etc). Without loss of generality, let us assume that $OVar$ and $AVar$ are disjoint. The set of all object formulas (with typical instances denoted $A$, $B$, etc) and the set of all attribute formulas (with typical instances denoted $a$, $b$, etc) are given by the rules

$$A ::= P \mid \bot \mid \neg A \mid (A \lor B) \mid \Box a$$

$$a ::= p \mid \bot \mid \neg a \mid (a \lor b) \mid \Box A$$

The other Boolean constructs are defined as usual. Let us adopt the standard rules for omission of the parentheses. A formula (with typical instances denoted $\alpha$, $\beta$, etc) is either an object formula or an attribute formula. The notion of “being a subformula of” is standard, the expression $\alpha \ll \beta$ denoting the fact that $\alpha$ is a subformula of $\beta$. A substitution is a pair $(\Theta, \theta)$ where $\Theta$ is a function assigning to each object variable $P$ an object formula $\Theta(P)$ and $\theta$ is a function assigning to each attribute variable $p$ an attribute formula $\theta(p)$. $(\Theta, \theta)$ induces a homomorphism $\cdot:(\Theta,\theta)$ assigning to each formula $\alpha$ a formula $(\alpha)^{(\Theta,\theta)}$ such that $(P)^{(\Theta,\theta)} = \Theta(P)$ and $(p)^{(\Theta,\theta)} = \theta(p)$. Remark that for all object formulas $A$ and for all attribute formulas $a$,

- $(A)^{(\Theta,\theta)}$ is an object formula,

- $(a)^{(\Theta,\theta)}$ is an attribute formula.

Let $OVar = P_1, P_2, \dots$ be an enumeration of $OVar$ and $AVar = p_1, p_2, \dots$ be an enumeration of $AVar$. We shall say that a substitution $(\Theta, \theta)$ is normal with respect to $OVar$ and $AVar$ iff for all positive integers $i$,

$$- \Theta(P_i) = P_i \text{ and } \theta(p_i) = \Box P_i \text{ or } \Theta(P_i) = \Box p_i \text{ and } \theta(p_i) = p_i.$$

Given a formula $\alpha$, $Var(\alpha)$ will denote the set of all variables occurring in $\alpha$. A formula $\alpha$ is said to be nice iff

$$- Var(\alpha) \subseteq OVar \text{ or } Var(\alpha) \subseteq AVar.$$
## 5.2 Semantics

Let $\mathbb{K} = (G, M, \Delta)$ be a formal context. A $\mathbb{K}$-valuation is a pair $(V, v)$ of functions where $V$ assigns to each object variable $P$ a subset $V(P)$ of $G$ and $v$ assigns to each attribute variable $p$ a subset $v(p)$ of $M$. $(V, v)$ induces a function $\cdot^{(V,v)}$ assigning to each formula $\alpha$ a subset $(\alpha)^{(V,v)}$ of $G \cup M$ such that $(P)^{(V,v)} = V(P), (\perp)^{(V,v)} = \emptyset, (\neg A)^{(V,v)} = G \setminus (A)^{(V,v)}, (A \lor B)^{(V,v)} = (A)^{(V,v)} \cup (B)^{(V,v)}, (\Box a)^{(V,v)} = \{g \in G: \text{ for all } m \in M, \text{ if } m \in (a)^{(V,v)} \text{ then } g \Delta m \}, (p)^{(V,v)} = v(p), (\perp)^{(V,v)} = \emptyset, (\neg a)^{(V,v)} = M \setminus (a)^{(V,v)}, (a \lor b)^{(V,v)} = (a)^{(V,v)} \cup (b)^{(V,v)} \text{ and } (\Box A)^{(V,v)} = \{m \in M: \text{ for all } g \in G, \text{ if } g \in (A)^{(V,v)} \text{ then } g \Delta m \}$. Remark that for all object formulas $A$ and for all attribute formulas $a$,

- $(A)^{(V,v)}$ is a subset of $G$ such that $(A)^{(V,v)\Delta} = (\Box A)^{(V,v)}$,

- $(a)^{(V,v)}$ is a subset of $M$ such that $(a)^{(V,v)\ominus} = (\Box a)^{(V,v)}$.

A formula $\alpha$ is said to be satisfiable iff

- there exists a formal context $\mathbb{K} = (G, M, \Delta)$ and a $\mathbb{K}$-valuation $(V, v)$ such that $(\alpha)^{(V,v)}$ is nonempty.

## 5.3 Decision

Now, for the nice satisfiability problem for $K_2$:

**input:** a nice formula $\alpha$,

**output:** determine whether $\alpha$ is satisfiable.

The next lemmas are central for proving that the problem of deciding equations in pure double Boolean algebras is **PSPACE**-complete.

**Theorem 2.** *The nice satisfiability problem for $K_2$ is PSPACE-hard.*

*Proof.* A reduction similar to the reduction from the $QBF$-validity problem to the satisfiability problem for $K$ considered in [1, Theorem 6.50] can be easily obtained.

Now, for the satisfiability problem for $K_2$:

**input:** a formula $\alpha$,

**output:** determine whether $\alpha$ is satisfiable.

**Theorem 3.** *The satisfiability problem for $K_2$ is in PSPACE.*

*Proof.* An algorithm similar to the *Witness* algorithm considered in [1, Theorem 6.47] can be easily obtained.

From Theorems 2 and 3, it follows immediately that the nice satisfiability problem for $K_2$ and the satisfiability problem for $\tilde{K}_2$ are both **PSPACE**-complete.
# 6 From $K_2$ to Pure Double Boolean Algebras

First, we consider the lower bound of the complexity of the problem of deciding the WP in pure double Boolean algebras. Given a nice formula $\alpha$, we wish to construct a pair $(s_1(\alpha), s_2(\alpha))$ of terms such that $\alpha$ is satisfiable iff there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s_1(\alpha))^m \neq (s_2(\alpha))^m$. Let $OVar = P_1, P_2, \dots$ be an enumeration of $OVar$, $AVar = p_1, p_2, \dots$ be an enumeration of $AVar$ and $Var = x_1, y_1, x_2, y_2, \dots$ be an enumeration of $Var$. The function $T(\cdot)$ assigning to each nice object formula $A$ a term $T(A)$ and the function $t(\cdot)$ assigning to each nice attribute formula $a$ a term $t(a)$ are such that $T(P_i) = x_i$, $T(\perp) = 0_l$, $T(\neg A) = -lT(A)$, $T(A \vee B) = T(A) \sqcup_l T(B)$, $T(\Box a) = -l -l -r -r t(a)$, $t(p_i) = y_i$, $t(\perp) = 1_r$, $t(\neg a) = -r t(a)$, $t(a \vee b) = t(a) \sqcap_r t(b)$ and $t(\Box A) = -r -r -l -l T(A)$. Let $(s_1(\cdot), s_2(\cdot))$ be the function assigning to each nice formula $\alpha$ a pair $(s_1(\alpha), s_2(\alpha))$ of terms such that if $\alpha$ is a nice object formula then $s_1(\alpha) = T(\alpha)$ and $s_2(\alpha) = 0_l$ and if $\alpha$ is a nice attribute formula then $s_1(\alpha) = t(\alpha)$ and $s_2(\alpha) = 1_r$. Obviously, $(s_1(\alpha), s_2(\alpha))$ can be computed in space $\log |\alpha|$. Moreover,

**Proposition 1.** If $\alpha$ is nice then $\alpha$ is satisfiable iff there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s_1(\alpha))^m \neq (s_2(\alpha))^m$.

*Proof.* Since $\alpha$ is nice, $Var(\alpha) \subseteq OVar$ or $Var(\alpha) \subseteq AVar$. Without loss of generality, let us assume that $Var(\alpha) \subseteq OVar$. Hence, there exists a positive integer $n$ such that $Var(\alpha) \subseteq \{P_1, \dots, P_n\}$.

(⇒) Suppose $\alpha$ is satisfiable, we demonstrate there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s_1(\alpha))^m \neq (s_2(\alpha))^m$. Since $\alpha$ is satisfiable, there exists a formal context $\mathbb{K} = (G, M, \Delta)$ and a valuation $(V, v)$ based on $\mathbb{K}$ such that $(\alpha)^{(V,v)}$ is nonempty. Let $\mathcal{H}(\mathbb{K}) = (\mathcal{H}(\mathbb{K}), \perp_l, \perp_r, \top_l, \top_r, \neg_l, \neg_r, \vee_l, \vee_r, \wedge_l, \wedge_r)$ and $m$ be a valuation based on $\mathcal{H}(\mathbb{K})$ such that for all positive integers $i$, if $i \le n$ then $m(x_i) = (V(P_i), V(P_i)^{\Delta})$. We show first that

**Lemma 10.** Let $A$ be a nice object formula and $A$ be a nice attribute formula. If $A \ll \alpha$ then $(T(A))^m = ((A)^{(V,v)}, (A)^{(V,v)^{\Delta}})$ and if $A \ll \alpha$ then $(t(a))^m = ((a)^{(V,v)^{\Delta}}, (a)^{(V,v)})$.

Continuing the proof of Proposition 1, since $(\alpha)^{(V,v)}$ is nonempty, by Lemma 10, if $\alpha$ is a nice object formula then $(T(\alpha))^m \neq (0_l)^m$ and if $\alpha$ is a nice attribute formula then $(t(\alpha))^m \neq (1_r)^m$. Hence, $(s_1(\alpha))^m \neq (s_2(\alpha))^m$. Thus, there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s_1(\alpha))^m \neq (s_2(\alpha))^m$.

(←) Suppose there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s_1(\alpha))^m \neq (s_2(\alpha))^m$, we demonstrate $\alpha$ is satisfiable. Let $\mathbb{K}(D) = (\mathcal{F}_p(D), \mathcal{I}_p(D), \Delta)$ and $(V, v)$ be a valuation based on $\mathbb{K}(D)$ such that for all positive integers $i$, if $i \le n$ then $V(P_i) = \mathcal{F}_{m(x_i)}$. Interestingly,

**Lemma 11.** Let $A$ be a nice object formula and $A$ be a nice attribute formula. If $A \ll \alpha$ then $(A)^{(V,v)} = \mathcal{F}_{(T(A))^m}$ and if $A \ll \alpha$ then $(A)^{(V,v)} = \mathcal{I}_{(t(a))^m}$.
Continuing the proof of Proposition 1, since $(s_1(\alpha))^m \neq (s_2(\alpha))^m$, if $\alpha$ is a nice object formula then $(T(\alpha))^m \neq (0_l)^m$ and if $\alpha$ is a nice attribute formula then $(t(\alpha))^m \neq (1_r)^m$. Hence, by Lemma 11, $(\alpha)^{(V,v)}$ is nonempty. Thus, $\alpha$ is satisfiable. This ends the proof of Proposition 1.

Hence, $(s_1(\cdot), s_2(\cdot))$ is a reduction from the nice satisfiability problem for $K_2$ to the WP in pure double Boolean algebras. Thus, by Theorem 2,

**Corollary 1.** The WP in pure double Boolean algebras is PSPACE-hard.

# 7 From Pure Double Boolean Algebras to $K_2$

Second, we consider the upper bound of the complexity of the WP in pure double Boolean algebras. Given a pair $(s,t)$ of terms, we wish to construct an object formula $O(s,t)$ and an attribute formula $A(s,t)$ such that there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \neq (t)^m$ iff some instance of $O(s,t)$ is satisfiable or some instance of $A(s,t)$ is satisfiable. Let $\mathbf{Var} = x_1, x_2, \dots$ be an enumeration of $\mathbf{Var}$, $\mathbf{OVar} = P_1, P_2, \dots$ be an enumeration of $\mathbf{OVar}$ and $\mathbf{AVar} = p_1, p_2, \dots$ be an enumeration of $\mathbf{AVar}$. The function $F(\cdot)$ assigning to each term $s$ an object formula $F(s)$ and the function $f(\cdot)$ assigning to each term $s$ an attribute formula $f(s)$ are such that $F(x_i) = P_i$, $f(x_i) = p_i$, $F(0_l) = \bot$, $f(0_l) = \Box \bot$, $F(0_r) = \Box \top$, $f(0_r) = \top$, $F(1_l) = \top$, $f(1_l) = \Box \top$, $F(1_r) = \Box \bot$, $f(1_r) = \bot$, $F(-l s) = \neg F(s)$, $f(-l s) = \Box \neg F(s)$, $F(-r s) = \Box \neg f(s)$, $f(-r s) = \neg f(s)$, $F(s \sqcup_l t) = F(s) \lor F(t)$, $f(s \sqcup_l t) = \Box (F(s) \lor F(t))$, $F(s \sqcup_r t) = \Box (f(s) \land f(t))$, $f(s \sqcup_r t) = f(s) \land f(t)$, $F(s \sqcap_l t) = F(s) \land F(t)$, $f(s \sqcap_l t) = \Box (F(s) \land F(t))$, $F(s \sqcap_r t) = \Box (f(s) \lor f(t))$ and $f(s \sqcap_r t) = f(s) \lor f(t)$. Let $O(\cdot, \cdot)$ be the function assigning to each pair $(s,t)$ of terms the object formula $O(s,t)$ such that $O(s,t) = \neg(F(s) \leftrightarrow F(t))$. Let $A(\cdot, \cdot)$ be the function assigning to each pair $(s,t)$ of terms the attribute formula $A(s,t)$ such that $A(s,t) = \neg(f(s) \leftrightarrow f(t))$. Obviously, $O(s,t)$ and $A(s,t)$ can be computed in space $\log |(s,t)|$. Moreover,

**Proposition 2.** There exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \neq (t)^m$ iff there exists a substitution $(\Theta, \theta)$ such that $(\Theta, \theta)$ is normal with respect to $\mathbf{OVar}$ and $\mathbf{AVar}$ and $O(s,t)^{(\Theta,\theta)}$ is satisfiable or $A(s,t)^{(\Theta,\theta)}$ is satisfiable.

*Proof.* Let $n$ be a positive integer such that $\mathrm{Var}(s) \cup \mathrm{Var}(t) \subseteq \{x_1, \dots, x_n\}$. (⇒) Suppose there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \neq (t)^m$, we demonstrate there exists a substitution $(\Theta, \theta)$ such that $(\Theta, \theta)$ is normal with respect to $\mathbf{OVar}$ and $\mathbf{AVar}$ and $O(s,t)^{(\Theta,\theta)}$ is satisfiable or $A(s,t)^{(\Theta,\theta)}$ is satisfiable. Let $(\Theta, \theta)$ be a normal substitution with respect to $\mathbf{OVar}$ and $\mathbf{AVar}$ such that for all positive integers $i$, if $i \le n$ then if $m(x_i)$ is in $D_l$ then $\Theta(P_i) = P_i$ and $\theta(p_i) = \Box P_i$ and if $m(x_i)$ is in $D_r$ then $\Theta(P_i) = \Box p_i$ and $\theta(p_i) = p_i$. Let $\mathbf{IK}(D) = (\mathcal{F}_p(D), \mathcal{I}_p(D), \Delta)$ and $(V,v)$ be a valuation based on $\mathbf{IK}(D)$ such that for all positive integers $i$, if $i \le n$ then $V(P_i) = \mathcal{F}_{m(x_i)}$ and $v(p_i) = \mathcal{I}_{m(x_i)}$. Remark that for all positive integers $i$,
if $i \le n$ then if $m(x_i)$ is in $D_l$ then $(P_i)^{(\Theta,\theta)}(V,v) = (P_i)^{(V,v)} = V(P_i) = \mathcal{F}_{m(x_i)}$ and if $m(x_i)$ is in $D_r$ then $(P_i)^{(\Theta,\theta)}(V,v) = (\Box p_i)^{(V,v)} = (p_i)^{(V,v)} \triangleleft = v(p_i)^{\triangleleft} = \mathcal{I}_{m(x_i)}^{\triangleleft} = \mathcal{F}_{m(x_i)}$. Similarly, for all positive integers $i$, if $i \le n$ then if $m(x_i)$ is in $D_l$ then $(p_i)^{(\Theta,\theta)}(V,v) = (\Box P_i)^{(V,v)} = (P_i)^{(V,v)} \triangleleft = V(P_i)^{\triangleleft} = \mathcal{F}_{m(x_i)}^{\triangleleft} = \mathcal{I}_{m(x_i)}$ and if $m(x_i)$ is in $D_r$ then $(p_i)^{(\Theta,\theta)}(V,v) = (p_i)^{(V,v)} = v(p_i) = \mathcal{I}_{m(x_i)}$. We first observe

**Lemma 12.** Let $u$ be a term. If $u \ll s$ or $u \ll t$ then $(F(u))^{(\Theta,\theta)}(V,v) = \mathcal{F}_{(u)^m}$ and $(f(u))^{(\Theta,\theta)}(V,v) = \mathcal{I}_{(u)^m}$.

Continuing the proof of Proposition 2, since $(s)^m \ne (t)^m$, $\mathcal{F}_{(s)^m} \ne \mathcal{F}_{(t)^m}$ or $\mathcal{I}_{(s)^m} \ne \mathcal{I}_{(t)^m}$. Hence, by Lemma 12, $O(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty or $A(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty. Thus, there exists a substitution $(\Theta,\theta)$ such that $(\Theta,\theta)$ is normal with respect to *OVar* and *AVar* and $O(s,t)^{(\Theta,\theta)}$ is satisfiable or $A(s,t)^{(\Theta,\theta)}$ is satisfiable.

(=$\ll$) Suppose there exists a substitution $(\Theta,\theta)$ such that $(\Theta,\theta)$ is normal with respect to *OVar* and *AVar* and $O(s,t)^{(\Theta,\theta)}$ is satisfiable or $A(s,t)^{(\Theta,\theta)}$ is satisfiable, we demonstrate there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \ne (t)^m$. Since $O(s,t)^{(\Theta,\theta)}$ is satisfiable or $A(s,t)^{(\Theta,\theta)}$ is satisfiable, there exists a formal context $\mathbb{K} = (G, M, \Delta)$ and a valuation $(V,v)$ based on $\mathbb{K}$ such that $O(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty or $A(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty. Let $\mathcal{H}(\mathbb{K}) = (\mathcal{H}(\mathbb{K}), \perp_l, \perp_r, \top_l, \top_r, \neg_l, \neg_r, \forall_l, \forall_r, \wedge_l, \wedge_r)$ and $m$ be a valuation based on $\mathcal{H}(\mathbb{K})$ such that for all positive integers $i$, if $i \le n$ then $m(x_i) = ((\Theta(P_i))^{(V,v)}, (\theta(p_i))^{(V,v)})$. Interestingly,

**Lemma 13.** Let $u$ be a term. If $u \ll s$ or $u \ll t$ then $(u)^m = ((F(u))^{(\Theta,\theta)}(V,v), (f(u))^{(\Theta,\theta)}(V,v))$.

Continuing the proof of Proposition 2, since $O(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty or $A(s,t)^{(\Theta,\theta)}(V,v)$ is nonempty, $F(s)^{(\Theta,\theta)}(V,v) \ne F(t)^{(\Theta,\theta)}(V,v)$ or $f(s)^{(\Theta,\theta)}(V,v) \ne f(t)^{(\Theta,\theta)}(V,v)$. Hence, by lemma 13, $(s)^m \ne (t)^m$. Thus, there exists a pure double Boolean algebra $\mathcal{D}$ and a valuation $m$ based on $\mathcal{D}$ such that $(s)^m \ne (t)^m$. This ends the proof of Proposition 2.

Hence, $O(\cdot, \cdot)$ and $A(\cdot, \cdot)$ are reductions from the WP in pure double Boolean algebras to the satisfiability problem for $K_2$. Thus, by Theorem 3,

**Corollary 2.** The WP in pure double Boolean algebras is in PSPACE.

# 8 Conclusion

Our results implicitly assume that the set *Var* of all individual variables is infinite and the depth of nesting of the left operations with the right operations is not bounded. Following the line of reasoning suggested in [4], we may see what
happens if we assume that the set *Var* of all individual variables is finite and
the depth of nesting of the left operations with the right operations is bounded.
Do we get a linear time complexity in this case?

The unification problem is quite different from the WP discussed here: given
terms *s*,*t*, decide whether there exists terms which can be substituted for the
variables in *s*,*t* so that the terms thus obtained are identically interpreted in all
pure double Boolean algebras. In Mathematics and Computer Science, unifica-
tion problems are of the utmost importance. At the time of writing, we know
nothing about the decidability/complexity of the unification problem in pure
double Boolean algebras.

Acknowledgements

Special acknowledgement is heartily granted to Christian Herrmann who made
several helpful comments for improving the correctness and the readability of
this article.

References

1. Blackburn, P., de Rijke, M., Venema, Y.: *Modal Logic*. Cambridge University Press (2001).

2. Davey, B, Priestley, H.: *Introduction to Lattices and Order*. Cambridge University Press (2002).

3. Ganter, B, Wille, R.: *Formal Concept Analysis: Mathematical Foundations*. Springer (1999).

4. Halpern, J.: *The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic*. Artificial Intelligence **75** (1995) 361–372.

5. Herrmann, C., Luksch, P., Skorsky, M., Wille, R.: *Algebras of semiconcepts and double Boolean algebras*. Technische Universität Darmstadt (2000).

6. Vormbrock, B.: *A first step towards protoconcept exploration*. In Eklund, P. (editor): *Concept Lattices*. Springer (2004) 208–221.

7. Vormbrock, B.: *Complete subalgebras of semiconcept algebras and protoconcept algebras*. In Ganter, B., Godin, R. (editors): *Formal Concept Analysis*. Springer (2005) 329–343.

8. Vormbrock, B.: *A solution of the word problem for free double Boolean algebras*. In Kuznetsov, S., Schmidt, S. (editors): *Formal Concept Analysis*. Springer (2007) 240–270.

9. Vormbrock, B., Wille, R.: *Semiconcept and protoconcept algebras: the basic theorems*. In Ganter, B., Stumme, G., Wille, R. (editors): *Formal Concept Analysis*. Springer (2005) 34–48.

10. Wille, R.: *Restructuring lattice theory: an approach based on hierarchies of concepts*. In Rival, I. (editor): *Ordered Sets*. D. Reidel (1982) 314–339

11. Wille, R.: *Boolean concept logic*. In Ganter, B., Mineau, G. (editors): *Conceptual Structures: Logical, Linguistic, and Computational Issues*. Springer (2000) 317–331.

12. Wille, R.: *Formal concept analysis as applied lattice theory*. In Ben Yahia, S., Me-phu Nguifo, E., Belohlavek, R. (editors): *Concept Lattices and their Applications*. Springer (2008) 42–67
# Annex

**Proof of Lemma 10.** By induction on $A$ and $a$.

**Basis.** Remind that $\mathrm{Var}(\alpha) \subseteq \{P_1, \dots, P_n\}$. In this respect, for all positive integers $i$, if $i \le n$ then $(T(P_i))^m = (x_i)^m = m(x_i) = (V(P_i), V(P_i)^\Delta) = ((P_i)^{(V,v)}, (P_i)^{(V,v)^\Delta})$.

**Hypothesis.** Suppose $A, B$ are nice object formulas such that $A, B \ll \alpha$, $(T(A))^m = ((A)^{(V,v)}, (A)^{(V,v)^\Delta})$ and $(T(B))^m = ((B)^{(V,v)}, (B)^{(V,v)^\Delta})$ and $a, b$ are nice attribute formulas such that $a, b \ll \alpha$, $(t(a))^m = ((a)^{(V,v)^\Delta}, (a)^{(V,v)})$ and $(t(b))^m = ((b)^{(V,v)^\Delta}, (b)^{(V,v)})$.

**Step.** We only consider the case of the nice object formula $\Box a$, the other cases being treated similarly. We have: $(T(\Box a))^m = (-_l -_l -_r -_r t(a))^m = \neg_l \neg_l \neg_r \neg_r(t(a))^m = \neg_l \neg_l \neg_r ((a)^{(V,v)^\Delta}, (a)^{(V,v)}) = \neg_l \neg_l (((a)^{(V,v)^\Delta}), (a)^{(V,v)}) = (((a)^{(V,v)^\Delta}), ((a)^{(V,v)^\Delta})^{\Box\Box}) = ((\Box a)^{(V,v)}, (\Box a)^{(V,v)^\Delta})$.

**Proof of Lemma 11.** By induction on $A$ and $a$.

**Basis.** Remind that $\mathrm{Var}(\alpha) \subseteq \{P_1, \dots, P_n\}$. In this respect, for all positive integers $i$, if $i \le n$ then $(P_i)^{(V,v)} = V(P_i) = \mathcal{F}_{m(x_i)} = \mathcal{F}_{(x_i)^m} = \mathcal{F}_{(T(P_i))^m}$.

**Hypothesis.** Suppose $A, B$ are nice object formulas such that $A, B \ll \alpha$, $(A)^{(V,v)} = \mathcal{F}_{(T(A))^m}$ and $(B)^{(V,v)} = \mathcal{F}_{(T(B))^m}$ and $a, b$ are nice attribute formulas such that $a, b \ll \alpha$, $(a)^{(V,v)} = \mathcal{I}_{(t(a))^m}$ and $(b)^{(V,v)} = \mathcal{I}_{(t(b))^m}$.

**Step.** We only consider the case of the nice object formula $\Box a$, the other cases being treated similarly. We have: $(\Box a)^{(V,v)} = \{F \in \mathcal{F}_p(D): \text{ for all } I \in \mathcal{I}_p(D), \text{ if } I \in (a)^{(V,v)} \text{ then } F \Delta I \} = \{F \in \mathcal{F}_p(D): \text{ for all } I \in \mathcal{I}_p(D), \text{ if } I \in \mathcal{I}_{(t(a))^m} \text{ then } F \Delta I \} = \mathcal{I}_{(t(a))^m}^{\Delta} = \mathcal{F}_{\neg_r \neg_r (t(a))^m} = \mathcal{F}_{\neg_l \neg_l \neg_r \neg_r (t(a))^m} = \mathcal{F}_{(-_l -_l -_r -_r t(a))^m} = \mathcal{F}_{(T(\Box a))^m}$.

**Proof of Lemma 12.** By induction on $u$.

**Basis.** Remind that $\mathrm{Var}(s) \cup \mathrm{Var}(t) \subseteq \{x_1, \dots, x_n\}$. In this respect, for all positive integers $i$, if $i \le n$ then $(F(x_i))^{(\Theta,\theta)}^{(V,v)} = (P_i)^{(\Theta,\theta)}^{(V,v)} = \mathcal{F}_{m(x_i)} = \mathcal{F}_{(x_i)^m}$ and $(f(x_i))^{(\Theta,\theta)}^{(V,v)} = (p_i)^{(\Theta,\theta)}^{(V,v)} = \mathcal{I}_{m(x_i)} = \mathcal{I}_{(x_i)^m}$.

**Hypothesis.** Suppose $u, v$ are terms such that $u \ll s$ or $u \ll t$, $v \ll s$ or $v \ll t$, $(F(u))^{(\Theta,\theta)}^{(V,v)} = \mathcal{F}_{(u)^m}$, $(f(u))^{(\Theta,\theta)}^{(V,v)} = \mathcal{I}_{(u)^m}$, $(F(v))^{(\Theta,\theta)}^{(V,v)} = \mathcal{F}_{(v)^m}$ and $(f(v))^{(\Theta,\theta)}^{(V,v)} = \mathcal{I}_{(v)^m}$.

**Step.** We only consider the case of the term $u \sqcap_l v$, the other cases being treated similarly. We have: $(F(u \sqcap_l v))^{(\Theta,\theta)}^{(V,v)} = (F(u) \wedge F(v))^{(\Theta,\theta)}^{(V,v)} = ((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)}^{(V,v)}) = (F(u))^{(\Theta,\theta)}^{(V,v)} \cap (F(v))^{(\Theta,\theta)}^{(V,v)} = \mathcal{F}_{(u)^m} \cap \mathcal{F}_{(v)^m} = \mathcal{F}_{(u)^m \wedge_l (v)^m} = \mathcal{F}_{(u \sqcap_l v)^m}$ and $(f(u \sqcap_l v))^{(\Theta,\theta)}^{(V,v)} = (\Box(F(u) \wedge F(v)))^{(\Theta,\theta)}^{(V,v)} = (\Box((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)}))^{(V,v)} = ((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)})^{(V,v)^\Delta} = ((F(u))^{(\Theta,\theta)}^{(V,v)} \cap (F(v))^{(\Theta,\theta)}^{(V,v)^\Delta})^{\Delta} = (\mathcal{F}_{(u)^m} \cap \mathcal{F}_{(v)^m})^{\Delta} = \mathcal{I}_{(u)^m \wedge_l (v)^m} = \mathcal{I}_{(u \sqcap_l v)^m}$.

**Proof of Lemma 13.** By induction on $u$.

**Basis.** Remind that $\mathrm{Var}(s) \cup \mathrm{Var}(t) \subseteq \{x_1, \dots, x_n\}$. In this respect, for all
positive integers $i$, if $i \le n$ then $(x_i)^m = m(x_i) = ((\Theta(P_i))^{(V,v)}, (\theta(p_i))^{(V,v)}) = ((P_i)^{(\Theta,\theta)}^{(V,v)}, (p_i)^{(\Theta,\theta)}^{(V,v)}) = ((F(x_i))^{(\Theta,\theta)}^{(V,v)}, (f(x_i))^{(\Theta,\theta)}^{(V,v)})$.

**Hypothesis.** Suppose $u, v$ are terms such that $u \ll s$ or $u \ll t$, $v \ll s$ or $v \ll t$, $(u)^m = ((F(u))^{(\Theta,\theta)}^{(V,v)}, (f(u))^{(\Theta,\theta)}^{(V,v)})$ and $(v)^m = ((F(v))^{(\Theta,\theta)}^{(V,v)}, (f(v))^{(\Theta,\theta)}^{(V,v)})$.

**Step.** We only consider the case of the term $u \sqcap_l v$, the other cases being treated similarly. We have: $(u \sqcap_l v)^m = (u)^m \wedge_l (v)^m = ((F(u))^{(\Theta,\theta)}^{(V,v)}, (f(u))^{(\Theta,\theta)}^{(V,v)}) \wedge_l ((F(v))^{(\Theta,\theta)}^{(V,v)}, (f(v))^{(\Theta,\theta)}^{(V,v)}) = ((F(u))^{(\Theta,\theta)}^{(V,v)} \cap (F(v))^{(\Theta,\theta)}^{(V,v)}, ((F(u))^{(\Theta,\theta)}^{(V,v)} \cap (F(v))^{(\Theta,\theta)}^{(V,v)})^\dagger) = (((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)}^{(V,v)}, ((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)}^{(V,v)})^\dagger) = ((F(u) \wedge (F(v))^{(\Theta,\theta)}^{(V,v)}, (\Box((F(u))^{(\Theta,\theta)} \wedge (F(v))^{(\Theta,\theta)}^{(V,v)}))^{(V,v)}) = ((F(u \sqcap_l v))^{(\Theta,\theta)}^{(V,v)}, (f(u \sqcap_l v))^{(\Theta,\theta)}^{(V,v)})$.