Interpretação Dialectica

Em teoria da prova, a Interpretação Dialectica é uma interpretação de prova da aritmética intuicionística (Aritmética de Heyting) em uma extensão de tipos finitos da aritmética primitiva recursiva, o chamado Sistema T. Foi desenvolvida por Kurt Gödel para fornecer uma prova de consistência da aritmética. O nome da interpretação vem do periódico Dialectica, onde o trabalho de Gödel foi publicado em uma edição especial dedicada a Paul Bernays em seu 70º aniversário.

Motivação

Através da tradução negativa de Gödel–Gentzen, a consistência da Aritmética de Peano clássica já havia sido reduzida à consistência da Aritmética de Heyting. A motivação de Gödel para desenvolver a interpretação Dialectica foi para obter uma prova de consistência relativa para a aritmética de Heyting (e conseqüentemente para a Aritmética de Peano).

Interpretação Dialectica da lógica intuicionística

A interpretação tem dois componentes: uma tradução de fórmula e uma tradução de prova. A tradução de fórmula descreve como cada fórmula $A$ da aritmética de Heyting é mapeada para uma fórmula sem quantificadores $A_{D}(x;y)$ do sistema T, onde $x$ e $y$ são tuplas de novas variáveis (não livres em $A$). Intuitivamente, $A$ é interpretada como $\exists x\forall yA_{D}(x;y)$. A tradução de prova mostra como uma prova de $A$ tem informação suficiente para testemunhar a interpretação de $A$, i.e. a prova de $A$ pode ser convertida em um termo fechado $t$ e uma prova de $A_{D}(t;y)$ no sistema T.

Tradução de fórmula

A fórmula sem quantificadores $A_{D}(x;y)$ é definida indutivamente na seguinte estrutura lógica de $A$, onde $P$ é uma fórmula atômica:

${\begin{array}{lcl}(P)_{D}&\equiv &P\\(A\wedge B)_{D}(x,v;y,w)&\equiv &A_{D}(x;y)\wedge B_{D}(v;w)\\(A\vee B)_{D}(x,v,z;y,w)&\equiv &(z=0\rightarrow A_{D}(x;y))\wedge (z\neq 0\to B_{D}(v;w))\\(A\rightarrow B)_{D}(f,g;x,w)&\equiv &A_{D}(x;fxw)\rightarrow B_{D}(gx;w)\\(\exists zA)_{D}(x,z;y)&\equiv &A_{D}(x;y)\\(\forall zA)_{D}(f;y,z)&\equiv &A_{D}(fz;y)\end{array}}$

Tradução de prova (correção)

A interpretação de fórmula é tal que sempre que $A$ é demonstrável na aritmética de Heyting então existe uma sequência de termos fechados $t$ tal que $A_{D}(t;y)$ é demonstrável no sistema T. A sequência de termos $t$ e a prova de $A_{D}(t;y)$ são construidos a partir da prova de $A$ na aritmética de Heyting. A construção de $t$ é bastante simples, exceto pelo axioma de contração $A\rightarrow A\wedge A$, o qual requer a suposição de que fórmulas sem quantificadores são decidíveis (Decidibilidade).

Princípios da caracterização

Também foi mostrado que a aritmética de Heyting estendida com os seguintes princípios

• Axioma da escolha
• Princípio de Markov
• Independência de premissa para fórmulas universais

são necessários e suficientes para caracterizar as fórmulas de HA, as quais são interpretáveis pela interpretação Dialectica.

Extensões da interpretação básica

A interpretação Dialectica básica da lógica intuicionista foi estendida em vários sistemas mais fortes. Intuitivamente, interpretação Dialectica pode ser aplicada a um desses sistemas, contanto que a interpretação Dialectica deste princípio extra pode ser testemunhada por termos no sistema T (ou em uma extensão do sistema T).

Indução

Dados os teoremas da incompletude de Gödel (que implicam que a consistência de PA não pode ser provada por Finitismo) é razoável esperar que o sistema T deve conter construções não-finitistas. Realmente é este o caso. As construções não-finitistas aparecem na interpretação da indução matemática. Para dar uma interpretação Dialectica de indução, Gödel faz uso dos funcionais recursivos primitivos, que são funções de alta ordem com descrições recursivas primitivas.

Lógica clássica

Fórmulas e provas na aritmética clássica também podem receber uma interpretação Dialectica ao embutí-las na aritmética de Heyting seguido da interpretação Dialectica da aritmética de Heyting. Shoenfield, em seu livro, combina a tradução negativa e a interpretação Dialectica em uma única interpretação da aritmética clássica.

Compreensão

Em 1962 Spector estendeu a interpretação Dialectica de Gödel da aritmética em uma análise matemática completa, ao mostrar como o esquema de escolhas contáveis pode ser dado uma interpretação Dialectica ao estender-se o sistema T com recursão bar.

Interpretação Dialectica da lógica linear

A interpretação Dialectica tem sido usada para construir um modelo do refinamento de Girard da lógica intuicionística conhecido como lógica linear, através dos espaços da Dialectica. Visto que a lógica linear é um refinamento da lógica intuicionística, a interpretação Dialectica da lógica linear pode ser vista como um refinamento da interpretação Dialectica da lógica intuicionística.

Apesar da interpretação linear no artigo de Shirarata validar a regra do enfraquecimento (na verdade é uma interpretação da lógica afim), a interpretação do espaços da Dialectica de Paiva não valida enfraquecimento para fórmulas arbitrárias.

Variantes da Interpretação Dialectica

Várias variantes da Interpretação Dialectica foram propostas. A variante de Diller-Nahm (para evitar o problema da contração), a monotônica de Kohlenbach e as interpretações limitadas de Ferreira-Oliva (para interpretar o lema fraco de König) são as mais notáveis. Tratamentos abrangentes da interpretação podem ser encontrados em, e