Tractable transformations from modal provability logics into first-order logic (Q4263154)

This work, consisting of six parts and an appendix, deals with modal provability logics, display calculi and transformations from LF into L. The main result of the paper is Theorem 5. The statements below are equivalent: 1. For all formulae \( \phi, \phi \in \text{LF} \) iff \( f(\phi,1) \in \text{L}\). 2. LF is pseudo displayable. Let K be the standard axiomatic Hilbert system and let L be an extension of K (including K). In the second part the following well-known extensions L of K: T, K4, S4, G, Grz are considered. (For the logics K4, KD4 and S4 the transformation approach is based on a resolution decision procedure considered by \textit{H. Ganzinger, U. Hustadt, C. Mayer} and \textit{R. Schmidt} [in: Advances in modal logic '98, AiML'98 (Uppsala University, Uppsala), 182-191 (1998)]. Let L be any proper displayable logic and let F be any formula generation map. The authors write LF to denote the logic obtained from L by addition of the scheme \( \square (F(p) \Rightarrow p) \Rightarrow \square p \). In part three the authors define the calculus \(\delta \text{LF}\). They say that LF is pseudo displayable iff for any \(\phi \in \text{FML}\), \(I \vdash \phi \) has a proof in \(\delta \text{LF}\) iff \( I \vdash \phi \) has a cut-free proof in \(\delta \text{LF}\). Then, using Belnap's proof-theoretical framework Display Logic [\textit{N. D. Belnap}, J. Philos. Logic 11, 375-417 (1982; Zbl 0509.03008)], the authors characterize 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. In most cases the proofs of the authors' results are omitted. For the entire collection see [Zbl 0917.00015].