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.

Principe

Rosser remplace le prédicat standard de démontrabilité par une relation de démontrabilité à la Rosser qui affirme «il existe une preuve de moi et il n'existe pas de preuve plus courte de ma négation», ou utilise de manière équivalente un ordre de témoins pour éviter l'hypothèse plus forte d'ω-consistance de l'argument original de Gödel.

Démonstration

Pour une théorie T récursivement axiomatisable on définit un prédicat RProv_T(x) à la Rosser qui quantifie sur l'existence de contrespreuves plus courtes et on applique la diagonalisation pour produire une phrase R vérifiant T ⊢ (R ↔ ¬RProv_T(⌜R⌝)). Si T est simplement consistante, des arguments sur preuves minimales montrent que T ne peut ni prouver R ni ¬R, donc R est indécidable dans T.

Mauvaise application

Supposer que les énoncés de Rosser éliminent toute subtilité métamatématique : ils affaiblissent l'hypothèse d'ω-consistance à la simple consistance mais exigent toujours l'axiomatisation effective et une formalisation correcte des comparaisons de preuves ; ils ne rendent pas toutes les démonstrations d'incomplétude triviales ni n'effacent les distinctions modèle-théoriques.

Conséquence

Montre que l'incomplétude tient sous des hypothèses de consistance plus faibles et clarifie le rôle de la comparaison de preuves dans l'indécidabilité ; il affine le résultat de Gödel en abaissant la condition de consistance pour construire des énoncés indécidables.

Inversion

Si une théorie prouve l'énoncé de Rosser ou sa négation, l'analyse des preuves utilisée dans la construction Rosser conduit à une contradiction, de sorte que la démontrabilité de l'un ou l'autre révèle l'inconsistance sous les hypothèses de la construction.

Limite

S'applique aux théories récursivement énumérables (effectivement axiomatisées) qui peuvent formaliser la notion de preuve et les notions de longueur/comparaison de preuves ; il ne s'applique pas aux systèmes non effectifs ni aux formalismes incapables de représenter l'ordre requis des preuves.

Tension sémantique

Entre en concurrence avec l'énoncé de Gödel en échangeant la force des hypothèses et la simplicité du prédicat de démontrabilité : les énoncés de Rosser utilisent une machinerie de comparaison de preuves plus élaborée pour obtenir l'indécidabilité sous des hypothèses plus faibles, produisant des comportements techniques et interprétations métamatématiques différents.

Synthèse

Un énoncé de Rosser est une phrase autoréférentielle arithmétisée conçue via une notion de démontrabilité sensible à la comparaison des preuves ; en évitant l'ω-consistance il montre que la simple consistance plus l'axiomatisation effective suffisent à produire des énoncés indécidables dans les théories formelles.