" Sobre proposiciones formalmente indecidibles de los Principia Mathematica y sistemas relacionados I " (" Sobre proposiciones formalmente indecidibles de los Principia Mathematica y sistemas relacionados I ") es un artículo de lógica matemática de Kurt Gödel . Enviado el 17 de noviembre de 1930, se publicó originalmente en alemán en el volumen de 1931 de Monatshefte für Mathematik und Physik . Se han publicado varias traducciones al inglés y el artículo se ha incluido en dos colecciones de artículos clásicos de lógica matemática. El artículo contiene los teoremas de incompletitud de Gödel , ahora resultados fundamentales en lógica que tienen muchas implicaciones para las pruebas de consistencia en matemáticas. El artículo también es conocido por introducir nuevas técnicas que Gödel inventó para probar los teoremas de incompletitud.
Los principales resultados establecidos son el primer y segundo teorema de incompletitud de Gödel , que han tenido un enorme impacto en el campo de la lógica matemática . Éstos aparecen como teoremas VI y XI, respectivamente, en el artículo.
Para demostrar estos resultados, Gödel introdujo un método conocido hoy como numeración de Gödel . En este método, a cada oración y prueba formal en aritmética de primer orden se le asigna un número natural particular. Gödel demuestra que muchas propiedades de estas pruebas pueden definirse dentro de cualquier teoría de la aritmética que sea lo suficientemente sólida como para definir las funciones recursivas primitivas . (La terminología contemporánea para funciones recursivas y funciones recursivas primitivas aún no se había establecido cuando se publicó el artículo; Gödel utilizó la palabra rekursiv ("recursivo") para lo que ahora se conoce como funciones recursivas primitivas). Desde entonces, el método de numeración de Gödel se ha vuelto común en la lógica matemática.
Debido a que el método de numeración de Gödel era novedoso y para evitar cualquier ambigüedad, Gödel presentó una lista de 45 definiciones formales explícitas de funciones recursivas primitivas y relaciones utilizadas para manipular y probar los números de Gödel. Las utilizó para dar una definición explícita de una fórmula Bew( x ) que es verdadera si y solo si x es el número de Gödel de una oración φ y existe un número natural que es el número de Gödel de una prueba de φ . El nombre de esta fórmula deriva de Beweis , la palabra alemana para prueba.
Una segunda técnica nueva inventada por Gödel en este artículo fue el uso de oraciones autorreferenciales. Gödel demostró que las paradojas clásicas de la autorreferencia, como " Esta afirmación es falsa ", pueden reformularse como oraciones formales autorreferenciales de la aritmética. De manera informal, la oración empleada para demostrar el primer teorema de incompletitud de Gödel dice "Esta afirmación no es demostrable". El hecho de que dicha autorreferencia pueda expresarse dentro de la aritmética no se conocía hasta que apareció el artículo de Gödel; el trabajo independiente de Alfred Tarski sobre su teorema de indefinibilidad se llevó a cabo en la misma época, pero no se publicó hasta 1936.
En la nota 48a, Gödel afirmó que una segunda parte del artículo establecería un vínculo entre las pruebas de consistencia y la teoría de tipos (de ahí la "I" al final del título del artículo, que denota la primera parte), pero Gödel no publicó una segunda parte del artículo antes de su muerte. Sin embargo, su artículo de 1958 en Dialectica mostró cómo se puede utilizar la teoría de tipos para proporcionar una prueba de consistencia para la aritmética.
Durante su vida se imprimieron tres traducciones al inglés del artículo de Gödel, pero el proceso no estuvo exento de dificultades. La primera traducción al inglés fue obra de Bernard Meltzer ; se publicó en 1963 como obra independiente en Basic Books y desde entonces ha sido reimpresa por Dover y reimpresa por Hawking ( God Created the Integers , Running Press, 2005:1097ff). La versión de Meltzer, descrita por Raymond Smullyan como una "buena traducción", fue criticada negativamente por Stefan Bauer-Mengelberg (1966). Según la biografía de Gödel escrita por Dawson (Dawson 1997:216),
Afortunadamente, la traducción de Meltzer fue pronto suplantada por una mejor preparada por Elliott Mendelson para la antología de Martin Davis The Undecidable ; pero tampoco llegó a conocimiento de Gödel hasta casi el último minuto, y la nueva traducción todavía no era del todo de su agrado... cuando se le informó de que no había tiempo suficiente para considerar la sustitución por otro texto, declaró que la traducción de Mendelson era "en general muy buena" y aceptó su publicación. [Más tarde lamentaría su aceptación, ya que el volumen publicado estaba estropeado en su totalidad por una tipografía descuidada y numerosos errores de imprenta.]
La traducción de Elliott Mendelson aparece en la colección The Undecidable (Davis 1965:5ff). Esta traducción también recibió una crítica dura por parte de Bauer-Mengelberg (1966), quien además de dar una lista detallada de los errores tipográficos también describió lo que él creía que eran errores graves en la traducción.
Una traducción de Jean van Heijenoort aparece en la colección From Frege to Gödel: A Source Book in Mathematical Logic (van Heijenoort 1967). Una reseña de Alonzo Church (1972) la describió como "la traducción más cuidadosa que se ha hecho", pero también le hizo algunas críticas específicas. Dawson (1997:216) señala:
La traducción que Gödel prefería era la de Jean van Heijenoort... En el prefacio del volumen, van Heijenoort señaló que Gödel era uno de los cuatro autores que habían leído y aprobado personalmente las traducciones de sus obras.
Este proceso de aprobación fue laborioso. Gödel introdujo cambios en su texto de 1931 y las negociaciones entre ambos fueron “prolongadas”: “En privado, Van Heijenoort declaró que Gödel era el individuo más tenazmente meticuloso que había conocido”. Entre ellos “intercambiaron un total de setenta cartas y se reunieron dos veces en la oficina de Gödel para resolver cuestiones relativas a sutilezas en el significado y uso de palabras alemanas e inglesas” (Dawson 1997:216-217).
Aunque no se trata de una traducción del artículo original, existe una cuarta versión muy útil que "cubre un terreno bastante similar al que cubre el artículo original de Gödel de 1931 sobre la indecidibilidad" (Davis 1952:39), así como las propias extensiones y comentarios de Gödel sobre el tema. Esta aparece como On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) y representa las conferencias tal como las transcribieron Stephen Kleene y J. Barkley Rosser mientras Gödel las impartía en el Instituto de Estudios Avanzados de Princeton, Nueva Jersey, en 1934. Davis añadió a esta versión dos páginas de erratas y correcciones adicionales de Gödel. Esta versión también es notable porque en ella Gödel describe por primera vez la sugerencia de Herbrand que dio lugar a la forma (general, es decir, Herbrand–Gödel) de recursión .