Minimal Non-contingency Logic
Steven T. Kuhn · Notre Dame Journal of Formal Logic · 1995
Simple finite axiomatizations are given for versions of the modal logics K and K4 with non-contingency (or contingency) as the sole modal primitive.This answers two questions of I. L. Humberstone.Modal logic is supposed to be the study of principles of reasoning involving necessity, possibility, impossibility, contingency, non-contingency, and related notions.It has become customary to construct systems in which necessity alone, or necessity and possibility, are treated as primitive connectives.In most such systems the modal concepts mentioned are all interdefinable, so that these systems can be regarded as systematizing, at least indirectly, reasoning involving all of them.Nevertheless, systems in which contingency or non-contingency are treated as primitive connectives have certain technical and philosophical interest (see Montgomery and Routley [5]).Such systems have been investigated in Montgomery and Routley [5], [6], [7], and Mortensen [4].(See also Brogan [1] for a discussion of Aristotle's logic of contingency.) The investigations were facilitated by the observation that necessity is definable in the systems considered.For example, in extensions of the system T, necessarily A is equivalent to A and not contingently A. Cresswell [2] provides examples of systems not containing T in which necessity is otherwise definable.In the contingency version of the "minimal" modal system K, however, necessity is not definable, and so a general account of the logic of contingency has not emerged so quickly.Humberstone [3] solves this problem by showing how to modify standard completeness arguments for necessity systems to a system in which non-contingency is primitive.The axiomatization in Section 3 of [3], however, contains a somewhat unwieldy rule schema, and the author asks whether a finite axiomatization is possible.This note answers that question affirmatively by presenting a considerably simpler completeness proof that does not require the unwieldy schema.It also solves another problem raised in [3], axiomatizing the non-contingency version of K4.Our base language is that of classical propositional logic with ∨ and ¬ as primitive connectives.We add two "modal" connectives, and ∇, for contingency