Le but des mathématiques est d'établir des vérités absolues qui ne sont pas liées à une réalité physique particulière. En ce sens, les mathématiques peuvent être considérées comme l'étude du néant, et paradoxalement ce néant a une structure très riche. Pour établir ces vérités de façon certaine, des mathématiciens comme Hilbert voulaient les faire reposer sur une construction rigoureuse faite de vérités simples considérées comme évidentes appelées axiomes, assemblées gràce à des régles considérées également comme évidentes. C'est ce qu'on appelle un système formel.
Mais Gödel a démontré que dans
tout système formel assez puissant pour posséder le concept de nombre,
on peut construire une proposition qui exprime sa propre indémontrabilité :
les propositions et les démonstrations sont codées par des nombres et on
construit une proposition de la forme :
"Il n'existe pas de nombre qui
code une démonstration de la proposition codée par le nombre g."
et qui a
pour code le nombre g lui-même. Pour cela on part de la proposition F
codée par le nombre f :
"Il n'existe pas de nombre qui code une démonstration de la proposition
codée par le nombre qui code la proposition obtenue en substituant par
le nombre u la variable libre de la proposition codée par le nombre u."
Cette proposition comporte une variable libre u.
En remplaçant cette variable par le code f de cette proposition, on obtient
la proposition G codée par g :
"Il n'existe pas de nombre qui code une démonstration de la proposition
codée par le nombre qui code la proposition obtenue en substituant par
le nombre f la variable libre de la proposition codée par le nombre f,
c'est-à-dire la proposition F".
Or la proposition obtenue en substituant par le nombre f la variable libre de
F étant la proposition G, celle-ci peut s'écrire :
"Il n'existe pas de nombre qui code une démonstration de G"
c'est-à-dire :
"Je ne suis pas démontrable".
On peut remarquer que cette construction est isomorphe à celle du
combinateur de point fixe en logique combinatoire et en lambda-calcul,
consistant à définir le point fixe d'une fonction comme l'auto-application
de cette fonction et de la fonction d'auto-application :
Y f = A (B f A) = B f A (B f A) = f (A (B f A))
La construction
de G consiste en quelque sorte à
construire un point fixe de la non démontrabilité.
On a donc une propositon G qui exprime sa propre indémontrabilité dans le système formel considéré. Si elle est vraie, le système est incomplet. Si elle est fausse, alors elle est démontrable et le système est inconsistant.
Pour franchir cette limitation, on pourrait ajouter la proposition G en axiome à un système S0 incomplet dans lequel elle n'est pas démontrable. On peut également ajouter une proposition appelée principe de réflexion qui dit que si d est le code d'une démonstration D et p est le code de la conclusion de D, alors la proposition P codée par p est vraie. Ce principe consiste en quelque sorte à donner au système une connaissance de lui-même. Mais on obtient alors un nouveau système formel S1 auquel on peut appliquer le même raisonnement pour obtenir une proposition G1 qui n'est pas démontrable dans S1. On pourrait alors ajouter S1 en axiome à G1 pour obtenir un système S2, et ainsi de suite. On pourrait même englober cette suite infinie de systèmes dans un système Sw qui aurait lui-même sa proposition gödelienne Gw qu'on pourrait ajouter à Sw pour obtenir Sw+1, et ainsi de suite, Sw+2, ... Sw*2, Sw*3, ... Sw^2, ... Sw^w, Sw^w^w, ... S epsilon0, S epsilon1 ... autrement dit une suite transfinie de systèmes formels. Feferman a démontré que l'itération transfinie du principe de réflexion permet d'engendrer toutes les vérités de l'arithmétique.
C'est là qu'intervient l'intelligence créative, car la production d'ordinaux transfinis de plus en plus grand n'est pas automatisable : à tout programme produisant une suite d'ordinaux x0, x1, x2, ... on peut associer un ordinal limite xw et continuer avec xw+1, ... Le problème consiste à s'apercevoir quand on est dans un processus régulier pour passer à la limite et continuer. Par exemple, quand on passe de 0 à suc 0, puis suc (suc 0), ... on voit que c'est un processus régulier qui a pour limite w. Mais plus on monte dans les grands ordinaux, plus les régularités deviennent subtiles et difficiles à déceler et plus on risque de tourner en rond en croyant avancer.
On peut ainsi emmagasiner de l'intelligence dans un grand ordinal
transfini et la restituer dans un système formel en effectuant l'inération
transfinie jusqu'à cet ordinal du principe de réflexion.
La quintessence de l'intelligence créative, non automatisable, consiste
à déceler des régularités. On peut la formaliser par la capacité à
représenter une expression par une description la plus compacte possible.
Par exemple, "rep 10 suc 0" (où rep désigne la répétition
d'une opération un certain nombre de fois) est plus compacte que
"suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 0)))))))))".
On pourrait produire une suite d'ordinaux transfinis de plus en plus grands
de la façon suivante : on part de 0 puis on répète indéfiniment un processus
consistant à prendre le successeur, décrire de façon compacte, et
quand un nombre n apparait dans une expression e[n], passer à la limite
de la fonction qui à x associe e[x].
Ainsi, on obtient 0, suc 0, suc (suc 0), ... et il arrive un moment (qui
dépend de la façon exacte de mesurer la taille d'une expression) où on
pourra compacter l'expression en une expression de la forme rep n suc 0,
par exemple rep 5 suc 0. On passe alors à la limite de (lambda x. rep x suc 0)
que l'on peut noter rep w suc 0, et qui vaut w, puis on continue avec
suc (rep w suc 0) = w + 1,... rep 5 suc (rep w suc 0),
rep w suc (rep w suc 0) = w * 2, ...
rep w (rep w suc) 0 = w ^ 2, ...
rep w (rep w (rep w suc)) 0 = w ^ 3, ...
rep 5 (rep w) suc 0 = w ^ 5,
rep w (rep w) suc 0 = w ^ w, ...
rep w (rep w) (rep w) suc 0 = w ^ w ^ w, ...
et ainsi de suite.