Glivenko's theorems from an ecumenical perspective

Résumé technique : Les théorèmes de Glivenko d'un point de vue œcuménique

Énoncé du problème
L'article aborde la relation fondamentale entre la logique classique (CL) et la logique intuitionniste (IL), en revisitant spécifiquement les théorèmes de Glivenko. Ces théorèmes établissent que si une formule est prouvable classiquement, sa double négation est prouvable intuitionnistement, et si une formule négative est prouvable classiquement, elle l'est également intuitionnistement. Bien que ces résultats soient bien compris dans le contexte de systèmes logiques séparés, l'article examine comment ces relations se manifestent au sein de systèmes œcuméniques. Les systèmes œcuméniques sont des cadres unifiés où les logiques classique et intuitionniste coexistent pacifiquement sans s'effondrer l'une dans l'autre, souvent en distinguant des opérateurs (par exemple, la disjonction classique par rapport à la disjonction intuitionniste) ou en étiquetant les formules pour indiquer leur nature logique. Le problème central consiste à déterminer comment les résultats de type Glivenko se traduisent lorsque le raisonnement classique et intuitionniste sont intégrés dans un seul système déductif, et à analyser les différences entre deux approches principales de l'œcuménisme : l'approche « inférentialiste » (distinguant les opérateurs) et l'approche « généraliste » (distinguant les formules via des étiquettes).

Méthodologie
Les auteurs emploient une analyse proof-théorique utilisant des systèmes de déduction naturelle. Ils examinent trois cadres œcuméniques spécifiques :

1. NE (Système de Prawitz) : Une approche inférentialiste où les logiciens classique et intuitionniste partagent des opérateurs neutres (conjonction, quantificateur universel, négation, absurdité) mais possèdent des versions distinctes des opérateurs non neutres (implication, disjonction, quantificateur existentiel).
2. ECI (Système de Barroso-Nascimento) : Une approche généraliste où un seul ensemble d'opérateurs est utilisé, mais les formules sont étiquetées avec une constante $c$ (par exemple, $A^c$) pour désigner un comportement classique. Ce système est construit sur la déduction naturelle intuitionniste augmentée de règles d'introduction ($I_C$) et d'élimination ($E_C$) pour l'étiquette.
3. NEK (Système inspiré par Krauss) : Une variante du système de Prawitz qui inclut une conjonction classique ($\land_c$) et un quantificateur universel classique ($\forall_c$), basée sur des travaux inédits de Krauss.

La méthodologie comprend :

• La définition de théorèmes de type Glivenko internes à ces systèmes (reliant les opérateurs/formules classiques à leurs contreparties intuitionnistes).
• La construction de déductions pour prouver ces relations internes.
• La définition de fonctions de traduction ($t_{ECI}$ et $t_{NEK}$) pour mapper les formules entre les systèmes.
• L'investigation de l'équivalence déductive de ces systèmes, en particulier dans le fragment propositionnel par rapport au fragment du premier ordre impliquant la quantification universelle.

Contributions et résultats clés

1. Théorèmes de Glivenko internes dans NE :
   Les auteurs démontrent que dans le système de Prawitz (NE), où des opérateurs distincts existent, une relation de type « Glivenko » vaut internement. Pour toute formule $C$ dont l'opérateur principal est classique, $C \vdash_{NE} \neg\neg C^*$, où $C^*$ est la formule avec l'opérateur classique remplacé par sa contrepartie intuitionniste. Cela s'applique à la disjonction classique ($\lor_c$), à l'implication ($\to_c$) et à la quantification existentielle ($\exists_c$). Un résultat correspondant vaut pour les formules négatives : $\neg C \vdash_{NE} \neg C^*$.

2. Trivialité des résultats de Glivenko dans ECI :
   Dans le système ECI, la relation entre une formule classique $A^c$ et sa contrepartie intuitionniste est structurellement triviale. Les règles du système produisent immédiatement $A^c \vdash_{ECI} \neg\neg A$. Par conséquent, la traduction $t_{ECI}$, qui mappe $A^c$ vers $\neg\neg A$, réduit le problème de la normalisation dans ECI à celui de la logique intuitionniste. Les auteurs montrent que, bien que cette traduction fonctionne pour la logique propositionnelle, elle obscurcit l'emplacement spécifique du raisonnement classique dans une déduction, à moins que la déduction ne soit soigneusement reconstruite pour suivre la « nature classique » des formules déduites.

3. Le cas de la conjonction classique et de NEK :
   L'article introduit NEK, qui ajoute la conjonction classique ($\land_c$) au système de Prawitz. Les auteurs prouvent que $\land_c$ satisfait les théorèmes de Glivenko internes ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). Ils montrent également que dans le fragment propositionnel (ou la logique du premier ordre sans quantificateurs universels), NEK et ECI sont déductivement équivalents. Cette équivalence est établie via une traduction $t_{NEK}$ qui mappe les opérateurs classiques dans NEK vers des formules étiquetées dans ECI.

4. La divergence avec la quantification universelle :
   Un résultat critique est l'échec de l'équivalence déductive entre NEK et ECI lorsque la quantification universelle est introduite.

   • Dans NEK, le quantificateur universel classique $\forall_c$ est défini par des règles harmoniques avec la logique intuitionniste. Cependant, le théorème de Glivenko interne échoue pour $\forall_c$ : $\vdash_{NEK} \forall_c x A(x)$ n'implique pas $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
   • Dans ECI, la formule étiquetée $(\forall x A(x))^c$ se comporte différemment. En raison des règles du système, $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ vaut.
   • Les auteurs expliquent cette divergence : Dans NEK, $\forall_c x A(x)$ est interprété comme $\neg \exists x \neg A(x)$, tandis que dans ECI, $(\forall x A(x))^c$ est effectivement interprété comme $\neg\neg \forall x A(x)$. Ces deux interprétations ne sont pas équivalentes intuitionnistement. L'article soutient que la « trivialité » des résultats de Glivenko dans ECI pour les formules universelles découle du fait que l'étiquette $c$ force une interprétation par double négation qui ne correspond pas au comportement sémantique du quantificateur universel classique dans l'approche inférentialiste.

Portée et affirmations
L'article affirme que la perspective œcuménique offre une compréhension plus profonde de l'interaction entre le raisonnement classique et intuitionniste. En comparant les approches « inférentialiste » (NE/NEK) et « généraliste » (ECI), les auteurs mettent en évidence une différence conceptuelle subtile mais significative :

• Les systèmes inférentialistes (Prawitz/Krauss) changent directement le sens des connecteurs en fournissant des règles d'introduction et d'élimination distinctes pour les opérateurs classiques.
• Les systèmes généralistes (ECI) changent le niveau de preuve, dotant la logique intuitionniste de moyens classiques de preuve (via l'étiquette $c$) qui altèrent indirectement le sens des opérateurs.

Les auteurs concluent que, bien que ces approches soient équivalentes en logique propositionnelle, elles divergent en présence de quantification universelle. Cette divergence suggère que le choix du cadre œcuménique n'est pas une simple préférence notationnelle, mais affecte le comportement logique des quantificateurs. L'article postule que la perspective œcuménique aide à identifier exactement où le raisonnement classique est nécessaire et clarifie que les principes classiques et intuitionnistes peuvent coexister sans que l'un ne s'effondre dans l'autre, à condition que le système soit construit avec attention à ces principes inférentiels distincts.