Todas las funciones reales continuas

Question

He oído que dentro del campo de intuitionistic matemáticas, todas las funciones reales continuas (es decir, no hay funciones discontinuas). Hay un buen libro donde puedo encontrar una prueba de este teorema?

Answer 1

Brouwer demostrado (para su propia satisfacción) que cada una de las funciones de $\mathbb{R}$ $\mathbb{R}$es continua. Los modernos sistemas constructivos rara vez son capaces de probar esto, pero son coherentes con ellos son incapaces de refutar. Estos sistema son (casi siempre) de conformidad con la clásica de las matemáticas en la que hay un montón de funciones discontinuas de$\mathbb{R}$$\mathbb{R}$. Un lugar donde usted puede encontrar algo acerca de esto es el clásico Variedades de Constructivo de las Matemáticas por los Puentes y Richman.

El mismo fenómeno se produce en la clásica computable análisis, por el camino. Cualquier computable en función de $f$ $\mathbb{R}$ $\mathbb{R}$que es bien definidos con respecto a la igualdad de reales (y por lo tanto es una función de $\mathbb{R}$ $\mathbb{R}$en el sentido normal de la palabra) es continua. En particular, la función característica de un singleton real nunca es computable. Este sería cubierto en cualquier computable análisis de texto, como el de Weihrauch.

Aquí es muy informal argumento de que tiene un grano de verdad. Debe aparecer ingenuamente correcto que si se puede "de manera constructiva" probar que algo es una función de$\mathbb{R}$$\mathbb{R}$, entonces se puede calcular la función. Por lo que el clásico hecho de que cada computable real de la función es continua sugiere que cualquier cosa que se puede demostrar de manera constructiva a ser una función real también será continua. Esto sugiere que no se puede demostrar de manera constructiva que cualquier clásico discontinua la función en realidad es una función. El grano de la verdad es que hay formas de hacer este argumento riguroso, tales como el método de la "realizabilidad".

Answer 2

Existe un topos de Grothendieck $\mathcal{E}$ en la que la declaración "cada una de las funciones de la Dedekind los números reales para los Dedekind números reales es continua" es cierto, en la lógica interna. Para ser un poco más precisos, en el topos $\mathcal{E}$, no es un objeto $R$ de Dedekind recortes de los números racionales, de tal manera que $$\forall f \in R^R . \, \forall \epsilon \in R . \, \forall x \in R . \, \epsilon > 0 \Rightarrow \exists \delta \in R . \, \forall x' \in R . \, \left| x - x' \right| < \delta \Rightarrow \left| f (x) - f (x') \right| < \epsilon$$ sostiene cuando se interpreta el uso de Kripke–Joyal semántica en $\mathcal{E}$. El topos $\mathcal{E}$ está construido de la siguiente manera: se toma una completa subcategoría $\mathbb{T}$ de la categoría de espacios topológicos $\textbf{Top}$ tal que

• $\mathbb{T}$ es pequeña,
• la línea real $\mathbb{R}$$\mathbb{T}$,
• para cada una de las $X \in \operatorname{ob} \mathbb{T}$ y cada subconjunto $U$$X$,$U \in \operatorname{ob} \mathbb{T}$, y
• $\mathbb{T}$ es cerrado bajo finito productos en $\textbf{Top}$;

y nos pusimos $\mathcal{E}$ a la categoría de poleas en $\mathbb{T}$ equipado con el sistema abierto de la inmersión de la topología. Entonces, uno puede mostrar que el objeto de la interna de Dedekind los números reales en el $\mathcal{E}$ es (isomorfo a) la representable gavilla $\mathbb{T}(-, \mathbb{R})$, y con más trabajo, uno encuentra que Brouwer "teorema" tiene en $\mathcal{E}$. Los detalles de la construcción y la prueba de validez se puede encontrar en [Poleas en la geometría y la lógica, Ch. VI, §9], aunque no he entendido en su totalidad.

Answer 3

Análisis Real: Un Enfoque Constructivo (2007) por Mark Bridger tendrá lo que quiere. En la Parte 157 de mi copia, en el Capítulo 4 Apéndice 1 es "No-Funciones Continuas", y la respuesta es ninguno, que puede ser construido en un determinado intervalo cerrado. Bajo el intuitionist lógica que se usa en este libro, el paso de las funciones y el como no puede ser definido en forma finita de intervalos cerrados, porque dicen que para una función de $f(x)$ con una discontinuidad en $0$, no se puede decir con precisión si $x<0$, $x=0$, o $x>0$ (como Carl Mummert señala en su comentario y respuesta). Sí, creo que eso es raro, pero es que algunos intuitionist lógica funciona.