CERPEC, UMR 7304, CNRS
Université de Provence
pierre.livet [chez] univ-provence.fr
Au lieu de fonder la preuve sur l’application d’une multitude de règles d’inférences pour remonter de la proposition qu’on veut prouver vers les axiomes (on remonte en utilisant les règles d’élimination des connecteurs et les règles structurelles) Girard a proposé de la fonder sur une interaction entre les développements qui partent de la proposition qu’on veut prouver et ceux qui partent de sa contre-proposition. Celle-ci résulte de celle-là par l’échange entre les parties gauche et droite de la relation de conséquence. Pour simplifier, quand la proposition dit |-A, la contre-proposition dit A|-. La contre-proposition implique donc d’avoir fait passer A à droite ce qui, on l’a vu, revient à attacher à A une négation, nous assurant bien ainsi qu’il s’agit d’une contre-proposition. Le principe de la ludique consiste alors à poursuivre en parallèle les développements de la proposition et de la contre-proposition. Ces développements donnent des arbres (partant d’une formule complexe comme racine d’un arbre, on obtient les formules qui résultent de sa décomposition - des ensembles de formules plus simples - comme des branches qui elles-mêmes se ramifient. On s’intéresse alors aux symétries entre les deux arbres de développements (symétries toujours par rapport à la relation de conséquence), et plus spécifiquement aux symétries d’une formule qui apparaît dans la branche d’un arbre à une formule qui apparaît dans une branche de l’autre. Ces formules sont dites « convergentes », quand ce qui est à la droite de la relation de conséquence dans l’une est à gauche de cette relation dans l’autre. Entre ces formules symétriques par rapport à la relation de conséquence, il y a une interaction, ce qui permet d’utiliser une notion de « coupure », qui en fait connecte deux expressions symétriques, et on peut alors éliminer les formules simples qui sont connectées.
Ce développement se poursuit en parallèle entre les deux arbres, mais...
Qu’est ce qui assure notre identité personnelle ? Les philosophes ont proposé des réponses toutes imparfaites, mais qu’il est intéressant de tenter d’ordonner. Nous pourrions sans doute traiter d’emblée l’identité personnelle comme un système d’isomorphismes, mais nous pouvons aussi tenter d’utiliser le travail en profondeur de Jean Yves Girard d’une manière plus diversifiée. La notion d’identité personnelle se révèle bien adaptée à ce genre de tentative, que nous allons maintenant développer.
Revenons sur la division des niveaux de profondeur logique que propose Girard : le niveau aléthique, (-1) qui s’intéresse seulement à ce qui est prouvable, cohérent et vrai ; le niveau fonctionnel (-2) qui traite de preuves, et peut différencier deux démonstrations d’un même énoncé, tout en disposant de critères d’équivalence entre deux preuves (isomorphisme de Curry-Howard) ; le niveau interactif (-3) qui fait jouer la dynamique de stratégies en interaction dans un jeu qui doit se terminer ; le niveau déontique (-4) qui élimine tout arbitre du jeu précédent et fait jouer des propositions qui se jugent les unes les autres, la simple poursuite du jeu faisant émerger la règle de l’interaction entre A et non A. A ce niveau, on tient compte des « localisations » des formules : chaque formule a un « lieu » disjoint de celui des autres et qui lui reste propre au cours de toutes les manipulations logiques. En particulier, à ce niveau, on peut écrire A et B= B et A, puisque le signe « = » nous informe que le A qui est à gauche de B a bien le même lieu propre que le A qui est à droite du B (même chose pour B). Mais l’identité A=A de fait pas sens, parce qu’elle ne nous donne aucune information, sauf à la lire comme une sorte d’isomorphisme entre deux copies de A : A’ et A’’, chacune de lieu propre [1] différent. Pour les identifier, il faudrait...