Herbrandizing search problems in Bounded Arithmetic

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 (esp. Σ^b₁ or Σ^b₂) of theories Sⁱ₂ and Tⁱ₂ 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 Σ^b₁‐consequences of Σ^b₂‐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 Σ^b₁(T¹₂), and also an axiomatization of Σ^b₁(T²₂). (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)