Two variants of noncontingency operator

Abstract

By slightly adapting two equivalent semantics of noncontingency operator, we obtain two variants, $⊡$ and $⊞$, with non-equivalent semantics. We show that on the class of models satisfying any of five basic properties (i.e. seriality, reflexivity, transitivity, symmetry, Euclidicity), the logic $\mathcal{L}(⊡)$, which has $⊡$ as the sole modal primitive, is less expressive than the logic $\mathcal{L}(⊞)$, which has $⊞$ as the sole modal primitive. We investigate the frame definability of both languages. We then axiomatize $\mathcal{L}(⊞)$ and $\mathcal{L}(⊡)$ over various classes of bimodal frames. Among other results, a notion of morphisms, called `$⊡$-morphisms', are provided to show the completeness of axiomatizations of $\mathcal{L}(⊡)$ over serial frames and also over symmetric frames.

27 pages