Technisch Overzicht: Inferentie-Gedrag Semantiek voor Alle∗-Connectieven in Twee-Dimensionale Sequentcalculi

1. Probleemstelling

Het artikel behandelt een centrale uitdaging binnen de Bewijs-Theoretische Semantiek (P-tS): hoe men betekenis-invariante semantische verklaringen voor logische connectieven kan bieden over verschillende logische systemen heen (bijv. klassieke, intuïtionistische, lineaire en dual-intuïtionistische logica's). Traditionele benaderingen, zoals Model-Theoretische Semantiek (M-tS) en Base-Extensie Semantiek (B-eS), lijden vaak aan "globalisme", waarbij het veranderen van de logica noodzakelijkerwijs de betekenis van connectieven verandert (bijv. de klassieke 'en' versus de intuïtionistische 'en'). Dit leidt tot een situatie waarin logische meningsverschillen worden gereduceerd tot loutere communicatieproblemen door verschillende definities, in plaats van substantiële meningsverschillen over gedeelde concepten.

De specifieke kwestie die dit artikel aanpakt, is het gebrek aan een systematische, formele implementatie van Inferentie-Gedrag Semantiek (I-bS), een recente benadering voorgesteld door Nagler [Nag26]. Ho ben I-bS een veelbelovend kader biedt om het "minimale inferentiegedrag" van een connectief te isoleren om de betekenis ervan te definiëren, mistte het voorheen een uitgebreide technische beoordeling over de ruimte van mogelijke verbindingsregels. Het doel van het artikel is om I-bS te valideren door het toe te passen op een enorme, ongestructureerde verzameling kandidaat-connectieven om te bepalen welke, zo ja welke, een onderscheidende, minimale betekenis bezitten die onafhankelijk is van specifieke structurele regels (zoals verzwakking of contractie).

2. Methodologie

De studie hanteert een rigoureuze, datagedreven benadering om de "betekenis" van connectieven te meten op basis van hun inferentiële gebruik in een minimale setting.

2.1 Object van Onderzoek: Alle∗-Connectieven

De auteurs definiëren de reikwijdte van het onderzoek als alle∗-connectieven: operationele regelparen die formuleerbaar zijn in twee-dimensionale sequentcalculi onder de volgende beperkingen:

• Operationele Regels: Moeten afzonderlijk, expliciet en symmetrisch zijn (Definitie 3).
• Beperkingen: Maximaal twee premissen-sequenten en maximaal twee actieve formules per regel.
• Totale Ruimte: Dit levert exact 10.816 syntactisch unieke regelparen op (combinaties van premissen-vormen en actieve formuleposities).

2.2 Testomgeving: Minimale Afleidbaarheidrelatie

Om de betekenis van een connectief te isoleren van de structurele kenmerken van specifieke logica's, maken de auteurs gebruik van een minimale achtergrondcalculus bestaande uit:

• Identiteit ($Id_{pr}$): Beperkt tot primitieve formules alleen.
• Cut ($Cut_{cd}$): Een context-differentierende Cut-regel.
• Structurele Aannames: De calculus gaat uit van Exchange (multisets) maar sluit Weakening en Contraction uit. Dit vertegenwoordigt de "substructurele kern" die gemeenschappelijk is voor veel logica's.

2.3 Meetinstrument: Inferentiegedrag

De kernmetriek is inferentiegedrag, gedefinieerd als het syntactische patroon dat een connectief vertoont wanneer de definieerbaarheid ervan wordt bewezen binnen de minimale calculus.

• Definieerbaarheidscriteria: Volgens Belnap [Bel62] is een connectief definieerbaar als de toevoeging ervan aan de calculus resulteert in een conservatieve extensie (geen nieuwe stellingen zonder het connectief) en uniciteit (het connectief is uniek bepaald tot isomorfie).
• Semantische Clausule: De "betekenis" van een connectief wordt geïdentificeerd als zijn minimale operationele regelpaar dat het minimale inferentiegedragsprofiel oplevert (de kortste lijst van componentposities die bezet worden door het connectief en zijn actieve formules tijdens een bewijs van definieerbaarheid).

2.4 Datageneratie en Analyse

De auteurs filteren de 10.816 kandidaten systematisch:

1. Filter 1 (Formuleerbaarheid): Alle 10.816 regelparen.
2. Filter 2 (Conservativiteit): Het bewijzen van Cut-eliminatie voor de positieve gevallen en het construeren van tegenvoorbeelden voor de niet-conservatieve gevallen. Dit reduceert de verzameling tot 376 conservatieve connectieven.
3. Filter 3 (Uniciteit): Het vaststellen van horizontale en verticale interafleidbaarheid. Dit reduceert de verzameling verder tot 150 uniek definieerbare connectieven.
4. Minimaliteitsanalyse: Onder de 150 definieerbare connectieven onderscheiden de auteurs tussen "minimale" connectieven en "bloatnectieven" (equivalente connectieven met syntactische redundanties). Door criteria voor premissetype-minimaliteit toe te passen (laagste cardinaliteit van premissen-sequenten), isoleren zij de werkelijk minimale semantische clausules.

3. Belangrijkste Bijdragen en Resultaten

3.1 Identificatie van 21 Minimaal Betekenisvolle Connectieven

Het primaire resultaat is de identificatie van exact 21 minimaal betekenisvolle connectieven. Deze komen overeen met bekende logische constanten en hun conversen/inversen, maar met precieze onderscheidingen tussen additieve (rooster) en multiplicatieve (groep) versies:

• Nul-ary: Bottom ($\bot$) en Top ($\top$).
• Unair: Twee vormen van negatie (Intuïtionistische $\neg$ en Dual-Intuïtionistische $\sim$), en een "triviale" converse negatie.
• Binair:
  • Conjunctie: Additieve ($\sqcap$) en Multiplicatieve ($\otimes$).
  • Disjunctie: Additieve ($\sqcup$) en Multiplicatieve ($\oplus$).
  • Implicatie: Additieve Rechts ($\rightsquigarrow$), Multiplicatieve Rechts ($\to$), Additieve Links, en Multiplicatieve Links.
  • Conversen en Inversen: Elk van de bovenstaande heeft onderscheidende semantische clausules voor hun conversen (het wisselen van componenten) en inversen.

3.2 Semantische Clausules en Kaders

Het artikel biedt expliciete semantische clausules (minimale regelparen) voor elk van de 21 connectieven. Cruciaal is dat het aantoont dat deze betekenissen logica-onafhankelijk zijn. Bijvoorbeeld, de semantische clausule voor multiplicatieve conjunctie ($\otimes$) is hetzelfde of deze nu voorkomt in Lineaire Logica, Klassieke Logica of Intuïtionistische Logica. De verschillen in hoe deze connectieven zich gedragen in volledige logica's (bijv. de equivalentie van $\otimes$ en $\sqcap$ in Klassieke Logica) worden toegeschreven aan structurele middelen (zoals Contraction en Weakening) in plaats van een verandering in de kernbetekenis van het connectief.

3.3 Semantische Interrelaties over Logica's

De studie brengt de semantische compatibiliteit van deze 21 connectieven in kaart over diverse logica's:

• Klassieke Logica (LK): Conflateert de additieve en multiplicatieve versies van conjunctie, disjunctie en implicatie. Het conflateert ook de twee vormen van negatie.
• Intuïtionistische Logica (LJ): Is compatibel met de additieve versies van conjunctie en disjunctie, en de "rechter" implicatie, maar vangt slechts de helft van de klassieke negatie op (specifiek $\neg_{min}$, exclusief $\sim_{min}$).
• Dual-Intuïtionistische Logica (LDJ): Vangt de andere helft van de klassieke negatie op ($\sim_{min}$) en de dualen van de andere connectieven.
• Lineaire Logica (LL): Maakt onderscheid tussen alle 21 connectieven en behandelt hen als semantisch verschillend.

3.4 Validatie van I-bS

Het artikel claimt de validatie van het Inference-Behaviour Semantics kader door aan te tonen dat wanneer het wordt toegepast op een blinde, uitputtende zoektocht naar mogelijke regels zonder bias naar een specifieke logica, de theorie van nature convergeert op exact de standaard connectieven die in gevestigde logische systemen worden gevonden. Het feit dat de "ruis" (de andere 10.795 regelparen) wordt weggefilterd als niet-definieerbaar of niet-minimaal, dient als een "sanity check" voor de theorie.

4. Betekenis en Claims

Het artikel positioneert zijn bevindingen als een verificatie van het Inference-Behaviour Semantics kader. De betekenis ligt in:

1. Logica-Onafhankelijkheid: Het biedt een methode om de betekenis van connectieven te definiëren die invariant zijn over verschillende logica's. Het veranderen van de logica (bijv. het toevoegen van Weakening) verandert niet de betekenis van het connectief; het verandert enkel de structurele context waarin het connectief opereert.
2. Resolutie van Betekenisverandering: Het biedt een semantische verklaring voor waarom klassieke en intuïtionistische logica's ogenschijnlijk van mening verschillen. Ze verschillen niet noodzakelijkerwijs van mening over de betekenis van "en" of "of"; eerder verschillen ze in welke minimale connectieven zij toestaan te interageren en welke structurele regels zij toestaan. Bijvoorbeeld, klassieke "en" is een conflatie van twee verschillende minimale betekenissen ($\otimes$ en $\sqcap$), terwijl intuïtionistische "en" strikt $\sqcap$ is.
3. Ontologische Soberheid: De benadering vereist geen externe modellen of bases, maar vertrouwt uitsluitend op de substructurele kern van het bewijssysteem.
4. Uitputtendheid: Door de gehele ruimte van formuleerbare regels onder de gegeven beperkingen te dekken, claimt het artikel een volledige taxonomie van minimale betekenisvolle connectieven in twee-dimensionale sequentcalculi te hebben geleverd.

De auteurs blijven bescheiden over de reikwijdte en merken op dat de resultaten relatief zijn aan de specifieke beperkingen (twee premissen, twee actieve formules, specifieke minimale calculus) en dat toekomstig werk mogelijk meer-dimensionale calculi, kwantificatie of alternatieve minimale afleidbaarheidrelaties kan verkennen. Echter, binnen de gedefinieerde scope, stelt het artikel dat I-bS erin slaagt de primitieve betekenissen van logische connectieven te isoleren.