Hispanopedia Wiki
Articulo de referencia

Teorema de Löb

En lógica matemática , el teorema de Löb establece que en la aritmética de Peano (AP) (o cualquier sistema formal que incluya la AP), para cualquier fórmula P , si es demostrabl...

Hispanopedia WikiContenido en espanolLectura gratuita

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

Si
PAGA⊢PAGrov(PAG)→PAG{\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} (P)\rightarrow P}}
entonces
PAGA⊢PAG{\displaystyle {\mathit {PA}}\vdash P}.

Un corolario inmediato (la contrapositiva ) 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, "Si1+1=3{\displaystyle 1+1=3}es demostrable en PA, entonces1+1=3{\displaystyle 1+1=3}" no es demostrable en PA. [ 1 ]

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

El teorema de Löb en lógica de la demostrabilidad.

La lógica de demostrabilidad abstrae los detalles de las codificaciones utilizadas en los teoremas de incompletitud de Gödel al expresar la demostrabilidad deϕ{\displaystyle \phi }en el sistema dado en el lenguaje de la lógica modal , por medio de la modalidad◻ϕ{\displaystyle \Box \phi }. Es decir, cuandoϕ{\displaystyle \phi }es una fórmula lógica, otra fórmula se puede formar colocando una caja delante deϕ{\displaystyle \phi }y pretende significar queϕ{\displaystyle \phi }es demostrable.

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

◻(◻PAG→PAG)→◻PAG,{\displaystyle \Box (\Box P\rightarrow P)\rightarrow \Box P,}

Conocido como axioma GL, por Gödel-Löb. Esto a veces se formaliza mediante la regla de inferencia:

Si
⊢◻PAG→PAG{\displaystyle \vdash \Box P\rightarrow P}
entonces
⊢PAG{\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,◻A→◻◻A{\displaystyle \Box A\rightarrow \Box \Box A}, entonces se vuelve redundante) y agregar el axioma anterior GL es el sistema más intensamente investigado en lógica de demostrabilidad.

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

Supondremos la siguiente gramática para las fórmulas:

  1. Siincógnita{\displaystyle X}es una variable proposicional , entoncesincógnita{\displaystyle X}es una fórmula.
  2. SiK{\displaystyle K}es una constante proposicional, entoncesK{\displaystyle K}es una fórmula.
  3. SiA{\displaystyle A}es una fórmula, entonces◻A{\displaystyle \Box A}es una fórmula.
  4. SiA{\displaystyle A}yB{\displaystyle B}son fórmulas, entonces también lo son¬A{\displaystyle \neg A},A→B{\displaystyle A\rightarrow B},A∧B{\displaystyle A\wedge B},A∨B{\displaystyle A\vee B}, yA↔B{\displaystyle A\leftrightarrow B}

Una oración modal es una fórmula en esta sintaxis que no contiene variables proposicionales. La notación⊢A{\displaystyle \vdash A}se utiliza para significar queA{\displaystyle A}es un teorema.

SiF(incógnita){\displaystyle F(X)}es una fórmula modal con una sola variable proposicionalincógnita{\displaystyle X}, entonces un punto fijo modal deF(incógnita){\displaystyle F(X)}es una oraciónΨ{\displaystyle \Psi }de tal manera que

⊢Ψ↔F(◻Ψ){\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, esto no es algo obvio de suponer, pero si interpretamos◻{\displaystyle \Box }como demostrabilidad en la aritmética de Peano, entonces la existencia de puntos fijos modales se deduce del lema diagonal .

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

  1. (necesidad) De⊢A{\displaystyle \vdash A}concluir⊢◻A{\displaystyle \vdash \Box A}En términos informales, esto significa que si A es un teorema, entonces es demostrable.
  2. (necesidad interna)⊢◻A→◻◻A{\displaystyle \vdash \Box A\rightarrow \Box \Box A}: Si A es demostrable, entonces es demostrable que es demostrable.
  3. (distributividad de la caja)⊢◻(A→B)→(◻A→◻B){\displaystyle \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}Esta regla permite aplicar el modus ponens dentro del operador de demostrabilidad. Si se puede demostrar que A implica B, y A es demostrable, entonces B es demostrable.

Demostración del teorema de Löb

Gran parte de la demostración no utiliza la suposición.◻PAG→PAG{\displaystyle \Box P\to P}, por lo que para facilitar la comprensión, la demostración a continuación se subdivide para dejar las partes que dependen de◻PAG→PAG{\displaystyle \Box P\to P}hasta el final.

DejarPAG{\displaystyle P}ser cualquier oración modal.

  1. Aplicar la existencia de puntos fijos modales a la fórmulaF(incógnita)=incógnita→PAG{\displaystyle F(X)=X\rightarrow P}De ello se deduce que existe una oración.Ψ{\displaystyle \Psi }de tal manera que⊢Ψ↔(◻Ψ→PAG){\displaystyle \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)}.
  2. ⊢Ψ→(◻Ψ→PAG){\displaystyle \vdash \Psi \rightarrow (\Box \Psi \rightarrow P)}, desde 1.
  3. ⊢◻(Ψ→(◻Ψ→PAG)){\displaystyle \vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))}, de 2 por la regla de necesidad.
  4. ⊢◻Ψ→◻(◻Ψ→PAG){\displaystyle \vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)}, a partir de 3 y la regla de distributividad de la caja.
  5. ⊢◻(◻Ψ→PAG)→(◻◻Ψ→◻PAG){\displaystyle \vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)}, regla de distributividad de la caja "⊢◻(A→B)→(◻A→◻B){\displaystyle \vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}" conA=◻Ψ{\displaystyle A=\Box \Psi }yB=PAG{\displaystyle B=P}.
  6. ⊢◻Ψ→(◻◻Ψ→◻PAG){\displaystyle \vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)}, de 4 y 5.
  7. ⊢◻Ψ→◻◻Ψ{\displaystyle \vdash \Box \Psi \rightarrow \Box \Box \Psi }, regla de necesidad interna.
  8. ⊢◻Ψ→◻PAG{\displaystyle \vdash \Box \Psi \rightarrow \Box P}, de 6 y 7. Ahora viene la parte de la demostración donde se utiliza la hipótesis.
  9. Supongamos que⊢◻PAG→PAG{\displaystyle \vdash \Box P\rightarrow P}En términos generales, es un teorema que dice que siPAG{\displaystyle P}Si es demostrable, entonces es, de hecho, cierto. Esta es una afirmación de solidez .
  10. ⊢◻Ψ→PAG{\displaystyle \vdash \Box \Psi \rightarrow P}, de 8 y 9.
  11. ⊢(◻Ψ→PAG)→Ψ{\displaystyle \vdash (\Box \Psi \rightarrow P)\rightarrow \Psi }, desde 1.
  12. ⊢Ψ{\displaystyle \vdash \Psi }, de 10 y 11.
  13. ⊢◻Ψ{\displaystyle \vdash \Box \Psi }, de 12 por la regla de necesidad.
  14. ⊢PAG{\displaystyle \vdash P}, de 13 y 10.

De forma más informal, podemos esbozar la demostración de la siguiente manera.

  1. DesdePAGA⊢PAGrovPAGA(PAG)→PAG{\displaystyle {\mathit {PA}}\vdash {\mathrm {Prov} _{PA}(P)\rightarrow P}}Por suposición, también tenemosPAGA⊢¬PAG→¬PAGrovPAGA(PAG){\displaystyle {\mathit {PA}}\vdash {\neg P\rightarrow \neg \mathrm {Prov} _{PA}(P)}}, lo cual implica{PAGA,¬PAG}⊢¬PAGrovPAGA(PAG){\displaystyle \{{\mathit {PA}},\neg P\}\vdash {\neg \mathrm {Prov} _{PA}(P)}}.
  2. Ahora, la teoría híbrida{PAGA,¬PAG}{\displaystyle \{{\mathit {PA}},\neg P\}}puede razonar de la siguiente manera:
    1. Suponer{PAGA,¬PAG}{\displaystyle \{{\mathit {PA}},\neg P\}}es inconsistente, entonces PA lo demuestra¬PAG→⊥{\displaystyle \neg P\to \bot {}}, que es lo mismo quePAG{\displaystyle P}.
    2. Sin embargo,{PAGA,¬PAG}{\displaystyle \{{\mathit {PA}},\neg P\}}ya sabe que¬PAGrovPAGA(PAG){\displaystyle \neg \mathrm {Prov} _ {PA}(P)}, una contradicción.
    3. Por lo tanto,{PAGA,¬PAG}{\displaystyle \{{\mathit {PA}},\neg P\}}es consistente.
  3. Según el segundo teorema de incompletitud de Gödel, esto implica{PAGA,¬PAG}{\displaystyle \{{\mathit {PA}},\neg P\}}es inconsistente.
  4. Por lo tanto, PA demuestra¬PAG→⊥{\displaystyle \neg P\to \bot {}}, que es lo mismo quePAG{\displaystyle P}.

Ejemplos

Una consecuencia inmediata 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 sencillos:

  • "Si1+1=3{\displaystyle 1+1=3}es demostrable en PA, entonces1+1=3{\displaystyle 1+1=3}" no es demostrable en PA, como1+1=3{\displaystyle 1+1=3}no es demostrable en PA (ya que es falso).
  • "Si1+1=2{\displaystyle 1+1=2}es demostrable en PA, entonces1+1=2{\displaystyle 1+1=2}" es demostrable en PA, al igual que cualquier enunciado de la forma "Si X, entonces1+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, ya que "El teorema de Ramsey finito reforzado es verdadero" no es demostrable en PA (a pesar de ser verdadero).

En 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 ": dicho razonador 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 deduce del teorema de Löb sustituyendo la afirmación falsa.⊥{\displaystyle \bot }para P.​

Recíprocamente: el teorema de Löb implica la existencia de puntos fijos modales.

La existencia de puntos fijos modales no solo implica el teorema de Löb, sino que el recíproco también es válido. Cuando el teorema de Löb se da como un axioma (esquema), la existencia de un punto fijo (salvo equivalencia demostrable)pag↔A(pag){\displaystyle p\leftrightarrow A(p)}para cualquier fórmula A ( p ) modalizada en p se puede derivar. [ 5 ] Por lo tanto, en la lógica modal normal , el axioma de Löb es equivalente a la conjunción del esquema axiomático 4 ,(◻A→◻◻A){\displaystyle (\Box A\rightarrow \Box \Box A)}y la existencia de puntos fijos modales.

Notas

  1. ↑ A menos que PA sea inconsistente (en cuyo caso cada afirmación es demostrable, incluyendo1+1=3{\displaystyle 1+1=3}).
  2. ↑ Löb 1955 .
  3. ↑ Neel, Krishnaswami (9 de mayo de 2016). "El teorema de Löb es (casi) el combinador Y" . Semantic Domain . 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 demostración . Estudios en lógica y fundamentos de las matemáticas. Vol.  137. Elsevier . pp. 475–546 . doi : 10.1016/S0049-237X(98)80022-0 . ISBN  978-0-444-89840-1.
  • 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". Journal of Symbolic Logic . 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.