##  [Enunciado de Rosser](/es/node/60106) 

 Definición

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

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

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

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

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

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

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

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

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.