Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem (Q647334)

In the paper a new characterization of the strict \(\forall \Sigma^{b}_{j}\)-sentences provable using \(\Sigma^{b}_{k}\)-induction for \(1 \leq j \leq k\) is given. As an application it is shown that in a certain sense Buss's witnessing theorem for strict \(\Sigma^{b}_{k}\)-formulas already holds over the relatively weak theory PV. A combinatorial principle is exhibited with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth-\(j\) Frege refutations form a strict hierarchy with \(j\), and hence that the relativized bounded arithmetic hierarchy can be separated by a family of \(\forall \Sigma^{b}_{1}\)-sentences.