NP search problems in low fragments of bounded arithmetic. (English) Zbl 1118.03051

The paper studies \(\forall\Sigma^b_1\)-consequences (i.e., definable NP search problems) of some fragments of bounded arithmetic. The known characterizations of \(\Sigma^b_1(T^i_2)\) for \(i\geq2\) in terms of reflection principles, or Herbrandization of induction axioms, are rather artificial and lack a direct combinatorial appeal useful for separation of the theories and other applications. The authors provide several combinatorial descriptions of the NP search problems definable in \(T^2_2\) and \(T^3_2\). Specifically, \(\Sigma^b_1(T^2_2)\) is characterized by a generalization of polynomial local search problems (PLS) called coloured PLS, a reflection principle for exponentially long resolution proofs in a succinct representation, or a statement of totality of so-called verifiable recursion (VR) programs. \(\Sigma^b_1(T^3_2)\) is similarly characterized by a reflection principle for the \(\roman{PK}_1=R(n)\) proof system, or a variant of the VR-totality problem.


03F30 First-order arithmetic and fragments
03F20 Complexity of proofs
Full Text: DOI


[1] Journal of Computer and System Sciences 48 pp 498–532– (1994)
[2] Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 36 pp 29–46– (1990)
[3] Proceedings of the 31st IEEE symposium on Foundations of Computer Science II pp 794–801– (1990)
[4] Mathematical Logic Quarterly 50 pp 577–586– (2004)
[5] Annals of Pure and Applied Logic 75 pp 79–88– (1995)
[6] Conference record of seventh annual ACM symposium on theory of computing pp 83–97– (1975)
[7] Archive for Mathematical Logic 38 pp 123–138– (1999)
[8] Witnessing functions in bounded arithmetic and search problems 63 pp 1095–1115– (1998)
[9] Proceedings of the London Mathematical Society 69 pp 1–21– (1994)
[10] Bounded arithmetic (1986)
[11] Journal of Computer and System Sciences 57 pp 3–19– (1998)
[12] Journal of Computer and System Sciences 64 pp 843–872– (2002) · Zbl 1051.03049
[13] Annals of Mathematics and Artificial Intelligence 6 pp 107–126– (1992)
[14] Random Structures and Algorithms 7 pp 15–39– (1995)
[15] Fundamenta Mathematicae 170 pp 123–140– (2001)
[16] Lower bounds to the size of constant-depth propositional proofs 59 pp 73–86– (1994) · Zbl 0798.03056
[17] Journal of Computer and System Sciences 37 pp 79–100– (1988)
[18] Mathematical Logic Quaterly 48 pp 375–377– (2002)
[19] Proceedings of Computer Science Logic 553 pp 308–312– (1992)
[20] Computational Complexity 3 pp 97–308– (1993)
[21] Provability of the pigeonhole principle and the existence of infinitely many primes 53 pp 1235–1244– (1988)
[22] DOI: 10.1007/BFb0075316
[23] 20th annual ACM symposium on the Theory of Computing pp 229–234– (1988)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.