7
$\begingroup$

From the Wikipedia article on 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?

$\endgroup$
4
  • $\begingroup$ It depends on what you want to study, equational theories of ( certain subclasses of ) rings, or certain theories which involve the total or even partial order as it relates to the operations. There are other complexity issues as well, e.g. bounded arithmetic. Samuel Buss is a name associated with this latter study. $\endgroup$ Commented Feb 20, 2015 at 1:40
  • 1
    $\begingroup$ I don't understand the question. The Wikipedia page tells you how to present PRA as an equational theory, and the history of this presentation. What else remains to be answered? $\endgroup$ Commented Feb 20, 2015 at 10:08
  • $\begingroup$ Would 'peano-arithmetic' fit this question? a tag specific to the "arithmetic foundations" aspect of the question is missing, and browsing questions relative to PRA gave no consistent obvious solution. $\endgroup$
    – YCor
    Commented Apr 24, 2020 at 9:19
  • $\begingroup$ @YCor It's not absolutely precise, but it might be a reasonable stopgap. I'll think about it. $\endgroup$ Commented Apr 24, 2020 at 9:38

2 Answers 2

10
$\begingroup$

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.)

$\endgroup$
4
  • $\begingroup$ Todd, is there any significance to $s \times 1_A$ and $g$ being backwards? $\endgroup$ Commented Dec 6, 2016 at 11:56
  • $\begingroup$ @goblin May be just the way I think. For an NNO, I often write $1 \stackrel{0}{\to} \mathbb{N} \stackrel{s}{\leftarrow} \mathbb{N}$ to suggest we are thinking of the $\mathbb{N}$ in the middle as equipped with coproduct inclusions, realizing an isomorphism $1 + \mathbb{N} \cong \mathbb{N}$. $\endgroup$ Commented Dec 6, 2016 at 12:48
  • $\begingroup$ Actually, that's exactly how I think about it; see example 2 here. $\endgroup$ Commented Dec 8, 2016 at 8:33
  • $\begingroup$ Can one explain how to prove the assertion that the morphisms $1\to N$ correspond bijectively to standard natural numbers? I understand one can assign, using the Lawvere theory morphism $f$, a unique natural number to any such morphism, and that one can construct a morphism for any natural number (inductively, as $s\circ \dots \circ s\circ 0$). But I am not sure how one can prove that the functorial map $\hom_T(1, N) \to \hom(1, \mathbb{N})\cong \mathbb{N}$ is injective, so a bijection. $\endgroup$ Commented Nov 7 at 12:21
3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .