ラムダ計算の文法に着目すれば、ラムダ計算は一つのゲーデル数で表すことができることを示す。
例えば、λx.xというラムダ式があって、次のように文字ごとに自然数を割り振っていこう。ただし、空白は無視できるものとする。
"λ" - 1
"x" - 2
"." - 3
"(" - 4
")" - 5
このとき、タプルa, bを<a, b>という形で書けるのだとすると、λx.xは次のように書ける。
<<<λ, x>, .>, x> = <<<1, 2>, 3>, 2>
このタプルを、次のゲーデル関数の一種である関数Gを使って、一つのゲーデル数に変換させる。
G(x, y) = ( (x+y) * (x+y+1) / 2) + x + 1)
すなわち、G(G(G(1, 2), 3), 2)を計算すると、一つのゲーデル数が得られる。こうして得られたゲーデル数集合をゲーデル数型Geとみなす
さて、つぎのような形無しラムダ計算とベータ簡約(->β)を与える。
(λx.x) λy.y ->β λy.y
このベータ簡約を次のような単純な型付きラムダ計算へと変換する（ただし、Ge はゲーデル数型とする）。
λω.λy.y ( (λx.x) λy.y): Ge -> Ge
しかるに、ゲーデル数の定義から、次のようなことが言える。
任意の二つの形無しラムダ計算A, Bによるβ簡約（A ->β B)から、ゲーデル数型の関数型（Ge -> Ge)が型付けできる単純な型付きラムダ（ (λω.B) A: Ge->Ge)へと変換できる (1.0)
次に、β正規形を持たないラムダ計算について考えてみる。不動点コンビネータであるYコンビネータにYコンビネータを関数適用させると、すなわち、Y Y ->β Y (Y Y) は、(1.0)より、
( λω.Y (Y Y) ) (Y Y): Ge -> Ge
さらに、最左評価戦略を用いて、Y Yを繰り返し次のようにベータ簡約できる。
Y Y ->β Y (Y Y)
->β (Y Y) (Y (Y Y))
->β (Y (Y Y)) (Y (Y Y))
Yコンビネータ自体にも自然数を割り振ると、(Y Y) (Y (Y Y))の式にも、(Y (Y Y)) (Y (Y Y))の式にも、両方とも関数Gを使って、一つのゲーデル数を求めることができる。そのため、結局、(1.0)より、
(λω.(Y Y) (Y (Y Y))) ( λω.Y (Y Y) ) (Y Y): (Ge -> Ge) -> Ge
(λω. (Y (Y Y)) (Y (Y Y))) (λω.(Y Y) (Y (Y Y))) ( λω.Y (Y Y) ) (Y Y):( (Ge -> Ge) -> Ge) -> Ge)
こうして見ていくと、Y Yのベータ簡約を繰り返したとき、その型付けは、ゲーデル数型を要素としたnタプル(n項組)である。例を挙げる。
(Ge -> Ge) -> Ge
( (Ge -> Ge) -> Ge) -> Ge)
<<Ge, Ge>, Ge>
<<<Ge, Ge>, Ge>, Ge>
このnタプルは、直積（カルテシアン積）である。また、nタプル二つとブール代数とを組み合わせて、べき集合モデルを作ることができる
