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"?

  • 6
    It's difficult to assign a single rigorous meaning to it, because things that classically would all be considered as the BFPT (eg "BFPT for Cauchy reals" and "BFPT for Dedekind reals") may not be constructively equivalent. But once a single statement (up to constructive equivalence) is chosen, then certainly its constructive probability is a rigorous question. – Peter LeFanu Lumsdaine Apr 13 '15 at 16:12
  • 2
    Related: mathoverflow.net/questions/105883/… – Piyush Grover Apr 13 '15 at 16:12
  • 2
    Since @PeterLeFanuLumsdaine mentioned the Cauchy/Dedekind issue, note that my answer specifically pertains to Cauchy reals as defined in the Bishop school of constructivism, for example. For (at least some common flavors of) Dedekind reals, dichotomy is constructively provable because $0$ can only lie in one of the two cuts of $\alpha$. In that case, the Bisection algorithm, for example, can be used to find a rapidly Cauchy sequence converging to a solution to the IVT but then it's not clear how to get a Dedekind real out of that. – François G. Dorais Apr 13 '15 at 18:48
  • 2
    So: Would L.E.J. Brouwer himself accept the proof? – Gerald Edgar Apr 13 '15 at 20:14
  • 2
    @Edgar. From the mathscinet review of Brouwer's 1952 article "Nonconstructible fixed points indicated by classical theorems" (I can't access the article itself, in Dutch) "The author gives a construction which from his point of view defines a topological transformation of a closed square into itself, for which no fixed point can be found [...]" – coudy Apr 13 '15 at 20:56
up vote 15 down vote accepted

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

  • 1
    Was Baigger the first? I thought it was Orevkov in 1963? – Timothy Chow Apr 14 '15 at 0:20
  • Yes, Orevkov was first. Baigger's work is built on Orevkov's construction and filling in some more details. – Arno Apr 14 '15 at 0:28
  • 1
    "Any computable function [...] has a computable root": I'm surprised by that. I'm pretty sure that not every such computable function has a constructively computable root. – TonyK Apr 14 '15 at 15:54
  • @TonyK: Using a modified bisection algorithm, we can compute an interval (as a closed set, ie approximated from the outside) on which the function is zero. Now comes the non-constructive case distinction: If the interval contains a single point, we can compute this. If not, it contains some rational (and rationals are computable). – Arno Apr 14 '15 at 17:32
  • 1
    @TonyK While being positive is not decidable, it is semidecidable. So we try for all rationals within the current bounds to find a proof that the function is positive/negative there. If the function is not constant 0, we'll find one eventually, and replace the appropriate current interval bound with it. – Arno Apr 14 '15 at 18:38

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!

  • 1
    This is not a constructive answer. Obviously what is meant by "constructive proof" is that when everything in sight is computable and decidable, then the proof allows to extract an algorithm which yields an approximation scheme. – Guntram Apr 13 '15 at 16:22
  • 1
    @Guntram: That's right: what I show is that IVT is actually equivalent to LLPO (assuming you believe LLPO can be repeated indefinitely in order to carry out the usual bisection argument). So if you believe LLPO is constructive or you have other ways to get around this issue, then everything is fine! – François G. Dorais Apr 13 '15 at 16:31
  • 1
    This is not a constructive proof, since it relies on the law of excluded middle, that either LLPO is constructive or it is not. What happens if this information cannot be computed? :-) – Asaf Karagila Apr 13 '15 at 16:54
  • 5
    @AsafKaragila: I was just joking or not Can you prove this constructively? – Emil Jeřábek Apr 13 '15 at 21:33
  • 6
    @Emil: It wasn't a constructive comment. :-) – Asaf Karagila Apr 14 '15 at 15:12

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)

  • 2
    Concerning the last paragraph: the finitized version of the problem is PPAD-complete, hence one shouldn’t expect any algorithm significantly faster than brute-force search. – Emil Jeřábek Apr 14 '15 at 10:25
  • Ok, good to know. – Simon Henry Apr 14 '15 at 10:48
  • $\mu$ is chosen using uniform continuity, such that $\mu < \epsilon/2$ and if $d(x,y) < \mu$ then $d(f(x),f(y))<\epsilon/2$. Now if $x_i$ is at distance $< \mu$ of an actual fixed point $p$ then $d(x,f(x_i)) < d(x_i,p) +d(p,f(p)) + d(f(p),f(x_i) ) < \epsilon $. So from the non constructive fixed point theorem one deduce the existence of an algorithme that produces the approximate fixed point claimed in my post. – Simon Henry Nov 21 '16 at 10:35
  • @ValerySaharov : That is a tricky question. what I can prove is that this version of the theorem holds in the internal logic of Grothendieck toposes by using Barr's Covering theorem, which is an external and non-constructive argument. Using this in the classyfing topos for uniformly continuous map from an n-simplex to itself (which exists) one can deduce the existence of a constructive proof of this theorem. So I can prove non-constructively that there is a constructive proof of the statement. (to be continued) – Simon Henry Jan 3 '17 at 15:20
  • Whether this constitute a constructive proof or not is subtle. If you are only a constructivist because you are interested in some model of constructive mathematics (like toposes or programs ) then you can accept this sort of arguement, but be aware that you only know that there exists a constructive proof without actually knowing the proof it self. People that are constructivist for more 'philosophical' reasons tend to reject this kind of argument (at least I have heard some people rejecting this sort of argument). – Simon Henry Jan 3 '17 at 15:27

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.

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.