On theories of bounded arithmetic for \(\mathrm{NC}^1\) (Q638497)

In the paper two theories are introduced: \(\mathrm{VNC}_{*}^{1}\) and its variant \(\overline{\mathrm{VNC}}_{*}^{1}\) -- they correspond to a subclass of \(\mathrm{NC}^{1}\) slightly larger than uniform \(\mathrm{NC}^{1}\). The author works with second-order theories in the spirit of Zambella. The theory \(\mathrm{VNC}_{*}^{1}\) is formulated in the usual language of second-order bounded arithmetic and the theory \(\overline{\mathrm{VNC}}_{*}^{1}\) has a richer language. Basic properties of those theories are proved. A general theorem on conservativity of the axiom of choice over theories meeting certain requirements is also proved. It is shown that propositional translations of \(\Sigma^{B}_{0}\) theorems of \(\overline{\mathrm{VNC}}_{*}^{1}\) have \(L\)-uniform polynomial-size Frege proofs.