OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation
Journal of Logic and Computation
Volume 12, Issue 5, October 2002: pp. 861884
Theoremhoodpreserving Maps Characterizing Cut Elimination for Modal Provability Logics
Stéphane Demri^{1} and Rajeev Goré^{1}
^{1}Lab. Spécification et Vérification, ENS de Cachan & CNRS UMR 8643, 61 Av. Pdt. Wilson, 94235 Cachan Cedex, France. Email: demri@lsv.enscachan.fr
^{2}Automated Reasoning Group and Department of Computer Science, Australian National University, Canberra ACT 0200, Australia. Email: rpg@arp.anu.edu.au
Propositional modal provability logics like G and Grz have arithmetical interpretations where [square][phgr] can be read as 'formula [phgr] is provable in Peano Arithmetic'. These logics are decidable but are characterized by classes of Kripke frames which are not firstorder definable. By abstracting the aspects common to their characteristic axioms we define the notion of a formula generation map F(P) in one propositional variable. We then focus our attention on the properly displayable subset of all (firstorder definable) Sahlqvist modal logics. For any logic L from this subset, we consider the (provability) logic LF obtained by the addition of an axiom based upon a formula generation map F(P) so that LF = L + F(P). The class of such logics includes G and Grz. By appropriately modifying the right introduction rules for [square], we give (not necessarily cutfree) display calculi for every such logic. We define the pseudodisplayable subset of these logics as those whose display calculi enjoy cutelimination for sequents of the form [top] [vdash] [phgr] for any formula [phgr]. We then show that for any provability logic LF having a conservative tense extension, there is a map f on formulae such that LF is pseudodisplayable if and only if f maps theorems of LF to theorems of the underlying logic L and vice versa. By using a standard renaming technique we can guarantee that there is a polynomialtime translation from LF into L. All proofs are purely syntactic and show the versatility of display calculi since similar results using traditional Gentzen calculi are not possible for as broad a range of logics and require further conditions. Our maps generalize previously known maps from G into K4. An application of our results gives an O(n.log n)^{3}) translation from the ('second order') provability logic Grz into a decidable subset of firstorder logic. Since each of our logics L is a Sahlqvist logic, it is firstorder definable, and hence each L has a translation into firstorder logic. Our results therefore show that all pseudodisplayable logics LF are 'essentially firstorder' even though their characteristic axiom may not be firstorder definable.
Keywords: Provability modal logic; display logic; cut elimination; manyone reduction
Table of Contents
FullText PDF (231 KB)
