Journal of Logic & Analysis 4:10 (2012) 1–20

1
ISSN 1759-9008

Fixed point theorems in constructive mathematics

MATTHEW HENDTLASS

Abstract: This paper gives the beginnings of a development of the theory of fixed
point theorems within Bishop’s constructive analysis. We begin with a construc-
tive proof of a result, due to Borwein, which characterises when some sets have the
contraction mapping property. A review of the constructive content of Brouwer’s
fixed point theorem follows, before we turn our attention to Schauder’s general-
isation of Brouwer’s fixed point theorem. As an application of our constructive
Schauder’s fixed point theorem we give an approximate version of Peano’s theorem
on the existence of solutions of differential equations. Other fixed point theorems
are mentioned in passing.

2010 Mathematics Subject Classification 03F55, 03F60, 46S30 (primary); 34A30,

47H10 (secondary)

Keywords: constructive analysis, fixed point theorems, differential equations

1 Introduction

Fixed-point theorems are a major tool in both functional analysis and mathematical
economics1 and are used to prove the existence of solutions to differential equations
and the existence of Nash equilibria among other things. Despite this, the constructive
literature on fixed point theorems has been scant2 . There are (at least) two reasons for
this:

(i) The standard proof of the simplest and most useful of the well known fixed point
theorems, the Banach fixed point theorem, is essentially constructive.
(ii) The non-constructive nature of Brouwer’s fixed point theorem, and the subse-
quent rejection of this theorem by Brouwer, is well known, and a constructive
approximate version for simplices (via Sperner’s lemma) is part of the folklore.
1
The main fixed point theorem used in mathematical economics, Kakutani’s fixed point
theorem, is given a constructive treatment in [16].
2
Although [9] gives a Bishop-style constructive treatment of Edelstein’s fixed point theorem;
and Kohlenbach [18, Chapter 18] examines contractive and nonexpansive fixed point theorems
for computational content using tools from proof theory.

Published: June 2012 doi: 10.4115/jla.2012.4.10

2 Matthew Hendtlass

Only recently has a fully constructive proof of the approximate version of Brouwer’s
fixed point theorem, for simplices, been presented [23].

By constructive mathematics we mean mathematics done in the framework of Bishop’s

constructive mathematics, which is essentially mathematics with intuitionistic logic
and dependent choice3 . Working with intuitionistic logic ensures that proofs proceed
in a manner which preserves computational meaning; in particular, a constructive proof
of ∃x P(x) embodies an algorithm for the construction of an object x and an algorithm
verifying that P(x) holds. In this manner, constructive mathematics can be viewed as a
high-level programming language. It should be noted that the constructive mathemati-
cian is interested only in what can in theory be computed, and is not concerned with
questions of practicality.

This paper is broken up into three sections. In the first we consider the fixed point
theorems of Banach and Brouwer; we prove that spaces with a strong connectedness
property are complete if and only if every contraction mapping has a fixed point, and
we give an approximate version of Brouwer’s fixed point theorem for uniformly se-
quentially continuous functions on totally bounded subsets of Rn with convex closures.
The second section presents a constructive treatment of Schauder’s fixed point theorem
and its extension due to Rothe. In the final section we give an application of our con-
structive Schuader’s fixed point theorem: we prove an approximate version of Peano’s
theorem on the existence of solutions of differential equations.

For convenience, we pause here to recall some constructive definitions. Let X be a

metric space and let S be a subset of X . If there exists x ∈ S, then S is said to be
inhabited; constructively this is a stronger property than S being nonempty, ¬(S = ∅).
An inhabited set S is said to be located if for each x ∈ X the distance
ρ (x, S) = inf {ρ(x, s) : s ∈ S}
from x to S exists. Let ε > 0. An ε-approximation to S is a subset T of S such
that for each s ∈ S, there exists t ∈ T such that ρ(s, t) < ε. We say that S is totally
bounded if for each ε > 0 there exists a finitely enumerable4 ε-approximation to S.
A metric space is said to be compact if it is complete and totally bounded. A totally
bounded subset of X is located [4, page 95, Propostion (4.4)].
3
See [4, 10, 12] for an introduction to constructive mathematics, and see [1, 5, 14, 19] for
constructive alternatives to ZFC.
4
A set is finitely enumerable if it is the image of {1, . . . , n} for some n ∈ N + , and a set is
finite if it is in bijection with {1, . . . , n} for some n ∈ N + ; constructively these notions are
distinct.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 3

2 The two main fixed point theorems

2.1 Banach’s fixed point theorem

A mapping f from a metric space X into itself is said to be a contraction mapping if

there exists a contraction constant r ∈ (0, 1) such that
ρ(f (x), f (y)) < rρ(x, y)
for all x, y ∈ X . A point x ∈ X is a fixed point of f if f (x) = x, and a metric space
S is said to have the contraction mapping property if every contraction mapping from
S into S has a fixed point. Any fixed point of a contraction mapping is necessarily
unique, and if a metric space S has the contraction mapping property, then so does its
completion.

The simplest and most useful of the standard fixed point theorems is the Banach fixed
point theorem: every contraction mapping of a complete metric space into itself has a
fixed point. The standard proof of this theorem (see [22] or the first part of the proof
of Theorem 1) is fully constructive.

We present a constructive proof of a result, due to Borwein [13], which characterises

when some sets with a strong connectedness property have the contraction mapping
property. A metric space X is said to be uniformly Lipschitz-connected if there exists a
positive real number L such that for all x, y ∈ X , there exists a function g : [0, 1] → X
such that g(0) = x, g(1) = y and
ρ(g(s), g(t)) 6 L|s − t|ρ(g(0), g(1))
for all s, t ∈ [0, 1].

Theorem 1 Let S be an inhabited uniformly Lipschitz-connected metric space. Then

S is complete if and only if it has the contraction mapping property.

Proof Suppose that S is complete. Let f be a contraction mapping on S with

contraction constant r ∈ (0, 1), and fix x ∈ S. Let x0 = x and xn = f n−1 (x) for each
n ∈ N. Then (xn )n>1 is a Cauchy sequence in S: if m > n > 1, then
m−1
X
rn
ρ (xn , xm ) 6 ρ xk , xk+1 < ρ (x0 , x1 ) −→ 0 as n −→ ∞.
1−r
k=n
Hence (xn )n>1 converges to some point x ∈ S; clearly f (x) = x.

Journal of Logic & Analysis 4:10 (2012)

4 Matthew Hendtlass

Conversely, suppose that S has the contraction mapping property, let (xn )n>1 be a
Cauchy sequence in S, and let x̂ be the limit of (xn )n>1 in the completion (Ŝ, ρ̂) of
(S, ρ). Without loss of generality we may take

ρ (xn , xm ) < 2− min{m,n} (m, n ∈ N).

Using countable choice and the uniform Lipschitz-connectedness of S, construct L > 0

and functions gk : [0, 1] → S (k ∈ N) such that for each k, gk (0) = xk+1 , gk (1) = xk ,
and
ρ(gk (s), gk (t)) < L|s − t|ρ(xk , xk+1 )

for all s, t ∈ [0, 1]. Using the gluing lemma [8], define a mapping
[
g : {0} ∪ [2−(k+1) , 2−k ] ∪ (1, ∞) → S ∪ {x̂}
k>1

by


 x̂ if t = 0
g(t) ≡ gk (2k+1 t − 1) if t ∈ [2−(k+1) , 2−k ]

x1 if t > 1.

Suppose that there exist t1 , t2 with t2 < t1 and ρ(g(t1 ), g(t2 )) > L|t1 −t2 |. By continuity
we may assume, without loss of generality that ti ∈ [2−ni , 2−ni +1 ] (i = 1, 2); set
s0 = t1 , sn1 −n2 = t2 , and sk = 2−n2 −1+k for 1 6 k 6 n1 − n2 − 1. Then
1 −n2
nX
ρ(g(sk−1 ), g(sk )) > ρ(g(t1 ), g(t2 ))
k=1
> L|t1 − t2 |
1 −n2
nX
= |sk−1 − sk |,
k=1

so there exists 1 6 k 6 n1 − n2 − 1 such that ρ(g(sk−1 ), g(sk )) > L|sk−1 − sk |. But

ρ(g(sk−1 ), g(sk )) = ρ gk (2k+1 sk−1 − 1), gk (2k+1 sk − 1))

6 L2k+1 |sk−1 − sk |ρ(xk+1 , xk )

6 L|sk−1 − sk |

—a contradiction. Hence

(1) ρ(g(s), g(t)) 6 L|s − t|

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 5

for all s, t in the domain of g. It follows that g is uniformly continuous on its domain,
and so extends to a uniformly continuous mapping g : [0, ∞) → S ∪ {b x} such that (1)
holds for all s, t ∈ [0, ∞).

Now define a uniformly continuous mapping h : b S → [0, ∞) by

2
h(x) ≡ ρ(x, b x).
L
Then g ◦ h is a contraction mapping on Ŝ, and therefore on S, and
x̂ = g(0) = g(h(x̂)) = g ◦ h(x̂).
Hence x̂ is the unique fixed point of g ◦ h in Ŝ. Since S has the contraction mapping
property, x̂ ∈ S, so (xn )n>1 converges.

2.2 Brouwer’s fixed point theorem

For completeness, we give a constructive proof of the approximate Brouwer fixed point
theorem, extended to uniformly sequentially continuous functions; for novelty we give
a proof based on David Gale’s proof from [15]. Before we do this we require a few
more definitions.

Let X be a metric space and let f be a function from X into X . If ρ(x, f (x)) < ε, then x
is called an ε-fixed point. A function f : X → X has approximate fixed points if for each
ε > 0 there exists an ε-fixed point of f in X . If every uniformly continuous function
from X into X has approximate fixed points, then X is said to have the approximate
fixed point property.

Gale’s proof of Brouwer’s fixed point theorem uses a generalisation of the game of
Hex. An n-dimensional Hex board of size k consists of vertices V = {1, . . . , k}n with
edges between two vertices x, y ∈ V if5 kx − yk = 1 and either xi 6 yi for each i or
yi 6 xi for each i. Then n-dimensional Hex is an n-player game where players take
turns to pick unclaimed vertices. A player gains an edge of the hex board if she owns
the nodes at either end; player i wins the game by connecting the two i-banks
i-bank 1 = {(v1 , . . . , vn ) ∈ V : vi = 0},
i-bank 2 = {(v1 , . . . , vn ) ∈ V : vi = k},
with her edges. The ‘Hex Theorem’ of [15] (which, being finitely combinatorial, is
fully constructive) says that any colouring of an n-dimensional Hex board with at most
n colours has a winner (for n > 2 there may be more than one).
5
We use k · k throughout to represent either the maximum norm or the supremum norm.

Journal of Logic & Analysis 4:10 (2012)

6 Matthew Hendtlass

Lemma 2 Let f be a function from the unit hypercube [0, 1]n into itself. Then for
n
all ε, δ > 0 either there exists
x ∈ [0, 1] such that ρ(x, f (x)) < ε or there exist
0
x, x ∈ [0, 1] such that ρ x, x < δ and ρ(f (x), f (x0 )) > ε.
n 0

Proof Write
f (x) = (f1 (x), . . . , fn (x)) ;
Fixing ε, δ > 0, without loss of generality take δ < ε/3. Pick N > 0 such that
1/N < δ , and subdivide [0, 1]n into an n-dimensional Hex board of size N . We
partition the set V of vertices of this Hex board into sets C1+ , C1− , . . . , Cn+ , Cn− , and B
such that
2ε
x ∈ C1+ ⇒ f1 (x) − x1 > ;
3
2ε
x ∈ C1− ⇒ x1 − f1 (x) > ;
3
..
.
+ 2ε
x ∈ Cn ⇒ fn (x) − xn > ;
3
2ε
x ∈ Cn− ⇒ xn − fn (x) > ;
3
x ∈ B ⇒ kf (x) − xk < ε.

By the Hex theorem, either B is inhabited, and there exists x ∈ [0, 1] such that
ρ(x, f (x)) < ε, or, as we may assume, there exists an i-path from i-bank 1 to i-bank
2 for some 1 6 i 6 n. Since no vertex of Ci+ has i-th coordinate 1 and no vertex of
Ci− has i-th coordinate 0, such a path contains points from each set. Hence there exist
adjacent vertices x, x0 such that x ∈ Ci+ and x0 ∈ Ci− . Then kx − x0 k < δ < ε/3,
fi (x) > fi (x0 ), and
fi (x) − fi (x0 ) = (fi (x) − x) + x − x0 + x0 − fi (x0 )

2ε ε 2ε
> − + = ε.
3 3 3
Therefore ρ(f (x), f (x0 )) > |fi (x) − fi (x0 )| > ε.

With this lemma at hand we can weaken the standard hypothesis of the approximate
Brouwer fixed point theorem; we only require that f : [0, 1]n → [0, 1]n be uniformly
sequentially continuous6 : for all sequences (xn )n>1 , (yn )n>1 in [0, 1]n , if ρ (xn , yn )
6
Throughout this paper, uniformly sequentially continuous can be substituted for uniformly
continuous in the definition of the approximate fixed point property.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 7

tends to zero as n → ∞, then ρ (f (xn ) , f (yn )) also tends to zero as n → ∞. It is

easy to see that uniform continuity implies uniform sequential continuity; the converse
cannot be proved constructively (see [7]).

Theorem 3 Let f be a uniformly sequentially continuous function from the unit

hypercube [0, 1]n into itself. Then f has approximate fixed points.

Proof We construct, using countable choice, sequences (xn )n>1 , xn0 n>1 as follows.

For each n ∈ N, apply Lemma 2 to construct either x ∈ [0, 1]n such that ρ(x, f (x)) < ε
or x, x0 ∈ [0, 1]n such that ρ(x, x0 ) < 1/n and ρ(f (x), f (x0 )) > ε. In the latter

case
we set xn = x and xn0 = x0 ; in the former we set xn = xn0 = x. Then ρ xn , xn0 n>1
converges to zero. Since

f is uniformly sequentially continuous, there exists N ∈ N
such that ρ f (xn ) , f xn0 < ε for all n > N . It follows that ρ (xN , f (xN )) < ε.

Next we extend the approximate Brouwer fixed point theorem, for uniformly continuous
functions, to compact convex subsets of Rn . A subset S of a normed space X is strictly
convex if for each ε > 0
there exists δ > 0 such that for all x, y in the boundary ∂S
of S, if7 ρ 12 (x − y), ∂S < δ , then kx − yk < ε. A normed space X is uniformly
convex if its unit ball is strictly convex: for all ε > 0 there exists δ > 0 such that for
all x, y ∈ X with kxk = kyk = 1, if 21 (x − y) > 1 − δ , then kx − yk < ε. Any inner
product space is uniformly convex [12, Page 93], and the Lp spaces for 1 < p < ∞
are uniformly convex [4, Chapter 7, (3.22)].

Let S be an inhabited subset of a metric space X , and let x ∈ X . We say that b ∈ S is

a closest point, or best approximation, to x in S if ρ(x, b) ≤ ρ(x, s) for all s ∈ S. The
following extends Theorem 6 of [11].

Theorem 4 Let S be a complete, located, convex subset of a uniformly convex normed

space X . Then each point in X has a unique closest point in S. Moreover, the mapping
Q from X to S sending x to the best approximation to x in S is uniformly continuous.

Proof The proof of Theorem 6 in [11] establishes that for each x ∈ X and each ε > 0
the set
Sεx = {y ∈ S : ρ(x, y) < ρ(x, S) + ε}
7
We do not require ∂S to be located here: for an arbitrary subset S of a metric space X we
use ‘ρ(x, S) < ε’ as a shorthand for ‘there exists s ∈ S with ρ(x, s) < ε. If S is located, then
this coincides with the standard meaning.

Journal of Logic & Analysis 4:10 (2012)

8 Matthew Hendtlass

has diameter no greater than ε, and hence that x has a unique best approximation in S.
y
To see that Q is uniformly continuous, observe that if kx − yk < ε/2, then Sε/2 ⊂ Sεx .
x
Hence Q(x), Q(y) ∈ Sε , so kQ(x) − Q(y)k 6 ε.

We call the mapping Q from the preceding theorem the projection onto S.

Theorem 5 Every totally bounded set S of Rn with convex closure has the approxi-
mate fixed point property.

Proof Let S be a subset of Rn satisfying the conditions of the theorem; without loss
of generality we may assume that S is both closed and a subset of the unit cube [0, 1]n .
Fix ε > 0 and let Q be the projection mapping from [0, 1]n onto S (which exists, by
the preceding theorem). Applying Theorem 3 to the mapping f ◦ Q : [0, 1]n → [0, 1]n ,
construct x ∈ [0, 1]n such that kx − f ◦ Q(x)k < ε/2. Then
kx − Q(x)k = ρ(x, S)
ε
6 kx − f ◦ Q(x)k < ,
2
so
kQ(x) − f (Q(x))k 6 kQ(x) − xk + kx − f ◦ Q(x)k
ε ε
< + = ε.
2 2
Hence Q(x) is an ε-fixed point of f .

For a subset S of a metric space X we write

Sε = {y ∈ X : ρ(x, y) < ε for some x ∈ S} .
Classically, Brouwer’s fixed point theorem holds for any metric space which is home-
omorphic to [0, 1]n ; this also holds constructively. For subsets of uniformly convex
normed spaces, this result is classically equivalent to, but seems constructively weaker
than, the following.

Proposition 6 Let X be a uniformly convex normed space, let S be a subset of X

with the approximate fixed point property, and let T be a subset of X such that for each
ε > 0 there exists a uniformly bicontinuous8 function fε : S → T such that fε (S) is
convex and totally bounded and
fε (S) ⊂ T ⊂ (fε (S))ε .
Then T has the approximate fixed point property.
8
A function f from X onto Y is uniformly bicontinuous if both f and its inverse are uniformly
continuous.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 9

Proof Let f be a uniformly continuous function from T into itself, and fix ε > 0. Let
δ > 0 be such that for all x, y ∈ T , if kx − yk < δ , then
fε/2 (x) − fε/2 (y) < ε/2,
where fε/2 is as in the statement of the proposition. Let Q be the projection onto
fε/2 (S) restricted to T , and let I : fε/2 (S) → T be the inclusion mapping; note that
kQ(t) − tk < ε/2 for all t ∈ T .

−1
Then fε/2 ◦ Q ◦ f ◦ I ◦ fε/2 is a uniformly continuous function from S into S. Hence
there exists x ∈ S such that

−1
kfε/2 ◦ Q ◦ f ◦ fε/2 (x) − xk < δ.
Then
kQ ◦ f ◦ fε/2 (x) − fε/2 (x)k < ε/2,
and so


f fε/2 (x) − fε/2 (x) 6 f ◦ fε/2 (x) − Q ◦ f ◦ fε/2 (x)
+ Q ◦ f ◦ fε/2 (x) − fε/2 (x)
ε ε
6 + = ε.
2 2
 
−1
Thus Q fε/2 (x) is an ε-fixed point of f .

The Brouwer fixed point theorem for uniformly continuous functions is equivalent to
the essentially nonconstructive lesser limited principle of omniscience,

LLPO: For each binary sequence (an )n>1 , either an = 0 for all even n or
an = 0 for all odd n.

A straightforward modification of the Brouwerian example on page 8 of [4] shows that

Brouwer’s fixed point theorem implies LLPO. In order to see the converse, suppose
that LLPO holds. Given a uniformly continuous function f from a compact convex
subset S of Rn into itself, define a uniformly continuous function g : S → R by
g(x) = kx − f (x)k. By Theorem 5 the infimum of g is zero. Since LLPO is equivalent
(see [17]) to the principle

MIN: Every uniformly continuous mapping from a compact metric space

into R attains its infimum.

Journal of Logic & Analysis 4:10 (2012)

10 Matthew Hendtlass

there exists x ∈ S such that g(x) = 0; x is then a fixed point of f .

To obtain the usual conclusion of the intermediate value theorem, it suffices to assume
that f : R → R is locally nonzero: for all x ∈ R and all ε > 0 there exists
y ∈ (x − ε, x + ε) such that f (y) 6= 0. The equivalent notion for Brouwer’s fixed point
theorem, that f : X → X is locally John Doe—for all x ∈ X and all ε > 0 there
exists y ∈ B(x, ε) such that f (y) 6= y—is not sufficient to prove Brouwer’s fixed point
theorem in higher dimensions: Orevkov [20] has given an example of a continuous
function from [0, 1]2 into itself with no fixed point. Further, Veldman [23] has shown
that Brouwer’s fixed point theorem for continuous functions with at most one fixed
point is equivalent to Brouwer’s fan theorem for detachable bars (see also [3]). (We
say that f has at most one fixed point if
max{ρ(x, f (x)), ρ(y, f (y))} > 0
whenever x 6= y.)

A function f : X → X , where X is a metric space, is nonexpansive if ρ(f (x), f (y)) 6

ρ(x, y) for all x, y ∈ X .

The standard Brouwerian example showing that Brouwer’s fixed point theorem implies
LLPO also shows that we cannot prove constructively that every nonexpansive mapping
on [0, 1] has the fixed point property.9 Using a standard classical argument (see for
example [22]), we can, however, show that such a mapping has approximate fixed
points.

Proposition 7 Let S be a bounded convex subset of a normed space X and let f be a

nonexpansive mapping of S into itself. Then f has approximate fixed points.

Proof Since we are only interested in approximate fixed points we may replace X by
its completion X̂ , and S by its closure in X̂ ; we may also assume that 0 ∈ S. Fix ε > 0
and let N > 0 be such that S is contained in the ball of radius N centered on 0. Pick
9
Classically, every continuous nonexpansive mapping on a bounded closed subset of a
uniformly convex Banach space has the fixed point property. The standard classical proof for
Hilbert spaces (see [22]) requires the statement that ‘every convex bounded closed subset of
a Hilbert space is weakly compact’, which implies LPO. As a consequence it seems likely
that the most general formulation of the nonexpansive fixed point theorem is not equivalent to
LLPO; however, if we restrict ourselves to weakly compact subsets of a Hilbert space, then
the nonexpansive fixed point theorem follows from MIN.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 11

r ∈ (1 − ε/N, 1), and let x be the unique fixed point of the contraction mapping rf .
Then
kf (x) − xk = kf (x) − rf (x)k = (1 − r)kf (x)k 6 (1 − r)N < ε.

Hence x is an ε-fixed point.

3 Schauder’s fixed point theorem

In this section we extend Brouwer’s fixed point theorem by considering compact convex
subsets of arbitrary Banach spaces; this gives us Schauder’s fixed point theorem.

We call a located subset S of a normed space X projective if there exists a uniformly

continuous projection function Q of X onto S such that ρ(x, Q(x)) = ρ(x, S) for each x
in X . We give an approximate version of Schauder’s fixed point theorem for projective
sets.

Lemma 8 Let S be a totally bounded subset of a metric space X , fix β > α > 0,
and let S0 be a convex set such that for each x ∈ S there exists x0 ∈ S0 such that
ρ(x, x0 ) < α/2. Then there exists a uniformly continuous function P from S into S0
such that kP(x) − xk < β for all x ∈ S.

Proof Let {x1 , . . . , xn } be an α/2-approximation to S, and for each 1 6 i 6 n

pick xi0 ∈ S0 such that ρ(xi , xi0 ) < α/2. Then for each x ∈ S there exists i such that
ρ(x, xi0 ) < α.

Let f1 , . . . , fn be the uniformly continuous functions from S into R given by

fi (x) = max 0, γ − kx − xi0 k ,



where γ = (α + β)/2. Then for each x ∈ S, there exists i such that

fi (x) > γ − α;

whence Pn
fi (x)xi0
P(x) ≡ Pi=1
n
i=1 fi (x)

defines a uniformly continuous map from S into S0 .

Journal of Logic & Analysis 4:10 (2012)

12 Matthew Hendtlass

Let r > 0 and write {1, . . . , n} as the disjoint union of two sets P, Q such that

i ∈ P ⇒ kx − x0 k < γ + r;
i ∈ Q ⇒ kx − x0 k > γ.

Then P(x) is a convex combination of points in P, so

kP(x) − xk 6 max{kx − xi0 k : i ∈ P} < γ + r.

Since r > 0 is arbitrary, it follows that kP(x) − xk 6 γ < β for all x ∈ S.

Theorem 9 Let S be an inhabited, totally bounded, projective subset of a normed

space X . Then S has the approximate fixed points property.

Proof Let f : S → be a uniformly continuous function. Fixing ε > 0, let {x1 , . . . , xn }

be an ε/8-approximation to S. Using [4, Lemma 2.5, Chapter 7], construct a finite-
dimensional subspace V of X , with a basis contained in S, such that

ρ(xi , V) < ε/8

for all i ∈ {1, . . . , n}. For each such i pick xi0 ∈ V such that kxi − xi0 k < ε/8. Then
for each x ∈ S, there exists i ∈ {1, . . . , n} such that kx − xi0 k < ε/4. Let S be the
closed convex hull of {x10 , . . . , xn0 }, and let Q : S0 → S be the restriction to S0 of the
projection onto S. If ni=1 λi = 1 and each λi ≥ 0, then
P

n
! n n
X X X
Q λi xi0 − λi xi0 ≤ λi Qxi0 − xi0
i=1 i=1 i=1
Xn
λi ρ xi0 , S


=
i=1
n
X ε
≤ λi xi0 − xi < ;
8
i=1

thus kQ(x) − xk < ε/4 for all x ∈ S0 .

Using Lemma 8, construct a uniformly continuous function P : S → S0 such that

kP(x) − xk < ε/3 for all x ∈ S. Then P ◦ f ◦ Q is a uniformly continuous map from
S0 into S0 ; by Brouwer’s fixed point theorem, Theorem 3, there exists x0 ∈ S0 such that

kP ◦ f ◦ Q(x0 ) − x0 k < 5ε/12;

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 13

write x = Q(x0 ). Then x ∈ S and

kf (x) − xk 6 kf (x) − P ◦ f ◦ Q(x0 )k + kP ◦ f ◦ Q(x0 ) − x0 k + kx0 − xk
= kf (x) − P(f (x))k + kP ◦ f ◦ Q(x0 ) − x0 k + kx0 − Q(x0 )k
< ε/3 + 5ε/12 + ε/4 = ε.
Hence x is an ε-fixed point of f .

By Theorem 4, every complete, located, convex subset of a uniformly convex space is

projective; this gives us the following result.

Corollary 10 Let S be an inhabited, totally bounded subset of a uniformly convex

normed space X such that the closure S of S is convex. Then S has the approximate
fixed points property.

Proof Since we are interested in approximate fixed points, replacing X with its
completion X̂ and S with its closure in X̂ , we may assume that S is compact and
convex. The result then follows from Theorems 4 and 9.

Strictly convex sets are also projective; the proof is similar to that of Theorem 4 (which,
in turn, is based on the proof of Theorem 6 of [11]).

Theorem 11 Let S be an inhabited, complete, located, strictly convex subset of a

normed space X . Then each point in X has a unique closest point in S. Moreover, the
mapping Q from X to S sending x to the best approximation to x in S is uniformly
continuous.

Proof Let x be a point of
X , fix ε > 0, and let δ ∈ (0, ε/2) be such that for all
x, y ∈ ∂S, if ρ 21 (x − y), ∂S < 2δ , then kx − yk < ε/2. Set

Sεx = {y ∈ S : kx − yk < ρ(x, S) + δ/2} ;

and fix y1 , y2 ∈ Sεx . Either ρ(x, S) < δ/2 and
ky1 − y2 k 6 ky1 − xk + ky2 − xk < δ + δ < ε,
or, as we may assume, ρ(x, S) > 0. Since S is located S ∪ ∼S is dense in X ; whence
we can apply Proposition 5.15 of [12] to construct the unique points y01 , y02 such that y0i
is in the intersection of
[x, yi ] ≡ {tx + (1 − t)y : t ∈ [0, 1]}

Journal of Logic & Analysis 4:10 (2012)

14 Matthew Hendtlass

and ∂S. Then, for i = 1, 2,

ρ(yi , y0i ) = ρ(x, yi ) − ρ(x, y0i ) < ρ(x, S) + δ/2 − ρ(x, S) = δ/2,
so
1 1 1
x − (y01 + y02 ) 6 kx − y01 k + kx − y02 k
2 2 2
1
kx − y1 k + ky1 − y01 k + kx − y2 k + ky2 − y02 k


6
2
< ρ(x, S) + 2δ.
Apply Proposition 7.15 of [12] again to construct the unique point z in the intersection
1
of [x, (y01 , y02 )] and the boundary of S. Then
2
1 1
ρ(z, (y01 + y02 )) = ρ(x, (y01 + y02 )) − ρ(x, z)
2 2
< ρ(x, S) + 2δ − ρ(x, S) = 2δ.
Therefore, by our choice of δ , ky01 − y2 0k < ε/2, and so
ρ(y1 , y2 ) 6 ρ(y1 , y01 ) + ρ(y01 , y02 ) + ρ(y02 , y2 )
< δ/2 + ε/2 + δ/2 < ε.

Hence the diameter of Sεx is no greater than ε. The proof then proceeds as in Theorem
4.

Corollary 12 Let S be an inhabited, totally bounded, strictly convex subset of a

normed space X such that the closure of S is strictly convex. Then S has the approxi-
mate fixed points property.

Proof As for Corollary 8.

In the proof of Theorem 9, we begin by approximating the convex, totally bounded

set S by a set S0 contained in a finite dimensional subspace of X . We then use f to
define a uniformly continuous map from S0 into itself to which we can apply Brouwer’s
fixed point theorem. In particular, this requires us to construct a uniformly continuous
map from S0 into S which is close to the identity map; it is in order to construct this
mapping that we require S to be projective. In the following result we circumvent this
requirement: by considering only open sets, we can ensure that S0 is contained in S;
we can then produce a uniformly continuous function from S0 into S0 by restricting the
domain of f , rather than composing f with a mapping from S0 into S, as in Theorem
9.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 15

Theorem 13 Every inhabited, open, totally bounded, convex subset of a normed space
has the approximate fixed points property.

Proof The proof is similar to that of the preceding theorem. Let S be an inhabited,
open, totally bounded, convex subset of a normed space X , and let f : S → S be a
uniformly continuous function. Let {x1 , . . . , xn } be an ε/6-approximation to S. We
construct, as follows, a finite-dimensional subspace V of X such that V contains an
ε/3-approximation {x10 , . . . , xn0 } to S. Let V1 = span{x1 } and x10 = x1 . Suppose that
we have constructed Vk−1 and x10 , . . . , xk0 and let r ∈ (0, ε/6) be such that B(xk , r) ⊂ S.
Either ρ(xk , Vk−1 ) > 0 or ρ(xk , Vk−1 ) < r. In the first case we set
Vk = span{Vk−1 , xk }
and xk = xk0 . In the second case, pick xk0 ∈ V such that kxk − xk0 k < r and set
Vk = Vk−1 . Set V = Vn ; it is easy to see that {x10 , . . . , xn0 } is an ε/3-approximation to
S.

Let S0 be the convex hull of {x10 , . . . , xn0 }. Then S0 ⊂ S and, by Lemma 8, there exists
a uniformly continuous function P : S → S0 such that kP(x) − xk < ε/2 for all x ∈ S.
Using Brouwer’s fixed point theorem, applied to P ◦ f |S0 : S0 → S0 , construct x ∈ S0
such that kP ◦ f (x) − xk < ε/2. Then
kf (x) − xk 6 kf (x) − P ◦ f (x)k + kP ◦ f (x) − xk
< ε/2 + ε/2 = ε.
Hence x is an ε-fixed point of f .

We can extend Theorem 9 to give an approximate version of Rothe’s theorem [21, 22]
for projective sets.

Theorem 14 Let S be a compact, convex, projective subset of a normed space X , and

let f be a uniformly continuous function from S into X which maps the boundary of S
into S. Then f has approximate fixed points.

Proof Fix ε > 0, let Q be the projection onto S, and let δ ∈ (0, ε/4) be such that if
kx − yk < δ , then kf (x) − f (y)k < ε. Since Q ◦ f is a uniformly continuous function
from S into S, it follows from Schauder’s fixed point theorem for projective sets that
there exists x ∈ S such that kQ ◦ f (x) − xk < δ . Suppose that ρ(f (x), S) > ε/4.
Thenf (x) ∈
/ S and ρ(x, y) > δ for all y ∈ ∂S—this contradicts that kQ ◦ f (x) − xk < δ .

Journal of Logic & Analysis 4:10 (2012)

16 Matthew Hendtlass

Therefore ρ(f (x), S) 6 ε/4, so

kf ◦ Q(x) − Q(x)k 6 kf ◦ Q(x) − f (x)k + kf (x) − Q ◦ f (x)k
+kQ ◦ f (x) − xk + kx − Q(x)k
< ε/4 + ε/4 + δ + δ < ε.
Hence Q(x) is an ε-fixed point of f .

Since Schauder’s fixed point theorem implies Brouwer’s fixed point theorem and fol-
lows from MIN, it is equivalent to LLPO.

4 An application

We give an application of the approximate Schauder fixed point theorem for uniformly
convex spaces (Corollary 10). A standard application of Schauder’s fixed point the-
orem is in proving Peano’s Theorem asserting the existence of solutions to particular
differential equations:
Peano’s Theorem Let A be a closed subset of R, let (x0 , y0 ) ∈ A, and let
r > 0 be such that if |x − x0 | 6 r and |y − y0 | 6 r, then (x, y) ∈ A. Let
f : A → R be continuous, let
M > sup {|f (x, y)| : |x − x0 | 6 r, |y − y0 | 6 r} ,
and set h = min {r, r/M}. Then the differential equation
(2) y0 = f (x, y), y (x0 ) = y0
has a solution y on the interval [x0 − h, x0 + h].
However, since the exact version of Peano’s Theorem is constructively equivalent to
LLPO (see [6], which also gives an alternative constructive proof of an approximate
Peano’s Theorem, [2] gives a proof that Peono’s Theorem implies LLPO), we can only
hope to prove an approximate version of Peano’s Theorem.

There is another, more pressing, problem: Peano’s Theorem asserts the existence
of solutions to particular differential equations in the normed space C(I), for some
interval I , with the supremum norm, but this normed space is not uniformly convex.
To overcome this difficulty, we first approximate the sup norm with a uniformly convex

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 17

norm—this relies on being able to restrict the possible solutions of (2) to a sufficiently
friendly subset of C(I).

A solution to the differential equation (2) on an interval I in R is precisely a fixed

point of the mapping U : C(I) → C(I) given by
Z x
U(y) = y0 + f (t, y(t))dt.
x0

The differential equation (2) is said to have approximate solutions on an interval I if

for all ε > 0 there exists a continuous function y : I → R such that kU(y) − yk < ε.

To prove a constructive version of Peano’s theorem, we need the following lemma.

A subset S of C(I) is Lipschitz if there exists M > 0 such that for all y ∈ S and all
x1 , x2 ∈ I we have
|y(x1 ) − y(x2 )| 6 M|x1 − x2 |;
that is, M is a Lipschitz constant for each y ∈ S. We call M a Lipschitz constant for S.

Lemma 15 If S is a bounded Lipschitz subset of C(I), then for each ε > 0 there
exists p > 1 such that | kyk − kykp | < ε for all y ∈ S.

Proof Fix ε > 0 and let N be a bound for S and M be a Lipschitz constant for S. It
suffices to choose p > 1 such that |kyk − kykp | < ε, where y is given by
  
4N 2 a+b
y(x) = max M, 1− x− − N.
b−a b−a 2
This is possible because, in C([−1, 1]),
Z 1 1/p
p
k1 − |x|kp = |1 − |x|| dt
−1
 Z 1 1/p
p
= 2 |1 − x| dt
0
 1/p
2
= −→ 1,
p+1
as p → ∞.

Theorem 16 Let A ⊂ R2 be closed, (x0 , y0 ) ∈ A◦ , and r > 0 be such that if

|x − x0 | 6 r, then (x, y) ∈ A. Let f : A → R be uniformly continuous, let
M > sup {|f (x, y)| : |x − x0 | 6 r, |y − y0 | 6 r} ,

Journal of Logic & Analysis 4:10 (2012)

18 Matthew Hendtlass

and let h = min {r, r/M}. Then the differential equation

y0 = f (x, y), y (x0 ) = y0
has approximate solutions.

Proof Fix ε > 0, let I = [x0 − h, x0 + h], and set

M = {y ∈ C(I) : |y(t) − y0 | 6 r for all t ∈ I} .
Since f is uniformly continuous, U is also uniformly continuous. Define


S = y ∈ M : kUyk 6 |y0 | + Mh ∧


∀x1 ,x2 ∈I |y(x1 ) − y(x2 )| 6 M|x1 − x2 | .
Let y ∈ M and t ∈ I . Then
Z x
|Uy(t) − y0 | = f (t, y(t))dt 6 Mh 6 r,
x0
Z x
kUyk = y0 + f (t, y(t))dt 6 |y0 | + Mh, and
x0
Z x2
|Uy(x1 ) − Uy(x2 )| 6 f (t, y(t))dt
x1
6 M|x1 − x2 |.
Hence U maps M into S. By (a slight variation of) [4, (5.6) pg. 102], S is compact;
and, by Lemma 15, there exists p > 1 such that
|kyk − kykp | < ε/2,
for all y ∈ S. We can now apply the Schauder fixed point theorem to U|S to construct
a y ∈ S such that kUy − ykp < ε/2. Then
kUy − yk < kUy − ykp + ε/2
< ε/2 + ε/2 = ε,
so y is an ε-fixed point of U .

The above proof readily extends to a system

y01 = f1 (y1 , . . . , yn , x)
y02 = f2 (y1 , . . . , yn , x)
..
.
y0n = fn (y1 , . . . , yn , x)
of linear ordinary differential equations.

Journal of Logic & Analysis 4:10 (2012)

Fixed point theorems in constructive mathematics 19

References

[1] P H G Aczel and M Rathjen, Notes on Constructive Set Theory, Report

No. 40, Institut Mittag-Leffler, Royal Swedish Academy of Sciences, 2001;
www.ml.kva.se/preprints/archive/2000-2001/2000-2001-40.pdf.
[2] M Beeson, Foundations of Constructive Mathematics: Metamathematical Studies,
Springer, Berlin/Heidelberg/New York, 1985.
[3] J Berger and H Ishihara, Brouwer’s fan theorem and unique existence in constructive
analysis, Math. Log. Quart., 51(4) (2005), 360–364; doi: 10.1002/malq.200410038.
[4] E A Bishop and D S Bridges, Constructive Analysis, Grundlehren der Math. Wiss., 279,
Springer-Verlag, Heidelberg, 1985.
[5] D S Bridges, A constructive Morse theory of sets, in: Mathematical Logic and its
Applications (D. Skordev, ed.), Plenum Publishing Corp., 1987, New York, 61–79.
[6] D S Bridges, Constructive solutions of differential equations, preprint.
[7] D S Bridges, H Ishihara, P Schuster, and L Vita, Strong continuity implies uniform
sequential continuity, Arch. Math. Logic 44 (2005) 887–895; doi: 10.1007/s00153-
005-0291-1.
[8] D S Bridges, I Loeb, Glueing continuous functions constructively, Arch. Math. Log.
49(5)(2010), 603–616 ; doi: 10.1007/s00153-010-0189-4.
[9] D S Bridges, F Richman, W H Julian, and R Mines, Extensions and Fixed Points of
Contractive Maps in Rn , J. of Math. Anal. and Appl., 165(2)(1992), 438-456; doi:
10.1016/0022-247X(92)90050-N.
[10] D S Bridges and F Richman, Varieties of Constructive Mathematics, London Math.
Soc. Lecture Notes 97, Cambridge Univ. Press, 1987.
[11] D S Bridges, F Richman, and P Schuster, Linear independence without choice, Ann.
Pure Appl. Logic 101(2000), 95–102; doi: 10.1016/S0168-0072(99)00030-5.
[12] D S Bridges and L S Vı̂ţă, Techniques of Constructive Analysis, Universitext, Springer-
New-York, 2006.
[13] J M Borwein, Completeness and the Contraction Principle, Proceedings of the American
Mathematical Society, 87(2)(1983), 246–250; doi: 10.2307/2043697.
[14] H M Friedman, Set Theoretic Foundations for Constructive Analysis, Ann. Math.
105(1)(1977), 1–28; doi: 10.2307/1971023.
[15] D Gale, The game of hex and the Brouwer fixed-point theorem, American Mathematical
Monthly, December 1979, 818-827; doi: 10.2307/2320146.
[16] M Hendtlass, Kakutani’s fixed point theorem in constructive mathematics, submitted
for publication.

Journal of Logic & Analysis 4:10 (2012)

20 Matthew Hendtlass

[17] H Ishihara, An omniscience principle, the König lemma and the Hahn-
Banach theorem, Z. Math. Logik Grundlagen Math. 36(1990), 237 – 240; doi:
10.1002/malq.19900360307.
[18] U Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathe-
matics, Springer Monographs in Mathematics, 2008.
[19] J Myhill, Constructive set theory, J. Symbolic Logic 40(3) (1975), 347–382; doi:
10.2307/2272159.
[20] V P Orevkov, A constructive map of the square into itself, which moves every con-
structive point, Dokl. Akad. Nauk SSSR 152(1963), 55–58.
[21] E Rothe, Zur Theorie der topologischen Ordnung und der Vektorfelder in Banachschen
Räumen, Compos. Math. 5(1937), 177-196.
[22] D R Smart, Fixed Point Theorems, Cambridge Univ.Press, 1974.
[23] W Veldman, Brouwer’s approximate fixed-point theorem is equivalent to Brouwer’s fan
theorem, in Logicism, Intuitionism, and Formalism, Part II, Synth. Libr., 341, Springer,
Dordrecht, 2009, 277–299,; doi: 10.1007/978-1-4020-8926-8 14.

Department of Pure Mathematics, University of Leeds

Leeds LS2 9JT, UK
[email protected]

Received: 23 August 2011 Revised: 13 February 2012

Journal of Logic & Analysis 4:10 (2012)