Database Reference
In-Depth Information
such that for any down-closed hereditary set
φ
K
,
Γ
K
=↓
K
.
R
≤
R
−
1
≤
φ
K
=
φ
φ
Definition 65
Based on definition of propositional logic WMTL in Definition
64
,
we are able to define the following Gödel-like translation from WMTL into this S4
extended bimodal logic:
1.
p
M
=
R
≤
R
−
1
≤
R
−
1
p
;
≤
ψ)
M
φ
M
∧
c
ψ
M
;
2.
(φ
∧
=
φ
M
∨
c
ψ
M
;
ψ)
M
3.
(φ
∨
=
R
≤
R
−
1
≤
4.
φ
M
⇒
c
ψ
M
ψ)
M
(φ
⇒
=
R
≤
R
−
1
≤
R
−
1
≤
¬
c
φ
M
∨
c
ψ
M
,
=
R
≤
R
−
1
≤
R
−
1
≤
where
¬
c
on the right-hand sides are the logical connectives of
classic propositional logic.
∧
c
,
∨
c
,
⇒
c
and
Notice that only for disjunction we obtained different translation of the Gödel
translation for IL.
Thus, based on Corollary
34
which gives us the relationships between the logi-
cal operators of an ordinary Heyting algebra
H
(W)
and the “closed” version
F
(W)
with a set of closed hereditary subsets in
→
F
(W)
, we are able to define a new autoreferential K
rip
k
e s
emantics for this mul-
timodal logic (for the three accessibility relations,
R
F
(W)
, by a homomorphism
Γ
:
H
(W)
,R
−
1
≤
and
R
−
1
) of weak
≤
≤
monoidal topos (its quotient algebra
L
alg
, when
W
=
Υ
and, by Corollary
35
,
Γ
is equal to power-view operator
T
).
Notice that from the fact that all three accessibility relations
R
,R
−
1
≤
and
R
−
1
≤
≤
are derived from the basic PO-relation
≤
of the lattice
(W,
≤
)
, in what follows, we
will use this simplification (by using only the relation
≤
) for this autoreferential
Kripke semantics:
Proposition 72
An autoreferential Kripke model of the “closed” algebraic logic
F
(W) in Corollary
34
,
based on the set of possible worlds in W
,
is a pair
M
=
((W,
(W)
,
for a set PR
of propositional symbols
,
is a mapping which assigns to each propositional symbol
p
≤
),V )
,
where (W,
≤
) is a Kripke frame and V
:
PR
→
F
∈
PRa closed hereditary subset V(p)
∈
F
(W)
,
so that V(p)is the set of possible
worlds at which p is true
(
with
0
V(p)
).
We now extend the notion of truth at a particular possible world a
∈
∈
W to all
formulae
,
by introducing the expression
M
|=
a
φ
,
to be read “a formula φ is true
in
M
at a”
,
defined inductively as follows
:
1.
M
|=
a
p iff a
∈
V(p)
,
and
M
|=
0
φ for every formula φ
;
2.
M
|=
a
φ
∧
ψ iff
M
|=
a
φ and
M
|=
a
ψ
;
