Journal article:

Samuel R. Buss and Jan Krajicek.
"An application of Boolean complexity to separation problems in bounded arithmetic."
Proceedings of the London Mathematical Society 69 (1994) 1-21.

Abstract: We develop a method for establishing the independence of some $\Sigma^b_i(\alpha)$-formulas from $S^i_2(\alpha)$. In particular, we show that $T^i_2(\alpha)$ is not $\forall\Sigma^b_i(\alpha)$-conservative over $S^i_2(\alpha)$.
We characterize the $\Sigma^b_1$-definable functions of~$T^1_2$ as being precisely the functions definable as projections of polynomial local search (PLS) problems.