Una variante de una oración de Gödel construida usando el truco de Rosser que debilita las hipótesis necesarias para la incompletitud: produce una oración indecidible para cualquier teoría consistente y recursivamente enumerable sin requerir ω-consistencia, empleando un predicado de demostrabilidad modificado que compara longitudes de prueba.

Principio

Rosser sustituye el predicado estándar de demostrabilidad por una relación de demostrabilidad Rosser que afirma 'existe una prueba de mí y no existe una prueba más corta de mi negación', o usa de forma equivalente un orden de testigos para evitar la hipótesis más fuerte de ω-consistencia del argumento original de Gödel.

Demostración

Para una T recursivamente axiomatizable se define un predicado al estilo Rosser RProv_T(x) que cuantifica sobre contrapruebas más cortas y se aplica diagonalización para producir una oración R con T ⊢ (R ↔ ¬RProv_T(⌜R⌝)). Si T es simplemente consistente, argumentos sobre pruebas mínimas muestran que T no puede probar ni R ni ¬R, por lo que R es indecidible en T.

Aplicación incorrecta

Suponer que las oraciones de Rosser eliminan toda sutileza metamatemática: debilitan la hipótesis de ω-consistencia a mera consistencia, pero aún requieren axiomatización efectiva y correcta formalización de comparaciones de pruebas; no vuelven triviales todas las pruebas de incompletitud ni borran distinciones modelo-teóricas.

Consecuencia

Muestra que la incompletitud se mantiene bajo hipótesis de consistencia más débiles y aclara el papel de la comparación de pruebas en la indecidibilidad; refina el resultado de Gödel bajando el requisito de consistencia para construir oraciones indecidibles.

Inversión

Si una teoría prueba la oración de Rosser o su negación, el análisis de pruebas usado en la construcción de Rosser conduce a una contradicción, de modo que la demostrabilidad de cualquiera de las dos revela inconsistencia bajo las hipótesis de la construcción.

Límite

Se aplica a teorías recursivamente enumerables (efectivamente axiomáticas) que pueden formalizar prueba y nociones de longitud/comparación de pruebas; no se aplica a sistemas no efectivos ni a formalismos que no puedan representar el orden requerido de las pruebas.

Tensión semántica

Compite con la oración de Gödel al intercambiar la fortaleza de las hipótesis por la simplicidad del predicado de demostrabilidad: las oraciones de Rosser usan maquinaria más elaborada de comparación de pruebas para lograr indecidibilidad con hipótesis más débiles, produciendo comportamientos técnicos e interpretaciones metamatemáticas distintos.

Síntesis

Una oración de Rosser es una oración autorreferencial aritmetizada diseñada mediante una noción de demostrabilidad sensible a la comparación de pruebas; al evitar la ω-consistencia demuestra que la mera consistencia junto con la axiomatización efectiva basta para producir oraciones indecidibles en teorías formales.