In what rigorous sense are Sperner's Lemma and the Brouwer Fixed Point Theorem equivalent?

I understand that one can give a proof of each of these propositions assuming the truth of the other. But this seems a bit squishy to me, since there is a trivial sense in which any two true theorems are equivalent (to any proof of Theorem A, prepend "Assume Theorem B", and vice versa; the objection "But the proof of Theorem A doesn't really use the assumption that Theorem B holds" seems more psychological than mathematical).

One might try to formalize the notion of equivalence by considering the lengths of proofs, saying "There is a derivation of Theorem A from Theorem B that is significantly shorter than any proof of Theorem A from scratch, and vice versa", but this too is squishy, in two distinct ways: the length of a proof depends on the formalization procedure one chooses, and "significantly shorter" is vague. Moreover, it's hard to imagine how one could work with this notion of equivalence, since the totality of all short proofs is going to be hard to get a handle on, for the usual reasons.

Can one find some sort of mathematical context (a topos, perhaps?) in which there is a rigorously defined (and not vacuously true) meaning of the equivalence between Sperner and Brouwer?

(For a recent article that discusses this equivalence and gives pointers to relevant literature, see "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" by Nyman and Su in the April 2013 issue of the American Mathematical Monthly, a version of which is available online at http://willamette.edu/~knyman/papers/Fan_Sperner.pdf .)

-
In this particular case a general topos would work to show that they are not equivalent. But in general, when discussing equivalence of statements $A$ and $B$, we have to do it in a context where not both of them are provable (or refutable), lest they are "lost in the background theory". The idea is to a fragment of mathematics that is just strong enough to express the statements. See François's answer, where he identifies the relevant weak logical setting for Spenne'r Lemma and Brouwer's fixed point theorem. –  Andrej Bauer May 22 '13 at 6:49

Sperner's lemma is not equivalent to Brouwer's Fixed Point Theorem. All that one can prove directly from Sperner's Lemma is the following weaker statement.

Approximate Fixed Point Theorem. Let $K$ be the standard $n$-dimensional simplex and let $f:K \to K$ be a continuous function. For every $\varepsilon \gt 0$ there is an $x \in K$ such that $|f(x) - x| \leq \varepsilon$.

A compactness argument is then needed to derive the existence of an actual fixed point for $f$.

The analysis is done in §IV.7 of Simpson's Subsystems of Second-Order Arithmetic and the conclusion is that the Brouwer Fixed Point Theorem is equivalent to the Weak König Lemma over the base system RCA0. On the other hand, since Sperner's Lemma is a finite combinatorial statement, it is provable in RCA0. The Approximate Fixed Point Theorem is also provable in RCA0 via Sperner's Lemma. The final compactness argument is however beyond the reach of RCA0.

-
For someone not into axioms, this can be the proof that they are practically "equivalent" - only one more line (compactness) is needed to derive Brouwer from Sperner. –  domotorp May 22 '13 at 8:19
François's answer is of course correct; however, it is precisely this example (Sperner's lemma vs. Brouwer's fixed point theorem) that has often made me wonder if there's an alternative to SOSOA that more closely matches our intuition about the equivalence between the two results. The "mathematician in the street" might be inclined to toss some amount of compactness into the background theory since it has the feel of a general logical principle. Somehow the "interesting" part of Sperner is the same as the "interesting" part of Brouwer, and it would be cool if we could formalize this intuition. –  Timothy Chow May 22 '13 at 14:22
Tim, isn't the Approximate Fixed Point Theorem exactly the "interesting part" of Brouwer's? (The Approximate Fixed Point Theorem is equivalent to Sperner's Lemma over some much weaker base systems but I don't think that's published anywhere.) –  François G. Dorais May 22 '13 at 15:13
François, your parenthetical comment is very close to what I was hoping for. My only remaining question is then whether some compactness principle can be adjoined to one of those "weaker base systems" to produce a rigorous formulation of "Sperner = Brouwer". –  Timothy Chow May 23 '13 at 14:39
I doubt it. These weaker systems try to capture complexity theory rather than computability theory, they are inherently finite in nature and so incorporating compactness doesn't make much sense. Maybe there is another way, but I don't know any. Compactness is pretty strong so other restrictions are likely to be lost in its shadow. –  François G. Dorais May 23 '13 at 16:20
Here is another perspective from theoretical computer science. Sperner's theorem represents the complexity class PPAD; This complexity class (described by Christos Papadimitriou) is represented also by finding approximate fix points and several important applications of the fixed-point theorem are known to be PPAD-complete, most famously computing Nash equilibrium of (even 2-players) games. Here is a nice introduction to PPAD by Paul Goldberg, that I found in the post "Brower, Sperner and PPAD$in this course site of Noam Nisan. - add comment The Brouwer fpp theorem has two components. One is hard-combinatorial, and the other one is soft-analytical (related to compactness). The equivalence in the given case means to neglect the soft part granted that the passage from the hard part to the soft one is simple, preferably trivial. Actually, the standard connection between Sperner lemma and the Brouwer fpp is not as smooth as it can be. The issue is the choice of the so to speak two stones on each shore--the combinatorial and the analytical--where one can jump easily from one to another. Let's keep in mind the Sperner lemma used in KKM proof as it appears in Kuratowski's Introduction to the set theory and topology. The easy jump (just a tiny step) from the Sperner lemma to the analysis shore is the theorem about an$n-1$-sphere not being a retract of the respective$n$-ball. Of course there is one more step to get to the actual fpp but--modulo a geometric argument (actually a bit annoying)--it is easily acceptable. Summary: talk about a so to speak equivalence of Sperner lemma and non-retractability. (Only then, in the second breath, you may mention fpp). - add comment The theoretical Computer Science perspective may be useful here. At least, TCS has developed a rigorous and precise sense in which what I'll call "discrete Brouwer" (François' "Approximate Fixed Point Theorem") and Sperner's Lemma are equivalent; and I think it captures the intuition you are seeking in your question. In TCS, we are often interested in the problem you state: understanding when and how$A$is equivalent to$B$while avoiding the issue that all true statements imply each other. The programme is to use reductions to transform one problem into the other, and vice versa. This works on two levels: Algorithmically and logically. Algorithmically, if we can transform an instance of problem$A$into an instance of problem$B$, such that a solution to$B$gives back a solution to the original$A$, then we say that$A$reduces to$B$. If we can also reduce$B$to$A$, then the problems are equivalent. Logically, we can interpret the existence of a correct algorithm for$B$as giving a proof of some theorem (e.g. Brouwer) relating to$B$, and if$A$reduces to$B$, then this immediately implies a proof of a theorem about$A$. (This is Curry-Howard.) When$A$and$B$can be reduced to each other, then a proof of either's associated theorem implies a proof of the other's. Sperner and Brouwer give a beautiful example, which I'll try to sketch as best I can. First, let me define two algorithmic problems. (Discrete BROUWER) Given$\epsilon$and a function$f$that takes coordinates in$[0,1]^2$and produces coordinates in$[0,1]^2$, output some coordinate$(x,y)$such that$\|(x,y) - f(x,y)\| \leq \epsilon$. (SPERNER) Given an integer$n$and a function$f$that takes integers$(a,b)$such that$a+b = n$(that is, points on a triangulation) and produces a color {red,green,blue} and satisfying the usual Sperner coloring constraints, output a set of three points$((a_1,b_1),(a_2,b_2),(a_3,b_3))$that (a) is a triangle and (b) is colored with three different colors. Now, (for this post,) let us just define the discrete Brouwer's Theorem and Sperner's Lemma to be the statements that a solution to the respective problems always exists, for any input. Now, the problems BROUWER and SPERNER are equivalent in a very precise and rigorous sense: We can reduce each to the other. This means that, given the input to SPERNER, we can show how to transform it into an input to BROUWER. We then can run any algorithm for BROUWER and obtain some output; we then show how to convert this output into an output for the original SPERNER problem. And what we can prove is that, if the algorithm we used for BROUWER is correct, then this algorithm for SPERNER will be correct. Note that we can prove this fact regardless of whether a correct algorithm for Brouwer actually exists or not! Similarly, we can reduce BROUWER to SPERNER by showing how to solve the first by a call to an algorithm for the second. OK - so far, we have not proven either discrete Brouwer's Theorem or Sperner's Lemma. But now we are in a wonderful spot: If we can only exhibit an algorithm for the SPERNER problem and prove that it is correct, then we will have done both: (1) proven Sperner's Lemma (such a triangle always exists, because we have proven that our algorithm always finds one!); and (2) proven a discrete Brouwer's Theorem (since there is a correct algorithm for SPERNER, we know how to construct an algorithm for BROUWER that always finds an$\epsilon\$-fixpoint; so such a fixpoint must always exist).