Godel Encoding

A Godel encoding of a formal syntax $S$ is an computable injective map:

$$┌-┐:S\rightarrowtail \mathbb{N}$$

that represents expressions, derivations, or programs as natural numbers. It is chosen so that relevant syntactic operations and predicates become computable, usually primitive recursive.