ChapitreCalculabilité

Représentation dans l'arithmétique de Robinson et théorème de Gödel-Rosser

L'arithmétique de Robinson, qui n'a pas de schéma de récurrence, démontre pourtant tous les énoncés vrais d'une forme simple : ceux qui ne contiennent que des quantificateurs bornés, puis ceux qui s'obtiennent à partir d'eux par des quantificateurs existentiels, les énoncés $\Sigma_1$. Comme tout ensemble récursivement énumérable se définit par une telle formule, deux ensembles récursivement énumérables disjoints se séparent par une formule que l'arithmétique de Robinson démontre sur les éléments du premier et réfute sur ceux du second : c'est l'astuce de Rosser, et elle donne la représentation des relations récursives.

Appliquée à une paire d'ensembles récursivement énumérables qu'aucun ensemble récursif ne sépare, elle démontre le premier théorème d'incomplétude sous la seule hypothèse de cohérence : une théorie cohérente qui contient l'arithmétique de Robinson n'a pas d'ensemble de théorèmes récursif, et, si ses axiomes forment un ensemble récursivement énumérable, elle n'est pas complète. Tout y est démontré dans le système formel de la logique, sans lemme diagonal ni théorème de Craig.