ECCC-Report TR01-024https://eccc.weizmann.ac.il/report/2001/024Comments and Revisions published for TR01-024en-usThu, 15 Mar 2001 00:37:24 +0200
Paper TR01-024
| A second-order system for polynomial-time reasoning based on Graedel's theorem |
Stephen Cook,
Antonina Kolokolova
https://eccc.weizmann.ac.il/report/2001/024We 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.
Thu, 15 Mar 2001 00:37:24 +0200https://eccc.weizmann.ac.il/report/2001/024