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.

3more comments