Technical reports

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

Rajeev Gore

February 1993, 19 pages

DOI: 10.48456/tr-288

Abstract

We present sound, (weakly) complete and cut-free tableau systems for the propositional normal modal logics S4.3, S4.3.1 and S4.14. When the modality □ is given a temporal interpretation, these logics respectively model time as a linear dense sequence of points; as a linear discrete sequence of points; and as a branching tree where each branch is a linear discrete sequence of points.

Although cut-free, the last two systems do not possess the subformula property. But for any given finite set of formulae X the “superformulae” involved are always bounded by a finite set of formulae X*L depending only on X and the logic L. Thus each system gives a nondeterministic decision procedure for the logic in question. The completeness proofs yield deterministic decision procedures for each logic because each proof is constructive.

Each tableau system has a cut-free sequent analogue proving that Gentzen’s cut-elimination theorem holds for these logics. The techniques are due to Hintikka and Rautenberg.

Full text

PDF (1.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-288,
  author =	 {Gore, Rajeev},
  title = 	 {{Cut-free sequent and tableau systems for propositional
         	   Diodorean modal logics}},
  year = 	 1993,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-288.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-288},
  number = 	 {UCAM-CL-TR-288}
}