Réseau de preuves

Les réseaux de preuves peuvent être définis pour différents fragments de la logique linéaire, on se restreint dans un premier temps au fragment multiplicatif (MLL) c'est-à-dire uniquement avec les symboles ${\displaystyle \otimes }$ et ${\displaystyle \wp }$.

On définit les réseaux de preuves par induction :

• Le lien axiome n'a aucune prémisse et a deux conclusions ${\displaystyle A}$ et ${\displaystyle A^{\bot }}$
• Le lien coupure a deux prémisses ${\displaystyle A}$ et ${\displaystyle A^{\bot }}$ et aucune conclusion
• Le lien fois a deux prémisses ${\displaystyle A}$ et ${\displaystyle B}$ et une conclusion ${\displaystyle A\otimes B}$
• Le lien par a deux prémisses ${\displaystyle A}$ et ${\displaystyle B}$ et une conclusion ${\displaystyle A\wp B}$

On obtient bien un hypergraphe, où les liens sont orientés de ses prémisses vers ses conclusions. On remarque :

• tout énoncé est prémisse d'au plus un lien
• tout énoncé est conclusion d'au plus un lien

On appelle alors :

• hypothèse du réseau un énoncé qui n'est conclusion d'aucun lien
• et conclusion du réseau un énoncé qui n'est prémisse d'aucun lien

Le critère de correction énonce alors que le séquent ${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{m}}$ est prouvable en logique linéaire multiplicative si et seulement si il existe un réseau correct dont les hypothèses sont ${\displaystyle A_{1},\ldots ,A_{n}}$ et les conclusions sont ${\displaystyle B_{1},\ldots ,B_{m}}$.

La logique linéaire restreinte au fragment multiplicatif est relativement peu expressive. Une extension des réseaux de preuves à MELL, c'est-à-dire aux exponentielles ${\displaystyle$ !} (bien sûr) et ${\displaystyle$ ?} (pourquoi pas), est possible mais nécessite l'ajout de la notion de boîte. Une boîte est la généralisation d'un lien axiome : vu de l'extérieur, une de boîte conclusion ${\displaystyle A_{1},\ldots ,A_{n}}$ est équivalent à un ensemble d'énoncé ${\displaystyle A_{1},\ldots ,A_{n}}$ qui serait deux à deux conséquence d'un lien axiome. À l'intérieur de la boîte on place un séquent quelconque qui a été prouvé de manière externe. On peut donc voir les boîtes comme un moyen d'intégrer aux réseaux de preuves des éléments provenant de l'extérieur, c'est-à-dire du calcul des séquents.

Pour intégrer les exponentielles à notre calcul, on se place dans le cadre du calcul mixte, c'est-à-dire que l'on se donne la possibilité de souligner n'importe quelle conclusion de lien, dénotant ainsi une gestion classique et non plus linaire de l'énoncé :

• L'introduction de bien sûr se fait en plaçant un réseau de conclusion ${\displaystyle A_{1},\ldots ,A_{n},B}$ dans une boîte de conclusion ${\displaystyle {\underline {A_{1}}},\ldots ,{\underline {A_{n}}},!B}$
• L'introduction de pourquoi pas se fait en plaçant un lien ayant pour prémisses ${\displaystyle n}$ occurrences de ${\displaystyle {\underline {A}}}$ et pour conclusion ${\displaystyle ?A}$

On remarque que :

1. Dans les deux cas, ${\displaystyle n}$ est éventuellement nul.
2. Dans le cas du bien sûr on peut supposer que le réseau n'a que des conclusions et pas de prémisses quitte à rajouter des liens axiomes (un prémisse ${\displaystyle A}$ devient une conclusion ${\displaystyle A^{\bot }}$)
3. Le lien pourquoi pas correspond à l'affaiblissement dans le cas 0-aire, à la déréliction dans le cas unaire et à la contraction dans le cas n-aire pour ${\displaystyle n\geq 1}$

L'ajout de quantificateurs au premier ordre est assez immédiat, on ajoute deux liens :

• Le lien pour tout a pour prémisse un énoncé ${\displaystyle A}$ et pour conclusion ${\displaystyle \forall xA}$ où ${\displaystyle x}$ est une variable fraiche ou eigenvariable
• Le lien il existe a pour prémisse un énoncé ${\displaystyle A[t/x]}$ et pour conclusion ${\displaystyle \exists xA}$. La notation ${\displaystyle A[t/x]}$ dénote alors la substitution de la variable ${\displaystyle x}$ par le terme ${\displaystyle t}$ dans l'énoncé ${\displaystyle A}$.

L'ajout des additifs aux réseaux de preuves constitue une tâche difficile si l'on tente de le faire en l'absence de boîtes. Les divers critères de correction proposés pour les réseaux additifs sans boîtes ne font pas l'unanimité chez les spécialistes du domaine.

Le critère original dû à Jean-Yves Girard s'exprime en termes de voyage dans un réseau : on simule le trajet d'une particule le long des hyperarêtes du réseau.

On introduit la notion d'interrupteur : un interrupteur ${\displaystyle I}$ sur un réseau de preuve est un choix d'orientation de chaque lien par de ce réseau, c'est-à-dire on considère que chaque lien par n'est relié qu'à une seule de ses deux prémisses. Si un réseau contient ${\displaystyle n}$ liens par, il y a alors ${\displaystyle 2^{n}}$ interrupteurs.

Le critère s’énonce alors ainsi : Un réseau de preuve est correct si et seulement si il est connexe et acyclique pour tout choix d'interrupteur, c'est-à-dire si et seulement si pour tout choix d'interrupteur le graphe obtenu est un arbre.

Le critère précédent s'étend facilement au cas des boîtes : Un réseau à boîte est correct si les réseaux contenus dans chaque boîte sont corrects et si le réseau obtenu en remplaçant chaque boîte par une hyperarrête l'est aussi (au sens précédent).

Le traitement des exponentielles se fait alors de la manière suivante :

• L'introduction de bien sûr se fait avec la méthode ci-dessus.
• Le lien pourquoi pas peut être considéré comme une généralisation d'un lien par : on généralise la notion d'interrupteur en demandant à faire un choix d'une prémisse pour chaque lien pourquoi pas.