Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados
«Sobre proposiciones formalmente indecidibles de Principia Mathematica y sistemas relacionados» 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.
From Wikipedia, the free encyclopedia
«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.
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ía 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 autorreferenciales. 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.
