Database Reference
In-Depth Information
1
≤
j
≤
m
A
j
∈
Ob
DB
sk
,m
≥
1,
A
=
TA
, and hence we can define a function
(f
=
1
≤
j
≤
m
f
j
)
β
−
1
(A)
∈
DB
(Υ,Ω)
with
f
j
={
id
R
:
R
→
R
|
R
∈
A
j
}:
Υ
→
Υ
,
so that
β(f)
=
TA
=
A
.
Based on this lemma, and from the fact that in the lattice
L
DB
we have that
for any object
A
' is the equivalence relation in this
lattice), we obtain that the lattice
L
DB
is equivalent to the lattice of only closed
objects and, consequently, the lattice of truth-values in
DB
(Υ,Ω)
is isomorphic to
the lattice
L
DB
. Thus we can use the meet and join operators of the lattice
L
DB
as
an algebraic counterparts of the logical operations for conjunction and disjunction,
respectively. Hence, we introduce the following non-standard propositional logic for
the weak monoidal topos
DB
:
∈
Ob
DB
,A
≈
TA
(where '
≈
Definition 62
In the weak monoidal database topos
DB
,a
DB
-valuation is a func-
tion
V
:
PR
→
DB
(Υ,Ω)
assigning to each propositional letter
p
∈
PR
atruth-
:
→
value (arrow)
V(p)
Υ
Ω
. This function is uniquely (inductively) extended to
all formulae of PL (where
are the logical operators conjunction and dis-
junction, respectively) by the following rules:
•
∧
and
∨
β
−
1
(β(V (φ))
V(φ
∧
ψ)
=
V(φ)
⊗
V(ψ)
=
⊗
β(V (ψ)))
:
Υ
→
Ω
;
β
−
1
(β(V (φ))
⊕
V(φ)
⊕
•
V(φ
∨
ψ)
=
V(ψ)
=
β(V (ψ)))
:
Υ
→
Ω
,
DB
(Υ,Ω)
=
where '
β
' is the bijection,
β
Ob
DB
sk
, in Lemma
19
.
We say that
φ
is
DB
-valid formula, denoted by
DB
:
|=
φ
, iff for every
DB
-
valuation
V
,
V(φ)
=
true
=
id
Υ
:
Υ
→
Ω
.
We can consider the reduction of this logic to only simple databases (from the
fact that complex databases are only disjoint union of the simple databases), by the
class of “simple”
DB
-valuation:
Definition 63
Let us define the strict complete sublattice of truth-values
L
DB
=
(Ob
DB
sk
,
,
⊗
,
⊕
)
=
(Ob
DB
sk
,
⊆
,
∩
,T
∪
)
⊂
L
DB
,
0
and the unique complex object equal to the top simple
object
Υ
. The “simple”
DB
-valuations for this complete sublattice is given by a
subset of functions
V
with the bottom object
⊥
:
PR
→
DB
(Υ,Ω)
assigning to each propositional letter
p
∈
V(p)
PR
a truth-value (arrow)
V(p)
Υ
is a
simple arrow in
DB
, and consequently,
V
may be equivalently substituted by
V
:
Υ
→
Ω
such that
={
f
:
Υ
→
Ω
}=
:
DB
(
Υ
,
Ω
)
, such that
V(p)
PR
→
={
V
(p)
}
with
true
=
id
Υ
:
Υ
→
Ω
and
false
=
1
⊥
:
Υ
→
Ω
. Then we obtain the unique extension to all formulae by:
β
−
1
(β(
V
(φ))
•
V
(φ
∧
ψ)
=
∩
β(
V
(ψ)))
:
Υ
→
Ω
;
β
−
1
(T (β(
V
(φ))
•
Ω
,
where '
β
' is a reduction of bijection in Lemma
19
to
β
V
(φ
∨
ψ)
=
∪
β(
V
(ψ))))
:
Υ
→
DB
(
Υ
,
Ω
)
=
:
Ob
DB
sk
of
only simple arrows, where
DB
sk
is a full skeletal subcategory of
DB
with only
closed simple objects.
