Skip Navigation

The provably total search problems of bounded arithmetic

  1. Alan Skelley
  1. Google
    1600 Amphitheatre Parkway
    Mountain View
    CA 94043
    USA
    alanoman{at}google.com
  1. Neil Thapen
  1. Institute of Mathematics
    Academy of Sciences of the Czech Republic
    Žitná 25
    115 67 Prague 1
    Czech Republic
  1. thapen{at}math.cas.cz
  1. 2000 Mathematics Subject Classification 03F30, 68Q15, 03F20.

  2. The first author was supported in part by Eduard Čech Center grant LC505 and NSERC PDF-313650-2005.

  3. The second author was supported in part by grant AV0Z10190503 and by Eduard Čech Center grant LC505.

  4. This work was partly carried out while the first author was at the Institute of Mathematics of the Academy of Sciences of the Czech Republic in Prague and at the Dipartimento di Informatica of the Università degli Studi di Roma ‘La Sapienza’.

  • Received March 20, 2008.
  • Revision received March 2, 2010.

Abstract

We give combinatorial principles GIk, based on k-turn games, which are complete for the class of NP search problems provably total at the kth level Tk2 of the bounded arithmetic hierarchy and hence characterize the Graphic consequences of Tk2. Our argument uses a translation of first-order proofs into large, uniform propositional proofs in a system in which the soundness of the rules can be witnessed by polynomial time reductions between games. We show that Graphic conservativity of Graphic over Graphic already implies Graphic conservativity of T2(α) over Graphic. We translate this into propositional form and give a polylogarithmic width CNF Graphic such that if Graphic has small R(log) refutations then so does any polylogarithmic width CNF which has small constant depth refutations. We prove a resolution lower bound for Graphic. We use our characterization to give a sufficient condition for the totality of a relativized NP search problem to be unprovable in Graphic in terms of a non-logical question about multiparty communication protocols.

This Article

  1. Proc. London Math. Soc. doi: 10.1112/plms/pdq044
  1. All Versions of this Article:
    1. pdq044v1
    2. 103/1/106 most recent

Classifications

Share

  1. Email this article

Published on behalf of

LMS logo

Impact Factor: 1.079

5-Yr impact factor: 1.246

Editors

Radha Kessar
Michael Singer

LMS journals now available in full MathJax HTML.

MathJax is an open-source JavaScript display engine that produces high-quality mathematics in all modern browsers.

To learn more about MathJax, please visit their site at www.MathJax.org.

Powered by MathJax

For Authors

Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.