Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style


Phuong Nguyen

VTC^0: A Second-Order Theory For TC^0


Graduate Department of Computer Science
University of Toronto, 2004


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

    1. Introduction
    2. The Class FO-Uniform TC^0
    3. The Theory VTC^0
    4. RSUV Isomorphism between VTC^0 and \Delta^b_1-CR
    5. Conclusion

Number of pages: 58

ISSN 1433-8092 | Imprint