Mostrar código-fonte de 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 [[Lógica de primeira ordem|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 &#x3D5; para a sua negação dupla {{Math|¬¬''&#x03D5;''}}.

O teorema de Glivenko determina:
: Se ''&#x3D5;'' é uma fórmula proposicional, então ''&#x3D5;'' é uma tautologia clássica [[se e somente se]] ¬¬''&#x3D5;'' é 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 ''&#x3D5;'' uma fórmula proposicional, então ''T'' ⊢ ''&#x3D5;'' na lógica clássica se e somente se ''T*'' ⊢ ¬¬''&#x3D5;'' 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 &#x3D5; em uma língua de primeira ordem outra fórmula &#x3D5;<sup>N</sup>, que é definida indutivamente:
* Se <math alt="ϕ">\phi</math> é atômica, então <math alt="ϕ">\phi^N</math> é <math alt="¬¬ϕ">\neg\neg\phi</math>
* <math alt="(ϕ ∧ θ)">(\phi \land \theta)^N</math> é <math>\phi^N \land \theta^N</math>
* <math alt="(ϕ ∨ θ)">(\phi \lor \theta)^N</math> é <math>\mbox{¬}(\mbox{¬}\phi^N \lor \mbox{¬}\theta^N)</math>
* <math alt="(ϕ → θ)">(\phi \rightarrow \theta)^N</math> é <math>\phi^N \rightarrow \theta^N</math>
* <math alt="(¬ϕ)">(\mbox{¬}\phi)^N
</math> é <math>\mbox{¬}\phi^N</math>
* <math alt="(∀''x'' ϕ)">(\forall x\phi)^N</math> é <math>\forall x\phi^N</math>
* <math alt="(∃''x'' ϕ)">(\exists x\phi)^N</math> é <math>\mbox{¬}\forall x \mbox{¬}\phi^N</math>  
Observe que &#x3D5;<sup>N</sup> é classicamente equivalente a &#x3D5;.

O teorema fundamental da corretude afirma:<ref>Avigad and Feferman 1998, p. 342; Buss 1998 p. 66</ref>
: Se T é um conjunto de axiomas e &#x3D5; uma fórmula, então T prova &#x3D5; utilizando a lógica clássica se, e somente se, T<sup>N</sup> prova &#x3D5;<sup>N</sup> usando a lógica intuicionista.
Aqui T<sup>N</sup> consiste em traduções de dupla-negação  de fórmulas em T.

Observe que &#x3D5; não precisa implicar sua tradução negativa &#x3D5;<sup>N</sup> na lógica de primeira ordem intuicionista. Troelsta e Van Dalen<ref>Troelsta, van Dalen 1988, Ch. 2, Sec. 3)</ref> 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 lógica|disjunção]] e quantificador existencial para
* {{Math|(''&#x03D5;'' ∨ ''θ'')<sup>''N''</sup>}} é {{Math|¬¬(''&#x03D5;<sup>N</sup>'' ∨ ''θ<sup>N</sup>'')}}
* {{Math|(∃''x &#x03D5;'')<sup>''N''</sup>}} é {{Math|¬¬∃''x &#x03D5;<sup>N</sup>''}}
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 [[Sigekatu Kuroda|Kuroda]]) é construir &#x3D5;<sup>N</sup> a partir de &#x3D5; , colocando ¬¬ antes da fórmula inteira e depois de cada quantificador universal. Observe que esta se reduz à tradução simples ¬¬&#x3D5; se &#x3D5; é proposicional.

Também é possível definir &#x3D5;<sup>N</sup> prefixando-se ¬¬ antes de cada subfórmula de &#x3D5;, tal como é feito por [[Andrei Kolmogorov|Kolmogorov]]. Tal tradução é a contrapartida lógica para a tradução de [[Programação funcional|linguagens funcionais de programação]] do [[continuation-passing style|estilo continuation-passing]] [[Estratégia de avaliação|chamada por nome]]  ao longo das linhas da [[Isomorfismo de Curry-Howard|correspondência Curry–Howard]] entre provas e programas.

== Resultados ==
A tradução da dupla-negação foi usada por Gödel&#x20;(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 &#x3D5; é demonstrável a partir de axiomas da [[Axiomas de Peano|aritmética de Peano]] , então, &#x3D5;<sup>N</sup> é demonstrável a partir de axiomas da [[Aritmética de Heyting|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 {{Math|''&theta;'' &and; ¬''&theta;''}} é interpretada como {{Math|''&theta;<sup>N</sup>'' &and; ¬''&theta;<sup>N</sup>''}}, que ainda é contraditória. Além disso, a prova desta relação é totalmente construtiva, dando um jeito de transformar uma prova de {{Math|''&theta;'' &and; ¬''&theta;''}} na aritmética de Peano em uma prova de {{Math|''&theta;<sup>N</sup>'' &and; ¬''&theta;<sup>N</sup>''}} em aritmética de Heyting. (Combinando a tradução da dupla-negação com a [[Friedman translation|tradução de Friedman]], é possível, na verdade, provar que a aritmética de Peano é [[Hierarquia aritmética|{{Math|Π{{sup sub|0|2}}}}]]-[[conservative extension|conservativa]] em relação à aritmética de Heyting.)

O mapeamento proposicional de &#x3D5; para {{Math|¬¬''&#x03D5;''}} não se estende para uma tradução correta da lógica de primeira ordem, porque {{Math|&forall;''x'' ¬¬''&#x03D5;''(''x'') → ¬¬&forall;''x'' ''&#x03D5;''(''x'')}} não é um teorema da lógica intuicionista de predicados. Isso explica por que &#x3D5;<sup>N</sup> deve ser definida de uma forma mais complicada no caso da primeira ordem.

== Veja também ==
* [[Interpretação Dialectica]]

== Notas ==
<references />
== Referências ==
* J. Avigad e [[Solomon Feferman|S. Feferman]] (1998), [http://www.academia.edu/160338/Godels_Functional_Dialectica_Interpretation "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.&#x20;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.&#x20;34&#x2013;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.&#x20;75&#x2013;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.&#x20;414&#x2013;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 ==
* "[http://plato.stanford.edu/entries/logic-intuitionistic/ A lógica intuicionista]", Enciclopédia de Filosofia de Stanford.
[[Categoria:Intuicionismo]]