In this paper a model for barrecursion is presented. It has as a novelty that it contains discontinuous functionals. The model is based on a concept called strong majorizability. This concept is a modification of Howard's majorizability notion; see [T, p. 456].

Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...) that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (shrink)

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)

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)

We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with Σ b 1 -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

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)

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)