We investigate the possibility to characterize (multi) functions that are Σ_i~b-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 Σ_1~b- and Σ_2~b-definable in the theories S_2~1 and T_2~1. (2) New characterizations of (multi) functions that are Σ_2~b- and Σ_3~b-definable in the theory T_2~2. (3) A new non-conservation result: the theory T_2~2(α) is not ∨ Σ_1~b(α)-conservative over the theory S_2~2(α). To prove that the theory T_2~2(α) is not ∨ Σ_1~b(α)-conservative over the theory S_2~2(α), we present two examples of a Σ_1~b(α)-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, …, a}, R) can have increasing iterates.
展开▼
