On the finite axiomatizability of
Chris Pollett · Mathematical logic quarterly · 2018
Abstract The question of whether the bounded arithmetic theories and are equal is closely connected to the complexity question of whether is 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 of and . Our dependent choice axiomatizations give new normal forms for the ‐consequences of and . We use these axiomatizations to give an alternative proof of the finite axiomatizability of and to show new results such as is finitely axiomatized and that there is a finitely axiomatized theory, , containing and contained in . On the other hand, we show that our theory for splits into a natural infinite hierarchy of theories. We give a diagonalization result that stems from our attempts to separate the hierarchy for .