ゲーデル数
ある形式理論のゲーデル数化が確立されると、その理論の各推論規則は自然数についての関数として表される。f がゲーデル写像で、論理式 A と B から推論規則 r によって数式 C が得られるとする。
A , B ⊢ r C {\displaystyle A,B\vdash _{r}C\ }
すると、次を満たす自然数の数論的関数 gr が存在するはずである。
g r ( f ( A ) , f ( B ) ) = f ( C ) {\displaystyle g_{r}(f(A),f(B))=f(C)\ }
これはゲーデルの用いたナンバリングにおいては真であり、符号化された論理式がそのゲーデル数から算術的に復元可能な他のナンバリング方式でも成り立つ。
従って、ペアノの公理のような数とその間の算術的関係に関する文を作ることができる形式理論においては、ゲーデル数化を使えば間接的にその理論自体に関する文を作ることができる。このような技法によってゲーデルは形式体系の属性の無矛盾性と完全性に関する結果の証明を行った。