Informally, the connection between induction and recursion is easy to see, especially when using induction to constructively prove the existence of something. For example, when proving that every natural number can be written as the sum of distinct powers of two, an inductive proof might go:
The number $0$ can be written as the empty sum, which is vacuously a sum of powers of two. Now consider $n > 0$, and assume as inductive hypothesis that each $k < n$ may be written as a sum of distinct powers of two. If $n$ is even, then $n = 2k$, and $k$ can be written as a sum of distinct powers of two: therefore so can $n$, simply increase the exponents in the expression for $k$ by 1. If $n$ is odd, then $n-1$ is even, and therefore can be written as a sum of distinct powers of two not including $2^0$. Thus we add $2^0$ to the expression for $n-1$ to obtain a way of writing $n$ as a sum of distinct powers of two. This concludes the proof.
The "recursion" side of this proof goes:
def powers_of_two(n):
if n == 0:
return []
if n % 2 == 0:
return [2*x for x in powers_of_two(n // 2)]
else:
return powers_of_two(n - 1) + [1]
Informally this is all good and well. However, I am wondering if there is a formal version of the statement "induction and recursion are isomorphic", and in what context one might prove such a statement.
In a type system with propositions-as-types, such as Homotopy Type Theory (I will write what follows with that in mind) it is not something you would prove, but something that is built in.
Indeed in Homotopy Type Theory, the type of natural numbers, $\mathbb N$, is given ("freely") by $\mathbb N: \mathcal U, 0: \mathbb N, \mathrm{succ}: \mathbb{N\to N}$ and the following "recursion" principle (I'm using quotes here, because it is as relevant for recursion as it is for induction and since your question is specifically about the distinction between those two, one has to be careful) :
given a family of types $C: \mathbb N\to \mathcal U$, $p:C(0)$ and $f: \displaystyle\prod_{n:\mathbb N}(C(n)\to C(\mathrm{succ}(n))$, we have $rec(C,p,f): \displaystyle\prod_{n:\mathbb N} C(n)$, together with the following "rules" (defining equations) : $rec(C,p,f)(0) \equiv p$, $f(n)(rec(C,p,f)(n)) \equiv rec(C,p,f)(\mathrm{succ}(n))$
Now say you have a type $X$, $p:X$ and a map $h:\mathbb N\to X\to X$ and want to define a map $H:\mathbb N\to X$ such that $H(0)\equiv p$ and $H(\mathrm{succ}(n)) \equiv h(n)(H(n))$, then this recursion principle allows you to do that, by putting $C(n):\equiv X$ and $f(n):\equiv h(n)$, so it recovers what you seem to call recursion.
Now to recover induction say you have a proposition $P(n)$ that you want to prove by induction. But in this setting, $P(n)$ is a type a proving $P(n)$ is finding $p:P(n)$, so all in all you want an element of $\displaystyle\prod_{n:\mathbb N}P(n)$. Now if you have $p:P(0)$ (read "I have a proof of $P(0)$") and $f: \displaystyle\prod_{n:\mathbb N}(P(n)\to P(\mathrm{succ}(n))$ (read "I have a proof of $\forall n, P(n)\implies P(\mathrm{succ}(n))$"), then the induction principle gives you $q: \displaystyle\prod_{n:\mathbb N}P(n)$, that is, a proof of "$\forall n, P(n)$".
So in this context the two principles aren't just "formally similar" or "isomorphic", they're literally the same.
This can be seen category-theoretically as well. Say you have for simplicity a topos $T$ with a natural numbers object $N$, that is $N$ has a global element $0: 1\to N$, and a map $s: N\to N$ that have the obvious universal property. This universal property is literally what encodes recursion, but induction can be found from it too.
Indeed say you have a property $P$ on $N$, which really means (category-theoretically) a map $N\to \Omega$ ($\Omega$ being the subobject classifier). Then saying that "$P(0)$ holds" means essentially "the composite $1\overset{0}{\to} N \overset{P}{\to} \Omega$ is the $\mathrm{true}$ morphism".
Saying "for all $n$, $P(n)\implies P(s(n))$" can be interpreted as "the map $\{n:P\}\to N\overset{s}{\to} N$ factors through $\{n:P\}$" where $\{n:P\}\to N$ is the pullback of $\mathrm{true}: 1\to \Omega$ along $P:N\to \Omega$ (the subobject of $N$ defined by $P$).
This means that we have a commutative square $\require{AMScd} \begin{CD}\{n:P\} @>>> \{n: P\} \\ @VVV @VVV \\ N @>{s}>> N \end{CD}$ which can be extended with a triangle with $1\to N$ and $1\to \{n:P\}$
But now by the NNO property of $N$, this map $\{n:P\}\to N$ has a section (it is a section because the map to $N$ is unique) : however it was a monomorphism, therefore it having a section implies that it is an isomorphism, so $\{n:P\} = N$ and $N\overset{P}{\to} \Omega = N\overset{\mathrm{true}_N}\to \Omega$, in other words "for all $n:N, P(n)$", so we get back the induction principle as an easy corollary of the NNO-property, which is what defines recursion.
I don't know enough about topoi and specifically their internal language, but it is easy to see how the recursion principle can be found from the induction principle even set-theoretically, and I don't think one needs the law of excluded middle (although one may need some more assumptions on $N$, like that $0$ is not in the image of $\mathrm{succ}$, which doesn't follow from NNO-ness; these conditions would be needed to make sure for instance that $N$ is decidable even without the LEM) so there should be a way to do that internally to a topos, but someone with more knowledge should say something about that. If that's true (it definitely is in $\mathbf{Set}$ with LEM), then this shows that (in a topos) the two principles are again similar.
Unfortunately what I did was only give systems where the two principles are similar or can be derived from one another or are the same; I didn't answer the question of "how to state that they are somewhat isomorphic", so you'll have to tell me if that's fine by you !