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
˕
=
|
˕
|
.
Search WWH ::




Custom Search