Uniform Interpolation of Basic Tense Logic

Technische Samenvatting: Uniforme Interpolatie van Basale Tense Logica

Probleemstelling
Het artikel behandelt het openstaande probleem van het vaststellen van de eigenschap van uniforme interpolatie voor basale tense logica (ook wel bekend als twee-weg modale logica of modale logica met converse), aangeduid als $K_t$. Terwijl de eigenschap van de Craig-interpolatie voor $K_t$ reeds goed gevestigd is via zowel proof-theoretische als semantische methoden, was de eigenschap van uniforme interpolatie — die vereist dat er voor elke formule $\phi$ en variabele $p$ een "uniforme interpolant" $\exists p.\phi$ bestaat waarvoor $\exists p.\phi$ onafhankelijk is van $p$ en de bewijsbaarheidrelaties met alle $p$-vrije formules behoudt — nog niet volledig voor deze logica is aangetoond. De auteur merkt op dat hoewel Visser (1996) een semantisch argument leverde voor de uniforme interpolatie van de basale modale logica $K$ met behulp van gelaagde bisimulaties, dit resultaat niet was uitgebreid naar de tense expansie met betrekking tot de converse modaliteiten.

Methodologie
Het artikel maakt gebruik van een semantische benadering door Vissers modeltheoretische argument gebaseerd op gelaagde (of begrensde) bisimulaties uit te breiden naar de context van tense logica. De methodologie verloopt via de volgende stappen:

1. Definities en Raamwerk: De auteur definieert de syntaxis en semantiek van de basale tense logica, waarbij het standaard Hilbert-systeem $H(K_t)$ en Kripke-semantiek met voorwaartse ($\square$) en achterwaartse ($\blacksquare$) modaliteiten worden geïntroduceerd. Het concept van gelaagde bisimulatie wordt aangepast voor tense logica, waarbij voorwaarden worden opgenomen voor zowel voorwaartse ($Forth$, $Back$) als achterwaartse ($Forth^{-1}$, $Back^{-1}$) transities, geïndexeerd door modale diepte $n$.
2. Bisimulatie Expansie-eigenschap: Een voldoende voorwaarde voor een normale tense logica $\Lambda_{\mathcal{F}}$ (geassocieerd met een frameklasse $\mathcal{F}$) om de eigenschap van uniforme interpolatie te bezitten, wordt geformuleerd. Deze voorwaarde, de bisimulatie expansie-eigenschap genoemd, vereist dat voor elke twee gepunteerde modellen $(M_1, w_1)$ en $(M_2, w_2)$ in $\mathcal{F}$ die bisimulair zijn tot diepte $n$ over een gedeelde verzameling variabelen, er een tussenliggend model $(N, x)$ in $\mathcal{F}$ bestaat dat hen verbindt via bisimulaties over de respectieve verzamelingen variabelen.
3. Constructie van het Tussenliggende Model: De kern van de technische bijdrage betreft het bewijzen dat de klasse van alle frames ($\mathcal{F}_{all}$) de bisimulatie expansie-eigenschap bezit. De auteur construeert een tussenliggend model $N$ door de disjuncte vereniging van de twee invoermodellen te nemen en een nieuwe "universele" toestand $T$ toe te voegen die met alle toestanden verbonden is. De relatie in $N$ wordt gedefinieerd over een productruimte die de toestanden van de oorspronkelijke modellen en een "laag"-index omvat, waardoor de bisimulatie-stappen die nodig zijn om de expansie-eigenschap te voldoen, effectief worden gesimuleerd.
4. Transferresultaten: Het artikel onderzoekt de instandhouding van de eigenschap van uniforme interpolatie onder diverse uitbreidingen:
   • Spiegelbeelden: Als een logica $\Lambda$ invariant is onder de spiegelbeeld-operatie (het verwisselen van $\square$ en $\blacksquare$), wordt de eigenschap overgedragen aan uitbreidingen door spiegelbeeld-axioma's.
   • Constante Axioma's: De eigenschap blijft behouden bij het toevoegen van constante formules (formules zonder propositionele variabelen).
   • Boxdot Translatie: De eigenschap wordt getoond te worden overgedragen naar de reflexieve tegenhanger van een logica via de boxdot-translatie.
5. Constructie van Tegenvoorbeelden: Om de grenzen van de eigenschap aan te tonen, analyseert het artikel de tense expansie van de modale logica $S4$ (aangeduid als $S4_t$). Met behulp van een specifieke modelconstructie (een oneindig pad met alternerende waarheidswaarden voor een propositie $r$) en een gelaagd bisimulatie-argument, bewijst de auteur dat $S4_t$ de eigenschap van uniforme interpolatie mist.

Belangrijkste Bijdragen en Resultaten

• Hoofdtheorema: Het artikel stelt vast dat de minimale basale tense logica $K_t$ de eigenschap van uniforme interpolatie bezit. Dit wordt bereikt door te bewijzen dat de klasse van alle frames de bisimulatie expansie-eigenschap bezit.
• Semantische Karakterisering: Er wordt aangetoond dat de uniforme interpolant in $K_t$ samenvalt met een bisimulatie kwantor. Specifiek geldt een formule $\exists p.\phi$ in een toestand dan en slechts dan als er een bisimulair model bestaat (waarin $p$ anders wordt geïnterpreteerd) waarin $\phi$ geldt.
• Extensie naar Sub-logica's: De eigenschap van uniforme interpolatie blijkt te gelden voor diverse uitbreidingen van $K_t$, inclusief die gedefinieerd door constante axioma's (bijv. het bestaan van eerste/laatste momenten) en spiegelbeeld-invariante uitbreidingen.
• Falen in $S4_t$: Het artikel bewijst dat de tense expansie van $S4$ ($S4_t$) niet de eigenschap van uniforme interpolatie heeft. Dit resultaat breidt de eerdere bevindingen van Ghilardi en Zawadowski over $S4$ uit naar de tense setting, waarbij wordt aangetoond dat de toevoeging van reflexiviteits- en transitiviteitsaxioma's de eigenschap van uniforme interpolatie doorbreekt.
• Transfermechanismen: Het artikel biedt formele bewijzen voor de transfer van de eigenschap van uniforme interpolatie via spiegelbeelden, constante uitbreidingen en de boxdot-translatie, wat de afleiding van resultaten voor logica's zoals $K_t \oplus T_\square$ en $K_t \oplus 4_\square$ (onder specifieke condities) mogelijk maakt.

Betekenis
Het artikel beweert een aanzienlijk gat in de literatuur met betrekking tot de meta-logische eigenschappen van basale tense logica te hebben opgelost. Door het semantische argument van Visser uit te breiden naar de twee-weg modale setting, bevestigt de auteur dat $K_t$ de eigenschap van uniforme interpolatie geniet, een resultaat dat voorheen onbekend was ondanks het wijdverbreide gebruik van deze logica in de filosofie, informatica en formele semantiek. Het werk verheldert de grens tussen logica's die deze sterke interpolatie-eigenschap bezitten (zoals $K_t$) en die welke dat niet doen (zoals $S4_t$), en biedt een robuust semantisch raamwerk (gelaagde bisimulaties) voor het analyseren van interpolatie in tense logica's. Verder suggereert het artikel dat de uniforme interpolant in $K_t$ semantisch begrepen kan worden als een temporele versie van een bisimulatie kwantor, wat een dieper conceptueel begrip biedt van de expressieve kracht van de logica. De resultaten leggen ook de basis voor toekomstig onderzoek naar uniforme Lyndon-interpolatie en de toepassing van deze technieken op multimodale en hybride tense logica's.