Si $HA \vdash (\forall n) [ A(n) \lor \lnot A(n)]$, entonces, en particular, para cada número natural $m$ tenemos que
$$
HA \vdash Un(\ulcorner m\urcorner) \lor \lnot Un(\ulcorner m \urcorner)$$
Aquí $\ulcorner m\urcorner$ está cerrado el plazo $S(S(S(S(\cdots S(0)\cdots)$ $m$ apariciones de $S$.
Ha es la disyunción de la propiedad: si $\phi,\psi$ son frases y $HA \vdash \phi \lor \psi$ $HA \vdash \phi$ o $HA \vdash \psi$. Por lo tanto, si $HA \vdash (\forall n) [ A(n) \lor \lnot A(n)]$ a continuación, para cada una de las $m$,
$$
HA \vdash Un(\ulcorner m\urcorner)
$$
o
$$
HA \vdash \lnot Un(\ulcorner m\urcorner)
$$
Los axiomas de HA son todos los enunciados verdaderos acerca de los números naturales, por lo que HA sólo demuestra una de esas dos fórmulas, y el que se demuestra que es cierto acerca de los números naturales.
Porque HA es un efectivo de la teoría, dado $m$ podemos enumerar derivaciones en HECTÁREAS hasta encontrar una derivación de $A(\ulcorner m\urcorner)$ o una derivación de $\lnot A(\ulcorner m\urcorner)$, y que nos dirá si $A(\ulcorner m\urcorner)$ mantiene. Por lo tanto, el conjunto de $\{m : A(m) \}$ debe ser recursivo.
No es necesario en esta prueba para asumir la $A$ es cuantificador libre. La fórmula $A$ puede ser arbitrariamente un complicado fórmula en el lenguaje de la HA. La única suposición es que la $HA \vdash (\forall n)[A(n)\lor \lnot A(n)]$.
De hecho, un resultado más fuerte que se conoce. Si $B(n,m)$ tiene dos variables libres, y $HA \vdash (\forall n)(\exists m) B(n,m)$, entonces existe una función computable $f$ tal que $B(n,f(n))$ mantiene para cada número natural $n$. Como en el anterior, $B$ puede ser arbitrariamente un fórmula complicada. Este fuerte resultado requiere más que sólo las técnicas básicas de arriba, y por lo general es probado con el método de realizabilidad.
