Database Reference
In-Depth Information
iff
∀
b
∈
φ
K
.(b,a)
∈
R
≤
λ
R
≤
K
.
iff
a
∈
φ
Thus,
¬
φ
K
=
λ
R
≤
(
φ
K
)
.
In fact, as follows from this example, the negation operator in intuitionistic logic
(i.e., Heyting algebra) has a Kripke semantics base on the accessibility relation
which is a PO relation '
' between the possible worlds. This fact, together with
the fact that in the autoreferential semantics we use the elements of
W
as possi-
ble worlds, explains why we have a special interest to consider the incompatibility
relation equal to the PO relation used in a complete lattice
(W,
≤
)
.
The resulting Galois connection on this partial order is the familiar Dedekind-
McNeile Galois connection of antitonic mappings
λ
and
ρ
, with
Γ
≤
=
ρλ
(by
↓
a
,
{
∈
|
≤
}
↑
{
∈
|
≤
}
we denote the ideal
b
W
b
a
and by
a
, we denote
b
W
a
b
):
=
a
a)
,
=
a
v)
.
λU
∈
W
|∀
u
∈
U.(u
≤
V
∈
W
|∀
v
∈
V.((a
≤
=↓
(S)
(the '
'
It is easy to verify that for every subset
S
⊆
W
, we obtain
Γ(S)
is extension of the
binary
join operator
∨
of the lattice to any subset
S
of elements
in
W
, that is, it is the l.u.b. of
S
in
W
, i.e.,
(S)
∈
W
).
In fact, for each singleton
U
={
b
}
,
λU
={
a
∈
W
|∀
u
∈{
b
}
.(u
≤
a)
}=↑
b
.
=
{
{
}|
Thus, from the additivity (point 1 of the lemma above), we obtain
λS
λ
b
}=↑
(S)
. Analogously, from the multiplicativity (point 2
of the lemma above), we obtain
ρS
=↓
where '
' is the extension of the
binary
meet operator
}=
{↑
b
∈
S
b
|
b
∈
S
∧
of the lattice to any subset
S
of elements in
W
, that is, it is the g.l.b.
of
S
in
W
.
Consequently,
λ
=↑
is a kind of an additive modal negation and
ρ
=↓
is a
=↓
↑
=
(
from
↑
kind of a multiplicative modal negation, so that
Γ
=
ρλ
=↓
from the logical point of view is a composition of these two modal
negations.
Notice that
Γ(
=
id
W
)
∅
)
=
Γ(
{
0
}
)
={
0
}
. Hence, from the monotone property of
Γ
and
from
∅⊆
U
(for any
U
∈
P
(W)
), we obtain
{
0
}=
Γ(
∅
)
⊆
Γ(U)
. That is, any stable
(closed) set contains the bottom element 0
∈
W
, and the minimal closed set is
{
0
}
and not the empty set
while, naturally, the maximal closed set is
W
. Notice that
we have similar facts for the database complete lattice
L
DB
=
∅
⊆
∩
∪
(Ob
DB
sk
,
,
,T
)
0
with the bottom object (a singleton)
⊥
={⊥}=∅
and with a similar property for
0
)
0
the power-view closure operator,
T(
⊥
=⊥
and
T(
Υ
)
=
Υ
for the bottom and
top objects in
Ob
DB
sk
, respectively.
Moreover, each closed set is a downclosed ideal and there is the bijection between
the set of closed sets and the set of algebraic truth-values in
W
, so that we are able
to define the representation theorem for a complete lattice
(W,
≤
)
as follows:
Proposition 68
(A
UTOREFERENTIAL
R
EPRESENTATION FOR
C
OMPLETE
I
NFINI
-
TA RY
D
ISTRIBUTIVE
L
ATTICES
)
Let (W,
≤
) be a complete infinitary distribu-
tive lattice
.
We define the Dedekind-McNeile coalgebra
↓:
W
→
P
(W)
,
where