32
$\begingroup$

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

$\endgroup$
7
  • 7
    $\begingroup$ 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. $\endgroup$ Apr 13, 2015 at 16:12
  • 2
    $\begingroup$ Related: mathoverflow.net/questions/105883/… $\endgroup$ Apr 13, 2015 at 16:12
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 13, 2015 at 18:48
  • 2
    $\begingroup$ So: Would L.E.J. Brouwer himself accept the proof? $\endgroup$ Apr 13, 2015 at 20:14
  • 2
    $\begingroup$ @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 [...]" $\endgroup$
    – coudy
    Apr 13, 2015 at 20:56

4 Answers 4

21
$\begingroup$

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

$\endgroup$
6
  • 2
    $\begingroup$ Was Baigger the first? I thought it was Orevkov in 1963? $\endgroup$ Apr 14, 2015 at 0:20
  • $\begingroup$ Yes, Orevkov was first. Baigger's work is built on Orevkov's construction and filling in some more details. $\endgroup$
    – Arno
    Apr 14, 2015 at 0:28
  • 1
    $\begingroup$ "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. $\endgroup$
    – TonyK
    Apr 14, 2015 at 15:54
  • $\begingroup$ @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). $\endgroup$
    – Arno
    Apr 14, 2015 at 17:32
  • 1
    $\begingroup$ @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. $\endgroup$
    – Arno
    Apr 14, 2015 at 18:38
28
$\begingroup$

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!

$\endgroup$
10
  • 1
    $\begingroup$ 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. $\endgroup$
    – Guntram
    Apr 13, 2015 at 16:22
  • 1
    $\begingroup$ @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! $\endgroup$ Apr 13, 2015 at 16:31
  • 2
    $\begingroup$ Now I'm not sure if you got that I was just joking or not. :| $\endgroup$
    – Asaf Karagila
    Apr 13, 2015 at 18:09
  • 6
    $\begingroup$ @AsafKaragila: I was just joking or not Can you prove this constructively? $\endgroup$ Apr 13, 2015 at 21:33
  • 9
    $\begingroup$ @Emil: It wasn't a constructive comment. :-) $\endgroup$
    – Asaf Karagila
    Apr 14, 2015 at 15:12
11
$\begingroup$

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)

$\endgroup$
7
  • 2
    $\begingroup$ 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. $\endgroup$ Apr 14, 2015 at 10:25
  • $\begingroup$ Ok, good to know. $\endgroup$ Apr 14, 2015 at 10:48
  • $\begingroup$ $\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. $\endgroup$ Nov 21, 2016 at 10:35
  • $\begingroup$ @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) $\endgroup$ Jan 3, 2017 at 15:20
  • $\begingroup$ 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). $\endgroup$ Jan 3, 2017 at 15:27
10
$\begingroup$

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).
$\endgroup$
3
  • $\begingroup$ What does $d(G_f, D) = 0$ mean? Thanks $\endgroup$
    – wlad
    Oct 3, 2019 at 14:10
  • $\begingroup$ @jkabrg : 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$. $\endgroup$ Oct 7, 2019 at 15:52
  • $\begingroup$ $D$ is simply the diagonal, and very inhabited ... you probably refer to the intersection of $G_f$ and $D$... Anyway, there is a lot of compactness going on indeed, also for instance to classically prove the equivalence with the usual BFPT. $\endgroup$ Oct 7, 2019 at 16:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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