Truque de Rosser

Para o teorema sobre a escassez de números primos, consulte o teorema de Rosser. Para uma introdução geral aos teoremas de incompletude, consulte Teoremas da incompletude de Gödel.

Em lógica matemática, o truque de Rosser é um método de prova de Teoremas da Incompletude de Gödel, sem o pressuposto de que a teoria a ser considerada é ω-consistente (Smorynski 1977, p. 840; Mendelson 1977, p. 160). Este método foi introduzido por J. Barkley Rosser, em 1936, como uma melhoria da prova original de Gödel dos teoremas de incompletude, que foi publicada em 1931.

Enquanto a prova original de Gödel usa uma frase que diz (informalmente) "Esta sentença não é demonstrável", o truque de Rosser usa uma fórmula que diz: "Se esta sentença for demonstrável, há uma prova menor de sua negação".

Contexto

O truque de Rosser começa com os pressupostos do teorema da incompletude de Gödel. Uma teoria T é selecionada, que é efetiva, consistente, e inclui um fragmento suficiente de aritmética elementar.

A prova de Gödel mostra que, para uma teoria qualquer existe uma fórmula Proof_T(x,y), que tem o significado que se pretende, que y é um código de número natural (um número de Gödel) para uma fórmula e x é o número de Gödel de uma prova, a partir de axiomas de T, da fórmula codificada por y. (No restante deste artigo, não há distinção entre o número y e a fórmula codificada por y, e o número de codificação de uma fórmula φ é denotado #φ). Além disso, a fórmula Pvbl_T(y) é definida como ∃x Proof_T(x,y). Esta destina-se a definir o conjunto de fórmulas demonstráveis a partir de T.

Os pressupostos de T também mostram que este é capaz de definir uma função de negação neg(y), com a propriedade de que, se y é um código para uma fórmula φ, então neg(y) é um código para a fórmula ¬φ. A função de negação pode assumir qualquer valor para entradas que não são códigos de fórmulas.

A sentença de Gödel da teoria T é uma fórmula φ, às vezes chamada G_T tal que T prova φ ↔ ¬Pvbl_T(#φ). A prova de Gödel mostra que, se T é consistente, então ela não pode provar sua sentença de Gödel; mas a fim de mostrar que a negação da sentença de Gödel também não é demonstrável, é necessário adicionar uma suposição mais forte de que a teoria é ω-consistente, não apenas consistente. Por exemplo, a teoria T=PA+¬G_PA prova ¬G_T. Rosser (1936) construiu uma diferente sentença auto-referencial que pode ser usada para substituir a sentença de Gödel na prova de Gödel, eliminando a necessidade de assumir ω-consistência.

A sentença de Rosser

Para uma teoria fixa da aritmética T, suponha que Proof_T(x,y) e neg(x) sejam o predicado de prova associadoe a função de negação.

Um predicado modificado de prova Proof^R_T(x,y) é definido como:

$\mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))],$

o que significa que

$\lnot \mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))].$

Este predicado modificado de prova é usado para definir um predicado de demonstrabilidade modificado Pvbl^R_T(y):

$\mathrm {Pvbl} _{T}^{R}(y)\equiv \exists x\mathrm {Proof} _{T}^{R}(x,y).$

Informalmente, Pvbl^R_T(y) é a alegação de que y é demonstrável através de uma prova codificada x tal que não há menor prova codificada da negação de y. Sob a suposição de que T é consistente, para cada fórmula φ a fórmula Pvbl^R_T(#φ) será verdadeira se, e somente se, Pvbl_T(#φ) for verdadeira. No entanto, estes predicados têm propriedades diferentes do ponto de vista de demonstrabilidade em T.

Usando o lema da diagonal, seja ρ uma fórmula tal que T prova ρ ↔ ¬Pvbl^R_T(#ρ). A fórmula ρ é a sentença de Rosser da teoria T.

Teorema de Rosser

Suponha que T seja uma teoria efetiva e consistente que inclui uma quantidade suficiente de aritmética, com a sentença de Rosser ρ. Então, conclui-se que (Mendelson 1977, p. 160):

1. T não prova ρ.
2. T não prova ¬ρ.

A prova (1) está como na prova de Gödel do primeiro teorema da incompletude. A prova (2) é mais complexa. Assuma que T prova ¬ρ e que e é um código de um número natural para a prova de ¬ρ em T. Por T ser consistente, não existe código para uma prova de ρ em T, então Proof^R_T(e,neg(#ρ)) vai ser verdadeira (porque não existe z < e que codifique uma prova de ρ).

A suposição de que T inclui aritmética suficiente garante que T vai provar

$\forall x(e\leq x\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (\#\rho ))],$

e (usando a suposição de consistência e o fato de que e é um número natural)

$\lnot \exists x<e\,\mathrm {Proof} _{T}(x,\#\rho ).$

A partir da fórmula anterior, as suposições sobre T mostram que elas provam

$\mathrm {Proof} _{T}(x,\#\rho )\to e\leq x.$

Assim, T prova

$\forall x[\mathrm {Proof} _{T}(x,\#\rho )\to \exists z\leq x\mathrm {Proof} _{T}(z,\mathrm {neg} (\#\rho ))].$

Mas esta última fórmula é demonstravelmente equivalente a ρ em T, por definição de ρ, o que significa que T prova ρ. Isso é uma contradição, como T foi assumida provar ¬ρ e assumiu ser consistente. Assim, T pode provar ¬ρ sob a suposição de que T é consistente.

Referências

• Mendelson (1977), Introdução à Lógica Matemática
• Smorynski (1977), "Os teoremas de incompletude", no Manual de Lógica Matemática, Jon Barwise, Ed. Holanda do norte, 1982, ISBN 0-444-86388-5
• Rosser (1936), "Extensões de alguns teoremas de Gödel e a Igreja", Journal of Symbolic Logic, v. 1, pp. 87–91.

Ligações externas

• Avigad (2007), "Computability e Incompletude", anotações de aula.