Article:

Arnold Beckmann and Samuel R. Buss.
"Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic."
Journal of Mathematical Logic 9, 1 (2009) 103-138.

Abstract:  The complexity class of $Pi^p_k$-polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1≤i≤k+1, the $Sigma^p_i$-definable functions of $T^{k+1}_2$ are characterized in terms of $\Pi^p_k$-PLS problems. These $\Pi^p_k$-PLS problems can be defined in a weak base theory such as $S^1_2$, and proved to be total in $T^{k+1}_2$. Furthermore, the $\Pi^p_k$-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new $\forall \Sigma^b_1(\alpha)$-principle that is conjectured to separate $T^k_2(\alpha)$ and $T^{k+1}_2(\alpha)$.

Talk slides:

Arnold Beckmann and Samuel R. Buss.
"Polynomial Local Search higher in the Polynomial Hierarchy and Bounded Arithmetic".
June 7, 2009
Research Workshop on Proof Theory and Constructivity
Leeds, England.

"Polynomial Local Search higher in the Polynomial Hierarchy and Bounded Arithmetic".
December 11, 2008.
BIRS Workshop on Computability, Reverse Mathematics and Combinatorics