BRICS RS-03-21 U. Kohlenbach: Some Logical Metatheorems with Applications in Functional Analysis BRICS

Basic Research in Computer Science

Some Logical Metatheorems with Applications in Functional Analysis

Ulrich Kohlenbach BRICS Report Series RS-03-21 ISSN 0909-0878 May 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, 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/03/21/

Some logical metatheorems with applications in functional analysis

Ulrich Kohlenbach^{∗}

BRICS^{†}

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

Keywords: Proof mining, functionals of finite type, convex analysis, fixed points, nonexpansive mappings, hyperbolic spaces. AMS Classification: 03F10, 03F35, 47H09, 47H10.

Abstract

In previous papers we have developed proof-theoretic techniques for extracting effective uniform bounds from large classes of ineffective existence proofs in functional analysis. ‘Uniform’ here means independence from parameters in compact spaces. A recent case study in fixed point theory systematically yielded uniformity even w.r.t. parameters in metrically bounded (but noncompact) subsets which had been known before only in special cases. In the present paper we prove general logical metatheorems which cover these applications to fixed point theory as special cases but are not restricted to this area at all. Our theorems guarantee under general logical conditions such strong uniform versions of non-uniform existence statements. Moreover, they provide algorithms for actually extracting effective uniform bounds and transforming the original proof into one for the stronger uniformity result. Our metatheorems deal with general classes of spaces like metric spaces, hyperbolic spaces, normed linear spaces, uniformly convex spaces as well as inner product spaces.

∗Partially supported by the Danish Natural Science Research Council, Grant no. 21-02-0474.

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

1 Introduction

The purpose of this paper is to establish a novel way of using proof theory to obtain new uniform existence results in mathematics together with effective versions thereof. The results we are concerned with in this paper belong to the area of analysis and, more specifically, nonlinear functional analysis. However, we are confident that our approach can be used e.g. in algebra as well.

The idea of making mathematical use of proof theoretic techniques has a long history which goes back to G. Kreisel’s program of ‘unwinding of proofs’ put forward in the 50’s (for more modern accounts see [38, 39]). The goal of this program is to systematically transform given proofs of mathematical theorems in such a way that explicit quantitative data, e.g. effective bounds, are extracted which were not visible beforehand. The main obstacle in reading off such information directly is usually the use of ineffective ‘ideal’ elements in a proof. ‘Unwinding of proofs’ has had applications in e.g. algebra ([6]), combinatorics ([2]) and number theory ([37, 41, 42]). In recent years, the present author has developed systematically (under the name ‘proof mining’) proof theoretic techniques specially designed for applications in analysis (see [25, 27, 29] and – for a survey – [35] and the articles cited there). We have carried out major case studies in the areas of Chebycheff approximation ([25, 26]), L_{1}-approximation (with P. Oliva, [34]) and metric fixed point theory (partly with L. Leuştean, [31, 32, 33]). The applications are based on metatheorems of the following form (first established in [25]): Let X be a Polish space and K a compact Polish space which are given in so-called standard representation by elements of the Baire space IN^{IN} and – for K – the space of functions f ∈ IN^{IN}, f ≤ M bounded by some fixed function M. Then one can extract from ineffective proofs of theorems of the form

∀x ∈ X∀y ∈ K∃z ∈ INA(x, y, z),

where A is a purely existential formula (in representatives of x, y), effective uniform (on K) bounds Φ(f_{x}) on ‘∃z’, i.e.

∀x ∈ X∀y ∈ K∃z ≤ Φ(f_{x}) A(x, y, z).

The crucial aspects in these applications are that 1) Φ(f_{x}) does not depend on y ∈ K (‘uniformity w.r.t. K’) but only on – some

representative f_{x} ∈ IN^{IN} of – x,

2) the extracted Φ will be of (usually low) subrecursive complexity (depending on the proof principles used).

A discussion of the relevance of this setting for numerous problems in numerical functional analysis is given in [35]. Whereas this covers the applications in approximation theory mentioned above, the applications in metric fixed point theory in [31, 32, 33] have produced systematically results going far beyond what is guaranteed by the existing metatheorems:

1) effective uniform bounds are obtained for theorems about arbitrary normed resp. so-called hyperbolic spaces (no separability assumption or assumptions on constructive representability),

2) independence of the bounds from parameters y (‘uniformity in y’) from bounded subsets of normed spaces resp. bounded hyperbolic spaces were obtained without any compactness condition.

It is the last point which is most interesting: general compactness arguments can be used to infer the existence of bounds which are uniform for compact spaces (and – under general conditions – even their computability) so that in this case it mainly is the explicit construction of such bounds (of low complexity) which is in question. For spaces which are not compact but only metrically bounded, by contrast, there are no general mathematical reasons why even ineffectively such a strong uniformity should hold. In fact, in the examples in metric fixed point theory we studied, only for special cases such (ineffective) uniformity results were known before and they were obtained by non-trivial and ad-hoc functional analytic techniques ([7, 10, 21]).

In this paper we prove new metatheorems which are strong enough to cover the main uniformity results we got in the aforementioned case studies as special cases. Moreover, they guarantee a-priori under rather general and easy to check logical conditions the existence of bounds which are uniform on arbitrary bounded convex subsets of general classes of spaces such as metric spaces, hyperbolic spaces, normed linear spaces, uniformly convex normed spaces and inner product spaces. The proofs of these metatheorems are based on novel extensions of the general proof theoretic technique of functional interpretation which goes back to [12]. This provides our metatheorems with algorithms to actually extract from given proofs of non-uniform existence theorems explicit effective uniform bounds. These algorithms correspond directly to the extraction technique used in the concrete examples in fixed point theory mentioned above. The importance of the metatheorems is that they can be used to infer new uniform existence results without having to carry out any actual proof analysis. In such applications, the proofs of the metatheorems (and the complicated proof theory used in them) can be treated as a ‘black box’. However, in contrast to model-theoretic applications of logic to analysis (e.g. transfer principles in non-standard analysis or model theoretic uses of ultrapowers, see also the discussion at the end of section 3 below), one can also open that box and explicitly run the extraction algorithm. This algorithm not only will extract an explicit effective bound (whose subrecursive complexity can be estimated in terms of the proof principles used) but will also transform the original proof into a new one for the stronger uniform bound which can again be written in ordinary mathematical terms and does not need the metatheorem (nor other tools from logic) any longer for its correctness.

It is clear that such strong uniformity results as discussed above can hold only under certain conditions: e.g. for concrete spaces like (C[0, 1], ∥ · ∥_{∞}) one can easily construct counterexamples: Let B denote the closed unit ball in (C[0, 1], ∥·∥_{∞}). By the Weierstraß approximation theorem we have

∀f ∈B∃n ∈ IN(n encodes the coefficients of a polynomial p ∈ Q[X] s.t. ∥f−p∥_{∞}< \frac{1}{2}),

but there is no uniform bound for n on the whole set B (consider e.g. f_{n} := sin(nx)). The reason why in the various examples from metric fixed point theory such uniformity results hold, obviously has to do with the fact that only general algebraic or geometric properties of whole classes of spaces (like: metric spaces, hyperbolic spaces, normed linear spaces, uniformly convex normed spaces, inner product spaces) are used but not genuinely analytical properties as e.g. separability on which our counterexample is based upon. It will turn out that the crucial condition on the properties permissible is that they can be expressed by axioms which have a generalized Gödel functional interpretation by so-called majorizable functionals and which only involve majorizable functionals as constants (see section 4 for technical details). In a setting suitably enriched by new constants, we can axiomatize the above mentioned classes of spaces even by purely universal ‘algebraic’ axioms (modulo an explicit ‘analytical’ Cauchy-representation of real numbers) so that this condition is satisfied for very simple reasons. It is the interface between the algebraic structures and the real number representation which will need some subtle care.

We focus in this paper on the structures listed above. It is clear, however, that many other structures (whose axioms may satisfy the logic condition mentioned above for more subtle reasons), e.g. further mathematically enriched structures, can be treated as well. In order to make the metatheorems as strong and easy to use for non-logicians as possible, we use the deductive framework of classical analysis based on full dependent choice (which includes full second-order arithmetic). Of course, in concrete proofs only small fragments are needed, which accounts for the low complexity of the bounds actually observed. However, using a strong formal framework makes it easy to check the formalizability of proofs and thereby the applicability of the metatheorems. The paper is organized as follows: section 2 develops the logical setting in which our results are formulated. The main metatheorems are stated in section 3 together with several applications. Section 4 is devoted to the proofs of the main results.

2 The formal framework

We now define our formal framework, the system A^{ω} of so-called (weakly extensional) classical analysis and its extensions by built-in mathematical structures. A^{ω} is formulated in the language of functionals of finite type and consists of a finite type extension PA^{ω} of first order Peano arithmetic PA and the axiom schema DC of dependent choice in all types which implies countable choice and hence arbitrary comprehension over natural numbers. As a consequence of this, full second order arithmetic (in the sense of [47]) is contained in A^{ω} (via the identification of subsets of IN with their characteristic functions).

Definition 2.1 The set T of all finite types is defined inductively by the clauses

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

Abbreviation: We usually omit outermost parantheses for types. The type 0 → 0 of unary number theoretic functions will often be denoted by 1.

Remark 2.2 Any type ρ ≠ 0 can be written in the following normal form

ρ = ρ_{1} → (ρ_{2} → … (ρ_{k} → 0) …)

which we usually abbreviate as

ρ_{1} → ρ_{2} → … → ρ_{k} → 0.

Objects of type 0 denote (in the intended model) natural numbers. Objects of type ρ → τ are operations mapping objects of type ρ to objects of type τ. E.g. 0 → 0 is the type of functions f : IN → IN and (0 → 0) → 0 is the type of operations F mapping such functions f to natural numbers, and so on. We only include equality =_{0} between objects of type 0 as a primitive predicate. Equality between objects of higher types s =_{ρ} t is a defined notion:

s =_{ρ} t :≡ ∀x_{1}^{ρ_{1}}, …, x_{k}^{ρ_{k}}(s(x_{1}, …, x_{k}) =_{0} t(x_{1}, …, x_{k})),

where

ρ = ρ_{1} → ρ_{2} → … ρ_{k} → 0.

i.e. higher type equality is defined as extensional equality. An operation F of type ρ → τ is called extensional if it respects this extensional equality, i.e. if

∀x^{ρ}, y^{ρ}(x =_{ρ} y → F (x) =_{τ} F (y)).

What we would like to have is an axiom stating that all functionals in our system are extensional. This, however, would be too strong a requirement for the metatheorems we are aiming at and their applications in functional analysis to hold. Instead we include a weaker quantifier-free so-called extensionality rule due to [48]^{1}

QF-ER : \frac{A_{0} → s =_{ρ} t}{A_{0} → r[s] =_{τ} r[t]}, where A_{0} is a quantifier-free formula.

The rule QF-ER allows to derive the equality axioms for type-0 objects

x =_{0} y → t[x] =_{τ} t[y]

but not for objects x, y of higher types (see [50],[16]). The system A^{ω} is defined as follows (further information can be found e.g. in [40]): on top of many-sorted classical logic with variables x^{ρ}, y^{ρ}, z^{ρ}, … for all types ρ ∈ T and quantifiers over those we have the following: Constants: O^{0} (zero), S^{1} (successor), Π_{ρ,τ}^{ρ→τ→ρ} (projectors), Σ_{δ,ρ,τ} (combinators of type (δ → ρ → τ) → (δ → ρ) → δ → τ), recursor constants \underline{R} for simultaneous primitive recursion in all types (see remark 2.3 below). Terms: variables x^{ρ} and constants c^{ρ} of type ρ are terms of type ρ. If t^{ρ→τ} is a term of type ρ → τ and s^{ρ} a term of type ρ, then (ts)^{τ} is a term of type τ. Instead of (… (ts_{1}) … s_{n}) we usually write t(s_{1}, …, s_{n}). Formulas are built up out of atomic formulas of the form s =_{0} t by means of the logical operators as usual. Non-logical axioms and rules:

1We will see further below that the need to restrict the use of extensionality has a natural mathematical interpretation. Moreover, working with the quantifier-free rule of extensionality will point us to the correct mathematical conditions in our applications.

(i) Reflexivity, symmetry and transitivity axioms for =_{0}, (ii) usual successor axioms for S: S(x) =_{0} S(y) → x =_{0} y, S(x) ≠_{0} 0, (iii) axiom schema of complete induction

(IA) : A(0) ∧ ∀x^{0}(A(x) → A(S(x))) → ∀x^{0}A(x),

where A(x) is an arbitrary formula of our language, (iv) axioms for Π_{ρ,τ}, Σ_{δ,ρ,τ} and \underline{R}\underline{ρ}:

(Π) : Π_{ρ,τ}x^{ρ}y^{τ} =_{ρ} x^{ρ},

(Σ) : Σ_{δ,ρ,τ}xyz =_{τ} xz(yz) (x^{δ→ρ→τ}, y^{δ→ρ}, z^{δ}),

(R) : \{ \begin{matrix}\underline{R}\underline{ρ}0\underline{y}\underline{z} =\underline{ρ} \underline{y} \\ \underline{R}\underline{ρ}(Sx^{0})\underline{y}\underline{z} =\underline{ρ} \underline{z}(\underline{R}\underline{ρ}x\underline{y}\underline{z})x, \end{matrix}

where \underline{ρ} = ρ_{1}, …, ρ_{k}, y_{i} is of type ρ_{i} and z_{i} of type ρ_{1} → … → ρ_{k} → 0 → ρ_{i}.

(v) quantifier-free extensionality rule QF-ER, (vi) quantifier free axiom of choice schema in all types:

QF-AC : ∀\underline{x}∃\underline{y}A_{0}(\underline{x}, \underline{y}) → ∃\underline{Y} ∀\underline{x}A_{0}(\underline{x}, \underline{Y} \underline{x}), where A_{0} is quantifier-free and \underline{x}, \underline{y} are tuples of variables of arbitrary types.

(vii) dependent choice DC:= {DC^{ρ} : ρ ∈T} in all types, where

DC^{ρ} : ∀x^{0}, y^{ρ}∃z^{ρ}A(x, y, z) → ∃f^{0→ρ}∀x^{0}A(x, f(x), f(S(x))), where A is an arbitrary formula and ρ an arbitrary type.

Remark 2.3 1) Our formulation of DC (first considered in [17] under the name (A.1))^{2} combines the usual formulation of dependent choice

∀x^{ρ}∃y^{ρ}A(x, y) → ∀x^{ρ}∃f^{0→ρ}[f(0) =_{ρ} x ∧ ∀z^{0}A(f(z), f(S(z)))]

and countable choice

∀x^{0}∃y^{ρ}A(x, y) → ∃f^{0→ρ}∀x^{0}A(x, f(x))

which are both provable in A^{ω} (see [17] for details).

2) One can in fact reduce simultaneous primitive recursion in higher types to ordinary primitive recursion in higher types. However, this is rather tedious (see [50]) and would cause further problems in the extensions of A^{ω} to new types defined below, see remark 4.2. That’s why we include constants for simultaneous recursion as primitives.

The purpose of the constants Π, Σ is to achieve closure under functional abstraction:

Lemma 2.4 For every term t[x^{ρ}]^{τ} one can construct in A^{ω} a term λx^{ρ}.t[x] of type ρ → τ such that

A^{ω} ⊢ (λx^{ρ}.t[x])(s^{ρ}) =_{τ} t[s].

Proof: See [50]. ⊣

We now aim at ‘adding’ abstract structures like general (classes of) metric spaces (X, d) to A^{ω} resulting in an extension A^{ω}[X, d]. The idea is to have in addition to the type 0 another ground type X together with variables x^{X}, y^{X}, z^{X}, … and quantifiers ∀x^{X}, ∃x^{X}, where these variables are intended to vary over the elements of the set X. We also add a new constant d_{X} for the (pseudo-)metric to the system with the usual axioms. In order to do so we first have to show how to introduce real numbers in A^{ω}, where we follow [25]:

We introduce real numbers as Cauchy sequences of rational numbers with fixed Cauchy modulus 2^{−n}. To this end we first have to define the ordered field (Q, +, ·, 0, 1, <) of rational numbers within A^{ω}: Rational numbers are represented as codes j(n, m) of pairs (n, m) of natural numbers (i.e. type-0 objects), where j is the

Cantor pairing function: j(n, m) represents the rational number \frac{\frac{n}{2}}{m+1} if n is even,

and the negative rational number −\frac{\frac{n+1}{2}}{m+1} otherwise. Since we use a surjective pairing function j, each number can be conceived as code of a uniquely determined rational number. We define an equality relation =Q on the representatives of the rational numbers, i.e. on IN, to be

2See also [40] where our formulation of DC is called ωAC.

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

and analogous in the remaining cases, where \frac{a}{b} = \frac{c}{d} is defined to hold if ad =_{0} cb when bd > 0. In order to express the statement that n represents the rational r, we write n =Q ⟨r⟩ or simply n = ⟨r⟩. Of course ⟨·⟩ is not a function of r since r possesses infinitely many representatives. Rational numbers are, strictly, speaking equivalence classes on IN w.r.t. =Q. By using only their representatives and =Q one can avoid formally introducing the set Q of all these equivalence classes.^{3} On IN one can easily define primitive recursive operations +Q, ·Q and predicates <Q, ≤Q such that e.g. ⟨r_{1}⟩ +Q ⟨r_{2}⟩ =Q ⟨r_{3}⟩ iff r_{1} + r_{2} = r_{3} for the rational numbers r_{1}, r_{2}, r_{3} which are represented by ⟨r_{1}⟩, ⟨r_{2}⟩, ⟨r_{3}⟩ (analogous for ·Q, <Q, ≤Q). The embedding of IN into Q can on the level of the codes be expressed by n ↦ ⟨n⟩ := j(2n, 0); 0Q := ⟨0⟩, 1Q := ⟨1⟩. One easily shows (within A^{ω}) that (IN, +Q, ·Q, 0Q, 1Q, <Q) is an ordered field (which represents (Q, +, ·, 0, 1, <) in A^{ω}). Each function f : IN → IN (i.e. each functional of type 1) can be interpreted as an infinite sequence of codes of rationals and therefore as representative of an infinite sequence of rationals. Real numbers are represented by functions f such that

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

∀n∀k > m ≥ n(|f(m) −Q f(k)|Q ≤Q Σ_{i=m}^{k−1}|f(i) −Q f(i + 1)|Q ≤Q

Σ_{i=n}^{∞}|f(i) −Q f(i + 1)|Q < ⟨2^{−n}⟩).

Each f which satisfies (∗) therefore represents a Cauchy sequence of rationals with Cauchy modulus 2^{−n}. In order to guarantee that each function f codes a real number, we introduce the following construction (which easily can be carried out by a term in A^{ω}) :

(∗∗) 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}

3In contrast to the representation of real numbers below we could constructively avoid to have many codes of a rational number by taking the minimal code.

f̂ always satisfies (∗). If (∗) holds for f then ∀n(fn =_{0} f̂n). Thus each function f codes a unique real number: the real number which is given by the Cauchy sequence coded by f̂. In the other direction, if f represents a Cauchy sequence of rationals with modulus 2^{−n}, then g(n) := f(n+1) satisfies (∗) and therefore represents the real number, given by f, in our sense. This shows that nothing is lost by our restriction of sequences satisfying (∗). The construction f ↦ f̂ enables one to reduce quantifiers ranging over IR to ∀f^{1} resp. ∃f^{1} without introducing any additional quantifiers. On the representatives (in the sense above) of real numbers (i.e. on the functionals of type 1) f_{1}, f_{2} we define an equivalence relation =_{IR} by

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

f_{1} =_{IR} f_{2} holds iff f_{1} and f_{2} represent the same real number (w.r.t. the usual identity relation on the reals). Whereas =Q is decidable, the relation =_{IR} is not but is a Π_{1}^{0}-predicate.

f_{1} <_{IR} f_{2} :≡ ∃n(f̂_{2}(n + 1) −Q f̂_{1}(n + 1) ≥Q ⟨2^{−n}⟩) ∈ Σ_{1}^{0},
f_{1} ≤_{IR} f_{2} :≡ ¬(f_{2} <_{IR} f_{1}) ∈ Π_{1}^{0}.

One easily defines functionals +_{IR}, −_{IR}, ·_{IR}, | · |_{IR} etc. on our codes of real numbers, which represent the usual operations +, −, ·, | · | etc. on IR: For example, define f_{1} +_{IR} f_{2} by

(f_{1} +_{IR} f_{2})(k) := f̂_{1}(k + 1) +Q f̂_{2}(k + 1).

Then f_{1} +_{IR} f_{2} =_{IR} f_{3} holds iff x_{1} + x_{2} = x_{3} for the real numbers x_{1}, x_{2}, x_{3} which are represented by f_{1}, f_{2}, f_{3}. +_{IR} is a functional of type 1 → 1 → 1. In a similar way one defines −_{IR} and – somewhat more complicated – ·_{IR}. The embedding of Q into IR is on the level of representatives given as follows: If n = ⟨r⟩ codes the rational number r, then λk.n represents r as a real number. Put together we can express the embedding of IN into IR by n_{IR} :=_{1} λk^{0}.nQ. In particular, 0_{IR} := λk.0Q, 1_{IR} := λk.1Q. IR denotes the set of all equivalence classes on the set of functions f w.r.t. =_{IR}. As in the case of Q, we use IR only informally and deal exclusively with the representatives and the operations defined on them. (IN^{IN}, +_{IR}, ·_{IR}, 0_{IR}, 1_{IR}, <_{IR}) is an Archimedean ordered field (provable in A^{ω}), which represents (IR, +, ·, 0, 1, <) in A^{ω}. One easily verifies the following fact:

Lemma 2.5 A^{ω} ⊢ ∀k(|f −_{IR} λn.f̂(k)|_{IR} <_{IR} ⟨2^{−k}⟩).

Due to the fact that the Cantor pairing function satisfies j(n, m) ≥_{0} n, m we get that for any number theoretic function α^{1}:

(α(0) + 1)Q ≥Q |α(0)|Q +Q 1Q

and hence (using lemma 2.5 with k = 0 and the fact that α̂(0) =_{0} α(0))

(α(0) + 1)_{IR} ≥_{IR} |α|_{IR}

which we will use repeatedly in the proofs of the main results. Each functional Φ^{0→1} can be conceived of as an infinite sequence of codes of real numbers and therefore as a representative of a sequence of real numbers. We have the following Cauchy completeness:

Lemma 2.6 A^{ω} ⊢ ∀Φ^{0→1}(∀n; m, k ≥ n(|Φ(m) −_{IR} Φ(k)|_{IR} ≤_{IR} ⟨2^{−n}⟩) →

∃f^{1}∀n(|Φ(n) −_{IR} f|_{IR} ≤_{IR} ⟨2^{−n}⟩)).

In fact, f can be defined as fk := Φ̂(k + 3)(k + 3).

Notation 2.7 For better readability we often simply write e.g. 2^{−k} in contexts like ‘… ≤Q 2^{−k}’ instead of its (canonical) code as rational number j(2, 2^{k} − 1). Similarly, we write ‘… ≤_{IR} 2^{−k}’ instead of ‘… ≤_{IR} λn.j(2, 2^{k} − 1)’, where λn.j(2, 2^{k} − 1) is the canonical representative of 2^{−k} as a real number.

As we will mainly quantify over elements in the unit interval [0, 1] we need the following effective operation which reduces quantification over [0, 1] to quantification over IR and hence – by the representation above – over type-1 objects (without introducing further quantifiers). In fact, only number theoretic functions bounded by a fixed function N will be needed to represent all elements of [0, 1]:

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

Note that λx^{1}.x̃ can easily be defined by a closed term in A^{ω}. One easily verifies the following

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

0_{IR} ≤_{IR} x ≤_{IR} 1_{IR} → x̃ =_{IR} x,
0_{IR} ≤_{IR} x̃ ≤_{IR} 1_{IR}, x̃ =_{IR} ˜ x̃ and
x̃ ≤_{1} N := λn.j(2^{n+3}, 2^{n+2} − 1).

In a similar way, one can represent not only IR but general Polish (complete separable metric) spaces P by IN^{IN}, where instead of the rational numbers one now takes a countable dense subset P_{c} of P. Things are slightly more complicated as the metric already on P_{c} will in general be real valued. A space (P, d) is called A^{ω}-definable if the restriction d_{c} of d to the codes of elements of P_{c} is represented by a closed term of A^{ω} which – provably in A^{ω} – is a pseudo-metric on these codes. Details can be found in [25] (see also [1]). Compact Polish spaces K can be represented (similarly to the representation of [0, 1] above) in such a way that the representing functions f are all bounded by some fixed function M ∈ IN^{IN}. K is A^{ω} definable if both d_{c} and M are given by A^{ω}-terms (again see [25],[1] for details). Using this representation a statement of the kind

(∗) ∀x ∈ P ∀y ∈ K A(x, y)

has – formalized in A^{ω} – the form

∀x^{1}∀y ≤_{1} M A(x, y),

where – if we write (∗) – we always tacitly assume that A(x^{1}, y^{1}) is extensional w.r.t. =_{P} , =_{K}

x_{1} =_{P} x_{2} ∧ y_{1} =_{K} y_{2} ∧ A(x_{1}, y_{1}) → A(x_{2}, y_{2})

and therefore really expresses a statement about elements in P, K.

In the proof of the main theorems below we will need a semantical argument based on the following (ineffective) construction which selects to a given x ∈ [0, ∞) a unique representative (x)_{∘} ∈ IN^{IN} out of all the representatives f ∈ IN^{IN} of x such that certain properties are satisfied (here and in the next lemma and definition, [0, ∞) refers to the ‘real’ space of all positive reals, i.e. not to the sets of representatives, ≤_{1} is pointwise order on IN^{IN}, and ≤ the usual order on [0, ∞)):

Definition 2.9 1) 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].

2) M(b) := λn.j(b2^{n+2}, 2^{n+1} − 1).

Lemma 2.10 1) If x ∈ [0, ∞), then (x)_{∘} is a representative of x in the sense of our representation of real numbers carried out above.

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 b ∈ IN and x ∈ [0, b], then (x)_{∘} ≤_{1} M(b).

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

5) M(b) is monotone, i.e. ∀n ∈ IN((M(b))(n) ≤_{0} (M(b))(n + 1)).

Proof: 1) Observe that (x)_{∘} satisfies (∗) and hence ˆ(x)_{∘} =_{1} (x)_{∘}.

2) Obvious from the definition of (x)_{∘}.

3) Here we use that the Cantor pairing function is monotone in its arguments.

4) and 5) follow again by the monotonicity of j. ⊣

Definition 2.11 (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) ∀x, y, z, w ∈ X, λ ∈ [0, 1](d(W (x, z, λ), W (y, w, λ)) ≤ (1−λ)d(x, y)+λd(z, w)).

Definition 2.12 Let (X, d, W) be a hyperbolic space. The set

seg(x, y) := { W (x, y, λ) : λ ∈ [0, 1] }

is called the metric segment with endpoints x, y (the conditions (i)−(iii) ensure that seg(x, y) is an isometric image of the real line segment [0, d(x, y)]).

Remark 2.13 If only condition (i) is satisfied, then (X, d, W) is a convex metric space in the sense of Takahashi ([49]). (i) − (iii) together are equivalent to (X, d, W) being a space of hyperbolic type in the sense of [10]. The condition (iv) (first considered as ‘condition III’ in [19]) is used in [45] to define the class of hyperbolic spaces. That class contains all normed linear spaces but also the open unit ball in complex Hilbert space with the hyperbolic metric as well as Hadamard manifolds (see [11],[45],[46]). The definition of ‘hyperbolic space’ as given in [45] is slightly more restrictive than ours since [45] considers a metric space (X, d) together with a family M of metric lines (rather than metric segments) so that hyperbolic spaces in that sense are always unbounded. Our definition (like Kirk’s notion of space of hyperbolic type and Takahashi’s notion of convex metric space) is in contrast to this such that every convex subset of a hyperbolic space is itself a hyperbolic space. Moreover, using a set M of segments has the consequence that in general it is not guaranteed (as in the case of metric lines) that for u, v ∈ seg(x, y) with (u, v) different from (x, y), seg(u, v) is a subsegment of seg(x, y) unless M is closed under subsegments.^{4} The theorems to which we will apply the metatheorems do hold even for spaces of hyperbolic type and so in particular for our notion of hyperbolic spaces. The reason we include condition (iv) is that this allows to formulate and to apply our metatheorems in the most easy way avoiding certain technicalities (to be discussed further below) which have to do with so-called extensionality conditions. It is for the same reason why it is convenient to have a notion of hyperbolic space which is closed under convex subset formation.

The theories A^{ω}[X, d] and A^{ω}[X, d, W] : A^{ω}[X, d] results by

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

X, i.e.

0, X ∈ T^{X}, ρ, τ ∈ T^{X} ⇒ ρ → τ ∈ T^{X}

(in particular, the schemes IA, QF-AC, DC and the rule QF-ER are now taken over the extended language),

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

(iii) adding a constant b_{X} of type 0,

(iv) adding a new constant d_{X} of type X → X → 1 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)),

4As a consequence of this we cannot derive (iv) from the special case for λ := \frac{1}{2} as in the setting of [45] and therefore we formulate (iv) for general λ ∈ [0, 1].

(4) ∀x^{X}, y^{X}(d_{X}(x, y) ≤_{IR} (b_{X})_{IR}(:=_{1} λk^{0}.j(2b_{X}, 0^{0})).

Still only equality at type 0 is a primitive 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] results from A^{ω}[X, d] by adding a new constant W_{X} of type X → X → 1 → X together with the axioms

(5) ∀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)),

(6) ∀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)),

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

(8) ∀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)).

Remark 2.14 The additional axioms of A^{ω}[X, d] express (modulo our representation of IR sketched above) that d_{X} represents a pseudo-metric d (on the universe the type-X variables are ranging over) which is bounded by b_{X}.^{5} Hence d_{X} represents a (b_{X}-bounded) metric on the set of equivalence classes generated by =_{X}. Rather than having to form such equivalence classes explicitly, we can talk about x^{X}, y^{X} but have to make sure that e.g. functionals f^{X→X} respect this equivalence relation, i.e.

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

in order to be entitled to refer to f as representing a function X → X. It is important to observe that 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). This restriction on the availability of extensionality is crucial for our results to hold (see the discussion at the end of section 3). However, we will be able to deduce from the mathematical properties of the functionals occurring in our applications sufficient extensionality: firstly, note that A^{ω}[X, d] proves that

∀x_{1}^{X}, x_{2}^{X}, y_{1}^{X}, y_{2}^{X}(x_{1} =_{X} x_{2} ∧ y_{1} =_{X} y_{2} → d_{X}(x_{1}, y_{1}) =_{IR} d_{X}(x_{2}, y_{2})).

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

Secondly, the W_{X}-axioms (6), (8) imply that W_{X} is continuous in all arguments and hence the extensionality of W_{X}, i.e. for all x_{1}^{X}, x_{2}^{X}, y_{1}^{X}, y_{2}^{X}, λ_{1}^{1}, λ_{2}^{1}

x_{1} =_{X} x_{2} ∧ y_{1} =_{X} y_{2} ∧ λ̃_{1} =_{IR} λ̃_{2} → W_{X}(x_{1}, y_{1}, λ̃_{1}) =_{X} W_{X}(x_{2}, y_{2}, λ̃_{2}).

Hence (5)-(8) in fact express (modulo the representation of IR and [0, 1]) that W_{X} represents a function W : X × X × [0, 1] → X which makes the bounded metric space induced by d into a bounded hyperbolic space. We always assume X to be non-empty by including a constant 0_{X} of type X.^{6} For the proof of our metatheorem below it will be of crucial importance that the axioms (1)-(8) are all purely universal (recall that =_{X}, =_{IR}, ≤_{IR}∈ Π_{1}^{0}).

Remark 2.15 1) As before we can define λ-abstraction in A^{ω}[X, d] and A^{ω}[X, d, W].

2) Every type ρ ∈ T^{X} can be written as ρ = ρ_{1} → … → ρ_{k} → τ where τ = 0 or τ = X. We define 0^{ρ} := λv_{1}^{ρ_{1}}, …, v_{k}^{ρ_{k}}.0^{0} resp. 0^{ρ} := λv_{1}^{ρ_{1}}, …, v_{k}^{ρ_{k}}.0_{X}.

Notation 2.16 Following [45] we often write ‘(1 − λ)x ⊕ λy’ for ‘W (x, y, λ)’.

Definition 2.17 1) Let (X, d) be a metric space. A function f : X → X is called nonexpansive (short: ‘f n.e.’) if

∀x, y ∈ X(d(f(x), f(y)) ≤ d(x, y)).

2) Let (X, d, W) be a hyperbolic space. A function f : X → X is called directionally nonexpansive (short: ‘f d.n.e.’) if

∀x ∈ X∀y ∈ seg(x, f(x))(d(f(x), f(y)) ≤ d(x, y)).

3 The main results

A bounded hyperbolic space is a hyperbolic space (X, d, W) where (X, d) is a bounded metric space, i.e. for some K ∈ IN: d(x, y) ≤ K for all x, y ∈ X.

6The reason why we denote this constant (which represents some arbitrary element of X) by ‘zero’ is that we use it in remark refrem.2.14.2) (in the same way is 0^{0} is used for the old types) to construct for each type a specific closed term of that type. In the case of normed linear spaces to be treated further below it will actually denote the 0-vector.

Definition 3.1 Let X be a non-empty 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_{ρ}.

Definition 3.2 We say that a sentence of L(A^{ω}[X, d, W]) holds in a bounded hyperbolic space (X, d, W) if it holds in the model of A^{ω}[X, d, W] 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, b_{X} is interpreted as some integer upper bound (also denoted ‘b’) for d, 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) := (d(x, y))_{∘}, where (·)_{∘} refers to the construction in definition 2.9.

Notation 3.3 For better readability we write when we want to express that a sentence A holds in (X, d, W) usually in A ‘d(x, y) ≤ 2^{−k}’ or ‘∀λ ∈ [0, 1](W (x, y, λ) = …)’ instead of ‘d_{X}(x, y) ≤_{IR} 2^{−k}’ or ‘∀λ^{1}(W_{X}(x, y, λ̃) =_{X} …)’ etc. Only when the syntactical form of A as a formal sentence of L(A^{ω}[X, d, W]) matters we have to spell out the precise formal representation.

Definition 3.4 Between functionals x^{ρ}, y^{ρ} of type ρ ∈ T we define a relation ≤_{ρ} by induction on ρ as follows:

x ≤_{0} y :≡ x ≤ y for the usual (prim.rec.) order on IN

x ≤_{ρ→τ} y :≡ ∀z^{ρ}(x(z) ≤_{τ} y(z)).

Definition 3.5 We say that a type ρ ∈ T^{X} has degree 1 if ρ = 0 → … → 0 (including ρ = 0). ρ has degree (0, X) if ρ = 0 → … → 0 → X (including ρ = X). A type ρ ∈ T^{X} has degree (1, X) if it has the form τ_{1} → … → τ_{k} → X (including ρ = X), where τ_{i} has degree 1 or (0, X).

Definition 3.6 A formula F is called ∀-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 quantifier and the types in \underline{σ} are of degree 1 or (1, X).

Theorem 3.7 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 B_{∀}(x^{σ}, y^{ρ}, z^{τ}, u^{0}) (C_{∃}(x^{σ}, y^{ρ}, z^{τ}, v^{0})) be a ∀-formula containing only x, y, z, u free (resp. a ∃-formula containing only 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 (non-empty) metric space (X, d) whose metric is bounded by b ∈ IN. The computational complexity of Φ can be estimated in terms of the strength of the A^{ω}-principle instances actually used in the proof (see remark 3.8 below).

2) For bounded hyperbolic spaces (X, d, W) statement ‘1)’ holds with ‘A^{ω}[X, d, W], (X, d, W)’ instead of ‘A^{ω}[X, d], (X, d)’.

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.

Remark 3.8 The proof of theorem 3.7 actually provides an extraction algorithm for Φ. The functional Φ can always be defined in the calculus T +BR of so-called bar recursive functionals, where T refers to Gödel’s primitive recursive functionals T ([12]) and BR refers to Spector’s schema of bar recursion ([48]). However, for concrete proofs usually only small fragments of A^{ω}[X, d, W] (corresponding to fragments of A^{ω}) will be needed to formalize the proof. In a series of papers we have calibrated the complexity of uniform bounds extractable from various fragments of A^{ω} (see e.g. [28],[29]). In particular, it follows from these results that a single use of sequential compactness only gives rise to at most primitive recursive complexity in the sense of Kleene (often only simple exponential complexity) and this corresponds exactly to the complexity of the bounds obtained in [31],[33](see applications 3.14,3.16 below and [35] for a general discussion). In many cases (e.g. if instead of sequential compactness only Heine-Borel compactness is used relative to weak arithmetic reasoning) even bounds which are polynomial in the input data can be obtained ([28]).

Remark 3.9 1) The most important aspect of theorem 3.7 is that the bound Φ(x, b) does not depend on y, z nor does it depend on X, d or W.

2) Theorem 3.7 holds also for convex metric spaces (resp. spaces of hyperbolic type) if in A^{ω}[X, d, W] the W_{X}-axioms (6) − (8) (resp. (8)) are dropped. However, then the extensionality of W_{X} is no longer provable so that one has to rely on the weak rule of quantifier-free extensionality instead which makes it harder to verify whether a given proof can in fact be formalized in such a setting. In the absence of (6), we extend the existing rule QF-ER by

(+) \frac{A_{0} → s^{1} =_{IR} t^{1}}{A_{0} → W_{X}(x, y, s̃) =_{X} W_{X}(x, y, t̃)} (A_{0} quantifier-free)

to have also for the scalar at least weak extensionality of W_{X} (A_{0} is quantifierfree). Note that the ‘official’ equality relation for type-1-objects is =_{1} so that (+) is not covered by QF-ER. The proofs of the main results also hold with this extended form of QF-ER. In the presence of (6), (+) is, of course, redundant.

Notation 3.10 Let f : X → X, then F ix(f) := {x ∈ X | x = f(x)}.

Corollary 3.11 1) Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space) and B_{∀}(x^{1}, y^{1}, z, f, u), C_{∃}(x^{1}, y^{1}, z, f, v) be as in the previous theorem. If A^{ω}[X, d, W] proves that

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

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

∀y ∈ K∀z ∈ X∀f : X → X( f n.e. ∧ ∀u ≤ Φ(x, b) B_{∀} → ∃v ≤ Φ(x, b) C_{∃})

holds in any hyperbolic space (X, d, W) whose metric is bounded by b.

2) An analogous result holds if ‘f n.e.’ is replaced by ‘f d.n.e’. Similarly for A^{ω}[X, d], (X, d).

Remark 3.12 Remark 3.8 applies to corollary 3.11 as well.

Proof: 1) The statement provable by assumption in A^{ω}[X, d, W] can be written as

∀x ∈ P ∀y ∈ K∀z^{X}, w^{X}, f^{X→X}( f n.e. ∧ f(w) =_{X} w ∧ ∀u ∈ IN B_{∀} → ∃v ∈ IN C_{∃}),

‘f(w) =_{X} w’ can be written as ‘∀k^{0}(d_{X}(w, f(w)) ≤_{IR} 2^{−k})’ where ‘d_{X}(w, f(w)) ≤_{IR} 2^{−k}’ and ‘f n.e.’ are ∀-formulas. Moreover, using the representation of P (resp. K) in A^{ω} quantification over x ∈ P (resp. y ∈ K) is expressed as quantification over all x^{1} (all y^{1} ≤ M for some closed function term M).^{7} Hence by theorem 3.7 there is a functional Φ such that for all x ∈ P, b ∈ IN, if ⟨x⟩ ∈ IN^{IN} represents x then

\{ \begin{matrix}∀y ∈ K∀z, w ∈ X∀f : X → X \\ ( f n.e. ∧ d(w, f(w)) ≤ 2^{−Φ(⟨x⟩,b)} ∧ ∀u ≤ Φ(⟨x⟩, b) B_{∀} → ∃v ≤ Φ(⟨x⟩, b) C_{∃}) \end{matrix}

holds in any b-bounded hyperbolic space (X, d, W), where Φ(⟨x⟩, b) depends on the representative ⟨x⟩ ∈ IN^{IN} of x ∈ P. By theorem 1 in [10] we have (since X is a bounded hyperbolic space),

∀n ∈ IN∃w ∈ X(d(w, f(w)) ≤ 2^{−n}).

Hence the corollary follows.

2) follows like 1) observing that ‘f directionally nonexpansive’ is – formalized in L(A^{ω}[X, d, W]) – a ∀-formula as well, namely

∀x^{X}∀λ^{1}(d_{X}(f(x), f(W_{X}(x, f(x), λ̃))) ≤_{IR} d_{X}(x, W_{X}(x, f(x), λ̃))).
⊣

Remark 3.13 Perhaps the most remarkable aspect of corollary 3.11 is that the restriction to functions f having a fixed point in the premise can be removed from the proof of the conclusion. This is significant since it is well-known that unless the space X has special geometric properties (e.g. being uniformly convex), nonexpansive selfmappings (not even of closed bounded convex subsets of Banach spaces) in general do not have a fixed point, whereas they do have approximate fixed points. Since the corollary (see its proof) reduces the assumption of a fixed point to that of approximate fixed points, the assumption becomes vacuous. In [32] we showed how to achieve such a reduction in the concrete case of a proof due to Groetsch [14]. In application 3.30 below we see that this can can be subsumed under the general metatheorems proved in this paper.

7For details concerning such representations see [25].

Application 3.14 Let (X, d, W) be a bounded hyperbolic space.

Let k ∈ IN, k ≥ 1 and (λ_{n})_{n∈IN} ⊂ [0, 1 − \frac{1}{k}] with ∑_{n=0}^{∞} λ_{n} = ∞ and define for

f : X → X, x ∈ X the Krasnoselski-Mann iteration starting from x by

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

In [10](Theorem 1) the following is proved^{8}

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

The proof given in [10] can easily be formalized in A^{ω}[X, d, W] (see the discussion below). As an application of corollary 3.11 we immediately obtain the following much stronger uniform version (see the discussion below): There exists (under the same assumptions on (λ_{n})) for any l, b ∈ IN an n ∈ IN such that

∀m ≥ n∀x ∈ X∀f : X → X( f nonexpansive → d(x_{m}, f(x_{m})) < 2^{−l})

holds in any b-bounded hyperbolic space (X, d, W) (i.e. the convergence d(x_{n}, f(x_{n})) → 0 is uniform in x, f and – except for b – in (X, d, W)). Moreover, the convergence depends on (λ_{n}) only via k and a function α : IN → IN

such that ∀m ∈ IN(m ≤ ∑_{i=0}^{α(m)} λ_{i}) and n is given by a computable functional Φ(k, α, b, l)

in k, α, b, l.

Proof: As mentioned already, A^{ω}[X, d, W] proves the following (formalized version of Theorem 1 in [10]): if k ≥ 1, λ_{(·)}^{0→1}, α : IN → IN are 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 ∈ IN, x^{X}, f^{X→X}( f nonexpansive → ∃n ∈ IN(d_{X}(x_{n}, f(x_{n})) <_{IR} 2^{−l})), where ‘(∗)’ is a ∀-formula and ‘d_{X}(x_{n}, f(x_{n})) <_{IR} 2^{−l}’ is a ∃-formula. By our representation of [0, 1] (lemma 2.8) we can assume that λ_{(·)} ≤_{0→1} λn.N^{1}. Hence (the proof of)^{9} corollary 3.11 yields the existence of a computable functional Φ(k, α, b, l) such that for n := Φ(k, α, b, l)

8For the case of normed linear spaces X and bounded convex subsets C ⊂ X this result is already due to [18]. [10] even treats spaces of hyperbolic type.

∀(λ_{m}) ⊂ [0, 1]^{∞}∀x ∈ X∀f : X → X((∗) ∧ f n.e. → d(x_{n}, f(x_{n})) < 2^{−l})

holds in any b-bounded hyperbolic space (X, d, W). One easily shows (see [10]) that (d(x_{n}, f(x_{n})))_{n∈IN} is a non-increasing sequence. Hence d(x_{n}, f(x_{n})) < 2^{−l} implies that

∀m ≥ n(d(x_{m}, f(x_{m})) < 2^{−l}),

which finishes the proof. ⊣

Remark 3.15 In [33](cor.3.14,rem.3.11) the following explicit bound Φ(k, α, b, l) are constructed (see also the discussion below)

Φ(k, α, b, l) := α̂(⌈2b · exp(k(M + 1))⌉ − 1, M)), where
M := (1 + 2b) · 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].

For b-bounded convex subsets of normed spaces this bound was already extracted in [31].

Application 3.14 continued: Corollary 3.11 not only allows one to get a uniform bound on existential quantifiers in the conclusion but also on universal quantifiers occurring in implicative premises (as we used already for eliminating the assumption ‘F ix(f) ≠ ∅’). In application 3.14 such a premise is ‘f is nonexpansive’ which can be written as

∀i^{0}∀y_{1}^{X}, y_{2}^{X}(d_{X}(f(y_{1}), f(y_{2})) ≤_{IR} (1 + 2^{−i}) ·_{IR} d_{X}(y_{1}, y_{2})),

9The proof shows that the only fact about the Polish space K used is that it can be represented by functions bounded by some fixed function M which for [0, 1]^{∞} follows immediately from our representation of [0, 1]. Instead we also could have used corollary 3.11 directly by referring to the standard representation of [0, 1]^{∞} as a A^{ω}-definable compact Polish space w.r.t. the product metric (see [47]).

where ∀y_{1}^{X}, y_{2}^{X}(d_{X}(f(y_{1}), f(y_{2})) ≤_{IR} (1 + 2^{−i}) ·_{IR} d_{X}(y_{1}, y_{2})) itself is a ∀-formula. Moreover, we can even treat the fact that (x_{n}) is defined to satisfy

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

as an assumption on some new parameter (x_{(·)}) of type 0 → X which is of degree (1, X) so that our bounds are uniform in (x_{(·)}). (∗) can be written as

(∗∗) ∀j, n(d_{X}(x_{0}, x) ≤_{IR} 2^{−j} ∧ d_{X}(x_{n+1}, (1 − λ_{n})x_{n} ⊕ λ_{n}f(x_{n})) ≤_{IR} 2^{−j}),

where d_{X}(x_{0}, x) ≤_{IR} 2^{−j} ∧ d_{X}(x_{n+1}, (1 − λ_{n})x_{n} ⊕ λ_{n}f(x_{n})) ≤_{IR} 2^{−j} is a ∀-formula. Hence we get in total: There exists a computable functional Φ(k, α, b, l) such that for all α ∈ IN, k, b, l ∈ IN, k ≥ 1 the following holds: Let (λ_{n}) be any sequence in [0, 1] which satisfies

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

(X, d, W) be any b-bounded hyperbolic space, x ∈ X, f : X → X and (x_{(·)}) be any sequence in X such that

∀y_{1}, y_{2} ∈ X(d(f(y_{1}), f(y_{2})) ≤ (1 + 2^{−Φ(k,α,b,l)}) · d(y_{1}, y_{2}))

and

∀n ≤ Φ(k, α, b, l)(d(x_{0}, x), d(x_{n+1}, (1 − λ_{n})x_{n} ⊕ λ_{n}f(x_{n})) ≤ 2^{−Φ(k,α,b,l)}),

then

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

So in order to achieve an approximate fixed point property along (x_{n}) it is sufficient that f is approximately nonexpansive and x_{n+1} is close to (1−λ_{n})x_{n}⊕λ_{n}f(x_{n}) where a bound on the allowed error terms is given by Φ.

Discussion: Application 3.14, in particular, yields Theorem 2 in [10] as an immediate consequence of our theorem 3.7 and the already mentioned Theorem 1 in [10], whereas [10] uses a functional analytic embedding argument: Theorem 2 of [10] states that (under the conditions on (λ_{n}) as in application 3.14) for any fixed bounded hyperbolic space the convergence d(x_{n}, f(x_{n})) → ∞ is uniform in the starting point x and the nonexpansive function f : X → X. The proof of Theorem 1 given in [10] can be formalized already in a small fragment of A^{ω}[X, d, W]. The formalization is particularly simple if one observes that the main part of the proof consists of establishing a certain inequality which is purely universal and therefore can be taken as an implicative assumption without changing the overall logical form of the statement. Hence it is not even necessary to verify whether this inequality actually is provable in A^{ω}[X, d, W] (see [34] for a discussion of this point). Extensionality issues of the kind discussed above do not occur since the extensionality of W and d trivially follows from the (X, d, W)-axioms and the extensionality of f follows from its assumed nonexpansivity so that, indeed every nonexpansive object f^{X→X} of type X → X defines a function f : X → X. As mentioned before, the proof of theorem 3.7 provides an algorithm for actually extracting an explicit uniform rate of convergence Φ. In [31] (for the case of convex subsets of normed linear spaces) and in [33] (for hyperbolic spaces) this has been carried out by analysing the proof in [4] for a generalization of the (non-uniform) convergence results of [18] and [10] to the case of unbounded convex sets resp. hyperbolic spaces.^{10} This yielded the rate of convergence stated in remark 3.15 and similar rates with even stronger uniformity features: it suffices to assume that there exists a point x^{∗} ∈ X whose iteration sequence is bounded rather than to assume that the whole space X is bounded (see [32],[33]). Moreover, carrying out the extraction algorithm transforms the proof of non-uniform convergence from [10],[4] into a new one for the correctness of the uniform rate of convergence which can again be formulated in ordinary mathematical terms without any reference to logical metatheorems. The relevance of such metatheorems as theorem 3.7 and its application 3.14 is that they provide in this and other cases an a-priori guarantee under easy to check logical conditions that such uniform and computable convergence rates exist already prior to any actual proof analysis.

The proof in [10](Theorem 1) of the (non-uniform) convergence d(x_{n}, f(x_{n})) → 0 easily extends to the larger class of directionally nonexpansive mappings introduced in [21] (see [21],[33]). Hence (see application 3.16 below) corollary 3.11.2 implies (for bounded X) the uniformity of the convergence even in this general setting. This gives an explanation (in general logical terms) why the direct construction in [33], obtained by logical analysis of that extension of the proof from [10] (in the modified form of [4]) of an explicit uniform rate of convergence was possible. Prior to [33], only the ineffective uniform convergence in x, f for the case of constant λ_{n} := λ ∈ (0, 1) and in the setting of bounded convex subsets of normed linear spaces was known due to [21], where a novel functional analytic embedding technique was used.

10The proof given in [4] is based on a small modification of the proof in [10] for the bounded case.

Application 3.16 Let (X, d, W) be a bounded hyperbolic space.

A^{ω}[X, d, W] proves that for all k ∈ IN, k ≥ 1 and (λ_{n})_{n∈IN} ⊂ [0, 1 − \frac{1}{k}] with ∑_{n=0}^{∞} λ_{n} =

∞ the following holds

∀x^{X}, f^{X→X}( f directionally nonexpansive → lim_{n→∞} d_{X}(x_{n}, f(x_{n})) = 0).

Hence (under the same assumptions on (λ_{n})) there exists for any l, b ∈ IN an n ∈ IN such that

∀m ≥ n∀x ∈ X∀f : X → X( f dir. nonexpansive → d(x_{m}, f(x_{m})) < 2^{−l})

holds in any b-bounded hyperbolic space (X, d, W) (i.e. the convergence d(x_{n}, f(x_{n})) → 0 is uniform in x, f and – except for b – in (X, d, W)). Moreover, the convergence depends on (λ_{n}) only via k and a function α : IN → IN

such that ∀m ∈ IN(m ≤ ∑_{i=0}^{α(m)} λ_{i}) and n is given by a computable functional Φ(k, α, b, l)

in k, α, b, l.

As in application 3.14 it suffices to assume f to be approximately directional nonexpansive:

∀y ∈ X∀z ∈ seg(y, f(y)) (d(f(y), f(z)) ≤ (1 − 2^{−Φ(k,α,b,l}) · d(y, z))

to obtain an n ≤ Φ(k, α, b, l) such that d(x_{n}f(x_{n})) < 2^{−l}. However, in contrast to the situation in application 3.14 we cannot weaken the requirement that

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

to an approximate form (see the discussion below).

Proof: Exactly as the proof of application 3.14. Since f is only assumed to be directionally nonexpansive, we cannot derive full extensionality of f but have to rely on the quantifier-free extensionality rule. That rule, however, is sufficient to formalize the adaptation of the proof of theorem 1 from [10] given in [33]: inspection of the proof shows that extensionality of f is only used to prove d_{X}(f(x_{n}), f(x_{n+1})) ≤_{IR} d_{X}(x_{n}, x_{n+1}) which follows from the directional nonexpansivity of f and f(x_{n+1}) =_{X} f(W_{X}(x_{n}, f(x_{n}), λ̃_{n})). The latter can be proved in A^{ω}[X, d, W] from the provable (by the explicit recursive definition of (x_{n})) fact that x_{n+1} =_{X} W_{X}(x_{n}, f(x_{n}), λ̃_{n}) by an application of QF-ER. ⊣

Remark 3.17 In [33] it is shown that the bound mentioned already in remark 3.15 actually also holds for directionally nonexpansive mappings.

Discussion: Since the need to use the quantifier-free rule of extensionality in the proof above requires

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

to be proved rather than assumed as a hypothesis on some parameter x_{(·)} we have to define in A^{ω}[X, d, W] the sequence (x_{n}) explicitly by recursion from x, f by means of an appropriate recursor operator of A^{ω}[X, d, W]. As a result we cannot treat the recursive equations as implicative assumptions and therefore cannot relax the equality by an approximate equality as in application 3.14. In logical terms this corresponds to the fact that the system A^{ω}[X, d, W] is not closed under the deduction theorem for axioms which are used to prove premises of the quantifier-free extensionality rule. Rather than being a disadvantage of the logical approach this restriction is necessary which can be explained in ordinary mathematical terms as follows: the need to establish ‘enough extensionality’ to formalize the proof prevents us from permitting an error term in the Krasnoselski-Mann iteration which in general would be incorrect as f can even be discontinuous outside of line segments seg(x, f(x)) (see [33] for an example).

Remark 3.18 In this paper we do not consider the condition of completeness on metric spaces since it is never needed in our applications. Let us, however, indicate how we could treat the subclasses of complete metric and hyperbolic spaces in our setting. Within A^{ω}[X, d] one can introduce the completion of X by considering all Cauchy sequences (x_{n}) ⊂ X with fixed Cauchy modulus. Quantification over such sequences reduces to quantification over all elements x^{0→X} of type 0 → X (without changing the logical complexity) by adapting the construction x̂ from [25] (used there for Polish spaces) which has the properties that

1) If ∀n ∈ IN(d_{X}(x(n), x(n + 1)) <_{IR} ⟨5 · 2^{−n−1}⟩), then ∀n(x(n) =_{X} x̂(n)),

2) For all x^{0→X} : ∀n ∈ IN(d_{X}(x̂(n), x̂(n + 1)) <_{IR} ⟨7 · 2^{−n−1}⟩). x̂ can be defined in A^{ω}[X, d] as follows

x̂(n) := \{ \begin{matrix}x(n), if ∀k < n([d_{X}(x(k), x(k + 1))](k + 1) <Q ⟨6 · 2^{−k−1}⟩), \\ x(k) for the least k < n s.t. ¬[…] otherwise. \end{matrix}

So quantification ∀x ∈ X̂A(x) over the completion X̂ of X is expressed as ∀x^{0→X}A(x̂), where A is an X̂-extensional property

∀x^{0→X}, y^{0→X}(x =_{X} y ∧ A(x) → A(y)).

Here

x =_{X} y :≡ d̂_{X}(x, y) =_{IR} 0_{IR},

where

d̂_{X}(x^{0→X}, y^{0→X})(n) :=_{0} [d_{X}(x̂(n + 5), ŷ(n + 5))](n + 5)

is the extension of d_{X} to X̂. A function F : X̂ → X̂ is given by an =_{X}-extensional functional f of type (0 → X) → 0 → X.

We now discuss the case of (real)^{11} normed linear spaces (X, ∥ · ∥) and bounded convex subsets C ⊂ X. Things are more complicated here as C itself is not a normed space. One way to cover this situation would be to use the characterization due to [43] of convex subsets of normed spaces in the setting of convex metric spaces in terms of further conditions on the function W. The additional conditions needed are

(I) that convex combinations do not depend on the order in which they are carried out and

(II) that the distance is homothetic.

In [43] it is proved that if X is a convex metric space satisfying (I),(II),^{12} then there is an isometry from X onto a convex subset of some normed space E which preserves convex combinations. Over the W -axioms (i)-(iv) one can formulate (I),(II) equivalently as purely universal conditions. So by just adding these conditions, our proof of theorem 3.7 extends without any change to this setting. However, the construction of the supporting space E is quite complicated and E is not fully uniquely determined by C. Moreover, a metatheorem covering normed linear spaces rather than only bounded convex subsets can be expected to have many more applications then the ones in fixed point theory treated in this paper. We first prove a metatheorem for general normed spaces which shows that (under logical conditions similar to the ones in theorem 3.7) one can get bounds uniform in norm-bounded parameters. This setting already allows us to establish uniformity for bounded closed balls. In a further theorem we will then ‘add’ an arbitrary bounded convex subset via its characteristic function. Here we will have again to consider extensionality issues as we only can stipulate weak extensionality for that characteristic function. Nevertheless, our theorem covers an application to a theorem of [14] obtained in [32].

11For simplicity we restrict ourselves in this paper to linear spaces over IR. However, we don’t expect any significant problems in covering the complex case as well.

12In the presence of (I),(II), the conditions (ii)-(iv) become derivable.

The theory A^{ω}[X, ∥ · ∥]: A^{ω}[X, ∥ · ∥] results from A^{ω} by

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

(ii) adding constants 0_{X}, 1_{X} of type X,

(iii) adding new constants +_{X} of type X → X → X, −_{X} of type X → X, ·_{X} of type 1 → X → X, ∥ · ∥_{X} of type X → 1 together with the axioms (writing as usual x+_{X}y, x−_{X}y, ∥x∥_{X} and α·_{X}x (or even αx) for +_{X}(x, y), +_{X}(x, −_{X}y), ∥·∥_{X}(x) and ·_{X}(α, x)):

(0) The (purely universal) vector space axioms for +_{X}, −_{X}, ·_{X}, 0_{X}, formulated with the equality relation =_{X} between objects of type X as defined below,

(1) ∀x^{X}(∥x −_{X} x∥_{X} =_{IR} 0_{IR}),
(2) ∀x^{X}, y^{X}(∥x −_{X} y∥_{X} =_{IR} ∥y −_{X} x∥_{X}),
(3) ∀x^{X}, y^{X}, z^{X}(∥x −_{X} z∥_{X} ≤_{IR} ∥x −_{X} y∥_{X} +_{IR} ∥y −_{X} z∥_{X}),
(4) ∀α^{1}, x^{X}, y^{X}(∥αx −_{X} αy∥_{X} =_{IR} |α|_{IR} ·_{IR} ∥x −_{X} y∥_{X}),
(5) ∀α^{1}, β^{1}, x^{X}(∥αx −_{X} βx∥_{X} =_{IR} |α −_{IR} β|_{IR} ·_{IR} ∥x∥_{X}),

(6) ∀x^{X}, y^{X}, u^{X}, v^{X}(∥(x +_{X} y) −_{X} (u +_{X} v)∥_{X} ≤_{IR} ∥x −_{X} u∥_{X} +_{IR} ∥y −_{X} v∥_{X}),

(7) ∀x^{X}, y^{X}(∥(−_{X}x) −_{X} (−_{X}y)∥_{X} =_{IR} ∥x −_{X} y∥_{X}),

(8) ∀x^{X}, y^{X}(|∥x∥_{X} −_{IR} ∥y∥_{X}|_{IR} ≤_{IR} ∥x −_{X} y∥_{X}).

Still only equality at type 0 is a primitive predicate. x^{X} =_{X} y^{X} is defined as ∥x −_{X} y∥_{X} =_{IR} 0_{IR}. Equality for complex types is defined as before as extensional equality using =_{0} and =_{X}.

Remark 3.19 A remark similar to remark 2.14 applies here: The additional axioms of A^{ω}[X, ∥ · ∥] express (modulo our representation of IR and [0, 1] sketched above) that:

1) (X, +_{X}, −_{X}, 0_{X}) is a (real) linear space with a pseudo-norm ∥ · ∥_{X}.

2) 1_{X} is an element of norm 1 in X.^{13}

The reason for the somewhat non-standard set of axioms (0) − (8) is as follows: since the only equality relation =_{X} we have for X-objects is defined in terms of +_{X}, −_{X}, ∥ · ∥_{X} we have to prove that it is reflexive, symmetric and transitive and that the vector space operations and the norm are =_{X}-extensional. The equality axioms follow immediately from (1) − (3). (4), (5) imply the extensionality of the scalar product

∀α^{1}, β^{1}, x^{X}, y^{X}(α =_{IR} β ∧ x =_{X} y → αx =_{X} βy).

(6), (7) imply the extensionality of +_{X} and −_{X}

∀x^{X}, y^{X}, u^{X}, v^{X}(x =_{X} y ∧ u =_{X} v → x +_{X} y =_{X} u +_{X} v)
∀x^{X}, y^{X}(x =_{X} y → −_{X}x =_{X} −_{X}y).

(8) yields the extensionality of ∥ · ∥_{X}

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

Hence ∥ · ∥_{X} is a norm on the set of equivalence classes generated by =_{X} and we can now prove all the usual basic vector space laws and properties of the norm. In particular, the usual axioms for the norm are derivable. Conversely, the axioms (0) − (8) all hold in any (real) normed linear space.

An alternative (but equivalent) approach would be to have just the usual norm axioms and to prove first the =_{X}-properties and the axioms (0) − (8) relying heavily on the extensionality rule QF-ER extended by

13This is equivalent to stating that the normed space is non-trivial, i.e. contains an element x whose norm is strictly positive. We then can define 1_{X} := \frac{x}{∥x∥_{X}} for such an x to get an element of norm 1.

\frac{A_{0} → s =_{IR} t}{A_{0} → ∀x^{X}(s ·_{X} x =_{X} t ·_{X} x)} (A_{0} quantifier-free)

which does not follow from QF-ER as the ‘official’ equality relation for type-1 objects is =_{1} .

As before we don’t form =_{X}-equivalence classes explicitly, but talk about x^{X}, y^{X} together with requirements that e.g. functionals f^{X→X} respect this equivalence relation, i.e.

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

in order to be entitled to refer to f as denoting a function X → X. Also as before it is important to observe that 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). This restricted form of extensionality is crucial for our results to hold (see the discussion at the end of this section).

The theory A^{ω}[X, ∥ · ∥, η] results from A^{ω}[X, ∥ · ∥] by adding a new constant η^{1} of type 1 together with the axiom (writing more short ∥ · ∥ instead of ∥ · ∥_{X})

(9) ∀x^{X}, y^{X}∀k^{0} (∥x∥, ∥y∥ <_{IR} 1_{IR} ∧ ∥\frac{x +_{X} y}{2} ∥ >_{IR} 1 − 2^{−η(k)} → ∥x −_{X} y∥ ≤_{IR} 2^{−k}).

Remark 3.20 (9) expresses that η is a modulus of uniform convexity of X which normally is formulated as follows:

(9^{∗}) ∀x^{X}, y^{X}∀k^{0} (∥x∥, ∥y∥ ≤_{IR} 1_{IR} ∧ ∥\frac{x +_{X} y}{2} ∥ ≥_{IR} 1 − 2^{−η(k)} → ∥x −_{X} y∥ ≤_{IR} 2^{−k}).

(9^{∗}) trivially implies (9). Conversely, A^{ω}[X, ∥ · ∥, η] proves (9^{∗}) with η̃(k) := η(k) + 1 using the continuity of the norm and the scalar product which can be derived in A^{ω}[X, ∥·∥]. The reason why we use the formulation (9) is that it is logically equivalent to a purely universal statement since <_{IR}∈ Σ_{1}^{0} and ≤_{IR}∈ Π_{1}^{0}.

The theory A^{ω}[X, ⟨·, ·⟩] results from A^{ω}[X, ∥ · ∥] by adding the so-called parallelogram law as a further axiom (10) to (1) − (8)

(10) ∀x^{X}, y^{X}(∥x +_{X} y∥_{X}^{2} +_{X} ∥x −_{X} y∥_{X}^{2} =_{IR} 2_{IR} ·_{IR} (∥x∥_{X}^{2} +_{X} ∥y∥_{X}^{2}),

where (·)^{2} is a functional of type 1 → 1 which represents on the representations of real numbers the function x ↦ x^{2} on IR. It is well-known that a norm satisfying (10) allows one to define an inner product function ⟨·, ·⟩ : X × X → IR: define a new functional ⟨·, ·⟩_{X} of type X → X → 1 by (writing ⟨x, y⟩_{X} for ⟨·, ·⟩_{X}(x, y)):

(+) ⟨x^{X}, y^{X}⟩_{X} :=_{1} (⟨\frac{1}{4}⟩)_{IR} ·_{IR} (∥x +_{X} y∥_{X}^{2} −_{X} ∥x −_{X} y∥_{X}^{2}).

⟨·, ·⟩_{X} represents an inner product on the space (of =_{X}-equivalence classes of) X and the norm ∥ · ∥_{X} can be recovered from ⟨·, ·⟩_{X} in the usual way

(++) ∥x∥_{X} := sqrt(⟨x, x⟩_{X}),

where sqrt^{1→1} represents the square root function IR → [0, ∞) on the representation of IR (which can easily be defined by a closed term of A^{ω}). Conversely, whenever a norm ∥ · ∥ is given by a (real valued) inner product via (++) then the norm satisfies (10) and the inner product can be recovered from that norm by (+). The proofs of these facts are all completely elementary (see e.g. [51]) and can be easily carried out in our formal setting. Hence A^{ω}[X, ⟨·, ·⟩] contains a proper axiomatization of the notion of a real inner product space (pre-Hilbert space). Definition 3.21 We say that a sentence of L(A^{ω}[X, ∥ · ∥]) holds in a nontrivial (real) normed linear space (X, ∥ · ∥) if it holds in the model of A^{ω}[X, ∥ · ∥] obtained by letting the variables range over the appropriate universes of the full set-theoretic type structure S^{ω,X} with the sets X, IN as the universes for the base types X and 0, where 0_{X} is interpreted by zero vector 0^{X} 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 the scalar multiplication in the IR-linear space X. Finally, ∥ · ∥_{X} is interpreted by λx ∈ X.(∥x∥)_{∘}, where (r)_{∘} for r ∈ IR_{+} as in definition 2.9. In A^{ω}[X, ∥ · ∥] we can extend the relation x ≤_{ρ} y from types ρ ∈ T to ρ ∈ T^{X}:

Definition 3.22 For functionals x^{ρ}, y^{ρ} of type ρ ∈ T^{X} define x ≤_{ρ} y by

x ≤_{0} y :≡ x ≤ y,
x ≤_{X} y :≡ ∥x∥_{X} ≤_{IR} ∥y∥_{X},
x ≤_{ρ→τ} y :≡ ∀z^{ρ}(x(z) ≤_{τ} y(z)).

Remark 3.23 ≤_{X} is not a partial order since it is not antisymmetric.

Theorem 3.24 1) Let σ be of degree 1 and ρ be of degree 1 or (1, X). s is a closed term of type σ → ρ and B_{∀}, C_{∃} are as in theorem 3.7. If

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

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

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

holds in any non-trivial (real) normed linear space (X, ∥ · ∥).

The computational complexity of Φ can be estimated in terms of the strength of the A^{ω}-principle instances actually used in the proof (3.8 above applies as well, see also remark 3.25 below).

2) For uniformly convex normed linear spaces (X, ∥ · ∥, η) with modulus of convexity η statement ‘1)’ holds with A^{ω}[X, ∥ · ∥, η] and (X, ∥ · ∥, η) instead of A^{ω}[X, ∥ · ∥] and (X, ∥ · ∥). Now (for σ of degree 1) n := Φ(x, η) is given by a computable functional Φ in x and a modulus of uniform convexity η. Analogously for (real) inner product spaces (X, ⟨·, ·⟩).^{14}

The comments about tuples and finite conjunctions of premises hold here as well.

Remark 3.25 Theorem 3.24 also applies to the case where x^{σ} has a type σ of degree (0, X) in the following way: let us first assume that σ = X. Quantification over all x^{X} can be written as ‘∀k^{0}∀x ≤_{X} (k)_{IR} ·_{X} 1_{X}’ so that theorem 3.24 yields a computable functional Φ(k) in k. This can be transformed into a functional Φ(x) in x if we have an operation M : X → IN such that M(x) ≥ ∥x∥. Even for effective normed spaces (X, ∥ · ∥) like IR such an M will not be computable as a function on X (for X = IR the computability of M would imply its continuity and hence M would be constant). However, it will usually be computable in a representative f_{x} ∈ IN^{IN} of x in the sense of the standard representation of Polish spaces as discussed further above. So for computationally meaningful (separable) normed spaces, there will be a computable M^{2} (usually of low complexity) such that M(f_{x}) ≥ ∥x∥ whenever f_{x} is a representative of x ∈ X and we can take Φ(M(f_{x})). For σ = 0 → X we can write quantification over x^{0→X} in the form ‘∀g^{1}∀x ≤_{0→X} λk.(g(k))_{IR} ·_{X} 1_{X}’ and theorem 3.24 yields a computable Φ(g) in g. Using M we can replace g in Φ(g) by λk.M(f_{x(k)}).

14Inner product spaces are uniformly convex with modulus (expressed in terms of ε > 0 rather than 2^{−k}) η(ε) := 1 − (1 − (ε/2)^{2})^{1/2}.

The theory A^{ω}[X, ∥ · ∥, C]: A^{ω}[X, ∥ · ∥, C] results from A^{ω}[X, ∥ · ∥] by adding new constants b_{X} of type 0, c_{X} of type X and χ_{C} of type X → 0 together with the axioms

(11) ∀x^{X}(χ_{C}(x) =_{0} 0 → ∥x∥_{X} ≤_{IR} (b_{X})_{IR}(=_{1} λk^{0}.j(2b_{X}, 0^{0})),

(12) ∀x^{X}, y^{X}, α^{1}(χ_{C}(x) =_{0} χ_{C}(y) =_{0} 0 → χ_{C}((1 −_{IR} α̃) ·_{X} x +_{X} α̃ ·_{X} y) =_{0} 0),

(13) χ_{C}(c_{X}) =_{0} 0.

The theories A^{ω}[X, ∥ · ∥, η, C] and A^{ω}[X, ⟨·, ·⟩, C] are defined analogously. Note that although the vector space operations and ∥·∥ are provably extensional, the characteristic function χ_{C} is not. However, by QF-ER we have the following weak form of χ_{C}-extensionality

\frac{A_{0} → s =_{X} t}{A_{0} → χ_{C}(s) =_{0} χ_{C}(t)} for quantifier-free A_{0}

(see also the discussion at the end of this section).

In the following ‘∀x^{C} A(x)’, ‘∀f^{1→C} A(f)’, ‘∀f^{X→C} A(f)’ and ‘∀f^{C→C} A(f)’ abbreviate

∀x^{X}(χ_{C}(x^{X}) =_{0} 0 → A(x)),
∀f^{1→X}(∀y^{1}(χ_{C}(f(y)) =_{0} 0) → A(f)),
∀f^{X→X}(∀y^{X}(χ_{C}(f(y)) =_{0} 0) → A(f)) and
∀f^{X→X}(∀x^{X}(χ_{C}(x) =_{0} 0 → χ_{C}(f(x)) =_{0} 0) → A(f̃)),

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 ‘→’. 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, τ_{i} = X or τ_{i} = C.

Remark 3.26 If one defines

f^{X→X} =_{C→X} g^{X→X} :≡ ∀x^{X}(χ_{C}(x) = 0 → f(x) =_{X} g(x))

then for all f^{X→X}, g^{X→X} the following provably holds

f =_{C→X} f̃ and f̃ =_{C→X} g̃ ↔ f̃ =_{X→X} g̃.

Remark 3.27 Note that for ρ of degree (1, X, C) a quantifier ‘∀x^{ρ}’ abbreviates

∀x^{ρ′}(B(x) → …),

where ρ′ is is the type of degree (1, X) resulting from ρ by replacing everywhere ‘C’ by ‘X’ and B is (logically equivalent to) a ∀-formula.

For f^{C→C} (i.e. for f^{X→X} satisfying ∀x^{X}(χ_{C}(x) =_{0} 0 → χ_{C}(f(x)) =_{0} 0)) ‘f nonexpansive’ is the ∀-formula

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

Definition 3.28 We say that a sentence A holds in (X, ∥ · ∥) and C if in addition to the requirements in definition 3.21 we stipulate that χ_{C} is interpreted as the characteristic function for C and c_{X} by some arbitrary element in C.

Theorem 3.29 1) Let σ be of degree 1 or (0, X) and ρ be of degree 1 or (1, X) and τ be a type of degree (1, X, C). s is a closed term of type σ → ρ and B_{∀}, C_{∃} are as in theorem 3.7. 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 such that

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

holds in any non-trivial (real) normed linear space (X, ∥·∥) and any non-empty b-bounded convex subset C ⊂ X. The computational complexity of Φ can be estimated in terms of the strength of the A^{ω}-principle instances actually used in the proof (3.8 and 3.25 apply as before).

2) For uniformly convex normed linear spaces (X, ∥ · ∥, η) with modulus of convexity η statement ‘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 η^{1} of uniform convexity for (X, ∥ · ∥). Analogously for (real) inner product spaces (X, ⟨·, ·⟩).

The comments about tuples and finite conjunctions of premises hold here as well.

Application 3.30 Let (X, ∥·∥, η) be a (non-trivial) uniformly convex normed linear space with convexity modulus η and C ⊂ X a non-empty bounded convex subset. In [14] it is proved (extending earlier results from [36] and [5]) that for all (λ_{n})_{n∈IN} ⊂

[0, 1] with ∑_{n=0}^{∞} λ_{n}(1 − λ_{n}) = ∞ the following holds^{15}

∀x ∈ C, f : C → C( f nonexpansive ∧ F ix(f) ≠ ∅ → lim_{n→∞} d(x_{n}, f(x_{n})) = 0).

The proof can easily formalized in A^{ω}[X, ∥ · ∥, η, C]. Since we cannot prove in A^{ω}[X, ∥ · ∥, η, C] that χ_{X} satisfies the extensionality axiom we have to rely on the weak quantifier-free extensionality rule to prove by induction on n that x_{n} ∈ C using that x_{0} = x ∧ x_{n+1} = (1 − λ_{n})x_{n} + λ_{n}f(x_{n}) provably holds. As an application of theorem 3.29 we get (similarly to corollary 3.11 and application 3.14):

One can extract a computable functional Φ(l, β, b, η) such that for any normed space (X, ∥ · ∥) with modulus of uniform convexity η, for any b-bounded convex subset C ⊂ X and any sequence (λ_{n}) in [0, 1] such that

∀m ∈ IN(m ≤ ∑_{i=0}^{β(m)} λ_{i}(1 − λ_{i}))

the following holds:

∀l∀m ≥ Φ(l, β, b, η)∀x ∈ C∀f : C → C( f nonexpansive → d(x_{m}, f(x_{m}) < 2^{−l})

(i.e. the convergence d(x_{n}, f(x_{n})) → 0 is uniform in x, f and – modulo the bound b resp. β – is also uniform w.r.t. to C and (λ_{n})). We also see (as in corollary 3.11) that the assumption of the existence of a fixed point is no longer needed. Although the latter follows from the fundamental Browder-Göhde-Kirk fixed point theory for uniformly convex Banach spaces X and closed bounded convex subsets C, this is of significance since we don’t need this deep result in our approach at all. In [32] we carried out the extraction algorithm behind the proof of theorem 3.29 applied to the proof in [14] and constructed an explicit uniform rate of convergence together with a completely elementary proof of its correctness as predicted by this application of theorem 3.29. The bound extracted in [32] is

15Note that the condition on (λ_{n}) is less restrictive than the conditions in application 3.14.

Φ(l, β, b, η) := β(⌈3(b + 1) · 2^{η(l+⌈log(b+1)⌉}) · 2^{l−1}⌉),

where η is as in (9^{∗}) above. For the special case of λ_{n} := \frac{1}{2} see also [22] and [30].

Final discussion on extensionality: As we emphasized several times, our systems must be based on weak extensionality (in the sense of QF-ER) only, whereas full extensionality has to be derived from the mathematical axioms of our theories if needed. We saw already in application 3.16 that we otherwise would get false consequences. In fact, suppose we could prove e.g. in A^{ω}[X, d] that

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

which can be written as

∀f^{X→X}∀x^{X}, y^{X}∀k ∈ IN∃n ∈ IN(d_{X}(x, y) ≤_{IR} 2^{−n} → d_{X}(f(x), f(y)) <_{IR} 2^{−k}),

where d_{X}(x, y) ≤_{IR} 2^{−n} (resp. d_{X}(f(x), f(y)) <_{IR} 2^{−k}) is a ∀-formula (resp. an ∃-formula), then theorem 3.7 would imply the existence of a computable function g : IN × IN → IN such that

∀f^{X→X}, ∀x^{X}, y^{X}∀k ∈ IN(d_{X}(x, y) ≤_{IR} 2^{−g(k,b)} → d_{X}(f(x), f(y)) <_{IR} 2^{−k})

holds for any b-bounded metric space (X, d), i.e. we would get that all functions f : X → X are equicontinuous with a common modulus of uniform continuity which, of course, is false for general b-bounded spaces (X, d). Similarly, if we add a new constant K^{X→X} to the system together with the axiom stating that K is extensional: if the resulting system still satisfies theorem 3.7 then we can use theorem 3.7 to infer that K is uniformly continuous on X. Hence theorem 3.7 can only hold if in fact K is assumed already to be uniformly continuous (which implies the extensionality of K). That is why we had to prove full extensionality of e.g. d_{X}, W_{X} and f^{X→X} from the d_{X}, W_{X}-axioms and the assumption on f being nonexpansive implying the uniform continuity of d_{X}, W_{X} and f. For the case of normed spaces, theorem 3.24 implies uniform continuity on the unit ball for all provably fully extensional functions f : X → X or f : X → IR. Again full extensionality of ∥ · ∥_{X}, ·_{X} was derived from their axioms implying in fact the uniform continuity. This is related to the notion of ‘uniform families of L-structures’ which plays in important role in the model theory of Banach spaces (see e.g. [15]). In our proof theoretic approach based on weak extensionality, however, we do not have to make such strong uniform continuity assumptions if the only use of extensionality we make is that provided by QF-ER. E.g. in application 3.16 we did not assume the continuity of our directionally nonexpansive mappings but could, nevertheless, apply theorem 3.7 since QF-ER was enough to formalize the proof. In addition to the effective nature of our results, this is yet another benefit of the proof theoretic approach to functional analysis and there does not seem to be any natural model theoretic counterpart to the weak form of extensionality formalized by QF-ER. In theorem 3.29 and application 3.30 we have another instance of the need to distinguish between full extensionality and weak extensionality: if we would have full extensionality of χ_{C}, then we could use theorem 3.29 to infer results of the kind that points x ∈ X close to C would ‘behave’ similar to points in C. However, unless C is topologically very simple (e.g. a closed ball, where we indeed could express C directly without any use of χ_{C}), this will certainly not be correct in general. Nevertheless, this did not prevent us from making application 3.30 since only QF-ER was used in connection with χ_{C}.

4 Proofs of theorems 3.7,3.24 and 3.29

The proof of theorem 3.7 is based on an extension of Spector’s [48] interpretation of classical analysis A^{ω} by bar recursive functionals (T+BR) to A^{ω}[X, d, W] and a subsequent interpretation of these functionals in an extension of the Howard-Bezem strongly majorizable functionals to T^{X}.^{16} Spector’s work (presented in full detail in [40]) generalizes Gödel’s well-known functional (‘Dialectica’) interpretation for intuitionistic and – via Gödel’s negative translation as intermediate step – classical arithmetic by the primitive recursive functionals R_{ρ} to A^{ω} by showing that the functional interpretation of the negative translation of DC can be realized by his socalled bar recursive functionals defined – in a version of simultaneous bar recursion – as follows:

Definition 4.1 Let \underline{ρ} = ρ_{1}, …, ρ_{m} and \underline{τ} = τ_{1}, …, τ_{k} be tuples of types in T. A^{ω} + (BR) is the extension of A^{ω} obtained by adding constants \underline{B}^{\underline{ρ},\underline{τ}} for simultaneous bar recursion with the axioms

16We will treat the case of A^{ω}[X, d, W] in detail. For A^{ω}[X, d] the proof then simply is obtained by disregarding all issues involving W.

\begin{matrix}(BR^{\underline{ρ},\underline{τ}}) : \\ \{ & \begin{matrix}x_{i}(\overline{\underline{y}, n^{0}}) <_{0} n → B_{i}^{\underline{ρ},\underline{τ}}(\underline{x}, \underline{z}, \underline{u}, n, \underline{y}) =_{τ_{i}} z_{i}(n, \underline{y}) \\ x_{i}(\overline{\underline{y}, n}) ≥_{0} n → B_{i}^{\underline{ρ},\underline{τ}}(\underline{x}, \underline{z}, \underline{u}, n, \underline{y}) =_{τ_{i}} u_{i}(λ\underline{D}\underline{ρ}. \underline{B}^{\underline{ρ},\underline{τ}}(\underline{x}, \underline{z}, \underline{u}, n′, \overline{\underline{y}, n} ∗ \underline{D}, n, \underline{y}) \end{matrix} \end{matrix}

for i = 1, …, k,

(\overline{\underline{y}, n})_{j}(k^{0}) =_{ρ_{j}} \{ \begin{matrix}y_{j}(k), if k < n \\ 0^{ρ_{j}}, otherwise \end{matrix}

and

(\overline{\underline{y}, n} ∗ \underline{D})_{j}(k^{0}) =_{ρ_{j}} \{ \begin{matrix}y_{j}(k), if k < n \\ D_{j}, if k = n \\ 0^{ρ_{j}}, otherwise \end{matrix}

for j = 1, …, m. A^{ω}[X, d, W]+ (BR) results if we add to A^{ω}[X, d, W] the constants \underline{B}^{\underline{ρ},\underline{τ}} together with (BR^{\underline{ρ},\underline{τ}}) for all tuples of types \underline{ρ}, \underline{τ} of the extended set of types T^{X}.

Remark 4.2 As already discussed in connection with recursion, also simultaneous bar recursion can be reduced to ordinary bar recursion in our weakly extensional setting by contracting tuples of functionals into single functionals using appropriate coding functionals. The absence of a pairing function j_{X} : X × X → X makes this technically somewhat involved as we would have to use the second of the options presented in [50](1.6.17) and used in [40]. This is the reason why we prefer to take simultaneous bar recursion (as we did in the case of recursion) as a primitive concept.

In [48],[40] the following rule is proved for sentences A:^{17}

A^{ω} ⊢ A

⇒ one can construct a tuple of closed terms \underline{t} of A^{ω}+(BR) s.t.

A^{ω} + (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 ([12]) of A′.

17The constructive ω-rule used in [40] for the conclusion is actually superfluous, see footnote 3 in [9].

Remark 4.3 Spector actually verified the functional interpretation (A′)_{D}(\underline{t}, \underline{y}) of A′ in a quantifier-free fragment of A^{ω}+(BR) (without the use of DC) but this is not needed for our purpose.

We now indicate how Spector’s result can be extended to A^{ω}[X, d, W].

Lemma 4.4 Let A be a sentence in the language of A^{ω}[X, d, W]. Then the following rule holds:

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

⇒ one can construct a tuple of closed terms \underline{t} of A^{ω}[X, d, W]+(BR) s.t.

A^{ω}[X, d, W] + (BR) ⊢ ∀\underline{y} (A′)_{D}(\underline{t}, \underline{y}).

Proof: Spector’s proof extends to A^{ω}[X, d, W] by observing the following points:

1) As in A^{ω} all prime formulas of A^{ω}[X, d, W] are of the form s =_{0} t and hence decidable. As a consequence of this, one can construct for any quantifier-free formula A_{0}(\underline{a}) (having only the free variables \underline{a}) a closed term t_{A_{0}} such that

A^{ω}[X, d, W] ⊢ ∀\underline{a}(t_{A_{0}}(\underline{a}) =_{0} 0 ↔ A_{0}(\underline{a})).

2) Using 1) the soundness of negative translation and subsequent functional interpretation for the logical axioms and rules, QF-ER and QF-AC extend to the new set of types T^{X} without any changes (using our extended closed terms 0^{ρ} at a few places). For QF-ER we use that =_{X} is purely universal and hence =_{ρ} is purely universal for all types ρ ∈ T^{X}.

3) The functional interpretation of the negative translation of the axiom schema of induction easily extends to all instances over the extended language and types T^{X} using \underline{R}\underline{ρ} for all \underline{ρ} ∈ T^{X}. As for the types T, the verification becomes particularly perspicuous if one treats IA in the equivalent form of an induction rule IR (see [50](3.5.5(iii))).

4) The functional interpretation of the negative translation of the axiom schema of dependent choice DC easily extends to all instances over the extended language and types T^{X} using \underline{B}^{\underline{ρ},\underline{τ}} for all type tuples \underline{ρ}, \underline{τ} ∈ T^{X}.

5) The functional interpretations of the negative translations of the axioms (1)- (8) are trivially equivalent to these axioms themselves as they are all purely universal and don’t contain ∨.

⊣

We now extend Bezem’s [3] type structure of hereditarily strongly majorizable functionals (which relies on a variant of Howard’s [16] notion of majorizability) to all types of T^{X}:

Definition 4.5 The extensional type structure M^{ω,X} := ⟨M_{ρ}⟩_{ρ∈T^{X}} of all hereditar-

ily strongly majorizable set-theoretical functionals of type ρ ∈ T^{X} over IN and a set X is defined as

M_{0} := IN, n s-maj_{0} m := n ≥ m ∧ n, m ∈ IN,
M_{X} := X, x^{∗} s-maj_{X} x :≡ x^{∗}, x ∈ M_{X},
x^{∗} s-maj_{τ→ρ} x :≡

x^{∗}, x ∈ M_{ρ}^{M_{τ}} ∧ ∀y^{∗}, y ∈ M_{τ} (y^{∗} s-maj_{τ} y → x^{∗}(y^{∗}) s-maj_{ρ} x^{∗}(y), x(y))

M_{τ→ρ} := {x ∈ M_{ρ}^{M_{τ}} | ∃x^{∗} ∈ M_{ρ}^{M_{τ}} : x^{∗} s-maj_{τ→ρ} x} (ρ, τ ∈ T^{X}) .

Here M_{ρ}^{M_{τ}} denotes the set of all total set-theoretical mappings from M_{τ} into M_{ρ}.

Lemma 4.6 1) x^{∗}, x ∈ M_{ρ}^{M_{τ}} ∧ x^{∗} s-maj x → x^{∗} s-maj x^{∗} ∧ x^{∗}, x ∈ M_{τ→ρ}.

2) Let ρ = ρ_{1} → … → ρ_{k} → τ. Then

x^{∗} s-maj_{ρ} x ↔

∀y_{1}^{∗}, y_{1}, …, y_{k}^{∗}, y_{k}( ⋀_{i=1}^{k}(y_{i}^{∗} s-maj_{ρ_{i}} y_{i}) → x^{∗}y_{1}^{∗} … y_{k}^{∗} s-maj_{τ} x^{∗}y_{1} … y_{k}, xy_{1} … y_{k}).

Proof: ‘1)’ is trivial, and ‘2)’ follows by induction on k using heavily ‘1)’. ⊣

There is an obvious syntactic counterpart of s-maj formulated in L(A^{ω}[X, d, W]) which we denote by ‘s-maj’ as well: for x^{ρ}, y^{ρ} we define s-maj_{ρ} as follows

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

Lemma 4.7 Let (X, d, W) be a non-empty bounded hyperbolic space. Then M^{ω,X} is a model of A^{ω}[X, d, W]+(BR) (for a suitable interpretation of the constants of A^{ω}[X, d, W]+(BR) in M^{ω,X}). Moreover, for any closed term t of A^{ω}[X, d, W]+(BR) one can construct a closed term t^{∗} which does not contain W_{X} and d_{X} such that

M^{ω,X} ⊧ t^{∗} s-maj t.

Proof: The constants of A^{ω}+(BR) – which are characterized by their defining axioms – are interpreted as in [3] except that they are now taken over the extended set of types T^{X} where M_{X} := X. For the new constants we take (writing simply M for M^{ω,X})

[b_{X}]_{M} := b ∈ IN for some bound b on d,
[0_{X}]_{M} := c for some c ∈ X,
[d_{X}]_{M} := λx, y ∈ X.(d(x, y))_{∘},
[W_{X}]_{M} := λx, y ∈ Xλα ∈ IN^{IN}. W (x, y, rα̃),

where (x)_{∘} is the construction from definition 2.9 and rα̃ ∈ [0, 1] is the unique real number represented by α̃ (see lemma 2.8).

In order to show that all these functionals are in M^{ω,X} we have to construct majorants. For the constants of A^{ω}+(BR) this is done (using lemma 4.6) as in [3] (see also [23])^{18}, but we have – in order to deal with the new types – to extend the functional max_{ρ} to the new types so that we still have the crucial property^{19}

∀x^{∗}, x, y^{∗}, y(x^{∗} s-maj_{ρ} x ∧ y^{∗} s-maj_{ρ}y → max_{ρ}(x^{∗}, y^{∗}) s-maj_{ρ} max_{ρ}(x, y), x, y).

18Bezem uses a variant of (BR) based on types for finite sequences \overline{y}(n) for y^{0→ρ}, n^{0} (and uses in x(\overline{y, n}) instead of our version of \overline{x, n} the variant where (y0, …, y(n−1)) is continued constantly with y(n − 1)). In the presence of sequence codings, sequence types can be defined. However, we don’t have a pairing function for the type X and therefore want to avoid sequence types altogether. This is achieved by our formulation (following e.g. [40]) for which Bezem’s majorizability construction can easily be adapted (see [23]). The proof becomes particularly perspicuous if one proves (as done in [23]) majorizability first for the variant of s-maj which at sequence types 0 → ρ is defined pointwise and then shows how to transform (hereditarily) pointwise majorants into majorants (using the construction x^{M} below for x of type 0 → ρ), see [23, 24].

19It is only this property of the functional max_{ρ} which is used. Instead of max_{ρ} one could have also used e.g. +_{ρ} or similar functionals.

Because of the trivial definition of s-maj for the type X we can simply define

max_{X}(x^{X}, y^{X}) := 0_{X}.

For complex types ρ → τ we define

max_{ρ→τ}(x, y) := λv^{ρ}. max_{τ}(xv, yv).

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

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

One easily shows that the following facts hold in M^{ω,X}

(M) \{ \begin{matrix}(·)^{M} s-maj (·)^{M}, \\ ∀x, y ∈ M_{0→ρ}(∀n ∈ IN(x(n) s-maj_{ρ} y(n)) → x^{M} s-maj_{0→ρ} x, y). \end{matrix}

Using the extended max_{ρ} and x^{M}, the construction of majorants for \underline{R}, \underline{B} easily extends to the new set of types T^{X}. For \underline{B} one needs that M^{ω,X} satisfies the axiom of dependent choice which follows from M_{ρ}^{M_{0}} = M_{0→ρ} (for all ρ ∈ T^{X}) which in turn is a consequence of (M), where we use DC on the meta-level.

For the new constants k := b_{X}, 0_{X}, d_{X}, W_{X} we construct closed terms k^{∗} of A^{ω}[X, d, W] as follows:

b_{X}^{∗} := b_{X}, 0_{X}^{∗} := 0_{X}, d_{X}^{∗} := λx^{X}, y^{X}.M(b_{X}), W^{∗} := λx^{X}, y^{X}, α^{1}.0_{X},

where M is defined in definition 2.9. One easily shows (using lemma 2.10.3 and 2.10.5 for d_{X}) that^{20}

M^{ω,X} ⊧ k^{∗} s-maj k.

Since t^{∗} s-maj_{ρ→τ} t and s^{∗} s-maj_{ρ} s implies that t^{∗}s^{∗} s-maj_{τ} ts the lemma follows. ⊣ Lemma 4.8 Let A be a sentence in the language of A^{ω}[X, d, W]. Then the following rule holds:

20Since the use of lemma 2.10 to show that [d_{X}^{∗}]_{M} s-maj [d_{X}]_{M} relies on the special choice of the representation of the real number d(x, y) provided by the construction (·)_{∘} used in [d_{X}]_{M}, we can not prove that

A^{ω}[X, d, W] ⊢ d_{X}^{∗} s-maj d_{X}.

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

Proof: Follows from lemmas 4.7 and 4.4. ⊣

Proof of theorem 3.7:

A^{ω}[X, d, W] ⊢ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(∀u^{0}B_{∀}(x, y, z, u) → ∃v^{0}C_{∃}(x, y, z, v))

implies

A^{ω}[X, d, W] ⊢ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}∃u, v(B_{∀}(x, y, z, u) → C_{∃}(x, y, z, v))

Since the formula

B_{∀}(x, y, z, u) → C_{∃}(x, y, z, v)

prenexes into a ∃-formula, (partial) functional interpretation of (the negative translation of)

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

yields

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

Hence by lemmas 4.7,4.8 there exist closed terms t_{U}^{∗}, t_{V}^{∗} , t_{U}, t_{V} (where t_{U}^{∗}, t_{V}^{∗} do not contain W_{X}, d_{X}) such that

M^{ω,X} ⊧ \{ \begin{matrix}t_{U}^{∗} s-maj t_{U} ∧ t_{V}^{∗} s-maj t_{V} ∧ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ} \\ (B_{∀}(x, y, z, t_{U}(x, y, z)) → C_{∃}(x, y, z, t_{V} (x, y, z))). \end{matrix}

σ is a type of degree 1. Define a functional M^{σ→σ} by^{21}

M(x) := x^{m} := λ\underline{v}^{0}. max_{0}\{x(w_{1}, …, w_{n}) : ⋀_{i=1}^{n}(w_{i} ≤_{0} v_{i})\}.

21For σ = 1, this coincides with the previously defined x^{M}.

Then

M^{ω,X} ⊧ ∀x^{σ}(x^{m} s-maj x).

Moreover, for a closed s^{∗} such that s^{∗} s-maj s, we get using that for ρ ∈ T

(+) x^{∗} s-maj_{ρ} x ∧ x ≥_{ρ} y → x^{∗} s-maj_{ρ} y,

the following

M^{ω,X} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)(s^{∗}(x^{m}) s-maj y).

Since z^{τ} has a type τ of degree (1, X) we have (due to the trivial definition of s-maj_{X}):

M^{ω,X} ⊧ ∀z^{τ}(0^{τ} s-maj_{τ} z).

So in total we obtain:

M^{ω,X} ⊧ \{ \begin{matrix}∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(t_{U}^{∗}(x^{m}, s^{∗}(x^{m}), 0^{τ}) ≥_{0} t_{U}(x, y, z) \\ ∧t_{V}^{∗} (x^{m}, s^{∗}(x^{m}), 0^{τ}) ≥_{0} t_{V} (x, y, z)). \end{matrix}

Hence, taking Ψ(x) := max(t_{U}^{∗}(x^{m}, s^{∗}(x^{m}), 0^{τ}), t_{V}^{∗} (x^{m}, s^{∗}(x^{m}), 0^{τ})),

M^{ω,X} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}[∀u ≤ Ψ(x) B_{∀}(x, y, z, u) → ∃v ≤ Ψ(x) C_{∃}(x, y, z, v)].

Since t_{U}^{∗}, t_{V}^{∗} do not contain W_{X}, d_{X}, the functional [Ψ]_{M} depends on (X, d, W) only via the interpretation of the constant b_{X} by some upper bound of d and the constant 0_{X} by some arbitrary element of X. We can treat b_{X} in Ψ as a variable (also called b) and define a functional Ψ′(b^{0}, x^{σ}) := (Ψ[b])(x). Then for any hyperbolic space (X, d, W) whose metric is bounded by b, (∗) holds with Ψ′(b, x) where 0_{X} in Ψ′ is interpreted by an arbitrary element of X. We now show that also the latter dependency can be eliminated: For ρ ∈ T^{X} we define ρ̂ inductively as follows

ˆ0 := 0, X̂:= 0, ρ̂ → τ := ρ̂ → τ̂,

i.e. ρ̂ is a result of replacing all occurrences of X in ρ by 0. In particular, ρ̂ ∈ T. For ρ ∈ T^{X} we define a relation x_{ρ} ∼_{ρ} y^{ρ} between functionals x_{ρ}, y^{ρ} of types ρ̂, ρ by induction on ρ :

\{ \begin{matrix}x^{0} ∼_{0} y^{0} :≡ x =_{0} y, x^{0} ∼_{X} y^{X} :≡ ⊤, \\ x^{_{ρ}→_{τ}} ∼_{ρ→τ} y^{ρ→τ} :≡ ∀u_{ρ}, v^{ρ}(u ∼_{ρ} v → xu ∼_{τ} yv). \end{matrix}

One easily shows that the following holds in M^{ω,X} 1) 0^{0} ∼_{0} 0^{0}, 0^{0} ∼_{X} 0_{X}, S^{1} ∼_{1} S^{1},

2) Π_{_{ρ},_{τ}} ∼ Π_{ρ,τ}, Σ_{_{δ},_{ρ},_{τ}} ∼ Σ_{δ,ρ,τ}, \underline{R}\underline{_{ρ}} ∼ \underline{R}\underline{ρ}, \underline{B}^{\underline{_{ρ}},\underline{_{τ}}} ∼ \underline{B}^{\underline{ρ},\underline{τ}}.

Let t^{ρ} be a closed term which does not contain W_{X}, d_{X} and t̂_{ρ} the result of replacing

all occurrences of 0_{X}, Π_{ρ,τ}, Σ_{δ,ρ,τ}, \underline{R}\underline{ρ}, \underline{B}^{\underline{ρ},\underline{τ}} in t by 0^{0}, Π_{_{ρ},_{τ}}, Σ_{_{δ},_{ρ},_{τ}}, \underline{R}\underline{_{ρ}}, \underline{B}^{\underline{_{ρ}},\underline{_{τ}}}.

Then t̂_{ρ} is a closed term of A^{ω} and

M^{ω,X} ⊧ t̂ ∼_{ρ} t.

Since Ψ′ is of type 0 → (σ → 0) ∈ T this yields for Φ := λb^{0}, x^{σ}.Ψ̂′(b, x)

M^{ω,X} ⊧ ∀b^{0}, x^{σ}(Φ(b, x) =_{0} Ψ′(b, x)).

Hence

M^{ω,X} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}[∀u ≤ Φ(x) B_{∀}(x, y, z, u) → ∃v ≤ Φ(x) C_{∃}(x, y, z, v)].

One easily verifies that for types γ of degree 1, (0, X) or (1, X)

M_{γ} = S_{γ},

where S^{ω,X} is the full set theoretic type structure over IN, X. Thus

(∗) S^{ω,X} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}[∀u ≤ Φ(x) B_{∀}(x, y, z, u) → ∃v ≤ Φ(x) C_{∃}(x, y, z, v)],

where Φ is treated in S^{ω,X} as a new constant c together with the interpretation [c]_{S^{ω,X}} = [Φ]_{M^{ω,X}}. This finished the proof as [Φ]_{M^{ω,X}} defines a computable functional^{22} in S_{0→(σ→0)} which does not depend on (X, d, W). ⊣

Proof of theorem 3.29 (the proof of theorem 3.24 follows just by disregarding all issues involving C in the proof of theorem 3.29): We now sketch the changes one has to make in the proof of theorem 3.7 in order to deal with the situation in theorem 3.29. The main difference is that we no longer can treat s-maj_{X} as trivial as before since the norm is unbounded on X. Instead we define

x^{∗} s-maj_{X} x :≡ x^{∗}, x ∈ M_{X} ∧ ∥x^{∗}∥ ≥ ∥x∥.

22Note that Φ is a closed term of A^{ω}.

M^{ω,X,∥·∥,C} is then defined just as M^{ω,X} but based on this new definition of s-maj_{X}. Again we have a syntactic version of s-maj in L(A^{ω}[X, ∥ · ∥, C]) (which we denote by ‘s-maj’ too) based on x^{∗} s-maj_{X} x :≡ ∥x^{∗}∥_{X} ≥_{IR} ∥x∥_{X}. One easily verifies that lemma 4.6 also holds for this new type structure and the new definition of s-maj. In order to prove that M^{ω,X,∥·∥,C} is a model of A^{ω}[X, ∥ · ∥, C]+(BR) we show that for any closed term t of A^{ω}[X, ∥ · ∥, C]+(BR) one can construct a closed term t^{∗} such that

M^{ω,X,∥·∥,C} ⊧ t^{∗} s-maj t,

where the constants of A^{ω}[X, ∥ · ∥, C]+(BR) are interpreted in M^{ω,X,∥·∥,C} as follows: The constants of A^{ω}+(BR) (extended to T^{X}) are interpreted as in M^{ω,X} above. For the new constants we take (writing simply M for M^{ω,X,∥·∥,C}):

[b_{X}]_{M} := b ∈ IN for some bound b for C, i.e. b ≥ ∥x∥ for all x ∈ C, [0_{X}]_{M} := 0^{X}, where 0^{X} is the zero vector of the linear space X, [1_{X}]_{M} := a for some a ∈ X with ∥a∥ = 1,^{23} [c_{X}]_{M} := c for some c ∈ C, [+_{X}]_{M} := addition in X, [−_{X}]_{M} := inverse of x w.r.t. + in X, [·_{X}]_{M} := λα ∈ IN^{IN}, x ∈ X.r_{α} · x, where r_{α} is the unique real number represented by α and ‘·’ refers to the scalar multiplication of the IR-linear space X, [∥ · ∥_{X}]_{M} := λx ∈ X.(∥x∥)_{∘}, where (r)_{∘} for r ∈ IR_{+} is the construction from 2.9,

[χ_{C}]_{M} := λx ∈ X. \{ \begin{matrix}0^{0}, if x ∈ C \\ 1^{0}, if x ∉ C. \end{matrix}

In order to show that all these functionals are in M^{ω,X,∥·∥,C} we have to construct majorants. For the constants of A^{ω}+(BR) (extended to T^{X}) this is done as in [3], where we – in order to deal with the new types – again have to extend the functionals max_{ρ} (and (·)^{M}) to the new types so that

23Since X is assumed to be non-trivial there exists a v ∈ X with ∥v∥ > 0 and hence an a := \frac{v}{∥v∥} with ∥a∥ = 1.

∀x^{∗}, x, y^{∗}, y(x^{∗} s-maj_{ρ} x ∧ y^{∗} s-maj_{ρ}y → max_{ρ}(x^{∗}, y^{∗}) s-maj_{ρ} max_{ρ}(x, y), x, y).

This is achieved as before except that - due to the new and non-trivial definition of s-maj_{X} - we now take for the base type X a new max_{X}-functional:

max_{X}(x^{X}, y^{X}) := max_{IR}(∥x∥_{X}, ∥y∥_{X}) ·_{X} 1_{X}.

For complex types ρ → τ we still define

max_{ρ→τ}(x, y) := λv^{ρ}. max_{τ}(xv, yv).

The construction x^{M} for types 0 → ρ with ρ = ρ_{1} → (ρ_{2} → … (ρ_{k} → X) …) is then as before but with the new max_{X} . One easily verifies, that (M) (from the proof above) still holds for this new definition of x^{M}.

For the new constants b_{X}, 0_{X}, 1_{X}, c_{X}, +_{X}, −_{X}, ·_{X}, ∥ · ∥_{X}, χ_{C} we construct majorants defined by the following closed terms:

b_{X}^{∗} := b_{X}, 0_{X}^{∗} := 0_{X}, 1_{X}^{∗} := 1_{X}, c_{X}^{∗} := (b_{X})_{IR} ·_{X} 1_{X},
+_{X}^{∗} := λx^{X}, y^{X}.(∥x∥_{X} +_{IR} ∥y∥_{X}) ·_{X} 1_{X},
−_{X}^{∗} := λx^{X}.x^{X},
·_{X}^{∗} := λα^{1}, x^{X}.(α(0) + 1)_{IR} ·_{X} x^{X},
∥ · ∥_{X}^{∗} := ∥ · ∥_{X},
χ_{C}^{∗} := λx^{X}.1^{0}.

One easily shows that for all constants k^{ρ}

M^{ω,X,∥·∥,C} ⊧ k^{∗} s-maj_{ρ} k :

For b_{X}, 0_{X}, 1_{X} and χ_{C} this is trivial. c_{X}^{∗} s-maj_{X}c_{X} follows from the axiom that ∥x∥_{X} ≤_{IR} (b_{X})_{IR} for all x ∈ C. For +_{X}^{∗}, −_{X}^{∗} one uses the basic axioms for +_{X}, −_{X} and ·_{X}. ·_{X}^{∗} s-maj ·_{X} : Let α^{∗} s-maj_{1} α, x^{∗} s-maj_{X} x. Then α^{∗}(0) ≥_{0} α(0) and thus (α^{∗}(0) + 1)_{IR} ≥_{IR} (α(0) + 1)_{IR} ≥_{IR} |α|_{IR} by the comment after lemma 2.5. Hence

∥(α^{∗}(0) + 1)_{IR} ·_{X} x^{∗}∥_{X} =_{IR} (α^{∗}(0) + 1)_{IR} ·_{IR} ∥x^{∗}∥_{X} ≥_{IR} \overbrace{(α(0) + 1)_{IR} ·_{IR} ∥x∥_{X}}^{=_{IR}∥(α(0)+1)_{IR}·_{X}x∥_{X}}

≥_{IR} |α|_{IR} ·_{IR} ∥x∥_{X} =_{IR} ∥α ·_{X} x∥_{X}.

∥ · ∥_{X} s-maj ∥ · ∥_{X} : Let x^{∗} s-maj_{X} x. Then ∥x^{∗}∥ ≥ ∥x∥ and hence by lemma 2.10.2^{24}

[∥x^{∗}∥_{X}]_{M} ≥_{1} [∥x∥_{X}]_{M}.

Thus, by lemma 2.10.4,

[∥x^{∗}∥_{X}]_{M} s-maj_{1} [∥x∥_{X}]_{M},

i.e.

M ⊧ ∥ · ∥_{X} s-maj ∥ · ∥_{X}.

Hence replacing in a closed term t of A^{ω}[X, ∥ · ∥, C]+(BR) every constant by its majorizing term we get a closed term t^{∗} such that

M^{ω,X,∥·∥,C} ⊧ t^{∗} s-maj_{ρ} t.

Note that t^{∗} does not contain +_{X}, −_{X}, c_{X} and χ_{C}. For types σ of degree 1 we define x^{m} as before. (+) extends to all types ρ ∈ T^{X}. Hence as before we get also for the more general types ρ permitted in theorem 3.29

M^{ω,X,∥·∥,C]} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)(s^{∗}(x^{m}) s-maj y),

where s^{∗} is a closed term such that s^{∗} s-maj s. The rest of the proof of theorem 3.29 is now similar to the proof of theorem 3.7 observing the following points: we can take c_{X}^{∗} as universal majorant for all C-elements. Hence functionals having a type of degree (1, X, C) are majorized by the constantc_{X}^{∗}-functional of the same type. Again it is crucial for the functional interpretation argument that all the axioms (0)-(8) and (11)-(13) are purely universal. By remark 3.27 permitting quantification over variables z^{τ} of degree (1, X, C) – instead of (1, X)

– in theorem 3.29 only causes an additional implicative premise which is an ∀-formula and, therefore, doesn’t change the logical form of the statements treated in theorem 3.29 compared to those treated in theorem 3.7. The argument used in theorem 3.7 to infer validity of the conclusion in S^{ω,X} from validity in M^{ω,X} now requires somewhat more care: we still have M_{ρ} = S_{ρ} for ρ of degree 1 or of degree (0, X), where for the latter we now need the extended construction x ↦ x^{m} to infer that x ∈ S_{ρ} implies x ∈ M_{ρ} for ρ of degree (0, X) (and also for degree 1). For types ρ of degree (1, X) we only get the inclusion

24Here we write again M for M^{ω,X,∥·∥,C}.

M_{ρ} ⊆ S_{ρ}

which, however is enough for our purpose: the only quantifiers over functionals of degree (1, X) in our conclusion are the ones hidden in the definition of ∀/∃-formulas and in ∀y ≤_{ρ} sx. Since ∀-formulas occur negatively only and ∃-formulas positively only, we just need the inclusion stated above. For y ≤ s(x), we can infer from y ∈ S_{ρ} and the fact that s^{∗}(x^{m}) s-maj y that y ∈ M_{ρ}. This finishes the proof of the fact that we can extract a functional Φ(b, x) which uniformly in x and an upper bound b for C produces the ‘n’ in the theorem (the independence from C is due to the fact that t^{∗} does not contain χ_{C} and c_{X}. Hence we don’t need here the construction t ↦ t̂ from the end of the proof of theorem 3.7). However, Φ is not computable and depends on (X, ∥·∥) as it involves 0_{X}, 1_{X}, ∥·∥_{X}, ·_{X} and (·)_{∘}. We now show (using that the type σ of x is of degree 1) how to modify Φ into a computable functional which does not depend on (X, ∥ · ∥) at all. To achieve all this we need a more involved version of the argument used at the end of the proof of theorem 3.7 in order to eliminate ·_{X}, ∥ · ∥_{X} and the ineffective construction (·)_{∘} from Φ: For ρ ∈ T^{X} we define ρ̂ ∈ T (different from ρ̂ used in the proof of theorem 3.7) inductively as follows:

ˆ0 := 0, X̂:= 1, ρ̂ → τ := ρ̂ → τ̂.

We define a new relation x_{ρ} ∼_{ρ} y^{ρ} between functionals x_{ρ}, y^{ρ} of types ρ̂, ρ by induction on ρ ∈ T^{X}, where we use (α^{1})_{∘} to denote (|r_{α}|)_{∘} with r_{α} being the unique real number represented by α:^{25}

\{ \begin{matrix}x^{0} ∼_{0} y^{0} :≡ x =_{0} y, x^{1} ∼_{X} y^{X} :≡ x =_{1} ∥y^{X}∥_{X}, \\ x^{_{ρ}→_{τ}} ∼_{ρ→τ} y^{ρ→τ} :≡ ∀u_{ρ}, v^{ρ}(u ∼_{ρ} v → xu ∼_{τ} yv). \end{matrix}

25I.e., (α^{1})_{∘}(n) = j(2k_{0}, 2^{n+1} − 1), where k_{0} := max k [⟨\frac{k}{2^{n+1}} ⟩ ≤_{IR} |α|_{IR}] .

One easily shows that the following holds in M^{ω,X,∥·∥,C} :

1) 0^{0} ∼_{0} 0^{0}, S^{1} ∼_{1} S^{1},

2) (0_{IR})_{∘} ∼_{X} 0_{X}, (1_{IR})_{∘} ∼_{X} 1_{X},

3) Π_{_{ρ},_{τ}} ∼ Π_{ρ,τ}, Σ_{_{δ},_{ρ},_{τ}} ∼ Σ_{δ,ρ,τ}, \underline{R}\underline{_{ρ}} ∼ \underline{R}\underline{ρ}, ˜ \underline{B}^{\underline{_{ρ}},\underline{_{τ}}} ∼ \underline{B}^{\underline{ρ},\underline{τ}},^{26}

4) λx^{1}.x ∼_{X→1} ∥ · ∥_{X}^{X→1},

5) λα^{1}, x^{1}.(|α|_{IR} ·_{IR} x)_{∘} ∼_{1→X→X} ·_{X}^{1→X→X}.

Let Φ̂^{0→σ→0} be the term which results from Φ^{0→σ→0} by replacing all occurrences of 0_{X}, 1_{X}, Π_{ρ,τ}, Σ_{δ,ρ,τ}, \underline{R}\underline{ρ}, \underline{B}^{\underline{ρ},\underline{τ}}, ∥ · ∥_{X}, ·_{X} in t by

(0_{IR})_{∘}, (1_{IR})_{∘}, Π_{_{ρ},_{τ}}, Σ_{_{δ},_{ρ},_{τ}}, \underline{R}\underline{_{ρ}}, \underline{B}^{\underline{_{ρ}},\underline{_{τ}}}, λx^{1}.x, λα^{1}, x^{1}.(|α|_{IR} ·_{IR} x)_{∘}.

Then

M^{ω,X,∥·∥,C} ⊧ Φ̂ ∼_{0→σ→0} Φ

and hence (since σ is assumed to be of degree 1)

M^{ω,X,∥·∥,C} ⊧ Φ̂ =_{0→σ→0} Φ.

In contrast to Φ, the functional Φ̂ no longer depends on the normed space (X, ∥ · ∥). However, it involves the noncomputable functional λx^{1}.(x)_{∘}. We now show that we can construct a functional Φ^{∗} which provides an upper bound for Φ̂ (and therefore satisfies the theorem as well) and does not involve λx^{1}.(x)_{∘}: One can easily construct primitive recursive strong majorants of (0_{IR})_{∘}, (1_{IR})_{∘} and λα^{1}, x^{1}.(|α|_{IR} ·_{IR} x)_{∘} using a primitive recursive majorant for λx^{1}.(x)_{∘} (e.g. λx^{1}, n^{0}.j((x(0) + 1) ·_{0} 2^{n+2}, 2^{n+1} − 1). All the other constants 0, S, Π, Σ, \underline{R}, \underline{B} occurring in Φ̂ have bar recursive majorants as discussed in connection with the proof of theorem 3.7. Hence we can construct a majorant Φ^{∗} of Φ̂ which does not involve (·)_{∘} any longer and satisfies

M^{ω,X,∥·∥,C} ⊧ ∀b^{0}, x^{σ}(Φ^{∗}(b, x^{m}) ≥_{0} Φ̂(b, x)).

26Here ˜ \underline{B}^{\underline{_{ρ}},\underline{_{τ}}} is as \underline{B}^{\underline{_{ρ}},\underline{_{τ}}} except that for types ρ_{i} of the form σ_{1} → … → σ_{k} → X we use in the definition of \overline{y, n} and \overline{y, n} ∗ D for ρ̂_{i} instead of 0^{ρ_{i}} the functional λv_{1}^{σ_{1}}, …, v_{k}^{σ_{k}}.((0)_{IR})_{∘}. One easily shows that B̃_{i}^{\underline{_{ρ}},\underline{_{τ}}} ∈ M^{ω} as well (with a bar recursive majorant). The reason for our modification is that we need that y_{1} ∼_{0→ρ_{i}} y_{2} implies ∀n(y_{1}n ∼_{ρ_{i}} y_{2}n) which relies on (0_{IR})_{∘} ∼_{X} 0_{X} whereas ¬(0^{1} ∼_{X} 0_{X}).

For uniformly convex spaces we recall that (9) is logically equivalent to a purely universal axiom and interpret η in M by a modulus of uniform continuity function. Finally, we observe that trivially η^{M} s-maj_{1} η so that we can take η^{∗} := η^{M}, and – for inner product spaces – we only have to note that (10) is purely universal. ⊣

Remark 4.9 In [9] a Gödel functional interpretation of an extension of A^{ω} by analytical comprehension for objects of arbitrary types is given via the intermediate step of a game quantifier translation ([8]). The interpretation is carried out in an extension of the bar recursive functionals to infinite types. In [23] we have extended the type structure of all strongly majorizable functionals to these infinite types and shown that this yields a model for Friedrich’s calculus. In view of this it seems likely that the results of this paper can be extended to this even stronger setting.

Acknowledgment: I am grateful to Philipp Gerhardy, Laurenţiu Leuştean and Paulo Oliva for their comments on an earlier version of this paper which helped to improve the presentation.

References

[1] Beeson, M., Foundations of constructive mathematics. Springer Verlag, Berlin, Heidelberg, New York (1985).

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

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

[4] Borwein, J., Reich, S., Shafrir, I., Krasnoselski-Mann iterations in normed spaces. Canad. Math. Bull. 35, pp. 21-28 (1992).

[5] Browder, F.E., Petryshyn, W.V., The solution by iteration of nonlinear functional equations in Banach spaces. Bull. Amer. Math. Soc. 72, pp. 571-575 (1966).

[6] Delzell, C., Kreisel’s unwinding of Artin’s proof-Part I. In: Odifreddi, P., Kreiseliana, 113-246, A K Peters, Wellesley, MA (1996).

[7] Edelstein, M., O’Brien, R.C., Nonexpansive mappings, asymptotic regularity and successive approximations. J. London Math. Soc. 17, pp. 547-554 (1978).

[8] Friedrich, W., Spielquantorinterpretation unstetiger Funktionale der höheren Analysis. Arch. math. Logik 24, pp. 73-99 (1984).

[9] Friedrich, W., Gödelsche Funktionalinterpretation für eine Erweiterung der klassischen Analysis. Zeitschr. f. math. Logik und Grundl. d. Math. 31, pp. 3-29 (1985).

[10] Goebel, K., Kirk, W.A., Iteration processes for nonexpansive mappings. In: Singh, S.P., Thomeier, S., Watson, B., eds., Topological Methods in Nonlinear Functional Analysis. Contemporary Mathematics 21, AMS, pp. 115-123 (1983).

[11] Goebel, K., Reich, S., Uniform convexity, hyperbolic geometry, and nonexpansive mappings. Monographs and Textbooks in Pure and Applied Mathematics,

83. Marcel Dekker, Inc., New York, ix+170 pp. (1984).

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

[13] Gödel, K., Collected Work, Vol.2, S. Feferman et al. eds. Oxford University Press, New York (1990).

[14] Groetsch, C.W., A note on segmenting Mann iterates. J. of Math. Anal. Appl. 40, pp. 369-372 (1972).

[15] Henson, C.W., Iovino, J., Ultraproducts in analysis. In: Analysis and Logic. London Mathematical Society LNS 262, pp. 1-112. Cambridge University Press (2002).

[16] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 454-461. Springer LNM 344 (1973).

[17] Howard, W.A., Kreisel, G., Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symbolic Logic 31, pp. 325-358 (1966).

[18] Ishikawa, S., Fixed points and iterations of a nonexpansive mapping in a Banach space. Proc. Amer. Math. Soc. 59, pp. 65-71 (1976).

[19] Itoh, S., Some fixed point theorems in metric spaces. Fund. Math. 102, pp. 109-117 (1979).

[20] Kirk, W.A., Krasnosel’skii iteration process in hyperbolic spaces, Numer. Funct. Anal. and Optimiz. 4, pp. 371-381 (1982).

[21] Kirk, W.A., Nonexpansive mappings and asymptotic regularity, Nonlinear Analysis, 40, pp. 323-332 (2000).

[22] Kirk, W.A., Martinez-Yanez, C., Approximate fixed points for nonexpansive mappings in uniformly convex spaces. Annales Polonici Mathematici 51, pp. 189-193 (1990).

[23] Kohlenbach, U., Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Beweisen. PhD Thesis, Frankfurt am Main, xxii+278pp. (1990).

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

[25] Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin’s proof for Chebycheff approximation. Ann. Pure Appl. Logic 64, pp. 27–94 (1993).

[26] Kohlenbach, U., New effective moduli of uniqueness and uniform a–priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numer. Funct. Anal. and Optimiz. 14, pp. 581–606 (1993).

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

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

[29] Kohlenbach, U., Arithmetizing proofs in analysis. In: Larrazabal, J.M., Lascar, D., Mints, G. (eds.), Logic Colloquium ’96, Springer Lecture Notes in Logic 12, pp. 115-158 (1998)

[30] Kohlenbach, U., On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In: Proceedings of the Fourth Workshop on Computability and Complexity in Analysis, J. Blanck, V. Brattka, P. Hertling (eds.), Springer LNCS 2064, pp. 119-145 (2001).

[31] Kohlenbach, U., A quantitative version of a theorem due to Borwein-Reich-Shafrir. Numer. Funct. Anal. and Optimiz. 22, pp. 641-656 (2001).

[32] Kohlenbach, U., Uniform asymptotic regularity for Mann iterates. J. Math. Anal. Appl. 279, pp. 531-544 (2003).

[33] Kohlenbach, U., Leuştean, L., Mann iterates of directionally nonexpansive mappings in hyperbolic spaces. Abstract and Applied Analysis, vol. 2003, issue 8, pp. 449-477 (2003).

[34] Kohlenbach, U., Oliva, P., Effective bounds on strong unicity in L_{1}- approximation. Ann. Pure Appl. Logic 121, pp. 1-38 (2003).

[35] Kohlenbach, U., Oliva, P., Proof mining: a systematic way of analysing proofs in analysis. To appear in: Proc. Steklov Inst. Math.

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

[37] Kreisel, G., Finiteness theorems in arithmetic: an application of Herbrand’s theorem for Σ_{2}-formulas. Proc. of the Herbrand symposium (Marseille, 1981), North-Holland (Amsterdam), pp. 39-55 (1982).

[38] Kreisel, G., Proof Theory and Synthesis of Programs: Potentials and Limitations. Eurocal ’85 (Linz 1985), Springer LNCS 203, pp. 136-150 (1986).

[39] Kreisel, G., Macintyre, A., Constructive logic versus algebraization I. Proc. L.E.J. Brouwer Centenary Symposium (Noordwijkerhout 1981), North-Holland (Amsterdam), pp. 217-260 (1982).

[40] Luckhardt, H., Extensional Gödel Functional Interpretation. Springer Lecture Notes in Mathematics 306 (1973).

[41] Luckhardt, H., Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symbolic Logic 54, pp. 234-263 (1989).

[42] Luckhardt, H., Bounds extracted by Kreisel from ineffective proofs. In: Odifreddi, P., Kreiseliana, 289–300, A K Peters, Wellesley, MA (1996).

[43] Machado, H.V., A characterization of convex subsets of normed spaces. Kodai Math. Sem. Rep. 25, pp. 307-320 (1973).

[44] Mann, W.R., Mean value methods in iteration. Proc. Amer. Math. Soc. 4, pp. 506-510 (1953).

[45] Reich, S., Shafrir, I., Nonexpansive iterations in hyperbolic spaces. Nonlinear Analysis, Theory, Methods and Applications 15, pp. 537-558 (1990).

[46] Reich, S., Zaslavski, A.J., Generic aspects of metric fixed point theory In: W. A. Kirk, B. Sims, editors, Handbook of Metric Fixed Point Theory, Kluwer Academic Publishers, pp. 557-576 (2001).

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

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

[49] Takahashi, W., A convexity in metric space and nonexpansive mappings, I. Kodai Math. Sem. Rep. 22, pp. 142-149 (1970).

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

[51] Weidmann, J., Linear operators in Hilbert spaces. Springer Graduate Texts in Mathematics 68, xii+402pp. (1980).

Recent BRICS Report Series Publications

RS-03-21 Ulrich Kohlenbach. Some Logical Metatheorems with Applications in Functional Analysis. May 2003. 55 pp.

RS-03-20 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. May 2003. 16 pp. Final version to appear in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003. This report supersedes the earlier BRICS report RS-03-11.

RS-03-19 Christian Kirkegaard, Anders Møller, and Michael I. Schwartzbach. Static Analysis of XML Transformations in Java. May 2003. 29 pp.

RS-03-18 Bartek Klin and Pawe� Sobociński. Syntactic Formats for Free: An Abstract Approach to Process Equivalence. April 2003. 41 pp.

RS-03-17 Luca Aceto, Jens Alsted Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. The Complexity of Checking Consistency of Pedigree Information and Related Problems. March 2003. 31 pp. This paper supersedes BRICS Report RS-02-42.

RS-03-16 Ivan B. Damgård and Mads J. Jurik. A Length-Flexible Threshold Cryptosystem with Applications. March 2003. 19 pp.

RS-03-15 Anna Ingólfsdóttir. A Semantic Theory for Value–Passing Processes Based on the Late Approach. March 2003. 48 pp.

RS-03-14 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. March 2003. 36 pp.

RS-03-13 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Evaluators and Abstract Machines. March 2003. 28 pp.

RS-03-12 Mircea-Dan Hernest and Ulrich Kohlenbach. A Complexity Analysis of Functional Interpretations. February 2003. 70 pp.

RS-03-11 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. February 2003. 14 pp. This report is superseded by the later report BRICS RS-03-20.