On axiom schemes for \(T\)-provably \(\Delta_1\) formulas (Q2449854): Difference between revisions

Let \(T\) be a theory in the language of PA, and let \(\Delta_1(T)\) be the set of formulas which are provably \(\Delta_1\) in \(T\). Motivated by the open question whether \(I\Delta_1\) is equivalent to \(B\Sigma_1\) over \(I\Delta_0\), the authors consider theories \(I\Delta_1(T)\), and \(L\Delta_1(T)\) axiomatized by Robinson's \(Q\) and the induction axioms and the least number principle, respectively, for all formulas in \(\Delta_1(T)\); and \(B\Delta_1(T)\), axiomatized by \(I\Delta_0\), and the collection axioms for all \(\Delta_1(T)\) formulas. It is shown that all three axiom systems can be characterized in terms of the classical schemes combined with suitable inference rules. For example, for each sentence \(\varphi\), \(I\Delta_1(T)\) proves \(\varphi\) if and only if \(\varphi\) is provable in \(I\Sigma_1\) and it is in the closure of \(\mathrm{Th}_{\Pi_2(T)}\) under non-nested applications of the induction rule for \(\Delta_1\) formulas and first-order logic. Several applications are explored. In particular, it is shown that \(I\Delta_1(T)\) and \(L\Delta_1(T)\) are equivalent for every \(T\) extending \(I\Delta_0+\exp\). In the study of parameter-free versions of \(\Delta_1(T)\)-schemes, the authors introduce corresponding parameter-free inference rules, and prove some conservativity results for \(\Sigma_2\) sentences. Among other results, there is a characterization of computable functions which are provably total in \(I\Delta_1(T)\), and those which are provably total in \(L\Delta_1(T)\), in terms of some subrecursive operators; and a reduction of the problem of \textit{A. Wilkie} and \textit{J. Paris} [Stud. Logic Found. Math. 126, 143--161 (1989; Zbl 0695.03019)] whether \(I\Delta_0+\lnot\exp\) implies \(B\Sigma_1\) to a purely recursion-theoretic question.