Theoremhood Preserving Maps Characterising Cut Elimination for Modal Provability Logics

Stéphane Demri & Rajeev Goré

Propositional modal provability logics like G and Grz have arithmetical interpretations where □φ can be read as “formula φ is provable in Peano Arithmetic”. These logics are decidable but are characterised by classes of Kripke frames which are not first-order 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 define a class of (provability) logics where each logic LF is obtained from a first-order definable (Sahlqvist) modal logic L 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 □, we give (not necessarily cut-free) display calculi for every such logic having a conservative tense extension. We define the pseudo-displayable subset of these logics as those whose display calculi enjoy cut-elimination for sequents of the form ⊤ ⊢ φ for any formula φ. We then show that for any provability logic LF there is a map f on formulae such that LF is pseudo-displayable 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 polynomial-time 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 generalise previously known maps from G into K4. An application of our results gives an O((n.logn)^{3}) translation from the (“second order”) provability logic Grz into a decidable subset of first-order logic. Since each of our logics L is a Sahlqvist logic, it is first-order definable, and hence each L has a translation into first-order logic. Our results therefore show that all pseudo-displayable logics LF are “essentially first-order” even though their characteristic axiom may not be first-order definable. Authors supported by an Australian Research Council International Researcher Exchange Award and Queen Elizabeth II Award respectively.

Addresses Stéphane Demri: Laboratoire LEIBNIZ C.N.R.S., 38000 Grenoble, France

E-mail: demri@imag.fr

Rajeev Goré: Auto. Reasoning Grp. & Dept. Comp. Sci., Australian National University, Canberra 0200, Australia

E-mail: rpg@arp.anu.edu.au