Debate

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...