On the scheme of induction for bounded arithmetic formulas (Q1104318)

This work constitutes, in my opinion, a fundamental paper in the metamathematics of weak systems of arithmetic. What the authors do for fragments of arithmetic is, in a sense, similar to what \textit{S. Feferman} did for strong systems like PA in the paper ``Arithmetization of metamathematics in a general setting'' [Fundam. Math. 49, 35-92 (1960; Zbl 0095.243)]. The method used here is, however, model-theoretic where Feferman's results have been proved syntactically. A rather weak theory in which there is a good arithmetization of the syntax is \(I\Delta_ 0+Exp\). The authors, however, work in a weaker system where Exp is replaced by the weaker statement \(\Omega_ 1\equiv \forall x\exists y\) \([y=x^{| x|}]\) (here \(| x|\) denotes the length of the binary expansion of x); in these systems, one can carry out a sufficient part of arithmetization of syntax: even if one cannot prove the principle \(\phi\) (x)\(\to \Pr ov\ulcorner \phi \dot x\urcorner\) for \(\phi x\in \Delta_ 0\), one can prove this principle for a subclass of \(\Delta_ 0\) formulas; there is sufficient to prove the principle Prov\(\ulcorner \phi \urcorner \to \Pr ov\ulcorner \Pr ov\ulcorner \phi \urcorner \urcorner\) and, therefore, Gödel's second incompleteness theorem. A lot of results about relative consistency or unprovability of consistency statements are proved, namely: 1) \(I\Delta_ 0+\Omega_ 1\vdash Con(I\Delta_ 0)\to Con(I\Delta_ 0+\Omega_ n)\) (where \(\Omega_ n\) states the totality of the iterated exponentiation exp(x,\(| x|,...,|...| x|...|_{n\quad times}).\) 2) \(I\Delta_ 0+\Omega_ n\nvdash Con(I\Delta_ 0)\). This is strengthened by the following: \(I\Delta_ 0+\exp \nvdash Con Q\) where Q is Robinson's arithmetic. 3) \(I\Delta_ 0+\exp \nvdash Con(I\Delta_ 0)\to Con(I\Delta_ 0+\exp).\) 4) If \(\phi\) \(x\in R\) \(+\), then \(I\Delta_ 0+\exp \vdash \forall x \neg \phi x\) iff \(I\Delta_ 0+\Omega_ 1+Con(I\Delta_ 0,k)\vdash \forall x \neg \phi x\) (here R \(+\) is a suitable subclass of \(\Delta_ 0\). Cf. the paper for the definition; furthermore Con(T,\(\kappa)\) is the sentence asserting that there is no proof of \(\bot\) from T involving only substitution instances of formulas of length \(\leq \kappa).\) 5) \(I\Delta_ 0+\exp\) is not \(\Pi_ 1\) conservative over \(I\Delta_ 0+\Omega_ 1\).