Gentzen systems for modal logic.
Lou Goble · Notre Dame Journal of Formal Logic · 1974
Nice Gentzen formulations of the normal modal systems T and S4 have been know for some time; see, for example, Kanger [5] or Curry [l].A similar formulation of S5 has also been given, but it is not so nice as the Elimination Theorem is not provable for it.I shall present here sets of rules for several of the non-normal modal systems which are akin to T and S4.Each of the L-systems to be defined here has an Elimination Theorem which may be proved by the methods of Gentzen [3].These systems are useful, in that each of them has a decision procedure, following, for example, Kleene [6], §80.1 Epistemic Systems In order to provide a decision procedure for Lewis' system S2, Ohnishi and Matsumoto [ll] defined a system, Q2, which had the property that a formula, A, was provable in S2 if and only if the consecution H(p ^> p)\\-A was provable in Q2.Q2 was formed by adjoining to any appropriate formulation of the classical propositional calculus, such as Gentzen's LK [3], the rules:where for (l(-N)Γ must be non-empty.Here, and elsewhere, A, B, C, etc. are well formed formulas formed from atomic formulas by means of propositional connectives, including N for necessity; Γ, Δ, etc. are any finite sequences of (zero or more) constituent formulas, A, B, C, etc. Consecutions a, β, etc. are expressions ΓII-Δ.NΓ is the result of applying the operator N to each member of Γ.Q2 is equivalent to the Hubert style system E2 introduced by Lemmon (see, for example, [8]), in the sense that A is provable in E2 if and only if \\-A is provable in Q2.Besides the axioms and rules for the classical propositional calculus, E2 has only the axioms A.