Alternative completeness theorems for modal systems.
Maxwell J. Cresswell · Notre Dame Journal of Formal Logic · 1967
Since the development of semantics for the modal systems T, S4 and S5 notably in [1] there have appeared several completeness theorems for these systems.Some, e.g.[I] 1 rely on the method of semantic tableaux which are shewn to give a decision procedure.A simpler proof, though one not yielding to decision procedure, follows from [3] 2 .In part I of this paper we shew, by extensions of known results, some relations between the completeness of S5, S4 and T. In part Π we shew how Anderson's [5] decision procedure for T can yield a relatively simple completeness proof for that system.I.The system T (v.[6]) is a system of propositional modal logic based on the following additions to some standard axiomatic basis for the propositional calculus, (L for necessity); LAI Lp^> p LA2 L(p D q) D {Lp D Lq) LR1 Hα-^hlα 54 is T with the addition of LA3 Lp-D LLp 55 is T with the addition of LA4 ~Lp D L ~ Lp We define validity in T, S4, and S5 in the manner of [1] as truth in all T, S4, S5 models.A T-model is an ordered triple where W is a set of objects (worlds), R a reflexive relation over W, and Fa function (assignment) taking as arguments a.) wffs of T b.) members of Wand as values the truth values 1 or 0, and satisfying the following: