TR01-024 Authors: Stephen Cook, Antonina Kolokolova

Publication: 15th March 2001 00:37

Downloads: 1967

Keywords:

We introduce a second-order system V_1-Horn of bounded arithmetic

formalizing polynomial-time reasoning, based on Graedel's

second-order Horn characterization of P. Our system has

comprehension over P predicates (defined by Graedel'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 S_2^1 or the second-order V_1^1), 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

V_1-Horn is finitely axiomatizable, and, as a corollary, that

the class of \forall\Sigma_1^b consequences of S^1_2 is finitely

axiomatizable as well, thus answering an open question.