We introduce a finitely axiomatizable second-order theory VTC^0, which is associated with the class FO-uniform TC^0. It consists of the base theory V^0 for AC^0 reasoning together with the axiom NUMONES, which states the existence of a "counting array" Y for any string X: the ith row of Y contains only the number of 1 bits up to (excluding) bit i of X. We introduce the notion of "strong \Delta _1^B-definability" for relationsd in a theory, and use a recursive characterization of the TC^0 relations (rather than functions) to show that the TC^0 relations are strongly \Delta _1^B-definable. It follows that the TC^0 functions are \sum _1^B-definable in VTC^0. We prove a general witnessing theorem for second-order theories and conclude that the \sum _1^B theorems of VTC^0 are witnessed by TC^0 functions. We prove that VTC^0 is RSUV isomorphic to the first order theory \Delta _1^b-CR of Johannsen and Pollett (the "minimal theory for TC^0"). \Delta _1^b-CR includes the \Delta _1^b comprehension rule, and J and P ask whether there is an upper bound to the nesting depth required for this rule. We answer "yes", because VTC^0, and therefore \Delta _1^b-CR, are finitely axiomatizable. Finally, we show that \sum _0^B theorems of VTC^0 translate to families of tautologies which have polynomial-size constant-depth TC^0-Frege proofs. We also show that PHP is a \sum _0^B theorem of VTC^0. These together imply that the family of propositional tautologies associated with PHP has polynomial-size constant-depth TC^0-Frege proofs.