BRICS RS-02-31 Kohlenbach & Oliva: Proof Mining: A Systematic Way of Analysing Proofs in Mathematics BRICS

Basic Research in Computer Science

Proof Mining: A Systematic Way of Analysing Proofs in Mathematics

Ulrich Kohlenbach Paulo B. Oliva BRICS Report Series RS-02-31 ISSN 0909-0878 June 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Ulrich Kohlenbach & Paulo B. Oliva.

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/02/31/

Proof Mining: A Systematic Way of Analysing Proofs in Mathematics

Ulrich Kohlenbach  Paulo Oliva
BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract

We call proof mining the process of logically analyzing proofs in mathematics with the aim of obtaining new information. In this survey paper we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that those techniques not only apply to proofs based on classical logic, but also to proofs which involve non-effective principles such as the attainment of the infimum of f ∈ C[0, 1] and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and fixed point theory where new results were obtained.

1 Introduction

Many theorems in mathematics can be expressed as simple equations e.g. stating that x as an element of some Polish space X is a root of a function f : X → ℝ. Theorems of this kind have been called complete. Such (essentially purely universal) theorems do not ask for any effective witnessing information. On the other hand, a theorem stating that f is (strictly) positive at a point x ∈ X is incomplete, for it leaves open how far from zero the value f(x) actually is. As a more intricate example, consider an implication between incomplete theorems such as

∗Basic Research in Computer Science, funded by the Danish National Research Foundation.

∀x ∈ X∀y ∈ K (f(x, y) ≠^{ℝ} 0 → g(x, y) ≠^{ℝ} 0),  (1)

where f, g : X × K → ℝ are continuous functions from the Polish space X and the compact Polish space K to the real numbers. Theorems of the form (1) can also be considered incomplete, since when f(x, y) is apart from zero by ε, the value g(x, y) must also be apart from zero by some δ. Until the relation between ε and δ is explicitly given theorem (1) would be considered incomplete. Interestingly enough, an implication between complete theorems can again become incomplete. Consider a theorem of the form

∀x ∈ X∀y ∈ K (f(x, y) =^{ℝ} 0 → g(x, y) =^{ℝ} 0).  (2)

If the value of f(x, y) is zero then the function g must also be zero at (x, y). Theorem (2), however, does not actually tell us how close to zero f(x, y) must be in order to make sure that g(x, y) is ε-close to zero. In other words, we still need a functional Φ satisfying: If |f(x, y)| ≤ Φ(x, y, ε) then |g(x, y)| ≤ ε. As we shall see in the following, the compactness of the space K will in general guarantee that such a Φ can be given independently of y.

It turns out that in many cases the information missing in an incomplete theorem can be extracted by purely logical analysis out of prima-facie ineffective proofs of the theorem. That is the main goal of proof mining. The program of proof mining goes back to G. Kreisel under the name of unwinding proofs^{1}. Already in the 50’s Kreisel called for a shift of emphasis in proof theoretic research guided by the question:

“What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”

1For discussions on the original program of Kreisel see [26, 69]. For an earlier approach for giving an effective interpretation of ineffective proofs of purely existential statements see [74].

Although proof mining has been applied e.g. to number theory [68, 69], combinatorics [8, 27] and algebra [22], the area of analysis, specially numerical functional analysis, is of particular interest. In analysis ineffectivity is due not only to the use of non-constructive logical reasoning but at the core of many principles (like compactness arguments) which are used to ensure convergence and which provably rely on the existence of non-computable reals. This paper surveys the main technique of monotone functional interpretation [48] currently used in proof mining in analysis and reports on recent case studies in approximation theory and fixed point theory where new results have been obtained.

The first step in analyzing the proof of a theorem consists of fixing the formal system needed for carrying out the proof of the theorem. That means: restricting the mathematical language and mathematical principles to be used in the proof. Fixing a restricted language enables us to pin point the logical form and logical complexity of the theorem. The restriction on the principles used dictates the techniques to be applied in the extraction and at the same time provides an a priori upper bound on the computational complexity of the functional realizing the theorem. The formal system which can be used to formalize a proof is clearly not unique. By showing that the proof can be formalized in a weak system interesting a priori information can be already obtained in this first step of proof mining. On the other hand, stronger systems will usually make the formalization of the proof and the extraction of information much simpler. Therefore, the choice of the mathematical strength of formal system is a compromise between a priori information and flexibility in formalizing the proof. As is confirmed by case studies, the proof theoretic techniques we are using are faithful to the numerical content of the actual proof analysed and the computational complexity of the extracted functional depends only on that proof, and not on the formal system used for the formalization and extraction. Hence, using weak systems is only an advantage when the a priori information is the only knowledge one wants to obtain. If the extraction of an actual functional is to be carried out, it is reasonable to choose a richer formal system in which proofs can be more easily formalized. The hard part then consists in performing the extraction of the functional. Therefore, in the present paper we shall mainly use Peano arithmetic in all finite types as the underlying arithmetical framework and focus on the next two steps of proof mining (for the study of weak fragments in the context of proof mining see e.g. [49, 54]).

The second task in analysing a theorem consists of finding out which information the theorem could provide. We will concentrate in this paper on theorems following the patterns (1) and (2) (or rather, a generalization of those two forms to be explained in the next section) and implications between them. As we shall see, it is a task on its own to realize that a theorem has this form. We devote Section 2 to explaining this process.

Finally, we must carry out the extraction. Once we know that some information can be extracted we shall look for an appropriate proof interpretation which will guide the process of extracting the information from the proof. The main goal of the article is to present in reasonable details the method of monotone functional interpretation [48] (to be presented in Section 3) combined with negative translation. We shall furnish the different steps of the interpretation with various examples from functional analysis. Based on these examples we will argue that (the combination of negative translation with) monotone functional interpretation (but not the usual Gödel functional interpretation as considered by Bishop [12]) in many cases provides the ‘right’ notion of numerical implication in analysis.

Note that the proof interpretations used here are purely syntactical transformations. Hence, given a completely formalized proof the extraction of information can be in principle done automatically via a computer^{2}. The difficult part of proof mining would then consist in fully formalizing a mathematical proof originally given in ordinary mathematical terms. That can be in general very tiresome and intricate. Therefore, the case studies reported here have been carried out using the approach of partially formalizing only the relevant parts of a proof to the point where one can be sure that they can be completely formalized, and then carrying out the extraction ‘by hand’. This can also be viewed as an advantage since when considering a particular proof various steps of the interpretations can be simplified.

In Section 4, we show that statements of the form (1) and (2) are in fact very common in mathematics. We carry out the monotone functional interpretation of those statements in order to show how concepts like modulus of uniqueness, continuity, monotonicity, contractivity, asymptotic regularity etc. naturally arise. In Section 5.1 we exemplify how this extends to implications between such statements. In the final three sections we treat more complex classes of proofs involving ineffective principles such as the attainment of the infimum for continuous functions on compact intervals and the principle of convergence for bounded monotone sequences or reals. We also report on recent extensive case studies where proofs involving those ineffective principles have been analyzed.

2Such a tool has been developed (cf. e.g. [9]) for a different proof interpretation based on modified realizability and A-translation.

1.1 Formal systems

Our base formal system consists of extensional classical arithmetic in all finite types E-PA^{ω}. In places where classical logic must/can be avoid we use intuitionistic arithmetic E-HA^{ω} (for details see [86] where E-PA^{ω} is denoted by E-HAω c). The finite types are inductively defined as: 0 is a finite type and if ρ and τ are finite types then ρ → τ is a finite type. An object of type ρ → τ denotes a mapping from objects of type ρ to objects of type τ. We often abbreviate the type 0 → 0 as 1.

We denote by T^{ω} both E-PA^{ω} as well as various subsystems of E-PA^{ω} such as PRA^{ω} (cf. [3]) and E-G_{n}A^{ω} (cf. [49]). T_{i}^{ω} is the intuitionistic counterpart of T^{ω}. We work in system containing equality (=) between objects of type 0 as the only predicate symbol. Equality between higher types is defined extensionally. In the same way the (pointwise) partial order ≤_{ρ} between objects of type ρ is defined as: x ≤_{ρ→τ} y :≡ ∀z^{ρ} (x(z) ≤_{τ} y(z)). Note that all quantifier-free formulas in our systems are decidable and can even be written as atomic formulas. We shall usually add to the base system T^{ω} the axiom of quantifier-free choice^{3}

QF-AC^{1,0} : ∀f^{1}∃n^{0} A_{0}(f, n) → ∃Φ∀f A_{0}(f, Φf).

2 Representation

As already mentioned, our formal systems only contain equality between natural numbers as a primitive notion. Therefore, when talking about more complex mathematical objects such that rationals, reals, continuous functions, etc. we first need to fix their representation in the system. Equality between those objects will then be defined extensionally. As a simple example we take the rational numbers which can be represented via coding of pairs into the natural numbers. Assuming the representation of the rational numbers, real numbers are represented via (representations of) Cauchy sequences ψ : ℕ → ℚ with fixed rate of convergence say 2^{−n}, i.e. a real number x is represented by a function ψ_{x} : ℕ → ℚ satisfying ∀n∀m, m̃ ≥ n (|ψ_{x}(m) −_{ℚ} ψ_{x}(m̃)| ≤ 2^{−n}). In a roughly similar way elements of Polish spaces X are represented as type one objects x^{1} (i.e. elements in the Baire space) via the so-called standard representation (see e.g. [7]). For particular spaces, often more convenient (though essentially equivalent) representations can be used. For instance, take the Polish space (C[0, 1], ∥ · ∥_{∞}) of all the real valued continuous functions on the interval [0, 1] with the uniform norm as metric. A function f ∈ C[0, 1] is represented via a pair of functions (f_{r}, ω_{f}) where f_{r} is the restriction of f to the rational numbers and ω_{f} is the modulus of uniform continuity of f (on [0, 1]). Note that both f_{r} and ω_{f} can be further represented as type one functions. Operations on Polish spaces are then represented as type two objects and so on.

3Here and in the following, A_{0}, B_{0}, C_{0}, … always denote quantifier-free formulas.

Returning to the issue of equality, given two real numbers x and y represented via ψ_{x} and ψ_{y}, the statement x =_{ℝ} y, on the level of representation, is defined as the Π_{1}^{0}-formula ∀n(|ψ_{x}(n + 1) −_{ℚ} ψ_{y}(n + 1)| ≤_{ℚ} 2^{−n}). Similarly, x < y is expressed by the Σ_{1}^{0}-formula ∃n(ψ_{y}(n + 1) −_{ℚ} ψ_{x}(n + 1) ≥_{ℚ} 2^{−n}). In order to discover the information hidden in the statement of a theorem, it is important to explicitly present all the quantifiers hidden in such defined equality notions for Polish spaces. In order to avoid to have to go down all the way to the intensional level of representations, it is very useful to note that x =_{ℝ} y is equivalent to both ∀n (|x − y| ≤ 2^{−n}) and ∀n (|x − y| < 2^{−n}). Although the matrices in both statements are still Π_{1}^{0} and Σ_{1}^{0} respectively, we can treat them as if they were quantifier-free since we can always choose the suitable form which does not increase the general logical form of the theorem is question. In this way, we have presented the hidden quantifiers of the equality without having to go into the representations of the real numbers x and y.

The representation of Polish spaces X can be arranged in such a way that every x^{1} represents some element of X (see [7] and [46] for details).

For compact Polish spaces K one can achieve that the representatives ψ are always number theoretic functions which are bounded by some fixed term s (even by the constant-1 function, i.e. by elements in the Cantor space). Let X and Y be Polish spaces. Moreover, let {K_{x}}_{x∈X} be a family of compact Polish spaces (subspaces of Y) parametrized by elements x ∈ X (e.g. X = ℝ^{+}, Y = ℝ^{2} and K_{x} = [−x, x]^{2}). If the family {K_{x}}_{x∈X} is sufficiently constructively given (see [46], Def. 3.22) the elements z ∈ K_{x} can be represented as z ≤_{1} sx, for a fixed term s. Again one can achieve that every function in that bounded set represents some element of the space.

Details on all this can be found in [7, 46] and – for very weak systems – in [54].

According to the representation, mathematical statements of the form (1) and (2) have logical counterparts

∀x^{1}∀y^{1} ≤ s(∃nA_{0}(x, y, n) → ∃mB_{0}(x, y, m)),  (3)
∀x^{1}∀y^{1} ≤ s(∀nA_{0}(x, y, n) → ∀mB_{0}(x, y, m)),  (4)

respectively. Note, moreover, that (3) and (4) are special cases of ^{4}

∀x^{1}∀y^{1} ≤ s̃x∃z^{0} B_{0}(x, y, z),  (5)

which in mathematical terms corresponds to statements of the form

∀x ∈ X∀y ∈ K_{x}∃z ∈ ℕ B_{1}(x, y, z),  (6)

where X is some Polish space, K_{x} a compact Polish space parametrized by x, and B_{1} is a purely existential formula (due to the quantifiers still present in e.g. |x − y| < 2^{−n} as discussed above).^{5}

3 Monotone functional interpretation

The functional (‘Dialectica’) interpretation introduced by Gödel [28] translates an arbitrary formula A in the language of E-HA^{ω} into another formula A^{D} (in the same language) having the form ∃x∀yA_{D}(x, y), for some quantifier free formula A_{D}.^{6} The translation is sound in the sense that if the formula A has been proved in HA^{ω} then from that proof one can extract a closed term t such that A_{D}(t, y) is provable in HA^{ω}.^{7} The soundness theorem has been adapted to many other systems both stronger ones as well as fragments of HA^{ω}. Via negative translation (and elimination of extensionality) it also applies to E-PA^{ω} and related systems (cf. [3, 67, 86]).

4Using that ‘∀x^{1}, n^{0}’ can be contracted to ‘∀x^{1}’. Actually, we not even need such encodings as our techniques are directly applicable to tuples x⃗ of variables of degree ≤ 1 instead of x^{1}.

5Note that the fact that B_{1} is purely existential just adds some more existential quantifiers to ‘∃z^{0}’.

6Actually, x, y are both tuples of variables whose length depends on the logical form of A. For simplicity we suppress the (correct) tuple notation here.

7Here HA^{ω} is a version of E-HA^{ω} where the extensionality axioms in higher types are restricted to a quantifier-free rule of extensionality ([86]). Such a restriction – which is necessary for the soundness theorem to hold (see [33]) – does not cause any problems for the applications treated in this paper since all the principles and theorems we consider are – because of their type restrictions – such that the ‘elimination-of-extensionality’-procedure from [67] applies.

Note that the formula A_{D}(t, y) is quantifier free, but will usually contain terms of higher types, even if all the terms in the original formula A have the type 0.

Definition 3.1 (Functional Interpretation) The interpretation associates to each formula A ∈ L(HA^{ω}) (by induction on the logical structure of A) another formula (A)^{D} of the form ∃x∀yA_{D}(x, y), where A_{D} is quantifier free, in the following manner:

A^{D} :≡ A, for atomic formulas A,

and assuming A^{D} = ∃x∀yA_{D}(x, y) and B^{D} = ∃z∀wB_{D}(z, w) we define

(A ∧ B)^{D} :≡ ∃x, z∀y, w(A_{D}(x, y) ∧ B_{D}(z, w)),

(A ∨ B)^{D} :≡ ∃p^{0}∃x, z∀y, w((p = 0 → A_{D}(x, y)) ∧ (p ≠ 0 → B_{D}(z, w))),

(A → B)^{D} :≡ ∃Ψ, Φ∀x, w(A_{D}(x, Φxw) → B_{D}(Ψx, w)),
(∃zA(z))^{D} :≡ ∃z, x∀yA_{D}(x, y, z),
(∀zA(z))^{D} :≡ ∃Ψ∀z, yA_{D}(Ψz, y, z),

where the types of Ψ and Φ can be inferred. We define ¬A as A → 0 = 1.

The most intricate interpretation is that of the implication. Let us analyse the functional interpretation of implication when both formulas A and B have the special form ∃xC_{0}(x) or ∀xC_{0}(x) (with C_{0} quantifier-free). Here we get (using implicitly that quantifier-free formulas A_{0}(a) can be written as atomic ones t_{A_{0}}(a) =_{0} 0 for suitable closed t_{A_{0}})

(∃xA_{0}(x) → ∃yB_{0}(y))^{D} ≡ ∃Φ∀x(A_{0}(x) → B_{0}(Φx))

and

(∀xA_{0}(x) → ∀yB_{0}(y))^{D} ≡ ∃Φ∀y(A_{0}(Φy) → B_{0}(y)).

This also holds if first negative translation has been applied. Note that e.g. the more simple modified realizability interpretation [87] only delivers a result in the first case (and if negative translation had been applied first, not even then). In Section 4 we shall see various examples of statements, commonly used in numerical analysis, having the forms ∃xA_{0}(x) → ∃yB_{0}(y) and ∀xA_{0}(x) → ∀yB_{0}(y). A detailed analysis of the treatment given to implication by functional interpretation can be found in [3].

We call extraction procedure the process of producing out of a proof of a sentence A a (tuple of) closed term(s) t of the underlying system and a proof of A_{D}(t, y). The soundness proof of functional interpretation actually provides such an extraction procedure. If only a bound on the term t is of interest a much simpler extraction procedure can be used. This variant of the extraction procedure which looks for a hereditarily monotone bound on the realizer of ∃x∀yA_{D}(x, y) we call (cf. [48]) monotone functional interpretation, or m.f.i. for short. In [48] it is shown that the soundness theorem for the monotone functional interpretation can be directly proved on the level of the monotone version.

In order to make the notion of ‘bound’ well behaving in higher types we use Bezem’s [10] strong majorizability relation ≥_{ρ}^{∗}, which is a variant of Howard’s [33] original hereditarily majorability relation. For numbers n ≥_{0}^{∗} m just means that n is greater or equal than m. For functions f and g, f ≥_{1}^{∗} g holds when f is monotone and is pointwise bigger than g. For higher types the relation is designed to be hereditarily monotone, i.e.

Φ^{∗} ≥_{ρ→τ}^{∗} Φ :≡ ∀x^{∗}∀x ≤_{ρ}^{∗} x^{∗}(Φ^{∗}x^{∗} ≥_{τ}^{∗} Φ^{∗}x ∧ Φ^{∗}x^{∗} ≥_{τ}^{∗} Φx.)

Three important properties of the relation ≥_{ρ}^{∗} are:

i) x ≥_{ρ}^{∗} y implies x ≥_{ρ}^{∗} x,

ii) x ≥_{ρ}^{∗} y ∧ y ≥_{ρ} z → x ≥_{ρ} z, (≥_{ρ} as defined in Section 1.1)

iii) for type one objects x^{1}, i.e. number theoretic functions, the function

x^{+} := λn. max_{m≤n} x(m)

always majorizes x.

Note that ≥_{ρ}^{∗} is not reflexive unless ρ = 0.

Using the relation ≥^{∗}, the monotone functional interpretation of a formula A (having functional interpretation ∃x^{ρ}∀y^{τ}A_{D}(x, y)) is defined as

∃x^{∗}∃x ≤_{ρ}^{∗} x^{∗}∀yA_{D}(x, y).

Theorem 3.2 ([45]) Let Δ be a set of closed axioms of the form

∀u^{1}∃v^{1} ≤ tu∀w^{0} A_{0}(u, v, w), where t is closed.

Suppose that ^{8}

T^{ω} + QF-AC^{1,0} + Δ ⊢ ∀x^{1}∀y^{1} ≤ sx∃z^{0}B_{0}(x, y, z).

From this proof one can extract a closed term Φ of T^{ω} such that,

T_{i}^{ω} + Δ_{ε} ⊢ ∀x^{1}∀y^{1} ≤ sx∃z ≤ Φx B_{0}(x, y, z),

where Δ_{ε} consists of the so-called ε-weakenings of the sentences in Δ, i.e.

∀u^{1}, w^{0}∃v^{1} ≤ tu∀i ≤ wA_{0}(u, v, i).

As shown in [45], the set of sentences Δ also includes the non-computational principle weak König lemma (WKL). Since HA^{ω} ⊢ WKL_{ε}, this provides a WKL-elimination.

The result above can also be stated in more mathematical terms. Let INF denote the principle

∀f ∈ C[0, 1]∃x ∈ [0, 1](f(x) =^{ℝ} inf_{y∈[0,1]} f(y)),

which can – using the representation of C[0, 1] – be written in form Δ (see [46]). Note that INF_{ε} is equivalent to

∀f ∈ C[0, 1]∀n∃x ∈ [0, 1](f(x) ≤ inf_{y∈[0,1]} f(y) + 2^{−n}),

which, given our representation of f ∈ C[0, 1], can be easily proved in HA^{ω}. One example of a corollary of Theorem 3.2 would be the following.

Theorem 3.3 ([46]) Let (X, d_{X}) be a T^{ω}-definable Polish space and {K_{x}}_{x∈X} a T^{ω}-definable family of compact sets in a Polish space Y. If

T^{ω} + QF-AC^{1,0} + INF ⊢ ∀x ∈ X∀y ∈ K_{x}∃z ∈ ℕB_{1}(x, y, z)

then, from this proof one can extract a closed term Φ of T^{ω} such that,

T_{i}^{ω} ⊢ ∀x ∈ X∀y ∈ K_{x}∃z ≤ Φx B_{1}(x, y, z), where B_{1}(x, y, z) is a Σ_{1}^{0}-formula (not containing further free variables) which is (provably in T^{ω}) extensional in x, y w.r.t. the relations =_{X} and =_{K_{x}}.

8B_{0}(x, y, z) contains no other free variables than x, y, z and that s is a closed term.

Remark 3.4 The constructivisation of the given proof provided by the metatheorems due to the reduction of the use of Δ to that of Δ_{ε} is quite independent from the construction of the bound which first uses even a stronger Skolemized version of Δ which then by subsequent manipulations can be reduced to Δ_{ε}. These subsequent steps can be omitted in applied proof mining. So the final proof of the result will normally again be ineffective although the meta-theorems guarantees that it can in principle be made constructive.

Note that, besides the simplicity of the extraction procedure, using monotone functional interpretation one obtains bounds which are independent of all parameters ranging over compact spaces.

The proofs of both meta-theorems above rely on the combination of negative translation and monotone functional interpretation. These two metatheorems are just special cases of a whole class of more general theorems proved by the first author in the papers cited and - for weak fragments - in [49]. In particular, many more analytical principles than INF can directly be seen to have the form Δ which avoids to have to analyse their proofs (say via WKL) in the proof mining process. Other WKL-related principles which do not have that form usually easily follow from a nonstandard principle of uniform boundedness (studied in [53, 58]) which is allowed to be used in the meta-theorems and can be eliminated from the proof of the conclusion. In this way large parts of given proofs can simply be skipped in the process of proof mining.

Whereas – as Theorem 3.3 shows – principles based on Heine-Borel compactness (WKL) do not contribute to the growth of extractable bounds, principles based on sequential compactness do contribute. Monotone functional interpretation (combined with a specially designed method of eliminating monotone Skolem functions) allows to calibrate the exact contribution of fixed instances of sequential compactness relative to weak fragments T^{ω} (see [50]). We shall discuss this in more detail in Sections 6 and 7.

Another important observation is that the bound Φ above will depend on the representation of x and will therefore not be an extensional function X → ℕ. In practice, however, Φ will usually be extensional in some natural enrichments of the input. The dependence on the representation is unavoidable in general. Consider the space X = ℝ. The only effective extensional (and therefore continuous) functions Φ : ℝ → ℕ would be constant functions.

Notation 3.5 For the rest of the paper all the Polish spaces are understood to be T^{ω}-definable. Examples of T^{ω}-definable Polish spaces are (ℝ^{n}, d_{E}), (ℝ^{n}, dmax), (C[0, 1], d_{∞}) and (L_{p}, d_{p}) for 1 ≤ p < ∞.

3.1 Monotone functional interpretation of theorems having the form (5)

In Bishop [12] some arguments are given in favour of taking the functional interpretation of implication as numerical implication, i.e. given a theorem C of the form

∃x∀yA_{0}(x, y) → ∃z∀wB_{0}(z, w),

A_{0} and B_{0} quantifier free, Bishop suggests that the numerical content of the theorem C is given by the existential quantifier in

C^{D} ≡ ∃Z, Y ∀x, w(A_{0}(x, Y xw) → B_{0}(Zx, w)).

In the following we argue, by considering implications between statements of the form (5) that if one is interested in uniform bounds (which is usually the case in analysis, see below) the monotone functional interpretation provides exactly the right kind of numerical information. As mentioned above, statements in analysis which have the logical form (5) appear in the special forms (3) and (4). Let us first analyze, from a purely logical point of view, how m.f.i. treats such statements. It is important to note that for statements of this form there is no difference whether m.f.i. is applied directly or to their negative translation.^{9} Therefore, in the following we only consider the monotone functional interpretation. The m.f.i. of (4) gives ^{10}

∃Φ^{∗}∃Φ ≤^{∗} Φ^{∗}∀x∀y ≤ sx∀m (A_{0}(x, y, Φxym) → B_{0}(x, y, m)),

which is equivalent (by elementary constructive reasoning)^{11} to

∃Ψ^{∗} ≤^{∗} Ψ^{∗}∀x∀y ≤ sx∀m∃n ≤ Ψ^{∗}x^{+}(s^{∗}x^{+})m (A_{0}(x, y, n) → B_{0}(x, y, m)).

9In logical terms this is due to the fact that m.f.i. satisfies the so-called Markov principle. As we are mainly interested in proofs based on full classical logic it is indeed the m.f.i. of the negative translation A′ of a statement A which matters.

10Note that the universal quantifier ‘hidden’ in y ≤_{1} sx is not essential, for using extensionality one can prove that ∀y ≤ sxA(y) is equivalent to ∀yA(min_{1}(y, sx)), where min_{1}(x, y) := λn. min(x(n), y(n)).

11In the direction ‘→’ we can take Ψ^{∗} := Φ^{∗}. In the other direction, suppose that Ψ^{∗} satisfies the second formula. Then

The formula above is in turn equivalent to

∃Ψ ≤^{∗} Ψ∀x∀y ≤ sx∀m (∀n ≤ Ψxm A_{0}(x, y, n) → B_{0}(x, y, m)).

In the same way, the monotone functional interpretation of (3) is equivalent to

∃Ψ ≤^{∗} Ψ∀x∀y ≤ sx∀n (A_{0}(x, y, n) → ∃m ≤ Ψxn B_{0}(x, y, m)).

In Section 4, we shall consider various mathematical concepts which have the logical form (1) and (2) (the mathematical counterparts of (3) and (4)) and therefore the form (6) where B_{1} is monotone in ‘z’ so that any (uniform) bound in fact provides a (uniform) realizer. For each of those statements we indicate the mathematical importance of the m.f.i., by showing that the modulus Ψ corresponds to an important analytical concept which has been studied extensively in the literature.

The fact that Ψ majorizes itself implies an important monotonicity behaviour. Assume we have shown that a Ψ (majorizing itself) exists such that

∀x^{1}∀y ≤ sx∃n ≤ ΨxB_{0}(x, y, n).

Let t^{1} be some closed term. By restricting the variable x to be bounded by t we immediately obtain the existence of a functional Ψ̃ := Ψ(t^{+}) (independent of x and y) such that

∀x ≤ t∀y ≤ sx∃n ≤ Ψ̃B_{0}(x, y, n).

In mathematical terms, assume that a modulus Ψ depends on an element x of some Polish space X. By restricting x to some compact subspace K ⊆ X we automatically obtain a modulus Φ independent of x (but which will depend only on some information about the compact space K). An instance of this general fact can be seen in Proposition 6.2, where we restrict f ∈ C[0, 1] to functions with common modulus of uniform continuity and bounded uniform norm, therefore obtaining independence from the function f.

We shall also see in the next section that inter-relations between such moduli created by m.f.i. play an important role in numerical functional analysis. We investigate this in more detail in Section 5, where we explain how monotone functional interpretation naturally transforms those moduli into one another via the treatment of implications.

Φ^{∗}xym := Ψ^{∗}x^{+}(s^{∗}x^{+})m and

Φxym := min i ≤ Φ^{∗}xym [A_{0}(x, y, i) → B_{0}(x, y, m)] satisfy the first formula.

4 Applying monotone functional interpretation to mathematics

In the following we consider what m.f.i. does when applied to standard concepts used in mathematics of the logical form treated in the previous section. As we shall see, in each case the interpretation suggests the existence of a modulus which corresponds to extensively studied analytical concepts. That indicates that, via a purely logical analysis, m.f.i. will in general ask/create the ‘right’ effective information about a theorem. As discussed in the previous section, there is no difference between the m.f.i. of a statement (6) and the m.f.i of its negative translation so that we only have to consider the former.

We should keep in mind that – as mentioned already – the functionals created by m.f.i. operate on the representation of mathematical objects in the formal system, rather than on the actual objects. For instance, a functional from a Polish space X to the rational numbers will have type ℕ^{ℕ} → ℕ and will not be extensional in general.

4.1 Uniqueness

Let (X, d_{X}) and (K, d_{K}) be Polish spaces, K compact. The fact that a T^{ω}- definable (and hence continuous) function f : X × K → ℝ for each given x ∈ X has at most one root in K can be expressed as

UNI(f) :≡ ∀x ∈ X; y_{1}, y_{2} ∈ K(⋀_{i=1}^{2} f(x, y_{i}) =^{ℝ} 0 → d_{K}(y_{1}, y_{2}) =^{ℝ} 0),

which has the form (2). The monotone functional interpretation of a uniqueness statement of the form UNI creates a modulus Φ : ℕ^{ℕ} × ℚ_{+}^{∗} → ℚ_{+}^{∗} such that

∀x ∈ X; y_{1}, y_{2} ∈ K; ε ∈ ℚ_{+}^{∗}(⋀_{i=1}^{2} |f(x, y_{i})| < Φ(x, ε) → d_{K}(y_{1}, y_{2}) < ε),

named modulus of uniqueness in [46]. The notion of modulus of uniqueness shows up e.g. in approximation theory where it has been extensively studied under the name of strong unicity or rate of strong uniqueness. For the case of Chebysheff approximation this was first investigated in [73]. For L_{1}-approximation strong unicity was studied e.g. by Björnestål [13, 14] and Kroó [63, 65]. See [5] for a survey on the relevance of this concept.

We mention here two applications of moduli of uniqueness. First, assume that K is a compact subset of the Polish space X and that each element of x ∈ X has a unique best approximation in K w.r.t. the metric d_{X}. A modulus of uniqueness Φ in this case provides necessary a priori information for computing the best approximation of x, uniformly in x, in the following way. Define f(x, y) := d_{X}(x, y) − dist(x, K), where dist(x, K) := inf_{y∈K} d_{X}(x, y). If X and K are effective spaces, then one can compute approximate solutions, i.e. elements y ∈ K such that |f(x, y)| < ε. Let (y_{n})_{n∈ℕ} be a sequence of elements of K such that |f(x, y_{n})| < Φ(x, 2^{−n}). Then – applying Φ to y_{n} and the best approximation y_{b} one infers that the sequence (y_{n})_{n∈ℕ} converges to the best approximation y_{b} ∈ K of x with rate of convergence 2^{−n}, i.e. d_{X}(y_{b}, y_{n}) < 2^{−n}. Note that it is crucial for the procedure above to be useful that Φ does not depend on y_{1} nor y_{2}, since it gets applied to context where one of the polynomials is the unknown y_{b}. Further details can be found in [46].

Under the assumptions above, define P : X → K to be the functional which maps x to its unique best approximation in K. As shown in [46], a modulus of uniqueness Φ automatically gives a modulus of pointwise continuity for the projection P, also called rate of smoothness/continuity,

∀x, y ∈ X(d_{X}(x, y) < \frac{1}{2}Φ(x, ε) → d_{X}(P(x), P(y)) < ε).

Again, the relationship between strong uniqueness and the smoothness of the projection operator has been studied extensively in the literature (cf. [1, 2, 6, 14]).

4.2 Convexity

Let (X, ∥ · ∥) denote a normed linear space whose unit ball B :≡ {x ∈ X : ∥x∥ ≤ 1} is compact (which – classically – amounts to X being finite dimensional). From the statement that X is strictly convex

CVX :≡ ∀x, y ∈ B(∥\frac{1}{2}(x + y)∥ =^{ℝ} 1 → ∥x − y∥ =^{ℝ} 0),

which is again of the form (2), monotone functional interpretation creates a modulus η : ℚ_{+}^{∗} → ℚ_{+}^{∗} satisfying

∀x, y ∈ B; ε ∈ ℚ_{+}^{∗}(∥\frac{1}{2}(x + y)∥ > 1 − η(ε) → ∥x − y∥ < ε).

If a normed space has such a modulus η it is called uniformly convex. Moreover, η is called modulus of uniform convexity. The crucial feature of uniform convexity, compared to strict convexity, is that η(ε) does not depend on x, y. It is well known that finite dimensional strictly convex normed spaces are uniformly convex. Monotone functional interpretation provides an effective version of this: From a proof of strict convexity of a compact unit ball one can extract a modulus of uniform convexity, provided the proof and the space can be represented in an appropriate formal system.

The notion of uniform convexity was introduced in 1936 by Clarkson [20] (see also [43]) and plays a crucial role in many parts of functional analysis. This is true, in particular, for the area of metric fixed point theory (see e.g. [17, 30, 31]). Here moduli of uniform convexity have been used to determine rates of convergence for Krasnoselski-Mann iterations of nonexpansive mappings which connects this concept with the concepts of rates of monotone convergence and rate of asymptotic regularity to be discussed in Sections 4.6 and 5.1 (cf. [18, 40, 56, 59]).

Moduli of uniform convexity also feature prominently in the area of best approximation theory, having a close connection with rates of strong unicity and rates of smoothness/continuity, concepts discussed in Sections 4.1 and 4.4. Among the many publications on the connection between moduli of uniform convexity and rates of strong unicity see e.g. [14, 35, 66, 77].

4.3 Contractivity

Let (K, d) be a compact Polish space. A function f : K → K is defined to be contractive if^{12}

CTR(f) :≡ ∀x, y ∈ K(x ≠ y → d(f(x), f(y)) < d(x, y)),

which has the form (1). The monotone functional interpretation of the statement that a T^{ω}-definable f is contractive creates a modulus η : ℚ_{+}^{∗} → ℚ_{+}^{∗} satisfying

12We may in fact consider the more general case of functions f : X × K → K, where X is a Polish space, in which case the modulus η will also depend on (a representation of)

x ∈ X. Similarly in Section 4.4 below.

∀x, y ∈ K; ε ∈ ℚ_{+}^{∗}(d(x, y) > ε → d(f(x), f(y)) + η(ε) < d(x, y)).

The concept of contractivity can be written also in the trivially equivalent form

∀x, y ∈ K(x ≠ y → ∃n ∈ ℕ(d(f(x), f(y)) < (1 − 2^{−n}) · d(x, y))),

in which case the interpretation yields a modulus η̃: ℚ_{+}^{∗} → ℕ satisfying

∀x, y ∈ K; ε ∈ ℚ_{+}^{∗}(d(x, y) > ε → d(f(x), f(y)) < (1 − 2^{−η̃(ε)}) · d(x, y)).

Such a modulus α(ε) := 1−2^{−η̃(ε)} has in fact been considered in the literature by Rakotch [78] and – in the context of Bishop style constructive analysis – in [16]. Using the boundedness of K, we can easily produce an η out of a given α and vice-versa.

As we will show in Section 5.1, it is exactly such a modulus which is needed to obtain a rate of convergence in Edelstein’s fixed point theorem [23, 78]. As in the case of moduli of uniqueness it is crucial here that η does not depend on x, y.

Numerous variants of the notion of ‘contractive mapping’ have been considered in the literature. The main purpose of those variants is to obtain generalizations of Edelstein’s classical fixed point theorem to more general classes of functions. Under monotone functional interpretation, those notions again give rise to appropriate moduli, and we expect that in many of these cases explicit rates of convergence can be provided in terms of the corresponding moduli of contractivity. For a survey of 25 notions of contractivity and generalizations of Edelstein’s result see [81]. This line of work is further continued in [21, 72, 82], to list only a few references.

4.4 Uniform continuity

Let (X, d_{X}) and (K, d_{K}) be Polish spaces, K compact. From the statement that a T^{ω}-definable f : K → X is a function

CTN(f) :≡ ∀x, y ∈ K(x =^{K} y → f(x) =^{X} f(y)),

which has the form (2), monotone functional interpretation creates a modulus ω : ℚ_{+}^{∗} → ℚ_{+}^{∗} satisfying

∀x, y ∈ K; ε ∈ ℚ_{+}^{∗}(d_{K}(x, y) < ω(ε) → d_{X}(f(x), f(y)) < ε).

Such ω plays a fundamental role in constructive mathematics (see [11]) and in computable analysis (see [42], [76] and [88]) where it is called modulus of uniform continuity. Numerous results indicate that ω provides the right computational information on continuous functions. For example, a function f : [0, 1] → ℝ which maps computable sequences in [0, 1] into computable sequences in ℝ has an effective uniform approximation by polynomials iff f has a computable modulus of uniform continuity ω (see [76]). On the other hand, numerical analysts define the function

Ω(ε) := sup_{d_{K}(x,y)≤ε} d_{X}(f(x), f(y))

to be the modulus of continuity of f. The function Ω clearly satisfies

∀x, y ∈ K; ε ∈ ℚ_{+}^{∗}(d_{K}(x, y) ≤ ε → d_{X}(f(x), f(y)) ≤ Ω(ε))

and is, in contrast to ω, unique. The continuity of f is now expressed as

ε ↘ 0 → Ω(ε) ↘ 0.

Apparently, the notions introduced by monotone functional interpretation and numerical analysis differ. However, one can observe that in analysis (cf. [65]) the modulus Ω is often used just for building a

Ω^{−1}(ε) := inf{δ ∈ [0, 1] : Ω(δ) = ε},

which is a roundabout and ineffective way of creating a particular modulus ω. That once again supports the thesis that monotone functional interpretation produces, by purely logical analysis, the right constructive modulus.

4.5 Monotonicity

Let f : [0, 1] → ℝ be a T^{ω}-definable strictly increasing (decreasing) function, i.e.,

MON(f) :≡ ∀x, y ∈ [0, 1](x − y > 0 → f(x) − f(y) > 0),

which has the form (1). From this statement monotone functional interpretation creates a modulus δ : ℚ_{+}^{∗} → ℚ_{+}^{∗} such that

∀x, y ∈ [0, 1]; ε ∈ ℚ_{+}^{∗}(x − y > ε → f(x) − f(y) > δ(ε)),

called modulus of monotonicity. Note that the modulus of monotonicity δ provides a modulus of uniform continuity for the inverse function f^{−1}.

4.6 Monotone convergence

Let X and K be Polish spaces, K compact. Moreover, let f : X×K×ℕ → ℝ_{+} be a function such that for any x ∈ X and y ∈ K the sequence (f(x, y, n))_{n∈ℕ} is non-increasing. Suppose that (f(x, y, n))_{n∈ℕ} converges to zero

CVG(f) :≡ ∀x ∈ X; y ∈ K; ε ∈ ℚ_{+}^{∗}∃n ∈ ℕ∀m ≥ n (f(x, y, m) < ε).

Since the sequence is non-increasing we can omit the innermost universal quantifier and get

CVG(f) ↔ ∀x ∈ X; y ∈ K; ε ∈ ℚ_{+}^{∗}∃n ∈ ℕ (f(x, y, n) < ε),

which has the form (6). Monotone functional interpretation creates a modulus δ : ℕ^{ℕ} × ℚ_{+}^{∗} → ℕ satisfying (inserting the omitted universal quantifier back)

∀x ∈ X; y ∈ K; ϵ ∈ ℚ_{+}^{∗}∀m ≥ δ(x, ε) (f(x, y, m) < ε),

i.e. monotone functional interpretation transforms pointwise convergence into uniform convergence. The monotone functional interpretation in this case can be viewed as a form of Dini’s theorem: Any non-increasing sequence (f_{n})_{n∈ℕ} of functions in C[0, 1] converging pointwise to zero converges uniformly to zero.

For a given function f : K → K and a starting point x ∈ K, let x_{n} denote the n-th iteration of f on x, i.e. x_{n} := f^{n}(x). The convergence of the sequence (d(x_{n}, x_{n+1}))_{n∈ℕ} to zero is normally called the asymptotic regularity of the function f

ASY(f) :≡ ∀x ∈ K∀ε ∈ ℚ_{+}^{∗}∃n∀m ≥ n(d(x_{m}, f(x_{m})) < ε).

In many cases the sequence (d(x_{n}, x_{n+1}))_{n∈ℕ} is non-increasing so that, by the discussion above, the m.f.i. of ASY(f) (also when applied to the negative translation of ASY(f)) creates a functional κ : ℚ_{+}^{∗} → ℕ satisfying

∀x ∈ K∀ε ∈ ℚ_{+}^{∗}∀m ≥ κ(ε)(d(x_{m}, f(x_{m})) < ε).

The monotonicity in these convergence statements is only used to be able to write the convergence in the logical form (6). This is crucial for applications in a context based on classical logic in which one applies m.f.i. to the negative translation of formulas. Without monotonicity the negative translation of

∃n ∈ ℕ∀m ≥ n (f(x, y, m) < ε)

would yield

¬¬∃n ∈ ℕ∀m ≥ n (f(x, y, m) < ε)

from which m.f.i. no longer extracts a modulus of convergence (we will come back to this in Section 7 below). In an intuitionistic context, however, one can use m.f.i. to extract moduli of convergence even without any monotonicity assumptions. This remains true in the presence of various highly ineffective principles (see [51]).

5 The monotone functional interpretation of implications

As we saw in the previous section, not only the concepts created via m.f.i. but also the interconnections between these concepts have been extensively exploited in mathematics. This can again be viewed as an instance of the general logical fact that the monotone functional interpretation of an implication A → B between two statements of the form (5) provides a procedure to transform a modulus for the interpretation of A into one for the interpretation of B. Furthermore, if the proof of A → B is formalized in a suitable formal setting in which monotone functional interpretation applies, we are actually able to extract such a procedure from the given proof. In the following, we shall illustrate this for the so-called Edelstein fixed point theorem, where the issues involved can be explained quite easily. In Sections 6 and 7, we survey results we obtained in more substantial examples which solved open problems in the literature.

5.1 Example 1: Edelstein fixed point theorem

In this section we illustrate with a simple example how the concepts described above interrelate via monotone functional interpretation. In this simple example the functionals required by m.f.i. can be easily provided. In more involved proofs, however, such as the ones presented in Sections 6.1 and 7.1, one also uses the interpretation to help extract from the given proof the desired functionals.

One form of the well-known Edelstein fixed point theorem can be stated as follows.

Proposition 5.1 ([23]) Let (K, d) be a compact metric space and f : K → K be contractive (in the sense of 4.3). From any starting point x ∈ K, the iteration (f^{n}(x))_{n∈ℕ} (also denoted by (x_{n})_{n∈ℕ}) converges to the unique fixed point of f.

We split Edelstein’s proof into three lemmas. First one shows that contractivity implies asymptotic regularity of the sequence (x_{n})_{n∈ℕ}. Note that the sequence (d(x_{n}, x_{n+1}))_{n∈ℕ} is non-increasing. The proof of the first lemma CTN(f) → ASY(f) provides a functional translating moduli of contractivity into moduli of asymptotic regularity for the function f.

Lemma 5.2 Let D_{K} denote an upper bound for the diameter of the compact space K. Moreover, define χ_{1}(η, ε) := \frac{D_{K}−ε}{η(ε)}+1. For any function f : K → K having moduli of contractivity η the function κ(ε) := χ_{1}(η, ε) is a modulus of asymptotic regularity for f, i.e.

∀x ∈ K∀ε ∈ ℚ_{+}^{∗}∀n ≥ κ(ε)(d(x_{n}, f(x_{n})) < ε).

Proof. Let x ∈ K be arbitrary. By the definition of diameter d(x, f(x)) = d(x_{0}, x_{1}) ≤ D_{K}. If d(x_{0}, x_{1}) ≤ ε then we are done, since d(x_{1}, x_{2}) < ε. Otherwise, since f is contractive we have that d(x_{1}, x_{2}) ≤ d(x_{0}, x_{1}) − η(ε) ≤ D_{K} − η(ε). In general, either d(x_{m}, x_{m+1}) ≤ ε for some m ≤ n or d(x_{n}, x_{n+1}) ≤ D_{K} − n · η(ε). Let n ≥ \frac{D_{K}−ε}{η(ε)}. In the first case, since the sequence (d(x_{n}, x_{n+1}))_{n∈ℕ} is non-increasing we have that d(x_{n}, x_{n+1}) ≤ ε. In the second case we have d(x_{n}, x_{n+1}) ≤ D_{K} − n · η(ε) ≤ ε. So for n ≥ κ(ε) we have d(x_{n}, x_{n+1}) < d(x_{n−1}, x_{n}) ≤ ε.

Remark 5.3 Note that instead of η we could have used Rakotch’s notion of modulus of contractivity α. The functional χ_{1}(α, ε) could then be defined as \frac{log ε−log D_{K}}{log α(ε)} + 1 in the lemma above.

In the second part we prove that contractivity implies uniqueness of the fixed point,

∀x, y ∈ K(d(x, f(x)) = d(y, f(y)) = 0 → d(x, y) = 0).

Again, the m.f.i. of the statement CTN(f) → UNI(λx.d(x, f(x))) asks for a functional translating moduli of contractivity into moduli of uniqueness. The following lemma can be easily verified.

Lemma 5.4 Define χ_{2}(η, ε) := \frac{η(ε)}{2}. For any function f : K → K having moduli of contractivity η the function Φ(ε) := χ_{2}(η, ε) is a modulus of uniqueness for the fixed point of f, i.e.

∀x, y ∈ K∀ε ∈ ℚ_{+}^{∗}(d(x, f(x)) < Φ(ε) ∧ d(y, f(y)) < Φ(ε) → d(x, y) ≤ ε).

Finally, the last lemma

ASY(f) ∧ UNI(λx.d(x, f(x))) → ∀x ∈ K((x_{n})_{n∈ℕ} converges)

shows that asymptotic regularity plus uniqueness implies convergence. The statement of convergence in the conclusion has more complex logical form than (5). Similarly as explained in Section 4.1, however, one can still give a procedure for producing uniformly out of moduli of asymptotic regularity and uniqueness a modulus of convergence.

Lemma 5.5 Define χ_{3}(κ, Φ, ε) := κ(Φ(ε)). For any function f : K → K having fixed point c, modulus of asymptotic regularity κ and modulus of uniqueness of fixed point Φ, the function δ(ε) := χ_{3}(κ, Φ, ε) is a modulus of convergence for the fixed point of f, i.e. ∀x ∈ K∀ε ∈ ℚ_{+}^{∗}∀n ≥ δ(ε)(d(x_{n}, c) ≤ ε).

When we combine all the three lemmas we obtain the effective version of Edelstein fixed point theorem.

Proposition 5.6 Let D_{K} denote the diameter of the compact space K. For any function f : K → K having modulus of contractivity η, and any starting point x ∈ K, the sequence (x_{n})_{n∈ℕ} converges to the fixed point c of f with rate of convergence ^{13}

δ(ε) := χ_{3}(λε.χ_{1}(η, ε), λε.χ_{2}(η, ε), ε) = \frac{D_{K} − η(ε)}{η(\frac{η(ε)}{2})} + 1,

i.e.

∀x ∈ K∀ε ∈ ℚ_{+}^{∗}∀n ≥ δ(ε) (d(x_{n}, c) ≤ ε).

Another quantitative version is given in Rakotch [78]. For a discussion of Edelstein’s fixed point theorem in the context of Bishop’s constructive mathematics see [16]. A recent domain theoretic approach to Edelstein’s theorem can be found in [71].

13Note that δ depends only on ε, D_{K} and η, but not x or f.

6 Proofs based on Heine-Borel compactness

We have presented how the computational content of sentences of the form (3), (4) and (5) (in mathematical terms (1), (2) and (6) respectively) should be understood. Moreover, we showed how to deal with implications between statements of this from. This provides a procedure for analysing in a very simple way proofs which only involve formulas of this kind. For the rest of the paper we shall focus on more complex principles which do not fall into the general form (5), and how to analyze proofs involving such principles.

In this section we focus on principles related to Heine-Borel compactness such as

• The attainment of the infimum: Every continuous function f : [a, b] → ℝ attains its infimum.

• Brouwer’s fixed point theorem for continuous functions f : [0, 1]^{n} → [0, 1]^{n}.

• Cauchy-Peano existence theorem.

Each of these principles are, even when the function f is given together with the modulus of uniform continuity, equivalent to WKL (see [83]) and rely on the existence of non-computable real numbers. We analyze in details below the attainment of the infimum (for the interval [0, 1]) which can be written more formally as

INF :≡ ∀f ∈ C[0, 1]∃x ∈ [0, 1](f(x) =^{ℝ} inf_{y∈[0,1]} f(y)),

which, as shown in [46], has the logical form Δ. If the principle INF has been used in the proof of a theorem of the form (5) at some point in the proof a modus ponens over an implication

∀u^{1}∃v^{1} ≤ tu∀w^{0}A_{0}(u, v, w) → ∀x∀y ≤ sx∃zB_{0}(x, y, z)  (7)

will take place. Negative translation of (7) gives

∀u^{1}¬¬∃v^{1} ≤ tu∀w^{0}A_{0}(u, v, w) → ∀x∀y ≤ sx¬¬∃zB_{0}(x, y, z)  (8)

and hence a-fortiori

∀u^{1}∃v^{1} ≤ tu∀w^{0}A_{0}(u, v, w) → ∀x∀y ≤ sx¬¬∃zB_{0}(x, y, z).  (9)

The m.f.i. of the premise of (9) asks for a Φ^{∗} satisfying

∃Φ ≤ t(Φ ≤^{∗} Φ^{∗} ∧ ∀u^{1}∀w^{0}A_{0}(u, Φu, w)),

which can be clearly taken to be Φ^{∗} := t^{∗}, for some t^{∗} majorizing t. The (partial) monotone functional interpretation of the implication (9) is realized by a functional χ^{∗} satisfying

∃χ ≤^{∗} χ^{∗}∀Φ ≤ t(∀u^{1}∀w^{0}A_{0}(u, Φu, w) → ∀x∀y ≤ sxB_{0}(x, y, χ(Φ, x, y))).

Note that χ^{∗}(t^{∗}, x^{+}, s^{∗}(x^{+})) majorizes χ(Φ, x, y). Therefore, given the truth of the premise of (7), and hence its Skolemized version

∃Φ ≤ t∀u, wA_{0}(u, Φu, w),

the functional Ψ(x) := χ^{∗}(t^{∗}, x^{+}, s^{∗}(x^{+})) satisfies the m.f.i. of the conclusion, i.e.

∀x∀y ≤ sx∃w ≤ Ψ(x) B_{0}(x, y, w).

The treatment of proof based on lemmas Δ presented here is due to [45], where more general forms of lemmas Δ are considered as well.

In the following section we report on a case study where a classical proof involving the principle INF has been analyzed and new results have been obtained.

6.1 Example 2: Jackson’s theorem

In [61] the authors have carried out the analysis of Cheney’s proof [19] of the following well-known theorem in L_{1}-approximation theory (‘approximation in the mean’).

Theorem 6.1 (Jackson’s theorem [37]) Let P_{n} denote the space of algebraic polynomials of degree bounded by n. For any number n and continuous function f ∈ C[0, 1] there exists a unique element of P_{n} which best approximates f w.r.t the L_{1}-norm.

This investigation yielded the first effective in all parameters modulus of uniqueness for L_{1}-approximation by polynomials of bounded degree. As it is clear from our Example 1, the difficulty in the analysis usually comes from the use of logically more complex principles.

Let us first outline how to bring Jackson’s theorem into the form (2). Recall that the L_{1}-norm of a function f ∈ C[0, 1] is defined as

∥f∥_{1} := ∫_{0}^{1} |f(x)| dx,

and p ∈ P_{n} is a best L_{1}-approximation of f from P_{n} if

∥f − p∥_{1} = dist_{1}(f, P_{n}) (:= inf_{p∈P_{n}} ∥f − p∥_{1}).

One easily observes that dist_{1}(f, P_{n}) = dist_{1}(f, K̃_{f,n}), where K̃_{f,n} denotes the compact space {p ∈ P_{n} : ∥p∥_{1} ≤ 2 ∥f∥_{1}}. The existence of a best approximation of f in P_{n} w.r.t. the L_{1}-norm follows from the fact that the continuous function G(f, p) := ∥f − p∥_{1} attains its infimum in K̃_{f,n}. The highly non-trivial part of Theorem 6.1 is the uniqueness of the best L_{1}-approximation.

Define F (f, p) := ∥f − p∥_{1} − dist_{1}(f, P_{n}). Uniqueness can be expressed as

∀n; f ∈ C[0, 1]; p_{1}, p_{2} ∈ P_{n} (⋀_{i=1}^{2} F (f, p_{i}) =^{ℝ} 0 → p_{1} = p_{2}).

Moreover, the space P_{n} can be replaced by the space K̃_{f,n} since any best L_{1}-approximation of f from P_{n} must belong to K̃_{f,n}, or the zero polynomial, which lives in K̃_{f,n}, would be a better approximation of f. Therefore, Theorem 6.1 can be stated as

∀n; f ∈ C[0, 1]; p_{1}, p_{2} ∈ K_{f,n} (⋀_{i=1}^{2} F (f, p_{i}) =^{ℝ} 0 → ∥p_{1} − p_{2}∥_{1} =^{ℝ} 0),

where for technical reasons we use the larger space

K_{f,n} :≡ \{p ∈ P_{n} : ∥p∥_{1} ≤ \frac{5}{2} ∥f∥_{1}\}.

Note that the space C[0, 1] equipped with the L_{1}-norm is not complete, and therefore it is not a Polish space. To bring Jackson’s theorem into the form (2) we use the Polish space (C[0, 1], ∥ · ∥_{∞}). Since the functions f in the space (C[0, 1], ∥ · ∥_{∞}), according to the representation, are endowed with a modulus ω_{f}, the functions ∥ · ∥_{1} : C[0, 1] → ℝ and F are PA^{ω}-definable.

Therefore, Jackson’s theorem falls into the general form described in Section 4.1. As we have seen, the computational content of a uniqueness statement such as the one above is given via a modulus of uniqueness Φ satisfying, for all f ∈ C[0, 1] and n ∈ ℕ,

∀p_{1}, p_{2} ∈ K_{f,n}; ε ∈ ℚ_{+}^{∗} (⋀_{i=1}^{2} F (f, p_{i}) ≤ Φ(f, n, ε) → ∥p_{1} − p_{2}∥_{1} ≤ ε),

independent of the polynomials p_{1} and p_{2}, which range over the compact space K_{f,n}. By the choice of the space K_{f,n} the modulus Φ can be easily extended to a modulus for the whole space P_{n}.

Recall that Φ depends on f via its representation as an element of the Polish space (C[0, 1], ∥ · ∥_{∞}). That is to say, Φ will (a priori) depend on the values of the function f as well as on a modulus of continuity for f. This apparent restriction of Theorem 3.2 is indeed an indication of which inputs are the right ones for the modulus of uniqueness. See, for instance, [13] and [64] where the modulus of uniform continuity is always used as an input for moduli of uniqueness.

Theorem 3.2 guarantees that from any proof of Jackson’s theorem formalizable in a system like E-PA^{ω} + QF-AC^{1,0} + INF we are able to extract a modulus of uniqueness Φ. One such proof, as shown in [44], was presented by Cheney [19] in 1965. Therefore, by Theorem 3.2 we obtain the following a priori information.

Proposition 6.2 Let K_{ω,M} be the compact subspace of C[0, 1] consisting of functions with modulus of continuity ω and uniform norm bounded by M. There exists a modulus of uniqueness Φ (given by a closed term of E-PA^{ω}, i.e. of Gödel’s T) depending only on ω, M, n and ε for the L_{1}-approximation of functions f ∈ K_{ω,M} from the space P_{n}.

In [61] the authors have carried out the extraction of such a modulus of uniqueness out of Cheney’s proof of Jackson’s theorem, providing explicitly the dependencies of Φ (a posteriori information).

Theorem 6.3 ([61]) Let

Φ(ω, n, ε) := min\{\frac{c_{n}ε}{8(n + 1)^{2}} , \frac{c_{n}ε}{2}ω_{n}(\frac{c_{n}ε}{2})\},

where

c_{n} := \frac{⌊n/2⌋!⌈n/2⌉!}{2^{4n+3}(n+1)^{3n+1}} and ω_{n}(ε) := min\{ω(\frac{ε}{4}), \frac{ε}{40(n+1)^{4}⌈ \frac{1}{ω(1)} ⌉}\}.

The functional λε.Φ(ω, n, ε) is a uniform modulus of uniqueness for the best L_{1}-approximation of any function f in C[0, 1] having modulus of uniform continuity ω from P_{n}, i.e. for all n and f ∈ C[0, 1]

∀p_{1}, p_{2} ∈ P_{n}; ε ∈ ℚ_{+}^{∗} (⋀_{i=1}^{2} F (f, p_{i}) ≤ Φ(ω, n, ε) → ∥p_{1} − p_{2}∥_{1} ≤ ε),

where ω is a modulus of uniform continuity of the function f.

Note that, using Markov’s inequality, from any upper bound on ∥p∥_{1} one can easily derive an upper bound on the absolute value of the actual coefficients of the polynomial p.

Although uniqueness of L_{1}-approximation was known since 1921, only in 1975 Björnestål [13] proved the existence of a modulus of uniqueness Φ having the form c_{f,n} ε ω_{n}(c_{f,n} ε), for some constant c_{f,n} depending on f and n. Björnestål’s proof is ineffective and does not supply c_{f,n}. In 1978, Kroó [63] improved Björnestål’s results by showing that a constant c_{ω,n}, depending only on the modulus of uniform continuity of f and n exists, but his proof is also ineffective and no constant is presented. Moreover, Kroó proves that the ε-dependency established by Björnestal is optimal.

By obtaining the modulus of uniqueness explicitly, as in Theorem 6.3, we get as a byproduct all those qualitative results. It should be observed that the form of the modulus Φ depends on the proof from which it was extracted. Different proofs could have given different moduli. The fact that Φ has optimal ε-dependency suggests that Cheney’s proof is in some sense optimal.

The modulus of uniqueness we have obtained can be used in various ways. For instance, as already mentioned, Φ/2 is a modulus for the pointwise continuity of the projection operator.

Theorem 6.4 ([61]) Let P(f, n) denote the operator which produces the best L_{1}-approximation of f from P_{n}. Then, for all n

∀f, g ∈ C[0, 1]; ε ∈ ℚ_{+}^{∗} (∥f − g∥_{1} ≤ \frac{Φ(ω_{f}, ε)}{2} → ∥P(f, n) − P(g, n)∥_{1} ≤ ε),

where ω_{f} denotes a modulus of uniform continuity of f.

The modulus of uniqueness Φ has also been used in [75] by the second author to give the first complexity upper bound on the sequence (p_{n})_{n∈ℕ} of best L_{1}-approximations of a polynomial-time computable function.

Theorem 6.5 ([75]) Let f ∈ C[0, 1] be polynomial-time computable, then the sequence (p_{n})_{n∈ℕ} is strongly NP computable in NP[B_{f}], where B_{f} is an oracle solving a left cut for integration.

As a final remark, note that both the existence and the uniqueness proof make use of the principle INF. While the existence statement has the same logical form of INF, and therefore the use of the principle cannot be eliminated from that proof (although the constructive existence follows via the effective modulus of uniqueness), the uniqueness theorem has the simpler logical form ∀∃, which indicates that INF is not really used in its full strength.

For another case study in the context of Chebycheff approximation see [46] and [47].

7 Proofs based on fixed uses of sequential compactness

By proofs based on sequential compactness we mean proofs which use principles like

• PCM (Principle of monotone convergence) :≡ If a sequence of reals (a_{n})_{n∈ℕ} is non-increasing and bounded from below (say by 0) then it is convergent.

• BW (Bolzano-Weierstraß principle) :≡ Any sequence of reals (a_{n})_{n∈ℕ} belonging to the cube e.g. [0, 1]^{d} has a convergent subsequence.

• A-A (The Arzelà-Ascoli lemma) :≡ Any sequence (f_{n})_{n∈N} ∈ C[0, 1] of equicontinuous and uniformly bounded functions has a convergent subsequence (w.r.t. ∥ · ∥_{∞}).

• Limsup (The existence of the limit superior) :≡ For any sequence (a_{n})_{n∈ℕ} ⊂ [0, 1] there exists a point x ∈ [0, 1] such that x = lim sup_{n→∞} a_{n}.

By a fixed use of sequential compactness we mean an application of such a principle to a particular sequence of reals/functions, in general built out of the parameters of the problem. We shall denote such a fixed application of e.g. PCM to a sequence (a_{n})_{n∈ℕ} as PCM(a_{n}).

Although the principles mentioned above are equivalent to full arithmetical comprehension even over weak base systems (see [55] and [83])^{14}, these principles are often only used for fixed sequences in the given proof. In this case, the contribution to the growth of extractable bounds is much lower. All this has been spelled out in great detail in [50] and [55] for all of the principles mentioned above. We only discuss here briefly PCM(a_{n}) as we will need this in the application discussed in Section 7.1. Let (a_{n})_{n∈ℕ} for the rest of this section denote a sequence in [0, N] for some N ∈ ℕ. PCM(a_{n}) can be written as

PCM(a_{n}) :≡ [Mon(a_{n}) → ∃a ∈ ℝ_{+}( lim_{n→∞} a_{n} = a)],

where Mon(a_{n}) :≡ ∀k(0 ≤ a_{k+1} ≤ a_{k} ≤ N). Since real numbers are represented as Cauchy sequences of rational numbers with fixed rate of convergence, PCM(a_{n}) is in fact equivalent (using QF-AC^{0,0}) to

Mon(a_{n}) → ∃f∀k∀m(m ≥ f(k) → |a_{f(k)} − a_{m}| ≤ \frac{1}{k + 1}).

It is the existence of the Cauchy modulus f which implies Π_{1}^{0}-comprehension which – by iteration – gives Π_{∞}^{0}-comprehension.

However, as mentioned already, the contribution is much weaker (under suitable conditions) when PCM(a_{n}) is applied only to a given fixed sequence (a_{n}) (definable in the parameters of the problem at hand) in a proof of a statement of the form (5) since then the iterated use of the principle is blocked. In fact over sufficiently weak fragments of classical arithmetic in all finite types (to which, though, the axioms Δ of the kind discussed above may be added) such a use of PCM(a_{n}) can be reduced to the use of the arithmetical version^{15}

PCMar(a_{n}) :≡ [Mon(a_{n}) → ∀k∃n∀m(m ≥ n → |a_{n} − a_{m}| ≤ \frac{1}{k + 1})]

14Nevertheless, those can also be treated by monotone functional interpretation using a weak form of monotone bar recursion (cf. Section 8).

15This reduction is very subtle and relies on a special technique of elimination of monotone Skolem functions taking into account a strong monotonicity property of the matrix of PCMar. We do not go here into this as in the application to be discussed below this passage is trivial.

which in turn is equivalent to ∀k∃n∀m(m ≥ n → |ã_{n} − ã_{m}| ≤ \frac{1}{k+1}), where

ã_{n} := max(0, min_{i≤n}(a_{i}, N)).

Hence, PCMar(a_{n}) has the logical form ∀k∃n∀mA_{0}(k, n, m), for an appropriate quantifier-free formula A_{0}. For simplicity we omit the parameter (a_{n})_{n∈ℕ} which, according to the representation of reals used, can be be encoded as a number theoretic function.

Let us now consider how monotone functional interpretation treats an implication with PCMar as premise and a statement of the form (5) as conclusion:

∀x^{1}∀y ≤_{1} sx(PCMar(t(x, y)) → ∃z^{0}B_{0}(x, y, z)),  (10)

where B_{0} is quantifier-free and t is a term creating sequences of reals uniformly in x and y. The (partial) monotone functional interpretation of the negative translation

∀x^{1}∀y ≤_{1} sx(∀k¬¬∃n∀mA_{0}(k, n, m) → ¬¬∃z^{0}B_{0}(x, y, z))  (11)

of (10) is realized by a functional Ω^{∗} satisfying

\{ \begin{matrix}∃Ω ≤^{∗} Ω^{∗}∀Ψ, x∀y ≤ sx \\ (∀k, gA_{0}(k, Ψ(k, g), g(Ψ(k, g))) → B_{0}(x, y, Ω(x, y, Ψ))). \end{matrix}

Suppose now that we have a functional Φ^{∗} satisfying the monotone functional interpretation of the negative translation of ∀x^{1}∀y ≤ sx PCMar(t(x, y)), i.e.

∃Φ ≤^{∗} Φ^{∗}∀x^{1}; y ≤ sx, k, g A_{0}(k, Φ(x, y, k, g), g(Φ(x, y, k, g))))  (12)

then χ(x, Φ^{∗}) := Ω^{∗}(x^{+}, s^{∗}x^{+}, Φ^{∗}(x^{+}, s^{∗}x^{+})) ≥ Ω(x, y, Φ(x, y)) for all x^{1} and y ≤ sx, where s ≤^{∗} s^{∗} and Φ(x, y) := λk, g.Φ(x, y, k, g). Hence

∀x^{1}∀y ≤_{1} sx∃z ≤ χ(x, Φ^{∗}) B_{0}(x, y, z).

So the contribution of the use of PCMar(t(x, y)) to the bound for the conclusion of (10) is given by a functional Φ^{∗} satisfying (12). One easily verifies that we can take

Φ^{∗}(x, y, k, g) := max_{i≤(k+1)N}(g^{i}(0)),  (13)

i.e. Φ^{∗} (in contrast to Φ!) basically is independent from the sequence t(x, y) and only depends on an upper bound N on the first element of the sequence. This feature will play a crucial role in the applications to metric fixed point theory which we will discuss in the next example.

7.1 Example 3: Asymptotic regularity of iterations of nonexpansive mappings

One of the most active areas of nonlinear functional analysis is the fixed point theory of nonexpansive mappings (see e.g. [41]). In this section we report on the results of a recent case study of proof mining carried out by the first author (see [56, 57, 59] and – together with Laurenţiu Leuştean – [60]).

Definition 7.1 Let (X, ∥ · ∥) be a normed linear space and C ⊆ X be a subset of X. A function f : C → C is called nonexpansive if

∀x, y ∈ C(∥f(x) − f(y)∥ ≤ ∥x − y∥).

In view of Banach’s result, the fixed point theory of contractions is rather simple. Even the case of contractive mappings enjoys – as we saw above – many of the features of contractions, e.g. the uniqueness of the fixed point. Things, however, change radically for nonexpansive functions. Fixed points, if existing at all, will not be unique and even if uniqueness holds the Banach iteration in general will not converge to the fixed point. Instead, other iterations play a crucial role here.

In the following, (X, ∥·∥) will be an arbitrary normed linear space, C ⊆ X a non-empty convex subset of X and f : C → C a nonexpansive mapping.

We consider the so-called Krasnoselski-Mann iteration starting from x ∈ C

x_{0} := x, x_{k+1} := (1 − λ_{k})x_{k} + λ_{k}f(x_{k}),

where (λ_{k})_{k∈ℕ} is a sequence of real numbers in [0, 1]. For more information on the relevance of this kind of generalized Krasnoselski [62] iterations see e.g [15, 25, 70, 80].

Let r_{C}(f) := inf_{x∈C} ∥x−f(x)∥. For the rest of this section we assume, following [15] and [36], that (λ_{k})_{k∈ℕ} is divergent in sum, which can be expressed (since λ_{k} ≥ 0) as^{16}

∀n, i ∈ ℕ∃k ∈ ℕ (∑_{j=i}^{i+k} λ_{j} ≥ n) ,  (14)

and that

∀k ∈ ℕ(λ_{k} ≤ 1 − \frac{1}{K}) for some K ∈ ℕ.  (15)

16This form will be particularly suitable below.

Theorem 7.2 ([15]) Suppose that (λ_{k})_{k∈ℕ} satisfies the conditions (14) and (15). Then the Krasnoselski-Mann iteration (x_{n})_{n∈ℕ} starting from any point x ∈ C satisfies

∥x_{n} − f(x_{n})∥ →^{n→∞} r_{C}(f).

Under quite general circumstances one can prove that r_{C}(f) = 0.

Theorem 7.3 ([15], [36]) Under the assumptions of the previous theorem and the additional assumption that there exists a x^{∗} ∈ C such that (x_{n}^{∗})_{n∈ℕ} is a bounded sequence the following holds

∀x ∈ C(∥x_{n} − f(x_{n})∥ →^{n→∞} 0) (called ‘asymptotic regularity’).

Remark 7.4 The special case of Theorem 7.3 in which only the asymptotic regularity of the sequence (x_{n}^{∗}) is conclude is due to Ishikawa [36].^{17} The striking aspect of Ishikawa’s theorem is that it does not rely on the assumption of X being uniformly convex as all results of that kind prior to [36] did. For uniformly convex spaces X, bounded C and constant λ_{k} = λ the result was proved in [18], and for general λ_{k} – even more general than in Ishikawa’s theorem – it follows from [32] for such spaces. If C is, moreover, compact and λ = \frac{1}{2}, asymptotic regularity was (for uniformly convex X) already proved in [62].

In oder to see that our general meta-theorem on proof mining can be applied to Theorem 7.2 we first have to find a proper formalization of the conclusion of the theorem. We first realize, that the ineffective existence of r_{C}(f) is not really needed to formulate the conclusion which can be stated without r_{C}(f) as

∀ε > 0∃n ∈ ℕ∀m ≥ n∀x^{∗} ∈ C(∥x_{m} − f(x_{m})∥ < ∥x^{∗} − f(x^{∗})∥ + ε). (16)

An easy and well-known lemma shows that (∥x_{n}−f(x_{n})∥)_{n∈ℕ} is non-increasing so that the discussion from 4.6 applies. Therefore, the quantifier ‘∀m ≥ n’ in (16) is in fact superfluous. Nevertheless, due to the alternation ∃n ∈ ℕ∀x^{∗} ∈ C, (16) still does not of the form ∀∃ required (as a consequence of the use of classical logic) by our meta-theorems 3.2 and 3.3.^{18} The following variant of (16), however, does have this form^{19}

17For constant λ_{k} = λ the result was independently obtained in [24].

18Indeed, an effective bound on ‘∃n’ in (16) would imply the computability of r_{C}(f) (in f, x, λ_{k} and ∥ · ∥) which is unlikely to be true in the general case.

∀ε > 0∀x^{∗} ∈ C∃n ∈ ℕ(∥x_{n} − f(x_{n})∥ < ∥x^{∗} − f(x^{∗})∥ + ε).  (17)

Under the assumption of the existence of r_{C}(f), formulations (16) and (17) are actually equivalent. In the following we shall study in more detail the form (17) of Theorem 7.2. Note that, in this case, a bound on n shall a priori depend on the additional input x^{∗}.

Let us now consider the assumptions of Theorem 7.2 and assume for the moment that X is complete and separable and C a subset which can be explicitly represented in our underlying formal system. Observe that the assumptions of C being convex and f a nonexpansive function are purely universal^{20}. Universal assumptions, however, do not change the logical form as required by our meta-theorem as they just add a couple of more existential quantifiers to the interpreted formula.

Monotone functional interpretation of the assumptions (14) and (15) on λ_{k} introduce new inputs, namely a bound α : ℕ × ℕ → ℕ such that

∀n, i ∈ ℕ(n ≤ ∑_{j=i}^{i+α(i,n)} λ_{j})  (18)

and a K ∈ ℕ such that

∀n ∈ ℕ(λ_{n} ≤ 1 − \frac{1}{K}),  (19)

where both (18), (19) are purely universal. Given α and K as additional inputs, we can take the quantification over the sequences (λ_{n}) as quantification over the compact Hilbert cube [0, 1]^{ℕ} plus an explicit stipulation that (λ_{n}) satisfies (18) and (19). From this the meta-theorem provides the a priori information that the bound on the convergence in Theorem 7.2 we are about to extract might depend on α, K (and x^{∗}) as new inputs which were not visible in the original formulation of the theorem, but that it will be independent from any particular (λ_{k}) itself (cf. Section 3.1).

19One can actually consider an intermediate version where x^{∗} is allowed to be a sequence depending on n. Bounds for this stronger form are obtained in [59].

20We do not even need to express explicitly that f (represented as a function on representatives of elements in x ∈ C) is extensional (i.e. respects the equivalence relation x =_{X} y expressing that x, y represent the same X-element) since the extensionality follows from the continuity of f which in turn follows from the fact that f is nonexpansive.

Let us now consider the lemmas used in the proof of Theorem 7.2. By far the largest part of the proof concerns a highly non-trivial inequality due to [29] (whose proof is based on [38] and also [36]): for all n, i ∈ ℕ

\{ \begin{matrix}(1 + ∑_{k=i}^{n+i−1} λ_{k})∥x_{i} − f(x_{i})∥ ≤ \\ ∥x_{i} − f(x_{i+n})∥ + [ ∏_{k=i}^{n+i−1} \frac{1}{1−λ_{k}} ] (∥x_{i} − f(x_{i})∥ − ∥x_{i+n} − f(x_{i+n})∥). \end{matrix}

Since this inequality is purely universal (as are two other simpler inequalities used) we can simply take it as yet another implicative assumption in the proof analysis, i.e. we do not have to consider its proof at all.

From the point of view of proof mining, the only problematic tool used in the proof is the ineffective fact that

the non-increasing sequence (∥x_{n} − f(x_{n})∥) of reals ≥ 0 has a limit,

which is just PCM(∥x_{n} − f(x_{n})∥), i.e. a fixed instance of PCM. As we have discussed above, the use of PCM in this case can be reduced, in the poof of Theorem 7.2, to its arithmetical version PCMar(∥x_{n} − f(x_{n})∥) which states that (∥x_{n} − f(x_{n})∥)_{n∈ℕ} is a Cauchy sequence. This reduction is sound provided the proof can be carried out relative to a rather weak framework like the fragment E-G_{3}A^{ω} of E-PA^{ω} which, in particular must not contain the iteration functional Φ_{it}(x, y, f) := f^{x}(y). In fact this is the case, though it seems at first sight impossible as the very sequence (x_{n}) is defined by iteration. We can, however, take

∀n (x_{n+1} = (1 − λ_{n})x_{n} + λ_{n}f(x_{n}))

just as one more purely universal implicative assumption and do not need for the proof analysis to prove that such a sequence can be formed. So in total, taking A to be the conjunction of all the universal assumptions considered we get

PCMar → (A → (17)),

where (17) (and hence A → (17)) is a ∀∃-formula. Therefore, the discussion of the modus ponens problem above applies and we can extract a bound for (17) in f, x, x^{∗}, α, K which, as a consequence of the use of PCMar, will involve a use of the iteration functional Φ_{it}. Indeed, in [57], the first author obtained the following quantitative version of Theorem 7.2 (as a matter of fact, we not even need to assume that (X, ∥ · ∥) is complete or separable).

Theorem 7.5 ([57]) Let (X, ∥ · ∥) be a normed linear space, C ⊆ X a nonempty convex subset and f : C → C a nonexpansive mapping. Let (λ_{k})_{k∈ℕ} be a sequence in [0, 1] which is divergent in sum and satisfies

∀k ∈ ℕ(λ_{k} ≤ 1 − \frac{1}{K})

for some K ∈ ℕ. Let α : ℕ → ℕ be such that

∀i, n ∈ ℕ(α(i, n) ≤ α(i + 1, n) ∧ n ≤ ∑_{s=i}^{i+α(i,n)−1} λ_{s}).

Let (x_{n})_{n∈ℕ} be the Krasnoselski-Mann iteration

x_{0} := x, x_{n+1} := (1 − λ_{n})x_{n} + λ_{n}f(x_{n}),

starting from x ∈ C. Then the following holds

∀x, x^{∗} ∈ C∀ε > 0∀n ≥ h(ε, x, x^{∗}, f, K, α)(∥x_{n} − f(x_{n})∥ < ∥x^{∗} − f(x^{∗})∥ + ε),

where^{21}

h(ε, x, x^{∗}, f, K, α) := α̂(⌈2∥x − f(x)∥ · exp(K(M + 1))⌉ ^{−^{.}} 1, M),

with M := ⌈\frac{1+2∥x−x^{∗}∥}{ε}⌉ and

α̂(0, M) := α̃(0, M), α̂(m + 1, M) := α̃(α̂(m, M), M) with α̃(m, M) := m + α(m, M) (m ∈ ℕ).

Instead of M we may use any upper bound ℕ ∋ M̃ ≥ \frac{1+2∥x−x^{∗}∥}{ε}. Likewise, ∥x − f(x)∥ may be replaced by any upper bound.

Remark 7.6 An α satisfying the conditions of the theorem can be com-

puted from any β : ℕ → ℕ such that n ≤ ∑_{s=0}^{β(n)} λ_{s} (for all n) by α(i, n) :=

max_{j≤i}(β′(j, n)), where β′(i, n) := β(n + i) − i + 1.

Perhaps the most useful aspect of Theorem 7.5 is that it displays the very limited dependency of the rate of uniform convergence from the input data x, f, x^{∗}, λ_{k} and X, C. In fact, if C is bounded with d ≥ diam(C), then the

21n −^{.} 1 = max(0, n − 1).

dependence from x, x^{∗} and f can be removed altogether as ∥x − f(x)∥ and ∥x−x^{∗}∥ both can be replaced by d. Moreover, it follows that the bound only depends on d but not on C itself (see [57]). In fixed point theory non-trivial functional analytic embedding techniques have been used for some 20 years to obtain (partial) such uniformity results for bounded C. In this way the independence from x is proved in [24] for constant λ_{k} := λ. In [29] this is extended to uniformity also w.r.t. f (for general λ_{k}) but not w.r.t. C (in the sense above). In [30] it is in fact conjectured that the uniformity in C might only hold in the much simpler case of uniformly convex case (cf. [40]). For constant λ, full uniformity was finally established in [4]. Our result gives full uniformity for general λ_{k} and even displays that the rate of convergence is to a large extend independent from λ_{k}, depending only on α and K.

The next theorem, which is based on Theorem 7.5, allows to push the uniformity even further to the case where C is no longer assumed to be bounded but only to contain some point x^{∗} whose iteration sequence (x_{n}^{∗}) is bounded, i.e. the context of Theorem 7.3.

Theorem 7.7 ([59]) Under the assumptions of Theorem 7.5 the following holds. Let d > 0, x, x^{∗} ∈ C be such that ∀n(∥x_{n}^{∗}∥ ≤ d) and ∥x − x^{∗}∥ ≤ d. Then

∀ε > 0∀n ≥ h(ε, d, K, α)(∥x_{n} − f(x_{n})∥ ≤ ε),

where

h(ε, d, K, α) := α̂(⌈12 · exp(K(M + 1))⌉ − 1, M),
with M := ⌈\frac{7d}{ε}⌉ and α̂ as in Theorem 7.5.

Note that the bound only depends on \frac{d}{ε}, K and α!

Proof. The theorem follows from [59] (Thm. 2.5 plus Remarks 2.2 and 2.6).

Whereas this result easily follows from the logical analysis in [57] (which resulted in Theorem 7.5) of the proof of Theorem 7.2 and does not use any functional analytic tools at all, it seems that the embedding techniques, as used e.g. in [29] and most recently in a new form in [39], are not applicable as they heavily rely on the boundedness of C. So the logical approach here not only gives new quantitative bounds but even new qualitative results which are superior to what has been achieved by more traditional functional analytic means. For more results in this direction and proofs of the results discussed see [56], [57] and [59].

Another benefit of the logical approach is that it easily generalizes to other settings for which the basic inequalities used in the proof of the Borwein-Reich-Shafrir result can be verified. Since no functional analytic embeddings are used there is no need to exploit any new analytic tool to obtain uniformity results. Very recently ([60]) the first author (together with Laurenţiu Leuştean) showed in this way that the results (as well as the basic structure of their proofs) presented above extend to hyperbolic spaces in the sense of Reich and Shafrir [79] (including the Hilbert ball with the hyperbolic metric) and – to a large extent – also to the still more general class of spaces of hyperbolic type [29] (which were first introduced in [85] under the name of ‘convex metric spaces’) and directionally nonexpansive mappings in the sense of [39]. In particular, strengthened versions of the main results of [39] follow as special cases.

8 Proofs based on applications of full sequential compactness

In the previous section we have shown how to treat proofs of theorems having the form (5) which make use of e.g. PCM applied to a fixed sequence (a_{n})_{n∈ℕ}. In this section we address the problem of analyzing such proofs in which PCM (or any of the other principles) is used to obtain the convergence of an arbitrary sequence, which is not actually built in the proof.

As mentioned above, such use of PCM is in fact equivalent to arithmetical comprehension. In this case we can not expect to give a constructive treatment of the proof without making use of bar recursion (cf. [84]).

For the sake of simplicity, all the sequences (a_{n})_{n∈ℕ} are assumed to be contained the interval [0, N]. We want to produce a functional realizing the m.f.i. of the negative translation of (cf. Section 7)

∀(a_{n})_{n∈ℕ}∃f∀k, m(m ≥ fk → |ã_{fk} − ã_{m}| ≤ \frac{1}{k + 1}).

We have seen in Section 7 that the m.f.i. of the arithmetical version of PCM,

∀(a_{n})_{n∈ℕ}∀k∃n∀m(m ≥ n → |ã_{n} − ã_{m}| ≤ \frac{1}{k + 1})  (20)

can be easily realized using the iteration functional. Formula (20) has the logical form ∀(a_{n})_{n∈ℕ}∀k∃n∀mA_{0}(k, n, m), for some quantifier free A_{0}. Note that PCM is obtained by an application of Π_{1}^{0}-AC to this formula

{∀(a_{n})_{n∈ℕ}∀k∃n∀mA_{0}(k, n, m) AC \atop ∀(a_{n})_{n∈ℕ}∃f∀k, mA_{0}(k, fk, m)}

To make constructive sense of PCM we first apply negative translation to the proof above to get a new proof (in the following we omit ∀(a_{n})_{n∈ℕ})

{∀k¬¬∃n∀mA_{0}(k, n, m) AC^{N}(∀mA_{0}(k, n, m)) \atop ¬¬∃f∀k, mA_{0}(k, fk, m)}

We finally apply functional interpretation to obtain

∃Φ^{2}∀k^{0}, g^{1} A_{0}(k, Φkg, g(Φkg)) (AC^{N}(∀mA_{0}(k, n, m)))^{D}
∀Ψ_{1}, Ψ_{2}∃fA_{0}(Ψ_{1}(f), f(Ψ_{1}(f)), Ψ_{2}(f))

As done in Section 7 (cf. (13)), we can define via iteration a functional Φ^{∗}

Φ^{∗}(k, g) := max_{i≤(k+1)N}(g^{i}(0)).

which majorizes a realizer of

∃Φ^{2}∀k^{0}, g^{1}A_{0}(k, Φkg, g(Φkg)),

i.e. ∃Φ ≤^{∗} Φ^{∗}∀k^{0}, g^{1}A(k, Φkg, g(Φkg)). We now set out to obtain a realizer for the monotone functional interpretation of AC^{N}(∀mA_{0}(k, n, m)), i.e.

∀k¬¬∃n∀mA_{0}(k, n, m) → ¬¬∃f∀k, mA_{0}(k, fk, m).

Monotone functional interpretation provides majorants for the realizers of the existential quantifiers of

∀Φ, Ψ_{1}, Ψ_{2}∃f, k, g[A_{0}(k, Φkg, g(Φkg)) → A_{0}(Ψ_{1}f, f(Ψ_{1}f), Ψ_{2}f)]. (21)

By BR_{0,1} we mean the bar recursive functional (defined by Spector [84]) satisfying the following equation:

BR_{0,1}(Y, G, H, s) =^{1} \{ \begin{matrix}G(s) & if Y (s ∗ λn.0) ≤ n \\ H(s, λy^{0}.BR_{0,1}(Y, G, H, s ∗ y)) & otherwise. \end{matrix}

Let p be a shorthand for Φ, Ψ_{1}, Ψ_{2}. Spector showed that by taking

Y := λp . Ψ_{1}
G := λp, s . s ∗ λn.0
H := λp, s, γ . γ(Φ(|s|, λy.Ψ_{2}(γ(y))))

the functionals

F := λp . BR_{0,1}(Y (p), G(p), H(p), ⟨ ⟩)
K := λp . Ψ_{1}(F(p))
G := λp, y . Ψ_{2}(BR_{0,1}(\overline{F(p)} K(p) ∗ y))

realize f, k and g in (21). Let BR_{0,1}^{∗} be the majorant of BR_{0,1} presented by Bezem [10]. Since we can easily find terms Y^{∗}, G^{∗} and H^{∗} which majorize Y, G and H above, we get that

F^{∗} := λp . BR_{0,1}^{∗}(Y^{∗}(p), G^{∗}(p), H^{∗}(p), ⟨ ⟩)
K^{∗} := λp . Ψ_{1}(F^{∗}(p))
G^{∗} := λp, y . Ψ_{2}(BR_{0,1}^{∗}(\overline{F^{∗}(p)}K^{∗}(p) ∗ max(\overline{F^{∗}(p)}K^{∗}(p), y))),

where max(s, x) := max{s_{0}, …, s_{|s|−1}, x}, are terms satisfying the monotone functional interpretation of AC^{N}. Note that λ(a_{n}), Ψ_{1}, Ψ_{2}.F((a_{n}), Φ, Ψ_{1}, Ψ_{2}) realizes

∀(a_{n})∀Ψ_{1}, Ψ_{2}∃f(Ψ_{2}(f) ≥ f(Ψ_{1}(f)) → |a_{f(Ψ_{1}f)} − a_{Ψ_{2}f}| ≤ \frac{1}{Ψ_{1}f + 1})),

and λ(a_{n}), Ψ_{1}, Ψ_{2}.F^{∗}(N, Φ^{∗}, Ψ_{1}, Ψ_{2}) is a majorant for this realizer.

Moreover, notice that this realizer is also independent of the sequence (a_{n})_{n∈ℕ}. Therefore, in the same way as we did in Section 7, uniformity results can still be obtained even when the full power of PCM is used in a proof of a theorem having the form (5).

Remark 8.1 By the above we can treat proofs in the system T^{ω}+QF-AC^{1,0}+ PCM. Note that for T^{ω} = PRA^{ω} the above system can be viewed as a finite type extension of ACA_{0} known from reverse mathematics. In that case the bound extracted by m.f.i. from a proof of a theorem of form (6) will be a closed term of type 2 of PRA^{ω}[BR_{0,1}] which (by [34, 52]) denotes a functional in Gödel’s primitive recursive functionals T of finite type (note that PRA^{ω} only contains the fragment T_{0} of T with primitive recursion on type 0).

References

[1] J. Angelos, M. Henry, E. Kaufman, Lenker T., and A. Kroó. Local and global Lipschitz constants. Journal of Approximation Theory, 46:137– 156, 1986.

[2] J. Angelos and A. Kroó. The equivalence of the moduli of continuity of the best approximation operator and of strong unicity in L^{1}. Journal of Approximation Theory, 46:129–136, 1986.

[3] J. Avigad and S. Feferman. Gödel’s functional (”Dialectica”) interpretation. In S. R. Buss, editor, Handbook of proof theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 337–405. Elsevier, North-Holland, Amsterdam, 1998.

[4] J Baillon and R. E. Bruck. The rate of asymptotic regularity is 0(\frac{1}{\sqrt{n}}). In Theory and applications of nonlinear operators of accretive and monotone type, volume 178 of Lecture Notes in Pure and Appl. Math., pages 51–81. Dekker, New York, 1996.

[5] M. Bartelt and W. Li. Error estimates and Lipschitz constants for best approximation in continuous function spaces. Computers and Mathematics with Application, 30(3-6):255–268, 1995.

[6] M. Bartelt and D. Schmidt. Lipschitz conditions, strong uniqueness, and almost Chebyshev subspaces of c(x). Journal of Approximation Theory, 40:202–215, 1984.

[7] M. J. Beeson. Foundations of Constructive Mathematics. Metamathematical Studies. Springer-Verlag, 1985.

[8] G. Bellin. Ramsey interpreted: a parametric version of Ramsey’s theorem. In Logic and computation (Pittsburgh, PA, 1987), volume 106, pages 17–37. Amer. Math. Soc., Providence, RI, 1990.

[9] U. Berger, H. Schwichtenberg, and W. Buchholz. Refined program extraction from classical proofs. Annals of Pure and Applied Logic, 114:3– 25, 2002.

[10] M. Bezem. Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. Journal of Symbolic Logic, 50:652–660, 1985.

[11] E. Bishop. Foundations of constructive analysis. McGraw-Hill, New York, 1967.

[12] E. Bishop. Mathematics as a numerical language. In A. Kino, J. Myhill, and R. E. Vesley, editors, Intuitionism and Proof Theory, pages 53–71. North-Holland Publishing Company, Amsterdam - London, 1970.

[13] B. O. Björnestål. Continuity of the metric projection operator I-III. The preprint series of Department of Mathematics 17, Royal Institute of Technology, Stockholm, TRITA-MAT, 1975.

[14] B. O. Björnestål. Local Lipschitz continuity of the metric projection operator. Approximation theory. Banach Center Publications, 4:43–53, 1979.

[15] J. Borwein, S. Reich, and I. Shafrir. Krasnoselski-Mann iterations in normed spaces. Canad. Math. Bull., 35:21–28, 1992.

[16] D. S. Bridges, F. Richman, W. H. Julian, and R. Mines. Extensions and fixed points of contractive maps in R^{n}. J. Math. Anal. Appl., 165(2):438– 456, 1992.

[17] F. E. Browder. Nonexpansive nonlinear operators in a Banach space. Proc. Nat. Acad. Sci. U.S.A., 54:1041–1044, 1965.

[18] F. E. Browder and W. V. Petryshyn. The solution by iteration of nonlinear functional equations in Banach spaces. Bull. Amer. Math. Soc., 72:571–575, 1966.

[19] E. W. Cheney. An elementary proof of Jackson’s theorem on meanapproximation. Mathematics Magazine, 38:189–191, 1965.

[20] J. A. Clarkson. Uniformly convex spaces. Transactions of the American Mathematical Society, 40:396–414, 1936.

[21] P. Collaço and J. Carvalho e Silva. A complete comparison of 25 contraction conditions. Nonlinear Anal., 30:471–476, 1998.

[22] C. Delzell. Kreisel’s unwinding of Artin’s proof. In P. Odifreddi, editor, Kreiseliana: About and around George Kreisel, pages 113–246. A. K. Peters, Wellesley, MA, 1996.

[23] M. Edelstein. On fixed and periodic points under contractive mappings. J. London Math. Soc., 37:74–79, 1962.

[24] M. Edelstein and R. C. O’Brien. Nonexpansive mappings, asymptotic regularity and successive approximations. J. London Math. Soc., 17:547– 554, 1978.

[25] H. W. Engl and A. Leitão. A Mann interative regularization method for elliptic Cauchy problems. Numer. Funct. Anal. and Optimiz., 22:861– 884, 2001.

[26] S. Feferman. Kreisel’s ‘Unwinding Program’. In P. Odifreddi, editor, Kreiseliana: about and around Georg Kreisel, pages 247–273. A. K. Peters, Wellesley Massachusetts, 1996.

[27] J.-Y. Girard. Proof Theory and Logical Complexity. Studies in Proof Theory, Bibliopolis. Bibliopolis, Naples, 1987.

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

[29] K. Goebel and W. A. Kirk. Iteration processes for nonexpansive mappings. In Topological Methods in Nonlinear Functional Analysis, volume 21 of Contemporary Mathematics, pages 115–123. AMS, 1983.

[30] K. Goebel and W. A. Kirk. Topics in metric fixed point theory, volume 28 of Cambridge studies in advanced mathematics. Cambridge University Press, 1990.

[31] K. Goebel and S. Reich. Uniform convexity, hyperbolic geometry, and nonexpansive mappings, volume 83 of Monographs and Textbooks in Pure and Applied Mathematics. Marcel Dekker, Inc., New York, 1984.

[32] C. W. Groetsch. A note on segmenting Mann iterates. J. of Math. Anal. and Appl., 40:369–372, 1972.

[33] W. A. Howard. Hereditarily majorizable functionals of finite type. In A. S. Troestra, editor, Metamathematical investigation of intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454–461. Springer Verlag, 1973.

[34] W. A. Howard. Ordinal analysis of simple cases of bar recursion. Journal of Symbolic Logic, 46(1):17–30, 1981.

[35] R. Huotari and S. Sahab. Strong unicity versus modulus of convexity. Bull. Austral. Math. Soc., 49:305–310, 1994.

[36] S. Ishikawa. Fixed points and iterations of a nonexpansive mapping in a Banach space. Proc. Amer. Math. Soc., 59:65–71, 1976.

[37] D. Jackson. Note on a class of polynomials of approximation. Transactions of the American Mathematical Society, 22:320–326, 1921.

[38] W. A. Kirk. Krasnoselskii’s iteration process in hyperbolic space. Numer.Funct. Anal. Optimiz., 4:371–381, 1982.

[39] W. A. Kirk. Nonexpansive mappings and asymptotic regularity. Nonlinear Analysis, 40:323–332, 2000.

[40] W. A. Kirk and C. Martinez-Yanez. Approximate fixed points for nonexpansive mappings in uniformly convex spaces. Annales Polonici Mathematici, 51:189–193, 1990.

[41] W. A. Kirk and B. Sims, editors. Handbook of Metric Fixed Point Theory. Kluwer Academic Publishers, 2001.

[42] K.-I. Ko. Complexity theory of real functions. Birkhäuser, Boston-Basel-Berlin, 1991.

[43] G. Koethe. Topoplogische Lineare Räume. Springer-Verlag Berlin-Göttingen-Heidelberg, 1960.

[44] U. Kohlenbach. Theory of majorizable and continuous functionals and their use for the extraction of bounds from non-constructive proofs: effective moduli of uniqueness for best approximations from ineffective proofs of uniqueness (german). PhD thesis, Frankfurt, pp. xxii+278, 1990.

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

[46] U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic, 64:27–94, 1993.

[47] U. Kohlenbach. New effective moduli of uniqueness and uniform a–priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization, 14:581–606, 1993.

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

[49] U. Kohlenbach. Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals. Archive for Mathematical Logic, 36:31–71, 1996.

[50] U. Kohlenbach. Arithmetizing proofs in analysis. Lecture Notes in Logic, 12:115–158, 1998.

[51] U. Kohlenbach. Relative constructivity. Journal of Symbolic Logic, 63:1218–1238, 1998.

[52] U. Kohlenbach. On the no-counterexample interpretation. Journal of Symbolic Logic, 64:1491–1511, 1999.

[53] U. Kohlenbach. The use of a logical principle of uniform boundedness in analysis. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundations of Mathematics, volume 280 of Synthese Library, pages 93– 106. Kluwer Academic Publishers, 1999.

[54] U. Kohlenbach. Proof theory and computational analysis. In Klaus Keimel Abbas Edalat, Achim Jung and Marta Kwiatkowska, editors, Electronic Notes in Theoretical Computer Science, volume 13. Elsevier Science Publishers, 2000.

[55] U. Kohlenbach. Things that can and things that can’t be done in PRA. Ann. Pure Appl. Logic, 102:223–245, 2000.

[56] U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In J. Blanck, V. Brattka, and P. Hertling, editors, Computability and Complexity in Analysis, (CCA’2000), volume 2064 of Lecture Notes in Computer Science, pages 119–145. Springer, 2001.

[57] U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numerical Functional Analysis and Optimization, 22:641– 656, 2001.

[58] U. Kohlenbach. Foundational and mathematical uses of higer types. In Reflections on the Foundations of Mathematics: Essay in Honor of Solomon Feferman, volume 15 of Lecture Notes in Logic. A. K. Peters, Ltd., 2002.

[59] U. Kohlenbach. Uniform asymptotic regularity for Mann iterates. BRICS Research Series RS-02-10, 17 pp., BRICS, 2002. Submitted.

[60] U. Kohlenbach and L. Leuştean. Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Preprint, 33 pages, 2002.

[61] U. Kohlenbach and P. Oliva. Proof mining in L_{1}-approximation. To appear in: Annals of Pure and Applied Logic.

[62] M. A. Krasnoselski. Two remarks on the method of successive approximation. Usp. Math. Nauk (N.S.), 10:123–127, 1955. (Russian).

[63] A. Kroó. On the continuity of best approximations in the space of integrable functions. Acta Mathematica Academiae Scientiarum Hungaricae, 32:331–348, 1978.

[64] A. Kroó. On the uniform modulus of continuity of the operator of best approximation in the space of periodic functions. Acta Math. Academiae Scientiarum Hungaricae, 34:185–203, 1979.

[65] A. Kroó. On strong unicity of L_{1}-approximation. Proceedings of the American Mathematical Society, 83(4):725–729, 1981.

[66] P.-K. Lin. Strongly unique best approximation in uniformly convex Banach spaces. J. Approx. Theory, 56:101–107, 1989.

[67] H. Luckhardt. Extensional Gödel Functional Interpretation – A Consistency Proof of Classical Analysis, volume 306. Springer Verlag, 1973.

[68] H. Luckhardt. Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. Journal of Symbolic Logic, 54:234–263, 1989.

[69] H. Luckhardt. Bounds extracted by Kreisel from ineffective proofs. In P. Odifreddi, editor, Kreiseliana: About and around George Kreisel, pages 289–300. A. K. Peters, Wellesley, MA, 1996.

[70] W. R. Mann. Mean value methods in iteration. Proc. Amer. Math. Soc., 4:506–510, 1953.

[71] K. Martin. Unique fixed points in domain theory. Electronic Notes in Theoretical Computer Science, 45, 2001. 11 pages.

[72] J. Meszáros. A comparison of various definitions of contractive type mappings. Bull. Calcutta Math. Soc., 84:167–194, 1992.

[73] D. J. Newman and H. S. Shapiro. Some theorems on Chebycheff approximation. Duke Mathematical Journal, 30:673–681, 1963.

[74] P. S. Novikoff. On the consistency of certain logical calculus. Matematiceskij sbornik (Recueil-Mathématique, T.12), 54:230–260, 1943.

[75] P. Oliva. On the computational complexity of best L_{1}-approximation. to appear in Mathematical Logic Quarterly.

[76] M. Pour-El and J. Ian Richards. Computability in Analysis and Physics. Perspectives in Mathematical Logic. Springer-Verlag, 1989.

[77] B. Prus and R. Smarzewski. Strongly unique best approximations and centers in uniformly convex spaces. J. Math. Anal. Appl., 121:10–21, 1987.

[78] E. Rakotch. A note on contractive mappings. Proceedings of the American Mathematical Society, 13:459–465, 1962.

[79] S. Reich and I. Shafrir. Non-expansive iterations in hyperbolic spaces. Nonlinear Analysis, Theory, Methods and Applications, 15:537–558, 1990.

[80] B. E. Rhoades. Fixed point iterations using infinite matrices. Trans. Amer. Math. Soc., 196:161–176, 1974.

[81] B. E. Rhoades. A comparision of various definitions of contractive mappings. Transactions of the American Mathematical Society, 226:257–290, 1977.

[82] B. E. Rhoades. Contractive definitions. In Th M. Rassias, editor, Nonlinear analysis, pages 513–526. World Sci. Publishing, Singapore, 1987.

[83] S. G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999.

[84] C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathmatics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics, volume 5, pages 1–27. American Mathematical Society, Providence, Rhode Island, 1962.

[85] W. Takahashi. A convexity in metric space and nonexapansive mappings. I. Kodai Math. Se. Rep., 22:142–149, 1970.

[86] A. S. Troelstra. Metamathematical investigation of intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer Verlag, 1973.

[87] A. S. Troelstra. Realizability. In S.R. Buss, editor, Handbook of proof theory, volume 137, pages 408–473. North Holland, Amsterdam, 1998.

[88] K. Weihrauch. Computable Analysis. Springer-Verlag, 2000.

Recent BRICS Report Series Publications

RS-02-31 Ulrich Kohlenbach and Paulo B. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. June 2002. 47 pp.

RS-02-30 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2002.

RS-02-29 Christian N. S. Pedersen and Tejs Scharling. Comparitive Methods for Gene Structure Prediction in Homologous Sequences. June 2002.

RS-02-28 Ulrich Kohlenbach and Laurenţiu Leuştean. Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces. June 2002. 33 pp.

RS-02-27 Anna Östlin and Rasmus Pagh. Simulating Uniform Hashing in Constant Time and Optimal Space. 2002. 11 pp.

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002.

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis for Dynamic XML. May 2002. 13 pp.

RS-02-23 Antonio Di Nola and Laurenţiu Leuştean. Compact Representations of BL-Algebras. May 2002. 25 pp.

RS-02-22 Mogens Nielsen, Catuscia Palamidessi, and Frank D. Valencia. On the Expressive Power of Concurrent Constraint Programming Languages. May 2002. 34 pp.

RS-02-21 ZoltánÉsik and Werner Kuich. Formal Tree Series. April 2002. 66 pp.

RS-02-20 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers (Preliminary Version). April 2002. 56 pp.