Annals of Pure and Applied Logic 124 (1-3):193-231 (2003)

We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's 35) second-order Horn characterization of P. Our system has comprehension over P predicates , and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates , and hence are more powerful than our system , or use Cobham's theorem to introduce function symbols for all polynomial-time functions . 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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(03)00056-3
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,909
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Bounded Arithmetic and the Polynomial Hierarchy.Jan Krajíček, Pavel Pudlák & Gaisi Takeuti - 1991 - Annals of Pure and Applied Logic 52 (1-2):143-153.
Notes on Polynomially Bounded Arithmetic.Domenico Zambella - 1996 - Journal of Symbolic Logic 61 (3):942-966.
Relating the Bounded Arithmetic and Polynomial Time Hierarchies.Samuel R. Buss - 1995 - Annals of Pure and Applied Logic 75 (1-2):67-77.

Add more references

Citations of this work BETA

On the Finite Axiomatizability of ∀Σ̂1b.Chris Pollett - 2018 - Mathematical Logic Quarterly 64 (1-2):6-24.

Add more citations

Similar books and articles

The Road to Two Theorems of Logic.William Craig - 2008 - Synthese 164 (3):333 - 339.
The Epistemic Basis of Defeasible Reasoning.Robert L. Causey - 1991 - Minds and Machines 1 (4):437-458.
Reverse Mathematics and Π21 Comprehension.Carl Mummert & Stephen G. Simpson - 2005 - Bulletin of Symbolic Logic 11 (4):526-533.
An Empirical Analysis of Modal Theorem Provers.Ullrich Hustadt & Renate A. Schmidt - 1999 - Journal of Applied Non-Classical Logics 9 (4):479-522.


Added to PP index

Total views
15 ( #643,414 of 2,402,091 )

Recent downloads (6 months)
1 ( #552,323 of 2,402,091 )

How can I increase my downloads?


My notes