El axioma de no elección , también llamado axioma de elección única , axioma de elección de función o principio de comprensión de función, es un postulado de existencia de función. La diferencia con el axioma de elección es que en el antecedente ya se concede que la existencia de es única para cada uno .
El principio es importante, pero como axioma es de interés únicamente para teorías que tienen poca comprensión y capacidad para codificar funciones. Este es el caso, por ejemplo, de algunas teorías de conjuntos constructivos débiles [1] o de algunas aritméticas de orden superior .
El principio establece que para todos los dominios , si para cada elemento hay exactamente uno que cumple alguna propiedad, entonces existe una función que asigna cada elemento a un dominio tal que la propiedad dada se cumple en consecuencia. Formalmente, esto se puede expresar de la siguiente manera:
Cuando se toma como cualquier predicado, se trata de un esquema axioma . Se pueden considerar restricciones a la complejidad del predicado; por ejemplo, sólo se pueden permitir fórmulas sin cuantificadores.
El axioma puede denotarse . También puede adoptarse solo para funciones de naturales a naturales, luego llamado . Cuando los valores de la función son secuencias, se puede llamar . Planteada teóricamente, la existencia de un codominio particular puede ser parte de la formulación.
En marcos aritméticos , las funciones pueden considerarse secuencias de números. Si un cálculo de prueba incluye el principio del tercero excluido , entonces la noción de predicado de función también es liberal, y entonces el principio de comprensión de funciones concede la existencia de objetos de función incompatibles con la tesis constructiva de la Iglesia . Así que este triple de principios (medio excluido, comprensión de funciones y tesis de Church) es inconsistente. La adopción de las dos primeras caracteriza las teorías clásicas comunes de orden superior, la adopción de las dos últimas caracteriza las matemáticas estrictamente recursivas, mientras que no adoptar la comprensión de funciones también puede ser relevante en un estudio clásico de computabilidad . De hecho, el principio de comprensión de funciones contables no necesita ser validado en modelos computables de teorías aritméticas débiles, incluso clásicas.
En la teoría de conjuntos, las funciones se identifican con sus gráficas de funciones. Usando la notación constructora de conjuntos , se puede caracterizar una colección de pares,
El axioma de reemplazo en la teoría de conjuntos de Zermelo-Fraenkel implica que en realidad se trata de un conjunto y una función en el sentido anterior. La elección única es, por tanto, un teorema. Nótese que no adopta el axioma de elección.
En la teoría intuicionista de conjuntos de Zermelo-Fraenkel y en algunas teorías más débiles, la elección única también es derivable. Como en el caso de las teorías de la aritmética, esto significa que ciertos axiomas constructivos son estrictamente constructivos (anticlásicos) en esas teorías.
El axioma también puede desempeñar un papel en la teoría de tipos, en particular cuando la teoría modela una teoría de conjuntos.
Las variantes de elección única de la teoría de flechas pueden fallar, por ejemplo, en categorías cerradas localmente cartesianas con buenas propiedades de límite y límite finito , pero con solo una noción debilitada de clasificador de subobjetos .
