Glivenko's theorems from an ecumenical perspective

Technische Samenvatting: Glivenko's Stellingen vanuit een Oecumenisch Perspectief

Probleemstelling
Het artikel behandelt de fundamentele relatie tussen klassieke logica (CL) en intuïtionistische logica (IL), met name door Glivenko's stellingen opnieuw te bezien. Deze stellingen stellen dat als een formule klassiek bewijsbaar is, haar dubbele negatie intuïtionistisch bewijsbaar is, en als een genegationeerde formule klassiek bewijsbaar is, deze ook intuïtionistisch bewijsbaar is. Hoewel deze resultaten goed begrepen zijn in de context van gescheiden logische systemen, onderzoekt het artikel hoe deze relaties zich manifesteren binnen oecumenische systemen. Oecumenische systemen zijn verenigde kaders waarin klassieke en intuïtionistische logica vreedzaam naast elkaar bestaan zonder in elkaar op te gaan, vaak door operatoren te onderscheiden (bijvoorbeeld klassieke versus intuïtionistische disjunctie) of door formules te labelen om hun logische aard aan te geven. Het centrale probleem is te bepalen hoe Glivenko-achtige resultaten vertalen wanneer klassiek en intuïtionistisch redeneren geïntegreerd zijn in één deductief systeem, en om de verschillen te analyseren tussen twee primaire benaderingen van oecumenisme: de "inferentialistische" aanpak (het onderscheiden van operatoren) en de "generalistische" aanpak (het onderscheiden van formules via labels).

Methodologie
De auteurs maken gebruik van een bewijstheoretische analyse met behulp van Natural Deduction-systemen. Zij onderzoeken drie specifieke oecumenische kaders:

1. NE (Prawitz's Systeem): Een inferentialistische aanpak waarbij klassieke en intuïtionistische logici neutrale operatoren delen (conunctie, universele kwantificatie, negatie, absurditeit) maar beschikken over distincte versies van niet-neutrale operatoren (implicatie, disjunctie, existentiële kwantificatie).
2. ECI (Barroso-Nascimento's Systeem): Een generalistische aanpak waarbij één set operatoren wordt gebruikt, maar formules worden gelabeld met een constante $c$ (bijvoorbeeld $A^c$) om klassiek gedrag aan te duiden. Dit systeem is gebaseerd op intuïtionistische natural deduction, aangevuld met introductie ($I_C$) en eliminatie ($E_C$) regels voor het label.
3. NEK (Krauss-geïnspireerd Systeem): Een variatie op Prawitz's systeem dat een klassieke conjunctie ($\land_c$) en een klassieke universele kwantificatie ($\forall_c$) omvat, gebaseerd op Krauss's ongepubliceerde werk.

De methodologie omvat:

• Het definiëren van interne Glivenko-achtige stellingen binnen deze systemen (relaties tussen klassieke operatoren/formules en hun intuïtionistische tegenhangers).
• Het construeren van afleidingen om deze interne relaties te bewijzen.
• Het definiëren van vertaalfuncties ($t_{ECI}$ en $t_{NEK}$) om formules tussen systemen te mappen.
• Het onderzoeken van de deductieve equivalentie van deze systemen, met name in het propositional fragment versus het eerste-orde fragment dat universele kwantificatie omvat.

Belangrijkste Bijdragen en Resultaten

1. Interne Glivenko-stellingen in NE:
   De auteurs tonen aan dat in Prawitz's systeem (NE), waar distincte operatoren bestaan, een "Glivenko-achtige" relatie intern geldt. Voor elke formule $C$ waarvan de hoofdoperator klassiek is, geldt $C \vdash_{NE} \neg\neg C^*$, waarbij $C^*$ de formule is waarbij de klassieke operator is vervangen door zijn intuïtionistische tegenhanger. Dit geldt voor klassieke disjunctie ($\lor_c$), implicatie ($\to_c$) en existentiële kwantificatie ($\exists_c$). Een overeenkomstig resultaat geldt voor genegationeerde formules: $\neg C \vdash_{NE} \neg C^*$.

2. Trivialiteit van Glivenko-resultaten in ECI:
   In het ECI-systeem is de relatie tussen een klassieke formule $A^c$ en zijn intuïtionistische tegenhanger structureel triviaal. De regels van het systeem leveren direct $A^c \vdash_{ECI} \neg\neg A$ op. Bijgevolg reduceert de vertaling $t_{ECI}$, die $A^c$ mapt naar $\neg\neg A$, het probleem van normalisatie in ECI tot dat van intuïtionistische logica. De auteurs tonen aan dat hoewel deze vertaling werkt voor propositielogica, deze de specifieke locatie van klassiek redeneren in een afleiding verduistert, tenzij de afleiding zorgvuldig wordt gereconstrueerd om de "klassieke aard" van afgeleide formules bij te houden.

3. Het Geval van Klassieke Conjunctie en NEK:
   Het artikel introduceert NEK, dat klassieke conjunctie ($\land_c$) toevoegt aan Prawitz's systeem. De auteurs bewijzen dat $\land_c$ voldoet aan de interne Glivenko-stellingen ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). Zij tonen ook aan dat in het propositional fragment (of eerste-orde logica zonder universele kwantificatoren) NEK en ECI deductief equivalent zijn. Deze equivalentie wordt vastgesteld via een vertaling $t_{NEK}$ die klassieke operatoren in NEK mapt naar gelabelde formules in ECI.

4. De Divergentie met Universele Kwantificatie:
   Een kritiek resultaat is het falen van deductieve equivalentie tussen NEK en ECI wanneer universele kwantificatie wordt geïntroduceerd.

   • In NEK wordt de klassieke universele kwantificator $\forall_c$ gedefinieerd via regels die harmonisch zijn met intuïtionistische logica. Echter, de interne Glivenko-stelling faalt voor $\forall_c$: $\vdash_{NEK} \forall_c x A(x)$ impliceert niet $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
   • In ECI gedraagt de gelabelde formule $(\forall x A(x))^c$ zich anders. Vanwege de regels van het systeem geldt $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$.
   • De auteurs verklaren deze discrepantie: In NEK wordt $\forall_c x A(x)$ geïnterpreteerd als $\neg \exists x \neg A(x)$, terwijl in ECI $(\forall x A(x))^c$ effectief wordt geïnterpreteerd als $\neg\neg \forall x A(x)$. Deze zijn intuïtionistisch niet equivalent. Het artikel betoogt dat de "trivialiteit" van Glivenko-resultaten in ECI voor universele formules ontstaat omdat het label $c$ een dubbel-negatie-interpretatie forceert die niet overeenkomt met het semantische gedrag van de klassieke universele kwantificator in de inferentialistische aanpak.

Betekenis en Aanspraken
Het artikel claimt dat het oecumenische perspectief een dieper begrip biedt van de wisselwerking tussen klassiek en intuïtionistisch redeneren. Door de "inferentialistische" (NE/NEK) en "generalistische" (ECI) benaderingen te vergelijken, benadrukken de auteurs een subtiel maar significant conceptueel verschil:

• Inferentialistische systemen (Prawitz/Krauss) veranderen de betekenis van connectieven direct door distincte introductie- en eliminatieregels voor klassieke operatoren te bieden.
• Generalistische systemen (ECI) veranderen het niveau van bewijs, waarbij intuïtionistische logica wordt uitgerust met klassieke bewijsmiddelen (via het label $c$) die indirect de betekenis van operatoren veranderen.

De auteurs concluderen dat hoewel deze benaderingen equivalent zijn in propositielogica, ze divergeren in aanwezigheid van universele kwantificatie. Deze divergentie suggereert dat de keuze van oecumenisch kader niet louter een notatievoorkeur is, maar de logische gedrag van kwantificatoren beïnvloedt. Het artikel stelt dat het oecumenische perspectief helpt om precies te identificeren waar klassiek redeneren noodzakelijk is en verduidelijkt dat klassieke en intuïtionistische principes kunnen coëxisteren zonder dat de een in de ander opgaat, mits het systeem is geconstrueerd met aandacht voor deze distincte inferentiële principes.