La prueba de consistencia de Gentzen

La prueba de consistencia de Gentzen es un resultado de la teoría de la demostración en lógica matemática , publicada por Gerhard Gentzen en 1936. Demuestra que los axiomas de Peano de la aritmética de primer orden no contienen contradicciones (es decir, son consistentes ), siempre que otro sistema utilizado en la demostración tampoco contenga contradicciones. Este otro sistema, conocido hoy como « aritmética recursiva primitiva con el principio adicional de inducción transfinita sin cuantificadores hasta el ordinal ε₀ _» , no es ni más débil ni más fuerte que el sistema de axiomas de Peano. Gentzen argumentó que evita los modos de inferencia cuestionables de la aritmética de Peano y que, por lo tanto, su consistencia es menos controvertida.

El teorema de Gentzen se refiere a la aritmética de primer orden: la teoría de los números naturales , incluyendo su suma y multiplicación, axiomatizada por los axiomas de Peano de primer orden . Esta es una teoría de "primer orden": los cuantificadores se extienden sobre los números naturales, pero no sobre conjuntos o funciones de números naturales. La teoría es lo suficientemente fuerte como para describir funciones enteras definidas recursivamente, como la exponenciación, los factoriales o la sucesión de Fibonacci .

Gentzen demostró que la consistencia de los axiomas de Peano de primer orden es demostrable sobre la teoría base de la aritmética recursiva primitiva con el principio adicional de inducción transfinita sin cuantificadores hasta el ordinal ε ₀ . La aritmética recursiva primitiva es una forma mucho más simplificada de aritmética que es bastante indiscutible. El principio adicional significa, informalmente, que existe un buen orden en el conjunto de árboles con raíz finitos . Formalmente, ε ₀ es el primer ordinal${\displaystyle \alpha }$de tal manera que${\displaystyle \omega ^{\alpha }=\alpha }$, es decir, el límite de la secuencia

${\displaystyle \omega ,\ \omega ^{\omega },\ \omega ^{\omega ^{\omega }},\ \ldots }$

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 los ordinales menores que ε _0. Esto se puede hacer de varias maneras, un ejemplo lo proporciona el teorema de la forma normal de Cantor . La demostración de Gentzen se basa en la siguiente suposición: para cualquier fórmula sin cuantificadores A(x), si hay un ordinal a < ε ₀ para el cual A(a) es falso, entonces hay al menos un ordinal de ese tipo.

Gentzen define una noción de "procedimiento de reducción" para demostraciones en aritmética de Peano. Para una demostración dada, dicho procedimiento produce un árbol de demostraciones, donde la demostración dada actúa como raíz del árbol, y las demás demostraciones son, en cierto sentido, "más simples" que la demostración dada. Esta creciente simplicidad se formaliza al adjuntar un ordinal < ε ₀ a cada demostración y al demostrar que, a medida que se desciende por el árbol, estos ordinales se hacen más pequeños con cada paso. Luego demuestra que si existiera una demostración de contradicción, el procedimiento de reducción daría como resultado una secuencia infinita estrictamente descendente de ordinales menores que ε ₀ producida por una operación recursiva primitiva sobre demostraciones que corresponden a una fórmula sin cuantificadores. ^{[ 1 ]}

La demostración de Gentzen resalta un aspecto comúnmente pasado por alto del segundo teorema de incompletitud de Gödel . A veces se afirma que la consistencia de una teoría solo puede probarse en una teoría más fuerte. La teoría de Gentzen, obtenida al agregar inducción transfinita sin cuantificadores a la aritmética recursiva primitiva, prueba la consistencia de la aritmética de Peano de primer orden (AP), pero no la contiene. Por ejemplo, no prueba la inducción matemática ordinaria para todas las fórmulas, mientras que AP sí lo hace (ya que todas las instancias de inducción son axiomas de AP). Sin embargo, la teoría de Gentzen tampoco está contenida en AP, puesto que puede probar un hecho de la teoría de números —la consistencia de AP— que AP no puede. Por lo tanto, en cierto sentido, las dos teorías son incomparables .

Dicho esto, existen otras formas más precisas 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 clave de la noción de interpretabilidad). Y, suponiendo que T no sea extremadamente débil, T misma podrá demostrar esta condición: si B es consistente, entonces T también lo es. Por lo tanto, T no puede demostrar que B es consistente, según el segundo teorema de incompletitud, mientras que B sí puede demostrar que T es consistente. Esto es lo que motiva la idea de usar la interpretabilidad para comparar teorías, es decir, la idea de que, si B interpreta a T, entonces B es al menos tan fuerte (en el sentido de "solidez de consistencia") como 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 aritmetizado . Así pues, 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), puesto que contiene Q y demuestra Con(PA), y por lo tanto la teoría de Gentzen interpreta PA. Pero, según el resultado de Pudlák, PA no puede interpretar la teoría de Gentzen, puesto 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, también interpretaría Q+Con(PA) y, por lo tanto, sería inconsistente, según el resultado de Pudlák. Así pues, en términos 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 con respecto a la importancia del resultado de consistencia de Gentzen después del 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 ]}

Es probable que todos los matemáticos hubieran aceptado el enfoque de Hilbert si este hubiera logrado llevarlo a cabo con éxito. Los primeros pasos fueron inspiradores y prometedores. Pero entonces Gödel le asestó un golpe tremendo (1931), del que aún no se ha recuperado. Gödel enumeró los símbolos, fórmulas y secuencias de fórmulas del formalismo de Hilbert de una manera particular, transformando así la afirmación de consistencia en una proposición aritmética. Pudo demostrar que esta proposición no puede probarse ni refutarse dentro del formalismo. Esto solo puede significar dos cosas: o bien el razonamiento con el que se da una prueba de consistencia debe contener algún argumento que no tenga contraparte formal dentro del sistema, es decir, no hemos logrado formalizar completamente el procedimiento de inducción matemática; o bien debemos abandonar por completo la esperanza de una prueba de consistencia estrictamente "finitista". Cuando G. Gentzen finalmente logró demostrar la consistencia de la aritmética, transgredió esos límites al afirmar como evidente un tipo de razonamiento que penetra en la "segunda clase de números ordinales" de Cantor.

Kleene (2009 , p. 479) hizo el siguiente comentario en 1952 sobre la importancia del resultado de Gentzen, particularmente en el contexto del programa formalista que fue iniciado por Hilbert. 

Las propuestas originales de los formalistas para garantizar la seguridad de las matemáticas clásicas mediante una prueba de consistencia no contemplaban la necesidad de utilizar un método como la inducción transfinita hasta ε₀ _. En la actualidad, la aceptación de la prueba de Gentzen como garantía para la teoría clásica de números, en el sentido de dicha formulación del problema, queda a criterio de cada uno, dependiendo de su disposición a aceptar la inducción hasta ε₀ _como un método finito.

En cambio, Bernays (1967) comentó si la limitación de Hilbert a los métodos finitos era demasiado restrictiva:

Así pues, quedó claro que el «punto de vista finito» no es la única alternativa a los métodos clásicos de razonamiento y que la idea de la teoría de la demostración no implica necesariamente dicha alternativa. Por consiguiente, se propuso ampliar los métodos de la teoría de la demostración: en lugar de reducirlos a métodos finitistas, bastaba con que los argumentos fueran de carácter constructivo, lo que nos permitía abordar formas de inferencia más generales.

La primera versión de la demostración de consistencia de Gentzen no se publicó en vida del autor debido a la objeción de Paul Bernays a un método implícito en la demostración. La demostración modificada, descrita anteriormente, se publicó en 1936 en los Anales . Gentzen publicó posteriormente dos demostraciones de consistencia más, una en 1938 y otra en 1943. Todas ellas se encuentran en ( Gentzen y Szabo, 1969 ) .

Kurt Gödel reinterpretó la demostración de Gentzen de 1936 en una conferencia en 1938, en lo que se conoció como la interpretación sin contraejemplo. Tanto la demostración 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 ε ₀ .

Otra prueba de la consistencia de la aritmética fue publicada por I. N. Khlodovskii en 1959.

La demostración de Gentzen es el primer ejemplo de lo que se denomina análisis ordinal de la teoría de la demostración . En el análisis ordinal, la solidez de las teorías se evalúa midiendo el tamaño de los ordinales (constructivos) que pueden demostrarse como bien ordenados, o, equivalentemente, el tamaño de un ordinal (constructivo) para el que se puede demostrar la inducción transfinita. Un ordinal constructivo es el tipo de orden de un buen ordenamiento recursivo de los números naturales.

En este lenguaje, el trabajo de Gentzen establece que el ordinal de la teoría de la demostración de la aritmética de Peano de primer orden es ε ₀ .

Laurence Kirby y Jeff Paris demostraron en 1982 que el teorema de Goodstein no puede probarse en aritmética de Peano. Su demostración se basó en el teorema de Gentzen. ^{[ 5 ]}

• Edwards, Paul, ed. (1967). "Paul Bernays". Enciclopedia de Filosofía . Vol.  3. MacMillan and Free Press. pág.  502.
• Feferman, Solomon (1960). "Aritmetización de la metamatemática en un contexto general" . Fundamenta Mathematicae . 49 (1): 35–92 . doi : 10.4064/fm-49-1-35-92 . ISSN 0016-2736 . 
• Gentzen, Gerhard (1936), "Die Widerspruchsfreiheit der reinen Zahlentheorie" , Mathematische Annalen , 112 : 493– 565, doi : 10.1007/BF01565428 , S2CID 122719892 – Traducido como "La consistencia de la aritmética", en ( Gentzen & Szabo 1969 ) .
• Gentzen, Gerhard (1938), "Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie", Forschungen zur Logik und zur Grundlegung der Exakten Wissenschaften , 4 : 19– 44– Traducido como "Nueva versión de la prueba de consistencia para la teoría elemental de números", en ( Gentzen & Szabo 1969 ) .
• Gentzen, Gerhard (1969), Szabo, ME (ed.), Obras completas de Gerhard Gentzen , Estudios de lógica y fundamentos de las matemáticas (  Edición en tapa dura), Ámsterdam: North-Holland, ISBN 978-0-7204-2254-2- una traducción al inglés de documentos.
• Gödel, K. (2001) [1938], «Conferencia en casa de Zilsel» , en Feferman, Solomon (ed.), Kurt Gödel: Obras completas , vol.  III Ensayos y conferencias inéditas (  edición de bolsillo), Oxford University Press Inc., pp. 87–113 , ISBN  978-0-19-514722-3
• Jervell, Herman Ruge (1999), Un curso de teoría de la demostración (edición preliminar del libro de texto  ), archivado del original el 7 de junio de 2011.
• Khlodovskii, IN (1959), "Una nueva prueba de la consistencia de la aritmética" (PDF) , Uspekhi Mat. Nauk , 14 (6 ( 90)): 105–140
• Kirby, L .; Paris, J. (1982), "Resultados de independencia accesibles para la aritmética de Peano" (PDF) , Bull. London Math. Soc. , 14 (4): 285–293 , CiteSeerX 10.1.1.107.3303 , doi : 10.1112/blms/14.4.285 , archivado del original (PDF) el 12 de septiembre de 2014. 
• Kleene, Stephen Cole (2009) [1952]. Introducción a la metamatemática . Ishi Press International. ISBN 978-0-923891-57-2.
• Pudlák, Pavel (1 de junio de 1985). "Recortes, declaraciones de consistencia e interpretaciones" . Journal of Symbolic Logic . 50 (2): 423– 441. doi : 10.2307/2274231 . ISSN 0022-4812 . JSTOR 2274231 .  
• Tait, WW (2005), "La reformulación de Gödel de la primera prueba de consistencia de Gentzen para la aritmética: la interpretación sin contraejemplo" (PDF) , The Bulletin of Symbolic Logic , 11 (2): 225–238 , doi : 10.2178/bsl/1120231632 , ISSN 1079-8986 , S2CID 9481361  
• Weyl, Hermann (2012). Niveles de infinito: Escritos selectos sobre matemáticas y filosofía . Nueva York: Dover Publications. ISBN 978-0-486-48903-2.