We show that Shoenfield's functional interpretation of Peano arithmetic can be factorized as a negative translation due to J. L. Krivine followed by Gödel's Dialectica interpretation. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).

We show how to extract effective bounds Φ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$ -sentences which depend on u only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$ ) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} (γ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ (...) ≤ 2, (*) can be weakened to $\bigwedge x^\delta, z^\tau\bigvee y \leq_\rho sx \bigwedge \tilde{z} \leq_\tau z F_0$ . This is used to establish new conservation results about weak König's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers. (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical assumptions (...) x εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)

We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] . This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied to fixed (...) sequences in Πi ∈ℕ[–ki, ki]. (shrink)

A pointwise version of the Howard-Bezem notion of hereditary majorization is introduced which has various advantages, and its relation to the usual notion of majorization is discussed. This pointwise majorization of primitive recursive functionals (in the sense of Gödel'sT as well as Kleene/Feferman's ) is applied to systems of intuitionistic and classical arithmetic (H andH c) in all finite types with full induction as well as to the corresponding systems with restricted inductionĤ↾ andĤ↾c.H and Ĥ↾ are closed under a generalized (...) fan-rule. For a restricted class of formulae this also holds forH c andĤ↾c.We give a new and very perspicuous proof that for each one can construct a functional such that $\tilde \Phi \alpha $ is a modulus of uniform continuity for Φ on {β1∣∧n(βn≦αn)}. Such a modulus can also be obtained by majorizing any modulus of pointwise continuity for Φ.The type structure ℳ of all pointwise majorizable set-theoretical functionals of finite type is used to give a short proof that quantifier-free “choice” with uniqueness (AC!)1,0-qf. is not provable within classical arithmetic in all finite types plus comprehension [given by the schema (C)ϱ:∨y 0ϱ∧x ϱ(yx=0⇔A(x)) for arbitraryA], dependent ω-choice and bounded choice. Furthermore ℳ separates several μ-operators. (shrink)

In this note we show that over a strong intuitionistic base theory, the recursive comprehension principle \ -CA does not imply the disjunctive Markov principle MP\.

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. (...) Cheney's proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to determine precisely the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems ${\cal T}^{\omega} :={\rm G}_n{\rm A}^{\omega} +{\rm AC}$ -qf $+\Delta$ , where (G $_n$ A $^{\omega})_{n \in {\Bbb N}}$ is a hierarchy of (weak) subsystems (...) of arithmetic in all finite types (introduced in [14]), AC-qf is the schema of quantifier-free choice in all types and $\Delta$ is a set of certain analytical principles which e.g. includes the binary König's lemma. We apply this method to show that the arithmetical closures of single instances of $\Pi^0_1$ -comprehension and -choice contribute to the growth of extractable bounds from proofs relative to ${\cal T}^\omega$ only by a primitive recursive functional in the sense of Kleene. In subsequent papers these results are widely generalized and the method is used to determine the arithmetical content of single sequences of instances of the Bolzano-Weierstraß principle for bounded sequences in ${\Bbb R}^d$ , the Ascoli-lemma and others. (shrink)

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do (...) not carry out the no-counterexample interpretation as a local proof interpretation and don't respect the modus ponens on the level of the no-counterexample interpretation of formulas A and A → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and--at least not constructively-- (γ) which are part of the definition of an 'interpretation of a formal system' as formulated in [15]. In this paper we determine the complexity of the no-counterexample interpretation of the modus ponens rule for (i) PA-provable sentences, (ii) for arbitrary sentences A, B ∈ L(PA) uniformly in functionals satisfying the no-counterexample interpretation of (prenex normal forms of) A and A → B, and (iii) for arbitrary A, B ∈ L(PA) pointwise in given α( 0 ) -recursive functionals satisfying the no-counterexample interpretation of A and A → B. This yields in particular perspicuous proofs of new uniform versions of the conditions (γ), (δ). Finally we discuss a variant of the concept of an interpretation presented in [17] and show that it is incomparable with the concept studied in [15], [16]. In particular we show that the no-counterexample interpretation of PA n by α( n (ω))-recursive functionals (n ≥ 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (δ). (shrink)

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a (...) uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theoremA(Aprenex) of first-order Peano arithmeticPAone can find ordinal recursive functionalsof order type < ε0which realize the Herbrand normal formAHofA.Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as alocalproof interpretation and don't respect the (...) modus ponens on the level of the nocounterexample interpretation of formulasAandA → B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (δ) and—at least not constructively—(γ) which are part of the definition of an ‘interpretation of a formal system’ as formulated in [15]. (shrink)

It is well known by now that large parts of mathematical reasoning can be carried out in systems which are conservative over primitive recursive arithmetic PRA . On the other hand there are principles S of elementary analysis which are known to be equivalent to arithmetical comprehension and therefore go far beyond the strength of PRA . In this paper we determine precisely the arithmetical and computational strength of weaker function parameter-free schematic versions S− of S, thereby exhibiting different levels (...) of strength between these principles as well as a sharp borderline between fragments of analysis which are still conservative over PRA and extensions which just go beyond the strength of PRA. (shrink)

In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel"s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for Π0 1-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.

LetA H be the Herbrand normal form ofA andA H,D a Herbrand realization ofA H. We showThere is an example of an (open) theory ℐ+ with function parameters such that for someA not containing function parameters Similar for first order theories ℐ+ if the index functions used in definingA H are permitted to occur in instances of non-logical axiom schemata of ℐ, i.e. for suitable ℐ,A In fact, in (1) we can take for ℐ+ the fragment (Σ 1 0 -IA)+ (...) of second order arithmetic with induction restricted toΣ 1 0 -formulas, and in (2) we can take for ℐ the fragment (Σ 1 0,b -IA) of first order arithmetic with induction restricted to formulas VxA(x) whereA contains only bounded quantifiers.On the other hand, $$PA^2 \vdash A^H \Rightarrow PA \vdash A,$$ wherePA 2 is the extension of first order arithmeticPA obtained by adding quantifiers for functions andA∈ℒ(PA). This generalizes to extensional arithmetic in the language of all finite types but not to sentencesA with positively occurring existential quantifiers for functions. (shrink)

This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...) . In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. (shrink)

The 2007 proceedings from the Annual European Meeting of the Association for Symbolic Logic.

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic in a finite types together with various forms of the axiom of choice and a numerical omniscience schema which implies classical logic for arithmetical formulas. Feferman subsequently observed that the proof theoretic strength of such systems can be determined by functional interpretation based on a non-constructive μ-operator and his well-known results on the strength of this operator from the 70's. In this note we consider a weaker form LNOS of NOS which (...) suffices to derive the strong form of binary König's lemma studied by Coquand/Palmgren and gives rise to a new and mathematically strong semi-classical system which, nevertheless, can proof theoretically be reduced to primitive recursive arithmetic PRA. The proof of this fact relies on functional interpretation and a majorization technique developed in a previous paper. (shrink)

In this paper the numerical strength of fragments of arithmetical comprehension, choice and general uniform boundedness is studied systematically. These principles are investigated relative to base systems Tnω in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive functions of low growth. We reduce the use of instances of these principles in Tnω-proofs of a large class of formulas to the use of instances of certain arithmetical principles thereby determining faithfully the arithmetical (...) content of the former. This is achieved using the method of elimination of Skolem functions for monotone formulas which was introduced by the author in a previous paper.As corollaries we obtain new conservation results for fragments of analysis over fragments of arithmetic which strengthen known purely first-order conservation results.We also characterize the provably recursive functions of type 2 of the extensions of Tnω based on these fragments of arithmetical comprehension, choice and uniform boundedness. (shrink)

Abstract.Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in the extended language, (...) the terms are ordinary PL-terms. In contrast to approaches to Herbrand’s theorem based on cut elimination orɛ-elimination this extraction technique is, except for the normalization step, of low polynomial complexity, fully modular and furthermore allows an analysis of the structure of the Herbrand terms, in the spirit of Kreisel ([13]), already prior to the normalization step. It is expected that the implementation of functional interpretation in Schwichtenberg’s MINLOG system can be adapted to yield an efficient Herbrand-term extraction tool. (shrink)

In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems (...) which allow one to prove similar uniformities even for unbounded spaces as long as certain local boundedness conditions are satisfied. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proof. Finally, we illustrate our main metatheorem by an example from metric fixed point theory. (shrink)

Goodman's theorem states that intuitionistic arithmetic in all finite types plus full choice, HA + AC, is conservative over first-order intuitionistic arithmetic HA. We show that this result does not extend to various subsystems of HA, HA with restricted induction.

It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule ofΠ 2 0 -inductionΠ 2 0 -IR isΠ 2 0 -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC 0,0-qf. More precisely we show that ℐ :=PRA 2 +Π 2 0 -IR+AC 0,0-qf proves the totality of the Ackermann function, wherePRA 2 is the extension ofPRA by number (...) and function quantifiers andΠ 2 0 -IR may contain function parameters.This is true even forPRA 2 +∑ 1 0 -IR+Π 2 0 -IR −+AC 0,0-qf, whereΠ 2 0 -IR − is the restriction ofΠ 2 0 -IR without function parameters. (shrink)

In 2007. Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP₁. That turned out to not be the proper formulation and so we proposed an alternative version FIPP₂. Tao himself formulated yet another version FIPP₃ in a revised version of his essay. We give (...) a counterexample to FIPP₁ and discuss for both of the versions FIPP₂ and FIPP₃ the faithfulness of their respective finitization of IPP by studying the equivalences IPP ↔ FIPP₂ and IPP ↔ FIPP₃ in the context of reverse mathematics ([9]). In the process of doing this we also introduce a continuous uniform boundedness principle CUB as a formalization of Tao's notion of a correspondence principle and study the strength of this principle and various restrictions thereof in terms of reverse mathematics, i.e., in terms of the "big five" subsystems of second order arithmetic. (shrink)

We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds while using the conceptual benefit of having precise realizers at the same time without having to construct them.

It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule ofΠ 2 0 -inductionΠ 2 0 -IR isΠ 2 0 -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC 0,0-qf. More precisely we show that ℐ :=PRA 2 +Π 2 0 -IR+AC 0,0-qf proves the totality of the Ackermann function, wherePRA 2 is the extension ofPRA by number (...) and function quantifiers andΠ 2 0 -IR may contain function parameters. This is true even forPRA 2 +∑ 1 0 -IR+Π 2 0 -IR −+AC 0,0-qf, whereΠ 2 0 -IR − is the restriction ofΠ 2 0 -IR without function parameters. (shrink)

It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule ofΠ 2 0 -inductionΠ 2 0 -IR isΠ 2 0 -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC 0,0-qf. More precisely we show that ℐ :=PRA 2 +Π 2 0 -IR+AC 0,0-qf proves the totality of the Ackermann function, wherePRA 2 is the extension ofPRA by number (...) and function quantifiers andΠ 2 0 -IR may contain function parameters. This is true even forPRA 2 +∑ 1 0 -IR+Π 2 0 -IR −+AC 0,0-qf, whereΠ 2 0 -IR − is the restriction ofΠ 2 0 -IR without function parameters. (shrink)

In recent years, proof theoretic transformations that are based on extensions of monotone forms of Gödel’s famous functional interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and (...) convex subsets of an abstract Hilbert space can be carried out in suitable formal systems that are covered by existing metatheorems developed in the course of the proof mining program. In particular, it follows that the monotone functional interpretation of this weak compactness principle can be realized by a functional Ω∗ definable from bar recursion of lowest type. While a case study on the analysis of strong convergence results that are based on weak compactness indicates that the use of the latter seems to be eliminable, things apparently are different for weak convergence theorems such as the famous Baillon nonlinear ergodic theorem. For this theorem we recently extracted an explicit bound on a metastable version of this theorem that is primitive recursive relative to Ω∗.In the current paper we for the first time give the construction of Ω∗ . As a corollary to the fine analysis of the use of bar recursion in this construction we obtain that Ω∗ elevates arguments in Tn at most to resulting functionals in Tn+2 . In particular, one can conclude from this that our bound on Baillon’s theorem is at least definable in T4. (shrink)

This book publishes for the first time notes from two notebooks of Gödel which formed the basis of a course on intuitionism Gödel delivered at Princeton in the.

We show that the so-called weak Markov's principle which states that every pseudo-positive real number is positive is underivable in [MATHEMATICAL SCRIPT CAPITAL T]ω ≔ E-HAω + AC. Since [MATHEMATICAL SCRIPT CAPITAL T]ω allows one to formalize Bishop's constructive mathematics, this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics . The underivability even holds if the ine.ective schema of full comprehension for negated formulas is added, which allows one to derive the law of excluded (...) middle for such formulas. (shrink)

In this note we show that proof-theoretic uniform boundedness or bounded collection principles which allow one to formalize certain instances of countable Heine–Borel compactness in proofs using abstract metric structures must be carefully distinguished from an unrestricted use of countable Heine–Borel compactness.

Along the line of Hirst‐Mummert and Dorais, we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2‐statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2‐statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi‐intuitionistic systems (...) including bar induction in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma. Our result is applicable to many mathematical principles whose sequential versions imply. (shrink)

This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In the (...) resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f. (shrink)

In this paper we study with proof-theoretic methods the function(al) s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functional provably recursive from $RCA_0 + COH + \Pi _1^0 - CP$ are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that $WKL_0 + \Pi _1^0 - (...) CP + COH$ is $\Pi _1^0 $ -conservative over PRA. Recent work of the first author showed that $\Pi _1^0 + CP + COH$ is equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs. For Ramsey's theorem for pairs and two colors $\left( {RT_2^2 } \right)$ we obtain the upper bounded that the type 2 functionals provable recursive relative to $RCA_0 + \sum\nolimits_2^0 {IA + RT_2^2 } $ are in T₁. This is the fragment of Gödel's system T containing only type 1 recursion—roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction of T₁-bounds from proofs that use RT2..... Moreover, this yields a new proof of the fact that $WKL_0 + \sum\nolimits_2^0 {IA} + RT_2^2 $ is $\Pi _1^0 $ -conservative over $RCA_0 + \sum\nolimits_2^0 { - IA} $ . The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using $\Pi _1^0 $ -comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for $RT_2^2 $. (shrink)