Classical Logic as Intuitionistic Logic with Duality

Technische Samenvatting: Klassieke Logica als Intuïtionistische Logica met Dualiteit

1. Het Probleem
Het artikel behandelt een fundamentele uitdaging in de betekenistheorie: het bieden van een bewijs-theoretische semantiek (P-tS) voor klassieke logica die voldoet aan anti-realistische (constructivistische) principes zonder te veronderstellen dat het principe van bivalentie of verificatie-transcendente waarheid van toepassing is. Hoewel Sandqvist succesvol een basis-extensie-semantiek (B-eS) heeft ontwikkeld voor intuïtionistische logica (IPL) en een versie voor klassieke logica (CPL), blijven er beperkingen bestaan. Sandquists CPL-semantiek is beperkt tot specifieke connectieven (oorspronkelijk $\to, \bot, \forall$) en steunt op een technisch complexe volledigheidsbewijsvoering waarbij bar-inductie wordt gebruikt. Bovendien worstelen bestaande benaderingen vaak met het constructief behandelen van de volledige propositionele taal (inclusief $\lor$ en $\exists$). De auteurs beogen dit op te lossen door een B-eS aan te bieden voor de volledige klassieke propositionele logica die een elementaire, constructieve volledigheidsbewijsvoering behoudt, waarmee zij het antwoord geven op de uitdaging van Dummett betreffende de verzoening van klassieke inferentie met anti-realistische betekenis.

2. Methodologie en Filosofisch Kader
De auteurs stellen een bilateralistisch kader voor waarin klassieke logica wordt geconceptualiseerd als "Intuïtionistische Logica + Dualiteit". Deze benadering wijkt af van traditionele visies door een onderscheid te maken tussen inhoud en illocutionaire kracht op atomair niveau, terwijl complexe formules worden behandeld als logico-grammaticale structuren in plaats van proposities die zelf kracht bezitten.

• Letterlijke tekens als Proposities: Het systeem introduceert "letterlijke tekens" ($L$) als de enige objecten van assertie en ontkenning. Een inhoud $c$ wordt gekoppeld aan een kracht om een positief letterlijk teken ($c^+$, assertie) of een negatief letterlijk teken ($c^-$, ontkenning) te vormen. Cruciaal is dat dualiteit primair is: $c^+$ en $c^-$ zijn onafhankelijke atomische taalhandelingen, niet gedefinieerd via negatie ($\neg$).
• Logico-Grammaticale Structuren: Complexe formules (bijv. $\phi \land \psi$) zijn geen proposities die geassertieerd of ontkend moeten worden, maar zijn structuren die redeneringen organiseren. Bijgevolg is het bilaterale onderscheid (assertie versus ontkenning) beperkt tot het atomaire niveau (de letterlijke tekens).
• Inferentiële Dualiteit: Klassieke aard wordt hersteld, niet door het toevoegen van een waarheidswaarde-semantiek, maar door het introduceren van twee harmonieuze inferentiële principes op atomair niveau (volgens Negri en von Plato):
  1. Exclusie (EXC1): Het samegelijkertig asserten en ontkennen van dezelfde inhoud leidt tot absurditeit ($l, l^\perp \vdash \bot$).
  2. Casusanalyse (EXC2): Als een conclusie volgt uit zowel een assertie als de duale ontkenning ervan, dan volgt deze direct ($l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$).

3. Technische Ontwikkeling

• Natuurlijke Deductie Systeem ($NK^\pm$): De auteurs definiëren een natuurlijk deductiesysteem dat bestaat uit standaard intuïtionistische regels ($NJ$) plus de atomische dualiteitsregels (EXC1 en EXC2). Dit systeem behandelt letterlijke tekens als de basis, waarbij complexe formules worden opgebouwd via standaard connectieven.
• Basis-Extensie-Semantiek (B-eS):
  • Basissen ($B$): Een basis is een verzameling atomische regels (inferentiële relaties tussen letterlijke tekens).
  • Afleidbaarheid ($\vdash_B$): Afleidbaarheid in een basis wordt inductief gedefinieerd. Het omvat standaard structurele regels (reflexiviteit, toepassing) en de twee nieuwe clausules (exc1, exc2) die dualiteit in de letterlijke tekens afdwingen.
  • Ondersteuning ($\Vdash_B$): De geldigheid van een formule wordt inductief gedefinieerd op de structuur van formules. Cruciaal is dat de ondersteuningsclausules voor connectieven ($\to, \land, \lor$) identiek zijn aan de intuïtionistische definities van Sandqvist. Het klassieke karakter van de semantiek wordt volledig gedragen door de dualiteitsclausules in de definitie van afleidbaarheid in de basis, en niet door de ondersteuningsclausules voor complexe formules.
  • Geldigheid ($\Gamma \Vdash \phi$): Een formule is geldig als deze in elke basis wordt ondersteund.

4. Belangrijkste Resultaten

• Correctheid (Theorem 5.1): Het systeem is correct: als $\Gamma \vdash_{NK^\pm} \phi$, dan $\Gamma \Vdash \phi$. Het bewijs verloopt via inductie op de afleiding, waarbij wordt aangetoond dat de klassieke regels (EXC1, EXC2) de ondersteuning behouden.
• Volledigheid (Theorem 6.2): Het systeem is volledig: als $\Gamma \Vdash \phi$, dan $\Gamma \vdash_{NK^\pm} \phi$.
  • Het bewijs past de elementaire methode van Sandqvist voor intuïtionistische logica aan.
  • Het maakt gebruik van een "simulatiebasis" ($\mathcal{N}$) die is geconstrueerd uit de subformules van de sequentie.
  • Een "afvlakkingsoperator" brengt complexe formules terug naar atomische letterlijke tekens binnen de simulatiebasis.
  • Het "Naturaliserende" lemma toont aan dat afleidbaarheid in de simulatiebasis kan worden terugvertaald naar afleidbaarheid in $NK^\pm$.
  • In tegen tegenstelling tot eerdere benaderingen, behandelt dit bewijs de volledige propositionele taal (inclusief $\lor$) en steunt het op elementaire wiskundige middelen, waarbij bar-inductie of canonieke modellen worden vermeden.

5. Betekenis en Claims
Het artikel beweert een nieuw bewijs-theoretische semantiek voor klassieke logica te bieden die:

1. IPL en CPL verenigt: Het toont aan dat klassieke logica begrepen kan worden als intuïtionistische logica aangevuld met een primair principe van dualiteit op atomair niveau.
2. Respect heeft voor Anti-Realisme: Door waarheidswaarden en bivalentie te vermijden, en door een constructief volledigheidsbewijs te gebruiken, biedt het een werkelijk anti-realistische fundering voor klassieke logica, waarmee het de fundamentele uitdaging van Dummett adresseert.
3. Technische Complexiteit Vereenvoudigt: Door bilateralisme te beperken tot letterlijke tekens en complexe formules als structureel te behandelen, bereiken de auteurs een volledigheidsbewijs van "opvallend elementair karakter", vergelijkbaar met het werk van Sandqvist op intuïtionistische logica, waarmee de technische moeilijkheden van eerdere klassieke B-eS pogingen worden overwonnen.
4. Een Alternatief Biedt voor Modeltheorie: De auteurs positioneren dit werk als een alternatief voor modeltheoretische semantiek en bestaande P-tS benaderingen die steunen op modeltheoretische concepten (zoals die van Makinson of Eckhardt en Pym), met als doel een zuiver inferentialistische account van klassieke logica te vestigen.

Het artikel concludeert dat dit kader de mogelijkheid opent voor een systematische behandeling van klassieke logica, analoog aan de systematische behandeling die al voor intuïtionistische logicaën is gevestigd binnen de P-tS traditie.