A second-order system for polytime reasoning based on Grädel's theorem. (Q1412837)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A second-order system for polytime reasoning based on Grädel's theorem. |
scientific article |
Statements
A second-order system for polytime reasoning based on Grädel's theorem. (English)
0 references
25 November 2003
0 references
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.
0 references
Bounded arithmetic
0 references
Polynomial time
0 references
Second-order system
0 references
Descriptive complexity
0 references