The counting hierarchy in binary notation

Abstract

We present a new recursion-theoretic characterization of $\mathsf{FCH}$, the hierarchy of counting functions, in binary notation. Afterwards we introduce a theory of bounded arithmetic, $\mathsf{TCA}$, that can be seen as a reformulation, in the binary setting, of Jan Johannsen and Chris Pollett's system ${\mathsf{D}}_2^0$. Using the previous inductive characterization of $\mathsf{FCH}$, we show that a strategy similar to the one applied to ${\mathsf{D}}_2^0$ can be used in order to characterize $\mathsf{FCH}$ as the class of functions provably total in $\mathsf{TCA}$.