Como dice Kaveh en un comentario, la cuestión no va a ser la elección. Normalmente, cuando examinamos lo que falla cuando intentamos formalizar una prueba clásica "no constructiva" en un sistema constructivo, el problema que descubrimos es que la prueba ya es no constructiva antes de que se invoque el axioma de elección.
En este caso, la cuestión es que todo el concepto de particiones y clases de equivalencia, que subyace a la prueba habitual de la paradoja de Banach-Tarski, se comporta de forma muy diferente en los sistemas constructivos.
Consideremos el caso más sencillo de un conjunto de Vitali en la recta real. Dos reales se definen como equivalentes si su diferencia es racional. Esa es una definición perfectamente buena en los sistemas constructivos, pero es fácil pasar por alto el hecho de que implica un cuantificador universal implícito sobre los racionales (o la capacidad de decir si un real arbitrario es racional). En este caso particular, los métodos estándar muestran que no será posible demostrar constructivamente[1] que "para todos los reales x y y , ya sea x equivale a y o x no es equivalente a y ". Así, ya no es posible demostrar que dos clases de equivalencia [x] y [y] son disjuntos o idénticos, es decir, es imposible demostrar que las clases de equivalencia forman una partición de la recta real. Pero este hecho es crucial para la prueba habitual de que el conjunto de Vitali no es medible. El mismo tipo de problema es fácil de detectar en la prueba habitual de la paradoja de Banach-Tarski.
- Más concretamente, esto será imposible en cualquiera de los sistemas formalizados habituales para la matemática constructiva, incluida la teoría de tipos intuicionista.
