摘要 : We give a new characterization of the strict ?σ_b~j sentences provable using σ_k~b, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss's witnessing theorem for strict σkb formulas already holds over the r... 展开 We give a new characterization of the strict ?σ_b~j sentences provable using σ_k~b, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss's witnessing theorem for strict σkb formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle 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 ?σ_b~1 sentences. 收起