Information Technology Reference
In-Depth Information
Proposition 9.
For every Kripke model
M
K
=
S, R, V
there exists an aug-
mented neighborhood model
M
N
=
S, N, V
such that for all s
∈
S and all ˕
∈
K
N
K
,s
N
,s
˕, i.e., ˕
M
=
˕
M
CL
,
M
˕
⃒⃐ M
.
K
=
Proof.
Let
M
S, R, V
be a Kripke model. Define a neighborhood model
N
=
M
S, N, V
by stipulating
N
(
s
)=
{
X
ↆ
S
|
R
(
s
)
ↆ
X
}
for each
s
∈
S
,
where
R
(
s
)=
{
t
∈
S
|
sRt
}
.
N
is augmented: if
X
We first show that
M
∈
N
(
s
)and
X
ↆ
Y
,then
R
(
s
)
ↆ
X
ↆ
Y
,thus
Y
∈
N
(
s
). Given any
X
∈
N
(
s
), we have
R
(
s
)
ↆ
X
.Fromthis
ↆ
{
=
N
(
s
), therefore
follows that
R
(
s
)
X
|
X
∈
N
(
s
)
}
∩
N
(
s
)
∈
N
(
s
).
K
,s
N
,s
Next, we show that for all
s
∈
S
and all
˕
∈
CL
,
M
˕
⃒⃐ M
˕
.
The proof proceeds by induction on
˕
. The only non-trivial case is ʔ
˕
.
˕
M
K
or
R
(
s
)
˕
)
M
K
K
,s
M
ʔ
˕
⃒⃐
Kripke semantics
R
(
s
)
ↆ
ↆ
(
¬
N
N
⃒⃐
IH
R
(
s
)
ↆ
˕
M
or
R
(
s
)
ↆ
¬
˕
)
M
(
N
N
˕
M
˕
)
M
⃒⃐
Def.
N
∈
N
(
s
)or(
¬
∈
N
(
s
)
N
,s
⃒⃐
Nb. semantics
M
ʔ
˕
N
=
Proposition 10.
For every augmented neighborhood model
M
S, N, V
,
K
=
there exists a Kripke model
M
S, R, V
such that for all s
∈
S and all
˕, i.e., ˕
M
N
=
˕
M
K
.
N
,s
K
,s
˕
∈
CL
,
M
˕
⃒⃐ M
N
=
Proof.
Let
M
S, N, V
be an augmented neighborhood model. Define a
by stipulating
R
(
s
)=
N
(
s
)foreach
s
K
=
Kripke model
M
S, R, V
∈
S
.
By induction on
˕
. The only non-trivial case is ʔ
˕
.
˕
M
N
˕
)
M
N
N
,s
M
ʔ
˕
⃒⃐
Nh. semantics
∈
N
(
s
)or(
¬
∈
N
(
s
)
⃒⃐
augmentation of
M
N
N
(
s
)
or
N
(
s
)
N
N
˕
M
˕
)
M
ↆ
ↆ
(
¬
˕
M
K
or
R
(
s
)
˕
)
M
K
⃒⃐
Def.
R,
IH
R
(
s
)
ↆ
ↆ
(
¬
K
,s
⃒⃐
Kripke semantics
M
ʔ
˕
The above two propositions have nice applications. For instance, by Prop. 9,
we get that ʔ(
˕ ∧ ˈ
)
→
ʔ
˕
is not valid on the class of augmented neighbor-
hood frames, because it is not valid on the class of Kripke frames. For another
example, consider the axiomatization
of contingency logic, which is known
to be complete under Kripke semantics [6]. By Prop. 10,
CL
is sound on the
class of augmented frames, because it is sound on the class of Kripke frames.
CL
6Con lu on
We proposed to interpret contingency logic on neighborhood models. We showed
that contingency logic is less expressive than modal logic on various classes of
neighborhood models, but equally expressive on other classes of models, and that
most standard properties of neighborhood frames, which are definable in modal
logic, are undefinable in contingency logic. We further proposed a decidable
axiomatization for classical contingency logic and provided a correspondence
