What's the Category Theoretic Treatment of Induction?

Question

I was doodling around in my discrete math class as my professor talked about induction. I noticed (in a vague way) that if you take the set of propositions $\phi(n), \ n \in \mathbb{N}$ to be objects then it might be possible to make morphisms between objects in the category i.e $f : \phi(n) \to \phi(m)$. For induction, specifically, if we have $f : \phi(n) \to \phi(n+1)$ well defined and at least $\phi(k)$ true for some k, then we necessarily can construct a whole class of morphisms (maybe a trivial category?) between the objects. Can anyone point me towards places that deal with induction at the categorical level? Alternatively, can you explain why what I just said is complete and utter nonsense? Thanks!

Answer 1

There's a few things going on here.

First, the entailment relationship $\vdash$ which states that $\varphi\vdash\psi$ if $\psi$ is provable from $\varphi$ produces a preorder on formulas (assuming $\varphi\vdash\varphi$ is derivable and the rule $\cfrac{\varphi\vdash\psi\quad\psi\vdash\chi}{\varphi\vdash\chi}$ is derivable which they often are or are even taken to be true axiomatically). Every preorder gives rise to a category where there is at most one arrow between any two objects, and so we can think of a "category of propositions".

Next, the way induction is typically handled categorically is via the notion of an initial $F$-algebra. For the natural numbers, we can consider a functor $F(X)\equiv 1+X$. ($F:\mathbf{Set}\to\mathbf{Set}$ say.) The initial $F$-algebra is then an object (set), typically notated $\mu F$, and an arrow (function) $\mathsf{in}:F\mu F\to \mu F$ with the property that for any other pair $(X,a:FX\to X)$ there is a unique arrow (function) $\mathsf{fold}_{(X,a)} : \mu F\to X$ such that $\mathsf{fold}_{(X,a)}\circ\mathsf{in} = a\circ F(\mathsf{fold}_{(X,a)})$. In diagram form, $$\require{AMScd} \begin{CD} F\mu F @>F(\mathsf{fold}_{(X,a)})>> FX \\ @V\mathsf{in}VV @VVaV \\ \mu F @>>\mathsf{fold}_{(X,a)}> X \end{CD}$$

Having a function $1+X\to X$ is the same thing as having a pair $(z,s)\in X\times X^X$. (Why?) The initial $F$-algebra for this particular $F$ is (uniquely isomorphic to) $\mathbb N$ with $\mathsf{in}$ being equivalent to $(0,x\mapsto x+1)$. The $\mathsf{fold}$ function let's us do structural recursion on $\mathbb N$. In particular, given $(z,s)\in X\times X^X$ corresponding to an $F$-algebra $a:1+X\to X$, $\mathsf{fold}_{(X,z,s)}$ satisfies the following constraints: $$\begin{align} \mathsf{fold}_{(X,z,s)}(0) & = z \\ \mathsf{fold}_{(X,z,s)}(n+1) & = s(\mathsf{fold}_{(X,z,s)}(n)) \end{align}$$ (Work out how this is just a restatement of the commutative diagram above.) Initiality states that 1) such a function does in fact exist for any other $F$-algebra, and 2) any function satisfying constraints like the above is, in fact, an instance of $\mathsf{fold}$. (You should prove that the natural numbers really are the initial $F$-algebra in this case.)

But this hasn't given us induction, just structural recursion. However, it turns out (see also this) that we can reduce induction to structural recursion. To do that, we first need to spell out what induction is a bit. The rule for induction on naturals states that for any predicate $P$: $$\cfrac{P(0)\qquad \forall n.P(n)\implies P(n+1)}{\forall n.P(n)}$$ That is, if $P$ holds for the base case ($0$), and given it holds for $n$ it holds for its successor, then $P$ holds for all natural numbers. We can actually generalize this (in fact, categorify) to instead of $P(n)$ being either "true" or "false" for each $n$, $P(n)$ will be a set, i.e. we have the $\mathbb N$-indexed family of sets $\{P(n)\}_{n\in\mathbb N}$. (We regain the binary case by only considering cases where the cardinality $|P(n)|\leq 1$.) We can then read the rule as "if $P(0)$ is non-empty, and for each $n$ there's a function $P(n)\to P(n+1)$, then for every $n$, $P(n)$ is non-empty".

We can build a category, $\mathcal P$, whose objects are pairs of a set $X$ and a family of sets $\{P(x)\}_{x\in X}$. An arrow $(X,\{P(x)\}_{x\in X})\to(Y,\{Q(y)\}_{y\in Y})$ is a pair of a function $f:X\to Y$ and a family of function $\{\varphi_x:P(x)\to Q(f(x))\}_{x\in X}$. I'll leave working out the identity and composition to you (or see the papers). We have a functor $U:\mathcal P \to \mathbf{Set}$ that just projects out the indexing set. We can also lift a functor $F:\mathbf{Set}\to\mathbf{Set}$ to a functor $\widehat F:\mathcal P \to \mathcal P$ such that $F \circ U =U \circ \widehat F$. We also have a functor $\{-\}:\mathcal P \to\mathbf{Set}$ defined via $\{(X,\{P(x)\}_{x\in X})\}\equiv \{(x,p)\mid x\in X\land p\in P(x)\}$ (or, in type-theoretic notation, the dependent sum $\Sigma x:X.P(x)$). This functor has a left adjoint $K_1:\mathbf{Set}\to\mathcal P$ which simply sends $X$ to the $X$-indexed family of singletons which is essentially the "constantly 'true' predicate on $X$". We can then build a functor $\Phi:\mathsf{Alg}_F\to\mathsf{Alg}_{\widehat F}$ which takes an algebra $FX\to X$ to $\widehat F(K_1 X)\to K_1 X$ and this has a right adjoint, $\Psi$, which takes $\widehat F(X,\{P(x)\}_{x\in X})\to (X,\{P(x)\}_{x\in X})$ to $F\{(X,\{P(x)\}_{x\in X})\}\to \{(X,\{P(x)\}_{x\in X})\}$. The upshot is if we start with an $\widehat F$-algebra in $\mathcal P$, $(f,\{\varphi_x\}_{x\in FX}):\widehat F(X,\{P(x)\}_{x\in X})\to(X,\{P(x)\}_{x\in X})$, then $\mathsf{fold}$ gives us an $F$-algebra homomorphism $(\mu F,\mathsf{in})\to\Psi(X,\{P(x)\}_{x\in X})$, which is to say a structurally recursive function $\mu F \to \{(x,p)\mid x\in X \land p\in P(x)\}$ such that if we project out the first component, we get the $\mathsf{fold}_{(X,f)}:\mu F\to X$. And, in particular, if $X=\mu F$ and $f=\mathsf{in}:$ then $\mathsf{fold}_{(X,f)} = id$.

That condensed half of those papers into a paragraph and was probably overwhelming. To illustrate the key parts for $\mathbb N$, let's return to our particular $F$, $FX=1+X$. The lift of $F$ is $\widehat F(X,\{P(x)\}_{x\in X})\equiv(FX,\{Q(z)\}_{z\in FX})$ where $Q(z)\equiv\begin{cases}\{*\},&\text{if }z = \mathsf{inl}(*)\\ P(x), & \text{if }z = \mathsf{inr}(x)\end{cases}$. If we consider an $\widehat F$-algebra whose index function is $\mathsf{in}:1+\mathbb N\to\mathbb N$, then this is exactly a $(1+\mathbb N)$-indexed family of functions $\{\varphi_z\}_{z\in FX}:Q(z)\to P(\mathsf{in}(z))$ which is to say $\varphi_{\mathsf{inl}(*)}:\{*\}\to P(0)$ and $\varphi_{\mathsf{inr}(n)} : P(n)\to P(n+1)$ which is exactly what the premise of the rule for induction is. Given such a $\widehat F$-algebra, we can build an $F$-algebra on $\{(n,p)\mid n\in N\land p\in P(n)\}$, call this $\{P\}$ for brevity, via $z\equiv(0,\varphi_{\mathsf{inl}(*)}(*))$ and $s(n, p) \equiv (n+1, \varphi_{\mathsf{inr}(n)}(p))$. With these definitions, $\mathsf{fold}_{(\{P\},z,s)} : \mathbb N \to \{P\}$ and the earlier reasoning gives $\pi_1(\mathsf{fold}_{(\{P\},z,s)}(n))=n$, or you can check this directly. In other words, $\mathsf{fold}_{(\{P\},z,s)}$ gives us a $p\in P(n)$ for every $n$, which is how we say $P(n)$ is "true" for all $n$.

The above can be generalized quite a bit. The papers refer to general results in fibered categories aka "fibrations", though they illustrate the results using the categories above. Nevertheless, more sophisticated forms of induction such as induction-recursion, induction-induction, and higher inductive types may or may not neatly fit into the generalized scheme.