BRICS RS-97-23 U. Kohlenbach: On the arithmetical content of restricted forms of comprehension BRICS

Basic Research in Computer Science

On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness

Ulrich Kohlenbach

BRICS Report Series RS-97-23 ISSN 0909-0878 August 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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/97/23/

On the arithmetical content of restricted forms of comprehension, choice and general uniform

boundedness

Ulrich Kohlenbach

BRICS^{∗}

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

August 5, 1997

Abstract

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 T_{n}^{ω} in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive function(al)s of low growth. We reduce the use of instances of these principles in T_{n}^{ω}-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.

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

1 Introduction

This paper studies the numerical strength of fragments Γ of arithmetical comprehension, choice and uniform boundedness relative to weak base systems, formulated in the language of all finite types, which are suited to formalize substantial parts of analysis. In a previous paper ([12]) we have introduced a hierarchy G_{n}A^{ω} of systems where the definable functions correspond to the well-known Grzegorczyk hierarchy. These systems extended by the schema of full quantifier-free choice

\begin{matrix}AC^{ρ,τ}-qf : ∀x^{ρ}∃y^{τ}A_{0}(x, y) → ∃Y^{τ(ρ)}∀x^{ρ}A_{0}(x, Y x), \\ AC-qf := ⋃_{ρ,τ∈T}\{AC^{ρ,τ}-qf \}, \end{matrix}

where A_{0} is a quantifier-free formula,^{1} and various non-constructive analytical axioms Δ, having the form

∀x^{ρ}∃y ≤_{τ} sx∀z^{δ}A_{0}(x, y, z),

including a generalized version of the binary König’s lemma, allow to carry out a great deal of classical analysis even for n = 2, 3. The axioms Δ and AC-qf do not contribute to the growth of extractable uniform bounds which in the particular case of G_{2}A^{ω} are polynomials (see [12],[14] and in particular [10] for more information).

In contrast to this, fragments of arithmetical comprehension and choice as well as generalizations of our principle of uniform Σ_{1}^{0}-boundedness (from [12]) to more complex formulas do contribute significantly to the arithmetic strength of the base systems. In [13] we developed a general method to calibrate faithfully this contribution and applied it to instances of Π_{1}^{0}- comprehension and Π_{1}^{0}-choice. These results were then used in [15] to determine the arithmetical strength of single sequences of instances of the Bolzano-Weierstraß theorem for bounded sequences in IR^{d}, the Ascoli-lemma and others.

In this paper we give a systematic treatment of the whole arithmetical hierarchy for comprehension, choice and uniform boundedness and determine precisely their arithmetical strength. We also consider much more complex formulas to be proved in these systems than we did in our previous papers.

1Throughout this paper A_{0}, B_{0}, C_{0}, … denote quantifier-free formulas. We allow bounded number quantifiers ∀x ≤_{0} t, ∃x ≤_{0} t to occur in A_{0}, B_{0}, C_{0}, … since they can be expressed in a quantifier-free way using the bounded search-functional μ_{b} from G_{n}A^{ω}. T denotes the set of all finite types.

In the following let us discuss now some of the difficulties one has to deal with in order to achieve this goal and which indicate already the type of results one can expect. For simplicity we restrict ourselves for the moment to the second-order system EA^{2}+ AC^{0,0}-qf instead of G_{n}A^{ω}+ AC-qf +Δ (which we actually are going to consider below). EA^{2} is an extension of Kalmar-elementary arithmetic (with number quantifiers) EA obtained by adding n-ary function quantifiers (for every n ≥ 1)^{2} and the schema of explicit definition of functions

ED : ∃f∀\underline{x}(f(\underline{x}) = t[\underline{x}]),

where t is a number term of EA^{2} and \underline{x} is a tuple of number variables. Furthermore EA^{2} contains the schema of quantifier-free induction for all quantifier-free formulas of EA^{2} which may contain function parameters. Finally EA^{2} contains constants and their defining equations for all elementary recursive functionals of type-level 2. In EA^{2} the schema of quantifier-free induction can be expressed equivalently as a single axiom

QF-IA : ∀f(f(0) = 0 ∧ ∀x(f(x) = 0 → f(x′) = 0) → ∀x(f(x) = 0)).

Let us consider furthermore the restriction of arithmetical choice to Π_{1}^{0}- (or equivalently to Σ_{2}^{0}-) formulas of L(EA^{2}) which like QF-IA can be expressed as a single second-order axiom ∀f Π_{1}^{0}-AC(f), where^{3}

Π_{1}^{0}-AC(f):≡ ∀a^{0}(∀x^{0}∃y^{0}∀z^{0}(f(a, x, y, z) = 0) → ∃g∀x, z(f(a, x, gx, z) = 0)).

Now by iteration one easily verifies that EA^{2} + ∀f Π_{1}^{0}-AC(f) proves already full arithmetical choice. So in order to prevent the arithmetical hierarchy of choice principles from collapsing we restrict ourselves to single instances of ∀fΠ_{1}^{0}-AC(f) which later on are allowed however to depend on the parameters of the theorem to be proved. For the moment we forbid completely the occurrence of function parameters in Π_{1}^{0}-AC, i.e. we consider the schema

Π_{1}^{0}-AC^{−} : ∀x^{0}∃y^{0}A(x, y) → ∃g∀x A(x, gx),

where A(x, y) is a Π_{1}^{0}-formula without function parameters.

2Since coding of finite tuples of numbers is available in EA one can in fact restrict oneself to unary function variables.

3The universal closure with respect to number parameters a^{0} is superfluous for ∀f Π_{1}^{0}- AC(f) since it can be captured by the universal closure ∀f. However below we consider single instances Π_{1}^{0}-AC(ξ) of ∀f Π_{1}^{0}-AC(f) where it does make a difference.

As a starting point for the introduction into our general program let us consider now the following question:

What arithmetical statements are provable in EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−}?

A first observation is that Π_{1}^{0}-AC^{−} proves Π_{1}^{0}-CA^{−}, i.e.

∃f∀x(f(x) = 0 ↔ A(x)),

where A(x) is a Π_{1}^{0}-formula without function parameters. Combined with the axiom QF-IA this yields every function parameter-free instance of Σ_{1}^{0}- IA. Hence the first-order system EA +Σ_{1}^{0}-IA is a subsystem of EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−}.

What is the precise relationship between EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−} and EA +Σ_{1}^{0}-IA? It will turn out that the former theory is conservative over the latter for some formulas, including Π_{3}^{0}-sentences, but not for all formulas. That EA^{2}+ AC^{0,0}-qf cannot be conservative over EA +Σ_{1}^{0}-IA without some restriction imposed on the formulas follows from the following observation:

By applying the functional Φ_{max}fx := max_{i≤x}(f(i)) to the function g in Π_{1}^{0}-AC^{−}

one obtains the corresponding instance of the so-called (bounded) collection principle for Π_{1}^{0}-formulas

Π_{1}^{0}-CP : ∀x ≤ a∃y A(x, y) → ∃z∀x ≤ a∃y ≤ z A(x, y),

where A ∈ Π_{1}^{0}. So EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−} proves every function parameter-free instance of Π_{1}^{0}-CP, i.e. EA +Π_{1}^{0}-CP is a subsystem of EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−}. It is well-known (see [18]) that there exists an instance A of Π_{1}^{0}-CP which is not provable in EA +Σ_{1}^{0}-IA. On the other hand EA +Π_{1}^{0}-CP is Π_{3}^{0}- conservative over EA +Σ_{1}^{0}-IA by a result due to H. Friedman and (implicitly) J.Paris/L.Kirby [17] (see e.g. [7] for details). The universal closure of the instance A of Π_{1}^{0}-CP can be shown to be equivalent to a Π_{4}^{0}-sentence in EA +Σ_{1}^{0}-IA. Hence EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−} is not Π_{4}^{0}-conservative over EA +Σ_{1}^{0}-IA.

Here is another arithmetical use of Π_{1}^{0}-AC^{−} we can make relative to EA^{2}+ AC^{0,0}-qf:

As mentioned above, Π_{1}^{0}-CA^{−} is a trivial consequence of Π_{1}^{0}-AC^{−} (in the presence of classical logic). Now combining Π_{1}^{0}-CA^{−} with AC^{0,0}-qf one can easily prove Δ_{2}^{0}-CA^{−} and therefore every function parameter-free instance of Δ_{2}^{0}-IA. Hence EA +Δ_{2}^{0}-IA is a subsystem of EA^{2}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−} as well even if the functional Φ_{max} were not included in EA^{2}.

So the arithmetical strength of Π_{1}^{0}-AC^{−} depends heavily on the second-order axioms, like QF-IA, AC^{0,0}-qf and the characterizing axioms for functionals as Φ_{max}, which are available in the context in which Π_{1}^{0}-AC^{−} is considered.^{4}

As a special corollary of the results of this paper it follows that EA^{2}+ AC^{0,0}-qf +Π_{k}^{0}-AC^{−} is Π_{k+2}^{0}-conservative over EA +Σ_{k}^{0}-IA, which implies the result of H. Friedman, J.Paris/L.Kirby. Furthermore we show that EA^{2}+ AC^{0,0}-qf +Π_{k}^{0}-AC^{−} is conservative over EA +Σ_{k}^{0}-IA w.r.t. monotone formulas of arbitrary complexity. These results are sensitive to small changes of the base system EA^{2}: E.g. if we add the primitive recursive functional Φ_{it} defined by

Φ_{it}fg0 := g(0) Φ_{it}fgx′ := f(x, Φ_{it}fgx)

to EA^{2}, then the Ackermann-function becomes provably total in EA^{2} + Φ_{it}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−} and the resulting system proves the consistency of EA +Σ_{1}^{0}-IA: EA^{2} + Φ_{it}+ AC^{0,0}-qf proves the second-order axiom of Σ_{1}^{0}-induction. Combined with Π_{1}^{0}-CA^{−} one obtains every function parameterfree instance of Σ_{2}^{0}-IA. Hence EA +Σ_{2}^{0}-IA (which is known to prove the totality of the Ackermann-function as well as the consistency of EA +Σ_{1}^{0}-IA) is a subsystem of EA^{2} + Φ_{it}+ AC^{0,0}-qf +Π_{1}^{0}-AC^{−}. Using a more involved argument one can show that already EA^{2} + Φ_{it} + Π_{1}^{0}-AC^{−} proves the totality of the Ackermann function (see chapter 12 of [10] for details on this).

So any proof of conservation of systems based on Π_{k}^{0}-AC^{−} over Σ_{k}^{0}-IA has to take into account carefully the structure of the functionals of type level 2 which are definable in the given system.

Things become of course even more complicated for the systems G_{n}A^{ω}+ AC-qf +Δ instead of EA^{2}+ AC^{0,0}-qf which we are treating in this paper. In particular we show the following result:

4Both aspects are not taken into account appropriately in [21] where Π_{k}^{0}-CA^{−} and Π_{k}^{0}-AC^{−} are studied systematically for the first time. As a consequence of this, theorems 5.8,5.13 and corollaries 5.9,5.14 in [21] are not correct (see [11] and in particular chapter 12 of [10] for a thorough investigation of this matter).

Let t, ξ_{1}, ξ_{2} be closed terms of G_{n}A^{ω} and B :≡ ∀u^{1}∀v ≤_{τ} tu B_{ar}(u, v) a sentence of G_{n}A^{ω} where B_{ar}(u, v) ∈ Π_{∞}^{0}. Then for every k ∈ IN the following rule holds

If

G_{n}A^{ω} + AC-qf + Δ ⊢

∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv) → B_{ar}(u, v))

then

G_{n}A^{ω} + Σ_{k}^{0}-IA + Δ̃ + Mon(B) ⊢ ∀u^{1}∀v ≤_{τ} tu B_{ar}(u, v),

where Mon(B) expresses that B is monotone in the sense of definition 2.3 below and Δ̃ := {∃Y^{ρδ} ≤ s∀x^{δ}, z^{γ}A_{0}(x, Y x, z) : ∀x^{δ}∃y ≤_{ρ} sx∀z^{γ}A_{0}(x, y, z) ∈ Δ}. (Δ and consequently Δ̃ may be empty).

If B_{ar} ∈ Π_{k+2}^{0}, then the monotonicity assumption Mon(B) can be avoided, i.e. the conlusion can be strengthened to

G_{n}A^{ω} + Σ_{k}^{0}-IA + Δ̃ ⊢ ∀u^{1}∀v ≤_{τ} tu B_{ar}(u, v).

These results will be used also to prove new conservation results for EA +Π_{k}^{0}-CP over EA +Σ_{k}^{0}-IA which strengthen the Friedman-Paris-Kirby result.^{5}

Finally we consider generalizations Π_{k}^{0}-UB^{−}|^{\} of the principle of uniform Σ_{1}^{0}- boundedness Σ_{1}^{0}-UB^{−} which was studied in [12].^{6} In [14] we showed that Σ_{1}^{0}-UB^{−} proves already relative to G_{2}A^{ω}+ AC-qf many important analytical theorems (like Dini’s theorem, the attainment of the maximum for f ∈ C([0, 1]^{d}, IR), the sequential Heine-Borel property for [0, 1]^{d}, the existence of an inverse function for every strictly monotone function f ∈ C[0, 1] and others) but does not contribute to the growth of extractable bounds, thereby guaranteing the extractability of polynomial bounds when applied in the context of G_{2}A^{ω}+ AC-qf.

5A proof-theoretic treatment of the Friedman-Paris-Kirby result was first given in [21].

However the proof in [21] contains a serious gap. See [1] for a correction of Sieg’s proof.

Another proof-theoretic treatment can be found in [3].

6Whereas we generally use the superscript ‘−’ to denote the restriction S^{−} of a schema S to function parameter-free instances of S, this superscript has a different meaning in the context of principles of uniform boundedness. Although this might be troublesome we wish to stick to the notation for these principles from [12] where they were introduced.

Whereas the straightforward generalization of Σ_{1}^{0}-UB^{−} to Π_{k}^{0}-formulas is inconsistent with G_{2}A^{ω} already for k = 1, our restricted version Π_{k}^{0}-UB^{−}|^{\} ( introduced in the present paper) is consistent. In [15] we implicitly used (a special case of) Π_{1}^{0}-UB^{−}|^{\} to prove the Bolzano-Weierstraß principle and the Ascoli-lemma and it were these proofs which were used to calibrate faithfully the arithmetical strength of these principles.

One of the results on Π_{k}^{0}-UB^{−}|^{\} to be proved in the present paper is that we may strengthen the assumption of the rule stated above by adding Π_{k}^{0}-UB^{−}|^{\}(ξ_{3}uv) to Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv).

2 Monotone formulas and their Skolem normal forms

In this section we review some of the proof-theoretic tools from [13] on which the present paper is based and also recall some of the basic concepts and definitions from [12]. The set T of all finite types is defined inductively by

(i) 0 ∈ T and (ii) ρ, τ ∈ T ⇒ τ(ρ) ∈ T.

Terms which denote a natural number have type 0. Elements of type τ(ρ) are functions which map objects of type ρ to objects of type τ. The set P ⊂ T of pure types is defined by

(i) 0 ∈ P and (ii) ρ ∈ P ⇒ 0(ρ) ∈ P.

Brackets whose occurrences are uniquely determined are often omitted, e.g. we write 0(00) instead of 0(0(0)). Furthermore we write for short τρ_{k} … ρ_{1} instead of τ(ρ_{k}) … (ρ_{1}). Pure types can be represented by natural numbers: 0(n) := n + 1. The types 0, 00, 0(00), 0(0(00)) … are so represented by 0, 1, 2, 3 . . .. For arbitrary types ρ ∈ T the degree of ρ (for short deg(ρ) ) is defined by deg(0) := 0 and deg(τ(ρ)) := max(deg(τ),deg(ρ) + 1). For pure types the degree is just the number which represents this type.

Description of the theories (E)–G_{n}A^{ω}

Our theories T^{ω} used in this paper are based on many–sorted classical logic formulated in the language of all finite types plus the combinators Π_{ρ,τ}, Σ_{δ,ρ,τ} which allow the definition of λ–abstraction. T_{i}^{ω} denotes the intuitionistic variant of T^{ω}. The systems G_{n}A^{ω} (for all n ≥ 1) are introduced in [12] to which we refer for details. G_{n}A^{ω} has as primitive relations =_{0}, ≤_{0} for objects of type 0, the constant 0^{0}, functions min_{0}, max_{0}, S^{00} (successor), A_{0}, …, A_{n}, where A_{i} is the i–th branch of the Ackermann function (i.e. A_{0}(x, y) = y′, A_{1}(x, y) = x + y, A_{2}(x, y) = x · y, A_{3}(x, y) = x^{y}, …), functionals of type level 2: Φ_{1}, …, Φ_{n}, where Φ_{1}fx = max_{0}(f0, …, fx) and Φ_{i} is the iteration of A_{i−1} on the f–

values for i ≥ 2, i.e. Φ_{2}fx = ∑_{i=0}^{x} fi, Φ_{3}fx = ∏_{i=0}^{x} fi, . . .. We also have a

bounded search functional μ_{b} and bounded predicative recursion provided by recursor constants R̃_{ρ} (where ‘predicative’ means that recursion is possible only at the type–0–level as in the case of the (unbounded) Kleene-Feferman recursors R̂_{ρ}). Moreover G_{n}A^{ω} contains a quantifier-free rule of extensionality QF–ER. In addition to the defining axioms for the constants of our theories all true sentences having the form ∀x^{ρ}A_{0}(x), where A_{0} is quantifier–free and deg(ρ) ≤ 2, are added as axioms. By ‘true’ we refer to the full set–theoretic model S^{ω}. In given proofs however only very special universal axioms will be used which can be proved in suitable extensions of our theories. Nevertheless we include them all as axioms in order to emphasize that (proofs of) universal sentences do not contribute to the growth of extractable bounds. In particular this covers all instances of the schema of quantifier-free induction (The main results in this paper are also valid for the variant of G_{n}A_{i}^{ω} where the universal axioms are replaced by the schema of quantifier–free induction). The restriction deg(ρ) ≤ 2 has a technical reason discussed in [12].

G_{∞}A^{ω} := ⋃_{n∈IN} G_{n}A^{ω}.

PA^{ω}, PA_{i}^{ω} are the extensions of G_{n}A^{ω}, G_{n}A_{i}^{ω} obtained by the addition of the schema of full induction and all (impredicative) primitive recursive functionals in the sense of [5]. E–T_{(i)}^{ω} denotes the theory which results from T_{(i)}^{ω} when the quantifier–free rule of extensionality is replaced by the axioms of extensionality (E)

∀x^{ρ}, y^{ρ}, z^{τρ}(x =_{ρ} y → zx =_{τ} zy)

for all finite types (x =_{ρ} y is defined as ∀z_{1}^{ρ_{1}}, …, z_{k}^{ρ_{k}}(xz_{1} … z_{k} =_{0} yz_{1} … z_{k}) where ρ = 0ρ_{k} … ρ_{1}). G_{n}R^{ω} and T denote the sets of all closed terms of (E)–G_{n}A_{(i)}^{ω} and (E)–PA_{(i)}^{ω}. T_{k} is the subset of all closed terms of T which contain the Gödel-recursors R_{ρ} for ρ of type level ≤ k only.

Definition 2.1 Between functionals of type ρ we define relations ≤_{ρ} (‘less or equal’) and s–maj_{ρ} (‘strongly majorizes’) by induction on the type:

\{ \begin{matrix}x_{1} ≤_{0} x_{2} :≡ (x_{1} ≤_{0} x_{2}), \\ x_{1} ≤_{τρ} x_{2} :≡ ∀y^{ρ}(x_{1}y ≤_{τ} x_{2}y); \end{matrix}

x^{∗} s–maj_{0} x :≡ x^{∗} ≥_{0} x,
x^{∗} s–maj_{τρ} x :≡ ∀y^{∗ρ}, y^{ρ}(y^{∗} s–maj_{ρ} y → x^{∗}y^{∗} s–maj_{τ} x^{∗}y, xy).

Remark 2.2 ‘s–maj’ is a variant of W.A. Howard’s relation ‘maj’ from [6] which is due to [2]. For more details see [8].

Let A(\underline{a}) be a formula of G_{n}A^{ω} (\underline{a} are all free variables of A) and ∃\underline{x}∀\underline{y}A_{D}(\underline{x}, \underline{y}, \underline{a}) its Gödel functional interpretation (see e.g. [24] for details on Gödel’s functional interpretation). We say that a tuple of closed terms \underline{t} realizes the monotone functional interpretation of A(\underline{a}) if^{7}

(∗) ∃\underline{x}(\underline{t} s-maj \underline{x} ∧ ∀\underline{a}, \underline{y} A_{D}(\underline{x} \underline{a}, \underline{y}, \underline{a}))

(Monotone functional interpretation which directly extracts a tuple \underline{t} satisfying (∗) from a proof of A(\underline{a}) was introduced in [9]. See also [12] for details.)

Definition 2.3 ([13]) Let A ∈ L(G_{n}A^{ω}) be a formula having the form

A ≡ ∀u^{1}∀v ≤_{τ} tu∃y_{1}^{0}∀x_{1}^{0} … ∃y_{k}^{0}∀x_{k}^{0}∃w^{γ}A_{0}(u, v, y_{1}, x_{1}, …, y_{k}, x_{k}, w),

where A_{0} is quantifier–free and contains only u, v, \underline{y}, \underline{x}, w free, t ∈ G_{n}R^{ω} and τ, γ are arbitrary finite types.

1) A is called (arithmetically) monotone if

\begin{matrix}Mon(A) :≡ \\ \{ & \begin{matrix}∀u^{1}∀v ≤_{τ} tu∀x_{1}, x̃_{1}, …, x_{k}, x̃_{k}, y_{1}, ỹ_{1}, … y_{k}, ỹ_{k} \\ ( ⋀_{i=1}^{k}(x̃_{i} ≤_{0} x_{i} ∧ ỹ_{i} ≥_{0} y_{i}) ∧ ∃w^{γ}A_{0}(u, v, y_{1}, x_{1}, …, y_{k}, x_{k}, w) \\ → ∃w^{γ}A_{0}(u, v, ỹ_{1}, x̃_{1}, …, ỹ_{k}, x̃_{k}, w)). \end{matrix} \end{matrix}

7Here \underline{t} s-maj \underline{x} means ⋀_{i}(t_{i} s-maj x_{i}).

2) The Herbrand normal form A^{H} of A is defined to be

A^{H} :≡ ∀u^{1}∀v ≤_{τ} tu∀h_{1}^{ρ_{1}}, …, h_{k}^{ρ_{k}}∃y_{1}^{0}, …, y_{k}^{0}, w^{γ}

\underbrace{A_{0}(u, v, y_{1}, h_{1}y_{1}, …, y_{k}, h_{k}y_{1} … y_{k}, w)}_{A_{0}^{H}:≡},

where ρ_{i} = 0 \underbrace{(0) … (0)}_{i}.

Remark 2.4 In definition 2.3 (and theorems 2.5,2.7 below) one may also have tuples ‘∃\underline{w}’ instead of ‘∃w^{γ}’ in A where \underline{w} = w_{1}^{γ_{1}}, …, w_{l}^{γ_{l}} and γ_{i} is arbitrary. Also instead of ∀u^{1} we may have ∀\underline{u} where \underline{u} = u_{1}^{ρ_{1}}, …, u_{q}^{ρ_{q}} with deg(ρ_{i}) ≤ 1 for 1 ≤ i ≤ q. In particular we can consider an innermost existential number quantifier ∃y_{k+1}^{0} as part of ∃\underline{w} and an outermost universal number quantifier ∀x_{0}^{0} as part of ∀\underline{u}. So for ∀x_{0}^{0} and ∃y_{k+1}^{0} no monotonicity is required in definition 2.3.1). Theorem 2.5 ([13]) Let n ≥ 1 and Ψ_{1}, …, Ψ_{k} ∈ G_{n}R^{ω}. Then

G_{n}A^{ω} + Mon(A) ⊢ ∀u^{1}∀v ≤_{τ} tu∀h_{1}, …, h_{k}( ⋀_{i=1}^{k}(h_{i} monotone)

→ ∃y_{1} ≤_{0} Ψ_{1}u\underline{h} … ∃y_{k} ≤_{0} Ψ_{k}u\underline{h}∃w^{γ}A_{0}^{H}) → A,

where (h_{i} monotone) :≡ ∀x_{1}, …, x_{i}, y_{1}, …, y_{i}( ⋀_{j=1}^{i}(x_{j} ≥_{0} y_{j}) → h_{i}\underline{x} ≥_{0} h_{i}\underline{y}).

Definition 2.6 (Bounded choice) b–AC:= ⋃_{δ,ρ∈T} {(b–AC^{δ,ρ})} denotes the schema of bounded choice

(b–AC^{δ,ρ}) : ∀Z^{ρδ}(∀x^{δ}∃y ≤_{ρ} Zx A(x, y, Z) → ∃Y ≤_{ρδ} Z∀xA(x, Y x, Z)). In general G_{n}A^{ω} ⊢ A^{H} does not imply G_{n}A^{ω} ⊢ A (see [13] for a detailed discussion of this phenomenon), which is in contrast to the first-order case where the derivability of A^{H} follows from that of A by Herbrand’s theorem (see [20]). If however A is monotone then this rule is valid also for G_{n}A^{ω} (but for very different reasons): Theorem 2.7 ([13]) Let A be as in thm.2.5 and Δ be a set of sentences ∀x^{δ}∃y ≤_{ρ} sx∀z^{η}G_{0}(x, y, z) where s is a closed term of G_{n}A^{ω} and G_{0} a quantifier-free formula, and let A′ denote the negative translation^{8} of A. Then the following rule holds:

G_{n}A^{ω}+AC–qf + Δ ⊢ A^{H} ∧ Mon(A) ⇒

G_{n}A^{ω} + Δ̃ ⊢ A, and by monotone functional interpretation one can

extract a tuple \underline{Ψ} ∈ G_{n}R^{ω} such that

G_{n}A_{i}^{ω} + Δ̃ ⊢ \underline{Ψ} satisfies the monotone functional interpretation of A′,

where Δ̃ := {∃Y ≤_{ρδ} s∀x^{δ}, z^{η}G_{0}(x, Y x, z) : ∀x^{δ}∃y ≤_{ρ} sx∀z^{η}G_{0}(x, y, z) ∈ Δ}. (In particular the second conclusion can be proved in G_{n}A_{i}^{ω} + Δ+ b-AC). The weakened conclusion G_{n}A^{ω} + Δ̃ + Mon(A) ⊢ A follows already from G_{n}A^{ω}+ AC-qf +Δ ⊢ A^{H}.^{9}

3 Making arithmetical comprehension monotone

In this section we consider the arithmetical content of instances Π_{k}^{0}-CA(ξuv) of Π_{k}^{0}-CA which are used in given proofs of sentences ∀u^{1}∀v ≤_{τ} tu B_{ar}(u, v) as discussed in the introduction.

Definition 3.1

Π_{k}^{0}-CA(f) :≡ ∃g^{1}∀x^{0}(gx =_{0} 0 ↔ ∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(x, \underline{u}) =_{0} 0)).^{10}

Remark 3.2 There is no need here to incorporate closure under number parameters in the definition of Π_{k}^{0}-CA(f), i.e. by defining

Π_{k}^{0}-CA(f) :≡ ∀l^{0}∃g^{1}∀x^{0}(gx =_{0} 0 ↔ ∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, x, \underline{u}) =_{0} 0)),

since the latter can be reduced to the former (relative to G_{n}A^{ω} for n ≥ 2) by coding l, x together and applying comprehension without number parameters to this pair.

8Here we can use Gödel’s [4] translation or any other of the various negative translations. For a systematical treatment of negative translations see [16].

9This last assertion is not stated in the formulation of the theorem in [13] but does follow immediately from its proof.

10Whether one has here ‘∃u_{k}^{0}’ or ‘∀u_{k}^{0}’ depends of course on whether k is even or odd.

In order to be able to apply the method of elimination of Skolem functions for monotone formulas from section 2 we follow this strategy: Construct an arithmetical principle A_{ar}(f) such that for suitable ξ_{1}, ξ_{2} ∈ G_{n}R^{ω}:

1) G_{n}A^{ω} ⊢ Mon(∀f A_{ar}(f)),

2) G_{n}A^{ω} ⊢ ∀f(A_{ar}^{S}(ξ_{1}f) → Π_{k}^{0}-CA(f)) and

3) G_{n}A^{ω} ⊢ ∀f(Π_{k}^{0}-CA(ξ_{2}f) → A_{ar}(f)). Because of 2) the use of Π_{k}^{0}-CA(ξuv) in a given proof of a monotone sentence ∀u^{1}∀v ≤_{τ} tu B_{ar}(u, v) can be reduced to the use of A_{ar}^{S}(ξ′uv) (where ξ′uv := ξ_{1}(ξuv)) which in turn (by 1) and theorem 2.7) can be reduced to the use of A_{ar}(ξ′uv). Because of 3) nothing is lost by this reduction. It will turn out that the correct principle A_{ar}(f) is a ‘monotone version’ Π_{k}^{0}-TND^{mon}(f) of the tertium-non-datur principle for Π_{k}^{0}-formulas. Definition 3.3 In the following m := \frac{k}{2} if k is even (resp. m := \frac{k−1}{2} if k is odd).

1) The Π_{k}^{0}-tertium-non-datur axiom is given by the following formula (where f is a function variable of appropriate type)^{11}

\begin{matrix}\underline{Π_{k}^{0}-TND} (f) :≡ \\ \{ & \begin{matrix}∀x^{0}(∀y_{1}^{0}∃z_{1}^{0} … ∀y_{m}^{0}∃z_{m}^{0}(∀y_{m+1}^{0})(f(x, y_{1}, z_{1}, …, y_{m}, z_{m}, (y_{m+1})) =_{0} 0) \\ ∨∃u_{1}^{0}∀v_{1}^{0} … ∃u_{m}^{0}∀v_{m}^{0}(∃u_{m+1}^{0})(f(x, u_{1}, v_{1}, …, u_{m}, v_{m}, (u_{m+1})) ≠ 0)), \end{matrix} \end{matrix}

2) We also need the following prenex normal form of Π_{k}^{0}-TND (f):

\begin{matrix}\underline{Π_{k}^{0}-TND} (f)^{pr} :≡ \\ \{ & \begin{matrix}∀x^{0}∃u_{1}^{0}∀y_{1}^{0}∃z_{1}^{0}∀v_{1}^{0} … ∃u_{m}^{0}∀y_{m}^{0}∃z_{m}^{0}∀v_{m}^{0}(∃u_{m+1}^{0}∀y_{m+1}^{0}) \\ (f(x, y_{1}, z_{1}, …, y_{m}, z_{m}, (y_{m+1})) =_{0} 0∨ \\ f(x, u_{1}, v_{1}, …, u_{m}, v_{m}, (u_{m+1})) ≠ 0), \end{matrix} \end{matrix}

11Here and in the following the quantifiers ∀y_{m+1}^{0}, ∃u_{m+1}^{0} are only present if k is odd.

3) The Skolem normal form of Π_{k}^{0}-TND (f)^{pr} is given by

\begin{matrix}\underline{(Π_{k}^{0}-TND (f)^{pr})^{S}} :≡ \\ \{ & \begin{matrix}∃h_{1}, …, h_{m}, (h_{m+1}), g_{1}, …, g_{m}∀x^{0}, y_{1}^{0}, v_{1}^{0}, …, y_{m}^{0}, v_{m}^{0}, (y_{m+1}) \\ (f(x, y_{1}, g_{1}(x, y_{1}), …, y_{m}, g_{m}(x, y_{1}, …, y_{m}, v_{1}, …, v_{m−1}), (y_{m+1})) =_{0} 0∨ \\ f(x, h_{1}x, v_{1}, …, h_{m}(x, y_{1}, …, y_{m−1}, v_{1}, …, v_{m−1}), v_{m}, \\ (h_{m+1}(x, y_{1}, …, y_{m}, v_{1}, …, v_{m}))) ≠ 0). \end{matrix} \end{matrix}

Remark 3.4 For n ≥ 2 we have coding of finite tuples (of fixed length) available in G_{n}A^{ω}. Hence quantifier-blocks can be contracted to a single quantifier. Since in all of our results we assume that (at least) n ≥ 2, it is no restriction in the definition above to consider only single quantifiers.

Lemma 3.5 For every k ∈ IN the following implication can be proved in G_{1}A^{ω}:

∀f((Π_{k}^{0}-TND (f)^{pr})^{S} → Π_{k}^{0}-CA (f)).

Proof: For notational simplicity we confine ourselves to the case k = 4 which well shows the general pattern of the proof for arbitrary k: (Π_{4}^{0}-TND(f)^{pr})^{S} yields the existence of functions g_{1}, g_{2}, h_{1}, h_{2} such that

(1) \{ \begin{matrix}∀x, y_{1}, v_{1}, y_{2}(f(x, y_{1}, g_{1}(x, y_{1}), y_{2}, g_{2}(x, y_{1}, y_{2}, v_{1})) = 0 \\ ∨∀v_{2}(f(x, h_{1}x, v_{1}, h_{2}(x, y_{1}, v_{1}), v_{2}) ≠ 0)). \end{matrix}

(1) in turn yields

(2) \{ \begin{matrix}∀x, y_{1}, v_{1}(∀y_{2}∃z_{2}f(x, y_{1}, g_{1}(x, y_{1}), y_{2}, z_{2}) = 0 \\ ∨∀v_{2}(f(x, h_{1}x, v_{1}, h_{2}(x, y_{1}, v_{1}), v_{2}) ≠ 0)), \end{matrix}

(3) \{ \begin{matrix}∀x, y_{1}, v_{1}(∀y_{2}∃z_{2}f(x, y_{1}, g_{1}(x, y_{1}), y_{2}, z_{2}) = 0 \\ ∨∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0)), \end{matrix}

(4) \{ \begin{matrix}∀x, y_{1}(∀y_{2}∃z_{2}f(x, y_{1}, g_{1}(x, y_{1}), y_{2}, z_{2}) = 0 \\ ∨∀v_{1}∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0)), \end{matrix}

(5) \{ \begin{matrix}∀x, y_{1}(∃z_{1}∀y_{2}∃z_{2}f(x, y_{1}, z_{1}, y_{2}, z_{2}) = 0 \\ ∨∀v_{1}∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0)) \end{matrix}

and finally

(6) ∀x(∀y_{1}∃z_{1}∀y_{2}∃z_{2}f(x, y_{1}, z_{1}, y_{2}, z_{2}) = 0∨∀v_{1}∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0)).

(1) applied to y_{1} := h_{1}x, v_{1} := g_{1}(x, h_{1}x), y_{2} := h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)) gives (∗) :≡ ∀x^{0}(f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), g_{2}(x, h_{1}x, h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)),

g_{1}(x, h_{1}x))) = 0∨∀v_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), v_{2}) ≠ 0)).

We now show (+) :≡ ∀x^{0}(f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), g_{2}(x, h_{1}x, h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), g_{1}(x, h_{1}x))) = 0 ↔ ∀y_{1}∃z_{1}∀y_{2}∃z_{2}(f(x, y_{1}, z_{1}, y_{2}, z_{2}) = 0)). (+) yields the claim of the lemma with

\begin{matrix}gx := Φxh_{1}h_{2}g_{1}g_{2} := \\ \{ & \begin{matrix}f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), \\ g_{2}(x, h_{1}x, h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), g_{1}(x, h_{1}x))). \end{matrix} \end{matrix}

Proof of (+): ‘→’: Φxfh_{1}h_{2}g_{1}g_{2} = 0 implies

¬∀v_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), v_{2}) ≠ 0).

Hence by (2) (putting y_{1} := h_{1}x, v_{1} := g_{1}(x, h_{1}x))

∀y_{2}∃z_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), y_{2}, z_{2}) = 0)

and therefore

∃z_{1}∀y_{2}∃z_{2}(f(x, h_{1}x, z_{1}, y_{2}, z_{2}) = 0),

i.e.

¬∀v_{1}∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0).

By (6) this implies

∀y_{1}∃z_{1}∀y_{2}∃z_{2}(f(x, y_{1}, z_{1}, y_{2}, z_{2}) = 0).

‘←’: Φxfh_{1}h_{2}g_{1}g_{2} ≠ 0 implies by (∗)

∀v_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), h_{2}(x, h_{1}x, g_{1}(x, h_{1}x)), v_{2}) ≠ 0)

and therefore

∃u_{2}∀v_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), u_{2}, v_{2}) ≠ 0),

i.e.

¬∀y_{2}∃z_{2}(f(x, h_{1}x, g_{1}(x, h_{1}x), y_{2}, z_{2}) = 0).

By (4) this yields (putting y_{1} := h_{1}x)

∀v_{1}∃u_{2}∀v_{2}(f(x, h_{1}x, v_{1}, u_{2}, v_{2}) ≠ 0)

and therefore

∃u_{1}∀v_{1}∃u_{2}∀v_{2}(f(x, u_{1}, v_{1}, u_{2}, v_{2}) ≠ 0),

which concludes the proof of (+) and hence of the lemma.

Definition 3.6 For a Π_{k}^{0}-formula A(\underline{a}) ≡ ∀x_{1}^{0}∃x_{2}^{0} … ∃^{(d)}x_{k}^{0}A_{0}(\underline{a}, x_{1}, x_{2}, …, x_{k}) of G_{n}A^{ω} (where \underline{a} are all free variables of A which may have arbitrary type) we define Ã(\underline{a}) :≡ ∀x_{1}^{0}∃x_{2}^{0} … ∃^{(d)}x_{k}^{0}∀x̃_{1} ≤ x_{1}∃x̃_{2} ≤ x_{2} … ∃^{(d)}x̃_{k} ≤ x_{k}A_{0}(\underline{a}, x̃_{1}, x̃_{2}, …, x̃_{k}).

In the following we need a variant Mon^{∗} of Mon where monotonicity is required for all number quantifiers (compare this with remark 2.4):

Definition 3.7 Let A(\underline{a}) :≡ ∀x_{1}^{0}∃y_{1}^{0} … ∀x_{k}^{0}∃y_{k}^{0}A_{0}(\underline{a}, x_{1}, y_{1}, …, x_{k}, y_{k}).^{12} Then

\begin{matrix}Mon^{∗}(A(\underline{a})) :≡ ∀x_{1}, x̃_{1}, y_{1}, ỹ_{1}, …, x_{k}, x̃_{k}, y_{k}, ỹ_{k}( ⋀_{i=1}^{k}(x̃_{i} ≤_{0} x_{i} ∧ ỹ_{i} ≥_{0} y_{i}) → \\ (A_{0}(\underline{a}, x_{1}, y_{1}, …, x_{k}, y_{k}) → A_{0}(\underline{a}, x̃_{1}, ỹ_{1}, …, x̃_{k}, ỹ_{k})). \end{matrix}

Lemma 3.8 For Ã(\underline{a}) as in the previous definition we have

G_{n}A^{ω} ⊢ Mon^{∗}(Ã(\underline{a})).

Proof: Trivial.

The Π_{k}^{0}-collection principle is the schema

\underline{Π_{k}^{0}-CP} : ∀x ≤_{0} a∃y^{0}A(x, y) → ∃z^{0}∀x ≤_{0} a∃y ≤_{0} z A(x, y),

for all Π_{k}^{0}-formulas A(x, y).

12Here the quantifiers ∀x_{1}^{0} and ∃y_{k}^{0} may be empty (‘dummy’) quantifiers.

Convention 3.9 In Π_{k}^{0}-CP (and other axiom schemas which we will consider below) A(x, y) may contain arbitrary parameters (besides x, y) of the language we consider. E.g. if we write G_{n}A^{ω} + Π_{k}^{0}-CP then instances of Π_{k}^{0}-CP may contain parameters of arbitrary type. In EA +Π_{k}^{0}-CP however (where EA denotes first-order elementary recursive arithmetic) instances of Π_{k}^{0}-CP of course contain only number parameters.

Π_{k}^{0}-CP is equivalent over many systems (e.g. G_{n}A^{ω} for n ≥ 3) to the axiom schema of finite choice for Π_{k}^{0}-formulas

\underline{Π_{k}^{0}-FAC} : ∀x ≤_{0} a∃y^{0}A(x, y) → ∃z^{0}∀x ≤_{0} a A(x, (z)_{x}),

for all Π_{k}^{0}-formulas A(x, y) (with the convention stated above).

In the presence of function variables as in G_{n}A^{ω} the schema Π_{k}^{0}-CP can be expressed as a single second-order axiom ∀fΠ_{k}^{0}-CP(f), where

\underline{Π_{k}^{0}-CP(f)} :≡ \begin{cases}∀l^{0}, a^{0}(∀x ≤_{0} a∃y^{0}∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, a, x, y, \underline{u}) =_{0} 0) \\ → ∃z^{0}∀x ≤_{0} a∃y ≤_{0} z∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, a, x, y, \underline{u}) =_{0} 0)). \end{cases}

By incorporating the universal closure w.r.t. to arithmetical parameters ∀l^{0}, a^{0} in Π_{k}^{0}-CP(f), we achieve that the universal closure of every instance of Π_{k}^{0}-CP which contains only number parameters can be written as a sentence Π_{k}^{0}-CP(ξ) in G_{n}A^{ω} where ξ is a closed term (essentially the characteristic function of the quantifier-free matrix of the Π_{k}^{0}-formula A(x, y)) which will be of importance below.

The same is true for the principle of Σ_{k}^{0}-induction Σ_{k}^{0}-IA(f) which we need below:

\underline{Σ_{k}^{0}-IA(f)} :≡ \{ \begin{matrix}∀l^{0}(∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(l, 0, \underline{u}) =_{0} 0)∧ \\ ∀x^{0}(∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(l, x, \underline{u}) =_{0} 0) → \\ ∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(l, x′, \underline{u}) =_{0} 0)) \\ → ∀x^{0}∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(l, x, \underline{u}) =_{0} 0)). \end{matrix}

Lemma 3.10 Let A(\underline{a}), Ã(\underline{a}) be as in definition 3.6. Then for suitable ξ_{1}, … ξ_{l}, ξ̃_{1}, …, ξ̃l̃ ∈ G_{n}R^{ω} the following holds:

G_{n}A^{ω} ⊢ ⋀_{i=1}^{l} Π_{k−2}^{0}-CP(ξ_{i}\underline{a}) → (A(\underline{a}) → Ã(\underline{a}))

and

G_{n}A^{ω} ⊢ ⋀_{i=1}^{l̃} Π_{k−3}^{0}-CP(ξ̃_{i}\underline{a}) → (Ã(\underline{a}) → A(\underline{a}))

(Here and in the following we use the convention that Π_{k}^{0}-S is empty (i.e. ≡ (0 = 0) for an axiom schema S if k < 0). Proof: Induction on k: For k = 0, 1 the lemma is trivial. So let k ≥ 1. k ↦ k + 1 : Consider

A(\underline{a}) ≡ ∀x_{1}^{0}∃x_{2}^{0} … ∃^{(d)}x_{k+1}^{0}A_{0}(\underline{a}, x_{1}, x_{2}, …, x_{k+1}) ∈ Π_{k+1}^{0}.

By the induction hypothesis applied to the Π_{k}^{0}-formula

∀x_{2}∃x_{3} … ∀^{(d)}x_{k+1}¬A_{0}(\underline{a}, x_{1}, …, x_{k+1})

we have instances Π_{k−2}^{0}-CP(ξ_{i}\underline{a}) (note that instances of Π_{k−3}^{0}-CP can be considered as instance of Π_{k−2}^{0}-CP as well) such that ⋀_{i} Π_{k−2}^{0}-CP(ξ_{i}\underline{a}) implies (relative to G_{n}A^{ω}

\begin{matrix}∃x_{2}∀x_{3} … ∃^{(d)}x_{k+1}A_{0} ↔ \\ ∃x_{2}∀x_{3} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x_{2}∀x̃_{3} ≤ x_{3} … A_{0}(\underline{a}, x_{1}, x̃_{2}, …, x̃_{k+1}). \end{matrix}

Hence

A(\underline{a}) ↔ ∀x_{1}∃x_{2} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x_{2} … ∃^{(d)}x̃_{k+1} ≤ x_{k+1}A_{0}(\underline{a}, x_{1}, x̃_{2}, …, x̃_{k+1}) ↔ ∀x_{1}∀x̃_{1} ≤ x_{1}∃x_{2} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x_{2} … A_{0}(\underline{a}, x̃_{1}, x̃_{2}, …, x̃_{k+1})

→^{Π{0 \atop k−1}-CP (_{ξ}\underline{a})} ; (logic)^{←}

∀x_{1}∃x_{2}∀x̃_{1} ≤ x_{1}∃x̂_{2} ≤ x_{2}∀x_{3} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x̂_{2} …∃^{(d)}x̃_{k+1} ≤ x_{k+1}A_{0}(\underline{a}, ˜ \underline{x}) ↔ ∀x_{1}∃x_{2}∀x̃_{1} ≤ x_{1}∀x_{3} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x_{2} … ∃^{(d)}x̃_{k+1} ≤ x_{k+1}A_{0}(\underline{a}, ˜ \underline{x}) ↔ ∀x_{1}∃x_{2}∀x_{3}∀x̃_{1} ≤ x_{1}∃x_{4} … ∃^{(d)}x_{k+1}∃x̃_{2} ≤ x_{2} … ∃^{(d)}x̃_{k+1} ≤ x_{k+1}A_{0}(\underline{a}, ˜ \underline{x}).

In the same way as we shifted ∀x̃_{1} ≤ x_{1} over ∃x_{2} we now move ∀x̃_{1} ≤ x_{1} over ∃x_{4}, then permute ∀x̃_{1} ≤ x_{1} with ∀x_{5}, move over ∃x_{6} and so on until we obtain Ã(\underline{a}). This requires only Π_{k−3}^{0}-instances (or simpler ones) of CP which can be considered a fortiori as instances Π_{k−2}^{0}-CP(ζ_{j}\underline{a}). Putting things together we have shown that (relative to G_{n}A^{ω}):

Π_{k−1}^{0}-CP(ξ̂\underline{a}) ∧ ⋀_{i} Π_{k−2}^{0}-CP(ξ_{i}\underline{a}) ∧ ⋀_{j} Π_{k−2}^{0}-CP(ζ_{j}\underline{a}) → (A(\underline{a}) → Ã(\underline{a}))

and

⋀_{i} Π_{k−2}^{0}-CP(ξ_{i}\underline{a}) ∧ ⋀_{j} Π_{k−2}^{0}-CP(ζ_{j}\underline{a}) → (Ã(\underline{a}) → A(\underline{a})),

which concludes the proof of the lemma.

Since in our main results we assume n ≥ 2 or n ≥ 3 for the level n of G_{n}A^{ω} we also use for simplicity G_{2}A^{ω} in the following definition and lemmas although some of them can be carried out even in G_{1}A^{ω}.

Definition 3.11 (and lemma) For m ∈ IN let Φ ∈ G_{2}R^{ω} be such that

G_{2}A^{ω} ⊢ ∀f^{(0)...(0)}, x^{0}, y_{1}^{0}, z_{1}^{0}, …, y_{m}^{0}, z_{m}^{0}, (y_{m+1})
(Φfxy_{1}z_{1} … y_{m}z_{m}(y_{m+1}) =_{0} 0
↔ ∀ỹ_{1} ≤ y_{1}∃z̃_{1} ≤ z_{1} … ∀ỹ_{m} ≤ y_{m}∃z̃_{m} ≤ z_{m}(∀ỹ_{m+1} ≤ y_{m+1})
(f(x, ỹ_{1}, z̃_{1}, …, ỹ_{m}, z̃_{m}, (ỹ_{m+1})) =_{0} 0)).

We denote Φf by f′.

Lemma 3.12 Let k ≥ 1. There are (effectively) finitely many terms ξ_{1}, …, ξ_{l} ∈ G_{2}R^{ω} such that

G_{2}A^{ω} ⊢ ∀f(( ⋀_{i=1}^{l} Π_{k−2}^{0}-CP(ξ_{i}f)) → (Π_{k}^{0}-CA(f) ↔ Π_{k}^{0}-CA(f′))).

Proof: The lemma follows from lemma 3.10.

Definition 3.13 The ‘monotone’ tertium-non-datur is given by

\begin{matrix}\underline{Π_{k}^{0}-TND}^{mon}(f) :≡ \\ \{ & \begin{matrix}∀x^{0}∃u_{1}^{0}∀y_{1}^{0}∃z_{1}^{0}∀v_{1}^{0} … ∃u_{m}^{0}∀y_{m}^{0}∃z_{m}^{0}∀v_{m}^{0}(∃u_{m+1}^{0}∀y_{m+1}^{0})∀x̃ ≤ x \\ (f′(x̃, y_{1}, z_{1}, …, y_{m}, z_{m}, (y_{m+1})) =_{0} 0∨f′(x̃, u_{1}, v_{1}, …, u_{m}, v_{m}, (u_{m+1})) ≠ 0), \end{matrix} \end{matrix}

Lemma 3.14 1) G_{2}A^{ω} ⊢ ∀f((Π_{k}^{0}-TND^{mon}(f))^{S} → (Π_{k}^{0}-TND(f′)^{pr})^{S}).

2) G_{2}A^{ω} ⊢ ∀f(Mon^{∗}(Π_{k}^{0}-TND^{mon}(f))).

Proof: 1) follows by putting x̃ := x.

2) Follows immediately from the definition of Π_{k}^{0}-TND^{mon}(f).

Proposition 3.15 G_{2}A^{ω} ⊢ ∀f((Π_{k}^{0}-TND^{mon}(f))^{S} → Π_{k}^{0}-CA(f′)).

Proof: Lemmas 3.5 and 3.14.1.

Lemma 3.16 One can construct a ξ ∈ G_{2}R^{ω} such that

G_{2}A^{ω}+ AC^{0,0}-qf ⊢ ∀f(Π_{k}^{0}-CA(ξf) → Π_{k}^{0}-CP(f)).

Proof: Using Π_{k}^{0}-CA(ξf) for a suitable ξ ∈ G_{2}R^{ω} one can reduce Π_{k}^{0}-CP(f) to Π_{0}^{0}-CP which is provable in G_{2}A^{ω}+ AC^{0,0}-qf.

Proposition 3.17 For a suitable ξ ∈ G_{2}R^{ω} one has

G_{2}A^{ω}+ AC^{0,0}-qf ⊢ ∀f((Π_{k}^{0}-TND^{mon}(ξf))^{S} → Π_{k}^{0}-CA(f)).

Proof: Induction on k: k = 0, 1 : easy. Let k > 1 and lets assume that the proposition holds for all m < k. Π_{k−2}^{0}-CP(ξ_{i}f) denote the instances of Π_{k−2}^{0}-collection from lemma 3.12 which are needed to show

Π_{k}^{0}-CA(f) ↔ Π_{k}^{0}-CA(f′).

Let ξ̂ ∈ G_{2}R^{ω} be (using lemma 3.16) such that^{13}

(1)G_{2}A^{ω}+ AC^{0,0}-qf ⊢ Π_{k−2}^{0}-CA(ξ̂f) → (Π_{k}^{0}-CA(f) ↔ Π_{k}^{0}-CA(f′)).

By the induction hypothesis we have

(2) G_{2}A^{ω}+ AC^{0,0}-qf ⊢ ∀f((Π_{k−2}^{0}-TND^{mon}(ξ̃f))^{S} → Π_{k−2}^{0}-CA(f))

for a suitable ξ̃ ∈ G_{2}R^{ω}. So by proposition 3.15 (3) :≡

G_{2}A^{ω}+AC^{0,0}-qf ⊢ (Π_{k}^{0}-TND^{mon}(f))^{S}∧(Π_{k−2}^{0}-TND^{mon}(ξ̃(ξ̂f)))^{S} → Π_{k}^{0}-CA(f).

13Note that two instances Π_{k}^{0}-CA(ξ_{1}f) ∧ Π_{k}^{0}-CA(ξ_{2}f) can be coded together into one instance Π_{k}^{0}-CA(ξ_{3}f) in G_{2}A^{ω}.

Introducing dummy quantifiers, (Π_{k−2}^{0}-TND^{mon}(ξ̃(ξ̂f)))^{S} can be reduced to (Π_{k}^{0}-TND^{mon}(ξ^{∗}f))^{S} for a suitable ξ^{∗} ∈ G_{2}R^{ω}. Furthermore

(4) (Π_{k}^{0}-TND^{mon}(h))^{S} → (Π_{k}^{0}-TND^{mon}(f))^{S} ∧ (Π_{k}^{0}-TND^{mon}(g))^{S}

for

h(x, \underline{y}, \underline{z}) = \{ \begin{matrix}f(x̃, \underline{y}, \underline{z}) if x = 2x̃ \\ g(x̃, \underline{y}, \underline{z}) if x = 2x̃ + 1. \end{matrix}

Hence

(5) (Π_{k}^{0}-TND^{mon}(ξf))^{S} → (Π_{k}^{0}-TND^{mon}(f))^{S} ∧ (Π_{k}^{0}-TND^{mon}(ξ^{∗}f))^{S}

for a suitable ξ ∈ G_{2}R^{ω}. By (3) and (5) we have

G_{2}A^{ω}+ AC^{0,0}-qf ⊢ (Π_{k}^{0}-TND^{mon}(ξf))^{S} → Π_{k}^{0}-CA(f).

Lemma 3.18 Let k ≥ 1 and A ∈ Σ_{k−1}^{0}. Then

G_{3}A^{ω} + Σ_{k}^{0}-IA ⊢ ∀x^{0}∃u^{0}∀x̃ ≤_{0} x(∀y^{0}A(x̃, y) ∨ ∃ũ ≤ u¬A(x̃, ũ)).

Proof: Assume

(+) ∀u^{0}∃x̃ ≤ x(∃y¬A(x̃, y) ∧ ∀ũ ≤ uA(x̃, ũ)).

We show by induction on n:

(∗) ∀n∃u, x̃ \overbrace{( \begin{matrix}lth x̃ = n + 1 ∧ ⋀_{{i,j≤n \atop i≠j}} ((x̃)_{i} ≠ (x̃)_{j}∧ \\ ⋀_{i≤n} ((x̃)_{i} ≤ x) ∧ ∀i ≤ n∃ũ ≤ u¬A((x̃)_{i}, ũ) \end{matrix} )}^{G(n,u,x̃)}

(For n = x + 1 this obviously is contradictory and so ¬(+) is proved). n = 0: (+) applied to u := 0 yields an x_{0} ≤ x such that A(x_{0}, 0) and ∃y_{0}¬A(x_{0}, y_{0}). (∗) is now satisfied by taking x̃ := ⟨x_{0}⟩, u := y_{0}. n → n + 1: Let u, x̃ be such that (∗) is satisfied for n. By (+) there exists an x_{n+1} ≤ x such that ∃y_{n+1}¬A(x_{n+1}, y_{n+1}) and ∀ũ ≤ uA(x_{n+1}, ũ). By (∗) we have ∀i ≤ n∃ũ ≤ u¬A((x̃)_{i}, ũ). Hence ∀i ≤ n((x̃)_{i} ≠ x_{n+1}) and so û := max(u, y_{n+1}), x̂ := x̃ ∗ ⟨x_{n+1}⟩ satisfy G(n + 1, û, x̂). It remains to show that ∃u, x̃G(n, u, x̃) is equivalent to a Σ_{k}^{0}-formula:

Using Σ_{k−1}^{0}-CP, ∃ũ ≤ u¬A((x̃)_{i}, ũ) can be shown to be equivalent to a Π_{k−1}^{0}- formula. Since Σ_{k−1}^{0}-CP follows from Σ_{k}^{0}-IA, the whole proof can be carried out in G_{3}A^{ω} + Σ_{k}^{0}-IA.

In contrast to Π_{k}^{0}-TND(f) its monotone version Π_{k}^{0}-TND^{mon}(f) does not hold logically. However it can be proved using Σ_{k}^{0}-induction. More precisely the following proposition holds:

Proposition 3.19 Let k ≥ 1. There are finitely many instances Σ_{k}^{0}-IA(ξ_{i}f) such that

G_{3}A^{ω} ⊢ ∀f(( ⋀_{i=1}^{l} Σ_{k}^{0}-IA(ξ_{i}f)) → Π_{k}^{0}-TND^{mon}(f)).

Proof: By (the proof of) lemma 3.18 there are instances Σ_{k}^{0}-IA(ξ_{i}f) which prove (relatively to G_{3}A^{ω})

(∗) \{ \begin{matrix}∀x∃u_{1}∀x̃ ≤ x(∀y_{1}∃z_{1} … ∀y_{m}∃z_{m}(∀y_{m+1})(f′(x̃, y_{1}, z_{1}, …, y_{m}, z_{m}) = 0) \\ ∨∃ũ ≤ u_{1}∀v_{1} … ∃u_{m}∀v_{m}(∃u_{m+1})(f′(x̃, ũ, v_{1}, …, u_{m}, v_{m}) ≠ 0)) \end{matrix}

and therefore by the definition of f′ (which makes ∃ũ ≤ u_{1}∀v_{1} … ∃u_{m}∀v_{m}(∃u_{m+1})(f′(x̃, ũ, v_{1}, …, u_{m}, v_{m}, (u_{m+1})) ≠ 0) monotone w.r.t. ∃ũ)

\{ \begin{matrix}∀x∃u_{1}∀x̃ ≤ x(∀y_{1}∃z_{1} … ∀y_{m}∃z_{m}(∀y_{m+1})(f′(x̃, y_{1}, z_{1}, …, y_{m}, z_{m},) = 0) \\ ∨∀v_{1} … ∃u_{m}∀v_{m}(∃u_{m+1})(f′(x̃, u_{1}, v_{1}, …, u_{m}, v_{m},) ≠ 0)), \end{matrix}

which is equivalent to (∗∗) :≡

\{ \begin{matrix}∀x∃u_{1}∀y_{1}∀x̃ ≤ x∃z_{1}(∀y_{2} … ∀y_{m}∃z_{m}(∀y_{m+1})(f′(x̃, y_{1}, z_{1}, …, y_{m}, z_{m},) = 0) \\ ∨∀v_{1} … ∃u_{m}∀v_{m}(∃u_{m+1})(f′(x̃, u_{1}, v_{1}, …, u_{m}, v_{m},) ≠ 0)). \end{matrix}

By a suitable instance of Π_{k−1}^{0}-CP and the monotonicity of (∗∗) w.r.t. ∃z_{1} one can ‘shift’ ∀x̃ ≤ x over ∃z_{1}. Now one continues in this way until one obtains Π_{k}^{0}-TND^{mon}(f) which needs only suitable instances of Π_{l}^{0}-CP with l < k − 1 which can be considered as instances of Π_{k−1}^{0}-CP. All the instances of Π_{k−1}^{0}-CP used follow from suitable instances of Σ_{k}^{0}-IA.

Corollary 3.20 G_{3}A^{ω} ⊢ ∀f(Π_{k}^{0}-CA(ξf) → Π_{k}^{0}TND^{mon}(f)) for a suitable ξ ∈ G_{3}R^{ω}.

4 Conservation results for Π_{k}^{0}-AC(f) and Δ_{k}^{0}- CA(f, g)

We are now ready to determine the arithmetical content of instances Π_{k}^{0}- CA(ξuv) and even Π_{k}^{0}-AC(ξuv) and Δ_{k+1}^{0}-CA(ξuv) in proofs of monotone sentences (and without monotonicity assumption if the logical complexity is restricted). It turns out that this content is given by certain instances of Π_{k}^{0}-TND^{mon}. Definition 4.1

Π_{k}^{0}-AC(f) :≡ \{ \begin{matrix}∀l^{0}(∀x^{0}∃y^{0}∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, x, y, \underline{u}) =_{0} 0) \\ → ∃g^{1}∀x^{0}∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, x, gx, \underline{u}) =_{0} 0)) \end{matrix}

\begin{matrix}Δ_{k}^{0}-CA(f, g) :≡ \\ \{ & \begin{matrix}∀l^{0}(∀x^{0}([∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(f(l, x, \underline{u}) =_{0} 0) ↔ \\ ∃v_{1}^{0}∀v_{2}^{0} … ∀^{(d)}v_{k}^{0}(g(l, x, \underline{v}) =_{0} 0)]) \\ → ∃h^{1}∀x^{0}(gx =_{0} 0 ↔ ∀u_{1}∃u_{2} … ∃^{(d)}u_{k}(f(l, x, \underline{u}) =_{0} 0))) \end{matrix} \end{matrix}

Δ_{k}^{0}-CA(f) :≡ Δ_{k}^{0}-CA(j_{1}^{1}f, j_{2}^{1}f) for the projection functions j_{i}^{1} ∈ G_{2}R^{ω}.

Lemma 4.2 Let k ∈ IN. Then for suitable ξ_{1}, ξ_{2} ∈ G_{2}R^{ω}:

1) G_{2}A^{ω}+ AC^{0,0}-qf ⊢ ∀f(Π_{k}^{0}-CA(ξ_{1}f) → Π_{k}^{0}-AC(f)).

2) G_{2}A^{ω}+ AC^{0,0}-qf ⊢ ∀f(Π_{k}^{0}-CA(ξ_{2}f) → Δ_{k+1}^{0}-CA(f)).

Proof: Obvious.

Below we also need a certain ‘non-standard’ axiom F^{−}

\begin{matrix}F^{−} :≡ \\ ∀Φ^{2(0)}, y^{1(0)}∃y_{0} ≤_{1(0)} y∀k^{0}, z^{1}, n^{0}( ⋀_{i<_{0}n}(zi ≤_{0} yki) → Φk(\overline{z, n}) ≤_{0} Φk(y_{0}k)), \end{matrix}

where, for z^{ρ0}, (\overline{z, n})(k^{0}) :=_{ρ} zk, if k <_{0} n and := 0^{ρ}, otherwise. F^{−} does not hold in the full set-theoretic type-structure but can be eliminated from proofs of monotone sentences in our theories. This axiom was introduced and studied in [12] and implies the principle of uniform Σ_{1}^{0}- boundedness which was mentioned in the introduction and which will be generalized in section 5 below.

Proposition 4.3 Let n ≥ 2, k ≥ 0 and B :≡ ∀u^{1}∀v ≤_{τ} tu∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0} be a sentence in L(G_{n}A^{ω}), where B_{0} is quantifier-free and t ∈ G_{n}R^{ω}. Let ξ_{1}, ξ_{2} ∈ G_{n}R^{ω} (of suitable types) and Δ a set of sentences having the form ∀x^{δ}∃y ≤_{ρ} sx∀z^{η}A_{0} (A_{0} quantifier-free, s ∈ G_{n}R^{ω}). Then for a suitable ξ ∈ G_{n}R^{ω} the following holds: If G_{n}A^{ω} + Δ+ AC-qf ⊢ ∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv) → ∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}) then G_{n}A^{ω} + Δ̃ + Mon(B) ⊢

∀u^{1}∀v ≤_{τ} tu(Π_{k}^{0}-TND^{mon}(ξuv) → ∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}) and in particular G_{max(3,n)}A^{ω} + Σ_{k}^{0}-IA + Δ̃ + Mon(B) ⊢ ∀u^{1}∀v ≤_{τ} tu∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}. In the assumption of the rule the theory G_{n}A^{ω}+Δ+ AC-qf can be strengthened to^{14} (G_{n}A^{ω} + Δ+ AC-qf ) ⊕ F^{−}. Then in the first conclusion G_{n}A^{ω} must be replaced by G_{max(3,n)}A^{ω}.

Proof: By lemma 4.2, proposition 3.17 and the fact that two instances of Π_{k}^{0}-CA can be coded together into a single instance of Π_{k}^{0}-CA, there is a ξ ∈ G_{n}R^{ω} such that

G_{n}A^{ω}+ AC^{0,0}-qf

⊢ ∀u^{1}∀v ≤_{τ} tu((Π_{k}^{0}-TND^{mon}(ξuv))^{S} → Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv). So the assumption of the rule implies

(1) \{ \begin{matrix}G_{n}A^{ω}+ AC-qf + Δ ⊢ \\ ∀u^{1}∀v ≤_{τ} tu(Π_{k}^{0}-TND^{mon}(ξuv) → ∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}). \end{matrix}

By lemma 3.14.2) the prenexation^{15} A^{pr} :≡ ∀u^{1}∀v ≤_{τ} tu∃x∀u_{1}∃y_{1}∀z_{1}∃v_{1} … ∃a_{1}∀b_{1} … ∃w^{γ}(TND_{0}^{mon}(ξuv) → B_{0}) of^{16}

14Here ⊕ means that F^{−} must not be used in the proof of the premise of an application of the quantifier–free rule of extensionality QF–ER. G_{n}A^{ω} satisfies the deduction theorem w.r.t ⊕ but not w.r.t +.

15Note that A^{pr} is not completely in prenex normal form because of the universal quantifiers hidden in v ≤_{τ} tu. However it has

the form required in theorem 2.7 used below.

A :≡ ∀u^{1}∀v ≤_{τ} tu(Π_{k}^{0}-TND^{mon}(ξuv) → ∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0})

is monotone if B is:

G_{n}A^{ω} ⊢ Mon(B) → Mon(A^{pr}).

Now (1) implies

G_{n}A^{ω}+ AC-qf + Δ ⊢ (A^{pr})^{H}

and therefore using theorem 2.7

G_{n}A^{ω} + Δ̃ + Mon(B) ⊢ A^{pr} i.e.
G_{n}A^{ω} + Δ̃ + Mon(B) ⊢ A.

The second part of the claim in the proposition now follows from proposition 3.19. The proof above can be combined with the elimination procedure for F^{−} given in [12](thm.4.21) yielding the claim about adding F^{−}.

Corollary 4.4 Let k ≥ 1, γ ≤ 2 and ξ_{1}, ξ_{2} ∈ G_{n}R^{ω}. Then the following rule holds

G_{∞}A^{ω} + Δ+ AC-qf ⊢
∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv) → ∃w^{γ}B_{0}(u, v, w))
⇒ ∃Φ ∈ T_{k−1} such that
PA_{i}^{ω} + Δ̃ ⊢ ∀u^{1}∀v ≤_{τ} tu∃w ≤_{γ} Φu B_{0}(u, v, w).

Again we may strengthen the theory in the assumption of the rule above by ⊕F^{−}.

Proof: The corollary follows from proposition 4.3 by observing that the condition Mon(∀u^{1}∀v ≤_{τ} tu∃w^{γ}B_{0}) is empty and using the fact that G_{∞}A^{ω}+ Δ̃ + Σ_{k}^{0}-IA has a monotone functional interpretation as developed in [9] (via negative translation) in PA_{i}^{ω}+Δ̃ by terms ∈ T_{k−1}. The latter follows from the proof that the negative translation of Σ_{k}^{0}-IA has a functional interpretation in T_{k−1} (provable in (a subsystem of) PA_{i}^{ω}) as given in [19] and the fact that every (closed) term of T_{k−1} can be majorized (in the sense of definition 2.1) by a suitable term in T_{k−1} which follows from Howard’s proof of this fact for full T as given in [6].

16TND_{0}^{mon} denotes the quantifier-free matrix of (some prenex normal form of) Π_{k}^{0}- TND^{mon}.

Corollary 4.5 Let n ≥ 3 and A be a Π_{1}^{1}-sentence.

If E-G_{n}A^{ω}+ AC^{1,0}-qf +Δ_{k+1}^{0}-CA^{−} + Π_{k}^{0}-AC^{−}+WKL ⊢ A
then G_{n}A^{ω} + Σ_{k}^{0}-IA + Mon(A) ⊢ A.

Proof: Using the deduction theorem for E-G_{n}A^{ω}, the fact that E-G_{3}A^{ω}+ AC^{1,0}-qf +F^{−} proves WKL (see [12]) and the existence of characteristic terms ∈ G_{n}R^{ω} for quantifier-free formulas of E-G_{n}A^{ω} the assumption implies

E-G_{n}A^{ω}+AC^{1,0}-qf + F^{−} ⊢ ⋀_{i=1}^{l} (Δ_{k+1}^{0}-CA(ξ_{i})) ∧ ⋀_{j=1}^{l̃} (Π_{k}^{0}-AC(ξ̃_{j})) → A

for certain terms ξ_{i}, ξ̃_{j} ∈ G_{n}R^{ω} (corresponding to the universal closures of the instances of Δ_{k+1}^{0}-CA^{−} and Π_{k}^{0}-AC^{−} used in the proof).

For suitable ξ, ξ̃ ∈ G_{n}R^{ω} we have

G_{n}A^{ω} ⊢ Δ_{k+1}^{0}-CA(ξ) → ⋀_{i=1}^{l} (Δ_{k+1}^{0}-CA(ξ_{i}))

and

G_{n}A^{ω} ⊢ Π_{k}^{0}-AC(ξ̃) → ⋀_{j=1}^{l̃} (Π_{k}^{0}-AC(ξ̃_{j})).

Together with elimination of extensionality (see e.g. [16]) we obtain

(G_{n}A^{ω}+ AC^{1,0}-qf) ⊕ F^{−} ⊢ Δ_{k+1}^{0}-CA(ξ) ∧ Π_{k}^{0}-AC(ξ̃) → A.

The conclusion now follows from proposition 4.3.

Lemma 4.6 Let ∀u^{1}∀v ≤_{τ} tu A(u, v) be a sentence with A(u, v) ∈ Σ_{k+1}^{0}. Then one can construct a sentence ∀u^{1}∀v ≤_{τ} tuÃ(u, v) with Ã(u, v) ∈ Σ_{k+1}^{0} such that

1) G_{n}A^{ω} ⊢ Mon(∀u^{1}∀v ≤_{τ} tuÃ(u, v)),

2) G_{n}A^{ω} ⊢ ∀u^{1}∀v ≤_{τ} tu( ⋀_{i=1}^{l} Π_{k−2}^{0}-CP(ξ_{i}uv) → (A(u, v) → Ã(u, v))),

3) G_{n}A^{ω} ⊢ ∀u^{1}∀v ≤_{τ} tu( ⋀_{i=1}^{l̃} Π_{k−1}^{0}-CP(ξ̃_{i}uv) → (Ã(u, v) → A(u, v))),

where ξ_{i}, ξ̃_{j} ∈ G_{n}R^{ω} are suitable terms.

Proof: Lemmas 3.8,3.10.

Corollary 4.7 Let n ≥ 3, ∀u^{1}∀v ≤_{τ} tu A(u, v) be a sentence in G_{n}A^{ω} with A(u, v) ∈ Σ_{k+1}^{0}, t ∈ G_{n}R^{ω} and ξ_{1}, ξ_{2} ∈ G_{n}R^{ω} of suitable types. Then the following rule holds:

If G_{n}A^{ω} + Δ+ AC-qf ⊢
∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA (ξ_{1}uv) ∧ Π_{k}^{0}-AC (ξ_{2}uv) → A(u, v))
then G_{n}A^{ω} + Σ_{k}^{0}-IA + Δ̃ ⊢ ∀u^{1}∀v ≤_{τ} tu A(u, v).

We may strengthen the theory in the assumption of the rule above by ⊕F^{−}.

Proof: Let Ã be as in lemma 4.6. Π_{k−2}^{0}-CP(ξ_{i}uv) follows from a corresponding

instance Π_{k−2}^{0}-AC(ξ̂_{i}uv) of Π_{k−2}^{0}-AC which can be considered as an instance

Π_{k}^{0}-AC(ξ̂_{i}uv) of Π_{k}^{0}-AC. All these instances Π_{k}^{0}-AC(ξ̂_{i}uv) (i = 1, …, l) can be combined with Π_{k}^{0}-AC(ξ_{2}uv) into a single instance Π_{k}^{0}-AC(ξ̂_{2}uv). Hence the assumption of the corollary yields

G_{n}A^{ω} + Δ+ AC-qf ⊢
∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA (ξ_{1}uv) ∧ Π_{k}^{0}-AC (ξ̂_{2}uv) → Ã(u, v)).

The conclusion now follows from proposition 4.3, lemma 4.6 and the fact that G_{n}A^{ω} + Σ_{k}^{0}-IA ⊢ Π_{k−1}^{0}-CP.

Corollary 4.8 For n ≥ 3, E-G_{n}A^{ω}+ AC^{1,0}-qf +Δ_{k+1}^{0}-CA^{−} + Π_{k}^{0}-AC^{−} + W KL is conservative w.r.t. Π_{k+2}^{0}-sentences over G_{n}A^{ω} + Σ_{k}^{0}-IA^{−}.

Proof: The corollary follows from the proofs of corollary 4.5 and corollary 4.7.

Remark 4.9 Corollary 4.8 is optimal in the following sense. For every k there is a sentence A ∈ Π_{k+3}^{0} such that

G_{3}A^{ω} + Π_{k}^{0}-AC^{−} ⊢ A, but G_{3}A^{ω} + Σ_{k}^{0}-IA ⊢ / A.

Proof: There is a first-order instance A (i.e. without parameters of type level > 0) of Π_{k}^{0}-FAC which does not follow from Σ_{k}^{0}-IA relative to e.g. G_{3}A^{ω} (see [18]). It is clear that G_{3}A^{ω} + Π_{k}^{0}-AC^{−} ⊢ A. Since the universal closure of A can be shown to be equivalent to a Π_{k+3}^{0}-sentence in G_{3}A^{ω} + Σ_{k}^{0}-IA^{−} (and hence in G_{3}A^{ω} + Π_{k}^{0}-AC^{−}), the claim follows.

Corollary 4.10 Let ∀u^{1}∀v ≤_{τ} tu A(u, v) be a sentence with A(u, v) ∈ Σ_{k+2}^{0}. Then for n ≥ 3 the following rule holds:

If G_{n}A^{ω} + Δ+ AC-qf ⊢
∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA (ξ_{1}uv) ∧ Π_{k}^{0}-AC (ξ_{2}uv) → A(u, v))
then G_{n}A^{ω} + Π_{k}^{0}-CP + Δ̃ ⊢ ∀u^{1}∀v ≤_{τ} tu A(u, v).

We may strengthen the theory in the assumption of the rule above by ⊕F^{−}.

Proof: The corollary follows analogously to the proof of corollary 4.7 using lemma 4.6 for k + 1 instead of k and the well-known fact (see e.g. [18]) that G_{n}A^{ω} + Π_{k}^{0}-CP ⊢ Σ_{k}^{0}-IA.

Corollary 4.11 For n ≥ 3, E-G_{n}A^{ω}+ AC^{1,0}-qf +Δ_{k+1}^{0}-CA^{−} + Π_{k}^{0}-AC^{−} + W KL is conservative w.r.t. Π_{k+3}^{0}-sentences over G_{n}A^{ω} + Π_{k}^{0}-CP^{−}.

Proof: The corollary follows from corollary 4.10 analogously to the proof of corollary 4.8.

Let EA be Kalmar-elementary arithmetic EA (with number quantifiers) and let us consider the variant G_{n}A_{−}^{ω} of G_{n}A^{ω} where the arbitrary true universal axioms 9) from its definition in [12] are replaced by the schema of quantifierfree induction (with arbitrary parameters)^{17} only. The results above also hold for G_{n}A_{−}^{ω} since no other universal axioms from 9) were used. EA can be considered as a subsystem of G_{3}A_{−}^{ω} and the latter is conservative over the former. Hence we obtain the following corollaries for EA:

Corollary 4.12 Let A be an arbitrary sentence of EA. Then the following rule holds:

EA + Π_{k}^{0}-CP ⊢ A ⇒ EA + Σ_{k}^{0}-IA + Mon(A) ⊢ A.

In particular we have the following

Corollary 4.13 Let A, Ã be sentences from EA such that 1) EA +Π_{k}^{0}-CP ⊢ A → Ã,

17Or equivalently the second-order axiom of quantifier-free induction.

2) EA +Σ_{k}^{0}-IA ⊢ Ã → A and

3) EA +Σ_{k}^{0}-IA ⊢ Mon(Ã). Then EA +Π_{k}^{0}-CP ⊢ A implies EA +Σ_{k}^{0}-IA ⊢ A.

Combined with lemma 4.6 we finally obtain Corollary 4.14 (Paris-Kirby [17], H. Friedman) EA +Π_{k}^{0}-CP is Π_{k+2}^{0}-conservative over EA +Σ_{k}^{0}-IA.

5 Generalized principles of uniform bound-

edness and their arithmetical content

In the following we define a generalization of the principle of uniform Σ_{1}^{0}- boundedness Σ_{1}^{0}-UB^{−} which was studied in [12],[14],[15]:

Σ_{1}^{0}–UB^{−} :≡ \{ \begin{matrix}∀y^{1(0)}(∀k^{0}∀x ≤_{1} yk∃z^{0} A(x, y, k, z) → ∃χ^{1}∀k^{0}, x^{1}, n^{0} \\ ( ⋀_{i<_{0}n}(xi ≤_{0} yki) → ∃z ≤_{0} χk A((\overline{x, n}), y, k, z))), \end{matrix}

where A ≡ ∃l^{0}A_{0}(l) is a purely existential formula. Σ_{1}^{0}-UB^{−} follows from F^{−} relative to G_{n}A^{ω}+ AC^{1,0}-qf (for n ≥ 2). In G_{2}A^{ω} + Σ_{1}^{0}–UB^{−} and hence in G_{2}A^{ω} + F^{−}+AC^{1,0}–qf one can give very short and perspicuous proofs of various important analytical theorems like

• Every pointwise continuous function f : [0, 1]^{d} → IR is uniformly continuous

• The attainment of the maximum value of f ∈ C([0, 1]^{d}, IR) on [0, 1]^{d} • The sequential form of the Heine–Borel covering property for [0, 1]^{d} • Dini’s theorem

• The existence of a uniformly continuous inverse function for every strictly increasing continuous function f : [0, 1] → IR.

Since F^{−} does not contribute to the growth of extractable bounds one can extract polynomial bounds from proofs in G_{2}A^{ω} + Σ_{1}^{0}–UB^{−}+ AC-qf.

Whereas the straightforward generalization of Σ_{1}^{0}-UB^{−} to Π_{k}^{0}-formulas is not consistent with G_{n}A^{ω} (see [15]), the following restricted form is (although it does – like Σ_{1}^{0}-UB^{−} – not hold in the full set-theoretic type structure):

Definition 5.1 Let ρ = 0(0)(0)(1(0))(1), k ≥ 0.

Π_{k}^{0}-UB^{−}|^{\}(g) :≡ \{ \begin{matrix}∀Φ^{ρ}, y^{1(0)}, a^{0}(∀k^{0}∀x ≤_{1} yk∃z^{0}A(g, Φ(x, y, k, z), k, z, a) → \\ ∃χ^{1}∀k^{0}∀x ≤_{1} yk∀l^{0}∃z ≤_{0} χk A(g, Φ((\overline{x, l}), y, k, z), k, z, a)), \end{matrix}

where A(g, v^{0}, k^{0}, z^{0}, a^{0}) :≡ ∀u_{1}^{0}∃u_{2}^{0} … ∃^{(d)}u_{k}^{0}(g(v, k, z, a, \underline{u}) =_{0} 0) ∈ Π_{k}^{0}.

Remark 5.2 G_{n}A^{ω} ⊢ Π_{0}^{0}-UB^{−}|^{\}(t) → Σ_{1}^{0}-UB^{−}, where t ∈ G_{1}R^{ω} such that t(v, k, z, a) =_{0} v.

In [15] we have shown that every single (sequence of) instance(s) of the Bolzano-Weierstraß principle for bounded sequences in IR^{d} and of the Ascolilemma (in the sense of [22]) follows from suitable instances of Π_{1}^{0}-UB^{−}|^{\} and used this to calibrate precisely the contribution of such instances to the growth of extractable bounds. This indicates the mathematical relevance of our generalized principles of uniform boundedness.

Proposition 5.3 Let n ≥ 2, k ≥ 0. For suitable ξ ∈ G_{n}R^{ω} we have

G_{n}A^{ω}+ AC^{1,0}-qf ⊢ F^{−} + Π_{k}^{0}-CA(ξg) → Π_{k}^{0}-UB^{−}|^{\}(g),

where g is a free (function) variable.

Proof: For a suitable ξ ∈ G_{2}R^{ω}, Π_{k}^{0}-CA(ξg) yields the existence of a function h such that

∀v^{0}, k^{0}, z^{0}, a^{0}(hvkza =_{0} 0 ↔ A(g, v, k, z, a)),

where A is as in definition 5.1. Using h, the assumption of Π_{k}^{0}-UB^{−}|^{\}(g) can be expressed as

∀k^{0}∀x ≤_{1} yk∃z^{0}(h(Φ(x, y, k, z), k, z, a) =_{0} 0).

By Σ_{1}^{0}-UB^{−}, which follows from F^{−} and AC^{1,0}-qf relative to G_{n}A^{ω} (see [12]), this yields

∃χ^{1}∀k^{0}∀x ≤_{1} yk∀l^{0}∃z ≤_{0} χk(h(Φ((\overline{x, l}), y, k, z), k, z, a) =_{0} 0)

and hence

∃χ^{1}∀k^{0}∀x ≤_{1} yk∀l^{0}∃z ≤_{0} χk A(g, Φ((\overline{x, l}), y, k, z), k, z, a).

Using proposition 5.3 we can strengthen proposition 4.3 and corollary 4.4 to Theorem 5.4 Let n ≥ 3, k ≥ 0 and B :≡ ∀u^{1}∀v ≤_{τ} tu∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0} be a sentence in L(G_{n}A^{ω}), where B_{0} is quantifier-free and t ∈ G_{n}R^{ω}. Let ξ_{1}, ξ_{2}, ξ_{3} ∈ G_{n}R^{ω} (of suitable types) and Δ a set of sentences having the form ∀x^{δ}∃y ≤_{ρ} sx∀z^{η}A_{0} (A_{0} quantifierfree, s ∈ G_{n}R^{ω}). Then for a suitable ξ ∈ G_{n}R^{ω} the following holds:

If

G_{n}A^{ω} + Δ+ AC-qf ⊢

∀u^{1}∀v ≤_{τ} tu(Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv) ∧ Π_{k}^{0}-UB^{−}|^{\}(ξ_{3}uv) →

∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0})

then

G_{n}A^{ω} + Δ̃ + Mon(B) ⊢

∀u^{1}∀v ≤_{τ} tu(Π_{k}^{0}-TND^{mon}(ξuv) → ∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}) and in particular G_{n}A^{ω} + Σ_{k}^{0}-IA + Δ̃ + Mon(B) ⊢ ∀u^{1}∀v ≤_{τ} tu∃a_{1}^{0}∀b_{1}^{0} … ∃a_{l}^{0}∀b_{l}^{0}∃w^{γ}B_{0}.

In the assumption of the rule the theory G_{n}A^{ω}+Δ+ AC-qf can be strengthened to (G_{n}A^{ω} + Δ+ AC-qf ) ⊕ F^{−}. Corollary 5.5 Let k ≥ 1, γ ≤ 2 and ξ_{1}, ξ_{2}, ξ_{3} ∈ G_{n}R^{ω}. Then the following rule holds

G_{∞}A^{ω} + Δ+ AC-qf ⊢ ∀u^{1}∀v ≤_{τ} tu

(Δ_{k+1}^{0}-CA(ξ_{1}uv) ∧ Π_{k}^{0}-AC(ξ_{2}uv) ∧ Π_{k}^{0}-UB^{−}|^{\}(ξ_{3}uv) → ∃w^{γ}B_{0}(u, v, w)) ⇒ ∃Φ ∈ T_{k−1} such that PA_{i}^{ω} + Δ̃ ⊢ ∀u^{1}∀v ≤_{τ} tu∃w ≤_{γ} Φu B_{0}(u, v, w).

Again we may strengthen the theory in the assumption of the rule above by ⊕F^{−}.

We now show that Π_{k}^{0}-CA(f) in fact is implied by suitable instances of Π_{k}^{0}-UB^{−}|^{\}:

Proposition 5.6 Let n ≥ 2, k ≥ 1. For suitable ξ_{1}, …, ξ_{l} ∈ G_{2}R^{ω} we have

G_{n}A^{ω} ⊢ ⋀_{i=1}^{l} Π_{k}^{0}-UB^{−}|^{\}(ξ_{i}f) → Π_{k}^{0}-CA(f),

where f is a free (function) variable.

Proof: Induction on k. k = 1: Π_{1}^{0}-CA(f) is logically equivalent to

(1) ∃g ≤_{1} 1∀x^{0}, y^{0}∃z^{0}((gx =_{0} 0 → f(x, y) =_{0} 0) ∧ (f(x, z) =_{0} 0 → gx =_{0} 0))

and hence to (2) :≡

¬∀g ≤_{1} 1∃x^{0}, y^{0}∀z^{0}¬((gx =_{0} 0 → f(x, y) =_{0} 0) ∧ (f(x, z) =_{0} 0 → gx =_{0} 0)).

For a suitable ξ_{1} ∈ G_{2}R^{ω}, Π_{1}^{0}-UB^{−}|^{\}(ξ_{1}f) yields the equivalence of (2) and

(3) \{ \begin{matrix}¬∃n^{0}∀g ≤_{1} 1∃x, y ≤ n∀z^{0} \\ ¬((gx =_{0} 0 → f(x, y) =_{0} 0) ∧ (f(x, z) =_{0} 0 → gx =_{0} 0)) \end{matrix}

i.e.

(4) \{ \begin{matrix}∀n^{0}∃g ≤_{1} 1∀x ≤ n \\ ((gx =_{0} 0 → ∀y ≤ nf(x, y) =_{0} 0) ∧ (∀z(f(x, z) =_{0} 0) → gx =_{0} 0)). \end{matrix}

Define

gx := \{ \begin{matrix}0^{0} if ∀y ≤ n(f(x, y) = 0) \\ 1^{0} otherwise. \end{matrix}

Let k ≥ 1. k ↦ k + 1: Π_{k+1}^{0}-CA(f) is equivalent to

(∗) \{ \begin{matrix}∃g ≤_{1} 1∀x^{0}, y^{0}∃z^{0}((gx =_{0} 0 → ∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(x, y, \underline{u}) =_{0} 0))∧ \\ (∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}(f(x, z, \underline{u}) =_{0} 0) → gx = 0)). \end{matrix}

By induction hypothesis there exists an instance Π_{k}^{0}-UB^{−}|^{\}(ξ_{2}f) (which can be considered as an instance Π_{k+1}^{0}-UB^{−}|^{\}(ξ_{2}f)) which implies (relative to G_{n}A^{ω}) Π_{k}^{0}-CA(f) and hence the existence of an h such that

∀x, a(h(x, a) =_{0} 0 ↔ ∃u_{1}∀u_{2} … ∀^{(d)}u_{k}(f(x, a, \underline{u}) =_{0} 0)).

By Π_{k+1}^{0}-UB^{−}|^{\}(ξ_{3}f) (for a suitable ξ_{3}) applied to the negation of (∗), Π_{k+1}^{0}-CA(f) is equivalent to

(∗∗) \{ \begin{matrix}∀n∃g ≤_{1} 1∀x ≤ n((gx =_{0} 0 → ∀y ≤ n∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}f(x, y, \underline{u}) =_{0} 0) \\ ∧(∀z∃u_{1}^{0}∀u_{2}^{0} … ∀^{(d)}u_{k}^{0}f(x, z, \underline{u}) = 0 → gx =_{0} 0)), \end{matrix}

which is satisfied by

gx := \{ \begin{matrix}0^{0} if ∀y ≤ n(h(x, y) = 0) \\ 1^{0} otherwise. \end{matrix}

Corollary 5.7 For n ≥ 2, k ≥ 1 the following holds:

1) G_{n}A^{ω} ⊢ ∀gΠ_{1}^{0}-UB^{−}|^{\}(g) → ∀g̃Π_{k}^{0}-CA(g̃).

2) G_{n}A^{ω} ⊢ ∀gΠ_{1}^{0}-UB^{−}|^{\}(g) ↔ ∀g̃Π_{k}^{0}-UB^{−}|^{\}(g̃). Proof: 1) By proposition 5.6 ∀gΠ_{1}^{0}-UB^{−}|^{\}(g) implies ∀fΠ_{1}^{0}-CA(f) and hence ∀fΠ_{k}^{0}-CA(f) (by iteration).

2) follows from 1) and the proof of proposition 5.3. Let B_{0,1} be the type-0-bar recursor constant of equality rank 1, i.e. B_{0,1} is characterized by the axioms

(BR_{0,1}) : \{ \begin{matrix}x^{2}(\overline{y^{1}, n^{0}}) < n → B_{0,1}xzuny =_{1} z \\ x(\overline{y, n}) ≥ n → B_{0,1}xzuny =_{1} u(λD^{0}. B_{0,1}xzun′(\overline{y, n} ∗ D)), \end{matrix}

where u is of type 1(1(0)) and

(\overline{y, n} ∗ D)(k^{0}) =_{1} \{ \begin{matrix}xk, if k < n \\ D, if k = n \\ 0^{1}, otherwise. \end{matrix}

Proposition 5.8 Let n ≥ 3, k ≥ 1, B_{0}(u, v, w) be a quantifer-free formula of G_{n}A^{ω} containing only u, v, w free, t^{τ1} ∈ G_{n}R^{ω}, γ ≤ 2. Then the following rule holds:

G_{n}A^{ω} + Δ+ AC-qf ⊢ ∀gΠ_{k}^{0}-UB^{−}|^{\}(g) → ∀u^{1}∀v ≤_{τ} tu∃w^{γ}B_{0}(u, v, w)

⇒ ∃Φ ∈ G_{n}R^{ω}[B_{0,1}] such that
G_{n}A^{ω} + Δ̃ + (BR_{0,1}) + (DC^{0}) ⊢ ∀u^{1}∀v ≤_{τ} tu∃w ≤_{γ} Φu B_{0}(u, v, w),

where

(DC^{0}) :≡ ∀x^{0}∃y^{0}A(x, y) → ∀x^{0}∃z^{1}(z0 =_{0} x ∧ ∀z_{1}^{0}A(zz_{1}, z(z′_{1}))).

Proof: By proposition 5.3 and corollary 5.7 one has

G_{n}A^{ω}+ AC^{1,0}-qf + ∀g Π_{1}^{0}-CA(g) ⊢ F^{−} → ∀g̃ Π_{k}^{0}-UB^{−}|^{\}(g̃).

Hence the assumption of the rule to be proved yields

G_{n}A^{ω} + Δ+ AC-qf + ∀g Π_{1}^{0}-CA(g) ⊢ F^{−} → ∀u^{1}∀v ≤_{τ} tu∃w^{γ}B_{0}(u, v, w).

From the work of Spector [23] it follows that G_{n}A^{ω}+ AC-qf +∀g Π_{1}^{0}-CA(g) has (via negative translation) a Gödel functional interpretation in G_{n}A_{i}^{ω} + (BR_{0,1}) by terms ∈ G_{n}R^{ω}[B_{0,1}]. In [2] it is shown that the type structure M^{ω} of the so-called strongly majorizable functionals forms a model of full bar recursion. From the proof of this fact (restricted to type-0-bar recursion) one obtains the construction of a term B_{0,1}^{∗} ∈ G_{n}R^{ω}[B_{0,1}] such that

G_{n}A^{ω} + (BR_{0,1}) + (DC^{0}) ⊢ B_{0,1}^{∗} s-maj B_{0,1},

where ‘s-maj’ is the corresponding syntactic notion of strong majorization as definined in definition 2.1. Therefore the proof of the fact that (the negative translation of) G_{n}A^{ω}+ AC-qf +Δ has a monotone functional interpretation (in the sense of [9]) in G_{n}A_{i}^{ω} by terms in G_{n}R^{ω} (see [12]) extends to G_{n}A^{ω} + Δ+ AC-qf +∀g Π_{1}^{0}-CA(g) yielding a monotone functional interpretation (via negative translation) in G_{n}A^{ω} + Δ̃ + (BR_{0,1}) + (DC^{0}) by terms in G_{n}R^{ω}[B_{0,1}]. This has the consequence that as in the case of G_{n}A^{ω} + Δ+ AC-qf (see the proof of theorem 4.21 in [12]) we can eliminate F^{−} from the proof of ∀u∀v ≤ tu∃w B_{0} and extract a uniform bound Φ on ‘∃w’ which now of course is only in G_{n}R^{ω}[B_{0,1}] (instead of G_{n}R^{ω}) and its verification can be carried out in G_{n}A^{ω} + Δ̃ + (BR_{0,1}) + (DC^{0}).

References

[1] Beklemishev, L.D., A proof-theoretic analysis of collection. Preprint 1996.

[2] Bezem, M.A., Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. J. Symb. Logic 50 pp. 652–660 (1985).

[3] Clote, P., Hájek, P., Paris, J., On some formalized conservation results in arithmetic. Arch. Math. Logic 30, pp. 201-218 (1990).

[4] Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, vol. 4 pp. 34–38 (1933).

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

[6] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (1973).

[7] Kay, R., Models of Peano Arithmetic. Oxford Logic Guides 15, Clarendon Press Oxford 1991.

[8] Kohlenbach, U., Pointwise hereditary majorization and some applications. Arch. Math. Logic 31, pp.227–241 (1992).

[9] Kohlenbach, U., Analysing proofs in analysis. In: W. Hodges, M. Hyland, C. Steinhorn, J. Truss, editors, Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993), pp. 225–260, Oxford University Press (1996).

[10] Kohlenbach, U., Real growth in standard parts of analysis. Habilitationsschrift, pp. xv+166, Frankfurt (1995).

[11] Kohlenbach, U., A note on the Π_{2}^{0}-induction rule. Arch. Math. Logic 34, pp. 279-283 (1995).

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

[13] Kohlenbach, U., Elimination of Skolem functions for monotone formulas. To appear in: Archive for Mathematical Logic.

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

[15] Kohlenbach, U., Arithmetizing proofs in analysis. To appear in: Proc. Logic Colloquium ’96 (San Sebastian).

[16] Luckhardt, H., Extensional Gödel functional interpretation. A consistency proof of classical analysis. Springer Lecture Notes in Mathematics 306 (1973).

[17] Paris, J., Kirby, L., Σ_{n}^{0}-collection schema in arithmetic. In: Logic Colloquium ’77, pp. 199-209. North-Holland, Amsterdam, 1978.

[18] 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).

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

[20] Shoenfield, J.R., Mathematical Logic, Addison-Wesley, New York, 1967.

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

[22] Simpson, S.G., Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations. J. Symbolic Logic 49,pp. 783–801 (1984).

[23] Spector, C., Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Recursive function theory, Proceedings of Symposia in Pure Mathematics, vol. 5 (J.C.E. Dekker (ed.)), AMS, Providence, R.I., pp. 1–27 (1962).

[24] Troelstra, A.S. (ed.) Metamathematical investigation of intuitionistic arithmetic and analysis. Springer Lecture Notes in Mathematics 344 (1973).

Recent BRICS Report Series Publications

RS-97-23 Ulrich Kohlenbach. On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. August 1997. 35 pp.

RS-97-22 Carsten Butz. Syntax and Semantics of the logic L_{ωω}^{λ}. July 1997. 14 pp.

RS-97-21 Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp.

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.

RS-97-19 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. Aappears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. To appear in Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FCT&TCS ’97 Proceedings, LNCS, 1997.

RS-97-18 Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. To appear as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press.

RS-97-17 Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 10 pp.

RS-97-16 Noga Alon, Martin Dietzfelbinger, Peter Bro Miltersen, Erez Petrank, and Gábor Tardos. Linear Hashing. June 1997. 22 pp. A preliminary version appeared with the title Is Linear Hashing Good? in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97, pages 465–474.

RS-97-15 Pierre-Louis Curien, Gordon Plotkin, and Glynn Winskel. Bistructures, Bidomains and Linear Logic. June 1997. 41 pp.

RS-97-14 Arne Andersson, Peter Bro Miltersen, Søren Riis, and Mikkel Thorup. Dictionaries on AC^{0} RAMs: Query Time Θ(\sqrt{log n/ log log n}) is Necessary and Sufficient. June 1997. 18 pp. Appears in 37th Annual Symposium on Foundations of Computer Science, FOCS ’96 Proceedings, pages 441–450.