Premium
Herbrandizing search problems in Bounded Arithmetic
Author(s) -
Hanika Jiří
Publication year - 2004
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200410005
Subject(s) - mathematics , mathematical proof , bounded function , characterization (materials science) , simplicity , relation (database) , relevance (law) , discrete mathematics , arithmetic , algebra over a field , computer science , pure mathematics , data mining , epistemology , mathematical analysis , philosophy , materials science , geometry , political science , law , nanotechnology
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 1 or Σ b 2 ) of theories S i 2 and T i 2 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 1 ‐consequences of Σ b 2 ‐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 1 ( T 1 2 ), and also an axiomatization of Σ b 1 ( T 2 2 ). (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)