ChapitreCalculabilité

Lemme diagonal et démontrabilité

Une relation représentée dans l'arithmétique de Robinson ne suffit pas à parler d'une fonction : il faut encore que la théorie démontre que la valeur est unique. Le plus petit témoin y pourvoit, et toute fonction récursive totale devient représentable. Appliquée à la fonction qui substitue à une variable d'une formule le chiffre de son propre code, cette représentation donne le lemme diagonal : pour toute propriété des codes exprimée par une formule, il existe un énoncé que l'arithmétique de Robinson démontre équivalent à l'assertion que son propre code a cette propriété.

Trois conséquences s'en tirent aussitôt. La vérité arithmétique n'est pas définissable dans le langage de l'arithmétique (Tarski). L'énoncé qui dit de lui-même qu'il n'est pas démontrable n'est pas démontrable si la théorie est cohérente, et il n'est pas réfutable si elle est $\omega$-cohérente (Gödel). Enfin, toute formule qui satisfait les trois conditions de dérivabilité de Hilbert, Bernays et Löb conduit au théorème de Löb et au second théorème d'incomplétude ; la première de ces conditions est démontrée ici pour toute théorie qui contient l'arithmétique de Robinson et dont les axiomes forment un ensemble récursivement énumérable ; les deux autres demandent de raisonner dans l'arithmétique de Peano sur ses propres démonstrations.