Information Technology Reference
In-Depth Information
3.2 Frame Definability
Formulas from standard modal logic can be used to capture properties of neigh-
borhood frames, e.g.,
p
corresponds to the property (
d
) [12, Section 2.4].
It is therefore remarkable that there is no such correspondence in
CL
for most
of the properties of neighborhood frames. Similarly, many properties of Kripke
frames do not correspond to frame axioms in contingency logic [16].
p
→
♦
Definition 6 (Frame Definability).
Let
ʓ
be a set of
CL
-formulas and
F
a
class of frames. We say that
ʓ
defines
F
if for all frames
F
,
F
is in
F
if and
only if
F
ʓ
. In this case we also say
ʓ
defines the property of
F
.If
ʓ
is a
singleton (e.g.
{
˕
}
), we usually write
F
˕ rather than
F
{
˕
}
.Aclassof
frames (or the corresponding frame property) is definable in
CL
if there is a set
of
CL
-formulas that defines it.
Proposition 7.
The frame properties
(
n
)
,
(
r
)
,
(
i
)
,
(
s
)
,
(
c
)
,
(
d
)
,
(
t
)
,
(
b
)
,
(4)
,
and
(5)
are not definable in
CL
.
Proof.
Consider the following frames
F
1
=
S
1
,N
1
,
F
2
=
S
2
,N
2
,
F
3
=
S
3
,N
3
and
F
4
=
S
4
,N
4
:
{
s
1
}
{
s
2
}
{
t
3
}
{
s
4
,t
4
}
!
! "
s
1
s
2
{
s
3
t
3
s
4
s
4
}
t
4
∅
∅
{
t
4
}
F
1
F
2
F
3
F
4
Observe that
F
2
does not satisfy either (
d
)or(
t
);
F
2
satisfies all of (
n
), (
s
), (
c
), (
b
), (4), and (5), while
F
1
satisfies (
d
)and(
t
) but
F
3
does not satisfy any of
F
3
satisfies (
r
)and(
i
), while
F
4
does not satisfy (
r
)or(
i
). For instance,
those;
{
s
2
}∈
N
2
(
s
2
) but
∅
=
S
2
\{
s
2
}∈
N
2
(
s
2
), thus
F
2
does not satisfy (
d
);
t
3
∈{
t
3
}
,
but
{u ∈ S
3
|{s
3
} ∈ N
3
(
u
)
}
=
{s
3
,t
3
} ∈ N
3
(
t
3
), thus
F
3
does not satisfy (
b
);
N
4
(
s
4
)=
∅ ∈ N
4
(
s
4
), thus
F
4
does not satisfy (
r
).
We next show that: for any
˕
∈
CL
,
F
1
˕
iff
F
2
˕
iff
F
3
˕
iff
F
4
˕
.
Suppose that
F
1
˕
, then there exists
M
1
=
F
1
,V
1
such that
M
1
,s
1
˕
.
Define a valuation
V
2
on
F
2
as
p
∈
V
2
(
s
2
)iff
p
∈
V
1
(
s
1
) for all
p
∈
P
.By
induction on
˕
, we can show that
˕
, where the only
non-trivial case ʔ
˕
is proved as the proof of Prop. 2. From this, it follows that
M
2
,s
2
M
1
,s
1
˕
iff
M
2
,s
2
˕
, therefore
F
2
˕
. The converse is similar. Therefore
F
1
˕
iff
F
2
˕
.
Similarly, we can show
˕
.
If (
d
) were to be defined by a set of
CL
-formulas, say ʓ, then since
F
2
˕
iff
F
3
˕
,and
F
3
˕
iff
F
4
F
1
sat-
isfies (
d
), we have
F
2
satisfies
(
d
), contradiction. Thus (
d
) is not definable in
CL
. The undefinability of other
properties in question can be proved similarly.
F
1
ʓ. Then we should also have
F
2
ʓ, i.e.,
