Dynamic Hypersequents for Public Announcement Logic

Résumé Technique : Hyper-séquentes Dynamiques pour la Logique de l'Annonce Publique

Énoncé du Problème
La Logique Épistémique Dynamique (LED), et plus spécifiquement la Logique de l'Annonce Publique (LAP), modélise l'évolution des connaissances par le biais de mises à jour d'information. Bien que la sémantique de la LAP soit bien comprise comme des transformations de modèles de Kripke (où une annonce restreint l'ensemble des mondes possibles), les cadres de preuve théorique existants peinent à capturer cette dynamique au niveau syntaxique. Les tentatives précédentes, incluant les méthodes de tableaux et divers calculs de séquentes (étiquetés et non étiquetés), échouent souvent à atteindre simultanément une propriété de sous-formule véritable, l'admissibilité de toutes les règles structurelles (y compris la contraction) et l'élimination syntaxique des coupures. De nombreux systèmes existants reposent sur des axiomes de réduction qui traduisent les formules dynamiques en formules statiques, obscurcissant ainsi la nature dynamique de la logique au sein du système de preuve lui-même.

Méthodologie
Les auteurs proposent un nouveau cadre de preuve théorique basé sur les hyper-séquentes dynamiques. Cette approche étend le calcul des hyper-séquentes pour S5 (introduit dans [15, 16]) en incorporant un mécanisme pour modéliser les transitions entre modèles épistémiques induites par des annonces publiques.

1. Séquentes Dynamiques : Une séquente dynamique est définie comme une séquence de séquentes standards étiquetées par des séquences finies distinctes d'annonces (par exemple, $\alpha_1 \Gamma_1 | \dots | \alpha_n \Gamma_n$). Intuitivement, une séquente dynamique représente un monde spécifique $w$ dans un modèle initial $M$ et ses « copies » dans des modèles mis à jour successivement $M_{\alpha}$.
2. Hyper-séquentes Dynamiques (HSD) : Une hyper-séquente dynamique est une collection de séquentes dynamiques. Cette structure représente syntaxiquement un modèle épistémique entier et ses mises à jour successives simultanément. Les auteurs interprètent une HSD comme une disjonction de formules modalisées, où chaque composant correspond à un monde dans le modèle ou à ses mises à jour.
3. Le Calcul ($DHSLAP$) : Les auteurs définissent un calcul $DHSLAP$ comprenant :
   • Règles Propositionnelles et Modales : Adaptées des calculs d'hyper-séquentes standards pour S5.
   • Règles d'Annonce : Des règles $(L[\cdot])$ et $(R[\cdot])$ qui décomposent les formules d'annonce publique $[A]B$. Ces règles gèrent explicitement la transition d'un état courant vers un état mis à jour en introduisant de nouvelles séquentes dynamiques étiquetées par la séquence d'annonce étendue $\alpha \cdot A$.
   • Règles Structurelles Dynamiques : Des règles spécifiques telles que $(Lat)$ et $(Rat)$ (Permanence Atomique), $(New)$ (assurant que les mondes dans les modèles mis à jour existent dans les précédents) et $(Recall)$ (assurant que la formule annoncée vaut dans le modèle précédent).
   • Règle Modale Dynamique : Une règle spécialisée $(L\Box_3)$ qui gère l'interaction entre la connaissance ($\Box$) et les séquences d'annonces, distinguant les mondes qui survivent à une mise à jour de ceux qui ne le font pas.

Contributions et Résultats Clés
L'article établit que $DHSLAP$ est un système de preuve robuste pour la LAP, atteignant plusieurs propriétés que les systèmes précédents ne parvenaient pas à réunir simultanément :

• Admissibilité des Règles Structurelles : Les auteurs prouvent l'admissibilité préservant la hauteur (hp-admissibilité) de l'affaiblissement, de la contraction et d'une règle de fusion. Crucialement, cela inclut la contraction, qui est souvent difficile à obtenir dans les logiques dynamiques sans perdre l'analyticité.
• Inversibilité des Règles Logiques : Toutes les règles logiques du calcul sont montrées comme étant hp-inversibles. Cette propriété est essentielle pour la recherche de preuves et l'établissement de l'élimination des coupures.
• Élimination Syntaxique des Coupures : L'article fournit une preuve de l'admissibilité de la règle de Coupure. La preuve repose sur une double induction : l'une sur la complexité HSD de la formule de coupure (une mesure de complexité relative à la séquence d'annonce) et l'autre sur la somme des hauteurs des dérivations des prémisses.
• Correction et Complétude : Le calcul est prouvé correct et complet par rapport à la sémantique standard de Kripke de la LAP. La preuve de complétude implique la dérivation de tous les axiomes de style Hilbert de la LAP, y compris les axiomes de réduction, au sein du cadre des hyper-séquentes dynamiques.
• Propriété de Sous-formule : En conséquence de l'élimination des coupures, le calcul jouit de la propriété de sous-formule, garantissant que toute formule dans une dérivation est une sous-formule de la séquente finale ou d'une annonce y figurant.

Signification et Revendications
Les auteurs affirment que ce travail représente une étape significative vers la réduction de l'écart entre le dynamisme sémantique de la LAP et sa théorie de la preuve syntaxique. En utilisant des hyper-séquentes dynamiques, le système capture le caractère dynamique de la logique par des moyens purement structurels, évitant le besoin d'éléments sémantiques explicites (comme des étiquettes pour les mondes) ou d'une réduction à une logique statique.

L'article affirme que, à leur connaissance, $DHSLAP$ est le premier calcul pour la LAP satisfaisant simultanément :

1. L'admissibilité de toutes les règles structurelles (y compris la contraction).
2. L'inversibilité de toutes les règles logiques.
3. L'élimination syntaxique des coupures.
4. Une propriété de sous-formule véritable.

Les auteurs concluent que le cadre des hyper-séquentes dynamiques est suffisamment expressif et robuste pour servir de fondement au développement de calculs de séquentes pour des classes plus larges de logiques épistémiques dynamiques impliquant différents types de mises à jour d'information. Ils suggèrent que des travaux futurs pourraient explorer la décidabilité, l'interpolation et l'analyse de la complexité dans ce cadre.