On the finite axiomatizability of ?∑_1~b(R_2~1)

摘要

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_2~1, is equal to S_2~1. We give new dependent choice-based axiomatizations of the ?∑_1~b-consequences of S_2~1 and R_2~1. Our dependent choice axiomatizations give new normal forms for the ?_1~b- consequences of S_2~1 and R_2~1.We use these axiomatizations to give an alternative proof of the finite axiomatizability of ?∑_1~b (S_2~1) and to show new results such as ?∑_1~b (R_3~1) is finitely axiomatized and that there is a finitely axiomatized theory, TUC, containing S_2~0 and contained in R_2~1. On the other hand, we show that our theory for ?∑_1~b (R_2~1) splits into a natural infinite hierarchy of theories. We give a diagonalization result that stems from our attempts to separate the hierarchy for ?∑_1~b (R_2~1).