ゲーデル数
ゲーデルはゲーデル数化を素因数分解に基づいて体系付けた。彼はまず、彼が使っている数式記法で出現する各基本シンボルにユニークな自然数を割り当てた。
シンボルの列である数式全体を符号化するため、ゲーデルは次のような体系を用いた。自然数の列 x 1 x 2 x 3 . . . x n {\displaystyle x_{1}x_{2}x_{3}...x_{n}} があるとき、ゲーデルによるその数列の符号化とは、小さいほうから n 個の素数を数列の各数値でべき乗したものの積となる。
e n c ( x 1 x 2 x 3 . . . x n ) = 2 x 1 ⋅ 3 x 2 ⋅ 5 x 3 ⋅ . . . ⋅ p n x n {\displaystyle \mathrm {enc} (x_{1}x_{2}x_{3}...x_{n})=2^{x_{1}}\cdot 3^{x_{2}}\cdot 5^{x_{3}}\cdot ...\cdot {p_{n}}^{x_{n}}}
算術の基本定理によれば、このようにして得られた値の素因数分解は一意に定まる。従って、ゲーデル数から元の数列を効率的に復元可能である。
ゲーデルはこの手法を2つのレベルで使った。第一に数式を構成するシンボル列を符号化するのに用い、第二に証明を表している数式列の符号化に用いた。これによって彼は、自然数に関する文と自然数の定理の立証性に関する文の間で対応を示した。
数列のゲーデル数化(Gödel numbering for sequences)には、より洗練され簡潔な方法が存在する。