Labelled Sequent Calculi for Propositional Team Logics

Technische Samenvatting: Gelabelde Sequentencalculi voor Propositionele Teamlogica's

Probleemstelling
Het artikel behandelt de bewijs theoretische uitdagingen die verbonden zijn aan propositionele logica's gebaseerd op teamsemantiek. Hoewel de semantische eigenschappen van naar beneden gesloten (downward-closed) teamlogica's — specifiek de basis inkwisitieve logica (InqB), propositionele intuïtionistische afhankelijkheidslogica (PID), en hun uitbreidingen met tensor-disjunctie (InqB∨ en PID∨) — goed begrepen zijn, blijft hun bewijstheorie onderontwikkeld. Bestaande analytische bewijs-systemen voor deze logica's, zoals multi-type display calculi of deep-inference sequentencalculi, maken vaak gebruik van complexe structurele verrijkingen van Gentzen-stijl sequenten. De auteurs identificeren een behoefte aan modulaire, gelabelde sequentencalculi die de specifieke bevredigingsvoorwaarden van teamsemantiek kunnen afhandelen, met name het gedrag van tensor-disjunctie (∨) en afhankelijkheidsatomen, terwijl eigenschappen zoals cut-admissibiliteit en terminerende bewijszoeking worden gewaarborgd.

Methodologie
De auteurs ontwikkelen twee families van gelabelde sequentencalculi voor de vier doel-logica's:

1. Algemene Gelabelde Calculi ($G(L)$): Deze systemen maken gebruik van labels geconstrueerd uit oneindige verzamelingen van teamvariabelen ($S$ voor singleton teams, $A$ voor willekeurige teams) gecombineerd met verzamelingstheoretische operaties (unie $\cup$ en doorsnede $\cap$). De labels representeren willekeurige teams, singleton teams en hun combinaties. De calculi bevatten:

   • Initiële Sequenten en Logische Regels: Deze spiegelen de bevredigingsvoorwaarden gedefinieerd in teamsemantiek (bijv. regels voor $\land$, $\lor$, $\to$, en de tensor $\lor$).
   • Orde-regels: Een reeks regels die de verzamelingstheoretische eigenschappen van teams formaliseren (bijv. transitiviteit, unie, doorsnede, en de lege team-eigenschap).
   • Speciale Regels: Een regel genaamd fin wordt geïntroduceerd om de aanname te behandelen dat de verzameling propositionele variabelen $P$ eindig is. Deze regel staat het systeem toe om elk team te beschrijven als een unie van $2^{|P|}$ evaluaties, wat cruciaal is voor het simuleren van de tensor-disjunctie over klassieke formules.
   • Modulariteit: De systemen zijn zodanig ontworend dat calculi voor PID en PID∨ worden verkregen door specifieke regels voor afhankelijkheidsatomen toe te voegen aan de calculi voor InqB en InqB∨.

2. Terminerende Calculi ($G^\star(L)$): Om automatische bewijszoeking te faciliteren, introduceren de auteurs een vereenvoudigde variant waarbij labels worden gedefinieerd als eindige verzamelingen van variabelen in plaats van complexe termen met unies en doorsneden. Deze aanpak elimineert de noodzaak voor relationele atomen en orde-regels, en vervangt deze door regels die direct opereren op de verzameling variabelen in een label.

Belangrijkste Bijdragen en Resultaten

• Soundness en Compleetheid: De auteurs bewijzen dat de algemene calculi $G(L)$ sound en volledig zijn met betrekking tot de corresponderende teamsemantiek en Hilbert-stijl axiomatiseringen. Dit wordt bereikt door de admissibiliteit van structurele regels (verzwakking, contractie, cut) aan te tonen en de admissibiliteit van afgeleide regels (zoals mp voor modus ponens en flat voor de platheid van klassieke formules) vast te stellen.
• Cut-Admissibiliteit: Een centraal technisch resultaat is het bewijs van cut-admissibiliteit voor alle vier de calculi. Het bewijs verloopt via inductie op de rang van de cut-formule en de hoogte van de afleiding, waarbij gebruik wordt gemaakt van een lexicografische ordening die rekening houdt met zowel de complexiteit van de formule als het label.
• Terminerende Bewijszoeking: Het artikel presenteert expliciete, terminerende bewijszoekingsalgoritmen voor de vereenvoudigde calculi $G^\star(L)$. Het algoritme construeert een bewijszoekingsboom van wortel naar blad (root-first). Er wordt bewezen dat het termineert omdat het aantal mogelijke gelabelde formules eindig is (gegeven een eindige verzameling propositionele variabelen en een eindige verzameling subformules).
• Beslissingsprocedures: Het terminerende karakter van de $G^\star(L)$ calculi impliceert dat de verzadigbaarheids- en geldigheidsproblemen voor InqB, PID, InqB∨ en PID∨ beslisbaar zijn. De auteurs bieden een tegenmodel-constructie aan vanuit elke verzadigde (open) tak van de bewijszoekingsboom, wat de compleetheid van de zoekprocedure waarborgt.

Betekenis en Claims
Het artikel claimt dat de primaire bijdrage ligt in het leveren van de eerste sound en complete gelabelde sequentencalculi voor het volledige bereik van propositionele teamlogica's, inclusief tensor-disjunctie en afhankelijkheidsatomen. De auteurs benadrukken twee duidelijke voordelen van hun aanpak:

1. Modulariteit: De bewijssystemen kunnen worden aangepast aan verschillende verzamelingen van connectieven of atomen door simpelweg regels toe te voegen of te verwijderen, een kenmerk dat niet aanwezig is in de meer rigide gestructureerde calculi uit de eerdere literatuur.
2. Terminatie en Beslisbaarheid: Door de labelstructuur te vereenvoudigen in $G^\star(L)$, bieden de auteurs een concrete beslissingsprocedure voor deze logica's, wat een belangrijke stap is voor geautomatiseerd redeneren in teamsemantiek.

De auteurs merken op dat hoewel de algemene calculi $G(L)$ kortere bewijzen kunnen opleveren door regels met vaste premissen en de mogelijkheid om over willekeurige deelverzamelingen te redeneren via variabelen, de vereenvoudigde calculi $G^\star(L)$ essentieel zijn voor het vaststellen van terminatie. Het werk is beperkt tot talen met eindig veel propositionele atomen, een noodzakelijke voorwaarde voor de fin-regel en de terminatie van de bewijszoeking in aanwezigheid van tensor-disjunctie. Het artikel concludeert door toekomstig werk te identificeren, waaronder het uitbreiden van deze systemen naar talen met oneindig veel atomen en het ontwikkelen van bewijssystemen voor andere klassen van teamlogica's, zoals die zonder intuïtionistische implicatie of die met de unie-sluitingseigenschap.