コルモゴロフ複雑性
ここで次のようなプログラムを考えよう。
任意の n について、このプログラムは形式体系S内のありとあらゆる証明を調べ上げて、K(s)≧L(但しL ≧ n )を満たす文字列と証明を探し出そうとする。主張(X)によりこのプログラムは必ず停止する。このプログラムの長さを U としよう。 このとき、ある整数 n0 があって、U + log2(n0) + C < n0 を満たす。ここで C は、次のプログラムがGenerateProvablyComplexString()を呼び出す前後の固定的な長さである。
プログラム GenerateProvablyParadoxicalString() は文字列 s を出力するが、このとき L が存在して K(s)≧L(但し L ≧ n0)を満たし、S内でこれを形式的に証明できる。特に K(s)≧n0 は真である。ところが、s は長さが U+log2(n0)+C であるプログラムでも生成できるので、その複雑性は n0 よりも小さい。これは矛盾である。よって主張(X)は成り立たないことが証明された。
同様のアイディアはチャイティンの定数の性質を証明する際にも使われている。