Una diferencia clave entre la matemática y la teoría de conjuntos es que los "conjuntos" en el reverso de las matemáticas son conjuntos de números naturales. Esto elimina algunos, pero no todos, los problemas dependiente de la elección.
$\mathsf{RCA}_0$ demuestra que si un lineal de pedidos $(L,\prec)$ no tiene menos de elemento, entonces se tiene una infinita disminución de la secuencia.
La prueba es simplemente comenzar con algún elemento $a_0$, y dado $a_i$ deje $a_{i+1}$ ser el primer elemento en el habitual orden de $\mathbb{N}$ tal que $a_{i+1} \not = a_i$$a_{i+1}\prec a_i$. Esta construcción da una computable disminución de la secuencia si $(L,\prec)$ es computable, y la construcción puede ser formalizado en el $\mathsf{RCA}_0$.
La misma prueba se muestra
$\mathsf{RCA}_0$ demuestra que si $(L, \prec)$ tiene un subconjunto con no menos de elemento, a continuación, hay un infinito disminución de la secuencia en $L$.
Por otro lado,
$\mathsf{RCA}_0$ demuestra que si un lineal de pedidos $(L, \prec)$ tiene una infinita disminución de la secuencia, entonces tiene un subconjunto con no menos de elemento.
Esta prueba utiliza un método diferente de la teoría de la recursividad. Suponga $(s_i)$ es un infinito $\prec$-disminución de la secuencia en $L$. El rango de $R$ de esta secuencia es un conjunto de la forma deseada, pero en general el rango de una función no puede ser un conjunto en $\mathsf{RCA}_0$, debido a que el rango corresponde a una r.e. establecer y $\mathsf{RCA}_0$ sólo puede computable conjuntos. Podemos ser inspirados por la prueba de que cualquier infinita r.e. tiene una infinita computable subconjunto.
Todo lo que necesitamos hacer es encontrar algún subconjunto infinito de $R$ que es cofinal en $R$. Para ello, formamos un conjunto $S$, que es el conjunto de
$n \in L$ tal que $n$ es enumeradas en ($s_i$) antes de que cualquier número mayor (en el sentido de $<_\mathbb{N}$) se enumera. Este conjunto puede ser formado en $\mathsf{RCA}_0$, por lo que el $\mathsf{RCA}_0$ demuestra que $S$ existe.
Para mostrar que $S$ es cofinal en $(s_i)$ requiere un poco de inducción argumento de que también puede ser formalizado en el $\mathsf{RCA}_0$. Después de un número $m$ es enumeradas en $S$, en la mayoría de las $m$ números pueden ser descartados antes de que el siguiente número es enumeradas en $S$. Por lo tanto $S$ es infinito. Pero esto significa que si $s_k \in S$ debe haber alguna $j > k$$s_j \in S$, como se desee.
