Uno puede construir una prueba por una pequeña variante de la prueba de que una forma recursiva axiomatized completo de la teoría es decidable.
$1$. Es bien sabido que no existe ningún algoritmo que, dado cualquier frase, $\varphi$ de Teoría de números, va a determinar si la frase es verdadera en los números naturales. Más precisamente, si el conjunto de las sentencias de la Teoría de los números está indizada $(\varphi_n)$ en cualquiera de las formas usuales, entonces el conjunto de $n$ tal que $\varphi_n$ que es verdad en $\mathbb{N}$ no es recursiva. De hecho, la situación es mucho peor que eso: el conjunto no está aún aritméticos.
$2.$ Supongamos que $T$ es una forma recursiva axiomatized extensión de la Aritmética de Peano. A continuación, hay una frase que $\varphi$ de Teoría de números tales que $\varphi$ no es ni demostrable ni rebatible en $T$. La idea es que podamos escribir un programa que lista las pruebas en $T$, ya que el conjunto de (índices) de pruebas es recursivamente enumerable.
Si para cada frase $\varphi$ de Teoría de números, uno de $\varphi$ o $\lnot\varphi$ es un teorema de $T$, tarde o temprano, uno de $\varphi$ o $\lnot\varphi$ se mostraría como en la frase final de una prueba en la lista. Este procedimiento daría un algoritmo para la determinación de la verdad de las oraciones en $\mathbb{N}$, contradiciendo ($1$).
Hay un tecnicismo menor que uno necesita para lidiar con ellos, ya que ZFC no es una extensión de la Aritmética de Peano. Para lidiar con eso, para cualquier frase, $\psi$ de Teoría de los números, podemos mecánicamente producir una sentencia de $\psi'$ de la Teoría de conjuntos tales que si $\psi'$ es un teorema de ZFC, entonces $\psi$ que es verdad en $\mathbb{N}$. La sentencia de $\psi'$ se obtiene a partir de la construcción habitual de $\mathbb{N}$, y su adición y la multiplicación, en ZFC.
