Name
Abstract | ||
|---|---|---|
We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's (Theoret. Comput. Sci. 101 (1992) 35) 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 S21 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 ∀Σ1b consequences of S21 is finitely axiomatizable as well, thus answering an open question. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S0168-0072(03)00056-3 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
03F35,68Q15,68Q19 | Polynomial hierarchy,Discrete mathematics,Bounded arithmetic,Algebra,Second-order logic,Predicate (grammar),Corollary,Mathematics | Journal |
Volume | Issue | ISSN |
124 | 1 | 0168-0072 |
Citations | PageRank | References |
9 | 0.76 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stephen Cook | 1 | 4864 | 2433.99 |
| Antonina Kolokolova | 2 | 50 | 10.09 |