BRICS

Basic Research in Computer Science

General Logical Metatheorems for Functional Analysis

Philipp Gerhardy Ulrich Kohlenbach BRICS Report Series RS-05-21 ISSN 0909-0878 July 2005 BRICS RS-05-21 Gerhardy & Kohlenbach: General Logical Metatheorems for Functional Analysis Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Philipp Gerhardy & Ulrich Kohlenbach.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/05/21/

General logical metatheorems for functional analysis

Philipp Gerhardy, BRICS, Department of Computer Science, University of Aarhus, Aabogade 34, DK-8200 Aarhus N, Denmark, currently: Department of Mathematics, Darmstadt University of Technology

Ulrich Kohlenbach, Department of Mathematics, Darmstadt University of Technology, Schlossgartenstraße 7, D-64289 Darmstadt, Germany

July 29, 2005

Abstract

In this paper we prove general logical metatheorems which state that for large classes of theorems and proofs in (nonlinear) functional analysis it is possible to extract from the proofs effective bounds which depend only on very sparse local bounds on certain parameters. This means that the bounds are uniform for all parameters meeting these weak local boundedness conditions. The results vastly generalize related theorems due to the second author where the global boundedness of the underlying metric space (resp. a convex subset of a normed space) was assumed. Our results treat general classes of spaces such as metric, hyperbolic, CAT(0), normed, uniformly convex and inner product spaces and classes of functions such as nonexpansive, Hölder-Lipschitz, uniformly continuous, bounded and weakly quasi-nonexpansive ones. We give several applications in the area of metric fixed point theory. In particular, we show that the uniformities observed in a number of recently found effective bounds (by proof theoretic analysis) can be seen as instances of our general logical results.

1 Introduction

In [22], the second author established - as part of a general project of applied proof theory - logical metatheorems which guarantee a-priorily the extractability of uniform bounds from large classes of proofs in functional analysis. ‘Uniformity’ here refers to the independence of the bounds from parameters ranging over compact subspaces (in the case of concrete Polish spaces) as well as abstract bounded (not necessarily compact!) metric spaces or bounded convex subsets of hyperbolic, CAT(0), normed, uniformly convex or inner product spaces. By ‘abstract’ spaces we mean that the proofs only use the general axioms for e.g. metric or hyperbolic spaces. If these axioms have a strong uniformity built-in (as in the classes just mentioned), then this property prevails also for theorems proved in strong theories based on these axioms. The metatheorems were derived using a monotone proof interpretation, namely an extension of Gödel’s so-called functional interpretation combined with a novel form of majorizability over function spaces of arbitrary types. The theorems were applied to results in metric fixed point theory to explain the extractability of strong uniform bounds that had been observed previously in several concrete cases ([18, 20, 24]) as well as to predict new such bounds which subsequently could, indeed, be found following the extraction algorithm provided by monotone functional interpretation ([23, 21]).

In the concrete applications it usually turned out that instead of the assumption of the whole space or some convex subset being bounded only some sparse local boundedness conditions were actually needed. This observation was the starting point of the present paper which establishes far reaching extensions of the results from [22] to unbounded spaces which guarantee uniform bounds under exactly such limited local boundedness assumptions. As we will show below, in most applications our new metatheorems completely close the gap which was left between the conclusions predicted by the old metatheorems and the general form of actual bounds constructed in the case studies. In particular, we now for the first time can explain a quantitative version of a well-known theorem of Borwein, Reich and Shafrir [2] on Krasnoselski-Mann iterations of nonexpansive mappings in unbounded hyperbolic spaces, which was found in [24], as an instance of the new metatheorems. The proofs still use a combination of functional interpretation and majorization but this time in a much more subtle way: both the functional interpretation as well as the majorization relation to be applied are parametrized by a point a of the space X in question. In the applications we will be able to achieve by a suitable choice of a (which in turn depends on the parameters of the problem) that the object constructed by the a-functional interpretation can be a-majorized by a term which no longer depends on a (nor the parameters involving the space X). This applies, furthermore, to large classes of mappings between such spaces, as e.g. nonexpansive, weakly quasinonexpansive, Lipschitz-Hölder, uniformly continuous or bounded mappings.

The results in this paper not only allow one to strengthen known existence results in functional analysis by establishing qualitatively new forms of uniform existence as well as new quantitative bounds, but also by weakening of the assumptions needed. E.g. assumptions of the form ‘f has a fixed point’ can for large classes of proofs and theorems be replaced by the much weaker assumption ‘f has approximate fixed points’. Finally, we will indicate how our results extend to contexts where several spaces X_{1}, …, X_{n} from the aforementioned classes of spaces as well as their products are simultanously present. We are confident that these results will have many more applications also outside the context of fixed point theory (see e.g. [25] for a survey of different topics to which this kind of ‘proof mining’ approach can be applied).

2 Definitions

The classes of general spaces we are considering are metric spaces, hyperbolic spaces (including CAT(0)-spaces) as well as normed spaces. Under a hyperbolic space we understand the following:

Definition 2.1. (X, d, W) is called a hyperbolic space if (X, d) is a metric space and W : X × X × [0, 1] → X a function satisfying

(i) ∀x, y, z ∈ X∀λ ∈ [0, 1](d(z, W (x, y, λ)) ≤ (1 − λ)d(z, x) + λd(z, y)),

(ii) ∀x, y ∈ X∀λ_{1}, λ_{2} ∈ [0, 1](d(W (x, y, λ_{1}), W (x, y, λ_{2})) = |λ_{1}−λ_{2}|·d(x, y)),

(iii) ∀x, y ∈ X∀λ ∈ [0, 1](W (x, y, λ) = W (y, x, 1 − λ)),

(iv) \{ \begin{matrix}∀x, y, z, w ∈ X, λ ∈ [0, 1] \\ (d(W (x, z, λ), W (y, w, λ)) ≤ (1 − λ)d(x, y) + λd(z, w)). \end{matrix}

Remark 2.2. As discussed in detail in [22], we obtain Takahashi’s [34] ‘convex metric spaces’ if the axioms (ii)-(iv) are dropped, and a notion which is equivalent to the concept of ‘space of hyperbolic type’ from [11] if we drop only (iv). As observed in [31, 2] and [32], several arguments in metric fixed point theory require a bit more of linear structure which gave rise to a notion of ‘hyperbolic space’^{1} in [14, 31] which adds axiom (iv) (for λ := \frac{1}{2}) and the requirement that any two points not only are connected by a metric segment but by a metric line. As a consequence of this (just as in the case of normed spaces) nontrivial hyperbolic spaces in the sense of [14, 31] always are unbounded and convex subsets of a hyperbolic space in general are no longer hyperbolic spaces themselves. The existence of metric lines allows one to derive the general axiom (iv) from the special case of λ = \frac{1}{2}. It turns out that if we state (iv) directly for general λ as above then the proofs in metric fixed point theory we are interested in (e.g. the main results in [2] and [32]) all go through for our more liberal notion of ‘hyperbolic space’ which not only has a simpler logical structure but also includes all convex subsets of hyperbolic (and in particular normed) spaces as well as all CAT(0)-spaces, whereas the more restricted notion used in [14, 31, 32] only covers CAT(0)-spaces having the geodesic line extension property (see [3] for details on CAT(0)-spaces).

As carried out in detail in [22] we formalize our classes of spaces on top of a formal system A^{ω} of classical analysis which is based on a language of functionals of finite type.

1Unfortunately, Kirk calls this notion in [14] ‘space of hyperbolic type’ although it differs from the definition of the latter in [11].

Definition 2.3. The set T of all finite types is defined inductively over the ground type 0 by the clauses

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

The formal system A^{ω} for analysis (which is based on the axioms of countable and dependent choice which, in particular, yield full comprehension for numbers) is defined as in [22]. Higher type equality is not a primitive predicate but defined extensionally. Instead of the full axiom of extensionality in all types, the system A^{ω} only has a quantifier-free rule of extensionality.^{2}

Before we can describe the extensions A^{ω}[X, d], A^{ω}[X, d, W] etc. of A^{ω} by an abstract metric space (X, d) or hyperbolic space (X, d, W) we briefly have to recall the representation of real numbers in the formal system A^{ω}:

In our formal systems based on A^{ω}, real numbers are represented by Cauchy sequences (a_{n})_{n} of rational numbers with Cauchy modulus 2^{−n}, i.e.

∀m, n(m, n ≥ k → |a_{m} − a_{n}| < 2^{−k}).

Rational numbers are represented as pairs (n, m) of natural numbers coded into a single natural number j(n, m), where j is the Cantor pairing function. If n is even j(n, m) represents the rational number \frac{n/2}{m+1}, if n is odd j(n, m) represents the negative number −\frac{(n+1)/2}{m+1}. Thus every natural number can be conceived as the code of a unique rational number. An equality relation =Q on the representatives of the rational numbers, as well as the usual operators +Q, −Q, ·Q, etc. and the predicates <Q, ≤Q are defined (primitive recursively) in the obvious way. Thus natural and rational numbers are represented by objects of type 0 and sequences of rational numbers by objects of type 1, i.e. by functions of type 0 → 0.

Real numbers are represented by functions f : IN → IN (i.e of type 1) s.t.

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

To ensure that each function f : IN → IN represents a real number we use the following construction:

f̂(n) := \{ \begin{matrix}f(n) if ∀k < n(|f(k) −Q f(k + 1)|Q <Q 2^{−k−1}), \\ f(k) for min k < n with |f(k) −Q f(k + 1)|Q ≥Q 2^{−k−1} otherwise. \end{matrix}

2See [22] for an extensive discussion of this crucial point.

For better readability we will usually write e.g. 2^{−n} instead of its (canonical) code ⟨2^{−n}⟩ := j(2, 2^{n} − 1). For every f : IN → IN the construction f̂, which can be carried out in A^{ω}, satisfies (∗), and if already f satisfies (∗) then ∀n(f(n) =_{0} f̂(n)). Thus every f codes a unique real number, namely the one given by the Cauchy sequence coded by f̂. The construction f ↦ f̂enables us to reduce quantifiers ranging over IR to ∀f^{1}, resp. ∃f^{1}, without introducing additional quantifiers. For natural numbers b ∈ IN we have the embedding (b)_{IR} via the constructing (b)_{IR} =_{1} λn.j(2b, 0).

The equivalence relation =_{IR} and the relations ≤_{IR} and <_{IR} on (representatives of) real numbers are defined notions. The relations =_{IR} and ≤_{IR} are given by Π_{1}^{0}-predicates while <_{IR} is given by a Σ_{1}^{0}-predicate:

f_{1} =_{IR} f_{2} :≡ ∀n(|f̂_{1}(n + 1) −Q f̂_{2}(n + 1)| <Q 2^{−n})
f_{1} <_{IR} f_{2} :≡ ∃n(f̂_{2}(n + 1) −Q f̂_{1}(n + 1) ≥Q 2^{−n})
f_{1} ≤_{IR} f_{2} :≡ ¬(f_{2} <_{IR} f_{1})

The operators +_{IR}, −_{IR}, ·_{IR},etc. on representatives of real numbers can be defined by simple primitive recursive functionals. For further details see [22].

For the interval [0, 1], which plays an important role in the formal treatment of hyperbolic spaces, we use a special representation by number theoretic functions IN → IN(which are bounded by a fixed function M):

Definition 2.4.

x̃(n) := j(2k_{0}, 2^{n+2} − 1), where k_{0} = max k ≤ 2^{n+2}[\frac{k}{2^{n+2}} ≤Q x̂(n + 2)].

One easily verifies the following:

Lemma 2.5. Provably in A^{ω}, for all x^{1}:

1. 0_{IR} ≤_{IR} x ≤_{IR} 1_{IR} → x̃ =_{IR} x,

2. 0_{IR} ≤_{IR} x̃ ≤_{IR} 1_{IR},

3. x̃ ≤_{1} M := λn.j(2^{n+3}, 2^{n+2} − 1),

4. x >_{IR} 1_{IR} → x̃ =_{IR} 1_{IR}, x <_{IR} 0_{IR} → x̃ =_{IR} 0_{IR}.

The theories of classical analysis extended with metric or normed linear spaces and their variants are defined almost as in [22]. The crucial difference is that while in [22] only bounded metric spaces (X, d) and bounded convex subsets C of normed linear spaces (X, ∥ · ∥) are considered, we now permit unbounded metric spaces (X, d) and unbounded convex subsets C. In [22], the boundedness is expressed by an axiom stating explicitly that (X, d), resp. the convex subsets C, are bounded by b. In our unbounded variants we omit this axiom. To distinguish the not-b-bounded theories from the b-bounded theories A^{ω}[X, d] and A^{ω}[X, ∥ · ∥, C] defined in [22], we will denote them by A^{ω}[X, d]_{−b} and A^{ω}[X, ∥ · ∥, C]_{−b}. We also consider theories A^{ω}[X, d, W]_{−b} capturing hyperbolic spaces and A^{ω}[X, d, W, CAT(0)]_{−b} capturing CAT(0)- spaces. More precisely, the theories A^{ω}[X, d]_{−b}, A^{ω}[X, d, W]_{−b} and A^{ω}[X, d, W, CAT(0)]_{−b} result by

(i) extending A^{ω} to the set T^{X} of all finite types over the two ground types 0 and X, i.e.

(i) 0, X ∈ T^{X}, (ii) ρ, τ ∈ T^{X} ⇒ (ρ → τ) ∈ T^{X}

(in particular, the constants Π_{ρ,τ}, Σ_{δ,ρ,τ}, R_{ρ} for λ-abstraction and primitive recursion (in the extended sense of Gödel [10]) and their defining axioms and the schemes IA (induction), QF-AC (quantifier-free choice in all types), DC (dependent countable choice) and the weak extensionality rule QF-ER are now taken over the extended language),

(ii) adding a constant 0_{X} of type X,

(iii) adding a new constant d_{X} of type X → X → 1 (representing the metric) together with the axioms

(1) ∀x^{X}(d_{X}(x, x) =_{IR} 0_{IR}),

(2) ∀x^{X}, y^{X}(d_{X}(x, y) =_{IR} d_{X}(y, x)),

(3) ∀x^{X}, y^{X}, z^{X}(d_{X}(x, z) ≤_{IR} d_{X}(x, y) +_{IR} d_{X}(y, z)).

In these axioms we refer to the representation of real numbers (including the definition of =_{IR}, ≤_{IR}) as sketched above.

Equality =_{0} at type 0 is the only a primitive equality predicate. x^{X} =_{X} y^{X} is defined as d_{X}(x, y) =_{IR} 0_{IR}. Equality for complex types is defined as before as extensional equality using =_{0} and =_{X} for the base cases.

A^{ω}[X, d, W]_{−b} results from A^{ω}[X, d]_{−b} by adding a new constant W_{X} of type X → X → 1 → X together with the axioms (where λ̃ is defined as above)

(4) ∀x^{X}, y^{X}, z^{X}∀λ^{1}(d_{X}(z, W_{X}(x, y, λ)) ≤_{IR} (1_{IR}−_{IR}λ̃)d_{X}(z, x)+_{IR}λ̃d_{X}(z, y)),

(5) ∀x^{X}, y^{X}∀λ_{1}^{1}, λ_{2}^{1}(d_{X}(W_{X}(x, y, λ_{1}), W_{X}(x, y, λ_{2})) =_{IR} |λ̃_{1}−_{IR}λ̃_{2}|_{IR}·_{IR}d_{X}(x, y)),

(6) ∀x^{X}, y^{X}∀λ^{1}(W_{X}(x, y, λ) =_{X} W_{X}(y, x, (1_{IR} −_{IR} λ))),

(7) \{ \begin{matrix}∀x^{X}, y^{X}, z^{X}, w^{X}, λ^{1} \\ (d_{X}(W_{X}(x, z, λ), W_{X}(y, w, λ)) ≤_{IR} (1_{IR} −_{IR} λ̃)d_{X}(x, y) +_{IR} λ̃d_{X}(z, w)). \end{matrix}

A^{ω}[X, d, W, CAT(0)]_{−b} results from A^{ω}[X, d, W]_{−b} by adding as further axiom the formalized form of the Bruhat-Tits or CN^{−}-inequality[4], i.e.

\begin{matrix}∀x^{X}, y_{1}^{X}, y_{2}^{X}(d_{X}(x, W_{X}(y_{1}, y_{2}, \frac{1}{2}))^{2} \\ ≤_{IR} \frac{1}{2}d_{X}(x, y_{1})^{2} +_{IR} \frac{1}{2}d_{X}(x, y_{2})^{2} −_{IR} \frac{1}{4}d_{X}(y_{1}, y_{2})^{2}). \end{matrix}

Remark 2.6. 1. The additional axioms of A^{ω}[X, d]_{−b} express (modulo our representation of IR sketched above) that d_{X} represents a pseudometric d (on the universe the type-X variables are ranging over).^{3} Hence d_{X} represents a metric on the set of equivalence classes generated by =_{X}. We do not form these equivalence classes explicitly but talk instead only about representatives x^{X}, y^{X}. However, it is important to stress that a functional f^{X→X} represents a function X → X only if it respects this equivalence relation, i.e.

∀x^{X}, y^{X}(x =_{X} y → f(x) =_{X} f(y)).

Due to our weak (quantifier-free) rule of extensionality we in general only can infer from a proof of s =_{X} t that f(s) =_{X} f(t). The restriction on the availability of extensionality is crucial for our results to hold (see the discussion in [22]). However, the extensionality of the constants d_{X}, W_{X} as well as the constants for normed linear spaces can all be proved to be fully extensional from their defining axioms. Likewise, for most (but not all) of the classes of functions which we will consider below (notably nonexpansive functions) the full extensionlity will follow from their defining conditions.

3Note that (1) − (3) imply that ∀x^{X}, y^{X}(d_{X}(x, y) ≥_{IR} 0_{IR}).

2. Our axiomatization of W_{X} given by the axioms (4)-(7) differs slightly from the one given in [22]. Our present axiomatization is equivalent to the extension of the one given in [22] by the additional axiom

W_{X}(x, y, λ) =_{X} W_{X}(x, y, λ̃)

using the property

{ \atop 1 −_{IR} λ} =_{IR} 1 −_{IR} λ̃

of our operation λ ↦ λ̃ (which follows using lemma 2.5.4). This additional axiom is trivially satisfied by the interpretation of W_{X} in the model S^{ω,X} from [22] so that it can be added without causing problems. The benefit of this is that then the axioms on W_{X} can be stated in the simple form given above compared to the more complicated formulation in [22]. The intuitive interpretation of W_{X} in a hyperbolic spaces (X, d, W) is that for x, y ∈ X we interpret W_{X}(x, y, λ) by W (x, y, rλ̃) where rλ̃ is the unique real number in [0, 1] that is represented by λ̃.

3. Our additional axiom CN^{−} used in defining A^{ω}[X, d, W, CAT(0)] differs from the one used in [22] (under the name CN^{∗}) but is in fact equivalent to the latter: CN^{−} is (over the W -axioms (i)-(iv)) equivalent to the more usual formulation CN of the Bruhat-Tits inequality[4] which states that every midpoint of y_{1}, y_{2} satisfies the inequality stated for W (y_{1}, y_{2}, \frac{1}{2}). The latter point provably (in A^{ω}[X, d, W]) is a midpoint so that CN implies CN^{−}. From CN^{−} is easily follows not only that every midpoint of y_{1}, y_{2} has to coincide with W (y_{1}, y_{2}, \frac{1}{2}) (so that CN follows) but even the quantitative version CN^{∗} of CN. In [22], CN^{∗} was used as axiom as it is (in contrast to CN) purely universal which is crucially used in the proofs). However, CN^{−} is purely universal too and equivalent to CN^{∗}. Since it easier to state we use this formulation here.

As for A^{ω}[X, ∥ · ∥, C]_{−b}, the corresponding theories for uniformly convex spaces, A^{ω}[X, ∥·∥, C, η]_{−b}, and real inner product spaces, A^{ω}[X, ∥·∥, C, ⟨·, ·⟩]_{−b}, are defined as in [22] except that the axioms stating the boundedness of C is dropped.

Finally, various moduli naturally occurring in analysis, such as e.g. a modulus of uniform continuity or a modulus of uniform convexity, are also represented by number theoretic functions IN → IN, i.e. objects of type 1. Thus e.g. the statement f : X → X is uniformly continuous with modulus ω : IR → IR:

∀x, y ∈ X∀ε > 0(d(x, y) ≤ ω(ε) → d(f(x), f(y)) ≤ ε)

is translated into

∀x, y ∈ X∀k ∈ IN(d(x, y) < 2^{−ω(k)} → d(f(x), f(y)) ≤ 2^{−k})

where ω : IN → IN and the translated statement is purely universal.

3 A generalized approach to majorization

In [22] the strong majorization relation, first introduced by Bezem[1] for the finite types T over IN, is extended to the types T^{X} with the new ground type X for metric spaces (X, d) and normed linear spaces (X, ∥ · ∥). Furthermore, a mapping ρ̂ between types ρ ∈ T^{X} and ρ̂ ∈ T, and a relation ∼_{ρ} between functionals of type ρ ∈ T^{X} and ρ̂ ∈T are defined inductively. By relating the constants of the theories A^{ω}[X, d] and A^{ω}[X, ∥ · ∥] (and their variants) to suitable functionals in A^{ω} via the relation ∼_{ρ} one can, combined with majorization in the types T^{X}, systematically eliminate the dependency on the type X in the extracted terms and obtain bounds independent of parameters ranging over bounded metric spaces, resp. bounded convex subsets of normed linear spaces.

In this section we present a generalized approach to extending the strong majorization relation to the types T^{X}. The (strong) majorization relation was defined by Howard and Bezem:

Definition 3.1 (Howard-Bezem, [12, 1]). The strong majorization relation s-maj over the finite types T is defined as follows:

• x^{∗} s-maj_{0} x :≡ x^{∗} ≥_{IN} x, where ≥_{IN} is the usual (primitive recursive) order on IN,

• x^{∗} s-maj_{ρ→τ} x :≡ ∀y^{∗}, y(y^{∗} s-maj_{ρ} y → x^{∗}y^{∗} s-maj_{τ} x^{∗}y, xy).

In [22], two different approaches are employed for metric and normed linear spaces respectively to extend the majorization relation to the new type X. For metric spaces only the restricted case of b-bounded spaces is treated, where b is an integer upper bound on the metric of the space. For bounded metric spaces the relation s-maj is extended to the types T^{X} by defining:

x^{∗} s-maj_{X} x :≡ (0 = 0), i.e. always true.

Usually extending majorization to a new type X imposes a kind of order on the elements of X which the majorization of the constants 0_{X}, d_{X} and W_{X} must respect. Since here the metric d_{X} can be bounded independently of the elements x, y ∈ X to which it is applied, namely by λx^{X}, y^{X}.(b)_{IR}, and since the function W_{X} merely produces new elements of X, in [22] the majorization relation on X could be defined to be always true (corresponding to a trivial order on X).

For normed linear spaces this approach does not work as non-trivial normed linear spaces always are unbounded. Instead in [22] the extension of the majorization relation to the new type X for normed linear spaces (X, ∥ · ∥) is defined via the norm:

x^{∗} s-maj_{X} x :≡ ∥x^{∗}∥_{X} ≥_{IR} ∥x∥_{X}.

The majorization of extracted terms in [22] then consists of three steps: First one majorizes the extracted terms in T^{X} – these majorants may still depend on the constants of A^{ω}[X, ∥ · ∥]. Next one eliminates the dependency on X using the relation ∼_{ρ} and an ineffective operator (·)_{∘} (to be defined below). Finally, the resulting terms are majorized once more in the types T to eliminate uses of the ineffective (·)_{∘}-operator.

As mentioned above, using these techniques it is possible to derive the independence of extracted bounds from parameters ranging over bounded metric spaces, resp. norm-bounded convex subsets C of normed linear spaces. The generalized approach to majorization we describe in this section aims to treat the more general cases of unbounded metric and hyperbolic spaces and normed linear spaces with unbounded convex subsets C, i.e. the theories A^{ω}[X, d]_{−b}, A^{ω}[X, d, W]_{−b} and A^{ω}[X, ∥ · ∥, C]_{−b}, and to derive similar uniformities under certain local boundedness conditions to be discussed in detail later. This generalized approach is based upon the first two steps of the previous treatment of normed linear spaces: (strong) majorization in the types T^{X} and the relation ∼_{ρ}. In [22], in the mapping ˆ · the type X with (X, d) a metric space was mapped to the type 0, while the type X with (X, ∥ · ∥) a normed linear space was mapped to the type 1. In this paper, we will map the type X to 0 in both cases:

Definition 3.2. For ρ ∈ T^{X} we define ρ̂ ∈ T inductively as follows

ˆ0 := 0, X̂ := 0, { \atop (ρ → τ)} := (ρ̂ → τ̂),

i.e. ρ̂ is the result of replacing all occurrences of the type X in ρ by the type 0.

The generalized approach to majorization will again involve the ()_{∘}-operator, but restricted to cases where the circle operator is effectively computable. Hence, the second application of strong majorization, used in the previous treatment of normed linear spaces to get rid of ineffective instances of the ()_{∘}-operator, is no longer necessary.

Combining Bezem’s notion of strong majorization s-maj and the idea of the relation ∼_{ρ} we define a family of (majorization) relations ≳_{ρ}^{a} between objects of type ρ ∈ T^{X} and their majorants of type ρ̂ ∈ T. The relation is parametrized by an element a ∈ X, where X is the underlying metric or normed linear space and a ∈ X serves as a reference point for comparing and majorizing elements of X. In L(A[X, d])_{−b}, resp. L(A[X, ∥ · ∥]), this is syntactically expressed as follows:

Definition 3.3. We define a ternary relation ≳_{ρ}^{a} between objects x, y and a of type ρ̂, ρ and X respectively by induction on ρ as follows:

• x^{0} ≳_{0}^{a} y^{0} :≡ x ≥_{IN} y,

• x^{0} ≳_{X}^{a} y^{X} :≡ (x)_{IR} ≥_{IR} d_{X}(y, a),

• x ≳_{ρ→τ}^{a} y :≡ ∀z′, z(z′ ≳_{ρ}^{a} z → xz′ ≳_{τ}^{a} yz) ∧ ∀z′, z(z′ ≳a ; ρ̂ z → xz′ ≳a ; τ̂

xz).

For normed linear spaces we choose a = 0_{X} ^{4}, so that d_{X}(x, a) =_{IR} ∥x∥_{X}.

4While it will turn out to be independent of the choice of a whether a given functional is a-majorizable or not, the choice of a is crucial to obtain “nice” majorants. See Section 9 for a detailed discussion.

As ≳^{a} is a relation between objects of different types, the definition of ≳_{ρ→τ}^{a} is slightly more complicated than the corresponding definition of s-maj_{ρ→τ}. The first part of the clause ensures that x is a “majorant” for y, the second part ensures that a majorant x also majorizes itself. Since majorants are of type ρ̂ ∈ T (where ≳a ; ρ̂ coincides with s-majρ̂), this corresponds to requiring that for all majorants x s-maj x, and so the definition of ≳_{ρ→τ}^{a} could equivalently be rewritten as:

x ≳_{ρ→τ}^{a} y :≡ ∀z′, z(z′ ≳_{ρ}^{a} z → xz′ ≳_{τ}^{a} yz) ∧ x s-maj_{ρ̂→τ̂} x.

Remark 3.4. Restricted to the types T the relation ≳^{a} is identical with the Howard-Bezem notion of strong majorizability s-maj and hence for ρ ∈ T we may freely write s-maj_{ρ} instead of ≳_{ρ}^{a}, as here the parameter a ∈ X is irrelevant. Without the requirement that “majorants” must be strongly self-majorizing, ≳^{a} restricted to T is identical with Howard’s notion of majorizability maj.

In the following, we call majorization in the sense of the relation ≳^{a} (strong) “a-majorization”, i.e. if t_{1} ≳^{a} t_{2} for terms t_{1}, t_{2} we say that t_{1} a-majorizes t_{2} and we call t_{1} an a-majorant. If neither term t_{i} depends on a we say that t_{1} uniformly a-majorizes t_{2}. We will in general aim at uniform majorants so that we can choose a appropriately (without having an effect on the majorants of the constants of our theories) to obtain bounds with the intended uniformity features.

For the normed case we also need a pointwise ≥_{ρ} relation between functionals of type ρ :

Definition 3.5. ≥_{ρ} is a binary relation between functionals of of type ρ and which is defined by induction on ρ as follows:

• x^{0} ≥_{0} y^{0} :≡ x ≥_{IN} y,

• x^{X} ≥_{X} y^{X} :≡ ∥x∥_{X} ≥_{IR} ∥y∥_{X},

• x ≥_{ρ→τ} y :≡ ∀z^{ρ}(xz ≥_{τ} yz).

The only nontrivial relation between ≳_{ρ}^{0_{X}} and ≥_{ρ} which holds in all types is the following one:

Lemma 3.6. For all x^{∗}, x, y of type ρ̂, ρ, ρ resp. the following holds (provably in A^{ω}[X, ∥ · ∥]):

x^{∗} ≳_{ρ}^{0_{X}} x ∧ x ≥_{ρ} y → x^{∗} ≳_{ρ}^{0_{X}} y.

Proof. Easy induction on ρ. □

4 Metatheorems for metric and hyperbolic spaces

Before we state the new metatheorems, we recall and add the following definitions:

Definition 4.1 ([22]). We say that a type ρ ∈ T^{X} has degree

• 1 if ρ = 0 → … → 0 (including ρ = 0),

• (0, X) if ρ = 0 → … → 0 → X (including ρ = X),

• (1, X) if it has the form τ_{1} → … → τ_{k} → X (including ρ = X), where τ_{i} has degree 1 or (0, X).

Definition 4.2. We say that a type ρ ∈ T^{X} has degree 1, if ρ̂ has degree 1. Amongst others, the type degree 1 covers types IN, X, IN → IN, IN → X, X → IN and X → X.

Definition 4.3. A formula F is called a ∀-formula (resp. ∃-formula) if it has the form F ≡ ∀\underline{a}\underline{σ}F_{qf}(\underline{a}) (resp. F ≡ ∃\underline{a}\underline{σ}F_{qf}(\underline{a})) where F_{qf} does not contain any quantifiers and the types in \underline{σ} are of degree 1 or (1, X).

The ()_{∘}-operator is defined as follows:

Definition 4.4 ([22]). For x ∈ [0, ∞) define (x)_{∘} ∈ IN^{IN} by

(x)_{∘}(n) := j(2k_{0}, 2^{n+1} − 1),

where

k_{0} := max k[\frac{k}{2^{n+1}} ≤ x].

Remark 4.5. ()_{∘} is a ‘semantic’ operator defined on the real numbers themselves (rather than representatives of real numbers). However, it has a counterpart ∘ : IN^{IN} → IN^{IN} defined as (f^{1})_{∘} = (|r|)_{∘}, where r is the real number represented by f, i.e. (f^{1})_{∘} ∈ IN^{IN} is defined by

(f)_{∘}(n) := j(2k_{0}, 2^{n+1} − 1),

where

k_{0} := max k[\frac{k}{2^{n+1}} ≤_{IR} |f|_{IR}].

In contrast to f̃^{1} defined before, this functional of type 1 → 1 is not computable, but in our bounds it will only be used in the form λn^{0}.((n)_{IR})_{∘} which is (even primitive recursively) computable. It will be clear from the context whether we refer to ∘ defined on [0, ∞) or on IN^{IN}.

We will use the following properties of the ()_{∘}-operator:

Lemma 4.6 ([22]). 1. If x ∈ [0, ∞), then (x)_{∘} is a representative of x in the sense of the representation of real numbers described in Section 2.

2. If x, y ∈ [0, ∞) and x ≤ y (in the sense of IR), then (x)_{∘} ≤_{IR} (y)_{∘} and also (x)_{∘} ≤_{1} (y)_{∘} (i.e. ∀n ∈ IN((x)_{∘}(n) ≤ (y)_{∘}(n))).

3. If x ∈ [0, ∞), then (x)_{∘} is monotone, i.e. ∀n ∈ IN((x)_{∘}(n) ≤_{0} (x)_{∘}(n + 1)).

4. If x, y ∈ [0, ∞) and x ≤ y (in the sense of IR), then (y)_{∘} s-maj_{1}(x)_{∘}

Proof. 1.-3. are part of Lemma 2.10 in [22]. 4. follows from 2. and 3.

Definition 4.7. Let X be a nonempty set. The full set-theoretic type structure S^{ω,X} := ⟨S_{ρ}⟩_{ρ∈T^{X}} over IN and X is defined by

S_{0} := IN, S_{X} := X, S_{ρ→τ} := S_{τ}^{S_{ρ}}.

Here S_{τ}^{S_{ρ}} is the set of all set-theoretic functions S_{ρ} → S_{τ}.

Using this and the ()_{∘}-operator we state the following definition:

Definition 4.8. We say that a sentence of L(A^{ω}[X, d, W]_{−b}) holds in a nonempty hyperbolic space (X, d, W) if it holds in the models^{5} of A^{ω}[X, d, W]_{−b} obtained by letting the variables range over the appropriate universes of the full set-theoretic type structure S^{ω,X} with the set X as the universe for the base type X, 0_{X} is interpreted by an arbitrary element of X, W_{X}(x, y, λ^{1}) is interpreted as W (x, y, rλ̃), where rλ̃ ∈ [0, 1] is the unique real number represented by λ̃^{1} and d_{X} is interpreted as d_{X}(x, y) :=_{1} (d(x, y))_{∘}.

Finally, we define the following functional, which is particularly useful for defining majorants for functionals of degree 1.

Definition 4.9 ([22]). For types 0 → ρ with ρ = ρ_{1} → … → ρ_{k} → 0, we define functionals (·)^{M} of types (0 → ρ) → 0 → ρ by :

x^{M}(y^{0}) := λ\underline{v}\underline{ρ}. max_{0}\{x(i, \underline{v}) | i = 1, …, y\}.

We now state the main version of our metatheorem for unbounded metric, hyperbolic and CAT(0)-spaces:

Theorem 4.10. 1. Let ρ be of degree (1, X) or 2 and let B_{∀}(x, u), resp. C_{∃}(x, v), contain only x, u free, resp. x, v free. Assume that the constant 0_{X} does not occur in B_{∀}, C_{∃} and that

A^{ω}[X, d]_{−b} ⊢ ∀x^{ρ}(∀u^{0}B_{∀}(x, u) → ∃v^{0}C_{∃}(x, v)).

Then there exists a partial computable functional^{6} Φ : Sρ̂ ⇀ IN s.t. Φ is defined on all strongly majorizable elements of Sρ̂ and the following holds in all nonempty metric spaces (X, d): for all x ∈ S_{ρ}, x^{∗} ∈ Sρ̂ if there exists an a ∈ X s.t. x^{∗} ≳^{a} x then^{7}

∀u ≤ Φ(x^{∗})B_{∀}(x, u) → ∃v ≤ Φ(x^{∗})C_{∃}(x, v).

In particular, if ρ is in addition of degree 1, then Φ : Sρ̂ × IN → IN is totally computable. If 0_{x} does occur in B_{∀} and/or C_{∃}, then the bound Φ depends (in addition to x^{∗}) on an upper bound IN ∋ n ≥ d(0_{X}, a).

5We use here the plural since the interpretation of 0_{X} is not uniquely determined.

6More precisely, Φ is given by a bar recursive term (in the sense of [33]) which defines a total functional in M_{ρ̂→0} where M^{ω} := ⟨M_{ρ}⟩ is the type structure of all strongly majorizable functionals [1]. Note that Mρ̂ ⊆ Sρ̂.

7Note that x^{∗} ≳^{a} x implies that x^{∗} s-majρ̂ x^{∗} and hence the strong majorizability of x^{∗} so that Φ(x^{∗}) is defined.

2. The theorem also holds for nonempty hyperbolic spaces A^{ω}[X, d, W]_{−b}, (X, d, W) and for A^{ω}[X, d, W, CAT(0)]_{−b} where (X, d, W) is a CAT(0) space.

Instead of single variables x, u, v and single premises ∀uB_{∀}(x, u) we may have tuples of variables and finite conjunctions of premises. In the case of a tuple \underline{x} we then have to require that we have a tuple \underline{x}^{∗} of a-majorants for a common a ∈ X for all the components of the tuple \underline{x}.

Remark 4.11. Another way to treat parameters x^{ρ}, ρ of degree (1, X) or 2 is to require for a majorant a computable functional t in S\underline{σ} → Sρ̂,^{8} where all σ_{i} are of degree 1. Then we may obtain a totally computable Φ : S\underline{σ} → IN such that given \underline{c} ∈ S\underline{σ}, if there exists an a ∈ X for which t(\underline{c}) ≳_{ρ}^{a} x then the bound Φ(\underline{c}) holds.

The restriction on the types of degree (1, X) or 2 is made necessary by the interpretation of dependent choice using bar recursive functionals. If a given proof does not use dependent choice, we can allow arbitrary types ρ in the parameters (with majorants of type ρ̂).

Remark 4.12. From the proof of Theorem 4.10 (to be given in section 9 below) two further extensions follow:

1. The language may be extended by a-majorizable constants (in particular constants of types 0 and 1, which always are uniformly majorizable) where the extracted bounds then additionally depend on (a-majorants for) the new constants.

2. The theory may be extended by purely universal axioms or, alternatively, axioms which can be reformulated into purely universal axioms using new majorizable constants if the types of the quantifiers are all of degree 2 or (1, X),^{9} as purely universal axioms are their own functional interpretation. Again the extracted bounds depend on (a-majorants for) these new constants. Then the conclusion holds in all metric (X, d) resp. hyperbolic (X, d, W) spaces which satisfy these axioms (under a suitable interpretation of the new constants if any).

8Since t is of degree 2, the computability of t implies its (strong) majorizability.

9This ensures that validity in S^{ω,X} implies validity in M^{ω,X} defined further below.

Remark 4.13. The need for the restriction to ∃-formulas C_{∃} in theorem 4.10 is a consequence of the fact that our theories are based on classical logic, where one can produce counterexamples already for formulas ∃v^{0}∀w^{0}C_{qf}(v, w) with C_{qf} quantifier-free. If one bases the system on intuitionistic logic instead this can (even in the presence of many ineffective principles) be avoided and effective bounds for formulas C of arbitrary complexity can be extracted (though no longer bounds on universal premises ∀u^{0}B_{∀}). See [9] for this.

As a corollary to the proof of Theorem 4.10 we obtain Theorem 3.7 in [22]:

Corollary 4.14. 1. Let σ, ρ be types of degree 1 and τ be a type of degree (1, X). Let s^{σ→ρ} be a closed term of A^{ω}[X, d] and let B_{∀}(x, y, z, u), resp. C_{∃}(x, y, z, v), contain only x, y, z, u free, resp. x, y, z, v free. If

∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(∀u^{0}B_{∀}(x, y, z, u) → ∃v^{0}C_{∃}(x, y, z, v))

is provable in A^{ω}[X, d], then one can extract a computable functional Φ : S_{σ} × IN → IN such that for all x ∈ S_{σ} and all b ∈ IN

∀y ≤_{ρ} s(x)∀z^{τ}[∀u ≤ Φ(x, b) B_{∀}(x, y, z, u) → ∃v ≤ Φ(x, b) C_{∃}(x, y, z, v)]

holds in any nonempty metric space (X, d) whose metric is bounded by b ∈ IN.

2. If the premise is proved in ‘A^{ω}[X, d, W]’, instead of ‘A^{ω}[X, d]’, then the conclusion holds in all b-bounded hyperbolic spaces.

3. If the premise is proved in ‘A^{ω}[X, d, W, CAT(0)]’, instead of ‘A^{ω}[X, d, W]’, then the conclusion holds in all b-bounded CAT(0)-spaces.

Instead of single variables x, y, z, u, v we may also have finite tuples of variables \underline{x}, \underline{y}, \underline{z}, \underline{u}, \underline{v} as long as the elements of the respective tuples satisfy the same type restrictions as x, y, z, u, v. Moreover, instead of a single premise of the form ‘∀u^{0}B_{∀}(x, y, z, u)’ we may have a finite conjunction of such premises.

Proof. Take a = 0_{X}. For x, which has type σ of degree 1, we easily see (even using only strong majorization s-maj) that x^{M} ≳^{0_{X}} x. Next, for the 0_{X}-majorant s^{∗} ≳^{0_{X}} s, which we can construct by induction on the structure of s as a closed term of A^{ω} (see Lemma 9.10 in Section 9), we have that s^{∗}(x^{M}) ≳_{1}^{0_{X}} y for all y ≤_{1} s(x). Given a bound b ∈ IN on the metric, let τ = τ_{1} → … → τ_{k} → X, then also λ\underline{x}τ̂_{i}.b ≳_{τ}^{0_{X}} z. Likewise, independent of the choice of a we have that the distance d(0_{X}, a) ≤ b, but for a = 0_{X} even d(0_{X}, a) = 0.

Then by Theorem 4.10 we can extract a (bar recursive) functional ϕ such that ϕ((x)^{M}, s^{∗}(x^{M}), λ\underline{x}τ̂_{i}.b, 0) is a bound on ∃v, resp. ∀u, for any b-bounded metric space. Since both the functional (·)^{M}, the 0_{X}-majorant s^{∗} for s and the 0_{X}-majorant λ\underline{x}τ̂_{i}.b for z are given by closed terms of A^{ω} (and hence primitive recursive in the sense of [10]), the functional

Φ :≡ λx, b.ϕ(x^{M}, s^{∗}(x^{M}), λ\underline{x}τ̂_{i}.b, 0)

is computable and yields the desired bound.

Note, that in A^{ω}[X, d] we have the boundedness of (X, d) as an axiom, while Theorem 4.10 only allows one to treat the boundedness of (X, d) as an implicative assumption. Since (due to the restrictions on our weak extensionality rule) our systems do not satisfy the deduction theorem^{10}, strictly speaking this corollary does not follow from Theorem 4.10, but rather from the proof of Theorem 4.10: As mentioned in Remark 4.12, we may freely add another purely universal axiom, i.e. the axiom that (X, d) is a b-bounded metric space, to the theory A^{ω}[X, d]_{−b}.

Similarly, one can derive Corollary 3.11 from [22], but we will state a generalized version of Corollary 3.11 from [22] below. For most applications to be discussed in this paper the following more concrete version of the metatheorem is sufficient:

Corollary 4.15. Let P (resp. K) be a A^{ω}-definable Polish space^{11} (resp. compact Polish space), let τ be of degree 1 and let B_{∀}, resp. C_{∃}, contain only x, y, z, u free, resp. x, y, z, v free, where furthermore 0_{X} does not occur in B_{∀}, C_{∃}. If

A^{ω}[X, d, W]_{−b} ⊢ ∀x ∈ P ∀y ∈ K∀z^{τ}(∀u^{0}B_{∀} → ∃v^{0}C_{∃}),

10See [22] for an extensive discussion of this point.

11For details on this see [22] and [16].

then there exists a computable functional Φ : IN^{IN} × IN^{(IN×...×IN)} → IN s.t. the following holds in every nonempty hyperbolic space (X, d, W): for all representatives r_{x} ∈ IN^{IN} of x ∈ P and all z^{∗} ∈ IN^{(IN×...×IN)} if there exists an a ∈ X for which z^{∗} ≳_{τ}^{a} z then

∀y ∈ K(∀u ≤ Φ(r_{x}, z^{∗})B_{∀} → ∃v ≤ Φ(r_{x}, z^{∗})C_{∃}).

As before, instead of single variables x, y, z and a single premise ∀u^{0}B_{∀}, we may have tuples of variables and a finite conjunction of premises. Analogously, for A^{ω}[X, d]_{−b} or A^{ω}[X, d, W, CAT(0)]_{−b} where then (X, d) resp. (X, d, W) is an arbitrary nonempty metric resp. CAT(0)-space.

Proof. Using the representation of P and K in A^{ω}, quantification over x ∈ P and y ∈ K can be expressed as quantification over all x^{1}, resp. all y^{1} ≤ s for some closed function term s. Then, for (type 1-)representatives r_{x} of elements x we have (r_{x})^{M} ≳^{a} r_{x}, while from s and x we obtain an a-majorant s^{∗}(x^{M}) for all y ≤ s(x). Finally, τ has degree 1, so by Theorem 4.10 we obtain a totally computable bound Φ(r_{x}, z^{∗}).

Definition 4.16. A function f : X → X on a metric space (X, d) is called

• nonexpansive (‘f n.e.’) if d(f(x), f(y)) ≤ d(x, y) for all x, y ∈ X,

• quasi-nonexpansive if ∀p, x ∈ X(d(p, f(p)) = 0 → d(f(x), f(p)) ≤ d(x, p)),

• weakly quasi-nonexpansive if ∃p ∈ X(d(p, f(p)) = 0∧∀x ∈ X(d(f(x), f(p)) ≤ d(x, p))) or – equivalently –

∃p ∈ X∀x ∈ X(d(f(x), p) ≤ d(x, p)).

• Lipschitz continuous if d(f(x), f(y)) ≤ L · d(x, y) for some L > 0 and for all x, y ∈ X,

• Hölder-Lipschitz continuous if d(f(x), f(y)) ≤ L · d(x, y)^{α} for some L > 0, 0 < α ≤ 1 and for all x, y ∈ X.

For normed linear spaces (X, ∥·∥) those definitions are to be understood w.r.t. the induced metric d(x, y) := ∥x − y∥.

The notion of quasi-nonexpansivity was introduced by Dotson in [6], the notion of weak quasi-nonexpansivity is (implicitly) due to B. Lambov and the second author[23] (note that in context where quasi-nonexpansive mappings are used it always is assumed that fixed points exists so that ‘weakly quasinonexpansive’ is indeed weaker than ‘quasi-nonexpansive’).^{12} Using that ≤_{IR} and =_{IR} are Π_{1}^{0}-statements, we observe that the above statements, except for ‘f quasi-nonexpansive’ and ‘f weakly quasi-nonexpansive’, can – when formalized in L(A^{ω}[X, d, W]) – be written as ∀-formulas, where in the case of Lipschitz and Hölder-Lipschitz the constants L, resp. L and α are assumed to be given as parameters. For ‘f weakly quasi-nonexpansive’, if we take the fixed point p as a parameter, the remaining formula can be written as a ∀-formula, so that to use ‘f weakly quasi-nonexpansive’ as a premise one needs to quantify over the additional parameter p. The statement ‘f quasi-nonexpansive’ is of the form ∀ → ∀ and hence not of a suitable form to serve as a premise, if we want to apply our metatheorems. Most theorems involving quasi-nonexpansive functions easily extend to the ‘weakly quasinonexpansive’ functions which makes our metatheorems applicable. For examples of this see [23].

As examples of weakly quasi-nonexpansive functions (communicated by L. Leustean) consider in the setting of normed linear spaces (with a convex subset C) the class of functions satisfying ∥f(x)∥ ≤ ∥x∥, which are weakly quasi-nonexpansive in the fixed point 0_{X}. To see that such functions need not by quasi-nonexpansive consider f : [0, 1] → [0, 1] (on the convex subset [0, 1] of IR) defined by f(x) := x^{2}, which has fixed points 0, 1, but only is weakly quasi-nonexpansive in 0.

For unbounded hyperbolic spaces (X, d, W) we now state the following corollary:

Corollary 4.17. 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space). Assume we can prove in A^{ω}[X, d, W]_{−b} the following sentence:

\begin{matrix}∀x ∈ P ∀y ∈ K∀z^{X}∀f^{X→X} \\ (f n.e. ∧ ∀u^{0}B_{∀}(x, y, z, f, u) → ∃v^{0}C_{∃}(x, y, z, f, v)), \end{matrix}

12The concept of weakly quasi-nonexpansive mapping has recently been formulated independently – under the name of J-type mapping – in [8] where the fixed point p is called a ‘center’.

where 0_{X} does not occur in B_{∀} and C_{∃}. Then there exists a computable functional Φ : IN^{IN} × IN → IN s.t. for all representatives r_{x} ∈ IN^{IN} of x ∈ P and all b ∈ IN

∀y ∈ K∀z^{X}∀f^{X→X}(f n.e. ∧ d_{X}(z, f(z)) ≤_{IR} (b)_{IR} ∧∀u^{0} ≤ Φ(r_{x}, b)B_{∀}(x, y, z, f, u) → ∃v^{0} ≤ Φ(r_{x}, b)C_{∃}(x, y, z, f, v))

holds in all nonempty hyperbolic spaces (X, d, W). Analogously, for A^{ω}[X, d, W, CAT(0)]_{−b} where (X, d, W) is a CAT(0) space.

2. The corollary also holds for an additional parameter ∀z′^{X} if we add the additional premise d_{X}(z, z′) ≤_{IR} (b)_{IR} to the conclusion.

3. Furthermore, the corollary holds for an additional parameter ∀c^{0→X} if one adds the premise ∀n(d_{X}(z, c(n)) ≤_{IR} (b)_{IR}) or just ∀n(d_{X}(z, c(n)) ≤_{IR} (g(n))_{IR}) to the conclusion, where the bound then additionally depends on g : IN → IN.

4. Statements 1., 2. and 3. also hold if we replace ‘f n.e.’ with ‘f Lipschitz continuous’ (with constant L ∈ Q_{+}^{∗}), ‘f Hölder-Lipschitz continuous’ (with constants L, α ∈ Q_{+}^{∗}, where α ≤ 1) or ‘f uniformly continuous’ (with modulus ω : IN → IN). For Lipschitz and Lipschitz-Hölder continuous functions the bound additionally depends on the given constants and for uniformly continuous functions the bound additionally depends on the given modulus of uniform continuity.

5. Furthermore, 1., 2. and 3. hold if we replace ‘f n.e.’ with ‘f weakly quasi-nonexpansive’. For weakly quasi-nonexpansive functions (with fixed point p) we need to state the additional premise ‘d_{X}(z, p) ≤_{IR} (b)_{IR}’ in the conclusion.

6. More generally, 1., 2. and 3. hold if in the conclusion f satisfies ‘d_{X}(z, f(z)) ≤_{IR} (b)_{IR}’ and if instead of ‘f n.e.’ we assume

∀z_{1}^{X}, z_{2}^{X}(d_{X}(z_{1}, z_{2})_{IR} <_{IR} (n)_{IR} → d_{X}(f(z_{1}), f(z_{2})) ≤_{IR} (Ω_{0}(n))_{IR}), (∗)

where Ω_{0} is a function IN → IN. The bound then depends on Ω_{0} and b.

7. Finally, 1.,2. and 3. hold if ‘f n.e.’ is replaced by

∀z̃^{X}(d_{X}(z, z̃)_{IR} <_{IR} (n)_{IR} → d_{X}(z, f(z̃)) ≤_{IR} (Ω(n))_{IR}), (∗∗)

where Ω is a function IN → IN. Then we can drop ‘d_{X}(z, f(z)) ≤_{IR} (b)_{IR}’ in the conclusion and the extracted bound only depends on Ω instead of b.

Proof. In the following we write for simplicity e.g. ‘d(z, z̃) ≤ n’ instead of its formal representation ‘d_{X}(z, z̃) ≤_{IR} (n)_{IR}’ as a formula of L(A^{ω}[X, d]). For 1., by the comment after Definition 4.16 the premise ‘f n.e.’ is a ∀- formula and hence an admissible premise in Corollary 4.15. The parameters ranging over the Polish spaces P, resp, compact Polish spaces K, are treated as before. Choose a = z, then trivially 0 ≳^{z} z and λn^{0}.(n + b) ≳^{z} f, as using d(z, f(z)) ≤ b and the nonexpansivity of f and assuming d(z, z̃) ≤ n we get^{13}

d(z, f(z̃)) ≤ d(z, f(z)) + d(f(z), f(z̃)) ≤ b + d(z, z̃) ≤ n + b.

For 2. and 3., note that trivially b ≳^{z} z, z′ and λn^{0}.b ≳^{z} c, resp. g^{M} ≳^{z} c.

For 4., 5. and 6., we will show that d(z, f(z)) ≤ b in conjunction with the requirement that f is Lipschitz continuous, Hölder-Lipschitz continuous, uniformly continuous or f satisfying (∗) allows one to derive an Ω such that f satisfies (∗∗), thereby reducing these cases to 7. Similarly, if f is weakly quasi-nonexpansive (with fixed point p) and the additional premise d(z, p) ≤ b is satisfied, f satisfies (∗∗). All these conditions on f, including (∗), can be written as purely universal formulas (in the case of ‘f weakly quasi-nonexpansive’ with a parameter p) and may hence serve as a premise according to our metatheorem.

For 7., if f satisfies ∀z̃ ∈ X(d(z, z̃) < n → d(z, f(z̃)) ≤ Ω(n)), then trivially λn.Ω^{M}(n + 1) ≳^{z} f, as d(z, z̃) ≤ n implies d(z, z̃) < n + 1 which by (∗∗) implies d(z, f(z̃)) ≤ Ω(n + 1). Using the fact that <_{IR} is a Σ_{1}^{0}-statement and ≤_{IR} is a Π_{1}^{0}-statement we can express (∗∗) as a ∀-formula. Also note, that f satisfying (∗∗) implies a bound on d(z, f(z)): since d(z, z) < 1 by (∗∗) we have d(z, f(z)) ≤ Ω(1).

If f is Lipschitz continuous with constant L > 0 then one shows, using d(z, f(z)) ≤ b and the triangle inequality and assuming d(z, z̃) ≤ n

d(z, f(z̃)) ≤ d(z, f(z)) + d(f(z), f(z̃)) ≤ L · d(z, z̃) + b ≤ L · n + b, so f satisfies (∗∗) with Ω(n) := L · n + b. If f is Hölder-Lipschitz continuous, i.e. d(f(x), f(y)) ≤ L · d(x, y)^{α} for constants L > 0 and 0 < α ≤ 1, then f satisfies (∗∗) with Ω(n) := L · n^{α} + b.

13Here and in the following we write for better readability simply d and b instead of d_{X} and (b)_{IR} etc.

If f : X → X with (X, d, W) a hyperbolic space is uniformly continuous with modulus^{14} ω, then f satisfies (∗∗) with Ω(n) := n·2^{ω(0)}+b+1. Given z, z̃ ∈ X with d(z, z̃) < n we can (using W with z, z̃ and suitable λ to construct z_{1}, W with z_{1}, z̃ and suitable λ to construct z_{2}, etc.) inductively construct points z_{1}, … z_{k−1} (with k = n · 2^{ω(0)} + 1) such that

d(z, z_{1}), d(z_{1}, z_{2}), …, d(z_{k−1}, z̃) < 2^{−ω(0)}

and hence

d(f(z), f(z_{1})), d(f(z_{1}), f(z_{2})), …, d(f(z_{k−1}), f(z̃)) ≤ 1(= 2^{−0}).

Then by the triangle inequality d(f(z), f(z̃)) ≤ k = n · 2^{ω(0)} + 1 and another use of the triangle inequality yields d(z, f(z̃)) ≤ d(z, f(z)) + d(f(z), f(z̃)) ≤ n · 2^{ω(0)} + b + 1.

For weakly quasi-nonexpansive functions f – with fixed point p and with the additional premise: ‘d(z, p) ≤ b’ – the function f satisfies (∗∗) with Ω(n) := n + 2b, as given d(z, z̃) < n

\begin{aligned}d(z, f(z̃)) & ≤ d(z, p) + d(f(z̃), p) ≤ d(z, p) + d(z̃, p) \\ & ≤ d(z, p) + d(z̃, z) + d(z, p) ≤ n + 2b. \end{aligned}

Alternatively, choosing a = p and writing (∗∗) with p instead of z (and adjusting the other majorants accordingly) f even satisfies (∗∗) with Ω(n) := n, as given d(p, z̃) < n

d(p, f(z̃)) ≤ d(p, z̃) ≤ n.

If f satisfies d(z, f(z)) ≤ b and (∗), then given d(z, z̃) < n,

d(z, f(z̃)) ≤ d(z, f(z)) + d(f(z), f(z̃)) ≤ Ω_{0}(n) + b

and hence f satisfies (∗∗) with Ω(n) := Ω_{0}(n) + b.

The results then follow using Corollary 4.15.

14Recall, that f : X → X uniformly continuous with modulus ω : IN → IN is defined as ∀x, y ∈ X∀k ∈ IN(d(x, y) < 2^{−ω(k)} → d(f(x), f(y)) ≤ 2^{−k}).

Note, that neither the space nor the range of f are in any way assumed to be bounded, but still the bound Φ is highly uniform as it depends only on b (and additional input L, α, ω, Ω_{0} and Ω as stated in cases 3.-7.), but not directly on the points z, z′, the sequence c or the function f.

Remark 4.18. Even if ‘z’ does not occur in B_{∀}, C_{∃} so that ‘∀z’ is a ‘dummy’ quantifier, we still need in 1.-4. and 6. in the conclusion a number b with b ≥ d(z, f(z) for some z as this is used in constructing a majorant for f. In 5. we could identify z with p (and b := 1 say) and construct a p-majorant of f. In 7. we can construct a uniform f-majorant without reference to b.

Remark 4.19. Note that for f nonexpansive, Lipschitz, Hölder-Lipschitz or uniformly continuous, f is provably extensional. For f weakly quasinonexpansive or f satisfying conditions (∗) or (∗∗) it does not follow that f is extensional. Thus in these cases, if an instance of the extensionality of f is used in a proof, it must either be provable via the extensionality rule (or one must explicitly require f to be (provably) extensional, e.g. by requiring that f is at least uniformly continuous).

Remark 4.20. Except for the case of f being uniformly continuous all results also hold for general (non-hyperbolic) metric spaces A^{ω}[X, d]_{−b}, (X, d). This also applies to corollaries 4.22 and 5.2 below. Note, that in general metric spaces uniformly continuous functions can in general not be majorized, i.e. for (∗∗) no suitable Ω(n) can be defined, because given x, y ∈ X we cannot construct intermediate points in order to be able to make use of the uniform continuity of f.

For a complete characterization of those metric spaces for which uniformly continuous functions f admit the definition of a suitable Ω see [30]. Otherwise, in the setting of metric spaces, we need to require explicitly that a given uniformly continuous function f with modulus ω also satisfies (∗∗) with a suitable Ω.

As a generalization of Corollary 3.11 in [22] we prove the following:

Definition 4.21. Let f : X → X, then

• for F ix(f) := {x^{X} | x =_{X} f(x)} the formula F ix(f) ≠ ∅ expresses f has a fixed point, • for F ix_{ε}(f, y, b) := {x^{X} | d_{X}(x, f(x)) ≤_{IR} ε ∧ d_{X}(x, y) ≤_{IR} b} and ε > 0

the formula F ix_{ε}(f, y, b) ≠ ∅ expresses f has an ε-fixed point in a bneighborhood of y.

Corollary 4.22. 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space) and let B_{∀} and C_{∃} be as before. If A^{ω}[X, d, W]_{−b} proves that

∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}(f n.e. ∧ F ix(f) ≠ ∅ ∧ ∀u^{0}B_{∀} → ∃v^{0}C_{∃})

then there exists a computable functional Φ^{1→0→0} (on representatives r_{x} : IN → IN of elements x of P) s.t. for all r_{x} ∈ IN^{IN}, b ∈ IN

∀y ∈ K ∀z^{X}, f^{X→X}(f n.e. ∧ ∀ε > 0F ix_{ε}(f, z, b) ≠ ∅ ∧d_{X}(z, f(z)) ≤_{IR} (b)_{IR} ∧ ∀u^{0} ≤ Φ(r_{x}, b)B_{∀} → ∃v^{0} ≤ Φ(r_{x}, b)C_{∃}).

holds in any nonempty hyperbolic space (X, d, W). Analogously, for A^{ω}[X, d, W, CAT(0)]_{−b} where then (X, d, W) has to be a CAT(0) space.

2. The corollary also holds if ‘f n.e.’ is replaced by f Lipschitz continuous, Hölder-Lipschitz continuous or uniformly continuous, where the extracted bound then additionally will depend on the respective constants and moduli.

3. Considering the premise ‘f weakly quasi-nonexpansive’, i.e.

∃p^{X}(f(p) =_{X} p ∧ ∀w^{X}(d_{X}(f(p), f(w)) ≤_{IR} d_{X}(p, w)))

instead of ‘f n.e. ∧F ix(f) ≠ ∅’ we may weaken this premise to

∀ε > 0∃p^{X}(d_{X}(f(p), p) ≤_{IR} ε ∧ d_{X}(z, p) ≤_{IR} (b)_{IR}
∧∀w^{X}(d_{X}(f(p), f(w)) ≤_{IR} d_{X}(p, w))).

4. Let Ψ : (X → X) → X → 1 be a provably extensional closed term of A^{ω}[X, d, W]_{−b}, then in 1. and 2. instead of ‘F ix(f) ≠ ∅’ we may weaken ‘Ψ(f, p) =_{IR} 0’, expressing that Ψ(f, ·) has a root p, to ‘∀ε > 0∃p ∈ X(d(z, p) ≤ b ∧ |Ψ(z, p)| ≤_{IR} ε)’, expressing that Ψ(f, ·) has ε-roots p which are b-close to z for every ε > 0.

Proof. Representing P and K in A^{ω}, quantification over x ∈ P and y ∈ K can be expressed as quantification over all x^{1}, resp. all y^{1} ≤ s for some closed function term s of A^{ω}. Thus the statement provable by assumption can be written as

∀x^{1} ∀y ≤_{1} s ∀z^{X}, p^{X}, f^{X→X}(f n.e. ∧ f(p) =_{X} p ∧ ∀u^{0}B_{∀} → ∃v^{0}C_{∃}),

where f(p) =_{X} p can be written as ∀k^{0}(d_{X}(p, f(p)) ≤_{IR} 2^{−k}) and both d_{X}(p, f(p)) ≤_{IR} 2^{−k} and f n.e., resp. the other conditions on f, are ∀- formulas.

For x we have x^{M} ≳^{a} x and from s we may obtain an a-majorant s^{∗} for s and hence for y ≤ s. By Corollary 4.17.2, under the additional (purely universal) premises d_{X}(z, p), d_{X}(z, f(z)) ≤_{IR} (b)_{IR}, we extract a functional Φ s.t. for all x ∈ P if r_{x} ∈ IN^{IN} represents x then

∀y ∈ K ∀z^{X}, p^{X}, f^{X→X}(d_{X}(z, p), d_{X}(z, f(z)) ≤_{IR} (b)_{IR} ∧ f n.e. ∧ d_{X}(f(p), p) ≤_{IR} 2^{−Φ(r_{x},b)} ∧ ∀u^{0} ≤ Φ(r_{x}, b)B_{∀} → ∃v^{0} ≤ Φ(r_{x}, b)C_{∃})

holds in all nonempty hyperbolic spaces (X, d, W) (similarly for the other conditions on f, except that then the extracted bound depends on the additional constants and moduli L, α and ω).

The statement d_{X}(z, p) ≤_{IR} (b)_{IR} ∧ d_{X}(f(p), p) ≤_{IR} 2^{−Φ(r_{x},b)} expresses that f has a 2^{−Φ(r_{x},b)}-fixed point in a b-neighborhood of z, which, since 2^{−Φ(r_{x},b)} does not depend on p, is implied by ∀ε > 0F ix_{ε}(f, z, b) ≠ ∅, so 1. and 2. follow from Corollary 4.17. The weakening of the premise ‘f weakly quasinonexpansive’ in 3. is treated similarly.

For 4., similar to the treatment of f(p) =_{X} p in 1., 2. and 3. we may write Ψ(f, p) =_{IR} 0 as ∀k^{0}(|Ψ(f, p)|_{IR} ≤_{IR} 2^{−k}). Then as before may weaken this statement to ∀ε > 0∃p^{X}(d_{X}(z, p) ≤_{IR} (b)_{IR} ∧ |Ψ(z, p)| ≤_{IR} ε).

Remark 4.23. Note, that in 1. the original premise ‘F ix(f) ≠ ∅’ is weakened to ‘∀ε > 0F ix_{ε}(f, z, b) ≠ ∅’. By Theorem 1 in [11], nonexpansive mappings on bounded hyperbolic spaces always have ε-fixed points for arbitrary ε > 0, while they need not have exact fixed points in general (not even in the case of bounded, closed and convex subsets of Banach spaces such as c_{0}). Hence, for bounded hyperbolic spaces and nonexpansive mappings the premise ‘∀ε > 0F ix_{ε}(f, z, b) ≠ ∅’ can be dropped, if b is taken as an upper bound on the metric d. For further discussion, see Remark 3.13 in [22].

5 Herbrand normal forms

The metatheorems in the previous sections allow one to treat at most classical proofs of formulas that prenex to the form ∀∃A_{qf}. Already for the formula class Π_{3}^{0}, i.e. ∀x^{0}∃y^{0}∀z^{0}A_{qf}(x, y, z), there are counterexamples where one no longer can extract effective bounds from a given classical proof. These counterexamples basically correspond to the undecidability of the halting problem for Turing machines.

However, the Herbrand normal form B^{H} = ∀x^{0}∀h_{z}^{1}∃y^{0}A_{qf}(x, y, h_{z}(y)) of B = ∀x^{0}∃y^{0}∀z^{0}A_{qf}(x, y, z) does have the appropriate form (and the Herbrand index function h_{z} has a suitable restricted type) to allow the extraction of a bound Φ(x, h_{z}) on ∃yA_{qf}(x, y, h_{z}(y)). Even though B and B^{H} are (ineffectively) equivalent, an extracted bound for ∃y in the Herbrand normal form B^{H} does not yield a bound for ∃y in the original formula B, as it may depend in addition to x on the index function h_{z}.

The extraction of bounds for Herbrand normal forms can be generalized to a large class of formulas, more precisely to those for which there exists a prenexation such that the Herbrand index functions are of suitable restricted type. The types of the Herbrand index functions depend on the ∃∀ configurations that occur in the prenexation. A configuration ∃y^{ρ}∀z^{τ} gives rise to ∀h_{z}^{ρ→τ}∃y^{ρ}, i.e. Herbrand index functions of type ρ → τ. Restricting ourselves to cases where the Herbrand index functions are guaranteed to have majorants, we only allow configurations ∃y^{ρ}∀z^{τ} where ρ = 0 and τ is of degree (0, X) or 1. Then the types of the Herbrand index functions are of degree (0, X) or 1 as well. This class of formulas covers all arithmetical formulas as well as many other interesting classes involving the extended types T^{X}.

Clearly, one may extract effective bounds for the Herbrand normal form of formulas if the Herbrand index functions are of suitable restricted type, where naturally, the extracted bounds depend on (a-majorants for) the Herbrand index functions. Of even greater interest is the fact that we may, similarly to the result of Corollary 4.22, weaken or even eliminate the premises of a theorem, even though the conclusion might be of too general form to allow one to extract effective bounds on A rather than A^{H}, as we will show next.

Definition 5.1. The class H of formulas consists of all formulas F that have a prenexation F′ ≡ ∃x_{1}^{ρ_{1}}∀y_{1}^{τ_{1}} … ∃x_{n}^{ρ_{n}}∀y_{n}^{τ_{n}}F_{∃}(\underline{x}, \underline{y}) where F_{∃} is an ∃-formula, the types ρ_{i} are of degree 0 and the types τ_{i} are of degree 1 or (0, X).

We state the following corollary:

Corollary 5.2. 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space) and let the formula A be in the class H, where moreover A does not contain 0_{X}. If A^{ω}[X, d, W]_{−b} proves a sentence

∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}(f n.e. ∧ F ix(f) ≠ ∅ → A)

then the following holds in every nonempty hyperbolic space (X, d, W):

\begin{matrix}∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X} \\ (f n.e. ∧ ∃b^{0}∀ε > 0(F ix_{ε}(f, z, b) ≠ ∅) → A). \end{matrix}

Analogously, for A^{ω}[X, d, W, CAT(0)]_{−b} where (X, d, W) is a CAT(0) space.

2. The corollary also holds if we replace ‘f n.e.’ with f Lipschitz continuous, Hölder-Lipschitz continuous or uniformly continuous.

3. Considering the premise ‘f weakly quasi-nonexpansive’, i.e.

∃p^{X}(f(p) =_{X} p ∧ ∀w^{X}(d_{X}(f(p), f(w)) ≤_{IR} d_{X}(p, w)))

instead of ‘f n.e. ∧F ix(f) ≠ ∅’ we may weaken this premise to

∃b^{0}∀ε > 0∃p^{X}(d_{X}(f(p), p) ≤_{IR} ε ∧ d_{X}(z, p) ≤_{IR} (b)_{IR}
∧∀w^{X}(d_{X}(f(p), f(w)) ≤_{IR} d_{X}(p, w))).

4. Let Ψ : (X → X) → X → 1 be a provably extensional closed term of A^{ω}[X, d, W]_{−b}, then in 1. and 2. instead of ‘F ix(f) ≠ ∅’ we may weaken ‘∃p^{X}Ψ(f, p) =_{IR} 0’, expressing that Ψ(f, ·) has a root in p, to ‘∃b^{0}∀ε > 0∃p^{X}(d_{X}(z, p) ≤_{IR} (b)_{IR} ∧ |Ψ(z, p)| ≤_{IR} ε)’, expressing that Ψ(f, ·) has ε-roots p which are b-close to z for every ε > 0.

Proof. Since A → A^{H} is logically valid, the statement

∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}(f n.e. ∧ F ix(f) ≠ ∅ → A)

trivially implies

∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}(f n.e. ∧ F ix(f) ≠ ∅ → A^{H})

where A^{H} is the Herbrand normal form of a suitable prenexation of A as suggested by the formula class H. Pulling outside the universal quantifiers in A^{H}, which range over the Herbrand index functions, the statement now has a suitable form and the index functions have a suitable type to make possible the extraction of an effective numerical bound (by Corollary 4.22) on the numerical universal quantifiers in the premise and existential quantifiers in the conclusion.

As is to be expected, the extracted bound depends on the parameter x via a representative r_{x}, on a bound b ≥ d(z, f(z)) (and b ≥ d(z, 0_{X}) if 0_{X} occurs in A) and on majorants for the Herbrand index functions. Such majorants always exist, as the Herbrand index functions h all are of type degree 1, in which case h^{M} is an a-majorant, or of type degree (0, X), i.e. basically a sequence of elements in X, in which case we (ineffectively) choose as an a-majorant h^{∗} any sequence of numbers such that h^{∗}(n) ≥ d(h(m), a) for all n ∈ IN and all m ≤ n, e.g. we may take h^{∗} := h̃^{M}, where h̃(n) := ⌈d(h(n), a)⌉. As before, using the representation of P and K in A^{ω}, we obtain majorants for (representatives of) x and y.

Thus, by Theorem 4.10 and reasoning as in the proof of Corollary 4.22 we may weaken the universal premise ‘F ix(f) ≠ ∅’ to ‘∀ε > 0F ix_{ε}(f, z, b) ≠ ∅’. Shifting the quantifiers ranging over the Herbrand index functions back in, we obtain:

\begin{matrix}∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}∀b^{0} \\ (f n.e. ∧ ∀ε > 0F ix_{ε}(f, z, b) ≠ ∅ ∧ d_{X}(z, f(z)) ≤_{IR} (b)_{IR} → A^{H}). \end{matrix}

But using that (ineffectively) A^{H} implies back A this yields that

\begin{matrix}∀x ∈ P ∀y ∈ K ∀z^{X}, f^{X→X}∀b^{0} \\ (f n.e. ∧ ∀ε > 0F ix_{ε}(f, z, b) ≠ ∅ ∧ d_{X}(z, f(z)) ≤_{IR} (b)_{IR} → A) \end{matrix}

holds in all nonempty hyperbolic spaces (X, d, W).

Finally, since here we are not interested in effective bounds but only the (classical) truth of the statement, we may furthermore omit the premise ‘d_{X}(z, f(z)) ≤_{IR} (b)_{IR}’: if for a given z ∈ X and f : X ∈ X there exists a b such that ‘∀ε > 0F ix_{ε}(f, z, b) ≠ ∅’ holds, then there also exists a b′ satisfying both premises, as we may simply take b′ = ⌈max(b, d_{X}(z, f(z)))⌉.

The cases 2., 3. and 4. are treated similarly.

To see that the restrictions on the types of the Herbrand index functions are necessary consider the following counterexample. In A^{ω}[X, d, W]_{−b} one trivially proves that:

∀f^{X→X}(f n.e. ∧ F ix(f) ≠ ∅ → F ix(f) ≠ ∅),

where ‘F ix(f) ≠ ∅’ is expressed by ‘∃z^{X}∀k^{0}(d_{X}(z, f(z)) ≤_{IR} 2^{−k})’.

Without the restrictions on the types of the Herbrand index functions in A^{H} and hence on A, Corollary 5.2 would allow us to weaken the premise ‘f has a fixed point’ to ‘f has ε-fixed points’ and in the case of bounded hyperbolic spaces even eliminate the premise completely since nonexpansive mappings on bounded hyperbolic spaces always have approximate fixed points. Hence we could prove that for bounded hyperbolic case every nonexpansive mapping has exact fixed points. As we mentioned already, this is false even for bounded closed convex subsets of Banach spaces, such as e.g. c_{0}.

This counterexample is ruled out by the restrictions on the types of the Herbrand index functions. Since the statement ‘f has a fixed point’ is expressed by ∃z^{X}∀k^{0}(d_{X}(z, f(z)) ≤_{IR} 2^{−k}), the resulting Herbrand index functions have the type X → 0. But already this very simple type is not allowed in the formula class H and hence not in our corollary.

6 Metatheorems for normed linear spaces

We now discuss the setting of (real) normed linear spaces with convex subsets C. As discussed in Machado[28], one may characterize convex subsets of normed spaces in the setting of hyperbolic spaces in terms of additional conditions on the function W. The additional conditions are (I) that the convex combinations do not depend on the order in which they are carried out, and (II) that the distance is homothetic. These additional conditions are:

(I) ∀x, y, z ∈ X∀λ_{1}, λ_{2}, λ_{3} ∈ [0, 1](λ_{1} + λ_{2} + λ_{3} =_{IR} 1 → W (z, W (y, x, \frac{λ_{1}}{1−λ_{3}} ), 1 − λ_{3}) = W (x, W (z, y, \frac{λ_{2}}{1−λ_{1}} ), 1 − λ_{1})),

(II) ∀x, y, z ∈ X∀λ ∈ [0, 1](d(W (z, x, λ), W (z, y, λ)) = λ · d(x, y)).

The formal version of axiom (I) will look slightly different, as expressing the axiom with λ_{1} +λ_{2} +λ_{3} =_{IR} 1 (with the equality as a premise) is problematic for our purposes. Equality on the reals is a universal statement and hence the axiom itself would no longer be purely universal.

Instead, given λ_{1}, λ_{2} we may explicitly define λ̄_{1}, λ̄_{2} and λ̄_{3} s.t. provably (in A^{ω}) both λ̄_{1} + λ̄_{2} + λ̄_{3} =_{IR} 1 and if λ_{i} ∈ [0, 1] and λ_{1} + λ_{2} + λ_{3} =_{IR} 1 then λ̄_{i} = λ_{i} for i = 1, 2, 3. The formal versions of the axioms are then as follows:

(I) ∀x^{X}, y^{X}, z^{X}∀λ_{1}^{1}, λ_{2}^{1} (W_{X}(z, W_{X}(y, x, \frac{λ̄_{1}}{1−λ̄_{3}} ), 1 − λ̄_{3}) = W_{X}(x, W_{X}(z, y, \frac{λ̄_{2}}{1−λ̄_{1}} ), 1 − λ̄_{1})), where λ̄_{1} =_{1} λ̃_{1}, λ̄_{2} =_{1} min_{IR}(λ̃_{2}, 1 −_{IR} λ̄_{1}) and λ̄_{3} =_{1} 1 −_{IR} (λ̄_{1} +_{IR} λ̄_{2}),

(II) ∀x^{X}, y^{X}, z^{X}∀λ^{1}(d_{X}(W_{X}(z, x, λ), W_{X}(z, y, λ)) =_{IR} λ̃ ·_{IR} d_{X}(x, y)),

where λ̃ is the construction in Definition 2.4. As discussed for the other (X, d, W) axioms in Remark 2.6, the axiom (II) is formulated with W_{X} to implicitly satisfy W_{X}(x, y, λ) =_{X} W_{X}(x, y, λ̃).

Thus, theorems concerning convex subsets of normed linear spaces which can be formalized A^{ω}[X, d, W]_{−b} + Machado’s two additional axioms can already be treated using the above Theorem 4.10 (as discussed in Remark 4.12). However, as discussed in [22], metatheorems covering normed linear spaces in general rather than just convex subsets of normed linear spaces can be expected to have many more applications, than the applications in fixed point theory investigated so far.

For the new metatheorem for normed linear spaces (with convex subset C) there are, compared to the new metatheorems for (unbounded) metric spaces, two differences: (1) we fix the choice a = 0_{X} and (2) one cannot meaningfully differentiate between 0_{X} occurring or not occurring in the theorem to be treated by the metatheorem since it implicitly occurs whenever the norm is used as the latter measures the distance from 0_{X} (in metric spaces, the only purpose of the constant 0_{X} was to witness the nonemptyness of the space by a closed term). It is this link between the constant 0_{X} and the other constants of normed linear spaces, that lets us choose a = 0_{X} (one could also use an arbitrary a, but then the majorant of the norm would depend on a, i.e. the norm is – in contrast to the metric – not uniformly majorizable).

As in [22], the type C for the convex subset C and quantification over elements of types involving C are defined notions, i.e. an element x ∈ X is of type C if χ_{C}(x) =_{0} 0, where χ_{C} is a constant of type X → 0 representing the characteristic function of C. Note, however, that our weakly extensional context does not allow us to prove that x =_{X} y ∧ χ_{C}(x) =_{0} 0 → χ_{C}(y) =_{0} 0 but only if s =_{X} t is provable that then χ_{C}(s) =_{0} χ_{C}(t) (see [22] for a discussion of this point).

Quantification is treated using the following abbreviations:

\begin{aligned}∀x^{C} A(x) & :≡ ∀x^{X}(χ_{C}(x^{X}) =_{0} 0 → A(x)), \\ ∀f^{1→C} A(f) & :≡ ∀f^{1→X}(∀y^{1}(χ_{C}(f(y)) =_{0} 0) → A(f)), \\ ∀f^{X→C} A(f) & :≡ ∀f^{X→X}(∀y^{X}(χ_{C}(f(y)) =_{0} 0) → A(f)) \\ ∀f^{C→C} A(f) & :≡ ∀f^{X→X}(∀x^{X}(χ_{C}(x) =_{0} 0 → χ_{C}(f(x)) =_{0} 0) → A(f̃)), \end{aligned}

where f̃(x) = \{ \begin{matrix}f(x), if χ_{C}(x) =_{0} 0 \\ c_{X}, otherwise. \end{matrix}

Analogously, for the corresponding ∃-quantifiers with ‘∧’ instead of ‘→’.

Note, that the additional premises to the conclusion are ∀-formulas if we have parameters of these defined types. This extends to types of degree (1, X, C) where ρ is of degree (1, X, C) if it has the form τ_{1} → … → τ_{k} → C, where τ_{i} has degree 1 or equals X or C. Also note, that if we write ‘f nonexpansive’ for a function f : C → C, this is to be understood as the ∀-formula

∀x^{X}, y^{X}(χ_{C}(x) =_{0} 0 =_{0} χ_{C}(y) → ∥f(x) − f(y)∥_{X} ≤_{IR} ∥x − y∥_{X}).

Analogously, for the other notions in Definition 4.16.

Remark 6.1. When we aim to treat parameters f : C → C in our metatheorems, we need to majorize not that f, but rather the extension f̃ to a function X → C. In [22], where only norm-bounded convex subsets C are considered, the extended function f̃ is easily majorized using the b-boundedness of C (as are parameters of type (1, X, C) in general). In this paper, where we consider unbounded convex subsets C, majorization must employ special properties of the function f, such as e.g. f being nonexpansive. However, the extension f̃ does in general not inherit such properties from f, so instead a majorant for f̃ in general will result from deriving a majorant for f on C from special properties of f, deriving a majorant for f̃ on X \ C from the definition of f̃ and taking the maximum over these two majorants.

Definition 6.2. We say that a sentence of L(A^{ω}[X, ∥ · ∥, C]_{−b} holds in a non-trivial (real) normed linear space with a nonempty convex subset C, if it holds in the models^{15} of A^{ω}[X, ∥ · ∥, C]_{−b} obtained by letting the variables range over the appropriate universes of the full set-theoretic type structure S^{ω,X} with the sets IN, X as the universes for the base types 0 and X. Here 0_{X} is interpreted by the zero vector of the linear space X, 1_{X} by some vector a ∈ X with ∥a∥ = 1, +_{X} is interpreted as addition in X, −_{X} is the inverse of x w.r.t. + in X, ·_{X} is interpreted as λα ∈ IN^{IN}, x ∈ X.r_{α} · x, where r_{α} is the unique real number represented by α and · refers to scalar multiplication in the IR-linear space X. Finally, ∥·∥_{X} is interpreted by λx ∈ X.(∥x∥)_{∘}. For the nonempty convex subset C ⊆ X, χ_{C} is interpreted as the characteristic function for C and c_{X} by some arbitrary element of C.

The new metatheorem for normed linear spaces is:

Theorem 6.3. 1. Let ρ be of degree (1, X), (1, X, C) or 2 and let B_{∀}(x, u), resp. C_{∃}(x, v), contain only x, u free, resp. x, v free. Assume

A^{ω}[X, ∥ · ∥, C]_{−b} ⊢ ∀x^{ρ}(∀u^{0}B_{∀}(x, u) → ∃v^{0}C_{∃}(x, v)),

Then there exists a partial computable functional Φ : Sρ̂ × IN ⇀ IN s.t. Φ is defined on all strongly majorizable elements of Sρ̂ and the following holds in all non-trivial (real) normed linear spaces (X, ∥ · ∥, C) with a nonempty convex subset C: for all x ∈ S_{ρ}, x^{∗} ∈ Sρ̂ and n ∈ IN if x^{∗} ≳^{0_{X}} x and (n)_{IR} ≥_{IR} ∥c_{X}∥_{X} then

15Again we use the plural, as in the setting of normed linear spaces the interpretation of 1_{X} and c_{X} are not uniquely determined.

∀u ≤ Φ(x^{∗}, n)B_{∀}(x, u) → ∃v ≤ Φ(x^{∗}, n)C_{∃}(x, v)).

In particular, if ρ is in addition of degree 1, then Φ : Sρ̂ × IN → IN is totally computable.

2. For uniformly convex spaces with modulus of uniform convexity η statement 1. holds with (X, ∥ · ∥, C, η), A^{ω}[X, ∥ · ∥, C, η]_{−b} instead of (X, ∥ · ∥, C), A^{ω}[X, ∥ · ∥, C]_{−b}, where the extracted bound Φ additionally depends on η.

3. Analogously, for real inner product spaces (X, ⟨·, ·⟩).

As in the metric case, instead of single variables x, u, v and single premises ∀uB_{∀}(x, u) we may have tuples of variables and finite conjunctions of premises.

Remark 6.4. In the case of metric spaces, if 0_{X} did not occur in the formula for which we want to extract a bound, the bound did not depend on a bound on the distance between the chosen a and 0_{X}. This is mainly because the axioms of A^{ω}[X, d]_{−b} place no requirements on 0_{X}. This is not the case for normed linear spaces, as in the theory A^{ω}[X, ∥ · ∥, C]_{−b} the constant c_{X} is necessary for the interpretation of one of the axioms and hence in general the extracted term may depend on a bound on the norm of c_{X}, even though c_{X} does not occur in the formulas B_{∀} and C_{∃}. However, if c_{X} does not occur in the formulas B_{∀} and C_{∃} and we have another parameter z ∈ C for which we have a bound on the norm, we need not explicitly demand a bound on ∥c_{X}∥, since in the model c_{X} may be interpreted by an arbitrary element of C and we then may interpret c_{X} by z.

As a corollary we prove Theorem 3.30 in [22].

Corollary 6.5. 1. Let σ be of degree 1 and ρ of degree 1 or (1, X) and let τ be a type of degree (1, X, C). Let s be a closed term of type σ → ρ and B_{∀}, C_{∃} as before. If

∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(∀u^{0}B_{∀}(x, y, z, u) → ∃v^{0}C_{∃}(x, y, z, v))

is provable in A^{ω}[X, ∥ · ∥, C] then one can extract a computable functional Φ : S_{σ} × IN → IN s.t. for all x ∈ S_{σ}

∀y ≤_{ρ} s(x)∀z^{τ}(∀u^{0} ≤ Φ(x, b)B_{∀}(x, y, z, u) → ∃v^{0} ≤ Φ(x, b)C_{∃}(x, y, z, v)) holds in any non-trivial (real) normed linear space (X, ∥ · ∥) and any nonempty b-bounded convex subset C ⊂ X (with ‘b_{X}’ interpreted by ‘b’).

2. For uniformly convex spaces (X, ∥ · ∥, η) with modulus of uniform convexity η ‘1.’ holds with A^{ω}[X, ∥ · ∥, C, η] and (X, ∥ · ∥, C, η) instead of A^{ω}[X, ∥ · ∥, C] and (X, ∥ · ∥, C). This time Φ is a computable functional in x, b and a modulus η of uniform convexity for (X, ∥·∥) (which interprets the constant ‘η’).

3. Analogously, for real inner-product spaces (X, ⟨·, ·⟩).

Proof. As before in the proof of Corollary 4.14, for x we have x^{M} ≳^{0_{X}} x and for s(x) ≥_{ρ} y we get (using Lemma 3.6) that s^{∗}(x^{M}) ≳^{0_{X}} y, where s^{∗} is some majorant of s (which exists by Lemma 9.12 as a closed term of A^{ω}). Next, given a bound b ∈ IN on the diameter of C, trivially (b)_{IR} ≥ ∥c_{X}∥ and writing τ = τ_{1} → … → τ_{k} → C, then also λ\underline{x}τ̂_{i}.b ≳_{τ}^{0_{X}} z.

Then by Theorem 6.3 we can extract a bar recursive functional ϕ such that ϕ((x)^{M}, s^{∗}(x^{M}), λ\underline{x}τ̂_{i}.b, b) is a bound on ∃v, resp. ∀u, for any non-trivial real normed linear space and any (nonempty)b-bounded convex subset C. Since both the functional (·)^{M}, the a-majorant s^{∗} for s and the a-majorant λ\underline{x}τ̂_{i}.b for z are given by closed terms of A^{ω}, the functional

Φ :≡ λx, b.ϕ(x^{M}, s^{∗}(x^{M}), λ\underline{x}τ̂_{i}.b, b)

is computable and yields the desired bound.

Note, that in A^{ω}[X, ∥ · ∥, C] we have the boundedness of C as an axiom, while Theorem 6.3 only allows one to treat the boundedness as an implicative assumption. Therefore, as in the proof of Corollary 4.14, this corollary follows from the proof of Theorem 6.3, rather than from the theorem itself.

We furthermore prove the analogue of Corollary 4.17, though with one important difference: it is no longer sufficient to just have a bound on ∥z − f(z)∥, ∥z − z′∥, etc. as in the metric case. Since the choice of a is fixed to a = 0_{X} in the normed linear case, we also need a bound on the distance between z and 0_{X}, i.e. ∥z∥. Moreover, for the functions f : C → C we consider as parameters, the majorization of f, or rather of the extension f̃ : X → C, requires special care (see Remark 6.1).

Corollary 6.6. 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space). Assume we prove in A^{ω}[X, ∥·∥, C]_{−b} a sentence

\begin{matrix}∀x ∈ P ∀y ∈ K∀z^{C}∀f^{C→C} \\ (f n.e. ∧ ∀u^{0}B_{∀}(x, y, z, f, u) → ∃v^{0}C_{∃}(x, y, z, f, v)), \end{matrix}

where c_{X} does not occur in B_{∀} and C_{∃}. Then there exists a computable functional Φ : IN^{IN} × IN → IN s.t. for all representatives r_{x} ∈ IN^{IN} of x ∈ P and all b ∈ IN

∀y ∈ K∀z^{C}∀f^{C→C}(f n.e. ∧ ∥z∥_{X}, ∥z − f(z)∥_{X} ≤_{IR} (b)_{IR} ∧∀u^{0} ≤ Φ(r_{x}, b)B_{∀}(x, y, z, f, u) → ∃v^{0} ≤ Φ(r_{x}, b)C_{∃}(x, y, z, f, v))

holds in all non-trivial normed linear spaces (X, ∥ · ∥) and nonempty convex subsets C. Analogously, for uniformly convex spaces (X, ∥·∥, C, η) and inner product spaces (X, ⟨·, ·⟩), where for uniformly convex spaces the bound Φ additionally depends on the modulus of uniform convexity η.

2. The corollary also holds for an additional parameter ∀z′^{C}, if we add the additional premise ∥z − z′∥_{X} ≤_{IR} (b)_{IR} to the conclusion.

3. Furthermore, the corollary holds for an additional parameter ∀c^{0→C} if we add the additional premise ∀n(∥z − c(n)∥_{X} ≤_{IR} (b)_{IR}) or just ∀n(∥z − c(n)∥_{X} ≤_{IR} (g(n))_{IR}) to the conclusion, where the bound then additionally depends on g : IN → IN.

4. 1., 2. and 3. also hold if we replace ‘f n.e.’ with ‘f Lipschitz continuous’ (with constant L ∈ Q_{+}^{∗}), ‘f Hölder-Lipschitz continuous (with constants L, α ∈ Q_{+}^{∗}, where α ≤ 1) or ‘f uniformly continuous’ (with modulus ω : IN → IN). For Lipschitz and Lipschitz-Hölder continuous functions the bound depends on the given constants, for uniformly continuous functions the bound depends on the given modulus of uniform continuity.

5. Furthermore, 1., 2. and 3. hold if we replace ‘f n.e.’ with ‘f weakly quasi-nonexpansive’. For weakly quasi-nonexpansive functions (with fixed point p) we need to state the additional premise ∥p∥_{X} ≤_{IR} (b)_{IR} in the conclusion.

6. 1.,2. and 3. also hold if we replace ‘f n.e.’ in the premise and the conclusion by

∀z_{1}^{C}, z_{2}^{C}(∥z_{1} − z_{2}∥_{X} <_{IR} (n)_{IR} → ∥f(z_{1}) − f(z_{2})∥_{X} ≤_{IR} (Ω_{0}(n))_{IR}), (∗)

where Ω_{0} is a function IN → IN and the bound additionally depends on Ω_{0}.

7. Finally, 1.,2. and 3. hold if the previous conditions on f are replaced

by

∀z̃^{C}(∥z̃∥_{X} <_{IR} (n)_{IR} → ∥f(z̃)∥_{X} ≤_{IR} (Ω(n))_{IR}), (∗∗)

where Ω is a function IN → IN and the bound additionally depends on Ω. In this case we can drop the assumption ‘∥z − f(z)∥_{X} ≤ (b)_{IR}’ in the conclusion whereas ‘∥z∥_{X} ≤ (b)_{IR}’ has to remain.

Note that (∗), (∗∗) are logically equivalent to ∀-formulas.

Proof. This is basically the same proof as the proof of Corollary 4.17, except for two points: (1) as discussed we need to fix a = 0_{X} and we need an additional premise, ∥z∥ ≤ b and (2) the 0_{X}-majorization of f (actually f̃) requires extra care. From the definition of f̃ it is obvious that n ≳_{X}^{0_{X}} f(x) for x ∈ X \ C if n ≥ ∥c_{X}∥. Also note, that since we assume c_{X} does not occur in B_{∀} and C_{∃} we may, by Remark 6.4 interpret c_{X} by the parameter z in the model, so that ∥c_{X}∥ ≤ b. Hence, given an a-majorant λn.f^{∗}(n) ≳_{X}^{0_{X}} f on the convex subset C, we obtain the 0_{X}-majorant λn.max(f^{∗}(n), b) for f̃ and thus the extracted bound does not depend on an explicit bound on the norm of c_{X}. In the following we may therefore focus on 0_{X}-majorants for f on the convex subset C.

For 1., 2. and 3. we have that b ≳^{0_{X}} z, 2b ≳^{0_{X}} z′ and λn^{0}.2b ≳^{0_{X}} c, resp. λn.g^{M}(n) + b ≳^{0_{X}} c. For λn^{0}.n + 3b ≳^{0_{X}} f, where f is nonexpansive, we reason as follows: assume ∥z̃∥ ≤ n then

∥f(z̃)∥ = ∥f(z̃) − f(z) + f(z) − z + z∥
≤ ∥f(z̃) − f(z)∥ + ∥f(z) − z∥ + ∥z∥
≤ ∥z̃ − z∥ + b + b
≤ ∥z̃∥ + ∥z∥ + 2b
≤ n + 3b.

Similarly, for 4.,5., 6. and 7. one obtains λn^{0}.Ω^{M}(n + 1) ≳^{0_{X}} f if Ω satisfies (∗∗) from 7. As in the metric case, one may obtain a bound on ∥f(z) − z∥ using (∗∗): ∥z∥ ≤ b(⇒ ∥z∥ < b + 1) implies ∥f(z)∥ ≤ Ω(b + 1) and hence ∥f(z) − z∥ ≤ Ω(b + 1) + b. For 4., 5. and 6. we derive the various Ωs, under the assumptions ∥z∥, ∥f(z) − z∥ ≤ b, as follows:

If f is Lipschitz continuous with constant L > 0 and we assume ∥z̃∥ ≤ n, then using the triangle inequality and the aforementioned assumptions

∥f(z̃)∥ ≤ ∥f(z̃) − f(z)∥ + ∥f(z) − z∥ + ∥z∥
≤ L · ∥z̃ − z∥ + b + b
≤ L · (n + b) + 2b,

so f satisfies (∗∗) with Ω(n) := L · (n + b) + 2b. Likewise, one obtains that f Hölder-Lipschitz continuous with constants L, α satisfies (∗∗) with Ω(n) := L · (n + b)^{α} + 2b.

For f uniformly continuous functions with modulus ω the argument is similar to that in the hyperbolic case: assuming ∥z̃∥ ≤ n and using ∥z∥ ≤ b we obtain ∥z̃− z∥ ≤ n + b. Dividing the line segment between z̃, z into (n + b) · 2^{ω(0)} + 1 pieces of length < 2^{−ω(0)} we obtain ∥f(z̃) − f(z)∥ ≤ (n + b) · 2^{ω(0)} + 1. Thus we obtain

∥f(z̃)∥ ≤ ∥f(z̃) − f(z)∥ + ∥f(z) − z∥ + ∥z∥ ≤ (n + b) · 2^{ω(0)} + 2b + 1,

i.e. f satisfies (∗∗) with Ω(n) := (n+b)·2^{ω(0)}+2b+1 for uniformly continuous functions f with modulus ω.

As in the metric case, for weakly quasi-nonexpansive functions, the fixed point p is an additional parameter and we require the additional premise ∥p∥ ≤ b. For weakly quasi-nonexpansive functions f, we then obtain Ω(n) := n + 2b as follows:

∥z̃∥ ≤ n → ∥f(z̃)∥ ≤ ∥f(z̃)−p∥+∥p∥ ≤ ∥z̃−p∥+∥p∥ ≤ ∥z̃∥+∥p∥+∥p∥ ≤ n+2b.

At last, if f satisfies ∥z − f(z)∥ ≤ b and (∗) with an Ω_{0}, then f satisfies (∗∗) with Ω(n) := Ω_{0}(n + b) + b.

The result then follows from Theorem 6.3.

Remark 6.7. The previous remark 4.18 applies accordingly in the normed case.

Defining, in the setting of normed linear spaces, the notions of F ix(f) and F ix_{ε}(f, z, b) as before, we prove the following corollary.

Corollary 6.8. 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space) and let B_{∀} and C_{∃} be as before. If A^{ω}[X, ∥·∥, C]_{−b} proves a sentence

∀x ∈ P ∀y ∈ K∀z^{C}, f^{C→C}(f n.e. ∧ F ix(f) ≠ ∅∀u^{0}B_{∀} → ∃v^{0}C_{∃}),

then there exists a computable functional Φ^{1→0→0} (on representatives r_{x} : IN → IN of elements of P) s.t. for all r_{x} ∈ IN^{IN}, b ∈ IN

∀y ∈ K∀z^{C}, f^{C→C}(f n.e. ∧ ∀ε > 0F ix_{ε}(f, z, b) ≠ ∅ ∧∥z∥_{X}, ∥z − f(z)∥_{X} ≤_{IR} (b)_{IR} ∧ ∀u^{0} ≤ Φ(r_{x}, b)B_{∀} → ∃v^{0} ≤ Φ(r_{x}, b)C_{∃})

holds in all non-trivial normed linear spaces (X, ∥ · ∥) with nonempty convex subset C for which ∥c_{X}∥ ≤ b. If c_{X} does not occur in B_{∀}, C_{∃}, we can drop the requirement that ∥c_{X}∥ ≤ b. Analogously, for uniformly convex spaces (X, ∥·∥, C, η) and inner product spaces (X, ⟨·, ·⟩), where for uniformly convex spaces the bound Φ additionally depends on the modulus of uniform convexity η.

2. The corollary also holds if ‘f n.e.’ is replaced by f Lipschitz continuous, Hölder-Lipschitz continuous or uniformly continuous, where the extracted bound then will depend on the respective constants and moduli.

3. Considering the premise ‘f weakly quasi-nonexpansive’, i.e.

∃p^{C}(f(p) =_{X} p ∧ ∀w^{X}(∥f(p) − f(w)∥_{X} ≤_{IR} ∥p − w∥_{X}))

instead of ‘f n.e. ∧F ix(f) ≠ ∅’ we may weaken this premise to

∀ε > 0∃p^{C}(∥f(p) − p∥_{X} ≤_{IR} ε ∧ ∥z − p∥_{X} ≤_{IR} (b)_{IR}
∧∀w ∈ X(∥f(p) − f(w)∥_{X} ≤_{IR} ∥p − w∥_{X})).

4. Let Ψ : (X → X) → X → 1 be a provably extensional closed term of A^{ω}[X, ∥ · ∥, C]_{−b}, then in 1. and 2. instead of ‘F ix(f) ≠ ∅’ we may weaken ‘Ψ(f, p) =_{IR} 0’ expressing that Ψ(f, ·) has a root p to ‘∀ε > 0∃p ∈ X(∥z − p∥_{X} ≤_{IR} (b)_{IR} ∧ |Ψ(f, p)| ≤_{IR} ε)’, expressing that Ψ(f, ·) has ε-roots p which are b-close to z for every ε > 0.

Proof. This is essentially the same proof as for Corollary 4.22, except that b not only bounds the distance between z and f(z) and the diameter of the subset where ε-fixed points are to be found, but also the norm of z itself and the norm of the element c_{X} of the convex subset C. The result then follows using Corollary 6.6.

Similar to Corollary 5.2 we may also in the setting of normed linear spaces allow a Herbrand normal form version of the previous corollary, which allows one to weaken premises even though the conclusion is of a too general form to allow extraction of explicit bounds.

7 Simultaneous treatment of several spaces

The generalized approach to majorization developed in the previous section may also be extended to simultaneously cover finite collections of spaces. Instead of a single space X and a single element a ∈ X we may have a collection of spaces X_{1}, …, X_{n} and corresponding elements a_{i} ∈ X_{i} that we take as reference points for the majorization relation. We then may consider elements of products of these spaces and functions between such productelements.

T^{X_{1},...,X_{n}} is the set of all finite types ρ over the ground types 0, X_{1}, …, X_{n}. For ρ ∈ T^{X_{1},...,X_{n}} the type ρ̂ defines the type which results from ρ by replacing all occurrences of X_{i}, 1 ≤ i ≤ n by 0. The relation ≳\underline{a} is then defined as follows:

Definition 7.1. We define a ternary relation ≳\underline{a} ; ρ between objects x, y and an n-tuple \underline{a} of type ρ̂, ρ and X_{1}, …, X_{n} respectively as follows:

• x^{0} ≳\underline{a} ; 0 y^{0} :≡ x ≥_{0} y,

• x^{0} ≳\underline{a} ; X_{i} y^{X_{i}} :≡ (x)_{IR} ≥_{IR} d_{X_{i}}(y, a_{i}),

• x ≳\underline{a} ; ρ→τ y :≡ ∀z′, z(z′ ≳\underline{a} ; ρ z → xz′ ≳\underline{a} ; τ yz) ∧ ∀z′, z(z′ ≳\underline{a} ; ρ̂ z → xz′ ≳\underline{a} ; τ

xz).

If X_{i} is a normed linear spaces we require a_{i} = 0_{X_{i}} s.t. d_{X_{i}}(x, a_{i}) =_{IR} ∥x∥_{X_{i}}.

E.g. if we have two metric spaces (X_{1}, d_{X_{1}}) and (X_{2}, d_{X_{2}}) then an (a_{1}, a_{2})- majorant for f^{X_{1}→X_{2}} is a function f^{∗} of type 1 such that

∀n^{0}, x^{X_{1}}(d_{X_{1}}(x, a_{1}) ≤_{IR} (n)_{IR} → d_{X_{2}}(f(x), a_{2}) ≤_{IR} (f^{∗}(n))_{IR}).

If f is nonexpansive and a_{2} := f(a_{1}), then f is (a_{1}, a_{2})-majorized by the identity function λn.n^{0}.

Functions involving product types are treated using “currying” in the form of the following two patterns:

• a function f : X_{1} × … × X_{n} → ρ is represented by f : X_{1} → … → X_{n} → ρ,

• a function ρ → X_{1} × … × X_{n} is represented by an n-tuple of functions f_{i} : ρ → X_{i}.

Thus e.g. a function f : X_{1} × X_{2} → X_{1} × X_{2} will be represented by a pair f_{1,2} : X_{1} → (X_{2} → X_{1,2}). A function g : (X_{1} × X_{2} → X_{1} × X_{2}) → X_{1} × X_{2} by a pair g_{1,2} : (X_{1} → (X_{2} → X_{1})) → ((X_{1} → (X_{2} → X_{2})) → X_{1,2}) and similar for products of greater arity and functions of more complex types.

8 Applications

Application 8.1. Let (X, d, W) be an arbitrary (nonempty) hyperbolic space,

k ∈ IN, k ≥ 1 and (λ_{n})_{n∈IN} a sequence in [0, 1 − \frac{1}{k}] with ∑_{n=0}^{∞} λ_{n} = ∞ and

define for f : X → X, x ∈ X the Krasnoselski-Mann iteration (x_{n})_{n} starting from x ([26, 29]) by

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

In [11](Theorem 1) the following is proved^{16}

∀x ∈ X, f : X → X((x_{n})_{n} bounded and f n.e. → lim_{n→∞} d(x_{n}, f(x_{n})) = 0).

As observed in [2], it actually suffices to assume that (x_{n}^{∗})_{n} starting from some x^{∗} is bounded. Therefore

∀x ∈ X, f : X → X(∃x^{∗} ∈ X((x_{n}^{∗})_{n} bounded) and f n.e.

→ lim_{n→∞} d(x_{n}, f(x_{n})) = 0).

The proof given in [11] (and [2]) can easily be formalized in A^{ω}[X, d, W]_{−b} (see [22] for more details on this). As an application of Corollary 4.17 we obtain (see the proof below) the following effective and uniform version: There exists a computable bound Φ(k, α, b, l) such that in any (nonempty) hyperbolic space (X, d, W), for any l, b, k ∈ IN and any α : IN → IN the following holds: if (λ_{n}) is a sequence in [0, 1) such that

∀n ∈ IN(λ_{n} ≤ 1 − \frac{1}{k} ∧ n ≤ ∑_{i=0}^{α(n)} λ_{i})

then

\begin{matrix}∀x, x^{∗} ∈ X∀f : X → X( ∀i, j(d(x, x^{∗}), d(x_{i}^{∗}, x_{j}^{∗}) ≤ b) \\ ∧f n.e. → ∀m ≥ Φ(k, α, b, l)d(x_{m}, f(x_{m})) < 2^{−l}). \end{matrix}

Proof. As mentioned already, A^{ω}[X, d, W]_{−b} proves the following (formalized version of Theorem 1 in [11]): if k ≥ 1, λ_{(·)}^{0→1} represents an element of the compact Polish space [0, 1]^{∞} (with the product metric) and α : IN → IN such that

(∗) ∀n ∈ IN(λ_{n} ≤_{IR} 1 − \frac{1}{k} ∧ n ≤_{IR} ∑_{i=0}^{α(n)} λ_{i}),

where ∑_{i=0}^{α(n)} λ_{i} represents the corresponding summation of the real numbers in

[0, 1] represented by λ_{i}, then

∀l, b ∈ IN, x, x^{∗}, f^{X→X}( (x_{n}^{∗})_{n} b-bounded ∧f n.e.

→ ∃n ∈ IN(d_{X}(x_{n}, f(x_{n})) <_{IR} 2^{−l})),

16For the case of convex subsets C ⊆ X of normed linear spaces (X, ∥ · ∥) this result is already due to [13]. [11] even treats spaces of hyperbolic type.

where ‘(∗)’ and ‘(x_{n}^{∗})_{n} b-bounded’ are a ∀-formulas and ‘d_{X}(x_{n}, f(x_{n})) <_{IR} 2^{−l}’ is a ∃-formula.

Now Corollary 4.17 yields the existence of a computable functional Φ(k, α, b, l) such that for n := Φ(k, α, b, l)

\begin{matrix}∀(λ_{m}) ∈ [0, 1]^{∞}∀x, x^{∗} ∈ X∀f : X → X((∗) ∧ ∀i, j(d(x, f(x)), d(x, x^{∗}), \\ d(x_{i}^{∗}, x_{j}^{∗}) ≤ b) ∧ f n.e. → ∃m ≤ n(d(x_{m}, f(x_{m})) < 2^{−l})) \end{matrix}

holds for all k, α, b, l in any (nonempty) hyperbolic space (X, d, W).

Since (d(x_{n}, f(x_{n})))_{n} is a non-increasing sequence ([11]) the conclusion actually implies

∀m ≥ Φ(k, α, b, l)(d(x_{m}, f(x_{m})) < 2^{−l}).

The only thing which remains to show is that the assumption ‘d(x, f(x)) ≤ b’ is redundant: by Theorem 1 from [11] we know, in particular, that d(x_{n}^{∗}, f(x_{n}^{∗})) → 0 and so a-fortiori

∃n ∈ IN(d(x_{n}^{∗}, f(x_{n}^{∗})) ≤ b).

Using d(x, x^{∗}), d(x_{i}^{∗}, x_{j}^{∗}) ≤ b for all i, j and the nonexpansivity of f yields

\begin{matrix}d(x, f(x)) ≤ \\ d(x, x^{∗}) + d(x^{∗}, x_{n}^{∗}) + d(x_{n}^{∗}, f(x_{n}^{∗})) + d(f(x_{n}^{∗}), f(x^{∗})) + d(f(x^{∗}), f(x)) ≤ 5b. \end{matrix}

So replacing ‘b’ in the bound by ‘5b’ we can drop the assumption ‘d(x, f(x)) ≤ b’.

As a corollary it follows, that for bounded hyperbolic spaces (X, d, W) the convergence d(x_{n}, f(x_{n})) → 0 is uniform in x, f and – except for a bound b on the metric – in (X, d, W). This corollary was first proved as Theorem 2 in [11]^{17} and was shown to follow from a general logical metatheorem in [22] where a detailed discussion of this point is given. In [24], the extraction of an actual effective uniform rate of convergence was carried out and it was noticed that the assumption on X to be bounded could be weakened to a bound b on d(x, x^{∗}) and (x_{n}^{∗})_{n} for some x^{∗} ∈ X. At that time, there was no explanation in terms of a general result from logic for the fact that these local bounds where sufficient. This latter fact can now for the first time be explained by our refined logical metatheorems as well. Note that the proof of Theorem 2 in [11] (as well as the alternative proof for constant λ_{n} = λ ∈ (0, 1) given in [15]) crucially uses that the whole space X is assumed to be bounded. So the uniformity result guaranteed a-priorily by the metatheorems of the present paper applied to Theorem 1 of [11] not only yields immediately Theorem 2 from [11] (called ‘main result’) but even a qualitatively stronger uniformity which apparently cannot be obtained by the functional analytic embedding techniques used in [11] (or in [15]).

17For the case of bounded convex subsets of normed spaces and constant λ_{n} = λ ∈ (0, 1)

the uniformity in x was already shown in [7] and – for (λ_{n})_{n} in [a, b] ⊂ (0, 1) and nonincreasing – in [5].

The aforementioned explicit bound extracted in [24](see theorem 3.21 and remark 3.13) is as follows (for the case of convex subsets of normed linear spaces the result is due already to [19, 20]):

Φ(k, α, b, l) := α̂(⌈12b · exp(k(M + 1))⌉ − 1, M)), where

M := (1 + 6b) · 2^{l}, α̂(0, n) := α̃(0, n), α̂(i + 1, n) := α̃(α̂(i, n), n), with α̃(i, n) := i + α^{+}(i, n), where α^{+}(i, n) := max_{j≤i}[α(n + j) − j + 1].

Before we come to the next application we need the following

Proposition 8.2 ([13, 11]). Let (X, d, W) be a (nonempty) compact hyperbolic space and (λ_{n}), f, (x_{n}) as in application 8.1. Then (x_{n})_{n} converges towards a fixed point of f (see [21] for details).

Proof. By the result mentioned in application 8.1 we have that d(x_{n}, f(x_{n})) → 0 since the compactness of X implies that X – and hence (x_{n})_{n} – is bounded. Using again the compactness of X, we know that (x_{n})_{n} has a convergent subsequence (x_{n_{k}})_{k} with limit x̂. One easily shows (using the continuity of f) that x̂ is a fixed point of f. The proof is concluded by verifying the easy fact that for any fixed point x̂ of f

∀n ∈ IN(d(x_{n+1}, x̂) ≤ d(x_{n}, x̂))

which implies that already (x_{n})_{n} converges towards x̂.

In particular it follows that (x_{n})_{n} is a Cauchy sequence and for this corollary one does not need the completeness of X but only its total boundedness: suppose X is totally bounded. Then its metric completion X̂ (which again is a hyperbolic space) is totally bounded too and hence compact. f extends to a nonexpansive function f̂ on the completion so that the previous result applies. Since f̂ coincides with f on X, also the Krasnoselski-Mann iteration of f̂ coincides with that of f when starting from a point x ∈ X. Hence we conclude that (x_{n})_{n} is a Cauchy sequence.

Application 8.3. Let us consider the proof of the Cauchy property of (x_{n}) from the asymptotic regularity (i.e. d(x_{n}, f(x_{n})) → 0) (taken as assumption)^{18} under the additional assumption of X being totally bounded, i.e. the proof of

(+) X totally bounded ∧ lim d(x_{n}, f(x_{n})) = 0 ∧ f n.e. → ∀k ∈ IN∃n ∈ IN∀m ≥ n(d(x_{n}, x_{m}) ≤ 2^{−k})

which can be formalized in A^{ω}[X, d, W]_{−b}.

In order to apply Corollary 4.17 we first have to modify (+) so that the logical form required in the corollary is obtained. In order to do so we first have to make the assumptions explicit:

• due to the fact that d(x_{n}, f(x_{n}))_{n} is non-increasing, we can write the asymptotic regularity equivalently as ∀l ∈ IN∃n ∈ IN(d(x_{n}, f(x_{n})) ≤ 2^{−l}) which asks for a witnessing rate of asymptotic regularity δ : IN → IN such that

(1) ∀l ∈ IN(d(x_{δ(l)}, f(x_{δ(l)})) ≤ 2^{−l}).

• the total boundedness of X is expressed by the existence of a sequence (a_{n})_{n} of points in X and a function γ : IN → IN such that

(2) ∀l ∈ IN, x ∈ X∃n ≤ γ(l)(d(x, a_{n}) ≤ 2^{−l}).

A function γ such that a sequence (a_{n})_{n} in X satisfying (2) exists is called a modulus of total boundedness for X.

It is important to notice that both (1) and (2) are (provably equivalent to) ∀-formulas.

18The proof relative to this assumption only uses that (λ_{n})_{n} is a sequence in [0, 1] but not the other assumptions on (λ_{n})_{n} (which are only needed to prove that d(x_{n}, f(x_{n})) → 0).

The conclusion, i.e. the Cauchy property of (x_{n}), is a Π_{3}^{0}-formula and so too complicated to be covered by our metatheorems. In fact, as shown in [21] there is no Cauchy rate computable in the parameters even for a very simple computable sequence of nonexpansive functions on X = [0, 1] and λ_{n} = \frac{1}{2}. We therefore modify the conclusion to its Herbrand normal form^{19}

(H) ∀l ∈ IN∀g : IN → IN∃n ∈ IN∀i, j ∈ [n; n + g(n)](d(x_{i}, x_{j}) < 2^{−l}),

where [n; m] denotes the subset {n, n + 1, …, m − 1, m} of IN for m ≥ n.

Classically, (H) is a equivalent to the Cauchy property for (x_{n})_{n} but – since the proof is ineffective – a computable bound on (H) does not yield a computable Cauchy modulus for (x_{n})_{n}. Note that

∃n ∈ IN∀i, j ∈ [n; n + g(n)](d(x_{i}, x_{j}) < 2^{−l})

is (equivalent to) an ∃-formula.

A^{ω}[X, d, W]_{−b} proves that

\begin{matrix}∀(λ_{m}) ∈ [0, 1]^{∞}∀x^{X}∀f^{X→X}, (a_{n})^{0→X}, l^{0}, γ^{1}, δ^{1}, g^{1} \\ ((1) ∧ (2) ∧ f n.e. → ∃m ∈ IN∀i, j ∈ [m; m + g(m)](d(x_{i}, x_{j}) < 2^{−l})). \end{matrix}

The total boundedness of X implies that the metric of X is bounded and a bound can be computed by b := max{d(a_{i}, a_{j}) : i, j ≤ γ(0)} + 2. However, in order to guarantee our result to be independent from (a_{n})_{n} we add a bound b of X as an additional input. Hence by Corollary 4.14 we obtain a computable bound n := Ω(l, b, γ, δ, g) such that for all (λ_{n}) in [0, 1], x ∈ X, (a_{n}) in X, f : X → X, l ∈ IN and γ, δ, g : IN → IN :

(1) ∧ (2) ∧ f n.e. → ∃m ≤ n∀i, j ∈ [m; m + g(m)](d(x_{i}, x_{j}) < 2^{−l})

holds in any (nonempty) b-bounded, totally bounded (with modulus γ) hyperbolic space (X, d, W).

A concrete bound Ω of this kind has in fact been extracted first in [21], where there extraction itself was guided by the algorithm provided by the proof of Corollary 4.14 as well as the proof-theoretic study of the Bolzano-Weierstraß principle carried out in [17]. This concrete Ω even is independent from b and is defined as follows

19More precisely, the Herbrand normal form of a slightly different but trivially equivalent formulation of the Cauchy property.

Ω(l, g, δ, γ) := max_{i≤γ(l+3)} Ψ_{0}(i, l, g, δ),

where

Ψ_{0}(0, l, g, δ) := 0

Ψ_{0}(n + 1, l, g, δ) := δ (l + 2 + ⌈log_{2}(max_{i≤n} g(Ψ_{0}(i, l, g, δ)) + 1)⌉) .

For X being b-bounded and (λ_{n}) s.t. λ_{i} ∈ [0, 1 − \frac{1}{k}], ∑_{i=0}^{α(n)} λ_{i} ≥ n, we can take

δ(l) := Φ(k, α, b, l) from application 8.1.

Application 8.4. Let (X, d, W), k, (λ_{n}), f, x and (x_{n}) be as in application 8.1. In [2], the following result is proved:

∀x ∈ X, f : X → X(f n.e. → lim_{n→∞} d(x_{n}, f(x_{n})) = r(f)),

where r(f) := inf_{y∈X} d(y, f(y)) is the so-called minimal displacement of f. As

(x_{n}) is no longer assumed to be bounded, r(f) can very well be strictly positive: e.g. for IR (with the natural metric) and f : IR → IR, f(x) := x + 1 we have r(f) = 1 although f is nonexpansive.

The above theorem can be written equivalently as follows (using again that (d(x_{n}, f(x_{n}))) is non-increasing):^{20}

∀l ∈ IN∀x, x^{∗} ∈ X, f : X → X∃n ∈ IN(d(x_{n}, f(x_{n})) < d(x^{∗}, f(x^{∗})) + 2^{−l}).

The proof given in [2] can be formalized in A^{ω}[X, d, W]_{−b} and so Corollary 4.17 yields (like in the proof of application 8.1 above) an effective bound n := Ψ(k, α, b, l) such that in any (nonempty) hyperbolic space (X, d, W), for

any l, b, k ∈ IN and any α : IN → IN such that λ_{n} ≤ \frac{1}{k} and n ≤ ∑_{i=0}^{α(n)} λ_{i} the

following holds

\begin{matrix}∀x, x^{∗} ∈ X∀f : X → X(d(x, x^{∗}), d(x, f(x)) ≤ b \\ ∧f n.e. → ∃k ≤ n(d(x_{k}, f(x_{k})) < d(x^{∗}, f(x^{∗})) + 2^{−l})) \end{matrix}

20For details see [20].

and so (by the fact that d(x_{n}, f(x_{n}))_{n} is non-increasing)

\begin{matrix}∀x, x^{∗} ∈ X∀f : X → X( d(x, x^{∗}), d(x, f(x)) ≤ b \\ ∧f n.e. → ∀m ≥ Ψ(k, α, b, l)(d(x_{m}, f(x_{m})) < d(x^{∗}, f(x^{∗})) + 2^{−l})). \end{matrix}

An explicit such bound Ψ (which is very similar to the bound Φ mentioned in connection with application 8.1) has been extracted first in [24] (for the special case of convex subsets of normed spaces this is already due to [19] and – in a stronger form – in [20]). Our refined metatheorems for the first time allow one to explain this finding as an instance of a general result in logic.

9 Proofs of Theorems 4.10 and 6.3

We focus on proving Theorems 4.10 and 6.3 for the theories A^{ω}[X, d, W]_{−b} and A^{ω}[X, ∥·∥, C]_{−b} respectively. From these proofs, the corresponding proofs for the other variants of the theories for metric and normed linear spaces can easily be obtained by treating one of the following kinds of extensions: (1) adding another purely universal axiom to the theory (purely universal axioms are their own functional interpretation), e.g. for A^{ω}[X, d, W, CAT (0)]_{−b}, or (2) adding a new majorizable constant to the language as e.g. for A^{ω}[X, ∥ · ∥, C, η]_{−b}, where the modulus of uniform convexity η is given as a number theoretic function η : IN → IN.

The proofs of Theorems 4.10 and 6.3 closely follow the general proof outline in [22], but both the interpretation of the theories A^{ω}[X, d, W]_{−b}, A^{ω}[X, ∥ · ∥, C]_{−b} by bar-recursive functionals and the subsequent interpretation of these functionals in an extension of the Howard-Bezem strongly majorizable functionals to all types T^{X} are now parametrized by an element a ∈ X for the relation ≳^{a}. For the interpretation of A^{ω}[X, d, W]_{−b} by barrecursive functionals this in effect leads to a family of functional interpretations parametrized by a ∈ X, where the interpretation of the element a ∈ X is fixed later during the majorization process (see Remark 9.11). For A^{ω}[X, ∥ · ∥, C]_{−b} the choice a = 0_{X} is fixed from the beginning.

Based on ≳^{a} we redefine Kohlenbach’s [22] extension of Bezem’s[1] type structure of hereditarily strongly majorizable set-theoretical functionals to all types T^{X} (based on ≳^{a} instead of s-maj) as follows:

Definition 9.1. Let (X, d) be a metric space, resp. (X, ∥·∥) a (real) normed linear space, and let a ∈ X be given. The extensional type structure M^{ω,X} of all hereditarily strongly a-majorizable set-theoretic functionals of type ρ ∈ T^{X} over IN and X is defined as

M_{0} := IN, n ≳_{0}^{a} m :≡ n ≥ m ∧ n, m ∈ IN,
M_{X} := X, n ≳_{X}^{a} x :≡ n ≥ d(x, a) ∧ n ∈ M_{0}, x ∈ M_{X},

where ≥ is the usual order on IR.

x^{∗} ≳_{ρ→τ}^{a} x :≡ x^{∗} ∈ M Mρ̂ ; τ̂ ∧ x ∈ M_{τ}^{M_{ρ}}

∧ ∀y^{∗} ∈ Mρ̂, y ∈ M_{ρ} (y^{∗} ≳_{ρ}^{a} y → x^{∗}y^{∗} ≳_{τ}^{a} xy)

∧ ∀y^{∗}, y ∈ Mρ̂ (y^{∗} ≳a ; ρ̂ y → x^{∗}y^{∗} ≳a ; τ̂ x^{∗}y),

M_{ρ→τ} := {x ∈ M_{τ}^{M_{ρ}} | ∃x^{∗} ∈ M Mρ̂ ; τ̂ : x^{∗} ≳_{ρ→τ}^{a} x} (ρ, τ ∈ T^{X}) .

Remark 9.2. Restricted to the types T, this type structure is identical to Bezem’s original type structure M^{ω} of strongly hereditarily majorizable functionals, as for ρ ∈ T the relations s-maj_{ρ} and ≳_{ρ}^{a} are the same and hence for ρ ∈ T we may freely write s-maj_{ρ} instead of ≳_{ρ}^{a}, as here the parameter a ∈ X is irrelevant.

Even though the a-majorization relation is parametrized by an element a ∈ X, the resulting model of all hereditarily strongly a-majorizable functionals is independent of the choice of a ∈ X, as the following lemma shows:

Lemma 9.3. Let a, b ∈ X be given. Then for every ρ ∈ T^{X} there is a mapping Φ_{ρ} of type ρ̂ → 0 → ρ̂ s.t. for all x^{∗} ∈ M a ; ρ̂, x ∈ M_{ρ}^{a} and all n ∈ IN s.t. d(a, b) ≤ n,

x^{∗} ≳_{ρ}^{a} x → Φ_{ρ}(x^{∗}, n) ≳_{ρ}^{b} x,

and for all x^{∗}, x̂ ∈ M a ; ρ̂

x^{∗} s-majρ̂ x̂ → Φ_{ρ}(x^{∗}, n) s-majρ̂ Φ_{ρ}(x̂, n).

In particular: M_{ρ}^{a} = M_{ρ}^{b} and – trivially – M a ; ρ̂ = M b ; ρ̂. Note, that this property is symmetric in a, b ∈ X.

Proof. The proof is by induction on the type ρ ∈ T^{X}.

For ρ = 0 define Φ_{0}(x, n) := x. Trivially M_{0}^{a} = M_{0}^{b} by definition.

For ρ = X the mapping Φ_{X} is the mapping Φ_{X}(x^{∗}, n) = x^{∗} +n, as x^{∗} ≳_{X}^{a} x is equivalent to x^{∗} ≥ d(x, a) but then by the triangle inequality x^{∗} +n ≥ d(x, b) and hence x^{∗} + n ≳_{X}^{b} x. Obviously, M_{X}^{a} = M_{X}^{b}.

For ρ = σ → τ, we need to construct the mapping Φ_{σ→τ} and show that x ∈ M_{σ→τ}^{a} implies x ∈ M_{σ→τ}^{b}. Assume x^{∗} ≳_{σ→τ}^{a} x for x ∈ M_{σ→τ}^{a}, and let y^{∗} ∈ Mσ̂ and y ∈ M_{σ} be given such that y^{∗} ≳_{σ}^{b} y. By the induction hypothesis for σ there is a Φ_{σ} such that, using the symmetry in a and b, Φ_{σ}(y^{∗}, n) ≳_{σ}^{a} y. Next, by the definition of ≳_{σ→τ}^{a} we have that x^{∗}(Φ_{σ}(y^{∗}, n)) ≳_{τ}^{a} xy. But then by the induction hypothesis for τ there is a mapping Φ_{τ} such that

Φ_{τ}(x^{∗}Φ_{σ}(y^{∗}, n), n) ≳_{σ}^{b} xy.

Also for y^{∗} s-majσ̂ ŷ we have by I.H. that Φ_{σ}(y^{∗}, n) s-majσ̂ Φ_{σ}(ŷ, n) and so for x^{∗} s-majρ̂ x̂ we get x^{∗}(Φ_{σ}(y^{∗}, n)) s-majτ̂ x̂(Φ_{σ}(ŷ, n)) which in turn implies that Φ_{τ}(x^{∗}(Φ_{σ}(y^{∗}, n))) s-majτ̂Φ_{τ}(x̂(Φ_{σ}(ŷ, n))). The desired Φ_{σ→τ} is then obtained by λ-abstracting x^{∗} and y^{∗}. In particular, λy^{∗}.Φ_{τ}(x^{∗}Φ_{σ}(y^{∗}, n), n) is a bmajorant for x and hence x ∈ M_{σ→τ}^{b}.

Remark 9.4. Even though it is independent of the choice of a ∈ X whether or not a certain functional is a-majorizable, the complexity and possible uniformities of the majorants depend crucially on the choice of a ∈ X. In particular, for normed linear spaces a-majorants for a ≠ 0_{X} will usually depend on an upper bound n ≥ ∥a∥ and hence will not have the uniformity w.r.t. a that we aim for in our applications.

We also need the following lemmas:

Lemma 9.5. x^{∗} ≳_{ρ}^{a} x → x^{∗} ≳a ; ρ̂ x^{∗} for all ρ ∈ T^{X}.

Proof. By induction on ρ using that by definition of ≳^{a} if x^{∗} ≳_{ρ→τ}^{a} x then

∀z^{∗}, z(z^{∗} ≳a ; ρ̂ z → x^{∗}z^{∗} ≳a ; τ̂ x^{∗}z).

Lemma 9.6. Let ρ = ρ_{1} → … → ρ_{k} → τ. Then x^{∗} ≳_{ρ}^{a} x iff

(I) ∀y_{1}^{∗}, y_{1}, …, y_{k}^{∗}, y_{k}( ⋀_{i=1}^{k}(y_{i}^{∗} ≳_{ρ_{i}}^{a} y_{i}) → x^{∗}y_{1}^{∗} … y_{k}^{∗} ≳_{τ}^{a} xy_{1} … y_{k}) and

(II) ∀y_{1}^{∗}, y_{1}, …, y_{k}^{∗}, y_{k}( ⋀_{i=1}^{k}(y_{i}^{∗} ≳a ; ρ̂_{i} y_{i}) → x^{∗}y_{1}^{∗} … y_{k}^{∗} ≳a ; τ̂ x^{∗}y_{1} … y_{k}).

Proof. By induction on k. The case k = 1 follows from the definition of ≳^{a}. k = n + 1: Let τ_{0} = ρ_{n+1} → τ. For ‘⇒’, we have by induction hypothesis

∀y_{1}^{∗}, y_{1}, … y_{n}^{∗}, y_{n}( ⋀_{i=1}^{n}(y_{i}^{∗} ≳_{ρ_{i}}^{a} y_{i}) → x^{∗}y_{1}^{∗} … y_{n}^{∗} ≳_{τ_{0}}^{a} xy_{1} … y_{n}).

Now assume y_{n+1}^{∗} ≳_{ρ_{n+1}}^{a} y_{n+1} then by definition of ≳^{a}

x^{∗}y_{n}^{∗} … y_{n}^{∗}y_{n+1}^{∗} ≳_{τ}^{a} xy_{1} … y_{n}y_{n+1},

so (I) follows. (II) can be treated analogously. For ‘⇐’, assume

∀y_{1}^{∗}, y_{1}, … y_{n+1}^{∗}, y_{n+1}( ⋀_{i=1}^{n+1}(y_{i}^{∗} ≳_{ρ_{i}}^{a} y_{i}) → x^{∗}y_{1}^{∗} … y_{n+1}^{∗} ≳_{τ}^{a} xy_{1} … y_{n+1})

and

∀y_{1}^{∗}, y_{1}, … y_{n+1}^{∗}, y_{n+1}( ⋀_{i=1}^{n+1}(y_{i}^{∗} ≳a ; ρ̂_{i} y_{i}) → x^{∗}y_{1}^{∗} … y_{n+1}^{∗} ≳a ; τ̂ x^{∗}y_{1} … y_{n+1}).

We need to show that under these assumptions (1) x^{∗}y_{1}^{∗} … y_{n}^{∗} ≳_{τ_{0}}^{a} xy_{1} … y_{n} and (2) x^{∗}y_{1}^{∗} … y_{n}^{∗} ≳a ; τ̂_{0} x^{∗}y_{1} … y_{n} hold, then using the induction hypothesis we are done. There are three cases to check:

(1a) ⋀_{i=1}^{n+1} y_{i}^{∗} ≳_{ρ_{i}}^{a} y_{i} → (x^{∗}y_{1}^{∗} … y_{n}^{∗})y_{n+1}^{∗} ≳_{τ}^{a} (xy_{1} … y_{n})y_{n+1},

(1b) ⋀_{i=1}^{n+1} y_{i}^{∗} ≳a ; ρ̂_{i} y_{i} → (x^{∗}y_{1}^{∗} … y_{n}^{∗})y_{n+1}^{∗} ≳a ; τ̂ (x^{∗}y_{1}^{∗} … y_{n}^{∗})y_{n+1},

(2) ⋀_{i=1}^{n+1} y_{i}^{∗} ≳a ; ρ̂_{i} y_{i} → (x^{∗}y_{1}^{∗} … y_{n}^{∗})y_{n+1}^{∗} ≳a ; τ̂ (x^{∗}y_{1} … y_{n})y_{n+1},

(1a) and (2) hold by assumption, (1b) follows from (1a) using Lemma 9.5.

We need following (primitive recursive) functionals for the types ρ ∈ T whose definitions we recall here:

Definition 9.7. For ρ = ρ_{1} → … → ρ_{k} → 0 ∈ T we define max_{ρ} by

max_{ρ}(x, y) := λv_{1}^{ρ}, …, v_{k}^{ρ_{k}}. max_{IN}(x\underline{v}, y\underline{v})

For types 0 → ρ with ρ = ρ_{1} → … → ρ_{k} → 0, we define functionals (·)^{M} of types (0 → ρ) → 0 → ρ by :

x^{M}(y^{0}) := λ\underline{v}\underline{ρ}. max_{IN}\{x(i, \underline{v}) | i = 1, …, y\}.

The next lemma is easy:

Lemma 9.8. If ∀n(x^{∗}(n) ≳_{ρ}^{a} x(n)) then (x^{∗})^{M} ≳_{0→ρ}^{a} x.

We now prove Theorem 4.10. We focus on hyperbolic spaces (X, d, W) and the corresponding theory A^{ω}[X, d, W]_{−b}. The case of ordinary metric spaces (X, d) follows by simply omitting the axioms concerning W, while for CAT(0) spaces we merely need to consider the additional purely universal axiom CN^{−}. The next lemma is an adaptation of the corresponding result from [22] and states that A^{ω}[X, d, W]_{−b} has (via its so-called negative translation) a Gödel functional interpretation in A^{ω}[X, d, W]_{−b} − {QF-AC} (actually even without DC and in a quantifier-free fragment of this theory) augmented by the schema (BR) of simultaneous bar recursion in all types of T^{X} (for A^{ω} this fundamental result is due to [33] (see [27] for a comprehensive treatment) which extends [10], where functional interpretation was introduced). Let A^{ω}[X, d, W]_{−b}^{−} := A^{ω}[X, d, W]_{−b} \ {QF-AC}. Analogously, we define A^{ω}[X, ∥ · ∥, C]_{−b}^{−} := A^{ω}[X, ∥ · ∥, C]_{−b} \ {QF-AC} etc.

Lemma 9.9 ([22]). Let A be a sentence in the language of A^{ω}[X, d, W]_{−b}. Then the following rule holds:

A^{ω}[X, d, W]_{−b} ⊢ A

⇒ one can construct a tuple of closed terms \underline{t} of A^{ω}[X, d, W]_{−b}+(BR) s.t. A^{ω}[X, d, W]_{−b}^{−} + (BR) ⊢ ∀\underline{y} (A′)_{D}(\underline{t}, \underline{y}).

where A′ is the negative translation of A and (A′)^{D} ≡ ∃\underline{x}∀\underline{y}(A′)_{D}(\underline{x}, \underline{y}) is the Gödel functional interpretation of A′.

Proof. This is Lemma 4.4 in [22],^{21} except that we have one less purely universal axiom to interpret: the axiom that the metric of (X, d, W) is bounded by b. Also, as discussed in Section 2 the axioms concerning the hyperbolic function have been reformulated to implicitly satisfy W_{X}(x, y, λ) =_{X} W_{X}(x, y, λ̃). Recall that, in general, purely universal axioms not containing ∨, such as the additional axioms for metric, hyperbolic and CAT(0) spaces, are interpreted by themselves.

Lemma 9.10. Let (X, d, W) be a nonempty hyperbolic space. Then M^{ω,X} is a model of A^{ω}[X, d, W]_{−b}^{−} +(BR) (for a suitable interpretation of the constants of A^{ω}[X, d, W]_{−b}^{−} +(BR) in M^{ω,X}), where we may interpret 0_{X} by an arbitrary element a ∈ X.

Moreover, for any closed term t of A^{ω}[X, d, W]_{−b}^{−} +(BR) one can construct a closed term t^{∗} of A^{ω} +(BR) – so in particular t does not contain the constants 0_{X}, d_{X} and W_{X} – such that

M^{ω,X} ⊧ ∀a^{X}∀n^{0}((n)_{IR} ≥ d(0_{X}, a) → t^{∗}(n) ≳^{a} t).

In particular, if we interpret 0_{X} by a ∈ X, then it holds in M^{ω,X} that t^{∗}(0^{0}) is an a-majorant of t

Proof. The constants of A^{ω}[X, d, W]_{−b}^{−} +(BR) are interpreted as in [22], so next we need to show that all these functionals are in M^{ω,X} by constructing a-majorants. To show that we can construct a suitable a-majorant t^{∗} for any closed term t of A^{ω}[X, d, W]_{−b}^{−} +(BR) it suffices to describe a-majorants for the constants of A^{ω}[X, d, W]_{−b}^{−} +(BR).

We first describe the (trivially uniform) a-majorants for the constants of classical analysis A^{ω}, which now are taken over the extended set of types T^{X}. Using Lemma 9.6 one easily verifies that:

• 0 ≳_{0}^{a} 0, • S ≳_{1}^{a} S,

21Correction to [22]: lemma 4.4 of [22] is stated with A^{ω}[X, d, W]+(BR) instead of A^{ω}[X, d, W] \ {QF-AC}+(BR) in the conclusion but the lemma also holds of course with the weaker theory as QF-AC disappears – as is well-known – during the functional interpretation. This is in fact needed since lemma 4.7 in [22] (corresponding to our lemma 9.10)

does not hold for A^{ω}[X, d, W]+(BR) as stated but only for A^{ω}[X, d, W]\{QF-AC}+(BR).

Analogously on p. 122, line 7.

• Π_{ρ̂,τ̂} ≳^{a} Π_{ρ,τ},

• Σ_{σ̂,ρ̂,τ̂} ≳^{a} Σ_{σ,ρ,τ}.

To produce a-majorants for the recursor \underline{R} and the bar-recursor \underline{B}^{22}, we only need the functional max_{ρ} defined for all types ρ ∈ T. As a-majorants for R and B only operate on the types T, we do not need to extend max_{ρ} to the types T^{X} as it was done in [22].

By induction on n and using Lemma 9.6 one easily proves ∀n(Rρ̂n ≳_{ρ}^{a} R_{ρ}n) and hence by Lemma 9.8 RM ; ρ̂ ≳_{ρ}^{a} R_{ρ}.

The majorant for the bar-recursor B is defined as

sB_{ρ,τ}^{∗} := λx, z, u, n, y.(B_{ρ,τ}x^{M}zu_{z})^{M}ny,

where x^{M}(y^{0→ρ}) := x(y^{M}) and u_{z} := λv, n, y. max(zny^{M}, uvny^{M}). As the defining axioms of B involve 0_{X}, we here assume a = 0_{X}, though by Lemma 9.3 given a bound on d(a, 0_{X}) we may transform this majorant into a majorant for any choice of a. If 0_{X} does not occur, such that we may interpret 0_{X} by a ∈ X, the dependency on 0_{X}, resp. a bound on d(a, 0_{X}) disappears.

The crucial step in proving B_{ρ̂,τ̂}^{∗} ≳^{0_{X}} B_{ρ,τ} is to establish the following: let x^{∗}, z^{∗}, u^{∗}, x, z, u, x̂, ẑ, û be given s.t. x^{∗} ≳_{α} x, x^{∗} ≳α̂ x̂, z^{∗} ≳_{β} z, z^{∗} ≳β̂ ẑ, u^{∗} ≳_{γ} u and u^{∗} ≳γ̂ û, where α, β and γ are determined by ρ and τ. Then

(+) ∀y ∈ M_{0→ρ̂}∀n^{0}Q(\overline{y, n}; n),

where Q(\overline{y, n}; n) :≡

\{ \begin{matrix}∀y^{∗}, ỹ, ˆ ỹ ∈ M^{ω,X}(∀k(y^{∗}k ≳_{ρ} ỹk ∧ y^{∗}k ≳ρ̂ ˆ ỹk) ∧ \overline{y^{∗}, n} =_{0→ρ̂} \overline{y, n} ⇒ \\ B^{+}x^{∗}z^{∗}u^{∗}ny^{∗} ≳_{τ} Bxzunỹ ∧ \\ B^{+}x^{∗}z^{∗}u^{∗}ny^{∗} ≳τ̂ B^{+}x^{∗}z^{∗}u^{∗}nˆỹ, B^{+}x̂ẑûnˆỹ), \end{matrix}

22As in [22], our formal systems are formulated with simultaneous recursion \underline{R} and simultaneous bar-recursion \underline{B}, both of which can be defined primitive recursively in ordinary recursion R and ordinary bar-recursion B. For convenience we will only discuss the ordinary recursors R and B. See [22] for a detailed discussion.

where B_{ρ,τ}^{+} := λx, z, u, n, y.B_{ρ,τ}x^{M}zu_{z}ny. By Lemma 9.6 and 9.8 it then follows that B^{∗} ≳ B and B^{∗}, B ∈ M^{ω,X}.

The proof of (+) uses the following form of dependent choice, also called bar induction (which holds in M^{ω,X} since by lemma 9.8 we have M_{0→ρ} = (M_{ρ})^{IN}):

\{ \begin{matrix}∀y ∈ M_{0→ρ̂}∃n_{0} ∈ IN∀n ≥ n_{0} Q(\overline{y, n}; n) ∧ \\ ∀y ∈ M_{0→ρ̂}, n ∈ IN(∀D ∈ Mρ̂ Q(\overline{y, n} ∗ D; n + 1) → Q(\overline{y, n}; n)) \\ → ∀y ∈ M_{0→ρ̂}, n_{0} ∈ INQ(\overline{y, n}; n). \end{matrix}

For the additional constants of A^{ω}[X, d, W]_{−b}^{−} we define the following amajorants:

• n^{0} ≳^{a} 0_{X} for every n with (n)_{IR} ≥_{IR} d_{X}(a, 0_{X}), where as just mentioned we can take n := 0 if we interpret 0_{X} by a,

• 0^{0} ≳^{a} a, since d_{X}(a, a) =_{IR} (0)_{IR},

• λx^{0}, y^{0}.((x + y)_{IR})_{∘} ≳^{a} d_{X}^{X→X→1},^{23}

• λz^{1}, x^{0}, y^{0}. max_{0}(x, y) ≳^{a} W_{X}^{1→X→X→X}.

The a-majorants for 0_{X} and a are obvious. The a-majorant for d_{X} follows from the triangle inequality: assume n_{1} ≳^{a} x and n_{2} ≳^{a} y then

d(x, y) ≤ d(x, a) + d(y, a) ≤ n_{1} + n_{2}.

Hence, as in the model M^{ω,X} the expression d_{X}(x, y) is interpreted by (d(x, y))_{∘} (see [22]) and by Lemma 4.6 n_{1} + n_{2} ≥_{IR} d(x, y) implies (n_{1} + n_{2})_{∘} s-maj_{1}d(x, y))_{∘}, the validity of the a-majorant for d_{X} follows.

Finally, the a-majorant for W_{X} can be justified by the first axiom for hyperbolic spaces:

∀x^{X}, y^{X}, z^{X}∀λ^{1}(d_{X}(z, W_{X}(x, y, λ)) ≤_{IR} (1 −_{IR} λ̃)d_{X}(z, x) +_{IR} λ̃d_{X}(z, y)),

The construction λ̃ turns representatives λ of arbitrary real numbers into representatives λ̃ of real numbers in the interval [0, 1]. Hence we may reason that d_{X}(z, W_{X}(x, y, λ)) is less than the maximum of d_{X}(z, x) and d_{X}(z, y) and hence less than the maximum of respective upper bounds on d_{X}(z, x) and d_{X}(z, y). Note that without the reformulation of axioms (4)-(7) for hyperbolic spaces discussed in Section 2 (see Remark 2.6), this reasoning only holds in the model M^{ω,X} (in which W_{X}(x, y, λ) is interpreted by W (x, y, rλ̃), where W is the function of the hyperbolic space (X, d, W) and rλ̃ is the real number in [0, 1] represented by λ̃) whereas now it is even provable in A^{ω}[X, d, W]_{−b}.

23Here we refer to remark 4.5.

Note, that the a-majorants for d_{X}, W_{X} are uniform, i.e. they do not depend on a. The a-majorant for a also does not depend on a, other than the requirement that the variable a and the element a in ≳^{a} denote the same element. Only the a-majorant for 0_{X} depends on a. Also note, that the (·)_{∘}- operator, which is ineffective in general, only is applied to natural numbers, where it is effectively (even primitive recursively) computable.

Thus given a closed term t of A^{ω}[X, d, W]_{−b}^{−} +(BR) we construct an amajorant t^{∗} by induction on the term structure from the a-majorants given above, where we furthermore λ-abstract the majorant n for 0_{X}. Then one easily shows that

M^{ω,X} ⊧ ∀a^{X}∀n^{0}((n)_{IR} ≥_{IR} d_{X}(0_{X}, a) → t^{∗}(n) ≳^{a} t).

where t^{∗} does not contain 0_{X}, d_{X} and W_{X} and we may take n := 0 if we interpret 0_{X} by a.

Lemma 9.10 also covers A^{ω}[X, d]_{−b}, simply by omitting the parts concerning the W -function, and A^{ω}[X, d, W, CAT(0)]_{−b}, as this theory contains no additional constants that need to be majorized but only another purely universal axiom which is interpreted by itself.

Proof of Theorem 4.10.

Assume

A^{ω}[X, d, W]_{−b} ⊢ ∀x^{ρ}(∀u^{0}B_{∀}(x, u) → ∃v^{0}C_{∃}(x, v)).

As in [22], this yields (using that negative translation and (partial) functional interpretation of the formula in question results in ∃U, V ∀x^{ρ}(B_{∀}(x, U(x)) → C_{∃}(x, V (x)))) by Lemmas 9.9 and 9.10 the extractabilty of closed terms t_{U}, t_{V} and t_{U^{∗}}, t_{V^{∗}}, the latter not containing 0_{X}, d_{X}, W_{X}, such that for all n^{0} ≥ d(0_{X}, a)

M^{ω,X} ⊧ \{ \begin{matrix}t_{U^{∗}}(n) ≳^{a} t_{U} ∧ t_{V^{∗}}(n) ≳^{a} t_{V} ∧ \\ ∀x^{ρ}(B_{∀}(x, t_{U}(x)) → C_{∃}(x, t_{V} (x))). \end{matrix}

Next, define the functional Φ(xρ̂, n) := max(t′_{U^{∗}}(n, x), t′_{V^{∗}}(n, x)), then

(+) M^{ω,X} ⊧ ∀u ≤ Φ(x^{∗}, n)B_{∀}(x, u) → ∃v ≤ Φ(x^{∗}, n)C_{∃}(x, v)

holds for all n ∈ IN, x ∈ M_{ρ} and x^{∗} ∈ Mρ̂ for which there exists an a ∈ X such that n ≥ d(0_{X}, a) and x^{∗} ≳^{a} x.

For the types γ of degree 1 or (1, X) of the quantifiers hidden in the definition of ∀/∃-formulas we have at least M_{γ} ⊆ S_{γ}, which is sufficient for our purposes. This is because types of that kind have arguments for whose types δ one has – using lemma 9.8 – that M_{δ} = S_{δ}. For parameters x^{ρ} with ρ of degree 2 or (1, X), we restricted ourselves to those x ∈ S_{ρ} which have a-majorants x^{∗} ∈ Sρ̂. Since functionals of such types ρ only have arguments of types τ for which M_{τ} = S_{τ} we get from x^{∗} ≳_{ρ}^{a} x (which implies that x^{∗} ≳a ; ρ̂ x^{∗}) that x^{∗} ∈ Mρ̂, x ∈ M_{ρ}. Hence Φ(x^{∗}, n) is defined and (+) yields

(++) S^{ω,X} ⊧ ∀u ≤ Φ(x^{∗}, n)B_{∀}(x, u) → ∃v ≤ Φ(x^{∗}, n)C_{∃}(x, v)

holds for all n ∈ IN, x ∈ S_{ρ} and x^{∗} ∈ Sρ̂ for which there exists an a ∈ X such that n^{0} ≥ d(0_{X}, a) and x^{∗} ≳^{a} x (here Φ(x^{∗}, n) is interpreted as [Φ(x^{∗}, n)]_{M^{ω,X}}).

This finishes the proof, as Φ is a partial functional (which is always defined on the majorizable elements of Sρ̂) in S_{ρ̂→0→0} which does not depend on (X, d, W).

Finally, if 0_{X} does not occur in either B_{∀} or C_{∃} we may freely interpret 0_{X} by a ∈ X. We then get majorants t_{U^{∗}}, t_{V^{∗}} and a resulting term Φ which no longer depend on a bound n on d(0_{X}, a) (as we can take n := 0).

Remark 9.11. The proof of the soundness theorem of Gödel’s functional interpretation (by closed terms) requires that we have closed terms for each type which we can use e.g. in order to construct the functional interpretation of axioms such as ⊥ → A. That closed term can be arbitrarily chosen and usually is taken as the constant-0-functional of suitable type, where for the type X one takes by default 0_{X}. However, one could have also chosen an open term such as the constant-a-functional for types which map arguments to the type X. So rather than having just one term extracted by functional interpretation we have a whole family of such terms parametrized by a^{X}. In the last step of the previous proof we make use of this by picking the a-th term according to our choice of the reference point a for ≳^{a}. By letting both ≳^{a} and the functional interpretation depend on a in a simultaneous way we achieve that the extracted majorant does not depend on the distance between a and any arbitrarily fixed constant such as 0_{X}.

For normed linear spaces we focus on the theory A^{ω}[X, ∥ · ∥, C]_{−b}. The further cases A^{ω}[X, ∥·∥, C, η]_{−b} and A^{ω}[X, ∥·∥, C, ⟨·, ·⟩]_{−b} follow by extending A^{ω}[X, ∥ · ∥, C]_{−b} respectively with an additional (majorizable) constant η for the modulus of uniform convexity or an additional purely universal axiom expressing the properties of the inner product in terms of the norm.

Lemma 9.12. Let (X, ∥ · ∥) be a non-trivial normed linear space with a nonempty convex subset C. Then M^{ω,X} is a model of A^{ω}[X, ∥ · ∥, C]_{−b}^{−} (for a suitable interpretation of the constants of A^{ω}[X, ∥ · ∥, C]_{−b} +(BR) in M^{ω,X}).

Moreover, for any closed term t of A^{ω}[X, ∥·∥, C]_{−b} +(BR) one can construct a closed term t^{∗} of A^{ω} +(BR) such that

M^{ω,X} ⊧ ∀n^{0}((n)_{IR} ≥_{IR} ∥c_{X}∥_{X} → t^{∗}(n) ≳^{0_{X}} t).

Similarly for A^{ω}[X, ∥ · ∥, C, η]_{−b}^{−} +(BR) and A^{ω}[X, ∥ · ∥, C, ⟨·, ·⟩]_{−b}^{−} +(BR).

Proof. The proof is almost the same as the above proof of Lemma 9.10 and as before the interpretation of the constants of A^{ω}[X, ∥ · ∥, C]_{−b}+(BR) is as in [22].

The main difference to the proof of Lemma 9.10 is that we fix a = 0_{X} (where 0_{X} now has to be interpreted by the zero vector of X), as otherwise we cannot define suitable (i.e. suitably uniform) majorants for the new constants of A^{ω}[X, ∥ · ∥, C]_{−b}. So now it suffices to state 0_{X}-majorants for the new constants:

• 0^{0} ≳^{0_{X}} 0_{X}, • 1^{0} ≳^{0_{X}} 1_{X},

• λx^{0}.((x)_{IR})_{∘} ≳^{0_{X}} ∥ · ∥_{X}^{X→1},

• λx^{0}, y^{0}.x + y ≳^{0_{X}} +_{X}^{X→X→X},

• λx^{0}.x ≳^{0_{X}} −_{X}^{X→X},

• λα^{1}, x^{0}.(α(0) + 1) · x ≳^{0_{X}} ·_{X}^{1→X→X}.

For the convex subset C, we have the characteristic term χ_{C} for the subset C, which is majorized as follows:

λx^{0}.1 ≳^{0_{X}} χ_{C}^{X→0}.

For the constant c_{X} ∈ C we have, given an n ≥ ∥c_{X}∥, the 0_{X}-majorant

n^{0} ≳_{X}^{0_{X}} c_{X}.

For uniformly convex spaces we 0_{X}-majorize the modulus η : IN → IN of uniform convexity by

(η)^{M} ≳_{1}^{0_{X}} η.

In [22], inner product spaces are defined by adding the so-called parallelogram law as another axiom. A norm satisfying the parallelogram law, allows one to define an inner product in terms of the norm and hence the inner product is immediately 0_{X}-majorizable. Inversely, if only an inner product is given the norm ∥ · ∥ can be recovered by defining ∥x∥ := \sqrt{⟨x, x⟩}.

The majorants for the constants of normed linear spaces, with the exception of the modulus η of uniform convexity, are only seemingly uniform, since they depend on properties of the norm and hence on the choice of a = 0_{X}. The 0_{X}-majorants for 0_{X}, 1_{X}, χ_{C} and c_{X} are obvious. For ∥ · ∥_{X} we need to consider the interpretation of ∥ · ∥_{X} in the model M^{ω,X}: the norm ∥x∥_{X} of an element x ∈ X is interpreted by the actual norm using the ()_{∘}-operator, i.e. by (∥x∥)_{∘}. In order to show that (in the model) λx.((x)_{IR})_{∘} ≳^{a} ∥ · ∥_{X} we need to show two things: (1) if n ≳^{0_{X}} x then ((n)_{IR})_{∘} s-maj_{1}(∥x∥)_{∘} and (2) if n ≥ m then ((n)_{IR})_{∘} s-maj_{1}((m)_{IR})_{∘} (recall that for ρ ∈ T s-maj_{1} and ≳_{1}^{a} are equivalent). For (1), if n ≳^{0_{X}} x then by definition (n)_{IR} ≥_{IR} ∥x∥_{X} and the result then follows by Lemma 4.6. For (2) the result follows directly from Lemma 4.6. For −_{X} the 0_{X}-majorant is derived straightforwardly from basic properties of the norm ∥ · ∥_{X}. For +_{X} we additionally use the triangle inequality to verify the majorant, i.e. ∥x + y∥ ≤ ∥x∥ + ∥y∥ and then if n_{1} ≳^{0_{X}} x and n_{2} ≳^{0_{X}} y we have that n_{1} + n_{2} ≥ ∥x + y∥, and the validity of the majorant follows.

Finally, for scalar multiplication ·_{X} we use that α codes a real number via a Cauchy sequence of rational numbers with fixed rate of convergence. The rational numbers in turn are represented by natural numbers using a monotone coding function such that (α(n))Q ≥Q |α(n)|Q for all n. Since |λn^{0}.α(0)−_{IR}α| ≤ 1 the natural number α(0)+1 is an upper bound for the real number represented by |α|_{IR}. Now let α^{∗} s-maj α. Then α^{∗}(0)+1 ≥ α(0)+1. Since ∥α · x∥_{X} =_{IR} |α|_{IR} ·_{IR} ∥x∥_{X} we, therefore, have that α^{∗}(0) + 1 taken as a natural number multiplied with an n ≳^{0_{X}} x is a 0_{X}-majorant for α ·_{X} x.

Proof of Theorem 6.3. As in the proof of Theorem 4.10

A^{ω}[X, ∥ · ∥, C]_{−b} ⊢ ∀x^{ρ}(∀u^{0}B_{∀}(x, u) → ∃v^{0}C_{∃}(x, v))

yields (using an easy adaptation of lemma 9.9 and Lemma 9.12) the extractability of closed terms t_{U}, t_{V} of A^{ω}[X, ∥ · ∥, C]_{−b}+(BR) and closed terms t_{U^{∗}}, t_{V^{∗}} of A^{ω}+(BR) (so, in particular, t_{U^{∗}}, t_{V^{∗}} do not contain 0_{X}, 1_{X}, c_{X}, +_{X}, −_{X}, ·_{X} or ∥ · ∥_{X}) such that for all n^{0} ≥ ∥c_{X}∥

M^{ω,X} ⊧ \{ \begin{matrix}t_{U^{∗}}(n) ≳^{0_{X}} t_{U} ∧ t_{V^{∗}}(n) ≳^{0_{X}} t_{V} ∧ \\ ∀x^{ρ}(B_{∀}(x, t_{U}(x)) → C_{∃}(x, t_{V} (x))). \end{matrix}

As before, defining Φ(xρ̂, n) := max(t_{U^{∗}}(n, x), t_{V^{∗}}(n, x)), we then have that

M^{ω,X} ⊧ ∀u ≤ Φ(x^{∗}, n)B_{∀}(x, u) → ∃v ≤ Φ(x^{∗}, n)C_{∃}(x, v)

holds for all n ∈ IN, x ∈ M_{ρ} and x^{∗} ∈ Mρ̂ for which n ≥ ∥c_{X}∥ and x^{∗} ≳^{0_{X}} x.

Also for normed linear spaces one verifies that for the types γ of degree 1 and (1, X) hidden in the definition of ∀/∃-formulas, we have the necessary inclusion M_{γ} ⊆ S_{γ}. For parameters x^{ρ} with types ρ of degree (1, X), (1, X, C) or 2, we again restricted ourselves to functionals which have 0_{X}-majorants x^{∗} and hence the necessary inclusions hold.

Thus, also

S^{ω,X} ⊧ ∀u ≤ Φ(x^{∗}, n)B_{∀}(x, u) → ∃v ≤ Φ(x^{∗}, n)C_{∃}(x, v)

holds for all n ∈ IN, x ∈ S_{ρ} and x^{∗} ∈ Sρ̂ for which n^{0} ≥ ∥c_{X}∥ and x^{∗} ≳^{0_{X}} x. In uniformly convex spaces the bound additionally depends on a modulus η of uniform convexity via its majorant η^{M}.

This finishes the proof, as Φ is a partial (resp. total, if ρ is in addition of degree 1) computable functional in S_{ρ̂→0→0}, defined on the majorizable elements of Sρ̂, which does not depend on (X, ∥ · ∥, C).

References

[1] M. Bezem. Strongly majorizable functionals of finite type: a model of bar recursion containing discontinous functionals. J. of Symbolic Logic, 50:652–660, 1985.

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

[3] M. Bridson and A. Haefliger. Metric spaces of non-positive curvature. Springer Verlag, Berlin, 1999.

[4] F. Bruhat and J. Tits. Groupes réductifs sur un corps local. I. Données radicielles valuées. Inst. Hautes Études Sci. Publ. Math., 41:5–251, 1972.

[5] C. E. Chidume. On the approximation of fixed points of nonexpansive mappings. Houston Journal of Mathematics, 7:345–355, 1981.

[6] W. Dotson. On the Mann iterative process. Trans. Amer. Math. Soc., 149:65–73, 1970.

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

[8] J. Garcia-Falset, E. Llorens-Fuster, and S. Prus. The fixed point property for mappings admitting a center. Talk given at ‘7th International Conference on Fixed Point Theory and its Applications’, Juky 17-23, 2005, Guanajuato, Mexico.

[9] P. Gerhardy and U. Kohlenbach. Strongly uniform bounds from semiconstructive proofs, 2004. Submitted.

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

[11] K. Goebel and W. A. Kirk. Iteration processes for nonexpansive mappings. In S. Singh, S. Thomeier, and B. Watson, editors, Topological Methods in Nonloinear Functional Analysis, volume 21 of Contemporaray Mathematics, pages 115–123. AMS, Providence, R.I., 1983.

[12] W. A. Howard. Hereditarily majorizable functionals of finite type. In A. Troelstra, editor, Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Springer LNM, pages 454–461. Springer-Verlag, Berlin, 1973.

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

[14] W. A. Kirk. Krasnosel’skii iteration process in hyperbolic spaces. Numer. Funct. Anal. Optimiz., 4:371–381, 1982.

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

[16] U. Kohlenbach. Effective moduli from ineffective uniqueness proofs. an unwinding of de La Vallee Poussin’s proof for Chebycheff approximation. Annals of Pure and Applied Logic, pages 27–94, 1993.

[17] U. Kohlenbach. Arithmetizing proofs in analysis. In Logic Colloquium ’96, volume 12 of Springer Lecture Notes in Logic, pages 115–158. Springer-Verlag, Berlin, 1998.

[18] U. Kohlenbach. A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numer. Funct. Anal. and Optimiz., 22:641–656, 2001.

[19] U. Kohlenbach. On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In Proc. of the Fourth Workshop on Computability and Complexity in Analysis, pages 119–145. Spinger Lecture Notes in Computer Science LNCS 2064, 2001.

[20] U. Kohlenbach. Uniform asymptotic regularity for Mann iterates. J. Math. Anal. Appl., 279:531–544, 2003.

[21] U. Kohlenbach. Some computational aspects of metric fixed point theory. Nonlinear Analysis, 61, no.5:823–837, 2005.

[22] U. Kohlenbach. Some logical metatheorems with applications in functional analysis. Trans. Amer. Math. Soc., 357:89–128, 2005.

[23] U. Kohlenbach and B. Lambov. Bounds on iterations of asymptotically quasi-non-expansive mappings. In Proc. International Conference on Fixed Point Theory and Applications, Valencia 2003, pages 143–172. Yokohama Publishers, 2004.

[24] U. Kohlenbach and L. Leuştean. Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Abstract and Applied Analysis, 8:449–477, 2003.

[25] U. Kohlenbach and P. Oliva. Proof mining: a systematic way of analyzing proofs in mathematics. Proc. Steklov Inst. Math, 242:136–164, 2003.

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

[27] H. Luckhardt. Extensional Gödel Functional Interpretation., volume 206 of Springer LNM. Springer-Verlag, Berlin, 1973.

[28] H. V. Machado. A characterization of convex subsets of normed spaces. Kodai Math. Sem. Rep., 25:307–320, 1973.

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

[30] A. G. O’Farrell. When uniformly-continuous implies bounded. Irish Math. Soc. Bulletin, 53:53–56, 2004.

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

[32] I. Shafrir. The approximate fixed point property in Banach and hyperbolic spaces. Israel J. Math., 71:211–223, 1990.

[33] C. Spector. Provably recursive functionals of analysis : a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In J. Dekker, editor, Proceedings of Symposia in Pure Mathematics, volume 5, pages 1–27. AMS, Providence, R.I., 1962.

[34] W. Takahashi. A convexity in metric and nonexpansive mappings. I. Kodai Math. Sem. Rep., 22:142–149, 1970.

Recent BRICS Report Series Publications

RS-05-21 Philipp Gerhardy and Ulrich Kohlenbach. General Logical Metatheorems for Functional Analysis. July 2005. 65 pp.

RS-05-20 Ivan B. Damgård, Serge Fehr, Louis Salvail, and Christian Schaffner. Cryptography in the Bounded Quantum Storage Model. July 2005.

RS-05-19 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas qLuttik. Finite Equational Bases in Process Algebra: Results and Open Questions. June 2005. 28 pp. To appear in the LNCS series in Jan Willem Klop’s 60th birthday volume.

RS-05-18 Peter Bogetoft, Ivan B. Damgård, Thomas Jakobsen, Kurt Nielsen, Jakob Pagter, and Tomas Toft. Secure Computing, Economy, and Trust: A Generic Solution for Secure Auctions with Real-World Applications. June 2005. 37 pp.

RS-05-17 Ivan B. Damgård, Thomas B. Pedersen, and Louis Salvail. A Quantum Cipher with Near Optimal Key-Recycling. May 2005.

RS-05-16 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. May 2005. ii+24 pp.

RS-05-15 Ma�gorzata Biernacka and Olivier Danvy. A Concrete Framework for Environment Machines. May 2005. ii+25 pp.

RS-05-14 Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. April 2005. ii+8 pp.

RS-05-13 Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the Dynamic Extent of Delimited Continuations. April 2005. ii+32 pp. Extended version of an article to appear in Information Processing Letters. Subsumes BRICS RS-05-2.

RS-05-12 Ma�gorzata Biernacka, Olivier Danvy, and Kristian Støvring. Program Extraction from Proofs of Weak Head Normalization. April 2005. 19 pp. Extended version of an article to appear in the preliminary proceedings of MFPS XXI, Birmingham, UK, May 2005.