Primitive recursive arithmetic via universal algebra

According to unpublished notes by Gavin Wraith ("Notes on arithmetic universes and Gödel incompleteness theorems" (1985)), PRA can be described as an equational theory or as a Lawvere theory, and is abstractly characterized as initial among all Lawvere theories whose generating object is a parametrized natural numbers object. (For some details on Wraith's notes, see Alan Morrison's Master's Thesis; see particularly chapter 5.)

This statement may take a bit of unpacking. Lawvere theories are a way of doing universal algebra categorically. Formally, a Lawvere theory is a category $T$ with finite products together with a product-preserving functor $\Phi: \text{Fin}^{op} \to T$ that is a bijection on objects. Here $\text{Fin}$ is the category whose objects are finite cardinals $k = \{0, \ldots, k-1\}$ and whose morphisms are functions between them. The cardinal $1$ generates (the objects of) $\text{Fin}$ by taking finite coproducts of copies of $1$; similarly it generates $\text{Fin}^{op}$ under finite products. Thus the special object $x = \Phi(1)$ generates the objects of $T$ by taking finite products: every object of $T$ is of the form $x^n$. General morphisms $x^n \to x^m$ are $m$-tuples of morphisms $x^n \to x$; we think of the morphisms $x^n \to x$ in $T$ as parametrizing the definable $n$-ary operations of an equational theory. [This categorical description of equational theories is closely related to the concept of clone. If you accept that every equational theory gives rise to a finitary monad on $Set$, then the corresponding Lawvere theory is the category opposite to the finitary Kleisli category consisting of finitely generated free objects. But this is a somewhat hurried discussion which I'll cut short here.] A morphism $F: S \to T$ is a product-preserving functor which is compatible with the given product-preserving functors $\text{Fin}^{op} \to S$ and $\text{Fin}^{op} \to T$.

A parametrized natural numbers object in a category with finite products $\mathbf{C}$ is an object $N$ that comes equipped with maps $z: 1 \to N$ (here $1$ denotes the terminal object, and read '$z$' as 'zero') and $s: N \to N$ (successor), such that given any objects $A, X$ of $\mathbf{C}$ and maps $f: A \to X$, $g: X \to X$, there exists a unique map $h: N \times A \to X$ such that the following diagram commutes:

$$\begin{array}{ccc} A & \stackrel{\langle z \circ !, 1_A\rangle}{\to} & N \times A & \stackrel{s \times 1_A}{\leftarrow} & N \times A \\ & f \searrow & \downarrow h & & \downarrow h \\ & & X & \underset{g}{\leftarrow} & X \end{array}$$

(here $!$ denotes the unique map $A \to 1$). This axiom is what you need to internalize primitive recursion in a category with finite products.

So now the Lawvere theories we are interested in are those for which the generator $x = \Phi(1)$ is a parametrized natural numbers object. A concrete example of such is the full subcategory of $Set$ whose objects are finite powers $\mathbb{N}^n$ of the set of natural numbers. For that matter, for any category with finite products and a natural numbers object $N$ (for example, a Grothendieck topos), you can cook up a Lawvere theory by considering the full subcategory consisting of finite powers of $N$. Or, the subcategory needn't be full: just retain enough arrows to retain finite product structure and primitive recursive structure guaranteed by the axiom of parametrized NNO's.

Finally, we are interested in the initial such Lawvere theory. As is the case with any initial algebraic object, the explicit construction is syntactic: we start with $N$ and $z: 1 \to N$ and $s: N \to N$ and use the axiom of parametrized NNO's together with finite cartesian product structure (products of copies of $N$, projection maps, diagonal maps) and categorical composition to generate formally all the arrows. (As a simple exercise, show how to construct formal addition and formal multiplication on $N$.) One thing to check is that morphisms $1 \to N$ (the definable constants of the equational theory, considered up to provable equality) correspond bijectively to standard natural numbers.

If $T$ is the initial such theory (which according to Wraith is PRA), with generator denoted $N$, and if $f: T \to Set$ is the unique Lawvere theory morphism sending $N$ to $\mathbb{N}$, then the functorial map $\hom_T(N^n, N) \to \hom(f(N^n), f(N)) \cong \hom(\mathbb{N}^n, \mathbb{N})$ is a surjection onto the total $n$-ary primitive recursive functions on the standard natural numbers. Is is an injection? No. For example, consider the primitive recursive "function" $G: N \to N$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in ZFC, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic living in the ZFC model $Set$, $G$ would be sent to the constant $0$ function mapping $\mathbb{N} \to \mathbb{N}$. But we could equally consider a model $\mathcal{M}$ of $ZFC + \neg Con(ZFC)$ and its natural number object $\mathbb{N}_\mathcal{M}$, in which $G$ would not be sent to the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $T$. (Thanks to Zhen Lin Low for supplying this argument, here.)


This is not an answer, just two hopefully interesting remarks, but much too long for a comment:


First, a simple-but-perhaps-interesting remark: since the rules governing primitive recursion (in stark contrast to general recursion!) are all equational, you can view the collection of primitive recursive functions as a many-sorted algebra in the variety with sorts $\{s_i: i\in\omega\}$ (the arities of the prim. rec. functions), language $\{0, S, \circ_{i, j}, \pi_{i, n}\}$ (the constant function $x\mapsto 0$, successor, composition ($i$-ary functions plugged into $j$-ary function), and projection ($n$-tuple onto $i$th coordinate)), satisfying the obvious equations. A word of caution: since this is a many-sorted variety, things are a bit weird, and this isn't exactly classical universal algebra anymore.

There are, of course, lots of other varieties in this language, including the trivial variety (one element of each sort). Of a given algebra, we can ask about its actions on the natural numbers, in the obvious sense (if this is what we care about, we may even want to add constant standing for the constant functions to our language). In this case, the standard set of primitive recursive functions is clearly the smallest algebra which admits an action on the naturals. (This idea, of which algebras in a variety are compatible with a certain existing structure, has been explored a bit; for example, for topological compatibility with the real line see http://people.math.sc.edu/mcnulty/preprints/hilbert.pdf.)

I don't immediately see a way to get rid of the many-sorted nature of this setup, but there might be one.

Obviously, this isn't really about $PRA$ itself, but it might be interesting to you.


Second: I'm not sure how related this is to what you are asking, but you might be interested in functional interpretations in proof theory.

Basically, the goal of a functional interpretation is to associate to a first-order theory of arithmetic a many-sorted theory whose objects of higher sorts "unwind" complicated statements about lower-sort objects - specifically, every first-order formula will be equivalent to a quantifier-free formula about higher-order objects.

The original example of a functional interpretation is Goedel's system T (the Dialectica interpretation): http://en.wikipedia.org/wiki/Dialectica_interpretation.

On that note, it's worth pointing out that there are higher-order versions of the primitive recursive functions: http://en.wikipedia.org/wiki/Primitive_recursive_functional. These are used in the study of functional interpretations.

Again, this isn't really related to your question, but you might find it interesting.