Enunciado de Rosser

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.