Database Reference
In-Depth Information
For the weak monoidal topos, we have the Kripke frame
(W,
≤
)
=
(
Υ
,
≤
)
and
Γ
=
T
, so that the complex algebra is equal to the factor algebra
L
alg
=
Ob
DB
sk
,
,
Υ
,
¬
,
⊗
,
⊕
,
⇒
,
{⊥}
=
Ob
DB
sk
,
0
,
Υ
=
,
¬
⊆
,
∩
,T
∪
,
⇒
,
⊥
F
(
Υ
)
in Proposition
71
, with
T
, and this autoreferential semantics is a new
Kripke semantics for the logic of the weak monoidal topos.
In fact, from Proposition
68
,
∪=
Γ
∪=
F
(
Υ
)
={↓
R
|
R
∈
Υ
}={
Γ in(R)
|
R
∈
Υ
}=
{
Γ
{
R
}|
R
∈
Υ
}={
T
{
R
}|
R
∈
Υ
}⊆
Ob
DB
sk
. Conversely, for each closed object
(instance-database)
A
=
TA
∈
Ob
DB
sk
we have from Lemma
22
A
=
TA
=↓
R
∈
F
(
Υ
)
where
R
=
(A)
∈
Υ
, that is,
Ob
DB
sk
⊆
F
(
Υ
)
as well. Thus,
Ob
DB
sk
=
F
(
Υ
)
. In this frame, the Kripke valuation
V
:
PR
→
F
(
Υ
)
is exactly the algebraic
DB
-valuation
Ob
DB
sk
in Proposition
71
.
Notice that, differently from the standard Kripke semantics of IL given in
Sect.
1.2
, the logical disjunction here is a modal operation as well.
In fact, the frame semantics of WMTL is a particular kind of a
general frame
F
=
V=
β
V
:
PR
→
(W)
is a set of closed
hereditary subsets of
W
closed under operations of Heyting algebra
F
(W)
(that is,
under
(W,
≤
,
F
(W))
where
(W,
≤
)
is a Kripke frame and
F
and
¬
∩
,T
∪
,
⇒
) and used to restrict the allowed valuations in the frame: a
model
M
based on Kripke frame
(W,
≤
)
is
admissible
in the general frame F if
{
a
∈
W
|
M
|=
a
p
}∈
F
(W)
for every propositional variable
p
∈
PR
. The closure
conditions on
F
(W)
then ensure that
{
a
∈
W
|
M
|=
a
φ
}∈
F
(W)
for every formula
φ
(not only variable).
From this point of view, a Kripke frame
(W,R)
may be identified with a general
frame in which
all
valuations are admissible, that is, a general frame
(W,R,
P
(W))
,
where
(W)
denotes the power set of
W
.
The Kripke semantics of the propositional WMTL (Weak Monoidal Topos
Logic), given by proposition above, is different from the Kripke semantics of the
IL given in Sect.
1.2
(with a general frame F
=
P
≤
(W,
,H(W))
where
H(W)
is the
⇒
h
), so that we have to
show that WMTL is not CPL, but satisfies all axioms (from 1 to 11 in Sect.
1.2
)of
IL (intuitionistic propositional logic), and consequently, is an intermediate logic.
The translation from WMTL into this S4 extended bimodal logic, given by Def-
inition
65
, can be expressed dually by algebraic embedding of the Heyting algebra
H
(
Υ
)
∩
∪
set of all hereditary subsets of
W
closed under
,
and
0
)
into an extended Heyting algebra by the two new
modal-negation operators
λ
(corresponding, by Lemma
24
, to logical operator
=
(H(
Υ
),
∩
,
∪
,
⇒
h
,
⊥
¬
λ
equal to
R
−
1
≤
¬
c
) and
ρ
(corresponding, by Lemma
24
, to logical operator
¬
ρ
equal
to
R
≤
¬
c
) which compose the closure operator
Γ
=
ρλ
, for any two hereditary-
subsets
S,S
1
∈
H(
Υ
)
, as follows:
1.
S
M
=
ρλS
;
S
1
)
M
S
M
S
1
2.
(S
∩
=
∩
;
S
1
)
;
S
1
)
M
ρλ(S
M
3.
(S
∪
=
∪
⇒
h
S
1
)
.
⇒
h
S
1
)
M
ρλ(S
M
4.
(S
=
