tl;dr Ce code genère cette formule mathématique, qui est vraie, mais indémontrable dans l'arithmétique de Tarksi. Woo.

Il y a quelques années, j'ai lu Les théorèmes d'incomplétude de Gödel, un petit bouquin de Smullyan qui explique de façon claire et simple les théorèmes d'incomplétude de Gödel (incroyable, n'est-ce pas ?). À l'époque, j'en avais vaguement entendu parler, ça avait l'air fascinant, et j'avais envie de savoir comment ça marchait pour de vrai, et comment on pouvait construire en pratique l'étrange animal dont mon prof de maths de l'époque (béni soit-il) avait mentionné l'existence : une proposition mathématique vraie mais indémontrable, qui par une étrange pirouette arrive à exprimer exactement « je ne suis pas démontrable ».

Le bouquin est très bien écrit, mais c'était quand même un poil ardu pour le taupin que j'étais, du coup je le lisais par petits bouts et puis l'oubliais. L'été entre mes deux années de prépa, je me suis plongé dedans sérieusement, et ai décidé d'avoir une lecture un peu plus organisée. Et comme je ne suis pas doué pour prendre des notes, et que j'ai compris que la preuve se résumait à répondre à la question « comment construit-on la proposition étrange qui affirme sa propre indémontrabilité ? », je me suis dit que j'allais faire mieux que prendre des notes, j'allais écrire la proposition pas à pas.

Évidemment, comme le fait si justement remarquer David Monniaux dans un récent billet, la construction est longue et la proposition obtenue est « très long[ue], illisible pour un humain », il n'est donc pas question de le faire à la main. Du coup, comme à l'époque, j'étais aussi en train d'apprendre OCaml (tout seul, parce que ma prépa pensait que c'était une bonne idée de nous apprendre le Pascal en cours d'informatique), je me suis dit que j'allais écrire un programme qui faisait ça à ma place.

Du coup, c'est ce que j'ai fait. C'était effectivement fastidieux, ça n'a — pour reprendre les mots pleins de sagesse et de vérité de David Monniaux « pas grand intérêt », mais je me suis quand même amusé, et ça m'a permis d'avoir une idée plus "pratique" de comment ça marchait (vu qu'écrire un programme qui génère la proposition revient essentiellement à refaire toute la preuve étape par étape). Et sur les conseils d'amis qui m'ont prétendu que ça valait la peine de ressortir ça de mes dossiers poussiérieux, je me suis dit que j'allais le publier ici. Voici donc le code avec une jolie coloration syntaxique, et voilà le fichier original.

C'est loin d'être le code le plus propre du monde (hé, je débutais), mais c'est commenté de façon assez extensive, et je l'ai relu et ré-indenté récemment, donc ça Devrait™ être lisible. Je reproduis presque intégralement la preuve dans les commentaires, mais c'est probablement beaucoup plus compréhensible avec le livre sous les yeux. Il y a peut-être des erreurs qui ont survécu aux multiples relectures ; et comme ce n'est pas vérifié en Coq, c'est impossible d'être absolument certain que le résultat est bien indécidable.

À propos de résultat, voici la formule obtenue. Il y a plusieurs choses à dire à son sujet. L'alphabet utilisé est décrit dans le commentaire en haut du fichier .ml, mais je l'imprime en utilisant des raccourcis (pour les opérations arithmétiques, et surtout pour les numéros de variable), pour que ça soit (ahem) plus lisible. Les E et les A sont des quantificateurs (OCaml n'aime pas Unicode), respectivement existentiels et universels.

La taille de la chaîne de caractère imprimée est de l'ordre de quelques centaines de milliers de caractères. Ça n'a en fait pas grande signification, étant donné que les nombres sont codés en unaire et que je les imprime en binaire… La véritable taille est donc plus grande, mais en fait, beaucoup plus grand, parce qu'elle contient des constantes du genre 812939 qui codent "en dur" le numéro de Gödel de certaines propositions. Évidemment, la présence de ces grosses constante n'est pas nécessaire, on pourrait écrire à la place un terme plus court qui est égal à cette formule… Bref, on ne peut pas dire grand-chose d'intelligent de la taille de cette formule, à part « c'est probablement non-trivial d'arriver sous la centaine de milliers de caractères à coup d'optimisations mineures ».

(La question « quelle est la plus petite formule indémontrable » est, je pense (sans avoir le moindre morceau de science pour étayer cette hypothèse), indécidable — je doute qu'on puisse prouver d'une formule « ceci est la plus petite formule indémontrable » — mais ne serait-ce que savoir qu'une formule de, disons, quelques centaines ou milliers de caractères est indémontrable serait intéressant. Peut-être qu'une piste serait d'utiliser le théorème d'incomplétude de Chaitin et d'encoder la formule K(s) ≥ L dans notre langage pour un L assez grand.)