Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

Technische Samenvatting: Naar Geautomatiseerde Bewijs-theoretische Semantiek: Inferentie-Gedragssemantiek voor 3-Dimensionale K3 en LP

Probleemstelling
De automatisering van logisch redeneren is goed gevestigd (bijv. via resolutie, stellingbewijzers en interactieve assistenten zoals Rocq en Lean), maar de geautomatiseerde verstrekking van bewijs-theoretische semantiek (P-tS) voor dergelijk redeneren blijft een openstaande uitdaging. Hoewel systemen zoals MUltlog automatisch sequentencalculi, tableaux en natuurlijke deductie-systemen kunnen genereren voor willekeurige eindwaardige logica's vanuit model-theoretische waarheidstabellen, missen zij de omgekeerde capaciteit: het genereren van bewijs-theoretische betekenispecificaties voor de connectieven binnen die systemen. Bestaande P-tS-benaderingen, zoals bewijs-theoretische geldigheid of basis-extensie-semantiek, zijn vaak calculus-afhankelijk, wat het vergelijken van de betekenissen van connectieven over verschillende logica's heen (bijv. klassiek versus intuïtionistisch) verhindert. Dit artikel beoogt het Inference-Behaviour Semantics (I-bS) raamwerk — dat de betekenis van connectieven modelleert via hun minimale inferentiegedrag — te integreren in het MUltlog-raamwerk om de generatie van P-tS voor meerwaardige logica's te automatiseren.

Methodologie
Dit artikel breidt het I-bS-raamwerk, dat voorheen beperkt was tot 2-dimensionale sequentencalculi, uit naar n-dimensionale sequentencalculi. De methodologie verloopt via de volgende stappen:

1. Formeel Apparaat: De auteur definieert $n$-dimensionale sequenten als $n$-tuples van multisets van formules. Om deze te interpreteren zonder terug te grijpen op model-theoretische waarheidswaarden, wordt een multilaterale lezing gehanteerd. Voor 3-dimensionale sequenten (specifiek voor de Strong Kleene-logica, K3, en de Logica van de Paradox, LP) houdt dit drie taalhandelingen in: assertie (dimensie 1), opschorting van oordeel (dimensie 2) en ontkenning (dimensie 3).
2. Minimale Afleidbaarheidsrelatie: Om de betekenis van connectieven te isoleren van de structurele kenmerken van een specifieke logica, definieert de auteur een minimale afleidbaarheidsrelatie bestaande uit Identiteit ($Id_3$) en een beperkte Cut-regel ($Cut_2$). Dit voorkomt de "verwarrende" effecten van volledige structurele regels (zoals Contractie en Verzwakking) die in standaardcalculi voorkomen.
3. Definieerbaarheid en Inferentiegedrag: Volgend een Belnap-stijl definitie, wordt een connectief gedefinieerd als deze de basiscalculus conservatief uitbreidt en uniek inter-afleidbaar is met een tegenhanger. De kernmetriek is inferentiegedrag ($ib$), een functie die de horizontale locaties (dimensies) en regeltoepassingen van een connectief tijdens zijn definiebaarheidsbewijs bijhoudt.
4. Betekenis-extensie: Om de betekenis van connectieven over verschillende dimensionaliteiten heen te vergelijken (bijv. 2D klassiek versus 3D paraconsistent), introduceert het artikel betekenis-extensie. Een $m$-dimensionaal connectief breidt de betekenis van een $n$-dimensionaal connectief uit ($m > n$) indien het inferentiegedrag van de laatste conservatief wordt behouden binnen een $n$-dimensionaal fragment van de eerste.

Kernbijdragen en Resultaten
Het artikel past dit uitgebreide raamwerk toe op twee 3-waardige logica's: K3 en LP, gebruikmakend van de 3-dimensionale sequentencalculi gegenereerd door MUltlog.

• Semantische Clausules voor K3/LP: De auteur bewijst uniciteit en conservativiteit voor zowel multiplicatieve als additieve versies van K3-connectieven relatief aan de minimale $\{Id_3, Cut_2\}$-relatie. De auteur leidt onderscheidende semantische clausules af voor elk versie van de connectieven (bijv. multiplicatieve conjunctie $\otimes$ versus additieve conjunctie $\sqcap$), waarmee wordt aangetoond dat standaard K3-calculi semantisch onderscheidbare connectieven confunderen vanwege hun structurele regels.
• Identiteit van K3 en LP Betekenissen: Een centraal resultaat is dat de connectieven in K3 en LP identieke betekenissen bezitten. Hoewel K3 en LP verschillen in hun aangewezen waarden (K3 wijst alleen dimensie 3 aan; LP wijst dimensies 2 en 3 aan), zijn hun verticale afleidbaarheidseigenschappen en operationele regels identiek. Bijgevolg zijn hun inferentiegedragingen in definiebaarheidsbewijzen identiek, wat resulteert in dezelfde semantische clausules.
• Betekenis-extensie van Klassieke Logica: Het artikel demonstreert dat de 3-dimensionale connectieven van K3 en LP betekenis-extensies zijn van hun klassieke tegenhangers in LK (2-dimensionaal). Door de 3-dimensionale semantische clausules te projecteren op de 1e en 3e dimensie (het verwijderen van de 2e dimensie), zijn de resulterende regels syntactisch identiek aan de semantische clausules van klassieke LK-connectieven. Dit bevestigt dat de K3/LP-connectieven klassieke betekenissen conservatief uitbreiden zonder deze te wijzigen.
• Omgang met Structurele Regels: De analyse onthult dat contextrestricties (bijv. het beperken van het aantal formules in sequentcomponenten) noodzakelijk zijn om het minimale inferentiegedrag te handhaven. Zonder deze restricties zouden standaard structurele regels (zoals Contractie) het inferentiegedrag veranderen, wat effectief de betekenis van de connectieven wijzigt.

Betekenis en Claims
Het artikel claimt de eerste fundamentele casestudy te bieden voor het uitbreiden van I-bS naar dimensies groter dan twee. De primaire betekenis ligt in:

1. Vergelijking tussen Calculi: Het vestigt een mechanisme om de betekenis van connectieven over logica's met verschillende dimensionaliteiten te vergelijken, waarmee een gat in de eerdere P-tS literatuur wordt gedicht die moeite had met het vergelijken van logica's met verschillende structurele eigenschappen.
2. Validatie van Logisch Pluralisme: De bevinding dat K3 en LP identieke betekenissen van de connectieven delen, ondersteunt een bewijs-theoretisch standpunt van logisch pluralisme waarbij verschillende logica's dezelfde betekenis van de connectieven kunnen delen ondanks verschillende aangewezen waarden of geldigheidsvoorwaarden.
3. Pad naar Automatisering: Door het succesvol in kaart brengen van 3-dimensionale calculi naar I-bS, legt het artikel de basis voor de integratie van I-bS in MUltlog. Het uiteindelijke doel is de geautomatiseerde generatie van semantische clausules voor elke eindwaardige logica. De auteur merkt op dat hoewel het huidige werk een handmatige casestudy is, het raamwerk is ontworpen om computationeel geïmplementeerd te worden, wat potentieel de geautomatiseerde generatie van bewijs-theoretische semantiek voor willekeurige meerwaardige logica's mogelijk maakt.

De auteur blijft bescheiden over de directe automatisering van het gehele proces en erkent dat het genereren van de noodzakelijke definiebaarheidsbewijzen voor willekeurige $n$-dimensionale calculi een computationele uitdaging blijft, hoewel het theoretische raamwerk nu aanwezig is.