Neighborhood Contingency Logic - Logic and Its Applications - page 94

However, on the class of neighborhood models satisfying ( t ), CL and ML are
equally expressive. This is as expected, as the results on Kripke semantics are
similar: once frames are reflexive, modal necessity is definable from contingency
[11]. Nevertheless, it is surprising that the same story goes with the class of
models satisfying ( c ).

Proposition 5. CL and ML are equally expressive on the class of neighborhood

models satisfying ( t ) .

Proof. Define a translation t from CL to ML , and a translation t from ML
to CL , such that each translation preserves propositional variables and Boolean
connectives, and t (ʔ ˕ )=

t ( ˕ ).
Due to Prop. 1, by induction on ˕ ∈ CL , we can show that ˕ ₔ t ( ˕ ).
Therefore CL ML .
Moreover, by induction, we show ( ): for any ˕

t ( ˕ )and t ( ˕ )=ʔ t ( ˕ )

t ( ˕ ) ∨ ¬ ∧

∈ ML ,wehave M t ˕ ₔ

t ( ˕ ), where

M t is the class of models satisfying ( t ). Given any M = S, N, V ∈

M t and any s ∈M . We only need to show the case for ˕ , i.e., M ,s ˕ iff

t ( ˕ ).
First, suppose that

ʔ t ( ˕ ) M ,s ∧

˕ ,then ˕ M ∈ M ,s N ( s ), by the induction hypothesis,

( t ( ˕ )) M ∈ N ( s ), then ( t ( ˕ )) M ∈ t ( ˕ )) M ∈

N ( s )or( ¬ N ( s ), i.e., M ,s

ʔ t ( ˕ ). From ( t ( ˕ )) M ∈ ( t ( ˕ )) M ,

N ( s ) and condition ( t ), it follows that s ∈

t ( ˕ ), therefore ʔ t ( ˕ ) t ( ˕ ).

that is, M ,s M ,s ∧

ʔ t ( ˕ ) t ( ˕ ). From ʔ t ( ˕ ), it Conversely, suppose that M ,s ∧ M ,s

follows that ( t ( ˕ )) M ∈ t ( ˕ )) M ∈ t ( ˕ )) M ∈ N ( s )or( ¬ N ( s ). If ( ¬ N ( s ), since

t ( ˕ )) M , i.e., t ( ˕ ), contrary to the

M satisfies ( t ), it follows that s ∈ ( ¬ M ,s ¬

t ( ˕ ), thus ( t ( ˕ )) M ∈

supposition M ,s N ( s ). By the induction hypothesis,

we have ˕ M ∈

˕ .
We have thus shown ( ), then ML

N ( s ), i.e., M ,s

CL , and therefore CL ≡ ML on the

class of models satisfying ( t ).

Proposition 6. CL and ML are equally expressive on the class of neighborhood

models satisfying ( c ) .

Proof. Define t and tr , respectively, as t and t in the proof of Prop. 5, except
that tr (

˕ )=ʔ tr ( ˕ ).
Similar to the corresponding proof in Prop. 5, we can show that CL ML .

Besides, by induction, we show ( ∗ ): for any ˕ ∈ ML ,wehave M c ˕ ₔ tr ( ˕ ),

where M c is the class of models satisfying ( c ). Given any M = S, N, V ∈ M c

and any s ∈M . We only need to show the case for ˕ , i.e., M ,s ˕ iff

M

ʔ tr ( ˕ ).
'Only if' can be shown easily due to

,s

ʔ ˕

ₔ ˕ ∨ ¬ ˕ .

tr ( ˕ )) M ∈
N ( s ). If ( ¬tr ( ˕ )) M ∈ N ( s ), since M satisfies ( c ), it follows that ( tr ( ˕ )) M ∈
N ( s ), thus we always have ( tr ( ˕ )) M ∈ N ( s ). By the induction hypothesis, we
have ˕ M ∈ N ( s ), i.e., M,s ˕ .
We have thus shown (

ʔ tr ( ˕ ), that is, ( tr ( ˕ )) M ∈

M ,s N ( s )or( ¬

Now suppose that

∗ ), then ML CL , and therefore CL ≡ ML on the

class of models satisfying ( c ).