Théorème de Löb

En logique mathématique, le théorème de Löb, démontré par Martin Hugo Löb (1921-2006), est une variante du second théorème d'incomplétude de Gödel. Il dit que pour toute théorie T satisfaisant les conditions de ce dernier — l'arithmétique de Peano par exemple — pour toute formule P, s'il est démontrable dans T que « si P est démontrable dans T alors P », alors P est démontrable dans T. En d'autres termes : si , alors où DemT(⌈P⌉) est une formule qui exprime que la formule P, de numéro de Gödel ⌈P⌉, est démontrable dans T. En résumé, l'hypothèse qu'un énoncé est démontrable dans une théorie donnée n'aide en rien à la démonstration de cet énoncé dans cette même théorie. Les théories auxquelles s'applique le théorème de Löb sont les mêmes que celles auxquelles s'applique le second théorème d'incomplétude : des théories arithmétiques (ou capables de représenter l'arithmétique) et qui peuvent représenter les démonstrations et leur combinatoire, comme l'arithmétique de Peano, et a fortiori les théories des ensembles usuelles, mais aussi une théorie arithmétique faible comme l'. Martin Löb publie le théorème et sa démonstration en 1955 dans un article en réponse à la question posée en 1952 par du statut dans une certaine théorie d'une formule (close) exprimant sa propre prouvabilité dans la même théorie : est-elle démontrable ou non dans ? Une telle formule existe, par le lemme de diagonalisation dont se sert Gödel dans sa démonstration du premier théorème d'incomplétude : Gödel l'utilise pour construire une formule équivalente à sa propre non-prouvabilité. On peut reformuler la question de Henkin comme celle de la prouvabilité dans une théorie arithmétique des énoncés tels que: DemT(⌈A⌉) ↔ A, Löb démontre qu'un tel énoncé est forcément prouvable dans . Il s'avère qu'au passage Löb démontre un énoncé bien plus général, qui est le théorème aujourd'hui appelé théorème de Löb, et qui apparaît dans l'article de 1955. Cependant Löb attribue cet énoncé, et la remarque qu'il a de fait démontré celui-ci, à un relecteur anonyme de la soumission.