Logic Colloquium 2008

Neil ThapenThe provably total search problems of bounded arithmeticInstitute of Mathematics, Academy of Sciences of the Czech Republic, Žitná 25, 115 67 Prague 1, Czech Republic thapen@math.cas.cz

We give natural combinatorial principles \mathrm{GI}_{k}, based on sequences of k-turn games, which are complete for the class of NP search problems provably total at the kth level T^{k}_{2} of the bounded arithmetic hierarchy and hence characterize the \forall\Sigma^{b}_{1} consequences of T^{k}_{2}. 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.