El teorema que afirma que ninguna teoría formal consistente y efectivamente axiomática capaz de representar suficiente aritmética puede demostrar su propia consistencia cuando la consistencia se formaliza dentro de la propia teoría; en términos simples, un sistema no puede certificar con sus propios recursos que está libre de contradicción.

Principio

Al formalizar un predicado de demostrabilidad y usar las mismas técnicas de diagonalización que en el primer teorema, se muestra que si una teoría T probara Con(T) (una oración que formaliza 'no existe prueba de una contradicción en T'), entonces T podría probar una oración que no puede probar consistentemente, produciendo inconsistencia.

Demostración

En Aritmética de Peano se representa el predicado 'x es una prueba en PA' y se formula Con(PA). El razonamiento al estilo Gödel produce una oración G tal que si PA probara Con(PA), entonces PA probaría G y contradiría la conclusión del primer teorema; por lo tanto, si PA es consistente no puede probar Con(PA).

Aplicación incorrecta

Afirmar que el teorema prohíbe cualquier prueba externa o en un sistema más fuerte de la consistencia — el teorema sólo impide que una teoría pruebe su propia consistencia por recursos formalizables dentro de ella misma; no impide pruebas metamatemáticas o en sistemas más potentes.

Consecuencia

Las pruebas de consistencia para una teoría deben proceder de teorías más fuertes, métodos no formales o suposiciones no formalizables en la propia teoría; esto configura la jerarquía de justificaciones fundacionales y señala la relatividad inevitable de las afirmaciones de consistencia.

Inversión

La contraposición suele expresarse así: si una teoría T prueba Con(T) entonces T es inconsistente; así, probar la propia consistencia dentro del mismo sistema formal equivale a inconsistencia bajo las hipótesis del teorema.

Límite

Requiere axiomatización efectiva y suficiente aritmética para representar la demostrabilidad y los predicados de prueba; no se aplica a sistemas que carecen de la capacidad de representar esas nociones sintácticas ni a marcos que alteren la formalización de la consistencia.

Tensión semántica

Genera tensión entre perspectivas internas y externas sobre la prueba: la demostrabilidad interna de Con(T) está vetada, mientras que externamente (en una metateoría más fuerte) puede demostrarse Con(T); esto distingue la auto-certificación sintáctica de la validación metateórica.

Síntesis

El segundo teorema de Gödel formaliza la intuición de que un sistema no puede, con sus propios recursos formales, establecer que esos recursos nunca producirán contradicción: codificando pruebas y demostrabilidad dentro de la teoría y usando argumentos diagonales se muestra que tal prueba interna conduce a la inconsistencia.