Abstract
We introduce a finitely axiomatizable second-order theory VTC^0 and show that it characterizes precisely the class uniform TC^0. It is simply the theory V^0 together with the axiom NUMONES, which states the existence of a ``counting array'' Y for any string X: the i-th row of Y contains only the number of 1 bits upto (excluding) bit i of X. First, we introduce the notion of ``strong \Delta_1^B-definability'' for relations in a theory, and use the recursive properties of TC^0 relations (rather than functions) to show that TC^0 relations are strongly \Delta_1^B-definable, and TC^0 functions are \Sigma_1^B-definable in VTC^0. Then, we generalize the Witnessing Theorem for V^0 and obtain the witnessing theorem for VTC^0 from this general result: \exists\Sigma_{0^+}^B(\Sigma_1^B) theorems of VTC^0 can be witnessed by TC^0 functions (here, \Sigma_{0^+}^B(\Sigma_1^B) formulas are those obtained from \Sigma_1^B formulas using \wedge, \vee and bounded number quantifications). Finally, we show that VTC^0 is RSUV isomorphic to the first-order theory \Delta-CR, which has been claimed the ``minimal'' theory for TC^0 by Johannsen and Pollett. This isomorphism shows that VTC^0 admits the \Sigma_{0^+}^B(\Delta_1^B) comprehension rule. Hence, in VTC^0, strong \Delta_1^B-definability and the usual \Delta_1^B-definability coincide. It also follows that \Delta-CR = \Delta-CR_i for some i. This answers affirmatively an open question by Johannsen and Pollett.
Table of Contents
