Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem (Q647334)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem |
scientific article |
Statements
Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem (English)
0 references
23 November 2011
0 references
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.
0 references
bounded arithmetic
0 references
proof complexity
0 references
search problems
0 references
0 references
0 references