Normal forms in modal logic.
Kit Fine · Notre Dame Journal of Formal Logic · 1975
KIT FINEThere are two main methods of completeness proof in modal logic.One may use maximally consistent theories or their algebraic counterparts, on the one hand, or semantic tableaux and their variants, on the other hand.The former method is elegant but not constructive, the latter method is constructive but not elegant.Normal forms have been comparatively neglected in the study of modal sentential logic.Their champions include Carnap [3], von Wright [10], Anderson [l] and Cresswell [4].However, normal forms can provide elegant and constructive proofs of many standard results.They can also provide proofs of results that are not readily proved by standard means.Section 1 presents preliminaries.Sections 2 and 3 establish a reduction to normal form and a consequent construction of models.Section 4 contains a general completeness result.Finally, section 5 provides normal formings for the logics T and K4.1 Preliminaries Formulas are constructed in the usual way from the following items: the set SI = {p 0 , p u . ..} of sentence letters; truthfunctional operators, say v and -the modal operator O; and the brackets ( and ).We follow standard conventions concerning abbreviations, bracketing and use-mention.In particular, we use T for p 0 v -p 0 and 1 for -T.The minimal logic K is the set of formulas derivable from the following postulates:) is the result of substituting B for A in C; similarly for (A Pi /B).We refer to postulates 1 and 4 together as PC.A logic is a set of formulas that contains K and is closed under the same rules as K.Given a