Definición
La afirmación de que para cualquier familia de conjuntos no vacíos existe una función (función de elección) que selecciona un elemento de cada conjunto de la familia, asegurando la existencia de una selección simultánea incluso cuando no se dispone de una regla explícita.

Principio

Principio
Existencia frente a constructividad: la idea organizadora es que se puede afirmar la existencia de selecciones globales a nivel de conjuntos sin aportar un procedimiento constructivo o definible; permite pasar de la no vaciedad local a un representante global.

Demostración

Demostración
Tomar una familia indexada de conjuntos no vacíos de dos elementos {A_i : i ∈ I} con I infinito (posiblemente no numerable). El axioma garantiza una función f con f(i) ∈ A_i para todo i, de modo que el producto cartesiano ∏_{i∈I} A_i no es vacío aunque no exista un algoritmo uniforme que elija las coordenadas.

Aplicación incorrecta

Aplicación incorrecta
Tratarlo como un algoritmo constructivo: suponer que porque existe una función de elección se puede calcular o describir explícitamente para familias arbitrarias; o aplicarlo cuando alguno de los A_i es vacío.

Consecuencia

Consecuencia
Permite muchos resultados de existencia global: todo espacio vectorial tiene una base, el lema de Zorn y el teorema del buen orden son demostrables de forma equivalente, y ciertos productos de conjuntos no vacíos están garantizados no vacíos; también puede dar lugar a objetos no constructivos como conjuntos no medibles.

Inversión

Inversión
Negar el axioma produce modelos de la teoría de conjuntos en los que hay familias de conjuntos no vacíos sin función de elección global, provocando el fallo de algunas consecuencias clásicas de existencia (por ejemplo, espacios vectoriales sin base en esos modelos).

Límite

Límite
Se aplica en marcos de teoría de conjuntos del tipo Zermelo–Fraenkel como principio de existencia global; no proporciona definibilidad, computabilidad ni una regla canónica de elección y no se acepta en enfoques estrictamente constructivos o computables salvo que se formule con contenido constructivo adicional.

Tensión semántica

Tensión semántica
Tensión con las nociones constructivas o efectivas de elección: 'existencia de una función de elección' frente a 'existencia de una regla explícita y definible' — muchas afirmaciones equivalentes al axioma son intuitivas en el enfoque clásico pero problemáticas constructivamente.

Síntesis

Síntesis
El Axioma de Elección es un principio de existencia no constructivo que eleva la no vaciedad local a la existencia de un selector global para familias arbitrarias de conjuntos, permitiendo teoremas de existencia potentes y a la vez generando tensiones con las demandas de constructibilidad y definibilidad.