Grands cardinaux, Woodin, Laver

Un exemple simple de telle fonction RECURSIVE TOTALE:

Entrée un entier n:

1/ regarder la conclusion de la preuve dont n est le code.

2/ Si elle est de la forme ZF + SuperBigGC prouve qu'une équation diophantienne E a une solution, lancer la recherche de ladite et la renvoyer, sinon, renvoyer 0

Cette fonction est non seulement récursive, mais aussi TOTALE mais aussi croît plus vite que n'importe quelle fonction récursive totale habituelle du quotidien des matheux (et pas qu'un peu).

@François D :
1) Je comprends ta confusion concernant les cardinaux Woodin.
Il y a quelque part dans le livre de Dehornoy une phrase où il dit que les cardinaux Woodin témoignent de l'existence de très grosses bestioles mais qu'en eux-mêmes ils ne sont pas si gros que ça.
C'est probablement cette phrase qui a jeté le trouble dans ton cerveau… et j'ai eu la même réaction que toi.
Comme la phrase n'était pas très claire je lui ai demandé de préciser : en fait un Woodin témoigne du fait qu'en dessous de lui il y a une tétrachiée de cardinaux mesurables, ce qui est pour le moins éloquent. Mais (contrairement à ce que je craignais), il ne dit rien sur ce qui se passe au-dessus de lui.
Ce qui fait dire à Dehornoy que les Woodin sont (relativement) petits, c'est que le plus petit Woodin (s'il existe) n'est pas mesurable, et même pas faiblement compact.
2) Concernant les cardinaux Laver : il y a 2 applications de l'existence d'un cardinal I3 (ou Laver) : la première concerne les groupes B-infinis de tresses à une infinité de brins (j'y connais que dalle), et là, Dehornoy a réussi à raccommoder les ficelles en montrant qu'on pouvait se passer de l'existence de GC et démontrer le résultat dans une théorie beaucoup plus faible (genre ZF ou encore moins, je ne sais plus).
Par contre pour les tables de Laver on ne sait rien faire pour l'instant sans hypothèse de GC.
Le seul truc qu'on sait c'est que le plus petit entier n tel que la nième table de Laver où la période de 1 est 32 (s'il existe) est un truc absolument énorme.
Il y a donc effectivement une solution algorithmique, mais il faudrait attendre des milliards d'années pour savoir si la période 32 apparaît… et encore cela ne nous dirait rien sur l'apparition éventuelle de la période 64.
Pour répondre à la fin de ta question 2), même si quelqu'un démontre dans Peano les résultats sur la périodicité des tables de Laver, ça ne prouvera rien sur l'existence ou non de GC.
Cela prouvera seulement que I3 n'est pas nécessaire à la preuve du théorème.
De toutes façons il y a un phénomène général : soit H n'importe quelle hypothèse de grande cardinalité.
Non seulement ZFC ne prouve pas H, mais la consistance de ZFC ne prouve pas la consistance de ZFC + H.
C'est pour ainsi dire une conséquence immédiate du second théorème d'incomplétude de Gödel.
En gros, la hiérarchie des grands cardinaux peut s'organiser en une suite H_0, H_1, …, H_n etc telle que (toujours en gros) la théorie ZFC + H_n+1 prouve la consistance de ZFC + H_n, mais la consistance de ZFC + H_n ne prouve pas la consistance de ZFC + H_n+1...
Et comme on n'est même pas sûr de la consistance de ZFC (ni même de Peano, ni même de Robinson = Peano faible), la conclusion de tout ça est qu'on passe une partie de notre vie à jouer à l'apprenti sorcier.
C'est exactement ce qu'a fait Kunen quand il a expliqué à Reinhardt que son GC révolutionnaire (l'ordinal critique d'un plongement élémentaire non trivial de V dans lui-même) était inconsistant avec ZFC.
Pour info : si tu tapes "Cantor's attic" dans google tu vas trouver une giga-tera-peta-tonne d'informations là-dessus.

@Christophe : si j'ai raconté des conneries ci-dessus tu as le droit de me le dire haut et fort !