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?