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

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

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.

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

Ver também

  • Auto-referência

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.
  • George Boolos and Richard Jeffrey, 1989. Computability and Logic, 3rd ed. Cambridge University Press. ISBN 0-521-38026-X ISBN 0-521-38923-2
  • Rudolf Carnap, 1934. Logische Syntax der Sprache. (English translation: 2003. The Logical Syntax of Language. Open Court Publishing.)
  • Hinman, Peter, 2005. Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0
  • Mendelson, Elliott, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
  • Raymond Smullyan, 1991. Gödel's Incompleteness Theorems. Oxford Univ. Press.
  • Raymond Smullyan, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
  • Alfred Tarski, 1936, "The Concept of Truth in Formal Systems" in Corcoran, J., ed., 1983. Logic, Semantics, Metamathematics: Papers from 1923 to 1938. Indianapolis IN: Hackett.