Provably total functions in $\mathsf{Q}$ I was interested in the relations between induction and recursion, and so a natural question (to my mind, anyway), was how much we can prove without appealing to induction, i.e. which functions are provably recursive in $\mathsf{Q}$ (Robinson Arithmetic). To recap, a function $f$ is provably recursive in an arithmetic theory $T$ iff there is a $\Sigma_1$ formula $\phi$ in the language of $T$ such that (i) $f(n)=m$ iff $T \vdash \phi(n, m)$ and (ii) $T \vdash \forall x \exists !y \phi(x, y)$.
Now, I thought that a function was provably recursive in $\mathsf{Q}$ iff it is a recursive function. My reasoning was as follows. A function is recursive iff it is representable in $\mathsf{Q}$, and, it is a well-known result (see this article for discussion) that representability in $\mathsf{Q}$ is equivalent to strong representability in $\mathsf{Q}$ which is equivalent to being provably total in $\mathsf{Q}$.
However, I immediately became confused, because, if I understood Fairtlough and Wainer ("Hierarchies of Provably Recursive Functions") correctly, the provable recursive functions of $\mathsf{I}\Sigma^0_1$ are exactly the primitive recursive functions. Since $\mathsf{I}\Sigma^0_1$ extends $\mathsf{Q}$, it is stronger than $\mathsf{Q}$, and therefore cannot prove that fewer functions are total. To add to the mess, I remember (but may be misremembering) Nelson claiming that $\mathsf{Q}$ cannot prove that exponentiation is total. If that is so, then obviously $\mathsf{Q}$ cannot prove that all recursive functions are total. But, again, I may be misremembering Nelson's claim.
So, on the one hand, it seems that every recursive functions is provably total in $\mathsf{Q}$, but, on the other, it seems that not even all primitive recursive functions are total in $\mathsf{Q}$. Clearly I have gone wrong somewhere.

Question 1: So, what are the provably total functions in $\mathsf{Q}$?

And, depending on the answer to this question, I have one or the other further question:

Question 2a: If $\mathsf{Q}$ does not prove, for every recursive function, that it is total, then what have I misunderstood about the equivalence between representability in $\mathsf{Q}$ and being provably total?


Question 2b: If every recursive function is provably total in $\mathsf{Q}$, then what have I misunderstood about $\mathsf{I}\Sigma^0_1$? Is there a different definition of provably total in play?

Any help in sorting this out would be greatly appreciated.
 A: The issue here is a subtle difference between two notions: "provable totality" (in the sense of Salehi) and "provable recursiveness." The former coincides with recursiveness, but the latter does not. Consequently, in my experience - and this explains my parenthetical above - both "provably total" and "provably recursive" are used to refer to the narrower class of functions.

Here are the relevant definitions:

*

*A function $f$ is (Salehi-)provably total (and these are the functions Salehi discusses) iff there is some formula $\eta$ such that:

*

*$T\vdash$ "For each $x$ there is exactly one $y$ such that $\eta(x,y)$."


*For each $a\in\mathbb{N}$ we have $T\vdash\eta(\underline{a},\underline{f(a)})$.




*A function is provably recursive (and these are the functions you describe in your OP) iff the above holds for some $\Sigma^0_1$ formula $\eta$.
The argument Salehi gives does indeed show that every total recursive function is provaby total in $\mathsf{Q}$. However, it does not show the same for provable recursiveness, and indeed provable recursiveness and (genuine) total recursiveness never coincide for reasonable theories since we can always diagonalize against proofs in such theories.
Note that we can similarly divide up the various representability notions into their "boldface" and "$\Sigma^0_1$" versions; however, this doesn't actually change anything now (and it's a good exercise to verify this).
Precisely because of the coincision above, provable totality in Salehi's sense isn't very interesting, and so these days (in my experience at least) "provably total" is usually used as a synonym for "provably recursive;" for example, see Hajek/Pudlak Remark (IV)$3.2$ or this nice survey of Weiermann. In particular, when we say "The provably total functions of $\mathsf{I\Sigma_1}$ are the primitive recursive functions," we're referring to provable recursiveness.

So what exactly are the provably recursive functions in $\mathsf{Q}$? Well, I can't actually seem to find an answer to this question. But this isn't too surprising I think: since $\mathsf{Q}$ is so weak this is a less interesting question than for stronger arithmetic theories.
That said, here's what I know (for simplicity I'll refer to functions rather than appropriate $\Sigma^0_1$ formulas). Let $\mathfrak{Q}$ be the class of $\mathsf{Q}$-provably recursive functions. The most obvious members of $\mathfrak{Q}$ are the "termlike functions," by which I mean the functions of the form $$f(x)=\begin{cases}
p_1(x) & \mbox{ if }\varphi_1(x)\mbox{ holds }\\
p_2(x) & \mbox{ if }\varphi_2(x)\mbox{ holds}\\
...\\
p_n(x) & \mbox{ if }\varphi_n(x)\mbox{ holds}\\
\end{cases}$$
for some sequence $p_1,..., p_n$ of polynomials and some sequence $\varphi_1,...,\varphi_n$ of $\Delta^0_1$ formulas which $\mathsf{Q}$ proves partition the universe. Trivially each termlike function is $\mathsf{Q}$-provably recursive.
However, this doesn't exhaust $\mathfrak{Q}$: we can to a certain extent get around the weakness of $\mathsf{Q}$ by looking at tame initial segments. Basically, say that a number $x$ is tame if "enough arithmetic" holds below $x$ (e.g. for all $y,z<x$ we have that $y^z$ is defined - it's a good exercise to pin down a sufficient notion of tameness here). Tameness is a $\Delta_1$ property, and $\mathsf{Q}$ proves that the set of tame numbers is an initial segment of the universe. So we can define a function $g$ which on the "tame part" diagonalizes against termlike functions and is always $0$ on the "wild part." Since every standard natural number is tame, we will in fact have that $g$ is not termlike.
Of course, this is pretty silly since this $g$ is eventually equal to a termlike function. So let's leap ahead:

For $T$ a theory of arithmetic possibly containing more funtion symbols than just $+$ and $\times$ (e.g. $\mathsf{PRA}$ or $\mathsf{PA}$ + a primitive for exponentiation), say that a $T$-provably recursive function $f(x_1,...,x_n)$ is $T$-special iff for every term $t(x_1,..., x_n, y_1,...,y_k)$ we have $$T\vdash\forall a_1,...,a_k\exists b\forall c_1>b, ..., c_n>b[f(c_1,...,c_n)\not=t(c_1,...,c_n, a_1,...,a_k)].$$ Basically, the $T$-special functions are those which are provably eventually different from each term function (with parameters allowed). Write "$\mathfrak{Spec}(T)$" for the set of $T$-special functions.

Before going forward, let me make a couple quick observations:

*

*We could also look at what happens if we replace "cofinally often" with "coboundedly often," but this doesn't seem as natural: for example, taking $T=\mathsf{PA}$ the function sending $x$ to $2^x$ if $x$ is even and to $0$ otherwise would count as special by this latter definition, while in my opinion it clearly shouldn't.


*We have to be careful in how we interpret $\mathfrak{Spec}(T)$: we can have a conservative extension $S$ of $T$ with $\mathfrak{Spec}(S)\subsetneq\mathfrak{Spec}(T)$ (consider expansions by definitions). So in order to treat $\mathfrak{Spec}(T)$ as a measure of the strength of $T$, we need to restrict attention to a single language - say, $\{+,\times\}$. Once we've done that, however, things are reasonably nice since if $T$ and $S$ are theories in the same language then $T\subseteq S$ implies $\mathfrak{Spec}(T)\subseteq\mathfrak{Spec}(S)$.
In my opinion, within a limited language like $\{+,\times\}$ a paucity of special functions can reasonably be considered a kind of weakness. And so this raises a natural question:

Does $\mathfrak{Spec}(\mathsf{Q})=\emptyset$?

I would tentatively interpret a positive answer to this question as a precise sense in which $\mathsf{Q}$-provable recursiveness is pretty trivial. But I don't know whether this is in fact the case; since it seems interesting, I've asked about it here.
