Is every non-empty $\Delta_0$ set provably the range of some primitive recursive function?

Question

Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. It's an easy theorem that there is a primitive recursive function $f:\mathbb{N} \rightarrow \mathbb{N}$ such that $Range(f) = \{n \in \mathbb{N} \mid A(n)\}$. I'm wondering if it's known whether either of the following strengthenings of this theorem are true:

Strengthening 1: Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. Can we find a $c \in \mathbb{N}$ such that $\varphi_c$ is primitive recursive, $\mathbb{N} \models \forall x (A(x) \rightarrow \exists y \varphi_c(y) {\downarrow} = x)$, and $PA \vdash \forall y \exists x (\varphi_c(y) {\downarrow} = x \wedge A(x))$?

Strengthening 2: Suppose $A(x)$ is a $\Delta_0$ formula defining a non-empty set of natural numbers. Can we find a $c \in \mathbb{N}$ such that $\varphi_c$ is primitive recursive, $PA \vdash \forall x (A(x) \rightarrow \exists y \varphi_c(y) {\downarrow} = x)$, and $PA \vdash \forall y \exists x (\varphi_c(y) {\downarrow} = x \wedge A(x))$?

(In the above, "$\varphi_c$" refers to the (partial) recursive function defined by the Turing machine whose Gödel code is c. "$\varphi_c(y) {\downarrow} = x$" is shorthand for a $\Sigma_1$ formula which says that with input y, the Turing machine with Gödel code c eventually halts and outputs x.)

Pedantic Clarification: Typically "$\phi_c(x){\downarrow} = y$" is an abbreviation for "$\exists t M(c,x,y,t)$", where (i) $M(c,x,y,t)$ is a $\Delta_0$ formula and (ii) $\mathbb{N} \models M(c,x,y,t)$ if and only if the Turing machine with Gödel code c halts after t steps on input x and produces output y. Let's call any formula $M$ satisying (i) and (ii) a "computation predicate". By this paper by H.B. Enderton, Strengthening 2 is false for certain choices of computation predicate.

It follows that any argument for Strengthening 2 which assumes that our choice of $\Delta_0$ computation predicate is arbitrary cannot suffice. We also need that PA proves certain facts about our chosen computation predicate. I suspect that any reasonable construction of a computation predicate will work (e.g., whatever construction is used in your favorite recursion theory book), so my question should be phrased more precisely as: is there a computation predicate such that Strengthenings 1 and 2 hold?

Answer 1

I think both strengthening 1 and 2 are true and it is a sketch for proof:

You can construct an effective procedure to find an index $c$ (of a primitive recursive function) for any $\Delta_0$ formula $A(x)$ such that $\mathbb{N}\models \forall x (A(x)\leftrightarrow \exists y \varphi_c(y)\downarrow =x)$ (because for writing a computer program to simulate $A(x)$ we do not need an unrestricted search loop, and all programs in which all search loops are restricted by a primitive recursive bound, computes a primitive recursive function). If we drop the part $\wedge A(x)$ from the condition $PA\vdash \forall y \exists x (\varphi_c(y)\downarrow =x \wedge A(x))$, it becomes the assertion that $\varphi_c$ is a total function and we know that all primitive recursive functions are provably total in $PA$ (in fact $I\Sigma_1$). I think that with a suitable choose of $c$ it would be provable in $PA$ that $\forall x (A(x)\leftrightarrow \exists y \varphi_c(y)\downarrow =x)$ (of course it need an exact proof by induction on complexity of $A(x)$) and if it can be proved, srengthening1 and 2 both hold.

Answer 2

I believe even strengthening 2 is a true statement, that can be proven by "simply" internalizing the proof of the original statement into $PA$.

Proof: Suppose $A(n_0)$ holds for some number $n_0\in\mathbb{N}$. In particular this is provable in $PA$: $$ PA\vdash A(\overline{n_0})$$ where $\overline{n}$ is the numeral representing $n$. This is a simple consequence of completeness of $PA$ (and indeed, much much weaker systems) for $\Delta_0$ sentences.

One can then build the following recursive function $f$:

• $f(0)=n_0$

• $f(n+1)= \begin{cases} n \mbox{ if $A(n)$ holds}\\ n_0 \mbox{ otherwise}\end{cases}$

The first case in the definition of $f(n+1)$ is easily decidable even for a p.r. function. This function is easy to define in $PA$, and it is easy to prove, again in $PA$, that $A(m)$ holds for every $f(n)=m$, and conversely that for every $m$ such that $A(m)$ hold, there is a corresponding $n$ with $f(n)=m$ (take $n=0$ if $m=n_0$ and $m+1$ otherwise).

The rule of thumb is:

$PA$ can prove everything you can prove in an informal argument that doesn't specifically involve consistency of $PA$ (or something stronger).

This has a few exceptions (e.g. the Paris-Harrington argument).