Wider systems for linear logic with fixed points: proof theory and complexity

1. Problématique et Contexte

Les points fixes (inductifs et co-inductifs) sont fondamentaux en logique et en informatique pour formaliser la récursion et l'induction. Ces dernières années, l'intérêt pour les systèmes de preuve structurels traitant des points fixes dans le cadre de la logique linéaire (notamment $\mu$MALL) a considérablement augmenté.

Cependant, la plupart des travaux antérieurs se sont limités à des règles de branchement $\omega$-finies (suites dénombrables), ce qui correspond à des modèles continus où les opérateurs atteignent leurs points fixes en au plus $\omega$ étapes. L'article vise à combler un vide théorique en étudiant des systèmes plus généraux où le branchement est indexé par un ordinal arbitraire (calculable) $\alpha$. Ces systèmes, notés $\mu$MALL$_{\alpha,\alpha}$, permettent de modéliser des structures plus complexes (comme les arbres bien fondés arbitraires) et des modèles de calculs où la fermeture nécessite plus de $\omega$ étapes.

La question centrale est de déterminer la complexité algorithmique du problème de décidabilité (la prouvabilité) dans ces systèmes étendus. Plus précisément : à quel niveau de la hiérarchie hyperarithmétique se situe le problème de prouvabilité pour un ordinal calculable $\alpha$ ?

2. Méthodologie

Les auteurs adoptent une approche combinant la théorie de la preuve structurelle et la théorie de la complexité descriptive (hiérarchie hyperarithmétique).

A. Fondations de la théorie de la preuve

Pour contrôler l'analyse de la complexité, les auteurs établissent d'abord des propriétés fondamentales pour les systèmes $\mu$MALL$_{\alpha,\alpha}$ :

1. Élimination des coupures (Cut-elimination) : Ils prouvent que toute preuve peut être transformée en une preuve sans coupure. Cela repose sur une mesure de complexité des formules appelée rang ($rk$).
2. Focalisation (Focussing) : Ils développent un système de preuve focalisé ($\mu$MALL$^{Fcf}_{\alpha,\alpha}$). Ce système organise la recherche de preuves en phases synchrones (non-inversibles, choix actifs) et asynchrones (inversibles, choix passifs). Cette discipline réduit drastiquement l'espace de recherche des preuves, ce qui est crucial pour l'analyse de la complexité.

B. Définition du Rang des Formules

Une contribution méthodologique majeure est la définition d'un rang de formule précis, basé sur les opérations arithmétiques naturelles (somme naturelle $\oplus$ et produit naturel $\otimes$) sur les ordinaux, plutôt que sur des opérations usuelles ou des maxima simples.

• Le rang d'une formule est défini de manière à ce que chaque étape de preuve (de bas en haut) réduise strictement le rang du séquent.
• Cette définition permet de borner la hauteur de l'espace de recherche de preuves sans coupure par un ordinal spécifique, $\omega^{\alpha^\omega}$.

C. Analyse de Complexité

• Majoration (Upper Bound) : En utilisant l'élimination des coupures et la focalisation, les auteurs montrent que la prouvabilité peut être décrite comme un processus itératif sur un ensemble de formules positives, dont la profondeur est bornée par le rang maximal des formules. Cela permet de coder le problème de prouvabilité dans la hiérarchie hyperarithmétique.
• Minoration (Lower Bound) : Pour prouver la dureté (hardness), ils réduisent le problème de vérité des sentences infinitaires calculables (complet pour chaque niveau de la hiérarchie hyperarithmétique) à la prouvabilité dans $\mu$MALL$_{\alpha,\alpha}$. Cette réduction utilise l'encodage de machines de Minsky (pour simuler le calcul) et de formules infinitaires calculables au sein du système logique, en exploitant les propriétés de focalisation pour garantir l'adéquation.

3. Résultats Principaux

Le résultat central de l'article est le théorème suivant (Théorème 2.8) :

Théorème : Pour tout ordinal calculable $\alpha \ge \omega$, le problème de prouvabilité dans le système $\mu$MALL$_{\alpha,\alpha}$ est $\Sigma^0_{\omega^{\alpha^\omega}}$-complet (sous réductions de Turing).

Cela signifie que :

1. Le problème appartient à la classe $\Sigma^0_{\omega^{\alpha^\omega}}$ de la hiérarchie hyperarithmétique.
2. Il est aussi difficile que n'importe quel problème de cette classe (il est complet).

Cas particuliers notables :

• Pour $\alpha = \omega$, le système est $\Sigma^0_{\omega^\omega}$-complet.
• Pour tout $\alpha$ tel que $\omega \le \alpha < \omega^\omega$, le système reste $\Sigma^0_{\omega^\omega}$-complet (car $\deg(\alpha) < \omega$, donc $\omega^{\alpha^\omega} = \omega^\omega$). Cela implique que tous ces systèmes sont équivalents en termes de complexité de Turing.

4. Contributions Clés

1. Généralisation des systèmes de points fixes : Extension de la logique linéaire avec points fixes à des règles de branchement transfinies arbitraires (calculables), dépassant la limitation aux modèles continus ($\omega$-branching).
2. Nouvelle notion de rang : Introduction d'une mesure de rang basée sur l'arithmétique naturelle des ordinaux, permettant des bornes de hauteur de preuve plus serrées et précises que les approches précédentes (comme celles de [2, 12]).
3. Complétude de la théorie de la preuve : Établissement de l'élimination des coupures et du théorème de focalisation pour ces systèmes infinis, démontrant la robustesse de la fondation proof-théorique de $\mu$MALL$_{\alpha,\alpha}$.
4. Classification précise de la complexité : Cartographie exacte de la complexité de ces logiques dans la hiérarchie hyperarithmétique, reliant la structure des ordinaux de fermeture ($\alpha$) directement au niveau de complexité ($\omega^{\alpha^\omega}$).

5. Signification et Impact

Ce travail a plusieurs implications importantes :

• Théorie de la preuve : Il démontre que les outils de la théorie de la preuve structurelle (focalisation, élimination des coupures) sont suffisamment puissants pour gérer des systèmes infinis complexes avec des ordinaux de branchement arbitraires.
• Complexité computationnelle : Il établit un lien direct entre la "taille" des modèles de points fixes (mesurée par l'ordinal de fermeture) et la puissance de calcul requise pour vérifier la vérité dans ces systèmes. La complexité croît de manière exponentielle avec l'ordinal $\alpha$ (via l'itération de l'opérateur $\omega^\cdot$).
• Comparaison des logiques : L'article offre un cadre pour comparer différentes approches des points fixes (règles explicites, preuves cycliques, preuves non bien-fondées) en termes de puissance expressive et de complexité. Il montre que l'ajout de branches transfinies augmente significativement la puissance de la logique par rapport aux versions finies ou $\omega$-finies.

En résumé, cet article fournit une fondation rigoureuse et une classification de complexité complète pour une famille étendue de logiques linéaires avec points fixes, reliant profondément la théorie des ordinaux, la théorie de la preuve et la théorie de la complexité.