¿Podemos rechazar la elección finita?

Question

Cuando la gente trabaja con conjuntos infinitos, hay a quien (con razón) no le gusta utilizar el axioma de elección. Esto es defendible, ya que el axioma es independiente de los otros axiomas de la teoría de conjuntos ZF.

Cuando la gente trabaja con conjuntos finitos, todavía hay algunas personas a las que no les gusta utilizar el "axioma finito de elección", es decir, no les gusta escoger un elemento distinguido de un conjunto, o un isomorfismo distinguido entre un conjunto con $n$ elementos y $\{0, 1, \ldots, n-1\}$ (sin algún algoritmo que lo elija, claro). Ésta sigue siendo una posición estéticamente defendible, ya que a menudo las pruebas que proceden de esa manera no dan tanta información como las pruebas que no utilizan la elección finita. Pero la teoría de conjuntos ZF nos permite hacer esto para conjuntos finitos.

¿Existe un marco general en el que podamos desautorizar, si así lo deseamos, el método del elemento distinguido? Tengo la corazonada de que el hecho de que, incluso para un espacio vectorial de dimensión finita $V$ , $V$ y $V^\ast$ no son naturalmente isomorfas es el primer paso hacia la "respuesta correcta", pero no veo realmente por dónde seguir a partir de ahí.

(Para que quede claro, como señala Ilya, me estoy refiriendo principalmente a la teoría de conjuntos; sé que/cómo la teoría de categorías nos habla de la no naturalidad del isomorfismo del espacio vectorial dual, en particular. Mi pregunta es: ¿hay algo que subsuma esto o que lo paralelice para construcciones más combinatorias)?

Answer 1

Obsérvese que, en un sentido puntilloso, ZFC no le permite hacer una elección finita ; en el mejor de los casos, simplemente te dice si hay opciones disponibles para elegir. En cambio, es el lógica que utiliza razonar con ZFC que le permita tomar decisiones.

En su lugar, podría cambiar su punto de vista sobre lo que significa un argumento de este tipo: los argumentos que implican hacer una elección arbitraria son, en cambio, funciones de definición, o implican elementos generalizados o razonamiento mediante teoría del tipo dependiente .

Por ejemplo, considere la siguiente prueba de que todo espacio vectorial $V$ tiene una base:

Elija un buen orden de $V$ . Sea $B$ es el conjunto de todos los elementos de $V$ que no puede escribirse como una combinación lineal de elementos más pequeños. .... Por lo tanto $B$ es una base.

Este argumento puede interpretarse, en cambio, como la definición de una función a partir del conjunto de bien-ordenaciones de $V$ al conjunto de bases de $V$ .

A veces, este punto de vista es tan natural que cambia incluso la forma de pensar sobre el tema; por ejemplo, al hacer álgebra lineal de dimensión finita, cuando veo las palabras "base de un espacio vectorial $V$ ", suelo leerlo como "isomorfismo $\mathbb{R}^n \to V$ ". (hay que admitir que hice este cambio de POV antes de aprender cualquier otra cosa que he descrito anteriormente)

Answer 2

Existe la teoría de los cuasiconjuntos en la que los elementos son indistinguibles. Véase

http://en.wikipedia.org/wiki/Quasi-set_theory

Answer 3

Mira el papel Computación sin elección y simetría de Benjamin Rossman. Parece que su intuición hacia la "respuesta correcta" era correcto. El resultado principal del artículo trata de los espacios vectoriales duales.

Del resumen:

... mostramos que existe un problema de función computable en tiempo polinomial isomorfismo-invariante computable en espacios vectoriales finitos ("dado un espacio vectorial vectorial finito V , salida del conjunto de hiperplanos en V") que no es computable por ningún programa CPT+C.