La informática teórica perspectiva puede ser útil aquí. Al menos, TCS ha desarrollado un riguroso y preciso sentido en que lo voy a llamar "discretos Brouwer" (François, "Aproximado Teorema de Punto Fijo") y Sperner del Lexema son equivalentes, y creo que se capta la intuición de que usted está buscando en su pregunta. En TCS, a menudo estamos interesados en el problema del estado: la comprensión de cuándo y cómo $A$ es equivalente a $B$, evitando el problema de que todos los enunciados verdaderos implican el uno al otro.
El programa es el uso de reducciones para transformar un problema en el otro, y viceversa. Esto funciona en dos niveles: a través de Algoritmos y lógica. A través de algoritmos, si podemos transformar una instancia del problema de $A$ en una instancia del problema de $B$, de tal manera que una solución a $B$ da una solución a la original $A$, entonces decimos que la $A$ reduce a $B$. Si también se pueden reducir los $B$ a $A$, entonces los problemas son equivalentes.
Lógicamente, se puede interpretar la existencia de un algoritmo correcto para $B$ como dar una prueba de algún teorema (por ejemplo, Brouwer) relativos a $B$, y si $A$ reduce a $B$, entonces esto implica inmediatamente una prueba de un teorema acerca de $A$. (Esto es de Curry-Howard.) Al $A$ e $B$ puede ser reducido a la otra, entonces una prueba de cualquiera de los asociados teorema implica una prueba de la de los demás. Sperner y Brouwer dar un hermoso ejemplo, que voy a tratar de esbozar lo mejor que pueda.
En primer lugar, permítanme definir dos algorítmica de problemas.
(Discrete BROUWER) Determinado $\epsilon$ y una función de $f$ que toma las coordenadas en $[0,1]^2$ y produce coordenadas en $[0,1]^2$, la salida de algunos coordinar $(x,y)$ tal que $\|(x,y) - f(x,y)\| \leq \epsilon$.
(SPERNER) Dado un entero $n$ y una función de $f$ que lleva enteros $(a,b)$ tal que $a+b = n$ (es decir, los puntos en una triangulación) y produce un color {rojo,verde,azul} y la satisfacción de las habituales de Sperner colorear limitaciones, la salida de un conjunto de tres puntos de $((a_1,b_1),(a_2,b_2),(a_3,b_3))$ (a) es un triángulo y (b) es de color con tres colores diferentes.
Ahora, (de este post) que nos acaba de definir el discreta del Teorema de Brouwer y Sperner del Lema a ser las declaraciones que una solución a los respectivos problemas siempre existe, para cualquier entrada.
Ahora, los problemas de BROUWER y SPERNER son equivalentes en un muy preciso y riguroso sentido: podemos reducir el uno al otro. Esto significa que, dada la entrada a SPERNER, podemos mostrar cómo transformarlo en una entrada de BROUWER. A continuación, puede ejecutar cualquier algoritmo de BROUWER y obtener algunos resultados, que a continuación se muestra cómo convertir este resultado en una salida para el original SPERNER problema. Y lo que podemos demostrar es que, si el algoritmo que utiliza para la BROUWER es correcta, entonces este algoritmo para SPERNER será correcta. Tenga en cuenta que nosotros podemos demostrar este hecho, independientemente de si un algoritmo correcto para Brouwer en realidad existe o no! Del mismo modo, podemos reducir BROUWER a SPERNER mostrando cómo resolver la primera por una llamada a un algoritmo para el segundo.
OK - hasta ahora, no hemos probado, ya sea discreta del Teorema de Brouwer o Sperner del Lexema. Pero ahora estamos en un lugar maravilloso: Si sólo se puede exhibir un algoritmo para la SPERNER problema y demostrar que es correcta, entonces habremos hecho las dos cosas: (1) demostrar Sperner del Lema (por ejemplo un triángulo siempre existe, porque hemos demostrado que nuestro algoritmo siempre encuentra uno!); y (2) demostrar una discreta del Teorema de Brouwer (ya que no hay un algoritmo correcto para SPERNER, sabemos cómo construir un algoritmo para BROUWER, que siempre encuentra una $\epsilon$-punto fijo; por tanto un punto fijo siempre debe existir).
Del mismo modo, si podemos demostrar que un algoritmo discretas de BROUWER (cuya corrección implica la discreta teorema de Brouwer), entonces nuestro reducción implica inmediatamente un algoritmo para la resolución de SPERNER y por lo tanto, Sperner del Lexema.
Por eso, cuando nos algorítmicamente reducir un problema para el otro, se construye una cadena de implicaciones: Cualquier algoritmo que siempre resuelve el problema que implica la existencia de un algoritmo para resolver el primer problema. En el caso de Brouwer/Sperner, esto nos permite mostrar que una solución para el primer problema con el que siempre existe.
Mi entendimiento es que el área de homotopy tipo de teoría (y tal vez otros campos relacionados) están interesados en el estudio de la estructura de tales cadenas de implicaciones y equivalencias, pero yo sé muy poco acerca de ella, así que voy a parar aquí. Espero que esto tiene sentido; quisiera saber si me puede aclarar nada!
P. S. Una más sutil/la cuestión es si realmente esto evita el problema de que todos los enunciados verdaderos implican el uno al otro. No creo que en un computabilidad sentido (?), pero no en la complejidad de un sentido: sólo podemos permitir que el polinomio de tiempo de las reducciones de entre los problemas. Ahora, si no hay manera de resolver cualquiera de BROUWER o SPERNER en el polinomio de tiempo, sin embargo, podemos reducir a los otros en el polinomio de tiempo, entonces, debe ser equivalente en algún sentido más fuerte: Nuestro reducción no sólo resolver el problema y dar algunos trivial de entrada (desde nuestro reducción sólo se ejecuta en el polinomio de tiempo, lo cual no es suficiente para resolver el problema). Así que esta caja negra algoritmo que estamos llamando para resolver el problema debe de estar haciendo el "trabajo pesado" en algún sentido. (Otra cosa es que no sabemos con certeza si BROUWER o SPERNER puede ser resuelto en el polinomio de tiempo, pero principalmente nos conjetura de que ellos no pueden.)
