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$

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