Sé que una prueba de Hindman del teorema que utiliza ultrafilters en los números naturales, y en última instancia, el axioma de elección. Pero el teorema en sí es esencialmente una combinatoria de propiedad de los números naturales, así que de alguna manera espero que no debe ser una prueba que no necesita de elección, sobre todo porque puede ser escrito de una forma totalmente "finitistic". Mi pregunta no es sobre Hindman del teorema de sí mismo; estoy interesado en saber si tenemos un método general de reducción de la prueba de$\sf ZFC$$\sf ZF$, por los teoremas que pueden expresarse en el lenguaje de la $\sf PA$.
Respuesta
¿Demasiados anuncios?Giro mi comentario en una respuesta:
Aritmética declaración comprobable en $\mathsf{ZFC}$ es comprobable en $\mathsf{ZF}$. El punto es que si $\mathsf{ZFC}$ demuestra que $\mathbb N\models\phi$, $\mathsf{ZF}$ demuestra que $L$ modelos de $\mathbb N\models\phi$. Para ver esto, observe que el $\mathsf{ZFC}$ prueba utiliza sólo un número finito de axiomas de la $\mathsf{ZFC}$, y es un teorema de $\mathsf{ZF}$ que $L$ satisface estos axiomas.
Podemos concluir señalando que, si $L\models \mathbb N\models\phi$,$\mathbb N\models \phi$.
El argumento puede ser empujado un poco. El Shoenfield absolutismo teorema nos da que la misma ofrece, no solo para la aritmética de las declaraciones de ($\Sigma^0_n$ algunos $n$), pero incluso para $\Sigma^1_2$ declaraciones. (Kanamori, el libro de los grandes cardenales, un análisis cuidadoso de este resultado). Y este no es el final de la historia: Salir de la aritmética jerarquía, aún podemos encontrar restos de lo absoluto; por ejemplo, ver aquí.