A characterization of recursive functions via arithmetical formulas Let $\mathcal{L}_A$ be the first order language of arithmetic with $+,\times,S$ and $0$. Let $\mathfrak{N}$ be the standard model of arithmetic. An $n$-ary relation $R$ on natural numbers is said to be definable in $\mathfrak{N}$ iff there is a formula $\varphi(x_1,\ldots,x_n)$ of $\mathcal{L}_A$ such that for all numbers $k_1,\ldots,k_n$:
\begin{equation}
R(k_1,\ldots,k_n)\longleftrightarrow\mathfrak{N}\models\varphi(\overline{k_1},\ldots,\overline{k_n})\,,
\end{equation}
where for a natural number $n$, $\overline{n}$ is the numeral denoting $n$.
It is true that recursively enumerable relations are exactly these which are definable in $\mathfrak{N}$ by $\Sigma_1$-formulas (i.e. these formulas in which only existential quantifiers are unbounded).
By the graph of an $n$-ary function $f$ from natural numbers to natural numbers I mean (standardly) the $(n+1)$-ary relation $\{(k_1,\ldots,k_n,k_{n+1})\mid f(k_1,\ldots,k_n)=k_{n+1}\}$.
My question is if it is true that the class of all recursive functions coincide with the class of these functions whose graphs are definable in $\mathfrak{N}$ by $\Sigma_1$-formulas? In other words, my question is if it is correct to characterize recursive functions as these whose graphs are recursively enumerable.
 A: We give an informal proof that relies on Church's Thesis: we will give an algorithm for computing $f$, and not a recursive description of $f$ in any of the varous formal senses. 
Suppose the graph of the function $f(x_1,x_2, \dots,x_n)$ is definable by a $\Sigma_1$ formula $\varphi(x_1,x_2,\dots,x_n,y)$. The formula involves the existentially quantified variables $t_1,\dots, t_m$. When we remove the existential quantifiers, we end up with a formula $\psi(t_1,t_2,\dots,t_m,x_1,x_2,\dots,x_n,y)$ with only bounded quantifiers. Thus for any natural numbers $c_1,c_2,\dots,c_m, a_1,a_2,\dots,a_n,b)$ we can mechanically verify whether $\psi(c_1,c_2,\dots,c_m, a_1,a_2,\dots,a_n,b)$ is true in $\mathbb{N}$. 
Line up the $m$-tuples of natural numbers as $\overline{V}_0,\overline{V}_1,\overline{V}_2,\dots$, using one of the standard pairing functions. Given any natural numbers $a_1,a_2,\dots,a_n, b$, we can verify whether there exist integers 
$c_1,c_2,\dots,c_m$ such that $\psi(c_1,c_2,\dots,c_m, a_1,a_2,\dots,a_n,b)$ is true in $\mathbb{N}$ by checking in turn whether $\psi(\overline{V}_0,a_1,a_2,\dots, a_n,b)$ is true, whether  $\psi(\overline{V}_1,a_1,a_2,\dots, a_n,b)$ is true, and so on. 
The procedure is guaranteed to terminate, so we have produced an algorithm for computing the representing predicate $R(x_1,x_2,\dots,x_n,y)$ of the function $f$. It follows that $R(x_1,x_2,\dots,x_n,y)$ is recursive. Indeed if we carry out the details we can show that $R(x_1,x_2,\dots,x_n,y)$ is primitive recursive. 
The relation $R(x_1,x_2,\dots,x_n,y)$ is functional: for any $a_1,a_2,\dots,a_n$ there exists a unique $b$ such that $R(a_1,a_2,\dots,a_n,b)$. Since 
$$f(x_1,x_2,\dots,x_n)=\mu y R(x_1,x_2,\dots, x_n,y),$$
$f$ is (general) recursive. 
For the other direction, we need to verify that the graph of every recursive function is definable by a $\Sigma_1$ formula. This is an immediate consequence of the fact that every r.e. predicate is so definable.   
