teorema de lob

Lógica de demostrabilidad

En lógica matemática , el teorema de Löb establece que en la aritmética de Peano (PA) (o cualquier sistema formal que incluya PA), para cualquier fórmula P , si es demostrable en PA que "si P es demostrable en PA entonces P es verdadero", entonces P es demostrable en PA. Si Prov( P ) significa que la fórmula P es demostrable, podemos expresar esto más formalmente como

Si

${\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}}$

entonces

${\displaystyle {\mathit {PA}}\vdash P}$.

Un corolario inmediato (el contrapositivo ) del teorema de Löb es que, si P no es demostrable en PA, entonces "si P es demostrable en PA, entonces P es verdadero" no es demostrable en PA. Por ejemplo, "Si es demostrable en PA, entonces " no es demostrable en PA. ^[1] ${\displaystyle 1+1=3}$ ${\displaystyle 1+1=3}$

El teorema de Löb lleva el nombre de Martin Hugo Löb , quien lo formuló en 1955. ^[2] Está relacionado con la paradoja de Curry . ^[3]

Teorema de Löb en lógica de demostrabilidad

La lógica de demostrabilidad se abstrae de los detalles de las codificaciones utilizadas en los teoremas de incompletitud de Gödel al expresar la demostrabilidad de en el sistema dado en el lenguaje de la lógica modal , por medio de la modalidad . ${\displaystyle \phi }$ ${\displaystyle \Box \phi }$

Entonces podemos formalizar el teorema de Löb mediante el axioma

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

conocido como axioma GL, de Gödel-Löb. A veces esto se formaliza mediante la regla de inferencia:

Si

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

entonces

${\displaystyle \vdash P}$.

La lógica de demostrabilidad GL que resulta de tomar la lógica modal K4 (o K , ya que el esquema de axioma 4 , , entonces se vuelve redundante) y agregar el axioma GL anterior es el sistema más intensamente investigado en lógica de demostrabilidad. ${\displaystyle \Box A\rightarrow \Box \Box A}$

Prueba modal del teorema de Löb

El teorema de Löb se puede demostrar dentro de la lógica modal utilizando sólo algunas reglas básicas sobre el operador de demostrabilidad (el sistema K4) más la existencia de puntos fijos modales.

Fórmulas modales

Asumiremos la siguiente gramática para fórmulas:

1. Si es una variable proposicional , entonces es una fórmula. ${\displaystyle X}$ ${\displaystyle X}$
2. Si es una constante proposicional, entonces es una fórmula. ${\displaystyle K}$ ${\displaystyle K}$
3. Si es una fórmula, entonces es una fórmula. ${\displaystyle A}$ ${\displaystyle \Box A}$
4. Si y son fórmulas, entonces también lo son , , , y ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle \neg A}$ ${\displaystyle A\rightarrow B}$ ${\displaystyle A\wedge B}$ ${\displaystyle A\vee B}$ ${\displaystyle A\leftrightarrow B}$

Una oración modal es una fórmula modal que no contiene variables proposicionales. Solemos decir que es un teorema. ${\displaystyle \vdash A}$ ${\displaystyle A}$

Puntos fijos modales

Si es una fórmula modal con una sola variable proposicional , entonces un punto fijo modal es una oración tal que ${\displaystyle F(X)}$ ${\displaystyle X}$ ${\displaystyle F(X)}$ ${\displaystyle \Psi }$

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

Supondremos la existencia de dichos puntos fijos para cada fórmula modal con una variable libre. Por supuesto, esto no es algo obvio de asumir, pero si lo interpretamos como demostrabilidad en la aritmética de Peano, entonces la existencia de puntos fijos modales se deriva del lema diagonal . ${\displaystyle \Box }$

Reglas modales de inferencia

Además de la existencia de puntos fijos modales, asumimos las siguientes reglas de inferencia para el operador de demostrabilidad , conocidas como condiciones de demostrabilidad de Hilbert-Bernays : ${\displaystyle \Box }$

1. (necesidad) De concluir : Informalmente, esto dice que si A es un teorema, entonces es demostrable. ${\displaystyle \vdash A}$ ${\displaystyle \vdash \Box A}$
2. (necesidad interna) : si A es demostrable, entonces es demostrable que es demostrable. ${\displaystyle \vdash \Box A\rightarrow \Box \Box A}$
3. (distributividad de caja) : esta regla le permite hacer modus ponens dentro del operador de demostrabilidad. Si es demostrable que A implica B, y A es demostrable, entonces B es demostrable. ${\displaystyle \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}$

Prueba del teorema de Löb

Gran parte de la prueba no hace uso del supuesto , por lo que para facilitar la comprensión, la prueba a continuación se subdivide para dejar las partes dependiendo hasta el final. ${\displaystyle \Box P\to P}$ ${\displaystyle \Box P\to P}$

Sea cualquier oración modal. ${\displaystyle P}$

1. Aplicar la existencia de puntos fijos modales a la fórmula . Entonces se deduce que existe una oración tal que . ${\displaystyle F(X)=X\rightarrow P}$ ${\displaystyle \Psi }$
   ${\displaystyle \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)}$
2. ${\displaystyle \vdash \Psi \rightarrow (\Box \Psi \rightarrow P)}$, de 1.
3. ${\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))}$, de 2 por la regla de necesidad.
4. ${\displaystyle \vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)}$, de 3 y la regla de distributividad de la caja.
5. ${\displaystyle \vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)}$, aplicando la regla de distributividad de la caja con y . ${\displaystyle A=\Box \Psi }$ ${\displaystyle B=P}$
6. ${\displaystyle \vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)}$, del 4 y 5.
7. ${\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi }$, de 6 por la regla de necesidad interna.
8. ${\displaystyle \vdash \Box \Psi \rightarrow \Box P}$, de 6 y 7.
   
   Ahora viene la parte de la prueba donde se utiliza la hipótesis.
   
   
9. Asumir que . En términos generales, es un teorema que si es demostrable, entonces, de hecho, es cierto. Ésta es una afirmación de solidez . ${\displaystyle \vdash \Box P\rightarrow P}$ ${\displaystyle P}$
10. ${\displaystyle \vdash \Box \Psi \rightarrow P}$, del 8 y 9.
11. ${\displaystyle \vdash (\Box \Psi \rightarrow P)\rightarrow \Psi }$, de 1.
12. ${\displaystyle \vdash \Psi }$, de 10 y 11.
13. ${\displaystyle \vdash \Box \Psi }$, de 12 por la regla de necesidad.
14. ${\displaystyle \vdash P}$, de 13 y 10.

De manera más informal, podemos esbozar la prueba de la siguiente manera.

1. Dado que por supuesto también tenemos , lo que implica . ${\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} _{PA}(P)\rightarrow P}}$ ${\displaystyle {\mathit {PA}}\vdash {\neg P\rightarrow \neg \mathrm {Prov} _{PA}(P)}}$ ${\displaystyle \{{\mathit {PA}},\neg P\}\vdash {\neg \mathrm {Prov} _{PA}(P)}}$
2. Ahora bien, la teoría híbrida puede razonar de la siguiente manera: ${\displaystyle \{{\mathit {PA}},\neg P\}}$
   1. Supongamos que es inconsistente, entonces PA prueba , que es lo mismo que . ${\displaystyle \{{\mathit {PA}},\neg P\}}$ ${\displaystyle \neg P\to \bot {}}$ ${\displaystyle P}$
   2. Sin embargo, ya se sabe que es una contradicción. ${\displaystyle \{{\mathit {PA}},\neg P\}}$ ${\displaystyle \neg \mathrm {Prov} _{PA}(P)}$
   3. Por tanto, es coherente. ${\displaystyle \{{\mathit {PA}},\neg P\}}$
3. Según el segundo teorema de incompletitud de Gödel, esto implica que es inconsistente. ${\displaystyle \{{\mathit {PA}},\neg P\}}$
4. Así, PA demuestra , que es lo mismo que . ${\displaystyle \neg P\to \bot {}}$ ${\displaystyle P}$

Ejemplos

Un corolario inmediato del teorema de Löb es que, si P no es demostrable en PA, entonces "si P es demostrable en PA, entonces P es verdadero" no es demostrable en PA. Dado que sabemos que PA es consistente (pero PA no sabe que PA es consistente), aquí hay algunos ejemplos simples:

• "Si es demostrable en PA, entonces " no es demostrable en PA, como tampoco lo es en PA (ya que es falso). ${\displaystyle 1+1=3}$ ${\displaystyle 1+1=3}$ ${\displaystyle 1+1=3}$
• "Si es demostrable en PA, entonces " es demostrable en PA, al igual que cualquier afirmación de la forma "Si X, entonces ". ${\displaystyle 1+1=2}$ ${\displaystyle 1+1=2}$ ${\displaystyle 1+1=2}$
• "Si el teorema de Ramsey finito reforzado es demostrable en PA, entonces el teorema de Ramsey finito reforzado es verdadero" no es demostrable en PA, como "El teorema de Ramsey finito reforzado es verdadero" no es demostrable en PA (a pesar de ser cierto).

En lógica doxástica , el teorema de Löb muestra que cualquier sistema clasificado como un razonador reflexivo de " tipo 4 " debe ser también " modesto ": tal razonador nunca puede creer "mi creencia en P implicaría que P es verdadero", sin creer también que P es verdad. ^[4]

El segundo teorema de incompletitud de Gödel se deriva del teorema de Löb al sustituir P ​​por el enunciado falso . ${\displaystyle \bot }$

Inversa: el teorema de Löb implica la existencia de puntos fijos modales

La existencia de puntos fijos modales no sólo implica el teorema de Löb, sino que lo contrario también es válido. Cuando el teorema de Löb se da como un axioma (esquema), se puede derivar la existencia de un punto fijo (hasta una equivalencia demostrable) para cualquier fórmula A ( p ) modalizada en p . ^[5] Así, en lógica modal normal , el axioma de Löb es equivalente a la conjunción del esquema de axioma 4 , y la existencia de puntos fijos modales. ${\displaystyle p\leftrightarrow A(p)}$ ${\displaystyle (\Box A\rightarrow \Box \Box A)}$

Notas

1. A menos que PA sea inconsistente (en cuyo caso todas las afirmaciones son demostrables, incluidas ). ${\displaystyle 1+1=3}$
2. Lob 1955.
3. Neel, Krishnaswami. "El teorema de Löb es (casi) el combinador Y". Dominio Semántico . Consultado el 9 de abril de 2024 .
4. Smullyan 1986.
5. Lindström 2006.

Referencias

• Boolos, George S. (1995). La lógica de la demostrabilidad . Prensa de la Universidad de Cambridge . ISBN 978-0-521-48325-4.
• Hinman, P. (2005). Fundamentos de Lógica Matemática . AK Peters. ISBN 978-1-56881-262-5.
• Japaridze, Giorgi; De Jongh, Dick (1998). "Capítulo VII - La lógica de la demostrabilidad". En Buss, Samuel R. (ed.). Manual de teoría de la prueba . Estudios de Lógica y Fundamentos de las Matemáticas. vol. 137. Elsevier . págs. 475–546. doi : 10.1016/S0049-237X(98)80022-0 .
• Lindström, Per (junio de 2006). "Nota sobre algunas construcciones de punto fijo en lógica de demostrabilidad". Revista de Lógica Filosófica . 35 (3): 225–230. doi :10.1007/s10992-005-9013-8. S2CID  11038803.
• Löb, Martín (1955). "Solución de un problema de Leon Henkin". Revista de Lógica Simbólica . 20 (2): 115-118. doi :10.2307/2266895. JSTOR  2266895. S2CID  250348262.
• Smullyan, Raymond M. (1986). "Lógicos que razonan sobre sí mismos". Actas de la conferencia de 1986 sobre aspectos teóricos del razonamiento sobre el conocimiento, Monterey (CA) . San Francisco (CA): Morgan Kaufmann Publishers Inc. págs. doi :10.1016/B978-0-934613-04-0.50028-4. ISBN 9780934613040.

enlaces externos

• "Teorema de Löb". 22 de marzo de 2013. PlanetMath . Consultado el 14 de diciembre de 2023 .
• Entrada "Lógica de demostrabilidad" de Rineke (LC) Verbrugge en la Enciclopedia de Filosofía de Stanford , 2017
• Yudkowsky, Eliezer (17 de agosto de 2008). "La guía de dibujos animados sobre el teorema de Löb" . Consultado el 14 de diciembre de 2023 .