Abstract

We study search problems and reducibilities between them with known or potential relevance to bounded arithmetic theories. Our primary objective is to understand the sets of low complexity consequences of theories Si2 and Ti2 for a small i, ideally in a rather strong sense of characterization; or, at least, in the standard sense of axiomatization. We also strive for maximum combinatorial simplicity of the characterizations and axiomatizations, eventually sufficient to prove conjectured separation results. To this end two techniques based on the Herbrand's theorem are developed. They characterize/axiomatize Σb1-consequences of Σb2-definable search problems, while the method based on the more involved concept of characterization is easier and gives more transparent results. This method yields new proofs of Buss' witnessing theorem and of the relation between PLS and Σb1, and also an axiomatization of Σb1