Sperner's lemma and Tucker's lemma

In their article "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" (American Mathematical Monthly, April 2013), Nyman and Su write "[W]e are unaware of a direct proof that Tucker's lemma implies Sperner's lemma".

Could there be a mathematical obstruction to finding a derivation of Sperner's lemma from Tucker's lemma? E.g., could there be a mathematical context (perhaps some fragment of ZF as a background theory), and in that context two propositions S and T that are recognizable as versions of Sperner's lemma and Tucker's lemma, such that T is true but S is false? Or a computational context in which finding "Sperner's maguffin" (a fully labeled n-simplex) is demonstrably harder than finding "Tucker's maguffin" (a complementary edge)?

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

• Since these are results in finite combinatorics, the right context would be the theories discussed by Steve Cook and Phuong Nguyen in their book Logical Foundations of Proof Complexity. – François G. Dorais May 22 '13 at 20:57
• Please can we clarify, for this and the other question, what the statement of Sperner's Lemma is that is under discussion. Is the Wikipedia article clear enough? en.wikipedia.org/wiki/Sperner_lemma – Paul Taylor May 22 '13 at 21:34
• @Paul Taylor: See willamette.edu/~knyman/papers/Fan_Sperner.pdf for clear statements of Sperner's lemma and Tucker's lemma. – James Propp May 23 '13 at 14:13
• Have you seen this? arxiv.org/pdf/1305.6158.pdf – domotorp Jun 7 '13 at 14:29
• @domotorp: Thanks for pointing out this article! It was very relevant and interesting. – James Propp Jun 14 '13 at 16:51

Are you familiar with Christos Papadimitriou's paper "On the complexity of the parity argument and other inefficient proofs of existence"? I remember that he discusses Sperner's Lemma, but I don't recall whether Tucker is there too, and the version of the paper available at http://www.cs.berkeley.edu/~christos/papers/On%20the%20Complexity.pdf seems to be an unsearchable scan of a hard copy.

• Indeed, I don't think that Tucker has been studied in the context of PPAD complexity. It has been of some interest to me if Borsuk-Ulam is part of this class of path following proofs that Papadimitriou introduced. – Rabee Tourky Jun 7 '13 at 8:42
• Both Borsuk-Ulam and Tucker have been studied and shown to be PPAD-complete in the linked paper. I also believe that this shows that Sperner can be derived from Tucker, however, it would be nice to have a simple, straightforward reduction. – domotorp Jun 7 '13 at 10:10
• It turned out that Tucker was erroneously claimed to be in PPAD, it is PPA-complete, see [here][1]. This means that Tucker cannot be derived from Sperner, as these classes can be separated by an orcale, see [here][2]. As I wrote earlier, Sperner can be derived from Tucker. [1]: eccc.weizmann.ac.il/report/2015/163 [2]: doi.org/10.1016/0168-0072(96)83747-X – domotorp Jul 31 '17 at 7:59
• @domotorp this is old, but it seems your comment should be an answer. – François G. Dorais Jun 3 '20 at 17:29

Hello, I'm one of the authors of this paper: arXiv:1305.6158 (PDF)

The way I see it, "Sperner's Lemma", as usually stated, is actually the "wrong" version of the theorem. The versions in my paper, which use cubic and octahedral labels, are in some sense, the more "natural" statements, at least as far as analogy with Tucker goes. As we show, they are implied by Tucker's lemma quite naturally via geometric embeddings.

Topologically, the various Sperner-like theorems are obviously the same. But it seems that you need a topological theorem (e.g. Brouwer) to establish their equivalence. For the same reason, it seems like you need a topological theorem to prove Sperner from Tucker. At the very least, the geometric approach doesn't make any sense, because the antipodality condition doesn't have a good analogy.

As for your question about mathematical contexts where T is True and S is false, I can't think of any context where that would really make sense. Maybe T can be provable and S can be unprovable, e.g. if you restricted yourself to a context where Brouwer, etc. can't be proven (maybe by accepting only axioms that yield constructive proofs).