Es más fácil pensar sobre el Teorema del Valor Intermedio, que es equivalente a la Brouwer de Punto Fijo Teorema de la unidad de intervalo.
El principal problema es que la dicotomía para (de Cauchy) números reales no es constructiva válido: dados dos números reales $\alpha,\beta$, no existe ningún algoritmo para decidir si $\alpha \leq \beta$ o $\alpha \geq \beta$. Este principio es equivalente al Menor de los Limitados Principio de la Omnisciencia (LLPO) y no la naturaleza constructiva es ilustrado por un clásico Brouwerian contraejemplo:
Definir la secuencia de los racionales $(a_n)_{n=0}^\infty$ por $a_n = (-2)^{-k}$ si $k \leq n$ y la primera aparición de la secuencia de $736667843909774044615061702878$ en $\pi$ comienza $k$-dígitos después del punto decimal; si no hay tal $k \leq n$,, a continuación,$a_n = 0$. Esta es una bien definida la secuencia de Cauchy (con una tasa de convergencia) de modo que el límite de $\alpha = \lim_{n\to\infty} a_n$ es una buena definición de número real. Es $\alpha \geq 0$ o $\alpha \leq 0$?
Si la secuencia ocurre en $\pi$, entonces eventualmente se sabe que $\alpha > 0$ o $\alpha < 0$, y responder en consecuencia. Sin embargo, si la secuencia no se producen en $\pi$, a pesar de que ambas respuestas son válidas en este caso, ni la respuesta puede ser comprobada la correcta sin una cantidad infinita de información acerca de los dígitos de $\pi$ (que en el ejemplo se asume que no se conoce en este momento).
Volviendo a el Teorema del Valor Intermedio, considere la función lineal a trozos $f:[-1,1]\to[-1,1]$ que interpola los puntos de $(-1,1),(-1/2,\alpha),(1/2,\alpha),(1,1)$. El Teorema del Valor Intermedio nos dice que hay un número $r \in [-1,1]$ tal que $f(r) = 0$. Tenga en cuenta que $\alpha \geq 0$ fib $r \leq 1/2$ e $\alpha \leq 0$ fib $r \geq -1/2$. Ahora, la determinación de si $r \leq 1/2$ o $r \geq -1/2$ es fácil: calcular $r$ de exactitud suficiente para saber que se encuentra dentro de un intervalo abierto con una longitud de $1$ y racional de los extremos; que el intervalo no puede contener tanto $1/2$ e $-1/2$ y eso es suficiente para saber si $r \leq 1/2$ o $r \geq -1/2$.
Así, a partir de lo anterior, podemos ver que si tuviéramos una constructivo prueba del Teorema del Valor Intermedio, tendríamos también una constructivo prueba de la dicotomía. Ya que no hay constructivo prueba de la dicotomía, no puede ser constructiva de la prueba del Teorema del Valor Intermedio y, por la misma razón, no puede ser constructiva de la prueba de la Brouwer de Punto Fijo Teorema.
El Brouwerian contraejemplo anterior podría no ser convincente ya que nosotros (al menos creo) que sabemos que no trivial de información acerca de $\pi$. Por supuesto, el número específico $\pi$ es irrelevante; es simplemente la elección tradicional para Brouwerian contraejemplos. Aquí está un ejemplo similar que se basa en la existencia de inseparables pares de computably conjuntos enumerables.
Decir una secuencia $(q_n)_{n=0}^\infty$ de los números racionales es rápidamente de Cauchy si $|q_n - q_m| \leq 1/2^N$ para todos los $m,n > N$. (Esta es una de las típicas definiciones de Cauchy de números reales.) Supongamos que tenemos un algoritmo de $M$ a decidir si el límite de una rápida secuencia de Cauchy es no negativa o el valor no positivo.
Ahora, dado un índice $e$, definir $(a_{e,n})_{n=0}^\infty$ a $a_{e,n} = (-1)^m/2^s$ si $e$-ésima máquina de Turing se detiene exactamente $s \leq n$ pasos y salidas de $m$, y establecer $a_{e,n} = 0$ si $e$-ésima máquina de Turing no se detiene en $n$ o menos pasos. Cada una de estas secuencias es efectivamente computable rápidamente la secuencia de Cauchy. Si puedo aplicar mi propuesta de $M$ a de la $e$-ésima secuencia, puedo obtener un total computable en función de $s:\mathbb N \to \{0,1\}$ que si $s(e) = 0$ entonces $\lim_{n\to\infty} a_{e,n} \leq 0$ e si $s(e) = 1$ entonces $\lim_{n \to \infty} a_{e,n} \geq 0$.
Tenga en cuenta que $\lim_{n\to\infty} a_{e,n} > 0$ fib $e$ pertenece al conjunto $A$ de todos los índices para las máquinas de Turing que detener, incluso con la salida, y $\lim_{n \to\infty} a_{e,n} \lt 0$ fib $e$ pertenece al conjunto $B$ de todos los índices para las máquinas de Turing que detener con impar de salida. El par $A,B$ es uno de los estándar de ejemplos prototípicos de una pareja inseparable, por lo que no es computable set $C$ tal que $A \subseteq C$ e $B \cap C = \varnothing$. Sin embargo, el conjunto $C = \{e : s(e) = 1\}$ hace exactamente eso!
