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].

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)

An introduction to the developments of nonstandard models. Beginning with Godel's incompleteness theorem, it covers the prime models, cofinal extensions, and extensions, Gaifman's construction of a definable type, Tennenbaum's theorem and Friedman's theorem on indicators, ending with a chapter on recursive saturation and resplendency.

IΣ n andBΣ n are well known fragments of first-order arithmetic with induction and collection forΣ n formulas respectively;IΣ n 0 andBΣ n 0 are their second-order counterparts. RCA0 is the well known fragment of second-order arithmetic with recursive comprehension;WKL 0 isRCA 0 plus weak König's lemma. We first strengthen Harrington's conservation result by showing thatWKL 0 +BΣ n 0 is Π 1 1 -conservative overRCA 0 +BΣ n 0 . Then we develop some model theory inWKL 0 and illustrate (...) the use of formalized model theory by giving a relatively simple proof of the fact thatIΣ 1 provesBΣ n+1 to be Π n+2-conservative overIΣ n . Finally, we present a proof-theoretic proof of the stronger fact that theΠ n+2 conservation result is provable already inIΔ 0 + superexp. ThusIΣ n+1 proves 1-Con (BΣ n+1) andIΔ 0 +superexp proves Con (IΣ n )↔Con(BΣ n+1). (shrink)

We investigate the provability or nonprovability of certain ordinary mathematical theorems within certain weak subsystems of second order arithmetic. Specifically, we consider the Cauchy/Peano existence theorem for solutions of ordinary differential equations, in the context of the formal system RCA 0 whose principal axioms are ▵ 0 1 comprehension and Σ 0 1 induction. Our main result is that, over RCA 0 , the Cauchy/Peano Theorem is provably equivalent to weak Konig's lemma, i.e. the statement that every infinite {0, 1}-tree (...) has a path. We also show that, over RCA 0 , the Ascoli lemma is provably equivalent to arithmetical comprehension, as is Osgood's theorem on the existence of maximum solutions. At the end of the paper we digress to relate our results to degrees of unsolvability and to computable analysis. (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)

We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...) generalized to relate a hierarchy of subsystems, all contained in the theory of arithmetic properties, to a corresponding hierarchy of fragments of arithmetic. The proof theoretic tools employed there are used to re-establish in a uniform, elementary way relationships between various fragments of arithmetic due to Parsons, Paris and Kirby, and Friedman. (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)

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)

ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...) Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander .P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand‐point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other. (shrink)