La matemática inversa es un programa de lógica matemática que busca determinar qué axiomas se requieren para probar teoremas de las matemáticas. Su método de definición se puede describir brevemente como "ir hacia atrás de los teoremas a los axiomas ", en contraste con la práctica matemática ordinaria de derivar teoremas de axiomas. Puede conceptualizarse como esculpir las condiciones necesarias a partir de las suficientes .
El programa de matemáticas inversas fue presagiado por los resultados en la teoría de conjuntos , como el teorema clásico de que el axioma de elección y el lema de Zorn son equivalentes sobre la teoría de conjuntos ZF . Sin embargo, el objetivo de las matemáticas inversas es estudiar los posibles axiomas de los teoremas ordinarios de las matemáticas en lugar de los posibles axiomas de la teoría de conjuntos.
La matemática inversa generalmente se lleva a cabo utilizando subsistemas de aritmética de segundo orden , donde muchas de sus definiciones y métodos están inspirados en trabajos previos en análisis constructivo y teoría de la demostración . El uso de la aritmética de segundo orden también permite emplear muchas técnicas de la teoría de la recursión ; muchos resultados en matemática inversa tienen resultados correspondientes en análisis computable . En las matemáticas inversas de orden superior , la atención se centra en los subsistemas de la aritmética de orden superior y el lenguaje más rico asociado. [ aclaración necesaria ]
El programa fue fundado por Harvey Friedman ( 1975 , 1976 ) y presentado por Steve Simpson . Una referencia estándar para el tema es Simpson (2009) , mientras que una introducción para no especialistas es Stillwell (2018) . Una introducción a las matemáticas inversas de orden superior, y también el artículo fundacional, es Kohlenbach (2005) .
En matemáticas inversas, uno comienza con un lenguaje marco y una teoría base, un sistema de axiomas central, que es demasiado débil para probar la mayoría de los teoremas que le pueden interesar, pero aún lo suficientemente poderoso como para desarrollar las definiciones necesarias para enunciar estos teoremas. Por ejemplo, para estudiar el teorema “Toda sucesión acotada de números reales tiene un supremo ” es necesario utilizar un sistema base que pueda hablar de números reales y sucesiones de números reales.
Para cada teorema que se puede establecer en el sistema base pero que no se puede probar en el sistema base, el objetivo es determinar el sistema de axiomas particular (más fuerte que el sistema base) que es necesario para probar ese teorema. Para mostrar que se requiere un sistema S para demostrar un teorema T , se requieren dos demostraciones. La primera prueba muestra que T es demostrable a partir de S ; esta es una prueba matemática ordinaria junto con una justificación de que puede llevarse a cabo en el sistema S . La segunda prueba, conocida como inversión , muestra que T mismo implica S ; esta prueba se realiza en el sistema base. La inversión establece que ningún sistema axiomático S′que extiende el sistema base puede ser más débil que S sin dejar de probar T .