Tractable transformations from modal provability logics into first-order logic

Abstract

We define a class of modal logics LF by uniformly extend­ing a class of modal logics L. Each logic L is characterised by a class of first-order definable frames, but the corresponding logic LF is some­times characterised by classes of modal frames that are not first-order definable. The class LF includes provability logics with deep arithmeti­cal interpretations. Using Belnap's proof-theoretical framework Display Logic we characterise the “pseudo-displayable” subclass of LF and show how to define polynomial-time transformations from each such LF into the corresponding L, and hence into first-order classical logic. Theorem provers for classical first-order logic can then be used to mechanise de­duction in these “psuedo-displayable second order” modal logics. Show more