Énoncé de Rosser

Une variante d'un énoncé de Gödel construite en utilisant l'astuce de Rosser qui affaiblit les hypothèses nécessaires pour l'incomplétude : elle donne un énoncé indécidable pour toute théorie consistante et récursivement énumérable sans exiger l'ω-consistance, en employant un prédicat de démontrabilité modifié comparant longueurs de preuve.