Exponentiation and second-order bounded arithmetic (Q922540)

The paper is devoted to the study of exponentiation in second-order bounded arithmetic \(V_ 2\) and \(V^ i_ 2\) [introduced by \textit{S. Buss} in ``Bounded arithmetic'' (1986; Zbl 0649.03042)]. It is proved that: (1) \(V^ i_ 2\vdash A(a)\) iff for some term t: \(S^ i_ 2\vdash ``2^{t(a)}\) exists \(\to\) A(a)'', A a bounded first-order formula, \(i\geq 1\), (2) \(V^ i_ 2\) (resp. \(V_ 2)\) is not \(\Pi^ b_ 1\)-conservative over \(S^ i_ 2\) (resp. over \(S_ 2)\), (3) any model of \(V_ 2\) not satisfying Exp satisfies the collection scheme \(B\Sigma^ 0_ 1\), (4) \(V^ 1_ 3\) is not \(\Pi^ b_ 1\)- conservative over \(S_ 2\).