Prouvabilité et incomplétude
Quand l'arithmétique parle de ses propres preuves
Cette rubrique réunit les deux fils des précédentes. L’arithmétique de Peano, une théorie écrite en calcul des prédicats, sait parler de ses propres démonstrations ; la boîte de la logique modale permet de mettre en forme ce qu’elle en dit. Plutôt que de suivre la démonstration classique des théorèmes de Gödel, entièrement menée dans l’arithmétique, on les lit ici avec les outils de la logique modale.
Voici sans doute l’usage le plus étonnant de la boîte. On lit désormais $\Box\phi$ comme « $\phi$ est prouvable » (dans une théorie fixée, par exemple l’arithmétique), et $\Diamond\phi=\neg\Box\neg\phi$ comme « on ne peut pas réfuter $\phi$ », c’est-à-dire « $\phi$ est compatible avec la théorie ». Avec ce simple changement de lecture, les théorèmes d’incomplétude de Gödel, réputés ardus, tiennent en quelques lignes de logique modale.
Dans Forever Undecided (1987), Raymond Smullyan fait tenir toute l’affaire dans une énigme. Un logicien visite l’île où les chevaliers disent toujours vrai et où les filous mentent toujours. Ce logicien est fiable : il ne croit jamais rien de faux. Un habitant lui déclare :
« Vous ne croirez jamais que je suis un chevalier. »
Si l’habitant était un filou, sa phrase serait fausse : le logicien finirait donc par croire que c’est un chevalier, et croirait une chose fausse, ce qui est exclu. C’est donc un chevalier, sa phrase est vraie… et le logicien ne le croira jamais. Il existe une vérité que ce logicien, pourtant irréprochable, ne peut pas atteindre.
Le plus piquant est que nous venons de le démontrer. Pourquoi le logicien ne tiendrait-il pas le même raisonnement ? Parce que ce raisonnement s’appuie sur sa propre fiabilité : s’il s’en croyait assuré, il conclurait « c’est un chevalier », et la phrase deviendrait fausse. Un logicien fiable ne peut pas être certain de l’être. Remplacez « croire » par « prouver » et « fiable » par « cohérent » : ce sont les deux théorèmes de Gödel.
Des nombres qui parlent de preuves
Souhaitant éprouver la solidité de l’édifice mathématique, et d’abord de l’arithmétique, Gödel imagine en 1931 une méthode astucieuse, une sorte de hack, pour faire parler l’arithmétique d’elle-même. Le cadre est l’arithmétique de Peano $\text{PA}$ : une théorie, c’est-à-dire un ensemble d’axiomes, écrite en logique du premier ordre et dont les entiers naturels sont un modèle. Gödel associe à chaque formule $\phi$ un numéro, son code de Gödel, noté $\ulcorner\phi\urcorner$. Un énoncé sur les nombres peut alors, de façon détournée, être un énoncé sur les formules.
Ce qui semblait à l’époque un tour de force est devenu banal à l’ère de l’informatique. Pour associer un nombre unique à une formule, il suffit de regarder le code binaire du fichier où elle est écrite (en ajoutant un « 1 » au début si ça commence par des « 0 »).
On peut coder de même un arbre de preuve complet, comme tout ce qu’on peut taper dans un traitement de texte. Dès lors, « $\phi$ est prouvable » devient une affirmation arithmétique : il existe un entier qui est le code d’une preuve de la formule de code $\ulcorner\phi\urcorner$. Gödel construit la formule qui dit cela et la baptise $\text{Bew}(x)$, de l’allemand beweisbar, « prouvable ». Notre boîte n’est qu’une abréviation :
$\Box\phi$ désigne la formule arithmétique $\text{Bew}(\ulcorner\phi\urcorner)$.
Que sait l’arithmétique de sa propre prouvabilité ? Trois choses, appelées conditions de dérivabilité (elles sont dues à Hilbert, Bernays et Löb), et qui vont nous rappeler des souvenirs :
| Ce que l'arithmétique démontre | Lecture | En logique modale |
|---|---|---|
| si $\vdash\phi$, alors $\vdash\Box\phi$ | une preuve de $\phi$ étant un objet fini, on peut vérifier que c'en est une | règle de nécessitation |
| $\vdash\Box(\phi\rightarrow\psi)\rightarrow(\Box\phi\rightarrow\Box\psi)$ | les preuves s'enchaînent par modus ponens | axiome $\text{(K)}$ |
| $\vdash\Box\phi\rightarrow\Box\Box\phi$ | si $\phi$ est prouvable, on peut prouver qu'elle l'est | axiome $\text{(4)}$ |
Autrement dit, la prouvabilité se comporte comme la boîte de la logique $\textbf{K4}$, et tout ce qu’on démontre dans $\textbf{K4}$ est vrai de $\text{Bew}$. En revanche, on se gardera d’ajouter l’axiome $\text{(T)}=\Box\phi\rightarrow\phi$, « ce qui est prouvable est vrai ». Il a l’air inoffensif, il est même vrai si la théorie est saine. Mais la théorie ne peut pas le démontrer, et c’est tout le sujet de cette section.
Le lemme de diagonalisation
Il manque un ingrédient : des formules qui parlent d’elles-mêmes. À première vue, c’est impossible. Une formule qui contiendrait son propre code serait plus longue que ce code, lequel est au moins aussi long qu’elle… Un programme qui voudrait afficher son propre texte bute sur la même difficulté : print("print(\"print(...)\")") ne fait que repousser le problème indéfiniment.
L’astuce consiste à ne jamais citer le tout, mais seulement un gabarit, accompagné d’une recette pour reconstituer le tout à partir du gabarit. Le philosophe Quine en a donné une version en langue naturelle, sans jamais écrire « cette phrase » :
« précédé de sa propre citation, donne une phrase qui a la propriété $S$ »
précédé de sa propre citation, donne une phrase qui a la propriété $S$.
La phrase a deux morceaux : un gabarit, entre guillemets, et une recette qui dit quoi en faire (« le faire précéder de sa propre citation »). Appliquée au gabarit, la recette reconstitue exactement la phrase entière. La phrase parle donc d’elle-même sans jamais se contenir.
Les informaticiens appellent quine, en hommage au philosophe, un programme qui affiche son propre code. En Python, deux lignes suffisent (lancez-le, puis comparez le résultat au code) :
On y retrouve le découpage de Quine :
- la chaîne
sest le gabarit, avec un trou%r; s % sest la recette : elle remplit le trou avec la citation des(son texte entre guillemets), c’est-à-dire « précédé de sa propre citation » ;- le résultat est le texte complet du programme, qu’il ne reste qu’à afficher.
Rien n’oblige à se contenter d’afficher son code : le programme peut calculer ce qu’il veut à son sujet. Celui-ci compte les lettres « e » de son propre texte :
C’est exactement le lemme qui suit : pour n’importe quelle propriété $S$ (ici « compter les e »), on fabrique un objet qui applique $S$ à son propre code.
Lemme de diagonalisation :
Pour toute formule arithmétique $S(x)$ à une variable libre, il existe un énoncé $\phi$ tel que
$\vdash\phi\leftrightarrow S(\ulcorner\phi\urcorner)$.
Une formule $S(x)$ à une variable libre exprime une propriété des nombres : en remplaçant $x$ par un nombre $n$, on obtient un énoncé $S(n)$ qui dit si $n$ a cette propriété, comme « $x$ est pair » ou « $x$ est le code d’une formule prouvable ». Et puisque chaque formule a un code, une propriété des nombres devient du même coup une propriété des formules : $S(\ulcorner\phi\urcorner)$ dit que la formule $\phi$ a la propriété $S$. Le lemme affirme donc que, quelle que soit la propriété $S$, il existe une formule qui dit d’elle-même « j’ai la propriété $S$ ». La preuve suit pas à pas la recette de Quine.
Étape 1 : la recette $d$. Si $n$ est le code d'une formule $A(x)$ à une variable libre, on note $d(n)$ le code de la formule obtenue en appliquant $A$ à son propre code :
$d(\ulcorner A(x)\urcorner)=\ulcorner A(\ulcorner A(x)\urcorner)\urcorner$.
Par exemple $d(\ulcorner x=0 \urcorner)=\ulcorner\,\ulcorner x=0 \urcorner = 0\,\urcorner$ : la formule « $x$ est nul », appliquée à son propre code, affirme que son code est nul (ce qui est faux, mais peu importe). C'est le « précédé de sa propre citation » de Quine, ou le s % s du programme. La fonction $d$ se calcule mécaniquement (décoder, substituer, recoder) : l'arithmétique sait donc en parler.
Étape 2 : le gabarit $g$. On pose $g(x)=S(d(x))$, qui affirme « la diagonale de $x$ a la propriété $S$ ». C'est le gabarit entre guillemets de la phrase de Quine, ou la chaîne s du programme.
Étape 3 : le gabarit appliqué à lui-même. On pose $\phi=g(\ulcorner g(x)\urcorner)$.
Étape 4 : la vérification. Par définition de $g$, l'énoncé $\phi$ affirme $S\big(d(\ulcorner g(x)\urcorner)\big)$. Or, par définition de $d$, $d(\ulcorner g(x)\urcorner)=\ulcorner g(\ulcorner g(x)\urcorner)\urcorner=\ulcorner\phi\urcorner$. L'énoncé $\phi$ affirme donc $S(\ulcorner\phi\urcorner)$ : il dit de lui-même qu'il a la propriété $S$. Comme ce calcul de $d$ est mécanique, l'arithmétique sait le refaire, et elle démontre $\phi\leftrightarrow S(\ulcorner\phi\urcorner)$.
Le schéma ci-dessous montre pourquoi l’on parle de diagonalisation. On range toutes les formules à une variable en lignes et tous les codes $n_0, n_1,\ldots$ en colonnes ; la case $A_i(n_j)$ applique la formule $A_i$ au code de $A_j$. La recette $d$ parcourt la diagonale (en rose), où chaque formule est appliquée à son propre code.
La ligne de $g$ (en bleu) parle de la diagonale : sa case de la colonne $n_j$ affirme que la case diagonale $A_j(n_j)$ a la propriété $S$. Dans la colonne de $g$ elle-même, la case diagonale visée est… la case de départ : $\phi=g(n_g)$ parle d'elle-même.
C’est le même mouvement que l’argument diagonal de Cantor, à une différence près. Cantor modifie la diagonale pour fabriquer un objet qui n’est dans aucune ligne. Ici, la ligne $g$ fait partie du tableau, et elle finit par croiser sa propre diagonale : au lieu d’une contradiction, on obtient un point fixe.
| Quine | Python | Arithmétique | |
|---|---|---|---|
| gabarit | « précédé de sa propre citation, donne… » | la chaîne s | $g(x)=S(d(x))$ |
| recette | précéder de sa citation | s % s | $d$ |
| résultat | la phrase entière | le texte du programme | $\phi=g(\ulcorner g(x)\urcorner)$ |
| ce qu'il en dit | « a la propriété $S$ » | print, count("e") | $S(\ulcorner\phi\urcorner)$ |
Le premier théorème d’incomplétude
Appliquons le lemme à la propriété « ne pas être prouvable », c’est-à-dire à $S(x)=\neg\text{Bew}(x)$. On obtient la célèbre formule de Gödel $G$ :
$\vdash G\leftrightarrow\neg\Box G$ (« je ne suis pas prouvable »)
Elle ressemble au paradoxe du menteur, « cette phrase est fausse », à une nuance près qui change tout. Le menteur parle de vérité et mène à une contradiction. $G$ parle de prouvabilité et ne mène qu’à une surprise. En effet, si $G$ était prouvable, on aurait $\vdash G$, donc $\vdash\Box G$ par nécessitation ; mais $G$ entraîne $\neg\Box G$, et la théorie prouverait une chose et son contraire. Dans une théorie cohérente, $G$ n’est donc pas prouvable. Or c’est exactement ce qu’elle affirme : $G$ est vraie et non prouvable.
Premier théorème d'incomplétude :
Dans toute théorie cohérente (on ne peut pas y prouver le faux), dont on sait reconnaître mécaniquement les axiomes et assez expressive pour décrire l'arithmétique, il existe un énoncé vrai qui n'est pas prouvable. La prouvabilité est plus faible que la vérité.
Ajouter $G$ aux axiomes ne répare rien : la nouvelle théorie a sa propre formule de Gödel, et tout recommence.
Le raisonnement ci-dessus se formalise entièrement dans la logique $\textbf{K4}$ : à partir de $\vdash G\leftrightarrow\neg\Box G$, on arrive à $\vdash\neg\Box\bot\rightarrow\neg\Box G$, « si aucune contradiction n’est prouvable, alors $G$ n’est pas prouvable ».
- $G\leftrightarrow\neg\Box G$
- $\Box G\rightarrow\neg G$ (à partir de 1.)
- $\Box(\Box G\rightarrow\neg G)$ (nécessitation)
- $\Box\Box G\rightarrow\Box\neg G$ (distribution de la boîte grâce à $\text{(K)}$)
- $\Box G\rightarrow\Box\neg G$ (par l'axiome $\text{(4)}= \Box G\rightarrow\Box\Box G$ et avec l'étape 4., on déduit $\Box G\rightarrow\Box\Box G\rightarrow\Box\neg G$)
- $\Box G\rightarrow(\Box G\land\Box\neg G)$ (à partir de 5. et $\Box G\rightarrow\Box G$)
- $\Box G\rightarrow\Box(G\land \neg G)$ (la boîte se distribue sur la conjonction)
- $\Box G\rightarrow\Box\bot$
- $\neg\Box\bot\rightarrow \neg\Box G$ (contraposée de 8.)
Ce petit calcul a une conséquence considérable. La formule $\neg\Box\bot$ dit « le faux n’est pas prouvable » : c’est la théorie qui affirme sa propre cohérence. Or la ligne 9 et la ligne 1 donnent ensemble $\vdash\neg\Box\bot\rightarrow G$. Si la théorie prouvait sa cohérence, elle prouverait donc $G$, ce qui est impossible. Une théorie cohérente ne peut pas prouver qu’elle l’est ! C’est le second théorème d’incomplétude, que l’on va retrouver par un chemin plus général.
David Hilbert rêvait de mettre les mathématiques à l’abri du doute en démontrant, par des moyens élémentaires et incontestables, que leurs axiomes ne mènent à aucune contradiction. Le 8 septembre 1930, dans sa ville natale de Königsberg, il conclut une allocution restée célèbre par ces mots, aujourd’hui gravés sur sa tombe : « Wir müssen wissen, wir werden wissen », nous devons savoir, nous saurons.
La veille, dans la même ville, à la fin d’une table ronde sur les fondements des mathématiques, un jeune homme de vingt-quatre ans avait indiqué en quelques phrases prudentes qu’il existait des énoncés arithmétiques vrais et indémontrables. Presque personne ne releva. John von Neumann, lui, comprit sur-le-champ, et écrivit à Gödel quelques semaines plus tard qu’il en avait tiré une conséquence remarquable : l’impossibilité de prouver la cohérence. Gödel lui répondit, courtoisement, qu’il venait de l’envoyer à l’imprimeur.
Le théorème de Löb
En 1952, le logicien Leon Henkin pose la question miroir. On sait ce que vaut la formule qui dit « je ne suis pas prouvable ». Que dire de celle qui affirme « je suis prouvable », $\vdash H\leftrightarrow\Box H$ ? Elle évoque non plus le menteur mais le diseur de vérité, « ce que je dis là est vrai », auquel aucune valeur de vérité ne semble s’imposer puisqu’un menteur dirait la même chose.
La réponse, donnée par Martin Löb en 1955, est une surprise : $H$ est prouvable, et donc vraie. C’est un cas particulier d’un résultat général.
Le théorème de Löb stipule que les seules formules $\phi$ pour lesquelles on peut prouver $\Box\phi\rightarrow\phi$ sont les formules prouvables :
Si $\vdash\Box\phi\rightarrow\phi$, alors $\vdash \phi$.
Le théorème affirme donc que si on peut prouver une formule en admettant qu’elle est prouvable, alors on peut la prouver tout court. C’est une sorte de méthode Coué logique, une prophétie autoréalisatrice : « si tu crois en toi, ça va le faire ». C’est bizarre, mais ça se démontre.
Lu dans l’autre sens, il est tout aussi troublant. On aimerait que la théorie sache, pour chaque $\phi$, que « si $\phi$ est prouvable, alors $\phi$ est vraie ». Löb nous dit qu’elle ne le démontre que pour les $\phi$ qu’elle démontre déjà, c’est-à-dire quand cela ne sert plus à rien. Voilà pourquoi $\text{(T)}$ ne peut pas être un axiome de la prouvabilité.
Preuve du théorème de Löb :
On suppose $\vdash \Box\phi\rightarrow\phi$.
Grâce au lemme de diagonalisation, on construit la formule arithmétique autoréférente suivante :
$\vdash\sigma\leftrightarrow (\Box\sigma\rightarrow\phi)$ (« si je suis prouvable, alors $\phi$ »).
- $\vdash\Box(\sigma\rightarrow (\Box\sigma\rightarrow\phi))$ (sens direct de la formule autoréférente, puis nécessitation)
- $\vdash\Box\sigma\rightarrow \Box(\Box\sigma\rightarrow\phi)$ puis $\vdash\Box\sigma\rightarrow (\Box\Box\sigma\rightarrow\Box\phi)$ (distribution de la boîte grâce à $\text{(K)}$, deux fois)
- Comme $\vdash \Box\sigma\rightarrow\Box\Box\sigma$ par $\text{(4)}$, on en tire $\vdash \Box\sigma\rightarrow\Box\phi$
- $\vdash \Box\sigma\rightarrow\phi$ (car $\vdash \Box\sigma\rightarrow\Box\phi\rightarrow\phi$ puisqu'on suppose $\vdash \Box\phi\rightarrow\phi$)
- $\vdash (\Box\sigma\rightarrow\phi)\rightarrow\sigma$ (sens réciproque de la formule autoréférente)
- $\vdash\sigma$ par modus ponens de 4. et 5.
- $\vdash\Box\sigma$ par nécessitation.
- $\vdash \phi$ par modus ponens de 4. et 7.
Smullyan adorait « démontrer » l’existence du père Noël à l’aide de la phrase suivante :
« Si cette phrase est vraie, alors le père Noël existe. »
Supposons la phrase vraie. Alors ce qu’elle dit a lieu : si elle est vraie, le père Noël existe. Comme on l’a supposée vraie, le père Noël existe. Nous venons de montrer que si la phrase est vraie, alors le père Noël existe… or c’est précisément la phrase. Elle est donc vraie, et le père Noël existe.
C’est le paradoxe de Curry, et la preuve de Löb en est la copie conforme, où « vraie » est remplacé par « prouvable » : la formule $\sigma$ dit « si je suis prouvable, alors $\phi$ ». Avec la vérité, on obtient une absurdité, signe qu’un langage ne peut pas contenir son propre prédicat de vérité (c’est un théorème de Tarski). Avec la prouvabilité, qui s’exprime bel et bien dans l’arithmétique, on obtient un théorème.
Le second théorème d’incomplétude
Second théorème d'incomplétude :
Une théorie cohérente, dont on sait reconnaître mécaniquement les axiomes et qui contient l'arithmétique, ne peut pas prouver sa propre cohérence. Les seules théories de ce type qui « prouvent » leur cohérence sont celles qui sont incohérentes, et qui prouvent donc n'importe quoi…
Ce théorème n'est autre que le théorème de Löb appliqué à $\phi=\bot$ !
La formule $\Box\bot\rightarrow\bot$ équivaut à $\neg\Box\bot$, l'énoncé de cohérence. Le théorème de Löb devient donc : si $\vdash\neg\Box\bot$, alors $\vdash\bot$. Par contraposition, si la théorie est cohérente ($\nvdash\bot$), alors elle ne prouve pas sa cohérence ($\nvdash\neg\Box\bot$).
Par dualité, $\Diamond P = \neg\Box\neg P$ exprime qu’on ne peut pas prouver que $P$ est fausse, autrement dit que $P$ est compatible avec la théorie. L’énoncé de cohérence $\neg\Box\bot$ s’écrit alors simplement $\Diamond\top$, et le second théorème prend, à l’intérieur même de la théorie, la forme $\Diamond\top\rightarrow \neg\Box\Diamond \top$ : « si la théorie est cohérente, alors elle ne peut pas le prouver ».
C’est la fin du programme de Hilbert sous sa forme initiale : pour prouver la cohérence de l’arithmétique, il faut des moyens qui la dépassent. Gerhard Gentzen, l’inventeur de la déduction naturelle et du calcul des séquents, y parviendra en 1936 au prix d’une récurrence sur des ordinaux infinis.
La logique GL
Le théorème de Löb peut lui-même être démontré par la théorie, ce qui en donne une version internalisée, devenue un axiome.
La logique de la prouvabilité de Gödel-Löb ($\textbf{GL}$) est formée à partir du système $\textbf{K}$ auquel on ajoute l'axiome de Löb $\text{(L)}=\Box(\Box\phi\rightarrow\phi)\rightarrow\Box\phi$ (c'est la version formalisée du théorème de Löb).
Avec $\phi=\bot$, l’axiome $\text{(L)}$ donne $\Box\neg\Box\bot\rightarrow\Box\bot$, soit, par contraposition et en notation diamant, $\Diamond\top\rightarrow\neg\Box\Diamond\top$ : on retrouve en une ligne le second théorème d’incomplétude.
On remarque que l’axiome $\text{(4)}$, dont on s’est tant servi, ne figure pas dans la définition. C’est qu’il est devenu superflu.
$\vdash_\textbf{GL}\text{(4)}=\Box\phi\rightarrow\Box\Box \phi$
Et donc $\textbf{K4}≤\textbf{GL}$ ($\textbf{K4}$ se réduit à $\textbf{GL}$).
Obtention d’un premier théorème : $\vdash_\textbf{K}\Box P\rightarrow \Box ((\Box P\land \Box\Box P)\rightarrow(P\land \Box P))$
Tout système de transition qui valide $\textbf{GL}$ valide donc $\text{(4)}$ : il est transitif !
À quoi ressemblent les mondes de la prouvabilité ? Certainement pas à ceux de la connaissance. Le modèle ci-dessous valide $\color{#1DB100}\text{(L)}$ en chacun de ses nœuds, mais on y voit échouer, au nœud $a$, l’axiome $\color{#F27200}\text{(T)}=\Box P \rightarrow P$ ainsi que $\color{#FF42A1}\neg P\rightarrow \Box\Diamond\neg P$, une instance de l’axiome $\text{(B)}$.
Les deux échecs ont un sens. Celui de $\text{(T)}$ confirme que $\textbf{GL}$ ne prouve pas « ce qui est prouvable est vrai ». Celui de $\text{(B)}$ tient à l’absence de retour : $a$ voit $b$, mais $b$, cul-de-sac, ne voit rien du tout, et rien n’y est donc possible, pas même $\neg P$. Dans un cul-de-sac, tout est nécessaire et rien n’est possible : $\textbf{GL}$ ne prouve donc ni l’axiome $\text{(D)}$, ni même $\Diamond\top$, sa propre cohérence. Les culs-de-sac ne sont pas un accident, ils sont indispensables, comme le montre la caractérisation suivante.
Un système de transition valide $\text{(L)}$ si et seulement s'il est transitif et ne contient aucun chemin infini $a_0\longrightarrow a_1\longrightarrow a_2\longrightarrow\cdots$
En particulier, un tel système est irréflexif (une boucle $a\longrightarrow a$ est un chemin infini $a\longrightarrow a\longrightarrow a\longrightarrow\cdots$) et asymétrique (un aller-retour $a\longrightarrow b\longrightarrow a$ aussi), et tout chemin finit dans un cul-de-sac.
Montrons le sens qui nous importe : dans un système $\mathcal{T}=(N,A)$ transitif et sans chemin infini, l'axiome de Löb est valide.
Supposons au contraire qu'il ne soit pas satisfait en un nœud $a$, pour une certaine valuation. On a donc $\langle \mathcal{T},a\rangle \not\models \Box(\Box P\rightarrow P)\rightarrow \Box P$, ce qui implique :
- $\langle \mathcal{T},a\rangle \models \Box(\Box P\rightarrow P)$, et
- $\langle \mathcal{T},a\rangle \not\models \Box P$.
La deuxième affirmation entraîne qu'il existe un nœud $a'\in N$ tel que $a\longrightarrow a'$ et $\langle \mathcal{T},a'\rangle \not\models P$.
Par contre, la première affirmation nous assure que $\langle \mathcal{T},a'\rangle \models \Box P\rightarrow P$.
Par conséquent $\langle \mathcal{T},a'\rangle \not\models \Box P$. Cela signifie qu'il existe un nœud $a''\in N$, successeur de $a'$ ($a'\longrightarrow a''$) tel que $\langle \mathcal{T},a''\rangle \not\models P$.
Par transitivité, $a \longrightarrow a''$. Or si on retourne à l'affirmation 1., on a aussi $\langle \mathcal{T},a''\rangle \models \Box P\rightarrow P$, et le même raisonnement fournit un successeur $a'''$ de $a''$, puis un autre, et ainsi de suite. On construit de fil en aiguille un chemin infini $a\longrightarrow a'\longrightarrow a''\longrightarrow\cdots$, ce qui est exclu.
Pour la réciproque, contentons-nous de voir pourquoi une boucle est interdite. Si $a\longrightarrow a$, on choisit la valuation où $P$ est fausse en $a$ et vraie partout ailleurs. Alors $\Box P$ est fausse en $a$, et $\Box P\rightarrow P$ est vraie partout (en $a$ parce que $\Box P$ y est fausse, ailleurs parce que $P$ y est vraie). Le nœud $a$ force donc $\Box(\Box P\rightarrow P)$ sans forcer $\Box P$ : l'axiome de Löb y est en défaut.
Les exemples les plus simples de tels systèmes sont les arbres finis, où une flèche relie chaque nœud à tous ses descendants (c’est la transitivité). Et il se trouve qu’ils suffisent. C’est plutôt génial que cette logique de la prouvabilité s’exprime naturellement sur des arbres finis, qui représentent intuitivement la notion de preuve (la racine représentant la formule prouvée, et les feuilles les axiomes).
Notons $\mathscr{C}_{\text{arbres finis}}$ la classe de ces arbres finis transitifs.
Correction et complétude :
$\vdash_\textbf{GL} \phi$ si et seulement si $\models_{\mathscr{C}_{\text{arbres finis}}}\phi$.
La correction découle de ce qui précède : l’axiome $\text{(K)}$ est valide partout, $\text{(L)}$ l’est dans tout arbre fini transitif, et les règles de la logique modale normale conservent la validité. La complétude, due à Krister Segerberg (1971), est plus délicate, car la méthode du modèle canonique du chapitre précédent ne s’applique plus telle quelle. Elle a une conséquence pratique agréable : pour savoir si une formule est un théorème de $\textbf{GL}$, il suffit de chercher un contre-exemple parmi des arbres finis de taille bornée. La logique $\textbf{GL}$ est décidable, alors que l’arithmétique, elle, ne l’est pas.
Retour à l’arithmétique : le théorème de Solovay
Reste la question essentielle. On a justifié les axiomes de $\textbf{GL}$ par des propriétés de la prouvabilité arithmétique. Mais en a-t-on oublié ? Existe-t-il d’autres lois générales de la prouvabilité, que $\textbf{GL}$ ne verrait pas ?
Pour donner un sens précis à la question, on appelle traduction arithmétique d’une formule modale le résultat obtenu en remplaçant chaque variable $P$, $Q$,… par un énoncé arithmétique de son choix, et chaque $\Box$ par $\text{Bew}$.
Théorème de Solovay (1976) :
Une formule modale est un théorème de $\textbf{GL}$ si et seulement si toutes ses traductions arithmétiques sont prouvables dans $\text{PA}$.
Le sens direct est la correction arithmétique de $\textbf{GL}$ : c’est le travail fait plus haut. La réciproque, sa complétude arithmétique, est le tour de force de Robert Solovay : si une formule modale n’est pas un théorème de $\textbf{GL}$, il existe un arbre fini qui la réfute, et Solovay parvient à « plonger » cet arbre dans l’arithmétique pour fabriquer des énoncés qui la réfutent aussi.
La boucle est bouclée. Tout ce que l’arithmétique est capable de démontrer, en toute généralité, sur sa propre prouvabilité tient dans un axiome, $\text{(L)}$, et se lit sur de petits arbres finis. Il est rare qu’un sujet aussi vertigineux se laisse résumer aussi simplement.