Glivenko's theorems from an ecumenical perspective

Resumen Técnico: Los Teoremas de Glivenko desde una Perspectiva Ecuménica

Planteamiento del Problema
El artículo aborda la relación fundamental entre la lógica clásica (CL) y la lógica intuicionista (IL), revisitando específicamente los teoremas de Glivenko. Estos teoremas establecen que si una fórmula es demostrable clásicamente, su doble negación es demostrable intuicionísticamente, y si una fórmula negada es demostrable clásicamente, también lo es intuicionísticamente. Aunque estos resultados son bien comprendidos en el contexto de sistemas lógicos separados, el artículo investiga cómo estas relaciones se manifiestan dentro de sistemas ecuménicos. Los sistemas ecuménicos son marcos unificados donde la lógica clásica y la intuicionista coexisten pacíficamente sin colapsar la una en la otra, a menudo distinguiendo operadores (por ejemplo, disyunción clásica frente a intuicionista) o etiquetando fórmulas para indicar su naturaleza lógica. El problema central es determinar cómo se traducen los resultados de tipo Glivenko cuando el razonamiento clásico e intuicionista se integran en un único sistema deductivo, y analizar las diferencias entre dos enfoques principales del ecumenismo: el enfoque "inferencialista" (distinguiendo operadores) y el enfoque "generalista" (distinguiendo fórmulas mediante etiquetas).

Metodología
Los autores emplean un análisis demostrativo-teórico utilizando sistemas de Deducción Natural. Examinan tres marcos ecuménicos específicos:

1. NE (Sistema de Prawitz): Un enfoque inferencialista donde los lógicos clásicos e intuicionistas comparten operadores neutrales (conjunción, cuantificador universal, negación, absurdo) pero poseen versiones distintas de operadores no neutrales (implicación, disyunción, cuantificador existencial).
2. ECI (Sistema de Barroso-Nascimento): Un enfoque generalista donde se utiliza un único conjunto de operadores, pero las fórmulas se etiquetan con una constante $c$ (por ejemplo, $A^c$) para denotar comportamiento clásico. Este sistema se construye sobre la deducción natural intuicionista, aumentada con reglas de introducción ($I_C$) y eliminación ($E_C$) para la etiqueta.
3. NEK (Sistema inspirado en Krauss): Una variación del sistema de Prawitz que incluye una conjunción clásica ($\land_c$) y un cuantificador universal clásico ($\forall_c$), basándose en trabajo inédito de Krauss.

La metodología implica:

• Definir teoremas de tipo Glivenko internos dentro de estos sistemas (relacionando operadores/fórmulas clásicos con sus contrapartes intuicionistas).
• Construir derivaciones para probar estas relaciones internas.
• Definir funciones de traducción ($t_{ECI}$ y $t_{NEK}$) para mapear fórmulas entre sistemas.
• Investigar la equivalencia deductiva de estos sistemas, particularmente en el fragmento proposicional versus el fragmento de primer orden que involucra cuantificación universal.

Contribuciones y Resultados Clave

1. Teoremas de Glivenko Internos en NE:
   Los autores demuestran que en el sistema de Prawitz (NE), donde existen operadores distintos, se cumple internamente una relación de "tipo Glivenko". Para cualquier fórmula $C$ donde el operador principal es clásico, $C \vdash_{NE} \neg\neg C^*$, donde $C^*$ es la fórmula con el operador clásico reemplazado por su contraparte intuicionista. Esto aplica a la disyunción clásica ($\lor_c$), la implicación ($\to_c$) y la cuantificación existencial ($\exists_c$). Un resultado correspondiente se cumple para fórmulas negadas: $\neg C \vdash_{NE} \neg C^*$.

2. Trivialidad de los Resultados de Glivenko en ECI:
   En el sistema ECI, la relación entre una fórmula clásica $A^c$ y su contraparte intuicionista es estructuralmente trivial. Las reglas del sistema producen inmediatamente $A^c \vdash_{ECI} \neg\neg A$. En consecuencia, la traducción $t_{ECI}$, que mapea $A^c$ a $\neg\neg A$, reduce el problema de la normalización en ECI al de la lógica intuicionista. Los autores muestran que, aunque esta traducción funciona para la lógica proposicional, oscurece la ubicación específica del razonamiento clásico en una derivación a menos que la derivación se reconstruya cuidadosamente para rastrear la "naturaleza clásica" de las fórmulas derivadas.

3. El Caso de la Conjunción Clásica y NEK:
   El artículo introduce NEK, que añade la conjunción clásica ($\land_c$) al sistema de Prawitz. Los autores prueban que $\land_c$ satisface los teoremas de Glivenko internos ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). También muestran que en el fragmento proposicional (o lógica de primer orden sin cuantificadores universales), NEK y ECI son deductivamente equivalentes. Esta equivalencia se establece mediante una traducción $t_{NEK}$ que mapea los operadores clásicos en NEK a fórmulas etiquetadas en ECI.

4. La Divergencia con la Cuantificación Universal:
   Un resultado crítico es el fracaso de la equivalencia deductiva entre NEK y ECI cuando se introduce la cuantificación universal.

   • En NEK, el cuantificador universal clásico $\forall_c$ se define mediante reglas que son armónicas con la lógica intuicionista. Sin embargo, el teorema de Glivenko interno falla para $\forall_c$: $\vdash_{NEK} \forall_c x A(x)$ no implica $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
   • En ECI, la fórmula etiquetada $(\forall x A(x))^c$ se comporta de manera diferente. Debido a las reglas del sistema, $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ se cumple.
   • Los autores explican esta discrepancia: En NEK, $\forall_c x A(x)$ se interpreta como $\neg \exists x \neg A(x)$, mientras que en ECI, $(\forall x A(x))^c$ se interpreta efectivamente como $\neg\neg \forall x A(x)$. Estos no son intuicionísticamente equivalentes. El artículo argumenta que la "trivialidad" de los resultados de Glivenko en ECI para fórmulas universales surge porque la etiqueta $c$ fuerza una interpretación de doble negación que no se alinea con el comportamiento semántico del cuantificador universal clásico en el enfoque inferencialista.

Significado y Afirmaciones
El artículo afirma que la perspectiva ecuménica ofrece una comprensión más profunda de la interacción entre el razonamiento clásico e intuicionista. Al comparar los enfoques "inferencialista" (NE/NEK) y "generalista" (ECI), los autores destacan una diferencia conceptual sutil pero significativa:

• Los sistemas inferencialistas (Prawitz/Krauss) cambian el significado de los conectivos directamente al proporcionar reglas de introducción y eliminación distintas para los operadores clásicos.
• Los sistemas generalistas (ECI) cambian el nivel de prueba, equipando la lógica intuicionista con medios clásicos de prueba (mediante la etiqueta $c$) que alteran indirectamente el significado de los operadores.

Los autores concluyen que, aunque estos enfoques son equivalentes en lógica proposicional, divergen en presencia de cuantificación universal. Esta divergencia sugiere que la elección del marco ecuménico no es meramente una preferencia notacional, sino que afecta el comportamiento lógico de los cuantificadores. El artículo postula que la perspectiva ecuménica ayuda a identificar exactamente dónde es necesario el razonamiento clásico y aclara que los principios clásicos e intuicionistas pueden coexistir sin que uno colapse en el otro, siempre que el sistema se construya prestando atención a estos principios inferenciales distintos.