# 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 {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:
    $\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:
    $P$
De
    $\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:
* Se $X$ é uma variável proposicional, então $X$ é uma fórmula.
* Se $K$ é uma constante proposicional, então $K$ é uma fórmula.
* Se $A$ é uma fórmula, então $\Box A$ é uma fórmula.
* Se $A$ e $B$ são fórmulas, então também são $\neg A$, $A\rightarrow 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 $\vdash 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 $\Psi$ tal que
    $\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 $\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 $\Box$ :
* De $\vdash A$ infere-se $\vdash \Box A$: Informalmente, isto diz que se A é um teorema, então é demonstrável.
* $\vdash \Box A\rightarrow \Box \Box A$: Se A é demonstrável, então é provado que é demostrável.
* $\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

* Suponha que haja uma sentença modal $P$ tal que $\vdash \Box P\rightarrow P$. Grosseiramente falando, é um teorema que se $P$ é demonstrável, então ele é, de fato, verdadeiro.
* Seja $\Psi$ uma sentença tal que $\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 $F(X)==X\rightarrow P$..
* De 2, segue-se que $\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)$.
* Da regra de inferência 1, segue-se que $\vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))$..
* De 4 e da regra de inferência 3, segue-se que $\vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)$..
* Da regra de inferência 3, segue-se que $\vdash \Box (\Box \Psi \rightarrow P)\rightarrow \Box \Box \Psi \rightarrow \Box P$
* De 5 e 6, segue-se que $\vdash \Box \Psi \rightarrow \Box \Box \Psi \rightarrow \Box P$
* Da regra de inferência 2, segue-se que $\vdash \Box \Psi \rightarrow \Box \Box \Psi$
* De 7 e 8, segue-se que $\vdash \Box \Psi \rightarrow \Box P$
* De 1 e 9, segue-se que $\vdash \Box \Psi \rightarrow P$
* De 10 e 2, segue-se que $\vdash \Psi$
* De 11 e da regra de inferência 1, segue-se que $\vdash \Box \Psi$
* De 12 e 10, segue-se que $\vdash P$