La thèse de Church entraîne l'incomplétude de Gödel

Une théorie formelle est la donnée d'un langage formel, d'un ensemble d'axiomes et d'un ensemble de règles d'inférence. On exige d'une théorie formelle les choses suivantes. On peut reconnaître mécaniquement si une formule du langage est un axiome. Et on peut vérifier mécaniquement si une formule est un théorème, c'est-à-dire est une formule du langage dérivable en un nombre fini d'applications des règles d'inférence à partir des axiomes. Si en plus on peut vérifier qu'une formule fermée n'est pas un théorème on dit que la théorie est complète. Une théorie est saine si elle ne prouve que des formules (de l'arithmétique par exemple) qui sont vraies. Le résultat de Gödel est qu'une telle théorie, saine et complète pour l'arithmétique, n'existe pas. Ceci constitue une généralisation du théorème de Gödel à partir de la thèse de Church:

Preuve. En effet, avec la thèse de Church, l'ensemble des fonctions (partielles et totales) calculables est identique à l'ensemble des fonctions programmables, par exemple en Fortran (pour fixer les idées). Considérons une énumération des fonctions de N dans N, programmables (en Fortran ou tout autre langage assez riche ce qui revient au même avec la thèse de Church). Une telle énumération est obtenue en placant les programmes Fortran disposant d'une seule entrée par ordre de longueur. Si plusieurs programmes ont la même longueur, on range ceux-ci par ordre ``alphabétique" (en décidant préalablement de placer un ordre arbitraire sur les touches du clavier). Voilà l'énumération :

$\varphi$₁(x), ϕ₂(x), ϕ₃(x), ϕ₄(x), ϕ₅(x), ϕ₆(x), ϕ₇(x), ...

Etant donné le caractère numériquement codables des programmes, il est possible de traduire les propositions du genre $\exists \; y\; \hspace{0.17em}\; \varphi (x)\; =\; y,\; \hspace{0.17em}\; \exists y\; \hspace{0.17em}\; \varphi (x)\; =\; y,...$ en proposition purement arithmétique. Etant donné le caractère mécanique de la génération des programmes, l'existence d'une théorie formelle saine et complète TFSC, rend la fonction (de 2 entrées) suivante $F$_TFSC intuitivement totale calculable :

$F$_TFSC(z,x) = {{ y $si$ \varphi $$_z(x) = y 0 $si\; TFSC\; prouve$ \hspace{0.17em}\; \exists \hspace{0.17em}\; y\; \varphi $$_z(x) = y }

Comme $F$_TFSC(z,x) est intuitivement calculable, on peut construire une énumération de toutes les fonctions totales calculables suivantes. Avec la thèse de Church, cette énumération contient toutes les fonctions totales calculables.

$\varphi$₁¹³³⁷¹*(x), ϕ₂¹³³⁷¹*(x), ϕ₃¹³³⁷¹*(x), ϕ₄¹³³⁷¹*(x), ϕ₅¹³³⁷¹*(x), ϕ₆¹³³⁷¹*(x), ϕ₇¹³³⁷¹*(x), ...

Mais dans ce cas la fonction diagonale, à une entrée, $G$_TFSC(x) = $\varphi$_x^*(x) +1$,\; est\; totale\; calculable,\; et\; elle\; est\; différente\; de\; toutes\; les\; fonctions$$\varphi$_i$.$G_TFSC$est\; totale\; et\; intuitivement\; calculable,\; mais\; est\; différente\; de\; toutes\; les\; fonctions\; fortran\; programmables,\; en\; contradiction\; avec\; la\; thèse\; de\; Church.\; La\; négation\; du\; théorème\; de\; Gödel\; réfute\; la\; thèse\; de\; Church.\; Donc\; la\; thèse\; de\; Church\; entra\backslash ine\; l\text{'}incomplétude\; de\; Gödel.\; Ce\; qu\text{'}il\; fallait\; démontrer.\; Bien\; s\backslash ur,\; dans$un certain sens G_TFSC$$est fortran programmable : il est possible de décrire l'algorithme présenté plus haut en fortran. Mais, et c'est ce que nous avons montré, la fonction décrite par cette procédure est nécessairement partielle. Pour certaine valeur de x$$G_TFSC(x)$diverge,\; et\; cela\; de\; façon\; non\; prouvable\; par\; la\; théorie\; TFSC.\; On\; pourrait\; trouver\; une\; théorie\; plus\; puissante\; TFSC$$,\; capable\; de\; décider\; si$G_TFSC$diverge,\; mais\; elle\; sera\; incapable\; de\; décider,\; pour\; certaine\; valeur\; de\; x,\; si\; la\; fonction\; correspondante$G_TFSC(x)$$ diverge. La thèse de Church rend absolue la notion de calculabilité, et relative la notion de prouvabilité. Il est raisonnable de penser que si cette preuve avait été présentée à Russell et Whitehead, ils n'auraient pas été convaincus. Ils auraient commencé par farouchement critiquer la thèse de Church, et se seraient sans aucun doute attelé à réfuter cette thèse avec Principia Mathematica. Ce faisant, ils seraient vraisemblablement arrivés au théorème d'incomplétude de Gödel. De cette façon, le théorème de Gödel (1931) confirme la thèse de Church, alias la loi de Post (1922). La thèse de Church confirme à son tour, et rend non triviale, l'hypothèse du mécanisme digitale. En effet, si la thèse de Church était fausse il pourrait exister des machines digitales capables de surpasser (en quantité de fonctions calculables) les ordinateurs. Le théorème de Gödel ne s'appliquerait pas a priori à de telles machines. Avec TC, le théorème de Gödel s'applique à toutes les machines digitales (suffisamment riches, c'est-à-dire capable de démontrer les théorèmes de l'arithmétique élémentaire). La thèse de Church donne donc apparemment un espoir aux non-mécanistes qui voudraient réfuter le mécanisme digital: il suffit de parvenir à montrer que le théorème de Gödel ne s'applique pas à nous, en exhibant par exemple une preuve informelle d'une vérité non machine-accessible. Mais avec TC, une telle preuve ne peut pas être effective, sinon elle est machine accessible. Avec TC et le mécanisme, le théorème de Gödel s'applique aux machines et s'applique à nous. La thèse de Church alliée au mécanisme fait des résultats d'incomplétude les prémisses d'une psychologie exacte (voir aussi le rapport technique Marchal 1995, et Myhill 1952). Judson Webb (1980) résume cette situation en affirmant que la thèse de Church est l'ange gardien du mécanisme. Il montre que la thèse de Church protège le mécanisme de toute vision réductionniste du monde des machines et qu'elle rend les réfutations du mécanisme (ou de la thèse de Church) presqu'automatiquement non-communicable à une troisième personne. Gödel, malgré son théorème de 1931, ne croira pas à d'emblée à la thèse de Church. Après la publication de l'article de Turing (voir [Davis, 1965]), il admettra la thèse de Church, et il estimera que la thèse de Church est une sorte de miracle épistémologique. Pour la première fois une notion métamathématique semble ne pas dépendre du système formel choisi. On dit, en informatique théorique, qu'une telle notion est ``machine indépendante". Cela introduit en quelque sorte une notion objective d'objectivi$té\; :une\; notion\; est\; objective\; si\; elle\; est\; valable\; pour\; toutes\; les\; machines\; universelles.\; C\text{'}est\; cette\; notion\; de\; machine-indépendance\; qui\; nous\; permet\; d\text{'}espérer\; isoler\; une\; mesure\; objective,\; machine\; universelle-indépendante,\; sur\; la\; collection\; entière\; des\; états\; computationnels.\; En\; absence\; du\; ``miracle\; de\; Gödel"\; le\; présent\; travail\; n\text{'}aurait\; aucun\; sens.\; Indépendamment\; de\; Post\; et\; de\; Church,\; Turing\; propose\; une\; thèse\; équivalente\; et\; l\text{'}appuie\; sur\; une\; analyse\; abstraite\; de\; la\; notion\; de\; calculateur\; humain.\; Gödel\; ne\; verra\; pas\; le\; bénéfice\; que\; la\; philosophie\; mécaniste\; peut\; tirer\; de\; la\; thèse\; de\; Church.\; En\; fait\; Gödel\; défendra\; une\; philosophie\; plutôt\; non-mécaniste\; [Wang,\; 1974,Marchal,\; 1990,Marchal,\; 1995].\; Il\; montrera\; par\; ailleurs\; que\; la\; thèse\; de\; Church\; entraîne\; l\text{'}existence\; de\; propositions$absolument indécidables pour l'esprit humain, ce qui ne sembla pas lui plaire . En fait Gödel est pié$gé\; :il\; se\; rend\; compte\; que\; la\; thèse\; de\; Church\; augmente\; considérablement\; la\; portée\; de\; son\; théorème\; d\text{'}incomplétude,\; mais\; il\; n\text{'}apprécie\; pas\; l\text{'}idée\; que\; la\; portée\; du\; théorème\; soit\; agrandie\; au\; point\; de\; s\text{'}appliquer\; à\; nous.\; Aujourd\text{'}hui\; la\; thèse\; de\; Church\; est\; acceptée\; de\; façon\; quasi-unanime\; par\; les\; (méta)mathématiciens\; et\; les\; philosophes\; concernés,\; mais\; cela\; ne\; doit\; en\; aucune\; façon\; nous\; faire\; oublier\; le\; caractère\; révolutionnaire,\; miraculeux\; de\; cette\; thèse.\; On\; définit\; habituellement\; la\; machine\; universelle\; de\; Turing\; comme\; étant\; une\; machine\; de\; Turing\; capable\; d\text{'}émuler\; (simuler\; parfaitement,\; aux\; temps\; d\text{'}éxécutions\; près)\; n\text{'}importe\; quelle\; machine$de Turing. On peut cependant démontrer que la machine de Turing est à même d'émuler n'importe quel programme fortran ou n'importe quel ordinateur quantique, etc. Avec la thèse de Church, la machine universelle de Turing peut émuler n'importe quelle machine digitale. C'est la thèse de Church qui permet de supprimer le qualificatif ``de Turing" pour la machine universelle. La thèse de Church rend ainsi la machine universelle vraiment universelle, et elle rend de la même façon le déployeur universel vraiment universel. En fait, c'est la notion même d'universalité qui est rendue machine-indépendante, et donc épistémologiquement absolue, au sens de Gödel [Gödel, 1946]. La thèse de Church met en outre en évidence une nécessaire activité capitale de la machine consistante universel$le\; :rester\; silencieuse\; lorqu\text{'}on\; lui\; pose\; certaines\; questions,\; ou\; devenir\; inconsistante,\; si\; elle\; veut\; avoir\; réponse\; à\; tout!\; Cela\; joue\; un\; rôle\; récurrant\; pour\; la\; dérivation\; des\; phénoménologies\; de\; l\text{'}esprit\; et\; de\; la\; matière.\; \%\; Bertrand\; Russell\; et\; Whitehead\; devant\; la\; démonstration\; plus\; haut\; \%\; aurait\; \%\; sans\; aucun\; doute\; rejetté\; la\; thèse\; de\; Church\; ...\; \%\; Théorème\; de\; Kleene,\; Case\; et\; autoreproduction.\; \%\; L\text{'}importance\; capitale\; de\; la\; machine\; silencieuse.\; \%\; La\; thèse\; de\; Church\; physique\; (cf\; Deutsch,\; Delahaye)\; \%\; Les\; degrés\; plus\; petits\; que\; 0\text{'}.\; Fonction\; limite\; calculable,\; \%\; et\; \%\; Oracle.\; Et\; le\; lemme\; de\; Shoenfield.\; \%\; thèse\; de\; Church\; intensionnelle\; (TCI),\; extensionnelle\; (TCE)$Remarque La thèse de Church n'est pas une proposition mathématique. Elle appartient au domaine de la philosophie des mathématiques. Elle est scientifique cependant, dans le sens qu'elle est en principe réfutable et confirmable. Par exemple, il suffirait de trouver une fonction ``clairement" calculable qui ne soit pas programmable pour la réfuter. Le fait que la thèse de Church entraîne le théorème de Gödel illustre qu'une thèse philosophique peut avoir des conséquences purement mathématiques (ce qui par ailleurs illustre encore son caractère réfutable et confirmable). Dans le présent travail l'hypothèse du computationnalisme joue un rôle analogue. Il s'agit d'une hypothèse à la fois philosophique et scientifique (en principe réfutable) qui permet de transformer le problème du corps et de l'esprit (réputé être un problème de philosophie) en un problème de pure mathématique (isoler une mesure unique satisfaisant à certaines contraintes sur l'ensemble des états computationnels).