Database Reference
In-Depth Information
The extended Heyting algebra
H
(
Υ
)
+
=
0
,
Lemma 25
(H(
Υ
),
∩
,
∪
,
⇒
h
,
⊥
λ
,
0
0
ρ
)
,
where
_)
,
is an algebraic dual of
the S
4
extended bimodal logic
(
by modal logical operators
λ
=⊥
∪
(
Υ
\
λ_) and
ρ
=⊥
∪
ρ(
Υ
\
R
−
1
≤
and
R
≤
,
respec-
tively
),
so called IM-logic
(
Intuitionistic Modal logic
[
26
]).
Proof
It is easy to show that
ρ
is
a multiplicative algebraic modal operator. In fact, for any two
S
1
,S
2
∈
H(
Υ
)
(we
recall that
λ
is an additive algebraic modal operator and
0
⊥
={⊥}
is an empty database with the empty relation
⊥
), we have:
={⊥}∪
Υ
S
2
)
={⊥}∪
Υ
λS
2
)
λ
(S
1
∪
S
2
)
\
λ(S
1
∪
\
(λS
1
∩
={⊥}∪
Υ
\
(λS
1
)
∪
Υ
\
(λS
2
)
=
λ
(S
1
)
∪
λ
(S
2
)
;
λ
⊥
0
={⊥}∪
Υ
λ
{⊥}
={⊥}∪
0
\
(
Υ
\
Υ
)
={⊥}∪∅=⊥
;
and hence
λ
is an additive modal algebraic operator, while,
ρ
Υ
S
2
)
=⊥
ρ
Υ
(S
2
)
0
0
ρ
(S
1
∩
S
2
)
=⊥
∪
\
(S
1
∩
∪
\
(S
1
)
∪
Υ
\
∪
ρ
Υ
(S
1
)
∩
ρ
Υ
(S
2
)
=
ρ
(S
1
)
0
=⊥
\
\
∩
ρ
(S
1
)
;
0
0
0
ρ
(
Υ
)
=⊥
∪
ρ(
Υ
\
Υ
)
=⊥
∪
ρ(
∅
)
=⊥
∪
Υ
=
Υ
,
and hence
ρ
is a multiplicative modal algebraic operator. Thus, these two algebraic
operators correspond to the logical modal operators
R
−
1
≤
and
R
≤
.
Consequently, WMTL can be regarded just as a fragment of classical bimodal
logics containing S4, whose dual is the Heyting algebra
=
F
0
,
L
alg
=
F
(
Υ
)
(
Υ
),
∩
,ρλ
∪
,ρλ
⇒
h
,
⊥
where
ρλ
=
Γ
=
T
,
ρλ
∪=
and, from Corollary
34
,
(ρλ
⇒
h
)
= ⇒
.
F
(
Υ
)
can be embedded
into a complete database Boolean algebra extended by three multiplicative algebraic
modal operators.
Let us show that this database Heyting algebra
L
alg
=
0
,
Υ
) is a complete Boolean
algebra with negation operator defined for every A
=
TA
∈
=
∩
∪
−
⊥
Corollary 36
The algebra
BA
(Ob
DB
sk
,
,
,
,
Ob
DB
sk
by
−
A
0
⊥
∪
(
Υ
\
A)
,
such that there is a homomorphism
:
(i)
_
.
BA
Υ
,
into the complete Boolean algebra
BA
Υ
=
:
BA
→
,
Υ
)
(
Proposition
70
).
(
Υ
,
∧
v
,
∨
v
,
¬
v
,
⊥
Consequently
,
the database Heyting algebra L
alg
=
F
(
Υ
) can be embedded
into the N-modal algebra
BA
+
=
0
,
Υ
,
∩
∪
−
⊥
1
,
2
,
3
)
,
where
(Ob
DB
sk
,
,
,
,
1
=
is the S
4
algebraic universal modal operator
(
Example
42
)
and
,
from Lemma
25
,
λ
R
≤
−
2
=−
λ
−=−
λ and
3
=
ρ
=
ρ
−
,
such that for every
A
=
TA
∈
Ob
DB
sk
and B
=
TB
∈
Ob
DB
sk
:
