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