¿ZFC pin de abajo, precisamente, el que los teoremas de PA puede y no se puede demostrar?

Question

Podemos mostrar (en $\mathrm{ZFC})$ que $\mathrm{PA}$ tiene un modelo. Por lo tanto:

$$\mathrm{ZFC} \vdash (\mathrm{PA} \not\vdash \bot)$$

Esta es probablemente una pregunta tonta, pero es cierto que para todas las condenas $\phi$ en el idioma de $\mathrm{PA}$, tenemos los siguientes? $$(\mathrm{ZFC} \vdash (\mathrm{PA} \vdash \phi)) \vee (\mathrm{ZFC} \vdash (\mathrm{PA} \not\vdash \phi))$$

Supongo que "no".

Answer 1

En primer lugar, si ZFC eran incompatibles, entonces la respuesta sería trivial ser "sí", así que la pregunta es de interés sólo si ZFC es consistente. Voy a utilizar libremente la consistencia de ZFC para el resto de la respuesta.

En ese caso, la respuesta es "no".

Es un estándar de hecho en la computabilidad teoría de que la ap es "inseparable de forma eficaz" de la teoría. Esto significa que si nos vamos a $$V = \{ \phi : PA \vdash \phi\}$$ and $$U = \{ \phi : PA \vdash \lnot \phi\}$$ then there is no computable "separating set" $C$ with $V \subseteq C$ and $C \cap U = \emptyset$. (Both $U$ and $V$ r.e. series porque PA es un efectivo de la teoría; inseparabilidad implica entre otras cosas que ninguno de ellos es computable).

Tenga en cuenta que (*): si $PA \vdash \phi$$ZFC \vdash \ulcorner PA \vdash \phi\urcorner$. Esto es debido a que si tenemos una derivación de $\phi$ en PA podemos convertirlo a una derivación de $\ulcorner PA \vdash \phi\urcorner$ en ZFC.

Ahora vamos a $$S = \{\phi : ZFC \vdash \ulcorner PA \vdash \phi\urcorner\}.$$ Then $S$ is an r.e. set also, and $V \subseteq S$ because of (*). Moreover, $U \cap S = \emptyset$. Suppose otherwise - then there would be a $\phi$ such that $ZFC\vdash \ulcorner PA \vdash \phi \urcorner$ and $PA \vdash \lnot \phi$. But then, using (*), $ZFC \vdash \ulcorner PA \vdash \lnot \phi\urcorner$. Pero ZFC demuestra $$ \lnot(\ulcorner PA \vdash \phi\urcorner \de la tierra \ulcorner PA \vdash \lnot \phi\urcorner) $$ porque ZFC demuestra PA es consistente (por ejemplo, Gentzen la consistencia de la prueba pasa a través de formalizarse en ZFC). Por lo tanto, debido a que ZFC es consistente, $U \cap S$ está vacía.

Si la pregunta tenía una respuesta positiva, $S$ sería computable. El algoritmo sería: dado $\phi$, enumerar derivaciones en ZFC hasta encontrar una derivación de $\ulcorner PA \vdash \phi\urcorner$ o una derivación de $\lnot \ulcorner PA \vdash \phi\urcorner$. Una respuesta afirmativa a la pregunta dice esta búsqueda siempre va a terminar, y ya que ZFC es consistente exactamente una de las dos opciones va a suceder. Entonces podemos decir si $\phi \in S$ por ver la opción que se produce.

Así que, en resumen, si la pregunta tenía una respuesta positiva, a continuación, $S$ sería una computable separar conjunto para$V$$U$, lo cual es imposible.

También, para aquellos que estén interesados, no es necesario usar el hecho de que ZFC tiene un $\omega$-modelo, sólo el hecho de que ZFC es consistente. Que se debe esperar, porque eficaces inseparabilidad es una muy buena forma de incompletitud.

Si usamos el hecho de que ZFC tiene un $\omega$-modelo, se obtiene una mucho más corta argumento, como se ha mencionado en los comentarios. En ese caso, tenemos para todos los $\phi$ que $ZFC \vdash \ulcorner PA \vdash \phi\urcorner$ si y sólo si $PA \vdash \phi$. Entonces, si la pregunta tenía una respuesta afirmativa, podríamos decidir arbitrariamente $\phi$ si $\phi \in V$ por la búsqueda de un ZFC derivación de $\ulcorner PA \vdash \phi\urcorner$ o una derivación de $\lnot \ulcorner PA \vdash \phi \urcorner$; la primera opción significaría $PA \vdash \phi$ y la segunda significaría $PA \not\vdash \phi$. Desde $V$ no es computable, que la contradicción significa que la pregunta tiene una respuesta negativa. Esta prueba es más fácil que el uso eficaz de la inseparabilidad, porque aprovecha una propiedad adicional de ZFC (teniendo un $\omega$-modelo, o más específicamente $\Sigma^0_1$ solidez) que no se utiliza en la prueba por inseparabilidad.