This post originally appeared on LocalCharts.
David Corfield made a very interesting observation: the three types of logical reasoning of Peirce’s, deduction, induction, abduction, correspond to three very elementary operations in category theory: composition, extension and lifting.
Let’s see what this means.
- Deduction. I observe \(A \to B\) and \(B \to C\). Then, by modus ponens, I can conclude \(A \to C\).
- Induction. I observe \(A \to B\), and also \(A \to C\). I conclude \(B \to C\).
- Abduction. I observe \(A \to C\) and \(B \to C\), I conclude \(A \to B\).
Clearly induction and abduction are not valid reasoning rules! But they are rules reasoners have to use if they want to make new knowledge out of the data they have. For instance, we use induction all the time, both ‘unconsciously’ when we learn facts from the world (‘I said the word mama, mama smiled, therefore the word mama makes mama smile’) and very consciously in science (‘We collected these data samples, and we infer a functional relationship of this kind’).
In fact you can see how the data for induction is literally the data of an indexed family of pairs \((a_i, b_i)_{i \in I}\), and the result of induction is to build a map \(f:A \to B\) such that \(f(a_i) = b_i\) for each \(i \in I\): it’s an interpolation problem!
But, again, this isn’t a valid logical rule: there might not be such \(f\), since e.g. there might \(a_i=a_j\) with \(b_i \neq b_j\) (so no function can interpolate the points), or even if the points are possible to interpolate, there’s just so many different functions that do so!
So to give some logical credence to induction, we have to find a way to at least solve the second problem, and thus make induction the more conservative conclusion we can make having observed that \(I \to A\) and \(I \to B\). In other words, solve the extension problem in a universal way.
This is the job for a Kan extension!
This means, first of all, moving from the unspecified 1-category I’ve been working on so far to an unspecified 2-category. Then a (right) Kan extension looks as follows:
The dashed arrow and the filling 2-cell are terminal at their job: every other such pair factors uniquely through them:
So this is the sense in which \({\rm ran}_a b\) is the ‘least general solution’ to this extension problem: every other solution factors through it. The right Kan extension only contains what’s justified to believe about the implication \(A \to B\).
There is also a nice formula for computing \({\rm ran}_a b\) in reasonable cases, if it exists: \[{\rm ran}_a b(a) = {\large \textstyle \int _{i:I} \int _{p:A(a,a_i)} b_i}\] An interpretation of this formula is that the value of the interpolation of \((a_i,b_i)_i\) at some given point \(a\) is the limit over \(i\) of all the values \(b_i\) which lie over an \(a_i\) related to \(a\). In other words, we ‘fill the gaps’ in the data by taking limits.
Of course this is far from what actual interpolation looks like, a problem which requires spending a bit more time thinking about what are the right generalizations for all these concepts to a ‘quantitative’ setting.
Still, we can test the proposed definition of ‘induction’ on something else: Peano induction! Is it a special case of induction? I claim it is.
What is mathematical induction? We are given a predicate \(\varphi : \mathbb {N}_0 \to 2\), where \(\mathbb {N}_0\) is the set of natural numbers, which we know satisfy \(\varphi (k) \to \varphi (k+1)\) and \(\varphi (b)\) for some \(b \in \mathbb {N}\). We conclude that \(\forall n \in \mathbb {N},\ (b \leq n) \to \varphi (n)\).
So let’s work in \(\bf Pos\), the 2-category of posets. We have a map \(i:\mathbb {N}_0 \to \mathbb {N}\) embedding the set of naturals in the poset of naturals. We have a predicate on \(\mathbb {N}_0\). We form its right Kan extension:
Such a Kan extension has form \[{\rm ran}_i \varphi (k) = \forall {n \in \mathbb {N}},\ (k \leq n) \to \varphi (n)\] which reads as ‘\({\rm ran}_i \varphi (k)\) is true when \(\varphi \) is always true from \(k\) onwards’.
How is this any useful for induction? Well, when \(\varphi \) satisfy the induction property then \(\varphi :\mathbb {N}_0 \to 2\) actually lifts to \(\mathbb {N} \to 2\), since \(\varphi (k) \to \varphi (k+1)\) is a monotonicity property. Then by universal property of the Kan extension, there is a (necessarily unique in this context) map into it:
This map corresponds to the implication \[\forall k \in \mathbb {N},\ \varphi (k) \to \forall {n_0 \in \mathbb {N}_0}\ (k \leq n_0) \to \varphi (n_0)\] which is equivalent to \[\forall k \in \mathbb {N}, \forall n \in \mathbb {N}, \varphi (k) \land (k \leq n) \to \varphi (n).\] Then given a base case \(\varphi (b)=\top \), we can conclude \[\forall n \in \mathbb {N}, (b \leq n) \to \varphi (n).\] So induction is a form of... induction after all!
What I really proved above is that for any poset \(W\), right extension along the inclusion \(i:W_0 \to W\) gives you well-founded induction. Indeed, for general posets we have \[{\rm ran}_i\varphi (v) = \forall w \in W, (v \leq w) \to \varphi (w)\] and ‘functoriality’ of \(\varphi \) is \[v \leq w \implies \varphi (v) \to \varphi (w)\] Thus the universal map \(\varphi \to {\rm ran}_i\varphi \) says that \[\forall v \in W\!,\ \varphi (v) \to (\forall w \in W, (v \leq w) \to \varphi (w))\] which is easily seen to be equivalent to \[\forall w \in W\!,\ (\forall v\in W\!, (v \leq w) \to \varphi (v)) \to \varphi (w).\] Of course this extends to categories as well, where you’d get some kind of ‘proof-relevant’ induction. One can give the same definition anywhere you can talk about right Kan extensions and the inclusion \(W_0 \to W\).