ATLAS
Ouvrir dans l'atlas →Théorème 4Lemme diagonal et démontrabilité
Théorème de Löb et second théorème d'incomplétude sous les conditions de dérivabilité
Soit une théorie qui contient , et une formule dont les variables libres sont parmi une variable . Pour un énoncé , on note l'énoncé , où est le chiffre du code de , et l'énoncé . La formule satisfait dans les conditions de dérivabilité si, pour tous énoncés et :
(D1) si , alors ;
(D2) ;
(D3) .
On note l'énoncé .
Si les axiomes de forment un ensemble récursivement énumérable, toute formule de démontrabilité pour satisfait (D1), par le point (ii) du nœud Démontrabilité (D1). Le second théorème d'incomplétude fait mener à elle-même le raisonnement du point (i) du premier théorème, « si démontrait , elle serait incohérente » (Premier théorème (Gödel)) ; les conditions (D2) et (D3) sont ce qu'il faut pour cela.
Soit une théorie qui contient , et une formule qui satisfait dans les conditions de dérivabilité.
(i) Théorème de Löb. Pour tout énoncé , si , alors .
(ii) Second théorème d'incomplétude. Si est cohérente, alors .
Démonstration
(i) Le lemme diagonal, appliqué à la formule , dont les variables libres sont parmi puisque est un énoncé, donne un énoncé tel que . Notons l'énoncé . La règle des tautologies donne , et (D1) donne . Deux applications de (D2), la première aux énoncés et , la seconde à et , donnent et (D3), appliquée à , donne . La règle des tautologies enchaîne ces trois formules : . Avec l'hypothèse , il vient , puis par l'équivalence qui définit . Alors (D1) donne , et le modus ponens donne .
(ii) Si , l'instance donne , et (i) donne . Comme (Égalité démontrable, (i)), démontrerait une formule et sa négation, ce qui est exclu.
□Au contraire de (D1), satisfaite par toute formule de démontrabilité, les conditions (D2) et (D3) portent sur la façon dont la formule est écrite, comme le montre la remarque suivante. Pour la formule naturelle, qui transcrit dans l'arithmétique la définition des démonstrations formelles à partir d'une formule qui définit les axiomes, (D2) revient à démontrer dans l'arithmétique de Peano que deux démonstrations mises bout à bout et suivies d'un modus ponens en forment une, et (D3) à démontrer à l'intérieur de l'arithmétique de Peano la Σ₁-complétude, appliquée à l'énoncé Σ₁ . Le point (ii) du nœud Incomplétude repose sur ces deux démonstrations, que ce chapitre ne contient pas : (D2) est démontrée au nœud Deuxième condition (D2), et (D3) au nœud Troisième condition (D3), qui en tire ce théorème pour la formule naturelle.
La façon d'écrire la formule compte. Soit une théorie cohérente qui contient et dont les axiomes forment un ensemble récursivement énumérable, une formule de démontrabilité pour , et . La formule est encore une formule de démontrabilité pour : la conjonction est Δ₀, et elle définit le même ensemble, puisque . Mais : de , la règle des tautologies tire , la généralisation en donne la formule universelle correspondante, et la règle des tautologies conclut, puisque . Par (ii), ne satisfait donc pas à la fois (D2) et (D3) dans , alors qu'elle satisfait (D1). L'erreur la plus répandue est de parler de « l'énoncé qui exprime la cohérence de » comme s'il n'y en avait qu'un : le second théorème porte sur un énoncé écrit d'une façon déterminée.
Le théorème de Löb répond à une question posée par Leon Henkin en 1952 (problème 3, Journal of Symbolic Logic 17, 1952, p. 160) : un énoncé qui affirme sa propre démontrabilité, , est-il démontrable ? Oui, puisque . La réponse est de M. H. Löb (« Solution of a problem of Leon Henkin », Journal of Symbolic Logic 20, 1955, p. 115-118), à qui l'on doit aussi la condition (D3) sous cette forme. Les conditions de dérivabilité remontent à D. Hilbert et P. Bernays (Grundlagen der Mathematik, vol. 2, Berlin, Springer, 1939), qui ont donné la première démonstration détaillée du second théorème ; Gödel (1931, théorème XI) n'en avait publié qu'une esquisse.