Una oración autorreferencial G construida (mediante el lema del punto fijo) para una teoría formal dada T que afirma efectivamente 'G no es demostrable en T'; su existencia es central en las pruebas de incompletitud porque, bajo hipótesis naturales, ni G ni su negación son demostrables en T.

Principio

Usar el lema del punto fijo/diagonal para producir una oración que nombre su propio estado de demostrabilidad codificando nociones sintácticas en aritmética; la oración se diseña de modo que la demostrabilidad de G en T contradiría la consistencia de T, conduciendo a la indecidibilidad.

Demostración

Para una teoría T recursivamente axiomática que represente la demostrabilidad, se construye una fórmula Prov_T(x) y se aplica el lema del punto fijo para obtener G con T ⊢ (G ↔ ¬Prov_T(⌜G⌝)). Si T es consistente, T no puede probar G; si T es suficientemente bien comportada tampoco puede probar ¬G, haciendo G indecidible en T.

Aplicación incorrecta

Confundir una oración de Gödel con una paradoja semántica (por ejemplo, el mentiroso) o afirmar que toda oración autorreferencial es una oración de Gödel; también llamar a cualquier oración no demostrable 'la' oración de Gödel sin referirse a la teoría y al codificado usados.

Consecuencia

Proporciona ejemplos explícitos de oraciones indecidibles en la teoría y muestra la brecha entre demostrabilidad sintáctica y verdad semántica; en el modelo estándar tal oración de Gödel será verdadera siempre que la teoría sea consistente.

Inversión

Negar la oración de Gödel produce una oración cuya demostrabilidad en T típicamente implica la inconsistencia de T; por tanto, probar ¬G dentro de T bajo las hipótesis usuales es prueba de inconsistencia.

Límite

Requiere que la teoría pueda representar nociones sintácticas y la demostrabilidad; diferentes codificaciones y elecciones producen oraciones de Gödel no únicas, de modo que la construcción depende del formalismo y no es canónica más allá de equivalencias demostrables en meta-teorías más ricas.

Tensión semántica

Se sitúa entre nociones de verdad semántica, demostrabilidad sintáctica y autorreferencia paradójica: se asemeja al mentiroso en forma pero difiere porque su construcción está aritmetizada y su indemostrabilidad deriva de la consistencia en lugar de un paradoja semántica.

Síntesis

Una oración de Gödel es una construcción aritmetizada autorreferencial que afirma su propia no-demostrabilidad en una teoría dada; mediante diagonalización convierte el codificado sintáctico en una oración aritmética indecidible explícita bajo la consistencia de la teoría.