Teorema de Löb

O teorema de Löb na lógica matemática, estabelece que em uma teoria com aritmética de Peano, para qualquer fórmula P, se é possível demonstrar que “se P é demonstrável, então P é verdadeiro", então P é demonstrável. I.e.

$\mathrm{s}\mathrm{e}PA⊢(Bew(\mathrm{\#}P)\to P),\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{o}PA⊢P$

Onde Bew(#P) significa que a fórmula P com número de Gödel #P é demonstrável.

O teorema de Löb deve seu nome a Martin Hugo Löb, que o formulou em 1955.

O teorema de Löb na lógica demonstrativa

A lógica demonstrativa se abstrai dos detalhes das fórmulas utilizadas nos teorema de incompletude de Gödel expressando a demonstrabilidade de P no sistema dado e na linguagem da lógica modal, por meio da modalidade. Pode-se formalizar o teorema de Löb mediante o axioma:

$◻(◻P\to P)\to ◻P,$

Conhecido como axioma GL, de Gödel-Löb. O mesmo às vezes é formalizado por meio da seguinte regra de inferência:

$P$

De

$◻P\to P.$

A lógica demonstrativa GL, que resulta de tomar a lógica modal K4 e agregar-lhe o axioma GL, é o sistema investigado com maior intensidade na lógica demonstrativa.

Prova Modal do teorema de Löb

O teorema de Löb's pode ser provado por meio da lógica modal usando apenas algumas regras básicas de prova mais a existência de pontos fixos modais

Fórmulas Modais

Vamos admitir a seguinte gramática para fórmulas:

1. Se $X$ é uma variável proposicional, então $X$ é uma fórmula.
2. Se $K$ é uma constante proposicional, então $K$ é uma fórmula.
3. Se $A$ é uma fórmula, então $◻A$ é uma fórmula.
4. Se $A$ e $B$ são fórmulas, então também são $\mathrm{\neg }A$, $A\to B$, $A\wedge B$, $A\vee B$, e $A\leftrightarrow B$

Uma sentença modal é uma fórmula modal que não contém variáveis proposicionais. Utilizamos $⊢A$ para exprimir que $A$ é um teorema

Pontos Fixos Modais

Se $F(X)$ é uma formula modal com somente uma variável proposicional $X$, então um ponto fixo modal de $F(X)$ é uma sentença $\mathrm{\Psi }$ tal que

$⊢\mathrm{\Psi }\leftrightarrow F(◻\mathrm{\Psi })$

Vamos supor a existência de tais pontos fixos para toda fórmula modal com uma variável livre. Isto, naturalmente, não é uma coisa óbvia para assumir, mas se nós interpretamos $◻$ como prova na aritmética de Peano, então a existência de pontos fixos modais é de fato verdade.

Regras Modais de Inferência

Além da existência de pontos fixos modais, assumimos as seguintes regras de inferência para o operador $◻$ :

1. De $⊢A$ infere-se $⊢◻A$: Informalmente, isto diz que se A é um teorema, então é demonstrável.
2. $⊢◻A\to ◻◻A$: Se A é demonstrável, então é provado que é demostrável.
3. $⊢◻(A\to B)\to (◻A\to ◻B)$: Esta regra permite que você faça modus ponens. Se é demonstrável que A implica B, e A é demonstrável, então B é demonstrável.

Prova do teorema de Löb

1. Suponha que haja uma sentença modal $P$ tal que $⊢◻P\to P$. Grosseiramente falando, é um teorema que se $P$ é demonstrável, então ele é, de fato, verdadeiro.
2. Seja $\mathrm{\Psi }$ uma sentença tal que $⊢\mathrm{\Psi }\leftrightarrow (◻\mathrm{\Psi }\to P)$. A existência de tal sentença segue a existência de um ponto fixo de fórmula $F(X)==X\to P$..
3. De 2, segue-se que $⊢\mathrm{\Psi }\to (◻\mathrm{\Psi }\to P)$.
4. Da regra de inferência 1, segue-se que $⊢◻(\mathrm{\Psi }\to (◻\mathrm{\Psi }\to P))$..
5. De 4 e da regra de inferência 3, segue-se que $⊢◻\mathrm{\Psi }\to ◻(◻\mathrm{\Psi }\to P)$..
6. Da regra de inferência 3, segue-se que $⊢◻(◻\mathrm{\Psi }\to P)\to ◻◻\mathrm{\Psi }\to ◻P$
7. De 5 e 6, segue-se que $⊢◻\mathrm{\Psi }\to ◻◻\mathrm{\Psi }\to ◻P$
8. Da regra de inferência 2, segue-se que $⊢◻\mathrm{\Psi }\to ◻◻\mathrm{\Psi }$
9. De 7 e 8, segue-se que $⊢◻\mathrm{\Psi }\to ◻P$
10. De 1 e 9, segue-se que $⊢◻\mathrm{\Psi }\to P$
11. De 10 e 2, segue-se que $⊢\mathrm{\Psi }$
12. De 11 e da regra de inferência 1, segue-se que $⊢◻\mathrm{\Psi }$
13. De 12 e 10, segue-se que $⊢P$

• Predefinição:Citar livro
• Predefinição:Citar livro

Ligações externas

• Löb's theorem at PlanetMath Predefinição:En
• The Cartoon Guide to Löb’s Theorem, by Eliezer Yudkowsky Predefinição:En
• Generalized Löb's Theorem.Jaykov Foukzon Predefinição:En