Demostración de consistencia de Gentzen

La demostración de consistencia de Gentzen de la aritmética de primer orden es un resultado pionero de la teoría de la demostración en lógica matemática publicado por Gerhard Gentzen en 1936. El resultado demuestra que los Los axiomas de Peano de aritmética de primer orden no contienen ninguna contradicción, es decir, son "consistentes", siempre y cuando otro sistema utilizado en la propia demostración tampoco contenga ninguna contradicción (es decir, se trata de una demostración de "consistencia relativa"). Este otro sistema, hoy llamado aritmética recursiva primitiva, junto con el principio adicional de inducción transfinita libre de cuantificadores hasta el ordinal límite ε₀", no es ni más fuerte ni más débil que el propio sistema de axiomas de Peano. Gentzen argumentó que su demostración evitaba los modos cuestionables de inferencia contenidos en la aritmética de Peano y que, por lo tanto, su consistencia es menos controvertida.

Teorema de Gentzen

El teorema de Gentzen se ocupa de 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 extiende sobre números naturales, pero no sobre conjuntos o funciones de números naturales. La teoría es lo suficientemente fuerte como para describir funciones de enteros definidas recursivamente como la exponenciación, los factoriales o los números de Fibonacci.

Gentzen demostró que la consistencia de los axiomas de Peano de primer orden es demostrable a partir de la aritmética recursiva primitiva con el principio adicional de inducción transfinita libre de cuantificador hasta el ε₀. La aritmética recursiva primitiva es una forma muy simplificada de aritmética que es bastante incontrovertida. El principio adicional significa, informalmente, que hay un bien ordenado en el conjunto de árboles de raíces finitas. Formalmente, ε₀ es el primer ordinal $\alpha$ tal que $\omega ^{\alpha }=\alpha$, es decir, el límite de la secuencia

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

Es un ordinal numerable mucho más pequeño que los ordinales numerables 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 ε₀. Esto se puede hacer de varias maneras, un ejemplo proporcionado por teorema de la forma normal de Cantor. La demostración de Gentzen se basa en la siguiente suposición: para cualquier fórmula libre de cuantificadores A(x) , si hay un ordinal a < ε₀ para el cual A(a) es falso, entonces hay un ordinal mínimo con dicha propiedad.

Gentzen define una noción de "procedimiento de reducción" para las demostraciones en la aritmética de Peano. Para una demostración dada, tal procedimiento produce un árbol de demostraciones, con la dada sirviendo como la raíz del árbol, y siendo las otras demostraciones "más simples" en cierto sentido que la dada inicialmente. Esta creciente simplicidad se formaliza adjuntando un < ordinal ε₀ a cada demostración, y mostrando que, a medida que uno se mueve hacia abajo en el árbol, estos ordinales se hacen más pequeños a cada paso. Luego muestra que si hubiera una demostración de una contradicción, el procedimiento de reducción resultaría en una secuencia infinita estrictamente descendente de ordinales menores que ε₀ producida por una operación recursiva primitiva sobre pruebas correspondientes a una fórmula libre de cuantificadores.​

Relación con el programa de Hilbert y el teorema de Gödel

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 matemática sólo puede ser demostrada en una teoría más fuerte. Sin embargo, 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 de primer orden (PA), pero no contiene a PA. Por ejemplo, no demuestra la inducción matemática ordinaria para todas las fórmulas, mientras que PA sí lo hace (ya que todas las instancias 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 teórico numérico, la consistencia de PA, que PA no puede. Por lo tanto, las dos teorías son, en cierto sentido, incomparables.

Dicho esto, hay otras formas más precisas de comparar la fuerza 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 gran punto de la noción de interpretabilidad). Y, suponiendo que T no es extremadamente débil, T mismo será capaz de demostrar esto condicionalmente: Si B es consistente, entonces también lo es T. Por lo tanto, T no puede probar que B es consistente, por el segundo teorema de incompletitud, mientras que B bien puede ser capaz de probar que T es consistente. Esto es lo que motiva la idea de usar la interpretabilidad para comparar teorías, es decir, el pensamiento de que, si B interpreta T, entonces B es al menos tan fuerte (en el sentido de "fuerza de consistencia") como T.

Una forma fuerte del segundo teorema de incompletitud, demostrado por Pavel Pudlák,​ que se basaba en el trabajo anterior de Solomon Feferman,​ afirma que ninguna teoría consistente T que contenga aritmética de Robinson, Q, puede interpretar Q más que Con(T), la afirmación de que T es consistente. Por el contrario, Q+Con(T) interpreta T, por una forma fuerte del [[teorema de completitud de Gödel|teorema de completitud]. Así que Q+Con(T) es siempre más lógicamente fuerte que T. Pero la teoría de Gentzen interpreta trivialmente Q+Con(PA), ya que contiene Q y demuestra Con(PA), y así 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 lo 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 sería 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 incompletitud de Gödel de 1931 en el plan de Hilbert para probar la consistencia de las matemáticas.​

Es probable que todos los matemáticos hubieran aceptado finalmente el enfoque de Hilbert si hubiera sido capaz de llevarlo a cabo con éxito. Los primeros pasos fueron inspiradores y prometedores. Pero luego Gödel le asestó un golpe terrible (1931), del que aún no se ha recuperado. Gödel enumeró los símbolos, fórmulas y secuencias de fórmulas en el formalismo de Hilbert de cierta manera, y así transformó la afirmación de consistencia en una proposición aritmética. Pudo demostrar que esta proposición no puede ser probada ni refutada dentro del formalismo. Esto puede significar sólo dos cosas: o bien el razonamiento por el cual se da una demostración de consistencia debe contener algún argumento que no tenga contrapartida formal dentro del sistema, es decir, no hemos logrado formalizar completamente el procedimiento de inducción matemática; o la esperanza de una demostración estrictamente "finitista" de consistencia debe ser abandonada por completo. Cuando G. Gentzen finalmente logró probar la consistencia de la aritmética, traspasó 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 iniciado por Hilbert.

Las propuestas originales de los formalistas para asegurar las matemáticas clásicas mediante una demostración de consistencia no contemplaban que un método como la inducción transfinita hasta ε₀ tendría que ser utilizado. Hasta qué punto la demostración de Gentzen puede ser aceptada como aseguramiento de la teoría clásica de números en el sentido de que la formulación del problema es, en el estado actual de las cosas, un asunto para el juicio individual, dependiendo de cuán listo esté uno para aceptar la inducción hasta ε₀ como un método finitario.

En contraste, Bernays (1967)​ comentó si el confinamiento de Hilbert a métodos finitarios era demasiado restrictivo:

Por lo tanto, se hizo evidente que el "Standpunkt finito" no es la única alternativa a las formas clásicas de razonamiento y no está necesariamente implícito en la idea de la teoría de la demostración. Por lo tanto, se sugirió una ampliación de los métodos de la teoría de la demostración: en lugar de una reducción a métodos finitistas de razonamiento, solo se requería que los argumentos fueran de carácter constructivo, lo que nos permitiera tratar con formas más generales de inferencia.

Otras demostraciones de consistencia aritmética

La primera versión de Gentzen de su demostración de consistencia no se publicó durante su vida porque Paul Bernays se había opuesto a un método utilizado implícitamente en la demostración. La demostración modificada, descrita anteriormente, fue publicada en 1936 en los Anales de Matemáticas| Anales]]. Gentzen publicó dos demostraciones de consistencia adicionales, una en 1938 y otra en 1943. Todos estos están contenidos 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 demostración de consistencia para la aritmética de Peano, también usando el ordinal ε₀.

Otra demostración de consistencia de la aritmética fue publicada por I. N. Khlodovskii, en 1959.

Sin embargo, otras demostraciones de consistencia de la aritmética fueron publicadas por: T. J. Stępień y Ł. T. Stępień (en 2018) y por S. Artemov (en 2019). En el artículo de Stępieńs se ha afirmado que la demostración de consistencia (publicada allí), del Sistema Aritmético, se realiza dentro de este Sistema.

En el artículo de Artemov se ha afirmado que la demostración publicada allí es formalizable en la aritmética de Peano.

Trabajo iniciado por la demostración de Gentzen

La demostración de Gentzen es el primer ejemplo de lo que se llama análisis ordinal teórico de la demostración. En el análisis ordinal, se mide la fuerza de las teorías midiendo cuán grandes son los ordinales (constructivos) que se puede demostrar que están bien ordenados, o equivalentemente qué tan grande es un ordinal (constructivo) que se puede probar la inducción transfinita. Un ordinal constructivo es el tipo de orden de un bien ordenamiento de los números naturales recursivo.

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

Laurence Kirby y Jeff Paris demostró en 1982 que el teorema de Goodstein no puede ser probado en la aritmética de Peano. Su demostración se basó en el teorema de Gentzen.

Referencias

Bibliografía

• Artemov, S. (2019). «The Provability of Consistency».

. 

• Gentzen, Gerhard (1936), «Die Widerspruchsfreiheit der reinen Zahlentheorie», Mathematische Annalen 112: 493-565, S2CID 122719892, doi:10.1007/BF01565428 . – Translated as "The consistency of arithmetic", in (Gentzen y 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 . – Translated as "New version of the consistency proof for elementary number theory", in (Gentzen y Szabo, 1969).
• Gentzen, Gerhard (1969), Szabo, M. E., ed., Collected Papers of Gerhard Gentzen, Studies in logic and the foundations of mathematics (Hardcover edición), Amsterdam: North-Holland, ISBN 978-0-7204-2254-2, (requiere registro) . - an English translation of papers.
• Gödel, K. (2001) [1938], «Lecture at Zilsel's», en Feferman, Solomon, ed., Kurt Gödel: Collected Works, III Unpublished Essays and Lectures (Paperback edición), Oxford University Press Inc., pp. 87-113, ISBN 978-0-19-514722-3 .
• Jervell, Herman Ruge (1999), A course in proof theory (textbook draft edición), archivado desde el original el 7 de junio de 2011 .
• Khlodovskii, I. N. (1959), «A new proof of the consistency of arithmetic», Uspekhi Mat. Nauk 14 (6(90)): 105-140 .
• Kirby, L.; Paris, J. (1982), «Accessible independence results for Peano arithmetic», Bull. London Math. Soc. 14 (4): 285-293, doi:10.1112/blms/14.4.285, archivado desde el original el 12 de septiembre de 2014  .
• Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2. 
• Stępień, T. J.; Stępień, Ł. T. (2018). «On the Consistency of the Arithmetic System».

. 

• Tait, W. W. (2005), «Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation», The Bulletin of Symbolic Logic 11 (2): 225-238, ISSN 1079-8986, S2CID 9481361, doi:10.2178/bsl/1120231632 .
• Weyl, Hermann (2012). Levels of infinity: Selected writings on mathematics and philosophy. New York: Dover Publications. ISBN 978-0-486-48903-2. 

• Datos: Q5533794