BRICS

Basic Research in Computer Science

Strongly Uniform Bounds from Semi-Constructive Proofs

Philipp Gerhardy Ulrich Kohlenbach BRICS Report Series RS-04-31 ISSN 0909-0878 December 2004 BRICS RS-04-31 Gerhardy & Kohlenbach: Strongly Uniform Bounds from Semi-Constructive Proofs Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Philipp Gerhardy & Ulrich Kohlenbach.

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

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

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

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

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

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

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

This document in subdirectory RS/04/31/

Strongly uniform bounds from semi-constructive proofs

Philipp Gerhardy  Ulrich Kohlenbach^{∗}

December, 2004

Abstract

In [12], the second author obtained metatheorems for the extraction of effective (uniform) bounds from classical, prima facie nonconstructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT(0) and normed linear spaces and guarantee the independence of the bounds from parameters raging over metrically bounded (not necessarily compact!) spaces. The use of classical logic imposes some severe restrictions on the formulas and proofs for which the extraction can be carried out. In this paper we consider similar metatheorems for semi-intuitionistic proofs, i.e. proofs in an intuitionistic setting enriched with certain non-constructive principles. Contrary to the classical case, there are practically no restrictions on the logical complexity of theorems for which bounds can be extracted. Again, our metatheorems guarantee very general uniformities, even in cases where the existence of uniform bounds is not obtainable by (ineffective) straightforward functional analytic means. Already in the purely intuitionistic case, where the existence of effective bounds is implicit, the metatheorems allow one to derive uniformities that may not be obvious at all from a given constructive proofs. Finally, we illustrate our main metatheorem by an example from metric fixed point theory.

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

1 Introduction

Proof mining is the application of logical, or more precisely, proof theoretic methods to the analysis of formal systems and proofs with the aim of extracting additional information from (mathematical) proofs. E.g. one might want to extract from a proof that a certain iteration sequence converges an effective, computable modulus of convergence and to establish the uniformity of such a modulus or even to state general a-priori conditions for the independence of an extracted modulus from certain parameters. In the classical case, i.e. formalizations of mathematics based on classical logic, the goal of proof mining is to extract realizers and bounds - we will focus on the extraction of bounds - from prima facie ineffective, nonconstructive proofs. The technique used to prove the existence of effective bounds and, if needed, to carry out the extraction is based on an interpretation of classical proofs via some negative translation and (a suitable form of) Gödel’s functional interpretation, further combined with majorization(see [8, 12]). Whereas previously only theorems involving constructively representable Polish spaces could be treated and uniformity in parameters was guaranteed only for the case of compact spaces ([8, 9]) recent results ([12]) due to the second author allow one to treat classes of arbitrary metric, hyperbolic, CAT(0) and normed linear spaces X. Moreover, under very general conditions, uniformity in parameters ranging over metrically bounded spaces can be inferred a-priorily even in cases where this could not have been obtained by usual ineffective functional analytic methods. However, both the raw material, classical proofs, and the techniques employed for the interpretation impose certain restrictions: One can use at most weak extensionality in the proofs to be analyzed, as full extensionality can be shown to be too strong under functional interpretation. In the context of [12] this is a severe restriction as it implies that not every object f^{X→X} of type X → X can be viewed as a function f : X → X.^{1} Also, as many classically true theorems cannot be given computational meaning (this includes already Π_{3}^{0}-sentences), the extraction of realizers and bounds can be carried out at most for (classical) proofs of sentences of the form ∀∃A_{qf} where A_{qf} is quantifier-free with some further restrictions on the types of the quantified variables. In this paper, we consider proof mining in the semi-intuitionistic case: intuitionistic analysis enriched with certain non-constructive principles. In the purely intuitionistic setting bounds and realizers are implicitly given. Nevertheless, even in the intuitionistic setting our results prove non-trivial consequences: as in the classical setting of [12] we can now guarantee very strong uniformity results (independence from parameters ranging over metrically bounded spaces). Even in the presence of various highly ineffective principles (such as comprehension in all types for arbitrary negated or ∃- free formulas and many others), most of the restrictions needed in the fully classical case disappear in our semi-constructive setting: we can now use full extensionality and extract realizers and bounds from (semi-intuitionistic) proofs of arbitrary formulas, with comparatively modest restrictions on the types of the quantified variables. The technique employed to establish these results for such semi-intuitionistic systems is a monotone variant of Kreisel’s modified realizability interpretation, so-called monotone modified realizability. The metatheorem for the semi-intuitionistic case we present in this paper is to some extent based on results in [10], and the extensions presented here can be considered as the counterpart to the extensions of [8] presented in [12] for the classical case. As stated above, both in the classical and the semi-intuitionistic case the metatheorems allow one to derive new, strong uniformity results, by giving general, easy to check conditions under which an extracted bound will be guaranteed to be independent from certain parameters - all of this without actually having to carry out the extraction. For the independence of (effective) bounds from parameters ranging over compact spaces such results are well known and have been treated in [9, 10]. For non-compact bounded metric or hyperbolic spaces there are no general mathematical reasons why such uniformities should hold, and in metric fixed point theory similar (ineffective) uniformity results have hitherto only been obtained in special cases by non-trivial functional analytic techniques (see [12, 14] for discussions of these points). Already in the context of fully intuitionistic proofs one can derive new uniformities that may not be obvious from a given constructive proof or a bound implicit in the proof. We illustrate the various aspects of the metatheorems by a very simple example from metric fixed point theory: First we state the original ineffective version of Edelstein’s fixed point theorem[3]. The main part of Edelstein’s fixed point theorem is of a too complicated logical form (namely Π_{3}^{0}) to directly allow the extraction via the classical metatheorem. Therefore in [15] an effective uniform bound for Edelstein’s fixed point theorem is extracted by splitting up Edelstein’s proof into three lemmas, each simple enough to allow the extraction of a bound. Next we present a variant of Edelstein’s fixed point theorem due to Rakotch[20]. Rakotch’s proof is fully constructive, which permits us to extract a uniform bound as guaranteed by the semiintuitionistic metatheorem. Finally, we compare the results with a treatment of Edelstein’s fixed point theorem in the setting of Bishop-style constructive mathematics by Bridges, Julian, Richman and Mines[2]. Both the classical and the intuitionistic metatheorem a-priorily guarantee uniformities not stated in the constructive proof by Bridges et. al. The bound extracted from Rakotch’s constructivized proof, while superior to the bound extracted in [15], is identical to the bound implicit in [2].

1As a consequence of this, the applications given in [12] mainly concern classes of functions, like nonexpansive functions, for which the extensionality can be deduced directly.

2 Formal systems

We now describe the classical and intuitionistic formal systems in which the extraction of bounds is carried out. For technical details see [12] and also [18].

Let A^{ω}(:= WE-PA^{ω} + DC) be the system of so-called weakly extensional classical analysis, based upon a finite type extension PA^{ω} of first order Peano arithmetic PA and the axiom schema DC of dependent choice in all types. Let A_{i}^{ω}(:= E-HA^{ω}+AC) denote the intuitionistic extensional counterpart of A^{ω}, i.e. fully extensional intuitionistic analysis with the full axiom of choice.

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

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

Objects of type 0 denote natural numbers, objects of type ρ → τ are operations mapping objects of type ρ to objects of type τ. 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:^{2}

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:

2Here we write s(x_{1}, …, x_{k}) for (… (sx_{1}) … x_{k}).

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

Ideally, we would like to have an axiom stating the extensionality for all functionals, but in the classical system A^{ω} full extensionality would be too strong for the metatheorems we are aiming at and their applications in functional analysis to hold. Instead in A^{ω} we include a weaker quantifier-free extensionality rule due to [24]:

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 one 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 [25], [5]). In the intuitionistic system A_{i}^{ω} we include the much stronger extensionality axiom:

E_{ρ} : ∀z^{ρ}, x^{ρ_{1}}, y^{ρ_{1}}, …, x^{ρ_{k}}, y^{ρ_{k}}(⋀_{i=1}^{k}(x_{i} =_{ρ_{i}} y_{i}) → z\underline{x} =_{0} z\underline{y}),

for all types ρ. The systems A^{ω} and A_{i}^{ω} are defined on top of many-sorted classical, resp. intuitionistic, logic with constants O^{0} (zero), S^{1} (successor), Π_{ρ,τ}^{ρ→τ→ρ} (projectors), Σ_{δ,ρ,τ} (combinators of type (δ → ρ → τ) → (δ → ρ) → δ → τ) and constants \underline{R}\underline{ρ} for simultaneous primitive recursion in all types.^{3} In addition to the defining equations for those constants, A^{ω} and A_{i}^{ω} contain as non-logical axioms:

1. Reflexivity, symmetry and transitivity axioms for =_{0},

2. the 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, 3. in A^{ω}:

3It is well-known that simultaneous primitive recursion in all finite types can be reduced to ordinary primitive recursion in all finite types over A_{i}^{ω}. However, in the extensions A_{(i)}^{ω}[X, …] to be discussed below this is rather complicated so that we prefer to take simultaneous recursion as a primitive concept as in [12].

• the quantifier-free extensionality rule QF-ER

• the 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,

• the axiom schema of dependent choice DC:= {DC^{ρ} : ρ ∈ T}:

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.

4. in A_{i}^{ω}:

• the axiom schema of extensionality E = {E_{ρ} : ρ ∈ T} for all types ρ

• the axiom schema of full choice AC:= {AC^{ρ,τ} : ρ, τ ∈ T}:

AC^{ρ,τ} : ∀x^{ρ}∃y^{τ}A(x, y) → ∃Y^{ρ→τ}∀xA(x, Y x).

where A is an arbitrary formula.

We next sketch extensions of A^{ω} and A_{i}^{ω} with an (non-empty) abstract metric space (X, d), resp. hyperbolic space or CAT(0) space (X, d, W) where for the somewhat involved details we refer to[12]:

The theories A^{ω}[X, d], A^{ω}[X, d, W] and A^{ω}[X, d, W, CAT(0)] result from extending A^{ω} (and also IA, R, QF-AC, DC, QF-ER, …) to the set T^{X} of all finite types over the two ground types 0 and X, and by adding constants d_{X} and – in the case of A^{ω}[X, d, W] and A^{ω}[X, d, W, CAT(0)] – W_{X} representing d, W and suitable (purely universal) axioms to A^{ω}. Moreover, we add a constant b_{X} (of type 0) for an upper bound of d_{X}. Equality is defined extensionally over the base types 0 and X, where x^{X} =_{X} y^{X} :≡ (d_{X}(x, y) =_{IR} 0_{IR}). Analogously, the theories A_{i}^{ω}[X, d], A_{i}^{ω}[X, d, W] and A_{i}^{ω}[X, d, W, CAT(0)] result from an extension of A_{i}^{ω}.

Similarly, one defines the extensions A^{ω}[X, ∥ · ∥, C] and A_{i}^{ω}[X, ∥ · ∥, C] of A^{ω} and A_{i}^{ω} with an abstract (non-trivial) normed linear space (X, ∥ · ∥) and a (non-empty) bounded convex subset C ⊂ X (again we refer to [12] for details):

The theories A^{ω}[X, ∥ · ∥, C] and A_{i}^{ω}[X, ∥ · ∥, C] result from extending A^{ω} and A_{i}^{ω} to the set T^{X} of all finite types over the two ground types 0 and X, and by adding constants for the vector space operations and ∥ · ∥ as well as for the characteristic function of C and an upper bound b_{X} on the norm of the elements of C with appropriate (purely universal) axioms to A^{ω} expressing the vector space and norm axioms as well as the boundedness and convexity of C. As before, equality is defined extensionally over the base types 0 and X.

Definition 2.2. Between functionals x^{ρ}, y^{ρ} of type ρ = τ_{1} → … → τ_{k} → 0 with τ_{i} ∈ T^{X} we define a relation ≤_{ρ} as follows:

x ≤_{ρ} y :≡ ∀\underline{z}\underline{τ}(x(\underline{z}) ≤_{0} y(\underline{z})

For A_{(i)}^{ω}[X, ∥ · ∥, C] we extend ≤_{ρ} to arbitrary types ρ ∈ T^{X} by defining for ρ = τ_{1} → … → τ_{k} → X:

x ≤_{ρ} y :≡ ∀\underline{z}\underline{τ}(∥x(\underline{z})∥_{X} ≤_{IR} ∥y(\underline{z})∥_{X}).

Definition 2.3. 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_{ρ}.

We say that a sentence of L(A^{ω}[X, d]), holds in a bounded metric space (X, d) if it holds in the model^{4} of A^{ω}[X, d] 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, and the constants of (X, d) interpreted by elements of the suitable universes as specified in [12]. Similarly for L(A^{ω}[X, d, W]), L(A^{ω}[X, d, W, CAT(0)]) and L(A^{ω}[X, ∥·∥, C]), and for the languages formed over the corresponding intuitionistic systems.

4Strictly speaking, we would have to use the plural here as the interpretation of constant b_{X} is not uniquely determined. For details see [12].

In the following (for ρ ∈ T) ‘∀x^{C} A(x)’, ‘∀f^{ρ→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^{ρ→X}(∀y^{ρ}(χ_{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) and (X, C) defined below.

Definition 2.4. We say that a type ρ ∈ T^{X} has degree

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

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

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

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

• (·, 0) if ρ = τ_{1} → … → τ_{k} → 0 (including ρ = 0) for arbitrary types τ_{i},

• (·, X) if ρ = τ_{1} → … → τ_{k} → X (including ρ = X) for arbitrary types τ_{i},

• (X, C) if ρ = τ_{1} → … → τ_{k} → C (including ρ = C) where τ_{i} ∈ T or τ_{i} = X or τ_{i} = C.

3 Extracting bounds from classical proofs

In this section we briefly restate material from [12].

Definition 3.1. 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).

For metric, hyperbolic and CAT(0) spaces we have the following metatheorem:

Theorem 3.2 ([12]). 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}) (resp. 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.

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)’.

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

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

The proof in [12] is based on an extension of Spector’s[24] extension of Gödel’s functional interpretation to classical analysis A^{ω} by bar recursive functionals (i.e. recursion over well-founded trees) to A^{ω}[X, d], resp. A^{ω}[X, d, W] and A^{ω}[X, d, W, CAT(0)], and a subsequent interpretation of these functionals in an extension M^{ω,X} of the Howard-Bezem[5, 1] strongly majorizable functionals M^{ω} to T^{X}. These extensions rest on the following observations:

1. As is the case with A^{ω}, the prime formulas of A^{ω}[X, d] are of the form s =_{0} t and hence decidable. Thus the soundness of negative translation and subsequent functional interpretation of the logical axioms and rules and the defining equations for combinators Σ, Π and the recursor R, the rule QF-ER and the axiom schema QF-AC extend to the new set of types T^{X} without any changes. Likewise the interpretation of the axiom schema of induction and the axiom schema of dependent choice extends to T^{X} using constants \underline{R}\underline{ρ} for simultaneous primitive recursion and \underline{B}^{\underline{ρ},\underline{τ}} for simultaneous bar recursion in all types \underline{ρ}, \underline{τ} ∈ T^{X}.

2. The functional interpretation of the negative translation of the new axioms of A_{(i)}^{ω}[X, d], A_{(i)}^{ω}[X, d, W] and A_{(i)}^{ω}[X, d, W, CAT(0)] are equivalent to themselves as they are purely universal and don’t contain ∨.

3. Bezem’s[1] type structure of hereditarily strongly majorizable functionals M^{ω} extends easily to all types of T^{X}, taking x^{∗} maj_{X} x always true. The realizer Ψ ∈ M^{ω,X} for a bound on u^{0}, v^{0} extracted by negative translation and functional interpretation depends on X via an interpretation of the constants of X. Using majorization we show that we can extract a bound which only depends on X via an interpretation of some integer bound b on the metric d.

4. Since for the restricted types γ of degree 1, (0, X) or (1, X) occurring

in

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

M_{γ} = S_{γ}, this bound holds in any b-bounded space (X, d), resp. (X, d, W) and (X, d, W, CAT(0)).

For a detailed proof, see [12].

Definition 3.3. 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. ([6]) 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)),

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

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

In [12], the following corollary of theorem 3.2 is derived which is specially tailored towards applications to metric fixed point theory:

Corollary 3.5 ([12]). 1. Let P (resp. K) be a A^{ω}-definable Polish space (resp. compact Polish space), given in so-called standard representation, 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^{0}B_{∀} → ∃v^{0}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’.

Note that in the corollary, the assumption F ix(f) ≠ ∅ has disappeared in the conclusion! For a discussion of this remarkable point see [12].

For normed linear spaces, the following metatheorem is proved in [12]:

Theorem 3.6 ([12]). Let σ be a type of degree 1, ρ of degree 1 or (1, X) and τ of degree (1, X, C). Let s^{σ→ρ} be a closed term of A^{ω}[X, ∥ · ∥, C] and B_{∀}(x^{σ}, y^{ρ}, z^{τ}, u^{0}) (resp. 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, ∥ · ∥, C], 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-trivial normed linear space (X, ∥ · ∥) and any non-empty b-bounded convex subset C. Instead of single variables and a single premise we may have tuples of variables and a finite conjunction of such premises.

Remark 3.7. In [12], there are also corresponding theorems proved for uniformly convex normed spaces (X, ∥ · ∥, η) with convexity modulus η (then the bound Φ(x, b, η) will additionally depend on the modulus η) and for inner product spaces.

The proof in [12] is based on the same fundamental ideas as the proof of Theorem 3.2, the main difference being that the majorization relation on objects of type X can no longer be treated as trivial as in the case of a bounded metric space. Instead one defines the majorization relation s-maj for elements of type X to be

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

Then one can prove, as before, the extractability of effective bounds, where the main difficulty is to define suitable majorants for the constants and constructions of A^{ω}[X, ∥ · ∥, C].

Discussion on extensionality: As mentioned above, one can only allow the weak extensionality rule instead of the full axiom of extensionality in the formal systems based on classical logic. In order to reverse the double negations introduced by the negative translation, it is strictly necessary that the interpretation we choose to interpret classical logic in particular interprets the Markov principle. However, together with the Markov Principle full extensionality would cause severe problems, as it allows us, when combined with functional interpretation, to obtain witnesses for potential universal quantifiers hidden in the extensionally defined equalities in the premise of implications, e.g. in the extensionality axiom itself. The extraction of witnesses combined with majorization, would thus transform an instance of the extensionality axiom into a statement about uniform continuity. An axiom stating the extensionality of a single function constant would allow us to prove its uniform continuity. E.g. the full extensionality axiom for type-X equality would even allow us to prove (in the context of A^{ω}[X, d]) the equicontinuity of all functions f^{X→X} which – of course – is not true in general (but does hold for the class of nonexpansive mappings f : X → X, whose full extensionality follows in A^{ω}[X, d]). A similar problem with extensionality arises from the representation of a convex subset C of a normed linear space via its characteristic function χ_{C}. Here we would like the characteristic function to respect the extensional equality, i.e.

x =_{X} y → χ_{C}(x) =_{0} χ_{C}(y).

In the presence of functional interpretation and majorization, this would not only yield that points x ∈ X close to C behave similar to points in C, it would also describe a modulus for how close to C you have to be to behave ‘sufficiently similar’. Unless the subset C is topologically very simple (e.g. a closed bounded ball), such statements will in general not be correct. Therefore, we must restrict the formal system to make unwanted or simply false conclusions, drawn from extensionality statements, impossible. In turn, when it is necessary to employ an extensional equality in a proof, we cannot simply assume extensionality: every statement of extensionality that is used in a proof must itself be explicitly proved with the use of QF-ER or follow from uniform continuity. For more details, see the discussion of extensionality in section 3 of [12].

4 Extracting bounds from semi-constructive proofs

The metatheorems from [12] which we briefly discussed in the previous section allow one to extract bounds from proofs in fairly strong systems, namely extensions of classical analysis with an abstract metric, hyperbolic, CAT(0) resp. normed linear space. However, the fact that the formal systems were based on classical logic imposes severe restrictions on the class of formulas for which extraction of bounds is possible. The first step in the extraction algorithm is to apply negative translation to the classical proof (of some formula F), i.e. to translate it into an essentially intutionistic proof of the negative translation F^{N} of F (which may, however, use the Markov principle to be discussed below). This restricts the extraction of bounds to ∀∃A-formulas for which the equivalence between the formula and its negative translation can be shown to hold under the Markov Principle, namely the class of formulas ∀∃A_{qf}, where A_{qf} is quantifier-free (or purely existential). In consequence, the interpretation must interpret the Markov Principle, as functional interpretation indeed does. In general, such an equivalence can be validated at most for ∀∃A_{qf}, as already the formula class Π_{3}^{0} yields counterexamples to the existence of effective bounds in the form of e.g. the halting problem. Secondly, the interpretation of the negative translation of the axiom of dependent choice by bar recursive functionals requires arguments which hold only in the model of hereditarily strongly majorizable functionals M^{ω,X} over the types IN and X but not in the full set-theoretic model S^{ω,X}. In consequence, for the extracted bounds to hold in S^{ω,X}, we must restrict the types of the quantified variables in the theorem to be proved to types of degree 1 or (1, X), as for those low types the proper inclusions between these two models hold. We will see now that the intuitionistic counterpart of A^{ω} and its extensions to metric, hyperbolic, CAT(0) and normed linear spaces do not suffer from such restrictions (even when strong ineffective principles are added):

In the classical case we used an extension of Gödel’s Dialectica interpretation combined with negative translation and majorization (monotone functional interpretation) to obtain the results. In the intuitionistic setting we derive these results from a monotone variant of Kreisel’s modified realizability interpretation (in short: mr-interpretation), the so-called monotone modified realizability interpretation. Kreisel’s mr-interpretation was introduced in [16, 17] and studied in great detail in [25, 26]. The monotone mr-interpretation was introduced in [10] and is studied in detail in [7]. This interpretation has the following nice properties:

1. As in the classical case, we can use the general metatheorem as a black box to prove (even qualitatively new) uniformity results without actually having to carry out the extraction.

2. Contrary to classical systems, we are no longer restricted to proofs of ∀∃A_{qf}-statements, but can allow ∀∃A-statements for arbitrary A. Furthermore, the additional restrictions on the quantifiers stated in Theorem 3.2 and Theorem 3.6 can be significantly relaxed.

3. We may add large classes of additional axioms Γ_{¬} which include highly ineffective principles such as full comprehension for arbitrary negated formulas (which is not even allowed in the classical context, where it would allow full comprehension for all formulas).

The Markov Principle in all finite types is the principle

M^{ω} : ¬¬∃\underline{x}A_{qf}(\underline{x}) → ∃\underline{x}A_{qf}(\underline{x}),

where A_{qf} is an arbitrary quantifier-free formula of A^{ω} and \underline{x} is a tuple of variables of arbitrary types (A_{qf} may contain further free variables).

As discussed above, in the classical case it is strictly necessary that the interpretation we choose interprets the Markov principle, and this imposes certain restrictions on the formal system. In the intuitionistic setting we can choose not to include the Markov Principle. As a consequence, when extending intuitionistic analysis with non-constructive principles we have an actual choice between two main directions in which to extend the formal system: with or without the Markov Principle M^{ω}: Extending the system with the Markov Principle would force us to both restrict extensionality to weak extensionality and to allow at most the independence of premise scheme for purely universal formulas. However, we could still – replacing the use of negative translation in the proofs of the main results in [12] by the reasoning used to prove theorem 3.18 in [10] (which is based on monotone functional interpretation rather than monotone modified realizability) – extract bounds for arbitrary formulas ∀∃A, instead of the restricted formula class ∀∃A_{qf}. We choose instead to extend our formal system in the direction without M^{ω}. Abandoning the Markov Principle allows us to add full extensionality and comprehension and independence of premise schemes for arbitrary negated formulas, as well as many other essentially non-constructive analytic or logical principles (see also [10]).

Let comprehension for negated formulas be the principle:

CA_{¬}^{ρ} : ∃Φ ≤_{ρ→0} λx^{ρ}.1^{0}∀y^{ρ}(Φ(y) =_{0} 0 ↔ ¬A(y)),

let the independence-of-premise principle for negated formulas be:

IP_{¬}^{ρ} : (¬A → ∃y^{ρ}B(y)) → ∃y^{ρ}(¬A → B(y)) (y ∉ FV(A)),

where in both cases A, B are arbitrary formulas. The union of these principles over all types ρ of the underlying language are denoted by CA_{¬} and IP_{¬} where – when working over the systems A_{i}^{ω}[X, …] – we allow arbitrary types ρ ∈ T^{X}.

Definition 4.1. A formula A ∈ A_{i}^{ω}, resp. A ∈ A_{i}^{ω}[…], is called ∃-free (or ‘negative’), if A is built up from prime formulas by means of ∧, →, ¬ and ∀ only, i.e. A contains neither ∃ nor ∨. We denote ∃-free formulas A by A_{ef}.

The principles CA_{ef} and IP_{ef} are the principles corresponding to CA_{¬} and IP_{¬}, where instead of ¬A we have an ∃-free formula A_{ef}.

We next recall Kreisel’s mr-interpretation and Bezem’s[1] notion of strong majorizability, which is an extension of Howard’s[5] notion of majorizability, for all types T^{X}. Combining these allows us to define the monotone mrinterpretation. For each formula A(\underline{a}), where \underline{a} are the free variables of A, Kreisel’s mrinterpretation defines, by induction on the logical structure of A, a corresponding formula ‘\underline{x} mr A’ (in words: \underline{x} modified realizes A), where \underline{x} is a (possibly empty) tuple of variables, which do not occur free in A. From a proof of A Kreisel’s mr-interpretation extracts a tuple of closed terms \underline{t} s.t. ∀\underline{a}(\underline{t}\underline{a} mr A(\underline{a})). For details see e.g. [25, 26].

Remark 4.2. 1. For every ∃-free formula A we have (\underline{x} mr A) ≡ A with \underline{x} the empty tuple.

2. (\underline{x} mr A) is always an ∃-free formula.

Definition 4.3 ([12], extending [5, 1]). The strong majorizability relation s-maj is defined as follows:

• x^{∗} s-maj_{0} x :≡ x^{∗} ≥ x

• x^{∗} s-maj_{X} x :≡ (0 =_{0} 0) in A_{(i)}^{ω}[X, d, …],

• x^{∗} s-maj_{X} x :≡ ∥x^{∗}∥_{X} ≥_{IR} ∥x∥_{X} in A_{(i)}^{ω}[X, ∥ · ∥, …],

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

Definition 4.4 ([10]). A tuple of closed terms \underline{t}^{∗} satisfies the monotone mr-interpretation of A(\underline{a}) if

∃\underline{z}(\underline{t}^{∗} s-maj \underline{z} ∧ ∀\underline{a}(\underline{z}\underline{a} mr A(\underline{a}))

We briefly recall some properties of the mr-interpretation. As we have the full axiom of choice AC in A_{i}^{ω}, resp. A_{i}^{ω}[…], one shows:

Proposition 4.5 (Troelstra[25]).

A_{i}^{ω} + IP_{ef} ⊢ A ↔ ∃\underline{x}(\underline{x} mr A)

Similarly for A_{i}^{ω}[…] + IP_{ef}.

Proof. By induction on the logical structure of A.

Corollary 4.6. 1. For every formula A ∈ A_{i}^{ω} we can construct an ∃-free

formula B_{ef} s.t.

A_{i}^{ω} + IP_{ef} ⊢ ¬A ↔ B_{ef}

Similarly for A_{i}^{ω}[…].

2. For every ∃-free formula A_{ef} ∈ A_{i}^{ω} we have that A_{i}^{ω} ⊢ A_{ef} ↔ ¬¬A_{ef}. Similarly for A_{i}^{ω}[…].

3. Over A_{i}^{ω} we have IP_{ef} ↔ IP_{¬} and CA_{ef} ↔ CA_{¬}. Similarly for A_{i}^{ω}[…].

Proof. 1. By Proposition 4.5 we have

A_{i}^{ω} + IP_{ef} ⊢ ¬A ↔ ∀\underline{y}((\underline{y} mr A) → ⊥),

where ∀\underline{y}((\underline{y} mr A) → ⊥) is ∃-free, as (\underline{y} mr A) is ∃-free.

2. This equivalence is provable intuitionistically in the context of decidable prime formulas.

3. A_{i}^{ω} + IP_{ef} ⊢ IP_{¬} follows from ‘1.’, A_{i}^{ω} + CA_{ef} ⊢ CA_{¬} follows from the fact that A_{i}^{ω} + CA_{ef} ⊢ IP_{ef} and ‘1.’. The converse implications follow from ‘2.’.

In the following, we will omit mentioning IP_{¬} and IP_{ef}, as they follow from the corresponding comprehension schemes CA_{¬} and CA_{ef} (and the decidability of =_{0}).

Discussion on extensionality, continued: As mentioned above, in the context of functional interpretation full extensionality is much too strong, as it would allow us to derive (when combined with the generalized majorizability from [12]) statements e.g. about uniform continuity which are not true in general. In the context of (monotone) modified realizability full extensionality is harmless. Extensionally defined equalities in the premise of implications, e.g. in instances of the extensionality axiom, as indeed instances of the extensionality axiom as a whole, are ∃-free and thus realized by the empty tuple. Informally speaking, functional interpretation is ‘too eager’, seeking to extract every possible and hence some unwanted bounds. In contrast, modified realizability is ‘lazy enough’ to only extract bounds where this is explicitly asked for, namely from positive existential statements. Where functional interpretation extracts bounds on universal premises in an implication, modified realizability leaves them alone. In practice, this allows us to remove the requirement to explicitly prove every extensional equality used in the proof and instead to simply assume it as a premise, leading to a more natural, intuitive treatment of extensionality.

We can prove the following theorem, corresponding to Theorem 3.2 in the classical setting:

Theorem 4.7. 1. Let σ be a type of degree 1, let ρ be a type of degree (·, 0) and let τ be a type of degree (·, X). Let s^{σ→ρ} be a closed term of A_{i}^{ω}[X, d] and let A(resp. B) be an arbitrary formula with only x, y, z, n (resp. x, y, z) free. Let Γ_{¬} be a set of sentences of the form ∀u^{α}(C → ∃v ≤_{β} tu∃w^{γ}¬D) with t^{α→β} be a closed term of A_{i}^{ω}[X, d], the type α arbitrary, the type β of degree (·, 0) and γ of degree (·, X). If

A_{i}^{ω}[X, d] + CA_{¬} + Γ_{¬} ⊢ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(¬B → ∃n^{0}A),

then one can extract a primitive recursive (in the sense of Gödel) functional Φ : S_{σ} × IN → IN such that for all b ∈ IN

∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}∃n ≤ Φ(x, b)(¬B → A)

holds in any (non-empty) metric space (X, d) whose metric is bounded by b ∈ IN and which satisfies Γ_{¬}.^{5}

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

3. If the premise is proved in A_{i}^{ω}[X, d, W, CAT(0)] instead of A_{i}^{ω}[X, d, W] then the conclusion holds in all b-bounded CAT(0) spaces satisfying Γ_{¬}.

As in the classical case, instead of single variables and single premises we may also have tuples of variables and a finite conjunction of premises.

Proof. Since prime formulas in A_{i}^{ω}[X, d] + CA_{¬} + Γ_{¬} are decidable, it follows from Corollary 4.6 that this theory is equivalent to the theory A_{i}^{ω}[X, d] + CA_{ef} + Γ′_{ef}, where Γ′_{ef} is the set of ∃-free formulas A′ equivalent to the formulas A ∈ Γ_{¬} (using Corollary 4.6). For the subsystem of A_{i}^{ω}[X, d] + CA_{ef} + Γ′_{ef} not involving (X, d), i.e. restricted to the types T, it is proved in [10] that this theory has a monotone mr-interpretation in its classical counterpart (for a somewhat more restricted set Γ′_{ef} even in itself) by terms in Gödel’s T. To extend the proof to the full theory A_{i}^{ω}[X, d]+CA_{¬}+Γ_{¬}, i.e. now involving the full range of types T^{X}, we observe the following:

5Here b_{X} is understood to be interpreted by b.

1. By similar arguments as in the classical case (see [12]) the soundness of the monotone mr-interpretation of the logical axioms and rules, the defining equations for combinators Σ, Π and the recursor R, axiom schemes E, AC and the axiom schema of induction extends to the types T^{X} without any changes.

2. The additional axioms of A_{i}^{ω}[X, d] are purely universal and do not contain ∨, and hence have a trivial monotone mr-interpretation by the empty tuple.

3. The additional ∃-quantifiers ranging over variables of type degree (·, X), both in the conclusion and in sentences of the set Γ_{¬}, resp. Γ′_{ef}, can easily be majorized using the constant b_{X} for the bound on d as shown in [12].

4. The monotone mr-interpretation extracts a realizer ψ ∈ S^{ω,X} depending only on a suitable interpretation of the constants of A_{i}^{ω}[X, d]: The majorization relation extends to T^{X} as in [12], so given a closed term ψ of A_{i}^{ω}[X, d] we can construct a majorant ψ^{∗}, by induction on the term structure of ψ such that

S^{ω,X} ⊧ ψ^{∗} s-maj ψ.

ψ^{∗} does not involve d_{X} and which depends on (X, d) only via the interpretation of the constant b_{X} by a bound b ∈ IN on the metric d and on the interpretation of 0_{X} by some arbitrary element of X. Using the same techniques as in the classical case ([12]) one can eliminate the latter dependency and construct from ψ^{∗} a functional Φ ∈ S_{0→(σ→0)} which is given by a closed term of A_{i}^{ω} (i.e. a primitive recursive functional in the sense of Gödel) s.t.

S^{ω,X} ⊧ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}∃n ≤ Φ(x, b)(¬B → A(x, y, z, n)).

Note that the negated premise ¬B, since – again by corollary 4.6 – it is equivalent to an existential free formula, does not in any way contribute to the extracted term. For A_{i}^{ω}[X, d, W] and A_{i}^{ω}[X, d, W, CAT(0)] the arguments are similar. In all three cases the final extracted term Φ is primitive recursive in the sense of Gödel, i.e. Φ is a closed term in Gödel’s T.

We furthermore show the following corollary, corresponding to Corollary 3.5 in the classical case:

Corollary 4.8. 1. Let P (resp. K) be a A_{i}^{ω}-definable Polish space (resp. compact Polish space) and let A, B and Γ_{¬} be as in the previous theorem. If A_{i}^{ω}[X, d, W] + CA_{¬} + Γ_{¬} proves that

∀x ∈ P ∀y ∈ K∀z^{X}, f^{X→X}(¬B → ∃n^{0}A)

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

∀y ∈ K∀z^{X}, f^{X→X}∃n ≤ Φ(x, b)(¬B → A)

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

2. The result also holds for A_{i}^{ω}[X, d], (X, d).

Proof. The details of the proof are similar to the classical case, i.e. by Theorem 4.7 we can extract a primitive recursive bound Φ(x, b) on n which holds in all spaces (X, d, W), resp. (X, d), whose metric is bounded by b.

Remark 4.9. As in the classical case, we can add additional assumptions about the function f, if of suitable logical form, to the premise. In the classical case we added the assumption ‘f n.e.’ and ‘F ix(f) ≠ ∅’ to the premise of the implication. Both assumptions can also be added in the semi-intuitionistic case. The condition ‘f n.e.’ is purely universal and hence is equivalent to its double negation. The statement ‘F ix(f) ≠ ∅’ can be written as ∃u^{X}C_{∀}, where C_{∀} is purely universal and so again equivalent to its double negation. Thus, first pulling out the existential quantifier from the premise ∃u^{X}C_{∀} as a universal quantifier just as ∀z^{X}, we can extract a bound Φ that does not depend on u and does not depend on any of the negated premises nor C_{∀}. Shifting the quantifier ∃u back in we get the result. In the classical case the premise ‘f n.e.’ ensures that a given f indeed behaves like a function, i.e. to prove the extensionality of f, as the weak extensionality rule QF-ER is not strong enough to ensure this. The weaker assumption ‘f d.n.e’ does not imply extensionality. This is the reason why in application 3.16 of [12] one carefully had to observe that QF-ER was in fact sufficient to formalize the proof in question. In the semi-intuitionistic case, where we allow full extensionality this is not necessary. The benefit of adding ‘F ix(f) ≠ ∅’ was that FI would weaken the statement to f has an approximate fixed point, which for non-expansive and even directionally non-expansive selfmappings of a bounded hyperbolic space is always true (see [4] and [14]) whereas ‘F ix(f) ≠ ∅’ is not. In the semi-intuitionistic case ‘F ix(f) ≠ ∅’ will not disappear from the premise, as monotone modified realizability does not weaken universal premises such as d_{X}(x, f(x)) =_{IR} 0_{IR}.

For normed linear spaces we prove the following semi-intuitionistic counterpart to Theorem 3.6:

Theorem 4.10. 1. Let σ be a type of degree 1, let ρ be a type of degree (·, 0) and let τ be a type of degree (X, C). Let s^{σ→ρ} be a closed term of A_{i}[X, ∥ · ∥, C] and let A(resp. B) be an arbitrary formula with only x, y, z, n (resp. x, y, z) free. Let Γ_{¬} be a set of sentences of the form ∀u^{α}(C → ∃v ≤_{β} tu∃w^{γ}¬D) with t^{α→β} be a closed term of A_{i}^{ω}[X, ∥·∥, C], the type α arbitrary, the type β of degree (·, 0) and γ of degree (X, C). If

A_{i}^{ω}[X, ∥ · ∥, C] + CA_{¬} + Γ_{¬} ⊢ ∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}(¬B → ∃n^{0}A),

then one can extract a primitive recursive (in the sense of Gödel) functional Φ : S_{σ} × IN → IN such that for all b ∈ IN

∀x^{σ}∀y ≤_{ρ} s(x)∀z^{τ}∃n ≤ Φ(x, b)(¬B → A)

holds in any nontrivial normed linear space (X, ∥·∥) and any b-bounded convex subset C which satisfy Γ_{¬}.

Instead of single variables and single premises we may also have tuples of variables and a finite conjunction of premises.

The proof is based on similar arguments as the proof of Theorem 3.6, resp. the variations due to the change of setting from classical to semi-intuitionistic discussed in the proof of Theorem 4.7. The variables of degree (X, C) in the sentences A ∈ Γ_{¬} can again easily be majorized by a suitable interpretation of the constant b_{X} by a bound b on the norm of the elements of the convex subset C.

Remark 4.11. In the classical case the construction of majorants d_{X}^{∗} resp. ∥ · ∥_{X}^{∗} depends on the interpretation of d_{X} resp. ∥ · ∥_{X} in the model S^{X,ω} via an ineffective operator ()_{∘}, which from a (representative of a) real number selects a canonical representative of that real number. As an operator of type 1 → 1, ()_{∘} is primitive recursive in

E^{2}(f^{1}) :=_{0} \{ \begin{matrix}0, if ∀x^{0}(f(x) =_{0} 0) \\ 1, if ¬∀x^{0}(f(x) =_{0} 0). \end{matrix}

Since the monotone functional interpretation of the defining axioms of (E^{2}) would require non-majorizable functionals (although E^{2} itselfs is trivially majorizable) one must not include the operator ()_{∘} to A^{ω}[X, …]. This causes no problems as ()_{o} only is involved in the interpretation of the theory in the model S^{ω,X}. Subsequently the ineffective ()_{o} operator can be majorized effectively! In the semi-constructive case we could actually add the ()_{∘} operator via E^{2} to the theory, as monotone modified realizability leaves the defining axioms of the E^{2} untouched, and carry out part of the argument regarding the ()_{∘} operator in the theory itself rather than in the model.

5 Application to Metric Fixed Point Theory

To illustrate the various aspects of Theorem 4.7 we consider three different proofs of (variants of) Edelstein’s Fixed Point Theorem: first a refinement of the original proof by Edelstein[3] developed in [15], next an alternative, constructive proof by Rakotch[20] and finally a more recent proof carried out in the framework of Bishop-style constructive mathematics by Bridges, Julian, Richman and Mines[2]. Though completely elementary, if not trivial, from a functional analytic point of view, this example serves well to demonstrate the various logical aspects of proof mining using the metatheorems presented in the previous sections. For recent non-trivial applications of proof mining see [11, 13, 14]. In [21], Rhoades presents a survey and comparison of a large number of different notions of contractivity, compiled from the literature on metric fixed point theory, for which fixed points theorems have been proven. Many of these notions of contractivity and the accompanying proofs of fixed point theorems are far more technical than the example presented in this section. Further surveys on notions of contractivity can be found in [22, 19]. We intend to treat such more general fixed point theorems based upon the more complicated notions of contractivity discussed in these survey articles in a subsequent paper.

Edelstein defines contractive (self-)mappings as follows:

Definition 5.1 (Edelstein[3]). A self-mapping f on a complete metric space (X, d) is contractive if for all x, y ∈ X: x ≠ y → d(f(x), f(y)) < d(x, y).

and Edelstein’s Fixed Point Theorem is:

Theorem 5.2 (Edelstein[3]). Let (X, d) be a complete metric space and let f be a contractive self-mapping on X s.t. for some x ∈ X the sequence {f^{n}(x)} has a convergent subsequence {f^{n_{i}}(x)}, then ξ = lim_{n→∞} f^{n}(x) exists and is a unique fixed point of f.

For a compact space (X, d) the sequence {f^{n}(x)} always has a convergent subsequence, and thus {f^{n}(x)} always converges to a unique fixed point. We are now interested in obtaining a computable (Cauchy) modulus δ for the sequence {f^{n}(x)} s.t. ∀m, n > N = δ(ε) : d(f^{m}(x), f^{n}(x)) < ε. In addition to ε, we must prima facie expect the rate of convergence δ to also depend on x, the space (X, d), the function f and a modulus of contractivity for f, if such a modulus exists. In an intuitionistic setting the meaning of the implication expressing the contractivity of f is to give a procedure to transform a witness of ‘d(x, y) > 0’ into a witness of ‘d(f(x), f(y)) < d(x, y)’. Proving (or assuming) contractivity of f in an intuitionistic setting yields a function that depending on x, y and an ε, by which d(x, y) is larger than 0, produces a δ by which d(f(x), f(y)) is smaller than d(x, y). Such a function, if uniform with regard to x, y ∈ X, is nothing else than a modulus of contractivity.

Remark 5.3. On compact metric spaces, or more generally, on bounded metric spaces monotone functional interpretation and monotone modified realizability automatically strengthen the general notion of contractivity to uniform contractivity, i.e. the existence of a modulus of contractivity. As we will see, the notion of uniform contractivity is sufficient even on unbounded metric spaces to guarantee the convergence of {f^{n}(x)} to a unique fixed point and to state an effective rate of convergence.

In [20] Rakotch considers functions with a multiplicative modulus of contractivity α s.t.

∀x, y ∈ X : d(x, y) > ε → d(f(x), f(y)) ≤ α(ε) · d(x, y)

where 0 ≤ α(ε) < 1 for all ε > 0.^{6} Rakotch’s multiplicative modulus of contractivity α is only one possible interpretation of witnessing the contractive inequality. From the point of view of logic, to witness an inequality s < t one has to produce an ε > 0 s.t. s + ε < t. This leads to a additive modulus of contractivity η s.t.

∀x, y ∈ X : d(x, y) > ε → d(f(x), f(y)) + η(ε) ≤ d(x, y)

It is easy to see that a modulus η can be defined given a modulus α:

η(ε) := (1 − α(ε)) · ε

To define a modulus α in terms of a modulus η we further assume that the metric d on X is bounded and define:

α(ε) := 1 − \frac{η(ε)}{b}

What is actually used to prove the convergence of the iteration sequence {f^{n}(x)} (irrespectively of whether one uses η or α) is that every such iteration sequence is bounded. Already without assuming the boundedness of X such a bound follows both from a multiplicative modulus α and an additive modulus η. It should be noted that it is strictly necessary for the moduli to be uniform with regard to x, y ∈ X, as otherwise a function, although contractive, might not have a fixed point. Edelstein’s non-uniform notion of contractivity x ≠ y → d(f(x), f(y)) < d(x, y) is in general only sufficient to prove the existence of a fixed point in compact spaces, where Edelstein’s notion is equivalent to the existence of uniform moduli α and η. In most other cases the equivalence fails. As a counterexample, consider the self-mapping f(x) := x + \frac{1}{x} of the interval [1, ∞). It is easy to see that the function f is contractive in the sense of Edelstein. Trivially, the function f has no fixed point. One furthermore proves by induction that for all n ≥ 1:

1 + ∑_{i=1}^{n} \frac{1}{i} ≤ f^{n}(1) ≤ n + 1

6Actually Rakotch requires α to be monotonically decreasing and to satisfy x ≠ y → d(f(x), f(y)) ≤ α(d(x, y))·d(x, y) instead. In the proof only the above property is needed, which follows from Rakotch’s requirements.

Since the sum ∑_{i=1}^{∞} \frac{1}{i} = ∞, the iteration sequence \{f^{n}(1)\} is unbounded, and hence f cannot have a modulus of contractivity α or η. Counterexamples even in the case of bounded metric spaces^{7} are discussed in [23].

Using a multiplicative modulus α, Rakotch proves the following variant of Edelstein’s Fixed Point Theorem:

Theorem 5.4 (Rakotch [20]). Let (X, d) be a complete metric space and let f be a contractive self-mapping on X with modulus of contractivity α, then ξ = lim_{n→∞} f^{n}(x) exists and is a unique fixed point of f.

The key step in the proof is to establish the following:

Lemma 5.5. Let (X, d) be a metric space and let f be a contractive selfmapping on X with modulus of contractivity α, then the iteration sequence {f^{n}(x)} is a Cauchy sequence.

We now expect that our metatheorems allow us to extract from a proof of Lemma 5.5 a Cauchy modulus δ; in fact it suffices to extract a bound on the modulus, as such a bound trivially also is a realizer for the modulus. Contrary to Rakotch’s proof, Edelstein’s original proof is a classical proof and since expressing that the sequence {f^{n}(x)} is a Cauchy sequence requires a Π_{3}^{0}- statement, the metatheorem for the classical case cannot be applied directly to extract a Cauchy modulus from Edelstein’s proof. In [15], Kohlenbach and Oliva use a trick to extract a bound from Edelstein’s non-constructive proof: The proof of Edelstein’s Fixed point theorem can be split up into three lemmas. Each of these lemmas is of a suitable logical form to allow extraction of a bound, and combining these bounds, the following modulus of convergence for f a self-map on a compact space K is extracted^{8}:

δ(α, b, ε) = \frac{log((1 − α(ε))\frac{ε}{2}) − log b}{log α((1 − α(ε))\frac{ε}{2})} + 1

where α is the modulus of contractivity for f, and b is a bound on the diameter of K. In accordance with Theorem 3.2, the same bound also holds if we replace the compact space K by a (more general) b-bounded metric space. Note that the Cauchy modulus δ is uniform with regard to x ∈ X and the function f.

7In fact even in the case of the closed unit ball of the Banach space c_{0}.

8Originally in [15] an additive modulus of contractivity η is considered. The extracted modulus of convergence is then δ(η, b, ε) = \frac{b−η(ε)}{η( \frac{η(ε)}{2} )}

Remark 5.6. In an unbounded space (X, d) the fact that - given a modulus of contractivity - each iteration sequence {f^{n}(x)} can be bounded yields a modulus of convergence depending, in addition to the modulus and ε, on f and the starting point x. We will discuss the details later.

The treatment of (the classical proof of) Edelstein’s fixed point theorem in [15] via monotone functional interpretation generalizes Edelstein’s result to bounded metric spaces, where using the strengthening of contractivity to uniform contractivity a Cauchy modulus for the sequence {f^{n}(x)} is extracted. Together with the observation that only the boundedness of the iteration sequence is needed not the boundedness of the whole space, the analysis of Edelstein’s classical, non-constructive proof yields essentially the same result as Rakotch’s theorem. However, with regard to the numerical quality of the modulus one can do better: As mentioned Rakotch’s proof is fully constructive, and one easily sees that the constructive proof can be formalized in A_{i}^{ω}[X, d]. Thus, without the tedious work of splitting up Edelstein’s proof, the metatheorem for the semi-intuitionistic case guarantees that we can extract an effective bound on the modulus of convergence or, without having to carry out the extraction, prove uniformities for the modulus of convergence.

In A_{i}^{ω}[X, d] we can express the fact that f^{X→X} represents a contractive function with modulus α^{1} (of type degree 1), in short: ‘f contr. α’, as

∀k^{0}∀x^{X}, y^{X}(d_{X}(x, y) ≥_{IR} 2^{−k} → d_{X}(f(x), f(y)) ≤_{IR} (1 − 2^{−α(k)}) ·_{IR} d_{X}(x, y))

Thus in the formal system A_{i}^{ω}[X, d] one can express Lemma 5.5 as:

Lemma 5.7. A_{i}^{ω}[X, d] proves

∀f^{X→X}∀x^{X}∀α^{1}∀k^{0}(f contr. α → ∃N^{0}∀m, n ≥_{0} N d_{X}(f^{m}(x), f^{n}(x)) ≤_{IR} 2^{−k}).

To see that Rakotch’s proof can be formalized in A_{i}^{ω}[X, d], one notes that the proof consists of two main parts: first it is shown that for any starting point x the sequence {f^{n}(x)} is bounded, then using this bound and the contractivity of f it is shown that {f^{n}(x)} is a Cauchy sequence and hence converges to a unique fixed point. Since the starting point x and the function f are merely used to produce a bound on the sequence {f^{n}(x)} and since the use of a modulus α, or equivalently a modulus η, implies that each iteration sequence is contained in some bounded subset of X, it is only a slight generalization to consider instead the case of a b-bounded space (X, d) in Lemma 5.7. Given a starting point x, the function f and an arbitrary ρ > 0, Rakotch shows that one can bound d(x, f^{n}(x)) for all n by

d(x, f^{n}(x)) ≤ b′ = max(ρ, \frac{2 · d(x, f(x))}{1 − α(ρ)})

Application 5.8. Theorem 4.7 a-priorily guarantees that there exists a bound δ(α, b, ε) on N that is uniform on X and f, i.e. the bound holds for all bbounded spaces (X, d) and all functions f with modulus of contractivity α. Moreover, by Theorem 4.7 we can extract an effective bound δ(α, b, ε) from Rakotch’s constructive proof, and since a bound on N also is a realizer, this gives us a modulus of convergence.

Proof. Since the relation ≤_{IR} can be expressed as a Π_{1}^{0}-predicate, the premise ‘f contr. α’ is ∃-free. The conclusion, the Cauchy property of the sequence {f^{n}(x)} is of the form ∀∃∀, but contrary to the classical case there are no restrictions on the logical form, so that we can extract an effective uniform bound δ(α, b, ε) on ∃N, i.e. an effective uniform Cauchy modulus for (f^{n}(x)).

For the actual “extraction” of a bound δ(α, b, ε), we briefly sketch the relevant, second part of Rakotch’s proof:^{9}

Let p ∈ IN be given, then by definition (we can assume d(x_{k}, x_{k+p}) > 0):

d(x_{k+1}, x_{k+p+1}) ≤ α(d(x_{k}, x_{k+p})) · d(x_{k}, x_{k+p}).

Now taking the product from k = 0 to n − 1 we get

d(x_{n}, x_{n+p}) ≤ d(x_{0}, x_{p}) · ∏_{k=0}^{n−1} α(d(x_{k}, x_{k+p})).

Since we consider a b-bounded space (X, d), obviously d(x_{0}, x_{p}) ≤ b, so

d(x_{n}, x_{n+p}) ≤ b · ∏_{k=0}^{n−1} α(d(x_{k}, x_{k+p})).

9Here we move for convenience tacitly to the more usual version of α as a function IR_{+}^{∗} → (0, 1).

If already d(x_{k}, x_{k+p}) < ε for some 0 ≤ k ≤ n − 1 we would be done, so assuming d(x_{k}, x_{k+p}) ≥ ε for all k = 0 … n − 1 and by

∀x, y ∈ X : d(x, y) ≥ ε → d(f(x), f(y)) ≤ α(ε) · d(x, y)

we get that

d(x_{n}, x_{n+p}) ≤ b · (α(ε))^{n}.

Then solving the inequality b·(α(ε))^{n} ≤ ε with regard to n yields the following Cauchy modulus:

δ(α, b, ε) = \frac{log ε − log b}{log α(ε)} + 1

The existence of the Cauchy modulus δ, with the described uniformities, is guaranteed by the semi-intuitionistic metatheorem, even without analyzing the proof. We can generalize the result further, as the proof clearly shows that it suffices to bound not the whole space, but only the iteration sequence, i.e. to bound d(x, f^{n}(x)) for all n. As discussed earlier, to produce a bound d(x, f^{n}(x)) it suffices to have a bound on d(x, f(x)). Thus for an unbounded space we have the rate of convergence:

δ′(α, ε, x, f) = δ(α, ε, b′)

where b′ is computed as described above.

As mentioned above, extracting a bound from the classical proof of Edelstein’s theorem was only possible by breaking up the proof into a couple of lemmas, each of suitable form to extract a bound, using the metatheorem for the classical case. Compared to the bound extracted from the Edelstein’s proof the bound from Rakotch’s constructive proof - guaranteed a-priorily by the metatheorem to exist and to be uniform on x ∈ X and f - is both (syntactically) simpler and better. Naturally, in many cases finding a constructive proof for a classically true theorem may be far less trivial than in the case of Rakotch’s variant of Edelstein’s theorem and in general, many classically true theorems may not have a constructive proof at all. However, as this example demonstrates, considering a constructive proof may yield significantly simpler and better bounds than in the classical case and may give fully uniform bounds from theorems having a logical form more complex than ∀∃, where the classical metatheorem in general fails, such as for example the Cauchy property of an iteration sequence. Moreover, monotone functional interpretation or monotone modified realizability may automatically lead to the necessary strengthenings of the mathematical notions involved, as e.g. strengthening the notion of contractivity to uniform contractivity. Finally, even for proofs that are developed in a fully constructive setting, the metatheorem for the semi-constructive case may reveal new uniformities not present in, or immediately obvious from, the theorem and proof under consideration. In [2] Bridges, et al. treat Edelstein’s fixed point theorem in the framework of Bishop-style constructive mathematics. A function f that is contractive in the sense of Rakotch is denoted by the concept of ‘f is an almost uniform contraction’. The following theorem is proved:

Theorem 5.9 ([2]). Let f : X → X be an almost uniform contraction on a complete metric space X. Then

1. f has a unique fixed point ξ in X; and

2. the sequence {f^{n}(x)} converges to ξ uniformly on each bounded subset of X.

This theorem largely corresponds to Rakotch’s theorem discussed above, but only the uniformity with regard to x ∈ X is stated, not the uniformity with regard to f or the bounded subset. Both uniformities follow already a-priorily from the existence of a (constructive) proof for Rakotch’s theorem by means of our metatheorem. Also a modulus of convergence is not explicitly stated, though both the uniformities and the effective modulus can be seen to be implicit in the proof. An analysis of the constructive proof in [2] easily yields an explicit modulus of convergence, which is identical to the bound extracted from Rakotch’s constructive proof.

References

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

[2] D. F. Bridges, F. Richman, W. H. Julian, and R. Mines. Extensions and Fixed Points of Contractive Maps in IR^{n}. J. Math. Anal. Appl., 165:438–456, 1992.

[3] M. Edelstein. On Fixed and Periodic Points under Contractive Mappings. J London Math. Soc., 37:74–79, 1962.

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

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

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

[7] U. Kohlenbach. Proof interpretations and the computational content of proofs. Draft, September 2004, ii+286pp, http://www.mathematik.tudarmstadt.de/∼kohlenbach/newcourse.ps.gz.

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

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

[10] U. Kohlenbach. Relative Constructivity. J. of Symbolic Logic, 63:1218– 1238, 1998.

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

[12] U. Kohlenbach. Some Logical Metatheorems with Applications in Functional Analysis. Trans. Am. Math. Soc., 357:89–128, 2005.

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

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

[15] U. Kohlenbach and P. Oliva. Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics. Proc. Steklov Inst. Math, 242:136–164, 2003.

[16] G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North-Holland Publishing Company, 1959.

[17] G. Kreisel. On weak completeness of intuitionistic predicate logic. J. of Symbolic Logic, 27:139–158, 1962.

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

[19] J. Meszáros. A Comparison of Various Definitions of Contractive Type Mappings. Bull. Calcutta Math. Soc., 84:167–194, 1992.

[20] E. Rakotch. A Note on Contractive Mappings. Proc. Am. Math. Soc., 13:459–465, 1962.

[21] B. E. Rhoades. A Comparison of Various Definitions of Contractive Mappings. Trans. Am. Math. Soc., 226:257–290, 1977.

[22] B. E. Rhoades. Contractive Definitions. In T. M. Rassias, editor, Nolinear Analysis, pages 513–526. World Sci. Publishing, Singapore, 1987.

[23] B. Sims. Examples of fixed point free mappings. In W. Kirk and B. Sims, editors, Handbook of Metric Fixed Point Theory, pages 35–48. Kluwer Academic Publishers, 2001.

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

[25] A. S. Troelstra, editor. Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Springer LNM. Springer-Verlag, Berlin, 1973.

[26] A. S. Troelstra. Realizability. In S. Buss, editor, Handbook of Proof Theory, pages 407–473. Elsevier Science B.V., 1998.

Recent BRICS Report Series Publications

RS-04-31 Philipp Gerhardy and Ulrich Kohlenbach. Strongly Uniform Bounds from Semi-Constructive Proofs. December 2004. 31 pp.

RS-04-30 Olivier Danvy. From Reduction-Based to Reduction-Free Normalization. December 2004. 27 pp. Invited talk at the 4th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2004 (Aachen, Germany, June 2, 2004).

RS-04-29 Ma�gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. December 2004. iii+45 pp.

RS-04-28 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects. December 2004. 44 pp. To appear in Theoretical Computer Science.

RS-04-27 Gerth Stølting Brodal, Rolf Fagerberg, and Gabriel Moruz. On the Adaptiveness of Quicksort. December 2004. 23 pp. To appear in Demetrescu and Tamassia, editors, Seventh Workshop on Algorithm Engineering and Experiments, ALENEX ’05 Proceedings, 2005.

RS-04-26 Olivier Danvy and Lasse R. Nielsen. Refocusing in Reduction Semantics. November 2004. iii+44 pp. This report supersedes BRICS report RS-02-04. A preliminary version appears in the informal proceedings of the Second International Workshop on Rule-Based Programming, RULE 2001, Electronic Notes in Theoretical Computer Science, Vol. 59.4.

RS-04-25 Mayer Goldberg. On the Recursive Enumerability of Fixed-Point Combinators. November 2004. 7 pp.

RS-04-24 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not Finitely Based over BPA with Interrupt. October 2004. 30 pp.

RS-04-23 Hans Hüttel and Jiří Srba. Recursion vs. Replication in Simple Cryptographic Protocols. October 2004. 26 pp. To appear in Vojtas, editor, 31st Conference on Current Trends in Theory and Practice of Informatics, SOFSEM ’05 Proceedings, LNCS,