VTCO: a second-order theory for TC0

We introduce a finitely axiomatizable second-order theory, which is VTC⁰ associated with the class FO-uniform TC⁰. It consists of the base theory V⁰ for AC⁰ 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 Δ₁^B-definability" for relations in a theory, and use a recursive characterization of the TC⁰ relations (rather than functions) to show that the TC⁰ relations are strongly Δ₁^B-definable. It follows that the TC⁰ functions are Σ₁^B-definable in VTC⁰. We prove a general witnessing theorem for second-order theories and conclude that theΣ₁^B theorems of VTC⁰ are witnessed by TC⁰ functions. We prove that VTC⁰ is RSUV isomorphic to the first order theory Δ₁^b-CR of Johannsen and Pollett (the "minimal theory for TC⁰"), Δ₁^b-CR includes the Δ₁^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⁰ , and therefore Δ₁^b-CR, are finitely axiomatizable. Finally, we show that Σ₁^B theorems of VTC⁰ translate to families of tautologies which have polynomial-size constant-depth TC⁰-Frege proofs. We also show that PHP is a Σ₀^B theorem of VTC⁰. These together imply that the family of propositional tautologies associated with PHP has polynomial-size constant-depth TC⁰-Frege proofs.