A second-order system for polytime reasoning using Gradel´s theorem

We introduce a second-order system V₁-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Gradel´s (1992) second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Gradel´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 (1986) S₂¹ or the second-order V₁ ¹), 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 (1996) P-def. Using our techniques, we also show that V₁-Horn is finitely, axiomatizable, and, as a corollary, that the class of ∀Σ₁^b consequences of S₂¹ is finitely axiomatizable as well, thus answering an open question