# Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados

«Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados» (en alemán: «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I») es un artículo acerca de lógica matemática escrito por Kurt Gödel. El artículo, con fecha de 17 de noviembre de 1930, fue publicado originalmente en alemán en el volumen de 1931 de Monatshefte für Mathematik. Existen varias traducciones impresas al inglés, y el artículo ha sido incluido en dos colecciones de artículos clásicos de lógica matemática. El artículo contiene teoremas que tienen varias implicaciones para las pruebas de consistencia en matemáticas y técnicas que Gödel inventó para probar estos teoremas.

## Resumen y resultados clave

Los resultados principales que establece el artículo son el primer y segundo teoremas de incompletitud, que tienen un enorme impacto en el campo de la lógica matemática. Estos aparecen como teoremas vi y xi, respectivamente, en el artículo.
A fin de probar estos resultados, Gödel introdujo en el artículo un método que se conoce como numeración de Gödel. En este método, a cada frase y prueba formal en aritmética de primer orden se le asigna un número natural particular. Gödel muestra que muchas propiedades de estas pruebas pueden ser definidas dentro de cualquier teoría de aritmética que sea suficientemente robusta como para definir las funciones de recursión primitiva. (La terminología contemporánea de recursión y recursión primitiva aún no se habían establecido cuando el artículo fue publicado; Gödel usó a palabra rekursiv ('recursivo') para lo que hoy se conocen como funciones de recursión primitiva.) Desde entonces, el método de numeración de Gödel se ha vuelto común en la lógica matemática.
Ya que el método de numeración de Gödel era novedoso, y para evitar la ambigüedad, Gödel presentó una lista de 45 definiciones formales explícitas de funciones de recursión primitiva y relaciones usadas para manipular y probar los números de Gödel. Él usó estos para dar una definición explícita de una fórmula, Bew(x) que es verdadera si y sólo si x es el número Gödel de una frase φ y existe un número natural que es el número Gödel de una prueba de φ (Beweis es la palabra alemana de "prueba").
Una segunda técnica novedosa inventada por Gödel en este artículo fue el uso de oraciones auto-referenciales. Gödel mostró que las paradojas clásicas de autorreferencia, como "Esta afirmación es falsa", pueden ser reformuladas como afirmaciones formales de aritmética. Informalmente, la afirmación usada para probar el primer teorema de incompletitud de Gödel dice "Esta afirmación no se puede probar". El hecho de que dicha autorreferencia pueda ser expresada dentro de la aritmética no era conocido hasta que se publicó el artículo de Gödel; el trabajo independiente de Alfred Tarski en su Teorema de indefinibilidad de Tarski se llevó a cabo aproximadamente al mismo tiempo pero no fue publicado sino hasta 1936.
En la nota al pie 48a, Gödel afirmó que planeaba una segunda parte del artículo que establecería un enlace entre las pruebas de consistencia y la teoría de tipos, pero Gödel no publicó una segunda parte antes de su muerte. Sin embargo, su artículo de 1958 en Dialectica mostró cómo la teoría de tipos puede ser usada para dar una prueba de consistencia de la aritmética.

## Traducciones publicadas en inglés

Durante la vida de Gödel se imprimieron tres traducciones al inglés del artículo, pero el proceso tuvo varias dificultades. La primera traducción al inglés fue de Bernard Meltzer; fue publicada en 1963 como una obra autocontenida de la editorial Basic Books y ha sido reimpresa por Dover y 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 (Bauer-Mengelberg 1966). De acuerdo a la biografía de Gödel escrita por Dawson (Dawson 1997:216):
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 Bauer-Mengelberg (1966), quien además de dar una lista detallada de los errores tipográficos también describió lo que él creían ser errores serios 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 1972 de Alonzo Church la describió como «la traducción más cuidadosa que ha sido hecha» pero también hizo críticas específicas de la misma. Dawson (1997:216) anota:
Este proceso de aprobación fue laborioso. Gödel introdujo cambios a su texto de 1931, y las negociaciones entre los hombres fueron «prolongadas»: «En privado van Heijenoort declaró que Gödel era el individuo más obstinadamente fastidioso que había conocido». Entre ellos se «intercambiaron un total de setenta cartas y se encontraron dos veces en la oficina de Gödel para resolver cuestiones acerca de las sutilezas en los significados y uso de palabras en alemán e inglés». (Dawson 1997:216-217).
Aunque no es una traducción del artículo original, una útil cuarta versión existe que «cubre los tópicos de forma similar a los que cubre el artículo original de 1931 de Gödel acerca de la indecidibilidad» (Davis 1952:39), así como las extensiones del mismo Gödel y su comentario sobre el tema. Esto aparece como On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) y representa las conferencias de acuerdo a la transcripción de Stephen Kleene y J. Barkley Rosser a medida que Gödel las pronunciaba en el Instituto de Estudios Avanzados en Princeton, Nueva Jersey en 1934. Dos páginas de erratas y correcciones adicionales de Gödel fueron añadidas por Davis a esta versión. Esta versión también es notable porque en ella, Gödel describe por primera vez la sugerencia de Herbrand que dio origen a la forma general (es decir, la forma Herbrand-Gödel) de la recursión.

## Bibliografía

* Bauer-Mengelberg, Stefan (1966). «Review of "The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions"». The Journal of Symbolic Logic 31 (3): 484-494.
* Church, Alonzo (1972). «Review of "A Source Book in Mathematical Logic 1879–1931"». The Journal of Symbolic Logic 37 (2): 405.
* Davis, Martin, ed. (1965). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Nueva York: Dover. ISBN 0-486-43228-9.
* Davis, Martin (2000). Engines of Logic: Mathematics and the Origin of the Computer. Nueva York: W. w. Norton & Company. ISBN 0-393-32229-7.
* Gödel, Kurt (1931). «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I». Monatshefte für Mathematik und Physik (38): 173-198. doi:10.1007/BF01700692.
* Gödel, Kurt (1958). «Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes». Dialectica 12: 280-287. Reimpreso en Gödel, Kurt (1990). Soloman Feferman et al., ed. Collected Works II. Oxford University Press.
* van Heijenoort, Jean, ed. (1967). From Frege to Gödel: A Source Book on Mathematical Logic 1879–1931. Harvard University Press.
* Gödel, Kurt (1962). On Formally Undecidable Propositions of Principia Mathematica and Related Systems. (Bernard Meltzer, trad.). Basic Books. ISBN 0-486-66980-7.
* Smullyan, Raymond (1966). «Review of "On Formally Undecidable Propositions of Principia Mathematica and Related Systems"». The American Mathematical Monthly 73 (3): 319–322.
* Dawson, John W. (1997). Logical Dilemmas: The Life and Work of Kurt Gödel. Wellesley, MA: A. K. Peters. ISBN 1-56881-256-6.