There is a famous story about Kleene trying to define a predecessor function on the natural numbers (or the Church numerals, to be clear) in the lambda calculus, not having any idea how to do it, and then figuring it out while at the dentist. In the same vein, I put forth this puzzle and solution.

Consider the smallest set of endofunctions on \(\mathbb{N}\) containing successor and closed under composition and primitive recursion (that is, if f is in the set, and k is a natural number, then the function \(n \mapsto f^n(k)\) is also in the set). Does this set contain a predecessor function (in the sense of a left inverse for the successor function)?

In other words, we consider those functions which can be built up using the bare structure of a category with natural numbers object, without presuming products or coproducts.

Alright, here is the answer in rot13, consider yourself warned, reading beyond this spoils it.


Vg vf eryngviryl fgenvtugsbejneq gb fubj ol fgehpgheny vaqhpgvba gung nal shapgvba ohvyg hc va guvf jnl rvgure unf n svavgr enatr be cerfreirf fgevpg vardhnyvgvrf. Ab cerqrprffbe shapgvba pna or bs guvf sbez. Guhf, ab cerqrprffbe shapgvba pna or ohvyg.