# Lema da diagonal

Na lógica matemática, o lema da diagonal ou teorema do ponto fixo estabelece a existência de sentenças auto-referenciais em certas teorias formais dos números naturais - especificamente as teorias que são fortes o suficiente para representar todas as funções computáveis. As sentenças, cuja existência é garantida pelo lema da diagonal podem então, por sua vez, ser usadas para provar resultados fundamentalmente limitativos, tais como teorema da incompletude de Gödel e o teorema da indefinibilidade de Tarski.

## Background

Seja N o conjunto de números naturais. A teoria T representa a função computável f : N→N se houver uma formula δ(x,y) na linguagem de T tal que, para cada n, T prova:(∀y) [f(n) = y ↔ δ(n,y)]. Aqui n é o numeral correspondente ao número natural n, que é definido como sendo o termo fechado 1+ ··· +1 (os n), e f(n) é o numeral correspondente a f(n). O lema da diagonal também exige que haja uma forma sistemática de atribuir a cada fórmula θ um número natural #(θ) chamado de [número de [Gödel]]. As fórmulas podem, então, ser representadas dentro da teoria dos números por seus correspondentes números de Gödel. O lema da diagonal se aplica a teorias capazes de representar todos as funções recursivas primitivas. Tais teorias incluem a aritmética de Peano e a mais fraca Aritmética de Robinson. Uma declaração comum do lema (conforme dados abaixo) faz a forte suposição de que a teoria que pode representar todas as funções computáveis.

## Enunciado do lema

Seja T uma teoria da lógica de primeira ordem na linguagem da aritmética capaz de representar todas as funções computáveis. Seja ψ uma fórmula na linguagem com uma variável livre. O lema da diagonal afirma que existe uma sentença φ tal que φ ↔ ψ(#(φ)) é demonstrável em T. Intuitivamente, φ é uma sentença auto-referencial dizendo que φ tem a propriedade ψ. A φ frase também pode ser vista como um ponto fixo da operação atribuindo a cada fórmula θ a setença ψ(#(θ)). A sentença φ construída na prova não é literalmente o mesmo que ψ (#(φ)), mas é demonstravelmente equivalente a ela na teoria T.

## Prova

Seja f: N→N a função definida por:
    f(#(θ)) = #(θ(#(θ)))
para cada T,a formula θ é uma variável livre, e f(n) = 0 caso contrário. A função f é computável, então não há uma fórmula δ representando f em T. Assim, para cada fórmula θ, T prova
    (∀y) [ δ(#(θ),y) ⇔ y = f(#(θ))],
que é para dizer
    (∀y) [ δ(#(θ),y) ⇔ y = #(θ(#(θ)))].
Agora defina a formula β(z) como:
    β(z) = (∀y) [δ(z,y) ⇒ ψ(y)],
depois
    β(#(θ)) ⇔ (∀y) [ y = #(θ(#(θ))) ⇒ ψ(y)],
que é para dizer
    β(#(θ)) ⇔ ψ(#(θ(#(θ))))
Seja φ a sentença β(#(β)). Então podemos provar para T que:
    (*) φ ⇔ (∀y) [ δ(#(β),y) ⇒ ψ(y)] ⇔ (∀y) [ (y = #(β(#(β))) ⇒ ψ(y)].
Para T, analisamos dois casos: 1. Assumindo φ se mantém, substituindo #(β(#(β)) para y na fórmula mais à direita em (*), obtém-se:
    (#(β(#(β)) = #(β(#(β))) → ψ(#(β(#(β))),
Since φ = β(#(β)), it follows that ψ(#(φ)) holds.
2. Por outro lado , suponha que ψ(#(β(#(β)))) se mantém. Em seguida, a fórmula final em (*) deve ser verdadeira, e φ também é verdadeiro.
Assim φ ↔ ψ(#(φ)) é demonstrável em T, como queríamos demonstrar.

## História

O lema da diagonal está intimamente relacionado com o teorema da recursividade de Kleene na teoria da computabilidade e suas respectivas provas são semelhantes. O lema é chamado de diagonal, porque tem algumas semelhanças com o Argumento de diagonalização de Cantor. Os termos do lema da diagonal ou ponto fixo não aparecem no artigo de Kurt Gödel(1931), ou em Tarski (1936). Carnap (1934) foi o primeiro a demonstrar que para qualquer fórmula ψ numa certa teoria T, satisfeitas algumas condições, não existe uma fórmula φ tal que φ ↔ ψ (#(φ)) é demonstrável em T. O trabalho de Carnap foi formulado em uma linguagem alternativa, pelo fato do conceito de função computável ainda não ter sido desenvolvido em 1934. Mendelson (1997 , p. 204) acredita que Carnap foi o primeiro a afirmar que algo como o lema da diagonal estava implícito no raciocínio de Gödel. Gödel ficou ciente do trabalho de Carnap em 1937.