It follows from Theorem 4.7 that \(f(\vec{x})\) is computable in polynomial time just in case it is provably total in \(\mathsf{S}^1_2\) relative to a \(\Sigma^b_1\)-definition. Buss (1986) also showed that \(\mathsf{S}^i_2 \subseteq \mathsf{T}^i_2 \subseteq \mathsf{S}^{i+1}_2\), that \(\mathsf{S}^i_2\) and \(\mathsf{T}^i_2\) are finitely axiomatizable, and that \(\mathsf{S}_2 = \mathsf{T}_2\). It is not known if either of the hierarchies of theories displayed above collapses or whether either \(\mathsf{S}_2\) or \(\mathsf{T}_2\) is finitely axiomatizable. However, either the existence of an \(i\) such that \(\mathsf{T}^i_2 = \mathsf{S}^{i+1}_2\) or the finite axiomatizability of \(\mathsf{S}_2\) or \(\mathsf{T}_2\) can be shown to entail the collapse of the Polynomial Hierarchy.