---
tag: 7RP93F2W47
kind: definition
name: Gödel numbering
msc: [03F40]
defines: MFJXPAF0R0
uses: [HYJ10AF6RT, KZSB5E471K, PPGD5KW8JC]
sources:
  - url: https://en.wikipedia.org/wiki/Gödel_numbering
---

## Definition

Let $\Sigma$ be a countable alphabet whose symbols are listed effectively, and let $\Sigma^*$ be the set of finite strings over $\Sigma$.
A *Gödel numbering* of $\Sigma^*$ is a map $\ulcorner \cdot \urcorner \colon \Sigma^* \to \N$ such that:

1. $\ulcorner \cdot \urcorner$ is injective;
2. $\ulcorner \cdot \urcorner$ is computable;
3. the set of codes $\set{\ulcorner w \urcorner : w \in \Sigma^*}$ is a [[computable set|PPGD5KW8JC]], and the inverse map from codes to strings is computable.

For a formal language, a Gödel numbering of its [[formulas|HYJ10AF6RT]] or proofs is the restriction of a Gödel numbering of its strings of symbols.

## Remarks

Example: give the symbols injective codes $c(s) \ge 1$, and let $p_1 = 2, p_2 = 3, p_3 = 5, \ldots$ be the primes.
Set $\ulcorner s_1 s_2 \cdots s_n \urcorner = p_1^{c(s_1)} p_2^{c(s_2)} \cdots p_n^{c(s_n)}$.
By unique factorization the map is injective, and the exponents of a number can be found by trial division, so all three clauses hold.

Non-example: the map that sends each string to its length is computable but fails clause 1, since different strings of the same length get the same number.

The code of a formula $\varphi$ is written $\ulcorner \varphi \urcorner$, and in a theory of arithmetic its numeral is also written $\ulcorner \varphi \urcorner$.
Any two Gödel numberings are related by a computable bijection between their sets of codes.