Categories of recursive functions
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
- finite limits (products and equalisers),
- pullback-stable disjoint coproducts (disjoint unions),
- pullback-stable effective quotients of equivalence relations,
- pullback-stable free monoids (list objects) in each fibre.
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.
Just as I said that an arithmetic universe is set theory for computation, so I claim that my programme Abstract Stone Duality is its general topology.
To study Wouter's second question we need to consider partial functions and in particular subobjects, which we expect to be recursively enumerable. It is natural to consider these to be the open subspaces.
ASD extends AU by allowing us to consider the topology (lattice of open or RE subspaces) of an object $X$ as another first class object. This is the exponential $\Sigma^X$, where $\Sigma$ is thought of as the Sierpinski space.
The object $\Sigma$ carries its own structure, in particular that of a distributive lattice The language is presented in Sections 4 and 5 of my paper on The Dedekind Reals in ASD with Andrej Bauer.
In this setting, we take the overt discrete object $X$ as our "sets"; these have $\exists_X:\Sigma^X\to\Sigma$ and $=_X:X\times X\to\Sigma$. The full subcategory of overt discrete objects is a pretopos and has free monoids.
Conversely, any arithmetic universe can be embedded as the full subcategory of overt discrete objects in a model of ASD.
To answer Wouter's second question we need to show how general recursion can be interpreted in ASD and conversely that ASD terms can be normalised.
The minimalisation operator $\mu$ takes a partial function $f:N\rightharpoonup 2$ and (possibly) returns the first $n$ for which $f(n)=1$. Partial functions may be rendered total using the lift constructor and then $\mu:(2_\bot)^N\to N_\bot$.
For the converse, given a term $\vdash\phi:\Sigma^N$ with $\vdash(\exists n.\phi n)=\top$, we must find a term $\vdash a:N$ with $\vdash(\phi a)=\top$. This is (the special case for ASD of) the existence theorem.
I should stress that ASD is not functional programming: there is no preferred reduction strategy. It is more like logic programming.
François will no doubt regard the state of the documentation of these results as a "mess".
The classical model of ASD is the category of locally compact spaces, which is rather short of good categorical structure. Of course, it is the purpose of ASD to rectify this.
The technology for cooking up objects of the category, and in particular for giving their recipes in a simple fashion, is still very much under development and has already gone through several versions. The first version was the abstract formulation of Stone duality that the adjunction $\Sigma^-\dashv\Sigma^-$ be monadic, which led to a structure that I called a nucleus.
My construction of the free monoid was a domain-theoretic tour de force in the manipulation of nuclei. If I (had had enough brain-space left and) had thought properly about the stability issue, I believe that I could have used a version of Milly's subsequent idea to prove this using the tools that I had developed in that paper.
At about the same time I was working on computable bases for locally compact spaces, which are rather easier to use than nuclei. I am currently trying to simplify that method with a view to proving a Kleene normal form for ASD terms (of general types) and thereby making the calculus more amenable to computation.
All of this ground to a halt became both of my parents had (different kinds of) dementia, but following their death I hope to get back to work this year.
Regarding question 1.: it's hard to find the statement spelled out in black and white in the literature. Apparently Gavin Wraith proved it in unpublished notes titled "Notes on arithmetic universes and Gödel incompleteness theorems" (1985). (And, one might imagine Joyal proved this as well in his unpublished work.) Happily, a crisp statement is provided in Alan Morrison's very fine Master's Thesis, Lemma 5.11: the functions representable in the initial Skolem theory (the initial object among Lawvere theories in which the generating object is a parametrized natural numbers object) are precisely the primitive recursive functions. He works through the details using a simple programming language of register machines, called PRIM. My understanding is that this is very closely modeled after Wraith's notes; see Maietti's article Joyal's arithmetic universes via type theory, especially her remark just after Definition 4.2.
Hot off the press is Gödel’s Incompleteness after Joyal by Joost van Dijk and Alexander Gietelink Oldenziel. From the introduction:
This article concerns an alternative proof of the first Gödel Incompleteness theorem in the language of category theory due to André Joyal, relying crucially on his newly introduced notion of 'Arithmetic Universe’. In 1973 Joyal lectured on his new proof, and a set of notes were circulated among a small group of workers in topos theory. Unfortunately, the proof has never been made publicly available. This document means to remedy this gap in the literature.