El truco de Rosser

En lógica matemática , el truco de Rosser es un método para demostrar una variante de los teoremas de incompletitud de Gödel que no se basa en el supuesto de que la teoría que se está considerando es ω-consistente (Smorynski 1977, p. 840; Mendelson 1977, p. 160). Este método fue introducido por J. Barkley Rosser en 1936, como una mejora de la demostración original de Gödel de los teoremas de incompletitud que se publicó en 1931.

Mientras que la prueba original de Gödel usa una oración que dice (informalmente) "Esta oración no es demostrable", el truco de Rosser usa una fórmula que dice "Si esta oración es demostrable, hay una prueba más corta de su negación".

Fondo

El truco de Rosser comienza con los supuestos del teorema de incompletitud de Gödel. Se selecciona una teoría que sea eficaz, consistente e incluya un fragmento suficiente de aritmética elemental. ${\displaystyle T}$

La prueba de Gödel muestra que para cualquier teoría de este tipo existe una fórmula que tiene el significado pretendido: es un código numérico natural (un número de Gödel) para una fórmula y es el número de Gödel para una prueba, a partir de los axiomas de , de la fórmula codificada por . (En el resto de este artículo, no se hace distinción entre el número y la fórmula codificada por , y el número que codifica una fórmula se denota .) Además, la fórmula se define como . Se pretende definir el conjunto de fórmulas demostrables a partir de . ${\displaystyle \operatorname {Proof} _{T}(x,y)}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle T}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle \phi }$ ${\displaystyle \#\phi }$ ${\displaystyle \operatorname {Pvbl} _{T}(y)}$ ${\displaystyle \exists x\operatorname {Proof} _{T}(x,y)}$ ${\displaystyle T}$

Los supuestos también muestran que es capaz de definir una función de negación , con la propiedad de que si es un código para una fórmula entonces es un código para la fórmula . La función de negación puede tomar cualquier valor para entradas que no sean códigos de fórmulas. ${\displaystyle T}$ ${\displaystyle {\text{neg}}(y)}$ ${\displaystyle y}$ ${\displaystyle \phi }$ ${\displaystyle {\text{neg}}(y)}$ ${\displaystyle \neg \phi }$

La frase de Gödel de la teoría es una fórmula , a veces denotada , tal que prueba  ↔ . La prueba de Gödel muestra que si es consistente entonces no puede probar su oración de Gödel; pero para demostrar que la negación de la oración de Gödel tampoco es demostrable, es necesario agregar una suposición más fuerte de que la teoría es ω-consistente , no simplemente consistente. Por ejemplo, lo demuestra la teoría en la que PA son los axiomas de Peano . Rosser (1936) construyó una oración autorreferencial diferente que puede usarse para reemplazar la oración de Gödel en la prueba de Gödel, eliminando la necesidad de asumir ω-consistencia. ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle G_{T}}$ ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}$ ${\displaystyle T}$ ${\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}$ ${\displaystyle \neg G_{T}}$

La sentencia de Rosser

Para una teoría aritmética fija , sea y el predicado de prueba y la función de negación asociados. ${\displaystyle T}$ ${\displaystyle \operatorname {Proof} _{T}(x,y)}$ ${\displaystyle {\text{neg}}(x)}$

Un predicado de prueba modificado se define como: ${\displaystyle \operatorname {Proof} _{T}^{R}(x,y)}$

$${\displaystyle \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))],}$$

Lo que significa que

$${\displaystyle \lnot \operatorname {Proof} _{T}^{R}(x,y)\equiv \operatorname {Proof} _{T}(x,y)\to \exists z\leq x[\operatorname {Proof} _{T}(z,\operatorname {neg} (y))].}$$

Este predicado de prueba modificado se utiliza para definir un predicado de demostrabilidad modificado : ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$

$${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {Proof} _{T}^{R}(x,y).}$$

Informalmente, es la afirmación que se puede demostrar mediante alguna prueba codificada de modo que no existe una prueba codificada más pequeña de la negación de . Bajo el supuesto de que es consistente, para cada fórmula la fórmula se cumplirá si y solo si se cumple, porque si hay un código para la prueba de , entonces (siguiendo la consistencia de ) no hay ningún código para la prueba de . Sin embargo, y tienen propiedades diferentes desde el punto de vista de la demostrabilidad en . ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$ ${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$ ${\displaystyle \phi }$ ${\displaystyle T}$ ${\displaystyle \neg \phi }$ ${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$ ${\displaystyle T}$

Una consecuencia inmediata de la definición es que si incluye suficiente aritmética, entonces se puede probar que para cada fórmula , implica . Esto se debe a que, de lo contrario, hay dos números , que codifican las pruebas de y , respectivamente, y satisfacen ambos y . (De hecho, sólo es necesario demostrar que tal situación no puede ser válida para dos números cualesquiera, además de incluir algo de lógica de primer orden) ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )}$ ${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))}$ ${\displaystyle n,m}$ ${\displaystyle \phi }$ ${\displaystyle \neg \phi }$ ${\displaystyle n<m}$ ${\displaystyle m<n}$ ${\displaystyle T}$

Usando el lema de la diagonal , sea una fórmula tal que demuestre ρ ↔ ¬ Pvbl ${\displaystyle \rho }$ ${\displaystyle T}$^RT
_​(#ρ).  ↔ . La fórmula es la frase de Rosser de la teoría . ${\displaystyle \rho }$ ${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\rho )}$ ${\displaystyle \rho }$ ${\displaystyle T}$

teorema de rosser

Sea una teoría eficaz y consistente que incluya una cantidad suficiente de aritmética, con la oración de Rosser . Entonces se cumple lo siguiente (Mendelson 1977, p. 160): ${\displaystyle T}$ ${\displaystyle \rho }$

1. ${\displaystyle T}$no prueba ${\displaystyle \rho }$
2. ${\displaystyle T}$no prueba ${\displaystyle \neg \rho }$

Para probar esto, primero se muestra que para una fórmula y un número , si se cumple, entonces se prueba . Esto se muestra de manera similar a lo que se hace en la prueba de Gödel del primer teorema de incompletitud: prueba una relación entre dos números naturales concretos; Luego se repasan todos los números naturales menores que uno por uno, y para cada uno se demuestra , nuevamente, una relación entre dos números concretos. ${\displaystyle y}$ ${\displaystyle e}$ ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ ${\displaystyle T}$ ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ ${\displaystyle T}$ ${\displaystyle \operatorname {Proof} _{T}(e,y)}$ ${\displaystyle z}$ ${\displaystyle e}$ ${\displaystyle z}$ ${\displaystyle T}$ ${\displaystyle \neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y))}$

El supuesto de que incluye suficiente aritmética (de hecho, lo que se requiere es lógica básica de primer orden) garantiza que también se cumple en ese caso. ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$

Además, si es consistente y prueba , entonces hay un código numérico para su prueba en , y no hay un código numérico para la prueba de la negación de en . Por lo tanto se sostiene y así se prueba . ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle e}$ ${\displaystyle T}$ ${\displaystyle \phi }$ ${\displaystyle T}$ ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ ${\displaystyle T}$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$

La prueba de (1) es similar a la prueba de Gödel del primer teorema de incompletitud: Supongamos que prueba ; luego se sigue, por la elaboración anterior, que prueba . Así lo demuestra también . Pero asumimos que prueba , y esto es imposible si es consistente. Nos vemos obligados a concluir que eso no lo prueba . ${\displaystyle T}$ ${\displaystyle \rho }$ ${\displaystyle T}$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\rho )}$ ${\displaystyle T}$ ${\displaystyle \neg \rho }$ ${\displaystyle T}$ ${\displaystyle \rho }$ ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle \rho }$

La prueba de (2) también usa la forma particular de . Supongamos que prueba ; luego se sigue, por la elaboración anterior, que prueba . Pero por la consecuencia inmediata de la definición del predicado de demostrabilidad de Rosser, mencionada en la sección anterior, se deduce que prueba . Así lo demuestra también . Pero asumimos que prueba , y esto es imposible si es consistente. Nos vemos obligados a concluir que eso no lo prueba . ${\displaystyle \operatorname {Proof} _{T}^{R}}$ ${\displaystyle T}$ ${\displaystyle \neg \rho }$ ${\displaystyle T}$ ${\displaystyle \operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))}$ ${\displaystyle T}$ ${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}$ ${\displaystyle T}$ ${\displaystyle \rho }$ ${\displaystyle T}$ ${\displaystyle \neg \rho }$ ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle \neg \rho }$

Referencias

• Mendelson (1977), Introducción a la lógica matemática
• Smorynski (1977), "Los teoremas de incompletitud", en Handbook of Mathematical Logic , Jon Barwise , Ed., Holanda Septentrional, 1982, ISBN  0-444-86388-5
• Barkley Rosser (septiembre de 1936). "Ampliaciones de algunos teoremas de Gödel y Church". Revista de Lógica Simbólica . 1 (3): 87–91. doi :10.2307/2269028. JSTOR  2269028. S2CID  36635388.

enlaces externos

• Avigad (2007), "Computabilidad e incompletitud", notas de conferencias.