Database Reference
In-Depth Information
defined as relative pseudo-complement in a complete distributive lattice
W
, that is,
for the
intuitionistic
logic implication.
In fact, if we consider that each formula is true in the bottom element (a “con-
tradiction” world) 0
∈
W
of the complete lattice
W
of “possible worlds”, then the
complex algebra of intuitionistic logic is a Heyting algebra,
=
H(W),
¬
h
,
H
(W)
⊆
,
∩
,
∪
,
⇒
h
,
based on r.p.c. lattice
(H(W),
⊆
,
∩
,
∪
,
{
}
,W)
, where
H(W)
is not a set of closed
subsets (as in
L
alg
) but a set of
hereditary
subsets
S
(with 0
0
∈
S
) of a poset
(W,
≤
)
such that if
a
∈
S
and
b
≤
a
then
b
∈
S
, and differently from
L
alg
, its meet oper-
ator is a simple set-union. The relative pseudo-complement for any two hereditary
subsets
U,V
∈
H(W)
is
(Z
∈
H(W)
|
Z
∩
U
⊆
V
}=
W
\
a
∈
W
|
(b,a)
∈
R
≤
,
U
⇒
h
V
=
b
∈
U
\
V
while in
L
alg
we apply the closure power-view operator
T
on it, as well. Based
on Kripke possible-worlds semantics, we obtain for
H
(W)
the modal propositional
logic with a universal modal logical operator of logic “necessity” '
' (for S4 frame
system with a reflexive and transitive accessibility relation
R
corresponding to the
partial order '
≤
' between the possible worlds in
W
) such that
φ
⇒
ψ
is logically
equivalent to
(φ
⇒
c
ψ)
with classic propositional implication '
⇒
c
', and
¬
φ
is
logically equivalent to
¬
c
φ
with a classic propositional negation '
¬
c
'.
Example 43
The smallest
nontrivial
bilattice is Belnap's 4-valued bilattice [
1
,
6
,
17
]
W
={
1
,
0
,
⊥
,
}
where 1 is
true
,0is
false
,
is inconsistent (both true and
false) or
possible
, and
is
unknown
. As Belnap observed, these values can be given
two natural orders:
truth
order,
⊥
≤
, and
knowledge
order,
≤
k
, such that 0
≤≤
1,
0
≤⊥≤
1, and
⊥≤
k
0
≤
k
,
⊥≤
k
1
≤
k
. The meet and join operators under
partial ordering '
'; they are natural generalizations of the
usual conjunction and disjunction notions. Meet and join under
≤
' are denoted '
∧
' and '
∨
≤
k
are denoted by
=⊥
=
∧⊥=
∨⊥=
'
' and '
', so that 0
1
,0
1
,
0 and
1.
¬
=
¬
=
¬⊥=⊥
¬=
The
bilattice negation
[
7
] is defined by
0
1,
1
0,
and
.
It is easy to see that the De Morgan law is valid,
¬
(a
∧
b)
=¬
a
∨¬
b
.
Thus, w.r.t. the truth ordering '
≤
', the elements in
F
(W)
are
↓
0
={
0
}
,
↓⊥=
{
0
,
⊥}
,
↓={
0
,
}
and
↓
1
=
W
. That is,
F
(W)
={{
0
}
,
{
0
,
⊥}
,
{
0
,
}
,W
}
.
From the isomorphism in Proposition
68
, we have the isomorphism
↓:
(W,
≤
,
∧
,
∨
,
0
,
1
)
F
(W),
⊆
,
∩
,
,
{
}
,W
.
0
↓⊥↓=↓
(
↓⊥∪↓
)
=↓
{
So that,
0
,
⊥
,
}=↓
1
=
W
=↓⊥∪↓
,
that is,
.
Notice that the set of hereditary subsets of
W
(see the introduction in Sect.
1.2
)is
equal to
H(W)
=∪
={{
0
}
,
{
0
,
⊥}
,
{
0
,
}
,
{
0
,
⊥
,
}
,W
}
, that is, to the lattice
(H(W),
⊆
,
∩
,
∪
,
{
0
}
,W)
which is, differently from
F
(W)
, closed under the set-union (join