Interpretação dialética - Dialectica interpretation

Em teoria da prova , a interpretação Dialectica é uma interpretação prova de aritmética intuitionistic ( aritmética de heyting ) para uma extensão finita tipo de aritmética recursiva primitiva , o chamado sistema de T . Ele foi desenvolvido por Kurt Gödel para fornecer uma prova de aritmética de consistência . O nome da interpretação vem do jornal Dialectica , onde o artigo de Gödel foi publicado em uma edição especial de 1958 dedicada a Paul Bernays em seu 70º aniversário.

Motivação

Por meio da tradução negativa de Gödel-Gentzen , a consistência da aritmética clássica de Peano já havia sido reduzida à consistência da aritmética de Heyting intuicionista . A motivação de Gödel para desenvolver a interpretação dialética foi obter uma prova de consistência relativa para a aritmética de Heyting (e, portanto, para a aritmética de Peano).

Interpretação dialética da lógica intuicionista

A interpretação tem dois componentes: uma tradução de fórmula e uma tradução de prova. A tradução da fórmula descreve como cada fórmula da aritmética de Heyting é mapeada para uma fórmula livre de quantificador do sistema T, onde e são tuplas de variáveis ​​novas (não aparecendo livres em ). Intuitivamente, é interpretado como . A tradução da prova mostra como uma prova de tem informações suficientes para testemunhar a interpretação de , ou seja, a prova de pode ser convertida em um termo fechado e uma prova de no sistema T. ${\ displaystyle A}$${\ displaystyle A_ {D} (x; y)}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle \ existe x \ para todos yA_ {D} (x; y)}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle t}$${\ displaystyle A_ {D} (t; y)}$

Tradução de fórmula

A fórmula livre de quantificador é definida indutivamente na estrutura lógica da seguinte forma, onde é uma fórmula atômica: ${\ displaystyle A_ {D} (x; y)}$${\ displaystyle A}$${\ displaystyle P}$

${\ displaystyle {\ 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 \ para B_ {D} (v; w)) \\ (A \ rightarrow B) _ {D} (f, g; x, w) & \ equiv & A_ {D} (x; fxw) \ rightarrow B_ {D} (gx; w) \\ (\ existe 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 (solidez)

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

Princípios de caracterização

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

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

é necessário e suficiente para caracterizar as fórmulas de AH que são interpretáveis ​​pela interpretação da Dialética.

Extensões de interpretação básica

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

Indução

Dado o teorema da incompletude de Gödel (que implica que a consistência de PA não pode ser provada por meios finitísticos ), é razoável esperar que o sistema T deva conter construções não finíticas. Realmente, esse é o caso. As construções não finíticas aparecem na interpretação da indução matemática . Para dar uma interpretação dialética da indução, Gödel faz uso do que é hoje chamado de funcionais recursivos primitivos de Gödel , que são funções de ordem superior com descrições recursivas primitivas.

Lógica clássica

As fórmulas e provas na aritmética clássica também podem receber uma interpretação dialética por meio de uma incorporação inicial na aritmética de Heyting seguida pela interpretação dialética da aritmética de Heyting. Shoenfield , em seu livro, combina a tradução negativa e a interpretação da Dialética em uma única interpretação da aritmética clássica.

Compreensão

Em 1962, Spector estendeu a interpretação da aritmética da Dialética de Gödel para a análise matemática completa, mostrando como o esquema da escolha contável pode receber uma interpretação dialética ao estender o sistema T com recursão de barra .

Interpretação dialética da lógica linear

A interpretação Dialética foi usada para construir um modelo de refinamento da lógica intuicionista de Girard , conhecido como lógica linear , por meio dos chamados espaços Dialética . Visto que a lógica linear é um refinamento da lógica intuicionista, a interpretação dialética da lógica linear também pode ser vista como um refinamento da interpretação dialética da lógica intuicionista.

Embora a interpretação linear na obra de Shirahata valide a regra do enfraquecimento (na verdade é uma interpretação da lógica afim ), a interpretação dos espaços dialéticos de Paiva não valida o enfraquecimento para fórmulas arbitrárias.

Variantes da interpretação Dialética

Várias variantes da interpretação da Dialética foram propostas desde então. Mais notavelmente a variante de Diller-Nahm (para evitar o problema de contração) e as interpretações monótonas e limitadas de Ferreira-Oliva de Kohlenbach (para interpretar o lema fraco de Kőnig ). Tratamentos abrangentes da interpretação podem ser encontrados em, e.

Referências