Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations

Résumé Technique : Unification des systèmes de séquents pour la logique de la prouvabilité de Gödel-Löb

Énoncé du Problème
L'article traite d'une lacune importante dans la théorie de la preuve de la logique de la prouvabilité de Gödel-Löb (GL). Bien que GL possède une grande variété de formalismes de type séquents sans coupure, les relations entre eux n'étaient pas pleinement établies. Plus précisément, des travaux antérieurs avaient établi des correspondances de preuve théorique entre :

1. Systèmes structurels : le système de séquents étiquetés de Negri ($G3KGL$) et le système d'hyper-séquents arborescents de Poggiolesi ($CSGL^*$), via Goré et Ramanayake.
2. Généralisations de la structure de preuve : le système de Gentzen de Sambin et Valentini ($GL_{seq}$), le système non bien fondé de Shamkanov ($GL_\infty$), et le système cyclique de Shamkanov ($GL_{circ}$), via Shamkanov.

Cependant, l'inter-translatabilité des preuves entre les systèmes structurels ($G3KGL$, $CSGL^*$) et les généralisations de la structure de preuve ($GL_{seq}$, $GL_\infty$, $GL_{circ}$) demeurait un problème ouvert. La difficulté inhérente réside dans la transformation de preuves utilisant des séquents structurels complexes (graphes ou arbres de séquents de Gentzen) en preuves utilisant des séquents de Gentzen standards, un processus qui nécessite de se "défaire" de ces données structurelles supplémentaires.

Méthodologie
L'auteur, Tim S. Lyon, résout ce problème ouvert en construisant une chaîne de transformations syntaxiques de preuves qui comble le fossé entre ces formalismes distincts. La méthodologie se déroule en trois phases principales :

1. Restructuration vers la forme end-active : L'article démontre d'abord comment restructurer les preuves dans le système d'hyper-séquents arborescents $CSGL^*$ en une forme « end-active ». Dans une preuve end-active, les formules principales et auxiliaires des règles d'inférence se trouvent uniquement aux (pré-)feuilles de la structure de séquence-arbre. Ceci est réalisé en permutant les règles non end-actives vers le bas dans l'arbre de preuve, en exploitant l'inversibilité préservant la hauteur des règles dans $CSGL^*$.

2. Linéarisation : Une nouvelle « technique de linéarisation » est introduite pour transformer ces preuves de séquents-arbres end-actives en preuves utilisant des séquents imbriqués linéaires. Cette technique implique d'identifier des chemins spécifiques du sommet vers une feuille dans le séquence-arbre et de « élaguer » les sous-arbres, ce qui revient à réduire la structure arborescente en une séquence linéaire de séquents de Gentzen. Ce processus produit un nouveau calcul, LNGL (Calcul de Séquents Imbriqués Linéaires pour GL).

3. Forme Normale et Traduction vers Gentzen : L'article montre que les preuves dans LNGL peuvent être transformées en une forme normale spécifique. Dans cette forme, les preuves progressent par étapes répétitives : règles locales, suivies des règles de propagation ($4L$ et $\Box L$), et enfin la règle modale ($\Box R$). Cette preuve structurée est ensuite traduite dans le système de Gentzen de Sambin et Valentini ($GL_{seq}$). Enfin, des transformations standards mappent les preuves de $GL_{seq}$ vers le système étiqueté $G3KGL$ et vers les systèmes cycliques/non bien fondés ($GL_{circ}$, $GL_\infty$).

Contributions Clés

• Nouveau Calcul (LNGL) : L'article introduit LNGL, le premier calcul de séquents imbriqués linéaires sans coupure pour la logique de Gödel-Löb. Ce système opère sur des lignes de séquents de Gentzen et conserve des propriétés fondamentales comme l'inversibilité et l'admissibilité du coup.
• Nouvelle Technique de Linéarisation : L'auteur présente une méthode générale pour extraire des systèmes de séquents imbriqués linéaires à partir de systèmes d'hyper-séquents arborescents. Cette technique est conjecturée comme étant applicable à d'autres logiques modales et apparentées pour générer de nouveaux systèmes imbriqués linéaires.
• Correspondance de Preuve Complète : L'article établit une correspondance syntaxique complète à six voies entre les systèmes suivants : $G3KGL$, $CSGL^*$, $LNGL$, $GL_{seq}$, $GL_\infty$, et $GL_{circ}$.
• Mappages Constructifs : Le travail fournit les premiers mappages de preuve constructifs entre les systèmes structurels (étiquetés, hyper-séquents arborescents, imbriqués linéaires) et le système de séquents cycliques ($GL_{circ}$).

Résultats
Le résultat principal est la démonstration que les preuves dans l'un des six principaux systèmes de séquents pour GL peuvent être syntaxiquement transformées en preuves dans n'importe quel autre. Spécifiquement :

• Les preuves dans $CSGL^*$ peuvent être transformées en preuves end-actives, puis linéarisées en LNGL.
• Les preuves dans LNGL peuvent être normalisées et transformées en $GL_{seq}$.
• Les preuves dans $GL_{seq}$ peuvent être transformées en $G3KGL$ et dans les systèmes cycliques ($GL_{circ}$, $GL_\infty$).
• L'article confirme que $LNGL$ est sain et complet pour GL, et que les preuves dans $LNGL$ peuvent être mises sous une forme normale où les applications de règles modales et locales se répètent par étapes.

Signification
L'article affirme « compléter le tableau » des correspondances de théorie de la preuve pour la logique de Gödel-Löb. En établissant ces transformations syntaxiques, ce travail permet le transfert de résultats (tels que les propriétés d'interpolation ou les bornes de complexité) entre les systèmes sans nécessiter de preuves indépendantes dans chaque formalisme. De plus, l'introduction de LNGL fournit un nouvel outil pour la recherche de preuves avec des propriétés de complexité optimales, tandis que la technique de linéarisation offre une voie potentielle pour générer des systèmes imbriqués linéaires pour d'autres logiques. Le travail fournit également le premier mappage constructif entre les systèmes structurels et les preuves cycliques, comblant un fossé entre différentes approches du raisonnement inductif/coinductif en logique modale.