We present a new recursion-theoretic characterization of FCH, the hierarchy of counting functions, in binary notation. Afterwards we introduce a theory of bounded arithmetic, TCA, that can be seen as a reformulation, in the binary setting, of Jan Johannsen and Chris Pollett's system D02. Using the previous inductive characterization of FCH, we show that a strategy similar to the one applied to D02 can be used in order to characterize FCH as the class of functions provably total in TCA.
Cite this article
Gilda Ferreira, The counting hierarchy in binary notation. Port. Math. 66 (2009), no. 1, pp. 81–94DOI 10.4171/PM/1832