A second-order system for polytime reasoning based on Grädel's theorem. (Q1412837)

The authors introduce a second-order system, \(V_{1}\)-Horn, of bounded arithmetic formalizing polynomial-time reasoning based on Grädel's second-order Horn characterization of P. It is proved that this system is equivalent to QPV and Zambella's P-def. It is also shown that \(V_{1}\)-Horn is finitely axiomatizable and that the class of \(\forall \Sigma^{b}_{1}\) consequences of \(S^{1}_{2}\) is finitely axiomatizable as well. This answers an open question.