All decidable predicates have corresponding statements in a formal language? [closed]

My book states the following theorem with no proof. Can anyone give an outline of the proof, or an explanation of how the formal statement is to be constructed?

Theorem:

Suppose that $M(x_1,...,x_n)$ is a decidable predicate. Then it is possible to construct a statement $σ(x_1,...,x_n)$ of $L$ [formal language of arithmetic] that is a formal counterpart of $M(x_1,...,x_n)$ in the following sense: for any $a_1,...,a_n ∈ ℕ$,

$M(a_1,...,a_n)$ holds iff $σ(a_1,...,a_n)$ is true.

• What is $L$? $\quad$ May 1, 2013 at 3:54
• L is the formal language of arithmetic with alphabet {0,1,+,×,=,¬,∧,∨,⇒,∃,∀,x,y,z,...} May 1, 2013 at 4:11
• In short one needs to create a sentence $\varphi(e,s,x,a_1,\ldots,a_n)$ that can be interpreted as "when a computer runs program $e$ it will have state $s$ on input $a_1, \ldots, a_n$ and output $x$". Then let $\sigma(a_1,\ldots,a_n) = \exists s\ \varphi(e,s,1,a_1\ldots,a_n)$ where $e$ is the program which decides $M$. (The trick it coding all this into arithmetic. That was a big part of Godel's First Incompleteness Theorem. Of course, they didn't have computers then...or Turing machines.) May 1, 2013 at 5:15
• I voted to close, because this is answered in standard textbooks. The details depend, of course, on which of the many equivalent definitions of computability one uses. My preference is "representability in Shoenfield's theory $N$ (a variant of Robinson's $Q$)", which trivializes the present question (but of course requires nontrivial work to be done elsewhere in the basics of computability theory). May 1, 2013 at 12:38