Logic in Computer Science (LICS 2004)

Paper: VTC⁰: A Second-Order Theory for TC⁰ (at LICS 2004)

Authors: Phuong Nguyen Stephen Cook

Abstract

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.

BibTeX

  @InProceedings{NguyenCook-VTCASecondOrderTheo,
    author = 	 {Phuong Nguyen and Stephen Cook},
    title = 	 {VTC⁰: A Second-Order Theory for TC⁰},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {378--387},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }