Every function that is representable in Robinson arithmetic, $\mathsf{Q}$, is computable

Question

I am reading through the proof of this theorem, in particular the one presented in the Open Logic project, where it appears as Lemma 20.3 currently.

The definitions in this text are as follows:

A function $f(x_0,\ldots,x_k)$ from the natural numbers to the natural numbers is said to be representable in $\mathsf{Q}$ if there is a formula $\varphi_f(x_0,\ldots x_k,y)$ such that whenever $f(n_0,\ldots, n_k)=m$, $\mathsf{Q}$ proves

1. $\varphi_f(\overline{n_0},\ldots,\overline{n_k},\overline{m})$ and

2. $\forall y(\varphi_f(\overline{n_0},\ldots,\overline{n_k},y)\rightarrow(\overline{m}=y))$;

and, as far as I understand it, the definition of computable is kept informal and intuitive (it seems to match the description on the Wikipedia article: Computable function § Definition).

---

Lemma. Every function that is representable in Robinson arithmetic, $\mathsf{Q}$, is computable.

The crux of the proof is that proofs/derivations are codable by natural numbers, and hence we can design an algorithm that searches through proofs until it finds one that has the correct conclusion. Here is our "computable algorithm":

• Enumerate derivations in $\mathsf{Q}$ (say, $\mathcal{D}_0, \mathcal{D}_1, \mathcal{D}_2,\ldots$);
• At each step $i$, check if $\mathrm{Conclusion}(\mathcal{D}_i)=\varphi_f(\overline{n_0},\ldots,\overline{n_k},\overline{m})$;
• If so, output $m$, otherwise repeat the process.

My problem with this is that the enumeration of the derivations is not given, and the detail here seems to be brushed over. In particular, if the enumeration is inconvenient, this procedure may never cease(?) Consider, for example, if I were searching for the number $7$ in the natural numbers $\Bbb{N}$, but I only look at the even ones $2$, $4$, $6$, $8$, $10$, $\ldots$ -- I will never find $7$.

Should this detail be highlighted, or is it not a problem?

If it is a problem: how do we know that there is a "convenient" enumeration of the derivations (e.g. the rationals, $\Bbb{Q}$, are enumerable, but the argument that we can do it in a nice way requires a clever arrangement)? Does it make sense to ask what this enumeration is?

Thankyou in advance.

---

Example of a silly enumeration which wouldn't help this proof (just use an axiom of $\mathsf{Q}$ for every natural number):

• $\mathcal{D}_0=\overline{0+0=0}\quad\mathsf{Q4}$

• $\mathcal{D}_1=\overline{1+0=1}\quad\mathsf{Q4}$

• $\mathcal{D}_2=\overline{2+0=2}\quad\mathsf{Q4}$

• $\mathcal{D}_3=\overline{3+0=3}\quad\mathsf{Q4}$

  $\vdots$

Answer 1

Since the derivations are (after all) coded by natural numbers, we may as well say "Work through the natural numbers $1,2,\ldots$", adding the additional check "at each step $i$, check if $i$ codes a derivation (which is primitive recursive). This way we will cover every derivation (to each one there is a corresponding natural number which is eventually checked.