Buss (1986) proved that the provably total functions of S^i_2 correspond to the functions computable at the i-th level of the polynomial hierarchy

We define the class \(\mathcal{F}\) of functions definable by limited recursion on notation to be the least class containing \(\mathcal{F}_0\) and closed under composition and the foregoing scheme. 4 (Cobham 1965; Rose 1984) \(f(\vec{x}) \in \textbf{FP}\) if and only if \(f(\vec{x}) \in \mathcal{F}\). 4 is significant because it provides another machine-independent characterization of an important complexity class. Recall, however, that Cobham was working at a time when the mathematical status