Por qué los teoremas de Gödel necesitan sus hipótesis

Conversación: Gödel incompleteness theorem hypotheses (resumen). Índice: documentos.

El contraejemplo que motiva la pregunta

La aritmética verdadera —el conjunto de todos los enunciados verdaderos sobre los enteros estándar en el lenguaje de la aritmética de Peano— es consistente, completa y contiene toda la aritmética que haga falta. Parece refutar a Gödel, y no lo hace: le falta la hipótesis decisiva, porque su conjunto de axiomas no es recursivamente enumerable.

Ahí está el fondo del asunto. Los teoremas de incompletitud no tratan de la verdad frente a la demostración —eso sería trivial para una teoría no computable—, sino de lo que puede demostrar un procedimiento mecánico.

Para qué sirve cada hipótesis

Hipótesis	Qué excluye	Qué pasa si se quita
Axiomas recursivamente enumerables	Teorías cuyos axiomas no se pueden listar ni reconocer con un algoritmo	La aritmética verdadera: completa, pero codifica la verdad «por arte de magia»
Consistencia	Teorías que lo demuestran todo	El resultado se vuelve vacío: una teoría inconsistente es completa
Aritmética suficiente	Teorías demasiado débiles para representar las funciones recursivas	Hay teorías completas y decidibles, como la aritmética de Presburger (solo suma) o la geometría elemental de Tarski
Lenguaje formal de primer orden	Sistemas sin noción mecánica de prueba	«Incompletitud» deja de estar definida

La lectura conjunta es la buena: las hipótesis describen el mínimo que hace falta para tener un sistema formal mecánicamente verificable y significativo, y el teorema muestra que ese mínimo es autodestructivo. Procedimiento efectivo más consistencia implica incompletitud.

La sentencia G y su construcción

Gödel construye una sentencia que «dice» yo no soy demostrable en PA, en tres pasos:

Numeración de Gödel. Cada símbolo, fórmula y prueba recibe un número natural. Una fórmula pasa a ser un número; una secuencia de fórmulas, otro.
Aritmetización de la demostrabilidad. Se define ProofSeq(y, x): «y codifica una secuencia que es una prueba válida cuya última línea es la fórmula de número x». Comprueba que cada paso sea axioma o se siga por una regla. Es una propiedad puramente aritmética. Y de ahí Prov(x) ≡ ∃y ProofSeq(y, x).
Diagonalización. El lema diagonal da una sentencia G con PA ⊢ G ↔︎ ¬Prov(⌈G⌉).

El salto conceptual es el segundo paso: una noción metalógica —ser demostrable— se convierte en una propiedad de números, sin mencionar lógica ni significado. ¬Prov(x) dice literalmente «ningún número codifica una prueba de x».

El argumento, bien hecho

La versión que apareció en la conversación es la que circula por todas partes y es incorrecta. Decía: «si G es demostrable, entonces G es verdadera, pero G dice que no es demostrable: contradicción». Eso presupone la corrección (que PA solo demuestre verdades), que es una hipótesis semántica mucho más fuerte que la consistencia, y justamente la que Gödel quería evitar. El argumento correcto es sintáctico y asimétrico:

PA no demuestra G, si PA es consistente. Si hubiera una prueba de G, su código n satisfaría ProofSeq(n, ⌈G⌉), y como PA demuestra todos los enunciados Σ₁ verdaderos, PA ⊢ Prov(⌈G⌉), es decir PA ⊢ ¬G. Con PA ⊢ G, PA sería inconsistente.
PA no demuestra ¬G, y aquí hace falta más: Gödel usó la ω-consistencia. Rosser (1936) lo mejoró con un truco sobre la fórmula —comparar longitudes de prueba— que logra la incompletitud con la sola consistencia.

La moraleja «G es verdadera pero indemostrable» es correcta, pero depende de un paso extra: se ve desde fuera, en el modelo estándar, y por eso el segundo teorema es más robusto que el primero como resultado filosófico.

El segundo teorema, que la conversación no llegó a mencionar

Si PA es consistente, PA no demuestra Con(PA), el enunciado que formaliza su propia consistencia. Y esto no sale solo del lema diagonal: exige las condiciones de derivabilidad de Hilbert-Bernays-Löb sobre Prov, que son información intensional sobre cómo está construido el predicado. Es la razón por la que el esquema general de Lawvere cubre el primer teorema y no el segundo, como se discute en Copiar y nombrar: la diagonal que une a Cantor y Gödel.

Para el libro es la pieza relevante: el programa de Hilbert pretendía cerrar el grafo de justificaciones desde dentro, y el segundo teorema demuestra que no se puede. Gentzen (1936) sí probó la consistencia de la aritmética, pero desde fuera, con inducción transfinita hasta ε₀ — y ese sistema externo pide a su vez justificación. Autorreferencia por un lado, regreso por el otro: el dilema de Aporías reflexivas de marco.

Fuentes

K. Gödel, «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I», Monatshefte für Mathematik und Physik 38 (1931).
J. B. Rosser, «Extensions of Some Theorems of Gödel and Church», Journal of Symbolic Logic 1 (1936).
D. Hilbert y P. Bernays, Grundlagen der Mathematik II (1939), condiciones de derivabilidad.
G. Gentzen, «Die Widerspruchsfreiheit der reinen Zahlentheorie», Mathematische Annalen 112 (1936).
True arithmetic, la entrada que abrió la conversación.
En el repo: Copiar y nombrar: la diagonal y la ficha claude/logicas/071_programa-hilbert.md.

Correcciones y puntos pendientes

Corregido: el análisis por casos de G que daba la conversación presupone corrección, no consistencia. Arriba está la versión sintáctica, con ω-consistencia o Rosser.
Corregido: la conversación decía que ProofSeq usa «suma, producto y exponenciación» como si las tres fueran primitivas. En el lenguaje de PA la exponenciación no lo es: la codificación de secuencias se hace con la función beta de Gödel, precisamente para no necesitarla.
Añadido: el segundo teorema, ausente de la conversación.
Fuera de alcance: la conversación derivó a las ecuaciones de campo de Einstein, que no tienen relación con el tema ni con el libro. Si alguna vez se usa ese tramo, hay que corregir una afirmación: Schwarzschild no es «la única solución exacta en vacío con simetría esférica» porque sí, sino por el teorema de Birkhoff, y la lista que da a continuación mezcla soluciones de vacío (Kerr) con una que no lo es (FLRW).