A small reflection principle for bounded arithmetic
Rineke Verbrugge, Albert Visser · Journal of Symbolic Logic · 1994
Abstract We investigate the theory IΔ0+Ω1 and strengthen [Bu86, Theorem 8.6] to the following: if NP ≠ co-NP, then Σ-completeness for witness comparison foumulas is not provable in bounded arithmetic. i.e., Next we study a “small reflection principle” in bounded arithmetic. We prove that for all sentences φ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlák in [Pu86]. Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas.