Database Reference
In-Depth Information
⊕¬
That is,
B
Υ
where
Υ
is the top element 1 of this complete distributive
lattice defined by this universe
B
=
1
=
0
U
(while
⊥
={⊥}
is its bottom element 0). In fact,
T
C
0
¬
0
,
B
=
∈
Ob
DB
sk
|
C
∩
B
=⊥
=⊥
from the fact that J
B
=
J
A
=
J
Υ
,
and for each
C
=
TC
∈
Ob
DB
sk
, from Lemma
23
,
0
J
C
⊆
C
, so that from
C
∩
B
=⊥
it must hold that J
C
∩
J
B
=
J
C
∩
J
Υ
=∅
, thus
0
. Hence, we obtain that
B
⊕¬
∪¬
J
C
=∅
and, consequently,
C
=⊥
B
=
T(B
B)
=
0
)
T(B
∪⊥
=
T(B
∪{⊥}
)
=
TB
=
TTA
=
TA
⊂
1
=
Υ
, because for an infinite
universe
the top object (instance database)
Υ
is composed of
also infinite
(but
with a finite arity) relations over this universe, while
TA
is composed of only finite
relations.
U
Let us consider an example where the excluded middle does not hold:
Example 47
Let us consider a continuation of Example
44
where
A
=
can(
I
,D)
has two infinite binary relations
R
1
and
R
2
:
R
1
=
r
can(
I
,
D
)
R
2
=
s
can(
I
,
D
)
a,b
b,ω
0
b,ω
1
ω
1
,ω
2
ω
1
,ω
3
ω
3
,ω
4
ω
3
,ω
5
ω
5
,ω
6
...
...
Let us consider a unary but infinite relation
=
0
,
1
,...
=
,...
∈
R
ω
4
i
|
i
=
ω
0
,
ω
4
,
ω
8
Υ
.
⊕¬
∪¬
TA)
. In this case,
¬
Let us show that
R/
∈
TA
TA
=
T(TA
TA
is a finite
database with all finite relations with values in the finite set
dom
\{
a,b
}
, and from
Example
44
we obtain that
R/
∈
T(
{
R
1
,R
2
}
)
=
TA
, and from the fact that
R
has no
value in
¬
R
1
,R
2
}∪¬
R
1
,R
2
}∪¬
⊕¬
TA
,
R/
∈
(T
{
TA)
⊆
T(T
{
TA)
=
TA
TA
,
so that for this instance-database
TA
∈
Ob
DB
sk
⊆
Υ
the excluded middle does not
hold.
A duality between finite Heyting algebras and finite posets has been known for
a long time. One such description was provided by the Jongh and Troelstra in [
4
].
They used the join-irreducible elements to get a representation of finite Heyting
algebras. So that any finite (thus complete) Heyting algebra
H
=
(X,
≤
,
∧
,
∨
,,
¬
,
0
,
1
)
is isomorphic to the Heyting algebra of hereditary subsets
H
X
+
=
H
X
+
,
,X
+
,
⊆
,
∩
,
∪
,
⇒
h
,
¬
h
,
∅
where
X
+
is the subset of join-irreducible elements of
X
.
