Théorème de Löb

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

En logique mathématique, le théorème de Löb, démontré par Martin Hugo Löb (de) (1921-2006), est une variante du second théorème d'incomplétude de Gödel[1]. 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ödelP⌉, 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'arithmétique primitive récursive.

Histoire[modifier | modifier le code]

L'article de Martin Löb contient effectivement l'énoncé du théorème de Löb. Mais il semble que cette contribution soit attribué à un relecteur anonyme de la soumission. Il s'avère que ce relecteur était Henkin. L'histoire est raconté par Smoryński[2],[3].

Théorème de Löb et théorème de Gödel[modifier | modifier le code]

Le second théorème d'incomplétude de Gödel se démontre à partir du théorème de Löb en considérant la formule 0 = 1 (ou toute autre formule absurde). En effet DemT(⌈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 le théorème de Löb à partir du second théorème d'incomplétude de Gödel. 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) à l'aide du raisonnement par l'absurde. Ainsi :

DemT(⌈A⌉) ≡T DemT+ ¬A(⌈0=1⌉) .

Si DemT(⌈A⌉) → A est démontrable dans T, alors dans la théorie T+ ¬A, on démontre ¬ DemT+ ¬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.

Le théorème de Löb en logique de la démontrabilité[modifier | modifier le code]

La logique de la démontrabilité (en) 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 dans un système donné dans le langage de la logique modale, par le biais d'une modalité . La construction se lit "la formule est démontrable".

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

,

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

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é[réf. nécessaire].

Référence[modifier | modifier le code]

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Löb's theorem » (voir la liste des auteurs).

  1. M. H. Löb, « Solution of a problem of Leon Henkin1 », The Journal of Symbolic Logic, vol. 20, no 2,‎ , p. 115–118 (ISSN 0022-4812 et 1943-5886, DOI 10.2307/2266895, lire en ligne)
  2. (en) C. Smoryński, The Development of Self-Reference: Löb’s Theorem, Birkhäuser Boston, (DOI 10.1007/978-0-8176-4769-8_9, lire en ligne), p. 110–133
  3. Panu Raatikainen, The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University, (lire en ligne)

Voir aussi[modifier | modifier le code]

Liens externes[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

(en) Peter G. Hinman, Fundamentals of Mathematical Logic, Wellesley, A K Peters, (ISBN 978-1-56881-262-5, LCCN 2005050968)