Does the Brouwer fixed point theorem admit a constructive proof?

Question

Wikipedia and a few websites (and a few mathoverflow answers) say there is a constructive proof of the Brouwer fixed point theorem, some others say no. The argument for a constructive proof is always the same. The Brouwer fixed point theorem is equivalent to some other results (Miranda, Sperner) where some algorithm produces some object (trichromatic triangle etc) related to a potential fixed point, but in fact, one also needs an additional compactness argument to conclude, and this last step does not appear to me to be constructive.

I am not a logician, so my question is

can one give a mathematical rigorous meaning to the following statement: "there is no constructive proof to the Brouwer fixed point theorem"?

Answer 1

You are correct in observing the flaw in the claims for BFPT to be constructive: There is no algorithm that takes a sequence in the unit hypercube and outputs some accumulation point of it. This task is in fact LESS(1) constructive that BFPT itself. We can be slightly less wasteful, and come up with a sequence converging to some fixed point of a function, but still, computing the limit of a converging sequence is less constructive thatn BFPT.

François has already explained how accepting BFPT compels us to also accept LLPO via IVT. However, IVT is in a sense more constructive than the more general BFPT: Any computable function $f : [0,1] \to [-1,1]$ with $f(0) = -1$ and $f(1) = 1$ has a computable root. However, a computable function $f : [0,1]^2 \to [0,1]^2$ can fail to have any computable fixed points at all.

A framework to compare how constructive certain theorems are is found in Weihrauch reducibility, and Brouwer's Fixed Point theorem is discussed in detail in: http://arxiv.org/abs/1206.4809

[1] For this, see http://arxiv.org/abs/1101.0792

Answer 2

It's easier to think about the Intermediate Value Theorem, which is equivalent to the Brouwer Fixed-Point Theorem for the unit interval.

The main issue is that dichotomy for (Cauchy) real numbers is not constructively valid: given two real numbers $\alpha,\beta$, there is no algorithm to decide whether $\alpha \leq \beta$ or $\alpha \geq \beta$. This principle is equivalent to the Lesser Limited Principle of Omniscience (LLPO) and it's non-constructive nature is illustrated by a classic Brouwerian counterexample:

Define the sequence of rationals $(a_n)_{n=0}^\infty$ by $a_n = (-2)^{-k}$ if $k \leq n$ and the first occurrence of the sequence $736667843909774044615061702878$ in $\pi$ begins $k$-digits after the decimal point; if there is no such $k \leq n$, then $a_n = 0$. This is a well-defined Cauchy sequence (with a known rate of convergence) so the limit $\alpha = \lim_{n\to\infty} a_n$ is a well-defined real number. Is $\alpha \geq 0$ or $\alpha \leq 0$?

If the given sequence does occur in $\pi$, then we will eventually know that $\alpha > 0$ or $\alpha < 0$ and respond accordingly. However, if the given sequence does not occur in $\pi$, though both answers are valid in this case, neither answer can be proven correct without an infinite amount of information about the digits of $\pi$ (which the example assumes is not known at this time).

Returning to the Intermediate Value Theorem, consider the piecewise linear function $f:[-1,1]\to[-1,1]$ that interpolates the points $(-1,1),(-1/2,\alpha),(1/2,\alpha),(1,1)$. The Intermediate Value Theorem says that there is a number $r \in [-1,1]$ such that $f(r) = 0$. Note that $\alpha \geq 0$ iff $r \leq 1/2$ and $\alpha \leq 0$ iff $r \geq -1/2$. Now, determining whether $r \leq 1/2$ or $r \geq -1/2$ is easy: compute $r$ to enough accuracy to know that it lies within an open interval with length $1$ and rational endpoints; that interval cannot contain both $1/2$ and $-1/2$ and that is enough to know whether $r \leq 1/2$ or $r \geq -1/2$.

So, from the above, we see that if we had a constructive proof of the Intermediate Value Theorem, we would also have a constructive proof of dichotomy. Since there is no constructive proof of dichotomy, there cannot be a constructive proof of the Intermediate Value Theorem and, for the same reason, there cannot be a constructive proof of the Brouwer Fixed-Point Theorem.

---

The Brouwerian counterexample above might not be convincing since we (at least believe) that we know nontrivial information about $\pi$. Of course, the specific number $\pi$ is irrelevant; it's just the traditional choice for Brouwerian counterexamples. Here is a similar example that relies on the existence of inseparable pairs of computably enumerable sets.

Say a sequence $(q_n)_{n=0}^\infty$ of rational numbers is rapidly Cauchy if $|q_n - q_m| \leq 1/2^N$ for all $m,n > N$. (This is one of the typical definitions of Cauchy real numbers.) Suppose we did have an algorithm $M$ to decide whether the limit of a rapidly Cauchy sequence is nonnegative or nonpositive.

Now given an index $e$, define $(a_{e,n})_{n=0}^\infty$ to be $a_{e,n} = (-1)^m/2^s$ if the $e$-th Turing machine halts in exactly $s \leq n$ steps and outputs $m$, and set $a_{e,n} = 0$ if the $e$-th Turing machine does not halt in $n$ or fewer steps. Each of these sequences is an effectively computable rapidly Cauchy sequence. If I apply my proposed $M$ to the $e$-th sequence, I obtain a total computable function $s:\mathbb N \to \{0,1\}$ such that if $s(e) = 0$ then $\lim_{n\to\infty} a_{e,n} \leq 0$ and if $s(e) = 1$ then $\lim_{n \to \infty} a_{e,n} \geq 0$.

Note that $\lim_{n\to\infty} a_{e,n} > 0$ iff $e$ belongs to the set $A$ of all indices for Turing machines that halt with even output, and $\lim_{n \to\infty} a_{e,n} \lt 0$ iff $e$ belongs to the set $B$ of all indices for Turing machines that halt with odd output. The pair $A,B$ is one of the standard prototypical examples of an inseparable pair, so there is no computable set $C$ such that $A \subseteq C$ and $B \cap C = \varnothing$. However, the set $C = \{e : s(e) = 1\}$ does exactly that!

Answer 3

I have thought about this recently, and here is I think the best constructively valid statement one can extract from Brouwer fixe point theorem (framework : internal logic of an elementary topos, real numbers are "Dedekind real numbers", i.e. two-sidded Dedekind cut, with the geometric version of the axiom) :

Theorem: Let $K$ be an $n$-dimensional simplex in $\mathbb{R}^m$. Let $f : K \rightarrow K$ be a uniformly continuous map, then for each $\epsilon >0$ there exists an $x \in K$ such that $d(x,f(x))<\epsilon$.

A few remark about it:

• One can of course replace the $n$-simplexe by an $n$-ball as there is an explicit (bi-uniform) homeomorphism between those two spaces.

• The uniform continuity of the map is not immediate at all as it is not possible to prove that $K$ is compact constructively. In fact, the uniformity of $f$ is equivalent to the fact that $f$ is defined as a map of the ``localic" $n$-simplex (which is always compact).

• Once we replaced $f$ by a map between the localic $n$-simplex the result can be imediately proved, at least in Grothendieck toposes, by using Barr's covering theorem. One can also go though the proof using Sperner lemma and check that it is constructive once all the additional hypothesis are added.

• Finally, I'm not convince that this produces any reasonable algorithms to actually find an "almost" fixed point : indeed, if you take a look to the complexity of the algorithm produced by the Sperner lemma argument, then it appears to be of the same order than the algorithm corresponding to the Barr covering argument which would be: Pick a $\mu$ small enough (depending on the uniform continuity of $f$), Pick a familly of $x_i$ in $K$ such that each $x$ in $K$ is at distant smaller than $\mu$ of $x_i$ and then try all the $x_i$, one of them has to satisfy $d(f(x_i),x_i)<\epsilon$ because of the non-constructive of Brouwer fixed point theorem. From this perspective, the Sperner's lemma agument is just a complex way of choosing the order in which you test the $x_i$ but it has no reason to be faster than any other at least in the worst case scenario (but maybe it is better "on average", I don't know)

Answer 4

One constructive version of the Brouwer fixed-point theorem which I find very elegant and illustrating runs like this:

Theorem (constructive Brouwer fixed-point theorem)

Let $B$ be the closed unit ball in $\mathbb{R}^n$ for $n\in\mathbb{N}$, and let $f$ be a uniformly continuous function from $B$ to itself. Let $G_f=\{(x,f(x))|\,x\in B\}$ be the graph of $f$ in $B\times B$, and let $D$ be the diagonal $\{(x,x)|\,x\in B\}$, also in $B\times B$.

Then $d(G_f, D)=0$.

This version is short, and yet provides all the constructive information needed for approximative BFP-versions.

---

[update for clarification, oct 2019:]

• For two subsets $A, B$ and $\rho\geq 0$ we write $d(A, B)=\rho$ when we can determine that $\inf(\{d(a,b)| a\in A, b\in B\})$ exists constructively and equals $\rho$.
• The above phrasing of the theorem is classically equivalent to the usual phrasing of the BFPT. (That also holds for Simon Henry's answer which in essence gives the same theorem. Still, one doesn't need a localic approach to prove it, it holds in plain BISH).