BRICS RS-98-41 U. Kohlenbach: The Computational Strength of Extensions of Weak König’s Lemma BRICS

Basic Research in Computer Science

The Computational Strength of Extensions of Weak König’s Lemma

Ulrich Kohlenbach BRICS Report Series RS-98-41 ISSN 0909-0878 December 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/41/

The computational strength of extensions of weak König’s lemma

Ulrich Kohlenbach

BRICS^{∗}

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

Abstract

The weak König’s lemma WKL is of crucial significance in the study of fragments of mathematics which on the one hand are mathematically strong but on the other hand have a low proof-theoretic and computational strength. In addition to the restriction to binary trees (or equivalently bounded trees), WKL is also ‘weak’ in that the tree predicate is quantifier-free. Whereas in general the computational and proof-theoretic strength increases when logically more complex trees are allowed, we show that this is not the case for trees which are given by formulas in a class Φ_{∞} where we allow an arbitrary function quantifier prefix over bounded functions in front of a Π_{1}^{0}-formula. This results in a schema Φ_{∞}-WKL. Another way of looking at WKL is via its equivalence to the principle

∀x∃y ≤ 1∀z A_{0}(x, y, z) → ∃f ≤ λx.1∀x, z A_{0}(x, fx, z),

where A_{0} is a quantifier-free formula (x, y, z are natural number variables). We generalize this to Φ_{∞}-formulas as well and allow function quantifiers ‘∃g ≤ s’ instead of ‘∃y ≤ 1’, where g ≤ s is defined pointwise. The resulting schema is called Φ_{∞}-b-AC^{0,1}. In the absence of functional parameters (so in particular in a second order context), the corresponding versions of Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1} turn out to be equivalent to WKL. This changes completely in the presence of functional variables of type 2 where we get proper hierarchies of principles Φ_{n}-WKL and Φ_{n}-b-AC^{0,1}. Variables of type 2 however are necessary for a direct representation of analytical objects and – sometimes – for a faithful representation of such objects at all as we will show in a subsequent paper. By a reduction of Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1} to a non-standard axiom F (introduced in a previous paper) and a new elimination result for F relative to various fragment of arithmetic in all finite types, we prove that Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1} do neither contribute to the provably recursive functionals of these fragments nor to their proof-theoretic strength. In a subsequent paper we will illustrate the greater mathematical strength of these principles (compared to WKL).

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

1 Introduction

The so-called weak König’s lemma WKL is of crucial significance in the study of fragments of mathematics which on the one hand are mathematically strong but on the other hand have a low proof-theoretic and computational strength (see e.g. [15],[10]). The prefix ‘weak’ has a twofold meaning: the full statement of König’s lemma is restricted in the formulation of WKL in two ways

1) instead of allowing arbitrary finitely branching trees we only have binary trees in WKL (note however that it wouldn’t make a difference if we would allow bounded trees in the sense of [15]);

2) the tree is represented by a function f and consequently the tree predicate f(n) = 0 expressing that n is the code of a finite branch in the tree represented by f is quantifier-free.

In view of 2), WKL could be denoted by QF-WKL, where ‘QF’ refers to ‘quantifierfree’. It is known that the removal of either of the restrictions above in general results in principles which, relative to certain weak subsystems of second order arithmetic or arithmetic in all finite types, are much stronger than WKL. E.g. the removal of 1) while keeping 2) would result in a principle called KL in the context of reverse mathematics which relative to the well-known system RCA_{0} is equivalent to arithmetical comprehension, whereas RCA_{0}+WKL is conservative over RCA_{0} (see [15]). The significance of the restriction 2) was pointed out first in [17], where it is shown that the binary König’s lemma applied to trees of arbitrary logical complexity implies comprehension of numbers for arbitrary complex predicates. In this paper we study an extension Φ_{∞}-WKL of (QF-)WKL to a certain class of formulas Φ_{∞} which are built up as follows: in front of a Π_{1}^{0}-formula (with arbitrary parameters) we have an arbitrary prefix of bounded function quantifiers ‘∀(∃)f ≤ s’ (where f ≤ g :≡ ∀x(fx ≤ gx)).^{1} Another way of looking at WKL is to view it as a weak bounded choice principle. Indeed, already relative to very weak base systems, WKL is equivalent to

Π_{1}^{0}-b-AC^{0,0} : ∀x∃y ≤ 1∀z A_{0}(x, y, z) → ∃f ≤ λx.1∀x, z A_{0}(x, fx, z),

where A_{0} is quantifier-free and x, y, z are number variables. We generalize this principle in two ways: we allow Φ_{∞}-formulas instead of the Π_{1}^{0}- formula ‘∀z A_{0}(x, y, z)’ and generalize the existential number quantifier ‘∃y ≤ 1’ to a function quantifier ‘∃g ≤ λx.1’. The resulting schema is called Φ_{∞}-b-AC^{0,1}.

If no parameters of types > 1 are present (so in particular in a second order context), the corresponding versions of Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1} turn out to be equivalent to WKL. This picture, however, changes drastically in the presence of higher type variables (actually the presence of parameters of type 2 suffices) where we get proper hierarchies of principles Φ_{n}-WKL and Φ_{n}-b-AC^{0,1}. Variables of type 2 however are necessary for a direct representation of analytical objects and – sometimes – for a representation of such objects which is faithful at all. That is why we couldn’t use WKL in our development of analysis in weak fragments of arithmetic in all finite types in [12],[13],[14], where e.g. continuous functions Φ : IR → IR are represented directly as type-2-functionals and not as in the second order context of reverse mathematics^{2}, but relied on certain non-standard principles F and F^{−} instead which are not true in the full set-theoretic type structure but can be eliminated from proofs of sentences having a certain restricted logical form. In this paper we show that Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1} can be derived from F and a schema of quantifier-free choice in higher types. Together with a new elimination result for F this is used to calibrate the proof-theoretic and computational strength of Φ_{∞}-WKL and Φ_{∞}-b-AC^{0,1}. It turns out that these principles do not contribute to the provably recursive function(al)s (up to type 2) of the underlying finite type systems we consider. Furthermore we obtain conservation results over primitive recursive arithmetic PRA resp. Peano arithmetic PA when these principles are added to the finite type versions of PRA and PA. The results of this paper can be understood also as an analysis of the greater mathematical strength of the non-standard principle F (compared to WKL) in terms of standard extensions of WKL. That this greater strength is actually needed already for the treatment of continuous functions when the latter are represented as mentioned above, will be discussed in a subsequent paper.

1See definition 2.1 for a precise definition and also remark 2.2.

2The need for a more flexible language than that of second-order arithmetic which includes variables of higher type for a direct formalization of analysis has been emphasized by S. Feferman in a number of writings, see e.g. [4].

Description of the theories E-G_{n}A^{ω}, E-PRA^{ω} and E-PA^{ω}

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.

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. The systems E-G_{n}A^{ω} (for all n ≥ 1) are introduced in [12] to which we refer for details. E-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 degree 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 as in the case of the (unbounded) Kleene-Feferman recursors R̂_{ρ}). In this paper our systems always contain 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}). In [12] we had 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, added as axioms.^{3} By ‘true’ we refer to the full set–theoretic model S^{ω}. In given proofs of course only very special universal axioms are used which can be proved in suitable extensions of our theories. Nevertheless one can include them all as axioms since they (more precisely their proofs) do not contribute to the provable recursive function(al)s of the system. In particular this covers all instances of the schema of quantifier-free induction. In this paper we prefer however to have only the schema of quantifier-free choice included to E-G_{n}A^{ω} instead of taking arbitrary universal axioms. We note nevertheless that all results of this paper (except for the conservation results over PA and PRA at the end of the paper) remain valid if we add an arbitrary set of universal axioms to our systems.

E-PRA^{ω} results if we add the functional

Φ_{it}0yf =_{0} y, Φ_{it}x′yf =_{0} f(x, Φ_{it}xyf)

to E-G_{∞}A^{ω} := ⋃_{n∈ω}{E-G_{n}A^{ω}}. The system E-PRA^{ω} is equivalent to Feferman’s system E-P̂A^{ω}|^{\} from [3] since Φ_{it} allows (relative to E-G_{∞}A^{ω}) to define the predicative recursor constants R̂_{ρ} (see [12]). E-PA^{ω} is the extension of E-PRA^{ω} obtained by the addition of the schema of full induction and all (impredicative) primitive recursive functionals in the sense of [6].

The schema of full choice is given by

AC^{ρ,τ} : ∀x^{ρ}∃y^{τ}A(x, y) → ∃Y^{τ(ρ)}∀x^{ρ}A(x, Y x), AC := ⋃_{ρ,τ∈T}{ AC^{ρ,τ}}.

3The restriction deg(ρ) ≤ 2 has a technical reason discussed in [12].

The schema of quantifier-free choice QF-AC^{ρ,τ} is defined as the restriction of AC^{ρ,τ} to quantifier-free formulas A_{0}.^{4}

The theory T + μ results from T if we add the non-constructive μ-operator μ^{2} to T together with the characterizing axiom

μ(f) = \{ \begin{matrix}the least x such that f(x) =_{0} 0, if ∃x^{0}(f(x) =_{0} 0) \\ 0, otherwise. \end{matrix}

Notation: For ρ = 0ρ_{k} … ρ_{1}, we define 1^{ρ} := λx_{1}^{ρ_{1}} … x_{k}^{ρ_{k}}.1^{0}, where 1^{0} := S0.

Definition 1.1 1) Between functionals of type ρ we define the relation ≤_{ρ} (‘less or equal’) by induction on the type:

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

2)

min_{0}(x_{1}^{0}, x_{2}^{0}) := min(x_{1}, x_{2}),
min_{ρτ}(x_{1}^{ρτ}, x_{2}^{ρτ}) := λy^{τ}. min_{ρ}(x_{1}y, x_{2}y).

In the following we will need the definition of the binary (‘weak’) König’s lemma as given in [17]:

Definition 1.2 (Troelstra(74)) WKL:≡ ∀f^{1}(T (f) ∧ ∀x^{0}∃n^{0}(lth n =_{0} x ∧ fn =_{0} 0) → ∃b ≤_{1} λk.1∀x^{0}(f(\overline{b}x) =_{0} 0)), where T f :≡ ∀n^{0}, m^{0}(f(n ∗ m) =_{0} 0 → fn =_{0} 0) ∧ ∀n^{0}, x^{0}(f(n ∗ ⟨x⟩) =_{0} 0 → x ≤_{0} 1) (i.e. T (f) asserts that f represents a 0,1–tree).

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

2 Principles of bounded choice in higher types: Φ_{∞}-b-AC^{0,1}

Definition 2.1 1) A ∈ Φ_{n} if

A ≡ ∀f_{1} ≤_{1} s_{1}[\underline{a}]∃f_{2} ≤_{1} s_{2}[\underline{a}] … ∀^{(d)}f_{n} ≤_{1} s_{n}[\underline{a}]∀x^{0}A_{0}(\underline{a}, f_{1}, …, f_{n}, x),

where A_{0} is quantifier-free and \underline{a} contains all free variables of A and s_{i} (which may have arbitrary types). The f_{i} must not occur in \underline{a}.

2) A ∈ Ψ_{n} if

A ≡ ∃f_{1} ≤_{1} s_{1}[\underline{a}]∀f_{2} ≤_{1} s_{2}[\underline{a}] … ∃^{(d)}f_{n} ≤_{1} s_{n}[\underline{a}]∀x^{0}A_{0}(\underline{a}, f_{1}, …, f_{n}, x),

where A_{0} and s_{i} as above.

3) The classes Φ_{n}^{−} and Ψ_{n}^{−} result if we restrict ourselves to parameters \underline{a} of type degree ≤ 1 in A_{0} and s_{i}.

Remark 2.2 One could also allow further universal number quantifiers ∀x^{0} (but no existential quantifiers) to occur in between the bounded function quantifiers in the definition of Φ_{n}. The results of this paper easily extend to this slightly generalized case. However, since our applications on which we will report in a subsequent paper do not need this we restrict ourselves to the definition of Φ_{n} as stated above in order to improve the readability of the proofs.

Remark 2.3 In the extensional context of our theories T we can code pairs of bounded function quantifiers of the same sort together:

∀f_{1} ≤_{1} s_{1}∀f_{2} ≤_{1} s_{2}A(f_{1}, f_{2}) ↔ ∀f ≤_{1} j(s_{1}, s_{2}) A(min_{1}(j_{1}f, s_{1}), min_{1}(j_{2}f, s_{2}))

for some monotone function pairing as used e.g. in [12]. Analogously for ∃f ≤_{1} s.

Definition 2.4

Φ_{n}-b-AC^{ρ,τ} : ∀a^{τρ}(∀x^{ρ}∃y ≤_{τ} ax A(x, y, a) → ∃Y ≤_{τρ} a∀x^{ρ} A(x, Y x, a)),

where A ∈ Φ_{n} (with arbitrary further parameters). Ψ_{n}-b-AC^{ρ,τ} (resp. Φ_{n}^{−}-b-AC^{ρ,τ}, Ψ_{n}^{−}-b-AC^{ρ,τ}) are defined as Ψ_{n}-b-AC^{ρ,τ} but with A ∈ Ψ_{n} (resp. A ∈ Φ_{n}^{−}, Ψ_{n}^{−}).

Φ_{∞}^{(−)}-b-AC^{ρ,τ} := ⋃_{n∈ω} Φ_{n}^{(−)}b-AC^{ρ,τ}.

Remark 2.5 In T =E-G_{3}A^{ω}, E-PRA^{ω} and E-PA^{ω} the schema Φ_{n}-b-AC^{ρ,τ} can be written as a single axiom (for each fixed n ∈ IN, ρ, τ) by replacing the quantifierfree matrix A_{0}(x, y, a, \underline{v}) of A by ‘Φxya\underline{v} =_{0} 0’, where Φ is a functional variable of suitable type, and replacing ‘f_{i} ≤_{1} s_{i}[\underline{a}]’ by ‘f_{i} ≤_{1} b_{i}’ for a free function variable b_{i}. This, however, is not possible for the restricted version Φ_{n}^{−}-b-AC^{ρ,τ}.

The next proposition shows that in the absence of parameters of types ≥ 2 (and so in particular in a second-order context) there is no point in considering Φ_{n}-b-AC^{0,1} instead of Π_{1}^{0}-b-AC^{0,0}(= Φ_{0}-b-AC^{0,0}).^{5} For its proof we need the following

Lemma 2.6 Let A_{0}(\underline{a}, g^{1}, y^{0}) be a quantifier-free formula of T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω} containing (in addition to g, y) only parameters \underline{a} of type levels ≤ 1 and let s be a term of T containing at most \underline{a} as free variables. Then one can construct a Π_{1}^{0}-formula B(\underline{a}) of T (containing only \underline{a} free) such that

T + WKL ⊢ ∀\underline{a}(B(\underline{a}) ↔ ∃g ≤_{1} s[\underline{a}]∀y^{0}A_{0}(\underline{a}, g, y)).

Proof: For T =E-PRA^{ω} and T = E-PA^{ω} this follows from (the proofs of) proposition 4.14 and corollary 4.15 in [10]. The use of the modulus t̃xyk of pointwise continuity in y used in the proof of proposition 4.14 in [10] can easily be replaced by a modulus t̂xk of uniform continuity on {y : y ≤_{1} sx}. For closed t ∈E-G_{3}A^{ω} such a modulus t̂ can be constructed in E-G_{3}A^{ω} by the method of [9] since the majorization argument used there is available in E-G_{3}A^{ω} as was shown in [12].

Proposition 2.7 Let m, n ≥ 0. Over T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω} the following principles are equivalent:

(i) WKL,

(ii) Φ_{0}-b-AC^{0,0},

(iii) Φ_{m}^{−}-b-AC^{0,1},

(iv) Ψ_{n}^{−}-b-AC^{0,1}.

Proof: We first show the following \underline{Claim}: Let A(\underline{a}) be a Φ_{n}^{−} (or Ψ_{n}^{−}) formula containing only parameters \underline{a} of type degree ≤ 1. Then one can construct a Π_{1}^{0}-formula B(\underline{a}) such that

T + WKL ⊢ A(\underline{a}) ↔ B(\underline{a}).

5This is in sharp contrast to the case where arbitrary parameters are allowed as we will see below.

\underline{Proof of the claim}: We proceed by meta-induction on n: n = 0 : In this case A ∈ Π_{1}^{0} and so B := A suffices. n → n + 1 : Case 1: A ∈ Φ_{n+1}. Then A(\underline{a}) ≡ ∀f ≤_{1} s[\underline{a}] Ã(\underline{a}, f), where Ã ∈ Ψ_{n}. By the induction hypothesis there exists a formula B̃(\underline{a}, f) ≡ ∀y^{0}B̃_{0}(\underline{a}, f, y) ∈ Π_{1}^{0} with

T + WKL ⊢ A(\underline{a}) ↔ ∀f ≤_{1} s[\underline{a}]∀y^{0}B̃_{0}(\underline{a}, f, y).

Let tB̃_{0} be a closed term of T such that

T ⊢ ∀\underline{a}, f, y(tB̃_{0}(\underline{a}, f, y) =_{0} 0 ↔ B̃_{0}(\underline{a}, f, y).

From results in [9] (using for the case of E-G_{3}A^{ω} also [12]) it follows that one can construct a closed term t̂B̃_{0} of T such that t̂B̃_{0}(\underline{a}, y) is (provably in T a modulus of uniform continuity for λf.tB̃_{0}(\underline{a}, f, y) on \{f : f ≤_{1} s[\underline{a}]\}. Using this modulus, ∀f ≤_{1} s[\underline{a}] B̃_{0}(\underline{a}, f, y) can be written as a quantifier-free formula and hence ∀f ≤_{1} s[\underline{a}]∀y B̃_{0}(\underline{a}, f, y) as a Π_{1}^{0}-formula B̂(\underline{a}). So

T + WKL ⊢ A(\underline{a}) ↔ B̂(\underline{a}).

Case 2: A(\underline{a}) ∈ Ψ_{n+1}. Then A(\underline{a}) ≡ ∃f ≤_{1} s[\underline{a}] Ã(\underline{a}, f) with Ã(\underline{a}, f) ∈ Φ_{n}. By I.H. there exists a formula B̃(\underline{a}, f) ≡ ∀y^{0}B̃_{0}(\underline{a}, f, y) ∈ Π_{1}^{0} with

T + WKL ⊢ A(\underline{a}) ↔ ∃f ≤_{1} s[\underline{a}]∀y^{0}B̃_{0}(\underline{a}, f, y).

By the lemma, there exists a Π_{1}^{0}-formula B̂(\underline{a}) such that

T + WKL ⊢ B̂(\underline{a}) ↔ ∃f ≤_{1} s[\underline{a}]∀y^{0}B̃_{0}(\underline{a}, f, y).

So again

T + WKL ⊢ A(\underline{a}) ↔ B̂(\underline{a})

with B̂ ∈ Π_{1}^{0}. This finishes the proof of the claim. The claim implies that

T + WKL ⊢ Φ_{m}^{−}-b-AC^{0,1} ↔ Ψ_{n}^{−}-b-AC^{0,1} ↔ Φ_{0}^{−}-b-AC^{0,1}

for all m, n ≥ 0. Also note that T ⊢ Φ_{0}-b-AC^{0,0} ↔ Φ_{0}^{−}-b-AC^{0,0} and

T ⊢ Φ_{0}^{−}-b-AC^{0,1} → Φ_{0}^{−}-b-AC^{0,0}.

Therefore it remains to show that α) T ⊢ Φ_{0}-b-AC^{0,0} → WKL,

β) T ⊢ WKL → Φ_{0}^{−}-b-AC^{0,1}.

Proof of α): Consider the formula^{6}

(+) \{ \begin{matrix}∀x^{0}∃n ≤_{0} 1∀k > 0(∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ m) = 0) \\ → ∃m ≤ \overline{1}(k − · 1)(lth(m) = k − · 1 ∧ f(x ∗ ⟨n⟩ ∗ m) = 0)). \end{matrix}

We now assume that T (f) and first show that (+) holds: Let x be arbitrary but fixed. Case 1: ∀k > 0∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ m) = 0). Then (using classical logic)

\begin{matrix}∀k > 0∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ ⟨0⟩ ∗ m) = 0)∨ \\ ∀k > 0∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ ⟨1⟩ ∗ m) = 0). \end{matrix}

In the case the first disjunct is true, choose n = 0 and n = 1 otherwise. Case 2: ∃k > 0¬∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ m) = 0). By the quantifier-free leastnumber-principle (hence by the schema QF-IA of quantifier-free induction) we find the least such k. Call it k_{0}. 2.1: k_{0} = 1 : Choose n ≤ 1 arbitrarily. 2.2: k_{0} > 1 : Then

∃m ≤ \overline{1}(k_{0} − · 1)(lth(m) = k_{0} − · 1 ∧ f(x ∗ m) = 0).

choose n := (m)_{0} for such an m. This finishes the proof of (+). By Π_{1}^{0}-b-AC^{0,0} applied to (+) we get a function g such that

\{ \begin{matrix}∀x^{0}(gx ≤_{0} 1 ∧ ∀k > 0(∃m ≤ \overline{1}k(lth(m) = k ∧ f(x ∗ m) = 0) \\ → ∃m ≤ \overline{1}(k − · 1)(lth(m) = k − · 1 ∧ f(x ∗ ⟨gx⟩ ∗ m) = 0))). \end{matrix}

Define h̃(0) := ⟨⟩, h̃(n + 1) := h̃(n) ∗ ⟨g(h̃(n))⟩. The definition of h̃ can be carried out in E-G_{3}A^{ω} using bounded recursion, since g ≤ 1 and therefore h̃(n) ≤ \overline{1}n (by [12], Φ_{⟨⟩}fx = \overline{f}x is definable in E-G_{3}A^{ω}).

6Here we use that our coding of finite sequences has the property that ∀n, m, f, g(n ≥ m ∧ ∀x(fx ≥ gx) → \overline{f}n ≥ \overline{g}m), which is the case for the coding from [12].

Now take h(n) := (h̃(n + 1))_{n}. By quantifier-free induction we show that (++) ∀n(h̃(n) = \overline{h}(n)): n = 0 : h̃(0) = ⟨⟩ = \overline{h}(0).

n → n + 1 : h̃(n + 1) = h̃(n) ∗ ⟨g(h̃n)⟩ =^{I.H.} \overline{h}n ∗ ⟨g(h̃n)⟩ =^{lth(h̃n)=n} \overline{h}(n) ∗ ⟨(h̃(n + 1))_{n}⟩ =

\overline{h}(n) ∗ ⟨hn⟩ = \overline{h}(n + 1).

Let k be arbitrary but fixed. We now show – again by quantifier-free induction on n – that

∀n < k∃m ≤ \overline{1}(k − · n)(lth(m) = k − · n ∧ f(\overline{h}(n) ∗ m) = 0) :

n = 0 : \overline{h}(0) ∗ m = m, hence the claim follows from T (f). n → n + 1 : We may assume that n + 1 < k : By I.H.

∃m̃ ≤ \overline{1}(k − · n)(lth(m̃) = k − · n ∧ f(\overline{h}(n) ∗ m̃) = 0).

Hence by g-definition

∃m ≤ \overline{1}(k − · (n + 1))(lth(m) = k − · (n + 1) ∧ f(\underbrace{\overline{h}n ∗ ⟨g(\overline{h}n)⟩}_{=\overline{h}(n+1) (++)} ∗m) = 0),

which is the claim for n + 1. So in total we have shown that T (f) implies

∀k∀n < k∃m ≤ \overline{1}(k − · n)(lth(m) = k − · n ∧ f(\overline{h}(n) ∗ m) = 0)

and hence

∀n(f(\overline{h}n) = 0),

i.e. h satisfies WKL. Proof of β : Let

∀a^{1(0)}(∀x^{0}∃y ≤_{1} ax∀z^{0}A_{0}(x, y, z, a, \underline{b} → ∃Y ≤_{1(0)} a∀x^{0}, z^{0}A_{0}(x, Y x, z, a, \underline{b}))

be an instance of Φ_{0}^{−}-b-AC^{0,1}, where all additional parameters \underline{b} have types of degree ≤ 1. From (the proof of) proposition 4.14 in [10]^{7} it follows (using the fact that the type 1(0) can be encoded into the type 1) that

\begin{matrix}(∗) T + WKL ⊢ ∀a, \underline{b}(∃Y ≤_{1(0)} a∀x^{0}, z^{0}A_{0}(x, Y x, z, a, \underline{b}) ↔ \\ ∀z^{0}∃Y ≤_{1(0)} a∀x^{0}∀z̃ ≤ z A_{0}(x, Y x, z̃, a, \underline{b})). \end{matrix}

7In [10] only the systems PA^{ω} and PRA^{ω} are treated. However all ingredients used in the proof of proposition 4.14 are also available for E-G_{3}A^{ω} (see [12]).

Relative to T , ∀x∃y ≤_{1} ax∀z^{0}A_{0}(x, y, z, a, \underline{b}) implies ∀z∀x∃y ≤_{1} ax∀z̃ ≤_{0} z A_{0}(x, y, z̃, a, \underline{b}). ∀z̃ ≤_{0} z A_{0}(x, y, z̃, a, \underline{b}) can be written as a quantifier-free formula Ã_{0}(x, y, z, a, \underline{b}). Let tÃ_{0} be a closed term such that

T ⊢ ∀x, y, z, a, \underline{b}(tÃ_{0}xyza\underline{b} =_{0} 0 ↔ Ã_{0}(x, y, z, a, \underline{b})).

As in the proof of the claim above, we use the fact that tÃ_{0} has a modulus of uniform continuity functional for λy^{1}.tÃ_{0}xyza\underline{b} on \{y : y ≤_{1} ax\} to replace ‘∃y ≤_{1} ax’ by a finite disjunction. Bounded search then yields (relative to T ) ∃Y ≤_{1(0)} a∀x∀z̃ ≤ z A_{0}(x, Y x, z̃, a, b)). Together with (∗) above, this concludes the proof of β.

Remark 2.8 The equivalence of WKL and Φ_{0}-b-AC^{0,0} is closely related to the equivalence of WKL with the so-called Σ_{1}^{0}-separation principle which has been established relative to RCA_{0} in the context of reverse mathematics (see [15]). The latter result in turn is closely related to theorem 6.1 of [7].

In the presence of higher type parameters the picture changes as we will show now.

Definition 2.9 We define the classes of formulas Π_{n}^{1,b} and Ψ_{n}^{1,b} simultaneously by induction on n:

(i) A ∈ Π_{0}^{1,b} = Σ_{0}^{1,b}, if A is quantifier-free;

(ii) if A(f) ∈ Π_{n}^{1,b}, then ∃f ≤_{1} 1 A(f) ∈ Σ_{n+1}^{1,b};

(iii) if A(f) ∈ Σ_{n}^{1,b}, then ∀f ≤_{1} 1 A(f) ∈ Π_{n+1}^{1,b}.

A may contain arbitrary parameters (of arbitrary types).

Definition 2.10 1) The schema of Π_{n}^{1,b}-comprehension is given by

Π_{n}^{1,b}-CA : ∃g^{1}∀x^{0}(gx = 0 ↔ A(x)),

where A(x) ∈ Π_{n}^{1,b} and may contain arbitrary parameters (of arbitrary types) in addition to x. Σ_{n}^{1,b}-CA is defined analogously but with Σ_{n}^{1,b} instead of Π_{n}^{1,b}.

2) The schema of Σ_{n}^{1,b}-choice is given by

Σ_{n}^{1,b}-AC : ∀x^{0}∃f ≤_{1} 1 A(x, f) → ∃g ≤_{1(0)} 1 A(x, gx),

where A(x, f) ∈ Σ_{n}^{1,b} and may contain arbitrary parameters.

Proposition 2.11 Let T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω}. Then

T + Ψ_{n+1}-b-AC^{0,0} ⊢ Π_{n}^{1,b}-CA.

Proof: Apply Ψ_{n+1}-b-AC^{0,0} to ∀x^{0}∃y ≤_{0} 1(y = 0 ↔ A(x)), where A(x) ∈ Π_{n}^{1,b} (note that A(x) can be prenexed into formulas Ã(x) ∈ Φ_{n+1} and Â ∈ Ψ_{n+1} making use of remark 2.3).

Corollary to the proof: In proposition 2.11 actually the restriction of b-AC^{0,0} to Boolean combinations of Φ_{n}- and Ψ_{n}-formulas instead of Ψ_{n+1}-formulas would have been sufficient.

Proposition 2.12 E-PA^{ω}+Π_{n}^{1,b}-CA+μ contains (modulo a canonical embedding which doesn’t change the first order part) the second order system (Π_{n}^{1}-CA) known from reverse mathematics.^{8}

Proof: Systems formulated in the language of second-order arithmetic with set variables like (Π_{n}^{1}-CA) can be embedded in (suitable) systems formulated in the language of functionals of all finite types by representing sets X by their characteristic functions χ_{X} and replacing formulas ‘t ∈ X’ by ‘χ_{X}(t) =_{0} 0’. In doing so and using the fact that the presence of μ allows to absorb an arbitrary arithmetical quantifier-prefix in front of a quantifier-free formula with arbitrary parameters uniformly in these parameters, the comprehension schema of (Π_{n}^{1}-CA) reduces to Π_{n}^{1,b}-CA above.

Together with the well-known fact that E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + μ can be reduced proof-theoretically to (Π_{1}^{0}-CA)_{<ε_{0}}^{9} and hence is proof-theoretically much weaker than (Π_{1}^{1}-CA), it follows from propositions 2.11, 2.12 together with remark 2.5 that

Corollary 2.13 E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + μ ⊢ / Ψ_{2}-b-AC^{0,0}.

Proposition 2.14 Let T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω}. Then

T + Ψ_{n}-b-AC^{0,1} ⊢ Σ_{n}^{1,b}-AC.

Proof: Obvious.

Proposition 2.15 E-PA^{ω} + Σ_{n}^{1,b}-AC +μ contains (modulo the previously mentioned canonical embedding) the second order system (Σ_{n}^{1}-AC).^{10}

Proof: Similar to the proof of proposition 2.12.

8In the notation of [15], (Π_{n}^{1}-CA) is the system Π_{n}^{1}-CA_{0}+full induction.

9This follows from [3] together with elimination of extensionality (see also [1]).

10In the notation of [15] this system is Σ_{n}^{1}-AC_{0}+full induction.

3 Generalization of WKL to more complex trees: Φ_{∞}-WKL

Definition 3.1 The generalization of WKL to Φ_{n}-trees is given by

Φ_{n}-WKL : ∀n^{0}∃f ≤_{1} 1∀ñ ≤ n A(\overline{f}ñ) → ∃f ≤_{1} 1∀n^{0}A(\overline{f}n),

where A(k^{0}) ∈ Φ_{n} (with arbitrary further parameters of arbitrary types). Ψ_{n}-WKL is defined analogously. Φ_{∞}-WKL:= ⋃_{n∈ω}{Φ_{n}-WKL}.

Remark 3.2 Like Φ_{n}-b-AC^{ρ,τ} (see remark 2.5) Φ_{n}-WKL can be written as a single axiom for each fixed n.

Proposition 3.3 E-G_{3}A^{ω} ⊢ WKL ↔ Φ_{0}-WKL ↔ Ψ_{0}-WKL.

Proof: Φ_{0}-WKL≡ Ψ_{0}-WKL holds by definition. We have to show WKL↔ Φ_{0}-WKL: The right-hand side obviously implies the left-hand side since Φ_{0}-WKL allows the tree-predicate to be given even by a Π_{1}^{0}-formula whereas in WKL T (f) is quantifierfree. So it remains to show that WKL→ Φ_{0}-WKL: Assume

(+) ∀n^{0}∃g ≤_{1} 1∀ñ ≤ n∀z^{0}A_{0}(\overline{g}ñ, z).

Define f such that

(++) f(x) =_{0} 0 ↔ ∀i < lth(x)((x)_{i} ≤ 1) ∧ ∀x̃ ⊑ x∀z ≤ lth(x)A_{0}(x̃, z),

where ‘x̃ ⊑ x’ means that x̃ is the code of an initial segment of the sequence coded by x (note that the right-hand side of (++) can be written as a quantifier-free formula in E-G_{3}A^{ω}). f satisfies T (f) and – by (+) – represents an infinite binary tree, i.e.

∀n∃g ≤_{1} 1 (f(\overline{g}n) = 0).

Hence WKL yields

∃g ≤_{1} 1∀n (f(\overline{g}n) = 0),

which implies

∃g ≤_{1} 1∀n∀m ≤ n∀z ≤ n A_{0}(\overline{g}m, z),

and therefore

∃g ≤_{1} 1∀n∀z A_{0}(\overline{g}n, z).

Proposition 3.4 Let T :=E-PA^{ω}. Then

T + Φ_{n+1}-WKL ⊢ Π_{n}^{1,b}-CA.

Proof: We use the following tree-predicate from [17]:

Ã(k) :≡ \{ \begin{matrix}(k)_{lth(k) −· 1} ≤ 1 ∧ ((k)_{lth(k) −· 1} = 0 → A(lth(k) − · 1))∧ \\ ((k)_{lth(k) −· 1} = 1 → ¬A(lth(k) − · 1))), if lth(k) > 0 \\ true, otherwise. \end{matrix}

For A ∈ Π_{n}^{1,b}, Ã(k) can be written as a Φ_{n+1}-formula (using remark 2.3). By induction on n we can prove in E-PA^{ω} that

∀n^{0}∃f ≤_{1} 1∀ñ ≤ nÃ(\overline{f}ñ).

Φ_{n+1}-WKL therefore yields the characteristic function for A(n).

Arguing as in the case of corollary 2.13 we obtain

Corollary 3.5 E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + μ ⊢ / Φ_{2}-WKL.

4 The computational strength of Φ_{∞}-b-AC^{0,1} and Φ_{∞}-WKL

In order to determine the effect (or rather non-effect as it will turn out) of Φ_{∞}-b-AC^{0,1} and Φ_{∞}-WKL on the provably recursive functionals when added to T , we make use of a certain non-standard axiom F which was introduced first in [12]^{11} (and has been applied e.g. in [14]):

F :≡ ∀Φ^{2(0)}, y^{1(0)}∃y_{0} ≤_{1(0)} y∀k^{0}∀z ≤_{1} yk(Φkz ≤_{0} Φk(y_{0}k)).

We call this axiom ‘non-standard’ since it does not hold in the full set-theoretic type structure S^{ω}. Nevertheless its use can be eliminated from certain proofs thereby yielding classically true results. This has been discussed extensively in [12] to which we refer for further information. In that paper we mainly made use of a weaker version F^{−} of F which allows a direct proof-theoretic elimination whereas our elimination of F was based on a model-theoretic argument. In this paper however we need the full version F and give a proof-theoretic reduction of the use of F to a standard principle for certain formulas (see theorem 4.6 below). We apply F via one of its consequences, the following principle of uniform Σ_{1}^{0}-boundedness:

11A special case of F was studied already in [11] and called also F in that paper but F_{0} in [12].

Definition 4.1 ([12]) The schema^{12} of uniform Σ_{1}^{0}–boundedness is defined as

Σ_{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} yk∃z ≤_{0} χk A(x, y, k, z)), \end{matrix}

where A ≡ ∃\underline{l}A_{0}(\underline{l}) and \underline{l} is a tuple of variables of type 0 and A_{0} is a quantifier–free formula (which may contain parameters of arbitrary types).

Proposition 4.2 ([12]) Let T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω}. Then T +QF-AC^{1,0} + F ⊢ Σ_{1}^{0}-UB.

Proposition 4.3 ([12]) E-G_{3}A^{ω} + Σ_{1}^{0}-UB ⊢ WKL.

Σ_{1}^{0}-UB implies the existence of a modulus of uniform continuity for each extensional Φ^{1(1)} on {z^{1} : z ≤_{1} y} (where ‘continuity’ refers to the usual metric on the Baire space IN^{IN}):

Proposition 4.4 ([12])

E-G_{3}A^{ω} + Σ_{1}^{0}-UB ⊢

∀Φ^{1(1)}∀y^{1}∃χ^{1}∀k^{0}∀z_{1}, z_{2} ≤_{1} y( ⋀_{i≤_{0}χk}(z_{1}i =_{0} z_{2}i) → ⋀_{j≤_{0}k}(Φz_{1}j =_{0} Φz_{2}j)).

Proposition 4.5 Let T :=E-G_{3}A^{ω}, E-PRA^{ω} or E-PA^{ω}. Then

T + QF-AC^{1,0} + QF-AC^{0,1} + F ⊢ Φ_{∞}-b-AC^{0,1}, Φ_{∞}-WKL.

12Like Φ_{n}-b-AC^{ρ,τ} (see remark 2.5), Σ_{1}^{0}-UB can be written as a single axiom. However the schematic version is easier to apply.

Proof: The idea of the proof is to use proposition 4.4 (together with propositions 4.2 and 4.3) to show similarly to the argument in the proof of proposition 2.7 that every A ∈ Φ_{n} (or ∈ Ψ_{n}) can be written as a Π_{1}^{0}-formula B. Whereas in the proof of proposition 2.7 we could use the fact that for every term t^{2}[\underline{a}] of T containing only variables \underline{a} of type ≤ 1 one can construct a modulus of uniform continuity on \{x : x ≤_{1} b\} (uniformly in \underline{a} and b), we have to use proposition 4.4 in the presence of arbitrary parameters. The latter provides such a modulus of uniform continuity only uniformly in number parameters but not uniformly in function parameters f unless the latter are themselves restricted to a compact set {f : f ≤_{1} b} (in which case a modulus that is independent of f does exist). However this is just the case in the situation at hand since all function variables f_{1}, …, f_{n} of A ∈ Φ_{n} which are not parameters are bounded and in the premise ∀x^{0}∃y ≤_{1} ax A(x, y, a) of Φ_{n}-b-AC^{0,1} the function variable y again is bounded. So all we need is

(∗) \{ \begin{matrix}∀Φ, a^{1(0)}, \underline{a}∃α^{1}∀x^{0}, z^{0}(λy^{1}, \underline{f}.(Φxzy\underline{f}a\underline{a})^{0} is uniformly continuous for all \\ y ≤_{1} ax, f_{1} ≤_{1} s_{1}[x, y, a, \underline{a}], …, f_{n} ≤_{1} s_{n}[x, y, a, \underline{a}] with modulus αxz), \end{matrix}

where \underline{a} are all the remaining free variables of s_{i} (which may have arbitrary types).^{13} Using Σ_{1}^{0}-UB one easily shows that

∀a^{1(0)}, \underline{a}∃b^{1(0)}∀x^{0}∀y ≤_{1} ax(s_{i}[x, y, a, \underline{a}] ≤_{1} bx).

Hence (∗) is (in the presence of Σ_{1}^{0}-UB) implied by

(∗∗) \{ \begin{matrix}∀Φ, a^{1(0)}, \underline{b}^{1(0)}∃α^{1}∀x^{0}, z^{0}(λy^{1}, \underline{f}.(Φxzy\underline{f}a\underline{a})^{0} is uniformly continuous for all \\ y ≤_{1} ax, f_{1} ≤_{1} b_{1}x, …, f_{n} ≤_{1} b_{n}x with modulus αxz). \end{matrix}

But this follows in T + Σ_{1}^{0}-UB (and therefore in T +QF-AC^{1,0} + F by proposition 4.2) similarly to the proof of proposition 4.4. Since by proposition 4.3 also WKL is available in this theory, we can argue as in the proof of the claim in the proof of proposition 2.7 and show that for A(a, y, x) ∈ Φ_{n} (with arbitrary additional parameters)

T + Σ_{1}^{0}-UB ⊢ ∀a^{1(0)}∃Φ∀x^{0}∀y ≤_{1} ax(A(a, y, x) ↔ ∀z^{0}(Φaxz =_{0} 0)).

Hence

(∗ ∗ ∗)T + Σ_{1}^{0}-UB ⊢ Φ_{0}-b-AC^{0,1} → Φ_{n}-b-AC^{0,1}.

13Here ‘z’ is the variable from the Π_{1}^{0}-kernel of A (which of course can be merged together with x).

We now show that (∗ ∗ ∗∗) T +QF-AC^{0,1} + Σ_{1}^{0}-UB ⊢ Φ_{0}-b-AC^{0,1} : Let

∀x^{0}∃y ≤_{1} ax∀z^{0}A_{0}(x, y, z) → ∃Y ≤_{1(0)} a∀x^{0}, z^{0}A_{0}(x, Y x, z)

be an instance of Φ_{0}-b-AC^{0,1} and assume that

∀Y ≤_{1(0)} a∃x^{0}, z^{0}¬A_{0}(x, Y x, z).

By Σ_{1}^{0}-UB we obtain (using an encoding of 1(0) into type 1)

(+)∃z^{0}∀Y ≤_{1(0)} a∃x∃z̃ ≤ z ¬A_{0}(x, Y x, z̃).

However

∀x^{0}∃y ≤_{1} ax∀z^{0} A_{0}(x, y, z)

yields

∀x^{0}, z^{0}∃y ≤_{1} ax∀z̃ ≤ z A_{0}(x, y, z̃)

and so – relative to T –

∀x^{0}, z^{0}∃y^{1}∀z̃ ≤ z A_{0}(x, min_{1}(y, ax), z̃),

which by QF-AC^{0,1} yields a contradiction to (+). (∗ ∗ ∗) and (∗ ∗ ∗∗) together with proposition 4.2 imply

T + QF-AC^{1,0} + QF-AC^{0,1} + F ⊢ Φ_{n}-b-AC^{0,1}

for every n ∈ IN.

Likewise as (∗ ∗ ∗), we obtain

T + Σ_{1}^{0}-UB ⊢ Φ_{0}-WKL → Φ_{n}-WKL

and hence (using propositions 4.3 and 3.3)

T + Σ_{1}^{0}-UB ⊢ Φ_{n}-WKL

and therefore by proposition 4.2

T + QF-AC^{1,0} + F ⊢ Φ_{n}-WKL,

which concludes the proof.

Notation: For f^{1} we define f^{M}(x) := max_{i≤x} f(i).

Theorem 4.6 Let ∀f^{1}, x^{0}∃y^{0}A_{0}(f, x, y) be a sentence of the language of T where T :=E-G_{n}A^{ω} (n ≥ 2), E-PRA^{ω} or E-PA^{ω}. Then the following rule holds

T + QF-AC^{1,0}+QF-AC^{0,1} + F ⊢ ∀f^{1}, x^{0}∃y^{0}A_{0}(f, x, y) ⇒ one can extract a closed term Ψ^{001} of T such that T̃ ⊢ ∀f^{1}, x^{0}A_{0}(f, x, Ψfx),

where

T̃ := \{ \begin{matrix}E-PA^{ω}, if T =E-PA^{ω} \\ E-PRA^{ω}, if T =E-G_{n}A^{ω} or E-PRA^{ω}. \end{matrix}

For T :=E-G_{2}A^{ω} (E-G_{3}A^{ω}, PRA^{ω}), Ψ is (provably in T ) bounded by a polynomial^{14} in f^{M}, x (Ψ is an elementary recursive functional resp. a (Kleene-)primitive recursive functional).

Proof: Extraction of Ψ: The extractability of Ψ from a proof of ∀f, x∃yA_{0}(f, x, y) in T + QF-AC^{1,0}+QF-AC^{0,1} + F with a verification in T_{−E}^{i} + F^{D} by elimination of extensionality, negative translation and subsequent monotone functional interpretation follows from (the proof of) theorem 4.9 in [12]. Here

F^{D} :≡ ∃Y ≤_{ρ} λΦ, y.y∀Φ^{2(0)}, y^{1(0)}, k^{0}, z^{1}(Φ(k, min_{1}(z, yk)) ≤_{0} Φ(k, Y Φyk)) and

T_{−E}^{i} results from T if we replace classical logic by intuitionistic logic and remove the extensionality axioms (E) (except extensionality for numbers x =_{0} y → fx =_{0} fy which we keep). From [12] it follows that Ψ is bounded by a polynomial in f^{M}, x if T =E-G_{2}A^{ω} and that Ψ is elementary recursive (resp. (Kleene-)primitive recursive) if T =E-G_{3}A^{ω} (resp. T =PRA^{ω}). As already F is not true in the full set-theoretic type structure S^{ω} this holds a fortiori for F^{D}. However, we now give a verification by a principle (∗) that is classically true): Classical verification of Ψ: By the deduction theorem for T_{−E}^{i} and direct (i.e. without preceeding negative translation) monotone functional interpretation we can extract a closed term χ of T such that

14‘Ψfx is a polynomial in f, x’ means that Ψfx can be written as a term t[f, x] which is built up from 0, S, +, · and f, x only. See [12] for a discussion of this notion.

\begin{matrix}T_{−E}^{i} ⊢ ∀Y ≤_{ρ} λΦ, y.y, f^{1}, x^{0}∃y^{1(0)}, k^{0}, z^{1} \\ (χ(Y, f, x)(k, min_{1}(z, yk)) ≤_{0} (χ(Y, f, x))(k, Y (χ(Y, f, x))yk) → A_{0}(f, x, Ψfx)). \end{matrix}

Using Howard’s majorizability as in [12] we can construct a closed term χ^{∗} which majorizes χ (provably in T^{i}) and consequently (using lemma 2.2.11 from [12])

T^{i} ⊢ ∀Y ≤ λΦ, y.y∀f, x(χ^{∗}(λΦ, y.y, f^{M}, x) maj χ(Y, f, x)).

Hence

T^{i} ⊢ ∃Y ≤_{ρ} λΦ, y.y, f^{1}, x^{0}∀Φ(Φ^{2(0)} majorizable → ∀y^{1(0)}, k^{0}, z^{1}
(Φ(k, min_{1}(z, yk)) ≤ Φ(k, Y Φyk))) → ∀f, xA_{0}(f, x, Ψfx).

Since ‘Φ majorizable’ implies that Φk is bounded on {z : z ≤_{1} yk} for all k, y and using that min_{1}(z, yk) ≤_{1} yk we obtain

T^{i} ⊢ (∗) → ∀f, x A_{0}(f, x, Ψfx),

where

(∗) :≡ \{ \begin{matrix}∃Y ≤_{ρ} λΦ, y.y∀Φ^{2(0)}, y^{1(0)}, k^{0}∀z ≤_{1} yk \\ (Φk bounded on \{v : v ≤_{1} yk\} → Φkz ≤_{0} Φ(k, Y Φyk)) \end{matrix}

with ρ = 1(0)(1(0))(2(0)). (∗) is classically true since E-PA^{ω}+AC ⊢ (∗) : By the least number principle we get

∀Φ^{2(0)}, y^{1(0)}, k^{0}(Φk bounded on {v : v ≤_{1} yk} → ∃v ≤_{1} yk∀z ≤_{1} yk(Φkz ≤_{0} Φkv))

and hence by classical logic

∀Φ^{2(0)}, y^{1(0)}, k^{0}∃v ≤_{1} yk(Φk bounded on {v : v ≤_{1} yk} → ∀z ≤_{1} yk(Φkz ≤_{0} Φkv)).

AC now yields (∗). A closer look at the proof of (∗) from E-PA^{ω}+AC above shows that only an instance of bounded choice b-AC was used. Moreover this instance can be written using only bounded quantifiers (note that ‘Φk bounded on {v : v ≤_{1} yk}’ is in fact equivalent (provably in E-PA^{ω}) to ‘∃v ≤_{1} yk∀z ≤_{1} yk(Φkz ≤_{0} Φkv)’). However we will not investigate this further but instead show that (∗) can be eliminated: Arithmetical verification of Ψ: We show that E-PA^{ω} + (∗) (resp. E-PRA^{ω} + (∗)) is conservative over E-PA^{ω} (resp. E-PRA^{ω}) w.r.t. sentences ∀f^{1}A_{0}(f), where A_{0} is quantifier-free (note that this concludes the proof of the theorem): Similarly to the proof of F̂ from MUC in [11](p. 241) one shows that

E-PA^{ω}+MUC ⊢ (∗),

where

MUC :≡ ∃Ω^{3}∀Φ^{2}∀y_{1}, y_{2} ≤_{1} 1(\overline{y}_{1}(ΩΦ) =_{0} \overline{y}_{2}(ΩΦ) → Φy_{1} =_{0} Φy_{2}).

Hence E-PA^{ω} + (∗) ⊢ ∀f^{1}A_{0}(f) implies that E-PA^{ω}+MUC ⊢ ∀f^{1}A_{0}(f). By negative translation we obtain (using that the negative translation of MUC is intuitionistically implied by MUC)

E-HA^{ω}+MUC ⊢ ∀f^{1}A_{0}(f),

where E-HA^{ω} is the intuitionistic version of E-PA^{ω}. Again as in [11](p. 241) we can conclude from there that

E-HA^{ω} ⊢ ∀f^{1}A_{0}(f).

It is not straightforward to see whether this last step which relies on non-trivial elimination arguments for choice sequences from [17] directly relativises to E-PRA^{ω}. That’s why we give a different argument for the latter system (which can be adopted also for an alternative proof for the former): In E-PRA^{ω} + Σ_{1}^{0}-IA one can show that the continuous functionals ECF form (pointwise) a model of E-PRA^{ω}. Moreover inspection of the proofs of 2.6.6,2.6.4 in [16] shows that E-PRA^{ω} + Σ_{1}^{0}-IA+Σ_{1}^{0}-UB^{−} ⊢ [MUC]_{ECF}, where Σ_{1}^{0}-UB^{−} is a restriction of Σ_{1}^{0}-UB (discussed in [12]) which allows a direct proof-theoretic elimination (see [12]). So we have

E-PRA^{ω} + Σ_{1}^{0}-IA+Σ_{1}^{0}-UB^{−} ⊢ [∀fA_{0}(f)]_{ECF}

and therefore^{15}

E-PRA^{ω} + Σ_{1}^{0}-IA+Σ_{1}^{0}-UB^{−} ⊢ ∀fA_{0}(f).

By the elimination procedure for Σ_{1}^{0}-UB^{−} ([12](thm.4.21)) and the fact that E-PRA^{ω}+ Σ_{1}^{0}-IA has (via elimination of extensionality and negative translation) a monotone functional interpretation in (E-)PRA^{ω} we obtain that E-PRA^{ω} ⊢ ∀fA_{0}(f).

15Here we use that E-PRA^{ω} ⊢ Ψf^{1} =_{0} x ↔ [Ψf]_{ECF} ≃ x for closed terms Ψ^{2} of E-PRA^{ω}. This however is easy since Ψf can be written as an ordinary primitive recursive functional in f since no higher type recursion is present in E-PRA^{ω}.

Corollary 4.7 1) E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} +Φ_{∞}-b-AC^{0,1} +Φ_{∞}-WKL is conservative over PA.

2) E-PRA^{ω}+QF-AC^{1,0}+QF-AC^{0,1} + Φ_{∞}-b-AC^{0,1} + Φ_{∞}-WKL is Π_{2}^{0}-conservative over PRA.

Proof: 1) Let A be a sentence of PA which is provable in E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+Φ_{∞}-b-AC^{0,1}+Φ_{∞}-WKL and hence in E-PA^{ω}+QF-AC^{1,0}+QF-AC^{0,1}+F. Then the Herbrand normal form A^{H} ≡ ∀\underline{f}∃\underline{y}A_{0}(\underline{f}, \underline{y}) of A is provable there a-fortiori. Hence by theorem 4.6

E-PA^{ω} ⊢ ∀\underline{f} A_{0}(\underline{f}, \underline{Ψ}(\underline{f}))

for suitable closed terms \underline{Ψ} of E-PA^{ω}. Thus

E-PA^{ω} ⊢ A^{H}.

By [8](thm.4.1) we can conclude that^{16}

PA ⊢ A.

2) For Π_{2}^{0}-sentences A the argument above relativises to E-PRA^{ω} yielding E-PRA^{ω} ⊢ A. The conclusion now follows from the well-known fact that E-PRA^{ω} is Π_{2}^{0}-conservative over PRA.

References

[1] Avigad, J., Feferman, S., Gödel’s functional (‘Dialectica’) interpretation. In: [2], pp. 337-405 (1998).

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

[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] Feferman, S., Infinity in mathematics: Is Cantor necessary?. In: G. Toraldo di Francia (ed.), L’infinito nella scienza, Istituto della Enciclopedia Italiana, Rome, pp. 151-209, 1987. Reprinted (with minor additions) in: [5].

16Warning: this argument does not apply to the subsystems E-PRA^{ω}, PRA; see [8] for a counterexample to this.

[5] Feferman, S., In the Light of Logic. Oxford University Press, 340 pp. (1998).

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

[7] Jockusch Jr., C.G., Soare, R.I., Π_{1}^{0} classes and degrees of theories. Trans. AMS 173, pp. 35-56 (1972).

[8] Kohlenbach, U., Remarks on Herbrand normal forms and Herbrand realizations. Arch. Math. Logic 31, pp. 305-317 (1992).

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

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

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

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

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

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

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

[15] Simpson, S.G., Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag. xiv+445 pp. 1999.

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

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

Recent BRICS Report Series Publications

RS-98-41 Ulrich Kohlenbach. The Computational Strength of Extensions of Weak König’s Lemma. December 1998. 23 pp.

RS-98-40 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. December 1998. 29 pp.

RS-98-39 Daniel Fridlender. An Interpretation of the Fan Theorem in Type Theory. December 1998. 15 pp. To appear in International Workshop on Types for Proofs and Programs 1998, TYPES ’98 Selected Papers, LNCS, 1999.

RS-98-38 Daniel Fridlender and Mia Indrika. An n-ary zipWith in Haskell. December 1998. 12 pp.

RS-98-37 Ivan B. Damgård, Joe Kilian, and Louis Salvail. On the (Im)possibility of Basing Oblivious Transfer and Bit Commitment on Weakened Security Assumptions. December 1998. 22 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EUROCRYPT ’99 Proceedings, LNCS, 1999.

RS-98-36 Ronald Cramer, Ivan B. Damgård, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient Multiparty Computations with Dishonest Minority. December 1998. 19 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EURO-CRYPT ’99 Proceedings, LNCS, 1999.

RS-98-35 Olivier Danvy and Zhe Yang. An Operational Investigation of the CPS Hierarchy. December 1998.

RS-98-34 Peter G. Binderup, Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. The Complexity of Identifying Large Equivalence Classes. December 1998. 15 pp.

RS-98-33 Hans Hüttel, Josva Kleist, Uwe Nestmann, and Massimo Merro. Migration = Cloning ; Aliasing (Preliminary Version). December 1998. 40 pp. To appear in 6th International Workshop on the Foundations of Object-Oriented, FOOL6 Informal Proceedings, 1998.