Tradução da dupla negação

Na teoria da prova, uma disciplina dentro da lógica matemática, tradução da dupla-negação, às vezes chamada de tradução negativa, é uma abordagem geral para a incorporação da lógica clássica na lógica intuicionista, normalmente através da tradução de fórmulas para fórmulas que são classicamente equivalentes, mas intuicionisticamente não equivalentes. Instâncias específicas da tradução da dupla negação incluem a tradução de Glivenko  para a lógica proposicional, e a tradução Gödel-Gentzen e a tradução Kuroda para a lógica de primeira ordem.

Lógica proposicional

A tradução da dupla-negação mais fácil de descrever vem do teorema de Glivenko, provado por Valery Glivenko em 1929. Ele mapeia cada fórmula clássica ϕ para a sua negação dupla ¬¬ϕ.

O teorema de Glivenko determina:

Se ϕ é uma fórmula proposicional, então ϕ é uma tautologia clássica se e somente se ¬¬ϕ é uma tautologia intuicionista.

O teorema de Glivenko implica a declaração mais geral:

Se T é um conjunto de fórmulas proposicionais, T* um conjunto que consiste em fórmulas duplamente negadas de T, e ϕ uma fórmula proposicional, então T ⊢ ϕ na lógica clássica se e somente se T* ⊢ ¬¬ϕ na lógica intuicionista.

Em particular, um conjunto de fórmulas proposicionais é intuicionisticamente consistente se e somente se ele é classicamente satisfatório.

Lógica de primeira ordem

A tradução de Gödel-Gentzen (em homenagem a Kurt Gödel e Gerhard Gentzen) associa a cada fórmula ϕ em uma língua de primeira ordem outra fórmula ϕ^N, que é definida indutivamente:

• Se $\phi$ é atômica, então $\phi ^{N}$ é $\neg \neg \phi$
• $(\phi \land \theta )^{N}$ é $\phi ^{N}\land \theta ^{N}$
• $(\phi \lor \theta )^{N}$ é ${\mbox{¬}}({\mbox{¬}}\phi ^{N}\lor {\mbox{¬}}\theta ^{N})$
• $(\phi \rightarrow \theta )^{N}$ é $\phi ^{N}\rightarrow \theta ^{N}$
• $({\mbox{¬}}\phi )^{N}$ é ${\mbox{¬}}\phi ^{N}$
• $(\forall x\phi )^{N}$ é $\forall x\phi ^{N}$
• $(\exists x\phi )^{N}$ é ${\mbox{¬}}\forall x{\mbox{¬}}\phi ^{N}$

Observe que ϕ^N é classicamente equivalente a ϕ.

O teorema fundamental da corretude afirma:

Se T é um conjunto de axiomas e ϕ uma fórmula, então T prova ϕ utilizando a lógica clássica se, e somente se, T^N prova ϕ^N usando a lógica intuicionista.

Aqui T^N consiste em traduções de dupla-negação  de fórmulas em T.

Observe que ϕ não precisa implicar sua tradução negativa ϕ^N na lógica de primeira ordem intuicionista. Troelsta e Van Dalen dão uma descrição (devido a Leivant) das fórmulas que implicam a sua tradução de Gödel–Gentzen.

Variantes

Existem várias definições alternativas da tradução negativa. Todas elas são demonstravelmente equivalentes na lógica intuicionista, mas podem ser mais fáceis de aplicar em contextos particulares.

Uma possibilidade é alterar as cláusulas de disjunção e quantificador existencial para

• (ϕ ∨ θ)^N é ¬¬(ϕ^N ∨ θ^N)
• (∃x ϕ)^N é ¬¬∃x ϕ^N

Em seguida, a tradução pode ser sucintamente descrita como: prefixo ¬¬ para cada fórmula atômica, disjunção, e quantificador existencial.

Outra possibilidade (conhecida como tradução de Kuroda) é construir ϕ^N a partir de ϕ , colocando ¬¬ antes da fórmula inteira e depois de cada quantificador universal. Observe que esta se reduz à tradução simples ¬¬ϕ se ϕ é proposicional.

Também é possível definir ϕ^N prefixando-se ¬¬ antes de cada subfórmula de ϕ, tal como é feito por Kolmogorov. Tal tradução é a contrapartida lógica para a tradução de linguagens funcionais de programação do estilo continuation-passing chamada por nome  ao longo das linhas da correspondência Curry–Howard entre provas e programas.

Resultados

A tradução da dupla-negação foi usada por Gödel (1933) para estudar a relação entre as teorias clássica e intuicionista para os números naturais ("aritmética"). Ele obtém o seguinte resultado:

Se uma fórmula ϕ é demonstrável a partir de axiomas da aritmética de Peano , então, ϕ^N é demonstrável a partir de axiomas da aritmética intuicionista de Heyting.

Este resultado mostra que, se a aritmética de Heyting é consistente, então a aritmética de Peano também é. Isto é porque uma fórmula contraditória θ ∧ ¬θ é interpretada como θ^N ∧ ¬θ^N, que ainda é contraditória. Além disso, a prova desta relação é totalmente construtiva, dando um jeito de transformar uma prova de θ ∧ ¬θ na aritmética de Peano em uma prova de θ^N ∧ ¬θ^N em aritmética de Heyting. (Combinando a tradução da dupla-negação com a tradução de Friedman, é possível, na verdade, provar que a aritmética de Peano é Π ⁰₂ -conservativa em relação à aritmética de Heyting.)

O mapeamento proposicional de ϕ para ¬¬ϕ não se estende para uma tradução correta da lógica de primeira ordem, porque ∀x ¬¬ϕ(x) → ¬¬∀x ϕ(x) não é um teorema da lógica intuicionista de predicados. Isso explica por que ϕ^N deve ser definida de uma forma mais complicada no caso da primeira ordem.

Veja também

• Interpretação Dialectica

Referências

• J. Avigad e S. Feferman (1998), "Gödel Funcional ("Dialectica" Interpretação", Manual da Teoria de Prova'', S. Buss, ed. Elsevier. ISBN 0-444-89840-9
• S. Buss (1998), "Introdução à Teoria de Prova", Manual de Prova de Teoria, S. Buss, ed. Elsevier. ISBN 0-444-89840-9
• G. Gentzen (1936), "Die Widerspruchfreiheit der reinen Zahlentheorie", Mathematische Annalen, v. 112, p. 493-565 (alemão). Reimpresso em tradução para o inglês como "A consistência da aritmética" em The collected papers of Gerhard Gentzen, M. E. Szabo, ed.
• V. Glivenko (1929), Sur quelques points de la logique de M. Brouwer, Bull. Soc. Matemática. Belg. 15, 183-188
• K. Gödel (1933), "Zur intuitionistischen Arithmetik und Zahlentheorie", Ergebnisse eines mathematischen Kolloquiums, v. 4, pp. 34–38 (alemão). Reimpresso em tradução para o inglês como "intuicionista aritmética e teoria dos números" na A Indecidíveis, M. Davis, ed. pp. 75–81.
• A. N. Kolmogorov (1925), "O príncipe tertium non datur" (russo). Reimpresso em tradução para o inglês como "No princípio dos excluídos por meio" De Frege para Gödel, van Heijenoort, ed. pp. 414–447.
• A. S. Troelsta (1977), "Aspectos da Matemática Construtiva", Handbook of Mathematical Logic", J. Barwise, ed. North-Holland. ISBN 0-7204-2285-X
• A. S. Troelsta e D. van Dalen (1988), o Construtivismo em Matemática. Uma Introdução, volumes 121, 123 de Estudos em Lógica e Fundamentos da Matemática, Norte–Holland.

Ligações externas

• "A lógica intuicionista", Enciclopédia de Filosofia de Stanford.