Uniform Interpolation of Basic Tense Logic

Résumé Technique : Interpolation Uniforme de la Logique de la Temporalité de Base

Énoncé du Problème
L'article traite du problème ouvert consistant à établir la propriété d'interpolation uniforme pour la logique de la temporalité de base (également appelée logique modale à deux voies ou logique modale avec converse), notée $K_t$. Bien que la propriété d'interpolation de Craig pour $K_t$ soit bien établie par des méthodes tant prouvistes que sémantiques, la propriété d'interpolation uniforme — qui exige l'existence d'un « interpolant uniforme » $\exists p.\phi$ pour toute formule $\phi$ et variable $p$ telle que $\exists p.\phi$ est indépendant de $p$ et préserve les relations de prouvabilité avec toutes les formules sans $p$ — n'avait pas été pleinement démontrée pour cette logique. L'auteur note que si Visser (1996) a fourni un argument sémantique pour l'interpolation uniforme de la logique modale de base $K$ en utilisant des bisimulations par couches, ce résultat n'avait pas été étendu à l'expansion tense impliquant la modalité de converse.

Méthodologie
L'article emploie une approche sémantique, étendant l'argument modèle-théorique de Visser basé sur les bisimulations par couches (ou bornées) au contexte de la logique de la temporalité. La méthodologie procède selon les étapes suivantes :

1. Définitions et Cadre : L'auteur définit la syntaxe et la sémantique de la logique de la temporalité de base, introduisant le système de Hilbert standard $H(K_t)$ et la sémantique de Kripke avec les modalités de passage vers l'avant ($\square$) et vers l'arrière ($\blacksquare$). Le concept de bisimulation par couches est adapté pour la logique de la temporalité, en incorporant des conditions pour les transitions vers l'avant ($Forth$, $Back$) et vers l'arrière ($Forth^{-1}$, $Back^{-1}$), indexées par la profondeur modale $n$.
2. Propriété d'Expansion de Bisimulation : Une condition suffisante pour qu'une logique de la temporalité normale $\Lambda_{\mathcal{F}}$ (associée à une classe de cadres $\mathcal{F}$) possède la propriété d'interpolation uniforme est formulée. Cette condition, nommée propriété d'expansion de bisimulation, exige que pour tout couple de modèles pointés $(M_1, w_1)$ et $(M_2, w_2)$ dans $\mathcal{F}$ qui sont bisimilaires jusqu'à la profondeur $n$ sur un ensemble partagé de variables, il existe un modèle intermédiaire $(N, x)$ dans $\mathcal{F}$ qui les relie via des bisimulations sur les ensembles de variables respectifs.
3. Construction du Modèle Intermédiaire : La contribution technique centrale consiste à prouver que la classe de tous les cadres ($\mathcal{F}_{all}$) possède la propriété d'expansion de bisimulation. L'auteur construit un modèle intermédiaire $N$ en prenant l'union disjointe des deux modèles d'entrée et en ajoutant un nouvel état « universel » $T$ connecté à tous les états. La relation dans $N$ est définie sur un espace produit impliquant les états des modèles originaux et un indice de « couche », simulant efficacement les étapes de bisimulation requises pour satisfaire la propriété d'expansion.
4. Résultats de Transfert : L'article étudie la préservation de la propriété d'interpolation uniforme sous diverses extensions :
   • Images Miroirs : Si une logique $\Lambda$ est invariante sous l'opération d'image miroir (échange de $\square$ et $\blacksquare$), la propriété se transfère aux extensions par des axiomes d'image miroir.
   • Axiomes Constantes : La propriété est préservée lors de l'ajout de formules constantes (formules sans variables propositionnelles).
   • Traduction Boxdot : La propriété est montrée comme se transférant à l'équivalent réflexif d'une logique via la traduction boxdot.
5. Construction de Contre-Exemple : Pour démontrer les limites de la propriété, l'article analyse l'expansion tense de la logique modale $S4$ (notée $S_4^t$). En utilisant une construction de modèle spécifique (un chemin infini avec des valeurs de vérité alternées pour une proposition $r$) et un argument de bisimulation par couches, l'auteur prouve que $S4_t$ ne possède pas la propriété d'interpolation uniforme.

Contributions Clés et Résultats

• Théorème Principal : L'article établit que la logique de la temporalité de base minimale $K_t$ possède la propriété d'interpolation uniforme. Ceci est réalisé en prouvant que la classe de tous les cadres satisfait la propriété d'expansion de bisimulation.
• Caractérisation Sémantique : Il est démontré que l'interpolant uniforme dans $K_t$ coïncide avec un quantificateur de bisimulation. Plus précisément, une formule $\exists p.\phi$ est vraie en un état si et seulement si il existe un modèle bisimilaire (où $p$ est interprété différemment) dans lequel $\phi$ est vraie.
• Extension aux Sous-logiques : La propriété d'interpolation uniforme est montrée comme s'appliquant à diverses extensions de $K_t$, incluant celles définies par des axiomes constants (ex: existence de moments premiers/derniers) et des extensions invariantes par image miroir.
• Échec dans $S4_t$ : L'article prouve que l'expansion tense de $S4$ ($S4_t$) ne possède pas la propriété d'interpolation uniforme. Ce résultat étend les conclusions antérieures de Ghilardi et Zawadowski sur $S4$ au cadre de la temporalité, montrant que l'ajout des axiomes de réflexivité et de transitivité brise la propriété d'interpolation uniforme.
• Mécanismes de Transfert : L'article fournit des preuves formelles pour le transfert de la propriété d'interpolation uniforme via les images miroirs, les extensions constantes et la traduction boxdot, permettant la dérivation de résultats pour des logiques telles que $K_t \oplus T_\square$ et $K_t \oplus 4_\square$ (sous certaines conditions).

Signification
L'article affirme résoudre une lacune importante dans la littérature concernant les propriétés méta-logiques de la logique de la temporalité de base. En étendant l'argument sémantique de Visser au cadre de la modalité à deux voies, l'auteur confirme que $K_t$ jouit de la propriété d'interpolation uniforme, un résultat qui était auparavant inconnu malgré l'usage répandu de cette logique en philosophie, en informatique et en sémantique formelle. Le travail clarifie la frontière entre les logiques qui possèdent cette propriété d'interpolation forte (comme $K_t$) et celles qui ne l'ont pas (comme $S4_t$), fournissant un cadre sémantique robuste (bisimulations par couches) pour analyser l'interpolation dans les logiques de la temporalité. De plus, l'article suggère que l'interpolant uniforme dans $K_t$ peut être compris sémantiquement comme une version temporelle d'un quantificateur de bisimulation, offrant une compréhension conceptuelle plus profonde de la puissance expressive de la logique. Les résultats posent également les bases de futures investigations sur l'interpolation de Lyndon uniforme et l'application de ces techniques aux logiques multimodales et hybrides de la temporalité.