BRICS RS-00-49 U. Kohlenbach: Higher Order Reverse Mathematics BRICS

Basic Research in Computer Science

Higher Order Reverse Mathematics

Ulrich Kohlenbach BRICS Report Series RS-00-49 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Ulrich Kohlenbach.

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/00/49/

Higher Order Reverse Mathematics

Ulrich Kohlenbach

BRICS^{∗}

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

Abstract

In this paper we argue for an extension of the second order framework currently used in the program of reverse mathematics to finite types. In particular we propose a conservative finite type extension RCA_{0}^{ω} of the second order base system RCA_{0}. By this conservation nothing is lost for second order statements if we reason in RCA_{0}^{ω} instead of RCA_{0}. However, the presence of finite types allows to treat various analytical notions in a rather direct way, compared to the encodings needed in RCA_{0} which are not always provably faithful in RCA_{0}. Moreover, the language of finite types allows to treat many more principles and gives rise to interesting extensions of the existing scheme of reverse mathematics. We indicate this by showing that the class of principles equivalent (over RCA_{0}^{ω}) to Feferman’s nonconstructive μ-operator forms a mathematically rich and very robust class. This is closely related to a phenomenon in higher type recursion theory known as Grilliot’s trick.

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

1 Introduction

Reverse mathematics as developed by H. Friedman, S. Simpson and others (see [16] for a comprehensive treatment) focuses on the language of second order arithmetic ‘because that language is the weakest one that is rich enough to express and develop the bulk of core mathematics’ ([16], p.viii). However, as we have argued in [14], already the treatment of continuous functions f : X → Y between Polish spaces X, Y not only requires a quite complicated encoding. Even more importantly, the restricted language makes it necessary (already for X = IN^{IN}, Y = IN) to use a constructively slightly enriched definition of continuous functions whose equivalence with the usual definition cannot be proved e.g. in the finite type extension E-PA^{ω}+QF-AC^{1,0} of (a variant with function variables instead of set variables of) the second order system RCA (i.e. RCA_{0} plus full induction, where RCA_{0} is the well-known base system used in reverse mathematics, see [16]). Here QF-AC^{1,0} denotes the schema of quantifier-free choice from functions to numbers. In fact, the encoding of continuous functions used in reverse mathematics amounts (for the spaces mentioned above) to the representation of such functions via an associate in the sense of Kleene and Kreisel. This representation, however, entails implicitly a (continuous) modulus of pointwise continuity which cannot be shown (in the finite type extension of RCA mentioned above) to exist for a general continuous functional φ : IN^{IN} → IN. Of course, in the presence of arithmetical comprehension the difference between the encoding of continuous functionals and their direct treatment disappears. For functions f : 2^{IN} → IN, already the binary König’s lemma WKL suffices for this but it is open whether this holds e.g. in E-PA^{ω}+QF-AC^{1,0} (see [14] for all this).

Thus already for those parts of analysis which only deal with continuous functions, there are reasons to extend the context of reverse mathematics to the language of arithmetic in all finite types. This need becomes even more urgent if one considers principles involving non-continuous functions since whereas one can reason and quantify about continuous functions in systems based on the language of RCA_{0} (though only using the constructively enriched representation mentioned above), one cannot even talk about single non-continuous functions f : IR → IR as objects (of course it is possible to formulate ∀∃-dependencies ‘∀x ∈ IR∃!y ∈ IR A(x, y)’ such that the function f : IR → IR which is uniquely determined by this property is non-continuous.

However, the existence of this function as an object cannot even been stated in the language of second order arithmetic).

In systems formulated in the language of functionals of all finite types, however, one can represent arbitrary (and hence in particular continuous) functions between Polish spaces in a rather direct way: the language contains variables for arbitrary functions f : IN^{IN} → IN^{IN} and via the so-called standard representation of elements of Polish spaces X, Y by number theoretic functions, arbitrary functions f : X → Y are directly given as functionals Φ_{f}^{1→1} : IN^{IN} → IN^{IN} which happen to be extensional w.r.t. =_{X} and =_{Y}, where g^{1} =_{X} h^{1} iff g, h represent the same element of X (similarly for Y).

The availability of variables for arbitrary (and not just continuous) functions within the language allows for an extension of reverse mathematics. In this paper we indicate that there is in fact an interesting kind of reverse mathematics for such principles which naturally takes place over a conservative finite type extension of RCA_{0} as base system.^{1} As a natural candidate we propose the system RCA_{0}^{ω} :=E-PRA^{ω}+QF-AC^{1,0}, where E-PRA^{ω} is Feferman’s ([4],[1]) restriction of E-PA^{ω} with quantifier-free induction and predicative primitive recursion only.^{2} We will show that RCA_{0}^{ω} is conservative over RCA_{0} so that for principles which can be formalized already in RCA_{0} nothing is lost by using RCA_{0}^{ω} as the base system.

In this paper we show that the principles which relative to RCA_{0}^{ω} are equivalent to

(∃^{2}) :≡ ∃φ^{2}∀f^{1}(φf =_{0} 0 ↔ ∃x^{0}(fx =_{0} 0))

form a rich and very robust class. We conjecture that one gets further interesting and robust classes by considering other functional existence principles than (∃^{2}), like the existence of the Suslin operator ([1],[4])

1Here (and also two sentences below) we again identify the official formulation of RCA_{0} (from [16]) with its (inessential) variant with function variables instead of set variabales.

As soon as we have defined that variant precisely in the next section we will call it RCA_{0}^{2} and reserve the name RCA_{0} for the official version. Note that Friedman’s original systems proposed in [5] also had function variables.

2It is an easy exercise to show that RCA_{0}^{ω} proves the second order axiom of Σ_{1}^{0}- induction on which RCA_{0} is based upon. ‘Predicative’ here means that we have only primitive recursion in the type 0 (but with parameters of arbitrary types). So for pure types this corresponds to the primitive recursive functionals in the sense of Kleene’s ([8])

schemata S1-S8.

(Suslin): ∃S^{2}∀f^{1}(S(f) =_{0} 0 ↔ ∃g∀x(f(\overline{g}x) =_{0} 0))

This indicates that there is an interesting extension of the currently existing kind of reverse mathematics to higher order statements.

2 Description of the theory RCA_{0}^{ω}

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) n ∈ P ⇒ n + 1 := n → 0 ∈ P.

Brackets whose occurrences are uniquely determined are often omitted. For arbitrary types ρ ∈ T the degree of ρ (for short deg(ρ) ) is defined by deg(0) := 0 and deg(ρ → τ) := max(deg(τ),deg(ρ) + 1).

The theory E-PRA^{ω} is based on many–sorted classical logic formulated in the language of all finite types plus the combinators Π_{ρ,τ}, Σ_{δ,ρ,τ} which allow the definition of λ–abstraction. Furthermore we include 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 ρ = ρ_{1} → … → ρ_{k} → 0). In addition to the defining axioms for the combinators, the Kleene recursor constant R_{0}, the equality axioms for type-0 equality and the successor axioms we have the schema of quantifier-free induction

QF-IA: A_{0}(0) ∧ ∀x(A_{0}(x) → A_{0}(x′)) → ∀xA_{0}(x),

where A_{0} is quantifier-free. This finishes the description of E-PRA^{ω}. The theory 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 quantifier-free choice for the types ρ, τ is given by

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

where A_{0} is quantifier-free.

The theory RCA_{0}^{ω} is defined as

RCA_{0}^{ω} :=E-PRA^{ω}+QF-AC^{1,0}.

In deviating slightly from the ‘official’ definition of RCA_{0} with set variables we define a version with function variables as follows

RCA_{0}^{2} :=E-PRA^{2}+QF-AC^{0,0},

where E-PRA^{2} denotes the second order fragment of E-PRA^{ω} (see [12] for details).

The base system RCA_{0} used in reverse mathematics can easily be seen as a subsystem of RCA_{0}^{2} by identifying sets with their characteristic functions. The axiom schemata of Σ_{1}^{0}-induction and Δ_{1}^{0}-comprehension from RCA_{0} are then easily derivable in RCA_{0}^{2} by QF-AC^{0,0} and – in the case of Σ_{1}^{0}-IA – the primitive recursive function

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

Conversely, RCA_{0}^{2} can be viewed as an inessential extension of RCA_{0} by indentifying functions with their graphs. The only ‘extension’ provided by RCA_{0}^{2} is the existence of primitive recursive type-2-functionals (in the sense of Kleene) which allow to define a new function g := Φ(f) primitive recursively in a function f. However, this can be simulated in RCA_{0} in the form ∀f∃gA_{Φ}(f, g), where A_{Φ}(f, g) expresses in terms of recursion equations that g = Φ(f).

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

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

Definition 2.1 (Troelstra(74)) WKL:≡ ∀f^{1}(T^{∞}(f) → ∃b ≤_{1} λk.1∀x^{0}(f(\overline{b}x) =_{0} 0)), where

T^{∞}(f) :≡ \{ \begin{matrix}∀n^{0}, m^{0}(f(n ∗ m) =_{0} 0 → fn =_{0} 0) \\ ∧∀n^{0}, x^{0}(f(n ∗ ⟨x⟩) =_{0} 0 → x ≤_{0} 1) \\ ∧∀x^{0}∃n^{0}(lth n =_{0} x ∧ fn =_{0} 0) \end{matrix}

(i.e. T^{∞}(f) asserts that f represents an infinite 0,1–tree).

3 First steps towards reverse mathematics in higher types

In this section we show that various analytical principles are equivalent to (∃^{2}) (over our base system RCA_{0}^{ω}). The fact that the class of these principles is rather rich and robust is mainly due to the following facts

1. a great deal of non-continuous analysis can be done already in RCA_{0}^{ω} + (∃^{2})

2. if a principle A implies the existence of a non-continuous function, then one can use an argument known as Grilliot’s trick (see [7]) to derive the existence of (∃^{2}).

We first show that nothing is lost by working relative to the base system RCA_{0}^{ω} instead of RCA_{0}^{2}:

Proposition 3.1 RCA_{0}^{ω} is a conservative extension of RCA_{0}^{2}.

Proof: Locally, one can show in RCA_{0}^{2} that the type structure ECF of all extensional hereditarily continuous functionals (see [17] for the technical definition) forms a model of RCA_{0}^{ω}, i.e.

(1) RCA_{0}^{ω} ⊢ A ⇒ RCA_{0}^{2} ⊢ [A]_{ECF}.

Together with the fact that

(2) RCA_{0}^{2} ⊢ ∀f^{1}(Φ(f) =_{0} [Φ]_{ECF}(f))

for all ordinary primitive recursive functionals Φ^{2} of type 2 (i.e. the functionals definable in RCA_{0}^{2}) this yields the conservation result.

(1) is proved similarly to (and in fact easier than) the corresponding result for E-HA^{ω}+QF-AC from [17](2.6.20). In particular, no induction beyond Σ_{1}^{0}-IA is needed. ⊣

As a corollary of proposition 3.1 we get that the finite type extensions RCA_{0}^{ω}+WKL and RCA_{0}^{ω} + Π_{∞}^{0}-CA etc. of the second order systems used in reverse mathematics are conservative over their second order part. However, we are now in the position to state conservation results which could not even been expressed with second order systems:

Theorem 3.2 ([4]) RCA_{0}^{ω}+(∃^{2}) is conservative over first order Peano arithmetic PA.

Definition 3.3 1. For k^{0}, f^{1} we define

( lim_{n→∞} f(n) =_{0} k) :≡ ∃n∀m > n(f(m) =_{0} k).

2. For g^{1}, g_{(·)}^{0→1} we define

( lim_{n→∞} g_{n} =_{1} g) :≡ ∀k∃n∀m > n(\overline{g_{m}}(k) =_{0} \overline{g}(k)).

3. A functional Φ^{2} is everywhere sequentially continuous if

∀g^{1}, ∀g_{(·)}^{0→1}( lim_{n→∞} g_{n} =_{1} g → lim_{n→∞} Φ(g_{n}) =_{0} Φ(g)).

4. A functional Φ^{1→1} is everywhere sequentially continuous if

∀g^{1}, ∀g_{(·)}^{0→1}( lim_{n→∞} g_{n} =_{1} g → lim_{n→∞} Φ(g_{n}) =_{1} Φ(g)).

Lemma 3.4 RCA_{0}^{ω} proves that the existence of a not everywhere sequentially continuous functional Φ^{1→1} implies the existence of a not everywhere sequentially continuous functional Ψ^{2}.

Proof: Define Φ̃(f, k) := \overline{Φ(f)}(k). If λf.Φ̃(f, k) is everywhere sequentially continuous for all fixed k then Φ is everywhere sequentially continuous. So if Φ is not everywhere sequentially continuous there must exist a k such that Ψ := λf.Φ̃(f, k) is not everywhere sequentially continuous. ⊣

The following result essentially is the observation that a recursion theoretic argument known as ‘Grilliot’s trick’ can be carried out in RCA_{0}^{ω}:

Proposition 3.5 Relative to RCA_{0}^{ω} the following principles are equivalent:

1. (∃^{2}),

2. there exists a functional Φ^{2} which is not everywhere sequentially continuous.

3. there exists a functional Φ^{1→1} which is not everywhere sequentially continuous.

Proof: 1. → 2. and 2. → 3. are obvious. 3. → 2. follows from lemma 3.4. So it remains to show that 2. → 1.

2. implies the existence of Φ^{2}, g_{(·)}^{0→1}, g^{1} such that

∀n∃m(\overline{g_{m}}(n) = \overline{g}(n) ∧ Φ(g_{m}) ≠ Φ(g)).

With QF-AC^{0,0} this yields

∃h^{1}∀n(\overline{g_{h(n)}}(n) = \overline{g}(n) ∧ Φ(g_{h(n)}) ≠ Φ(g)).

So with g̃_{n}(k) := g_{h(n+1)}(k) and Φ̃(f) := \{ \begin{matrix}1, if Φ(f) ≠ Φ(g) \\ 0, otherwise \end{matrix} we get

∀n∀i ≤ n(g̃_{n}(i) = g(i)) ∧ ∀n, m(Φ̃(g̃_{n}) = Φ̃(g̃_{m}) ≠ Φ̃(g)).

We are now in the position to apply Grilliot’s trick as in the proof of prop.3.4 in [13]. For completeness we repeat that short argument here: In RCA_{0}^{ω} we can define a functional ξ(f^{1}, g̃_{(·)}^{0→1}, i^{0}) such that

ξ(f, g̃_{(·)}, i) = \{ \begin{matrix}g̃_{j}(i), for the least j < i such that f(j) > 0 if it exists \\ g̃_{i}(i), otherwise. \end{matrix}

Using ∀j∀i ≤ j(g̃_{j}(i) = g̃_{i}(i)) and ∀i(g̃_{i}(i) = g(i)) one gets

(1) ∃j(f(j) > 0) → ξ(f, g̃_{(·)}) =_{1} g̃_{j} for the least such j

and

(2) ∀j(f(j) = 0) → ξ(f, g̃_{(·)}) =_{1} g.

Hence by the extensionality axiom for type-2-functionals we obtain

∀j(f(j) = 0) ↔ Φ̃(ξ(f, g̃_{(·)}) = Φ̃(g).

Thus φ := λf^{1}.\overline{sg} ∘ |Φ̃(ξ(\overline{sg} ∘ f, g̃_{(·)}) − Φ̃(g)|, where \overline{sg}(x) := 0 for x ≠ 0 and \overline{sg}(x) := 1 otherwise, satisfies (∃^{2}). ⊣ Definition 3.6

1. (μ^{2}) :≡ ∃μ^{2}∀f^{1}(∃x^{0}(fx = 0) → f(μf) = 0) (see [4]),

2. The uniform weak König’s lemma UWKL is the principle

UWKL :≡ ∃Φ^{1→1}∀f^{1}(T^{∞}(f) → ∀x^{0}(f((\overline{Φf})x) = 0)) ([13]).

Proposition 3.7 ([13]) Relative to RCA_{0}^{ω} the following principles are pairwise equivalent:

(i) (∃^{2}),

(ii) (μ^{2}),

(iii) UWKL.

Remark 3.8 In addition to WKL and UWKL one can also consider an intermediate ‘weak’ uniform version of WKL which asserts for every given sequence (f_{n})_{n∈IN} of infinite binary trees the existence of a sequence (b_{n})_{n∈IN} of infinite paths b_{n} of f_{n}. This version however is implied already by WKL (relative to RCA_{0}^{ω}).

We now sketch the representation of real numbers and functions f : IR → IR but only to the very limited extent needed here (for more details see [2],[9] and [11]. A systematic treatment of a general theory of representations can be found in [19]). Rational numbers are represented as codes j(n, m) of pairs (n, m) of natural numbers n, m. j(n, m) represents

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

Here j is the surjective pairing function j(x, y) := \frac{1}{2}((x + y)^{2} + 3x + y). On the codes of Q, i.e. on IN, we have an equivalence relation by

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

and analogously in the remaining cases, where \frac{a}{b} = \frac{c}{d} is defined to hold iff ad =_{0} cb (for bd > 0).

On IN one easily defines functions | · |Q, +Q, −Q, ·Q :Q, maxQ, minQ ∈ RCA_{0}^{ω} and (quantifier–free) relations <Q, ≤Q which represent the corresponding functions and relations on Q. We sometimes omit the index Q if this does not cause any confusion. We write ⟨q⟩ to denote the canonical code of q ∈ Q. We next want to represent real numbers as Cauchy sequences of rational number with rate of convergence 2^{−n}. Using the encoding of rational numbers by natural numbers, such a Cauchy sequence is given by a function f^{1} satisfying

(∗) ∀n∀m, m̃(m, m̃ ≥ n → |f(m) −Q f(m̃)| <Q ⟨2^{−n}⟩).

(∗) is implied by

(∗∗) ∀n(|f(n) −Q f(n + 1)| <Q ⟨2^{−n−1}⟩)

and conversely for any f satisfying (∗), f̃(n) := f(n + 1) satisfies (∗∗). That is why we can use the more convenient condition (∗∗) on our representing sequences instead of (∗). To achieve that any function f^{1} can be viewed as a representative of (a uniquely determined) real number we use the construction

f̂(n) := \{ \begin{matrix}f(n), if ∀k < n(|f(k) −Q f(k + 1)|Q <Q ⟨2^{−k−1}⟩), \\ f(k) for the least k < n s.t. |f(k) −Q f(k + 1)| ≥Q ⟨2^{−k−1}⟩, \\ otherwise. \end{matrix}

f̂ always satisfies (∗∗) and if already f satisfies (∗∗) then f =_{1} f̂. So in particular ˆ f̂ =_{1} f̂. On the representatives of reals, i.e. on the number theoretic functions f_{1}^{1}, f_{2}^{1}, we can define an equivalence relation =_{IR}

f_{1} =_{IR} f_{2} :≡ ∀n(f̂_{1}(n + 1) −Q f̂_{2}(n + 1)| <Q ⟨2^{−n}⟩),

which holds iff f_{1} and f_{2} represent the same real number. Similarly one defines relations ≤_{IR} and <_{IR}. Note that =_{IR}, ≤_{IR}∈ Π_{1}^{0} while <_{IR}∈ Σ_{1}^{0}. The usual arithmetical operations +_{IR}, −_{IR} etc. can easily be defined as functionals (definable in RCA_{0}^{ω}) on the representation of the real numbers. Functions F : IR → IR are represented as functionals Φ^{1→1} which satisfy

∀f_{1}, f_{2}(f_{1} =_{IR} f_{2} → Φ(f_{1}) =_{IR} Φ(f_{2})).

In a similar but technically somewhat more involved way one can also represent more general Polish spaces X, Y by IN^{IN} and functions F : X → Y as functionals Φ^{1→1} respecting the corresponding equivalence relations =_{X} and =_{Y} (for details see e.g. [9]).

Lemma 3.9 RCA_{0}^{ω} proves

1. ∀f_{1}, f_{2}, n(\overline{f}_{1}(n + 2) =_{0} \overline{f}_{2}(n + 2) → |f_{1} −_{IR} f_{2}| <_{IR} ⟨2^{−n}⟩).

2. ∀f^{1}, f_{(·)}^{0→1}(∀n(|f_{n} −_{IR} f| <_{IR} ⟨2^{−n−2}⟩ → ∃f̃^{1}, f̃_{(·)}^{0→1}(f̃ =_{IR} f ∧ ∀n(f̃_{n} =_{IR} f_{n} ∧ \overline{f̃_{n}}(n) =_{0} \overline{f̃}(n)))).

Proof: 1. follows from

\overline{f}_{1}(n + 2) = \overline{f}_{2}(n + 2) → \overline{f̂_{1}}(n + 2) = \overline{f̂_{2}}(n + 2)

and

|f −_{IR} λk.f̂(n + 1)| <_{IR} ⟨2^{−n−1}⟩.

2. Define f̃:= λk.f̂(k + 3), f̃_{n}(k) := \{ \begin{matrix}f̂_{n}(k + 3), for k ≥ n \\ f̂(k + 3), for k < n. \end{matrix}

It is clear that

f̃ =_{IR} f ∧ ∀n(\overline{f̃_{n}}(n) =_{0} \overline{f̃}(n)).

It remains to show that ∀n(f̃_{n} =_{IR} f_{n}). This easily follows from the fact that f̃_{n} satisfies (∗∗) (so that ˆ f̃_{n} =_{1} f̃_{n} for all n). Thus we have to show the latter. The only problematic case is |f̃_{n}(n − 1) −Q f̃_{n}(n)| < ⟨2^{−n}⟩ (for n ≥ 1) which we establish as follows (using the assumption ∀n(|f_{n} −_{IR} f| <_{IR} ⟨2^{−n−2}⟩):

|f̃_{n}(n − 1) −Q f̃_{n}(n)| =Q |f̂(n + 2) −Q f̂_{n}(n + 3)|
≤Q |f̂(n + 2) −Q f̂_{n}(n + 2)| + |f̂_{n}(n + 2) −Q f̂_{n}(n + 3)|
≤_{IR} |λk.f̂(n + 2) −_{IR} f| + |f −_{IR} f_{n}| + |f_{n} −_{IR} λk.f̂_{n}(n + 2)|
+|f̂_{n}(n + 2) −Q f̂_{n}(n + 3)|
<_{IR} ⟨2^{−n−2} + 2^{−n−2} + 2^{−n−2} + 2^{−n−3}⟩ <Q ⟨2^{−n}⟩.

⊣

Proposition 3.10 The following principles are pairwise equivalent relative to RCA_{0}^{ω}:

1. (∃^{2}), 2. the function F : IR → IR determined by

F (x) := \{ \begin{matrix}0, for x ≤_{IR} 0 \\ 1, for x >_{IR} 0 \end{matrix}

exists,

3. there exists a function F : IR → IR which is not everywhere sequentially continuous.

Proof: 1. → 2. and 2. → 3. are obvious. It remains to show that 3. → 1. Let F : IR → IR, x ∈ IR and (x_{n}) be a sequence in IR such that

x_{n} → x ∧ ¬(F (x_{n}) → F (x)),

where ‘→’ indicates convergence in the sense of IR. Then

∃l∀k∃n(|x_{n} −_{IR} x| <_{IR} ⟨2^{−k}⟩ ∧ |F (x_{n}) −_{IR} F (x)| >_{IR} ⟨2^{−l}⟩).

Since <_{IR}∈ Σ_{1}^{0}, we can apply QF-AC^{0,0} to obtain

∃l∃g∀k(|x_{g(k)} −_{IR} x| <_{IR} ⟨2^{−k−3}⟩ ∧ |F (x_{g(k)}) −_{IR} F (x)| >_{IR} ⟨2^{−l}⟩).

Lemma 3.9.b) applied to f_{k} := x_{g(k)} yields f̃_{k}, f̃ with

f̃ =_{IR} x ∧ ∀k(f̃_{k} =_{IR} x_{g(k)} ∧ \overline{f̃_{k}}(k) =_{0} \overline{f̃}(k)).

F is given by some functional Φ^{1→1}. Using the extensionality of Φ w.r.t. =_{IR} we get

∀k(|Φ(f̃_{k}) −_{IR} Φ(f̃)| >_{IR} ⟨2^{−l}⟩)

and hence by lemma 3.9.a)

∀k(\overline{Φ(f̃_{k})}(l + 2) ≠ \overline{Φ(f̃)}(l + 2)).

So put together we have shown that

∃l∀k(\overline{f̃}_{k}(k) =_{0} \overline{f̃}(k) ∧ \overline{Φ(f̃_{k})}(l + 2) ≠ \overline{Φ(f̃)}(l + 2)).

Hence Φ^{1→1} is not everywhere sequentially continuous (in the sense of definition 3.3.4). By proposition 3.5 this implies (∃^{2}). ⊣ Proposition 3.11 With RCA_{0}^{ω} replaced by RCA_{0}^{ω}+QF-AC^{0,1} one can add

‘4. there exists a function F : IR → IR which is not everywhere ε-δ-continuous’

to the list of equivalences in proposition 3.10.

Proof: This follows from the fact that E-PRA^{ω}+QF-AC^{0,1} proves the (local) equivalence of sequential and ε-δ-continuity of F : IR → IR in any point x ∈ IR (see theorem 4.1 in [14]). ⊣

Notation: \overline{C} denotes the space of all functions f ∈ C[0, 1] with f(0) ≤ 0 ∧ f(1) ≥ 0.

We now consider uniform versions of the following principles:

1. the intermediate value theorem:

∀f ∈ \overline{C} ∃x ∈ [0, 1](f(x) =_{IR} 0),

2. the attainment of the maximum principle: ∀f ∈ C([0, 1]^{d})∃x ∈ [0, 1]^{d}∀y ∈ [0, 1]^{d}(f(x) ≥_{IR} f(y)),

3. Brouwer’s fixed point theorem:

∀f ∈ C([0, 1]^{d}, [0, 1]^{d})∃x ∈ [0, 1]^{d}(f(x) =_{IR}_{d} x).

These principles differ in strength: whereas 2. and 3. imply (already for continuous functions as defined in reverse mathematics) WKL, 1.can be proved in RCA_{0}^{ω} (see [16]). In fact, there is also some difference between 2. and 3., since even the restriction of 2. to uniformly continuous functions which are given with a modulus of uniform continuity implies WKL whereas 3. is provable in RCA_{0} for such functions (see the proof of thm.5.1.b in [15]). In contrast to this, the uniform versions of 1.-3. are all equivalent to (∃^{2}) (indepedently of whether e.g. f ∈ C[0, 1] is given as a type-2 functional, with a code in the sense of reverse matheatics, or even with a modulus of uniform continuity).

Proposition 3.12 The following principles are pairwise equivalent relative to RCA_{0}^{ω}:

1. (∃^{2}),

2. ∃F : \overline{C} → [0, 1]∀f ∈ \overline{C} (f(F (f)) =_{IR} 0), 3. the restriction of 2) to Lipschitz continuous functions with λ = 1,

4. ∃F : C([0, 1]^{d}) → [0, 1]^{d}∀f ∈ C([0, 1]^{d})∀y ∈ [0, 1]^{d}(f(F (f)) ≥_{IR} f(y)),

5. the restriction of 4) to Lipschitz continuous functions with λ = 1,

6. ∃F : C([0, 1]^{d}, [0, 1]^{d}) → [0, 1]^{d}∀f ∈ C([0, 1]^{d}, [0, 1]^{d})(f(F (f)) =_{IR}_{d} F (f)).

7. the restriction of 6) to Lipschitz continuous functions with λ = 1.

Proof: It is a routine verification, that 2.-7. can be proved within RCA_{0}^{ω} + (∃^{2}) by inspecting the proofs of the non-uniform versions of these theorems. This holds true even if f ∈ C[0, 1] (and similarly f ∈ C([0, 1]^{d}) and f ∈ C([0, 1]^{d}, [0, 1]^{d})) is given just as a functional of type 1 → 1 which happens to be ε-δ-continuous w.r.t. the usual topologies of [0, 1] and IR, but without any witness information for this continuity. We sketch this for 4. and d = 1: Let r_{n} be a suitable enumeration of all rational numbers in [0, 1] and define^{3}

g(n) := \{ \begin{matrix}μi ≤ 2^{n} − 1[∀k^{0}, l^{0}∃j^{0}(r_{j} ∈ [\frac{i}{2^{n}} , \frac{i+1}{2^{n}}] ∧ f(r_{j}) ≥_{IR} f(r_{k}) − 2^{−l})], \\ if existent \\ 0^{0}, otherwise. \end{matrix}

Note that g is (Kleene-)primitive recursively definable in (∃^{2}) and (a functional representing) f since the property ‘[…]’ is arithmetical. In RCA_{0}^{ω} + (∃^{2}) one easily shows that the case ‘otherwise’ cannot occur. Moreover, using the continuity of f it follows that (g(n)/2^{n})_{n∈IN} is a Cauchy sequence with rate of convergence 2^{−n} which converges to the least x ∈ [0, 1] such that f(x) = sup_{y∈[0,1]} f(y). We now prove that any of 2.-7. implies (∃^{2}). It is clear that it suffices to consider the case of Lipschitz continuous functions. We show this now for 3. (for 5. and 7. the proofs are very similar): Let f_{0} : [0, 1] → IR be the constant-0-function f_{0}(x) := 0. C is the space of all Lipschitz continuous functions f ∈ C[0, 1] with Lipschitz constant λ = 1 satisfying f(0) ≤ 0, f(1) ≥ 0, and F : C → [0, 1] is a function that satisfies 3. Case 1: F (f_{0}) ∈ [0, \frac{1}{2}]. For y ∈ [0, 1], define f_{y} : [0, 1] → IR by f_{y}(x) := yx−y. f_{y} ∈ C and f_{y}(0) ≤ 0, f_{y}(1) ≥ 0 for all y ∈ [0, 1]. Moreover,

∀y ∈ (0, 1]∀x ∈ [0, 1](f_{y}(x) =_{IR} 0 ↔ x =_{IR} 1).

3For notational simplicity we write here \frac{i}{2^{n}} and 2^{−l} instead of their codes.

Hence

∀y ∈ (0, 1](F (f_{y}) =_{IR} 1).

Define g : [0, 1] → IR by g(y) := F (f_{y}). Then g(0) = F (f_{0}) ∈ [0, \frac{1}{2}] and

∀y ∈ (0, 1](g(y) = F (f_{y}) = 1).

Hence, ĝ : IR → IR, ĝ(y) := g(min_{IR}(1, max_{IR}(0, y)) is not sequentially continuous at y := 0. Case 2: F (f_{0}) ∈ [\frac{1}{2}, 1]. Analogously to case 1 but with f_{y}(x) := yx. In both case we have constructed (Kleene-)primitive recursively in F a function g : IR → IR which is not everywhere sequential continuous. Hence, proposition 3.10 yields the existence of (∃^{2}). ⊣

Above we saw that certain principles which in their non-uniform version are different w.r.t. to the set existence axioms needed to prove them are equivalent in their uniform formulation. We now indicate that also the opposite phenomenon can occur: Consider again the attainment of the maximum principle (for simplicity only for dimension 1)

(a) ∀f ∈ C[0, 1]∃x ∈ [0, 1]∀y ∈ [0, 1](f(x) ≥_{IR} f(y))

and also the existence of the supremum

(b) ∀f ∈ C[0, 1]∃y ∈ IR(y =_{IR} sup_{x∈[0,1]} f(x)).

¿From ordinary reverse mathematics it is well-known that both principles are equivalent to WKL (relative to RCA_{0} and using the encoding of such functions as pointwise continuous functions as in [16]), i.e. without a modulus of uniform continuity). We saw above that the uniform version of (a) is equivalent to (∃^{2}) (independently of whether f is assumed to be uniformly continuous or even given with a modulus of uniform continuity or not). Let’s consider the uniform version of (b). The status now depends on the representation: it is easy to define a functional in RCA_{0}^{ω} which computes the supremum of f uniformly in f and a modulus of uniform continuity of f. If, however, f is just given as a pointwise continuous functions one has to compute a modulus of uniform continuity first. This can be achieved uniformly in f (given as a functional φ^{1→1} which is extensional w.r.t. =_{IR}) by the following so-called fan functional

(MUC): ∃Ω^{3}∀φ^{2}∀f_{1}, f_{2} ≤_{1} 1(\overline{f_{1}}(Ω(φ)) =_{0} \overline{f_{2}}(Ω(φ)) → φ(f_{1}) =_{0} φ(f_{2})).

(MUC) is inconsistent with (∃^{2}) but consistent relative to RCA_{0}^{ω}. Moreover, adapting the proof of theorem 2.6.4 in [17] one can show

Proposition 3.13 RCA_{0}^{ω}+MUC is conservative over RCA_{0}^{2}+WKL (and hence Π_{2}^{0}-conservative over PRA).

Since the uniform version of (b) (for pointwise continuous functions)^{4} can be proved in RCA_{0}^{ω}+MUC it is proof-theoretically weaker than the uniform version of (a).

Final Comments:

1. The equivalence results established in this paper also hold for the subsystem RCA_{0}^{ω^{∗}} :=E-G_{3}A^{ω}+QF-AC^{1,0} of RCA_{0}^{ω} with elementary recursive functionals only (i.e. E-G_{3}A^{ω} only contains 0, S, +, ·, exp and bounded predicative recursion). The absence of Φ_{it} blocks the derivability of Σ_{1}^{0}-IA and, in fact, RCA_{0}^{ω^{∗}} (which is a higher order extension of the system RCA_{0}^{∗} from [16]) is Π_{2}^{0}-conservative over Kalmarelementary arithmetic EA.

2. The results in this paper depend crucially on the fact that our system RCA_{0}^{ω} contains full extensionality (for type-2-objects). In [13] we have shown that in a setting where (E) is replaced by Spector’s weak quantifier-free rule of extensionality e.g. UWKL is as weak as WKL.

3. One could argue to use instead of systems based on a fixed system of finite types more flexible systems like Feferman’s systems of explicit mathematics are appropriate subsystems of (classical versions of) Martin-Löf type theories. However, in neither of these settings has been formulated a natural equivalent to the system WKL_{0}, i.e. a system with the same mathematical strength then WKL_{0} but which at the same time allows a finitistic reduction to primitive recursive arithmetic PRA. The problem here seems to be that these frameworks treat a principle like WKL automatically in its uniform version UWKL which, however, is (in an extensional setting) proof-theoretically as strong as (∃^{2}) as we saw above. In our view it is one of the most interesting outcomes of reverse mathematics that large parts of mathematics can be carried out in a PRA-reducible system like WKL_{0}.

4Actually, MUC even suffices to prove this for arbitrary functions f : IR → IR. We don’t know whether the (classically valid) restriction of MUC to pointwise continuous functionals φ^{2} suffices to prove the uniform version of (b). The problem is, that the pointwise continuity of f : IR → IR does not imply that a functional φ^{1→1} representing f is pointwise continuous in the sense of the Baire space.

References

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

[2] Beeson, M.J., Foundations of Constructive Mathematics. Springer Ergebnisse der Mathematik und ihrer Grenzgebiete 3.Folge, Bd.6., Berlin Heidelberg New York Tokyo 1985.

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

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

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

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

[7] Grilliot, T.J., On effectively discontinuous type-2 objects. J. Symbolic Logic 36, pp. 245–248 (1971).

[8] Kleene, S.C., Recursive functionals and quantifiers of finite types I. Trans Amer.Math. Soc. 91, pp. 1-52 (1959).

[9] Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallee Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic 64, pp. 27-94 (1993).

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

[11] Kohlenbach, U., Proof theory and computational analysis. Electronic Notes in Theoretical Computer Science, Vol. 13, Elsevier (1998).

[12] Kohlenbach, U., Things that can and things that can’t be done in PRA. Ann. Pure Appl. Logic 102, pp. 223-245 (2000).

[13] Kohlenbach, U., On the uniform weak König’s lemma. To appear in: Ann. Pure Appl. Logic (special issue in honor of Professor A. S. Troelstra).

[14] Kohlenbach, U., Foundational and mathematical uses of higher types. To appear in forthcoming Festschrift in honor of Professor Solomon Feferman.

[15] Shioji, N., Tanaka, K., Fixed point theory in weak second-order arithmetic. Ann. Pure Appl. Logic 47, pp. 167-188 (1990).

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

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

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

[19] Weihrauch, K., Computable Analysis. Springer, Berlin 2000.

Recent BRICS Report Series Publications

RS-00-49 Ulrich Kohlenbach. Higher Order Reverse Mathematics. December 2000. 18 pp.

RS-00-48 Marcin Jurdziński and Jens Vöge. A Discrete Stratety Improvement Algorithm for Solving Parity Games. December 2000.

RS-00-47 Lasse R. Nielsen. A Denotational Investigation of Defunctionalization. December 2000. Presented at 16th Workshop on the Mathematical Foundations of Programming Semantics, MFPS ’00 (Hoboken, New Jersey, USA, April 13–16, 2000).

RS-00-46 Zhe Yang. Reasoning About Code-Generation in Two-Level Languages. December 2000.

RS-00-45 Ivan B. Damgård and Mads J. Jurik. A Generalisation, a Simplification and some Applications of Paillier’s Probabilistic Public-Key System. December 2000. 18 pp. To appear in Fourth International Workshop on Practice and Theory in Public Key Cryptography, PKC ’01 Proceedings, LNCS, 2001. This revised and extended report supersedes the earlier BRICS report RS-00-5.

RS-00-44 Bernd Grobauer and Zhe Yang. The Second Futamura Projection for Type-Directed Partial Evaluation. December 2000. To appear in Higher-Order and Symbolic Computation. This revised and extended report supersedes the earlier BRICS report RS-99-40 which in turn was an extended version of Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’00 Proceedings, 2000, pages 22–32.

RS-00-43 Claus Brabrand, Anders Møller, Mikkel Christensen, Ricky, and Michael I. Schwartzbach. PowerForms: Declarative Client-Side Form Field Validation. December 2000. 21 pp. To appear in World Wide Web Journal, 4(3), 2000.

RS-00-42 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. The <bigwig> Project. December 2000. 25 pp.

RS-00-41 Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. The DSD Schema Language and its Applications. December 2000. 32 pp. Shorter version appears in Heimdahl, editor, 3rd ACM SIGSOFT Workshop on on Formal Methods in Software Practice, FMSP ’00 Proceedings, 2000, pages 101–111.