J'ai déjà exploré assez en détail le sujet des (très très) grands nombres. Je ne vais pas revenir sur tout ce que j'ai dit (et comme d'habitude, je tenterai de ne garder mes posts indépendants les uns des autres), mais je veux me servir de cette question pour illustrer quelques faits de logique rigolo.
[Ajout : voir aussi ce message sur Reddit où j'explique de façon peut-être plus pédagogique (mais en anglais) en gros les mêmes choses que ci-dessous.]
Imaginons qu'un génie pervers nous mette devant un ordinateur et nous donne la tâche d'écrire — dans un langage de programmation idéalisé de notre choix — un programme qui calcule le nombre le plus grand possible avant de s'arrêter. (Le programme en question tournera sur l'Infinitiplex du génie, équivalent à une machine de Turing qui dispose de ressources de calcul illimitées : donc ni le temps de calcul ni la mémoire consommée ne sont à prendre en compte, seul importe le nombre renvoyé ; en revanche, évidemment, la taille du programme doit rester humainement gérable ; par ailleurs, le programme doit effectuer un calcul déterministe et s'arrêter de lui-même, sans intervention extérieure.)
La stratégie intelligente à utiliser serait quelque chose comme ceci :
Soit T une théorie logique raisonnablement puissante et contenant l'arithmétique ; par exemple : ZFC. [On verra plus bas qu'on devra supposer la Σ₁-véracité-arithmétique de T.]
Appelons F:N↦F(N) (ou plus exactement FT) la fonction ainsi calculée :
- énumérer toutes les suites de symboles de longueur ≤N,
- parmi celles-ci, rechercher toutes celles qui sont des démonstrations valides dans la théorie T (c'est-à-dire que chaque ligne est soit un axiome de T soit le résultat de lignes antérieures par application des règles de la logique, ce qui se teste algorithmiquement sans aucun problème),
- parmi celles-ci, rechercher toutes celles dont la conclusion est de la forme
l'exécution de la machine de Turing <M> termine (quand démarre à partir d'un ruban vierge)[on peut, bien sûr, remplacer les machines de Turing par toute autre langage de programmation idéalisé bien défini donc susceptible d'être formalisé dans l'arithmétique],- lancer (c'est-à-dire, simuler) l'exécution de toutes ces machines de Turing M, et attendre qu'elles s'arrêtent, en comptant le nombre de pas d'exécution,
- renvoyer la somme de tous ces temps d'exécution.
Le programme effectue le calcul de F(101000) (disons).
D'ailleurs, je ne suis pas le seul à proposer cette idée : un concours de ce genre a été fait (écrire le programme en C idéalisé qui calcule le nombre le plus grand possible en 512 octets de code source), et le gagnant est celui qui a utilisé cette stratégie avec, pour T le calcul des constructions de Coquand-Huet, une logique d'ordre supérieur qui a l'avantage d'unifier le programme et sa preuve de terminaison. Je suis d'ailleurs très impressionné que quelqu'un ait réussi à implémenter la normalisation du calcul des constructions en 512 octets de C.
Dès que la théorie T est raisonnablement puissante, ceci calcule un nombre extraordinairement grand. Pour tout T non ridiculement faible, la valeur FT(10↑1000) va dépasser, par exemple, le nombre de Graham (et de très loin) : en effet, il est très facile de montrer que le programme évident qui calcule ce nombre, et le convertit en unaire, termine — ceci demande certainement moins de 10↑1000 symboles à démontrer, et ce, dans une théorie T passablement faible. Donc, au cours du calcul de F(10↑1000), on va énumérer cette démonstration, puis exécuter le programme correspondant, et du coup, F(10↑1000) dépasse largement le nombre de Graham. Ce même argument vaut — par définition même de la fonction F — pour toute valeur qui peut être calculée par un programme dont la terminaison peut être prouvée par une démonstration de longueur raisonnable (dans le système T choisi).
Plus le système T est puissant, plus il montrera la
terminaison de machines de Turing compliquées, et plus le
nombre FT(10↑1000) calculé sera
grand. Par exemple, si T est l'arithmétique de Peano du
premier ordre, comme expliqué ci-dessus, on peut facilement formaliser
le fait que la machine qui calcule
la fonction
d'Ackermann termine (i.e., Peano sait que cette fonction est bien
définie), donc F(10↑1000) va dépasser les quantités
facilement construites à partir de la fonction d'Ackermann (ou ses
variantes, ce qui inclut le nombre de Graham qui est essentiellement
64 itérations de la fonction d'Ackermann). Pour un
système T capable de prouver la terminaison
des suites
de Goodstein (cette fois, Peano ne suffit plus,
mais ZFC si), alors le nombre va dépasser tout ce qu'on
peut raisonnablement décrire avec des opérations comme la longueur
de la suite de Goodstein commençant par <tant>
(cette
fonction croissant considérablement plus vite que la fonction
d'Ackermann).
En fait, comme je vais l'expliquer, si le but est de fabriquer le nombre le plus grand possible, il vaut mieux viser le système T le plus fort possible, plutôt qu'essayer d'améliorer d'autres aspects du programme (par exemple remplacer 10↑1000 par 10↑(10↑1000) ou quelque chose comme ça, ou même imbriquer 10↑1000 fois la fonction F).
Voici une première observation assez triviale : le système T lui-même ne peut pas prouver en moins de N symboles que F(N) est bien définie (i.e., que le programme qui le calcule termine) : en effet, si c'était le cas, le calcul de F(N) lui-même ferait partie des machines M dont il énumère une preuve de terminaison, et du coup F(N) se simulerait lui-même, or dans ce cas il ne termine certainement pas. Ou, si on préfère : comme F(N) est plus grand que le résultat de tout calcul M dont T prouve la terminaison en moins de N symbole, T ne peut évidemment pas prouver la terminaison de ce calcul-là.
Ceci peut ressembler à un paradoxe. La terminaison
de F(N) n'est-elle pas évidente pour n'importe
quel N ? Après tout, l'énumération des chaînes de longueur
au plus N termine évidemment, et pour ce qui est de la
seconde partie du calcul, on a une preuve (dans T)
de la terminaison de chacune des machines M qui sont
lancées, donc il faut bien qu'elles terminent. C'est, en effet, le
cas, si on a fait l'hypothèse suivante sur la théorie T :
que dès que celle-ci prouve la terminaison d'une machine de
Turing M, alors cette machine termine effectivement ; cette
hypothèse (T ne dit pas de bêtises, au moins s'agissant
de la terminaison des machines de Turing
), i.e., le fait que
certaines conclusions de T
soient vraies, s'appelle
la Σ₁-véracité-arithmétique de la théorie T (on dit
parfois : 1-consistance de T ; la définition n'est pas tout
à fait la même, mais au final cela revient au même). Si on veut, il
s'agit d'une affirmation plus forte que la consistance
de T : la consistance de T demande
que T ne démontre pas l'énoncé absurde 0=1, la
Σ₁-véracité-arithmétique demande que tout ce que T démontre
et qui peut se mettre sous la forme <telle> machine de Turing
termine (à partir d'un ruban vierge)
est vrai, ce qui est
visiblement plus fort (si T démontre 0=1, elle démontre
n'importe quoi, y compris que termine une machine de Turing qui fait
une boucle infinie triviale). (La Σ₁-véracité-arithmétique
de T est même assez trivialement équivalente à
l'énoncé pour tout N, la
valeur FT(N) est définie
[i.e., le calcul termine]
.)
Digression : Un exemple de
théorie consistante mais non Σ₁-arithmétiquement-vraie
(=1-consistante) est la théorie PA♠ définie
comme PA + ¬Consis(PA), i.e., l'arithmétique
de Peano (PA) à laquelle on ajoute
l'axiome l'arithmétique de Peano est inconsistante
. D'après le
théorème d'incomplétude de Gödel, cette
théorie PA♠ est consistante (puisque
si PA+¬Consis(PA) démontrait 0=1, alors par
pure application des règles de logique, PA démontrerait
Consis(PA)), même si cela peut sembler étrange vu qu'elle
prétend elle-même être inconsistante ! Et comme elle
(PA♠) prétend que PA démontre 0=1, elle
prétend que la machine de Turing qui énumère toutes les chaînes de
caractère à la recherche d'une preuve de 0=1 dans PA
termine — or cette machine, en vrai, ne termine pas,
donc PA♠ n'est pas Σ₁-arithmétiquement-vraie.
Du coup, le fait que T (supposée consistante) ne puisse
pas prouver que pour tout N le calcul
de F(N) termine ne doit pas être une surprise :
c'est un avatar du théorème de Gödel, selon lequel T ne
peut même pas prouver que T ne prouve pas 0=1, donc a
fortiori pas que ce qu'elle démontre est vrai, même pas pour
quelque chose d'aussi trivial que 0=1
ou encore
moins <telle> machine de Turing termine
.
En revanche, si T♯ est une théorie
contenant T et qui prouve (ou qui postule) que T
est Σ₁-arithmétiquement-vraie (il n'y a pas de difficulté à formaliser
cette notion), alors la
fonction F♯:=FT♯ associée
à T♯ est considérablement plus grande que la
fonction F:=FT associée
à T : en effet, d'après l'hypothèse faite, on peut écrire
dans T♯ toute démonstration qu'on pouvait déjà écrire
dans T, mais aussi utiliser le principe si T
montre qu'une machine de Turing s'arrête, alors elle s'arrête
vraiment
, et donc conclure (en un nombre raisonnable de symboles)
que F est bien définie. Donc (pour peu que la preuve de la
Σ₁-véracité-arithmétique de T dans T♯ ne soit
pas d'une longueur délirante) F♯(10↑1000) va sans
difficulté
dépasser F(F(F(⋯(F(10↑1000)))))
avec F(10↑1000) imbrications de la fonction F
(puisque dès qu'on sait que la fonction F est bien définie,
on n'a aucun mal à écrire des programmes qui terminent en l'utilisant
de cette manière).
Le raisonnement du paragraphe précédent vaut, notamment,
si T est PA (l'arithmétique de Peano du
premier ordre) est T♯ est ZFC : en
effet, ZFC montre sans difficulté que toute conséquence
arithmétique de PA est vraie, et en particulier toute
conséquence du type <telle> machine de Turing termine
.
Donc la fonction F associée à ZFC
croît considérablement plus vite que celle associée
à PA (euphémisme !). De façon peut-être plus
surprenante, le raisonnement vaut aussi si T
est ZFC et que T♯ s'obtient en rajoutant
l'hypothèse (IC) de l'existence
d'un cardinal
inaccessible : en effet, ZFC+IC démontre
l'existence de ce qu'on appelle un « modèle transitif »
de ZFC, i.e., un ensemble qui se comporte comme un petit
monde dans lequel tous les axiomes de ZFC sont vrais
(pour la même relation d'appartenance), ce modèle ayant les mêmes
entiers naturels que les vrais,
donc ZFC+IC démontre que toute conséquence
arithmétique de ZFC est vraie, et en particulier
que toute machine de Turing dont ZFC démontre la
terminaison termine effectivement.
Ainsi, FZFC+IC croît
beaucoup plus vite que FZFC. Et la
même chose vaut essentiellement pour toute notion de grand cardinal
par rapport à une moins forte : plus on ajoute des grands cardinaux en
pertant de T=ZFC, plus on obtient des
fonctions qui croissent vite (et donc, in fine, des valeurs
plus grandes de F(10↑1000) : il y a quelque chose de
satisfaisant à ce que les grands cardinaux aident à fabriquer des
grands entiers naturels).
Bref, ZFC+IC prouve, de façon raisonnablement courte, que FZFC(N) est défini pour tout N, et notamment que FZFC(10↑1000) l'est. Comme je l'ai expliqué, par ailleurs, il est évident que ZFC seul ne peut pas prouver en moins de 10↑1000 symboles que FZFC(10↑1000) est défini. En fait ZFC prouve bien que FZFC(10↑1000) est défini, et la démonstration est certes longue, mais pas beaucoup plus longue que 10↑1000 symboles (disons à la louche que 10↑10000 devraient suffire : en tout cas, nettement moins que les nombres totalement colossaux produits par nos diverses fonctions F). Pourquoi ? Cela résulte de l'observation triviale suivante : une démonstration de longueur inférieure à N (disons 10↑1000) dans ZFC ne peut pas utiliser d'axiome de ZFC de longueur supérieure à ce nombre (rappelons que ZFC a un nombre infini d'axiomes, à cause du schéma de compréhension et surtout celui de remplacement) ; or un lemme de réflexion montre, dans ZFC, que tout sous-ensemble fini explicite donné des axiomes de ZFC a un « modèle transitif », et donc (ce qui nous intéresse ici) a des conséquences arithmétiques vraies. (On peut même, pour tout k explicite donné, que ZFC dont le schéma de remplacement a été limité aux prédicats ayant au plus k alternations de quantificateurs — voir aussi ici — a un modèle transitif ; et la démonstration se fait suivant un modèle simple en fonction de k.) Quand on analyse, cette démonstration écrite complètement dans ZFC, on voit qu'elle fait une longueur polynomiale en N (avec un degré sans doute assez petit et des coefficients raisonnables — je n'ai pas fait l'analyse complète). Notamment, ZFC prouve que FZFC(10↑1000) est bien défini en une longueur certes plus longue que 10↑1000 symboles, mais certainement moins longue que 10↑10000.
Pour récapituler, on est dans la situation un peu étonnante suivante :
- Pour chaque N (explicite), ZFC prouve
que
FZFC(N) existe
(i.e. que toute machine de Turing dont ZFC prouve la terminaison en moins de N symboles termine effectivement) ; de plus, une preuve de ce fait est de longueur polynomiale en N et est produite par un programme extrêmement simple en fonction de N (il s'agit de la bête application d'un certain motif) ; mais toute preuve doit être de longueur supérieure à N. - De plus, ZFC+IC (ou même des hypothèses
plus faibles au-dessus de ZFC) prouve (en une longueur
tout à fait raisonnable)
que
FZFC(N) existe pour tout N
. - En revanche, ZFC (supposé consistant) ne prouve pas
que
FZFC(N) existe pour tout N
.
Ceci illustre plusieurs phénomènes. D'une part, l'accélération des
démonstrations : la longueur de la plus courte preuve
dans ZFC
de FZFC(10↑1000) existe
est,
disons, quelque part entre 10↑1000 et 10↑10000 symboles, alors que
dans ZFC+IC, elle est nettement plus courte
que 10↑1000 symboles. (Notons que
l'énoncé FZFC(10↑1000)
existe
est même prouvable dans PA ou dans des
systèmes extrêmement faibles de l'arithmétique : après tout,
pour prouver qu'une machine de Turing termine, il suffit d'écrire sa
trace d'exécution complète comme démonstration ! Mais ceci donne une
démonstration de longueur vraiment colossale, puisque comparable au
nombre dont elle affirme l'existence.)
Ensuite, c'est un cas très explicite d'incomplétude : pour
chaque N on peut produire, selon un motif simple, une
démonstration dans ZFC
de FZFC(N)
existe
, mais on ne peut pas en produire une de pour
tout N, FZFC(N)
existe
. Du coup, je trouve que ceci illustre la mauvaise foi de
la position épistémologique je ne crois qu'à ce qui est démontré
dans ZFC
: personne ne va écrire séparément la
démonstration
de FZFC(N) existe
pour un N donné (ça n'a aucun intérêt : elle se produit
trivialement en fonction de N), mais cette position oblige
à dire qu'on l'accepte que comme démonstration du fait
que FZFC(N)
existe
pour n'importe quel N, mais pas du même énoncé
quantifié par pour tout N
! Ceci vaut notamment
pour les gens qui se cachent derrière leur petit doigt en disant je
ne sais pas si ZFC est consistant
(de
fait, ZFC ne le démontre pas) : je rappelle que
l'énoncé pour
tout N, FZFC(N)
existe
implique notamment la consistance de ZFC (il
est équivalent à sa Σ₁-véracité-arithmétique), or je viens d'expliquer
qu'il faut être pas mal de mauvaise foi pour prétendre ne pas savoir
que pour
tout N, FZFC(N)
existe
alors qu'on sait pour tout N
que FZFC(N)
existe
!
D'un autre côté, si on cherche à calculer le nombre le plus grand possible (pour répondre au défi du génie pervers), on est devant le problème insoluble suivant : quelle est la théorie la plus forte possible dont on soit « convaincu » qu'elle soit Σ₁-arithmétiquement-vraie ? Après tout, ZFC n'est le cadre « orthodoxe » des mathématiques que par une sorte d'accident historique (le schéma de remplacement est déjà une sorte d'axiome de grand cardinal appliqué à la classe des ordinaux et revient plus ou moins à dire que celle-ci est un cardinal inaccessible), il n'est pas magiquement plus convaincant que ZFC+IC sous prétexte qu'on a plus travaillé dedans (ou même, fait semblant de travailler dedans). Les axiomes de grands cardinaux les plus forts connus au-dessus de ZFC et au sujet desquels on ne semble pas arriver à montrer d'inconsistance sont les axiomes de rank-into-rank (et spécifiquement l'axiome I0 de Woodin) ; il y en a peut-être d'encore plus forts si on supprime l'axiome du choix [les choses sont confuses quant à la force arithmétique de ces axiomes : cf. ici].
Je souligne que plus fort
ici fait référence à la
force arithmétique de ces théories, et même à la force
arithmétique Σ₁, c'est-à-dire à la capacité à montrer que des machines
de Turing s'arrêtent : on ne demande pas de croire que ces grands
cardinaux « existent » en un sens platonique profond, juste de croire
qu'ajouter à la théorie des ensembles le postulat de leur existence
produit des conséquences exactes sur l'arrêt des machines de Turing !
(On pourrait même utiliser
le théorème de
Matiâsevič-Robinson-Davis-Putnam pour reformuler ces conséquences
sous la forme d'existence de solutions d'équations
diophantiennes.)
Il se trouve que les systèmes connus qui sont arithmétiquement les plus forts (i.e., qui au moins paraissent arithmétiquement vrais et qui produisent les conséquences les plus fortes, donc la fonction FT la plus grande) sont tous des théories des ensembles de type ZF(C) obtenues en ajoutant des axiomes de grands cardinaux. Il n'y a pas de raison évidente à ça : il pourrait très bien s'agir d'autres types de théories des ensembles (je pense aux théories des ensembles de type NF(U) ; d'ailleurs, certaines variantes se mesurent très bien contre ZF) ou encore de systèmes de typage (par exemple, le calcul des constructions inductives (CCI) se compare bien à ZFC [correction : les choses sont plus obscures que ça, cf. l'entrée suivante] et l'ajout d'univers de types à CCI à l'ajout de cardinaux inaccessibles à ZFC, donc on pourrait imaginer des extensions du calcul des constructions qui soient au niveau de force arithmétique de ZFC + tel ou tel grand cardinal ; mais je ne crois pas qu'on en ait défini), ou une tout autre chose. Je ne sais pas s'il faut y voir le signe qu'il est plus naturel de faire des théories fortes à partir de ZF(C) ou simplement que ZF a été plus étudié.
Addendum () :
Je peux aussi faire la remarque rigolote suivante : dans le même ordre
d'idées que ce que je décris ci-dessus, on pourrait écrire un
programme de compression [sans perte] qui est en un certain sens
optimal modulo la force d'une théorie logique T. Ce
programme effectue le calcul suivant : donnée une donnée Y
à comprimer, on énumère, dans l'ordre de longueur, toutes les
démonstrations dans T (par exemple : ZFC) dont
la conclusion est de la forme la machine de Turing M,
quand on lui fournit l'entrée X, termine
(noter que
cette démonstration doit faire au moins la longueur de M
plus celle de X, juste pour énoncer la conclusion) ; à
chaque fois qu'on en trouve une, on simule l'exécution de la
machine M sur l'entrée X, et dès qu'on en trouve
une dont la sortie coïncide avec le Y à comprimer, on
s'arrête, la compression étant alors donnée par le couple
(M,X) (on pourrait d'ailleurs se passer
de X complètement et produire seulement M, mais
l'intérêt de mettre les deux est qu'on n'a pas à s'embêter à chercher
comment encoder optimalement les machines de Turing). Bref, la
compression de Y est le couple (M,X)
pour lequel on a la plus courte démonstration dans T du
fait que M termine sur X et pour lequel par
ailleurs le résultat de ce calcul vaut Y (attention !, ce
dernier fait est vérifié par le programme de compression mais n'est
pas inscrit dans la démonstration faite dans T !). Ce
programme de compression termine si la théorie T est
Σ₁-arithmétiquement-vraie, car toutes les exécutions simulées de
couples (M,X) termineront, et on finira bien par
en trouver une qui produit la sortie Y voulue (au pire, et
c'est ce qui se passera presque toujours si Y est
« aléatoire », on tombera sur la démonstration du fait que la machine
qui termine immédiatement sans rien faire — donc qui calcule la
fonction identité — termine quand on la lance sur
l'entrée Y elle-même). On peut décomprimer
(retrouver Y) en simulant l'exécution de la
machine M sur l'entrée X. Mon programme de
compression sera, à une constante près, au moins aussi bon que,
disons, gzip, parce qu'on peut facilement prouver
dans ZFC que gunzip termine sur toute
entrée, donc la démonstration du fait que
(où X est la sortie
de gunzip
termine sur l'entrée Xgzip(Y)) a une longueur comparable à celle
de X plus une petite constante indépendante
de X, et du coup borne la taille de la sortie de mon
programme. On pourrait dire que mon programme calcule non pas
la complexité
de Kolmogorov de Y, mais son approximation vue par la
théorie T.