Database Reference
In-Depth Information
3.
M
|=
a
φ
∨
ψ iff
∀
b(a
b implies
∃
c(c
b and (
M
|=
c
φ or
M
|=
c
ψ)))
;
4.
M
|=
a
φ
⇒
ψ iff
∀
b(a
b implies
∃
c(c
b implies
∀
w(w
≤
c implies (
M
|=
w
φ implies
M
|=
w
ψ))))
;
5.
M
|=
a
¬
φ iff
M
|=
a
φ
⇒
0
iff
∀
b(a
b implies
∃
c(c
b implies
∀
w(w
≤
c implies not
M
|=
w
φ)))
.
Proof
BasedonCorollary
34
, we obtain:
1.
φ
∨
ψ
is equal to
R
≤
R
−
1
≤
(φ
∨
c
ψ)
(different from standard Kripke represen-
tation);
2.
φ
⇒
c
ψ)
is a stan-
dard Kripke representation for intuitionistic implication (given by point 4 in the
introduction, Sect.
1.2
);
⇒
ψ
is equal to
R
≤
R
−
1
≤
R
−
1
(φ
⇒
c
ψ)
, where
R
−
1
≤
(φ
≤
3.
≤
¬
c
φ
is a standard Kripke rep-
resentation for intuitionistic negation (given by point 5 in the introduction,
Sect.
1.2
);
Consequently, the complex algebra for this modal Kripke semantics is equal to
the “closed” algebra
F
(W)
¬
φ
is equal to
R
≤
R
−
1
≤
R
−
1
≤
¬
c
φ
, where
R
−
1
,
¬
=
F
⊆
∩
∪
⇒
)
, where for any two
V
1
,V
2
∈
(
(W),
,
,Γ
,
F
(W)
:
V
2
=
Γ
(V
1
,V
2
)
V
1
∪
=
a
b
(a,b)
c
(b,c)
V
2
)
R
−
1
≤
∈
W
|∀
∈
R
≤
implies
∃
∈
and
(c
∈
V
1
∪
=
a
b
(a,b) /
c
(b,c)
V
2
)
R
−
1
∈
W
|∀
∈
R
≤
or
∃
∈
and
(c
∈
V
1
∪
≤
=
a
b
(a,b)
c
(b,c)
V
2
)
R
−
1
∈
|∃
∈
∃
∈
∈
V
1
∪
W
R
≤
and
and
(c
≤
=
W
\
a
∈
W
|∃
b
(a,b)
∈
R
≤
∃
c
(b,c)
∈
R
−
1
≤
and
(c
∈
V
1
∪
V
2
)
and
R
≤
a
=
\
∈
|
∈
W
W
(a,b)
∃
c((b,c)
∈
R
−
1
≤
b
∈
W
and
and
(c
∈
V
1
∪
V
2
))
R
≤
a
=
W
\
∈
W
|
(a,b)
∈
\
c
∈
V
1
∪
V
2
{
R
−
1
b
∈
W
b
∈
W
|
(b,c)
∈
≤
}
=
W
\
{
a
∈
W
|
a
b
}
\
c
∈
V
1
∪
V
2
{
b
∈
W
b
∈
W
|
c
b
}
,
V
1
⇒
V
2
=
W
\
{
a
∈
W
|
a
b
}
b
∈
W
\
c
∈
V
3
{
b
∈
W
|
c
b
}
(
c
∈
V
1
\
V
2
↑
where
V
3
=
W
\
c)
.
