Glivenko's theorems from an ecumenical perspective

Resumo Técnico: Teoremas de Glivenko sob uma Perspectiva Ecumênica

Enunciação do Problema
O artigo aborda a relação fundamental entre a lógica clássica (CL) e a lógica intuicionista (IL), revisitando especificamente os teoremas de Glivenko. Estes teoremas estabelecem que, se uma fórmula é demonstrável classicamente, sua dupla negação é demonstrável intuicionisticamente, e se uma fórmula negada é demonstrável classicamente, ela também é demonstrável intuicionisticamente. Embora esses resultados sejam bem compreendidos no contexto de sistemas lógicos separados, o artigo investiga como essas relações se manifestam dentro de sistemas ecumênicos. Sistemas ecumênicos são frameworks unificados onde as lógicas clássica e intuicionista coexistem pacificamente sem colapsar uma na outra, frequentemente distinguindo operadores (por exemplo, disjunção clássica versus intuicionista) ou rotulando fórmulas para indicar sua natureza lógica. O problema central é determinar como resultados do tipo Glivenko se traduzem quando o raciocínio clássico e intuicionista são integrados em um único sistema dedutivo, e analisar as diferenças entre duas abordagens principais ao ecumenismo: a abordagem "inferencialista" (distinguindo operadores) e a abordagem "generalista" (distinguindo fórmulas via rótulos).

Metodologia
Os autores empregam uma análise prova-teórica utilizando sistemas de Dedução Natural. Eles examinam três frameworks ecumênicos específicos:

1. NE (Sistema de Prawitz): Uma abordagem inferencialista onde lógicos clássicos e intuicionistas compartilham operadores neutros (conjunção, quantificador universal, negação, absurdo), mas possuem versões distintas de operadores não neutros (implicação, disjunção, quantificador existencial).
2. ECI (Sistema de Barroso-Nascimento): Uma abordagem generalista onde um único conjunto de operadores é utilizado, mas as fórmulas são rotuladas com uma constante $c$ (por exemplo, $A^c$) para denotar comportamento clássico. Este sistema é construído sobre a dedução natural intuicionista, acrescida de regras de introdução ($I_C$) e eliminação ($E_C$) para o rótulo.
3. NEK (Sistema inspirado em Krauss): Uma variação do sistema de Prawitz que inclui uma conjunção clássica ($\land_c$) e um quantificador universal clássico ($\forall_c$), baseado em trabalho não publicado de Krauss.

A metodologia envolve:

• Definir teoremas internos do tipo Glivenko dentro desses sistemas (relacionando operadores/fórmulas clássicos a seus correspondentes intuicionistas).
• Construir derivações para provar essas relações internas.
• Definir funções de tradução ($t_{ECI}$ e $t_{NEK}$) para mapear fórmulas entre sistemas.
• Investigar a equivalência dedutiva desses sistemas, particularmente no fragmento proposicional versus no fragmento de primeira ordem envolvendo quantificação universal.

Principais Contribuições e Resultados

1. Teoremas Internos de Glivenko no NE:
   Os autores demonstram que, no sistema de Prawitz (NE), onde existem operadores distintos, uma relação "do tipo Glivenko" vale internamente. Para qualquer fórmula $C$ onde o operador principal é clássico, $C \vdash_{NE} \neg\neg C^*$, onde $C^*$ é a fórmula com o operador clássico substituído por seu correspondente intuicionista. Isso aplica-se à disjunção clássica ($\lor_c$), implicação ($\to_c$) e quantificação existencial ($\exists_c$). Um resultado correspondente vale para fórmulas negadas: $\neg C \vdash_{NE} \neg C^*$.

2. Trivialidade dos Resultados de Glivenko no ECI:
   No sistema ECI, a relação entre uma fórmula clássica $A^c$ e seu correspondente intuicionista é estruturalmente trivial. As regras do sistema produzem imediatamente $A^c \vdash_{ECI} \neg\neg A$. Consequentemente, a tradução $t_{ECI}$, que mapeia $A^c$ para $\neg\neg A$, reduz o problema da normalização no ECI ao da lógica intuicionista. Os autores mostram que, embora essa tradução funcione para a lógica proposicional, ela obscurece a localização específica do raciocínio clássico em uma derivação, a menos que a derivação seja cuidadosamente reconstruída para rastrear a "natureza clássica" das fórmulas derivadas.

3. O Caso da Conjunção Clássica e do NEK:
   O artigo introduz o NEK, que adiciona a conjunção clássica ($\land_c$) ao sistema de Prawitz. Os autores provam que $\land_c$ satisfaz os teoremas internos de Glivenko ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$). Eles também mostram que, no fragmento proposicional (ou lógica de primeira ordem sem quantificadores universais), o NEK e o ECI são dedutivamente equivalentes. Essa equivalência é estabelecida via uma tradução $t_{NEK}$ que mapeia operadores clássicos no NEK para fórmulas rotuladas no ECI.

4. A Divergência com a Quantificação Universal:
   Um resultado crítico é o fracasso da equivalência dedutiva entre NEK e ECI quando a quantificação universal é introduzida.

   • No NEK, o quantificador universal clássico $\forall_c$ é definido via regras que são harmônicas com a lógica intuicionista. No entanto, o teorema interno de Glivenko falha para $\forall_c$: $\vdash_{NEK} \forall_c x A(x)$ não implica $\vdash_{NEK} \neg\neg \forall_i x A(x)$.
   • No ECI, a fórmula rotulada $(\forall x A(x))^c$ comporta-se de maneira diferente. Devido às regras do sistema, $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ vale.
   • Os autores explicam essa discrepância: No NEK, $\forall_c x A(x)$ é interpretado como $\neg \exists x \neg A(x)$, enquanto no ECI, $(\forall x A(x))^c$ é efetivamente interpretado como $\neg\neg \forall x A(x)$. Estes não são equivalentes intuicionisticamente. O artigo argumenta que a "trivialidade" dos resultados de Glivenko no ECI para fórmulas universais surge porque o rótulo $c$ força uma interpretação de dupla negação que não se alinha com o comportamento semântico do quantificador universal clássico na abordagem inferencialista.

Significado e Alegações
O artigo alega que a perspectiva ecumênica oferece uma compreensão mais profunda da interação entre o raciocínio clássico e intuicionista. Ao comparar as abordagens "inferencialista" (NE/NEK) e "generalista" (ECI), os autores destacam uma diferença conceitual sutil, mas significativa:

• Sistemas inferencialistas (Prawitz/Krauss) alteram o significado dos conectivos diretamente, fornecendo regras distintas de introdução e eliminação para operadores clássicos.
• Sistemas generalistas (ECI) alteram o nível da prova, equipando a lógica intuicionista com meios clássicos de prova (via o rótulo $c$) que alteram indiretamente o significado dos operadores.

Os autores concluem que, embora essas abordagens sejam equivalentes na lógica proposicional, elas divergem na presença de quantificação universal. Essa divergência sugere que a escolha do framework ecumênico não é meramente uma preferência notacional, mas afeta o comportamento lógico dos quantificadores. O artigo postula que a perspectiva ecumênica ajuda a identificar exatamente onde o raciocínio clássico é necessário e esclarece que os princípios clássicos e intuicionistas podem coexistir sem que um colapse no outro, desde que o sistema seja construído com atenção a esses princípios inferenciais distintos.