We prove that any proof of a [Formula: see text] sentence in the theory [Formula: see text] can be translated into a proof in [Formula: see text] at the cost of a polynomial increase in size. In fact, the proof in [Formula: see text] can be obtained by a polynomial-time algorithm. On the other hand, [Formula: see text] has nonelementary speedup over the weaker base theory [Formula: see text] for proofs of [Formula: see text] sentences. We also show that for (...) [Formula: see text], proofs of [Formula: see text] sentences in [Formula: see text] can be translated into proofs in [Formula: see text] at a polynomial cost in size. Moreover, the [Formula: see text]-conservativity of [Formula: see text] over [Formula: see text] can be proved in [Formula: see text], a fragment of bounded arithmetic corresponding to polynomial-time computation. For [Formula: see text], this answers a question of Clote, Hájek and Paris. (shrink)

Let$\left\langle {{W_n}:n \in \omega } \right\rangle$be a canonical enumeration of recursively enumerable sets, and supposeTis a recursively enumerable extension of PA (Peano Arithmetic) in the same language. Woodin (2011) showed that there exists an index$e \in \omega$(that depends onT) with the property that if${\cal M}$is a countable model ofTand for some${\cal M}$-finite sets,${\cal M}$satisfies${W_e} \subseteq s$, then${\cal M}$has an end extension${\cal N}$that satisfiesT+We=s.Here we generalize Woodin’s theorem to all recursively enumerable extensionsTof the fragment${{\rm{I}\rm{\Sigma }}_1}$of PA, and remove the countability restriction (...) on${\cal M}$whenTextends PA. We also derive model-theoretic consequences of a classic fixed-point construction of Kripke (1962) and compare them with Woodin’s theorem. (shrink)