A Gödel numbering is an effective injective map $\ulcorner \cdot \urcorner$ from the set of expressions (terms, formulas, proofs) of a formal system to the natural numbers. Each expression $\varphi$ is assigned a unique Gödel number $\ulcorner \varphi \urcorner \in \mathbb{N}$, and the map is chosen so that basic syntactic operations (substitution, checking well-formedness) correspond to computable functions on Gödel numbers.

A function $f: \mathbb{N}^k \to \mathbb{N}$ is representable in a theory $T$ if there exists a formula $\varphi(x_1, \ldots, x_k, y)$ such that for all $n_1, \ldots, n_k \in \mathbb{N}$: $T \vdash \varphi(\underline{n_1}, \ldots, \underline{n_k}, \underline{f(n_1, \ldots, n_k)})$ and $T \vdash \forall y \, (\varphi(\underline{n_1}, \ldots, \underline{n_k}, y) \to y = \underline{f(n_1, \ldots, n_k)})$, where $\underline{m}$ denotes the numeral for $m$.

For any formula $\psi(x)$ with one free variable, there exists a sentence $\sigma$ such that $T \vdash \sigma \leftrightarrow \psi(\ulcorner \sigma \urcorner)$. Here $T$ is any theory extending Robinson arithmetic $Q$. The sentence $\sigma$ effectively "says of itself" that $\psi$ holds of its Gödel number.