Database Reference
In-Depth Information
In this way, generally, the logic is internally represented in a standard topos
C
.We
shall say that
φ
is a
C
-valid formula, denoted by
C
|=
φ
, iff for every
C
-valuation
V
,
V(φ)
Ω
.
Based on this translation, it was demonstrated that any
C
-valid formula is a the-
orem of classical propositional logic (CPL), but CPL is not sound for
C
-validity: in
fact, the “law of excluded middle”,
φ
∨¬
φ
,
is not
C
-valid.
Moreover, it was demonstrated that the 'topos logic' based on the topos-valuation
is
intuitionistic
propositional logic (see, for example, [
8
]), that is, from the algebraic
point of view, it is a Heyting algebra (it was demonstrated that a collection of arrows
(truth-values) in
C
(
1
,Ω)
is a Heyting algebra).
A Heyting algebra is based on a complete
distributive
lattice where logical con-
junction is interpreted by the meet lattice operation, logical disjunction by the
join lattice operation, while logical implication
φ
⇒
ψ
by the relative-pseudo-
complement, and logical negation
=
true
:
1
→
0, where 0 is the logical
falsity (in a Heyting algebra it is the bottom element of its complete distributive
lattice).
From the fact that
DB
is not a standard topos but a kind of weak monoidal topos,
it is plausible to consider that its “logic” is a kind of weakening of intuitionistic
logic. In what follows, we will try to describe this new non-standard propositional
logic.
Notice that the
DB
is not
well-pointed (from Proposition
67
), so that the way to
“internalize the logic” in
DB
has to be very different w.r.t. to the case of standard
topoi presented previously. The terminal object
1
in
DB
is the zero object
¬
φ
is equal to
φ
⇒
0
⊥
={⊥}
,
1
so that we have only one arrow
→
Ω
, and hence the collection of arrows
DB
(
1
,Ω)
is a singleton and, consequently, cannot represent the collection of truth
values of its logic. But, as in the case of the subobject classifier pullback diagram
in
DB
, where the truth-arrow (
true
) is equal to the identity arrow
id
Υ
:
⊥
:
1
Υ
→
Ω
(in
DB
,wehave
Ω
Υ
), the set of truth values is the collection
DB
(Υ,Ω)
of
arrows. Consequently, we have to discover which kind of algebra is represented by
this collection
DB
(Υ,Ω)
, and then to define a logic of such an algebra.
In Sect.
8.1.5
, we defined the complete algebraic database lattice
L
DB
=
(Ob
DB
,
=
,
⊕
)
(see Proposition
51
), where the meet operation is equal to the
database-matching operator
,
⊗
and the join operator is equal to the generalized
database-merging operator in Definition
57
. In order to make a relationship between
the collection
DB
(Υ,Ω)
of truth-values (arrows) with this complete (but not dis-
tributive) lattice
L
DB
, we will use the following property (based on the symmetry
property of arrows and objects in
DB
):
⊗
Lemma 19
There is a bijection β between the truth-values and closed objects in
DB
,
that is
,
β
:
DB
(Υ,Ω)
=
Ob
DB
sk
,
such that for any truth-value f
:
Υ
→
Ω
,
=
f which is a closed object in the skeletal category
DB
sk
equivalent to
DB
(
by Proposition
50
).
β(f)
Ω
in
DB
(Υ,Ω)
, from Proposition
6
,
f
Proof
For each truth-value
f
:
Υ
→
Υ
⊗
Ω
=
Υ
(recall that
Ω
=
Υ
=
Υ
∪
(
ω
Υ
)
), and from the fact that
⊥∈
f
,
0
⊥
=
{⊥}
f
, so that
β
is a surjective mapping. Conversely, for each closed object
A
=
