Technical reports

Cut-free sequent and tableau systems for propositional normal modal logics

Rajeev Prakhakar Goré

May 1992, 160 pages

DOI: 10.48456/tr-257

Abstract

We present a unified treatment of tableau, sequent and axiomatic formulations for many propositional normal modal logics, thus unifying and extending the work of Hanson, Segerberg, Zeman, Mints, Fitting, Rautenberg and Shvarts. The primary emphasis is on tableau systems as the completeness proofs are easier in this setting. Each tableau system has a natural sequent analogue defining a finitary provability relation for each axiomatically formulated logic L. Consequently, any tableau proof can be converted into a sequent proof which can be read downwards to obtain an axiomatic proof. In particular, we present cut-free sequent systems for the logics S4.3, S4.3.1 and S4.14. These three logics have important temporal interpretations and the sequent systems appear to be new.

All systems are sound and (weakly) complete with respect to their known finite frame Kripke semantics. By concentrating almost exclusively on finite tree frames we obtain finer characterisation results, particularly for the logics with natural temporal interpretations. In particular, all proofs of tableau completeness are constructive and yield the finite model property and decidability for each logic.

Most of these systems are cut-free giving a Gentzen cut-elimination theorem for the logic in question. But even when the cut rule is required, all uses of it remain analytic. Some systems do not possess the subformula property. But in all such cases the class of “superformulae” remains bounded, giving an analytic superformula property. Thus all systems remain totally amenable to computer implementation and immediately serve as nondeterministic decision procedures for the logics they formulate. Furthermore, the constructive completeness proofs yield deterministic decision procedures for all the logics concerned.

In obtaining these systems we domonstrate that the subformula property can be broken in a systematic and analytic way while still retaining decidability. This should not be surprising since it is known that modal logic is a form of second order logic and that the subformula property does not hold for higher order logics.

Full text

PDF (9.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-257,
  author =	 {Gor{\'e}, Rajeev Prakhakar},
  title = 	 {{Cut-free sequent and tableau systems for propositional
         	   normal modal logics}},
  year = 	 1992,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-257.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-257},
  number = 	 {UCAM-CL-TR-257}
}