Réseau de preuves

Les réseaux de preuves, inventés par le logicien Jean-Yves Girard en 1986 dans le cadre de la logique linéaire, sont un outil de démonstration formel pour cette même logique (c'est-à-dire une alternative aux séquents qui sont aussi employés en logique classique et intuitionniste). Grossièrement, il s'agit d'un équivalent de la déduction naturelle de la logique intuitionniste adaptée à la logique linéaire. Ils s'en différencient cependant par le caractère géométrique de cette approche : une preuve est formée par un hypergraphe et le critère de correction peut s'exprimer comme un parcours de graphe.

Définition

Définition inductive des réseaux de preuves pour MLL

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 ⊗ et ⅋.

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

• Le lien axiome n'a aucune prémisse et a deux conclusions A et A^⊥ ;
• Le lien coupure a deux prémisses A et A^⊥ et aucune conclusion ;
• Le lien fois a deux prémisses A et B et une conclusion A ⊗ B ;
• Le lien par a deux prémisses A et B et une conclusion A ⅋ 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 A₁, ..., A_n ⊢ B₁, ..., B_m est prouvable en logique linéaire multiplicative si et seulement s'il existe un réseau correct dont les hypothèses sont A₁, ..., A_n et les conclusions sont B₁, ..., B_m.

Réseaux à boîtes

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 ! (bien sûr) et ? (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 boîte de conclusion A₁, ..., A_n est équivalent à un ensemble d'énoncé A₁, ..., 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 A₁, ..., A_n, B dans une boîte de conclusion A₁, ..., A_n, !B ;
• L'introduction de pourquoi pas se fait en plaçant un lien ayant pour prémisses n occurrences de A et pour conclusion ?A.

On remarque que :

1. Dans les deux cas, 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 A devient une conclusion A^⊥) ;
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 n ≥ 1.

Les quantificateurs

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é A et pour conclusion ∀x A où x est une variable fraiche ou eigenvariable ;
• Le lien il existe a pour prémisse un énoncé A[t/x] et pour conclusion ∃x A. La notation A[t/x] dénote alors la substitution de la variable x par le terme t dans l'énoncé A.

Les additifs

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.

Critères de correction

Un critère de correction est un critère permettant de caractériser les réseaux correspondant à des preuves dans le calcul des séquents. En effet, alors que les séquents ont une correction locale (suivi des règles du calcul considéré) et une élimination des coupures globales, les réseaux de preuves ont une correction globale et une élimination des coupures locales.

Critère original

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.

Critère de Danos-Regnier

On introduit la notion d'interrupteur : un interrupteur 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 n liens par, il y a alors 2ⁿ interrupteurs.

Le critère s’énonce alors ainsi : Un réseau de preuve est correct si et seulement s'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.

Critère pour les réseaux avec boites

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.