Self provers and \(\Sigma_{1}\) sentences (Q2903747)

According to the authors, this paper is the second in a series of three related papers on modal methods in interpretability logics and applications. The first one is [\textit{E. Goris} and \textit{J. J. Joosten}, Log. J. IGPL 16, No. 4, 371--412 (2009; Zbl 1162.03033)]. 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. Stud. Logic Found. Math. 137, 475--546 (1998; Zbl 0915.03019)]. NEWLINENEWLINENEWLINE In the first paper the authors established some construction method for interpretability logics. Most techniques are aimed at establishing modal completeness of interpretability logics with respect to Veltman semantics. In the paper under review the construction method is used to obtain more results. The system ILM is interpretability logic of Peano arithmetic (see [\textit{A. Berarducci}, J. Symb. Log. 55, No. 3, 1059--1089 (1990; Zbl 0725.03037)]). The modal completeness of the system ILM was already proven in [\textit{D. de Jongh} and \textit{F. Veltman}, in: Proc. Summer Sch. Conf. Ded. 90th Anniv. Arend Heyting, Chaika/Bulg. 1988, 31--42 (1990; Zbl 0794.03026)]. Among these new results are some admissible rules for the systems ILM and GL (Gödel-Löb provability logic). Moreover, the new proof of modal completeness of ILM is used to classify all the essentially \(\Delta_1\) and \(\Sigma_1\) formulas of ILM (a modal interpretability sentence is essentially \(\Sigma_1\) if it is in theories \(T\) provably \(\Sigma_1\) for any arithmetical realization). A self-prover is a formula \(\varphi\) that implies its own provability, i.e., \(\varphi\rightarrow \square\varphi\). Each formula \(\varphi\) generates a self-prover \(\varphi\wedge \square \varphi\). The authors use the construction method to characterize those sentences of GL that generate a self-prover that is trivial in the sense that it is \(\Sigma_1\).