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 da por sentado que la existencia de es única para cada .
El principio es importante, pero como axioma es de interés únicamente para teorías que tienen una comprensión débil y la capacidad de codificar funciones. Este es el caso, por ejemplo, de algunas teorías de conjuntos constructivos débiles [1] o 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 en que asigna cada elemento a un tal que la propiedad dada cumple en consecuencia. Formalmente, esto puede enunciarse de la siguiente manera:
Cuando se toma como cualquier predicado, se trata de un esquema axiomático . Se pueden considerar restricciones a la complejidad del predicado; por ejemplo, solo se pueden permitir fórmulas sin cuantificadores.
El axioma puede denotarse como . También puede adoptarse únicamente para funciones de los números naturales a los números naturales, en cuyo caso se lo llama . Cuando los valores de la función son secuencias, se lo puede llamar . En teoría, la existencia de un codominio particular puede ser parte de la formulación.
En los marcos aritméticos , las funciones pueden tomarse como secuencias de números. Si un cálculo de prueba incluye el principio de tercero excluido , entonces la noción de predicado de función también es liberal, y entonces el principio de comprensión de función concede la existencia de objetos de función incompatibles con la tesis de Church constructiva . Por lo tanto, este triple de principios (tercero excluido, comprensión de función y tesis de Church) es inconsistente. La adopción de los dos primeros caracteriza las teorías clásicas comunes de orden superior, la adopción de los dos últimos caracteriza las matemáticas estrictamente recursivas, mientras que no adoptar la comprensión de función también puede ser relevante en un estudio clásico de computabilidad . De hecho, el principio de comprensión de función contable 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áficos de función. Mediante la notación de construcción 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 este es en realidad un conjunto y una función en el sentido antes mencionado. La elección única es, por lo 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, también se puede derivar una elección única. Como en el caso de las teorías aritméticas, 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 basadas en la teoría de flechas pueden fallar, por ejemplo, en categorías cerradas cartesianas locales con buen límite finito y buenas propiedades límite pero con solo una noción debilitada de un clasificador de subobjetos .
