Teorema de Löb

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 de manera más formal 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 verdadera” 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 debe su nombre a 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 . Es decir, cuando es una fórmula lógica, se puede formar otra fórmula colocando un recuadro delante de , y tiene la intención de significar que es demostrable. ${\displaystyle \phi }$ ${\displaystyle \Box \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \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. Esto a veces 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 axiomático 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}$

Demostración modal del teorema de Löb

El teorema de Löb se puede demostrar dentro de la lógica modal usando 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 las 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 en esta sintaxis que no contiene variables proposicionales. La notación se utiliza para indicar 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 de 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 tales puntos fijos para cada fórmula modal con una variable libre. Por supuesto, 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 sigue 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 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)}$

Demostración 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 que dependen de hasta el final. ${\displaystyle \Box P\to P}$ ${\displaystyle \Box P\to P}$

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

1. Aplica la existencia de puntos fijos modales a la fórmula . De ello 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)}$, desde 1.
3. ${\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))}$, a partir del 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 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 }$, a partir del 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. Supongamos que . En términos generales, es un teorema que si es demostrable, entonces es, de hecho, verdadero. Esta es una afirmación de solidez . ${\displaystyle \vdash \Box P\rightarrow P}$ ${\displaystyle P}$
10. ${\displaystyle \vdash \Box \Psi \rightarrow P}$, de 8 y 9.
11. ${\displaystyle \vdash (\Box \Psi \rightarrow P)\rightarrow \Psi }$, desde 1.
12. ${\displaystyle \vdash \Psi }$, de 10 y 11.
13. ${\displaystyle \vdash \Box \Psi }$, a partir del 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. Ya que por suposición, 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 demuestra , que es lo mismo que . ${\displaystyle \{{\mathit {PA}},\neg P\}}$ ${\displaystyle \neg P\to \bot {}}$ ${\displaystyle P}$
   2. Sin embargo, ya se sabe que hay una contradicción. ${\displaystyle \{{\mathit {PA}},\neg P\}}$ ${\displaystyle \neg \mathrm {Prov} _{PA}(P)}$
   3. Por lo tanto, es consistente. ${\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. Por lo tanto, 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 verdadera" 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 es demostrable 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, como lo es cualquier enunciado 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 AP, entonces el teorema de Ramsey finito reforzado es verdadero" no es demostrable en AP, como "El teorema de Ramsey finito reforzado es verdadero" no es demostrable en AP (a pesar de ser verdadero).

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

El segundo teorema de incompletitud de Gödel se deriva del teorema de Löb sustituyendo la afirmación falsa por P. ${\displaystyle \bot }$

Recíproco: El teorema de Löb implica la existencia de puntos fijos modales.

No sólo la existencia de puntos fijos modales implica el teorema de Löb, sino que también es válido el recíproco. Cuando el teorema de Löb se da como axioma (esquema), se puede derivar la existencia de un punto fijo (hasta equivalencia demostrable) para cualquier fórmula A ( p ) modalizada en p . ^[5] Así, en la lógica modal normal , el axioma de Löb es equivalente a la conjunción del esquema de axiomas 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 cada afirmación es demostrable, incluida ). ${\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 . Cambridge University Press . 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". Journal of Philosophical Logic . 35 (3): 225–230. doi :10.1007/s10992-005-9013-8. S2CID  11038803.
• Löb, Martin (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. pp. 341–352. 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 sobre "Lógica de la demostrabilidad" de Rineke (LC) Verbrugge en la Stanford Encyclopedia of Philosophy , 2017