Database Reference
In-Depth Information
(
ω
⊥
0
1
1
)
, and the true logical value by the maximal information flux
⊥
⊥
∪
Υ
=
id
Υ
=
true
, that is, the bottom and the top objects of the lattice
L
DB
=
,
⊕
(Ob
DB
,
)
.
Another analogous approach which can be used is based on modal logics (see,
for example, Definition 10 in [
18
] for the Kripke semantics where the bottom el-
ement of the lattice is considered as a trivial world in which any logical formula
is satisfied): if we consider each relation as a possible world, then the set with the
empty relation
,
⊗
0
⊥
={⊥}
corresponds to the falsity, while the set of all relations
(equal to
Υ
) to the truth. In this interpretation, the lattice
L
DB
is used as a PO
set of the possible worlds, analogously to the Kripke interpretation of the intuition-
istic propositional logic, i.e., for the topoi. And this closely relates our weak topos
with the Kripke semantics of its propositional logic based on the subobject classifier
in
DB
.
Let us show that in the
DB
category, differently from
Set
, the “characteristic
function”
C
f
from
A
into
Ω
can be represented by a morphism
C
f
=
f
OP
in
B
◦
:
Υ
, with
in
B
=
1
≤
i
≤
k
(in
B
i
:
A
→
B
i
→
Υ
i
=
Υ
)
such that
C
f
ij
=
.
C
f
=
f
f
OP
in
B
i
◦
ij
:
A
j
→
Υ
i
=
Υ
|
f
ij
∈
Hence
TB
i
∩
f
OP
C
f
f
f
C
f
=
f
OP
in
B
i
◦
ij
|
f
ij
∈
=
ij
|
f
ij
∈
(by duality)
TB
i
∩
f
ij
|
,
f
f
f
ij
|
=
f
ij
∈
=
f
ij
∈
i.e.,
C
f
f
, so that
C
f
≈
f
≈
A
(characteristic arrow is well defined).
Consequently, we are ready for a formal definition of the subobject classifier
in the
DB
category, based on the limit cone (see the pullback diagram in Proposi-
tion
27
) of the diagram
Υ
B
C
f
true
Ω
A
, as follows:
Theorem 18
The subobject classifier for
DB
is the object Ω
=
Υ with the arrow
true
Ω that satisfies the Ω-axiom
:
For any given subobject B
=
id
Υ
:
Υ
−→
=
1
≤
i
≤
k
B
i
=
1
≤
j
≤
m
A
j
,
with k,m
A
≥
1
and
f
={
σ
:{
1
,...,k
}→{
1
,...,m
}
(
i
.
e
.,
a monomorphism f
:
B
→
A with
f
iσ(i)
:
B
i
→
A
σ(i)
|
1
≤
i
≤
k
}
;
see Theorem
6
),
there is one and only one characteristic
:
A
→
Υ
,
where in
B
=
1
≤
i
≤
k
(in
B
i
:
B
i
→
Υ
i
=
Υ
)
,
in
B
◦
f
OP
morphism C
f
=
and p
A
with
p
Υ
in
B
B and with outgoing arrows p
Υ
with the vertex LimP
=
A
×
=
and
p
A
id
A
=
,
such that the diagram
