Conservative fragments of \({{S}^{1}_{2}}\) and \({{R}^{1}_{2}}\) (Q535152)

The paper studies weak fragments of Buss's theories of bounded arithmetic. One of the main problems in the area is to separate levels of Buss's hierarchy. While the general problem is considered very difficult due to its connection to major unsolved questions in computational complexity theory (collapse of the polynomial hierarchy), there is some hope that we might be able to directly separate theories at the lower end of the hierarchy. The author is particularly interested in the question whether \(R^1_2\neq S^1_2\), and to this end he investigates low-complexity fragments (such as \(\Sigma^b_0\), \(\hat\Sigma^b_1\)) of \(R^1_2\), \(S^1_2\), and related theories. The paper defines theories \(T^{-1,\tau}_2\) characterizing the \(\forall\Sigma^b_0\) consequences of \(T^{0,\tau}_2\) (= \(\Sigma^b_0\)-induction for numbers bounded by a term from \(\tau\)); in particular, \(T^{-1}_2\) is the \(\forall\Sigma^b_0\) fragment of \(T^0_2\) and \(S^1_2\). Then the author presents function algebras \(\mathcal A\Sigma^\tau_\infty\) and proves a witnessing theorem for a certain class of theories (including \(T^{-1,\tau}_2\)) with respect to these algebras. As a special case, this gives a description of \(\Sigma^b_0\)-definable functions of \(T^{-1}_2\); the relevant algebra is then shown not to contain division by \(3\), which implies \(T^{-1}_2\neq T^0_2\), and, by a similar argument, \(R^1_2\) is not \(\forall\hat\Sigma^b_1\)-conservative over \(T^{0,\tau}_2\) for suitable \(\tau\). In the next section, the author introduces theories \(\text{TComp}^\tau\) based on open comprehension axioms allowing for a controlled amount of recursive dependence in the defining formulas. The main result is a witnessing theorem which implies, among others, that \(R^1_2\) is \(\forall\hat\Sigma^b_1\)-conservative over \(\text{TComp}^{\{||\text{id}||\}}\), \(\hat C^0_2\) is \(\forall\hat\Sigma^b_1\)-conservative over \(\text{TComp}^{\{\text{cl}\}}\), and \(T^0_2\) can be axiomatized by induction for sharply bounded \(\exists\forall\)-formulas.