David Madore's WebLog: Une version de Gödel sur l'inséparabilité des théorèmes et antithéorèmes

Index of all entries / Index de toutes les entréesXML (RSS 1.0) • Recent comments / Commentaires récents

Entry #2410 [older|newer] / Entrée #2410 [précédente|suivante]:

(mardi)

Une version de Gödel sur l'inséparabilité des théorèmes et antithéorèmes

(Le mot antithéorème, dans le titre et dans ce qui suit, désigne un énoncé P dont la négation logique, que je note ¬P, est un théorème, i.e., un énoncé réfutable alors qu'un théorème désigne un énoncé démontrable. Si vous avez du mal à distinguer vrai/faux de théorème/antithéorème, vous pouvez réviser ici.)

Je fais de temps en temps des remarques sur le théorème de Gödel (par exemple ici), il semble que ce soit un sujet dont on n'arrête pas d'extraire du jus. J'ai fait une remarque à ce sujet récemment sur MathOverflow, je me dis qu'elle pourrait intéresser mes lecteurs, donc je vais tenter de l'expliquer. Je vais essayer de reléguer les détails ou les complément un peu plus techniques à plein de notes : ceux qui veulent juste the big picture peuvent ignorer ces notes (et, dans tous les cas, il vaut peut-être mieux les garder pour une seconde lecture). Pour ceux qui veulent vraiment juste the bottom line, j'explique ici, en utilisant un tout petit peu de calculabilité, pourquoi il existe non seulement des énoncés indémontrables et irréfutables (i.e., « logiquement indécidables »), mais même de tels énoncés dont l'indémontrabilité et l'irréfutabilité sont elles-mêmes indémontrables (i.e., « logiquement indécidablement indécidables »). J'avoue qu'il y a un peu plus de subtilités dans tous les sens que ce que je pensais (i.e., beaucoup de notes), mais j'espère qu'on peut quand même en retenir quelque chose sans comprendre tous les détails.

La clé de tout ça, c'est de méditer sur la manière dont un algorithme (i.e., une machine de Turing) peut séparer les théorèmes et les antithéorèmes, ou le vrai et le faux — en gros, montrer qu'il ne peut pas, même pas en un sens assez faible.

Voici un premier fait : il est possible de produire un algorithme (i.e., une machine de Turing) qui, quand on lui donne un énoncé mathématique P, termine en répondant oui lorsque P est un théorème, et termine en répondant non lorsque P est un antithéorème (i.e., ¬P est un théorème). Il suffit, pour cela, d'énumérer toutes les démonstrations mathématiques possibles (par exemple en énumérant toutes les suites de symboles possibles, en vérifiant pour chacune s'il s'agit d'une démonstration conforme aux règles de la logique, tout ceci étant faisable algorithmiquement), et si on tombe sur une démonstration de P, on s'arrête et on répond oui, tandis que si on tombe sur une démonstration de ¬P, on s'arrête et on répond non. Je n'ai pas précisé dans quel système axiomatique je me place, cela pourrait être, par exemple, l'arithmétique de Peano [du premier ordre] PA ou la théorie des ensembles ZFC (mais dans ce cas, il faudra la supposer cohérente, ce que ZFC lui-même ne peut pas prouver, sans quoi tout énoncé serait à la fois théorème et antithéorème ce qui n'est pas bien intéressant). Bien sûr, tout cela est complètement théorique (dans la vraie vie, la démonstration automatisée ne sert que dans des théories extrêmement étroites, pas pour des énoncés mathématiques « généraux »). Mais le point théorique à souligner, c'est que l'algorithme que je viens de décrire ne termine pas si P n'est ni un théorème ni un antithéorème (i.e., s'il est logiquement indécidable dans la théorie considérée) : la contrainte est seulement que si P est un théorème, l'algorithme termine en répondant oui, et si ¬P est un théorème, l'algorithme termine en répondant non.

Voici un deuxième fait : il n'est pas possible de faire un algorithme (i.e., une machine de Turing) qui, quand on lui donne un énoncé mathématique P, termine en répondant oui lorsque P est vrai, et termine en répondant non lorsque P est faux (i.e., ¬P est vrai). En fait, ce n'est même pas possible si on se limite[#] à ce que P soit un énoncé arithmétique (c'est-à-dire, qui ne parle que d'entiers : voir ici pour une petite discussion) ; ni même si on se limite encore plus à ce que P soit un énoncé arithmétique Π₁ (c'est-à-dire un énoncé de la forme pour tout entier naturel n, on a Q(n), où Q, lui, est arithmétique et algorithmiquement testable en temps fini pour chaque n donné ; voir ici pour une discussion). La démonstration de ce deuxième fait est facile si on connaît un tout petit peu de calculabilité, plus exactement, l'indécidabilité algorithmique du problème de l'arrêt : si un algorithme comme je décrit ci-dessus (i.e., capable de dire si un énoncé est vrai ou faux) existait, il serait notamment capable de dire si l'énoncé <tel algorithme> ne termine pas quand on le lance sur <telle entrée> est vrai ou faux (ceci est bien un énoncé arithmétique, et il est même arithmétique Π₁), et du coup, de résoudre algorithmiquement le problème de l'arrêt.

[#] À vrai dire, si je ne mets pas une restriction de ce genre, c'est encore pire : on ne peut même pas énoncer formellement ce que ça voudrait dire d'avoir un algorithme qui répond oui ou non selon que l'énoncé est vrai ou faux.

Quand on met ensemble les deux faits que je viens de dire, on obtient le théorème de Gödel : en effet, s'il est possible de faire un algorithme qui répond oui sur les théorèmes et non sur les antithéorème, et impossible de faire un algorithme qui répond oui sur les énoncés vrais et non sur les énoncés faux, c'est forcément que les deux concepts ne sont pas identiques !, et donc, si tant est que tous les théorèmes de la théorie sont bien vrais (ou au moins les théorèmes arithmétiques, ou au moins[#2] les théorèmes arithmétiques Σ₁), il y a forcément des énoncés vrais, et même forcément des énoncés arithmétiques Π₁ vrais[#3], mais qui ne sont pas des théorèmes. C'est le théorème de Gödel, et c'est d'ailleurs peut-être la manière la plus simple de le voir. La construction peut être rendue explicite (car l'indécidabilité du problème de l'arrêt l'est). Je crois que cette façon de démontrer le théorème de Gödel était une motivation importante pour Turing dans l'étude du problème de l'arrêt.

[#2] Un énoncé arithmétique Σ₁ est la négation d'un énoncé arithmétique Π₁, c'est-à-dire qu'il est de la forme il existe un entier naturel n tel qu'on ait Q(n)Q est testable. Une propriété intéressante de ces énoncés arithmétiques Σ₁ est que s'ils sont vrais (i.e., s'il existe un tel entier naturel), alors ils sont automatiquement démontrables (dans toute théorie contenant un fragment ridiculement faible de l'arithmétique), puisqu'il suffit d'exhiber le n et de constater qu'il marche. • L'hypothèse réciproque, à savoir que tout théorème arithmétique Σ₁ de la théorie est vrai, s'appelle la Σ₁-correction (soundness en anglais), ou simplement 1-correction. C'est une hypothèse un peu plus faible que la ω-cohérence que Gödel a supposée dans son papier (et dont je ne vais pas expliquer le sens précis), mais plus forte que la cohérence. • Pour ce qui est des énoncés arithmétiques Π₁, en revanche, la simple cohérence d'une théorie (contenant un minimum d'arithmétique) suffit à garantir que les théorèmes arithmétiques Π₁ sont vrais : car si ∀n.Q(n) est faux, c'est que ∃nQ(n) est vrai, or je viens d'expliquer qu'il est alors forcément démontrable, c'est-à-dire que ∀n.Q(n) est un antithéorème, et il ne peut pas être un théorème puisque la théorie était supposée cohérente.

[#3] Un peu plus précisément : comme tout énoncé arithmétique Σ₁ vrai est un théorème (note précédente), et comme on a fait l'hypothèse que tout théorème arithmétique Σ₁ est vrai, c'est que vrai et théorème sont synonymes pour les énoncés arithmétique Σ₁, i.e., faux et antithéorème sont synonymes pour les énoncés arithmétiques Π₁ ; et comme l'algorithme qui répond oui sur les théorèmes arithmétiques Π₁ et non sur les antithéorèmes arithmétiques Π₁ (=les énoncés arithmétiques Π₁ faux), ne peut pas distinguer parfaitement le vrai et le faux, il y a forcément un énoncé arithmétique Π₁ vrai qui n'est pas un théorème.

Bon, c'est intéressant, mais on peut faire mieux.

Posons-nous la question de savoir si on peut renforcer le premier fait : au lieu de vouloir simplement que mon algorithme termine en répondant oui lorsque P est un théorème, et termine en répondant non lorsque P est un antithéorème (i.e., ¬P est un théorème), je vais vouloir, en plus, qu'il termine toujours. Autrement dit, je veux un algorithme qui, quand on lui donne un énoncé P (peut-être seulement arithmétique, voire arithmétique Π₁), termine toujours, et réponde oui lorsque P est un théorème et non lorsque P est un antithéorème. Remarquez que si P n'est ni l'un ni l'autre, j'accepte que mon algorithme réponde n'importe quoi (soit oui, soit non, soit pouêt, soit 42, peu importe), mais il doit toujours terminer. Est-ce possible ? Non (au moins sous l'hypothèse que la théorie sur laquelle je travaille contient l'arithmétique de Peano PA ; par exemple, cela fonctionne pour PA lui-même et pour ZFC — en fait, même des théories beaucoup plus faibles que PA suffiraient).

Je répète ça comme troisième fait :

Il n'existe pas d'algorithme qui, quand on lui donne un énoncé mathématique P, ou même simplement un énoncé arithmétique Π₁, (1) termine toujours, et ce (2) en répondant oui lorsque P est un théorème, et (3) en répondant non lorsque P est un antithéorème (i.e., ¬P est un théorème).

Tout ceci se comprenant pour une théorie contenant PA.

Je veux maintenant expliquer pourquoi ce troisième fait est vrai (i.e., en esquisser une démonstration), et expliquer pourquoi il conduit à des conséquences qui généralisent le théorème de Gödel, et notamment à l'existence d'énoncés logiquement indécidablement indécidables (ou même plus).

Comment montrer ce troisième fait ? Il faut partir[#3b] de l'existence d'ensembles récursivement énumérables et récursivement inséparables : cela signifie qu'il existe deux machines de Turing (=algorithmes) A₁ et A₂ qui énumèrent[#4] des ensembles respectivement S₁ et S₂, tels que ces ensembles soient disjoints (S₁∩S₂=∅), et que de plus, il n'existe pas de machine de Turing U qui termine toujours, répond 1 sur les entiers de S₁ (i.e., énumérés par A₁) et 2 sur ceux de S₂ (i.e., énumérés par A₂) (sur les entiers qui ne sont ni dans S₁ ni dans S₂, la machine U peut répondre ce qu'elle veut). L'existence de S₁ et S₂ est un résultat standard de la calculabilité et se démontre de façon semblable à l'indécidabilité algorithmique du problème de l'arrêt, je vais donner les détails en note[#5]. J'aurai aussi besoin du fait que l'arithmétique de Peano PA démontre que S₁ et S₂ sont disjoints, ce qui ne pose pas de problème particulier (la démonstration que je donne en note fonctionne parfaitement bien dans PA).

[#3b] (Ajout) Comme jonas me le signale en commentaire (), on peut condenser un peu la démonstration et prouver directement le « troisième fait » en construisant, si V est une machine qui (au moins sur les énoncés Π₁) termine toujours, renvoie oui sur un théorème et non sur un antithéorème, l'énoncé P qui affirme V lancée sur P ne termine pas en répondant oui (si V lancée sur P ne termine pas, cela contredit (1), si elle termine en répondant oui alors une trace de ce fait réfute P, donc P est un antithéorème et ceci contredit (3), et si elle termine en répondant non alors une trace de ce fait le prouve, et un système très faible suffit à réfuter le fait qu'elle termine en répondant oui, donc P est un théorème et ceci contredit (2)).

[#4] Dire que A énumère S signifie que A crache une liste d'entiers S : par exemple on peut imaginer que l'algorithme tourne en continu et de temps en temps produit un nombre, et que S est l'ensemble de tous ces nombres, ou bien que l'algorithme prend en entrée un entier et en revoie un autre et que S est l'ensemble des entiers qui peuvent être renvoyés, ça n'a pas d'importance.

[#5] Voici comment on peut faire : soit S₁ l'ensemble des entiers e tels que la e-ième machine de Turing, quand on la lance sur l'entier e, termine et renvoie 2, et soit S₂ l'ensemble des entiers e tels que la e-ième machine de Turing, quand on la lance sur l'entier e, termine et renvoie 1. Il est clair que S₁ et S₂ sont disjoints (une machine ne peut pas à la fois renvoyer 1 et 2). Pour montrer qu'ils sont récursivement énumérables, plus exactement énumérés par des machines A₁ et A₂, on construit la machine A₁ qui exécute de façon déployée toutes les machines de Turing en lançant chacune sur l'argument donné par son propre numéro, et dès qu'une machine e (exécutée sur e) termine en renvoyant 2, la machine A₁ énumère ce e ; tandis que A₂ fait pareil pour les machines qui terminent en renvoyant 1. Enfin, s'il existait une machine U qui, quand on lui fournit un entier k, termine toujours en renvoyant 1 lorsque kS₁ et 2 lorsque kS₂, on voit qu'on peut facilement modifier U pour ajouter l'hypothèse qu'elle renvoie toujours soit 1 soit 2 (il suffit de la modifier pour renvoyer 2 dès qu'elle renvoie autre chose que 1) ; cette machine a un numéro, disons e, et si on exécute U sur e lui-même, elle doit terminer et renvoyer 1 ou 2 : mais si elle renvoie 1, la définition de S₂ signifie que eS₂, auquel cas la définition de U implique qu'elle doit renvoyer 2, une contradiction, et on a de même une contradiction dans l'autre cas. C'est donc que U ne peut pas exister.

Une fois acquise l'existence de A₁ et A₂ énumérant des ensembles S₁ et S₂ récursivement inséparables comme je viens de le définir, on va montrer le « troisième fait » (qui signifie, en fait que les théorèmes et les antithéorèmes, même si on se limite aux énoncés arithmétiques Π₁, sont récursivement inséparables).

(Démonstration du « troisième fait » énoncé ci-dessus :)

Imaginons qu'on ait une machine V qui termine toujours, renvoie oui sur un théorème et non sur un antithéorème.

Je considère l'algorithme U suivant. Donné un entier n, je fabrique l'énoncé A₂ n'énumère jamais l'entier n (i.e., nS₂, mais je l'écrit comme ça pour rendre bien clair le fait que :) cet énoncé, appelons-le P, est arithmétique Π₁. J'applique maintenant V à l'énoncé P en question, j'obtiens forcément une réponse en temps fini (puisque V termine toujours) : si cette réponse est oui je renvoie 1 (je signifiant U, bien sûr), tandis que si elle est autre chose, je renvoie 2.

Considérons tour à tour les deux cas que je viens de dire :

  • Si V renvoie oui sur P, comme ce n'est pas non, c'est que l'affirmation P selon laquelle A₂ n'énumère jamais n n'est pas un antithéorème, i.e., l'affirmation ¬P selon laquelle A₂ énumère n n'est pas un théorème ; i.e., il n'y a pas de preuve que A₂ énumère n, et du coup, A₂ n'énumère effectivement jamais n (car si A₂ énumérait n, le fait de le constater par une trace d'exécution constituerait une démonstration[#6]), autrement dit, nS₂.
  • Inversement, si V renvoie autre chose que oui sur P, c'est que l'affirmation P selon laquelle A₂ n'énumère jamais n n'est pas un théorème, mais du coup il n'est pas un théorème que A₁ énumère n (car c'est un théorème que A₁ et A₂ n'énumèrent jamais un entier commun), et comme ci-dessus ceci montre que A₁ n'énumère pas n, bref, nS₁.

J'ai donc construit une machine U qui termine toujours en répondant 1 ou 2, et quand nS₁, elle répond 1, tandis que quand nS₂, elle répond 2 (j'ai montré les affirmations contraposées). Ceci contredit l'inséparabilité récursive supposée de S₁ et S₂.

[#6] Ceci était encore une instance de si un énoncé arithmétique Σ₁ est vrai, alors il est démontrable (ou bien sa contraposée : si un énoncé arithmétique Π₁ n'est pas démontrable, alors il est faux) : voir la note #2.

Il y avait plein de négations empilées dans ce que j'ai écrit (j'espère d'ailleurs ne pas en avoir mis une en trop ou en moins par ci ou par là par inattention), mais globalement, pas de difficulté particulière à cette démonstration. Au final, j'ai prouvé mon troisième fait.

Voyons maintenant comment on peut s'en servir, de manière semblable à la façon dont j'ai montré le théorème de Gödel ci-dessus.

Je commence par redémontrer le théorème de Gödel, avec une petite variante. Pour cela, comme dans le « premier fait » ci-dessus, je construis une machine de Turing qui, donné un énoncé P, va énumérer toutes les démonstrations possibles : (A) si elle trouve une démonstration de ¬P, elle termine et répond non, (B) si elle trouve une démonstration de P, elle termine et répond oui. Si la théorie est cohérente, les recherches (A) et (B) ne peuvent pas aboutir simultanément[#7], la machine va renvoyer oui sur tous les théorèmes et non sur tous les antithéorèmes : d'après mon « troisième fait », il y a forcément des énoncés sur lesquels elle ne termine pas, c'est-à-dire, qui ne sont dans aucun des deux cas, et ceci prouve l'existence d'énoncés que ne réfute pas et ne démontre pas non plus (i.e., qui sont logiquement indécidables). La seule différence par rapport à ma démonstration précédente, est que cette fois-ci je n'ai pas du tout parlé de vérité, et j'ai seulement utilisé la cohérence de la théorie cadre (les précisions techniques sont dans la note qui suit). Comme précédemment, on peut obtenir un énoncé logiquement indécidable qui soit arithmétique Π₁, et il est alors vrai (voir la note #2) ; et la construction peut être rendue tout à fait explicite.

[#7] Je souligne que les recherches (A) et (B) ont lieu en parallèle. La cohérence est utilisée pour affirmer que si ¬P est un théorème, P n'en est pas un : il n'y a donc pas de risque que la machine réponde oui parce qu'elle aurait trouvé une démonstration de P avant celle de ¬P, et vice versa. La démontration du théorème de Gödel que j'avais utilisée précédemment (en utilisant mon « deuxième fait »), elle, utilisait la 1-correction, ce qui est plus fort que la cohérence. Ici, j'obtiens un énoncé logiquement indécidable à partir de la seule cohérence de la théorie : c'est le théorème de Gödel-Rosser.

Pour aller plus loin, je vais avoir envie de considérer deux théories simultanément. Jusqu'à présent, il y avait une théorie T sous-entendue quand j'écris quelque chose comme P est un théorème : cette théorie pouvait être par exemple l'arithmétique de Peano PA, ou la théorie des ensembles ZFC, ou plein d'autres choses. En gros j'ai besoin qu'elle démontre des énoncés arithmétiques de base et notamment la récursive inséparabilité des ensembles S₁ et S₂ que j'ai utilisés (pour cela il suffit qu'elle contienne PA ou même moins) ; j'ai besoin que l'ensemble des axiomes de la théorie soit récursif (i.e., qu'on puisse algorithmiquement décider ce qui est un axiome et ce qui ne l'est pas) de manière à pouvoir énumérer les démonstrations ; et j'ai aussi eu besoin ici ou là de supposer qu'elle était cohérente, voire plus, mais je l'ai toujours dit explicitement.

Maintenant je vais vouloir parler de deux théories T♭ et T (cette dernière va servir de métathéorie pour la première) où T♭ est incluse dans T (au moins au sens où tout théorème de T♭, ou au moins tout théorème arithmétique Π₁, est un théorème de T) : le lecteur qui ne veut pas se compliquer la vie peut s'imaginer par exemple que T♭ est PA et que T est ZFC ; ou bien, s'il préfère, que T♭ est l'une des deux (PA ou ZFC) et que T est la théorie T♭+Consis(T♭) qui ajoute à T♭ l'axiome que T est cohérente. (On a le droit de prendre T égale à T♭ mais ce que je dirai sera alors très peu intéressant.)

Je vais maintenant construire une machine de Turing qui, donné un énoncé P, va énumérer toutes les démonstrations possibles dans T : comme précédemment, (A) si elle trouve une démonstration de ¬P dans T, elle termine et répond non, (B) si elle trouve une démonstration de P dans T, elle termine et répond oui ; mais maintenant j'ajoute les clauses supplémentaires suivantes : (C) si la machine trouve une démonstration dans T du fait que P est indémontrable dans T, elle termine et répond non, et (D) si elle trouve une démonstration dans T du fait que P est irréfutable (i.e., ¬P est indémontrable) dans T, elle termine et répond oui. Si la théorie T est cohérente[#8], la machine va renvoyer oui sur tous les théorèmes de T♭ et non sur tous les antithéorèmes de T♭ : d'après mon « troisième fait », il y a forcément des énoncés sur lesquels elle ne termine pas, c'est-à-dire, qui ne sont dans aucun des quatre cas, et ceci prouve l'existence d'énoncés que T (A) ne réfute mais (B) ne démontre pas non plus (i.e., qui sont logiquement indécidables dans T), mais dont T ne démontre pas qu'ils sont (C) indémontrables ni (D) irréfutables, même[#9] dans T♭. Bref, on peut dire que ces énoncés sont logiquement indécidablement indécidables.

[#8] Plus précisément : si P est un théorème de T♭, et a fortiori de T, comme la théorie T est cohérente, ¬P n'est pas un théorème de T (donc la recherche (A) ne peut pas aboutir) ; mais par ailleurs, P est un théorème de T est aussi un théorème de T (car il suffit d'exhiber une démonstration pour démontrer l'existence d'une démonstration : ceci était encore une instance de si un énoncé arithmétique Σ₁ est vrai, alors il est démontrable [en l'occurrence dans T]), i.e, P n'est pas indémontrable dans T est un théorème de T, et de nouveau par cohérence de T, P est indémontrable dans T n'est pas un théorème de T (donc la recherche (C) ne peut pas aboutir) ; mais comme la recherche (B), elle, aboutit, la machine termine et répond oui. Et symétriquement, si ¬P est un théorème de T♭, la machine termine et répond non.

[#9] Pourquoi écrire même dans T♭ ? Parce que si P est indémontrable/irréfutable dans T, elle l'est a fortiori dans T♭ ; et du coup, il devrait être plus facile de démontrer l'indémontrabilité/irréfutabilité dans T♭ de P que celle dans T (en l'occurrence l'indémontrabilité/irréfutabilité dans T est vraie, et l'indémontrabilité/irréfutabilité dans T♭ n'est pas démontrable dans T). • Quant à la raison pour laquelle j'ai besoin de deux théories : ce que j'ai dit reste valable si T♭ est T, seulement dans ce cas la conclusion n'est pas intéressante, parce que T, supposée cohérente, ne peut pas prouver la cohérence de T (c'est le second théorème d'incomplétude), c'est-à-dire qu'elle ne peut même pas prouver que T ne prouve pas tous les théorèmes, et a fortiori, elle ne peut pas prouver que T ne prouve pas P, ni que T ne prouve pas ¬P — mais c'est pour des raisons « idiotes ».

De nouveau, la construction peut être rendue tout à fait explicite. Par ailleurs, P peut être choisi arithmétique Π₁ : on obtient alors un énoncé vrai (voir la note #2), indémontrable et irréfutable (dans T), et dont l'indémontrabilité et l'irréfutabilité (même dans T♭) sont eux-mêmes indémontrables[#9b][#10] (dans T).

[#9b] (Ajout) Ce que je raconte est un peu redondant, je ne sais pas si ça simplifie ou complique les choses, mais je peux signaler que la recherche (B) recouvre la recherche (D) : en effet, si T démontre que T♭ ne réfute pas P, alors T démontre P (car on peut tenir dans T le raisonnement suivant : si P n'était pas vrai, il serait réfutable dans T♭ — toujours car il suffit d'exhiber un contre-exemple — et a contrario, si T♭ ne réfute pas P, c'est que P est vrai). Du coup, je peux juste dire : un énoncé indémontrable et irréfutable dans T, et dont T ne démontre pas non plus l'indémontrabilité dans T♭ (tout le reste en découle).

[#10] Et on peut aussi les rendre irréfutables : soit, ce qui est le plus naturel, en supposant la 1-correction de T (car alors si P est indémontrable/irréfutable dans T♭, resp. irréfutable, on ne peut pas prouver le contraire dans T !) ; soit, sous l'hypothèse plus faible que T ne prouve pas que T♭ est incohérente, en refaisant l'astuce de Rosser, c'est-à-dire en ajoutant encore des recherches à la machine : (E) si la machine trouve une démonstration dans T du fait que P est réfutable (i.e., ¬P est démontrable) dans T♭, elle termine et répond non, et (F) si elle trouve une démonstration dans T du fait que P est démontrable dans T♭, elle termine et répond oui.

J'ai notamment démontré, sous l'hypothèse que ZFC est cohérent, qu'il existe des énoncés arithmétiques Π₁ qui soient vrais mais indécidables, mais dont ZFC ne prouve pas que ces énoncés soient indémontrables, ni qu'ils soient irréfutables, dans l'arithmétique de Peano. Toutes sortes de variantes[#11] sont possibles selon le même raisonnement, il faut juste fabriquer attentivement la machine de Turing sur laquelle on raisonne, et vérifier très soigneusement qu'elle répond oui sur les théorèmes (d'une certaine théorie contenant un minimum d'arithmétique) et non sur les antithéorèmes. Je laisse par exemple en exercice au lecteur de formuler des résultats sur l'existence d'énoncés indécidablement indécidablement indécidables et ainsi de suite (je ne vois pas trop comment monter à des ordinaux infinis, mais je n'exclus pas que ce soit possible).

[#11] Voici un exemple d'autre chose qu'on pourrait montrer dans le même genre : soit PA′ := PA+Consis(PA) la théorie obtenue en ajoutant à PA l'affirmation de sa cohérence ; et soit PA♠ := PA+¬Consis(PA) la théorie obtenue en ajoutant à PA l'affirmation de son incohérence. La théorie PA′ est cohérente (c'est un théorème de ZFC : ℕ en est un modèle) ; la théorie PA♠ l'est aussi (c'est une conséquence de la cohérence de PA et du second théorème d'incomplétude), bien que PA♠ affirme être elle-même incohérente (elle n'est pas 1-correcte, mais elle est quand même cohérente) ; en revanche, la réunion de PA′ et PA♠ est incohérente (ces deux théories ont des axiomes trivialement contradictoires). Maintenant, on peut faire une machine de Turing qui, donné P un énoncé arithmétique Π₁, recherche en parallèle des démonstrations dans PA′ et dans PA♠ : si elle trouve une démonstration de ¬P dans l'une ou l'autre, elle termine et renvoie non, et si elle trouve une démonstration de P dans l'une ou l'autre, elle termine et renvoie oui. Alors cette machine répondra oui pour tout théorème de PA (car sa négation ne peut pas être un théorème ni de PA′ ni de PA♠) et non pour tout antithéorème de PA. D'après mon « troisième fait », on en déduit qu'il existe un énoncé P arithmétique Π₁ (forcément vrai), qui n'est ni démontrable ni réfutable ni dans PA′ ni dans PA♠ : autrement dit, ni ajouter l'axiome Consis(PA) à PA ni ajouter sa négation ¬Consis(PA) ne permet de trancher quant à cet énoncé P ni dans un sens ni dans l'autre. Et en combinant avec ce que j'ai fait avant, on peut aussi obtenir que ni l'indémontrabilité de P dans PA ni son irréfutabilité ne soient démontrables dans PA′ (la question ne se pose pas pour PA♠ puisque PA♠ croit que tout énoncé est un théorème de PA ; mais on peut certainement trouver quand même des choses à ajouter de ce côté-là).

Ajout : Pour être un peu plus explicite, je pourrais donner la forme des différents énoncés qu'on obtient. L'énoncé classique G de Gödel est un énoncé qui signifie (informellement) : G n'est pas démontrable (dans la théorie T) (sous l'hypothèse que T est cohérente, cet énoncé est vrai, donc pas démontrable, et sous l'hypothèse que T est 1-correcte, il n'est pas non plus réfutable). L'énoncé de Gödel-Rosser G′ signifie : pour toute démonstration de G′ (dans T), il existe une démonstration de ¬G′ qui soit plus courte (sous l'hypothèse que T est cohérente, cet énoncé est vrai et n'est ni démontrable ni réfutable). Un exemble d'énoncé « logiquement indécidablement indécidable » G″ est : pour toute démonstration, dans T, de G″ ou bien du fait que G″ est démontrable dans T♭, il existe une démonstration, toujours dans T, de ¬G″ ou bien du fait que G″ est irréfutable dans T♭, qui soit plus courte (cet énoncé est vrai, indémontrable dans T, irréfutable dans T, et il est également indémontrable dans T qu'il est indémontrable dans T♭ ou irréfutable dans T♭). Le fait que ces différents énoncés G,G′,G″ fassent référence à eux-mêmes n'est pas un problème en vertu de l'astuce classique « quinienne » qui permet de construire de tels énoncés auto-référents par diagonalisation. Il est vrai que, complètement développé, un énoncé tel que G″ va être très pénible à écrire (déjà G s'écrit quelque chose comme : soit P l'énoncé obtenu en substituant à la variable libre (notée entre cornets) la valeur de R lui-même dans la formule R suivante : soit P l'énoncé obtenu en substituant à la variable libre (notée entre cornets) la valeur de R lui-même dans la formule R suivante : <Q> ; alors P n'est pas démontrable (dans la théorie T) ; alors P n'est pas démontrable (dans la théorie T) ; alors G″ devient vraiment lourd).

Pour conclure, je dirais que le « troisième fait » cité plus haut est un peu une forme ultime du théorème de Gödel (en tout cas sous sa variante Turing), un outil à fabriquer toutes sortes de théorèmes de Gödel. Je ne connais pas son histoire : il apparaît dans un article de Smullyan (Undecidability and Recursive Inseparability, Z. Math. Logik Grundlagen Math. 4 (1958), 143–147), mais ce dernier suggère que le résultat figure déjà dans un livre de Kleene (Introduction to Metamathematics, apparemment vers la page 313 de l'édition van Nostrand de 1952), je n'ai pas vérifié. Je suppose que plein de gens ont eu cette même idée. Je ne sais pas non plus à qui est due l'observation que ceci permet de construire des énoncés indécidablement indécidables : de même que pour le « troisième fait » (théorème de Kleene-Smullyan ?), et comme sans doute plein de gens qui se seraient posé cette question, je l'ai redécouvert indépendamment, mais il est évident que je suis loin d'être le premier, j'ai eu la flemme de chercher qui ce premier avait pu être.

↑Entry #2410 [older|newer] / ↑Entrée #2410 [précédente|suivante]

Recent entries / Entrées récentesIndex of all entries / Index de toutes les entrées