ロッサーのからくり
ゲーデルの証明は、任意のそのような理論に対してある論理式formula_2が存在し、その意図された意味はformula_3はある論理式の自然数のコード (ゲーデル数) であり、formula_4はformula_1の公理からformula_3によってコード化された論理式の証明へのゲーデル数であることを示す (以降本記事では、数formula_3とformula_3によってコード化された論理式を区別せず、論理式formula_9のコードである数をformula_10で表す)。加えて、論理式formula_11をformula_12と定義する。これはformula_1から証明可能な論理式の集合を定義することを意図している。