La prueba de consistencia de Gentzen es el resultado de la teoría de la prueba en lógica matemática , publicada por Gerhard Gentzen en 1936. Muestra que los axiomas de Peano de la aritmética de primer orden no contienen una contradicción (es decir, son " consistentes "), siempre que exista otro determinado. El sistema utilizado en la prueba tampoco contiene contradicciones. Este otro sistema, hoy llamado " aritmética recursiva primitiva con el principio adicional de inducción transfinita sin cuantificadores hasta el ordinal ε 0 ", no es ni más débil ni más fuerte que el sistema de axiomas de Peano. Gentzen argumentó que evita los modos cuestionables de inferencia contenidos en la aritmética de Peano y que, por lo tanto, su consistencia es menos controvertida.
El teorema de Gentzen se ocupa de la aritmética de primer orden: la teoría de los números naturales , incluidas su suma y multiplicación, axiomatizada por los axiomas de Peano de primer orden . Ésta es una teoría de "primer orden": los cuantificadores se extienden a los números naturales, pero no a conjuntos o funciones de números naturales. La teoría es lo suficientemente sólida como para describir funciones enteras definidas de forma recursiva , como la exponenciación, los factoriales o la secuencia de Fibonacci .
Gentzen demostró que la coherencia de los axiomas de Peano de primer orden se puede demostrar sobre la teoría básica de la aritmética recursiva primitiva con el principio adicional de inducción transfinita sin cuantificadores hasta el ordinal ε 0 . La aritmética recursiva primitiva es una forma de aritmética mucho más simplificada que no genera controversia. El principio adicional significa, informalmente, que existe un buen ordenamiento en el conjunto de árboles con raíces finitas . Formalmente, ε 0 es el primer ordinal tal que , es decir, el límite de la secuencia
Es un ordinal contable mucho más pequeño que los ordinales contables grandes . Para expresar ordinales en el lenguaje de la aritmética, se necesita una notación ordinal , es decir, una forma de asignar números naturales a ordinales menores que ε 0 . Esto se puede hacer de varias maneras, un ejemplo lo proporciona el teorema de la forma normal de Cantor . La prueba de Gentzen se basa en el siguiente supuesto: para cualquier fórmula A(x) sin cuantificadores, si hay un ordinal a < ε 0 para el cual A(a) es falso, entonces existe al menos ese ordinal.
Gentzen define una noción de "procedimiento de reducción" para pruebas en aritmética de Peano. Para una prueba dada, tal procedimiento produce un árbol de pruebas, donde la dada sirve como raíz del árbol y las otras pruebas son, en cierto sentido, "más simples" que la dada. Esta creciente simplicidad se formaliza adjuntando un ordinal < ε 0 a cada prueba y mostrando que, a medida que uno desciende en el árbol, estos ordinales se hacen más pequeños con cada paso. Luego muestra que si hubiera una prueba de una contradicción, el procedimiento de reducción daría como resultado una secuencia infinita estrictamente descendente de ordinales menores que ε 0 producida por una operación recursiva primitiva en pruebas correspondientes a una fórmula sin cuantificadores. [1]
La prueba de Gentzen destaca un aspecto comúnmente pasado por alto del segundo teorema de incompletitud de Gödel . A veces se afirma que la coherencia de una teoría sólo puede demostrarse mediante una teoría más sólida. La teoría de Gentzen obtenida agregando inducción transfinita sin cuantificadores a la aritmética recursiva primitiva demuestra la consistencia de la aritmética de Peano (PA) de primer orden pero no contiene PA. Por ejemplo, no prueba la inducción matemática ordinaria para todas las fórmulas, mientras que PA sí lo hace (ya que todos los casos de inducción son axiomas de PA). Sin embargo, la teoría de Gentzen tampoco está contenida en PA, ya que puede probar un hecho de la teoría de números (la consistencia de PA) que PA no puede. Por tanto, las dos teorías son, en cierto sentido, incomparables .
Dicho esto, existen otras formas más sutiles de comparar la solidez de las teorías, la más importante de las cuales se define en términos de la noción de interpretabilidad . Se puede demostrar que, si una teoría T es interpretable en otra B, entonces T es consistente si B lo es. (De hecho, este es un punto importante de la noción de interpretabilidad.) Y, suponiendo que T no es extremadamente débil, T mismo podrá probar esto de manera muy condicional: si B es consistente, entonces también lo es T. Por lo tanto, T no puede demostrar que B es consistente, mediante el segundo teorema de incompletitud, mientras que B bien puede ser capaz de demostrar que T es consistente. Esto es lo que motiva la idea de utilizar la interpretabilidad para comparar teorías, es decir, la idea de que, si B interpreta T, entonces B es al menos tan fuerte (en el sentido de "fuerza de coherencia") como lo es T.
Una forma fuerte del segundo teorema de incompletitud, demostrada por Pavel Pudlák, [2] quien se basó en trabajos anteriores de Solomon Feferman , [3] afirma que ninguna teoría consistente T que contenga la aritmética de Robinson , Q, puede interpretar Q más Con(T ), la afirmación de que T es consistente. Por el contrario, Q+Con(T) sí interpreta T, mediante una forma fuerte del teorema de completitud aritmetizada . Entonces Q+Con(T) es siempre más fuerte (en un buen sentido) que T. Pero la teoría de Gentzen interpreta trivialmente Q+Con(PA), ya que contiene Q y prueba Con(PA), por lo que la teoría de Gentzen interpreta PA. Pero, según el resultado de Pudlák, PA no puede interpretar la teoría de Gentzen, ya que la teoría de Gentzen (como se acaba de decir) interpreta Q+Con(PA), y la interpretabilidad es transitiva. Es decir: si PA interpretara la teoría de Gentzen, entonces también interpretaría Q+Con(PA) y, por tanto, sería inconsistente, según el resultado de Pudlák. Entonces, en el sentido de fuerza de consistencia, caracterizada por la interpretabilidad, la teoría de Gentzen es más fuerte que la aritmética de Peano.
Hermann Weyl hizo el siguiente comentario en 1946 sobre la importancia del resultado de consistencia de Gentzen tras el impacto devastador del resultado de incompletitud de Gödel de 1931 en el plan de Hilbert para demostrar la consistencia de las matemáticas. [4]
Kleene (2009, p. 479) hizo el siguiente comentario en 1952 sobre la importancia del resultado de Gentzen, particularmente en el contexto del programa formalista iniciado por Hilbert.
Por el contrario, Bernays (1967) comentó si el confinamiento de Hilbert a métodos finitos era demasiado restrictivo:
La primera versión de Gentzen de su prueba de coherencia no se publicó durante su vida porque Paul Bernays se había opuesto a un método utilizado implícitamente en la prueba. La prueba modificada, descrita anteriormente, se publicó en 1936 en los Anales . Gentzen publicó dos pruebas de coherencia más, una en 1938 y otra en 1943. Todas ellas están contenidas en (Gentzen y Szabo 1969).
Kurt Gödel reinterpretó la prueba de Gentzen de 1936 en una conferencia de 1938 en lo que llegó a conocerse como la interpretación sin contraejemplo. Tanto la prueba original como la reformulación pueden entenderse en términos de teoría de juegos. (Tait 2005).
En 1940 , Wilhelm Ackermann publicó otra prueba de consistencia para la aritmética de Peano, utilizando también el ordinal ε 0 .
Otra prueba de la coherencia de la aritmética fue publicada por IN Khlodovskii en 1959.
Otras pruebas de la coherencia de la aritmética fueron publicadas por: TJ Stępień y Ł. T. Stępień (en 2018) y por S. Artemov (en 2019). En el artículo de Stępieńs se afirma que la prueba de consistencia (publicada allí), del Sistema Aritmético, se realiza dentro de este Sistema. [ cita necesaria ]
En el artículo de Artemov se afirma que la prueba allí publicada es formalizable en Peano Arithmetic. [ cita necesaria ]
La prueba de Gentzen es el primer ejemplo de lo que se llama análisis ordinal de la teoría de la prueba . En el análisis ordinal, se mide la solidez de las teorías midiendo qué tan grandes son los ordinales (constructivos) que se puede demostrar que están bien ordenados o, de manera equivalente, qué tan grande se puede demostrar que un ordinal (constructivo) es una inducción transfinita. Un ordinal constructivo es el tipo de orden de un buen ordenamiento recursivo de números naturales.
En este lenguaje, el trabajo de Gentzen establece que el ordinal de la teoría de la prueba de la aritmética de Peano de primer orden es ε 0 .
Laurence Kirby y Jeff Paris demostraron en 1982 que el teorema de Goodstein no puede demostrarse en aritmética de Peano. Su demostración se basó en el teorema de Gentzen.
