Teorema de Löb

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[editar | editar código-fonte]

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 . Se pode 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 \Box A é uma fórmula.
  4. 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[editar | editar código-fonte]

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[editar | editar código-fonte]

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

  1. De \vdash A infere-se \vdash \Box A: Informalmente, isto diz que se A é um teorema, então é demonstrável.
  2. \vdash \Box A \rightarrow \Box \Box A: Se A é demonstrável, então é provado que é demostrável.
  3. \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[editar | editar código-fonte]

  1. 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.
  2. 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..
  3. De 2, segue-se que \vdash \Psi \rightarrow (\Box \Psi \rightarrow P).
  4. Da regra de inferência 1, segue-se que \vdash \Box(\Psi \rightarrow (\Box \Psi \rightarrow P))..
  5. De 4 e da regra de inferência 3, segue-se que \vdash \Box\Psi \rightarrow \Box(\Box \Psi \rightarrow P)..
  6. Da regra de inferência 3, segue-se que \vdash \Box(\Box \Psi \rightarrow P) \rightarrow \Box\Box\Psi \rightarrow \Box P
  7. De 5 e 6, segue-se que \vdash \Box \Psi \rightarrow \Box\Box\Psi \rightarrow \Box P
  8. Da regra de inferência 2, segue-se que \vdash \Box \Psi \rightarrow \Box \Box \Psi
  9. De 7 e 8, segue-se que \vdash \Box \Psi \rightarrow \Box P
  10. De 1 e 9, segue-se que \vdash \Box \Psi \rightarrow P
  11. De 10 e 2, segue-se que \vdash \Psi
  12. De 11 e da regra de inferência 1, segue-se que \vdash \Box \Psi
  13. De 12 e 10, segue-se que \vdash P

Referências

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

Ligações externas[editar | editar código-fonte]