A second-order system for polytime reasoning based on Grädelʹs theorem Original Research Article

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.