Two Variants of Noncontingency Operator

By slightly adapting two equivalent semantics of noncontingency operator, we obtain two variants, ⊡ and ⊞, with nonequivalent semantics. We show that on the class of models satisfying any of five basic properties (i.e., seriality, reflexivity, transitivity, symmetry, Euclideanness), the logic L(⊡), which has ⊡ as the sole modal primitive, is less expressive than the logic L(⊞), which has ⊞ as the sole modal primitive. We investigate the frame definability of both languages. We then axiomatize L(⊞) and 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 L(⊡) over serial frames and also over symmetric frames.