Neighborhood Contingency Logic - Logic and Its Applications - page 97

Proof. By induction on ˕ . The base cases and Boolean cases are straightforward.
The non-trivial case is ʔ ˕ .

⃒⃐ semantics ˕ M c ˕ ) M c

c ,s

N c ( s )or( N c ( s ) M ʔ ˕ ∈ ¬ ∈

N c ( s )or N c ( s )

⃒⃐ IH | ˕ |∈ |¬ ˕ |∈

⃒⃐ Def. N c ʔ ˕ ∈ s or ʔ ¬ ˕ ∈ s

⃒⃐ Δ Equ ʔ ˕ ∈ s

We also need to prove that N c is well defined.
Lemma 2. If

N c ( s ) and | ˕ |∈ | ˕ | = | ˈ | ,then ʔ ˈ ∈ s.

N c ( s ), Proof. Assume that the conditions hold, to show that ʔ ˈ ∈ s .From | ˕ |∈

it follows that ʔ ˕ ∈ s .By | ˕ | = | ˈ | ,wehave ˕ ₔ ˈ :otherwise, ¬ ( ˕ ₔ ˈ )

S c such

would be consistent, then by Lindenbaum's Lemma, there exists s ∈

that ¬ ( ˕ ₔ ˈ ) ∈ s ,thus ˕ ∈ s ⃔ ˈ ∈ s , contrary to | ˕ | = | ˈ | .By RE ʔweget

ʔ ˕ ₔ ʔ ˈ ,thusʔ ˈ ∈ s .

Theorem 1. is sound and strongly complete with respect to the class of

all neighborhood frames.

CCL

Proof. Soundness is clear from Prop. 1. For completeness, suppose that ʓ ˕ ,
then ʓ ∪{¬˕} is consistent. By Lindenbaum's Lemma, there exists s ∈ S c such
that ʓ ∪{¬ ˕ }ↆ s . By Lemma 1, ʓ ˕ , as desired.

is the smallest contingency logic under neighbor-
hood semantics; this is why we call

Thm. 1 indicates that CCL

classical contingency logic. Surprisingly,
the same logic is also characterized by the class of frames satisfying ( c ).
Theorem 2. CCL

CCL

is sound and strongly complete with respect to the class of
frames satisfying ( c ) .

S c , N c ( s ) satisfies Proof. Due to Thm. 1, it suces to show that for each s ∈

( c ).
Let s S c . Assume that X N c ( s ). By definition of N c , X = N c ( s )

∈ ∈ | ˕ |∈

for some ˕ ,andthenʔ ˕ ∈ s .Byʔ Equ ,wehaveʔ ¬ ˕ ∈ s . Using definition of

N c again, we obtain that N c ( s ), i.e., S N c ( s ), thus S N c ( s ).

|¬ ˕ |∈ \| ˕ |∈ \ X ∈

Due to ʔ ˕ ₔ ˕ ∨ ¬ ˕ , and the decidability of classical modal logic [3],

the logic CCL is also decidable.

Proposition 8 (Decidability of CCL ). The logic CCL is decidable.

5 Neighborhood Semantics and Kripke Semantics

This section deals with the relationship between neighborhood semantics and
Kripke semantics for contingency logic. The result is: there is a one-to-one cor-
respondence between augmented neighborhood frames and Kripke frames for
CL . Thus neighborhood semantics for CL can be seen as an extension of Kripke
semantics for CL .