Théorème de Löb

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 Leon Henkin (en) du statut dans une certaine théorie T d'une formule (close) exprimant sa propre prouvabilité dans la même théorie T : est-elle démontrable ou non dans T ? 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 T des énoncés A tels que[2]:

Löb démontre qu'un tel énoncé est forcément prouvable dans T. 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. Il s'avère que ce relecteur était Henkin. L'histoire est racontée par Smoryński[3] - [4].

Le second théorème d'incomplétude de Gödel est simplement le cas particulier du théorème de Löb obtenu en considérant la formule 0 = 1 (ou toute autre formule absurde). En effet Dem_T(⌈0 = 1⌉)→ 0 = 1 exprime bien que 0 = 1 n'est pas démontrable, c'est-à-dire la cohérence de la théorie T, et le théorème de Löb énonce alors que si celle-ci est démontrable, alors 0 = 1 est démontrable, c'est-à-dire que la théorie est contradictoire : c'est exactement le second théorème d'incomplétude de Gödel.

Réciproquement on déduit assez directement le théorème de Löb du second théorème d'incomplétude de Gödel grâce à un raisonnement par l'absurde. Il suffit de remarquer que la démontrabilité de A dans la théorie T équivaut à la non cohérence de la théorie T + ¬A, et que cette équivalence se démontre dans la théorie T (sous les hypothèses déjà nécessaires pour le théorème), c'est là où intervient le raisonnement par l'absurde. Ainsi :

Si Dem_T(⌈A⌉) → A est démontrable dans T, alors dans la théorie T+ ¬A, on démontre ¬ Dem_{T+ ¬A}(⌈0=1⌉), c'est-à-dire la cohérence de cette théorie. La théorie T+ ¬A est donc contradictoire par le second théorème d'incomplétude, et donc A est démontrable dans T.

Löb démontre directement son théorème à partir des conditions de démontrabilité de Hilbert-Bernays[5].

La logique de la démontrabilité s'abstrait des détails de l'encodage utilisé dans le théorème d'incomplétude de Gödel, exprimant la notion de démontrabilité de ${\displaystyle \phi }$ dans un système donné dans le langage de la logique modale, par le biais d'une modalité ${\displaystyle \Box }$. La construction ${\displaystyle \Box }$${\displaystyle \phi }$ se lit « la formule ${\displaystyle \phi }$ est démontrable ».

Dans ce cadre, on peut formaliser le théorème de Löb par l'axiome suivant, connu sous le nom d'axiome GL, pour Gödel-Löb :

${\displaystyle \Box (\Box P\rightarrow P)\rightarrow \Box P}$,

On peut aussi formaliser le théorème de Löb sous la forme d'une règle d'inférence :

${\displaystyle {\frac {\Box P\rightarrow P}{\Box P}}}$

La logique GL de la démontrabilité, résultant de l'ajout de l'axiome GL à une logique modale K4, est le système de logique de démontrabilité le plus étudié.