L'idée de Théétète

La justifiabilité formelle, qu'elle soit justifiable (axiomatisée par G) ou incommunicable (axiomatisée par G$*$), ne distingue pas la première et la troisième personne. Elle ne distingue pas ``moi" de mon doppelgänger. De plus ni G, ni G* ne prouvent simultanément la réflexion $A\; \to A$ et la nécessitation $\{AA\}$. Cela exclut l'usage directe de la justifiabilité formelle pour capturer la connaissabilité de la machine. Une des plus vieilles idées de la philosophie, qui est énoncée notamment par Platon (voir le Ménon, et surtout le Théétète, voir [Platon, 1950], voir aussi [Burnyeat, 1991]) est de définir la connaissance par la justification vraie, de définir la connaissance de $A$ par la justification de $A$ accompagné --par définition-- de la vérité de $A$. Cela revient à définir un nouveau connecteur modal correspondant à

En vertu du théorème de Tarski, il n'est pas possible d'interpréter arithmétiquement cette modalité par une formule du genre

puisqu'il n'existe pas de prédicat arithmétisable ``Vrai" représentant la vérité arithmétique. Et de fait, cette forme de connaissance n'est pas arithmétisable. Si on admet que cette connaissance décrit bien une connaissance de la première personne, cela garantit que la première personne ne pourra se reconnaître en aucune présentation à la troisième personne d'elle-même. Ce qui est effectivement le cas avec le computationnalisme. La machine peut cependant communiquer (à la troisième personne) des propositions sur cette connaissabilité. Il est évident qu'à présent, la formule de réflexion $A\; \to A$ est un schéma de formules communicables, puisque la machine prouve triviale$ment\; :$

On obtient ainsi une logique à la troisième personne du discours de la première personne. La première personne, sous la forme d'une logique intuitioniste IL, peut être retrouvée en inversant une transformation proposée indépendamment par Kolmogorov en 1932 et par Gödel en 1933 pour interpréter modalement la logique intuitioniste [Kolmogorov, 1932, Gödel, 1933]. Une preuve précise de l'idée de Gödel apparaît chez McKinsey et Tarski [McKinsey and Tarski, 1948]. Grâce au travail de Grzegorczyk de 1967, de façon indépendante Kuznetsov Muravitsky 1977, Goldblatt 1978, et Boolos 1980 ont pu démontrer que la logique S4Grz, disposant de la formule de Kripke, et des règles du modus ponens et nécessitation, ainsi que de la curieuse formule de Grzegorczyk $1967\; :$

$((A\; \to A)\; \to A)\; \to A$

axiomatise complètement la prouvabilité sur la connaissabilité [Grzegorczyk, 1967, Kuznetsov and Muravitsky, 1977, Goldblatt, 1978, Boolos, 1980c, Boolos, 1980a, Boolos, 1980b]. De même Goldblatt a pu démontrer la complétude de la logique IL pour son interprétation arithmétique (Goldblatt 1978). Boolos et Goldblatt ont démontré que notre ``sujet", qu'il soit décrit à la troisième personne (S4Grz) ou par son discours à la première personne (IL) ne distingue pas la connaissabilité de la vérité. En effet, les ``starifications" de ces logiques n'apportent pas de propositions nouvelles: S4Grz = S4Grz$*$, IL = IL$*$. Du point de vue du sujet, il n'y a pas de vérités qui ne soient pas connaissables (voir plus loin pour les références). G$*$ permet de démontrer que la première et troisième personne sont extensionnellement identiques (démontre les mêmes propositions de l'arithmétique). Il s'agit bien de la même personne vue selon des points de vue différents.