Teoría de conjuntos constructiva
La teoría constructiva de conjuntos es una aproximación al constructivismo matemático siguiendo el programa de la teoría axiomática de conjuntos . Normalmente se utiliza el mismo lenguaje de primer orden con " " y " " de la teoría de conjuntos clásica, por lo que no debe confundirse con un enfoque de tipos constructivos . Por otro lado, algunas teorías constructivas sí están motivadas por su interpretabilidad en teorías tipo .
Además de rechazar la ley del tercero excluido ( ), las teorías de conjuntos constructivas a menudo requieren algunos cuantificadores lógicos en sus axiomas para ser acotados , motivados por resultados ligados a la impredicatividad .
La lógica de las teorías de conjuntos discutidas aquí es constructiva en el sentido de que rechaza , es decir, que la disyunción se cumple automáticamente para todas las proposiciones. Entonces, esto requiere el rechazo de los principios de elección fuerte y la reformulación de algunos axiomas estándar. Por ejemplo, el Axioma de Elección implica para las fórmulas en el esquema de Separación adoptado, por el teorema de Diaconescu . Resultados similares valen para el Axioma de Regularidad en su forma estándar. Como regla, para probar una disyunción particular , ya sea o necesita ser probado. En ese caso, se dice que la disyunción es decidible. A su vez, las teorías constructivas tienden a no permitir muchas demostraciones clásicas de propiedades que son, por ejemplo, demostrablemente indecidibles computacionalmente . A diferencia de la lógica mínima más conservadora , aquí la lógica subyacente permite la eliminación de doble negación para predicados decidibles y las formulaciones de teoremas con respecto a construcciones finitas tienden a no diferir de sus contrapartes clásicas.
En particular, una restricción a la lógica constructiva conduce a requisitos más estrictos con respecto a qué caracterizaciones de un conjunto que involucra colecciones ilimitadas constituyen una función (matemática, y por lo tanto siempre implicando total ). Esto se debe a menudo a que el predicado en una posible definición basada en casos puede no ser decidible. En comparación con la contraparte clásica, generalmente es menos probable que se demuestre la existencia de relaciones que no se pueden realizar. Esto entonces también afecta la demostrabilidad de los enunciados sobre órdenes totales como el de todos los números ordinales , expresados por la verdad y la negación de los términos en el orden que define la disyunción . Y esto a su vez afecta la fuerza teórica de la prueba definida en el análisis ordinal .
