Classical Logic as Intuitionistic Logic with Duality

Resumo Técnico: A Lógica Clássica como Lógica Intuicionista com Dualidade

1. O Problema
O artigo aborda um desafio fundamental na teoria do significado: fornecer uma semântica de prova (P-tS) para a lógica clássica que adira a princípios anti-realistas (construtivistas) sem pressupor o princípio da bivalência ou a verdade de transcendência de verificação. Embora Sandqvist tenha desenvolvido com sucesso a semântica de extensão de base (B-eS) para a lógica intuicionista (IPL) e uma versão para a lógica clássica (CPL), permanecem limitações. A semântica CPL de Sandqvist é restrita a conectivos específicos (inicialmente $\to, \bot, \forall$) e depende de uma prova de completude tecnicamente complexa envolvendo indução por barra. Além disso, abordagens existentes frequentemente têm dificuldade em tratar a linguagem proposicional completa (incluindo $\lor$ e $\exists$) de forma construtiva. Os autores visam resolver isso oferecendo uma B-eS para a lógica proposicional clássica completa que mantenha uma prova de completude elementar e construtiva, respondendo assim ao desafio de Dummett sobre a reconciliação da inferência clássica com o significado anti-realista.

2. Metodologia e Estrutura Filosófica
Os autores propõem uma estrutura bilateralista onde a lógica clássica é concebida como "Lógica Intuicionista + Dualidade". Esta abordagem diverge das visões tradicionais ao distinguir entre conteúdo e força ilocucionária no nível atômico, enquanto trata fórmulas complexas como estruturas logico-gramaticais, em vez de proposições que possuem força por si mesmas.

• Literais como Proposições: O sistema introduz "literais" ($L$) como os únicos objetos de asserção e negação. Um conteúdo $c$ é emparelhado com uma força para formar um literal positivo ($c^+$, asserção) ou um literal negativo ($c^-$, negação). Crucialmente, a dualidade é primitiva: $c^+$ e $c^-$ são atos de fala atômicos independentes, não definidos via negação ($\neg$).
• Estruturas Logico-Gramaticais: Fórmulas complexas (ex: $\phi \land \psi$) não são proposições a serem asseridas ou negadas, mas sim estruturas que organizam o raciocínio. Consequentemente, a distinção bilateral (asserção vs. negação) é restrita ao nível atômico (literais).
• Dualidade Inferencial: A classicidade é recuperada não pela adição de uma semântica de valor de verdade, mas pela introdução de dois princípios inferenciais harmoniosos no nível atômico (seguindo Negri e von Plato):
  1. Exclusão (EXC1): Asserir e negar o mesmo conteúdo leva ao absurdo ($l, l^\perp \vdash \bot$).
  2. Análise de Caso (EXC2): Se uma conclusão segue tanto de uma asserção quanto de sua negação dual, ela segue diretamente ($l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$).

3. Desenvolvimento Técnico

• Sistema de Dedução Natural ($NK^\pm$): Os autores definem um sistema de dedução natural composto por regras intuicionistas padrão ($NJ$) mais as regras de dualidade atômica (EXC1 e EXC2). Este sistema trata os literais como a base, com fórmulas complexas construídas via conectivos padrão.
• Semântica de Extensão de Base (B-eS):
  • Bases ($B$): Uma base é um conjunto de regras atômicas (relações inferenciais entre literais).
  • Derivabilidade ($\vdash_B$): A derivabilidade em uma base é definida indutivamente. Inclui regras estruturais padrão (reflexividade, aplicação) e as duas novas cláusulas (exc1, exc2) que impõem a dualidade no nível do literal.
  • Suporte ($\Vdash_B$): A validade de uma fórmula é definida indutivamente sobre a estrutura das fórmulas. Crucialmente, as cláusulas de suporte para os conectivos ($\to, \land, \lor$) são idênticas às definições de Sandqvist para a lógica intuicionista. O caráter clássico da semântica é carregado inteiramente pelas cláusulas de dualidade na definição da derivabilidade na base, não pelas cláusulas de suporte para fórmulas complexas.
  • Validade ($\Gamma \Vdash \phi$): Uma fórmula é válida se for suportada em todas as bases.

4. Resultados Principais

• Correção (Teorema 5.1): O sistema é correto: se $\Gamma \vdash_{NK^\pm} \phi$, então $\Gamma \Vdash \phi$. A prova procede por indução na derivação, mostrando que as regras clássicas (EXC1, EXC2) preservam o suporte.
• Completude (Teorema 6.2): O sistema é completo: se $\Gamma \Vdash \phi$, então $\Gamma \vdash_{NK^\pm} \phi$.
  • A prova adapta o método elementar de Sandqvist para a lógica intuicionista.
  • Utiliza uma "base de simulação" ($\mathcal{N}$) construída a partir dos subfórmulas do sequente.
  • Um operador de "achatamento" mapeia fórmulas complexas para literais atômicos dentro da base de simulação.
  • O lema de "Naturalização" demonstra que a derivabilidade na base de simulação pode ser traduzida de volta para a derivabilidade em $NK^\pm$.
  • Ao contrário de abordagens anteriores, esta prova lida com a linguagem proposicional completa (incluindo $\lor$) e baseia-se em recursos matemáticos elementares, evitando a indução por barra ou modelos canônicos.

5. Significância e Alegações
O artigo afirma fornecer uma nova semântica de prova para a lógica clássica que:

1. Unifica IPL e CPL: Demonstra que a lógica clássica pode ser compreendida como a lógica intuicionista suplementada por um princípio primitivo de dualidade no nível atômico.
2. Respeita o Anti-Realismo: Ao evitar valores de verdade e a bivalência, e ao utilizar uma prova de completude construtiva, oferece um fundamento genuinamente anti-realista para a lógica clássica, abordando o desafio fundacional de Dummett.
3. Simplifica a Complexidade Técnica: Ao restringir o bilateralismo aos literais e tratar as fórmulas complexas como estruturais, os autores alcançam uma prova de completude de "caráter surpreendentemente elementar", comparável ao trabalho de Sandqvist sobre a lógica intuicionista, superando as dificuldades técnicas de tentativas anteriores de B-eS clássica.
4. Oferece uma Alternativa à Teoria dos Modelos: Os autores posicionam este trabalho como uma alternativa à semântica de teoria dos modelos e às abordagens de P-tS existentes que dependem de conceitos de teoria dos modelos (como os de Makinson ou Eckhardt e Pym), visando estabelecer um relato puramente inferencialista da lógica clássica.

O artigo conclui que este arcabouço abre a possibilidade de um tratamento sistemático das lógicas clássicas, análogo ao tratamento sistemático já estabelecido para as lógicas intuicionistas dentro da tradição P-tS.