Résumé technique : Sur le rôle de la connectivité dans les preuves de la logique linéaire

Énoncé du problème

L'article traite du problème fondamental des critères de correction en logique linéaire (LL). Bien que le passage des preuves de calcul des séquents de type arbre aux réseaux de preuves (structures de preuve) de type graphe constitue une contribution majeure à la théorie de la preuve, déterminer si une structure de preuve arbitraire représente une preuve logique valide demeure un défi complexe.

Dans le fragment purement multiplicatif sans unités ($MLL^-$), le critère de Danos-Regnier (souvent noté ACC) est une condition bien établie, nécessaire et suffisante : une structure de preuve est une preuve si et seulement si tous ses « graphes de commutation » sont acycliques et connectés. Cependant, en présence d'unités ($\mathbf{1}$ et $\bot$) et d'exponentielles (le fragment $MELL$), la situation est plus difficile. La propriété AC (acyclicité) est une condition nécessaire mais non suffisante pour la correction dans $MELL$ sans la règle de mix. La propriété ACC (acyclicité + connectivité) échoue dans $MELL en raison de la présence des règles d'affaiblissement et de la constante $\bot$, qui introduisent naturellement des composantes déconnectées.

La communauté sait depuis longtemps qu'une propriété nécessaire pour qu'une structure de preuve soit une preuve dans $MELL$ est $ACC^\sharp_w$ : chaque graphe de commutation doit être acyclique, et le nombre de composantes connexes doit être exactement égal au nombre de nœuds $\bot$ (affaiblissement) plus un. Cependant, cette propriété n'est pas suffisante pour le cas général (comme le démontrent les contre-exemples de la Figure 3a). L'article note qu'il est probablement impossible de trouver un critère de correction réalisable pour le fragment complet avec unités ($MLL$) en raison de la dureté NP de la prouvabilité dans le fragment multiplicatif de constantes uniquement.

La question centrale qui motive ce travail est : Quel est le sens logique de la connectivité ? Plus précisément, la propriété nécessaire $ACC^\sharp_w$ peut-elle devenir une propriété suffisante en identifiant des fragments géométriques ou syntaxiques spécifiques de la logique linéaire où elle est vérifiée ?

Méthodologie

Les auteurs emploient une approche géométrique de la théorie de la preuve, analysant les propriétés topologiques des structures de preuve (spécifiquement leurs graphes de commutation) sans dépendre fortement des contraintes de typage dans l'analyse initiale.

1. Cadre non typé : Les auteurs développent d'abord leurs résultats dans un cadre non typé. Ils définissent les structures de preuve comme des graphes orientés acycliques (DAG) avec des types de nœuds spécifiques (ax, cut, $\otimes$, $\parr$, $\bot$, $\mathbf{1}$, et $\bullet$). Cela leur permet d'isoler des conditions géométriques indépendantes des types de formules.
2. Graphes de commutation et connectivité : Ils utilisent le concept de graphes de commutation (induits par la sélection d'une prémisse pour chaque nœud $\parr$) pour définir des propriétés telles que l'acyclicité ($AC$) et le décompte des composantes ($C^\sharp_w$).
3. La condition $(\neg w \otimes)$ : L'innovation méthodologique centrale est l'introduction d'une condition géométrique locale appelée $(\neg w \otimes)$. Une structure de preuve satisfait cette condition si aucune prémisse d'un nœud $\otimes$ (tensor) ou cut n'est la conclusion d'un nœud d'« effacement » (un nœud $\bot$, $\parr$, ou $\bullet$ dont toutes les prémisses sont des conclusions de nœuds d'effacement).
   • Intuitivement, cela interdit aux nœuds d'« effacement » de nourrir directement les nœuds « multiplicatifs ».
4. Séquentialisation par induction : Les auteurs prouvent leurs principaux théorèmes par induction sur le nombre d'arcs de la structure de preuve. Ils démontrent que sous la condition $(\neg w \otimes)$, la propriété $ACC^\sharp_w$ garantit l'existence d'un nœud de « division » (un nœud cut ou $\otimes$ terminal) qui décompose de manière unique la structure, permettant une reconstruction récursive d'une preuve du calcul des séquents.
5. Sauts canoniques : Pour les fragments où la condition $(\neg w \otimes)$ ne se vérifie pas naturellement (ou pour affiner la séquentialisation), les auteurs introduisent une méthode consistant à ajouter des « sauts » (des arcs partant des nœuds $\bot$ vers d'autres nœuds) dans une position canonique. Cela permet de recouvrer la propriété ACC complète ou d'établir des relations d'équivalence entre les preuves.

Contributions et résultats clés

1. Le théorème principal pour les structures de preuve non typées

Le résultat principal de l'article est le Théorème 47 :

Soit $R$ une structure de preuve $(\neg w \otimes)$. Si $R$ satisfait $ACC^\sharp_w$ (graphes de commutation acycliques avec un nombre de composantes $= \# \bot + 1$), alors $R$ est séquentialisable (c'est-à-dire qu'elle correspond à une preuve valide du calcul des séquents).

Ce résultat établit que $ACC^\sharp_w$, auparavant connue comme une condition seulement nécessaire, devient un critère de correction suffisant pour la classe spécifique des structures de preuve $(\neg w \otimes)$.

2. Caractérisation du fragment $(\neg \bot \otimes)LL$

Les auteurs définissent un fragment typé de $MLL$ appelé $(\neg \bot \otimes)LL$ (Définition 50), où les formules sont restreintes de sorte que la conclusion d'un nœud d'effacement ne puisse pas être une prémisse d'un nœud $\otimes$.

• Corollaire 52 : Pour toute structure de preuve dans ce fragment, $R$ est séquentialisable si et seulement si $R \models ACC^\sharp_w$.
• Signification : Cela fournit un critère de correction réalisable pour un fragment de $MLL$ qui inclut des unités, surmontant les barrières de complexité du fragment complet.

3. Séquentialisation canonique et équivalence de preuves

Dans la section 4, les auteurs affinent le processus de séquentialisation pour $(\neg \bot \otimes)LL$.

• Ils définissent une position canonique pour les sauts (Définition 58), notée $\langle R \rangle^m_w$, qui assigne un nœud cible spécifique à chaque nœud $\bot$ en fonction de la structure de la preuve.
• Théorème 62 : Si une structure de preuve sans saut dans ce fragment satisfait $ACC^\sharp_w$, il existe une preuve du calcul des séquents qui correspond à la structure totale canonique avec sauts.
• Corollaire 66 : Cela conduit à une procédure de décision simplifiée pour l'équivalence de preuves (permutation des règles). Deux preuves dans $(\neg \bot \otimes)LL$ sont équivalentes si et seulement si leurs déséquentialisations (les structures de preuve sous-jacentes sans sauts) sont identiques. Cela contraste avec le $MLL$ complet, où ce problème est PSPACE-complet.

4. Extensions aux exponentielles et à la logique intuitionniste

• Extensions MELL (Section 5) : Les résultats sont étendus au fragment multiplicatif exponentiel ($MELL$). Le fragment $(\neg ? \otimes)LL$ (Définition 69) et le fragment polarisé ($LL_{pol}$) sont montrés comme satisfaisant les mêmes critères de correction. Cela recouvre les résultats connus pour les réseaux de preuves polarisés (Corollaire 72).
• Logique linéaire intuitionniste (Section 6) : Les auteurs étudient le fragment intuitionniste ($IMELL$). Ils prouvent que pour les structures de preuve sans cut dans le fragment intuitionniste de constantes uniquement ($ICOMLL$), la propriété $ACC^\sharp_w$ est équivalente au fait d'avoir exactement une conclusion de sortie (Proposition 77, Théorème 82). Cela fournit une caractérisation géométrique de l'exigence intuitionniste.

Signification et affirmations

L'article revendique une importance dans les domaines suivants :

1. Interprétation géométrique de la logique : Ce travail fait progresser la compréhension de la relation entre les propriétés géométriques (connectivité) et la validité logique. Il démontre que la connectivité n'est pas simplement une contrainte technique mais porte un sens logique spécifique concernant l'interaction entre les règles d'effacement (affaiblissement) et les règles multiplicatives.
2. Affinement des critères de correction : En isolant la condition $(\neg w \otimes)$, les auteurs montrent que la condition nécessaire « faible » $ACC^\sharp_w$ est en réalité suffisante pour une classe de preuves non triviale et intéressante. Cela comble le fossé entre le bien élevé $MLL^-$ et le complexe $MELL$.
3. Complexité et équivalence : L'article souligne que restreindre le langage logique pour satisfaire des conditions géométriques (comme $(\neg w \otimes)$) peut réduire drastiquement la complexité des problèmes de décision, tels que l'équivalence de preuves, les faisant passer de PSPACE-complet à décidable en temps polynomial (via une simple égalité structurelle).
4. Unification : L'approche unifie divers critères de correction existants (y compris ceux pour la logique polarisée et la logique intuitionniste) sous l'égide des propriétés de connectivité et du décompte des composantes, suggérant une perspective géométrique unifiée sur différents fragments de la logique linéaire.

Les auteurs déclarent explicitement que leur objectif est de « laisser la connectivité parler » et de comprendre ses implications logiques, plutôt que de proposer de nouvelles applications computationnelles ou des propositions expérimentales. Le travail est présenté comme une contribution théorique à la « théorie des réseaux de preuves », se concentrant sur les propriétés structurelles qui distinguent les preuves valides des graphes arbitraires.