How can we express “induction is the same as recursion”, formally?

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.

• What are your formal definitions of induction and recursion? – Peter Taylor Jul 3 at 10:27
• @PeterTaylor, that is part of my question: how and in what system could we formally define induction and recursion to prove (or at least state) that they are the same/isomorphic/....? – Mees de Vries Jul 3 at 10:29
• In some type theories with the propositions-as-types philosophy (specifically Homotopy Type Theory) they are literally the same thing. Indeed a proposition is a type in this context, and proving "$\forall n, P(n)$" amounts to finding an element of $\prod_n P(n)$: proving something by induction is, in that context, defining a function by induction. If you're more bent on category theory, you could argue similarly in a category with a natural numbers object and a subobject classifier (e.g. a topos) (cont.) – Max Jul 3 at 11:58
• (cont.) In this context, since you also have a "truth-value object" you can see recursion and induction as being the same principle : the universal property of the NNO – Max Jul 3 at 11:59
• @Max, thank you very much. If you want to flesh your comments out into an answer I'd be happy to accept. – Mees de Vries Jul 3 at 12:59

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 !

• This is exactly the sort of thing I was hoping for! The category-theoretic part was enlightening. I assume the HoTT part was too, but I'll have to take a bit longer to digest that. :-) – Mees de Vries Jul 4 at 7:42
• In the context of categories: I think we can dispense with most of the structure of the topos, no? Really what you need is the natural numbers object (and maybe something like finite completeness, or whatever). Then instead of using $P: N \to \Omega$ at all, you work only with the subobject $\{n: P\}$. The base case is showing that $0 \to N$ factorizes through $\{n:P\} \to N$, and the inductive step is showing that $\{n:P\}\to N \to^s N$ factorizes through $\{n:P\}$, and the conclusion is that $\{n:P\}\cong N$. If you already accept that an NNO encodes recursion, you're done. – Mees de Vries Jul 4 at 7:45
• You are completely right, I said "topos" so I wouldn't have to think about the specific hypotheses, but it's total overkill + they seem to have the converse implication as well, at least heuristically. Also the choice of "topos" was mostly there to see that the two parts of the answer were somehow related (cartesian closed categories are models of typed lambda-calculus which is of course related to type theory) – Max Jul 4 at 8:17

Suppose we have $$x_0 \in X$$ and function $$f: X\to X$$. Then induction will hold on $$(X,f,x_0)$$ iff $$X=\{ x_0, f(x_0), f(f(x_0)), \cdots \}$$. Put another way, every element of $$X$$ but $$x_0$$ itself can be reached by repeated succession (using $$f$$ as the successor function) starting at $$x_0$$.

Example: Let $$X=\{ a, b\}$$, and let function $$f:X \to X$$ be such that $$f(a)=b$$ and $$f(b)=a$$. Notice that apart for $$a$$, there is only one other element of $$X$$, namely $$b$$. And $$b$$ can be reached by single application of the successor function $$f$$ starting at $$a$$. Therefore, induction holds on $$(X,f,a)$$, i.e. $$\forall P \subset X: [a\in P \land \forall x\in P:[ f(x)\in P] \implies P = X]$$

• This is an interesting observation but I don't think it addresses my question; I don't really see recursion in your description (at least, not any more than I already do in any form of induction). – Mees de Vries Jul 4 at 7:46
• @MeesdeVries I guess it depends on what you mean by recursive. – Dan Christensen Jul 4 at 14:06
• @MeesdeVries I found the following definition online: "characterized by recurrence or repetition; relating to or involving the repeated application of a rule, definition, or procedure to successive results." Not what you had in mind? – Dan Christensen Jul 4 at 18:23
• To me recursion is about constructing an object by defining what happens at a base value and at a "successor value", like with a natural numbers object in a category, or the recursion operator from primitive recursive functions. – Mees de Vries Jul 6 at 8:47
• @MeesdeVries How then is $\{ x_0, f(x_0), f(f(x_0)), \cdots \}$ not recursive? The base value is $x_0$, and $f(y)$ is the successor of $y$ for all $y\in X$. – Dan Christensen Jul 6 at 18:10