El truco de Rosser

Para conocer el teorema sobre la escasez de números primos, consulte el teorema de Rosser . Para una introducción general a los teoremas de incompletitud, consulte los teoremas de incompletitud de Gödel .

En lógica matemática , el truco de Rosser es un método para probar los teoremas de incompletitud de Gödel sin 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 prueba 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".

Antecedentes

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

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

Las suposiciones sobre ${\displaystyle T}$ también muestra que es capaz de definir una función de negación ${\displaystyle {\text{neg}}(y)}$, con la propiedad de que si ${\displaystyle y}$ es un código para una fórmula ${\displaystyle \phi }$ luego ${\displaystyle {\text{neg}}(y)}$ es un código para la fórmula ${\displaystyle \neg \phi }$. La función de negación puede tomar cualquier valor para las entradas que no son códigos de fórmulas.

La frase de Gödel de la teoría ${\displaystyle T}$ es una formula ${\displaystyle \phi }$, a veces denotado ${\displaystyle G_{T}}$, tal que ${\displaystyle T}$ prueba ${\displaystyle \phi }$ ↔${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}$. La prueba de Gödel muestra que si${\displaystyle T}$es consistente entonces no puede probar su sentencia de Gödel; pero para mostrar 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 meramente consistente. Por ejemplo, la teoría${\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}$, en el que PA es axiomas de Peano , demuestra${\displaystyle \neg G_{T}}$. 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 la consistencia ω.

La sentencia de Rosser

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

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

${\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 probabilidad modificado:${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$:

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

Informalmente ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$ es la afirmación de que ${\displaystyle y}$ es demostrable a través de alguna prueba codificada ${\displaystyle x}$ tal que no hay prueba codificada más pequeña de la negación de ${\displaystyle y}$. Bajo el supuesto de que${\displaystyle T}$ es consistente, para cada fórmula ${\displaystyle \phi }$ la formula ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$ se mantendrá si y solo si ${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$ tiene, porque si hay un código para la prueba de ${\displaystyle \phi }$, luego (siguiendo la consistencia de ${\displaystyle T}$) no hay un código para la prueba de ${\displaystyle \neg \phi }$. Sin embargo,${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$ y ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$ tienen diferentes propiedades desde el punto de vista de la demostrabilidad en ${\displaystyle T}$.

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

Usando el lema diagonal , deje${\displaystyle \rho }$ ser una fórmula tal que ${\displaystyle T}$ demuestra ρ ↔ ¬ Pvbl^R
_T(# ρ). ${\displaystyle \rho }$ ↔${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\rho )}$. La formula${\displaystyle \rho }$es la oración de Rosser de la teoría${\displaystyle T}$.

Teorema de Rosser

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

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 ${\displaystyle y}$ y un numero ${\displaystyle e}$, Si ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ aguanta, entonces ${\displaystyle T}$ prueba ${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$. Esto se muestra de manera similar a lo que se hace en la demostración de Gödel del primer teorema de incompletitud:${\displaystyle T}$ prueba ${\displaystyle \operatorname {Proof} _{T}(e,y)}$, una relación entre dos números naturales concretos; uno luego repasa todos los números naturales${\displaystyle z}$ menor que ${\displaystyle e}$ uno por uno, y para cada uno ${\displaystyle z}$, ${\displaystyle T}$ prueba ${\displaystyle \neg \operatorname {Proof} _{T}(z,{\text{(neg}}(y))}$, nuevamente, una relación entre dos números concretos.

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

Además, si ${\displaystyle T}$ es consistente y demuestra ${\displaystyle \phi }$, entonces hay un número ${\displaystyle e}$ codificación para su prueba en ${\displaystyle T}$, y no hay codificación numérica para la prueba de la negación de ${\displaystyle \phi }$ en ${\displaystyle T}$. Por lo tanto${\displaystyle \operatorname {Proof} _{T}^{R}(e,y)}$ sostiene, y por lo tanto ${\displaystyle T}$ prueba ${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$.

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

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

Referencias

• Mendelson (1977), Introducción a la lógica matemática
• Smorynski (1977), "Los teoremas de la incompletitud", en Handbook of Mathematical Logic , Jon Barwise , Ed., North Holland, 1982, ISBN  0-444-86388-5
• Barkley Rosser (septiembre de 1936). "Extensiones de algunos teoremas de Gödel e Church" . Revista de lógica simbólica . 1 (3): 87–91. JSTOR  2269028 .

Enlaces externos

• Avigad (2007), " Computability and Incompleteness ", notas de clase.