BRICS RS-98-18 U. Kohlenbach: Things that can and things that can’t be done in PRA BRICS

Basic Research in Computer Science

Things that can and things that can’t be done in PRA

Ulrich Kohlenbach BRICS Report Series RS-98-18 ISSN 0909-0878 September 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/18/

Things that can and things that can’t be done in PRA

Ulrich Kohlenbach

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade, Bldg. 540 DK-8000 Aarhus C, Denmark kohlenb@brics.dk

September 1998

Abstract

It is well-known by now that large parts of (non-constructive) mathematical reasoning can be carried out in systems T which are conservative over primitive recursive arithmetic PRA (and even much weaker systems). On the other hand there are principles S of elementary analysis (like the Bolzano-Weierstraß principle, the existence of a limit superior for bounded sequences etc.) which are known to be equivalent to arithmetical comprehension (relative to T ) and therefore go far beyond the strength of PRA (when added to T ). In this paper we determine precisely the arithmetical and computational strength (in terms of optimal conservation results and subrecursive characterizations of provably recursive functions) 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.

1 Introduction

It is well-known by now, mainly from work done on the program of so-called reverse mathematics (although not using the reverse direction explicitly), that substantial parts of mathematics (and in particular analysis) can be carried out in systems T which are conservative over primitive recursive arithmetic PRA (see [25] for a systematic account). This is of interest for mainly two reasons

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

1) If a Π_{2}^{0}-sentence A is provable in T and the conservation of T over PRA has been established proof-theoretically, then one can extract a primitive recursive program which realizes A from a given proof. Typically the resulting program will have a quite restricted complexity or rate of growth (compared to merely being primitive recursive). In fact in a series of papers we have shown that in many cases even a polynomial bound is guaranteed (see [9],[11],[14] among others).

2) One can argue that PRA formalizes what has been called finitistic reasoning (see e.g. [26]). If the conservation of T over PRA has been established finitistically (which is possible for mathematically strong systems T (see [22],[8]), then all the mathematics which can be carried out in T has a finitistic justification (see [24],[25] for a discussion of this).

In this paper we exhibit a sharp boundary between finistically reducible parts of analysis and extensions which provably go beyond the strength of PRA. More precisely we study the (proof-theoretical and numerical) strength of function parameterfree schematic forms of^{1}

• the convergence (with modulus of convergence) of bounded monotone sequences (a_{n})_{n∈IN} ⊂ IR principle (PCM)

• the Bolzano-Weierstraß principle (BW) for (a_{n})_{n∈IN} ⊂ [0, 1]^{d}

• the Ascoli-Arzela principle for bounded sequences (f_{n})_{n∈IN} ⊂ C[0, 1] of equicontinuous functions (A-A)

• the existence of the limit superior principle for (a_{n})_{n∈IN} ⊂ [0, 1] (Limsup).

Let us discuss what we mean by ‘function parameter-free schematic form’ in more detail for BW: ‘Schematic’ means that an instance BW(t) of BW is given by a term t of the underlying system which defines a sequence in [0, 1]^{d}. We allow number parameters k in t, i.e. we consider sequences ∀k ∈ IN BW(t[k]) of instances of BW, but not function parameters. Allowing function parameters to occur in BW would make the schema equivalent to the single second-order sentence

(∗) ∀(a_{n}) ⊂ [0, 1]^{d} BW(a_{n}).

1For precise formalizations of these principles in systems based on number and function variables see [12] on which the present paper partially relies. We slightly deviate from the notation used in [12] by writing (PCM),(PCM_{ar}) instead of (PCM2),(PCM1).

It is well-known by the work on program of reverse mathematics that (∗) is equivalent to the schema of arithmetical comprehension (relative to weak fragments of second-order arithmetic). On the other hand, the restriction of BW to function parameter-free instances – in short: BW^{−} – is much weaker since the iterated use of BW is now no longer possible.

We calibrate precisely the strength of PCM^{−}, BW^{−}, A-A^{−} and Limsup^{−} relative secondorder extensions of primitive recursive arithmetic PRA (thereby completing research started in [12]). It turns out that the results depend heavily on what type of extension of PRA we choose: One option is straightforward: extend PRA by number and variables x^{0} and quantifiers for objects f^{ρ} of type-level 1, i.e. ρ = 0(0) ⋯ (0), where ρ(0) is the type of functions from

IN into objects of type ρ (note that modulo λ-abstraction objects of type 0 \overbrace{(0) … (0)}^{n} are just n-ary number theoretic functions).^{2} We have the axioms and rules of many-sorted classical predicate logic as well as symbols and defining equations for all primitive recursive functionals of type level ≤ 2 in the sense of Kleene [7] (i.e. ordinary primitive recursion uniformly in function parameters, for details see e.g. [6](II.1) or [21]). We also have a schema of quantifier-free induction (w.r.t. to this extended language) and λ-abstraction for number variables, i.e.

(λ\underline{y}.t[\underline{y}])\underline{x} = t[\underline{x}], \underline{x}, \underline{y} tuples of the same length.

So PRA^{2} is the second-order fragment of the (restricted) finite type system P̂A^{ω}|^{\} from [3]. It is clear that the resulting system PRA^{2} is conservative over PRA. We often write 1 instead of 0(0).

Another option is to impose a restriction on the type-2-functionals which are allowed. We include functionals of arbitrary Grzegorczyk level in the sense of [9]^{3} (including all elementary recursive functionals) but not the iteration functional

(It) Φ_{it}(0, y, f) = y, Φ_{it}(x + 1, y, f) = f(x, Φ_{it}(x, y, f)),

although it is primitive recursive in the sense of Kleene (and not only in the extended sense of Gödel [5], ‘=’ is equality between natural numbers). We call the resulting system PRA_{−}^{2}. On easily shows that PRA^{2} is a definitorial extension of PRA_{−}^{2} + (It).

2So we could have used also variables and quantifiers for n-ary functions instead and treat sequences of functions as f_{n} := λm.f(n, m). However the use of variables f^{0(0)...(0)} is more convenient since it avoids the use of the λ-operator in many cases.

3This means that we allow all the type-2-functionals Φ_{n} from [9] plus a bounded search operator and bounded recursion – uniformly in function parameters – on the ground type (see [9]).

EA^{2} is the restriction of PRA_{−}^{2} to elementary recursive function(al)s only (see [20] for a definition of ‘elementary recursive functional’).

Remark 1.1 In contrast to the class of primitive recursive functions, there exists no Grzegorzcyk hierarchy for primitive recursive functionals which would include all of them: if Φ_{it} would occur at a certain level of such a hierarchy, then this hierarchy would collapse to this level since all primitive recursive functions can be obtained from the initial functions and Φ_{it} by substitution.

The schema of quantifier-free choice for numbers is given by

AC^{0,0}-qf : ∀x^{0}∃y^{0}A_{0}(x, y) → ∃f∀xA_{0}(x, fx),

where A_{0} is a quantifier-free formula.^{4} We also consider the binary König’s lemma as formulated in [27]:

WKL :≡ ∀f^{1}(T (f) ∧ ∀x^{0}∃n^{0}(lth(n) =_{0} x ∧ f(n) =_{0} 0) → ∃b ≤_{1} 1∀x^{0}(f(\overline{b}x) =_{0} 0)),

where b ≤_{1} 1 :≡ ∀n(bn ≤ 1) and

T (f) :≡ ∀n^{0}, m^{0}(f(n ∗ m) = 0 → f(n) = 0) ∧ ∀n^{0}, x^{0}(f(n ∗ ⟨x⟩) = 0 → x ≤ 1)

(here lth, ∗, \overline{b}x, ⟨·⟩ refer to a standard elementary recursive coding of finite sequences of numbers).

One easily shows that the schema of Σ_{1}^{0}-induction is derivable in PRA^{2}+ AC^{0,0}-qf (but not in PRA_{−}^{2}+ AC^{0,0}-qf). The schema of recursive comprehension is already provable in PRA_{−}^{2}+ AC^{0,0}-qf. So PRA^{2}+ AC^{0,0}-qf (resp. PRA^{2}+ AC^{0,0}-qf + WKL) is a function variable version of the system RCA_{0} (resp. WKL_{0}) used in reverse mathematics, which uses set variables instead of function variables. The main results of this paper are^{5}

Theorem 1.2 1) PRA_{−}^{2}+PCM^{−} contains PRA+Σ_{1}^{0}-IA.

2) PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−} is Π_{3}^{0}-(but not Π_{4}^{0}-)conservative over PRA+Σ_{1}^{0}-IA and hence Π_{2}^{0}-conservative over PRA.

Corollary 1.3 The provably recursive functions of PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−} are exactly the primitive recursive ones.

4Throughout this paper A_{0}, B_{0}, C_{0}, … denote quantifier-free formulas.

5Here and in the following we denote the (conservative) extension of PRA by first-order predicate logic also by PRA.

Theorem 1.4 1) PRA_{−}^{2}+Limsup^{−} contains PRA+Σ_{2}^{0}-IA.

2) PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−}+Limsup^{−} is Π_{4}^{0}-conservative over PRA+Σ_{2}^{0}-IA.

Corollary 1.5 The provably recursive functions of PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−}+Limsup^{−} are exactly the α(< ω^{(ω^{ω})})- recursive ones,^{6} i.e. the functions definable in the fragment T_{1} of Gödel’s T ([5]) with recursion of level ≤ 1 only, which includes the Ackermann function. This results also holds for EA^{2} instead of PRA_{−}^{2}.

Theorem 1.6 PRA^{2}+ PCM^{−} is closed under the function parameter-free rule Σ_{2}^{0}-IR^{−} of Σ_{2}^{0}-induction.

Corollary 1.7 Every α(< ω^{(ω^{ω})})-recursive (i.e. T_{1}-definable) function (including the Ackermann function) is provably recursive in PRA^{2}+ PCM^{−}.

Together with the fact that PRA^{2}+AC^{0,0}-qf+WKL is Π_{2}^{0}-conservative over PRA (see [22] and for more general results [8]) this yields

Corollary 1.8 PRA^{2}+AC^{0,0}-qf+WKL ⊢ / PCM^{−} (this holds a fortiori for BW^{−}, A-A^{−} and Limsup^{−} instead of PCM^{−}).

Theorem 1.9 Let P be PCM^{−}, BW^{−} or A-A^{−}. Then PRA^{2}+ AC^{0,0}-qf +P contains PRA +Π_{2}^{0}-IA (=PRA +Σ_{2}^{0}-IA).

So relative to PRA^{2}+ AC^{0,0}-qf, the principles PCM^{−}, BW^{−} and A-A^{−} are not conservative over PRA. Relative to PRA_{−}^{2} (+AC^{0,0}-qf +WKL) these principles are conservative over PRA but the principle Limsup^{−} is not.

2 Preliminaries

We first indicate how to represent real numbers and the basic arithmetical operations and relations on them in EA^{2}. The results of this section a fortiori hold for PRA_{−}^{2} instead of EA^{2}.

6Here α-recursive is meant in the sense of [16], i.e. unnested. In contrast to this the notion of αrecursiveness as used e.g. in [2],[21] corresponds to nested recursion.

The representation of IR presupposes a representation of Q: Let j be the Cantor pairing function. Rational numbers are represented as codes j(n, m) of pairs (n, m) of natural numbers n, m. j(n, m) represents

the rational number \frac{\frac{n}{2}}{m + 1}, if n is even, and the negative rational − \frac{\frac{n+1}{2}}{m + 1} if n is odd.

Because of the surjectivity of j, every natural number is a code of a uniquely determined rational number. On the codes of Q, i.e. on IN, we define an equivalence relation by

n_{1} =Q n_{2} :≡ \frac{\frac{j_{1}n_{1}}{2}}{j_{2}n_{1} + 1} = \frac{\frac{j_{1}n_{2}}{2}}{j_{2}n_{2} + 1} if j_{1}n_{1}, j_{1}n_{2} both are even

and analogously in the remaining cases, where \frac{a}{b} = \frac{c}{d} is defined to hold iff ad =_{0} cb (for bd > 0). On IN one easily defines functions | · |Q, +Q, −Q, ·Q :Q, maxQ, minQ ∈ EA^{2} and (quantifierfree) relations) <Q, ≤Q which represent the corresponding functions and relations on Q. In the following we sometimes omit the index Q if this does not cause any confusion.

Notational convention: For better readability we often write e.g. \frac{1}{k+1} instead of its code

j(2, k) in IN. So e.g. we write x^{0} ≤Q \frac{1}{k+1} for x ≤Q j(2, k).

Real numbers are represented as Cauchy sequences (q_{n})_{n∈IN} of rational numbers with fixed rate of convergence

∀n∀m, m̃ ≥ n(|q_{m} − qm̃| ≤ \frac{1}{n + 1}).

By the coding of rational numbers as natural numbers, sequences of rationals are just functions f^{1} (and every function f^{1} can be conceived as a sequence of rational numbers in a unique way). In particular representatives of real numbers are functions f^{1} modulo this coding. We now show that every function can be viewed of as an representative of a uniquely determined Cauchy sequence of rationals with modulus 1/(k + 1) and therefore can be conceived as an representative of a uniquely determined real number. To this end we need the following functional f̂.

Definition 2.1 The functional λf^{1}.f̂ ∈ EA^{2} is defined such that

f̂n = \{ \begin{matrix}fn, if ∀k, m, m̃ ≤_{0} n(m, m̃ ≥_{0} k → |fm −Q fm̃| ≤Q \frac{1}{k+1}) \\ f(n_{0} − 1) for n_{0} := min l ≤_{0} n[∃k, m, m̃ ≤_{0} l(m, m̃ ≥_{0} k ∧ |fm −Q fm̃| >Q \frac{1}{k+1})], \\ otherwise. \end{matrix}

One easily proves in EA^{2} that

1) if f^{1} represents a Cauchy sequence of rational numbers with modulus 1/(k + 1), then ∀n^{0}(fn =_{0} f̂n),

2) for every f^{1} the function f̂ represents a Cauchy sequence of rational numbers with

modulus 1/(k + 1). Following the usual notation we write (x_{n}) instead of fn and (x̂_{n}) instead of f̂n. Definition 2.2 1) (x_{n}) =_{IR} (x̃_{n}) :≡ ∀k^{0}(|x̂_{k} −Q ˆ x̃_{k}| ≤Q \frac{3}{k+1});

2) (x_{n}) <_{IR} (x̃_{n}) :≡ ∃k^{0}(ˆx̃_{k} − x̂_{k} >Q \frac{3}{k+1});

3) (x_{n}) ≤_{IR} (x̃_{n}) :≡ ¬(ˆx̃_{n}) <_{IR} (x̂_{n});

4) (x_{n}) +_{IR} (x̃_{n}) := (x̂_{2n+1} +Q ˆ x̃_{2n+1});

5) (x_{n}) −_{IR} (x̃_{n}) := (x̂_{2n+1} −Q ˆ x̃_{2n+1});

6) |(x_{n})|_{IR} := (|x̂_{n}|Q);

7) (x_{n}) ·_{IR} (x̃_{n}) := (x̂_{2(n+1)k} ·Q ˆ x̃_{2(n+1)k}), where k := ⌈maxQ(|x_{0}|Q + 1, |x̃_{0}|Q + 1)⌉;

8) For (x_{n}) and l^{0} we define

(x_{n})^{−1} := \{ \begin{matrix}(maxQ(x̂_{(n+1)(l+1)^{2}}, \frac{1}{l+1})^{−1}), if x̂_{2(l+1)} >Q 0 \\ (minQ(x̂_{(n+1)(l+1)^{2}}, \frac{−1}{l+1})^{−1}), otherwise; \end{matrix}

9) max_{IR} ((x_{n}), (x̃_{n})) := ( maxQ(x̂_{n}, ˆ x̃_{n})), min_{IR} ((x_{n}), (x̃_{n})) := ( minQ(x̂_{n}, ˆ x̃_{n})). Sequences of real numbers are coded as sequences f^{1(0)} of codes of real numbers. The principles PCM and PCM_{ar} of convergence for bounded monotone sequences are given by^{7}

PCM_{ar}(f^{1(0)}) :≡
∀n(0 ≤_{IR} f(n + 1) ≤_{IR} f(n)) → ∀k∃n∀m, m̃ ≥ n(|fm −_{IR} fm̃| ≤ \frac{1}{k+1}),

7The restriction to decreasing sequences and the special lower bound 0 is of course inessential.

PCM(f^{1(0)}) :≡
∀n(0 ≤_{IR} f(n + 1) ≤_{IR} f(n)) → ∃g∀k∀m, m̃ ≥ gk(|fm −_{IR} fm̃| ≤ \frac{1}{k+1}).

Relative to PRA_{−}^{2}, PCM is equivalent to the principle stating the convergence of f with a modulus of convergence (PCM_{ar} does not imply in PRA_{−}^{2} the existence of a limit since reals have to be given as Cauchy sequences with given rate of convergence). For monotone sequences the existence of a modulus of convergence can be obtained from the existence of a limit by the use of AC^{0,0}-qf. So relative to PRA_{−}^{2}+ AC^{0,0}-qf we don’t have to distinguish between our formulation of PCM, the existence of a limit of f and the existence of a limit together with a modulus of convergence. PCM^{−} and PCM_{ar}^{−} denote the function parameter-free schematic versions of PCM(f) and PCM_{ar}(f) (in the sense discussed in the introduction). Let BW(f) be the statement

(f^{1(0)} codes a sequence ⊂ [0, 1]^{d} ⇒ this sequence has a limit point in [0, 1]^{d}) (for details see [12]). In [12] we also discuss the (relative to PRA_{−}^{2} slightly stronger) principle BW^{+}(f) expressing that f possesses a convergent subsequence (with modulus of convergence). All the results of this paper are valid for both versions BW(f) and BW^{+}(f) and so we don’t distinguish between them and denote their function parameter-free schematic forms both by BW^{−}. Likewise for the Arzela-Ascoli lemma (see [12] for the precise formulations of A-A(f) and A-A^{+}(f)). We define the limit superior according to the so-called ε-definition, i.e. a ∈ [−1, 1] is the limit superior of (x_{n}) ⊂ [−1, 1] if^{8}

(∗) ∀k(∀m∃n > m(|a − x_{n}| ≤ \frac{1}{k + 1}) ∧ ∃l∀j > l(x_{j} ≤ a + \frac{1}{k + 1})).

(∗) implies (relative to PRA_{−}^{2}) that a is the maximal limit point of (x_{n}). The reverse direction follows with the use of BW (we don’t know whether it can be proved in PRA_{−}^{2}). Limsup(f) is the principle stating

(f codes a sequence ⊂ [−1, 1] ⇒ this sequence has a lim sup in the sense of (∗)). Limsup^{−} is the corresponding function parameter-free schematic version.

8Again the restriction to the particular bound 1 is inessential.

3 Things that can be done in (a conservative extension of) PRA resp. in PRA +Σ_{2}^{0}-IA

In this section we draw some consequences of our results from [12] and [13] and formulate them in a way which fits into the present framework.

Theorem 3.1 Every Π_{3}^{0}-theorem of PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−} is provable in PRA+Σ_{1}^{0}-IA.

Proof: From the proofs of propositions 5.5 and 5.6 from [12] and proposition 5.5.2) below it follows that there exist instances Π_{1}^{0}-CA(ξ_{j}) which prove, relative to E-G_{∞}A^{ω}+AC^{1,0}- qf+F^{−} all universal closures G̃_{i} of the instances G_{i} of PCM^{−}, BW^{−} and A-A^{−} which are used in the proof of the Π_{3}^{0}-sentence A ≡ ∀x∃y∀z A_{0}(x, y, z) ∈ PRA. The instances Π_{1}^{0}-CA(ξ_{j}) can be coded together into a single instance Π_{1}^{0}-CA(ξ) (see again the proof of proposition 5.5 from [12]). Since furthermore PRA_{−}^{2} ⊂ E-G_{∞}A^{ω} and – by [9] (section 4) – WKL can be derived in E-G_{∞}A^{ω}+AC^{1,0}-qf +F^{−},^{9} we obtain

E-G_{∞}A^{ω}+ AC^{1,0}-qf + F^{−} ⊢ Π_{1}^{0}-CA(ξ) → A.

Corollary 4.7 from [13] (combined with the elimination of extensionality procedure as used in the proof of corollary 4.5 in [13]) yields that

G_{∞}A^{ω} + Σ_{1}^{0}-IA ⊢ A,

and hence (since G_{∞}A^{ω} + Σ_{1}^{0}-IA can easily be seen to be conservative over PRA+Σ_{1}^{0}-IA)^{10}

PRA +Σ_{1}^{0}-IA ⊢ A.

□ Remark 3.2 1) In section 4 below we will show that already PRA_{−}^{2}+PCM^{−} contains

PRA+Σ_{1}^{0}-IA.

2) Already PRA_{−}^{2}+ AC^{0,0}-qf+PCM^{−} is not Π_{4}^{0}-conservative over PRA+Σ_{1}^{0}-IA: From proposition 5.5 below it follows that PRA_{−}^{2}+ AC^{0,0}-qf+PCM^{−} proves Π_{1}^{0}-CA^{−} and therefore every function parameter-free instance of the principle of Π_{1}^{0}-collection principle Π_{1}^{0}-CP. Hence PRA+Π_{1}^{0}-CP is a subsystem of PRA_{−}^{2}+ AC^{0,0}-qf+PCM^{−}. However from [17] we know that there exists an instance of Π_{1}^{0}-CP which cannot be proved in PRA +Σ_{1}^{0}-IA. The claim now follows from the fact that (the universal closure of) every instance of Π_{1}^{0}-CP can be shown to be equivalent to a Π_{4}^{0}-sentence in PRA+Σ_{1}^{0}- IA.

9In the proof of theorem 4.27 from [9], AC^{0,1}-qf is only needed to derive the strong sequential version WKL_{seq} of WKL.

10We work here in the variant of G_{∞}A^{ω} where the universal axioms 9) are replaced by the schema of quantifier-free induction.

Corollary 3.3 Let A ≡ ∀x∃yA_{0}(x, y) be a Π_{2}^{0}-sentence in L(PRA). Then the following rule holds:

PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−} ⊢ ∀x∃yA_{0}(x, y)

⇒ one can extract a primitive recursive function p such that

PRA ⊢ A_{0}(x, px).

Proof: The corollary follows from theorem 3.1 and the well-known fact that PRA+Σ_{1}^{0}-IA is Π_{2}^{0}-conservative over PRA. □

Theorem 3.4 Every Π_{4}^{0}-theorem of PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−}+Limsup^{−} is provable in PRA +Σ_{2}^{0}-IA.

Proof: One easily shows (relative to PRA_{−}^{2}+AC^{0,0}-qf that Limsup^{−} follows from Π_{2}^{0}-CA^{−}: for sequences (q_{n}) ⊂ [0, 1] of rational numbers this is particularly straightforward (the general case can be reduced to this one): by Π_{2}^{0}-CA define f such that for i < 2^{j}

f(i, j) = 0 ↔ ∞-many elements of (q_{n}) are in [\frac{i}{2^{j}} , \frac{i+1}{2^{j}}].

Let g(j) := maximal i < 2^{j}[f(i, j) = 0]. Then (a_{n}) defined by a_{n} := \frac{g(j)}{2^{j}} is a Cauchy sequence which converges (with rate 2^{n}) to the limsup (in the sense of (∗)) of (q_{n}). The theorem now follows from [13](corollary 4.7) similar to the use of this corollary in the proof of theorem 3.1 above. □

Remark 3.5 In section 5 below we will show that already PRA_{−}^{2}+Limsup^{−} contains PRA+Σ_{2}^{0}-IA.

Definition 3.6 By T_{n} we denote the fragment of Gödel’s calculus T of primitive recursive functionals in all finite types where one only has recursor constants R_{ρ} with deg(ρ) ≤ n (see [19] for details).

Corollary 3.7 Let A ≡ ∀x∃yA_{0}(x, y) be a Π_{2}^{0}-sentence in L(PRA). Then the following rule holds:

PRA_{−}^{2}+AC^{0,0}-qf+WKL+PCM^{−}+BW^{−}+A-A^{−}+Limsup^{−} ⊢ ∀x∃yA_{0}(x, y)

⇒ one can extract a closed term Φ^{1} of T_{1} such that

T_{1} ⊢ A_{0}(x, Φx).

Proof: The corollary follows from theorem 3.4 and Parsons’ result from [19] that PRA+Σ_{n+1}^{0}-IA has (via negative translation) a Gödel functional interpretation in T_{n}. □

Remark 3.8 Our results in [12] and [13] actually can be used to obtain stronger forms of the corollaries 3.3 and 3.7 since in [12],[13] we

1) allowed finite type extensions of the systems in the corollaries 3.3 and 3.7,

2) considered more general conclusions A ≡ ∀u^{1}∀v ≤_{ρ} tu∃z^{τ} A_{0}(x, y, z) (where ρ is an arbitrary type and τ ≤ 2) and showed how to extract uniform bounds Φ ∈ T_{0} (resp. ∈ T_{1} in the case of corollary 3.7) such that ∀u^{1}∀v ≤_{ρ} tu∃z ≤_{τ} ΦuA_{0}(x, y, z),

3) allowed the instances of PCM, BW, A-A, Limsup to depend on the parameters u, v of the conclusion and

4) allowed more general analytical axioms Δ (than only F^{−}).

4 Some proof theory of PRA^{2} + Π_{1}^{0}-AC^{−}

We consider the following schemata:

Π_{1}^{0}-CA^{−} : ∃f^{1}∀x^{0}(fx = 0 ↔ ∀yA_{0}(x, y)),
Π_{1}^{0}-ÂC^{−} : ∃f^{1}∀x^{0}, z^{0}(¬A_{0}(x, fx) ∨ A_{0}(x, z)),
Π_{1}^{0}-AC^{−} : ∀x^{0}∃y^{0}∀z^{0}A_{0}(x, y, z) → ∃f^{1}∀x, zA_{0}(x, fx, z),

where A_{0} is quantifier–free and has no function parameters. Π_{1}^{0}-CA(g) is the form of Π_{1}^{0}-CA^{−} where A_{0}(x, y) is replaced by g(x, y) = 0. Similarly for Π_{1}^{0}-ÂC(g) and Π_{1}^{0}-AC(g). One easily verifies the following

Lemma 4.1 1) PRA^{2} proves the implications Π_{1}^{0}-AC^{−} → Π_{1}^{0}-ÂC^{−} → Π_{1}^{0}-CA^{−}.

2) PRA^{2}+AC^{0,0}-qf proves Π_{1}^{0}-CA^{−} ↔ Π_{1}^{0}-ÂC^{−} ↔ Π_{1}^{0}-AC^{−}.

Proposition 4.2 1) PRA^{2}+Π_{1}^{0}-ÂC^{−} is closed under Σ_{2}^{0}-IR^{−} (i.e. the induction rule for Σ_{2}^{0}-formulas without function parameters) and hence contains the first-order system PRA+Σ_{2}^{0}-IR.

2) PRA^{2} + Π_{1}^{0}-ÂC^{−} proves every Π_{3}^{0}-theorem of PRA +Π_{2}^{0}-IA.

3) Every function which is definable in T_{1} (i.e. every α(< ω^{(ω^{ω})})-recursive function is provably recursive in PRA^{2} + Π_{1}^{0}-ÂC^{−}. In particular PRA^{2} + Π_{1}^{0}-ÂC^{−} (and a fortiori PRA^{2} + Π_{1}^{0}-AC^{−}) proves the totality of the Ackermann function.

Proof: 1) Let A ≡ ∃y^{0}∀z^{0}A_{0}(a^{0}, x^{0}, y^{0}, z^{0}) be a Σ_{2}^{0}–formula which contains only a, x free. Suppose that PRA^{2} proves:

Π_{1}^{0}–ÂC^{−} → ∃y∀zA_{0}(a, 0, y, z) ∧ ∀x(∃y∀zA_{0}(a, x, y, z) → ∃y∀zA_{0}(a, x′, y, z)).

For notational simplicity we assume that only one instance of Π_{1}^{0}–ÂC^{−} without parameters is used (every instance of Π_{1}^{0}–ÂC^{−} with a number parameter a can be reduced to a parameterfree one by coding a and x together) and let this instance be ∃f∀a, b( \underbrace{¬G_{0}(a, fa) ∨ G_{0}(a, b)}_{G̃_{0}:≡}).

Then

(1) PRA^{2} ⊢ ∃f∀a, bG̃_{0} → ∃y∀zA_{0}(a, 0, y, z) and
(2) PRA^{2} ⊢ ∃f∀a, bG̃_{0} → ∀x(∃y∀zA_{0}(a, x, y, z) → ∃y∀zA_{0}(a, x′, y, z)).

Since

\begin{matrix}∀g(∀a, x, y, z(\overbrace{¬A_{0}(a, x, y, gaxy) ∨ A_{0}(a, x, y, z)}^{Ã_{0}(a,x,y,z,g):≡}) \\ → ∀a, x, y(g̃axy = 0 ↔ ∀zA_{0}(a, x, y, z))), \end{matrix}

where

g̃axy := \{ \begin{matrix}1, if ¬A_{0}(a, x, y, gaxy) \\ 0, otherwise \end{matrix}

is primitive recursive in g, one has

(1)^{∗} PRA^{2} ⊢ ∀f, g(∀a, bG̃_{0} ∧ ∀a, x, y, zÃ_{0} → ∃y_{0}(g̃(a, 0, y_{0}) = 0))

(2)^{∗}\begin{cases}PRA^{2} ⊢ \\ ∀f, g(∀a, bG̃_{0} ∧ ∀a, x, y, zÃ_{0} → ∀x(∃y_{1}(g̃axy_{1} = 0) → ∃y_{2}(g̃ax′y_{2} = 0))). \end{cases}

Using functional interpretation combined with normalization (and the fact that the finite type extension of PRA^{2} obtained by adding variables and quantifiers for all finite types as well as the Π, Σ-combinators is conservative over PRA^{2}) or alternatively cut-elimination as in [21]) one obtains closed terms Φ_{1}, Φ_{2} of PRA^{2} such that

(3) PRA^{2} ⊢ \{ \begin{matrix}∀f, g(∀a, bG̃_{0} ∧ ∀a, x, y, zÃ_{0} → g̃(a, 0, Φ_{1}fga) = 0 \\ ∧∀x, y_{1}(g̃(a, x, y_{1}) = 0 → g̃(a, x′, Φ_{2}(fgaxy_{1}) = 0)). \end{matrix}

Using ordinary (Kleene–) primitive recursion we define in PRA^{2} a functional Φ by

\{ \begin{matrix}Φfga0 =_{0} Φ_{1}fga \\ Φfgax′ =_{0} Φ_{2}(f, g, a, x, Φfgax). \end{matrix}

Using only quantifier-free induction, (3) yields

PRA^{2} ⊢ ∀f, g(∀a, bG̃_{0} ∧ ∀a, x, y, zÃ_{0} → ∀x(g̃(a, x, Φfgax) = 0)),

hence PRA^{2} ⊢ ∀f, g(∀a, bG̃_{0} ∧ ∀a, x, y, zÃ_{0} → ∀x∃y∀zA_{0}(a, x, y, z) and therefore PRA^{2} + Π_{1}^{0}-ÂC^{−} ⊢ ∀x∃y∀zA_{0}(a, x, y, z).

2) follows from 1) using the result from [19] that PRA+Σ_{2}^{0}-IR proves every Π_{3}^{0}-theorem of PRA+Π_{2}^{0}-IA and the fact that PRA^{2} + Σ_{2}^{0}-IR^{−} ⊇ PRA +Σ_{2}^{0}-IR.

3) follows from 2) and the fact (see e.g. [18]) that the provably recursive functions of PRA+Π_{2}^{0}–IA are just the functions definable in T_{1} (i.e. the α(< ω^{(ω^{ω})})-recursive functions) which includes the Ackermann function.

□

Remark 4.3 The only part of the proof of proposition 4.2 which cannot be carried out with PRA_{−}^{2} instead of PRA^{2} is the definition of Φ.

Proposition 4.4 PRA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-CA^{−} contains PRA +Π_{2}^{0}-IA (=PRA +Σ_{2}^{0}-IA).

Proof: One easily shows that PRA^{2}+ AC^{0,0}-qf proves the second-order axiom of Σ_{1}^{0}- induction

∀f(∃y(f(0, y) = 0 ∧ ∀x(∃y(f(x, y) = 0) → ∃y(f(x′, y) = 0)) → ∀x∃y(f(x, y) = 0)).

Together with Π_{1}^{0}-CA^{−} this yields every function parameter-free instance of Σ_{2}^{0}-induction. □

5 Where the convergence of bounded monotone sequences of real numbers goes beyond PRA

We now determine the pointwise relationship of PCM_{ar} and PCM to Σ_{1}^{0}-IA and Π_{1}^{0}-ÂC and use this to calibrate the strength of PCM^{−} relative to PRA^{2}.

We first show a result which in particular implies that, relatively to EA^{2}, the principle (PCM_{ar}) is equivalent to the axiom of Σ_{1}^{0}-induction

Σ_{1}^{0}-IA : ∀g^{000}(∃y^{0}(g0y =_{0} 0)∧∀x^{0}(∃y^{0}(gxy =_{0} 0) → ∃y^{0}(gx′y =_{0} 0)) → ∀x^{0}∃y^{0}(gxy =_{0} 0)).

Remark 5.1 This axiom is (relative to EA^{2}) equivalent to the schema of induction for all Σ_{1}^{0}-formulas in L(EA^{2}) : Let ∃y^{0}A_{0}(\underline{f}, \underline{x}, y) be a Σ_{1}^{0}–formula (containing only \underline{f}, \underline{x} as free function and number variables). There exists a term t_{A_{0}} ∈ EA^{2} such that

EA^{2} ⊢ ∀\underline{x}(∃y^{0}A_{0}(\underline{f}, \underline{x}, y) ↔ ∃y^{0}(t_{A_{0}} \underline{f} \underline{x}y =_{0} 0)).

Proposition 5.2 One can construct functionals Ψ_{1}, Ψ_{2} ∈ EA^{2} such that:

1) EA^{2} proves

∀a^{1(0)}(∀k^{0}[∃y^{0}(Ψ_{1}ak0y =_{0} 0) ∧ ∀x^{0}(∃y^{0}(Ψ_{1}akxy =_{0} 0) → ∃y^{0}(Ψ_{1}akx′y =_{0} 0)) →

∀x^{0}∃y^{0}(Ψ_{1}akxy =_{0} 0)] → [∀n^{0}(0 ≤_{IR} a(n + 1) ≤_{IR} an)
→ ∀k^{0}∃n^{0}∀m, m̃ ≥_{0} n(|am −_{IR} am̃| ≤_{IR} \frac{1}{k+1})]).

2) EA^{2} proves

∀g^{000}([∀n^{0}(0 ≤Q Ψ_{2}g(n + 1) ≤Q Ψ_{2}gn ≤Q 1) →

∀k^{0}∃n^{0}∀m, m̃ ≥_{0} n(|Ψ_{2}gm −Q Ψ_{2}gm̃| ≤Q \frac{1}{k+1})]

→ [∃y^{0}(g0y =_{0} 0) ∧ ∀x^{0}(∃y^{0}(gxy =_{0} 0) → ∃y^{0}(gx′y =_{0} 0)) → ∀x^{0}∃y^{0}(gxy =_{0} 0)]).

Proof: 1) Assume that ∀n^{0}(0 ≤_{IR} a(n + 1) ≤_{IR} an) and ∃k∀n∃m > n(|am −_{IR} an| >_{IR} \frac{1}{k+1}). By Σ_{1}^{0}–IA one proves that

(+) ∀n^{0}∃i^{0}(lth(i) = n∧∀j <_{0} n((i)_{j} < (i)_{j+1}∧ ˆ (a((i)_{j}) −_{IR} a((i)_{j+1}))(3(k+1)) >Q \frac{2}{3(k + 1)})).

Let C ∈ IN be such that C ≥ a_{0}. For n := 3C(k + 1), (+) yields an i ∈ IN such that

\begin{matrix}∀j < 3C(k + 1)((i)_{j} < (i)_{j+1}) and \\ ∀j < 3C(k + 1)(a((i)_{j}) −_{IR} a((i)_{j+1}) >_{IR} \frac{1}{3(k+1)}). \end{matrix}

Hence a((i)_{0}) −_{IR} a((i)_{3C(k+1)}) > C which contradicts the assumption ∀n(0 ≤_{IR} a_{n} ≤_{IR} C). Define

Ψ_{1}akni :=_{0}

0, if lth(i) = n ∧ ∀j <_{0} n((i)_{j} < (i)_{j+1} ∧ ˆ (a((i)_{j}) −_{IR} a((i)_{j+1}))(3(k + 1)) >Q \frac{2}{3(k+1)}) 1, otherwise.

2) Define Ψ_{2} ∈ EA^{2} such that Ψ_{2}gn =Q 1 −Q ∑_{i=1}^{n} \frac{χgni}{i(i+1)}, where χ ∈ EA^{2} such that

χgni =_{0} \{ \begin{matrix}1, if ∃l ≤_{0} n(gil =_{0} 0) \\ 0, otherwise. \end{matrix}

Using ∑_{i=1}^{∞} \frac{1}{i(i+1)} = 1 (which is provable in EA^{2}) it follows that

∀n^{0}(0 ≤Q Ψ_{2}g(n + 1) ≤Q Ψ_{2}gn ≤Q 1).

By the assumption there exists an n_{x} for every IN ∋ x > 0 such that

∀m, m̃ ≥ n_{x}(|Ψ_{2}gm −Q Ψ_{2}gm̃| < \frac{1}{x(x + 1)}).

Claim: ∀x̃(0 < x̃ ≤_{0} x → (∃y(gx̃y = 0) ↔ ∃y ≤ n_{x}(gx̃y = 0))): Assume that ∃l^{0}(gx̃l = 0) ∧ ∀l ≤ n_{x}(gx̃l ≠ 0) for some x̃ > 0 with x̃ ≤ x. Subclaim: Let l_{0} be minimal such that gx̃l_{0} = 0. Then l_{0} > n_{x} and

Ψ_{2}g(max(l_{0}, x̃)) ≤Q Ψ_{2}g(max(l_{0}, x̃) − 1) −Q \frac{1}{x̃(x̃ + 1)}.

Proof of the subclaim: i) ∑_{i=1}^{max(l_{0},x̃)} \frac{χg(max(l_{0},x̃))i}{i(i+1)} contains \frac{1}{x̃(x̃+1)} as an element of the sum,

since gx̃l_{0} = 0 and therefore χg(max(l_{0}, x̃))x̃ = 1.

ii) ∑_{i=1}^{max(l_{0},x̃)−1} \frac{χg(max(l_{0},x̃)−1)i}{i(i+1)} does not contain \frac{1}{x̃(x̃+1)} as an element of the sum:

Case 1. x̃ ≥ l_{0}: Then max(l_{0}, x̃) − 1 = x̃ − 1 < x̃. Case 2. l_{0} > x̃: Then max(l_{0}, x̃) − 1 = l_{0} − 1. Since l_{0} is the minimal l such that gx̃l = 0, it follows that

∀i ≤ max(l_{0}, x̃) − 1(gx̃i ≠ 0) and thus χg(max(l_{0}, x̃) − 1)x̃ = 0,

which finishes case 2. Because of

χg(max(l_{0}, x̃) − 1)i ≠ 0 → χg(max(l_{0}, x̃))i ≠ 0,

i) and ii) yield

∑_{i=1}^{max(l_{0},x̃)} \frac{χg(max(l_{0}, x̃))i}{i(i + 1)} ≥ ∑_{i=1}^{max(l_{0},x̃)−1} \frac{χg(max(l_{0}, x̃) − 1)i}{i(i + 1)} + \frac{1}{x̃(x̃ + 1)},

which concludes the proof of the subclaim. The subclaim implies

max(l_{0}, x̃) − 1 ≥ n_{x} ∧ |Ψ_{2}g(max(l_{0}, x̃)) −Q Ψ_{2}g(max(l_{0}, x̃) − 1)| ≥ \frac{1}{x(x + 1)}.

However this contradicts the construction of n_{x} and therefore concludes the proof of the claim. Assume

(a) ∃y_{0}(g0y_{0} = 0).

Define Φ ∈ EA^{2} such that

Φgx̃y = \{ \begin{matrix}min ỹ ≤_{0} y[gx̃ỹ =_{0} 0], if ∃ỹ ≤_{0} y(gx̃ỹ =_{0} 0) \\ 0^{0}, otherwise. \end{matrix}

By the claim above and (a) we obtain for y := max(n_{x}, y_{0}):

(b) ∀x̃ ≤_{0} x(∃ỹ(gx̃ỹ =_{0} 0) ↔ gx̃(Φgx̃y) =_{0} 0).

QF–IA applied to A_{0}(x) :≡ (gx(Φgxy) =_{0} 0) yields

g0(Φg0y) = 0 ∧ ∀x̃ < x(gx̃(Φgx̃y) = 0 → gx̃′(Φgx̃′y) = 0) → gx(Φgxy) = 0.

From this and (a), (b) we obtain

∃y_{0}(g0y_{0} = 0) ∧ ∀x̃ < x(∃ỹ(gx̃ỹ = 0) → ∃ỹ(gx̃′ỹ = 0)) → ∃ỹ(gxỹ = 0).

Corollary 5.3

EA^{2} ⊢ Σ_{1}^{0}-IA ↔ PCM_{ar}.

Remark 5.4 1) From the proof of proposition 5.2 it follows that 2) is already provable in the intuitionistic variant EA_{i}^{2} of EA^{2}. In particular

EA_{i}^{2} ⊢ PCM_{ar} → Σ_{1}^{0}-IA.

The other implication Σ_{1}^{0}-IA → (PCM_{ar}) cannot be proved intuitionistically since (PCM_{ar}) implies the non–constructive so–called ‘limited principle of omniscience’ (see [15] for a discussion on this).

2) Proposition 5.2 provides much more information than corollary 5.3. In particular one can compute (in EA^{2}) uniformly in g a decreasing sequence of positive rational numbers such that the Cauchy property of this sequence implies induction for the Σ_{1}^{0}– formula A(x) :≡ ∃y(gxy = 0). The converse is not that explicit but Ψ_{1} provides an arithmetical family A_{k}(x) :≡ ∃y(Ψ_{1}akxy = 0) of Σ_{1}^{0}–formulas such that the induction principle for these formulas implies the Cauchy property of the decreasing sequence of positive reals a.

3) The proof of proposition 5.2.2) could be simplified a bit by using ∑_{i=0}^{∞} 2^{−i} instead of ∑_{i=1}^{∞} \frac{1}{i(i+1)}. However a_{n} :=_{IR} ∑_{i=1}^{n} \frac{1}{i(i+1)} as a sequence of real numbers (but not as rational numbers) can be defined already at the second level of the Grzegorczyk hierarchy so that the implication PCM_{ar} → Σ_{1}^{0}-IA holds even in G_{2}A^{ω} (see [14]).

We now show that Π_{1}^{0}-ÂC(a) can be reduced to PCM(ξa) (for a suitable ξ ∈ EA^{2}) relative to EA^{2} and that PCM(a) can be reduced to Π_{1}^{0}-AC(ζa).

Proposition 5.5 1) EA^{2} ⊢ ∀f^{1(0)}(PCM(λn^{0}.Ψ_{2}f′n) → Π_{1}^{0}-ÂC(f)),^{11}

where Ψ_{2} ∈ EA^{2} is the functional from prop. 5.2.2) such that Ψ_{2}fn =Q 1−Q ∑_{i=1}^{n} \frac{χfni}{i(i+1)}

and χ ∈ EA^{2} such that

χfni =_{0} \{ \begin{matrix}1^{0}, if ∃l ≤_{0} n(fil =_{0} 0) \\ 0^{0}, otherwise, and \end{matrix}

f′ := λx, y.\overline{sg}(fxy).

2) For a suitable closed term Φ of EA^{2} we have

EA^{2} ⊢ ∀f^{1}(Π_{1}^{0}-AC(Φf) → PCM(f)).

11Strictly speaking we refer here to the embedding λk.Ψ_{2}f′n of Q into IR instead of Ψ_{2}f′n.

Proof: 1) From the proof of prop.5.2.2) we know

(1) ∀n^{0}(0 ≤Q Ψ_{2}f′(n + 1) ≤Q Ψ_{2}f′n)

and

(2) \{ \begin{matrix}∀x >_{0} 0∀n((∀m, m̃ ≥ n → |Ψ_{2}f′m −Q Ψ_{2}f′m̃| <Q \frac{1}{x(x+1)}) → \\ ∀x̃(0 <_{0} x̃ ≤_{0} x → (∃y(f′x̃y = 0) ↔ ∃y ≤_{0} n(f′x̃y = 0)))) \end{matrix}

By (1) and (PCM)(λn^{0}.Ψ_{2}f′n) there exists a function h^{1} such that

∀x >_{0} 0∀m, m̃ ≥_{0} hx(|Ψ_{2}f′m −Q Ψ_{2}f′m̃| <Q \frac{1}{x(x + 1)}).

Hence by (2)

∀x >_{0} 0(∃y(f′xy = 0) ↔ ∃y ≤_{0} hx(f′xy = 0)).

Furthermore, classical logic yields ∃z_{0}(f0z_{0} ≠_{0} 0 ∨ ∀y(f0y = 0)). One now easily concludes that Π_{1}^{0}-ÂC(f).

2) Let Ψ_{1} ∈ EA^{2} be as in proposition 5.2.1. By Π_{1}^{0}-CA(Ψ̃_{1}f), where Ψ̃_{1}fxy = Ψ_{1}(f, j_{1}x, j_{2}x, y), there exists a function g such that

∀k^{0}, x^{0}(gkx = 0 ↔ ∃y(Ψ_{1}(f, k, x, y) = 0)).

Hence (by applying QF-IA to ‘gkx = 0’) one gets

\begin{matrix}∀k^{0}(∃y^{0}(Ψ_{1}fk0y =_{0} 0) ∧ ∀x^{0}(∃y^{0}(Ψ_{1}fkxy =_{0} 0) → ∃y^{0}(Ψ_{1}fkx′y =_{0} 0)) \\ → ∀x^{0}∃y^{0}(Ψ_{1}fkxy =_{0} 0)) \end{matrix}

and therefore (by proposition 5.2.1) PCM_{ar}(f). For a suitable Φ̃ ∈ EA^{2}, Π_{1}^{0}-AC(Φ̃f) allows to derive PCM(f) from PCM_{ar}(f). Π_{1}^{0}-CA(Ψ̃_{1}f) follows from Π_{1}^{0}-AC(Ψ̂_{1}f) for a suitable Ψ̂_{1} ∈ EA^{2}. Finally both instances Π_{1}^{0}-AC(Φ̃f) and Π_{1}^{0}-AC(Ψ̂_{1}f) can be coded together into a single instance Π_{1}^{0}-AC(Φf) for a suitable Φ ∈ EA^{2} (using that the universal closure w.r.t. arithmetical parameters is incorporated into the definition of Π_{1}^{0}-AC(f)). Hence

EA^{2} ⊢ ∀f^{1}(Π_{1}^{0}-AC(Φf) → PCM(f)).

□

Lemma 4.1.2) and proposition 5.5 imply Corollary 5.6 EA^{2}+AC^{0,0}-qf ⊢ Π_{1}^{0}-CA^{−} ↔ PCM^{−} and EA^{2} ⊢ PCM^{−} → Π_{1}^{0}-ÂC^{−}. Analogously for PRA_{−}^{2}, PRA^{2} instead of EA^{2}.

Theorem 3.1, remark 3.2.2) and corollary 5.6 yield theorem 1.2 from the introduction.

Remark 5.7 Proposition 5.5 in particular yields that relatively to EA^{2} the principle PCM:≡ ∀f PCM(f) implies CA_{ar}. For RCA_{0} instead of EA^{2} this implication is stated in [4]. A proof (which is different from our proof) can be found in [23].

Proposition 4.2 and proposition 5.5 together yield (using the fact that finitely many instances of Π_{1}^{0}-ÂC^{−} can be coded into a single function and number parameter-free instance)

Theorem 5.8 Let A ∈ Π_{3}^{0}-theorem of PRA +Π_{2}^{0}-IA. Then one can construct a primitive recursive sequence (q_{n})^{1} of (codes of) rational numbers such that

PRA ⊢ ∀n, m(n ≥_{0} m → 0 ≤Q q_{n} ≤Q q_{m} ≤Q 1)

and

PRA^{2} + PCM(q_{n}) ⊢ A.

Corollary 5.9 PRA^{2}+ PCM^{−} proves every Π_{3}^{0}-theorem of PRA+Π_{2}^{0}-IA. In particular: PRA^{2}+ PCM^{−} proves the totality of the Ackermann function (and more general of every α(< ω^{(ω^{ω})})-recursive function, i.e. of every function definable in T_{1}).

Theorem 5.10 Let P be PCM^{−}, BW^{−} or A-A^{−}. Then PRA^{2}+ AC^{0,0}-qf +P contains PRA +Π_{2}^{0}-IA (=PRA +Σ_{2}^{0}-IA).

Proof: For PCM^{−} this follows from proposition 4.4, lemma 4.1 and proposition 5.5. BW^{−} and A-A^{−} imply PCM^{−} relative to PRA^{2}+ AC^{0,0}-qf. □

6 Where the existence of the limit superior of bounded sequences goes beyond PRA

Theorem 6.1 PRA_{−}^{2}+ Limsup^{−} contains PRA +Σ_{2}^{0}-IA.

Proof: Let f be a function IN → IN and define q_{n}^{f} := \frac{1}{f(n)+1}. Then obviously (q_{n})_{IN} ⊂ [0, 1] ∩ Q. Let a := lim sup_{n→∞} q_{n}^{f}. Claim 1: For k ∈ IN, k > 0 we have

a ≥_{IR} \frac{1}{k} ↔ a >_{IR} \frac{1}{k + 1} ↔ ∀n∃m ≥ n(f(m) < k).

Proof of claim 1: →^{1} is trivial. →^{2}: Assume ∃n∀m ≥ n(f(m) ≥ k). Then ∃n∀m ≥ n(q_{m}^{f} ≤Q \frac{1}{k+1}) and hence (since a is a limit point of (q_{m}^{f})) a ≤_{IR} \frac{1}{k+1}. ←^{2}: ∀n∃m ≥ n(f(m) < k) implies ∀n∃m ≥ n(f(m) ≤ k − 1) and therefore

(1) ∀n∃m ≥ n(q_{m}^{f} ≥Q \frac{1}{k} =Q \frac{1}{k + 1} + \frac{1}{k(k + 1)}).

Since a is the maximal limit point of (q_{n}^{f})_{nIN}, we have

(2) ∃n∀m ≥ n(q_{m}^{f} <_{IR} a + \frac{1}{k(k + 1)}).

(1) and (2) yield that a >_{IR} \frac{1}{k+1}. ←^{1}: We have already shown that a >_{IR} \frac{1}{k+1} implies ∀n∃m ≥ n(f(m) ≤ k − 1) and so ∀n∃m ≥ n(q_{m}^{f} ≥ \frac{1}{k}) and hence a ≥_{IR} \frac{1}{k}. Claim 2: Relative to PRA_{−}^{2} we have

∀a^{1}, k^{0}(a =_{IR} lim sup_{n→∞} q_{n}^{f} ∧ ∀n∃m ≥ n(f(m) < k)

→ ∃k_{0} ≤ k(k_{0} minimal such that ∀n∃m ≥ n(f(m) < k_{0})).

Proof of claim 2: Assume a =_{IR} lim sup_{n→∞} q_{n}^{f} and ∀n∃m ≥ n(f(m) < k). Then, by claim 1, a ≥_{IR} \frac{1}{k}. We now show that there exists a k_{0} such that 0 < k_{0} ≤ k and a =_{IR} \frac{1}{k_{0}} (it is clear that k_{0} is minimal such that ∀n∃m ≥ n(f(m) < k_{0}) since otherwise (by claim 1) a ≥_{IR} \frac{1}{k_{0}−1}). Let k_{0}, 0 < k_{0} ≤ k, be such that |\frac{1}{k_{0}} −Q a(2k(k + 1))| is minimal. Then \frac{1}{k_{0}+1} <_{IR} a and, if k_{0} − 1 > 0, a <_{IR} \frac{1}{k_{0}−1}, since

\frac{1}{2k(k + 1)} ≤ \frac{1}{2} (\frac{1}{k_{0}} − \frac{1}{k_{0} + 1}) <^{if k_{0}−1>0} \frac{1}{2} (\frac{1}{k_{0} − 1} − \frac{1}{k_{0}} )

and |a − a(2k(k + 1))| < \frac{1}{2k(k+1)}. Claim 1 now implies that a =_{IR} \frac{1}{k_{0}} . Claim 3: Relative to PRA_{−}^{2} we have

∀a^{1}, k^{0}(a =_{IR} lim sup_{n→∞} q_{n}^{f} ∧ ∀n∃m ≥ n(f(m) = k)

→ ∃k_{0} ≤ k(k_{0} minimal such that ∀n∃m ≥ n(f(m) = k_{0})).

Proof of claim 3: Assume that ∃a^{1}(a =_{IR} lim sup_{n→∞} q_{n}^{f}). Then

∃k∀n∃m ≥ n(fm = k) ⇒

∃k∀n∃m ≥ n(fm < k + 1) ⇒^{Claim2}

∃k( k least such that ∀n∃m ≥ n(fm < k + 1)) ⇒

∃k( k least such that ∀n∃m ≥ n(fm = k)).

Claim 4: Let R(l^{0}, k^{0}, m^{0}) be a primitive recursive predicate. Then there exists a primitive recursive function f such that

PRA ⊢ ∀l, k∀k̃ ≤ k(∀n∃m ≥ n R(l, k̃, m) ↔ ∀n∃m ≥ n(flkm = k̃)).

Proof of Claim 4: Define (using the Cantor pairing function j and its projections j_{i})

t̃lkm := \{ \begin{matrix}j_{1}m, if R(l, j_{1}m, j_{2}m) \\ k + 1, otherwise. \end{matrix}

We show (for all l and all k̃ ≤ k)

∀n∃m ≥ n(t̃lkm = k̃) ↔ ∀n∃m ≥ n R(l, k̃, m).

‘→’: Let n_{0} := max_{i≤n} j(k̃, i) and m > n_{0} such that t̃lkm = k̃. Then j_{1}m = k̃, R(l, k̃, j_{2}m)

and j_{2}m > n, since m = j(k̃, j_{2}m) > n_{0}. Hence ∃m ≥ n R(l, k̃, m). ‘←’: Let m ≥ n be such that R(l, k̃, m). Then t̃(l, k, j(k̃, m)) = k̃. Since j(k̃, m) ≥ m ≥ n, we get ∃m ≥ n(t̃lkm = k̃). Claim 5: Let R(k, n, m) be primitive recursive and R̃(k, n, m) :≡ R(k, n, m) ∧ ∀m̃ < m¬R(k, n, m̃). Then PRA +Σ_{1}^{0}-IA proves

∀k(∀n∃m R(k, n, m) ↔ ∀n∃m ≥ n(lth(j_{2}m) = j_{1}m + 1 ∧ ∀ñ ≤ j_{1}m R̃(k, ñ, (j_{2}m)ñ))).

Proof of Claim 5: ‘→’: Assume ∀n∃m R(k, n, m) and hence ∀n∃m R̃(k, n, m). By the principle of finite choice for Σ_{1}^{0}-formulas (which follows from Σ_{1}^{0}-IA, see [17]) we obtain ∃m̃(lth(m̃) = n + 1 ∧ ∀ñ ≤ n R̃(k, ñ, (m̃)ñ)). So m := j(n, m̃) satisfies the right-hand side of the equivalence. ‘←’: Assume

(+) ∀n∃m ≥ n(lth(j_{2}m) = j_{1}m + 1 ∧ ∀ñ ≤ j_{1}m R̃(k, ñ, (j_{2}m)ñ))

and suppose that ∃n∀m¬R(k, n, m) and hence ∃n∀m¬R̃(k, n, m). By the least number principle for Π_{1}^{0}-formulas (which easily follows from Σ_{1}^{0}-IA) we get a least such n, call it n_{0}. Hence

∀n < n_{0}∃m R̃(k, n, m).

Again by finite Σ_{1}^{0}-choice we obtain

(++) ∃m_{0}(lth(m_{0}) = n_{0} ∧ ∀n < n_{0}R̃(k, n, (m_{0})_{n})).

By (+) there exists an m > j(n_{0} − · 1, m_{0}) such that

(+ + +) lth(j_{2}m) = j_{1}m + 1 ∧ ∀ñ ≤ j_{1}m R̃(k, ñ, (j_{2}m)ñ).

Then either j_{1}m ≥ n_{0} or j_{1}m < n_{0} ∧ j_{2}m > m_{0}. The first case yields a contradiction to ∀m¬ R̃(k, n_{0}, m) and the second case contradicts the fact that (by R̃-definition) (++) and (+ + +) imply

∀ñ < lth(j_{2}m)((j_{2}m)ñ = (m_{0})ñ).

We now finish the proof of the theorem. By the claims 3-5 and the fact that PRA_{−}^{2}+ Limsup^{−} ⊢ PCM_{ar}^{−} (which in turn yields Σ_{1}^{0}-IA^{−} by proposition 5.2.2, so that PRA +Σ_{1}^{0}- IA is a subsystem of PRA_{−}^{2}+ Limsup^{−}), we obtain in PRA_{−}^{2}+ Limsup^{−} the least number principle instance

∃k∀n∃m R(l, k, n, m) → ∃k( k minimal such that ∀n∃m R(l, k, n, m)).

Hence PRA_{−}^{2}+ Limsup^{−} proves every function parameter-free Π_{2}^{0}-instance of the least number principle, i.e. Π_{2}^{0}-LNP^{−}. It is an easy exercise to show that this in turn implies Σ_{2}^{0}-IA^{−} which concludes the proof of the theorem since PRA+Σ_{2}^{0}-IA is a pure first-order theory. □

As an immediate corollary of the theorems 3.4 and 6.1 we get theorem 1.4 from the introduction. Corollary 1.5 follows from theorem 1.4 using the fact that PRA+Σ_{2}^{0}-IA has via negative translation a Gödel functional interpretation in T_{1} (see [19]) and that the functions definable in T_{1} are exactly the α(< ω^{(ω^{ω})})-recursive ones (see [18]).

References

[1] Buss, S.R. (editor), Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics Vol 137, Elsevier, vii+811 pp. (1998).

[2] Fairlough, M., Wainer, S., Hierarchies of provably recursive functions. In: [1] pp. 149-207.

[3] Feferman, S., Theories of finite type related to mathematical practice. In: Barwise, J. (ed.), Handbook of Mathematical Logic, pp. 913-972, North-Holland, Amsterdam (1977).

[4] Friedman, H., Systems of second-order arithmetic with restricted induction (abstract). J. Symbolic Logic 41, pp. 558-559 (1976)

[5] Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, pp. 280-287 (1958).

[6] Hinman P.G., Recursion-Theoretic Hierarchies. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, Heidelberg, New York 1978.

[7] Kleene, S.C., Introduction to Metamathematics. North-Holland (Amsterdam), Noordhoff (Groningen), Van Nostrand (New-York) 1952.

[8] Kohlenbach, U., Effective bounds from ineffective proofs in analysis: an application of functional interpretation and majorization. J. Symbolic Logic 57, pp. 1239–1273 (1992).

[9] Kohlenbach, U., Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Arch. Math. Logic 36, pp. 31-71 (1996).

[10] Kohlenbach, U., Elimination of Skolem functions for monotone formulas in analysis. Arch. Math. Logic 37, pp. 363-390 (1998).

[11] Kohlenbach, U., The use of a logical principle of uniform boundedness in analysis. To appear in: Proc. ‘Logic in Florence 1995’.

[12] Kohlenbach, U., Arithmetizing proofs in analysis. In: Larrazabal, J.M. et al. (eds.), Proceedings Logic Colloquium 96 (San Sebastian), Springer Lecture Notes in Logic 12, pp. 115–158 (1998).

[13] Kohlenbach, U., On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness. To appear in: Ann. Pure and Applied Logic.

[14] Kohlenbach, U., Proof theory and computational analysis.

Electronic Notes in Theoretical Computer Science 13, Elsevier (http://www.elsevier.nl/locate/entcs/volume13.html), 1998.

[15] Mandelkern, M., Limited omniscience and the Bolzano–Weierstraß principle. Bull. London Math. Soc. 20, pp. 319-320 (1988).

[16] Parsons, C., Ordinal recursion in partial systems of number theory (abstract). Notices AMS 13, pp. 857-858 (1966).

[17] Parsons, C., On a number theoretic choice schema and its relation to induction. In: Intuitionism and proof theory, pp. 459-473. North-Holland, Amsterdam (1970).

[18] Parsons, C., Proof-theoretic analysis of restricted induction schemata (abstract). J. Symbolic Logic 36, p.361 (1971).

[19] Parsons, C., On n-quantifier induction. J. Symbolic Logic 37, pp. 466-482 (1972).

[20] Rose, H.E., Subrecursion: Functions and hierarchies. Oxford Logic Guides 9, Clarendon Press Oxford 1984.

[21] Schwichtenberg, H., Proof theory: some applications of cut-elimination. In: Barwise, J. (ed.), Handbook of Mathematical Logic, North–Holland, Amsterdam, pp. 867-895 (1977).

[22] Sieg, W., Fragments of arithmetic. Ann. Pure Appl. Logic 28,pp. 33–71 (1985).

[23] Simpson, S.G., Reverse Mathematics. Proc. Symposia Pure Math. 42, pp. 461-471, AMS, Providence (1985).

[24] Simpson, S.G., Partial realizations of Hilbert’s Program. J. Symbolic Logic 53, pp. 349-363 (1988).

[25] Simpson, S.G., Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag. To appear.

[26] Tait, W.W., Finitism. Journal of Philosophy 78, pp. 524-546 (1981).

[27] Troelstra, A.S., Note on the fan theorem. J. Symbolic Logic 39, pp. 584–596 (1974).

Recent BRICS Report Series Publications

RS-98-18 Ulrich Kohlenbach. Things that can and things that can’t be done in PRA. September 1998. 24 pp.

RS-98-17 Roberto Bruni, José Meseguer, Ugo Montanari, and Vladimiro Sassone. A Comparison of Petri Net Semantics under the Collective Token Philosophy. September 1998. 20 pp. To appear in 4th Asian Computing Science Conference, ASIAN ’98 Proceedings, LNCS, 1998.

RS-98-16 Stephen Alstrup, Thore Husfeldt, and Theis Rauhe. Marked Ancestor Problems. September 1998.

RS-98-15 Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the Overhead of ML Exceptions by Selective CPS Transformation. September 1998. 31 pp. To appear in the proceedings of the 1998 ACM SIGPLAN Workshop on ML, Baltimore, Maryland, September 26, 1998.

RS-98-14 Sandeep Sen. The Hardness of Speeding-up Knapsack. August 1998. 6 pp.

RS-98-13 Olivier Danvy and Morten Rhiger. Compiling Actions by Partial Evaluation, Revisited. June 1998. 25 pp.

RS-98-12 Olivier Danvy. Functional Unparsing. May 1998. 7 pp. This report supersedes the earlier report BRICS RS-98-5. Extended version of an article to appear in Journal of Functional Programming.

RS-98-11 Gudmund Skovbjerg Frandsen, Johan P. Hansen, and Peter Bro Miltersen. Lower Bounds for Dynamic Algebraic Problems. May 1998. 30 pp.

RS-98-10 Jakob Pagter and Theis Rauhe. Optimal Time-Space Trade-Offs for Sorting. May 1998. 12 pp.

RS-98-9 Zhe Yang. Encoding Types in ML-like Languages (Preliminary Version). April 1998. 32 pp.

RS-98-8 P. S. Thiagarajan and Jesper G. Henriksen. Distributed Versions of Linear Time Temporal Logic: A Trace Perspective. April 1998. 49 pp. To appear in 3rd Advanced Course on Petri Nets, ACPN ’96 Proceedings, LNCS, 1998.