¿Es Rosser ' truco s necesario?

Question

Una versión de Gödel del primer teorema de la incompletitud va como sigue:

Cualquier verdadero, definably axiomatized teoría de la $T$, en el lenguaje de la aritmética es incompleta.

(por $T$ ser verdadero me refiero a $\mathbb{N}\vDash T$). Una explícita prueba de ello (evitando Tarski del undefinability resultado) se procede a la construcción de una sentencia de Gödel para la teoría, es decir, una sentencia de $\sigma$ tal que $Q\vdash (\sigma\iff \lnot\mathrm{Bwb}_T(\ulcorner\sigma\urcorner))$ donde $Q$ es de Robinson aritmética y $\mathrm{Bwb}$ es el provability predicado.

Uno puede hacer un poco de revolver todo con la hipótesis y obtener Rosser la versión del teorema:

Cualquier consistentes, de forma recursiva axiomatized teoría de la $T$, en el lenguaje de la aritmética que se extiende $Q$ es incompleta.

Rosser la prueba de esta versión consiste en una inteligente de diagonalización en el espíritu de la sentencia de Gödel. Pero este engaño necesario? Se puede demostrar fácilmente que, bajo los supuestos de Rosser del teorema, $T$ no demostrar su sentencia de Gödel $\sigma$, pero yo no veo ninguna manera obvia de mostrar que $T$ no demuestran $\lnot\sigma$ sin adición de supuestos como la veracidad, $\omega$-consistencia o algo similar.

Mi pregunta es, entonces, si Rosser el truco es realmente necesario para producir el resultado. Para ser más específicos, existe una teoría, la satisfacción de los supuestos de Rosser del teorema, que demuestra la negación de su propia sentencia de Gödel?

Tenga en cuenta que la obvia primer intento de $T+\lnot\sigma$ no parece funcionar, ya que $\sigma$ podría no ser el Gödel oración de esta nueva teoría.

Answer 1

Permítanme restringir la atención a la constante, de forma recursiva axiomatized extensiones $T$ de la Aritmética de Peano PA.

Una consideración preliminar: Para este tipo de $T$, se puede formalizar en $T$ la prueba de que la consistencia de $T$ implica que la sentencia de Gödel $\sigma$ $T$ es improbable. Desde $\sigma$ afirma precisamente este unprovability, obtenemos que la Con($T$) implica $\sigma$, que probablemente se encuentre en $T$. (Este es el corazón de la demostración del segundo teorema de la incompletitud.) Por el contrario, $\sigma$, la afirmación de que algo (es decir, a sí mismo) es improbable en $T$, implica inmediatamente Con($T$). Así, la sentencia de Gödel $\sigma$ se puede probar (en $T$) equivalente a la consistencia de la $T$.

En vista de este estudio preliminar, tu pregunta es equivalente a preguntar si algunos de esos teoría de la $T$ puede probar su propia inconsistencia (aunque en realidad consistente). La respuesta es sí. Deje $T$ PA $\neg$Con(PA). Esta teoría es consistente, por Gödel del segundo teorema de la incompletitud. Pero ya que se extiende PA y afirma la inconsistencia de la PA, la prueba de su propia inconsistencia.