TransWikia.com

What subsystem of second-order arithmetic is needed for the recursion theorem?

MathOverflow Asked on November 3, 2021

In its simplest version, the recursion theorem states that for any $minmathbb{N}$ and any function $g:mathbb{N}rightarrowmathbb{N}$, there exists a function $f:mathbb{N}rightarrowmathbb{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?

One Answer

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_1textsf{-Ind}$ over $mathsf{RCA}_0^{star}$. Here $mathsf{RCA}_0^{star}$ is $mathsf{EA}+Delta^0_1text{-}mathsf{CA}+Delta^0_0text{-}mathsf{Ind}$ and $mathsf{RCA}_0=mathsf{RCA}_0^{star}+Sigma^0_1text{-}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 yvarphi(x,y)$$ of $Sigma^0_1textsf{-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 yvarphi(x,y)$ and claim that $forall xexists yvarphi(x,y)$. Using $Delta^0_1textsf{-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_0textsf{-Ind}$. Thus we prove the instance of $Sigma^0_1textsf{-Ind}$.

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

Answered by Fedor Pakhomov on November 3, 2021

Add your own answers!

Ask a Question

Get help from others!

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP