I have a couple of conjectures on recursive functions, that I feel must have been proved or refuted by someone else, but I don't know where to look. In short:
1. The primitive recursive functions form a pseudoinitial small finite product category with natural number object.
2. The partial recursive functions form a pseudoinitial small regular category with natural number object.
The longer version is as follows.
In non closed Cartesian categories, the natural number objects should be defined in a more stable way: $N$ together with $0:1\to N$ and $s:N\to N$ is a natural number object if for each $f:X\to Y$ and $g:Y\to Y$ there is an $h:N\times X \to Y$ such that $h(0,x) = f(x)$ and $h(n+1,x) = g(h(n,x))$. This roughly means that the projection $N\times X\to X$ is a natural number object in the slice over $X$ for every object $X$.
A 0-cell in a 2-category is pseudoinitial if there is an up to isomorphism unique 1-cell to every other two cell.
The first conjecture in full is as follows: The 2-category of small finite product category with a chosen natural number object and finite product preserving functors which preserve the choice of natural number object and all natural transformations, has a pseudoinitial 0-cell. One of these pseudoinitial 0-cells is the category whose objects are powers of $\mathbb N$ and whose morphisms are primitive recursive functions.
The second conjecture says that there is a pseudoinitial object in the category of small regular categories with NNO. This time the category of recursively enumerable sets and recursive functions is such a pseudoinitial 0-cell.
The conjectures fail if non standard models of arithmetic can exclude primitive / partial recursive functions that exists in the standard model: categories of non standard recursive functions could be counterexamples.
Have you seen anything like this before? If so, am I right?
Best Answer
The relevant piece of categorical folklore here is the notion of arithmetic universe.
This was studied by André Joyal in 1973 with the goal of proving Gödel's Incompleteness Theorems in a categorical fashion. However, André never published anything and many people have tried without success to obtain any notes from him. I went to his office in Montréal in 1991 to get them, but just came away with a copy of Lawvere's thesis.
Thanks to Todd for providing the link to Milly Maietti's recent paper, about which I did not know. Since it provides much of the technical information and bibliography, I will just give a more informal description.
An arithmetic universe is essentially set theory as it is taught to computer science students, ie with finite powersets instead of general ones. So it has
The first three of these give a pretopos, which we might think of as the "inorganic" part of finitary set theory and the last is the "organic" part, recursion. This is more than the questioner said, but disjoint unions and lists rather than just numbers are very useful for mathematical constructions.
Another way of seeing this collection of structures is that they are the minimum that is needed to construct the free internal gadget of the same (or pretty much any useful) kind.
I digress here for a little terminological rant. Milly describes the correspondence between the categorical structure and type theory. She, following widespread custom, calls the latter the internal language, but I claim that this name is wrong and would prefer proper language.
A language is a structure capable of mathematical abstraction and internalisation just as much as a group is. For the application to Gödel's theorem, one would like to internalise the equivalence between diagrams and symbols that Milly describes, and so talk about internal categories and internal languages. But the language that she sets out is an external one.
Anyway, one can construct the free arithmetic universe (I really think that introducing 2-categorical notions of initiality here makes things unnecessarily more difficult to understand) inside any arithmetic universe, and in particular in the free one.
Having done that, in the outer category one can construct the equaliser $$ G \rightarrowtail {\bf 1} \rightrightarrows H\equiv{Hom}(1,2), $$ where $H$ is a certain hom-object of the internal category.
The statement of consistency is $G\cong{\bf 0}$ and André's version of Gödel's theorem is that this does not hold. There have been moments in the quarter century since I first heard about this when I thought that I understood why, but now is not one of those moments.
Now that other people, especially Milly, have done the donkey-work to build the infrastructure for this theorem, I wish André would write up the proof of the punch-line.
Milly and I both wrote papers about arithmetic universes for CTCS in Copenhagen in 2004, but I did not present mine because I broke my leg. They nevertheless both appear in the ENTCS proceedings. If you read the footnotes you will see that she and I disagreed about the definition, so I would like to explain that.
I just asked for free monoids, whereas she said that they have to be stable under pullback. This was because I thought that stability could be proved from the other structure. I had overlooked something, but later Milly had an idea for filling in the gap. We studied this idea together in Padova in 2009, but it was not correct. I had other ideas but have not thought about the subject since then. I do not know whether she subsequently found a correct proof.