A Small Reflection Principle for Bounded Arithmetic
Verbrugge, Rineke ; Visser, Albert
J. Symbolic Logic, Tome 59 (1994) no. 1, p. 785-812 / Harvested from Project Euclid
We investigate the theory $I\Delta_0 + \Omega_1$ and strengthen [Bu86. Theorem 8.6] to the following: if $\mathrm{NP} \neq \mathrm{co-NP}$. then $\Sigma$-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. We prove that for all sentences $\varphi$ $I\Delta_0 + \Omega_1 \vdash \forall x \operatorname{Prov}(\ulcorner \forall y \leq \bar{x} (\operatorname{Prf} (y. \overline{\ulcorner \varphi \urcorner}) \rightarrow \varphi)\urcorner).$ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlak 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 $\Sigma$-completeness for witness comparison formulas.
Publié le : 1994-09-14
Classification: 
@article{1183744548,
     author = {Verbrugge, Rineke and Visser, Albert},
     title = {A Small Reflection Principle for Bounded Arithmetic},
     journal = {J. Symbolic Logic},
     volume = {59},
     number = {1},
     year = {1994},
     pages = { 785-812},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744548}
}
Verbrugge, Rineke; Visser, Albert. A Small Reflection Principle for Bounded Arithmetic. J. Symbolic Logic, Tome 59 (1994) no. 1, pp.  785-812. http://gdmltest.u-ga.fr/item/1183744548/