A second-order system for polytime reasoning based on Grädel's theorem.
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.
scientific article; zbMATH DE number 2009287
scientific article