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.

${\displaystyle \mathrm {se} \ PA\vdash (Bew(\#P)\rightarrow P)\mathrm {,entao} \ PA\vdash 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:

${\displaystyle \Box (\Box P\rightarrow P)\rightarrow \Box P,}$

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

${\displaystyle P}$

De

${\displaystyle \Box P\rightarrow 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 ${\displaystyle X}$ é uma variável proposicional, então ${\displaystyle X}$ é uma fórmula.
2. Se ${\displaystyle K}$ é uma constante proposicional, então ${\displaystyle K}$ é uma fórmula.
3. Se ${\displaystyle A}$ é uma fórmula, então ${\displaystyle \Box A}$ é uma fórmula.
4. Se ${\displaystyle A}$ e ${\displaystyle B}$ são fórmulas, então também são ${\displaystyle \neg A}$, ${\displaystyle A\rightarrow B}$, ${\displaystyle A\wedge B}$, ${\displaystyle A\vee B}$, e ${\displaystyle A\leftrightarrow B}$

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

Pontos Fixos Modais

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

${\displaystyle \vdash \Psi \leftrightarrow F(\Box \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 ${\displaystyle \Box }$ 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 ${\displaystyle \Box }$ :

1. De ${\displaystyle \vdash A}$ infere-se ${\displaystyle \vdash \Box A}$: Informalmente, isto diz que se A é um teorema, então é demonstrável.
2. ${\displaystyle \vdash \Box A\rightarrow \Box \Box A}$: Se A é demonstrável, então é provado que é demostrável.
3. ${\displaystyle \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box 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 ${\displaystyle P}$ tal que ${\displaystyle \vdash \Box P\rightarrow P}$. Grosseiramente falando, é um teorema que se ${\displaystyle P}$ é demonstrável, então ele é, de fato, verdadeiro.
2. Seja ${\displaystyle \Psi }$ uma sentença tal que ${\displaystyle \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)}$. A existência de tal sentença segue a existência de um ponto fixo de fórmula ${\displaystyle F(X)==X\rightarrow P}$..
3. De 2, segue-se que ${\displaystyle \vdash \Psi \rightarrow (\Box \Psi \rightarrow P)}$.
4. Da regra de inferência 1, segue-se que ${\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))}$..
5. De 4 e da regra de inferência 3, segue-se que ${\displaystyle \vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)}$..
6. Da regra de inferência 3, segue-se que ${\displaystyle \vdash \Box (\Box \Psi \rightarrow P)\rightarrow \Box \Box \Psi \rightarrow \Box P}$
7. De 5 e 6, segue-se que ${\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi \rightarrow \Box P}$
8. Da regra de inferência 2, segue-se que ${\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi }$
9. De 7 e 8, segue-se que ${\displaystyle \vdash \Box \Psi \rightarrow \Box P}$
10. De 1 e 9, segue-se que ${\displaystyle \vdash \Box \Psi \rightarrow P}$
11. De 10 e 2, segue-se que ${\displaystyle \vdash \Psi }$
12. De 11 e da regra de inferência 1, segue-se que ${\displaystyle \vdash \Box \Psi }$
13. De 12 e 10, segue-se que ${\displaystyle \vdash P}$

Referências

• Hinman, P. (2005). Fundamentals of Mathematical Logic. [S.l.]: A K Peters. ISBN 1-56881-262-0 
• Boolos, George S. (1995). The Logic of Provability. [S.l.]: Cambridge University Press. ISBN 0-521-48325-5 

Ligações externas

• Löb's theorem at PlanetMath (em inglês)
• The Cartoon Guide to Löb’s Theorem, by Eliezer Yudkowsky (em inglês)
• Generalized Löb's Theorem.Jaykov Foukzon (em inglês)