Can we find a formula defining a recursively enumerable set? By Post's Theorem we know that a set $A\subseteq\mathbf{N}$ is recursively enumerable iff it is definable by a $\Sigma_1$-formula, i.e. there exists a $\Sigma_1$-formula $\varphi(x)$ with $x$ free such that for every number $n$:
\[
n\in A\longleftrightarrow \mathfrak{N}\vDash\varphi(\overline{n})
\]
where $\mathfrak{N}$ is the standard model of the first-order language of Peano Arithmetic.
I have the following question: given a r.e. set $A$ can we always find a $\Sigma_1$-formula defining it?
 A: The definition of a recursive enumerable set is that it is the domain of some partial recursive function. 
There is a recursive primitive function $\psi$, such that $\psi(n,t,x)=0$ if and only if $\phi_n(x)$ (the recursive function $n$ on entry $x$) halts in less than $t$ steps, else $\psi(n,t,x)=1$. Any recursive primitive function can be defined by a $\Delta_0$-formula. Hence
$$\phi_n(x)\mbox{ halts } \Leftrightarrow \exists t\; \psi(n,t,x)=0$$
The existence of $\psi$ is a consequence of Kleene T-predicate
A: The answer to this question is that it depends on how we are "given" the r.e. set $A$. In most situations, the answer is yes. For example, if we are given a Turing machine (or a C++ program or anything like that) to list all the elements of $A$, then yes, we can convert that into a $\Sigma^1_1$ definition of $A$. The same holds if we're given a Turing machine (or ...) that halts on any input $x$ iff $x\in A$ (as in Xoff's answer). The same goes if we're given a formula weakly representing $A$ in Peano Arithmetic (or in ZFC or in Robinson's Q or ...).  But not if we're given $A$ by just a black box for deciding membership in $A$ (plus a promise that it is r.e.). And not if we're just given a definition of $A$ in the language of PA (or ZFC or ...) (plus again a promise that it's r.e.).
A: By the axiom of choice there is a function that maps each r.e. set to one of its definitions. We can 'find' the definition in that sense. This function cannot be too nice, however, because that would decide the extensional equivalence of two definitions.
Let $f$ be a function that maps each set to one of its definitions. For each arithmetical statement $p$ there is a set $\{n|p\}$. The equality of definitions $f(\{n|p\}) = f(\mathbb N)$ is way to decide if $p$ is true. G\"odel's incompleteness theorems say we can't do that.
