__Preprint:__

**
Arnold Beckmann and Samuel R. Buss.
"Characterizing Definable Search Problems
in Bounded Arithmetic via Proof Notations"
In **

**
Download submitted version:
PDF.
**

**Abstract:**
The complexity class of $\pip k$-Polynomial Local Search (PLS) problems
with $\pip\ell$-goal is introduced,
and is used to give new characterisations of definable search problems
in fragments of Bounded Arithmetic.
The characterisations are established via notations for propositional proofs
obtained by translating Bounded Arithmetic proofs using
the Paris-Wilkie-translation.
For $\ell\le k$, the $\sib{\ell+1}$-definable search problems
of $\rT^{k+1}_2$ are exactly characterised by
$\pip k$-PLS problems with $\pip\ell$-goals.
These $\pip k$-PLS problems can be defined in a weak base theory such as
$\rS^1_2$, and proved to be total in $\rT^{k+1}_2$.
Furthermore, the $\pip k$-PLS definitions can be Skolemised with simple
polynomial time functions.
The Skolemised $\pip k$-PLS definitions give rise to a new
$\forall\sib1(\al)$ principle conjectured to separate
$\rT^{k}_2(\al)$ from $\rT^{k+1}_2(\al)$.