The provably total NP search problems of weak second order bounded arithmetic

We define a new NP search problem, the “local improvement” principle, about labellings of an acyclic, bounded-degree graph. We show that, provably in PV , it characterizes the ∀ Σ 1 b consequences of V 2 1 and that natural restrictions of it characterize the ∀ Σ 1 b consequences of U 2 1 and of the bounded arithmetic hierarchy. We also show that over V 0 it characterizes the ∀ Σ 0 B consequences of V 1 and hence that, in some sense, a miniaturized version of the principle gives a new characterization of the ∀ Π 1 b consequences of S 2 1 . Throughout our search problems are “type-2” NP search problems, which take second-order objects as parameters.