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?

  • 2
    $\begingroup$ I'm curious how you formalize partial functions in 2. $\endgroup$ – François G. Dorais Apr 4 '13 at 14:55
  • 3
    $\begingroup$ I think 1 is also sensitive to formalization, but not as much. The problem is not that functions can be omitted but that they can be accidentally identified. For example, there is a p.r. function $c$ such that $c(x) = 0$ unless $x$ is a Gödel code of a PA-proof of $0=1$, in which case $c(x)=1$. In the standard model, $c$ is the identically $0$ function. If these are actually the same in your category, then it is not initial since there are models where $c$ is not identically $0$. However, this is can be fixed using intensional equality instead of extensional equality. $\endgroup$ – François G. Dorais Apr 4 '13 at 15:04
  • 3
    $\begingroup$ No, a nonstandard Gödel code doesn't give a proof in any reasonable sense. $\endgroup$ – François G. Dorais Apr 4 '13 at 16:46
  • 2
    $\begingroup$ So for 2, you're just looking at a regular category with finite limits (or just products?) and a parametrized nno? (Disjoint coproducts too?) $\endgroup$ – François G. Dorais Apr 4 '13 at 16:48
  • 2
    $\begingroup$ @Francois: I assume regular categories have finite limits. The definition of NNO is in the question, but 'parametrized' sounds like a good description. $\endgroup$ – Wouter Stekelenburg Apr 5 '13 at 7:04

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.

| cite | improve this answer | |
  • 5
    $\begingroup$ Of course, one source for this is tac.mta.ca/tac/volumes/24/3/24-03abs.html $\endgroup$ – Todd Trimble Apr 7 '13 at 15:53
  • 2
    $\begingroup$ Thank you so much for writing this! I was very interested in all this a few years ago but I couldn't resolve some issues and I eventually (but reluctantly) just walked around them. The main one was exactly that: how much do you need to prove the stability of free monoids. Mind you, at that time, it wasn't even clear whether Joyal's (mythical) arithmetic universe had any free monoids beyond the nno. Anyway, if you, Maietti (or anyone else) figure this mess out, I really want to know! $\endgroup$ – François G. Dorais Apr 7 '13 at 22:58
  • $\begingroup$ I should make it clear that there is no disagreement between Milly and me as to what properties an arithmetic universe must have: certainly the free monoids should be stable. If you are looking at them "from the inside", ie what you can do with an AU when you have one, that settles the question. The point is economy of what you need to check if you're constructing one, as I was in my 2005 CTCS/ENTCS paper. Once you have some "organic" "set theory" you can bootstrap useful stuff from parsimonious basic assumptions. However, I suspect that this question is still open. $\endgroup$ – Paul Taylor Apr 8 '13 at 9:08
  • 1
    $\begingroup$ Francois, what is it that you regard as a mess? Maybe you can try to persuade Andre to write up Godel's theorem, but surely we should thank Milly for doing what she has done. Yes, there was ambiguity about whether an AU should have free monoids or just N, but the consensus now is for monoids. As to whether they are stable as a theorem, that is my "fault", but this is just an open conjecture like any other. $\endgroup$ – Paul Taylor Apr 10 '13 at 11:33
  • 2
    $\begingroup$ I have just had an email from Milly saying "The question if free monoids are enough to get parameterized list objects is still open to me". Her papers are at www.math.unipd.it/~maietti/papers but unfortunately there are only filenames and no index.html. $\endgroup$ – Paul Taylor Apr 23 '13 at 8:23

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.

| cite | improve this answer | |

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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.