From the [Wikipedia article on Primitive recursive arithmetic](https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic):



> 
> *"Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. "*
> 
> 
> 


Later:



> 
> *"It is possible to formalise PRA in such a way that it has no logical connectives at all - a sentence of PRA is just an equation between two terms."*
> 
> 
> 


This suggests it may be possible to present primitive recursive arithmetic as a purely algebraic system, in the style of universal algebra.


Is this possible? References?



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](https://www.cs.bham.ac.uk/~sjv/MorrisonAUs.pdf); see particularly chapter 5.) 


This statement may take a bit of unpacking. [Lawvere theories](http://ncatlab.org/nlab/show/Lawvere+theory) 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](http://en.wikipedia.org/wiki/Clone_%28algebra%29). 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](http://ncatlab.org/nlab/show/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](https://nforum.ncatlab.org/discussion/624/natural-numbers-object/?Focus=41234#Comment_41234).) 


