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 cierta otra 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 libre de 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 de inferencia cuestionables 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 , incluidas 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 números naturales, pero no sobre 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 exponenciación, factoriales o la secuencia de Fibonacci .
Gentzen demostró que la consistencia 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 libre de cuantificadores hasta el ordinal ε 0 . La aritmética recursiva primitiva es una forma mucho más simplificada de aritmética que no es controvertida. El principio adicional significa, informalmente, que hay un buen orden en el conjunto de árboles de raíces finitas . Formalmente, ε 0 es el primer ordinal tal que y es un ordinal contable mucho más pequeño que los grandes ordinales contables . Es el límite de la secuencia:
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 proporcionado por el teorema de la forma normal de Cantor . Requerimos para cualquier fórmula libre de cuantificador A (x): si hay un ordinal a <ε 0 para el cual A (a) es falso, entonces hay un ordinal mínimo.
Gentzen define una noción de "procedimiento de reducción" para demostraciones en aritmética de Peano. Para una prueba dada, tal procedimiento produce un árbol de pruebas, con la dada que sirve como la 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 se mueve hacia abajo 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 resultaría en una secuencia descendente infinita de ordinales menor que ε 0 producida por una operación recursiva primitiva en las demostraciones correspondientes a una fórmula libre de cuantificadores. [1]
Es posible interpretar la demostración de Gentzen en términos de teoría de juegos ( Tait 2005 ).
Relación con el programa de Hilbert y el teorema de Gödel
La demostración de Gentzen destaca un aspecto que comúnmente se pasa por alto del segundo teorema de incompletitud de Gödel . A veces se afirma que la consistencia de una teoría solo puede demostrarse en una teoría más sólida. La teoría de Gentzen obtenida mediante la adición de 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 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 teórico 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 poderosas 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 punto importante de la noción de interpretabilidad). Y, suponiendo que T no es extremadamente débil, T mismo podrá probar esto mismo condicional: si B es consistente, entonces también lo es T. Por lo tanto, T no puede Demuestre que B es consistente, por el segundo teorema de incompletitud, mientras que B bien puede probar que T es consistente. Esto es lo que motiva la idea de utilizar 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 lo es.
Una forma sólida del segundo teorema de incompletitud, demostrado por Pavel Pudlák, [2] que se basaba en trabajos anteriores de Solomon Feferman , [3] establece que ninguna teoría T consistente 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) no interpretar T, por una forma fuerte de la arithmetized teorema de completitud . Entonces, Q + Con (T) siempre es 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 interpretó 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 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 luego 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, en última instancia, todos los matemáticos hubieran aceptado el enfoque de Hilbert si hubiera podido llevarlo a cabo con éxito. Los primeros pasos fueron inspiradores y prometedores. Pero entonces Gödel le asestó un tremendo golpe (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 el razonamiento mediante el cual se da una prueba de consistencia debe contener algún argumento que no tenga una contraparte formal dentro del sistema, es decir, no hemos logrado formalizar completamente el procedimiento de inducción matemática; o se debe renunciar por completo a la esperanza de una prueba de coherencia estrictamente "finitista". Cuando G. Gentzen finalmente logró demostrar 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 la matemática clásica mediante una prueba de coherencia no contemplaban que se tuviera que utilizar un método como la inducción transfinita hasta ε 0 . Hasta qué punto se puede aceptar la prueba de Gentzen como una garantía de la teoría de números clásica en el sentido de que la formulación del problema es en el estado actual de cosas una cuestión de juicio individual, dependiendo de qué tan listo esté uno para aceptar la inducción hasta ε 0 como un finitario método.
Otras pruebas de coherencia de la aritmética
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 Annals . Gentzen continuó publicando dos pruebas de coherencia más, una en 1938 y otra en 1943. Todas ellas están contenidas en ( Gentzen & Szabo 1969 ).
En 1940 Wilhelm Ackermann publicó otra prueba de consistencia para la aritmética de Peano, también usando el ordinal ε 0 .
Trabajo iniciado por la prueba de Gentzen
La prueba de Gentzen es el primer ejemplo de lo que se llama análisis ordinal teórico de la prueba . En el análisis ordinal, uno mide la fuerza de las teorías midiendo qué tan grandes son los ordinales (constructivos) que se puede probar que están bien ordenados, o de manera equivalente, qué tan grande un ordinal (constructivo) puede probarse la inducción transfinita. Un ordinal constructivo es el tipo de orden de un recursivo bien ordenado de números naturales.
Laurence Kirby y Jeff Paris demostraron en 1982 que el teorema de Goodstein no se puede demostrar en la aritmética de Peano. Su demostración se basó en el teorema de Gentzen.
Notas
- ↑ Véase Kleene (2009 , págs. 476–499) para una presentación completa de la prueba de Gentzen y varios comentarios sobre el significado histórico y filosófico del resultado.
- ↑ Pudlak, Pavel (1 de junio de 1985). "Cortes, declaraciones de coherencia e interpretaciones" . Revista de lógica simbólica . 50 (2): 423–441. doi : 10.2307 / 2274231 . ISSN 0022-4812 . JSTOR 2274231 .
- ^ Feferman, S. "Aritmetización de la metamatemática en un entorno general" . Fundamenta Mathematicae . 49 (1). ISSN 0016-2736 .
- ^ Weyl (2012 , p. 144).
Referencias
- Gentzen, Gerhard (1936), "Die Widerspruchsfreiheit der reinen Zahlentheorie" , Mathematische Annalen , 112 : 493–565, doi : 10.1007 / BF01565428- 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 de números elementales", en ( Gentzen & Szabo 1969 ).
- Gentzen, Gerhard (1969), Szabo, ME (ed.), Collected Papers of Gerhard Gentzen , Estudios en lógica y fundamentos de las matemáticas (edición de tapa dura), Amsterdam: North-Holland, ISBN 978-0-7204-2254-2 - una traducción al inglés de artículos.
- Gödel, K. (2001) [1938], "Lecture at Zilsel's" , en Feferman, Solomon (ed.), Kurt Gödel: Collected Works , vol.III Ensayos y conferencias inéditos (edición de bolsillo), Oxford University Press Inc. , págs. 87-113, ISBN 978-0-19-514722-3
|volume=
tiene texto extra ( ayuda ) - Jervell, Herman Ruge (1999), Un curso de teoría de la prueba (edición del borrador del libro de texto), archivado desde el original el 7 de junio de 2011
- 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 desde el 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.
- Tait, WW (2005), "Reformulación de Gödel de la primera prueba de coherencia de Gentzen para la aritmética: la interpretación sin contraejemplos" (PDF) , The Bulletin of Symbolic Logic , 11 (2): 225-238, doi : 10.2178 / bsl / 1120231632 , ISSN 1079-8986
- Weyl, Hermann (2012). Niveles de infinito: Escritos seleccionados sobre matemáticas y filosofía . Nueva York: Publicaciones de Dover. ISBN 978-0-486-48903-2.