Information Technology Reference
In-Depth Information
4 Classical Contingency Logic
In this section, we present an axiomatization for classical contingency logic,
which is sound and strongly complete with respect to both the class of all neigh-
borhood frames, and also the class of all neighborhood frames satisfying (
c
). And
we obtain decidability for this logic.
Definition 7 (Proof System
CCL
).
The
proof system
CCL
is the set of
CL
-
formulas including axioms
and
ʔ
, and closed under the rule
ʔ
.
TAUT
Equ
RE
all instances of tautologies
TAUT
ʔ
ʔ
˕
ₔ
ʔ
¬
˕
Equ
˕
ₔ
ˈ
ʔ
RE
ʔ
˕
ₔ
ʔ
ˈ
A
derivation of
˕
from ʓ
, notation:
ʓ
-formulas
such that each formula is either the instantiation of an axiom, or an element
in
ʓ
, or follows from the prior formulas in the sequence by an inference rule. A
derivation of
˕ is a derivation of ˕ from the empty set
˕, is a finite sequence of
CL
∅
.Wewrite
˕ if there
is a derivation of ˕ in
CCL
.
We will show that
CCL
is sound and strongly complete with respect to the
class of all neighborhood frames, and also the class of all neighborhood frames
satisfying (
c
). For this, we introduce some definition and notation. Let ʓ be a set
of
CL
-formulas. We say ʓ is
CCL
-consistent
,ifʓ
↥
;ʓis
maximal
, if for every
˕
-consistent
and maximal. Recall that every consistent set can be extended to a maximal
consistent set (Lindenbaum's Lemma).
∈
CL
,
˕
∈
ʓor
¬
˕
∈
ʓ; ʓ is
maximal
CCL
-consistent
,ifitis
CCL
Definition 8 (Soundness, Strong Completeness).
Let S be a logical sys-
tem, and let
F
be a class of frames.
-
S is
sound
with respect to
F
, if for any ˕,
S
˕ implies
F
˕.
-
S is
strongly complete
with respect to
F
, if for any set of formulas
ʓ
and
any ˕,
ʓ
F
˕ implies
ʓ
S
˕.
Now we construct the canonical model of
CCL
.
Definition 9 (Canonical Model).
The
canonical neighborhood model
of
CCL
c
=
S
c
,N
c
,V
c
is the tuple
M
, such that
-
S
c
=
{
s
|
s is a maximal
CCL
-consistent set
}
-
N
c
(
s
)=
{|
˕
||
ʔ
˕
∈
s
}
-
V
c
(
p
)=
{
s
|
s
∈|
p
|}
where |˕|
=
{s ∈ S
c
| ˕ ∈ s} is the
proof set
of ˕ in
CCL
.
S
c
and formula ˕,
c
,s
Lemma 1 (Truth Lemma).
For any s
∈
M
˕ iff
c
s. That is to say, ˕
M
˕
∈
=
|
˕
|
.