Database Reference
In-Depth Information
R
W as an
incompatibility
relation for set-based negation operators
λ and ρ
,
with the following properties
:
for any U,V
⊆
W
×
⊆
W
,
OP
λ
R
V
=
λ
R
U
∩
λ
R
V
,
with λ
R
∅=∅
OP
1. (
Additivity
)
λ
R
(U
∪
V)
=
λ
R
U
∪
=
W
;
OP
V)
=
ρ
R
(U
∪
V)
=
ρ
R
U
∩
ρ
R
V
,
with ρ
R
W
OP
2. (
Multiplicativity
)
ρ
R
(U
∩
=
ρ
R
∅=
W
;
3.
λ
R
(U
∩
V)
⊇
λ
R
U
∪
λ
R
V
,
ρ
R
(U
∩
V)
⊇
ρ
R
U
∪
ρ
R
V
,
and λ
R
ρ
R
V
⊇
V
,
ρ
R
λ
R
U
⊇
U
.
Setting
Γ
R
=
ρ
R
λ
R
:
P
(W)
→
P
(W)
, the operator
Γ
R
is a monotone mapping and
a closure operator such that for any
U,V
∈
P
(W)
1.
U
⊆
V
implies
Γ
R
(U)
⊆
Γ
R
(V )
;
2.
U
⊆
Γ
R
(U)
, for any
U
∈
P
(W)
;
3.
Γ
R
Γ
R
(U)
⊆
Γ
R
(U)
, thus, from facts 1 and 2,
Γ
R
Γ
R
(U)
=
Γ
R
(U)
.
{
∈
P
|
=
}
The set
is called the set of
stable
(i.e., closed) sets.
We will consider the case when
(W,R
≤
)
is a complete lattice with the binary
relation
R
≤
={
(a,b)
∈
W
2
U
(W)
U
Γ
R
(U)
|
a
≤
b
}
, equal to the partial order '
≤
' in the lattice
(W,
)
. This choice is meaningful and based on the fact that we try to connect
the weak monoidal topos with the algebraic complete lattice
L
DB
=
≤
(Ob
DB
sk
,
⊆
,
∩
)
(in Definition
63
), with the standard topos intuitionistic logic and its Heyting
algebra.
In what follows, we denote by
R
−
1
,T
∪
W
2
=
\
the inverse relation of
R
, and by
R
R
the complement of
R
.
Example 42
Let us consider the Kripke semantics of the intuitionistic negation
(point 5 in the introduction, Sect.
1.2
), given by
5.
M
|=
a
¬
φ
iff
∀
b(a
≥
b
implies not
M
|=
b
φ)
,
so that the set of worlds where
¬
φ
is satisfied is denoted by
¬
φ
K
={
a
∈
W
|
M
|=
a
¬
φ
}∈
H(W).
Let us show that this semantics is a particular case of additive negation operator
λ
R
of th
e Bi
rkhoff polarity, when the incompatibility relation is
R
W
2
={
(a,b)
∈
|
a
W
2
b
}=
R
≤
, and
R
≤
is a binary poset relation '
≤
', i.e.,
R
≤
={
(a,b)
∈
|
a
≤
b
}
.
In fact,
M
|=
a
¬
φ
iff
M
|=
a
R
−
1
≤
¬
c
φ
(from S4 modal Kripke semantics for intuitionistic negation)
b
(a,b)
M
|=
b
¬
c
φ
R
−
1
≤
iff
∀
∈
implies
iff
∀
b(a
≥
b
does not imply
M
|=
b
φ)
(point 5 in Sect.
1.2
)
b
b
K
iff
∀
≤
a
implies
b/
∈
φ
b
b
a
iff
∀
∈
φ
K
implies
b
b
b
R
≤
iff
∀
∈
φ
K
implies
(b,a)
∈
