Witnessing functions in bounded arithmetic and search problems
Mario Chiari, Jan Krajı́ček · Journal of Symbolic Logic · 1998
Abstract We investigate the possibility to characterize (multi)functions that are -definable with smalli(i= 1, 2, 3) in fragments of bounded arithmeticT2in 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 and -definable in the theories and . (2) New characterizations of (multi)functions that are and -definable in the theory . (3) A new non-conservation result: the theory is not -conservative over the theory . To prove that the theory is not -conservative over the theory , we present two examples of a -principle separating the two theories: (a) the weak pigeonhole principle WPHP(a2,f, g) formalizing that no functionfis a bijection betweena2andawith the inverseg, (b) the iteration principle Iter(a, R, f) formalizing that no functionfdefined on a strict partial order ({0,…, a},R) can have increasing iterates.