Is the statement "Every primitive recursive function is total" provable in $PA$?

Question

In a computer science handout I found online (google: primitive recursive functions Prim Rec Fcns Initial Functions: N), the following claim is made:

Every primitive recursive function is total.

Is this provable in Peano Arithmetic? If so, I would like to see the proof.

Thanks in advance.

Answer 1

Bram28 is right that it takes nontrivial work to express the relevant statement in PA; however, I think they overstate the situation. The task is no harder than talking about provability in PA.

Here's a rough sketch of how it goes. First, we need to represent primitive recursive functions appropriately in the language of arithmetic. We handle this by assigning numbers to ways of building primitive recursive functions. A primitive recursive function can be represented by a finite tree whose nodes are labelled appropriately; I'll leave the exact coding as an exercise, but basically the leaves are labelled with "$0$," "$S$", or "$Proj_i$" for some $i$, and the non-leaf nodes are labelled either "Compose" or "Recurse" (there's a bit more to it of course, but this should give you the idea). Note that this is basically a syntax tree.

Via usual Goedel numbering, we get a formula $\varphi$ defining the set $D$ of numbers which are codes for primitive recursive functions, and a formula $\psi$ defining the relation $Ev(x, y, z)$ interpreted as $$Ev(a, b, c)\iff a\in D\mbox{ and $f(b)=c$ where $f$ is the p.r. function coded by $a$}.$$ (Again, this is analogous to the provability situation: we have a definable set of numbers coding sentences, a definable set of numbers coding proofs, and a definable relation "$x$ is a proof of $y$.")

Totality is now trivial to express: $$\forall x, y[\varphi(x)\implies\exists z(\psi(x, y, z))].$$

So now the only task is proving it. Here we use induction on the rank of the p.r. code $x$; this is no more complicated than other inductions in PA. In particular, every p.r. code has finite rank, so no transfinite induction is needed. (Incidentally, we can also prove single-valuedness - $\psi(x, y, z)\wedge\psi(x, y, z')\implies z=z'$ - and this is of course much easier than the totality statement above.)

Indeed, much less than PA is needed for this; by my estimate, the subtheory $\mathsf{I\Sigma_2}$ should suffice. (I am not sure whether $I\Sigma_1$ can do it; although $\mathsf{I\Sigma_1}$ does prove that every specific p.r. function is total, I'm not sure whether it proves "every p.r. function is total". EDIT: since the set of primitive recursive codes is recursive and the provably total functions of $\mathsf{I\Sigma_1}$ are exactly the primitive recursive functions, $\mathsf{I\Sigma_1}$ clearly can't prove this: basically, whenever a reasonable theory $T$ proves "$f_i$ is total for each $i$," it also proves "$x\mapsto \sum_{i<x}f_i(x)+1$ is total." I suspect however that $\mathsf{B\Sigma_2}$, which is substantially weaker than $\mathsf{I\Sigma_2}$, is enough. EDIT EDIT: $\mathsf{B\Sigma_2}$ is not enough in fact, per
Emil Jeřábek's comment below, since it is $\Sigma_3$-conservative over $\mathsf{I\Sigma_1}$.)

Answer 2

I would say the biggest problem with this is the very symbolization of this statement. Peano Arithmetic does not have symbols to express this in any direct way like $\forall x ((Fun(x) \land PrRec(x)) \rightarrow Total(x))$ ... PA only has symbols for very basic arithmetic: $0$, $s$, $+$, and $*$. These symbols together are called the Language of Arithmetic or $L_A$.

Now, we can try to use expressions of $L_A$ to express other things. For example, to express $x < y$ we can use $\exists z : y = x + s(z)$, and as such we can use $<$ in PA with the understanding that it is shorthand for this expression.

But in order to talk about functions, you really need some set-theoretic primitives: functions (defined over natural numbers) would be special kinds of relations, which are sets of tuplets of numbers ... but we don't have those set-theoretic primitives in PA.

Then again, we can encode tuplets of numbers using single numbers, and we can even do it using $L_A$. This is far from trivial though, and doing any proofs within such an encoding would become a real pain, but I suppose it would be possible.

Symbolizing 'primitive recursive' brings up another issue however: To say that primitive recursive functions are all and only those that are built up by elementary functions like the zero function, successor function (hey, we have that one: $S$!), identity function, and the operations of composition and recursion is ... difficult to say the least. In fact, I am not sure if this is even possible using PA and first-order logic ... maybe you have to start using second-order logic (and again, some set-theory) to really define this as a class of objects that is recursively closed under these operations.

Assuming we can do the symbolization though, I would say the proof is completely trivial: all the basic functions are total, and using composition and recursion preserves totality, and all this would be fairly easy to show once the expressive machinery is in place. But it is getting the claim expressed in a workable format that's the main problem!