ラムダ計算
2つのラムダ式を入力とし、それらが同値であるかどうかを判定するアルゴリズムは存在しない。これは決定不可能性が示された歴史的に最初の問題である。ここで使われる「アルゴリズム」という言葉も、もちろんきちんと定義されなければならない。チャーチは自身の証明の中で帰納的関数をその定義に用いたが、現在ではこれは適切なその他のアルゴリズムの定義と等価であることが知られている。
チャーチの証明ではこの問題を、あたえられたラムダ式に正規形が存在するかどうかという問題に帰している。正規形とは、それ以上簡約のできない同値なラムダ式のことである。チャーチの証明ではまず、この問題が決定可能である、つまり、ラムダ式で表現可能であると仮定する。クリーネによる結果とゲーデル数のラムダ式表現を用いることによってチャーチは、対角線論法によりパラドキシカルなラムダ式 e を構成した。この e を、それ自身を表すゲーデル数に適用すると矛盾が導かれる。
詳しくいえば次のようである。まず X {\displaystyle X} を正規形の存在性を判定するラムダ式とする。 A {\displaystyle A} を2つのラムダ式のゲーデル数から、それらを適用してできるラムダ式を計算する関数を表すラムダ式、 N {\displaystyle N} を自然数からそれを表すラムダ式の表現のゲーデル数を求める関数を表すラムダ式とする。すなわち、