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).

Similarly, if we can exhibit an algorithm for discrete BROUWER (whose correctness implies the discrete Brouwer theorem), then our reduction above immediately implies an algorithm for solving SPERNER and therefore, Sperner's Lemma.

So, when we algorithmically reduce one problem to the other, we construct a chain of implication: Any algorithm that always solves the other problem implies an algorithm for always solving the first problem. In the case of Brouwer/Sperner, this allows us to show that a solution to the first problem always exists.

My understanding is that the area of *homotopy type theory* (and perhaps other related fields) are interested in studying the structure of such chains of implications and equivalences, but I know very little about it, so I will stop here. I hope this makes sense; let me know if I can clarify anything!

P.S. A more subtle/further question is whether this really avoids the issue that all true statements imply each other. I don't think it does in a computability sense (?), but it does in a complexity sense: We can only allow *polynomial-time* reductions between problems. Now, if there is no way to solve either BROUWER or SPERNER in polynomial time, yet we can reduce either to the other in polynomial time, then they must be equivalent in some stronger sense: Our reduction cannot just solve the problem and give some trivial input (since our reduction only runs in polynomial time, which is not enough to solve the problem). So this black-box algorithm we are calling to solve the other problem must be doing the "heavy lifting" in some sense. (Another catch is that we don't know for sure whether BROUWER or SPERNER can be solved in polynomial time, but we mainly conjecture that they cannot.)

notequivalent. 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 toexpressthe statements. See François's answer, where he identifies the relevant weak logical setting for Spenne'r Lemma and Brouwer's fixed point theorem. $\endgroup$ – Andrej Bauer May 22 '13 at 6:49