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
    0 references
    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

    Identifiers