Réfutation de Lucas et Penrose

On peut, sans user de l'hypothèse du computationnalisme, utiliser les logiques G, G$*$, S4Grz, pour invalider de façon précise l'usage des phénomènes d'incomplétude visant à réfuter le mécanisme comme celle de Lucas que Penrose a remis récemment sur le tapis [Lucas, 1961, Lucas, 1968, Penrose, 1989]. La part correcte de ces tentatives de réfutation montre seulement que si nous sommes des machines alors nous ne pouvons pas savoir quelle machine nous sommes, ce qui rejoint les conclusions de [Benacerraf, 1967], mais aussi les conclusions naturelles du computationnalisme obtenues avec les expériences par la pensée. Regardons cela de plus près. Ce sera l'occasion de préciser rigoureusement la version arithmétique de l'idée de Théétète. En 1959, Lucas a tenté de réfuter le computationnalisme, sous la forme béhavioriste d'une sorte de test de Turing limité aux propositions de l'arithmétique informelle (voir Lucas 1961, voir aussi Penrose 1989, qui utilise cet argument et défend alors la possibilité d'une théorie quantique de la conscien$ce : notons que je propose exactement l'inverse, accepter le computationnalisme et dériver de l'incomplétude une phénoménologie quantique de la matière). L'argumentation de Lucas illustre à la fois la difficulté d'identifier le connaisseur sujet ``" avec la machine objet ``" et les difficultés conceptuelles qui se présentent lors des expériences par la pensée de multiplication de soi-même. Je pense avec Post (1922!), et Webb (1980) qui a consacré un ouvrage sur cet argument, que le raisonnement de Lucas est invalide. Je partage néanmoins avec Lucas et Penrose l'idée que le théorème de Gödel s'applique aux machines digitales. Cette dernière remarque est bien sûr une digression puisqu'avec notre stratégie pour isoler les phénoménologies nous nous sommes limités aux machines Löbiennes, qui sont a priori sujettes aux phénomènes d'incomplétudes. Je pense, à présent, comme Benacerraf (1967), qu'une bonne partie du raisonnement de Lucas peut être rendu valide : la conclusion antimécaniste doit être affaiblie. Ce n'est pas que je ne suis pas une machine, mais seulement que si je suis une machine, alors je ne peux pas me reconnaître, de façon prouvable ou communicable, dans cette machine; ce que nous avons déjà illustré avec le computationnalisme au moyen de l'expérience par la pensée de la duplication de soi. Je propose une reconstruction de cet argument, due en partie à [Benacerraf, 1967, Chihara, 1972, Reinhardt, 1985, Reinhardt, 1986], voir aussi [Wang, 1974]. Cette reconstruction de la réfutation de Lucas, est formellement similaire aux critiques du mécanisme basées sur les expériences par la pensée de l'autoduplication (si je suis duplicable, je ne peux pas me reconnaître dans le dupliqué). Lucas prend comme hypothèse qu'il est sain (A →A) et il décide de se comparer seulement aux machines saines (A →A). Lucas commet une identification entre machine et système formel (ce qui, on l'a vu, est une conséquence plausible du computationnalisme, au niveau adéquat avec la thèse de Church, mais nous n'avons pas besoin de cette identification: il est évident que si ``je" suis une machine saine alors ``je" suis une machine Löbienne). La communicabilité de la machine Löbienne est arithmétisable et diagonalisable, c'est-à-dire qu'il existe un énoncé arithmétique p tel que p ↔ p. La machine saine lui étant présentée, Lucas peut trouver cet énoncé p, et démontrer p ↔p. L'argumentation de Lucas, ou plutôt sa reconstruction, peut alors être résumée dans la dérivation suivante : �$

$1)\; (p$ \leftrightarrow $p)$ machine\; löbienne;$2)\; (p$ \to $p)$ calcul\; propositionnel;$3)\; p$ \to $p$ la\; machine\; est\; saine\; ...$$ (par\; hypothèse!)$4)\; (p$ \to $p)$ ...\; sait\; Lucas;$5)\; (p$ \to $(p$ \wedge $p))$ calc.\; prop.\; +\; 2)\; et\; 4)$6)\; (p$ \to $)$ calcul\; propositionnel;$7)\; p$ calcul\; propositionnel;$8)\; p$ par\; 7)\; et\; 1)$9)\; p$ par\; 7)\; etp$ \to $p$$

et donc l'ensemble des propositions arithmétiques $p$ que je (Lucas) peux savoir, c'est-à-dire telles que $p$, est différent de l'ensemble des propositions arithmétiques $p$ que la machine peut savoir (= démontrer, selon Lucas), c'est-à-dire telles que $p$. Lucas semble être à même de se distinguer de toutes les machines (saines) sur un test de Turing limité à l'arithmétique. Où est l'er$reur\; ?En\; faveur\; de\; Lucas,\; une\; chose\; est\; claire\; :\; si$ $obéit\; à\; S4,\; il\; n\text{'}est\; pas\; arithmétiquement\; définissable\; (il\; n\text{'}est\; pas\; finitairement\; définissable\; par\; lui-même).\; En\; effet,\; dans\; ce\; cas,\; il\; serait\; diagonalisable\; et\; il\; existerait\; un\; énoncé$ p$tel\; que$ p\; \leftrightarrow p$,\; donc$ p\; \to \; p$,\; or$ p\; \to p$(par\; la\; réflexion\; T),\; donc$ p$,\; donc$ p$(puisque$ p\; \leftrightarrow \; p$),\; donc$ p$(par\; nécessitation),\; donc$ $,\; puisqu\text{'}on\; a\; à\; la\; fois$ p$et$ p$.\; Remarquons\; la\; similarité\; de\; cette\; preuve\; avec\; la\; réfutation\; de\; Lucas.\; Un\; raisonnement\; similaire\; montre\; directement\; que\; G$ *$ne\; peut\; pas\; être\; fermé\; pour\; la\; nécessitation,\; puisqu\text{'}il\; a\; la\; réflexion.\; On\; voit\; en\; fait\; qu\text{'}aucune\; forme\; de\; communicabilité\; ne\; peut\; être\; à\; la\; fois\; diagonalisable,\; obéir\; à\; l\text{'}axiome\; de\; réflexion\; et\; être\; fermée\; pour\; la\; nécessitation.\; En\; passant,\; on\; obtient\; une\; démonstration\; du\; théorème\; de\; Tarski\; comme\; quoi\; la\; vérité\; arithmétique\; n\text{'}est\; pas\; arithmétiquement\; définissable.\; En\; effet\; si\; tel\; était\; le\; cas,\; on\; disposerait\; d\text{'}un\; prédicat\; ``Vrai"\; de\; vérité,\; et\; l\text{'}idée\; de\; Théétète\; pourrait\; produire\; une\; connaissance\; ``$ p$"\; qui\; serait\; intensionnellement\; équivalente\; à$ Bew(p\; )\; \wedge Vrai(p\; )$,\; qui\; obéirait\; à\; la\; réflexion,\; serait\; fermé\; pour\; la\; nécessitation\; et\; serait\; en\; même\; temps\; diagonalisable.\; Pour\; trouver\; de\; façon\; précise\; l\text{'}erreur\; de\; Lucas\; dans\; notre\; contexte,\; c\text{'}est-à-dire\; avec\; le\; computationnalisme,\; il\; reste\; à\; appliquer\; l\text{'}idée\; de\; Théétète\; à\; la\; logique\; G.\; En\; réalité\; ceci\; n\text{'}est\; pas\; nécessaire,\; on\; peut\; se\; contenter\; de\; travailler\; dans\; une\; arithmétique\; étendue\; avec\; S4\; (comme\; l\text{'}arithmétique\; épistémique\; de\; [Reinhardt,\; 1985,Reinhardt,\; 1986],\; ou\; de\; [Shapiro,\; 1985]).\; S4\; désigne\; le\; système\; suivant\; :$

$$ AXIOMES\; \hspace{0.17em}:$(\; A$ \to $B)$ \to $(A$ \to $B)$ K$A$ \to $A$ T$A$ \to $A4$ RÈGLES\; \hspace{0.17em}:$$ \{\; A\; ,\; \hspace{0.17em}\; A$ \to $BB\; \}$$ MP$$ \{\; AA\; \}$$ NEC$$

Dans ce cas, cependant, la relation entre la prouvabilité dans la théorie et la prouvabilité informelle n'est pas claire. L'avantage de l'idée de Théétète appliquée à une machine auto-référentiellement correcte est de garantir au départ l'égalité extensionnelle de la prouvabilité formelle et de la prouvabilité intuitive. L'idée de Théétète est capturée de façon précise par la transformation modale BGKM (pour Boolos 1980, Goldblatt 1978, Kusnetzov et Muravitsky 1977) de l'ensemble des formules modales dans l'ensemble des formules modales : MPL $\to$ MPL : Les variables propositionnelles sont supposées avoir été ordonnées $p$_i.

$$ BGKM(p$$_i) = p_i, $BGKM(A$ \vee $B)\; =$ BGKM(A)$ \vee $$ BGKM(B),$$$ $BGKM(A$ \wedge $B)\; =$ BGKM(A)$ \wedge $$ BGKM(B),$$$ $BGKM(A)\; =$ BGKM(A),$$ $BGKM(A)\; =\; ($ BGKM(A))$ \wedge $$ BGKM(A).$$$

On peut alors démontrer:

où S4Grz est naturellement le système S4 $+$ Grz:

$$ AXIOMES\; \hspace{0.17em}:$(\; A$ \to $B)$ \to $(A$ \to $B)$ K$A$ \to $A$ T$A$ \to $A4((\; A$ \to $A)$ \to $A)$ \to $A$ Grz$$ RÈGLES\; \hspace{0.17em}:$$ \{\; A\; ,\; \hspace{0.17em}\; A$ \to $BB\; \}$$ MP$$ \{\; AA\; \}$$ NEC$$

On regarde alors le raisonnement de Lucas au niveau de la vérité G$*$, et on constate que l'erreur se situe dans le passage de la ligne 3) à la ligne 4) puisque $G*\; 3)$, mais $G*\; 4)$. En composant BGKM avec l'interprétation arithmétique (dans le langage de la machine löbienne) de G, on obtient une interprétation arithmétique de $$ , c'est-à-dire, on obtient les transformations (paramétrées par $F$)Ê: $MB$_F o BGKM : LPM $\to$ L(M), et

Ainsi $p$ est interprété par Bew$(p\; )\; \wedge p$. La théorie S4Grz, constitue ainsi une axiomatisation naturelle de la connaissabilité (intuitive et non diagonalisable) de la machine. Le bord flou du sujet --y compris l'incapacité qu'il a de se reconnaître objectivement-- est capturé par le fait que $$ n'est pas effectivement définissable par la machine, ni arithmétisable, ni diagonalisable. Comme il fallait s'y attendre, l'idée de Théétète empêche le sujet de se définir effectivement lui-même. De même, le sujet machine peut se dupliquer, mais il ne peut pas effectivement (de façon effective, constructive, communicable, ou connaissable) se reconnaître dans le dupliqué. On rejoint d'une certaine façon l'idée de Brouwer (le fondateur de la philosophie intuitioniste, cf [van Stigt, 1990]) selon laquelle le sujet (et son oeuvre) n'est pas (prouvablement) axiomatisable. La formule de Grzegorczyk entraîne l'antisymétrie de la relation d'accessibilité pour les modèles finis. Cela suggère une interprétation temporelle (au sens subjectif) du développement local de la connaissance du sujet, ce qui permet une interprétation arithmétique du temps subjectif à-la-Bergson 1939 (voir aussi Dogen 1232-1253), ce qui encore est proche de la philosophie de la conscience et du développement temporel du soi de Brouwer (voir [Brouwer, 1905, Brouwer, 1983], voir aussi [Grzegorczyk, 1964]). Et de fait, une logique intuitioniste représentable arithmétiquement, IL, émerge à ce stade. En effet, Gödel (1933) a suggéré et McKinsey Tarski (1948) ont démontré qu'on peut interpréter la logique intuitioniste dans le système modal S4. Grzegorczyk a étendu le résultat pour S4Grz. Voilà la transformation de 1933 de Gödel. Attention il s'agit d'une transformation du langage propositionnel (non modal) dans le langage propositionnel modal LPM:

$$ G33(p$$_i) = p_i $G33(A$ \wedge $B)\; =$ G33(A)$ \wedge $$ G33(B)$$$ $G33(A$ \vee $B)\; =$ G33(A)$ \vee $$ G33(B)$$$ $G33(A$ \to $B)\; =$ G33(A)$ \to $$ G33(B)$$$ $G33(A)\; =$ G33(A)$$

% futur KG On a, avec IL pour Logique Intuitioniste (Grzegorczyk 1967)Ê:

Il suffit de composer les différentes transformations pour extraire l'interprétation arithmétique de l'intuitionismeÊ (Goldblatt 1978, voir aussi Artemov 1990):

J'argumente, avec le computationnalisme, en faveur de l'idée qu'il s'agit de la part solipsiste du sujet. Un résultat formel, qui confirme ce point de vue, est que le passage à G$*$ ne rajoute aucune formule : ni pour S4Grz (Boolos 1980a, 1980b), ni pour IL (Goldblatt 1978). Les propositions absolument indécidables mais vraies, c'est-à-dire telles que G$*\; p\; \wedge p$, ne sont pas des images de propositions intuitionistes par la transformation BGKM. Avec des notations évidentes, Boolos et Goldblatt ont démontré que S4Grz = S4Grz* et IL = IL* : le solipsiste identifie correctement (de son point de vue) la prouvabilité et la vérité. Notons qu'Artemov justifie (proprement) que l'idée de Théétète, précisément l'idée de définir la prouvabilité intuitive $$ par la prouvabilité formelle accompagnée de la vérité, $p\; \wedge p$, peut être érigée en une thèse de philosophie des mathématiques (comme l'est la thèse classique de Church, voir Artemov 1990, Marchal 1995). Conclusion. Lucas a essayé de tirer une contradiction de l'ensemble des propositions $\{p\; \to p,\; p\; \to p,\; p\; \leftrightarrow p\}$, où $p$ est une proposition arithmétique, $$ représente la prouvabilité par une machine auto-référentiellement correcte et $$ représente la prouvabilité intuitive de l'incorrigible Lucas. La part correcte du raisonnement de Lucas montre seulement le caractère contradictoire de l'ensemble $\{p\; \to p,\; p\; \to p,\; (p\; \leftrightarrow p)\}$. On a bien G$*\; p\; \to p,G*\; p\; \to p,G*\; (p\; \leftrightarrow p)$, mais G$*\; (p\; \leftrightarrow p)$. On retrouve bien la solution de Benacerraf. Je mentionne le fait que Penrose commet clairement cette erreur dans ``The Emperor's New Mind" [Penrose, 1989], mais ne la commet plus dans ``The Shadow of the Mind". Il ne semble toutefois pas tenir compte de cette correction [Penrose, 1994]. Penrose semble persuadé que la proposition ``je suis une machine" n'a de sens intéressant que si elle entraîne la proposition ``je sais quelle machine je suis". Mais, avec les expériences par la pensée, j'ai démontré que si le computationnalisme est correct, alors je ne peux jamais démontrer (ni savoir, avec l'idée de Théétète) quelle machine je suis. Et encore avec l'idée de Théétète, on vient de démontrer que cette impossibilité est l'apanage de toutes les machines löbiennes. Et on voit ici que les machines löbiennes elles-mêmes peuvent démontrer que si elles sont consistantes, alors, elles ne peuvent pas démontrer qu'elles sont telles ou telles autres machines. Notons que la question de savoir si une machine (löbienne) peut démontrer qu'elle est une machine non spécifiée est ouverte. Une telle question peut être formalisée dans l'extension du premier ordre de G$*$ (qui n'est pas complètement axiomatisable), et sort du cadre de ce travail (voir [Marchal, 1995, Reinhardt, 1985, Reinhardt, 1986]). Pour paraphraser Post 1922, l'argument ``Gödélien" ne peut pas montrer que l'homme n'est pas une machine. Post ajoute que l'argument montre seulement que l'homme ne peut pas construire une machine prouvant les mêmes théorèmes (de l'arithmétique) que lui. Ceci est encore trop dire puisqu'avec le second théorème de récursion de Kleene [Kleene, 1952], on peut rendre une machine quelconque (extensionnellement parlant) autoreproductible.ÊCe que je montre (avec le mécanisme) c'est qu'un sujet ne peut pas à la fois construire une machine capable de prouver les mêmes théorèmes (de l'arithmétique) que lui et en même temps prouver qu'il en est bien ainsi, c'est-à-dire prouver que cette machine est capable de prouver les mêmes théorèmes que lui. En interprétant $$ par ``je sais" et $$ par ``il croit", où ``il" joue le rôle d'une duplication de ``moi" (le rôle du doppelgänger), les situations paradoxales des expériences par la pensée sont suffisamment clarifiées pour confirmer (cela ne veut pas dire prouver) la thèse digitale et empêcher qu'on ne prenne des expériences par la pensée reposant sur la duplication, pour des réfutations du mécanisme. En résumé, les erreurs dans l'usage du théorème de Gödel, ou des paradoxes de la duplication, pour réfuter le mécanisme reviennent en général (et à une reconstruction logique de l'argument près) à un usage simultané de T, Nec et de la diagonalisation (ou de la représentabilité arithmétique). Le tableau suivant récapitule la situation et peut servir de garde-fou contre ce genre de confusion intensionnelle en philosophie (mécaniste) de l'esprit:

G G$*$ S4Grz

T $-$ $+$ $+$

Nec $+$ $-$ $+$

Diag $+$ $+$ $-$

D'autres applications de ces logiques à la philosophie de l'esprit (aux rêves, aux réalités artificielles, aux malins génies et au cogito de Descartes, à la conscience-durée selon Brouwer-Bergson, etc.) sont proposées dans le rapport technique Marchal 1995. On peut consulter aussi [Slezak, 1983] pour une analyse assez semblable du cogito cartésien. Cette dernière résulte aussi d'une réfutation approfondie de Lucas [Slezak, 1982]. Notons encore que cette phénoménologie de la connaissance fournit une solution au problème du connaisseur (the Knower Paradox, [Kaplan and Montague, 1961], voir aussi [Grim, 1991]).