On the finite axiomatizability of ∀(Σ)over-cap1b((R)over-cap21)

The question of whether the bounded arithmetic theories S-2(1) and R-2(1) are equal is closely connected to the complexity question of whether P is equal to NC. In this paper, we examine the still open question of whether the prenex version of R-2(1), (R) over cap (1)(2), is equal to S-2(1). We give new dependent choice- based axiomatizations of the. for all(Sigma) over cap (b)(1)- consequences of S-2(1) and (R) over cap (1)(2). Our dependent choice axiomatizations give new normal forms for the for all(Sigma) over cap (b)(1) consequences of S-2(1) and (R) over cap (1)(2). We use these axiomatizations to give an alternative proof of the finite axiomatizability of. for all(Sigma) over cap (b)(1)( S12) and to show new results such as. for all(Sigma) over cap (b)(1)((R) over cap (1)(3)) is finitely axiomatized and that there is a finitely axiomatized theory, TUC, containing (S) over cap (0)(2) and contained in (R) over cap (1)(2). On the other hand, we show that our theory for. for all(Sigma) over cap (b)(1)((R) over cap (1)(2)) splits into a natural infinite hierarchy of theories. We give a diagonalization result that stems from our attempts to separate the hierarchy for. for all(Sigma) over cap (b)(1) ((R) over cap (1)(2)). (C)2018 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.