Théorème de Gödel : Incomplétude des Systèmes Formels

Le théorème d’incomplétude de Gödel expliqué : pourquoi les mathématiques formelles ont des limites

En 1931, Kurt Gödel a démontré des limites fondamentales à tout système formel d’arithmétique suffisamment puissant. Ses théorèmes d’incomplétude établissent qu’il est impossible de construire un système cohérent capable de prouver toutes les vérités sur les nombres entiers naturels. Cette découverte a brisé le rêve d’une formalisation complète des mathématiques.

Une tendance unificatrice en science et en mathématiques

À la charnière des XIXᵉ et XXᵉ siècles, la science connaissait une forte tendance à l’unification. Newton a uni la gravité terrestre et la mécanique céleste. Maxwell a réduit l’électricité, le magnétisme et la lumière à un seul champ électromagnétique. Darwin a expliqué la diversité du vivant par la sélection naturelle.

Les mathématiciens ont poursuivi une synthèse similaire : déduire l’arithmétique, la géométrie et l’analyse à partir d’un seul ensemble d’axiomes. Frege proposait de définir les nombres via la théorie des ensembles :

• 0 = ∅ (l’ensemble vide)
• 1 = {∅}
• 2 = {∅, {∅}}

Le successeur d’un nombre n était défini comme la réunion de tous les nombres précédents — ce qui permettait de formaliser entièrement l’arithmétique. Mais le paradoxe de Russell a fait s’effondrer ce système : ses axiomes impliquaient une contradiction — la fameuse « classe de tous les ensembles qui ne se contiennent pas eux-mêmes ».

La crise des fondements et le programme de Hilbert

Le paradoxe de Russell a déclenché une crise des fondements en mathématiques. David Hilbert y a répondu avec un ambitieux programme de formalisation exigeant trois propriétés pour tout système axiomatique :

• La complétude (K) : le système prouve toute vérité arithmétique.
• La cohérence (K) : le système ne prouve jamais de faussetés.
• La décidabilité : il existe un algorithme permettant de déterminer si une affirmation donnée est prouvable ou non.

Hilbert exigeait que ces propriétés soient démontrées métamathématiquement — c’est-à-dire à l’aide d’un raisonnement fini et concret sur le système lui-même.

Principia Mathematica de Russell et Whitehead

Bertrand Russell et Alfred North Whitehead ont rédigé les Principia Mathematica (PM) — un système logique axiomatique assez puissant pour reconstruire l’ensemble des mathématiques. Ils ont reconstruit l’arithmétique depuis zéro, mettant plus de 300 pages à démontrer que 1 + 1 = 2.

Pour analyser PM, Gödel a simplifié sa syntaxe en un langage inspiré du Lisp-PM :

| Symbole | Signification | Exemple |

|---------|---------------|---------|

| 0 | zéro | 0 |

| next | successeur | (next 0) |

| + | addition | (+ 0 (next 0)) |

| | multiplication | ( 0 (next 0)) |

| = | égalité | (= 0 (* 0 (next 0))) |

Opérateurs logiques :

| Symbole | Signification | Exemple |

|---------|---------------|---------|

| not | négation | (not (= 0 1)) |

| or | disjonction | (or (= 0 1) (not (= 0 1))) |

| when | implication | (when 0 (or 0 1)) |

| there-is | quantificateur existentiel | (there-is x (= 4 (* x 2))) |

Les axiomes de PM incluaient des tautologies telles que :

• (when (or p p) p)
• (when p (or p q))
• La commutativité et l’associativité de la disjonction
• La règle du syllogisme

À partir de celles-ci, l’égalité et l’arithmétique ont été dérivées pas à pas.

La numérotation de Gödel : coder la syntaxe en nombres

Gödel a appliqué un codage à la Cantor pour associer à chaque formule un nombre entier naturel unique. Chaque symbole s’est vu attribuer un nombre de Gödel distinct, basé sur les nombres premiers :

| Symbole | Nombre de Gödel |

|---------|----------------|

| ( | 1 |

| ) | 3 |

| 0 | 5 |

| next | 7 |

| + | 9 |

| * | 11 |

| = | 13 |

| not | 15 |

| or | 17 |

| when | 19 |

| there-is | 21 |

| a, b, c, … | 2, 4, 6, … |

La formule (there-is a (= (next 0) a)) devient une suite de tokens ; son nombre de Gödel est alors calculé comme G = 2^g₁ × 3^g₂ × 5^g₃ × …, où chaque gᵢ est le nombre de Gödel du i-ième token. Cela établit une correspondance biunivoque parfaite entre formules et entiers naturels.

Fait crucial : l’arithmétique du Lisp-PM est exprimable en elle-même — longueur des formules, substitution et démontrabilité se ramènent toutes à des fonctions récursives primitives, rendant l’autoréférence possible.

Autoréférence et le théorème d’incomplétude

Gödel a construit une formule G affirmant sa propre improuvabilité : ∃p Proof(p, ⌜G⌝) — « Il n’existe aucun démonstration de numéro p de moi-même. »

Grâce au lemme diagonal (un théorème du point fixe) :

G ≡ ¬Provable(⌜G⌝)

Théorème 1 : Si PM est cohérent, alors G est vraie mais improuvable dans PM.

Théorème 2 : Si PM est cohérent, alors Con(PM) (l’affirmation de la cohérence de PM) est improuvable dans PM.

Points clés :

• Tout système interprétant l’arithmétique de Peano est incomplet.
• La cohérence d’un système ne peut pas être prouvée à l’intérieur de ce système.
• Les entiers naturels codent la syntaxe — ce qui rend l’autoréférence possible.
• Le programme de Hilbert est fondamentalement irréalisable.
• Vérité et démontrabilité ne sont pas équivalentes.

Conséquences pour l’informatique

Le théorème de Gödel est logiquement équivalent au problème de l’arrêt de Turing. Les systèmes formels possèdent des « zones aveugles » inhérentes. En programmation, cela se manifeste par :

• Des fonctions non calculables (ex. : un oracle hypothétique de l’arrêt).
• Des « bombes logiques » intégrées aux outils de vérification.
• Des limites strictes à la vérification formelle des logiciels.

Les assistants de preuve modernes (Coq, Lean) reconnaissent explicitement cette incomplétude — ils reposent sur des axiomes fiables plutôt que de prétendre à une certitude absolue.

— Editorial Team