Witnessing Functions in Bounded Arithmetic and Search Problems
Chiari, Mario ; Krajicek, Jan
J. Symbolic Logic, Tome 63 (1998) no. 1, p. 1095-1115 / Harvested from Project Euclid
We investigate the possibility to characterize (multi) functions that are $\Sigma^b_i$-definable with small i (i = 1, 2, 3) in fragments of bounded arithmetic T$_2$ in terms of natural search problems defined over polynomial-time structures. We obtain the following results: (1) A reformulation of known characterizations of (multi)functions that are $\Sigma^b_1$- and $\Sigma^b_2$-definable in the theories S$^1_2$ and T$^1_2$. (2) New characterizations of (multi)functions that are $\Sigma^b_2$- and $\Sigma^b_3$-definable in the theory T$^2_2$. (3) A new non-conservation result: the theory T$^2_2 (\alpha)$ is not $\forall\Sigma^b_1 (\alpha)$-conservative over the theory S$^2_2 (\alpha)$. To prove that the theory T$^2_2 (\alpha)$ is not $\forall\Sigma^b_1 (\alpha)$-conservative over the theory S$^2_2 (\alpha)$, we present two examples of a $\Sigma^b_1 (\alpha)$-principle separating the two theories: (a) the weak pigeonhole principle WPHP (a$^2$, f, g) formalizing that no function f is a bijection between a$^2$ and a with the inverse g, (b) the iteration principle Iter (a, R, f) formalizing that no function f defined on a strict partial order ($\{0,\dots,a\}$, R) can have increasing iterates.
Publié le : 1998-09-14
Classification: 
@article{1183745583,
     author = {Chiari, Mario and Krajicek, Jan},
     title = {Witnessing Functions in Bounded Arithmetic and Search Problems},
     journal = {J. Symbolic Logic},
     volume = {63},
     number = {1},
     year = {1998},
     pages = { 1095-1115},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745583}
}
Chiari, Mario; Krajicek, Jan. Witnessing Functions in Bounded Arithmetic and Search Problems. J. Symbolic Logic, Tome 63 (1998) no. 1, pp.  1095-1115. http://gdmltest.u-ga.fr/item/1183745583/