VTC0: A second-order theory for TC0.

Description

We introduce a finitely axiomatizable second-order theory VTC 0 and show that it characterizes precisely the class uniform TC0. It is simply the theory V0 [12] 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 upto (excluding) bit i of X. First, we introduce the notion of "strong DB1 -definability" for relations in a theory, and use the recursive properties of TC0 relations (rather than functions) to show that TC0 relations are strongly DB1 -definable, and TC0 functions are SB1 -definable in VTC0. Then, we generalize the Witnessing Theorem for V0 [12], and obtain the witnessing theorem for VTC0 from this general result: ∃SB0+ SB1 theorems of VTC0 can be witnessed by TC0 functions (here, SB0+S B1 formulas are those obtained from SB1 formulas using ∧,∨ and bounded number quantifications). Finally, we show that VTC0 is RSUV isomorphic to the first-order theory Db1 -CR, which has been claimed the "minimal" theory for TC0 [20]. This isomorphism shows that VTC0 admits the SB0+D B1 comprehension rule. Hence, in VTC0, strong DB1 -definability and the usual DB1 -definability coincide. It also follows that Db1 - CR = Db1 - CRi, for some i. This answers affirmatively an open question from [20].

Subjects

Links

• URL