Oh, I see, defining the problem away! Neat. (I think you mean “with $1$ replaced by an arbitrary $n$”)

I will edit the entry to make this more clear.

]]>Interesting point. I notice, though, that the claim as stated only says that

a morphism $k \to 1$ of the Lawvere theory is a function $\mathbb{N}^k \to \mathbb{N}^1$ belonging to the class [of partial recursive functions]

whereas you seem to be objecting to a version of this statement with $k$ replaced by an arbitrary $n$. It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms $k\to 1$, and then *define* the morphisms $k\to n$ to be what they have to be to make it a Lawvere theory, namely $n$-tuples of partial recursive functions $\mathbb{N}^k \to \mathbb{N}^1$ — which, as you note, are not the same as single partial recursive functions $\mathbb{N}^k \to \mathbb{N}^n$.

Put differently, partial recursive functions “naturally” form a cartesian operad, which we can then make into its equivalent Lawvere theory.

]]>I think the claim (here) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product $\mathbb{N}^k$ is not the product in any category whose objects are finite powers of $\mathbb{N}$ and whose morphisms are some class of partial functions closed under composition and including projections and diagonals. There is a unique partial function $\mathbb{N}^m \to \mathbb{N}^{k+l}$ induced from a pair of partial functions $\mathbb{N}^m \to \mathbb{N}^k$ and $\mathbb{N}^m \to \mathbb{N}^l$, but the usual triangles don’t commute! The cartesian product here is only a ’restriction product’, namely a lax product in the locally posetal 2-category determined by the given category of partial functions.

Since the primitive recursive functions are total and include projections, that’s not a problem.

I’m not sure what I want to put in place of the current statement: a disclaimer? an explanation of what goes wrong? An attempt at outlining a generalisation of a Lawvere theory?

]]>Sorry, yes, I came from the café, and your nice definition of Ackermann in the free ccc! That was indeed the context of my comment #4, which should perhaps have gone on the cafe instead.

]]>Yes, thanks. I don’t know if you looked carefully at the nLab article, but I did record a detailed proof there that Ackermann cannot live in the standard category whose objects are finite powers $\mathbb{N}^n$ in $Set$ and whose morphisms are primitive recursive maps between them. If it lived in the initial category with products and a *parametrized* NNO, then you could transfer it along the product-preserving map over to the standard category. Meanwhile, at the Café I explicitly wrote down a definition of Ackermann in the free CCC with NNO, which I assume you saw (because otherwise, it’d be quite a coincidence that you started this thread just now), but in case not, it’s here.

Meanwhile, I’ve added another Café comment here.

]]>Incidentally, my understanding of the fact that Ackermann is not definable in the free category with products and a natural numbers object, but is definable in the free ccc with a natural numbers object, is that the former category contains functions with termination ordinal $\lt \omega^\omega$, whereas the latter contains functions with termination ordinal $\lt \epsilon_0$. (In the sense of ordinal analysis.)

]]>Thanks, you’re right, they put an extra f in the inductive step. This is the version I learnt as a student, and also the version on wikipedia. I don’t know a case for using one or the other, though.

]]>Thanks, Sam. The definition I wrote comes from the lecture notes of Stephen Simpson that I put in the references.

Let’s see: if $A_0(m) = m+1$, then I seem to get $A_1(m) = A_0^m(1) = m+1$ as well. So maybe those other references use a slightly different recursive rule?

]]>Comment about Ackermann function. I don’t know what Ackermann originally wrote, but most texts use A_0(m)=m+1, if I understand correctly.

]]>