Fan, Jie and Wang, Yanjing and van Ditmarsch, Hans
Advances in Modal Logic Vol.10, College Publications, 10: 178—196, 2014
Publication year: 2014

Abstract. A formula is contingent if it is possibly true and possibly false. A formula is non- contingent if it is not contingent, i.e., if it is necessarily true or necessarily false. In an epistemic setting, a formula is contingent’ means that you are ignorant about its value, whereas a formula is non-contingent’ means that you know whether it is true. Although non-contingency is definable in terms of necessity as above, necessity is not always definable in terms of non-contingency, as studied in the literature. We propose an almost-definability’ schema AD for non-contingency logic, the logic with the noncontingency operator as the only modality, making precise when necessity is definable with non-contingency. Based on AD we propose a notion of bisimulation for non- contingency logic, and characterize non-contingency logic as the (non-contingency) bisimulation invariant fragment of modal logic and of first-order logic. A known pain for non-contingency logic is the absence of axioms characterizing frame properties. This makes it harder to find axiomatizations of non-contingency logic over given frame classes. In particular, no axiomatization over symmetric frames is known, despite the rich results about non-contingency logic obtained in the literature since the 1960s. We demonstrate that the almost-definability’ schema AD can guide our search for proper axioms for certain frame properties, and help us in defining the canonical models. Following this idea, as the main result, we give a complete axiomatization of non-contingency logic over symmetric frames.