Logic in Computer Science (LICS 2001)

Paper: A Second-Order System for Polytime Reasoning Using Grädel's Theorem (at LICS 2001)

Authors: Stephen Cook Antonina Kolokolova

Abstract

We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's [15] second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Grädel's second-order Horn formulas), and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates (such as Buss's S12 or the second-order V11), and hence are more powerful than our system (assuming the polynomial hierarchy does not collapse), or use Cobham's theorem to introduce function symbols for all polynomial-time functions (such as Cook's PV and Zambella's P-def). We prove that our system is equivalent to QPV and Zambella's P-def. Using our techniques, we also show that V1-Horn is finitely axiomatizable, and, as a corollary, that the class of \forall\Sigma_1^b consequences of S12 is finitely axiomatizable as well, thus answering an open question.

BibTeX

  @InProceedings{CookKolokolova-ASecondOrderSystemf,
    author = 	 {Stephen Cook and Antonina Kolokolova},
    title = 	 {A Second-Order System for Polytime Reasoning Using Grädel's Theorem},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {Joseph Halpern},
    month =	 {June}, 
    pages =      {177--186},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }