He aquí una explicación de por qué la elección contable no es problemática en las matemáticas constructivas.
Para esta discusión es útil formular el axioma de elección de la siguiente manera:
$(\forall x \in X . \exists y \in Y . R(x,y)) \implies \exists f \in Y^X . \forall x \in X . R(x,f(x))$
Esto dice que una relación total $R \subseteq X \times Y$ contiene una función. La formulación habitual del axioma de elección es equivalente a la anterior. En efecto, si $(S_i)_{i \in I}$ es una familia de conjuntos no vacíos tomamos $X = I$ , $Y = \bigcup_i S_i$ y $R(i,x) \iff x \in S_i$ para obtener una función de elección $f : I \to \bigcup_i S_i$ . A la inversa, dada una relación total $R \subseteq X \times Y$ considera la familia $(S_x)_{x \in X}$ donde $S_x = \lbrace y \in Y \mid R(x,y)\rbrace$ y aplicar el axioma de elección habitual.
Una forma de ver los conjuntos en matemáticas constructivas es imaginar que son colecciones junto con dado igualdad, es decir, una especie de "preajustes" dotados de relaciones de equivalencia. En realidad, esto tiene sentido si pensamos en cómo implementamos los conjuntos abstractos en los ordenadores: cada elemento del conjunto abstracto está representado por una secuencia finita de bits, donde cada elemento puede tener muchas representaciones válidas (y esto es inevitable en general). Pondré dos ejemplos concretos:
-
un número natural $n \in \mathbb{N}$ se representa en el sistema binario habitual, y permitamos ceros a la izquierda, de modo que $42$ está representado por $101010$ así como $0101010$ , $00101010$ etc.
-
un real (computable) $x \in \mathbb{R}$ se representa mediante código máquina (una cadena binaria) que calcula aproximaciones arbitrariamente buenas de $x$ . En concreto, un fragmento de código $p$ representa $x$ cuando $p(n)$ produce un número racional distinto de $x$ como máximo $2^{-n}$ . Por supuesto, sólo representamos computable reales de esta manera, y cada real computable tiene muchas representaciones diferentes.
Déjame escribir $\mathbb{R}$ para el conjunto de los reales computables, porque esos son los únicos reales relevantes para esta discusión.
Una diferencia esencial entre el primer ejemplo y el segundo es que existe una elección canónica computable de representantes para los elementos de $\mathbb{N}$ (cortar los ceros iniciales), mientras que no existe una opción canónica para $\mathbb{R}$ ya que si la tuviéramos podríamos decidir la igualdad de los reales computables y, en consecuencia, resolver el problema de Halting.
Según la interpretación constructiva de la lógica, un enunciado de la forma
$\forall x \in X . \exists y \in Y . R(x, y)$
se cumple si existe un programa $p$ que toma como entrada un representante de $x \in X$ y produce un representante para $y \in Y$ junto con un testigo de $R(x,y)$ . Crucial, $p$ no tiene por qué respetar la igualdad de $X$ . Por ejemplo,
$\forall x \in \mathbb{R} . \exists n \in \mathbb{N} . x < n$
se acepta porque podemos escribir un programa que tome como entrada un representante de $x$ a saber, un programa $p$ como se ha descrito anteriormente, y da como salida un número natural mayor que $x$ por ejemplo $round(p(0)) + 1000$ . Sin embargo, el número $n$ dependerá necesariamente de $p$ y no hay forma de hacer que dependa sólo de $x$ (computablemente).
Veamos de nuevo el axioma de la elección:
$(\forall x \in X . \exists y \in Y . R(x,y)) \implies \exists f \in Y^X . \forall x \in X . R(x,f(x))$
Aceptamos esto si existe un programa que toma como entrada un $p$ presenciar la totalidad de $R$ y emite un representante de una función de elección $f$ así como un testigo de que $\forall x \in X. R(x, f(x))$ retenciones. Esto es probemático porque $p$ no tiene por qué respetar la igualdad de $X$ mientras que un representante de $f$ debe respetar la igualdad. No está claro de dónde podríamos sacarla, y con ejemplos concretos podemos demostrar que no la hay. Ya falla lo siguiente:
$(\forall x \in \mathbb{R} . \exists n \in \mathbb{N} . x < n) \implies \exists f \in \mathbb{N}^\mathbb{R} . \forall x \in \mathbb{R} . x < f(x)$ .
En efecto, todo mapa computable $f : \mathbb{R} \to \mathbb{N}$ es constante (porque uno no constante nos permitiría escribir un oráculo de Halting).
Sin embargo, si nos especializamos en elección contable
$(\forall n \in \mathbb{N} . \exists y \in Y . R(n,y)) \implies \exists f \in Y^\mathbb{N} . \forall n \in \mathbb{N} . R(n,f(n))$
entonces puede producir el programa deseado. Dado $p$ que atestigua la totalidad de $R$ defina el siguiente programa $q$ que representa una función de elección: $q$ toma como entrada una representación binaria de un número natural $n$ posiblemente con ceros a la izquierda, elimina los ceros a la izquierda y aplica $p$ . Ahora bien, aunque $p$ no respetaba la igualdad de los números naturales, $q$ lo hace porque aplica $p$ a representantes canónicamente elegidos.
En general, aceptaremos la elección para aquellos conjuntos $X$ que tienen representantes canónicos computables para sus elementos. Vale, esto ha sido un poco rápido, pero espero haber captado la idea.
Permítanme terminar con un comentario general. La mayoría de los matemáticos en activo no pueden imaginar universos matemáticos alternativos porque han sido formados a conciencia para pensar en un único universo matemático, a saber, la teoría clásica de conjuntos. Como resultado, su intuición matemática ha sido víctima de la teoría clásica de conjuntos. El primer paso para entender por qué alguien puede poner en duda un principio matemático que le parece evidentemente cierto es ampliar su horizonte estudiando otros universos matemáticos. A menor escala, esto es bastante obvio: no se puede dar sentido a la geometría no euclidiana interpretando los puntos y las rectas como los del plano euclidiano. Del mismo modo, no se puede entender en qué puede fallar el axioma de elección interpretándolo en la teoría clásica de conjuntos. Usted debe cambiar a un universo diferente, aunque creas que no hay ninguno... Por supuesto, esto requiere cierto esfuerzo, pero es una auténtica revelación.