Arnold Beckmann and Sam Buss
Journal of Mathematical Logic 2009, 9(1): 103-138
Publication year: 2009

The complexity class of Π^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 Σ^b_i – definable functions of T^k+1_2 are characterized in terms of Π^p_k – PLS problems. These Π^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 Π^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 ∀Σ^b_1(α) – principle that is conjectured to separate T^k_2(α) and T^k+1_2(α) .