AbstractThe question of whether the bounded arithmetic theoriesandare equal is closely connected to the complexity question of whetheris equal to. In this paper, we examine the still open question of whether the prenex version of,, is equal to. We give new dependent choice‐based axiomatizations of the‐consequences ofand. Our dependent choice axiomatizations give new normal forms for the‐consequences ofand. We use these axiomatizations to give an alternative proof of the finite axiomatizability ofand to show new results such asis finitely axiomatized and that there is a finitely axiomatized theory,, containingand contained in. On the other hand, we show that our theory forsplits into a natural infinite hierarchy of theories. We give a diagonalization result that stems from our attempts to separate the hierarchy for.