Provability and interpretability logics with restricted realizations (Q435232)

The provability logic GL (Gödel-Löb) is a simple modal description of provability. The axioms of GL are all tautologies, \(\square (A\rightarrow B)\rightarrow (\square A\rightarrow \square B),\) \(\square (\square A\rightarrow A)\rightarrow \square A.\) The inference rules of GL are modus ponens and necessitation \(A/ \square A.\) Modal provability logic usually studies the operator `provability in PA' as the modal connective necessary, \(\square.\) The propositional provability logic GL was axiomatized by \textit{R. M. Solovay} [Isr. J. Math. 25, 287--304 (1976; Zbl 0352.02019)]. The paper under review deals with restricted cases of Solovay's theorem where an alternative proof method is available. The authors study provability logics of some theory with restricted arithmetical realizations. The result is a logic of linear frames. After that, the interpretability logics are considered. An interpretability logic is a modal description of the notion of relativized interpretability between two theories. For detailed definitions see e.g. [\textit{A. Visser}, CSLI Lect. Notes 87, 307--359 (1998; Zbl 0915.03020); \textit{G. Japaridze} and \textit{D. de Jongh}, in: Handbook of proof theory. Amsterdam: Elsevier, 475--546 (1998; Zbl 0915.03019)]. An interpretability logic can be viewed as an extension of provability logic. The authors give upper bounds for the logic IL(PRA). The characterization of IL(PRA) remains a major open question in interpretability logics (see e.g. [\textit{M. Bílkova} et al., Ann. Pure Appl. Logic 16, No. 2, 128--138 (2009; Zbl 1184.03011)]). It is necessary to mention that upper bounds are connected with linear frames, too. The new method is used to obtain the nontrivial result \(\mathrm{IL(PRA)}\subset \mathrm{ILM}\).