ゲーデル数
ゲーデル数化は一意ではなく、ゲーデル数を使った証明では様々な定義方法が存在する。
K 個の基本シンボルがあるとする。各基本シンボルと基数 K の位取り記数法の数字との写像(ここでは h と名づける)によって別のゲーデル数化を構築する。すると、n 個のシンボルからなる文字列で構成される数式 s 1 s 2 s 3 ... s n {\displaystyle s_{1}s_{2}s_{3}\dots s_{n}} は次の数に写像される。
h ( s 1 ) × K ( n − 1 ) + h ( s 2 ) × K ( n − 2 ) + ⋯ + h ( s n − 1 ) × K 1 + h ( s n ) × K 0 {\displaystyle h(s_{1})\times K^{(n-1)}+h(s_{2})\times K^{(n-2)}+\cdots +h(s_{n-1})\times K^{1}+h(s_{n})\times K^{0}}
ゲーデル数(ゲーデルすう、英: Gödel number)は、数理論理学において何らかの形式言語のそれぞれの記号や論理式に一意に割り振られる自然数である。クルト・ゲーデルが不完全性定理の証明に用いたことから、このように呼ばれている。また、ゲーデル数を割り振ることをゲーデル数化(英: Gödel numbering)と呼ぶ。
ゲーデル数のアイデアを暗に使っている例としては、コンピュータにおけるエンコードが挙げられる。 コンピュータでは何でも0と1で表し、「apple」のような文字列も0と1による数字で表す。 ゲーデル数化とは、このように文字列に数字を対応させる事を指す。
ゲーデル数化は、数式におけるシンボルに数を割り当てる符号化の一種でもあり、それによって生成された自然数の列が文字列を表現する。この自然数の列をさらに1つの自然数で表現することもでき、自然数についての形式的算術理論を適用可能となる。
ゲーデルの論文が発表された1931年以来、ゲーデル数はより広範囲な様々な数学的オブジェクトに自然数を割り振るのに使われるようになっていった。