He leído que el Teorema de Cantor se puede demostrar en teoría de tipos (aunque no he encontrado/entendido tal demostración). Sin embargo, tengo entendido que la teoría de tipos puede ser impredicativa y, como tal, eso no me ayudaría mucho.
Tengo la impresión de que la demostración que he visto en Wikipedia del Teorema de Cantor es impredicativa. Si no lo es, acláreme, ya que es evidente que no la entiendo. Si lo es, entonces mi pregunta sigue en pie.
Saludos.
EDIT: Acabo de notar que el OP nunca dijo que ¡de los teoremas de Cantor bajo escrutinio! A continuación asumo que se trata de la incontabilidad de los reales.
Tl;dr: La demostración del teorema de Cantor es completamente predicativa.
La predicatividad es, por supuesto, una noción algo informal, pero en última instancia se trata de los peligros percibidos de auto-referencia . La autorreferencia se interpreta aquí de forma amplia: una definición de un objeto $\alpha$ es impredicativo si implica cuantificar sobre un conjunto que contiene $\alpha$ . Por ejemplo, el ejemplo habitual es que la existencia de límites mínimos superiores de conjuntos acotados no vacíos de reales es impredicativa: esto se debe a que la definición de " $\alpha$ es el l.u.b. de $A$ " es
$\alpha$ es un límite superior de $A$ y para todos los límites superiores $\beta$ de $A$ tenemos $\alpha\le\beta$ .
La cuantificación en negrita sobre los límites superiores es una cuantificación sobre un conjunto que contiene $\alpha$ , por lo que es impredicativo.
Así que su pregunta equivale a: ¿qué tipo de cuantificación se utiliza en el argumento de Cantor?
Tomemos la siguiente versión del teorema de Cantor para simplificar:
Si $F$ es una función de $\mathbb{N}$ al conjunto de secuencias infinitas de $0$ s y $1$ s, entonces hay alguna secuencia infinita de $0$ s y $1$ s no en el rango de $F$ .
(Obsérvese que las secuencias infinitas de $0$ s y $1$ no se corresponden exactamente con los números reales en $[0,1]$ : esto se debe a que un único real no tiene por qué tener una única expansión binaria. Este es un punto menor, pero significa que las cosas son un poco más fáciles de visualizar cuando se trabaja con secuencias en lugar de con reales, al menos al principio).
La prueba es la siguiente:
Dejemos que $g_F$ sea la secuencia ${\color{red}{\mbox{defined by}}}$ : el $n$ a la vez de $g_F$ es $0$ si el $n$ a la vez de $F(n)$ es $1$ y el $n$ a de $g_F$ es $1$ si el $n$ a de $F(n)$ es $0$ . ${\color{red}{\mbox{Then}}}$ $g_F\not\in ran(F)$ ya que para cada $n$ tenemos $F(n)(n)\not=g_F(n)$ .
Esta prueba tiene dos partes, que he resaltado en rojo. En orden de mayor relevancia, son:
El verificación que $g_F\not\in ran(F)$ . Esto es lo más sencillo que se puede hacer, y de hecho es incluso intuitivamente válido; pero ni siquiera necesitamos observar esto, ya que la lógica predicativa está bien con el medio excluido ...
... es el construcción de $g_F$ que nos importa. Pero aquí no hay nada impredicativo: definir $g_F$ no cuantificamos sobre todas las funciones, sino que sólo tenemos que mirar el funcional específico $F$ y su alcance $ran(F)$ . En ningún momento de la definición de $g_F$ cuantificamos sobre cualquier conjunto que contenga $g_F$ .
(Por cierto, la definición de la función $\mathcal{G}$ enviando $F$ a $g_F$ es también totalmente predicativo: mientras que implica cuantificar sobre todos los mapas de $\mathbb{N}$ a infinitas secuencias binarias, él mismo no es un mapa de este tipo).
La prueba de Cantor de que no existe una biyección entre un conjunto $X$ y su conjunto de poderes $\Bbb{P}(X)$ es así: si $f : X \to \Bbb{P}(X)$ es una función cualquiera, entonces $\{x \in X \mid x \notin f(x)\}$ es miembro de $\Bbb{P}(X)$ que no está en el rango de $f$ . Este es un argumento constructivo: usted me da una $f$ y te doy algo que no está en su rango. Esto no requiere ningún razonamiento impredicativo.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
