Database Reference
In-Depth Information
, i.e., the excluded middle is valid and hence the
closure in the topological space is a model of
CPC
and not of
IPC
.
Consequently,
φ
∨¬
φ
=R
Consequently, it is natural to consider the subclass of
infinite
Heyting algebras
in
HA
DB
in order to examine their intuitionistic properties (because we obtained
by Lemma
26
that the subset of finite Heyting algebras in
HA
DB
corresponds to
CPC
).
Let us show that indeed the class of Heyting algebras for databases
HA
DB
in
Definition
64
(where for each
dom
,
L
alg
=
(Ob
DB
sk
,
,
⊗
,
⊕
,
⇒
,
¬
)
∈
HA
DB
),
that is, its WMTL logic is not CPL (standard propositional) but intuitionistic (or
strictly an intermediate) logic:
Theorem 19
The WMTL does not satisfy the “excluded middle” axiom of CPL
.
Proof
We have to show that the excluded middle axiom 12,
φ
φ
(see Sect.
1.2
in the introduction), does not hold in WMTL, that is, there exists a Heyting algebra
in the class
∨¬
⊕¬
HA
DB
with
B
=
∈
=
Υ
.
By Definition
31
in Sect.
5.1
of
Σ
R
(SPJRU) algebra, for a given set of vari-
ables (relational symbols)
X
, the set of terms with variables
TA
Ob
DB
sk
such that
B
B
T
P
X
of this algebra
is defined inductively, thus finitely, by the set of its basic finitary operators. Thus,
in Sect.
5.1.1
, it is shown that for each database instance
A
, the database
TA
is
obtained by a unique surjective mapping
α
#
:
T
P
X
TA
, and the following initial
algebra commutative diagram
where
α
:
A
→
A
⊆
TA
defines this particular database instance
A
of a schema
A
with the set of relational symbols in
X
.
Let us consider an infinite universe of values
U
=
dom
∪
SK
, with an infinite
α
∗
(
0
schema
A
with unary relational symbols, so that
A
=
A
)
=⊥
∪{
R
i
=
α(r
i
)
=
0
{
d
i
}|
d
i
∈
U
}=
(from Lemma
23
)
=⊥
∪
J
Υ
.
0
Let us consider the closed object
B
=
TA
=
T(
⊥
∪
J
Υ
)
, so that
TB
is the set
of all
finite
relations (because
T
P
X
is an infinite set of all finite-length terms of
SPJRU algebra, by considering that in
Σ
R
we have an infinite set of u
na
ry 'select'
operations “_ WHERE
C
i
” for the conditions
C
i
equal to “
name
=
d
i
” for each
distinct
d
i
∈
U
).
Let us show that the “excluded-middle” axiom does not hold for the Heyting
algebra with this infinite universe
U
,
,
¬
,
¬
L
alg
=
(Ob
DB
sk
,
,
⊗
,
⊕
,
⇒
)
=
(Ob
DB
sk
,
⊆
,
∩
,T
∪
,
⇒
)
∈
HA
DB
.
