Database Reference
In-Depth Information
Notice that inverse of this isomorphism
↓
is the homomorphism:
:
F
(
Υ
),
⊆
,
∩
,T
∪
,
⇒
,
¬
,
⊥
0
,
Υ
(
Υ
,
≤
,
∧
,
∨
,,
¬
,
⊥
,R
Υ
).
K
⊂
K
F
, and
consequently,
Log(K)
can be different from
IPC
(**). In fact, we obtain:
Let
K
⊂
K
DB
be a strict subset of all finite Kripke frames, so that
Lemma 26
K
⊂
K
DB
of all finite rooted descriptive frames in
Proposition
72
,
based on finite complete lattices (
Υ
,
For the subset
≤
)
,
we obtain that Log(
K
)
=
CPC
.
This subset
K
corresponds to the subset of Heyting algebras in
HA
DB
with top
elements
Υ
obtained from finite database universes
U
.
Proof
From the isomorphism (in Proposition
68
, when
X
=
Υ
with
Γ
=
T
),
F
,
Υ
=
Ob
DB
sk
,
0
,
Υ
,
↓:
(
Υ
,
≤
,
∧
,
∨
,
⊥
,R
Υ
)
(
Υ
),
⊆
,
∩
,
,
{⊥}
⊆
,
∩
,T
∪
,
⊥
the top element
Υ
=↓
R
Υ
is finite, thus defined by a finite universe
U
, i.e., when
J
Υ
={
R
=
d
|
d
∈
U
}
is finite, and hence from Lemma
23
,
Υ
J
Υ
, i.e.,
Υ
=
T
Υ
T
J
Υ
).
From the fact that
CPC
=
φ)
(see the introduction, Sect.
1.2
), it is
enough to show that for each Heyting algebra
L
alg
=
Ob
DB
sk
,
=
IPC
+
(φ
∨¬
0
,
Υ
∈
HA
DB
,
¬
⊆
,
∩
,T
∪
,
⇒
,
⊥
¬
with finite set of atoms J
Υ
, for any closed database
B
=
TA
∈
Ob
DB
sk
,
B
B
=
∪¬
T(B
B)
=
Υ
. In fact, from Lemma
23
, for each
C
=
TC
∈
Ob
DB
sk
,
C
J
C
,
that is,
C
=
TC
=
T
J
C
. Thus,
T
C
0
T
,
¬
B
=
∈
Ob
DB
sk
|
C
∩
B
⊆⊥
=
{
C
∈
Ob
DB
sk
|
J
C
∩
J
B
=∅}
and hence J
¬
B
=
J
Υ
\
J
B
.
Consequently, J
T(B
∪¬
B)
=
J
B
∪¬
B
=
J
B
∪
J
¬
B
=
J
Υ
, so that, from
B
∪¬
B
J
B
∪¬
B
we obtain
B
¬
∪¬
B
=
T(B
B)
=
T
J
B
∪¬
B
=
T
J
Υ
=
T
Υ
=
Υ
.
For example, the class of all database mapping systems with the universe equal to
a finite domain
dom
, i.e., without Skolem constants and, consequently, with all
tgds without existential quantification on the right side of material implication (Data
Integration with complete information) has WMTL equal to classical propositional
logic.
Consequently, from the fact that the subset of all finite Heyting algebras in
HA
DB
defines the CPL, the intuitionistic property of WMTL has to be determined
by its subclass of
infinite
complete Heyting algebras.
Let us consider the infinite complete Heyting algebra obtained from the canonical
model of
IPC
, based on theories with disjunction property.
U
=
