(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)
où 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 ∃n.¬Q(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
ouilorsque P est un théorème, et (3) en répondantnonlorsque 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
(si V lancée sur P ne termine pas, cela
contredit (1), si elle termine en répondant oui
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 k∈S₁ et 2 lorsque k∈S₂, 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 e∈S₂, 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
ouisur un théorème etnonsur 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., n∉S₂, 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 estouije renvoie 1 (jesignifiant 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
ouisur P, comme ce n'est pasnon, 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, n∉S₂.- Inversement, si V renvoie autre chose que
ouisur 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, n∉S₁.J'ai donc construit une machine U qui termine toujours en répondant 1 ou 2, et quand n∈S₁, elle répond 1, tandis que quand n∈S₂, 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 :
; alors G″ devient
vraiment lourd).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)
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.
Ajout () : Voir cette question sur MathOverflow pour la question du degré de Turing d'un ensemble séparant les théorèmes et les antithéorèmes (il s'avère qu'on peut le trouver bas par le théorème de la base basse). Voir aussi cette entrée ultérieure pour une discussion sur une généralisation des degrés de Turing dans laquelle cette question intervient.