Nous nous intéressons ici à un texte de Schopenhauer intitulé “Dialectica eristica”, traduit en français par l’art d’avoir toujours raison [1], texte souvent qualifié de mineur ou de digression philosophique. Nous proposons alors une digression de la digression. Il ne s’agit pas de développer un propos philosophique ni une étude des jeux logiques à la mode médiévale. En fait, ce texte nous interpelle car il fait écho à l’actualité de la logique contemporaine. Dans ce texte Schopenhauer se propose de définir la dialectique comme l’art de gagner les controverses indépendamment de la recherche de la vérité ; or c’est en “libérant” les preuves formelles de la stricte recherche de la vérité que J.-Y. Girard a proposé une nouvelle théorie logique : la Ludique [Girard-01]. Dans ce texte fondateur, son auteur qualifie cette théorie d’approche purement interactive de la Logique ; nous sommes alors curieux de faire résonner cette approche radicalement nouvelle en logique mathématique dans d’autres champs concernés de près ou de loin par la logique : la dialectique ici, la pragmatique plus généralement.
Parmi les caractéristiques originales et prometteuses de la Ludique on trouve l’abolition d’une dualité qui résistait jusqu’alors en logique : la dualité syntaxe/sémantique. Le dépassement de cette dualité est l’aboutissement d’un changement de point de vue : la Ludique privilégie le point de vue internaliste ; la connaissance d’un objet ne se fait pas via le passage dans un autre monde [2], mais via le résultat de ses interactions avec des objets de même nature. Ainsi que le décrit C. Faggian [Faggian-02b], ce dépassement est réalisé dans le monde des preuves formelles par un double processus : l’abstraction de la syntaxe ; la concrétisation de la sémantique. D’une part on manipule des objets plus généraux que des preuves formelles, en particulier on donne un statut à des preuves qui se terminent par un échec...
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...