Saltar para o conteúdo

Lema da diagonal

Origem: Wikipédia, a enciclopédia livre.

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.[1]

Seja N o conjunto de números naturais. A teoria T representa a função computável f : NN se houver uma formula δ(x,y) na linguagem de T tal que, para cada n, T prova:(∀y) [f(n) = y ↔ δ(n,y)].[2] 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

[editar | editar código-fonte]

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. [3] 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.

Seja f: NN 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.

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. [4]

Referências

  1. See Boolos and Jeffrey (2002, sec. 15) and Mendelson (1997, Prop. 3.37 and Cor. 3.44 ).
  2. For details on representability, see Hinman 2005, p. 316
  3. Smullyan (1991, 1994) are standard specialized references. The lemma is Prop. 3.34 in Mendelson (1997), and is covered in many texts on basic mathematical logic, such as Boolos and Jeffrey (1989, sec. 15) and Hinman (2005).
  4. See Gödel's Collected Works, Vol. 1, p. 363, fn 23.