Chapitre 4, section 5 : Théorème de Gödel

Annexe : arithmétique du premier ordre (FAQ).

Question. Je ne comprends pas ce qu'est une formule logique en arithmétique ; par exemple il me semble absurde de dire que x + y est vrai ou faux.

Réponse. Exact, x + y n'est pas une formule logique, c'est un terme. Voici la définition rigoureuse des formules logiques :

Les symboles '+' et '*' (addition et multiplication) sont des symboles de fonctions, et permettent de construire des termes. Le symbole '=' (égalité) est le seul symbole de prédicat, et permet de construire des formules logiques ; seules les formules logiques sont vraies ou fausses, pas les termes.

Question. La formule "p est premier" n'est ni démontrable ni réfutable, cela dépend de p. Voici une démonstration pas chère du théorème de Gödel.

Réponse. Non, dans le théorème de Gödel, proposition signifie formule close (c'est-à-dire sans variable libre). Noter qu'il existe des formules non closes démontrables, par exemple a + b = b + a, mais dans ce cas la formule est équivalente à sa clôture obtenue en ajoutant ∀ab en tête de la formule.

Question. Puisqu'on peut coder la fonction exponentielle avec une formule qui utilise les opérateurs '+' et '*', pourquoi ne pas coder de la même façon la multiplication à l'aide de '+', et l'addition à l'aide de la fonction successeur ?

Réponse. C'est impossible. Le codage décrit section 5.3 utilise les nombres premiers (nous n'avons pas donné les détails) pour coder les listes, ce qui suppose que l'on dispose déjà de l'opérateur de multiplication.

L'arithmétique de Peano privée du symbole de multiplication (et donc des axiomes à son sujet), est appelée arithmétique de Presburger, et son principal intérêt est d'être un exemple de théorie non triviale et complète : toutes les propositions sont démontrables ou réfutables. Il est donc certainement impossible de définir la multiplication à partir de l'addition en logique du premier ordre. On peut montrer qu'il est de même impossible de définir l'addition à partir de la fonction successeur.

Il existe d'autres formalismes logiques, en particulier l'arithmétique du second ordre (voir ci-dessous) et le λ-calcul, qui permettent de définir l'addition et la multiplication ; mais en arithmétique du premier ordre, ce sont des symboles constitutifs du langage, avec leurs axiomes.

Question. Existe-t-il une théorie appelée arithmétique du second ordre, et quelles sont les différences avec l'arithmétique du premier ordre ?

Réponse. Oui. En arithmétique du second ordre il existe une classe supplémentaire de formules logiques, qui permettent d'énoncer des propriétés sur les formules (prédicats) du premier ordre ; en particulier une formule du second ordre peut comporter des quantificateurs ∀P et ∃P, où P désigne un prédicat. On peut donc énoncer un (unique) axiome de récurrence, au lieu d'utiliser un axiome différent pour chaque prédicat P, comme on le fait en arithmétique du premier ordre :

P . [ P (0) ∧ ∀x . P (x) ⇒ P (x + 1) ] ⇒ ∀x P (x)

En un sens l'arithmétique du second ordre est plus simple. Mais un prédicat P (x) correspond à un ensemble d'entiers E : xE si et seulement si la formule P (x) est vraie (cf. définition de la fonction caractéristique d'un ensemble).

Une théorie d'ordre deux permet donc de manipuler les ensembles, et repose sur le développement préalable d'une théorie formelle des ensembles. Au contraire, l'arithmétique du premier ordre est une théorie formelle de l'arithmétique, qui évite le recours à une théorie des ensembles.

Question. L'arithmétique du premier ordre est-elle une théorie aussi puissante que l'arithmétique du second ordre ?

Réponse. Pas tout à fait. Il y a deux différences principales :

Question. Le théorème de Gödel est un théorème technique concernant l'arithmétique du premier ordre, il suffit d'utiliser une "bonne" théorie de l'arithmétique pour qu'il disparaisse ?

Réponse. Non. Le théorème de Gödel est vrai dans toute théorie formelle assez puissante pour décrire l'arithmétique. L'arithmétique du premier ordre est en quelque sorte une théorie minimale, qui suffit pour que le paradoxe apparaisse.

Question. Pourquoi existe-t-il plusieurs systèmes de preuves ? J'ai toujours entendu dire qu'il n'existe que deux règles de déduction, le modus ponens (de A et AB on peut déduire B ), et la généralisation (de P (x) on peut déduire x P (x) ).

Réponse. Le système avec deux règles de déduction est le plus connu pour des raisons historiques ; on l'appelle système de Hilbert. Il est simple, mais les preuves qu'il produit sont particulièrement illisibles. Les logiciens, puis les informaticiens, ont mis au point des systèmes plus complexes, mais plus utiles et efficaces en pratique. On utilise surtout des systèmes dérivés des systèmes de séquents : un séquent comporte à la fois des hypothèses (prémisses) et des formules déductibles de ces hypothèses ; les règles de déduction permettent d'enchaîner les séquents, au lieu d'enchaîner simplement des formules. Voir les cours de logique propositionnelle et de logique du premier ordre, par Jean Goubault-Larrecq.

Question. Je voudrais voir une formule arithmétique qui ne soit ni démontrable, ni réfutable ; est-ce possible ?

Réponse. Oui. Il ne faut pas confondre cette question avec celle de construire une procédure indécidable, qui n'a pas de sens. Hélas, les formules ni démontrables, ni réfutables, sont appelées indécidables par certains auteurs, et l'on n'y comprend plus rien ; pour éviter une confusion de terminologie aussi catastrophique, on les appelle ici irrésolubles, mais l'usage de ce terme, dans ce contexte, est loin d'être universel.

Il y a plusieurs méthodes pour construire des formules irrésolubles :

Les théorèmes qu'on peut démontrer en arithmétique du second ordre, mais pas en arithmétique du premier ordre (voir ci-dessus), sont eux aussi irrésolubles, mais seulement dans le cadre de l'arithmétique du premier ordre. Les méthodes précédentes sont au contraire valables pour toute théorie formelle de l'arithmétique.

Question. En quoi consiste le paradoxe du menteur ?

Réponse. Si quelqu'un dit "en ce moment, je mens", il est difficile de savoir si cette affirmation est vraie ou fausse ! Dans les deux cas, on aboutit à une contradiction.

Gödel n'a pas suivi exactement la voie décrite section 5.3 pour démontrer son théorème ; celle-ci est postérieure de quelques années, et est due à ses contemporains, en particulier Church et Turing. Au lieu de coder les procédures informatiques, dont le concept commençait seulement à émerger, Gödel a codé directement par des formules arithmétiques les preuves formelles (celles qu'on peut écrire en arithmétique du premier ordre). Puis il a montré qu'on peut construire des formules Φ qui "parlent" d'elles-mêmes (le principe est le même que celui des procédures récursives) : Φ énonce une propriété … de Φ. Il a pu alors formaliser le paradoxe du menteur, en construisant une formule M qui énonce que … M n'est pas démontrable (le principe est le même que celui des procédures contradictoires construites pour prouver le théorème de Rice). Par construction, M n'est ni démontrable, ni réfutable.

Question. Peut-on dire d'une formule irrésoluble (c'est-à-dire ni démontrable ni réfutable) qu'elle n'est ni vraie ni fausse ?

Réponse. Non, du moins si l'on veut conserver le principe du tiers exclu, qui est l'un des axiomes de la logique classique (par opposition, la logique privée de ce principe est dite constructive, ou intuitionniste).

Une formule irrésoluble peut être "déclarée vraie", c'est-à-dire ajoutée comme axiome ; ou "déclarée fausse" : dans ce cas on ajoute sa négation comme axiome. Dans le premier cas, on est sûr de ne pas introduire de contradiction dans la théorie (par exemple dans l'arithmétique du premier ordre), puisque la formule n'est pas réfutable ; idem dans le second cas, puisque la formule n'est pas démontrable.

Des paradoxes peuvent apparaître : par exemple si Φ est irrésoluble en arithmétique du premier ordre, mais démontrable en arithmétique du second ordre, ajouter ¬Φ comme axiome à l'arithmétique du premier ordre produit certainement une théorie curieuse : c'est le paradoxe des modèles non standard de l'arithmétique du premier ordre, et tout un livre leur est consacré (Richard Kaye, Models of Peano Arithmetic).

Idem pour la formule M qui traduit le paradoxe du menteur, et "affirme" : M n'est pas démontrable. Elle semble nécessairement vraie, sinon elle devient démontrable, contradiction. Mais alors ne vient-on pas de démontrer M ? Pour s'en sortir, il faut :

  1. examiner soigneusement ce que veut dire que M "affirme" (ou "énonce") qu'elle n'est pas démontrable (cf. Podnieks, références ci-dessous) ;

  2. énoncer plus rigoureusement le théorème d'incomplétude de Gödel, qui dit en fait que toute théorie formelle de l'arithmétique est incomplète (il existe des formules irrésolubles), ou alors contradictoire ;

  3. tenir compte du second théorème de Gödel, qui, en étudiant soigneusement ses propres constructions (il était bien placé pour cela), en a déduit qu'une théorie formelle de l'arithmétique ne peut jamais prouver sa propre non-contradiction ; autrement dit la formule qui énonce :

    " il n'existe pas de démonstration de 0 = 1 "

    est indémontrable. C'est un nouvel exemple de formule irrésoluble "explicite".

Pour en savoir plus