Teorema de Löb - Löb's theorem

Em lógica matemática , o teorema de Löb afirma que na aritmética de Peano (PA) (ou qualquer sistema formal incluindo PA), para qualquer fórmula P , se for demonstrável em PA que "se P é demonstrável em PA, então P é verdadeiro", então P é demonstrável no PA. Mais formalmente, se Prov ( P ) significa que a fórmula P é demonstrável, então

${\ displaystyle \ mathrm {if} \ PA \ vdash ({\ rm {Prov}} (P) \ rightarrow P) \ mathrm {, então} \ PA \ vdash P,}$

ou

${\ displaystyle {\ dfrac {PA \ vdash {\ rm {Prov}} (P) \ rightarrow P} {PA \ vdash P}}.}$

Um corolário imediato (o contrapositivo ) do teorema de Löb é que, se P não é demonstrável em PA, então "se P é demonstrável em PA, então P é verdadeiro" não é demonstrável em PA. Por exemplo, "Se é demonstrável em PA, então " não é demonstrável em PA. ${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$

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

Teorema de Löb na lógica de provabilidade

A lógica da provabilidade se abstrai dos detalhes das codificações usadas nos teoremas da incompletude de Gödel , expressando a provabilidade de no sistema dado na linguagem da lógica modal , por meio da modalidade . ${\ displaystyle \ phi}$${\ displaystyle \ Box \ phi}$

Então, podemos formalizar o teorema de Löb pelo axioma

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

conhecido como axioma GL, para Gödel – Löb. Isso às vezes é formalizado por meio de uma regra de inferência que infere

${\ displaystyle P}$

de

${\ displaystyle \ Box P \ rightarrow P.}$

A lógica de comprovabilidade GL que resulta de tomar a lógica modal K4 (ou K , uma vez que o esquema do axioma 4 , torna-se redundante) e adicionar o axioma GL acima é o sistema mais intensamente investigado na lógica de comprovabilidade. ${\ displaystyle \ Box A \ rightarrow \ Box \ Box A}$

Prova modal do teorema de Löb

O teorema de Löb pode ser provado dentro da lógica modal usando apenas algumas regras básicas sobre o operador de comprovabilidade (o sistema K4) mais a existência de pontos fixos modais.

Fórmulas modais

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

1. Se é uma variável proposicional , então é uma fórmula. ${\ displaystyle X}$${\ displaystyle X}$
2. Se é uma constante proposicional, então é uma fórmula. ${\ displaystyle K}$${\ displaystyle K}$
3. Se é uma fórmula, então é uma fórmula. ${\ displaystyle A}$${\ displaystyle \ Box A}$
4. Se e são fórmulas, assim são , , , , e ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle \ neg A}$${\ displaystyle A \ rightarrow B}$${\ displaystyle A \ wedge B}$${\ displaystyle A \ vee B}$${\ displaystyle A \ leftrightarrow B}$

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

Pontos fixos modais

Se for uma fórmula modal com apenas uma variável proposicional , então um ponto fixo modal de é uma frase tal que ${\ displaystyle F (X)}$${\ displaystyle X}$${\ displaystyle F (X)}$${\ displaystyle \ Psi}$

${\ displaystyle \ vdash \ Psi \ leftrightarrow F (\ Box \ Psi)}$

Assumiremos a existência de tais pontos fixos para cada fórmula modal com uma variável livre. Obviamente, isso não é algo óbvio de se supor, mas se interpretarmos como demonstrabilidade na aritmética de Peano, então a existência de pontos fixos modais decorre do lema diagonal . ${\ displaystyle \ Box}$

Regras modais de inferência

Além da existência de pontos fixos modais, assumimos as seguintes regras de inferência para o operador de provabilidade , conhecidas como condições de provabilidade de Hilbert-Bernays : ${\ displaystyle \ Box}$

1. (necessitação) De concluem : Informalmente, este diz que se A é um teorema, então é provável. ${\ displaystyle \ vdash A}$${\ displaystyle \ vdash \ Box A}$
2. (necessidade interna) : Se A é demonstrável, então é provável que seja demonstrável. ${\ displaystyle \ vdash \ Box A \ rightarrow \ Box \ Box A}$
3. (distributividade da caixa) : Esta regra permite fazer modus ponens dentro do operador de comprovação. Se for provável que A implica B, e A é provável, então B é provável. ${\ displaystyle \ vdash \ Box (A \ rightarrow B) \ rightarrow (\ Box A \ rightarrow \ Box B)}$

Prova do teorema de Löb

1. Suponha que haja uma sentença modal tal que . Grosso modo, é um teorema de que, se for demonstrável, então é, de fato, verdadeiro. Esta é uma afirmação de solidez . ${\ displaystyle P}$${\ displaystyle \ vdash \ Box P \ rightarrow P}$
   ${\ displaystyle P}$
   
2. Da existência de pontos fixos modais para cada fórmula (em particular, a fórmula ) segue-se que existe uma frase tal que . ${\ displaystyle X \ rightarrow P}$${\ displaystyle \ Psi}$${\ displaystyle \ vdash \ Psi \ leftrightarrow (\ Box \ Psi \ rightarrow P)}$
3. De 2, segue-se isso . ${\ displaystyle \ vdash \ Psi \ rightarrow (\ Box \ Psi \ rightarrow P)}$
4. Da regra de necessidade, segue-se isso . ${\ displaystyle \ vdash \ Box (\ Psi \ rightarrow (\ Box \ Psi \ rightarrow P))}$
5. De 4 e da regra de distributividade da caixa, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box (\ Box \ Psi \ rightarrow P)}$
6. Aplicando a regra de distribuição de caixa com e nos dá . ${\ displaystyle A = \ Box \ Psi}$${\ displaystyle B = P}$${\ displaystyle \ vdash \ Box (\ Box \ Psi \ rightarrow P) \ rightarrow (\ Box \ Box \ Psi \ rightarrow \ Box P)}$
7. De 5 e 6, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi \ rightarrow (\ Box \ Box \ Psi \ rightarrow \ Box P)}$
8. Da regra de necessidade interna, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box \ Box \ Psi}$
9. De 7 e 8, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi \ rightarrow \ Box P}$
10. De 1 a 9, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi \ rightarrow P}$
11. De 2, segue-se isso . ${\ displaystyle \ vdash (\ Box \ Psi \ rightarrow P) \ rightarrow \ Psi}$
12. De 10 e 11, segue-se que ${\ displaystyle \ vdash \ Psi}$
13. De 12 e a regra de necessidade, segue-se isso . ${\ displaystyle \ vdash \ Box \ Psi}$
14. De 13 a 10, segue-se isso . ${\ displaystyle \ vdash P}$

Exemplos

Um corolário imediato do teorema de Löb é que, se P não é demonstrável em PA, então "se P é demonstrável em PA, então P é verdadeiro" não é demonstrável em PA. Dado que sabemos que o PA é consistente (mas o PA não sabe que o PA é consistente), aqui estão alguns exemplos simples:

• "Se é demonstrável em PA, então " não é demonstrável em PA, como não é demonstrável em PA (visto que é falso). ${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$${\ displaystyle 1 + 1 = 3}$
• "Se é demonstrável em PA, então " é demonstrável em PA, como qualquer declaração da forma "Se X, então ". ${\ displaystyle 1 + 1 = 2}$${\ displaystyle 1 + 1 = 2}$${\ displaystyle 1 + 1 = 2}$
• "Se o teorema de Ramsey finito fortalecido é provável em PA, então o teorema de Ramsey finito fortalecido é verdadeiro" não é provável em PA, como "O teorema de Ramsey finito fortalecido é verdadeiro" não é provável em PA (apesar de ser verdadeiro).

Na lógica doxástica , o teorema de Löb mostra que qualquer sistema classificado como um raciocinador " tipo 4 " reflexivo também deve ser " modesto ": tal raciocinador nunca pode acreditar "minha crença em P implicaria que P é verdadeiro", sem primeiro acreditar que P é verdade.

O segundo teorema da incompletude de Gödel segue do teorema de Löb, substituindo P pela afirmação falsa . ${\ displaystyle \ bot}$

Converse: o teorema de Löb implica a existência de pontos fixos modais

Não só a existência de pontos fixos modais implica o teorema de Löb, mas o inverso também é válido. Quando o teorema de Löb é dado como um axioma (esquema), a existência de um ponto fixo (até equivalência demonstrável) para qualquer fórmula A ( p ) modalizada em p pode ser derivada. Assim, na lógica modal normal , o axioma de Löb é equivalente ao conjunto do esquema axioma 4 , e a existência de pontos fixos modais. ${\ displaystyle p \ leftrightarrow A (p)}$${\ displaystyle (\ Box A \ rightarrow \ Box \ Box A)}$

Notas

Citações

Referências

• Boolos, George S. (1995). A lógica da provabilidade . Cambridge University Press. ISBN   978-0-521-48325-4 .
• Löb, Martin (1955), "Solution of a Problem of Leon Henkin", Journal of Symbolic Logic , 20 (2): 115-118, JSTOR   2266895
• Hinman, P. (2005). Fundamentos da Lógica Matemática . AK Peters. ISBN   978-1-56881-262-5 .
• Verbrugge, Rineke (LC) (1 de janeiro de 2016). "Lógica de Provabilidade" . The Stanford Encyclopedia of Philosophy . Obtido em 6 de abril de 2016 .

links externos

• Teorema de Löb no PlanetMath
• The Cartoon Guide to Löb's Theorem, de Eliezer Yudkowsky