Database Reference
In-Depth Information
into the
N
-modal algebra
BA
+
=
0
,
Υ
,
(Ob
DB
sk
,
∩
,
∪
,
−
,
⊥
1
,
2
,
3
)
is given
by the following equalities of these algebra operators:
TA
TB
=
3
−
2
−
(T A
∪
TB),
and
⇒
=
3
−
2
−
1
(
−
∪
TA
TB
TA
TB),
for any
TA,TB
∈
Ob
DB
sk
.
9.2.4 Weak Monoidal Topos and Intuitionism
From the fact that a propositional formula
φ
is a theorem of intuitionistic logic
iff it is
HA
-valid (i.e., valid in any Heyting algebra, as specified by point 8 in the
introduction, Sect.
1.2
), and the fact that the
DB
weak monoidal topos is based
on a “closed” Heyting algebra
L
alg
=
,
¬
(Ob
DB
sk
,
,
⊗
,
⊕
,
⇒
)
=
(Ob
DB
sk
,
⊆
,
,
¬
∩
)
(defined in Proposition
71
), we conclude that each theorem of in-
tuitionistic logic is a theorem for this weak monoidal topos.
We have seen that this subset of “closed” Heyting algebras (by a Birkhoff-
polarity closure operator
Γ
, as demonstrated by Corollary
34
) has a Kripke seman-
tics (in Proposition
72
) different from the ordinary Kripke semantics of intuition-
istic logic (given in the introduction, Sect.
1.2
), we can suppose that the
DB
weak
monoidal topos can have more theorems than intuitionistic logic.
An intuitionistic
general
frame is a triple F
=
,T
∪
,
⇒
H
(W,R
≤
,
)
, where
(W,R
≤
)
is an
intuitionistic frame (with poset
R
≤
) and
H
⊆
H(W)
is a set of upsets (hereditary
subsets of
W
) such that
∅
and
W
belong to
H
, and
H
is closed under
∩
,
∪
and
⇒
h
is a relative pseudo-complement defined, for any two hereditary subsets
U,V
∈
H
),
by
=
a
b
(a,b)
V
⇒
h
V
∈
|∀
∈
∈
∈
U
W
R
≤
and
b
U
implies
b
a
R
≤
.
=
W
\
∈
X
|
(b,a)
∈
b
∈
U
\
V
Hence, from a general frame F we derive its complete Heyting algebra
F
+
=
(
H
,
⊆
,
∩
,
∪
,
⇒
h
,
∅
,W).
Every intuitionistic Kripke frame can be seen as a general frame, where
H
is the set
H(W)
of
all
hereditary subsets of F.
•
A general frame F is called
refined
if for each
a,b
∈
W
,
(a,b) /
∈
R
implies that
there is a
V
∈
H
such that
a
∈
V
and
b/
∈
V
;
and
S
⊆{
•
A general frame F is called
compact
if for each
S
⊆
H
X
\
V
|
V
∈
S
has the finite intersection property (i.e., every intersection of finite
elements of
S
H
}
,if
S
∪
S
is nonempty) then
S
S
=∅
∪
∩
;
•
A general frame F is called
descriptive
if it is refined and compact;
