Database Reference
In-Depth Information
S
(W)
|↓
b
=
Γ
∪
∈
H(W)
|
S
⊆↓
c
∈
F
c
∩↓
a
⊆↓
S
(W)
b
|↓
(from 3)
=
Γ
∪
∈
H(W)
|
S
⊆↓
c,S
∩↓
a
⊆↓
c
∈
F
∪
S
b
=
Γ
∈
H(W)
|
S
∩↓
a
⊆↓
=
↓
⇒
h
↓
Γ(
a
b),
thus, for any
S
1
,S
2
∈
H(W)
,
Γ(Γ(S
1
)
⇒
h
Γ(S
2
))
=
(Γ S
1
)
⇒
(Γ S
2
)
, and
S
S
2
S
1
⇒
h
S
2
=
∈
|
∩
S
1
⊆
H(W)
S
(monotonicity of
Γ
)
S
∈
H(W)
|
ΓS
∩
ΓS
1
⊆
ΓS
2
=
S
ΓS
2
=
(from 3)
=
∈
H(W)
|
S
∩
ΓS
1
⊆
(Γ S
1
)
⇒
h
(Γ S
2
).
Thus,
Γ(S
1
⇒
h
S
2
)
=
Γ(Γ(S
1
)
⇒
h
Γ(S
2
))
=
(Γ S
1
)
⇒
(Γ S
2
)
, and hence
Γ
is
a homomorphism for relative pseudo-complements as well (thus
Γ(
¬
h
S
1
)
=
¬
(Γ S
1
)
).
The Heyting algebra
F
(W)
for closed hereditary subsets of a complete lattice
(W,
≤
)
will be used in what follows for the logic of the weak monoidal topos.
9.2.2 DB-Truth-Value Algebra and Birkhoff Polarity
It is well known that the semantics of intuitionistic logic of the standard topoi was
provided by Samuel Kripke [
10
], by introducing the concept of the truth of a given
propositional formula
φ
in a “possible world”
a
∈
W
for a given model
M
of such
a logic, denoted by
M
|=
a
φ
.
In such a Kripke semantics (extended to all propositional logics with
modal
log-
ical operators as well) we denote the set of all possible worlds where this formula
φ
is true in a given model
M
={
∈
|
M
|=
a
φ
}
by
φ
a
W
.
Remark
Notice that in the original Kripke semantics, we can have
φ
be the empty
set, while here, in our “lifted” Kripke semantics
M
|=
0
φ
(each formula is true in
the “contradiction” world
a
=
. This lifting is
necessary in our case because we will use a logic for databases and every simple
database
A
0
∈
W
) is always satisfied 0
∈
φ
∈
Ob
DB
is not the empty set of relations (in fact,
⊥∈
A
for each simple
object
A
in the
DB
category).
The complex algebra of such sets for the intuitionistic logic is a Heyting algebra,
H
(W)
¬
h
)
where
H(W)
is not a set of closed subsets but
a set of
hereditary
subsets
S
(with 0
=
(H(W),
⊆
,
∩
,
∪
,
⇒
h
,
∈
S
) of a poset
(W,
≤
)
such that if
a
∈
S
and
b
≤
a
then
b
∈
S
, and differently from
L
DB
, its join operator is the simple set-union.
