On the provability logic of bounded arithmetic (Q685071)

\(I\Delta_ 0+ \Omega_ 1\) is a weak fragment of Peano Arithmetic which has received much attention in recent years. Its weakness consists in the fact that it does not prove that exponentiation is a total function (\(I\Delta_ 0+\Omega_ 1\) has an axiom expressing the totality of the sub-exponential function \(x^{\log(x)}\) and the scheme of induction restricted to bounded formulas). The authors study the provability logic of \(I\Delta_ 0+ \Omega_ 1\) in the spirit of a classical paper of \textit{R. M. Solovay} [Isr. J. Math. 25, 287-304 (1976; Zbl 0352.02019)], which considers the corresponding problem for Peano Arithmetic. Solovay's result is known to hold for every reasonable theory proving the totality of the exponential function, but is not known to be true for weak theories like \(I\Delta_ 0+ \Omega_ 1\). The authors prove some containments of the form \(\text{L}\subseteq\text{PL}\Omega\subset\text{Th}({\mathcal C})\), where L is the provability logic of PA, \(\text{PL}\Omega\) is the provability logic of \(I\Delta_ 0+ \Omega_ 1\), and \(\mathcal C\) is a suitable class of Kripke frames. They also prove that it is unlikely that \(\text{PL}\Omega\) is the theory of a class of Kripke frames, unless \(\text{PL}\Omega=\text{L}\). More precisely if \(\text{PL}\Omega=\text{Th}({\mathcal C})\), then every binary tree can be homomorphically embedded into some frame of \(\mathcal C\). It remains open whether \(\text{PL}\Omega=\text{L}\). The latter problem might depend on difficult questions of computational complexity. In fact if \(\text{PL}\Omega\neq \text{L}\), it would follow that \(I\Delta_ 0+ \Omega_ 1\) does not prove its completeness with respect to \(\Sigma^ 0_ 1\)-formulas, and \textit{a fortiori} it does not prove the Matiyasevich-Robinson-Davis-Putnam theorem (every r.e. set is diophantine). On the other hand if \(I\Delta_ 0+ \Omega_ 1\) did prove its completeness with respect to \(\Sigma^ 0_ 1\)-formula, it would follow not only that \(\text{L}=\text{PL}\Omega\), but also that \(\text{NP}=\text{co-NP}\). The possibility remains that \(\text{L}= \text{PL}\Omega\) and that one could give a proof of this fact without making use of \(\Sigma^ 0_ 1\)-completeness. Such a project is not without challenge due to the ubiquity of \(\Sigma^ 0_ 1\)-completeness in the whole area of provability logic.