Technische Samenvatting: Interpolatie via Gegeneraliseerde Splitsing

Probleemstelling

Het artikel behandelt de bewijs-theoretische bewijsvoering van de Lyndon-interpolatiestelling. Hoewel interpolatie is vastgesteld voor diverse logica's (klassiek, intuïtionistisch, modaal, lineair) met behulp van model-theoretische, automata-theoretische of syntactische methoden, steunt de meest gebruikelijke bewijs-theoretische benadering op Maehara's methode. Deze methode extraheert chirurgisch een interpolant uit een snijvrij sequentiebewijs. Echter, de aanpak van Maehara en haar moderne varianten missen vaak modulariteit; kleine wijzigingen aan een bewijssysteem (bijv. het toevoegen van nieuwe regels) vereisen vaak dat de volledige interpolatiebewijsvoering opnieuw wordt gedaan. Bovendien mengt de traditionele sequentiecalculus "kern"-logische regels met structurele regels (zoals verzwakking en contractie), wat het moeilijk maakt om de logische essentie van een afleiding te scheiden van de aspecten van hulpbronbeheer (resource management).

De auteur stelt een nieuwe methode voor die de sequentiecalculus volledig vermijdt door gebruik te maken van deep inference technieken. Het doel is om interpolatie niet louter te formuleren als de existentie van een formule, maar als een structurele decompositie van een afleiding, waardoor een meer modulaire en generaliseerbare bewijstechniek wordt bereikt.

Methodologie

De voorgestelde methodologie is geworteld in deep inference, een bewijs-theoretisch kader waarin inferentieregels op elke diepte binnen een formule kunnen worden toegepast, in plaats van alleen bij de wortel. De kern van de aanpak bestaat uit drie belangrijke technische componenten:

1. Gegeneraliseerde Splitsingslemma:
   Het standaard splitsingslemma in deep inference stelt dat als een formule $(A \otimes B) \parr K$ bewijsbaar is, de context $K$ kan worden gesplitst in $K_A$ en $K_B$ zodanig dat $A \parr K_A$ en $B \parr K_B$ bewijsbaar zijn. De auteur generaliseert dit naar afleidingen met een willekeurige premisse $J$ (in plaats van enkel de eenheid $1$). Specifiek, indien $J \vdash (A \otimes B) \parr K$, kan de afleiding worden gedecomposeerd in een "up-fragment" (het afleiden van een gesplitste context uit $J$) en een "down-fragment" (het afleiden van $K$ uit de gesplitste context), terwijl simultaan de sub-afleidingen voor $A$ en $B$ worden geïsoleerd. Cruciaal is dat deze generalisatie specifieke regels vereist (aangeduid als $p'_{\downarrow}, d'_{\downarrow}, d'_{0\downarrow}$) die niet strikt noodzakelijk zijn voor volledigheid, maar essentieel zijn voor de decompositie.

2. Kern/Niet-kern Scheiding:
   De bewijssystemen worden gedecomposeerd in een kern-fragment (bevattende logische regels en specifieke structurele regels zoals $p'_{\downarrow}$) en een niet-kern fragment (bevattende standaard structurele regels zoals verzwakking, contractie en promotie). Een sleutellemma toont aan dat elke afleiding in het volledige systeem kan worden gepermuteerd naar een vorm waarbij het kern-fragment eerst wordt toegepast, gevolgd door het niet-kern fragment, waarbij de multiplicatieve structuur van de conclusie behouden blijft. Deze scheiding maakt de interpolatiebewijsvoering modulair: de kern handelt de logische splitsing af, terwijl het niet-kern fragment het hulpbronbeheer afhandelt.

3. Flipping Lemma:
   Bouwend op de gegeneraliseerde splitsing, introduceert de auteur een "flipping"-mechanisme. Dit lemma staat de transformatie toe van een afleiding waarbij een "up-fragment" (analoog aan cut-introductie) boven een "down-fragment" (analoog aan cut-eliminatie) staat, naar een nieuwe afleiding waarbij de rollen zijn omgedraaid of gestructureerd. Specifiek kan een afleiding van $H$ naar $F \parr K$ via een up-fragment en een down-fragment worden getransformeerd naar een afleiding van $F^\perp \otimes H$ naar $K$ via een geflipte up-fragment en down-fragment, waarbij een intermediaire formule $I$ wordt geïntroduceerd.

Belangrijkste Bijdragen

1. Een Nieuwe Bewijs-theoretische Methode voor Interpolatie:
   Het artikel presenteert een bewijs van de Lyndon-interpolatiestelling dat niet leunt op de sequentiecalculus. In plaats daarvan gebruikt het het gegeneraliseerde splitsingslemma en het flipping lemma binnen deep inference systemen. Deze aanpak beschouwt interpolatie als een decompositie van een afleiding in een up-fragment en een down-fragment, gescheiden door een interpolant $I$.

2. Theorem 1 (Decompositie Theorem):
   De centrale resultaat stelt dat elke afleiding $A \vdash_X B$ gedecomposeerd kan worden in:
   $$A \xrightarrow{\delta_1} I \xrightarrow{\delta_2} B$$
   waarbij $\delta_1$ enkel regels gebruikt uit het up-fragment ($X^\uparrow$) en $\delta_2$ enkel regels uit het down-fragment ($X^\downarrow$). De formule $I$ dient als de Lyndon-interpolant. Dit theorem wordt gepresenteerd als zowel een versterking van de standaard interpolatiestelling (het leveren van expliciete bewijzen voor $A \vdash I$ en $I \vdash B$) als een generalisatie van de cut-eliminatiestelling.

3. Nieuwe Bewijssystemen voor Modale Logica's:
   De auteur introduceert nieuwe cut-vrije deep inference bewijssystemen voor de modale logica's K, KT, K4 en S4. Bestaande deep inference systemen voor modale logica werden als ontoereikend beschouwd (specifiek door het gebrek aan de noodzakelijke kern/niet-kern scheiding of cut-eliminatie eigenschappen). Deze nieuwe systemen maken het mogelijk om de interpolatieresultaten uit te breiden van lineaire en klassieke logica naar deze modale logica's.

4. Modulariteit van Bewijs:
   De methodologie vestigt een modulaire structuur voor interpolatiebewijzen. Omdat het kern-fragment het gegeneraliseerde splitsingslemma onafhankelijk van het niet-kern fragment bevredigt, vereisen kleine wijzigingen in het bewijssysteem (bijv. het toevoegen van nieuwe modaliteiten of structurele regels) geen volledige herleiding van de interpolatiestelling, mits de kern/niet-kern scheiding gehandhaafd blijft.

Resultaten

Het artikel demonstreert succesvol de flexibiliteit van de aanpak door deze toe te passen op:

• Lineaire Logica: Het bewijzen van interpolatie voor systemen inclusief multiplicatieve, additieve en exponentiële fragmenten (MELL).
• Klassieke Logica: Het aantonen dat de resultaten voor lineaire logica de resultaten voor klassieke logica impliceren via een translatie, en het bieden van een direct bewijs voor het systeem SKS.
• Modale Logica's: Het vaststellen van interpolatie voor K, KT, K4 en S4 met behulp van de nieuw ontworpen bewijssystemen.

In alle gevallen levert de methode een Lyndon-interpolant op (die de polariteit van propositionele symbolen behoudt) en construeert zij expliciete afleidingen voor de implicaties van de interpolant. Het artikel merkt ook op dat de decompositie in up- en down-fragmenten op twee manieren leidt tot cut-eliminatie: direct (indien de premisse de eenheid is) en via een "flipping"-operatie die een cut-vrije afleiding van de implicatie construeert.

Betekenis en Claims

Het artikel claimt dat de primaire betekenis ligt in de modulariteit. Verwijzend naar de observatie van Girard dat het gebrek aan modulariteit een grote beperking is in de huidige bewijs-theorie, betoogt de auteur dat traditionele methoden (zoals die van Maehara) een "redo van scratch" afdwingen wanneer een bewijssysteem wordt gewijzigd. In contrast hiermee isoleert de gepresenteerde deep inference aanpak de logische kern van de structurele regels, waardoor interpolatiebewijzen robuust zijn tegen systeemvariaties.

De auteur benadrukt ook dat de methode een diepere connectie tussen interpolatie en cut-eliminatie onthult. Het decompositie-theorem suggereert dat interpolatie een specifiek geval is van een "inverse cut-eliminatie", waarbij de interpolant fungeert als een brug tussen het up-fragment (cut-introductie) en het down-fragment (cut-eliminatie).

Ten slotte positioneert het artikel dit werk als een stap naar het begrijpen van interpolatie in logica's waar geen sequentiecalculus bestaat, waarbij gesuggereerd wordt dat de kern/niet-kern scheiding een algemeen criterium zou kunnen zijn voor de existentie van interpolatie in andere logische systemen. De auteur merkt bescheiden op dat hoewel de methode krachtig is, deze momenteel steunt op specifieke ontwerpkeuzes in de inferentieregels (zoals de inclusie van $p'_{\downarrow}$), en dat verder werk nodig is om deze resultaten uit te breiden naar eerste-orde logica en andere modale logica's.