Pero

Question

Si tenemos una consistente y axiomatizable extensión de la PA, que vamos a llamar a $T$, me pregunto si es posible tener una sentencia de $\phi$ tal que $T \vdash Prov_T(\phi)$ pero $T \nvdash \phi$ donde $Prov_T(x)$ expresa "$x$ es comprobable en $T$".

Nota muy importante es que asumimos $T$ contiene "suficiente inducción", que cumple las siguientes derivability condiciones:

(1) "reflexión", que es el si $T \vdash \sigma$ $T \vdash Prov_T(\sigma)$ y (2) un "formal" de la versión de modus ponens tal que $T \vdash Prov_T(a) \land Prov_T(a \rightarrow b) \rightarrow Prov_T(b)$ para cualquier condenas $a$$b$.

Mi intuición es que hay una frase de $\phi$ ya que @Noé Schweber puntos en este post que la solidez no podría mantener.

Por otro lado, también creo que Lob del teorema es relevante y algunos de adaptación podrían demostrar que $T \vdash Prov_T(\phi)$ $T \vdash \phi$ si utilizamos el derivability para adaptar la unidad de negocio del teorema. Cualquier sugerencias?

Answer 1

Tome $T$ a ser la aritmética de Peano (PA) + la frase "PA es inconsistente" (por ejemplo,$Prov_{PA}(0=1)$)

A continuación, $T$ es recursivamente axiomatizable; y por Gödel del teorema de la incompletitud, $T$ es consistente (de lo contrario $PA \vdash Con(PA)$, así que PA es inconsistente, lo cual es absurdo; a menos PA es incoherente, pero entonces toda la discusión es inútil, porque lo que no existe una extensión de la PA - de todos modos, si estamos trabajando en ZF, PA es claramente consistente, así que estamos contentos con esto)

Desde $T$ es consistente, y $PA \vdash \neg (0=1)$,$T\nvdash 0=1$.

Sin embargo, por la definición misma de la $T$, $T\vdash Prov_{PA}(0=1)$ y por lo $T\vdash Prov_T(0=1)$ porque de cualquier forma recursiva axiomatisable extensión de PA $S$ y cada una de las $\phi$,$PA\vdash (Prov_{PA}(\phi) \implies Prov_S(\phi))$.

Por lo tanto hemos encontrado una $T$.

Esta primera parte (antes de editar) respondió "es posible ?" pregunta; ahora si se preguntan acerca de un arbitrario $T$ (podemos encontrar una $\phi$ todos los $T$ ?), la respuesta es no, siendo el mejor ejemplo de PA. De hecho, si $PA\vdash Prov_{PA}(\sigma)$,$\mathbb{N}\models Prov_{PA}(\sigma)$, por lo que no es una prueba real en el PA de $\sigma$: $PA\vdash \sigma$. De hecho, este argumento muestra que cualquier recursivamente axiomatizable extensión de PA que se contiene en cierto aritmética (la teoría de la $\mathbb{N}$) tienen la propiedad de que no hay tal $\phi$: de hecho tenemos una solidez condición: si $\mathbb{N}\models Prov_T(\sigma)$, $T\vdash \sigma$

Answer 2

Edificio de Max excelente respuesta, de lo que se trata aquí es que hay muchos diferentes "nice" de las propiedades de una teoría puede tener, y en ellos se obtienen conclusiones diferentes.

• Ser consistente. 'Nuff dijo.

• Ser recursivamente axiomatizable. Esto es necesario con el fin de hablar de provability de una teoría en el lenguaje de la aritmética. (OK eso no es del todo cierto, en general, todo lo que necesitamos es que la teoría sea definible, pero el trabajo con aritméticamente definido teorías pueden conducir a resultados extraños por lo que es razonable restringir la atención a las axiomatizations aquí.)

• De ser lo suficientemente fuerte. Una teoría de la ampliación de PA (de hecho, incluso mucho menos) tiene la propiedad de que es $\Sigma_1$ completa: cada cierto $\Sigma_1$ frase es demostrable en la teoría. Este en particular implica que si $T$ es lo suficientemente fuerte (y recursivamente axiomatizable), a continuación, $T\vdash\phi$ implica $T\vdash Prov_T(\phi)$ por cada $\phi$.

• De ser lo suficientemente correcta. Consistente suficientemente fuerte recursivamente axiomatizable teorías pueden ser bastante raro, por ejemplo, PA+$\neg$Con(PA). Tenemos un interés separado en no demasiado estúpidas teorías, es decir, teorías que no prueban "manifiestamente falsas" de las oraciones. Tales teorías se llama "sonido" - más específicamente, si $T$ es una teoría que demuestra sólo (no necesariamente todos!) verdadero el enunciado de tipo $\Gamma$, entonces se dice $T$ $\Gamma$-sonido. E. g. PA+$\neg$Con(PA) es no $\Sigma_1$ sonido, ya que demuestra la falsa $\Sigma_1$ frase "$Prov_{PA}(\underline{\ulcorner 0=1\urcorner})$." La corrección es particularmente relevante aquí, y algo sutil, así que voy a dar tres más comentarios sobre ella:

  • En primer lugar, tenga en cuenta que la corrección está en tensión con integridad. Para hacer una teoría de la "más completa" queremos fortalecer , mientras que para hacer una teoría de la "más correcta" debilitar "(por la eliminación de ofender a los axiomas).

  • Segundo, $\Gamma$-soundess principios no son el único tipo de corrección que son de interés. Por ejemplo, considere la siguiente propiedad: $$\mbox{If $T$ proves $\neg \phi(\underline{n})$ for each $n\in\mathbb{N}$, then $T$ doesn't prove $\exists x\phi(x)$.}$$ (Note that the conclusion is not "then $T$ proves $\forall x\neg\phi(x)$"!) This property is called $\omega$-consistencia. Históricamente, esta fue una suposición de Gödel necesarios en su prueba, que fue posteriormente eliminado por Rosser. El término "coherencia" en vez de "solidez" en el nombre del principio refleja el hecho de que realmente es una consistencia de la propiedad *con respecto a un más fuerte de lo habitual, la prueba del sistema. De hecho, la solidez de los principios en general pueden considerarse como "mayor coherencia de los principios".

  • Por último, vale la pena señalar que en la cara de la solidez de los principios puede requerir algún tipo de "Platónico compromiso" para hacer sentido de la frase "$\Sigma_{17}$-sonido," necesitamos (en la cara de ella) cometer a la noción de que $\Sigma_{17}$ declaraciones han definido valores de verdad. Si creemos que $\mathbb{N}$ "existe" (???), entonces esto no es problemático, pero el más "matemática escepticismo" adoptamos rápidamente se puede hacer sospechar siquiera la noción de solidez (mientras que la coherencia, ser $\Pi_1$, es algo más aceptable). Esto nos lleva también a cuestiones fundamentales, y realmente es ortogonal a su pregunta aquí, así que no quiero ir a entrar en más detalle, en particular, en mi opinión, es mejor cuando el aprendizaje de los conceptos básicos de este tema, al menos temporalmente, de adoptar la posición de que $\mathbb{N}$ "realmente existente" y toda la aritmética declaraciones (al menos) se han definido valores de verdad - pero de todos modos vale la pena mencionar.

---

La conexión con tu pregunta es la siguiente:

Supongamos $T$ es una constante, recursivamente axiomatizable, lo suficientemente fuerte como teoría. Entonces es posible que haya algunos $\phi$ tal que $T\vdash Prov_T(\phi)$ pero $T\not\vdash\phi$; por ejemplo, tome $T$ PA+$\neg$Con(PA) y $\phi$"$0=1$." Sin embargo, esta es descartada si $T$ es, además, supone ser $\omega$-consistente$^1$ $\Sigma_1$- sonido$^2$.

$^1$Esto fue lo Gödel utilizado $\omega$-consistencia en su original argumento, a pesar de que él podría haber hecho con los más débiles$^3$ asunción de $\Sigma_1$-solidez sin cambiar el argumento; no sé cuando esto fue observado por primera vez.

$^2$Tenga en cuenta que $\Sigma_1$-la solidez y la $\Sigma_1$-integridad - el último de los cuales sigue por la supuesta fuerza de $T$ - junto implica que el $\Sigma_1$ teoremas de $T$ son exactamente los verdaderos $\Sigma_1$ declaraciones, pero no implica que $T$ demuestra cada cierto $\Pi_1$ declaración, y, de hecho, desde el conjunto de la verdadera $\Sigma_1$ las declaraciones no es recursiva sabemos que esto no puede suceder desde $T$ es recursivamente axiomatizable.

$^3$Sí, $\omega$-consistencia es estrictamente más fuerte que $\Sigma_1$ solidez! El punto es que $\omega$-consistencia se aplica a todos los $\phi$, no sólo a $\phi$ de una cierta complejidad.