9
$\begingroup$

In its simplest version, the recursion theorem states that for any $m\in\mathbb{N}$ and any function $g:\mathbb{N}\rightarrow\mathbb{N}$, there exists a function $f:\mathbb{N}\rightarrow\mathbb{N}$ such that $f(0)=m$ and $f(n+1) = g(f(n))$. There are many more complicated versions, with multiple variables and parameters and course-of-values recursion and so on. But that’s the gist of it.

Now the recursion theorem, no matter which version of it you take, is a statement in the language of second-order arithmetic. And I'm pretty sure that it’s provable in $Z_2$, i.e. full second-order arithmetic. But my question is, what is the weakest subsystem of second-order arithmetic capable of proving it?

Do different versions of the recursion theorem require different subsystems to prove it?

$\endgroup$
1
  • 2
    $\begingroup$ It looks to me like any such version should be provable in RCA_0. $\endgroup$
    – Wojowu
    Jul 21 '20 at 9:58
11
$\begingroup$

As Wojowu already pointed out $\mathsf{RCA}_0$ proves recursion theorem. You could find a proof in Simpson's book [1], Section II.3.

In fact primitive recursion theorem is equivalent to $\Sigma^0_1\textsf{-Ind}$ over $\mathsf{RCA}_0^{\star}$. Here $\mathsf{RCA}_0^{\star}$ is $\mathsf{EA}+\Delta^0_1\text{-}\mathsf{CA}+\Delta^0_0\text{-}\mathsf{Ind}$ and $\mathsf{RCA}_0=\mathsf{RCA}_0^{\star}+\Sigma^0_1\text{-}\mathsf{Ind}$. So we need to prove in $\mathsf{RCA}_0^{\star}+\mathsf{PrimRec}$ any given instance $$\exists y\;\varphi(0,y)\land \forall x\;(\exists y\;\varphi(x,y)\to \exists y\;\varphi(x+1,y))\to \forall x\;\exists y\varphi(x,y)$$ of $\Sigma^0_1\textsf{-Ind}$, where $\varphi$ is $\Delta^0_0$.

Indeed let us reason in $\mathsf{RCA}_0^{\star}+\mathsf{PrimRec}$. We assume $\exists y\;\varphi(0,y)\land \forall x\;(\exists y\;\varphi(x,y)\to \exists y\;\varphi(x+1,y))$ and claim $\forall x\;\exists y\varphi(x,y)$ and claim that $\forall x\exists y\varphi(x,y)$. Using $\Delta^0_1\textsf{-CA}$ and premise of induction we form the following function $g(x)$: $$g(x)=\begin{cases}\langle y_0,\ldots,y_{n-1},\min\{y_{n}\mid \varphi(n,y_{n})\}\rangle &\text{, if $x=\langle y_0,\ldots,y_{n-1}\rangle$ and}\\ & \text{$\;\;\;$ $\varphi(i,y_i)$, for all $i< n$}\\ 0&\text{, otherwise}\end{cases}$$ We applying primitive recursion to $g$ and put $f(0)=\langle \rangle$. The resulting $f$ maps $n$ to a sequence $\langle y_0,\ldots,y_{n-1}\rangle$ such that $\varphi(0,y_0),\ldots,\varphi(n-1,y_{n-1})$. Note that the latter fact could be verified by $\Delta^0_0\textsf{-Ind}$. Thus we prove the instance of $\Sigma^0_1\textsf{-Ind}$.

[1] Simpson, S. G. (2009). Subsystems of second order arithmetic (Vol. 1). Cambridge University Press.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.