A short note on essentially \(\Sigma_1\) sentences (Q1945709)

A modal formula \(F\) is essentially \(\Sigma_1\) with respect to theory \(T\) if, under any arithmetical interpretations \(\ast\) into \(T,\) \(F^\ast\) is a \(\Sigma_1\) formula. \textit{A.~Visser} proved in [Ann.~Pure~App.~Logic 73, No. 1, 109--142 (1995; Zbl 0828.03008)] that a formula \(F\) of the provability logic GL (Gödel-Löb) is essentially \(\Sigma_1\) with respect to PA if and only if \(F\) is provably equivalent in GL to a disjunction of formulas of the form \(\square B\). In [Stud.\ Fuzziness Soft Comput.\ 24, 246--254 (1999; Zbl 0923.03025)], \textit{D.\ de Jongh} and \textit{D.\ Pianigiani} extended the result to system \(R\) of Guaspari-Solovay. \textit{E.\ Goris} and \textit{J.\ J.\ Joosten} classified in [Log. J. IGPL 16, No. 4, 371--412 (2008; Zbl 1162.03033); ibid. 20, No. 1, 1--21 (2012; Zbl 1252.03140)] all essentially \(\Sigma_1\) sentences of ILM (interpretability logic with Montagna principle) with respect to interpretations in essentially reflexive recursively enumerable arithmetical theories. In the paper under review, the authors show that a characterization of this kind can be obtained also for formulas of the interpretability logic ILP, with respect to any finitely axiomatizable \(\Sigma_1\)-sound extension of \(\mathrm{I}\Delta_0 + \mathrm{Supexp}.\) It is proved that the same characterization does not extend to \(\mathrm I\Delta_0+\mathrm{Exp}\) and a conjecture is formulated about essentially \(\Sigma_1\) ILP-formulas with respect to \(\mathrm I\Delta_0+\mathrm{Exp}.\)