proving mathematical induction by recursion in type theory?

Question

the principle of mathematical induction says: $$\forall P,\quad [P(0) \land\forall n, P(n)\to P(n+1)]\quad \to \quad \forall n, P(n)$$

The proof I've seen for this is by contradiction: Assume that the conclusion doesn't hold. Then by well-orderedness there is a smallest element $x$ that doesn't satisfy $P$. Hence $x-1$ satisfies $P$, and by the induction step, so does $x$. Contradiction.

However, this proof does not actually have the structure in which I naturally think if induction. I think of induction as using the induction hypothesis to iterate/recurse sequentially over all the numbers, until you've reached the number that you want.

The way I intuitively think of induction corresponds much more to an iterative algorithm. In this sense induction is constructive, and the (classical logical) notion of proving $\phi$ by showing $\phi \to \neg \phi$ seems unnecessary. I would like to think of induction as a constructive idea, as a recursive program (in the sense of "proofs as programs" in the curry-howard isomorphism, without using classical logic).

The idea I came up with is to simply directly define a recursive proof, but it doesn't seem sensible:

$$\begin{align}\text{ind}&:\forall n, P(n)\to P(n+1)\\ \text{base}&:P(0)\\ \text{general}&:\forall n, P(n) := \lambda n, \begin{cases}\text{base}\quad & \text {if } n=0\\ \text{ind}(n-1) (\text{general}(n-1))&\text{else}\end{cases} \end{align}$$

Is there a way to think of induction like this, as a constructive program using recursion? I don't think my particular way of doing it is strictly speaking correct.

Answer 1

Response to Question

Induction is equivalent to well ordering + every element is either 0 or the successor of another element. (Assuming some reasonable set of other axioms)

You've given one direction of the proof already. The other is fairly straightforward. This is in set theory though. We give the proof you've usually seen, because it's easy in set theory to construct a well ordered set where every element is either 0 or the successor of another element. (I don't actually study set theory, but I think this is all true).

I can't figure out what you're trying to define or say in your proposed definition. What is $P$? What are ind, base, and general? Are they terms of a type? Are they labels? Is $P$ a function? Is it a proposition? What is going on here?

The Type Theory

Type theory doesn't start with set theory. Instead we need to define a natural numbers type. I won't go into the details of that here, for those see the natural numbers type article on nLab.

Instead, I'll translate the term elimination rule, which corresponds to induction. Let $sx$ denote the successor of $x$ if $x$ is a natural number.

If for each $x : \newcommand\N{\Bbb{N}}\N$ we have a type $P(x)$, $p_0:P(0)$, and if given $x:\N$ and $p:P(x)$ we can produce a term $p_s(x,p) : P(sx)$, then for any $n:\N$, we can produce a term $\operatorname{rec}^n_P(p_0,p_s):P(n)$.

If $P$ is a proposition type, then this says that if $P(0)$ is true, and if for any $x$ such that $P(x)$ is true, we can prove that $P(x+1)$ is true, then we can prove for any $n\in \N$ that $P(n)$ is true.

By the computation rule, we have moreover that $\newcommand\rec{\operatorname{rec}}\rec^{sn}_P(p_0,p_s) = p_s(n,\rec^n(p_0,p_s))$.

I.e., you can think of $\lambda n:\N. \rec^n_P(p_0,p_s)$ as being a recursively defined function in $\prod_{n:\N} P(n)$.