The provably total search problems of bounded arithmetic†
- Institute of Mathematics
Academy of Sciences of the Czech Republic
Žitná 25
115 67 Prague 1
Czech Republic
- thapen{at}math.cas.cz
-
2000 Mathematics Subject Classification 03F30, 68Q15, 03F20.
-
The first author was supported in part by Eduard Čech Center grant LC505 and NSERC PDF-313650-2005.
-
The second author was supported in part by grant AV0Z10190503 and by Eduard Čech Center grant LC505.
-
↵† 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
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
conservativity of
over
already implies
conservativity of T2(α) over
. We translate this into propositional form and give a polylogarithmic width CNF
such that if
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
. We use our characterization to give a sufficient condition for the totality of a relativized NP search problem to be unprovable
in
in terms of a non-logical question about multiparty communication protocols.
- © 2011 London Mathematical Society






