Database Reference
In-Depth Information
Based on Kripke possible-worlds semantics, we obtain for
H
(W)
the modal
propositional logic with a universal modal logical operator of logical “necessity”
'
' (with the S4 frame system, i.e., with a reflexive and transitive accessibility
relation
R
−
1
R
−
1
≤
corresponding to a partial order '
≥
' between the possible worlds in
≤
W
) such that
φ
⇒
ψ
is logically equivalent to
R
−
1
≤
(φ
⇒
c
ψ)
with the standard
propositional implication '
⇒
c
', and
¬
φ
is logically equivalent to
R
−
1
≤
¬
c
φ
with
the standard negation '
¬
c
' (see Example
42
).
It is clear that the logical interpretation of
L
DB
has to be different just because
each of its join operators is preceded by the closure operation
T
for which we have
to find the right logical interpretation. Taking in account these differences between
the standard Kripke semantics (with its Heyting complex algebra
H
(W)
) and our
DB lattice of truth-values
L
DB
, we need to develop a new Kripke semantics for the
weak monoidal topos logic.
Hence, in an analogous way, we will present a possible-worlds semantics for the
algebraic logic of the weak monoidal topos
DB
. First of all, we have to establish
what are the possible worlds in such a logic: from the fact that the sets
φ
={
a
∈
W
|
M
|=
a
φ
}
of this logic have to be the elements in
Ob
DB
sk
, we conclude that
is a simple
closed
object (database), composed of
finitary
relations
. Consequently, the possible worlds for the weak monoidal topos
φ
∈
Ob
DB
sk
, i.e., each
φ
DB
must contain all relations, i.e.,
W
⊇
Υ
=
A
∈
Ob
DB
A
(see Definition
26
in
Sect.
3.2.5
).
In such a possible-worlds semantics, each propositional formula
φ
represents an
instance-database whose extension is given by
φ
, and hence for a given relation
R
,
R
W
”.
Notice that every relation
R
∈
Υ
is finitary (i.e., with finite value
ar(R)
), but
can have an infinite number of tuples as well. From Theorem
1
, each non-closed
database
A
∈
φ
iff
M
|=
R
φ
, that is, iff
φ
is“trueintheworld
a
=
R
∈
∈
Ob
DB
is a finite subset of
Υ
, that is,
A
⊆
ω
Υ
if
A
=
TA
. A closed
∈
database
TA
Ob
DB
instead may have an infinite number of relations, if
A
have a
relation with the infinite number of tuples.
An (observationally) equivalent relation
R
A
to a given database
A
, that is, such
that
T(
TA
, may be given as a Cartesian product of all relations in
A
(be-
cause from
R
A
by finitary projections we can obtain all relations in
A
). However, in
order to have
R
A
∈
{
R
A
}
)
=
Υ
, we must ensure the condition that
ar(R
A
)
is finite number,
that is, that
(the number of relations in
A
) is finite. In order to guarantee this fini-
tary property of transformations of each instance-database into an equivalent single
relation in
Υ
(based on the algebraic property of the closure power-view operator
T
, Proposition
52
in Sect.
8.1.5
), the first attempt is as follows:
|
A
|
Let us denote a vector of a relation R by R
1
≤
i
≤
ar(R)
π
i
(R) if
Lemma 21
R
∈
A
R
obtained from a database-instance A
.
We denote the unary Skolem relation by
−
SK
2;
R otherwise
.
Analogously
,
we define a vector relation A
ar(R)
≥
{
ω
i
|
ω
i
∈
}
≤
v
) such that for any
SK
.
Based on this
,
we introduce the PO set (
Υ
,
Υ
,
R
1
≤
v
R
2
iff R
1
⊆
R
1
,
and we denote the derived
equality by R
1
v
R
2
iff
(
R
1
≤
v
R
2
and R
2
≤
v
R
2
).
two relations
,
R
1
,R
2
∈
